Fomalization of AST (syntax and semantics) and general helper lemmas for AST-to-CFG phase validation

BoogieLang/BackedgeElim.thy

@@ -2,7 +2,7 @@ section \<open>A collection of lemmas, definitions and tactics that aid the cert
 CFG-to-DAG phase\<close>
 
 theory BackedgeElim
-imports Semantics Util TypeSafety "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools"
+imports Lang Semantics Util TypeSafety "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools"
 begin
 
 subsection \<open>State equality up to a set\<close>
@@ -597,7 +597,7 @@ proof -
   from cfg_dag_rel_havoc[OF Rel SameModH StateWt TyExists] obtain cs2A cs2B ns2' where
     "cs2 = cs2A@cs2B" and StateRel1:"nstate_same_on \<Lambda> ns1 ns2' {}" and A2Red1:"A,M,\<Lambda>,\<Gamma>,\<Omega> \<turnstile> \<langle>cs2A, Normal ns2\<rangle> [\<rightarrow>] Normal ns2'"
     and RelHavoc:"cfg_dag_rel c [] pre_invs post_invs cs1 cs2B"
-    by meson
+    by metis
 
   with StateWt2 have StateWtNs2':"state_well_typed A \<Lambda> \<Omega> ns2'" using cfg_dag_rel_no_calls_2 red_cmds_state_wt_preserve Rel
     by (metis list_all_append)
@@ -725,7 +725,7 @@ lemma dag_lemma_assms_subset:
   using nstate_same_on_subset
   by blast
 
-definition dag_lemma_conclusion :: "'a absval_ty_fun \<Rightarrow> proc_context \<Rightarrow> var_context \<Rightarrow> 
+definition dag_lemma_conclusion :: "'a absval_ty_fun \<Rightarrow> mbodyCFG proc_context \<Rightarrow> var_context \<Rightarrow> 
                    'a fun_interp \<Rightarrow> rtype_env \<Rightarrow> expr list \<Rightarrow>
                     cmd list \<Rightarrow> 'a nstate \<Rightarrow> 'a state \<Rightarrow> bool \<Rightarrow> bool"
   where "dag_lemma_conclusion A M \<Lambda> \<Gamma> \<Omega> post_invs cs2 ns2 s' c \<equiv>
@@ -1099,7 +1099,7 @@ next
         by blast
       from PostHolds show ?thesis 
         unfolding valid_configuration_def expr_all_sat_def      
-        by (metis "2"(3) finished_remains local.RedNormalReturn(1) local.RedNormalReturn(2) prod.inject relpowp_imp_rtranclp state.distinct(1) state.inject)
+        by (metis "2" (3) finished_remains local.RedNormalReturn(1) local.RedNormalReturn(2) prod.inject relpowp_imp_rtranclp state.distinct(1) state.inject)
   next
     case (RedFailure cs)
     then show ?thesis   
@@ -1115,7 +1115,7 @@ qed
 
 text \<open>The following lemma is a global block theorem helper lemma for the case where the block
 before the CFG-to-DAG phase has no successor (i.e., not a return block) and 
-he corresponding block B' after the CFG-to-DAG phase has one successor B''. B'' is the unique exit block
+the corresponding block B' after the CFG-to-DAG phase has one successor B''. B'' is the unique exit block
 generated by Boogie and the assertion of the postcondition is added to the end of B''.\<close>
 
 lemma cfg_dag_helper_return_2:
@@ -1212,7 +1212,7 @@ proof -
     RedCsA:"(A,M,\<Lambda>,\<Gamma>,\<Omega> \<turnstile> \<langle>csA,Normal ns2\<rangle> [\<rightarrow>] Normal ns2)" and
     InvsHold2:"list_all (expr_sat A \<Lambda> \<Gamma> \<Omega> ns2) post_invs"
     using cfg_dag_rel_post_invs[OF Rel refl refl refl BlockCorrect] InvsWt
-    by meson
+    by metis
   have InvsHold1:"list_all (expr_sat A \<Lambda> \<Gamma> \<Omega> ns1) post_invs" 
     apply (rule List.List.list.pred_mono_strong)
     apply (rule InvsHold2)
@@ -1303,7 +1303,7 @@ lemma cfg_dag_empty_propagate_helper:
 lemma strictly_smaller_helper: "j'' \<le> j' \<Longrightarrow> j = Suc j' \<Longrightarrow> j'' < j"
   by simp
 
-definition loop_ih :: "'a absval_ty_fun \<Rightarrow> proc_context \<Rightarrow> var_context \<Rightarrow> 
+definition loop_ih :: "'a absval_ty_fun \<Rightarrow> mbodyCFG proc_context \<Rightarrow> var_context \<Rightarrow> 
                    'a fun_interp \<Rightarrow> rtype_env \<Rightarrow> mbodyCFG \<Rightarrow> vname list \<Rightarrow> expr list \<Rightarrow> expr list \<Rightarrow>
                     'a nstate \<Rightarrow> 'a state \<Rightarrow> nat \<Rightarrow> nat + unit \<Rightarrow> nat \<Rightarrow> bool"
   where "loop_ih A M \<Lambda> \<Gamma> \<Omega> G H invs posts ns1 s' node_id  m' j\<equiv> 
