Theory Phi_Semantics_Framework

section ‹Modular Formalization of Program Semantics›

text ‹Using the Virtual Datatype, Resource Space, Fiction Space, now in this section it is
  feasible to formalize the semantics of programs modularly and extensibly.

The section first presents an empty formalization (framework) of computation states
consisting of empty types, empty values, empty resources, and empty fictions.
It serves for future formalization of any specific program semantics.

Then on this empty formalization of computation states.
The framework formalizes computations using state-error-exception monad,
supporting most of control flows and therefore most of (imperative) languages.
›

theory Phi_Semantics_Framework
  imports Resource_Space Virtual_Datatype.Virtual_Datatype Debt_Axiom.Debt_Axiom
          "HOL-Library.Monad_Syntax"
  keywords "resource_space" :: thy_goal
  abbrevs "<throws>" = "𝗍𝗁𝗋𝗈𝗐𝗌"
    and "<proc>" = "𝗉𝗋𝗈𝖼"
begin


text ‹The section provides the initial empty semantics of computation states
  serving as the base for any further substantial formalization.›

subsection ‹Type›

unspecified_type TY

debt_axiomatization 𝗉𝗈𝗂𝗌𝗈𝗇 :: TY

subsection ‹Value›

unspecified_type VAL
instance VAL :: sep_magma ..

text ‹The semantic value is a separation magma. It is nothing related to the semantic
  or the specification framework themselves but just to be helpful in some situation for
  formalization of some semantics such as that in aggregate the separation can represent
  concatenation of fields.›


subsubsection ‹Deep Representation of Aggregated Values›

class VAL =
  fixes to_val   :: ‹'a ⇒ VAL›
    and from_val :: ‹VAL ⇒ 'a›
  assumes from_to_val[simp]: ‹from_val (to_val x) = x›

class VALs =
  fixes to_vals    :: ‹'a ⇒ VAL list›
    and from_vals  :: ‹VAL list ⇒ 'a›
  assumes from_to_vals[simp]: ‹from_vals (to_vals x) = x›

class FIX_ARITY_VALs = VALs +
  fixes vals_arity :: ‹'a itself ⇒ nat›
  assumes length_to_vals[simp]: ‹length (to_vals x) = vals_arity TYPE('a)›

instantiation VAL :: VAL begin
definition to_val_VAL :: ‹VAL ⇒ VAL› where ‹to_val_VAL = id›
definition from_val_VAL :: ‹VAL ⇒ VAL› where ‹from_val_VAL = id›
instance by standard (simp add: to_val_VAL_def from_val_VAL_def)
end

instantiation unit :: FIX_ARITY_VALs begin
definition to_vals_unit    :: ‹unit ⇒ VAL list›   where ‹to_vals_unit v  = []›
definition from_vals_unit  :: ‹VAL list ⇒ unit›   where ‹from_vals_unit _ = ()›
definition vals_arity_unit :: ‹unit itself ⇒ nat› where ‹vals_arity_unit _ = 0›
instance by standard (simp_all add: vals_arity_unit_def to_vals_unit_def)
end

instantiation VAL :: FIX_ARITY_VALs begin
definition to_vals_VAL    :: ‹VAL ⇒ VAL list›   where ‹to_vals_VAL v  = [v]›
definition from_vals_VAL  :: ‹VAL list ⇒ VAL›   where ‹from_vals_VAL  = hd›
definition vals_arity_VAL :: ‹VAL itself ⇒ nat› where ‹vals_arity_VAL _ = 1›
instance by standard (simp_all add: to_vals_VAL_def from_vals_VAL_def vals_arity_VAL_def)
end

instantiation prod :: (FIX_ARITY_VALs, FIX_ARITY_VALs) FIX_ARITY_VALs begin

definition to_vals_prod    :: ‹'a × 'b ⇒ VAL list›
  where ‹to_vals_prod v = (case v of (v1,v2) ⇒ to_vals v1 @ to_vals v2)›
definition from_vals_prod  :: ‹VAL list ⇒ 'a × 'b›
  where ‹from_vals_prod vs = (@v. to_vals v = vs)›
definition vals_arity_prod :: ‹('a × 'b) itself ⇒ nat›
  where ‹vals_arity_prod _ = vals_arity TYPE('a) + vals_arity TYPE('b)›

instance apply standard
  apply (clarsimp simp add: to_vals_prod_def from_vals_prod_def)
  apply (smt (verit) Eps_case_prod_eq Eps_cong append_eq_append_conv from_to_vals length_to_vals split_def)
  by (clarsimp simp add: to_vals_prod_def vals_arity_prod_def)

end

instantiation list :: (VAL) VALs begin
definition to_vals_list :: ‹'a list ⇒ VAL list› where ‹to_vals_list = map to_val›
definition from_vals_list :: ‹VAL list ⇒ 'a list› where ‹from_vals_list = map from_val›
instance by standard (induct_tac x; simp add: to_vals_list_def from_vals_list_def)
end



subsection ‹Resource›

unspecified_type RES
unspecified_type RES_N
type_synonym resource = ‹RES_N ⇒ RES›
type_synonym 'T resource_entry = "(RES_N, RES, 'T) Resource_Space.kind"

