diff --git a/BoogieLang/Ast.thy b/BoogieLang/Ast.thy new file mode 100644 index 0000000..559482e --- /dev/null +++ b/BoogieLang/Ast.thy @@ -0,0 +1,217 @@ +section \Semantics of the AST\ + +theory Ast + imports Main Semantics Lang BackedgeElim + +begin + +subsection \AST definition\ + +type_synonym name = string +type_synonym label = string +type_synonym guard = expr +type_synonym invariant = expr + +datatype transfer_cmd + = Goto label + | Return + +datatype parsed_structured_cmd + = ParsedIf "guard option" "bigblock list" "bigblock list" + | ParsedWhile "guard option" "invariant list" "bigblock list" + | ParsedBreak nat + | WhileWrapper parsed_structured_cmd + +and bigblock + = BigBlock "name option" "cmd list" "parsed_structured_cmd option" "transfer_cmd option" + + +text \A Boogie statement represented as an AST is a list of \<^typ>\bigblock\\ + +type_synonym ast = "bigblock list" + +subsection \AST semantics\ + +text \We define a continuation-based small-step semantics.\ + +datatype cont + = KStop + | KSeq "bigblock" cont + | KEndBlock cont + +type_synonym 'a ast_config = "bigblock * cont * ('a state)" + +fun convert_list_to_cont :: "bigblock list \ cont \ cont" where + "convert_list_to_cont [] cont0 = cont0" + | "convert_list_to_cont (x#xs) cont0 = KSeq x (convert_list_to_cont xs cont0)" + +text\auxillary function to find the label a Goto statement is referring to\ +fun find_label :: "label \ bigblock list \ cont \ ((bigblock * cont) option)" where + "find_label lbl [] cont = None" + | "find_label lbl ((BigBlock bb_name cmds None None) # []) cont = + (if (Some lbl = bb_name) then (Some ((BigBlock bb_name cmds None None), cont)) else (None))" + | "find_label lbl ((BigBlock bb_name cmds None None) # bbs) cont = + (if (Some lbl = bb_name) + then (Some ((BigBlock bb_name cmds None None), (convert_list_to_cont ( bbs) cont))) + else (find_label lbl bbs cont))" + | "find_label lbl ((BigBlock bb_name cmds (Some (ParsedIf guard then_bbs else_bbs)) None) # bbs) cont = + (if (Some lbl = bb_name) + then (Some ((BigBlock bb_name cmds (Some (ParsedIf guard then_bbs else_bbs)) None), (convert_list_to_cont ( bbs) cont))) + else (if (find_label lbl then_bbs cont \ None) + then (find_label lbl (then_bbs @ bbs) cont) + else (find_label lbl (else_bbs @ bbs) cont)))" + | "find_label lbl ((BigBlock bb_name cmds (Some (ParsedWhile guard invariants body_bbs)) None) # bbs) cont = + (if (Some lbl = bb_name) + then (Some ((BigBlock bb_name cmds (Some (ParsedWhile guard invariants body_bbs)) None), (convert_list_to_cont ( bbs) cont))) + else (if (find_label lbl body_bbs cont \ None) + then (find_label lbl body_bbs (convert_list_to_cont ((bbs)@[(BigBlock None [] (Some (ParsedWhile guard invariants body_bbs)) None)]) cont)) + else (find_label lbl bbs cont)))" + | "find_label lbl ((BigBlock bb_name cmds (Some (ParsedBreak n)) None) # bbs) cont = + (if (Some lbl = bb_name) + then (Some ((BigBlock bb_name cmds (Some (ParsedBreak n)) None), (convert_list_to_cont ( bbs) cont))) + else (find_label lbl bbs cont))" + | "find_label lbl ((BigBlock bb_name cmds (Some (WhileWrapper while_loop)) None) # bbs) cont = + find_label lbl ((BigBlock bb_name cmds (Some while_loop) None) # bbs) cont" + | "find_label lbl ((BigBlock bb_name cmds None (Some transfer_stmt)) # bbs) cont = + (if (Some lbl = bb_name) + then (Some ((BigBlock bb_name cmds None (Some transfer_stmt)), (convert_list_to_cont ( bbs) cont))) + else (find_label lbl bbs cont))" + | "find_label lbl ((BigBlock bb_name cmds (Some s) (Some t)) # bbs) cont = None" + +fun get_state :: "'a ast_config \ 'a state" + where + "get_state (bb, cont, s1) = s1" + +fun is_final :: "'a ast_config \ bool" + where + "is_final ((BigBlock bb_name [] None None), KStop, s1) = True" + | "is_final other = False" + +text \Small-step semantics\ + +inductive red_bigblock :: "'a absval_ty_fun \ 'm proc_context \ var_context \ 'a fun_interp \ rtype_env \ ast \ 'a ast_config \ 'a ast_config \ bool" + ("_,_,_,_,_,_ \ (\_\ \/ _)" [51,0,0,0] 81) + for A :: "'a absval_ty_fun" and M :: "'m proc_context" and \ :: var_context and \ :: "'a fun_interp" and \ :: rtype_env and T :: ast + where + RedSimpleCmds: + "\(A,M,\,\,\ \ \cs, (Normal n_s)\ [\] s1) \ (cs \ Nil) \ + \ A,M,\,\,\,T \ \((BigBlock bb_name cs str_cmd tr_cmd), cont0, Normal n_s)\ \ + ((BigBlock bb_name [] str_cmd tr_cmd), cont0, s1)" + + | RedFailure_or_Magic: + "\ (s1 = Magic) \ (s1 = Failure); \ (is_final ((BigBlock bb_name [] str_cmd tr_cmd), cont0, s1)) \ + \ A,M,\,\,\,T \ \((BigBlock bb_name [] str_cmd tr_cmd), cont0, s1)\ \ + ((BigBlock bb_name [] None None), KStop, s1)" + + | RedSkip: + "A,M,\,\,\,T \ \((BigBlock bb_name [] None None), (KSeq b cont0), Normal n_s)\ \ + (b, cont0, Normal n_s)" + + | RedSkipEndBlock: + "A,M,\,\,\,T \ \((BigBlock bb_name [] None None), (KEndBlock cont0), Normal n_s)\ \ + ((BigBlock bb_name [] None None), cont0, Normal n_s)" + + | RedReturn: + "A,M,\,\,\,T \ \(BigBlock bb_name [] None (Some Return), cont0, Normal n_s)\ \ + ((BigBlock bb_name [] None None), KStop, Normal n_s)" + + | RedParsedIfTrue: + "\\ b. bb_guard = (Some b) \ A,\,\,\ \ \b, n_s\ \ LitV (LBool True) \ + \ A,M,\,\,\,T \ \((BigBlock bb_name [] + (Some (ParsedIf bb_guard (then_hd # then_bbs) elsebigblocks)) None), cont0, Normal n_s)\ \ + (then_hd, (convert_list_to_cont ( then_bbs) cont0), Normal n_s)" + + | RedParsedIfFalse: + "\\b. bb_guard = (Some b) \ A,\,\,\ \ \b, n_s\ \ LitV (LBool False) \ + \ A,M,\,\,\,T \ \((BigBlock bb_name [] + (Some (ParsedIf bb_guard thenbigblocks (else_hd # else_bbs))) None), cont0, Normal n_s)\ \ + (else_hd, (convert_list_to_cont ( else_bbs) cont0), Normal n_s)" + + | RedParsedWhileWrapper: + "A,M,\,\,\,T \ + \((BigBlock bb_name [] + (Some (WhileWrapper str)) None), cont0, Normal n_s)\ \ + ((BigBlock bb_name [] + (Some str) None), (KEndBlock cont0), Normal n_s)" + + | RedParsedWhile_InvFail: + "\\ b. bb_guard = (Some b) \ A,\,\,\ \ \b, n_s\ \ LitV (LBool True); + bb_invariants = invs1@[I]@invs2; + expr_all_sat A \ \ \ n_s invs1; + A,\,\,\ \ \I, n_s\ \ BoolV False \ + \ A,M,\,\,\,T \ + \((BigBlock bb_name [] + (Some (ParsedWhile bb_guard bb_invariants (bb_hd # body_bbs))) None), cont0, Normal n_s)\ \ + ((BigBlock bb_name [] None None), KStop, Failure)" + + | RedParsedWhileTrue: + "\\ b. bb_guard = (Some b) \ A,\,\,\ \ \b, n_s\ \ LitV (LBool True); + (expr_all_sat A \ \ \ n_s bb_invariants) \ + \ A,M,\,\,\,T \ + \((BigBlock bb_name [] + (Some (ParsedWhile bb_guard bb_invariants (bb_hd # body_bbs))) None), cont0, Normal n_s)\ \ + (bb_hd, convert_list_to_cont ((body_bbs)@[(BigBlock bb_name [] (Some (ParsedWhile bb_guard bb_invariants (bb_hd # body_bbs))) None)]) cont0, Normal n_s)" + + + | RedParsedWhileFalse: + "\\ b. bb_guard = (Some b) \ A,\,\,\ \ \b, n_s\ \ LitV (LBool False); + (expr_all_sat A \ \ \ n_s bb_invariants) \ + \ A,M,\,\,\,T \ \((BigBlock bb_name [] + (Some (ParsedWhile bb_guard bb_invariants bigblocks)) None), cont0, Normal n_s)\ \ + ((BigBlock bb_name [] None None), cont0, Normal n_s)" + + | RedBreak0: + "A,M,\,\,\,T \ \((BigBlock bb_name [] (Some (ParsedBreak 0)) None), (KEndBlock cont0), Normal n_s)\ \ + ((BigBlock bb_name [] None None), cont0, Normal n_s)" + + | RedBreakN: + "A,M,\,\,\,T \ + \((BigBlock bb_name [] (Some (ParsedBreak n)) None), (KSeq b cont0), Normal n_s)\ \ + ((BigBlock None [] (Some (ParsedBreak n)) None), cont0, Normal n_s)" + + | RedBreakNPlus1: + "A,M,\,\,\,T \ + \((BigBlock bb_name [] (Some (ParsedBreak (n + 1))) None), (KEndBlock cont0), Normal n_s)\ \ + ((BigBlock None [] (Some (ParsedBreak n)) None), cont0, Normal n_s)" + + | RedGoto: + "\ (find_label label T KStop) = Some (found_bigblock, found_cont) \ + \ A,M,\,\,\,T \ \((BigBlock bb_name [] None (Some (Goto label))), cont0, Normal n_s)\ \ + (found_bigblock, found_cont, (Normal n_s))" + +abbreviation red_bigblock_k_step :: "'a absval_ty_fun \ 'm proc_context \ var_context \ 'a fun_interp \ rtype_env \ ast \ 'a ast_config \ nat \ 'a ast_config \ bool" + ("_,_,_,_,_,_ \_ -n\^_/ _" [51,0,0,0,0] 81) +where "red_bigblock_k_step A M \ \ \ T c1 n c2 \ ((red_bigblock A M \ \ \ T)^^n) c1 c2" + +subsection \Procedure Correctness\ + +text\defining correctness of the AST\ + +fun convert_ast_to_program_point :: "ast \ bigblock \ cont" where + "convert_ast_to_program_point [] = ((BigBlock None [] None None), KStop)" + | "convert_ast_to_program_point (b#bs) = (b, convert_list_to_cont bs KStop)" + +fun init_ast :: "ast \ 'a nstate \ 'a ast_config" + where + "init_ast [] ns1 = ((BigBlock None [] None None), KStop, Normal ns1)" + | "init_ast (b#bbs) ns1 = (b, convert_list_to_cont ( bbs) KStop, Normal ns1)" + +definition valid_configuration + where "valid_configuration A \ \ \ posts bb cont state \ + state \ Failure \ + (is_final (bb, cont, state) \ (\ns'. state = Normal ns' \ expr_all_sat A \ \ \ ns' posts))" + +definition proc_body_satisfies_spec :: "'a absval_ty_fun \ 'm proc_context \ var_context \ 'a fun_interp \ rtype_env \ expr list \ expr list \ ast \ 'a nstate \ bool" + where "proc_body_satisfies_spec A M \ \ \ pres posts ast ns \ + expr_all_sat A \ \ \ ns pres \ + (\ bb cont state. (rtranclp (red_bigblock A M \ \ \ ast) (init_ast ast ns) (bb, cont, state)) \ + valid_configuration A \ \ \ posts bb cont state)" + +fun proc_all_pres :: "ast procedure \ expr list" + where "proc_all_pres p = map fst (proc_pres p)" + +fun proc_checked_posts :: "ast procedure \ expr list" + where "proc_checked_posts p = map fst (filter (\x. \ snd(x)) (proc_posts p))" + +end + diff --git a/BoogieLang/Ast_Cfg_Transformation.thy b/BoogieLang/Ast_Cfg_Transformation.thy new file mode 100644 index 0000000..dfdbab3 --- /dev/null +++ b/BoogieLang/Ast_Cfg_Transformation.thy @@ -0,0 +1,2253 @@ +section \Generic lemmas used to validate AST-to-CFG phase\ + +theory Ast_Cfg_Transformation + imports Main Ast Semantics BackedgeElim +begin + +type_synonym 'a satisfies_spec_func_type = + "'a absval_ty_fun \ mbodyCFG proc_context \ var_context \ 'a fun_interp \ rtype_env \ expr list \ expr list \ ast \ 'a nstate \ bool" + +subsection \Syntactic helper relations\ + +inductive syntactic_equiv :: "expr \ expr \ bool" (infixl "\" 40) + where + neg_refl: "UnOp Not e1 \ UnOp Not e1" + | neg_equiv1: "UnOp Not (Lit (LBool True)) \ (Lit (LBool False))" + | neg_equiv2: "UnOp Not (Lit (LBool False)) \ (Lit (LBool True))" + | double_neg: "UnOp Not (UnOp Not e1) \ e1" + | neg_eq: "UnOp Not (a \Eq\ b) \ (a \Neq\ b)" + | neg_neq: "UnOp Not (a \Neq\ b) \ (a \Eq\ b)" + | neg_lt: "UnOp Not (a \Lt\ b) \ (b \Le\ a)" + | neg_le: "UnOp Not (a \Le\ b) \ (b \Lt\ a)" + | neg_gt: "UnOp Not (a \Gt\ b) \ (b \Ge\ a)" + | neg_ge: "UnOp Not (a \Ge\ b) \ (b \Gt\ a)" + +inductive ast_cfg_rel :: "expr option \ cmd list \ bigblock \ cmd list \ bool" + where + Rel_Guard_true: + "\bb = (BigBlock name cs1 any_str any_tr); ast_cfg_rel None [] bb cs2\ \ + ast_cfg_rel (Some block_guard) [] bb ((Assume block_guard) # cs2)" + | Rel_Guard_false: + "\bb = (BigBlock name cs1 any_str any_tr); ast_cfg_rel None [] bb cs2; (UnOp Not block_guard) \ c \ \ + ast_cfg_rel (Some block_guard) [] bb ((Assume c) # cs2)" + | Rel_Invs: + "\bb = (BigBlock name [] any_str any_tr)\ \ ast_cfg_rel None assertions bb assertions" + | Rel_Main_test: + "\bb = (BigBlock name cs1 any_str any_tr); cs1 = c#cs\ \ ast_cfg_rel None [] bb cs1" + +subsection \Miscellaneous helper lemmas\ + +lemma not_true_equals_false: + assumes "A,\,\,\ \ \UnOp unop.Not expr, ns1\ \ BoolV True" + shows "A,\,\,\ \ \expr, ns1\ \ BoolV (False)" + using assms +proof cases + case (RedUnOp v) + from this obtain b1 where "v = LitV (LBool b1)" + by (metis (no_types) map_option_eq_Some option.simps(3) unop_eval.simps(1) unop_eval_val.elims unop_not.elims) + from this RedUnOp have + expand1: "A,\,\,\ \ \expr,ns1\ \ (LitV (LBool b1))" and + expand2: "unop_eval_val unop.Not (LitV (LBool b1)) = Some (BoolV True)" + by auto + then show ?thesis by fastforce +qed + +lemma not_false_equals_true: + assumes "A,\,\,\ \ \UnOp unop.Not expr, ns1\ \ BoolV False" + shows "A,\,\,\ \ \expr, ns1\ \ BoolV (True)" + using assms +proof cases + case (RedUnOp v) + from this obtain b1 where "v = LitV (LBool b1)" + by (auto elim: lit_val_elim[where v=v]) + with RedUnOp have + expand1: "A,\,\,\ \ \expr,ns1\ \ (LitV (LBool b1))" and + expand2: "unop_eval_val unop.Not (LitV (LBool b1)) = Some (BoolV False)" + by auto + then show ?thesis by fastforce +qed + +lemma true_equals_not_false: + assumes "A,\,\,\ \ \expr, ns1\ \ BoolV True" + shows "A,\,\,\ \ \UnOp unop.Not expr, ns1\ \ BoolV (False)" + using assms by (auto intro: RedUnOp) + +lemma false_equals_not_true: + assumes "A,\,\,\ \ \expr, ns1\ \ BoolV False" + shows "A,\,\,\ \ \UnOp unop.Not expr, ns1\ \ BoolV (True)" + using assms by (auto intro: RedUnOp) + +lemma equiv_preserves_value: + assumes "a \ b" + and "red_expr A \ \ \ a ns (BoolV boolean)" + shows "red_expr A \ \ \ b ns (BoolV boolean)" + using assms +proof cases + case (neg_refl e1) + then show ?thesis using assms by simp +next + case neg_equiv1 + then show ?thesis using assms by (metis (full_types) RedLit not_true_equals_false val_elim) +next + case neg_equiv2 + then show ?thesis using assms by (metis (full_types) RedLit not_false_equals_true val_elim) +next + case double_neg + then show ?thesis using assms by (metis (full_types) not_false_equals_true not_true_equals_false) +next + case (neg_eq e1 e2) + from this assms have unop_red: "A,\,\,\ \ \UnOp unop.Not (e1 \Eq\ e2), ns\ \ BoolV boolean" by simp + from this obtain v1 v2 bopRes where + redE1: "A,\,\,\ \ \e1, ns\ \ v1" and + redE2: "A,\,\,\ \ \e2, ns\ \ v2" and + binopEval: "binop_eval_val Eq v1 v2 = Some bopRes" and + unopEval: "unop_eval_val unop.Not bopRes = Some (BoolV boolean)" + by auto + + have bopResEq:"bopRes = BoolV (\boolean)" + by (insert unopEval, rule lit_val_elim[where v=bopRes]) auto + + have "binop_eval_val Neq v2 v1 = Some (BoolV boolean)" + apply (insert binopEval bopResEq) + apply (rule lit_val_elim[where v=v2]; rule lit_val_elim[where v=v1]) + by auto + + thus ?thesis + by (auto intro: RedBinOp redE1 redE2 simp: \b = _\) +next + case (neg_neq e1 e2) + from this assms have unop_red: "A,\,\,\ \ \UnOp unop.Not (e1 \Neq\ e2), ns\ \ BoolV boolean" by simp + from this obtain v1 v2 bopRes where + redE1: "A,\,\,\ \ \e1, ns\ \ v1" and + redE2: "A,\,\,\ \ \e2, ns\ \ v2" and + binopEval: "binop_eval_val Neq v1 v2 = Some bopRes" and + unopEval: "unop_eval_val unop.Not bopRes = Some (BoolV boolean)" + by auto + + have bopResEq:"bopRes = BoolV (\boolean)" + by (insert unopEval, rule lit_val_elim[where v=bopRes]) auto + + have "binop_eval_val Eq v2 v1 = Some (BoolV boolean)" + apply (insert binopEval bopResEq) + apply (rule lit_val_elim[where v=v2]; rule lit_val_elim[where v=v1]) + by auto + + thus ?thesis + by (auto intro: RedBinOp redE1 redE2 simp: \b = _\) +next + case (neg_lt e1 e2) + from this assms have unop_red: "A,\,\,\ \ \UnOp unop.Not (e1 \Lt\ e2), ns\ \ BoolV boolean" by simp + from this obtain v1 v2 bopRes where + redE1: "A,\,\,\ \ \e1, ns\ \ v1" and + redE2: "A,\,\,\ \ \e2, ns\ \ v2" and + binopEval: "binop_eval_val Lt v1 v2 = Some bopRes" and + unopEval: "unop_eval_val unop.Not bopRes = Some (BoolV boolean)" + by auto + + have bopResEq:"bopRes = BoolV (\boolean)" + by (insert unopEval, rule lit_val_elim[where v=bopRes]) auto + + have "binop_eval_val Le v2 v1 = Some (BoolV boolean)" + apply (insert binopEval bopResEq) + apply (rule lit_val_elim[where v=v2]; rule lit_val_elim[where v=v1]) + by auto + + thus ?thesis + by (auto intro: RedBinOp redE1 redE2 simp: \b = _\) +next + case (neg_le e1 e2) + from this assms have unop_red: "A,\,\,\ \ \UnOp unop.Not (e1 \Le\ e2), ns\ \ BoolV boolean" by simp + from this obtain v1 v2 bopRes where + redE1: "A,\,\,\ \ \e1, ns\ \ v1" and + redE2: "A,\,\,\ \ \e2, ns\ \ v2" and + binopEval: "binop_eval_val Le v1 v2 = Some bopRes" and + unopEval: "unop_eval_val unop.Not bopRes = Some (BoolV boolean)" + by auto + + have bopResEq:"bopRes = BoolV (\boolean)" + by (insert unopEval, rule lit_val_elim[where v=bopRes]) auto + + have "binop_eval_val Lt v2 v1 = Some (BoolV boolean)" + apply (insert binopEval bopResEq) + apply (rule lit_val_elim[where v=v2]; rule lit_val_elim[where v=v1]) + by auto + + thus ?thesis + by (auto intro: RedBinOp redE1 redE2 simp: \b = _\) +next + case (neg_gt e1 e2) + from this assms have unop_red: "A,\,\,\ \ \UnOp unop.Not (e1 \Gt\ e2), ns\ \ BoolV boolean" by simp + from this obtain v1 v2 bopRes where + redE1: "A,\,\,\ \ \e1, ns\ \ v1" and + redE2: "A,\,\,\ \ \e2, ns\ \ v2" and + binopEval: "binop_eval_val Gt v1 v2 = Some bopRes" and + unopEval: "unop_eval_val unop.Not bopRes = Some (BoolV boolean)" + by auto + + have bopResEq:"bopRes = BoolV (\boolean)" + by (insert unopEval, rule lit_val_elim[where v=bopRes]) auto + + have "binop_eval_val Ge v2 v1 = Some (BoolV boolean)" + apply (insert binopEval bopResEq) + apply (rule lit_val_elim[where v=v2]; rule lit_val_elim[where v=v1]) + by auto + + thus ?thesis + by (auto intro: RedBinOp redE1 redE2 simp: \b = _\) +next + case (neg_ge e1 e2) + from this assms have unop_red: "A,\,\,\ \ \UnOp unop.Not (e1 \Ge\ e2), ns\ \ BoolV boolean" by simp + from this obtain v1 v2 bopRes where + redE1: "A,\,\,\ \ \e1, ns\ \ v1" and + redE2: "A,\,\,\ \ \e2, ns\ \ v2" and + binopEval: "binop_eval_val Ge v1 v2 = Some bopRes" and + unopEval: "unop_eval_val unop.Not bopRes = Some (BoolV boolean)" + by auto + + have bopResEq:"bopRes = BoolV (\boolean)" + by (insert unopEval, rule lit_val_elim[where v=bopRes]) auto + + have "binop_eval_val Gt v2 v1 = Some (BoolV boolean)" + apply (insert binopEval bopResEq) + apply (rule lit_val_elim[where v=v2]; rule lit_val_elim[where v=v1]) + by auto + + thus ?thesis + by (auto intro: RedBinOp redE1 redE2 simp: \b = _\) +qed + +text \If all invariants hold, then the block containing the assertions corresponding to the invariants doesn't fail\ +lemma asserts_hold_if_invs_hold: + assumes "expr_all_sat A \ \ \ ns1 invs" + and "assertions = map Assert invs" + shows "A,M,\,\,\ \ \assertions, Normal ns1\ [\] Normal ns1" + using assms +proof (induction invs arbitrary: assertions) + case Nil + then show ?case by (simp add: RedCmdListNil) +next + case (Cons e_inv invs_tail) + from Cons(2) have prem1: "expr_all_sat A \ \ \ ns1 invs_tail" by (simp add: expr_all_sat_def) + from Cons(3) have prem2: "List.tl assertions = map Assert invs_tail" by simp + from prem1 prem2 have end2: "A,M,\,\,\ \ \List.tl assertions,Normal ns1\ [\] Normal ns1" + using Cons(1) by blast + + from Cons(2) have act1: "expr_sat A \ \ \ ns1 e_inv" by (simp add: expr_all_sat_def) + from Cons(3) have act2: "List.hd assertions = (Assert e_inv)" by simp + from act1 act2 have end1: "A,M,\,\,\ \ \List.hd assertions,Normal ns1\ \ Normal ns1" + by (simp add: expr_sat_def red_cmd.intros(1)) + + then show ?case using end1 end2 by (simp add: Cons.prems(2) RedCmdListCons) +qed + +text \If the block containing the assertions corresponding to the invariants doesn't fail, then all invariants hold\ +lemma invs_hold_if_asserts_reduce: + assumes "A,M,\,\,\ \ \assertions, s0\ [\] s1" + and "s0 = Normal ns1" + and "s1 \ Failure" + and "assertions = map Assert invs" + shows "expr_all_sat A \ \ \ ns1 invs" + using assms +proof (induction arbitrary: invs rule: red_cmd_list.induct) + case (RedCmdListNil s) + hence "invs = []" by simp + then show ?case by (simp add: expr_all_sat_def) +next + case (RedCmdListCons c s s'' cs s') + from RedCmdListCons have "cs = map Assert (List.tl invs)" using assms by auto + from RedCmdListCons have "c = Assert (hd invs)" by auto + + from RedCmdListCons this \s = Normal ns1\ show ?case + proof cases + case RedAssertOk thus ?thesis + using RedCmdListCons \c = Assert (hd invs)\ \s = Normal ns1\ \cs = map Assert (List.tl invs)\ + by (metis RedCmdListCons.IH RedCmdListCons.prems(2) + RedCmdListCons.prems(3) cmd.inject(1) expr_all_sat_def expr_sat_def + list.collapse list.discI list.map_disc_iff list_all_simps(1) state.inject) + next + case RedAssertFail thus ?thesis using failure_stays_cmd_list RedCmdListCons(2) RedCmdListCons(5) by blast + qed auto +qed + +text \If one invariant doesn't hold, then the block containing the assert cmds corresponding to the invariants fails\ +lemma one_inv_fails_assertions: + assumes InvsEq: "invs = invs1 @ [I] @ invs2" + and AllSat: "expr_all_sat A \ \ \ ns1 invs1" + and InvFail: "A,\,\,\ \ \I,ns1\ \ BoolV False" + and AssertionsEq: "assertions = map Assert invs" + shows "A,M,\,\,\ \ \assertions, Normal ns1\ [\] Failure" + using assms +proof - + from InvsEq AssertionsEq obtain assum1 a_fail assum2 where + left: "assum1 = map Assert invs1" and + mid_fail: "a_fail = Assert I" and + right: "assum2 = map Assert invs2" and + concat: "assertions = assum1 @ [a_fail] @ assum2" + by simp + from AllSat left have left_red: "A,M,\,\,\ \ \assum1, Normal ns1\ [\] Normal ns1" using asserts_hold_if_invs_hold by simp + from mid_fail have "A,M,\,\,\ \ \a_fail, Normal ns1\ \ Failure" using red_cmd.intros(2) assms(3) by simp + from this left_red have "A,M,\,\,\ \ \assum1 @ [a_fail] @ assum2, Normal ns1\ [\] Failure" using failure_stays_cmd_list + by (simp add: RedCmdListCons failure_red_cmd_list red_cmd_list_append) + thus ?thesis using concat by auto +qed + +lemma valid_config_implies_not_failure: + assumes "Semantics.valid_configuration A \ \ \ posts m' s'" + shows "s' \ Failure" + using Semantics.valid_configuration_def assms by blast + +lemma valid_config_implies_satisfied_posts: + assumes "Semantics.valid_configuration A \ \ \ posts m' s'" + shows "is_final_config (m', s') \ (\ns_end. s' = Normal ns_end \ (expr_all_sat A \ \ \ ns_end) posts)" + using Semantics.valid_configuration_def assms by (metis) + +text \If an \<^term>\ast_config\ (bigblock, cont, state) is an ending configuration, then any corresponding cfg block is locally correct.\ +lemma end_static: + assumes "A,M,\1_local,\,\,T \ \(BigBlock any [] None None, KStop, Normal ns1)\ \ (step_bb, step_cont, step_state)" + shows "step_state \ Failure \ (\ns1'. step_state = Normal ns1' \ A,M,\0,\,[] \ \any_block ,Normal ns1\ [\] Normal ns1')" + using assms + by (cases) auto + +lemma end_return: + assumes "A,M,\1_local,\,\,T \ \(BigBlock any [] None (Some Return), KStop, Normal ns1)\ \ (step_bb, step_cont, step_state)" + shows "step_state \ Failure \ (\ns1'. step_state = Normal ns1' \ A,M,\0,\,[] \ \[] ,Normal ns1\ [\] Normal ns1')" + using assms + by (cases) (auto simp add: RedCmdListNil) + +text \If an ast configuration is final, then any transition in the ast will stay in the same configuration.\ +lemma final_is_static: + assumes "is_final ((BigBlock name [] None None), start_cont, start_state)" + shows "\A M \ \ \ T end_bb end_cont end_state. + (red_bigblock A M \ \ \ T ((BigBlock name [] None None), start_cont, start_state) (end_bb, end_cont, end_state)) \ + ((end_bb, end_cont, end_state) = ((BigBlock name [] None None), start_cont, start_state))" + using assms +proof - + fix A M \ \ \ T end_bb end_cont end_state + have cont_eq: "start_cont = KStop" using assms is_final.elims(1) by blast + assume prem1: "(red_bigblock A M \ \ \ T ((BigBlock name [] None None), start_cont, start_state) (end_bb, end_cont, end_state))" + from prem1 show "((end_bb, end_cont, end_state) = ((BigBlock name [] None None), start_cont, start_state))" using cont_eq + proof cases + case RedFailure_or_Magic thus ?thesis using cont_eq by blast + qed auto +qed + +lemma final_is_static_propagate: + assumes "rtranclp (red_bigblock A M \ \ \ T) start_config end_config" + and "is_final start_config" + and "start_config = ((BigBlock name [] None None), start_cont, start_state)" + shows "end_config = ((BigBlock name [] None None), start_cont, start_state)" + using assms +proof (induction rule: rtranclp.induct) + case (rtrancl_refl a) + then show ?case using assms by simp +next + case (rtrancl_into_rtrancl a b c) + then have inter_is_same: "b = (BigBlock name [] None None, start_cont, start_state)" and inter_is_final: "is_final b" by auto + have "start_cont = KStop" using rtrancl_into_rtrancl(4) is_final.elims(1) rtrancl_into_rtrancl.prems(2) by blast + from rtrancl_into_rtrancl(2) show ?case + using inter_is_same inter_is_final \start_cont = KStop\ + proof cases + case RedFailure_or_Magic + thus ?thesis + using inter_is_same inter_is_final \start_cont = KStop\ + by (auto simp add: RedFailure_or_Magic) + qed auto +qed + +lemma magic_propagates: + assumes "A,M,\,\,\,T \ (bb, cont, Magic) -n\^j (reached_bb, reached_cont, reached_state)" + shows "reached_state = Magic" + using assms +proof (cases j) + case 0 + hence "(reached_bb, reached_cont, reached_state) = (bb, cont, Magic)" using assms by fastforce + thus ?thesis by simp +next + case (Suc j') + from this obtain first_inter where + red1: "A,M,\,\,\,T \ \(bb, cont, Magic)\ \ first_inter" and + red_rest: "A,M,\,\,\,T \ first_inter -n\^j' (reached_bb, reached_cont, reached_state)" + by (metis assms relpowp_Suc_E2) + hence reached_conj: "((get_state first_inter) = Magic) \ ((is_final first_inter) = True)" + proof cases + case RedFailure_or_Magic + thus ?thesis by simp + qed + hence magic_reached: "(get_state first_inter) = Magic" by simp + have final_config: "is_final first_inter" using reached_conj by simp + hence "\ name. first_inter = ((BigBlock name [] None None), KStop, Magic)" using magic_reached + by (metis get_state.simps is_final.elims(2)) + from this obtain name1 where concrete: "first_inter = ((BigBlock name1 [] None None), KStop, Magic)" + by blast + from red_rest show ?thesis using final_config magic_reached concrete final_is_static_propagate + by (metis prod.inject relpowp_imp_rtranclp) +qed + +text \The following are simple helper lemmas used in the proofs that involve applying induction hypotheses to prove global correctness of loop-heads.\ + +lemma smaller_helper: "k < j \ k < (Suc j)" + by simp + +lemma less_trans_inv: "(y :: nat) < z \ x < y \ x < z" + using less_trans by simp + +lemma eq_to_succ: "x = y \ x < (Suc y)" by simp + +lemma strictly_smaller_helper2: "j'' < j' \ j = Suc j' \ j'' < j" + by simp + +lemma strictly_smaller_helper3: "j'' < j' \ j''' < j'' \ j = Suc j' \ j''' < j" + by simp + +lemma strictly_smaller_helper4: "j' = Suc (Suc j'') \ k < j'' \ j = Suc j' \ k < j" + by simp + +lemma smaller_helper5: "j = Suc j1 \ j1 = Suc (Suc j2) \ j2 < j" + by simp + +text \The following are helper lemmas related to taking steps through assume cmds in a given ast- or cfg-trace.\ + +lemma push_through_assumption_test1: + assumes ExtendedCorrect: "(\ s2'.(red_cmd_list A M \ \ \ (c#cs2) (Normal ns1) s2') \ s2' \ Failure)" + and assume_cmd: "c = Assume guard" + and guard_holds: "A,\,\,\ \ \guard, ns1\ \ LitV (LBool True)" + shows "(\ s2'.(red_cmd_list A M \ \ \ cs2 (Normal ns1) s2') \ s2' \ Failure)" + using RedAssumeOk RedCmdListCons ExtendedCorrect assume_cmd guard_holds + by blast + +lemma push_through_assumption0: + assumes assume_cmd: "c = Assume guard" + and guard_holds: "A,\,\,\ \ \guard, ns1\ \ LitV (LBool True)" + shows "\ s. (red_cmd_list A M \ \ \ (cs2) (Normal ns1) s) \ (red_cmd_list A M \ \ \ (c#cs2) (Normal ns1) s)" + using RedAssumeOk RedCmdListCons assume_cmd guard_holds + by blast + +lemma push_through_assumption1: + assumes assume_cmd: "c = Assume not_guard" + and NotGuardEquiv: "UnOp Not guard \ not_guard" + and guard_fails: "A,\,\,\ \ \guard, ns1\ \ LitV (LBool False)" + shows "\ s. (red_cmd_list A M \ \ \ (cs2) (Normal ns1) s) \ (red_cmd_list A M \ \ \ (c#cs2) (Normal ns1) s)" + by (metis NotGuardEquiv assume_cmd equiv_preserves_value false_equals_not_true guard_fails push_through_assumption0) + +lemma guard_holds_push_through_assumption: + assumes block_correctness: + "reached_state \ Failure \ + (\ ns1'. reached_state = Normal ns1' \ (red_cmd_list A M \ \ \ (cs2) (Normal ns1) (Normal ns1')))" + and assume_cmd: "c = Assume guard" + and guard_holds: "A,\,\,\ \ \guard, ns1\ \ LitV (LBool True)" + shows "reached_state \ Failure \ + (\ ns1'. reached_state = Normal ns1' \ (red_cmd_list A M \ \ \ (c#cs2) (Normal ns1) (Normal ns1')))" + by (simp add: assume_cmd block_correctness guard_holds push_through_assumption0) + +lemma guard_holds_push_through_assumption2: + assumes block_correctness: + "reached_state \ Failure \ + (\ ns1'. reached_state = Normal ns1' \ (red_cmd_list A M \ \ \ (c#cs2) (Normal ns1) (Normal ns1')))" + and assume_cmd: "c = Assume guard" + and guard_holds: "A,\,\,\ \ \guard, ns1\ \ LitV (LBool True)" + shows "reached_state \ Failure \ + (\ ns1'. reached_state = Normal ns1' \ (red_cmd_list A M \ \ \ (cs2) (Normal ns1) (Normal ns1')))" + using assume_cmd assume_true_cmds block_correctness by blast + +lemma guard_fails_push_through_assumption: + assumes block_correctness: + "reached_state \ Failure \ + (\ ns1'. reached_state = Normal ns1' \ (red_cmd_list A M \ \ \ (cs2) (Normal ns1) (Normal ns1')))" + and assume_cmd: "c = Assume not_guard" + and NotGuardEquiv: "UnOp Not guard \ not_guard" + and guard_fails: "A,\,\,\ \ \guard, ns1\ \ LitV (LBool False)" + shows "reached_state \ Failure \ (\ ns1'. reached_state = Normal ns1' \ (red_cmd_list A M \ \ \ (c#cs2) (Normal ns1) (Normal ns1')))" + using NotGuardEquiv assume_cmd block_correctness guard_fails push_through_assumption1 by blast + +lemma guard_fails_push_through_assumption2: + assumes block_correctness: "reached_state \ Failure \ (\ ns1'. reached_state = Normal ns1' \ (red_cmd_list A M \ \ \ (c#cs2) (Normal ns1) (Normal ns1')))" + and assume_cmd: "c = Assume not_guard" + and "UnOp Not guard \ not_guard" \\not required for lemma, but makes lemma in sync with analogous lemma above\ + and guard_fails: "A,\,\,\ \ \guard, ns1\ \ LitV (LBool False)" + shows "reached_state \ Failure \ (\ ns1'. reached_state = Normal ns1' \ (red_cmd_list A M \ \ \ (cs2) (Normal ns1) (Normal ns1')))" + using assume_cmd assume_true_cmds block_correctness by blast + +lemma correctness_propagates_through_assumption: + assumes "\m s. (A,M,\,\,\,G \(Inl n0, Normal ns1) -n\* (m, s)) \ s \ Failure" + and "node_to_block G ! n0 = [Assume c]" + and "UnOp Not guard \ c" + and "A,\,\,\ \ \guard, ns1\ \ BoolV False" + and "List.member (out_edges G ! n0) n1" + shows "\ m s. (A,M,\,\,\,G \(Inl n1, Normal ns1) -n\* (m, s)) \ s \ Failure" +proof - + fix m1 s1 + have "A,\,\,\ \ \c, ns1\ \ BoolV True" using assms(3-4) equiv_preserves_value false_equals_not_true by blast + then have a1: "(A,M,\,\,\ \ \[Assume c], Normal ns1\ [\] (Normal ns1))" by (meson RedAssumeOk RedCmdListCons RedCmdListNil) + show "(A,M,\,\,\,G \(Inl n1, Normal ns1) -n\* (m1, s1)) \ s1 \ Failure" + proof - + assume "(A,M,\,\,\,G \(Inl n1, Normal ns1) -n\* (m1, s1))" + thus "s1 \ Failure" using a1 assms(1-2) assms(5) dag_verifies_propagate by blast + qed +qed + +lemma correctness_propagates_through_assumption2: + assumes "\m s. (A,M,\,\,\,G \(Inl n0, Normal ns1) -n\* (m, s)) \ s \ Failure" + and "node_to_block G ! n0 = [Assume guard]" + and "A,\,\,\ \ \guard, ns1\ \ BoolV True" + and "List.member (out_edges G ! n0) n1" + shows "\ m s. (A,M,\,\,\,G \(Inl n1, Normal ns1) -n\* (m, s)) \ s \ Failure" +proof - + fix m1 s1 + have a1: "(A,M,\,\,\ \ \[Assume guard], Normal ns1\ [\] (Normal ns1))" + by (meson RedAssumeOk assms(3) red_cmd_list.simps) + show "(A,M,\,\,\,G \(Inl n1, Normal ns1) -n\* (m1, s1)) \ s1 \ Failure" + proof - + assume "(A,M,\,\,\,G \(Inl n1, Normal ns1) -n\* (m1, s1))" + thus "s1 \ Failure" using a1 assms(1-2) assms(4) dag_verifies_propagate by blast + qed +qed + +lemma correctness_propagates_through_assumption3: + assumes "\m s. (A,M,\,\,\,G \(Inl n0, Normal ns1) -n\* (m, s)) \ + (is_final_config (m, s) \ + (\ns_end. s = Normal ns_end \ (expr_all_sat A \1_local \ \ ns_end) posts))" + and "node_to_block G ! n0 = [Assume c]" + and "UnOp Not guard \ c" + and "A,\,\,\ \ \guard, ns1\ \ BoolV False" + and "List.member (out_edges G ! n0) n1" + shows "\ m s. (A,M,\,\,\,G \(Inl n1, Normal ns1) -n\* (m, s)) \ + (is_final_config (m, s) \ + (\ns_end. s = Normal ns_end \ (expr_all_sat A \1_local \ \ ns_end) posts))" +proof - + fix m1 s1 + have "A,\,\,\ \ \c, ns1\ \ BoolV True" using assms(3-4) equiv_preserves_value false_equals_not_true by blast + then have a1: "(A,M,\,\,\ \ \[Assume c], Normal ns1\ [\] (Normal ns1))" by (meson RedAssumeOk RedCmdListCons RedCmdListNil) + show "(A,M,\,\,\,G \(Inl n1, Normal ns1) -n\* (m1, s1)) \ + (is_final_config (m1, s1) \ + (\ns_end. s1 = Normal ns_end \ (expr_all_sat A \1_local \ \ ns_end) posts))" + proof - + assume "(A,M,\,\,\,G \(Inl n1, Normal ns1) -n\* (m1, s1))" + thus "(is_final_config (m1, s1) \ (\ns_end. s1 = Normal ns_end \ (expr_all_sat A \1_local \ \ ns_end) posts))" + using a1 assms by (metis RedNormalSucc converse_rtranclp_into_rtranclp) + qed +qed + +lemma correctness_propagates_through_assumption4: + assumes "\m s. (A,M,\,\,\,G \(Inl n0, Normal ns1) -n\* (m, s)) \ + (is_final_config (m, s) \ (\ns_end. s = Normal ns_end \ + (expr_all_sat A \1_local \ \ ns_end) posts))" + and "node_to_block G ! n0 = [Assume guard]" + and "A,\,\,\ \ \guard, ns1\ \ BoolV True" + and "List.member (out_edges G ! n0) n1" + shows "\ m s. (A,M,\,\,\,G \(Inl n1, Normal ns1) -n\* (m, s)) \ (is_final_config (m, s) \ + (\ns_end. s = Normal ns_end \ (expr_all_sat A \1_local \ \ ns_end) posts))" +proof - + fix m1 s1 + have a1: "(A,M,\,\,\ \ \[Assume guard], Normal ns1\ [\] (Normal ns1))" + by (meson RedAssumeOk assms(3) red_cmd_list.simps) + show "(A,M,\,\,\,G \(Inl n1, Normal ns1) -n\* (m1, s1)) \ + (is_final_config (m1, s1) \ + (\ns_end. s1 = Normal ns_end \ (expr_all_sat A \1_local \ \ ns_end) posts))" + proof - + assume "(A,M,\,\,\,G \(Inl n1, Normal ns1) -n\* (m1, s1))" + thus "(is_final_config (m1, s1) \ (\ns_end. s1 = Normal ns_end \ (expr_all_sat A \1_local \ \ ns_end) posts))" + using a1 assms by (metis RedNormalSucc converse_rtranclp_into_rtranclp) + qed +qed + +lemma correctness_propagates_through_empty: + assumes "\m s. (A,M,\,\,\,G \(Inl n0, Normal ns1) -n\* (m, s)) \ s \ Failure" + and "node_to_block G ! n0 = []" + and "List.member (out_edges G ! n0) n1" + shows "\ m s. (A,M,\,\,\,G \(Inl n1, Normal ns1) -n\* (m, s)) \ s \ Failure" +proof - + fix m1 s1 + have a1: "(A,M,\,\,\ \ \[], Normal ns1\ [\] (Normal ns1))" by (rule RedCmdListNil) + show "(A,M,\,\,\,G \(Inl n1, Normal ns1) -n\* (m1, s1)) \ s1 \ Failure" + proof - + assume "(A,M,\,\,\,G \(Inl n1, Normal ns1) -n\* (m1, s1))" + thus "s1 \ Failure" by (metis a1 assms(1-3) dag_verifies_propagate) + qed +qed + +lemma correctness_propagates_through_empty2: + assumes "\m s. (A,M,\,\,\,G \(Inl n0, Normal ns1) -n\* (m, s)) \ + (is_final_config (m, s) \ + (\ns_end. s = Normal ns_end \ (expr_all_sat A \1_local \ \ ns_end) posts))" + and "node_to_block G ! n0 = []" + and "List.member (out_edges G ! n0) n1" + shows "\ m s. (A,M,\,\,\,G \(Inl n1, Normal ns1) -n\* (m, s)) \ + (is_final_config (m, s) \ + (\ns_end. s = Normal ns_end \ (expr_all_sat A \1_local \ \ ns_end) posts))" +proof - + fix m1 s1 + have a1: "(A,M,\,\,\ \ \[], Normal ns1\ [\] (Normal ns1))" by (meson RedAssumeOk assms(3) red_cmd_list.simps) + show "(A,M,\,\,\,G \(Inl n1, Normal ns1) -n\* (m1, s1)) \ + (is_final_config (m1, s1) \ + (\ns_end. s1 = Normal ns_end \ (expr_all_sat A \1_local \ \ ns_end) posts))" + proof - + assume "(A,M,\,\,\,G \(Inl n1, Normal ns1) -n\* (m1, s1))" + thus "(is_final_config (m1, s1) \ (\ns_end. s1 = Normal ns_end \ (expr_all_sat A \1_local \ \ ns_end) posts))" + using a1 assms by (metis RedNormalSucc converse_rtranclp_into_rtranclp) + qed +qed + +subsection \Pairs of helper lemma + global lemma for certain special cases.\ + +text \The following are pairs of lemmas. Each pair consists of a helper lemma and a global block lemma. + The helper lemma ensures that if a valid AST configuration is a starting point of a trace and + the configuration is such that only certain rules, which don't change the state of the configuration, + can be applied for the trace to continue, then either the trace will finish in a valid configuration + after applying them or a different valid configuration will be reached from which the trace will continue. + The global block lemma proves the correctness of that AST trace, given the correctness of all cfg traces + starting in a cfg block related to the big block in the starting AST configuration. + Note that a syntactic relation between the big block and the cfg block does not need to be shown here, as these global block lemmas are only ever applied in conjuction with + other more generic global block lemmas, which will have already shown the syntactic relation.\ + +text \Pair 1: The starting configuration represents a point in the program after a loop, and + therefore the continuation needs to be adjusted.\ + +lemma endblock_skip: + assumes "A,M,\,\,\,T \(bb0, KEndBlock cont0, Normal ns3) -n\^l (reached_bb, reached_cont, reached_state)" + and "bb0 = BigBlock name [] None None" + shows "(valid_configuration A \ \ \ posts reached_bb reached_cont reached_state) \ + (\ l1. (A,M,\,\,\,T \(bb0, cont0, Normal ns3) -n\^l1 (reached_bb, reached_cont, reached_state)) \ (l = Suc l1) )" +proof (cases l) + case 0 + then show ?thesis by (metis Ast.valid_configuration_def assms(1) get_state.simps is_final.simps(6) relpowp_fun_conv state.simps(3)) +next + case 1: (Suc l1) + then show ?thesis + proof - + from 1 assms obtain inter_bb inter_cont inter_state where + step1: "(red_bigblock A M \ \ \ T (BigBlock name [] None None, KEndBlock cont0, Normal ns3) (inter_bb, inter_cont, inter_state))" and + rest: "A,M,\,\,\,T \(inter_bb, inter_cont, inter_state) -n\^l1 (reached_bb, reached_cont, reached_state)" + by (metis (no_types) prod_cases3 relpowp_Suc_D2) + from this step1 have "(inter_bb, inter_cont, inter_state) = (BigBlock name [] None None, cont0, Normal ns3)" + by (cases) auto + then show ?thesis using "1" assms(2) rest by blast + qed +qed + +lemma ending_after_skipping_endblock: + assumes "j = Suc j'" + and "A,M,\,\,\,T \(bb, KEndBlock cont0, Normal ns1'') -n\^j' (reached_bb, reached_cont, reached_state)" + and "bb = BigBlock None [] None None" + and "\m3 s3. (A,M,\,\,\,G \(Inl n, Normal ns1'') -n\* (m3, s3)) \ s3 \ Failure" + and "\m' s'. (A,M,\,\,\,G \(Inl n, Normal ns1'') -n\* (m', s')) \ + is_final_config (m', s') \ \ns_end. s' = Normal ns_end \ (expr_all_sat A \1_local \ \ ns_end) posts" + and "(cont_guard = Some guard) \ (A,\,\,\ \ \guard,ns1''\ \ BoolV False)" + and "\ j''. + j' = Suc j'' \ + A,M,\,\,\,T \(bb, cont0, Normal ns1'') -n\^j'' (reached_bb, reached_cont, reached_state) \ + (\m' s'. A,M,\,\,\,G \(Inl n, Normal ns1'') -n\* (m', s') \ s' \ Failure) \ + (\m' s'. (A,M,\,\,\,G \(Inl n, Normal ns1'') -n\* (m', s')) \ + is_final_config (m', s') \ \ns_end. s' = Normal ns_end \ (expr_all_sat A \1_local \ \ ns_end) posts) \ + ((cont_guard = Some guard) \ (A,\,\,\ \ \guard,ns1''\ \ BoolV False)) \ (valid_configuration A \ \ \ posts reached_bb reached_cont reached_state)" + shows "valid_configuration A \ \ \ posts reached_bb reached_cont reached_state" +proof - + from assms(2-3) have disj_a: + "(valid_configuration A \ \ \ posts reached_bb reached_cont reached_state) \ + (\ l2. (A,M,\,\,\,T \(bb, cont0, Normal ns1'') -n\^l2 (reached_bb, reached_cont, reached_state)) \ (j' = Suc l2) )" + by (simp add: endblock_skip) + thus ?thesis + proof cases + assume "(valid_configuration A \ \ \ posts reached_bb reached_cont reached_state)" thus ?thesis by simp + next + assume "\ ((valid_configuration A \ \ \ posts reached_bb reached_cont reached_state))" + hence "(\ l2. (A,M,\,\,\,T \(bb, cont0, Normal ns1'') -n\^l2 (reached_bb, reached_cont, reached_state)) \ (j' = Suc l2) )" + using disj_a by blast + thus ?thesis + proof - + obtain l2_conc where conc_trace: "(A,M,\,\,\,T \(bb, cont0, Normal ns1'') -n\^l2_conc (reached_bb, reached_cont, reached_state))" and + succ_rel: "(j' = Suc l2_conc)" + using \\l2. (A,M,\,\,\,T \(bb, cont0, Normal ns1'') -n\^l2 (reached_bb, reached_cont, reached_state)) \ j' = Suc l2\ by blast + show ?thesis + apply (rule assms(7)) + apply (rule succ_rel) + apply (rule conc_trace) + apply (rule assms(4)) + apply (simp) + apply (rule assms(5)) + apply assumption+ + using assms(6) false_equals_not_true + by blast + qed + qed +qed + +text \Pair 2: The starting configuration represents a point in the program after a loop and the + continuation needs to be adjusted and subsequently entered. + (This could be replaced by a simpler lemma.)\ +lemma endblock_skip2: + assumes "A,M,\,\,\,T \(bb0, KEndBlock (KSeq bb_next cont0), Normal ns3) -n\^l (reached_bb, reached_cont, reached_state)" + and "bb0 = BigBlock None [] None None" + shows "(valid_configuration A \ \ \ posts reached_bb reached_cont reached_state) \ + (\ l2. (A,M,\,\,\,T \(bb_next, cont0, Normal ns3) -n\^l2 (reached_bb, reached_cont, reached_state)) \ (l = Suc (Suc l2)) )" + using assms +proof (cases l) + case 0 + then show ?thesis by (metis Ast.valid_configuration_def assms(1) get_state.simps is_final.simps(6) relpowp_fun_conv state.simps(3)) +next + case 1: (Suc l1) + then show ?thesis + proof (cases l1) + case 0 + from 1 assms this have "(red_bigblock A M \ \ \ T (BigBlock None [] None None, KEndBlock (KSeq bb_next cont0), Normal ns3) (reached_bb, reached_cont, reached_state))" + by fastforce + then show ?thesis + proof cases + case RedSkipEndBlock thus ?thesis by (simp add: Ast.valid_configuration_def) + qed auto + next + case 2: (Suc l2) + from 2 1 have "l = Suc (Suc l2)" by auto + from 2 1 assms obtain inter_bb inter_cont inter_state inter_bb2 inter_cont2 inter_state2 where + step1: "(red_bigblock A M \ \ \ T (BigBlock None [] None None, KEndBlock (KSeq bb_next cont0), Normal ns3) (inter_bb, inter_cont, inter_state))" and + step2: "(red_bigblock A M \ \ \ T (inter_bb, inter_cont, inter_state) (inter_bb2, inter_cont2, inter_state2))" and + rest: "A,M,\,\,\,T \(inter_bb2, inter_cont2, inter_state2) -n\^l2 (reached_bb, reached_cont, reached_state)" + by (metis (no_types) prod_cases3 relpowp_Suc_D2) + from this step1 have "(inter_bb, inter_cont, inter_state) = (BigBlock None [] None None, (KSeq bb_next cont0), Normal ns3)" + proof cases + case RedSkipEndBlock thus ?thesis + by blast + qed auto + from step2 this have "(inter_bb2, inter_cont2, inter_state2) = (bb_next, cont0, Normal ns3)" + proof cases + case RedSkip + thus ?thesis + using \(inter_bb, inter_cont, inter_state) = (BigBlock None [] None None, KSeq bb_next cont0, Normal ns3)\ + by fastforce + qed auto + hence "(A,M,\,\,\,T \(bb_next, cont0, Normal ns3) -n\^l2 (reached_bb, reached_cont, reached_state)) \ (l = Suc (Suc l2))" + using rest \l = Suc (Suc l2)\ + by simp + then show ?thesis by blast + qed +qed + +lemma ending_after_skipping_endblock2: + assumes "j = Suc j'" + and "A,M,\,\,\,T \(bb, KEndBlock (KSeq bigblock_next cont0), Normal ns1'') -n\^j' (reached_bb, reached_cont, reached_state)" + and "bb = BigBlock None [] None None" + and "\m3 s3. (A,M,\,\,\,G \(Inl n, Normal ns1'') -n\* (m3, s3)) \ s3 \ Failure" + and "\m' s'. (A,M,\,\,\,G \(Inl n, Normal ns1'') -n\* (m', s')) \ + is_final_config (m', s') \ \ns_end. s' = Normal ns_end \ (expr_all_sat A \1_local \ \ ns_end) posts" + and "(cont_guard = Some guard) \ (A,\,\,\ \ \guard,ns1''\ \ BoolV False)" + and "\ j''. + j' = Suc (Suc j'') \ + A,M,\,\,\,T \(bigblock_next, cont0, Normal ns1'') -n\^j'' (reached_bb, reached_cont, reached_state) \ + (\m' s'. A,M,\,\,\,G \(Inl n, Normal ns1'') -n\* (m', s') \ s' \ Failure) \ + (\m' s'. (A,M,\,\,\,G \(Inl n, Normal ns1'') -n\* (m', s')) \ + is_final_config (m', s') \ \ns_end. s' = Normal ns_end \ (expr_all_sat A \1_local \ \ ns_end) posts) \ + ((cont_guard = Some guard) \ (A,\,\,\ \ \guard,ns1''\ \ BoolV False)) \ + valid_configuration A \ \ \ posts reached_bb reached_cont reached_state" + shows "valid_configuration A \ \ \ posts reached_bb reached_cont reached_state" +proof - + from assms(2-3) have disj_a: + "(valid_configuration A \ \ \ posts reached_bb reached_cont reached_state) \ + (\ l2. (A,M,\,\,\,T \(bigblock_next, cont0, Normal ns1'') -n\^l2 (reached_bb, reached_cont, reached_state)) \ + (j' = Suc (Suc l2)) )" + by (simp add: endblock_skip2) + thus ?thesis + proof cases + assume "(valid_configuration A \ \ \ posts reached_bb reached_cont reached_state)" thus ?thesis by simp + next + assume "\ ((valid_configuration A \ \ \ posts reached_bb reached_cont reached_state))" + hence "(\ l2. (A,M,\,\,\,T \(bigblock_next, cont0, Normal ns1'') -n\^l2 (reached_bb, reached_cont, reached_state)) \ + (j' = Suc (Suc l2)) )" + using disj_a by blast + thus ?thesis + proof - + obtain l2_conc where conc_trace: "(A,M,\,\,\,T \(bigblock_next, cont0, Normal ns1'') -n\^l2_conc (reached_bb, reached_cont, reached_state))" and + succ_rel: "(j' = Suc (Suc l2_conc))" + using \\l2. (A,M,\,\,\,T \(bigblock_next, cont0, Normal ns1'') -n\^l2 (reached_bb, reached_cont, reached_state)) \ j' = Suc (Suc l2)\ + by blast + show ?thesis + apply (rule assms(7)) + apply (rule succ_rel) + apply (rule conc_trace) + apply (rule assms(4)) + apply (simp) + apply (rule assms(5)) + apply simp+ + using assms(6) false_equals_not_true + by blast + qed + qed +qed + +text \Pair 3: The starting configuration represents a point in the program before a loop and, more + specifically, before the loop has been 'unwrapped'. + The 'wrapper' construct exists to accomodate the handling of breaks, which this theory + doesn't currently cover.\ + +lemma wrapper_to_endblock: + assumes "A,M,\,\,\,T \(bb0, cont0, Normal ns) -n\^l (reached_bb, reached_cont, reached_state)" + and "bb0 = BigBlock name [] (Some (WhileWrapper loop)) None" + shows "(valid_configuration A \ \ \ posts reached_bb reached_cont reached_state) \ + (\ l1. (A,M,\,\,\,T \((BigBlock name [] (Some loop) None), KEndBlock cont0, Normal ns) -n\^l1 + (reached_bb, reached_cont, reached_state)) \ (l = Suc l1))" + using assms +proof (cases l) + case 0 + hence "(reached_bb, reached_cont, reached_state) = (bb0, cont0, Normal ns)" using assms(1) by simp + then show ?thesis by (simp add: Ast.valid_configuration_def assms(2)) +next + case 1: (Suc l1) + then show ?thesis + proof - + from 1 assms obtain inter_bb inter_cont inter_state where + step1: "(red_bigblock A M \ \ \ T (bb0, cont0, Normal ns) (inter_bb, inter_cont, inter_state))" and + rest: "A,M,\,\,\,T \(inter_bb, inter_cont, inter_state) -n\^l1 (reached_bb, reached_cont, reached_state)" + by (metis (no_types) prod_cases3 relpowp_Suc_D2) + from this have "(inter_bb, inter_cont, inter_state) = (BigBlock name [] (Some loop) None, KEndBlock cont0, Normal ns)" + proof cases + case RedParsedWhileWrapper thus ?thesis using assms(2) by auto + qed (auto simp add: assms(2)) + hence "(A,M,\,\,\,T \(BigBlock name [] (Some loop) None, KEndBlock cont0, Normal ns) -n\^l1 (reached_bb, reached_cont, reached_state)) \ (l = Suc l1)" + using rest \l = Suc l1\ assms(2) by simp + then show ?thesis by blast + qed +qed + +lemma ending_after_unwrapping: + assumes "A,M,\,\,\,T \(bb, cont0, Normal ns1'') -n\^j (reached_bb, reached_cont, reached_state)" + and "bb = BigBlock name [] (Some (WhileWrapper loop)) None" + and "\m3 s3. (A,M,\,\,\,G \(Inl n, Normal ns1'') -n\* (m3, s3)) \ s3 \ Failure" + and "\m' s'. (A,M,\,\,\,G \(Inl n, Normal ns1'') -n\* (m', s')) \ + is_final_config (m', s') \ \ns_end. s' = Normal ns_end \ (expr_all_sat A \1_local \ \ ns_end) posts" + and "\ j''. + j = Suc j'' \ + A,M,\,\,\,T \(BigBlock name [] (Some loop) None, KEndBlock cont0, Normal ns1'') -n\^j'' (reached_bb, reached_cont, reached_state) \ + (\m' s'. A,M,\,\,\,G \(Inl n, Normal ns1'') -n\* (m', s') \ s' \ Failure) \ + (\m' s'. (A,M,\,\,\,G \(Inl n, Normal ns1'') -n\* (m', s')) \ + is_final_config (m', s') \ \ns_end. s' = Normal ns_end \ (expr_all_sat A \1_local \ \ ns_end) posts) \ + (valid_configuration A \ \ \ posts reached_bb reached_cont reached_state)" + shows "valid_configuration A \ \ \ posts reached_bb reached_cont reached_state" +proof - + from assms(1-2) have disj_a: + "(valid_configuration A \ \ \ posts reached_bb reached_cont reached_state) \ + (\ l1. (A,M,\,\,\,T \(BigBlock name [] (Some loop) None, KEndBlock cont0, Normal ns1'') -n\^l1 (reached_bb, reached_cont, reached_state)) \ (j = Suc l1) )" + by (simp add: wrapper_to_endblock) + thus ?thesis + proof cases + assume "(valid_configuration A \ \ \ posts reached_bb reached_cont reached_state)" thus ?thesis by simp + next + assume "\ ((valid_configuration A \ \ \ posts reached_bb reached_cont reached_state))" + hence "(\ l2. (A,M,\,\,\,T \(BigBlock name [] (Some loop) None, KEndBlock cont0, Normal ns1'') -n\^l2 (reached_bb, reached_cont, reached_state)) \ (j = Suc l2) )" + using disj_a by blast + thus ?thesis + proof - + obtain l2_conc where conc_trace: "(A,M,\,\,\,T \(BigBlock name [] (Some loop) None, KEndBlock cont0, Normal ns1'') -n\^l2_conc (reached_bb, reached_cont, reached_state))" and + succ_rel: "(j = Suc l2_conc)" + using \\l2. (A,M,\,\,\,T \(BigBlock name [] (Some loop) None, KEndBlock cont0, Normal ns1'') -n\^l2 (reached_bb, reached_cont, reached_state)) \ j = Suc l2\ by blast + show ?thesis + apply (rule assms(5)) + apply (rule succ_rel) + apply (rule conc_trace) + apply (rule assms(3)) + apply (simp) + apply (rule assms(4)) + apply simp+ + done + qed + qed +qed + +text \Pair 4: The starting configuration represents a point in the program after a loop and before a consecutive 'unwrapped' loop. + (This is potentially redundant but I couldn't conclude one example proof without it)\ +lemma endblock_skip_wrapper: + assumes "A,M,\,\,\,T \ (bb0, KEndBlock (KSeq (BigBlock name [] (Some (WhileWrapper str)) tr) cont0), Normal ns3) -n\^l + (reached_bb, reached_cont, reached_state)" + and "bb0 = BigBlock None [] None None" + shows "(valid_configuration A \ \ \ posts reached_bb reached_cont reached_state) \ + (\ l3. (A,M,\,\,\,T \((BigBlock name [] (Some str) tr), KEndBlock cont0, Normal ns3) -n\^l3 (reached_bb, reached_cont, reached_state)) \ + l = Suc (Suc (Suc l3)) )" + using assms +proof (cases l) + case 0 + then show ?thesis by (metis Ast.valid_configuration_def assms(1) get_state.simps is_final.simps(6) relpowp_fun_conv state.simps(3)) +next + case 1: (Suc l1) + then show ?thesis + proof (cases l1) + case 0 + from 1 assms this have + "(red_bigblock A M \ \ \ T (BigBlock None [] None None, KEndBlock (KSeq (BigBlock name [] (Some (WhileWrapper str)) tr) cont0), Normal ns3) (reached_bb, reached_cont, reached_state))" + by fastforce + then show ?thesis + proof cases + case RedSkipEndBlock thus ?thesis by (simp add: Ast.valid_configuration_def) + qed auto + next + case 2: (Suc l2) + then show ?thesis + proof (cases l2) + case 0 + from 2 1 have "l = Suc (Suc l2)" by auto + from 2 1 assms obtain inter_bb inter_cont inter_state where + step1: "(red_bigblock A M \ \ \ T (BigBlock None [] None None, KEndBlock (KSeq (BigBlock name [] (Some (WhileWrapper str)) tr) cont0), Normal ns3) (inter_bb, inter_cont, inter_state))" and + step2: "(red_bigblock A M \ \ \ T (inter_bb, inter_cont, inter_state) (reached_bb, reached_cont, reached_state))" + using "0" by auto + from this step1 have "(inter_bb, inter_cont, inter_state) = (BigBlock None [] None None, (KSeq (BigBlock name [] (Some (WhileWrapper str)) tr) cont0), Normal ns3)" + proof cases + case RedSkipEndBlock thus ?thesis + by blast + qed auto + from step2 this have "(reached_bb, reached_cont, reached_state) = ((BigBlock name [] (Some (WhileWrapper str)) tr), cont0, Normal ns3)" + proof cases + case RedSkip thus ?thesis using \(inter_bb, inter_cont, inter_state) = (BigBlock None [] None None, (KSeq (BigBlock name [] (Some (WhileWrapper str)) tr) cont0), Normal ns3)\ by fastforce + qed auto + then show ?thesis by (simp add: Ast.valid_configuration_def) + next + case 3: (Suc l3) + from 3 2 1 have "l = Suc (Suc (Suc l3))" by auto + from 3 2 1 assms obtain inter_bb inter_cont inter_state inter_bb2 inter_cont2 inter_state2 inter_bb3 inter_cont3 inter_state3 where + step1: "(red_bigblock A M \ \ \ T (BigBlock None [] None None, KEndBlock (KSeq (BigBlock name [] (Some (WhileWrapper str)) tr) cont0), Normal ns3) (inter_bb, inter_cont, inter_state))" and + step2: "(red_bigblock A M \ \ \ T (inter_bb, inter_cont, inter_state) (inter_bb2, inter_cont2, inter_state2))" and + step3: "(red_bigblock A M \ \ \ T (inter_bb2, inter_cont2, inter_state2) (inter_bb3, inter_cont3, inter_state3))" and + rest: "A,M,\,\,\,T \ (inter_bb3, inter_cont3, inter_state3) -n\^l3 (reached_bb, reached_cont, reached_state)" + by (metis (no_types) get_state.cases relpowp_Suc_D2) + + from this step1 have "(inter_bb, inter_cont, inter_state) = (BigBlock None [] None None, (KSeq (BigBlock name [] (Some (WhileWrapper str)) tr) cont0), Normal ns3)" + proof cases + case RedSkipEndBlock thus ?thesis + by blast + qed auto + from step2 this have "(inter_bb2, inter_cont2, inter_state2) = ((BigBlock name [] (Some (WhileWrapper str)) tr), cont0, Normal ns3)" + proof cases + case RedSkip thus ?thesis using \(inter_bb, inter_cont, inter_state) = (BigBlock None [] None None, (KSeq (BigBlock name [] (Some (WhileWrapper str)) tr) cont0), Normal ns3)\ by fastforce + qed auto + from step3 this have "(inter_bb3, inter_cont3, inter_state3) = ((BigBlock name [] (Some str) tr), KEndBlock cont0, Normal ns3)" + proof cases + case RedParsedWhileWrapper thus ?thesis using \(inter_bb2, inter_cont2, inter_state2) = (BigBlock name [] (Some (WhileWrapper str)) tr, cont0, Normal ns3)\ by fastforce + qed auto + hence "(A,M,\,\,\,T \((BigBlock name [] (Some str) tr), KEndBlock cont0, Normal ns3) -n\^l3 (reached_bb, reached_cont, reached_state)) \ (l = Suc (Suc (Suc l3)))" + using \l = Suc (Suc (Suc l3))\ rest by blast + thus ?thesis by blast + qed + qed +qed + +lemma ending_after_skipping_endblock_and_unwrapping: + assumes "j = Suc j'" + and "A,M,\,\,\,T \(bb, + KEndBlock (KSeq (BigBlock None [] (Some (WhileWrapper (ParsedWhile next_guard next_invs (next_body_bb#body_bbs)))) None) cont1), + Normal ns1'') -n\^j' + (reached_bb, reached_cont, reached_state)" + and "bb = BigBlock None [] None None" + and corr: "\m3 s3. (A,M,\,\,\,G \(Inl n, Normal ns1'') -n\* (m3, s3)) \ s3 \ Failure" + and "\m' s'. (A,M,\,\,\,G \(Inl n, Normal ns1'') -n\* (m', s')) \ + is_final_config (m', s') \ \ns_end. s' = Normal ns_end \ (expr_all_sat A \1_local \ \ ns_end) posts" + and guard_false: "(cont_guard = Some guard) \ (A,\,\,\ \ \guard,ns1''\ \ BoolV False)" + and "node_to_block G ! n = [Assume c]" + and "(UnOp Not guard) \ c" + and "List.member (out_edges(G) ! n) n1" + and "\ j'''. + j' = Suc (Suc (Suc j''')) \ + node_to_block G ! n = [Assume c] \ + (UnOp Not guard) \ c \ + List.member (out_edges(G) ! n) n1 \ + A,M,\,\,\,T \((BigBlock None [] (Some (ParsedWhile next_guard next_invs (next_body_bb#body_bbs))) None), KEndBlock cont1, Normal ns1'') -n\^j''' + (reached_bb, reached_cont, reached_state) \ + (\m' s'. A,M,\,\,\,G \(Inl n, Normal ns1'') -n\* (m', s') \ s' \ Failure) \ + (\m' s'. (A,M,\,\,\,G \(Inl n, Normal ns1'') -n\* (m', s')) \ + is_final_config (m', s') \ \ns_end. s' = Normal ns_end \ (expr_all_sat A \1_local \ \ ns_end) posts) \ + (Ast.valid_configuration A \ \ \ posts reached_bb reached_cont reached_state)" + shows "(Ast.valid_configuration A \ \ \ posts reached_bb reached_cont reached_state)" + using assms +proof - + from assms(2-3) have disj_a: + "(valid_configuration A \ \ \ posts reached_bb reached_cont reached_state) \ + (\ l3. (A,M,\,\,\,T \ ((BigBlock None [] (Some (ParsedWhile next_guard next_invs (next_body_bb#body_bbs))) None), KEndBlock cont1, Normal ns1'') + -n\^l3 (reached_bb, reached_cont, reached_state)) \ (j' = Suc (Suc (Suc l3))) )" + by (simp add: endblock_skip_wrapper) + thus ?thesis + proof cases + assume "(valid_configuration A \ \ \ posts reached_bb reached_cont reached_state)" thus ?thesis by simp + next + assume "\ ((valid_configuration A \ \ \ posts reached_bb reached_cont reached_state))" + hence skipped_endblock: + "(\ l3. (A,M,\,\,\,T \((BigBlock None [] (Some (ParsedWhile next_guard next_invs (next_body_bb#body_bbs))) None), KEndBlock cont1, Normal ns1'') + -n\^l3 (reached_bb, reached_cont, reached_state)) \ (j' = Suc (Suc (Suc l3))) )" + using disj_a by blast + thus ?thesis + proof - + obtain l3_conc where + conc_trace: "(A,M,\,\,\,T \((BigBlock None [] (Some (ParsedWhile next_guard next_invs (next_body_bb#body_bbs))) None), KEndBlock cont1, Normal ns1'') + -n\^l3_conc (reached_bb, reached_cont, reached_state))" and + succ_rel: "(j' = Suc (Suc (Suc l3_conc))) " + using skipped_endblock by blast + show ?thesis + apply (rule assms(10)) + apply (rule succ_rel) + apply (simp add: assms) + apply (rule assms(8)) + apply (rule assms(9)) + apply (rule conc_trace) + apply (simp add: corr) + apply (rule assms(5)) + apply blast+ + done + qed + qed +qed + +subsection \Local block lemmas\ +text \The following are lemmas proving local relations between various kinds of ast-bigblocks and cfg-blocks\ + +text \Local relation between an ast-bigblock starting with a non-empty set of simple commands and a cfg-block containing the same simple commands\ +lemma block_local_rel_generic: + assumes block_rel: "ast_cfg_rel guard invs bb cs2" + and "guard = None" + and "invs = []" + and Red_bb_to: "red_bigblock A M \ \ \ T (bb, cont0, (Normal ns1)) (reached_bb, reached_cont, reached_state)" + and Red_impl: "(\ s2'.((red_cmd_list A M \ \ \ cs2 (Normal ns1) s2') \ (s2' \ Failure)))" + and "bb = (BigBlock name cs1 any_str any_tr)" + and "cs1 \ Nil" + and "cs2 \ Nil" + shows "reached_state \ Failure \ + (\ns1'. reached_state = Normal ns1' \ (A,M,\,\,\ \ \cs2, Normal ns1\ [\] Normal ns1'))" + using assms +proof (induction arbitrary: ns1) + case (Rel_Main_test bb name cs1 any_str any_tr) + thus ?case + proof (cases cs1) + case Nil + then show ?thesis using \cs1 \ Nil\ by simp + next + case (Cons a list) + then have "red_bigblock A M \ \ \ T ((BigBlock name (a#list) any_str any_tr), cont0, (Normal ns1)) (reached_bb, reached_cont, reached_state)" + using Rel_Main_test by blast + then have "A,M,\,\,\ \ \(a#list), Normal ns1\ [\] reached_state" using Rel_Main_test(5) + proof cases + case RedSimpleCmds thus ?thesis by blast + qed + then have "A,M,\,\,\ \ \cs1, Normal ns1\ [\] reached_state" using Cons by simp + + then show ?thesis using Rel_Main_test by auto + qed +qed (auto) + +text \Local relation between a loop-only(no simple commands) ast-bigblock and a corresponding cfg-block containing assertions of the loop invariants\ +lemma block_local_rel_loop_head: + assumes block_rel: "ast_cfg_rel None assert_invs bb assertions" + and "bb = (BigBlock name [] (Some (ParsedWhile loop_guard invs (bb0#body_bbs))) any_tr)" + and "assert_invs = map Assert invs" + and Red_bb: "red_bigblock A M \ \ \ T (bb, cont0, (Normal ns1)) (reached_bb, reached_cont, reached_state)" + and Red_impl: "(\ s2'.((red_cmd_list A M \ \ \ assertions (Normal ns1) s2') \ (s2' \ Failure)))" + shows "reached_state \ Failure \ + (\ns1'. reached_state = Normal ns1' \ (A,M,\,\,\ \ \assertions, Normal ns1\ [\] Normal ns1'))" + using assms +proof cases + case Rel_Invs + hence "assertions = map Assert invs" using assms(3) by simp + from Red_bb show ?thesis + proof cases + case RedParsedWhileTrue + thus ?thesis using \assertions = (map Assert invs)\ + by (simp add: asserts_hold_if_invs_hold assms(2)) + next + case RedParsedWhileFalse + thus ?thesis using \assertions = (map Assert invs)\ + by (simp add: asserts_hold_if_invs_hold assms(2)) + next + case RedParsedWhile_InvFail + thus ?thesis + using Red_impl \assertions = map Assert invs\ one_inv_fails_assertions assms(2) + by blast + qed (auto simp add: assms(2)) +next + case Rel_Main_test + hence "assertions = map Assert invs" + using assms(2-3) by simp + from Red_bb show ?thesis + proof cases + case RedParsedWhileTrue + thus ?thesis using \assertions = (map Assert invs)\ + by (simp add: asserts_hold_if_invs_hold assms(2)) + next + case RedParsedWhileFalse + thus ?thesis using \assertions = (map Assert invs)\ + by (simp add: asserts_hold_if_invs_hold assms(2)) + next + case RedParsedWhile_InvFail + thus ?thesis using Red_impl \assertions = map Assert invs\ one_inv_fails_assertions assms(2) + by blast + qed (auto simp add: assms(2)) +qed + +subsection \Global block lemmas\ + +text \The following are lemmas proving global relations between various kinds of ast-bigblocks and cfg-blocks\ + +text \Global lemma for a big block, which concludes the program.\ +lemma generic_ending_block_global_rel: + assumes syn_rel: "ast_cfg_rel None [] bb cs2" + and j_step_ast_trace: "A,M,\,\,\,T \ (bb, cont0, (Normal ns1)) -n\^j (reached_bb, reached_cont, reached_state)" + and "bb = (BigBlock name cs1 None any_tr)" + and "((any_tr = None)) \ (any_tr = (Some Return))" + and ending: "any_tr = None \ cont0 = KStop" + and node_to_block_assm: "node_to_block(G) ! n = related_block" + and block_id: + "(related_block = cs2) \ + (related_block = c#cs2) \ c = Assume guard \ (red_expr A \ \ \ guard ns1 (BoolV True)) \ + (related_block = c#cs2) \ c = Assume not_guard \ (UnOp Not guard \ not_guard) \ (red_expr A \ \ \ guard ns1 (BoolV False))" + and "out_edges G ! n = []" + and cfg_reaches_not_failure: "\ m' s'. (red_cfg_multi A M \ \ \ G ((Inl n),(Normal ns1)) (m',s')) \ (s' \ Failure)" + and cfg_satisfies_posts: "\ m' s'. (red_cfg_multi A M \ \ \ G ((Inl n),(Normal ns1)) (m',s')) \ + is_final_config (m',s') \ (\ ns_end. s' = Normal ns_end \ (expr_all_sat A \ \ \ ns_end) post_invs)" + and local_rel: "\ step_bb step_cont step_state. + red_bigblock A M \ \ \ T (bb, KStop, (Normal ns1)) (step_bb, step_cont, step_state) \ + (\ s2'.((red_cmd_list A M \ \ \ (node_to_block(G) ! n) (Normal ns1) s2') \ (s2' \ Failure))) \ + step_state \ Failure \ + (\ns1'. step_state = Normal ns1' \ (A,M,\,\,\ \ \node_to_block(G) ! n, Normal ns1\ [\] Normal ns1'))" + shows "(valid_configuration A \ \ \ post_invs reached_bb reached_cont reached_state)" + using assms +proof (cases cs2) + case Nil + hence "cs1 = []" using ast_cfg_rel.cases syn_rel assms(3) by blast + thus ?thesis + proof (cases any_tr) + case None thus ?thesis + proof - + have complete: "(red_cfg_multi A M \ \ \ G ((Inl n),(Normal ns1)) (Inr (), Normal ns1))" + using block_id \out_edges G ! n = []\ Nil node_to_block_assm + by (metis RedCmdListNil RedNormalReturn push_through_assumption0 push_through_assumption1 r_into_rtranclp) + hence "(expr_all_sat A \ \ \ ns1) post_invs" using cfg_satisfies_posts + using is_final_config.simps(2) by blast + thus ?thesis using complete Ast.valid_configuration_def + by (metis None Pair_inject \cs1 = []\ assms(3) cfg_satisfies_posts ending final_is_static_propagate is_final.simps(1) is_final_config.simps(2) j_step_ast_trace relpowp_imp_rtranclp state.distinct(1)) + qed + next + case (Some a) + then show ?thesis + proof (cases j) + case 0 + from this j_step_ast_trace assms(3) + have "(reached_bb, reached_cont, reached_state) = ((BigBlock name [] None (Some Return)), cont0, (Normal ns1))" + using \cs1 = []\ Some assms(4) by simp + then show ?thesis by (simp add: valid_configuration_def) + next + case (Suc j') + thus ?thesis + proof (cases a) + case (Return) + from Suc j_step_ast_trace assms(3) obtain inter_bb inter_cont inter_state where + step0: "A,M,\,\,\,T \ \((BigBlock name cs1 None any_tr), cont0, (Normal ns1))\ \ (inter_bb, inter_cont, inter_state)" and + rest0: "A,M,\,\,\,T \ (inter_bb, inter_cont, inter_state) -n\^j' (reached_bb, reached_cont, reached_state)" + by (metis prod_cases3 relpowp_Suc_D2) + from cfg_reaches_not_failure have + cfg_local: "(\ s2'.((red_cmd_list A M \ \ \ (node_to_block(G) ! n) (Normal ns1) s2') \ (s2' \ Failure)))" + using assms(5) dag_verifies_propagate_2 by blast + + from step0 Return assms(3) Some Nil syn_rel have + inter_state_resolution: "inter_state = Normal ns1" + proof cases + case RedReturn + thus ?thesis by (simp add: RedReturn) + qed (auto simp add: \cs1 = []\) + + from this cfg_local step0 have + "inter_state \ Failure \ + (\ns1'. inter_state = Normal ns1' \ (A,M,\,\,\ \ \node_to_block(G) ! n, Normal ns1\ [\] Normal ns1'))" + using assms by (metis RedReturn \cs1 = []\) + + from step0 have inter_conc: "(inter_bb, inter_cont, inter_state) = ((BigBlock name [] None None), KStop, Normal ns1)" + using \cs1 = []\ Return Some + by (cases) auto + + hence "(red_cfg A M \ \ \ G ((Inl n),(Normal ns1)) (Inr (), Normal ns1))" + by (simp add: RedNormalReturn + \inter_state \ Failure \ (\ns1'. inter_state = Normal ns1' \ A,M,\,\,\ \ \node_to_block G ! n,Normal ns1\ [\] Normal ns1')\ + assms(8)) + + hence "(red_cfg_multi A M \ \ \ G ((Inl n),(Normal ns1)) (Inr (), Normal ns1))" by simp + hence "(expr_all_sat A \ \ \ ns1) post_invs" + using cfg_satisfies_posts is_final_config.simps(2) by blast + then have "is_final (inter_bb, inter_cont, inter_state)" + using inter_conc is_final.simps(1) by blast + then have "(valid_configuration A \ \ \ post_invs inter_bb inter_cont inter_state)" + unfolding valid_configuration_def + apply (simp only: get_state.simps) + apply (simp add: inter_conc) + using \(expr_all_sat A \ \ \ ns1) post_invs\ expr_all_sat_def inter_conc by blast + then show ?thesis + by (metis \is_final (inter_bb, inter_cont, inter_state)\ final_is_static_propagate inter_conc prod.sel(1) prod.sel(2) relpowp_imp_rtranclp rest0) + next + case (Goto x3) + thus ?thesis using assms(4) Some by blast + qed + qed + qed +next + case (Cons) + hence "cs1 \ []" using ast_cfg_rel.simps syn_rel assms(3) by blast + thus ?thesis + proof (cases j) + case 0 + from this j_step_ast_trace assms(3) + have eq: "(reached_bb, reached_cont, reached_state) = ((BigBlock name cs1 None any_tr), cont0, (Normal ns1))" by simp + then show ?thesis + proof (cases any_tr) + case None + then show ?thesis using eq \cs1 \ []\ Ast.valid_configuration_def get_state.simps + by (metis is_final.simps(2) list.collapse state.distinct(1)) + next + case (Some a) + then show ?thesis + proof (cases a) + case (Goto x1) + then show ?thesis using Some assms(4) by blast + next + case Return + then show ?thesis using eq Some by (simp add: Ast.valid_configuration_def) + qed + qed + next + case (Suc j') + from this j_step_ast_trace assms(3) obtain inter_bb inter_cont inter_state where + step: "A,M,\,\,\,T \ \((BigBlock name cs1 None any_tr), cont0, (Normal ns1))\ \ (inter_bb, inter_cont, inter_state)" and + rest: "A,M,\,\,\,T \ (inter_bb, inter_cont, inter_state) -n\^j' (reached_bb, reached_cont, reached_state)" + by (metis prod_cases3 relpowp_Suc_D2) + then show ?thesis + proof (cases any_tr) + case None + from step this have concrete_inter: "(inter_bb, inter_cont, inter_state) = (BigBlock name [] None None, cont0, inter_state)" + by (cases) (auto simp add: RedSimpleCmds ending) + + have Red_impl: "(\ s2'.((red_cmd_list A M \ \ \ (node_to_block(G) ! n) (Normal ns1) s2') \ (s2' \ Failure)))" + using assms(5) cfg_reaches_not_failure dag_verifies_propagate_2 by blast + + have "cont0 = KStop" using None by (simp add: ending) + + from step \cont0 = KStop\ have local_corr: + "inter_state \ Failure \ + (\ns1'. inter_state = Normal ns1' \ (A,M,\,\,\ \ \node_to_block(G) ! n, Normal ns1\ [\] Normal ns1'))" + using Red_impl block_local_rel_generic local.Cons local.step syn_rel assms by (cases) blast+ + + hence "(\ns1'. inter_state = Normal ns1' \ red_cfg A M \ \ \ G ((Inl n),(Normal ns1)) (Inr (), Normal ns1'))" + by (simp add: RedCmdListNil RedNormalReturn assms(7-8) local.Cons) + + hence "(\ns1'. inter_state = Normal ns1' \ red_cfg_multi A M \ \ \ G ((Inl n),(Normal ns1)) (Inr (), Normal ns1'))" + by blast + hence posts_sat: "\ns1'. inter_state = Normal ns1' \ (expr_all_sat A \ \ \ ns1') post_invs" + using cfg_satisfies_posts is_final_config.simps(2) by blast + + have "is_final (inter_bb, inter_cont, inter_state)" using concrete_inter ending \cont0 = KStop\ by simp + + hence valid_inter: "(valid_configuration A \ \ \ post_invs inter_bb inter_cont inter_state)" + unfolding valid_configuration_def + using posts_sat local_corr by auto + + then show ?thesis + by (metis Pair_inject \is_final (inter_bb, inter_cont, inter_state)\ concrete_inter final_is_static_propagate relpowp_imp_rtranclp rest) + next + case (Some transfer) + then show ?thesis + proof (cases transfer) + case (Goto x1) + then show ?thesis using Some assms(4) by blast + next + case (Return) + from step this Some have concrete_inter: "(inter_bb, inter_cont, inter_state) = (BigBlock name [] None (Some Return), cont0, inter_state)" + proof cases + case RedSimpleCmds thus ?thesis using Return Some by blast + qed (auto simp add: \cs1 \ []\) + + have Red_impl: "(\ s2'.((red_cmd_list A M \ \ \ (node_to_block(G) ! n) (Normal ns1) s2') \ (s2' \ Failure)))" + using dag_verifies_propagate_2 assms(5) cfg_reaches_not_failure by blast + + from step have local_corr: + "inter_state \ Failure \ + (\ns1'. inter_state = Normal ns1' \ (A,M,\,\,\ \ \node_to_block(G) ! n, Normal ns1\ [\] Normal ns1'))" + using Red_impl \cs1 \ []\ assms(3) block_id block_local_rel_generic list.distinct(1) + local.Cons node_to_block_assm push_through_assumption0 push_through_assumption1 syn_rel + by metis + + hence "(\ns1'. inter_state = Normal ns1' \ red_cfg A M \ \ \ G ((Inl n),(Normal ns1)) (Inr (), Normal ns1'))" + by (simp add: RedCmdListNil RedNormalReturn assms(7-8) local.Cons) + + hence "(\ns1'. inter_state = Normal ns1' \ red_cfg_multi A M \ \ \ G ((Inl n),(Normal ns1)) (Inr (), Normal ns1'))" by blast + hence posts_sat: "\ns1'. inter_state = Normal ns1' \ (expr_all_sat A \ \ \ ns1') post_invs" + using cfg_satisfies_posts is_final_config.simps(2) by blast + + from step have "inter_state \ Failure" using Red_impl block_local_rel_generic local.Cons assms + using local_corr by fastforce + + then show ?thesis + proof (cases inter_state) + case (Normal x1) + then show ?thesis + proof (cases j') + case 0 + then show ?thesis using concrete_inter + by (metis Ast.valid_configuration_def \inter_state \ Failure\ get_state.simps is_final.simps(4) relpowp_0_E rest) + next + case (Suc j'') + from this rest obtain inter_bb2 inter_cont2 inter_state2 where + snd_step: "A,M,\,\,\,T \ \(inter_bb, inter_cont, inter_state)\ \ (inter_bb2, inter_cont2, inter_state2)" and + snd_rest: "A,M,\,\,\,T \ (inter_bb2, inter_cont2, inter_state2) -n\^j'' (reached_bb, reached_cont, reached_state)" + by (metis get_state.cases relpowp_Suc_E2) + then have inter2_conc: "(inter_bb2, inter_cont2, inter_state2) = ((BigBlock name [] None None), KStop, inter_state)" + using concrete_inter \inter_state \ Failure\ Normal + by (cases) blast+ + hence "is_final (inter_bb2, inter_cont2, inter_state2)" by simp + hence valid_inter: "(valid_configuration A \ \ \ post_invs inter_bb2 inter_cont2 inter_state2)" + using Ast.valid_configuration_def \inter_state \ Failure\ inter2_conc posts_sat by blast + then show ?thesis + by (metis \is_final (inter_bb2, inter_cont2, inter_state2)\ final_is_static_propagate inter2_conc prod.inject relpowp_imp_rtranclp snd_rest) + qed + next + case Failure + then show ?thesis using \inter_state \ Failure\ by simp + next + case Magic + then show ?thesis by (metis valid_configuration_def \inter_state \ Failure\ magic_propagates rest state.simps(5)) + qed + qed + qed + qed +qed + +text \Global lemma for a big block with a non-empty set of simple commands that enters a loop after it executes its simple cmds.\ +lemma block_global_rel_while_successor: + assumes j_step_ast_trace: + "A,M,\,\,\,T \ (bb, cont1, Normal ns1) -n\^j (reached_bb, reached_cont, reached_state)" + and syn_rel: "ast_cfg_rel None [] bb cmds" + and "bb = (BigBlock name cmds (Some (WhileWrapper (ParsedWhile guard invs (body_bb0#body_bbs)))) None)" + and "cmds \ []" + and "node_to_block(G) ! n = related_block" + and block_id: + "(related_block = cmds) \ + (related_block = c#cmds) \ c = Assume entry_guard \ (red_expr A \ \ \ entry_guard ns1 (BoolV True)) \ + (related_block = c#cmds) \ c = Assume not_guard \ (UnOp Not entry_guard \ not_guard) \ (red_expr A \ \ \ entry_guard ns1 (BoolV False))" + and cfg_is_correct: "\ m' s'. (red_cfg_multi A M \ \ \ G ((Inl n),(Normal ns1)) (m',s')) \ (s' \ Failure)" + and cfg_satisfies_posts: "\ m' s'. (red_cfg_multi A M \ \ \ G ((Inl n),(Normal ns1)) (m',s')) \ + is_final_config (m',s') \ (\ ns_end. s' = Normal ns_end \ (expr_all_sat A \ \ \ ns_end) posts)" + and block_local_rel: + "\ reached_bb_inter reached_cont_inter reached_state_inter. + (red_bigblock A M \ \ \ T (bb, cont1, (Normal ns1)) (reached_bb_inter, reached_cont_inter, reached_state_inter)) \ + (\ s2'.((red_cmd_list A M \ \ \ (node_to_block G ! n) (Normal ns1) s2') \ (s2' \ Failure))) \ + (reached_state_inter \ Failure \ (\ns1'. reached_state_inter = Normal ns1' \ (A,M,\,\,\ \ \(node_to_block G ! n), Normal ns1\ [\] Normal ns1')))" + and global_rel_succ: + "\ ns2 k. + k < j \ + (\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m3 s3. (A,M,\,\,\,G \ (Inl msuc2, Normal ns2) -n\* (m3, s3)) \ s3 \ Failure)) \ + (\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m' s'. (A,M,\,\,\,G \(Inl msuc2, Normal ns2) -n\* (m', s')) \ + is_final_config (m', s') \ + (\ns_end. s' = Normal ns_end \ (expr_all_sat A \ \ \ ns_end) posts))) \ + A,M,\,\,\,T \ ((BigBlock name [] (Some (ParsedWhile guard invs (body_bb0#body_bbs))) None), KEndBlock cont1, Normal ns2) -n\^k + (reached_bb, reached_cont, reached_state) \ + (valid_configuration A \ \ \ posts reached_bb reached_cont reached_state)" + shows "(valid_configuration A \ \ \ posts reached_bb reached_cont reached_state)" + using assms +proof cases + assume "j = 0" + then have "(reached_bb, reached_cont, reached_state) = + ((BigBlock name cmds (Some (WhileWrapper (ParsedWhile guard invs (body_bb0#body_bbs)))) None), cont1, Normal ns1)" using j_step_ast_trace assms(3) by auto + thus ?thesis by (simp add: valid_configuration_def) +next + assume "j \ 0" + from this obtain j' where "j = Suc j'" using not0_implies_Suc by blast + from this j_step_ast_trace assms(3) obtain inter_bb inter_cont inter_state where + first_step: "A,M,\,\,\,T \ \((BigBlock name cmds (Some (WhileWrapper (ParsedWhile guard invs (body_bb0#body_bbs)))) None), cont1, Normal ns1)\ \ (inter_bb, inter_cont, inter_state)" and + rest: "A,M,\,\,\,T \ (inter_bb, inter_cont, inter_state) -n\^j' (reached_bb, reached_cont, reached_state)" + by (metis (no_types) get_state.cases relpowp_Suc_D2) + from this have a1: "(inter_bb, inter_cont, inter_state) = ((BigBlock name [] (Some (WhileWrapper (ParsedWhile guard invs (body_bb0#body_bbs)))) None), cont1, inter_state)" + proof cases + case RedSimpleCmds thus ?thesis by blast + qed (auto simp add: \cmds \ []\) + have Red_impl: "(\ s2'.((red_cmd_list A M \ \ \ (node_to_block G ! n) (Normal ns1) s2') \ (s2' \ Failure)))" using dag_verifies_propagate_2 cfg_is_correct assms(5) + by blast + have local_conclusion: "inter_state \ Failure \ (\ns1'. inter_state = Normal ns1' \ (A,M,\,\,\ \ \(node_to_block G ! n), Normal ns1\ [\] Normal ns1'))" + using Red_impl first_step assms(3-4) block_local_rel_generic syn_rel block_local_rel by blast + show ?thesis + proof (cases inter_state) + case (Normal x1) + hence "(A,M,\,\,\ \ \(node_to_block G ! n), Normal ns1\ [\] inter_state)" using local_conclusion by blast + then show ?thesis + proof (cases j') + case 0 + then show ?thesis + by (metis Normal a1 nat.discI rest wrapper_to_endblock) + next + case 2: (Suc j'') + hence Red_cfg_conc: + "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m3 s3. (A,M,\,\,\,G \ (Inl msuc2, inter_state) -n\* (m3, s3)) \ s3 \ Failure))" + using dag_verifies_propagate Normal \A,M,\,\,\ \ \(node_to_block G ! n),Normal ns1\ [\] inter_state\ assms(5) cfg_is_correct + by blast + + hence Red_cfg_sat_conc: + "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m' s'. (A,M,\,\,\,G \(Inl msuc2, inter_state) -n\* (m', s')) \ + is_final_config (m', s') \ + (\ns_end. s' = Normal ns_end \ (expr_all_sat A \ \ \ ns_end) posts)))" + by (metis (no_types) Normal RedNormalSucc cfg_satisfies_posts converse_rtranclp_into_rtranclp local_conclusion) + + from 2 j_step_ast_trace assms(3) obtain inter_bb2 inter_cont2 inter_state2 where + first_step_2: "A,M,\,\,\,T \ \(inter_bb, inter_cont, inter_state)\ \ (inter_bb2, inter_cont2, inter_state2)" and + rest_2: "A,M,\,\,\,T \ (inter_bb2, inter_cont2, inter_state2) -n\^j'' (reached_bb, reached_cont, reached_state)" + by (metis get_state.cases relpowp_Suc_E2 rest) + from this have a3: "(inter_bb2, inter_cont2, inter_state2) = + ((BigBlock name [] (Some (ParsedWhile guard invs (body_bb0#body_bbs))) None), KEndBlock cont1, inter_state)" + using a1 Normal + proof cases + case RedParsedWhileWrapper + thus ?thesis using a1 by fastforce + qed auto + + have "j'' < j" by (simp add: "2" \j = Suc j'\) + then show ?thesis using a3 rest_2 Normal Red_cfg_conc assms(9) cfg_satisfies_posts Red_cfg_sat_conc global_rel_succ + by fastforce + qed + next + case Failure + then show ?thesis using local_conclusion by blast + next + case Magic + then show ?thesis by (metis valid_configuration_def local_conclusion magic_propagates rest state.simps(5)) + qed +qed + +text \Global lemma for a big block that's the head of a loop. + This means that it is a big block with a while-loop as its structured command and its set of simple commands is empty. + The body of the loop is required to be non-empty.\ +lemma block_global_rel_loop_head: + assumes block_rel: "ast_cfg_rel None assertions bb assertions" + and ast_trace: "A,M,\,\,\,T \ (bb, cont0, (Normal ns1)) -n\^j (reached_bb, reached_cont, reached_state)" + and cfg_correct: "(\ m2 s2. ((red_cfg_multi A M \ \ \ G (Inl n, Normal ns1) (m2, s2)) \ (s2 \ Failure)))" + and cfg_satisfies_post: "(\ m2 s2. (red_cfg_multi A M \ \ \ G (Inl n, Normal ns1) (m2, s2)) \ + is_final_config (m2, s2) \ \ns_end. s2 = Normal ns_end \ (expr_all_sat A \ \ \ ns_end) posts)" + and "bb = (BigBlock name [] any_str any_tr)" + and bb_successor_while: "any_str = Some (ParsedWhile cont_guard invs (bb0#body_bbs))" + and block_local_rel: + "\ reached_bb_inter reached_cont_inter reached_state_inter. + (red_bigblock A M \ \ \ T (bb, cont0, (Normal ns1)) (reached_bb_inter, reached_cont_inter, reached_state_inter)) \ + (\ s2'.((red_cmd_list A M \ \ \ assertions (Normal ns1) s2') \ + (s2' \ Failure))) \ + reached_state_inter \ Failure \ + (\ns1'. reached_state_inter = Normal ns1' \ (A,M,\,\,\ \ \assertions, Normal ns1\ [\] Normal ns1'))" + and "node_to_block(G) ! n = assertions" + and "cont0 = KEndBlock cont1" + and succ_correct: + "\ ns1'' loop_guard j'. + j = Suc j' \ + (\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m3 s3. ((A,M,\,\,\,G \ (Inl(msuc2), Normal ns1'') -n\* (m3, s3)) \ s3 \ Failure))) \ + (\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m' s'. ((A,M,\,\,\,G \(Inl (msuc2), Normal ns1'') -n\* (m', s')) \ + is_final_config (m', s') \ + (\ns_end. s' = Normal ns_end \ (expr_all_sat A \ \ \ ns_end) posts)))) \ + ((cont_guard = Some loop_guard) \ + (red_expr A \ \ \ loop_guard ns1'' (BoolV True)) \ + A,M,\,\,\,T \ (bb0, convert_list_to_cont (( body_bbs)@[bb]) (KEndBlock cont1), (Normal ns1'')) -n\^j' (reached_bb, reached_cont, reached_state)) \ + ((cont_guard = Some loop_guard) \ + (red_expr A \ \ \ loop_guard ns1'' (BoolV False)) \ + A,M,\,\,\,T \ ((BigBlock name [] None None), KEndBlock cont1, (Normal ns1'')) -n\^j' (reached_bb, reached_cont, reached_state)) \ + ((cont_guard = None) \ + ((A,M,\,\,\,T \ ((BigBlock name [] None None), KEndBlock cont1, (Normal ns1'')) -n\^j' (reached_bb, reached_cont, reached_state)) \ + (A,M,\,\,\,T \ (bb0, convert_list_to_cont (( body_bbs)@[bb]) (KEndBlock cont1), (Normal ns1'')) -n\^j' (reached_bb, reached_cont, reached_state)))) \ + (Ast.valid_configuration A \ \ \ posts reached_bb reached_cont reached_state)" + shows "(Ast.valid_configuration A \ \ \ posts reached_bb reached_cont reached_state)" + using assms cases +proof - + show ?thesis + proof cases + assume "j = 0" + hence "(reached_bb, reached_cont, reached_state) = ((BigBlock name [] any_str any_tr), cont0, (Normal ns1))" using ast_trace assms(5) by simp + thus ?thesis by (simp add: Ast.valid_configuration_def \cont0 = KEndBlock cont1\) + next + assume "j \ 0" + from this obtain j' where "j = Suc j'" using not0_implies_Suc by blast + + from ast_trace this assms(5) obtain inter_bb inter_cont inter_state where + first_step: "A,M,\,\,\,T \ \((BigBlock name [] any_str any_tr), cont0, (Normal ns1))\ \ (inter_bb, inter_cont, inter_state)" and + rest: "A,M,\,\,\,T \ (inter_bb, inter_cont, inter_state) -n\^j' (reached_bb, reached_cont, reached_state)" + by (metis prod_cases3 relpowp_Suc_D2) + + show ?thesis + proof (cases cont_guard) + case None + from first_step show ?thesis using bb_successor_while + proof cases + case RedParsedWhileTrue + hence concrete_inter1: "(inter_bb, inter_cont, inter_state) = (bb0, convert_list_to_cont (( body_bbs)@[(BigBlock name [] any_str any_tr)]) cont0, (Normal ns1))" + using bb_successor_while None by blast + + from first_step + have succ_cfg_correct: "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m3 s3. ((A,M,\,\,\,G \ (Inl(msuc2), inter_state) -n\* (m3, s3)) \ s3 \ Failure)))" + by (metis Pair_inject assms(5) assms(8) block_local_rel cfg_correct concrete_inter1 dag_verifies_propagate dag_verifies_propagate_2) + + from first_step + have succ_cfg_satisfies_post: + "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ + (\m' s'. ((A,M,\,\,\,G \(Inl (msuc2), inter_state) -n\* (m', s')) \ + is_final_config (m', s') \ + (\ns_end. s' = Normal ns_end \ (expr_all_sat A \ \ \ ns_end) posts))) )" + using cfg_satisfies_post + by (metis (no_types) RedNormalSucc assms(5) assms(8) block_local_rel cfg_correct converse_rtranclp_into_rtranclp dag_verifies_propagate_2 local.RedParsedWhileTrue(4)) + + show ?thesis using \j = Suc j'\ succ_cfg_correct succ_cfg_satisfies_post None rest concrete_inter1 succ_correct assms(5) \cont0 = KEndBlock cont1\ by blast + next + case RedParsedWhileFalse + hence concrete_inter2: "(inter_bb, inter_cont, inter_state) = ((BigBlock name [] None None), cont0, (Normal ns1))" by simp + + from first_step + have succ_cfg_correct: "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m3 s3. ((A,M,\,\,\,G \ (Inl(msuc2), inter_state) -n\* (m3, s3)) \ s3 \ Failure)))" + by (metis assms(5) assms(8) block_local_rel cfg_correct dag_verifies_propagate dag_verifies_propagate_2 local.RedParsedWhileFalse(5)) + + from first_step + have succ_cfg_satisfies_post: + "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ + (\m' s'. ((A,M,\,\,\,G \(Inl (msuc2), inter_state) -n\* (m', s')) \ + is_final_config (m', s') \ + (\ns_end. s' = Normal ns_end \ (expr_all_sat A \ \ \ ns_end) posts))) )" + using cfg_satisfies_post + by (metis (no_types) RedNormalSucc assms(5) assms(8) block_local_rel cfg_correct converse_rtranclp_into_rtranclp dag_verifies_propagate_2 local.RedParsedWhileFalse(5)) + + show ?thesis using \j = Suc j'\ succ_cfg_correct succ_cfg_satisfies_post None rest concrete_inter2 succ_correct \cont0 = KEndBlock cont1\ by blast + next + case RedParsedWhile_InvFail thus ?thesis using assms(8) block_local_rel cfg_correct dag_verifies_propagate_2 first_step assms(5) by blast + qed auto + next + case (Some concrete_loop_guard) + then show ?thesis + proof cases + assume guard_true: "(red_expr A \ \ \ concrete_loop_guard ns1 (BoolV True))" + hence guard_not_false: "\ (red_expr A \ \ \ concrete_loop_guard ns1 (BoolV False))" using expr_eval_determ by blast + + from first_step show ?thesis + proof cases + case RedParsedWhileTrue + hence concrete_inter3: "(inter_bb, inter_cont, inter_state) = (bb0, convert_list_to_cont (( body_bbs)@[(BigBlock name [] any_str any_tr)]) (cont0), (Normal ns1))" + using bb_successor_while Some by blast + + from first_step + have succ_cfg_correct: "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m3 s3. ((A,M,\,\,\,G \ (Inl(msuc2), inter_state) -n\* (m3, s3)) \ s3 \ Failure)))" + by (metis Pair_inject assms(5) assms(8) block_local_rel cfg_correct concrete_inter3 dag_verifies_propagate dag_verifies_propagate_2) + + from first_step + have succ_cfg_satisfies_post: + "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ + (\m' s'. ((A,M,\,\,\,G \(Inl (msuc2), inter_state) -n\* (m', s')) \ + is_final_config (m', s') \ + (\ns_end. s' = Normal ns_end \ (expr_all_sat A \ \ \ ns_end) posts))) )" + using cfg_satisfies_post + by (metis (no_types) RedNormalSucc assms(5) assms(8) block_local_rel cfg_correct converse_rtranclp_into_rtranclp dag_verifies_propagate_2 local.RedParsedWhileTrue(4)) + + show ?thesis using \j = Suc j'\ succ_cfg_correct succ_cfg_satisfies_post Some guard_true rest concrete_inter3 succ_correct assms(5) \cont0 = KEndBlock cont1\ by blast + next + case RedParsedWhile_InvFail thus ?thesis using assms(8) block_local_rel cfg_correct dag_verifies_propagate_2 first_step assms(5) by blast + qed (auto simp add: bb_successor_while Some guard_not_false) + next + assume guard_not_true: "\ (red_expr A \ \ \ concrete_loop_guard ns1 (BoolV True))" + thus ?thesis + proof cases + assume guard_false: "(red_expr A \ \ \ concrete_loop_guard ns1 (BoolV False))" + + from first_step show ?thesis + proof cases + case RedParsedWhileFalse + hence concrete_inter4: "(inter_bb, inter_cont, inter_state) = ((BigBlock name [] None None), cont0, (Normal ns1))" by simp + + from first_step + have succ_cfg_correct: "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m3 s3. ((A,M,\,\,\,G \ (Inl(msuc2), inter_state) -n\* (m3, s3)) \ s3 \ Failure)))" + by (metis assms(5) assms(8) block_local_rel cfg_correct dag_verifies_propagate dag_verifies_propagate_2 local.RedParsedWhileFalse(5)) + + from first_step + have succ_cfg_satisfies_post: + "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ + (\m' s'. (((A,M,\,\,\,G \(Inl (msuc2), inter_state) -n\* (m', s'))) \ + is_final_config (m', s') \ + (\ns_end. s' = Normal ns_end \ (expr_all_sat A \ \ \ ns_end) posts))) )" + using cfg_satisfies_post + by (metis (no_types) RedNormalSucc assms(5) assms(8) block_local_rel cfg_correct converse_rtranclp_into_rtranclp dag_verifies_propagate_2 local.RedParsedWhileFalse(5)) + + show ?thesis using \j = Suc j'\ succ_cfg_correct succ_cfg_satisfies_post Some guard_false rest concrete_inter4 succ_correct \cont0 = KEndBlock cont1\ by blast + next + case RedParsedWhile_InvFail thus ?thesis using Some bb_successor_while guard_not_true by blast + qed (auto simp add: bb_successor_while Some guard_not_true) + next + assume guard_not_false: "\ (red_expr A \ \ \ concrete_loop_guard ns1 (BoolV False))" + from first_step show ?thesis + proof cases + case RedParsedWhile_InvFail thus ?thesis using Some bb_successor_while guard_not_true by blast + qed (auto simp add: bb_successor_while Some guard_not_true guard_not_false) + qed + qed + qed + qed +qed + +text \Global lemma for a big block, which enters an if-statement after executing its simple cmds (if there are any).\ +lemma block_global_rel_if_successor: + assumes block_rel: "ast_cfg_rel None [] bb cs2" + and ast_trace: "A,M,\,\,\,T \ (bb, cont0, (Normal ns1)) -n\^j (reached_bb, reached_cont, reached_state)" + and "bb = (BigBlock name cs1 any_str any_tr)" + and "node_to_block(G) ! n = related_block" + and block_id: + "(related_block = cs2) \ + (related_block = c#cs2) \ c = Assume guard \ (red_expr A \ \ \ guard ns1 (BoolV True)) \ + (related_block = c#cs2) \ c = Assume not_guard \ (UnOp Not guard \ not_guard) \ (red_expr A \ \ \ guard ns1 (BoolV False))" + and cfg_correct: "(\ m2 s2. ((red_cfg_multi A M \ \ \ G (Inl n, Normal ns1) (m2, s2)) \ (s2 \ Failure)))" + and cfg_satisfies_post: "(\ m2 s2. (red_cfg_multi A M \ \ \ G (Inl n, Normal ns1) (m2, s2)) \ + is_final_config (m2, s2) \ \ns_end. s2 = Normal ns_end \ (expr_all_sat A \ \ \ ns_end) posts)" + and bb_successor_if: "any_str = Some (ParsedIf cont_guard (then0#then_bbs) (else0#else_bbs))" + and block_local_rel: + "\ reached_bb_inter reached_cont_inter reached_state_inter. (red_bigblock A M \ \ \ T ((BigBlock name cs1 any_str any_tr), cont0, (Normal ns1)) (reached_bb_inter, reached_cont_inter, reached_state_inter)) \ + (\ s2'.((red_cmd_list A M \ \ \ (node_to_block(G) ! n) (Normal ns1) s2') \ (s2' \ Failure))) \ + cs1 \ [] \ cs2 \ [] \ + (reached_state_inter \ Failure \ (\ns1'. reached_state_inter = Normal ns1' \ (A,M,\,\,\ \ \(node_to_block(G) ! n), Normal ns1\ [\] Normal ns1')))" + and succ_correct: + "\ ns1'' block_guard k. + k < j \ + (\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m3 s3. ((A,M,\,\,\,G \ (Inl(msuc2), Normal ns1'') -n\* (m3, s3)) \ s3 \ Failure))) \ + (\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m' s'. ((A,M,\,\,\,G \(Inl (msuc2), Normal ns1'') -n\* (m', s')) \ + is_final_config (m', s') \ + (\ns_end. s' = Normal ns_end \ (expr_all_sat A \ \ \ ns_end) posts)))) \ + ( (cont_guard = Some block_guard) \ + (red_expr A \ \ \ block_guard ns1'' (BoolV True)) \ + A,M,\,\,\,T \ (then0, convert_list_to_cont ( then_bbs) cont0, (Normal ns1'')) -n\^k (reached_bb, reached_cont, reached_state) ) \ + ( (cont_guard = Some block_guard) \ + (red_expr A \ \ \ block_guard ns1'' (BoolV False)) \ + A,M,\,\,\,T \ (else0, convert_list_to_cont ( else_bbs) cont0, (Normal ns1'')) -n\^k (reached_bb, reached_cont, reached_state) ) \ + ( (cont_guard = None) \ + ((A,M,\,\,\,T \ (then0, convert_list_to_cont ( then_bbs) cont0, (Normal ns1'')) -n\^k (reached_bb, reached_cont, reached_state)) \ + (A,M,\,\,\,T \ (else0, convert_list_to_cont ( else_bbs) cont0, (Normal ns1'')) -n\^k (reached_bb, reached_cont, reached_state)) ) ) \ + (Ast.valid_configuration A \ \ \ posts reached_bb reached_cont reached_state)" + shows "(Ast.valid_configuration A \ \ \ posts reached_bb reached_cont reached_state)" + using assms cases +proof cases + case Rel_Main_test + have not_end: "(cont0 \ KStop) \ any_str \ None \ any_tr \ None" using bb_successor_if by simp + show ?thesis + proof (cases cs2) + case Nil hence \cs1 = []\ by (simp add: local.Rel_Main_test(2)) + thus ?thesis using local.Nil local.Rel_Main_test(2) by auto + next + case (Cons) + hence "cs1 \ []" using assms(3) local.Rel_Main_test by auto + thus ?thesis + proof (cases j) + case 0 + hence "(reached_bb, reached_cont, reached_state) = ((BigBlock name cs1 any_str any_tr), cont0, (Normal ns1))" using ast_trace assms(3) by auto + then show ?thesis by (simp add: Ast.valid_configuration_def bb_successor_if) + next + case 1: (Suc j') + from this assms(3) obtain inter_bb inter_cont inter_state where + first_step: "red_bigblock A M \ \ \ T ((BigBlock name cs1 any_str any_tr), cont0, (Normal ns1)) (inter_bb, inter_cont, inter_state)" and + rest_of_steps: "A,M,\,\,\,T \ (inter_bb, inter_cont, inter_state) -n\^j' (reached_bb, reached_cont, reached_state)" + by (metis ast_trace get_state.cases relpowp_Suc_E2) + + from cfg_correct Cons block_id + have local_rel_corr: "(\ s2'.((red_cmd_list A M \ \ \ (cs2) (Normal ns1) s2') \ (s2' \ Failure)))" + using dag_verifies_propagate_2 + by (metis push_through_assumption0 push_through_assumption1 \node_to_block(G) ! n = related_block\) + + from local_rel_corr first_step Cons + have a2: "(inter_state \ Failure \ (\ns1'. inter_state = Normal ns1' \ (A,M,\,\,\ \ \(node_to_block G ! n), Normal ns1\ [\] Normal ns1')))" + using block_local_rel local.Rel_Main_test assms(3) + by (metis \cs1 \ []\ assume_ml bigblock.inject block_id state.simps(7) \node_to_block(G) ! n = related_block\) + + from first_step Cons \cs1 \ []\ + have a1: "(inter_bb, inter_cont, inter_state) = ((BigBlock name [] any_str any_tr), cont0, inter_state)" + proof cases + case RedSimpleCmds then show ?thesis by (auto simp add: RedSimpleCmds) + qed auto + + show ?thesis + proof (cases inter_state) + case 2: (Normal x1) + from rest_of_steps show ?thesis + proof (cases j') + case 0 + then show ?thesis + by (metis Ast.valid_configuration_def a1 a2 bb_successor_if get_state.simps is_final.simps(3) relpowp_0_E rest_of_steps) + next + case 3: (Suc j'') + from this rest_of_steps obtain snd_inter_bb snd_inter_cont snd_inter_state where + snd_step: "red_bigblock A M \ \ \ T ((BigBlock name [] any_str any_tr), cont0, inter_state) (snd_inter_bb, snd_inter_cont, snd_inter_state)" and + snd_rest_of_steps: "A,M,\,\,\,T \ (snd_inter_bb, snd_inter_cont, snd_inter_state) -n\^j'' (reached_bb, reached_cont, reached_state)" + by (metis a1 get_state.cases relpowp_Suc_D2) + + thus ?thesis + proof (cases cont_guard) + case None + from snd_step this show ?thesis + proof cases + case RedParsedIfTrue + hence eq: "(snd_inter_bb, snd_inter_cont, snd_inter_state) = (then0, convert_list_to_cont ( then_bbs) cont0, inter_state)" using None bb_successor_if 1 by auto + + from first_step + have succ_cfg_correct: "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m3 s3. ((A,M,\,\,\,G \ (Inl(msuc2), inter_state) -n\* (m3, s3)) \ s3 \ Failure)))" + proof cases + case RedSimpleCmds show ?thesis using 2 RedSimpleCmds(3) dag_verifies_propagate assms(3-4) Rel_Main_test(1) cfg_correct a2 by blast + qed (auto simp add: \cs1 \ Nil\) + + have succ_cfg_sat: "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m' s'. ((A,M,\,\,\,G \(Inl (msuc2), inter_state) -n\* (m', s')) \ + is_final_config (m', s') \ + (\ns_end. s' = Normal ns_end \ (expr_all_sat A \ \ \ ns_end) posts))))" + using cfg_satisfies_post cfg_correct local.Cons + by (metis (no_types) "2" RedNormalSucc a2 converse_rtranclp_into_rtranclp) + + have "j'' < j" using 1 3 using Suc_lessD by blast + + thus ?thesis using eq snd_rest_of_steps succ_correct None 2 succ_cfg_correct succ_cfg_sat by blast + next + case (RedParsedIfFalse) + hence eq: "(snd_inter_bb, snd_inter_cont, snd_inter_state) = (else0, convert_list_to_cont ( else_bbs) cont0, inter_state)" using None bb_successor_if 1 by auto + + from first_step + have succ_cfg_correct: "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m3 s3. ((A,M,\,\,\,G \ (Inl(msuc2), inter_state) -n\* (m3, s3)) \ s3 \ Failure)))" + proof cases + case RedSimpleCmds show ?thesis using 2 RedSimpleCmds(3) dag_verifies_propagate assms(3-4) Rel_Main_test(1) cfg_correct a2 by blast + qed (auto simp add: \cs1 \ Nil\) + + have succ_cfg_sat: "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m' s'. ((A,M,\,\,\,G \(Inl (msuc2), inter_state) -n\* (m', s')) \ + is_final_config (m', s') \ + (\ns_end. s' = Normal ns_end \ (expr_all_sat A \ \ \ ns_end) posts))))" + using cfg_satisfies_post cfg_correct local.Cons + by (metis (no_types) "2" RedNormalSucc a2 converse_rtranclp_into_rtranclp) + + have "j'' < j" using 1 3 using Suc_lessD by blast + + thus ?thesis using eq snd_rest_of_steps succ_correct None 2 succ_cfg_correct succ_cfg_sat by blast + qed (auto simp add: bb_successor_if 2) + next + case (Some block_guard) + then show ?thesis + proof cases + assume guard_true: "(red_expr A \ \ \ block_guard x1 (BoolV True))" + hence guard_not_false: "\ (red_expr A \ \ \ block_guard x1 (BoolV False))" using expr_eval_determ by blast + from snd_step have eq: "(snd_inter_bb, snd_inter_cont, snd_inter_state) = (then0, convert_list_to_cont ( then_bbs) cont0, inter_state)" + proof cases + case RedParsedIfTrue thus ?thesis using guard_true bb_successor_if by (simp add: RedParsedIfTrue) + qed (auto simp add: guard_not_false bb_successor_if 2 Some) + + from first_step + have succ_cfg_correct: "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m3 s3. ((A,M,\,\,\,G \ (Inl(msuc2), inter_state) -n\* (m3, s3)) \ s3 \ Failure)))" + proof cases + case RedSimpleCmds show ?thesis using 2 eq RedSimpleCmds(3) dag_verifies_propagate assms(3-4) Rel_Main_test(1) cfg_correct a2 by blast + qed (auto simp add: \cs1 \ Nil\) + + have succ_cfg_sat: "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m' s'. ((A,M,\,\,\,G \(Inl (msuc2), inter_state) -n\* (m', s')) \ + is_final_config (m', s') \ + (\ns_end. s' = Normal ns_end \ (expr_all_sat A \ \ \ ns_end) posts))))" + using cfg_satisfies_post cfg_correct local.Cons + by (metis (no_types) "2" RedNormalSucc a2 converse_rtranclp_into_rtranclp) + + have "j'' < j" using 1 3 using Suc_lessD by blast + + thus ?thesis using eq guard_true snd_rest_of_steps succ_correct Some succ_cfg_correct 2 succ_cfg_sat by blast + next + assume guard_not_true: "\ (red_expr A \ \ \ block_guard x1 (BoolV True))" + thus ?thesis + proof cases + assume guard_false: "(red_expr A \ \ \ block_guard x1 (BoolV False))" + from snd_step have eq: "(snd_inter_bb, snd_inter_cont, snd_inter_state) = (else0, convert_list_to_cont ( else_bbs) cont0, inter_state)" + proof cases + case RedParsedIfFalse thus ?thesis using guard_false bb_successor_if by (simp add: RedParsedIfFalse) + qed (auto simp add: guard_not_true bb_successor_if 2 Some) + + from first_step + have succ_cfg_correct: "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m3 s3. ((A,M,\,\,\,G \ (Inl(msuc2), inter_state) -n\* (m3, s3)) \ s3 \ Failure)))" + proof cases + case RedSimpleCmds show ?thesis using 2 RedSimpleCmds(3) dag_verifies_propagate assms(3-4) Rel_Main_test(1) cfg_correct a2 by blast + qed (auto simp add: \cs1 \ Nil\) + + have succ_cfg_sat: "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m' s'. ((A,M,\,\,\,G \(Inl (msuc2), inter_state) -n\* (m', s')) \ + is_final_config (m', s') \ + (\ns_end. s' = Normal ns_end \ (expr_all_sat A \ \ \ ns_end) posts))))" + using cfg_satisfies_post cfg_correct local.Cons + by (metis (no_types) "2" RedNormalSucc a2 converse_rtranclp_into_rtranclp) + + have "j'' < j" using 1 3 using Suc_lessD by blast + + thus ?thesis using eq guard_false snd_rest_of_steps succ_correct Some 2 succ_cfg_correct succ_cfg_sat by blast + next + assume guard_not_false2: "(\ (red_expr A \ \ \ block_guard x1 (BoolV False)))" and + guard_not_true2: "(\ (red_expr A \ \ \ block_guard x1 (BoolV True)))" + thus ?thesis + proof - + from snd_step have False using guard_not_false2 guard_not_true2 bb_successor_if Some 2 + by (cases) auto + thus ?thesis by simp + qed + qed + qed + qed + qed + next + case Failure + then show ?thesis + using \inter_state \ Failure \ (\ns1'. inter_state = Normal ns1' \ A,M,\,\,\ \ \(node_to_block G ! n),Normal ns1\ [\] Normal ns1')\ + by linarith + next + case Magic + then show ?thesis by (metis Ast.valid_configuration_def a2 magic_propagates rest_of_steps state.distinct(3)) + qed + qed + qed +next + case Rel_Invs + hence "cs2 = []" by simp + have not_end: "(cont0 \ KStop) \ any_str \ None \ any_tr \ None" using bb_successor_if by simp + show ?thesis + proof (cases cs2) + case Nil + thus ?thesis + proof (cases j) + case 0 + hence "(reached_bb, reached_cont, reached_state) = ((BigBlock name cs1 any_str any_tr), cont0, (Normal ns1))" using ast_trace assms(3) by auto + then show ?thesis by (simp add: Ast.valid_configuration_def bb_successor_if) + next + case 1: (Suc j') + from this assms(3) obtain snd_inter_bb snd_inter_cont snd_inter_state where + snd_step: "red_bigblock A M \ \ \ T ((BigBlock name [] any_str any_tr), cont0, (Normal ns1)) (snd_inter_bb, snd_inter_cont, snd_inter_state)" and + snd_rest_of_steps: "A,M,\,\,\,T \ (snd_inter_bb, snd_inter_cont, snd_inter_state) -n\^j' (reached_bb, reached_cont, reached_state)" + using Rel_Invs + by (metis ast_trace bigblock.inject local.Rel_Invs(1) relpowp_Suc_E2 surj_pair) + + thus ?thesis + proof (cases cont_guard) + case None + from snd_step this show ?thesis + proof cases + case RedParsedIfTrue + hence eq: "(snd_inter_bb, snd_inter_cont, snd_inter_state) = (then0, convert_list_to_cont ( then_bbs) cont0, (Normal ns1))" using None bb_successor_if 1 by auto + + have succ_cfg_correct: "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m3 s3. ((A,M,\,\,\,G \ (Inl(msuc2), (Normal ns1)) -n\* (m3, s3)) \ s3 \ Failure)))" + using assms(5) cfg_correct correctness_propagates_through_empty local.Nil \node_to_block(G) ! n = related_block\ + by (metis (full_types) correctness_propagates_through_assumption correctness_propagates_through_assumption2) + + have succ_cfg_sat: "\msuc2 m' s' ns_end. List.member (out_edges(G) ! n) msuc2 \ (A,M,\,\,\,G \(Inl (msuc2), Normal ns1) -n\* (m', s')) \ + is_final_config (m', s') \ + (s' = Normal ns_end) \ (expr_all_sat A \ \ \ ns_end) posts" + proof + fix msuc2 m' s' ns_end + assume a: "List.member (out_edges G ! n) msuc2" and + b: "A,M,\,\,\,G \(Inl msuc2, Normal ns1) -n\* (m', s')" and + c: "is_final_config (m', s')" and + d: "(s' = Normal ns_end)" + have one_block_advance: "A,M,\,\,\,G \(Inl n, Normal ns1) -n\ (Inl msuc2, Normal ns1)" + using local.Nil \node_to_block(G) ! n = related_block\ assms(5) + a b c + by (metis RedCmdListNil RedNormalSucc push_through_assumption0 push_through_assumption1) + show "(expr_all_sat A \ \ \ ns_end) posts" using cfg_satisfies_post b c a succ_cfg_correct one_block_advance + by (meson converse_rtranclp_into_rtranclp d) + qed + have "j' < j" using 1 using Suc_lessD by blast + thus ?thesis using eq snd_rest_of_steps succ_correct None succ_cfg_correct succ_cfg_sat by blast + next + case (RedParsedIfFalse) + hence eq: "(snd_inter_bb, snd_inter_cont, snd_inter_state) = (else0, convert_list_to_cont ( else_bbs) cont0, Normal ns1)" using None bb_successor_if 1 by auto + + from snd_step + have succ_cfg_correct: "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m3 s3. ((A,M,\,\,\,G \ (Inl(msuc2), (Normal ns1)) -n\* (m3, s3)) \ s3 \ Failure)))" + using assms(5) cfg_correct correctness_propagates_through_empty local.Nil \node_to_block(G) ! n = related_block\ + by (metis (full_types) correctness_propagates_through_assumption correctness_propagates_through_assumption2) + + have succ_cfg_sat: "\msuc2 m' s' ns_end. List.member (out_edges(G) ! n) msuc2 \ (A,M,\,\,\,G \(Inl (msuc2), Normal ns1) -n\* (m', s')) \ + is_final_config (m', s') \ + (s' = Normal ns_end) \ (expr_all_sat A \ \ \ ns_end) posts" + proof + fix msuc2 m' s' ns_end + assume a: "List.member (out_edges G ! n) msuc2" and + b: "A,M,\,\,\,G \(Inl msuc2, Normal ns1) -n\* (m', s')" and + c: "is_final_config (m', s')" and + d: "(s' = Normal ns_end)" + have one_block_advance: "A,M,\,\,\,G \(Inl n, Normal ns1) -n\ (Inl msuc2, Normal ns1)" + using local.Nil \node_to_block(G) ! n = related_block\ assms(5) + a b c + by (metis RedCmdListNil RedNormalSucc push_through_assumption0 push_through_assumption1) + show "(expr_all_sat A \ \ \ ns_end) posts" using cfg_satisfies_post b c a succ_cfg_correct one_block_advance + by (meson converse_rtranclp_into_rtranclp d) + qed + + have "j' < j" using 1 using Suc_lessD by blast + + thus ?thesis using eq snd_rest_of_steps succ_correct None succ_cfg_correct succ_cfg_sat by blast + qed (auto simp add: bb_successor_if) + next + case (Some block_guard) + then show ?thesis + proof cases + assume guard_true: "(red_expr A \ \ \ block_guard ns1 (BoolV True))" + hence guard_not_false: "\ (red_expr A \ \ \ block_guard ns1 (BoolV False))" using expr_eval_determ by blast + from snd_step have eq: "(snd_inter_bb, snd_inter_cont, snd_inter_state) = (then0, convert_list_to_cont ( then_bbs) cont0, Normal ns1)" + proof cases + case RedParsedIfTrue thus ?thesis using guard_true bb_successor_if by (simp add: RedParsedIfTrue) + qed (auto simp add: guard_not_false bb_successor_if Some) + + from snd_step + have succ_cfg_correct: "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m3 s3. ((A,M,\,\,\,G \ (Inl(msuc2), Normal ns1) -n\* (m3, s3)) \ s3 \ Failure)))" + using assms(5) cfg_correct correctness_propagates_through_empty local.Nil \node_to_block(G) ! n = related_block\ + by (metis (full_types) correctness_propagates_through_assumption correctness_propagates_through_assumption2) + + have succ_cfg_sat: "\msuc2 m' s' ns_end. List.member (out_edges(G) ! n) msuc2 \ (A,M,\,\,\,G \(Inl (msuc2), Normal ns1) -n\* (m', s')) \ + is_final_config (m', s') \ + (s' = Normal ns_end) \ (expr_all_sat A \ \ \ ns_end) posts" + proof + fix msuc2 m' s' ns_end + assume a: "List.member (out_edges G ! n) msuc2" and + b: "A,M,\,\,\,G \(Inl msuc2, Normal ns1) -n\* (m', s')" and + c: "is_final_config (m', s')" and + d: "(s' = Normal ns_end)" + have one_block_advance: "A,M,\,\,\,G \(Inl n, Normal ns1) -n\ (Inl msuc2, Normal ns1)" + using local.Nil \node_to_block(G) ! n = related_block\ assms(5) + a b c + by (metis RedCmdListNil RedNormalSucc push_through_assumption0 push_through_assumption1) + show "(expr_all_sat A \ \ \ ns_end) posts" using cfg_satisfies_post b c a succ_cfg_correct one_block_advance + by (meson converse_rtranclp_into_rtranclp d) + qed + + have "j' < j" using 1 using Suc_lessD by blast + + thus ?thesis using eq guard_true snd_rest_of_steps succ_correct Some succ_cfg_correct succ_cfg_sat by blast + next + assume guard_not_true: "\ (red_expr A \ \ \ block_guard ns1 (BoolV True))" + thus ?thesis + proof cases + assume guard_false: "(red_expr A \ \ \ block_guard ns1 (BoolV False))" + from snd_step have eq: "(snd_inter_bb, snd_inter_cont, snd_inter_state) = (else0, convert_list_to_cont ( else_bbs) cont0, Normal ns1)" + proof cases + case RedParsedIfFalse thus ?thesis using guard_false bb_successor_if by (simp add: RedParsedIfFalse) + qed (auto simp add: guard_not_true bb_successor_if Some) + + from snd_step + have succ_cfg_correct: "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m3 s3. ((A,M,\,\,\,G \ (Inl(msuc2), Normal ns1) -n\* (m3, s3)) \ s3 \ Failure)))" + using assms(5) cfg_correct correctness_propagates_through_empty local.Nil \node_to_block(G) ! n = related_block\ + by (metis (full_types) correctness_propagates_through_assumption correctness_propagates_through_assumption2) + + have succ_cfg_sat: "\msuc2 m' s' ns_end. List.member (out_edges(G) ! n) msuc2 \ (A,M,\,\,\,G \(Inl (msuc2), Normal ns1) -n\* (m', s')) \ + is_final_config (m', s') \ + (s' = Normal ns_end) \ (expr_all_sat A \ \ \ ns_end) posts" + proof + fix msuc2 m' s' ns_end + assume a: "List.member (out_edges G ! n) msuc2" and + b: "A,M,\,\,\,G \(Inl msuc2, Normal ns1) -n\* (m', s')" and + c: "is_final_config (m', s')" and + d: "(s' = Normal ns_end)" + have one_block_advance: "A,M,\,\,\,G \(Inl n, Normal ns1) -n\ (Inl msuc2, Normal ns1)" + using local.Nil \node_to_block(G) ! n = related_block\ assms(5) + a b c + by (metis RedCmdListNil RedNormalSucc push_through_assumption0 push_through_assumption1) + show "(expr_all_sat A \ \ \ ns_end) posts" using cfg_satisfies_post b c a succ_cfg_correct one_block_advance + by (meson converse_rtranclp_into_rtranclp d) + qed + + have "j' < j" using 1 using Suc_lessD by blast + + thus ?thesis using eq guard_false snd_rest_of_steps succ_correct Some succ_cfg_correct succ_cfg_sat by blast + next + assume guard_not_false2: "(\ (red_expr A \ \ \ block_guard ns1 (BoolV False)))" and + guard_not_true2: "(\ (red_expr A \ \ \ block_guard ns1 (BoolV True)))" + thus ?thesis + proof - + from snd_step have False using guard_not_false2 guard_not_true2 bb_successor_if Some + by (cases) auto + thus ?thesis by simp + qed + qed + qed + qed + qed + next + case Cons + thus ?thesis using \cs2 = []\ by simp + qed +qed + +text \Global lemma for a generic big block. This means that neither a loop, nor an if-statement is entered after its simple commands are executed.\ +lemma block_global_rel_generic: + assumes block_rel: "ast_cfg_rel None [] bb cs2" + and ast_trace: "A,M,\,\,\,T \ (bb, cont0, (Normal ns1)) -n\^j (reached_bb, reached_cont, reached_state)" + and "bb = (BigBlock name cs1 any_str any_tr)" + and node_to_block_assm: "node_to_block(G) ! n = related_block" + and block_id: + "(related_block = cs2) \ + (related_block = c#cs2) \ c = Assume guard \ (red_expr A \ \ \ guard ns1 (BoolV True)) \ + (related_block = c#cs2) \ c = Assume not_guard \ (UnOp Not guard \ not_guard) \ (red_expr A \ \ \ guard ns1 (BoolV False))" + and cfg_correct: "(\ m2 s2. ((red_cfg_multi A M \ \ \ G (Inl n, Normal ns1) (m2, s2)) \ (s2 \ Failure)))" + and cfg_satisfies_post: "(\ m2 s2. (red_cfg_multi A M \ \ \ G (Inl n, Normal ns1) (m2, s2)) \ + is_final_config (m2, s2) \ \ns_end. s2 = Normal ns_end \ expr_all_sat A \ \ \ ns_end posts)" + and trivial_bb_successor: "(cont0 = KSeq bb1 cont1) \ any_str = None \ any_tr = None" + and block_local_rel: + "\ reached_bb_inter reached_cont_inter reached_state_inter. + (red_bigblock A M \ \ \ T (bb, cont0, (Normal ns1)) (reached_bb_inter, reached_cont_inter, reached_state_inter)) \ + (\ s2'.((red_cmd_list A M \ \ \ (node_to_block(G) ! n) (Normal ns1) s2') \ (s2' \ Failure))) \ + cs1 \ [] \ + cs2 \ [] \ + reached_state_inter \ Failure \ + (\ns1'. reached_state_inter = Normal ns1' \ (A,M,\,\,\ \ \(node_to_block(G) ! n), Normal ns1\ [\] Normal ns1'))" + and succ_correct: + "\ ns1'' k. + k < j \ + \msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m3 s3. ((A,M,\,\,\,G \ (Inl(msuc2), Normal ns1'') -n\* (m3, s3)) \ s3 \ Failure)) \ + \msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m' s'. ((A,M,\,\,\,G \(Inl (msuc2), Normal ns1'') -n\* (m', s')) \ + is_final_config (m', s') \ + (\ns_end. s' = Normal ns_end \ expr_all_sat A \ \ \ ns_end posts))) \ + A,M,\,\,\,T \ (bb1, cont1, (Normal ns1'')) -n\^k (reached_bb, reached_cont, reached_state) \ + (Ast.valid_configuration A \ \ \ posts reached_bb reached_cont reached_state)" + shows "(Ast.valid_configuration A \ \ \ posts reached_bb reached_cont reached_state)" + using assms cases +proof cases + case Rel_Main_test + have not_end: "(cont0 \ KStop) \ any_str \ None \ any_tr \ None" using trivial_bb_successor by simp + from ast_trace show ?thesis + proof (cases cs2) + case Nil hence \cs1 = []\ by (simp add: local.Rel_Main_test(2)) + thus ?thesis using local.Nil local.Rel_Main_test(2) by blast + next + case (Cons) + hence "cs1 \ Nil" using assms(3) local.Rel_Main_test by blast + from ast_trace this show ?thesis + proof (cases j) + case 0 + hence "(reached_bb, reached_cont, reached_state) = ((BigBlock name cs1 any_str any_tr), cont0, (Normal ns1))" using ast_trace assms(3) by auto + then show ?thesis unfolding Ast.valid_configuration_def by (simp add: trivial_bb_successor) + next + case succ_0: (Suc j') + from this assms(3) obtain inter_bb inter_cont inter_state where + first_step: "red_bigblock A M \ \ \ T ((BigBlock name cs1 any_str any_tr), cont0, (Normal ns1)) (inter_bb, inter_cont, inter_state)" and + rest_of_steps: "A,M,\,\,\,T \ (inter_bb, inter_cont, inter_state) -n\^j' (reached_bb, reached_cont, reached_state)" + by (metis ast_trace get_state.cases relpowp_Suc_D2) + + from cfg_correct Cons block_id node_to_block_assm + have local_rel_corr: "(\ s2'.((red_cmd_list A M \ \ \ cs2 (Normal ns1) s2') \ (s2' \ Failure)))" + apply (simp) + apply (rule disjE) + apply simp + apply (rule dag_verifies_propagate_2) + apply blast + apply assumption + apply simp + apply (rule disjE) + apply simp + apply (metis dag_verifies_propagate_2 push_through_assumption0) + apply (metis dag_verifies_propagate_2 push_through_assumption1) + done + + from local_rel_corr first_step + have a2: "(inter_state \ Failure \ (\ns1'. inter_state = Normal ns1' \ (A,M,\,\,\ \ \(node_to_block G ! n), Normal ns1\ [\] Normal ns1')))" + using block_local_rel assms(3) \cs1 \ []\ Cons + by (metis bigblock.inject cfg_correct dag_verifies_propagate_2 local.Rel_Main_test(1)) + + from first_step \cs1 \ Nil\ + have a1: "(inter_bb, inter_cont, inter_state) = ((BigBlock name [] any_str any_tr), cont0, inter_state)" + proof cases + case RedSimpleCmds then show ?thesis by (auto simp add: RedSimpleCmds) + qed auto + + show ?thesis + proof (cases inter_state) + case 1: (Normal x1) + from rest_of_steps show ?thesis + proof (cases j') + case 0 + then show ?thesis + by (metis valid_configuration_def a1 a2 get_state.simps is_final.simps(5) relpowp_0_E rest_of_steps trivial_bb_successor) + next + case 2: (Suc j'') + from this rest_of_steps obtain snd_inter_bb snd_inter_cont snd_inter_state where + snd_step: "red_bigblock A M \ \ \ T ((BigBlock name [] any_str any_tr), cont0, inter_state) (snd_inter_bb, snd_inter_cont, snd_inter_state)" and + snd_rest_of_steps: "A,M,\,\,\,T \ (snd_inter_bb, snd_inter_cont, snd_inter_state) -n\^j'' (reached_bb, reached_cont, reached_state)" + by (metis a1 get_state.cases relpowp_Suc_D2) + + from snd_step have snd_step_equiv: "(snd_inter_bb, snd_inter_cont, snd_inter_state) = (bb1, cont1, inter_state)" + proof cases + case RedSkip thus ?thesis using trivial_bb_successor by (simp add: RedSkip) + qed (auto simp add: trivial_bb_successor "1") + + from first_step + have succ_cfg_correct: "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m3 s3. ((A,M,\,\,\,G \ (Inl(msuc2), inter_state) -n\* (m3, s3)) \ s3 \ Failure)))" + proof cases + case RedSimpleCmds show ?thesis + using 1 snd_step_equiv RedSimpleCmds(3) dag_verifies_propagate Rel_Main_test(1) cfg_correct assms(3-5) a2 + by blast + qed (auto simp add: \cs1 \ Nil\) + + have succ_cfg_sat: "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m' s'. ((A,M,\,\,\,G \(Inl (msuc2), inter_state) -n\* (m', s')) \ + is_final_config (m', s') \ + (\ns_end. s' = Normal ns_end \ expr_all_sat A \ \ \ ns_end posts))))" + using cfg_satisfies_post cfg_correct local.Cons + by (metis (no_types) "1" RedNormalSucc a2 converse_rtranclp_into_rtranclp) + + have "j'' < j" using succ_0 2 by simp + + then show ?thesis using expr_all_sat_def snd_step_equiv succ_correct snd_rest_of_steps "1" succ_cfg_correct succ_cfg_sat by auto + qed + next + case Failure + then show ?thesis + using \inter_state \ Failure \ (\ns1'. inter_state = Normal ns1' \ A,M,\,\,\ \ \node_to_block(G) ! n,Normal ns1\ [\] Normal ns1')\ + by linarith + next + case Magic + then show ?thesis by (metis valid_configuration_def a2 magic_propagates rest_of_steps state.distinct(3)) + qed + qed + qed +next + case Rel_Invs + have not_end: "(cont0 \ KStop) \ any_str \ None \ any_tr \ None" using trivial_bb_successor by simp + from ast_trace show ?thesis + proof (cases cs2) + case Nil + thus ?thesis + proof (cases j) + case 0 + hence "(reached_bb, reached_cont, reached_state) = ((BigBlock name cs1 any_str any_tr), cont0, (Normal ns1))" using ast_trace assms(3) by auto + then show ?thesis by (simp add: Ast.valid_configuration_def trivial_bb_successor) + next + case 1: (Suc j') + from this assms(3) obtain snd_inter_bb snd_inter_cont snd_inter_state where + snd_step: "red_bigblock A M \ \ \ T ((BigBlock name [] any_str any_tr), cont0, (Normal ns1)) (snd_inter_bb, snd_inter_cont, snd_inter_state)" and + snd_rest_of_steps: "A,M,\,\,\,T \ (snd_inter_bb, snd_inter_cont, snd_inter_state) -n\^j' (reached_bb, reached_cont, reached_state)" + by (metis ast_trace bigblock.inject local.Nil local.Rel_Invs relpowp_Suc_E2 surj_pair) + + hence eq: "(snd_inter_bb, snd_inter_cont, snd_inter_state) = (bb1, cont1, (Normal ns1))" using trivial_bb_successor 1 + by (cases) auto + + have succ_cfg_correct: "(\msuc2. List.member (out_edges(G) ! n) msuc2 \ (\m3 s3. ((A,M,\,\,\,G \ (Inl(msuc2), (Normal ns1)) -n\* (m3, s3)) \ s3 \ Failure)))" + using assms(4-5) cfg_correct correctness_propagates_through_empty local.Nil + by (metis (no_types) correctness_propagates_through_assumption correctness_propagates_through_assumption2) + + have succ_cfg_sat: "\msuc2 m' s' ns_end. List.member (out_edges(G) ! n) msuc2 \ (A,M,\,\,\,G \(Inl (msuc2), Normal ns1) -n\* (m', s')) \ + is_final_config (m', s') \ + (s' = Normal ns_end) \ (expr_all_sat A \ \ \ ns_end) posts" + proof + fix msuc2 m' s' ns_end + assume a: "List.member (out_edges G ! n) msuc2" and + b: "A,M,\,\,\,G \(Inl msuc2, Normal ns1) -n\* (m', s')" and + c: "is_final_config (m', s')" and + d: "(s' = Normal ns_end)" + have one_block_advance: "A,M,\,\,\,G \(Inl n, Normal ns1) -n\ (Inl msuc2, Normal ns1)" + using local.Nil \node_to_block(G) ! n = related_block\ assms(5) + a b c + by (metis RedCmdListNil RedNormalSucc push_through_assumption0 push_through_assumption1) + show "(expr_all_sat A \ \ \ ns_end) posts" using cfg_satisfies_post b c a succ_cfg_correct one_block_advance + by (meson converse_rtranclp_into_rtranclp d) + qed + + have "j' < j" using 1 using Suc_lessD by blast + + thus ?thesis using eq snd_rest_of_steps succ_correct succ_cfg_correct succ_cfg_sat by blast + qed + next + case (Cons) + hence "cs1 \ Nil" using assms(3) local.Rel_Invs by blast + from ast_trace this show ?thesis + using local.Cons local.Rel_Invs(1) by fastforce + qed +qed + +definition loop_IH + where "loop_IH j A M \ \ \ T bb0 cont0 G block_index posts reached_bb reached_cont reached_state \ + (\k ns1. k < j \ + (A,M,\,\,\,T \(bb0, cont0, Normal ns1) -n\^k (reached_bb, reached_cont, reached_state)) \ + (\m' s'. (red_cfg_multi A M \ \ \ G ((Inl block_index),(Normal ns1)) (m',s')) \ (s' \ Failure)) \ + (\m' s'. (A,M,\,\,\,G \(Inl block_index, Normal ns1) -n\* (m', s')) \ + is_final_config (m', s') \ (\ns_end. s' = Normal ns_end \ (expr_all_sat A \ \ \ ns_end) posts)) \ + (Ast.valid_configuration A \ \ \ posts reached_bb reached_cont reached_state))" + +lemma loop_IH_prove: + assumes "\ k ns1. k < j \ + (A,M,\,\,\,T \(bb0, cont0, Normal ns1) -n\^k (reached_bb, reached_cont, reached_state)) \ + (\m' s'. (red_cfg_multi A M \ \ \ G ((Inl block_index),(Normal ns1)) (m',s')) \ (s' \ Failure)) \ + (\m' s'. (A,M,\,\,\,G \(Inl block_index, Normal ns1) -n\* (m', s')) \ + is_final_config (m', s') \ (\ns_end. s' = Normal ns_end \ (expr_all_sat A \ \ \ ns_end) posts)) \ + (Ast.valid_configuration A \ \ \ posts reached_bb reached_cont reached_state)" + shows "loop_IH j A M \ \ \ T bb0 cont0 G block_index posts reached_bb reached_cont reached_state" + using assms + unfolding loop_IH_def + by blast + +lemma loop_IH_apply: + assumes "loop_IH j A M \ \ \ T bb0 cont0 G block_index posts reached_bb reached_cont reached_state" + and "k < j" + and "(A,M,\,\,\,T \(bb0, cont0, Normal ns1) -n\^k (reached_bb, reached_cont, reached_state))" + and "(\m' s'. (red_cfg_multi A M \ \ \ G ((Inl block_index),(Normal ns1)) (m',s')) \ (s' \ Failure))" + and "(\m' s'. (A,M,\,\,\,G \(Inl block_index, Normal ns1) -n\* (m', s')) \ + is_final_config (m', s') \ (\ns_end. s' = Normal ns_end \ (expr_all_sat A \ \ \ ns_end posts)))" + shows "(Ast.valid_configuration A \ \ \ posts reached_bb reached_cont reached_state)" + using assms + unfolding loop_IH_def + by blast + +subsection \Procedure correctness\ + +text \The main lemma used to complete proof of the correctness of an \<^term>\ast_procedure\.\ +lemma end_to_end_util2: + assumes AExpanded: "\ \ end_bb end_cont end_state ns (M::mbodyCFG proc_context). + rtranclp (red_bigblock B M \ \ [] ast) (init_ast ast ns) (end_bb, end_cont, end_state) \ + (\ v. (closed ((type_of_val B) v))) \ + (\ t. ((closed t) \ (\ v. (((type_of_val B) v) = t)))) \ + (fun_interp_wf B fun_decls \) \ + (axiom_assm B \ constants (ns::(('a)nstate)) axioms) \ + (expr_all_sat B \ \ [] ns all_pres) \ + (state_typ_wf B [] (local_state ns) (snd \)) \ + (state_typ_wf B [] (global_state ns) (fst \)) \ + (unique_constants_distinct (global_state ns) unique_consts) \ + ((global_state ns) = (old_global_state ns)) \ + ((binder_state ns) = Map.empty) \ + (Ast.valid_configuration B \ \ [] checked_posts end_bb end_cont end_state)" + and "all_pres = proc_all_pres proc_ast" + and "checked_posts = proc_checked_posts proc_ast" + and ABody: "procedure.proc_body proc_ast = Some (locals, ast)" + and AVarContext:"\ = (constants@global_vars, (proc_args proc_ast)@locals)" + and ARets:"proc_rets proc_ast = []" + and "proc_ty_args proc_ast = 0" + shows "proc_is_correct B fun_decls constants unique_consts global_vars axioms proc_ast + (Ast.proc_body_satisfies_spec :: 'a absval_ty_fun \ mbodyCFG proc_context \ var_context \ 'a fun_interp \ rtype_env \ expr list \ expr list \ ast \ 'a nstate \ bool)" +proof - + show "proc_is_correct B fun_decls constants unique_consts global_vars axioms proc_ast (Ast.proc_body_satisfies_spec :: 'a absval_ty_fun \ mbodyCFG proc_context \ var_context \ 'a fun_interp \ rtype_env \ expr list \ expr list \ ast \ 'a nstate \ bool)" + 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 \ \ gs ls end_bb end_cont end_state + assume Atyp:"(\t. closed t \ (\v. type_of_val B v = t)) \ (\v. closed (type_of_val B v))" and + FunWf:"fun_interp_wf B fun_decls \" and + ARenv: "list_all closed \ \ length \ = proc_ty_args proc_ast" and + WfGlobal: "state_typ_wf B \ gs (constants @ global_vars)" and + WfLocal: "state_typ_wf B \ ls (proc_args proc_ast @ locals @ proc_rets proc_ast)" and + UniqueConsts: "unique_constants_distinct gs unique_consts" and + AxSat: "axioms_sat B (constants, []) \ + \old_global_state = Map.empty, global_state = state_restriction gs constants, local_state = Map.empty, binder_state = Map.empty\ + axioms" and + APres: "expr_all_sat B (constants @ global_vars, proc_args proc_ast @ locals @ proc_rets proc_ast) \ \ + \old_global_state = gs, global_state = gs, local_state = ls, binder_state = Map.empty\ (map fst (proc_pres proc_ast))" and + Ared: "rtranclp + (red_bigblock + B ([]::mbodyCFG proc_context) (constants @ global_vars, + proc_args proc_ast @ + locals @ + proc_rets + proc_ast) \ \ ast) (init_ast ast \old_global_state = gs, global_state = gs, local_state = ls, binder_state = Map.empty\) + (end_bb, end_cont, end_state)" + have Contexteq:"\ = (constants @ global_vars, proc_args proc_ast @ locals @ proc_rets proc_ast)" + using AVarContext ARets by simp + from ARenv \proc_ty_args proc_ast = 0\ have "\ = []" by simp + have "Ast.valid_configuration B \ \ [] checked_posts end_bb end_cont end_state" + apply (rule AExpanded) + apply (subst Contexteq) + using Ared \\ = []\ + apply fastforce + apply (simp add: Atyp) + apply (simp add: Atyp) + apply (simp add: FunWf) + unfolding nstate_global_restriction_def + using AxSat + apply simp + using APres \\ = []\ \all_pres = _\ Contexteq + apply simp + using Contexteq WfLocal \\ = []\ + apply simp + using Contexteq WfGlobal \\ = []\ + apply simp + using UniqueConsts + apply simp + apply simp + apply simp + done + thus "Ast.valid_configuration B (constants @ global_vars, proc_args proc_ast @ locals @ proc_rets proc_ast) \ \ + (map fst (filter (\x. \ snd x) (proc_posts proc_ast))) end_bb end_cont end_state" + using Contexteq \\ = []\ \checked_posts = _\ + by simp + qed +qed + +end \ No newline at end of file diff --git a/BoogieLang/BackedgeElim.thy b/BoogieLang/BackedgeElim.thy index b8440cf..aa8b780 100644 --- a/BoogieLang/BackedgeElim.thy +++ b/BoogieLang/BackedgeElim.thy @@ -2,7 +2,7 @@ section \A collection of lemmas, definitions and tactics that aid the cert CFG-to-DAG phase\ 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 \State equality up to a set\ @@ -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 \ ns1 ns2' {}" and A2Red1:"A,M,\,\,\ \ \cs2A, Normal ns2\ [\] 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 \ \ 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 \ proc_context \ var_context \ +definition dag_lemma_conclusion :: "'a absval_ty_fun \ mbodyCFG proc_context \ var_context \ 'a fun_interp \ rtype_env \ expr list \ cmd list \ 'a nstate \ 'a state \ bool \ bool" where "dag_lemma_conclusion A M \ \ \ post_invs cs2 ns2 s' c \ @@ -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 \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''.\ lemma cfg_dag_helper_return_2: @@ -1212,7 +1212,7 @@ proof - RedCsA:"(A,M,\,\,\ \ \csA,Normal ns2\ [\] Normal ns2)" and InvsHold2:"list_all (expr_sat A \ \ \ 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 \ \ \ 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'' \ j' \ j = Suc j' \ j'' < j" by simp -definition loop_ih :: "'a absval_ty_fun \ proc_context \ var_context \ +definition loop_ih :: "'a absval_ty_fun \ mbodyCFG proc_context \ var_context \ 'a fun_interp \ rtype_env \ mbodyCFG \ vname list \ expr list \ expr list \ 'a nstate \ 'a state \ nat \ nat + unit \ nat \ bool" where "loop_ih A M \ \ \ G H invs posts ns1 s' node_id m' j\ @@ -1419,9 +1419,10 @@ lemma backedge_loop_head_helper: subsection \Helper lemma for final end-to-end theorem\ + lemma end_to_end_util: assumes AExpanded:"\ \ m' s' ns M. - A,M,\,\,[],cfg_body \ (Inl n, Normal ns) -n\* (m', s') \ + A,M,\,\,[],cfg_body \ (Inl n, Normal ns) -n\* (m', s') \ (\ v. (closed ((type_of_val A) v))) \ (\ t. ((closed t) \ (\ v. (((type_of_val A) v) = t)))) \ (fun_interp_wf A fun_decls \) \ @@ -1429,6 +1430,7 @@ lemma end_to_end_util: (expr_all_sat A \ \ [] ns all_pres) \ (state_typ_wf A [] (local_state ns) (snd \)) \ (state_typ_wf A [] (global_state ns) (fst \)) \ + unique_constants_distinct (global_state ns) unique_consts \ ((global_state ns) = (old_global_state ns)) \ ((binder_state ns) = Map.empty) \ (valid_configuration A \ \ [] checked_posts m' s')" and @@ -1442,17 +1444,18 @@ 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 unique_consts 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 unique_consts 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 \ \ gs ls m' s' + fix \ \ gs ls m' s' assume Atyp:"(\t. closed t \ (\v. type_of_val A v = t)) \ (\v. closed (type_of_val A v))" and FunWf:"fun_interp_wf A fun_decls \" and ARenv: "list_all closed \ \ length \ = proc_ty_args proc" and WfGlobal: "state_typ_wf A \ gs (constants @ global_vars)" and WfLocal: "state_typ_wf A \ ls (proc_args proc @ locals @ proc_rets proc)" and + UniqueConsts: "unique_constants_distinct gs unique_consts" and AxSat: "axioms_sat A (constants, []) \ \old_global_state = Map.empty, global_state = state_restriction gs constants, local_state = Map.empty, binder_state = Map.empty\ axioms" and @@ -1473,7 +1476,7 @@ proof - apply (subst \n = entry cfg_body\) apply (subst Contexteq) using Ared \\ = []\ - apply fastforce + apply fastforce apply (simp add: Atyp) apply (simp add: Atyp) apply (simp add: FunWf) @@ -1485,6 +1488,8 @@ proof - using Contexteq WfLocal \\ = []\ apply simp using Contexteq WfGlobal \\ = []\ + apply simp + using UniqueConsts apply simp apply simp apply simp diff --git a/BoogieLang/CFGOptimizationsLoop.thy b/BoogieLang/CFGOptimizationsLoop.thy new file mode 100644 index 0000000..31430aa --- /dev/null +++ b/BoogieLang/CFGOptimizationsLoop.thy @@ -0,0 +1,1212 @@ +theory CFGOptimizationsLoop + imports Boogie_Lang.Semantics Boogie_Lang.Util +begin + +definition hybrid_block_lemma_target_succ_verifies + where "hybrid_block_lemma_target_succ_verifies A M \ \ \ G' tgt_block s1' posts \ + (\ns1'. s1' = Normal ns1' \ + (\target_succ. List.member (out_edges(G') ! tgt_block) target_succ \ + (\m2' s2'. (A,M,\,\,\,G' \ (Inl target_succ, (Normal ns1')) -n\* (m2', s2')) \ + valid_configuration A \ \ \ posts m2' s2') + ) + )" + +definition hybrid_block_lemma_target_verifies + where "hybrid_block_lemma_target_verifies A M \ \ \ G' tgt_block tgt_cmds ns posts \ + (\s1'. (A,M,\,\,\ \ \tgt_cmds, Normal ns\ [\] s1') \ \\First reduce the coalesced commands\ + (if (out_edges(G') ! tgt_block = []) then valid_configuration A \ \ \ posts (Inr()) s1' else s1' \ Failure) \ + \\All successor blocks of \<^term>\tgt_block\ must verify\ + hybrid_block_lemma_target_succ_verifies A M \ \ \ G' tgt_block s1' posts + )" + +subsection \Definition loop induction hypothesis and global block Lemma for blocks in a loop\ + +definition loop_ih_optimizations + where "loop_ih_optimizations A M \ \ \ G G' LoopHeader LoopHeader' m' s' j posts\ + \j' ns1'. ((j' \ j) \ + (A,M,\,\,\,G \(Inl LoopHeader, Normal ns1') -n\^j' (m', s')) \ + (\m1' s1'.( A,M,\,\,\,G' \(Inl LoopHeader', Normal ns1') -n\* (m1', s1')) \ valid_configuration A \ \ \ posts m1' s1') \ + valid_configuration A \ \ \ posts m' s')" + +definition global_block_lemma_loop + where "global_block_lemma_loop A M \ \ \ G G' src_block tgt_block lsLoopHead posts \ + \m' ns s' j. + (red_cfg_k_step A M \ \ \ G ((Inl src_block),(Normal ns)) j (m',s')) \ + (\m1' s1'. (A,M,\,\,\,G' \ (Inl tgt_block, (Normal ns)) -n\* (m1', s1')) \ valid_configuration A \ \ \ posts m1' s1') \ + (\(LoopHead,LoopHead')\lsLoopHead. loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' j posts) \ + valid_configuration A \ \ \ posts m' s'" + +definition hybrid_block_lemma_loop + where "hybrid_block_lemma_loop A M \ \ \ G G' src_block tgt_block tgt_cmds lsLoopHead posts\ + \m' ns s' j. + (red_cfg_k_step A M \ \ \ G ((Inl src_block),(Normal ns)) j (m',s')) \ + hybrid_block_lemma_target_verifies A M \ \ \ G' tgt_block tgt_cmds ns posts \ + (\(LoopHead,LoopHead')\lsLoopHead. loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' j posts) \ + valid_configuration A \ \ \ posts m' s'" + + +subsection \Helper Lemmas\ + +lemma target_verifies: + assumes oneStep: "A,M,\,\,\,G \ (Inl a, Normal ns) -n\ (Inl b, Normal ns')" + and cmd: "node_to_block(G) ! a = node_to_block(G') ! c" + and targetVerifies: "(\m1' s1'. (A,M,\,\,\,G' \(Inl c, Normal ns) -n\* (m1', s1')) \ valid_configuration A \ \ \ posts m1' s1')" + and member: "List.member (out_edges(G') ! c) d" + shows "\m1' s1'. (A,M,\,\,\,G'\(Inl d, Normal ns') -n\* (m1', s1')) \ valid_configuration A \ \ \ posts m1' s1'" +proof - + have "A,M,\,\,\,G' \ (Inl c, Normal ns) -n\ (Inl d, Normal ns')" + using oneStep cmd + apply (cases) + by (simp add: RedNormalSucc cmd member) + + then show ?thesis + by (meson targetVerifies converse_rtranclp_into_rtranclp) +qed + +lemma one_step_not_failure: + assumes "(\m1' s1'. (A,M,\,\,\,G' \(Inl a, Normal ns) -n\* (m1', s1')) \ valid_configuration A \ \ \ posts m1' s1')" + and "node_to_block G ! b = node_to_block G' ! a" + and "A,M,\,\,\,G \ (Inl b, Normal ns) -n\ (c, d)" + shows "d \ Failure" + using assms(3) +proof cases + case (RedNormalSucc cs ns' n') + then show ?thesis by auto +next + case (RedNormalReturn cs ns') + then show ?thesis by auto +next + case (RedFailure cs) + then show ?thesis + by (metis assms(1) assms(2) r_into_rtranclp red_cfg.RedFailure valid_configuration_def) +next + case (RedMagic cs) + then show ?thesis by auto +qed + +lemma hybrid_block_lemma_loop_elim: + assumes "hybrid_block_lemma_loop A M \ \ \ G G' src_block tgt_block tgt_cmds lsLoopHead posts" + and "A,M,\,\,\,G \ (Inl src_block, (Normal ns)) -n\^j (m', s')" + and "hybrid_block_lemma_target_verifies A M \ \ \ G' tgt_block tgt_cmds ns posts" + and "\(LoopHead, LoopHead')\lsLoopHead. loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' j posts" + shows "valid_configuration A \ \ \ posts m' s'" + using assms + unfolding hybrid_block_lemma_loop_def + by blast + +lemma loop_ih_optimizations_one_less: + assumes "loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' j posts" + shows "loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' (j-1) posts" + using assms + unfolding loop_ih_optimizations_def + by (meson diff_le_self le_trans) + +lemma loop_ih_optimizations_more_less: + assumes "loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' j posts" and + "j' \ j" + shows "loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' j' posts" + using assms + unfolding loop_ih_optimizations_def + by (meson diff_le_self le_trans) + + +lemma loop_global_block_subset: + assumes "global_block_lemma_loop A M \ \ \ G G' src_block tgt_block lsSubset posts" + and "(lsSubset) \ (lsLoopHead)" + shows "global_block_lemma_loop A M \ \ \ G G' src_block tgt_block lsLoopHead posts" + using assms + unfolding global_block_lemma_loop_def + by blast + +lemma normal_target_verifies_show_hybrid_verifies: + assumes TargetVerifies: "\m1' s1'. (A,M,\,\,\,G' \(Inl tgt_block, Normal ns) -n\* (m1', s1')) \ valid_configuration A \ \ \ posts m1' s1'" + and TgtCmds: "node_to_block G' ! tgt_block = tgt_cmds" + shows "hybrid_block_lemma_target_verifies A M \ \ \ G' tgt_block tgt_cmds ns posts" + unfolding hybrid_block_lemma_target_verifies_def hybrid_block_lemma_target_succ_verifies_def +proof (rule allI | rule impI)+ + fix s1' + assume oneStep: "A,M,\,\,\ \ \tgt_cmds,Normal ns\ [\] s1'" + show "((if out_edges G' ! tgt_block = [] + then valid_configuration A \ \ \ posts (Inr ()) s1' + else s1' \ Failure)) \ (\ns1'. s1' = Normal ns1' \ (\target_succ. List.member (out_edges(G') ! tgt_block) target_succ \ (\m2' s2'. (A,M,\,\,\,G' \ (Inl target_succ, (Normal ns1')) -n\* (m2', s2')) \ valid_configuration A \ \ \ posts m2' s2')))" + proof (cases "out_edges G' ! tgt_block = []") + case True + have "valid_configuration A \ \ \ posts (Inr ()) s1'" + by (metis RedFailure RedNormalReturn TargetVerifies TgtCmds True oneStep r_into_rtranclp valid_configuration_def) + then show ?thesis + by (simp add: True member_rec(2)) + next + case False + have "s1' \ Failure" + using TargetVerifies + unfolding valid_configuration_def + using RedFailure TgtCmds oneStep by blast + have "(\ns1'. s1' = Normal ns1' \ (\target_succ. List.member (out_edges(G') ! tgt_block) target_succ \ (\m2' s2'. (A,M,\,\,\,G' \ (Inl target_succ, (Normal ns1')) -n\* (m2', s2')) \ valid_configuration A \ \ \ posts m2' s2')))" + by (metis (no_types, lifting) RedNormalSucc TargetVerifies TgtCmds converse_rtranclp_into_rtranclp oneStep) + then show ?thesis + using \s1' \ Failure\ + using False by presburger + qed +qed + +lemma hybrid_block_lemma_target_succ_verifies_intro: + assumes + "\ns1' target_succ m2' s2'. s1' = Normal ns1' \ + List.member (out_edges(G') ! tgt_block) target_succ \ + (A,M,\,\,\,G' \ (Inl target_succ, (Normal ns1')) -n\* (m2', s2')) \ + valid_configuration A \ \ \ posts m2' s2'" + shows "hybrid_block_lemma_target_succ_verifies A M \ \ \ G' tgt_block s1' posts" + using assms + unfolding hybrid_block_lemma_target_succ_verifies_def + by blast + +lemma red_cmd_append_failure_preserved: + assumes "(A,M,\,\,\ \ \cs,Normal ns\ [\] s)" + and "s = Failure" + \\Theoretically, it would be fine to directly write + \<^prop>\A,M,\,\,\ \ \cs,Normal ns\ [\] Failure\, but then the standard induction tactic + does not carry over that the resulting state is a failure state\ + shows "A,M,\,\,\ \ \cs@cs',Normal ns\ [\] Failure" + using assms + apply induction + apply (simp add: failure_red_cmd_list) + by (simp add: RedCmdListCons) + +lemma red_cfg_magic_preserved: + assumes "A,M,\,\,\,G \(b, s0) -n\* (m', s')" and "s0 = Magic" + shows "s' = Magic" + using assms +proof (induction rule: rtranclp_induct2) + case refl + then show ?case by simp +next + case (step a b a b) + then show ?case + using red_cfg.cases by blast +qed + +lemma magic_lemma_assume_false: + assumes "A,M,\,\,\ \ \cs, s\ [\] s'" + and "s'\Failure" + and "s = Normal ns" + and "(Assume (Lit (LBool False))) \ set (cs)" + shows "s' = Magic" + using assms +proof (induction arbitrary: ns) + case (RedCmdListNil s) + then show ?case + by simp +next + case (RedCmdListCons c s s'' cs s') + then show ?case +proof (cases "c = (Assume (Lit (LBool False)))") + case True + hence "s'' = Magic" using RedCmdListCons + by (meson RedLit assume_red_false) + then show ?thesis using RedCmdListCons + by (simp add: magic_stays_cmd_list_2) +next + case False + then show ?thesis + proof (cases "s''") + case (Normal x1) + then show ?thesis + by (metis False RedCmdListCons.IH RedCmdListCons.prems(1) RedCmdListCons.prems(3) set_ConsD) + next + case Failure + then show ?thesis + using RedCmdListCons.hyps(2) RedCmdListCons.prems(1) failure_stays_cmd_list by blast + next + case Magic + then show ?thesis + using RedCmdListCons.hyps(2) magic_stays_cmd_list_2 by blast + qed +qed +qed + +lemma assert_false_failure: + assumes "A,M,\,\,\ \ \Assert (Lit (LBool False)), Normal ns\ \ s" + shows "s = Failure" + using assms + by (cases) auto + +lemma magic_lemma_assert_false: + assumes "A,M,\,\,\ \ \cs, s\ [\] s'" + and "s = Normal ns" + and "(Assert (Lit (LBool False))) \ set (cs)" + shows "s' = Magic \ s' = Failure" + using assms +proof (induction arbitrary: ns) + case (RedCmdListNil s) + then show ?case + by simp +next + case (RedCmdListCons c s s'' cs s') + then show ?case +proof (cases "c = (Assert (Lit (LBool False)))") + case True + hence "s'' = Failure" using RedCmdListCons + by (metis True assert_false_failure) + + then show ?thesis + using RedCmdListCons.hyps(2) failure_stays_cmd_list_aux by blast +next + case False + then show ?thesis + proof (cases "s''") + case (Normal x1) + then show ?thesis + using False RedCmdListCons.IH RedCmdListCons.prems(2) by auto + next + case Failure + then show ?thesis + using RedCmdListCons.hyps(2) RedCmdListCons.prems(1) failure_stays_cmd_list by blast + next + case Magic + then show ?thesis + using RedCmdListCons.hyps(2) magic_stays_cmd_list_2 by blast + qed +qed +qed + +lemma BlockID_no_succ: + assumes "node_to_block G ! block = cs" + and "out_edges G ! block = []" + and "A,M,\,\,\,G \(Inl block, Normal ns) -n\ (m', s')" + shows "m' = Inr()" + using assms(3) +proof cases + case (RedNormalSucc cs ns' n') + then show ?thesis + by (simp add: assms(2) member_rec(2)) +next + case (RedNormalReturn cs ns') + then show ?thesis by simp +next + case (RedFailure cs) + then show ?thesis + by simp +next + case (RedMagic cs) + then show ?thesis + by simp +qed + +lemma hybrid_block_lemma_loop_eq_loop_heads: + assumes "hybrid_block_lemma_loop A M \ \ \ G G' succ tgt_block tgt_cmds_0 lsLoopHeads1 posts" + and "lsLoopHeads1 = lsLoopHeads2" + shows "hybrid_block_lemma_loop A M \ \ \ G G' succ tgt_block tgt_cmds_0 lsLoopHeads2 posts" + using assms + by simp + +subsection \Main Lemmas for Loops\ + +subsubsection \Main Lemma 1: Shows that the Loop Global Block Lemma holds if for all successors either the global + block lemma holds or there exists a pair of Loop Headers such that the Loop global block + lemma holds or the successor is equal to one of the Loop Heads\ + +lemma loopBlock_global_block: + assumes SuccBlocks: "out_edges G ! src_block = ls" + and GlobalBlockSucc: "\x\set(ls).(\lsSubsetList. lsSubsetList\lsLoopHead \ global_block_lemma_loop A M \ \ \ G G' x (f x) lsSubsetList posts) \ (\(LoopHead, LoopHead')\lsLoopHead. (x = LoopHead \ f x = LoopHead'))" + and FunctionCorr: "\x\set(ls). f x \ set(out_edges G' ! tgt_block)" + and TargetBlock: "node_to_block G' ! tgt_block = tgt_cmds" + and SourceBlock: "node_to_block G ! src_block = src_cmds" + and NotCoalesced: "tgt_cmds = src_cmds" + and NoSuccEq: "ls = [] \ out_edges G' ! tgt_block = []" + shows "global_block_lemma_loop A M \ \ \ G G' src_block tgt_block lsLoopHead posts" + unfolding global_block_lemma_loop_def +proof (rule allI | rule impI)+ + fix m' ns s' j + assume k_step: "A,M,\,\,\,G \(Inl src_block, Normal ns) -n\^j (m', s')" and + IH: "\(LoopHead, LoopHead')\lsLoopHead. loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' j posts" and + TargetVerifies: "(\m1' s1'. (A,M,\,\,\,G' \(Inl tgt_block, Normal ns) -n\* (m1', s1')) \ valid_configuration A \ \ \ posts m1' s1')" + show "valid_configuration A \ \ \ posts m' s'" + proof (cases rule: relpowp_E2_2[OF k_step]) + case 1 + then show ?thesis + unfolding valid_configuration_def + by fastforce + next + case (2 a b m) + have OneStepResult: "b \ Failure" + apply (rule one_step_not_failure[where ?G = G and ?b = src_block and ?c = a]) + apply (rule TargetVerifies) + apply (simp add: NotCoalesced SourceBlock TargetBlock) + by (simp add: "2"(2)) + then show ?thesis + proof (cases "b = Magic") + case True + have "A,M,\,\,\,G \(a, b) -n\* (m', s')" + by (meson "2"(3) rtranclp_power) + then show ?thesis + using True red_cfg_magic_preserved + unfolding valid_configuration_def + by blast + next + case False + from this obtain ns1 where "b = Normal ns1" + using OneStepResult state.exhaust by blast + from \A,M,\,\,\,G \ (Inl src_block, Normal ns) -n\ (a, b)\ show ?thesis + proof cases + case (RedNormalSucc cs ns' succ) + have succInList: "succ \ set(ls)" + using SuccBlocks in_set_member local.RedNormalSucc(5) by force + have oneStepG: "A,M,\,\,\,G \ (Inl src_block, Normal ns) -n\ (Inl succ, Normal ns')" + using "2"(2) local.RedNormalSucc(1) local.RedNormalSucc(2) by auto + then show ?thesis + proof (cases "\lsSubsetList. lsSubsetList\lsLoopHead \ global_block_lemma_loop A M \ \ \ G G' succ (f(succ)) lsSubsetList posts") + case True + from this obtain lsSubset where subset: "lsSubset\lsLoopHead" and globalBlockLoop: "global_block_lemma_loop A M \ \ \ G G' succ (f(succ)) lsSubset posts" + by auto + have steps: "A,M,\,\,\,G \(Inl succ, Normal ns') -n\^(j - 1) (m', s')" + using "2"(1) "2"(3) local.RedNormalSucc(1) local.RedNormalSucc(2) by auto + have "\(LoopHeadG,LoopHeadG')\lsSubset. loop_ih_optimizations A M \ \ \ G G' LoopHeadG LoopHeadG' m' s' j posts" + using IH subset by auto + hence loopIH: "\(LoopHeadG,LoopHeadG')\lsSubset. loop_ih_optimizations A M \ \ \ G G' LoopHeadG LoopHeadG' m' s' (j - 1) posts" + using loop_ih_optimizations_one_less + using case_prodI2 by blast + have "\m1' s1'.( A,M,\,\,\,G' \(Inl (f(succ)), Normal ns') -n\* (m1', s1')) \ valid_configuration A \ \ \ posts m1' s1'" + apply (rule target_verifies[where ?c = tgt_block]) + apply (rule oneStepG) + apply (simp add: NotCoalesced SourceBlock TargetBlock) + apply (rule TargetVerifies) + using succInList FunctionCorr in_set_member by fastforce + then show ?thesis + using globalBlockLoop loopIH steps + unfolding global_block_lemma_loop_def valid_configuration_def + by blast + next + case False + from this obtain LoopHeadG LoopHeadG' where "succ = LoopHeadG \ f(succ) = LoopHeadG'" and "(LoopHeadG, LoopHeadG')\lsLoopHead" + using GlobalBlockSucc succInList by force + hence SuccEqLoopHead: "succ = LoopHeadG \ f(succ) = LoopHeadG'" + using GlobalBlockSucc succInList + by force + + have verifies: "\m1' s1'.( A,M,\,\,\,G' \(Inl (f(succ)), Normal ns') -n\* (m1', s1')) \ valid_configuration A \ \ \ posts m1' s1'" + apply (rule target_verifies[where ?c = tgt_block]) + apply (rule oneStepG) + apply (simp add: NotCoalesced SourceBlock TargetBlock) + apply (rule TargetVerifies) + using succInList FunctionCorr in_set_member by fastforce + + have "loop_ih_optimizations A M \ \ \ G G' LoopHeadG LoopHeadG' m' s' j posts" + using IH SuccEqLoopHead False \(LoopHeadG, LoopHeadG') \ lsLoopHead\ + by fastforce + + then show ?thesis + using SuccEqLoopHead verifies + unfolding loop_ih_optimizations_def + by (metis "2"(1) "2"(3) diff_Suc_1 diff_le_self local.RedNormalSucc(1) local.RedNormalSucc(2)) + qed + next + case (RedNormalReturn cs ns') + have "A,M,\,\,\ \ \tgt_cmds, Normal ns\ [\] s'" + by (metis "2"(3) NotCoalesced Pair_inject SourceBlock finished_remains local.RedNormalReturn(1) local.RedNormalReturn(2) local.RedNormalReturn(3) local.RedNormalReturn(4) relpowp_imp_rtranclp) + hence "A,M,\,\,\,G' \(Inl tgt_block, Normal ns) -n\ (m', s')" + using NotCoalesced TargetBlock RedNormalReturn NoSuccEq + by (metis "2"(3) SourceBlock SuccBlocks finished_remains red_cfg.RedNormalReturn relpowp_imp_rtranclp) + + then show ?thesis + unfolding valid_configuration_def + using TargetVerifies valid_configuration_def by blast + next + case (RedFailure cs) + then show ?thesis + using OneStepResult by auto + next + case (RedMagic cs) + then show ?thesis + by (simp add: False) + qed + qed + qed +qed + +subsubsection \Main Lemma 2: Shows that the Loop Global Block Lemma holds for a loop Head. + Note that src_block and tgt_block are both Loop Heads in this case.\ + + +lemma loopHead_global_block: + assumes SuccBlocks: "out_edges G ! src_block = ls" + and GlobalBlockSucc: + "\x\set(ls). ( \lsSubsetList. lsSubsetList\(lsLoopHead \ {(src_block,tgt_block)}) \ + global_block_lemma_loop A M \ \ \ G G' x (f x) lsSubsetList posts ) + \ (\(LoopHead, LoopHead')\(lsLoopHead\{(src_block,tgt_block)}). (x = LoopHead \ f x = LoopHead'))" + and FunctionCorr: "\x\set(ls). f x \ set(out_edges G' ! tgt_block)" + and TargetBlock: "node_to_block G' ! tgt_block = tgt_cmds" + and SourceBlock: "node_to_block G ! src_block = src_cmds" + and NotCoalesced: "tgt_cmds = src_cmds" + and NoSuccEq: "ls = [] \ out_edges G' ! tgt_block = []" + shows "global_block_lemma_loop A M \ \ \ G G' src_block tgt_block lsLoopHead posts" +unfolding global_block_lemma_loop_def +proof (rule allI | rule impI)+ + fix m' ns s' j + assume k_step: "A,M,\,\,\,G \(Inl src_block, Normal ns) -n\^j (m', s')" and + TargetVerifies: "\m1' s1'. (A,M,\,\,\,G' \(Inl tgt_block, Normal ns) -n\* (m1', s1')) \ valid_configuration A \ \ \ posts m1' s1'" and + IH: "\(LoopHead, LoopHead')\lsLoopHead. loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' j posts" + show "valid_configuration A \ \ \ posts m' s'" using TargetVerifies k_step GlobalBlockSucc IH + proof (induction j arbitrary: ns rule: less_induct) + case (less j) + then show ?case + proof (cases rule: relpowp_E2_2[OF less(3)]) + case 1 + then show ?thesis + unfolding valid_configuration_def + by auto + next + case (2 a b m) + have OneStepResult: "b \ Failure" + apply (rule one_step_not_failure[where ?G = G and ?b = src_block and ?c = a]) + apply (rule less.prems(1)) + apply (simp add: NotCoalesced SourceBlock TargetBlock) + by (simp add: "2"(2)) + then show ?thesis + proof (cases "b = Magic") + case True + have "A,M,\,\,\,G \(a, b) -n\* (m', s')" + by (meson "2"(3) relpowp_imp_rtranclp) + then show ?thesis + using True red_cfg_magic_preserved + unfolding valid_configuration_def + by blast + next + case False + from \A,M,\,\,\,G \ (Inl src_block, Normal ns) -n\ (a, b)\ show ?thesis + proof (cases) + case (RedNormalSucc cs ns' succ) + have succInList: "succ \ set(ls)" + using SuccBlocks in_set_member local.RedNormalSucc(5) by fastforce + + obtain LoopHeadG LoopHeadG' lsSubsetList where cond: "global_block_lemma_loop A M \ \ \ G G' succ (f(succ)) lsSubsetList posts \ (succ = LoopHeadG \ f(succ) = LoopHeadG')" and elem: "(LoopHeadG, LoopHeadG')\(lsLoopHead\{(src_block, tgt_block)}) \ lsSubsetList \ lsLoopHead\{(src_block, tgt_block)}" + using succInList less.prems(3) + by blast + have oneStepG: "A,M,\,\,\,G \ (Inl src_block, Normal ns) -n\ (Inl succ, Normal ns')" + using "2"(2) local.RedNormalSucc(1) local.RedNormalSucc(2) + by simp + + then show ?thesis + proof (cases "global_block_lemma_loop A M \ \ \ G G' succ (f(succ)) lsSubsetList posts") + case True + have loopIHSrcTgt: "loop_ih_optimizations A M \ \ \ G G' src_block tgt_block m' s' (j-1) posts" + unfolding loop_ih_optimizations_def + proof (rule allI | rule impI)+ + fix j' ns1' + assume "j' \ j-1" and + j'Step: "A,M,\,\,\,G \(Inl src_block, Normal ns1') -n\^j' (m', s')" and + TargetVer: "\m1' s1'. (A,M,\,\,\,G' \(Inl tgt_block, Normal ns1') -n\* (m1', s1')) \ valid_configuration A \ \ \ posts m1' s1'" + show "valid_configuration A \ \ \ posts m' s'" + using less.IH + proof - + have strictlySmaller: "j' < j" + using "2"(1) \j' \ j - 1\ verit_comp_simplify1(3) by linarith + have loopIHHolds: "\(LoopHead, LoopHead')\lsLoopHead. loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' j' posts" + using less.prems(4) loop_ih_optimizations_more_less + by (metis (no_types, lifting) \j' \ j - 1\ case_prodD case_prodI2 loop_ih_optimizations_one_less) + thus "valid_configuration A \ \ \ posts m' s'" + using j'Step TargetVer less.IH strictlySmaller GlobalBlockSucc loopIHHolds + by blast + qed + qed + have globalBlockLoopHolds: "global_block_lemma_loop A M \ \ \ G G' succ (f(succ)) lsSubsetList posts" + using True by simp + have steps: "A,M,\,\,\,G \(Inl succ, Normal ns') -n\^(j - 1) (m', s')" + using "2"(1) "2"(3) local.RedNormalSucc(1) local.RedNormalSucc(2) by force + have succVerifies: "\m1' s1'. (A,M,\,\,\,G' \(Inl (f succ), Normal ns') -n\* (m1', s1')) \ valid_configuration A \ \ \ posts m1' s1'" + apply (rule target_verifies[where ?c = tgt_block]) + apply (rule oneStepG) + apply (simp add: NotCoalesced SourceBlock TargetBlock) + apply (simp add: less.prems(1)) + using succInList FunctionCorr in_set_member by fastforce + have "\(LoopHead, LoopHead')\lsLoopHead \ {(src_block, tgt_block)}. loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' (j - 1) posts" + using IH loop_ih_optimizations_one_less loopIHSrcTgt less.prems(4) Un_iff + by blast + hence "\(LoopHead, LoopHead')\lsSubsetList. loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' (j - 1) posts" + using elem by auto + then show ?thesis + using globalBlockLoopHolds steps succVerifies + unfolding global_block_lemma_loop_def + by blast + next + case False + hence SuccEqLoopHead: "succ = LoopHeadG \ f(succ) = LoopHeadG'" + using cond by auto + then show ?thesis + proof (cases "(LoopHeadG, LoopHeadG') = (src_block, tgt_block)") + case True + have srcAgain: "A,M,\,\,\,G \(Inl src_block, Normal ns') -n\^(j-1) (m', s')" + using "2"(1) "2"(3) SuccEqLoopHead True local.RedNormalSucc(1) local.RedNormalSucc(2) by auto + have TargetVerifiesAgain: "\m1' s1'. (A,M,\,\,\,G' \(Inl tgt_block, Normal ns') -n\* (m1', s1')) \ valid_configuration A \ \ \ posts m1' s1'" + using TargetVerifies + by (metis FunctionCorr NotCoalesced Pair_inject SourceBlock SuccEqLoopHead TargetBlock True converse_rtranclp_into_rtranclp in_set_member less.prems(1) local.RedNormalSucc(3) local.RedNormalSucc(4) red_cfg.RedNormalSucc succInList) + have strictlySmaller: "j-1(LoopHead,LoopHead')\lsLoopHead. loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' (j-1) posts" + using less(5) loop_ih_optimizations_one_less + by blast + then show ?thesis + using less.IH srcAgain TargetVerifiesAgain less(4) strictlySmaller + by presburger + next + case False + hence "(LoopHeadG, LoopHeadG') \ (lsLoopHead)" + using elem by auto + hence loopIH: "loop_ih_optimizations A M \ \ \ G G' LoopHeadG LoopHeadG' m' s' j posts" + using less.prems(4) + by fastforce + have "A,M,\,\,\,G \(Inl succ, Normal ns') -n\^m (m', s')" + using "2"(3) local.RedNormalSucc(1) local.RedNormalSucc(2) by auto + hence stepsFromSucc: "A,M,\,\,\,G \(Inl succ, Normal ns') -n\^(j-1) (m', s')" + using \j = Suc m\ + by simp + have "\m1' s1'. (A,M,\,\,\,G' \(Inl (f succ), Normal ns') -n\* (m1', s1')) \ valid_configuration A \ \ \ posts m1' s1'" + apply (rule target_verifies[where ?c = tgt_block]) + apply (rule oneStepG) + apply (simp add: NotCoalesced SourceBlock TargetBlock) + apply (simp add: less.prems(1)) + using succInList FunctionCorr in_set_member by fastforce + then show ?thesis + using stepsFromSucc loopIH SuccEqLoopHead + unfolding loop_ih_optimizations_def + by (meson diff_le_self) + qed + qed + next + case (RedNormalReturn cs ns') + have "A,M,\,\,\ \ \tgt_cmds, Normal ns\ [\] s'" + by (metis "2"(3) NotCoalesced Pair_inject SourceBlock finished_remains local.RedNormalReturn(1) local.RedNormalReturn(2) local.RedNormalReturn(3) local.RedNormalReturn(4) relpowp_imp_rtranclp) + hence "A,M,\,\,\,G' \(Inl tgt_block, Normal ns) -n\ (m', s')" + using NotCoalesced TargetBlock RedNormalReturn NoSuccEq + by (metis "2"(3) SourceBlock SuccBlocks finished_remains red_cfg.RedNormalReturn relpowp_imp_rtranclp) + + then show ?thesis + unfolding valid_configuration_def + using TargetVerifies + by (meson less.prems(1) r_into_rtranclp valid_configuration_def) + next + case (RedFailure cs) + then show ?thesis + by (simp add: OneStepResult) + next + case (RedMagic cs) + then show ?thesis + by (simp add: False) + qed + qed + qed + qed +qed + + +subsubsection \Main Lemma 3: Reduce the set of loop heads when we know that the loop global block lemma holds\ + +text \The use case for this lemma is when a loop head gets coalesced\ + +lemma loopHead_global_block_hybrid: + assumes OneSucc:"out_edges G ! src_block = [succ]" + and HybridHoldsSucc: "hybrid_block_lemma_loop A M \ \ \ G G' succ tgt_block tgt_cmds_0 (lsLoopHead \ {(src_block, tgt_block)}) posts" + and SrcCmds: "node_to_block G ! src_block = src_cmds" + and TgtCmds: "node_to_block G' ! tgt_block = tgt_cmds" + and CoalescedBlock: "tgt_cmds = src_cmds@tgt_cmds_0" + shows "global_block_lemma_loop A M \ \ \ G G' src_block tgt_block lsLoopHead posts" + unfolding global_block_lemma_loop_def +proof (rule allI | rule impI)+ + fix m' ns s' j + assume k_step: "A,M,\,\,\,G \(Inl src_block, Normal ns) -n\^j (m', s')" and + TargetVerifies: "\m1' s1'. (A,M,\,\,\,G' \(Inl tgt_block, Normal ns) -n\* (m1', s1')) \ valid_configuration A \ \ \ posts m1' s1'" and + IH: "\(LoopHead, LoopHead')\lsLoopHead. loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' j posts" + show "valid_configuration A \ \ \ posts m' s'" using TargetVerifies k_step IH + proof (induction j arbitrary: ns rule: less_induct) + case (less j) + then show ?case + proof (cases rule: relpowp_E2_2[OF less(3)]) + case 1 + then show ?thesis + unfolding valid_configuration_def + by auto + next + case (2 a b m) + from \A,M,\,\,\,G \ (Inl src_block, Normal ns) -n\ (a, b)\ have OneStepResult: "b \ Failure" + proof cases + case (RedNormalSucc cs ns' n') + then show ?thesis + by simp + next + case (RedNormalReturn cs ns') + then show ?thesis + by simp + next + case (RedFailure cs) + then show ?thesis + using valid_configuration_def + by (metis assms(3) assms(4) assms(5) less.prems(1) r_into_rtranclp red_cfg.RedFailure red_cmd_append_failure_preserved) + next + case (RedMagic cs) + then show ?thesis + by simp + qed + then show ?thesis + proof (cases "b = Magic") + case True + have "A,M,\,\,\,G \(a, b) -n\* (m', s')" + by (meson "2"(3) relpowp_imp_rtranclp) + then show ?thesis + using True red_cfg_magic_preserved + unfolding valid_configuration_def + by blast + next + case False + from \A,M,\,\,\,G \ (Inl src_block, Normal ns) -n\ (a, b)\ show ?thesis + proof cases + case (RedNormalSucc cs ns' n') + have "n' = succ" + by (metis OneSucc local.RedNormalSucc(5) member_rec(1) member_rec(2)) + hence mSteps: "A,M,\,\,\,G \(Inl succ, Normal ns') -n\^m (m', s')" + using "2"(3) local.RedNormalSucc(1) local.RedNormalSucc(2) by blast + have "hybrid_block_lemma_target_verifies A M \ \ \ G' tgt_block tgt_cmds ns posts" + apply (rule normal_target_verifies_show_hybrid_verifies) + using less.prems(1) apply blast + by (simp add: TgtCmds) + + hence hybridTargetVerifies: "hybrid_block_lemma_target_verifies A M \ \ \ G' tgt_block tgt_cmds_0 ns' posts" + using less(2) + unfolding hybrid_block_lemma_target_verifies_def + using SrcCmds CoalescedBlock local.RedNormalSucc(3) local.RedNormalSucc(4) red_cmd_list_append by blast + have loopIH: "loop_ih_optimizations A M \ \ \ G G' src_block tgt_block m' s' m posts" + unfolding loop_ih_optimizations_def + proof (rule allI | rule impI)+ + fix j' ns1' + assume "j'\m" and + steps: "A,M,\,\,\,G \(Inl src_block, Normal ns1') -n\^j' (m', s')" and + TarVer: "\m1' s1'. (A,M,\,\,\,G' \(Inl tgt_block, Normal ns1') -n\* (m1', s1')) \ valid_configuration A \ \ \ posts m1' s1'" + show "valid_configuration A \ \ \ posts m' s'" + using less.IH + proof - + have strictlySmaller:"j'j' \ m\ by auto + have "\(LoopHead, LoopHead')\lsLoopHead. loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' j' posts" + using loop_ih_optimizations_more_less less(4) + by (metis (no_types, lifting) \j' < j\ case_prodD case_prodI2 order_less_imp_le) + thus "valid_configuration A \ \ \ posts m' s'" + using strictlySmaller TarVer steps less.IH + by blast + qed + qed + have "m\j" + by (simp add: "2"(1)) + hence "\(LoopHead, LoopHead')\lsLoopHead \ {(src_block, tgt_block)}.loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' m posts" + using loop_ih_optimizations_more_less less(4) loopIH + by blast + then show ?thesis + using HybridHoldsSucc mSteps hybridTargetVerifies + unfolding hybrid_block_lemma_loop_def + by blast + next + case (RedNormalReturn cs ns') + then show ?thesis + by (simp add: OneSucc) + next + case (RedFailure cs) + then show ?thesis + by (simp add: OneStepResult) + next + case (RedMagic cs) + then show ?thesis + by (simp add: False) + qed + qed + qed + qed +qed + + +subsubsection \Main Lemma 4: Shows that the Loop Hybrid Block Lemma holds if a block in a loop was coalesced\ + +lemma loopBlock_global_block_hybrid: + assumes SuccBlocks: "out_edges G ! src_block = ls" + and GlobalBlockSucc: + "\x\set(ls). + (\lsSubsetList. lsSubsetList\lsLoopHead \ global_block_lemma_loop A M \ \ \ G G' x (f x) lsSubsetList posts) + \ (\(LoopHead, LoopHead')\lsLoopHead. (x = LoopHead \ f x = LoopHead'))" + and FunctionCorr: "\x\set(ls). f x \ set (out_edges G' ! tgt_block)" + and SourceBlock: "node_to_block G ! src_block = src_cmds" + and NoSuccEq: "ls = [] \ out_edges G' ! tgt_block = []" + shows "hybrid_block_lemma_loop A M \ \ \ G G' src_block tgt_block src_cmds lsLoopHead posts" + unfolding hybrid_block_lemma_loop_def +proof (rule allI | rule impI)+ + fix m' ns s' j + + assume k_step: "A,M,\,\,\,G \(Inl src_block, Normal ns) -n\^j (m', s')" and + IH: "\(LoopHead, LoopHead')\lsLoopHead. loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' j posts" and + TargetVerifies: "hybrid_block_lemma_target_verifies A M \ \ \ G' tgt_block src_cmds ns posts" + + show "valid_configuration A \ \ \ posts m' s'" + proof (cases rule: relpowp_E2_2[OF k_step]) + case 1 + then show ?thesis + unfolding valid_configuration_def + using is_final_config.simps(1) by blast + next + case (2 a b m) + from \A,M,\,\,\,G \ (Inl src_block, Normal ns) -n\ (a, b)\ have OneStepResult: "b \ Failure" + proof cases + case (RedNormalSucc cs ns' n') + then show ?thesis by blast + next + case (RedNormalReturn cs ns') + then show ?thesis by blast + next + case (RedFailure cs) + then show ?thesis + by (metis SourceBlock TargetVerifies hybrid_block_lemma_target_verifies_def valid_configuration_def) + next + case (RedMagic cs) + then show ?thesis by blast + qed + then show ?thesis + proof (cases "b = Magic") + case True + have "A,M,\,\,\,G \(a, b) -n\* (m', s')" + by (meson "2"(3) rtranclp_power) + then show ?thesis + unfolding valid_configuration_def + using True red_cfg_magic_preserved + by blast + next + case False + from \A,M,\,\,\,G \ (Inl src_block, Normal ns) -n\ (a, b)\ show ?thesis + proof cases + case (RedNormalSucc cs ns' succ) + have succInList: "succ \ set(ls)" + using SuccBlocks in_set_member local.RedNormalSucc(5) by force + have oneStepG: "A,M,\,\,\,G \ (Inl src_block, Normal ns) -n\ (Inl succ, Normal ns')" + using "2"(2) local.RedNormalSucc(1) local.RedNormalSucc(2) by auto + then show ?thesis + proof (cases "\lsSubsetList. lsSubsetList\lsLoopHead \ global_block_lemma_loop A M \ \ \ G G' succ (f(succ)) lsSubsetList posts") + case True + from this obtain lsSubset where subset: "lsSubset\lsLoopHead" and globalBlockLoop: "global_block_lemma_loop A M \ \ \ G G' succ (f(succ)) lsSubset posts" + by auto + + have mSteps: "A,M,\,\,\,G \(Inl succ, Normal ns') -n\^m (m', s')" + using "2"(3) local.RedNormalSucc(1) local.RedNormalSucc(2) by auto + have "m\j" + by (simp add: "2"(1)) + then have "\(LoopHead, LoopHead')\lsLoopHead. loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' m posts" + using loop_ih_optimizations_more_less IH + by blast + then have IH_holds: "\(LoopHead, LoopHead')\lsSubset. loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' m posts" + using subset by blast + + have transCl: "A,M,\,\,\,G \(Inl succ, Normal ns') -n\* (m', s')" + by (metis "2"(3) local.RedNormalSucc(1) local.RedNormalSucc(2) relpowp_imp_rtranclp) + + have "\m1' s1'.( A,M,\,\,\,G' \(Inl (f(succ)), Normal ns') -n\* (m1', s1')) \ valid_configuration A \ \ \ posts m1' s1'" + using GlobalBlockSucc TargetVerifies + unfolding hybrid_block_lemma_target_verifies_def hybrid_block_lemma_target_succ_verifies_def + by (metis (mono_tags, lifting) FunctionCorr SourceBlock in_set_member local.RedNormalSucc(3) local.RedNormalSucc(4) succInList) + + then show ?thesis + using True IH_holds mSteps subset globalBlockLoop + unfolding global_block_lemma_loop_def + by presburger + next + case False + from this obtain LoopHeadG LoopHeadG' where + cond: "global_block_lemma_loop A M \ \ \ G G' succ (f(succ)) lsLoopHead posts \ (succ = LoopHeadG \ f(succ) = LoopHeadG')" + and inList: "(LoopHeadG, LoopHeadG')\lsLoopHead" + using GlobalBlockSucc case_prodE succInList by fastforce + then show ?thesis + proof (cases "global_block_lemma_loop A M \ \ \ G G' succ (f(succ)) lsLoopHead posts") + case True + have "loop_ih_optimizations A M \ \ \ G G' LoopHeadG LoopHeadG' m' s' j posts" + using IH inList + by blast + hence "loop_ih_optimizations A M \ \ \ G G' LoopHeadG LoopHeadG' m' s' (j - 1) posts" + using IH + unfolding loop_ih_optimizations_def + by (meson less_imp_diff_less linorder_not_less) + + have loopIH: "\(LoopHead, LoopHead')\lsLoopHead. loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' (j - 1) posts" + using IH loop_ih_optimizations_one_less + by blast + + have steps: "A,M,\,\,\,G \(Inl succ, Normal ns') -n\^(j - 1) (m', s')" + using "2"(1) "2"(3) local.RedNormalSucc(1) local.RedNormalSucc(2) by auto + + have "\m1' s1'.( A,M,\,\,\,G' \(Inl (f(succ)), Normal ns') -n\* (m1', s1')) \ valid_configuration A \ \ \ posts m1' s1'" + using GlobalBlockSucc TargetVerifies + unfolding hybrid_block_lemma_target_verifies_def hybrid_block_lemma_target_succ_verifies_def + by (metis (no_types, opaque_lifting) FunctionCorr SourceBlock in_set_member local.RedNormalSucc(3) local.RedNormalSucc(4) succInList) + then show ?thesis + using True loopIH steps + unfolding global_block_lemma_loop_def + by presburger + next + case False + hence SuccEqLoopHead: "succ = LoopHeadG \ f(succ) = LoopHeadG'" + using GlobalBlockSucc succInList cond + by force + + have verifies: "\m1' s1'.( A,M,\,\,\,G' \(Inl (f(succ)), Normal ns') -n\* (m1', s1')) \ valid_configuration A \ \ \ posts m1' s1'" + using GlobalBlockSucc TargetVerifies + unfolding hybrid_block_lemma_target_verifies_def hybrid_block_lemma_target_succ_verifies_def + by (metis (mono_tags, lifting) FunctionCorr SourceBlock in_set_member local.RedNormalSucc(3) local.RedNormalSucc(4) succInList) + + have "loop_ih_optimizations A M \ \ \ G G' LoopHeadG LoopHeadG' m' s' j posts" + using IH inList + by fastforce + + then show ?thesis + using SuccEqLoopHead verifies + unfolding loop_ih_optimizations_def + by (metis "2"(1) "2"(3) diff_Suc_1 diff_le_self local.RedNormalSucc(1) local.RedNormalSucc(2)) + qed + qed + next + case (RedNormalReturn cs ns') + have "out_edges G' ! tgt_block = []" + using NoSuccEq SuccBlocks local.RedNormalReturn(5) by auto + have "m' = Inr()" + by (metis "2"(3) Pair_inject finished_remains local.RedNormalReturn(1) relpowp_imp_rtranclp) + then show ?thesis + using TargetVerifies + unfolding hybrid_block_lemma_target_verifies_def valid_configuration_def + by (metis "2"(3) Pair_inject SourceBlock \out_edges G' ! tgt_block = []\ finished_remains local.RedNormalReturn(1) local.RedNormalReturn(2) local.RedNormalReturn(3) local.RedNormalReturn(4) relpowp_imp_rtranclp) + next + case (RedFailure cs) + then show ?thesis + by (simp add: OneStepResult) + next + case (RedMagic cs) + then show ?thesis + by (simp add: False) + qed + qed + qed +qed + + +subsubsection \Main lemma 5 (extending hybrid global block lemmas for loops)\ + +text \The following lemma shows that given the loop hybrid global block lemma for block i, we can construct +the loop hybrid block lemma for block i-1. Below the suffix 1 is used for i and 0 is used for i-1.\ + +lemma extend_hybrid_global_block_lemma_loop: + assumes NextGlobal: "hybrid_block_lemma_loop A M \ \ \ G G' src_block_1 tgt_block tgt_cmds_1 lsLoopHead posts" + and SourceBlock: "node_to_block G ! src_block_0 = cs" + and SourceSucc: "out_edges G ! src_block_0 = [src_block_1]" + "tgt_cmds_0 = cs@tgt_cmds_1" + shows + "hybrid_block_lemma_loop A M \ \ \ G G' src_block_0 tgt_block tgt_cmds_0 lsLoopHead posts" + unfolding hybrid_block_lemma_loop_def +proof (rule allI | rule impI)+ \\Here, we are applying initial proof rule to get rid of universal quantifiers and implications\ + fix m' ns s' j + assume k_step: "A,M,\,\,\,G \(Inl src_block_0, Normal ns) -n\^j (m', s')" and + TargetVerifies: "hybrid_block_lemma_target_verifies A M \ \ \ G' tgt_block tgt_cmds_0 ns posts" and + IH: "\(LoopHead, LoopHead')\lsLoopHead. loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' j posts" + show "valid_configuration A \ \ \ posts m' s'" + proof (cases rule: relpowp_E2_2[OF k_step]) + case 1 + then show ?thesis + unfolding valid_configuration_def + using is_final_config.simps(1) by blast + next + case (2 b s0) + from \A,M,\,\,\,G \ (Inl src_block_0, Normal ns) -n\ (b, s0)\ + have OneStepResult: "s0 \ Failure \ (\ns0. (s0 = Normal ns0 \ b = Inl src_block_1 \ + A,M,\,\,\ \ \cs,Normal ns\ [\] Normal ns0))" + proof cases + case (RedNormalSucc cs ns' n') + then show ?thesis + using SourceSucc SourceBlock + by (simp add: member_rec(1) member_rec(2)) + next + case (RedNormalReturn cs ns') + then show ?thesis + using SourceSucc + by simp + next + case (RedFailure cs) + hence "A,M,\,\,\ \ \cs@tgt_cmds_1,Normal ns\ [\] Failure" + using red_cmd_append_failure_preserved + by fast + hence False + using TargetVerifies \ node_to_block G ! src_block_0 = cs\ \tgt_cmds_0 = _\ SourceBlock + unfolding hybrid_block_lemma_target_verifies_def + by (metis valid_configuration_def) + thus ?thesis + by simp + next + case (RedMagic cs) + then show ?thesis by auto + qed + + show ?thesis + proof (cases "s0 = Magic") + case True + have "A,M,\,\,\,G \(b, s0) -n\* (m', s')" + by (meson "2"(3) relpowp_imp_rtranclp) + thus "valid_configuration A \ \ \ posts m' s'" + using red_cfg_magic_preserved[OF \A,M,\,\,\,G \(b, s0) -n\* (m', s')\] True + unfolding valid_configuration_def + by blast + next + case False + from this obtain ns0 where "s0 = Normal ns0" + using OneStepResult state.exhaust by auto + + hence RedBlock0: "A,M,\,\,\ \ \cs,Normal ns\ [\] Normal ns0" + and RedSuccBlock: "A,M,\,\,\,G \(Inl src_block_1, Normal ns0) -n\^(j-1) (m', s')" + using OneStepResult apply auto[1] + using "2"(1) "2"(3) OneStepResult \s0 = Normal ns0\ by auto + + show ?thesis + proof (rule hybrid_block_lemma_loop_elim[OF NextGlobal RedSuccBlock]) + show "hybrid_block_lemma_target_verifies A M \ \ \ G' tgt_block tgt_cmds_1 ns0 posts" + unfolding hybrid_block_lemma_target_verifies_def + proof (rule allI, rule impI, rule conjI) + fix s1' + assume "A,M,\,\,\ \ \tgt_cmds_1,Normal ns0\ [\] s1'" + with RedBlock0 have "A,M,\,\,\ \ \cs@tgt_cmds_1,Normal ns\ [\] s1'" + by (simp add: red_cmd_list_append) + thus "if out_edges G' ! tgt_block = [] then valid_configuration A \ \ \ posts (Inr ()) s1' else s1' \ Failure" + using TargetVerifies \tgt_cmds_0 = cs @ tgt_cmds_1\ + unfolding hybrid_block_lemma_target_verifies_def + by simp + next + fix s1' + assume "A,M,\,\,\ \ \tgt_cmds_1,Normal ns0\ [\] s1'" + with RedBlock0 have RedTgtCmds0:"A,M,\,\,\ \ \tgt_cmds_0 ,Normal ns\ [\] s1'" + using \tgt_cmds_0 = _\ + by (simp add: red_cmd_list_append) + + + thus "hybrid_block_lemma_target_succ_verifies A M \ \ \ G' tgt_block s1' posts" + using TargetVerifies + unfolding hybrid_block_lemma_target_verifies_def + by fast + qed + + show "\(LoopHead, LoopHead')\lsLoopHead. loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' (j-1) posts" + using IH loop_ih_optimizations_one_less + by blast + qed + qed + qed +qed + +subsubsection \Main lemma 6 (converting loop hybrid global block lemma to normal loop global block lemma)\ + +lemma convert_hybrid_global_block_lemma_loop: + assumes HybridGlobal: "hybrid_block_lemma_loop A M \ \ \ G G' src_block tgt_block tgt_cmds lsLoopHead posts" + and TargetBlock: "node_to_block G' ! tgt_block = tgt_cmds" + shows "global_block_lemma_loop A M \ \ \ G G' src_block tgt_block lsLoopHead posts" + unfolding global_block_lemma_loop_def +proof (rule allI | rule impI)+ + fix m' ns s' j + assume RedSource: "A,M,\,\,\,G \(Inl src_block, Normal ns) -n\^j (m', s')" and + TargetVerifies: "\m1' s1'. (A,M,\,\,\,G' \(Inl tgt_block, Normal ns) -n\* (m1', s1')) \ valid_configuration A \ \ \ posts m1' s1'" and + IH: "\(LoopHead, LoopHead')\lsLoopHead. loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' j posts" + show "valid_configuration A \ \ \ posts m' s'" + proof (rule hybrid_block_lemma_loop_elim[OF HybridGlobal RedSource]) + show "hybrid_block_lemma_target_verifies A M \ \ \ G' tgt_block tgt_cmds ns posts" + unfolding hybrid_block_lemma_target_verifies_def + proof (rule allI, rule impI) + fix s1' + assume RedTgtCmds: "A,M,\,\,\ \ \tgt_cmds,Normal ns\ [\] s1'" + + have "s1' \ Failure" + proof (rule ccontr) + assume "\ s1' \ Failure" + hence "s1' = Failure" by simp + have "(A,M,\,\,\,G' \(Inl tgt_block, Normal ns) -n\* (Inr (), Failure))" + apply (rule converse_rtranclp_into_rtranclp) + apply (rule RedFailure) + apply (rule TargetBlock) + using RedTgtCmds \s1' = Failure\ + apply blast + by simp + thus False + using TargetVerifies + unfolding valid_configuration_def + by blast + qed + moreover have "hybrid_block_lemma_target_succ_verifies A M \ \ \ G' tgt_block s1' posts" + proof (rule hybrid_block_lemma_target_succ_verifies_intro) + fix ns1' tgt_succ m2' s2' + assume "s1' = Normal ns1'" and + TargetSucc: "List.member (out_edges G' ! tgt_block) tgt_succ" and + RedTargetSucc: "A,M,\,\,\,G' \(Inl tgt_succ, Normal ns1') -n\* (m2', s2')" + + text \We can construct an execution beginning from \<^term>\tgt_block\\ + have "A,M,\,\,\,G' \(Inl tgt_block, Normal ns) -n\* (m2', s2')" + apply (rule converse_rtranclp_into_rtranclp) + apply (rule RedNormalSucc) + apply (rule TargetBlock) + using RedTgtCmds \s1' = Normal ns1'\ + apply blast + apply (rule TargetSucc) + apply (rule RedTargetSucc) + done + + thus "valid_configuration A \ \ \ posts m2' s2'" + using TargetVerifies + by blast + qed + + ultimately show + "(if out_edges G' ! tgt_block = [] then valid_configuration A \ \ \ posts (Inr ()) s1' else s1' \ Failure) \ hybrid_block_lemma_target_succ_verifies A M \ \ \ G' tgt_block s1' posts" + by (metis RedNormalReturn RedTgtCmds TargetBlock TargetVerifies r_into_rtranclp valid_configuration_def) + qed + + show "\(LoopHead, LoopHead')\lsLoopHead. loop_ih_optimizations A M \ \ \ G G' LoopHead LoopHead' m' s' j posts" + using IH by auto + qed +qed + +subsubsection \Main Lemma 7: Following Lemma shows correctness of pruning of unreachable blocks if the block was not coalesced\ + +lemma pruning_not_coalesced_loop: + assumes SuccBlocks: "out_edges G ! src_block = ls" + and TargetBlock: "node_to_block G' ! tgt_block = tgt_cmds" + and SourceBlock: "node_to_block G ! src_block = src_cmds" + and Pruning: "(Assume (Lit (LBool False))) \ set (src_cmds) \ (Assert (Lit (LBool False))) \ set (src_cmds)" + and NotCoalesced: "tgt_cmds = src_cmds" + and NoSuccEq: "ls = [] \ out_edges G' ! tgt_block = []" + shows "global_block_lemma_loop A M \ \ \ G G' src_block tgt_block lsLoopHead posts" + unfolding global_block_lemma_loop_def +proof (rule allI | rule impI)+ + fix m' ns s' j + assume k_step: "A,M,\,\,\,G \(Inl src_block, Normal ns) -n\^j (m', s')" and + TargetVerifies: "\m1' s1'.( A,M,\,\,\,G' \(Inl tgt_block, Normal ns) -n\* (m1', s1')) \ valid_configuration A \ \ \ posts m1' s1'" + show "valid_configuration A \ \ \ posts m' s'" + proof - + from k_step have RedSource: "A,M,\,\,\,G \(Inl src_block, Normal ns) -n\* (m', s')" + by (simp add: relpowp_imp_rtranclp) + show ?thesis + proof (cases rule: converse_rtranclpE2[OF RedSource]) + case 1 + then show ?thesis + unfolding valid_configuration_def + using is_final_config.simps(1) by blast + next + case (2 a b) + from \A,M,\,\,\,G \ (Inl src_block, Normal ns) -n\ (a, b)\ show ?thesis + proof cases + case (RedNormalSucc cs ns' n') + have "(Assume (Lit (LBool False))) \ set (cs) \ (Assert (Lit (LBool False))) \ set (cs)" + using Pruning SourceBlock local.RedNormalSucc(3) by blast + then show ?thesis + proof (cases "(Assume (Lit (LBool False))) \ set (cs)") + case True + hence "b = Magic" + using local.RedNormalSucc(4) magic_lemma_assume_false by blast + then show ?thesis + by (simp add: local.RedNormalSucc(2)) + next + case False + hence "b = Magic \ b = Failure" + using \Assume (Lit (LBool False)) \ set cs \ Assert (Lit (LBool False)) \ set cs\ local.RedNormalSucc(4) magic_lemma_assert_false + by blast + then show ?thesis + by (simp add: local.RedNormalSucc(2)) + qed + next + case (RedNormalReturn cs ns') + have "A,M,\,\,\ \ \tgt_cmds, Normal ns\ [\] s'" + by (metis "2"(2) NotCoalesced Pair_inject SourceBlock finished_remains local.RedNormalReturn(1) local.RedNormalReturn(2) local.RedNormalReturn(3) local.RedNormalReturn(4)) + hence "A,M,\,\,\,G' \(Inl tgt_block, Normal ns) -n\ (m', s')" + using NotCoalesced TargetBlock RedNormalReturn NoSuccEq + "2"(2) SuccBlocks finished_remains red_cfg.RedNormalReturn + by blast + then show ?thesis + unfolding valid_configuration_def + using TargetVerifies valid_configuration_def by blast + next + case (RedFailure cs) + then show ?thesis + unfolding valid_configuration_def + by (metis NotCoalesced SourceBlock TargetBlock TargetVerifies r_into_rtranclp red_cfg.RedFailure valid_configuration_def) + next + case (RedMagic cs) + then show ?thesis + unfolding valid_configuration_def + using "2"(2) red_cfg_magic_preserved by blast + qed + qed + qed +qed + +subsubsection \Main Lemma 8: Following Lemma shows correctness of pruning of unreachable blocks if the block was coalesced\ + +lemma pruning_coalesced_loop: + assumes TargetBlock: "node_to_block G' ! tgt_block = tgt_cmds" + and SourceBlock: "node_to_block G ! src_block = src_cmds" + and Pruning: "(Assert (Lit (LBool False))) \ set (src_cmds) \ (Assume (Lit (LBool False))) \ set (src_cmds)" + and Coalesced: "tgt_cmds = cs@src_cmds" + and NoSuccEq: "out_edges G ! src_block = [] \ out_edges G' ! tgt_block = []" + shows "hybrid_block_lemma_loop A M \ \ \ G G' src_block tgt_block src_cmds lsLoopHead posts" + unfolding hybrid_block_lemma_loop_def +proof (rule allI | rule impI)+ + fix m' ns s' j + assume k_step: "A,M,\,\,\,G \(Inl src_block, Normal ns) -n\^j (m', s')" and + TargetVerifies: "hybrid_block_lemma_target_verifies A M \ \ \ G' tgt_block src_cmds ns posts" + show "valid_configuration A \ \ \ posts m' s'" + proof - + have RedSource: "A,M,\,\,\,G \(Inl src_block, Normal ns) -n\* (m', s')" + by (meson k_step rtranclp_power) + show ?thesis + proof (cases rule: converse_rtranclpE2[OF RedSource]) + case 1 + then show ?thesis + unfolding valid_configuration_def + by fastforce + next + case (2 a b) + from \A,M,\,\,\,G \ (Inl src_block, Normal ns) -n\ (a, b)\ show ?thesis + proof cases + case (RedNormalSucc cs ns' n') + have "(Assume (Lit (LBool False))) \ set (cs) \ (Assert (Lit (LBool False))) \ set (cs)" + using Pruning SourceBlock local.RedNormalSucc(3) by blast + then show ?thesis + proof (cases "(Assume (Lit (LBool False))) \ set (cs)") + case True + hence "b = Magic" + using local.RedNormalSucc(4) magic_lemma_assume_false by blast + then show ?thesis + by (simp add: local.RedNormalSucc(2)) + next + case False + hence "b = Magic \ b = Failure" + using \Assume (Lit (LBool False)) \ set cs \ Assert (Lit (LBool False)) \ set cs\ local.RedNormalSucc(4) magic_lemma_assert_false + by blast + then show ?thesis + by (simp add: local.RedNormalSucc(2)) + qed + next + case (RedNormalReturn cs ns') + have "out_edges G' ! tgt_block = []" + by (simp add: NoSuccEq local.RedNormalReturn(5)) + have "m' = Inr()" + using BlockID_no_succ + by (metis "2"(1) "2"(2) finished_remains local.RedNormalReturn(5)) + then show ?thesis + using TargetVerifies + unfolding hybrid_block_lemma_target_verifies_def valid_configuration_def + by (metis "2"(2) Pair_inject SourceBlock \out_edges G' ! tgt_block = []\ finished_remains local.RedNormalReturn(1) local.RedNormalReturn(2) local.RedNormalReturn(3) local.RedNormalReturn(4)) + next + case (RedFailure cs) + then show ?thesis + using SourceBlock TargetVerifies hybrid_block_lemma_target_verifies_def + by (metis valid_configuration_def) + next + case (RedMagic cs) + then show ?thesis + unfolding valid_configuration_def + using "2"(2) red_cfg_magic_preserved by blast + qed + qed + qed +qed + +end \ No newline at end of file diff --git a/BoogieLang/HelperML.thy b/BoogieLang/HelperML.thy index 65613a4..f368689 100644 --- a/BoogieLang/HelperML.thy +++ b/BoogieLang/HelperML.thy @@ -13,7 +13,9 @@ fun assm_full_simp_solved_tac ctxt = (asm_full_simp_tac ctxt |> SOLVED') fun assm_full_simp_solved_with_thms_tac thms ctxt = (asm_full_simp_tac (add_simps thms ctxt) |> SOLVED') fun fastforce_tac ctxt thms = Clasimp.fast_force_tac (add_simps thms ctxt) -\ + +fun simp_only_tac thms ctxt = asm_full_simp_tac (add_simps thms (Simplifier.clear_simpset ctxt)) +\ ML \ diff --git a/BoogieLang/Lang.thy b/BoogieLang/Lang.thy index b799431..3601a9d 100644 --- a/BoogieLang/Lang.thy +++ b/BoogieLang/Lang.thy @@ -94,31 +94,31 @@ CFG of a procedure body is represented by: text \Procedure pre- and postconditions contain a boolean to indicate whether they are free (true) or checked (false).\ -record procedure = +record 'struct_ty procedure = proc_ty_args :: nat proc_args :: vdecls proc_rets :: vdecls proc_modifs :: "vname list" proc_pres :: "(expr \ bool) list" proc_posts :: "(expr \ bool) list" - proc_body :: "(vdecls \ mbodyCFG) option" + proc_body :: "(vdecls \ 'struct_ty) option" -fun proc_checked_pres :: "procedure \ expr list" +fun proc_checked_pres :: "'struct_ty procedure \ expr list" where "proc_checked_pres p = map fst (filter (\x. \ snd(x)) (proc_pres p))" -fun proc_free_pres :: "procedure \ expr list" +fun proc_free_pres :: "'struct_ty procedure \ expr list" where "proc_free_pres p = map fst (filter (\x. snd(x)) (proc_pres p))" -fun proc_all_pres :: "procedure \ expr list" +fun proc_all_pres :: "'struct_ty procedure \ expr list" where "proc_all_pres p = map fst (proc_pres p)" -fun proc_checked_posts :: "procedure \ expr list" +fun proc_checked_posts :: "'struct_ty procedure \ expr list" where "proc_checked_posts p = map fst (filter (\x. \ snd(x)) (proc_posts p))" -fun proc_all_posts :: "procedure \ expr list" +fun proc_all_posts :: "'struct_ty procedure \ expr list" where "proc_all_posts p = map fst (proc_posts p)" -fun proc_free_posts :: "procedure \ expr list" +fun proc_free_posts :: "'struct_ty procedure \ expr list" where "proc_free_posts p = map fst (filter (\x. snd(x)) (proc_posts p))" definition exprs_to_only_checked_spec :: "expr list \ (expr \ bool) list" @@ -135,18 +135,18 @@ lemma exprs_to_only_checked_spec_2: "es = map fst (filter (\x. \ sn unfolding exprs_to_only_checked_spec_def by (induction es) auto -type_synonym pdecl = "pname \ procedure" +type_synonym 'struct_ty pdecl = "pname \ 'struct_ty procedure" text \An axiom is a boolean expression that can refer to constants.\ 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 \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 diff --git a/BoogieLang/Passification.thy b/BoogieLang/Passification.thy index e95fd19..0089a80 100644 --- a/BoogieLang/Passification.thy +++ b/BoogieLang/Passification.thy @@ -27,7 +27,7 @@ lemma dependent_ext: unfolding dependent_def by blast -definition set_red_cmd :: "'a absval_ty_fun \ proc_context \ var_context \ 'a fun_interp \ rtype_env \ cmd \ 'a nstate set \ 'a state set" +definition set_red_cmd :: "'a absval_ty_fun \ 'm proc_context \ var_context \ 'a fun_interp \ rtype_env \ cmd \ 'a nstate set \ 'a state set" where "set_red_cmd A M \ \ \ c N = {s. \n_s. n_s \ N \ A,M,\,\,\ \ \c, Normal n_s\ \ s}" text \\<^term>\set_red_cmd\ lifts the command reduction to the reduction of a a set of input states \ @@ -1211,7 +1211,7 @@ definition passive_block_conclusion where "passive_block_conclusion A M \ \' \ \ U0 D1 R R_old cs2 s' = (s' \ Magic \ (\ U1 \ U0. U1 \ {} \ dependent A \' \ U1 D1 \ passive_sim A M \ \' \ \ cs2 s' R R_old U1))" -definition passive_lemma_assms :: "'a absval_ty_fun \ proc_context \ var_context \ var_context \ +definition passive_lemma_assms :: "'a absval_ty_fun \ 'struct_ty proc_context \ var_context \ var_context \ 'a fun_interp \ rtype_env \ vname list \ passive_rel \ passive_rel \ ('a nstate) set \ vname set \ 'a nstate \ bool" where "passive_lemma_assms A M \ \' \ \ W R R_old U0 D0 ns = @@ -1254,7 +1254,7 @@ definition passive_sim_cfg_fail definition dependent_2 where "dependent_2 A \' \ U0 m = dependent A \' \ U0 {y. y \ m}" -definition passive_lemma_assms_2 :: "'a absval_ty_fun \ proc_context \ var_context \ var_context \ +definition passive_lemma_assms_2 :: "'a absval_ty_fun \ 'struct_ty proc_context \ var_context \ var_context \ 'a fun_interp \ rtype_env \ vname \ passive_rel \ passive_rel \ ('a nstate) set \ vname set \ 'a nstate \ bool" where "passive_lemma_assms_2 A M \ \' \ \ w_min R R_old U0 D0 ns = diff --git a/BoogieLang/ROOT b/BoogieLang/ROOT index 4cbda4b..c803af1 100644 --- a/BoogieLang/ROOT +++ b/BoogieLang/ROOT @@ -16,3 +16,6 @@ session Boogie_Lang = "HOL" + PassificationEndToEnd PassificationML BackedgeElim + CFGOptimizationsLoop + Ast + Ast_Cfg_Transformation \ No newline at end of file diff --git a/BoogieLang/Semantics.thy b/BoogieLang/Semantics.thy index eeef2f3..8645ace 100644 --- a/BoogieLang/Semantics.thy +++ b/BoogieLang/Semantics.thy @@ -111,8 +111,8 @@ should not happen).\ definition update_var :: "var_context \ 'a nstate \ vname \ 'a val \ 'a nstate" where "update_var \ n_s x v = - (case (map_of (snd \) x) of Some res \ n_s\local_state := local_state(n_s)(x \ v)\ | - None \ n_s\global_state := global_state(n_s)(x \ v) \)" + (case (map_of (snd \) x) of Some res \ n_s\local_state := (local_state(n_s))(x \ v) \ | + None \ n_s\global_state := (global_state(n_s))(x \ v) \)" definition update_var_opt :: "var_context \ 'a nstate \ vname \ 'a val option \ 'a nstate" where @@ -414,7 +414,7 @@ fun instantiate :: "rtype_env \ ty \ ty" lemma instantiate_nil [simp]: "instantiate [] \ = \" by (induction \) (simp_all add: map_idI) -type_synonym proc_context = "pdecl list" +type_synonym 'struct_ty proc_context = "'struct_ty pdecl list" subsection \Expression reduction (big-step semantics)\ @@ -520,9 +520,9 @@ definition where_clauses_all_sat_context :: "'a absval_ty_fun \ var_ subsection \Command reduction (big-step semantics)\ -inductive red_cmd :: "'a absval_ty_fun \ proc_context \ var_context \ 'a fun_interp \ rtype_env \ cmd \ 'a state \ 'a state \ bool" +inductive red_cmd :: "'a absval_ty_fun \ 'm proc_context \ var_context \ 'a fun_interp \ rtype_env \ cmd \ 'a state \ 'a state \ bool" ("_,_,_,_,_ \ ((\_,_\) \/ _)" [51,51,0,0,0] 81) - for A :: "'a absval_ty_fun" and M :: proc_context and \ :: var_context and \ :: "'a fun_interp" and \ :: rtype_env + for A :: "'a absval_ty_fun" and M :: "'m proc_context" and \ :: var_context and \ :: "'a fun_interp" and \ :: rtype_env where RedAssertOk: "\ A,\,\,\ \ \e, n_s\ \ LitV (LBool True) \ \ A,M,\,\,\ \ \Assert e, Normal n_s\ \ Normal n_s" @@ -574,9 +574,9 @@ inductive_cases RedHavoc_case: "A,M,\,\,\ \ \Command list reduction (big-step semantics)\ -inductive red_cmd_list :: "'a absval_ty_fun \ proc_context \ var_context \ 'a fun_interp \ rtype_env \ cmd list \ 'a state \ 'a state \ bool" +inductive red_cmd_list :: "'a absval_ty_fun \ 'm proc_context \ var_context \ 'a fun_interp \ rtype_env \ cmd list \ 'a state \ 'a state \ bool" ("_,_,_,_,_ \ ((\_,_\) [\]/ _)" [51,0,0,0] 81) - for A :: "'a absval_ty_fun" and M :: proc_context and \ :: var_context and \ :: "'a fun_interp" and \ :: rtype_env + for A :: "'a absval_ty_fun" and M :: "'m proc_context" and \ :: var_context and \ :: "'a fun_interp" and \ :: rtype_env where RedCmdListNil: "A,M,\,\,\ \ \[],s\ [\] s" | RedCmdListCons: "\ A,M,\,\,\ \ \c,s\ \ s''; A,M,\,\,\ \ \cs,s''\ [\] s' \ \ @@ -589,9 +589,9 @@ subsection \CFG reduction (small-step semantics)\ type_synonym 'a cfg_config = "(node+unit) \ 'a state" -inductive red_cfg :: "'a absval_ty_fun \ proc_context \ var_context \ 'a fun_interp \ rtype_env \ mbodyCFG \ 'a cfg_config \ 'a cfg_config \ bool" +inductive red_cfg :: "'a absval_ty_fun \ mbodyCFG proc_context \ var_context \ 'a fun_interp \ rtype_env \ mbodyCFG \ 'a cfg_config \ 'a cfg_config \ bool" ("_,_,_,_,_,_ \ (_ -n\/ _)" [51,0,0,0] 81) - for A :: "'a absval_ty_fun" and M :: proc_context and \ :: var_context and \ :: "'a fun_interp" and \ :: rtype_env and G :: mbodyCFG + for A :: "'a absval_ty_fun" and M :: "mbodyCFG proc_context" and \ :: var_context and \ :: "'a fun_interp" and \ :: rtype_env and G :: mbodyCFG where RedNormalSucc: "\node_to_block(G) ! n = cs; A,M,\,\,\ \ \cs,Normal ns\ [\] Normal ns'; List.member (out_edges(G) ! n) n' \ \ A,M,\,\,\,G \ (Inl n, Normal ns) -n\ (Inl n', Normal ns')" @@ -611,13 +611,13 @@ inductive_cases RedNormalSucc_case: "A,M,\,\,G,\ \Reflexive and transitive closure of CFG reduction\ -abbreviation red_cfg_multi :: "'a absval_ty_fun \ proc_context \ var_context \ 'a fun_interp \ rtype_env \ mbodyCFG \ 'a cfg_config \ 'a cfg_config \ bool" +abbreviation red_cfg_multi :: "'a absval_ty_fun \ mbodyCFG proc_context \ var_context \ 'a fun_interp \ rtype_env \ mbodyCFG \ 'a cfg_config \ 'a cfg_config \ bool" ("_,_,_,_,_,_ \_ -n\*/ _" [51,0,0,0] 81) where "red_cfg_multi A M \ \ \ G \ rtranclp (red_cfg A M \ \ \ G)" text \N-step CFG reduction\ -abbreviation red_cfg_k_step :: "'a absval_ty_fun \ proc_context \ var_context \ 'a fun_interp \ rtype_env \ mbodyCFG \ 'a cfg_config \ nat \ 'a cfg_config \ bool" +abbreviation red_cfg_k_step :: "'a absval_ty_fun \ mbodyCFG proc_context \ var_context \ 'a fun_interp \ rtype_env \ mbodyCFG \ 'a cfg_config \ nat \ 'a cfg_config \ bool" ("_,_,_,_,_,_ \_ -n\^_/ _" [51,0,0,0,0] 81) where "red_cfg_k_step A M \ \ \ G c1 n c2 \ ((red_cfg A M \ \ \ G)^^n) c1 c2" @@ -682,7 +682,7 @@ definition valid_configuration s' \ Failure \ (is_final_config (m',s') \ (\ns'. s' = Normal ns' \ expr_all_sat A \ \ \ ns' posts))" -definition proc_body_satisfies_spec :: "'a absval_ty_fun \ proc_context \ var_context \ 'a fun_interp \ rtype_env \ expr list \ expr list \ mbodyCFG \ 'a nstate \ bool" +definition proc_body_satisfies_spec :: "'a absval_ty_fun \ mbodyCFG proc_context \ var_context \ 'a fun_interp \ rtype_env \ expr list \ expr list \ mbodyCFG \ 'a nstate \ bool" where "proc_body_satisfies_spec A M \ \ \ pres posts mbody ns \ expr_all_sat A \ \ \ ns pres \ (\ m' s'. (A, M, \, \, \, mbody \ (Inl (entry(mbody)), Normal ns) -n\* (m',s')) \ @@ -707,6 +707,42 @@ abbreviation axiom_assm where "axiom_assm A \ consts ns axioms \ (axioms_sat A (consts, []) \ (nstate_global_restriction ns consts) axioms)" +text \The following condition specifies what must hold for the list of constants with a unique modifier. + The condition states that all corresponding values in the state must be distinct. Note that constants + without unique modifiers may have values that clash with unique constants, which is consistent with the + verification condition generated by Boogie (status 21.10.2023). + Note that the verification condition only forces distinctness between values of unique constants of + the \<^emph>\same\ type. Here, we force distinctness between values of all unique constants. These two + definitions are equivalent, since values of different types are distinct in Boogie by default + (every value can have only one type as reflected by the function \<^const>\type_of_val\).\ + +definition unique_constants_distinct :: "'a named_state \ vname list \ bool" + where "unique_constants_distinct ns xs \ distinct (map (\x. the (ns x)) xs)" + +fun proc_is_correct :: "'a absval_ty_fun \ fdecls \ vdecls \ vname list \ vdecls \ axiom list \ 'struct_ty2 procedure \ + ('a absval_ty_fun \ 'struct_ty proc_context \ var_context \ 'a fun_interp \ rtype_env \ expr list \ expr list \ 'struct_ty2 \ 'a nstate \ bool) \ + bool" + where + "proc_is_correct A fun_decls constants unique_consts global_vars axioms proc proc_body_satisfies_spec_general = + (case proc_body(proc) of + Some (locals, struct) \ + ( ( (\t. closed t \ (\v. type_of_val A (v :: 'a val) = t)) \ (\v. closed ((type_of_val A) v)) ) \ + (\ \. fun_interp_wf A fun_decls \ \ + ( + (\\ gs ls. (list_all closed \ \ length \ = proc_ty_args proc) \ + (state_typ_wf A \ gs (constants @ global_vars) \ + state_typ_wf A \ ls ((proc_args proc)@ (locals @ proc_rets proc)) \ + unique_constants_distinct gs unique_consts \ + (axioms_sat A (constants, []) \ (global_to_nstate (state_restriction gs constants)) axioms) \ + (proc_body_satisfies_spec_general + A [] (constants@global_vars, (proc_args proc)@(locals@(proc_rets proc))) \ \ + (proc_all_pres proc) (proc_checked_posts proc) struct + \old_global_state = gs, global_state = gs, local_state = ls, binder_state = Map.empty\ ) ) + ) + ))) + | None \ True)" + +(* fun proc_is_correct :: "'a absval_ty_fun \ fdecls \ vdecls \ vdecls \ axiom list \ procedure \ bool" where "proc_is_correct A fun_decls constants global_vars axioms proc = @@ -725,18 +761,21 @@ fun proc_is_correct :: "'a absval_ty_fun \ fdecls \ vdec ) ))) | None \ True)" +*) -text \\<^term>\proc_is_correct A fun_decls constants global_vars axioms proc\ gives the definition +text \\<^term>\proc_is_correct A fun_decls constants unique_consts global_vars axioms proc proc_body_satisfies_spec_general\ gives the definition that a procedure \<^term>\proc\ is correct w.r.t. the type interpretation \<^term>\A\ the function declarations \fun_decls\, constants \<^term>\constants\, global variables \<^term>\global_vars\ and Boogie axioms \<^term>\axioms\. +\<^term>\unique_consts\ denotes the list of constants with a unique modifier. Since the current proof generation does not support procedure calls yet, we just instantiate the procedure context to the empty list here. -In our certificates, we prove (\<^term>\\A. proc_is_correct A fun_decls constants global_vars axioms proc\), -i.e., we prove procedure correctness for every type interpretation (\ is a universal quantifier at +In our certificates, we prove +\<^prop>\\A. proc_is_correct A fun_decls constants unique_consts global_vars axioms proc proc_body_satisfies_spec_general\. +That is, we prove procedure correctness for every type interpretation (\ is a universal quantifier at the meta level). Note that for certain type interpretations procedure correctness is trivial (see -the definition of \<^term>\proc_is_correct\). +the definition of \<^const>\proc_is_correct\). \ subsection \Properties of the semantics\ diff --git a/BoogieLang/Util.thy b/BoogieLang/Util.thy index 1b8bed6..6d89342 100644 --- a/BoogieLang/Util.thy +++ b/BoogieLang/Util.thy @@ -375,6 +375,14 @@ lemma lookup_var_global_no_locals: "lookup_var (G,[]) n_s x = global_state n_s x unfolding lookup_var_def by simp +lemma globals_locals_helper: + assumes "\ a. a \ A \ a \ a_max" + and "\ b. b \ B \ b_min \ (b :: vname)" + and "a_max < b_min" + shows "A \ B = {}" + using assms + by fastforce + lemma map_of_append: "map_of (xs1) x = Some y \ map_of (xs1@xs2) x = Some y" by simp @@ -385,13 +393,13 @@ lemma update_var_same_state: using assms update_var_def lookup_var_def proof (cases "map_of (snd \) x") case None - hence update_global:"?ns' = ns\global_state := global_state(ns)(x \ v)\" + hence update_global:"?ns' = ns\global_state := (global_state(ns))(x \ v)\" by (simp add: update_var_def) from assms have global_ns:"global_state ns x = Some v" by (metis None lookup_var_global prod.collapse) - have "global_state(ns)(x \ v) = global_state ns" + have "(global_state(ns))(x \ v) = global_state ns" apply (rule HOL.ext) by (simp add: global_ns) then show ?thesis @@ -399,13 +407,13 @@ proof (cases "map_of (snd \) x") by simp next case (Some a) - hence update_local:"?ns' = ns\local_state := local_state(ns)(x \ v)\" + hence update_local:"?ns' = ns\local_state := (local_state(ns))(x \ v)\" by (simp add: update_var_def) from assms have local_ns:"local_state ns x = Some v" by (metis Some lookup_var_local prod.collapse) - have "local_state(ns)(x \ v) = local_state ns" + have "(local_state(ns))(x \ v) = local_state ns" apply (rule HOL.ext) by (simp add: local_ns) then show ?thesis diff --git a/README.md b/README.md index eae6916..e978d17 100644 --- a/README.md +++ b/README.md @@ -4,7 +4,7 @@ Moreover, it contains helper theory files to support the [validation of the Boog verifier](https://github.com/gauravpartha/boogie_proofgen/), which is currently being developed. -The theory files are compatible with Isabelle 2021 (but not backwards +The theory files are compatible with Isabelle 2022 (and not backwards compatible with older versions). ## More details on the theory files @@ -15,7 +15,8 @@ The theory files for the Boogie language itself are given by: * `Lang.thy`: Syntax of the Boogie language * `BoogieDeBruijn.thy`: Some formalization on DeBruijn binders * `Semantics.thy`: Semantics of the Boogie language and definition of procedure -correctness +correctness (only describes control-flow graphs in terms of control flow) +* `Ast.thy`: Semantics of Boogie AST (uses `Semantics.thy` for control flow independent elements) * `Util.thy`: Some helper lemmas * `Typing.thy`: Boogie's type system * `TypeSafety.thy`: Type safety proof for expressions @@ -34,6 +35,8 @@ the passification source CFG is correct under the assumption of the VC. * `PassificationML.thy`: Some ML tactics used in the certification of the passification phase. * `BackedgeElim.thy`: Main theory that helps deal with the certification of the CFG-to-DAG phase. +* `CFGOptimizationsLoop.thy`: Main theory that helps deal with the certification of the CFG optimizations phase. +* `Ast_to_Cfg_Validation.thy`: Main theory that helps deal with the certification of the AST-to-CFG phase. * `TypingHelper.thy`: Helper lemmas/definitions for proving that expressions are well-typed. * `TypingML.thy`: ML tactic to prove that an expression is well-typed.