@@ -1419,9 +1419,10 @@ lemma backedge_loop_head_helper:
 
 subsection \<open>Helper lemma for final end-to-end theorem\<close>
 
+
 lemma end_to_end_util:
   assumes AExpanded:"\<And> \<Gamma> m' s' ns M.
-          A,M,\<Lambda>,\<Gamma>,[],cfg_body  \<turnstile> (Inl n, Normal ns) -n\<rightarrow>* (m', s') \<Longrightarrow>
+           A,M,\<Lambda>,\<Gamma>,[],cfg_body  \<turnstile> (Inl n, Normal ns) -n\<rightarrow>* (m', s') \<Longrightarrow>
            (\<And> v. (closed ((type_of_val A) v))) \<Longrightarrow>
            (\<And> t. ((closed t) \<Longrightarrow> (\<exists> v. (((type_of_val A) v) = t)))) \<Longrightarrow>
            (fun_interp_wf A fun_decls \<Gamma>) \<Longrightarrow>
@@ -1442,12 +1443,12 @@ lemma end_to_end_util:
           "proc_ty_args proc = 0" and
           "n = entry cfg_body"
           (*"const_decls = prog_consts prog"*)
-  shows "proc_is_correct A fun_decls constants global_vars axioms proc"
+        shows "proc_is_correct A fun_decls constants global_vars axioms proc Semantics.proc_body_satisfies_spec"
 proof -
-  show "proc_is_correct A fun_decls constants global_vars axioms proc"
+  show "proc_is_correct A fun_decls constants global_vars axioms proc Semantics.proc_body_satisfies_spec"
   proof( (simp only: proc_is_correct.simps), subst ABody, simp split: option.split, (rule allI | rule impI)+,
          unfold proc_body_satisfies_spec_def,(rule allI | rule impI)+)  
-    fix \<Gamma> \<Omega> gs ls m' s'
+    fix \<Gamma> \<Omega> gs ls m' s' 
     assume Atyp:"(\<forall>t. closed t \<longrightarrow> (\<exists>v. type_of_val A v = t)) \<and> (\<forall>v. closed (type_of_val A v))" and
            FunWf:"fun_interp_wf A fun_decls \<Gamma>" and
            ARenv: "list_all closed \<Omega> \<and> length \<Omega> = proc_ty_args proc" and
@@ -1473,7 +1474,7 @@ proof -
                 apply (subst \<open>n = entry cfg_body\<close>)
                 apply (subst Contexteq)
       using Ared \<open>\<Omega> = []\<close>
-                apply fastforce
+               apply fastforce
               apply (simp add: Atyp)
              apply (simp add: Atyp)
             apply (simp add: FunWf)

BoogieLang/Lang.thy

@@ -93,31 +93,31 @@ CFG of a procedure body is represented by:
 
 text \<open>Procedure pre- and postconditions contain a boolean to indicate whether they are free (true) or 
       checked (false).\<close>
-record procedure =
+record 'struct_ty procedure =
   proc_ty_args :: nat
   proc_args :: vdecls
   proc_rets :: vdecls
   proc_modifs :: "vname list"
   proc_pres :: "(expr \<times> bool) list" 
   proc_posts :: "(expr \<times> bool) list"
-  proc_body :: "(vdecls \<times> mbodyCFG) option"
+  proc_body :: "(vdecls \<times> 'struct_ty) option"
 
-fun proc_checked_pres :: "procedure \<Rightarrow> expr list"
+fun proc_checked_pres :: "'struct_ty procedure \<Rightarrow> expr list"
   where "proc_checked_pres p = map fst (filter (\<lambda>x. \<not> snd(x)) (proc_pres p))"
 
-fun proc_free_pres :: "procedure \<Rightarrow> expr list"
+fun proc_free_pres :: "'struct_ty procedure \<Rightarrow> expr list"
   where "proc_free_pres p = map fst (filter (\<lambda>x. snd(x)) (proc_pres p))"
 
-fun proc_all_pres :: "procedure \<Rightarrow> expr list"
+fun proc_all_pres :: "'struct_ty procedure \<Rightarrow> expr list"
   where "proc_all_pres p = map fst (proc_pres p)"
 
-fun proc_checked_posts :: "procedure \<Rightarrow> expr list"
+fun proc_checked_posts :: "'struct_ty procedure \<Rightarrow> expr list"
   where "proc_checked_posts p = map fst (filter (\<lambda>x. \<not> snd(x)) (proc_posts p))"
 
-fun proc_all_posts :: "procedure \<Rightarrow> expr list"
+fun proc_all_posts :: "'struct_ty procedure \<Rightarrow> expr list"
   where "proc_all_posts p = map fst (proc_posts p)"
 
-fun proc_free_posts :: "procedure \<Rightarrow> expr list"
+fun proc_free_posts :: "'struct_ty procedure \<Rightarrow> expr list"
   where "proc_free_posts p = map fst (filter (\<lambda>x. snd(x)) (proc_posts p))"
 
 definition exprs_to_only_checked_spec :: "expr list \<Rightarrow> (expr \<times> bool) list"