setup ‹Sign.mandatory_path "RES"›

consts DOMAIN :: ‹RES_N ⇒ RES sep_homo_set›

debt_axiomatization sort: ‹OFCLASS(RES, sep_algebra_class)›

setup ‹Sign.parent_path›

instance RES :: sep_algebra using RES.sort .

setup ‹Sign.mandatory_path "RES"›

debt_axiomatization ex_RES_not_1: ‹∃r::RES. r ≠ 1›

lemma ex_two_distinct:
  ‹∃r1 r2 :: resource. r1 ≠ r2›
  unfolding fun_eq_iff apply simp
  by (meson RES.ex_RES_not_1)

setup ‹Sign.parent_path›

instantiation RES :: sep_carrier_1 begin
definition mul_carrier_RES :: ‹RES ⇒ bool› where ‹mul_carrier_RES = (λ_. True)›
  ― ‹As a type specially defined to represent the representation of resources, it is noisy-free.›
instance by (standard; simp add: mul_carrier_RES_def)
end

interpretation RES: "resource_space" RES.DOMAIN .

ML_file ‹resource_space_more.ML›
 
ML ‹Resource_Space.define_command \<^command_keyword>‹resource_space› "extend resource semantics"›


subsection ‹Abnormal›

unspecified_type ABNM


subsection ‹All-in-One Semantics›

debt_axiomatization Well_Type :: ‹TY ⇒ VAL set›
  where Well_Type_disjoint: ‹ta ≠ tb ⟹ Well_Type ta ∩ Well_Type tb = {}›
    and Well_Type_poison[simp]: ‹Well_Type 𝗉𝗈𝗂𝗌𝗈𝗇 = {}›

debt_axiomatization Can_EqCompare :: ‹resource ⇒ VAL ⇒ VAL ⇒ bool›
  where can_eqcmp_sym: "Can_EqCompare res A B ⟷ Can_EqCompare res B A"

consts EqCompare :: ‹VAL ⇒ VAL ⇒ bool›
(*  and   eqcmp_refl:  "EqCompare A A"
    and   eqcmp_sym:   "EqCompare A B ⟷ EqCompare B A"
    and   eqcmp_trans: "EqCompare A B ⟹ EqCompare B C ⟹ EqCompare A C" *)

debt_axiomatization Zero :: ‹TY ⇒ VAL option›
  where zero_well_typ: "pred_option (λv. v ∈ Well_Type T) (Zero T)"

definition has_Zero :: ‹TY ⇒ bool›
  where ‹has_Zero T ⟷ Zero T ≠ None›

lemma Zero_𝗉𝗈𝗂𝗌𝗈𝗇[simp]:
  ‹ Zero 𝗉𝗈𝗂𝗌𝗈𝗇 = None ›
  by (metis Well_Type_poison empty_iff not_None_eq option.pred_inject(2) zero_well_typ)

lemma has_Zero_𝗉𝗈𝗂𝗌𝗈𝗇[simp]:
  ‹ ¬ has_Zero 𝗉𝗈𝗂𝗌𝗈𝗇 ›
  unfolding has_Zero_def
  by simp

lemma Well_Type_unique:
  ‹v ∈ Well_Type ta ⟹ v ∈ Well_Type tb ⟹ ta = tb›
  using Well_Type_disjoint by blast

(*
abbreviation ‹Valid_Type T ≡ Satisfiable (Well_Type T)›*)


subsection ‹Formalization of Computation›