@@ -134,18 +134,18 @@ lemma exprs_to_only_checked_spec_2: "es = map fst (filter (\<lambda>x. \<not> sn
   unfolding exprs_to_only_checked_spec_def
   by (induction es) auto
 
-type_synonym pdecl = "pname \<times> procedure"
+type_synonym 'struct_ty pdecl = "pname \<times> 'struct_ty procedure"
 
 text \<open>An axiom is a boolean expression that can refer to constants.\<close>
 type_synonym axiom = expr
 
-record prog =
+record 'struct_ty prog =
   prog_ty_constr :: tdecls 
   prog_funcs :: fdecls
   prog_consts :: vdecls
   prog_globals :: vdecls
   prog_axioms :: "axiom list"
-  prog_procs :: "pdecl list"
+  prog_procs :: "'struct_ty pdecl list"
 
 text \<open>Type declarations are ignored by the semantics (all possible types are taken into account, which
 is more general and the resulting semantics can be reduced to the case where one only quantifies over 

BoogieLang/Passification.thy

@@ -27,7 +27,7 @@ lemma dependent_ext:
   unfolding dependent_def
   by blast
 
-definition set_red_cmd :: "'a absval_ty_fun \<Rightarrow> proc_context \<Rightarrow> var_context \<Rightarrow> 'a fun_interp \<Rightarrow> rtype_env \<Rightarrow> cmd \<Rightarrow> 'a nstate set \<Rightarrow> 'a state set"
+definition set_red_cmd :: "'a absval_ty_fun \<Rightarrow> 'm proc_context \<Rightarrow> var_context \<Rightarrow> 'a fun_interp \<Rightarrow> rtype_env \<Rightarrow> cmd \<Rightarrow> 'a nstate set \<Rightarrow> 'a state set"
   where "set_red_cmd A M \<Lambda> \<Gamma> \<Omega> c N = {s. \<exists>n_s. n_s \<in> N \<and> A,M,\<Lambda>,\<Gamma>,\<Omega> \<turnstile> \<langle>c, Normal n_s\<rangle> \<rightarrow> s}"
 
 text \<open>\<^term>\<open>set_red_cmd\<close> lifts the command reduction to the reduction of a a set of input states \<close>
@@ -1201,7 +1201,7 @@ definition passive_block_conclusion
   where "passive_block_conclusion A M \<Lambda> \<Lambda>' \<Gamma> \<Omega> U0 D1 R R_old cs2 s' = 
   (s' \<noteq> Magic \<longrightarrow> (\<exists> U1 \<subseteq> U0. U1 \<noteq> {} \<and> dependent A \<Lambda>' \<Omega> U1 D1 \<and> passive_sim A M \<Lambda> \<Lambda>' \<Gamma> \<Omega> cs2 s' R R_old U1))"
 
-definition passive_lemma_assms :: "'a absval_ty_fun \<Rightarrow> proc_context \<Rightarrow> var_context \<Rightarrow> var_context \<Rightarrow> 
+definition passive_lemma_assms :: "'a absval_ty_fun \<Rightarrow> 'struct_ty proc_context \<Rightarrow> var_context \<Rightarrow> var_context \<Rightarrow> 
                    'a fun_interp \<Rightarrow> rtype_env \<Rightarrow> vname list \<Rightarrow> passive_rel \<Rightarrow> passive_rel \<Rightarrow> 
                   ('a nstate) set \<Rightarrow> vname set \<Rightarrow> 'a nstate \<Rightarrow> bool"
   where "passive_lemma_assms A M \<Lambda> \<Lambda>' \<Gamma> \<Omega> W R R_old U0 D0 ns = 
@@ -1244,7 +1244,7 @@ definition passive_sim_cfg_fail
 definition dependent_2
   where "dependent_2 A \<Lambda>' \<Omega> U0 m = dependent A \<Lambda>' \<Omega> U0 {y. y \<le> m}"
 
-definition passive_lemma_assms_2 :: "'a absval_ty_fun \<Rightarrow> proc_context \<Rightarrow> var_context \<Rightarrow> var_context \<Rightarrow> 
+definition passive_lemma_assms_2 :: "'a absval_ty_fun \<Rightarrow> 'struct_ty proc_context \<Rightarrow> var_context \<Rightarrow> var_context \<Rightarrow> 
                    'a fun_interp \<Rightarrow> rtype_env \<Rightarrow> vname \<Rightarrow> passive_rel \<Rightarrow> passive_rel \<Rightarrow> 
                   ('a nstate) set \<Rightarrow> vname set \<Rightarrow> 'a nstate \<Rightarrow> bool"
   where "passive_lemma_assms_2 A M \<Lambda> \<Lambda>' \<Gamma> \<Omega> w_min R R_old U0 D0 ns = 

BoogieLang/ROOT

@@ -16,3 +16,5 @@ session Boogie_Lang = "HOL" +
     PassificationEndToEnd
     PassificationML
     BackedgeElim
+    Ast
+    Ast_Cfg_Transformation