subsubsection ‹Explicit Annotation of Semantic Arguments and Returns›

text ‹Arguments and Returns are wrapped by φarg type.
  It helps the programming framework and syntax parser to recognize which one is an argument
  or a return, among values that may be used for other purposes of specification.›

datatype 'a φarg = φarg (dest: 'a)
hide_const (open) dest


definition unreachable :: ‹'a::VALs› where ‹unreachable = undefined›

lemma φarg_forall: ‹All P ⟷ (∀x. P (φarg x))› by (metis φarg.exhaust)
lemma φarg_exists: ‹Ex P  ⟷ (∃x. P (φarg x))› by (metis φarg.exhaust)
lemma φarg_All: ‹(⋀x. PROP P x) ≡ (⋀x. PROP P (φarg x))›
proof
  fix x :: 'a assume A: ‹(⋀x. PROP P x)› then show ‹PROP P (φarg x)› .
next
  fix x :: ‹'a φarg› assume A: ‹⋀x. PROP P (φarg x)›
  from ‹PROP P (φarg (φarg.dest x))› show "PROP P x" by simp
qed


definition ‹φV_none = φarg ()›
definition φV_pair ("_❙, _" [11,10] 10) where ‹φV_pair x y = φarg (φarg.dest x, φarg.dest y)›
definition ‹φV_case_prod f x ≡ case x of φarg (a,b) ⇒ f (φarg a) (φarg b)›
definition ‹φV_fst x = map_φarg fst x›
definition ‹φV_snd x = map_φarg snd x›
abbreviation ‹φV_nil ≡ φarg []›
definition ‹φV_cons h l = φarg (φarg.dest h # φarg.dest l)›
definition ‹φV_hd l = φarg (hd (φarg.dest l))›
definition ‹φV_tl l = φarg (tl (φarg.dest l))›

lemma φV_simps[simp]:
  ‹φV_pair (φV_fst v) (φV_snd v) = v›
  ‹φV_fst (φV_pair u y) = u›
  ‹φV_snd (φV_pair x u) = u›
  ‹φV_fst (φarg (xa,xb)) = φarg xa›
  ‹φV_snd (φarg (xa,xb)) = φarg xb›
  ‹φV_cons (φarg h) (φarg l) = φarg (h#l)›
  ‹φV_hd (φV_cons hv lv) = hv›
  ‹φV_tl (φV_cons hv lv) = lv›
  ‹φV_case_prod f (φV_pair a b) = f a b›
  ‹φV_case_prod f = (λv. f (φV_fst v) (φV_snd v))›
(*  ‹φV_case_prod (λa b. f2 (φV_pair a b)) = f2›
  ‹φV_case_prod (λa. φV_case_prod (λb c. f3 (φV_pair a (φV_pair b c)))) = f3›
  ‹φV_case_prod (λa. φV_case_prod (λb. φV_case_prod (λc d. f4 (φV_pair a (φV_pair b (φV_pair c d)))))) = f4› *)
  unfolding φV_pair_def φV_fst_def φV_snd_def φV_cons_def φV_hd_def φV_tl_def φV_case_prod_def
    apply (cases v, simp)
    apply (cases v, simp)
    apply (cases v, simp)
    apply simp apply simp apply simp
    apply simp apply simp apply simp
    apply (simp add: fun_eq_iff φarg_forall) .


paragraph ‹More auxiliary properties›

lemma split_paired_All_φarg:
  "(∀x. P x) ⟷ (∀a b. P (φV_pair a b))"
  by (metis φV_simps(1))

lemma split_paired_Ex_φarg:
  "(∃x. P x) ⟷ (∃a b. P (φV_pair a b))"
  by (metis φV_simps(1))

lemma split_paired_all_φarg:
  "(⋀x. PROP P x) ≡ (⋀a b. PROP P (φV_pair a b))"
  unfolding φarg_All φV_pair_def split_paired_all by simp

lemma split_paired_All_φarg_unit:
  "(∀x. P x) ⟷ P φV_none"
  by (simp add: φarg_forall φV_none_def)

lemma split_paired_Ex_φarg_unit:
  "(∃x. P x) ⟷ P φV_none"
  by (simp add: φarg_exists φV_none_def)

lemma split_paired_all_φarg_unit:
  "(⋀x. PROP P x) ≡ PROP P φV_none"
  unfolding φarg_All φV_pair_def split_paired_all φV_none_def by simp




(* datatype unreachable = unreachable

instantiation unreachable :: VALs begin
definition to_vals_unreachable :: ‹unreachable ⇒ VAL list› where ‹to_vals_unreachable _ = undefined›
definition from_vals_unreachable :: ‹VAL list ⇒ unreachable› where ‹from_vals_unreachable _ = unreachable›
definition vals_arity_unreachable :: ‹unreachable itself ⇒ nat›
  where ‹vals_arity_unreachable _ = length (undefined::VAL list)›

instance apply standard
  apply (simp_all add: to_vals_unreachable_def from_vals_unreachable_def vals_arity_unreachable_def)
  by (metis unreachable.exhaust)
end
*)

paragraph ‹Syntax›

notation (do_notation) φV_fst ("_⇩'(⇩1⇩')")
                   and φV_snd ("_⇩'(⇩2⇩')")


subsubsection ‹Monadic Formalization›

text ‹‹('ret,'ex,'RES_N,'RES) state› represents any potential returning state of a program.

▪ ‹Success v r› represents a successful returning state with return value ‹v› and resulted resource
  state ‹r›.

▪ ‹Abnormal v r› represents the computation throws an exception of value ‹v›, at the
  moment when the state of the resources is ‹r›.

▪ ‹NonTerm› represents the execution does not terminate.

▪ ‹Invalid› represents the computation is invalid.
  It defines the domain of valid programs, which are the ones that never never generates
  an execution path that results in ‹Invalid›.

▪ ‹Assumption_Violated› represents the computation that results in an execution path that is not
  considered or modelled by the trust base.
  For example, the formalization of the allocation instruction may assume the size of the object
  to be allocated is always less than the size of the address space (e.g., ‹2⇧3⇧2› bytes).
  In another case users may assume the size of their objects is representable by ‹𝗌𝗂𝗓𝖾_𝗍›.
  ‹Assumption_Violated› enables an easy way for semantic assumptions, e.g., to assume ‹P›,
  \[ ‹if P then do-something else return Assumption_Violated› \]
  ‹Assumption_Violated› is admitted by any post-condition, i.e.,
  \[ {⊤} return Assumption_Violated {⊥} \]
  Computations returning ‹Assumption_Violated› are trusted by the trust base.
  This additional increment in the trust base is controllable, because whether and where to
  use the ‹Assumption_Violated›, this is determined by the formalization of instruction semantics,
  which belongs to the trust base already.
›

declare [ [typedef_overloaded] ]

datatype 'ret comp =
      Success ‹'ret φarg› (resource: resource)
    | Abnormal ‹ABNM› (resource: resource)
    | Invalid (*TODO: rename to Stuck*)
    | AssumptionBroken
    | NonTerm (*TODO: rename to NonTerminating*)

declare [ [typedef_overloaded = false] ]


lemma split_comp_All:
  ‹All P ⟷ (∀v r. P (Success v r)) ∧ (∀v r. P (Abnormal v r)) ∧ P Invalid
                ∧ P AssumptionBroken ∧ P NonTerm›
  by (metis comp.exhaust)

lemma split_comp_Ex:
  ‹Ex P ⟷ (∃v r. P (Success v r)) ∨ (∃v r. P (Abnormal v r)) ∨ P Invalid
                ∨ P AssumptionBroken ∨ P NonTerm›
  by (metis comp.exhaust)

hide_const(open) resource

declare comp.split[split]

text ‹Procedure is the basic building block of a program on the semantics formalization.
It represents a segment of a program, which is defined inductively,

▪ Any instruction instantiated by any arguments is a procedure
▪ Any lambda abstraction of a procedure is a procedure
▪ Sequential composition ‹f ⤜ g› is a procedure iff ‹f, g› are procedures.
▪ A control flow combinator combines several procedures into a procedure

Control flow combinator does not include the sequential composition combinator ‹⤜›.

Any function, routine, or sub-routine in high level languages is a procedure but a procedure
does not necessarily corresponds to them nor any basic block in assemble representations.

A procedure is not required to be a valid program necessarily.
Procedure is only a syntax structure and the semantics of invalid operations or programs
is expressed by returning ‹Invalid›.

%% Not Required:
% ❙‹Normal Form of Procedures› (NFP) is defined by the following BNF,
% \begin{align}
% ‹NFP p› \Coloneqq & ‹return v›
%                 | & ‹i ⤜ p›   & &\text{for ‹i ∈ Instructions›} \\
%                 | & ‹λx. p›
%                 | & ‹c p p ⋯ p› & &\text{‹c› is a control flow combinator.}
% \end{align}
% It essentially says any lambda abstraction occurring in the left hand side of a sequential
% composition ‹(λx. f) ⤜ g› can be expanded to the whole term, i.e., ‹λx. (f ⤜ g)›.
% And any body of the control flows is also in NFP.
% It is obvious the NFP can express equivalently any procedure.
% NFP is used later in CoP to construct any procedure.

% TODO: value annotation and slightly-shallow representation.
 ›

type_synonym 'ret proc = "resource ⇒ 'ret comp set"
type_synonym ('arg,'ret) proc' = "'arg φarg ⇒ 'ret proc"

definition bind :: "'a proc ⇒ ('a,'b) proc' ⇒ 'b proc"
  where "bind f g = (λres. ⋃((λy. case y of Success v x ⇒ g v x
                                           | Abnormal v x ⇒ {Abnormal v x}
                                           | Invalid ⇒ {Invalid}
                                           | NonTerm ⇒ {NonTerm}
                                           | AssumptionBroken ⇒ {AssumptionBroken}
                              ) ` f res))" 


adhoc_overloading Monad_Syntax.bind bind

definition ‹det_lift f x = {f x}›

definition Return ("𝗋𝖾𝗍𝗎𝗋𝗇")
  where ‹Return = det_lift o Success›

definition Nondet :: ‹'ret proc ⇒ 'ret proc ⇒ 'ret proc›
  where ‹Nondet f g = (λres. f res ∪ g res)›

term ‹f ⤜ Return›
term ‹do { x <- (f::'a proc); Return xaa }›

lemma proc_bind_SKIP'[simp]:
  "f ⤜ Return ≡ f"
  "Return any ⤜ ff ≡ ff any"
  "(g ⪢ Return any) ⪢ f ≡ g ⪢ f"
  "(λv. Return v ⤜ h) ≡ h"
  unfolding bind_def atomize_eq fun_eq_iff det_lift_def set_eq_iff Return_def
  by (clarsimp; metis comp.exhaust)+

lemma proc_bind_return_none[simp]:
  "f_nil ⪢ Return φV_none ≡ f_nil"
  for f_nil :: ‹unit proc›
  unfolding bind_def atomize_eq fun_eq_iff det_lift_def set_eq_iff Return_def φV_none_def
  apply (clarsimp)
  subgoal for x y
  apply rule
    apply clarsimp
    subgoal for z
      apply (cases z; simp add: φarg_All) .
  apply (rule bexI[where x=y]; clarsimp simp add: φarg_All) . .

lemmas proc_bind_SKIP[simp] =
  proc_bind_SKIP'[unfolded Return_def, simplified]
  proc_bind_return_none[unfolded Return_def, simplified]

lemma proc_bind_assoc[simp]:
  "((A ⤜ B) ⤜ C) = (A ⤜ (λx. B x ⤜ C))" for A :: ‹'a proc›
  unfolding bind_def fun_eq_iff det_lift_def set_eq_iff
  by clarsimp


definition Valid_Proc :: ‹'ret proc ⇒ bool›
  where ‹Valid_Proc f ⟷ (∀v s s'. Success v s' ∈ f s ∧ s ∈ RES.SPACE ⟶ s' ∈ RES.SPACE)
                             ∧ (∀e s s'. Abnormal e s' ∈ f s ∧ s ∈ RES.SPACE ⟶ s' ∈ RES.SPACE)›

lemma Valid_Proc_bind:
  ‹ Valid_Proc f
⟹ (⋀v. Valid_Proc (g v))
⟹ Valid_Proc (f ⤜ g)›
  unfolding Valid_Proc_def bind_def
  subgoal premises prems
    apply (clarsimp; rule; clarsimp)
    apply (case_tac x; simp add: Bex_def split_comp_Ex)
    using prems(1) prems(2) apply blast
    apply (case_tac x; simp add: Bex_def split_comp_Ex)
    using prems(1) prems(2) apply blast
    using prems(1) by blast .
  


end