Theory Tuple4

theory Tuple4_LLVM imports Tuple4 IsaSAT_Literals_LLVM begin hide_const (open) NEMonad.ASSERT NEMonad.RETURN text ‹ This is the setup for accessing and modifying the state as an abstract tuple of 15 elements. The construction is kept generic (even if still targetting only our state). There is a lot of copy-paste that would be nice to automate at some point. We define 3 sort of operations: ▸ extracting an element, replacing it by an default element. Modifies the state. The name starts with text‹exctr› ▸ reinserting an element, freeing the current one. Modifies the state. The name starts with text‹update› ▸ in-place reading a value, possibly with pure parameters. Does not modify the state. The name starts with text‹read› › instantiation tuple4 :: (llvm_rep,llvm_rep,llvm_rep,llvm_rep) llvm_rep begin definition to_val_tuple4 where ‹to_val_tuple4 ≡ (λS. case S of Tuple4 M N D i ⇒ LL_STRUCT [to_val M, to_val N, to_val D, to_val i])› definition from_val_tuple4 :: ‹llvm_val ⇒ ('a, 'b, 'c, 'd) tuple4› where ‹from_val_tuple4 ≡ (λp. case llvm_val.the_fields p of [M, N, D, i] ⇒ Tuple4 (from_val M) (from_val N) (from_val D) (from_val i))› definition [simp]: "struct_of_tuple4 (_ :: ('a, 'b, 'c, 'd) tuple4 itself) ≡ VS_STRUCT [struct_of TYPE('a), struct_of TYPE('b), struct_of TYPE('c), struct_of TYPE('d)]" definition [simp]: "init_tuple4 :: ('a, 'b, 'c, 'd) tuple4 ≡ Tuple4 init init init init" instance apply standard unfolding from_val_tuple4_def to_val_tuple4_def struct_of_tuple4_def init_tuple4_def comp_def tuple4.case_distrib subgoal by (auto simp: init_zero fun_eq_iff from_val_tuple4_def split: tuple4.splits) subgoal for v by (cases v) (auto split: list.splits tuple4.splits) subgoal for v by (cases v) (simp add: LLVM_Shallow.null_def to_val_ptr_def split: tuple4.splits) subgoal by (simp add: LLVM_Shallow.null_def to_val_ptr_def to_val_word_def init_zero split: tuple4.splits) done end subsubsection ‹Setup for LLVM code export› text ‹Declare structure to code generator.› lemma to_val_tuple17[ll_struct_of]: "struct_of TYPE(('a, 'b, 'c, 'd) tuple4) = VS_STRUCT [ struct_of TYPE('a::llvm_rep), struct_of TYPE('b::llvm_rep), struct_of TYPE('c::llvm_rep), struct_of TYPE('d::llvm_rep)]" by (auto) lemma node_insert_value: "ll_insert_value (Tuple4 M N D i) M' 0 = Mreturn (Tuple4 M' N D i)" "ll_insert_value (Tuple4 M N D i) N' (Suc 0) = Mreturn (Tuple4 M N' D i)" "ll_insert_value (Tuple4 M N D i) D' 2 = Mreturn (Tuple4 M N D' i)" "ll_insert_value (Tuple4 M N D i) i' 3 = Mreturn (Tuple4 M N D i')" by (simp_all add: ll_insert_value_def llvm_insert_value_def Let_def checked_from_val_def to_val_tuple4_def from_val_tuple4_def) lemma node_extract_value: "ll_extract_value (Tuple4 M N D i) 0 = Mreturn M" "ll_extract_value (Tuple4 M N D i) (Suc 0) = Mreturn N" "ll_extract_value (Tuple4 M N D i) 2 = Mreturn D" "ll_extract_value (Tuple4 M N D i) 3 = Mreturn i" apply (simp_all add: ll_extract_value_def llvm_extract_value_def Let_def checked_from_val_def to_val_tuple4_def from_val_tuple4_def) done text ‹Lemmas to translate node construction and destruction› lemma inline_return_node[llvm_pre_simp]: "Mreturn (Tuple4 M N D i) = doM { r ← ll_insert_value init M 0; r ← ll_insert_value r N 1; r ← ll_insert_value r D 2; r ← ll_insert_value r i 3; Mreturn r }" apply (auto simp: node_insert_value) done lemma inline_node_case[llvm_pre_simp]: "(case r of (Tuple4 M N D i) ⇒ f M N D i) = doM { M ← ll_extract_value r 0; N ← ll_extract_value r 1; D ← ll_extract_value r 2; i ← ll_extract_value r 3; f M N D i }" apply (cases r) apply (auto simp: node_extract_value) done lemma inline_return_node_case[llvm_pre_simp]: "doM {Mreturn (case r of (Tuple4 M N D i) ⇒ f M N D i)} = doM { M ← ll_extract_value r 0; N ← ll_extract_value r 1; D ← ll_extract_value r 2; i ← ll_extract_value r 3; Mreturn (f M N D i) }" apply (cases r) apply (auto simp: node_extract_value) done lemma inline_direct_return_node_case[llvm_pre_simp]: "doM {(case r of (Tuple4 M N D i) ⇒ f M N D i)} = doM { M ← ll_extract_value r 0; N ← ll_extract_value r 1; D ← ll_extract_value r 2; i ← ll_extract_value r 3; (f M N D i) }" apply (cases r) apply (auto simp: node_extract_value) done lemmas [llvm_inline] = tuple4.Tuple4_a_def tuple4.Tuple4_b_def tuple4.Tuple4_c_def tuple4.Tuple4_d_def fun tuple4_assn :: ‹ ('a ⇒ _ ⇒ llvm_amemory ⇒ bool) ⇒ ('b ⇒ _ ⇒ llvm_amemory ⇒ bool) ⇒ ('c ⇒ _ ⇒ llvm_amemory ⇒ bool) ⇒ ('d ⇒ _ ⇒ llvm_amemory ⇒ bool) ⇒ ('a, 'b, 'c, 'd) tuple4 ⇒ _ ⇒ assn› where ‹tuple4_assn a_assn b_assn' c_assn d_assn S T = (case (S, T) of (Tuple4 M N D i, Tuple4 M' N' D' i') ⇒ (a_assn M (M') ∧* b_assn' N (N') ∧* c_assn D (D') ∧* d_assn i (i'))) › locale tuple4_state_ops = fixes a_assn :: ‹'a ⇒ 'xa ⇒ assn› and b_assn :: ‹'b ⇒ 'xb ⇒ assn› and c_assn :: ‹'c ⇒ 'xc ⇒ assn› and d_assn :: ‹'d ⇒ 'xd ⇒ assn› and a_default :: 'a and a :: ‹'xa llM› and b_default :: 'b and b :: ‹'xb llM› and c_default :: 'c and c :: ‹'xc llM› and d_default :: 'd and d :: ‹'xd llM› begin definition tuple4_int_assn :: ‹_ ⇒ _ ⇒ assn› where ‹tuple4_int_assn = tuple4_assn a_assn b_assn c_assn d_assn› definition remove_a :: ‹('a, 'b, 'c, 'd) tuple4 ⇒ 'a × ('a, 'b, 'c, 'd) tuple4› where ‹remove_a tuple4 = (case tuple4 of Tuple4 x1 x2 x3 x4 ⇒ (x1, Tuple4 a_default x2 x3 x4))› definition remove_b :: ‹('a, 'b, 'c, 'd) tuple4 ⇒ 'b × ('a, 'b, 'c, 'd) tuple4› where ‹remove_b tuple4 = (case tuple4 of Tuple4 x1 x2 x3 x4 ⇒ (x2, Tuple4 x1 b_default x3 x4))› definition remove_c :: ‹('a, 'b, 'c, 'd) tuple4 ⇒ _ × ('a, 'b, 'c, 'd) tuple4› where ‹remove_c tuple4 = (case tuple4 of Tuple4 x1 x2 x3 x4 ⇒ (x3, Tuple4 x1 x2 c_default x4))› definition remove_d :: ‹('a, 'b, 'c, 'd) tuple4 ⇒ _ × ('a, 'b, 'c, 'd) tuple4› where ‹remove_d tuple4 = (case tuple4 of Tuple4 x1 x2 x3 x4 ⇒ (x4, Tuple4 x1 x2 x3 d_default))› definition update_a :: ‹'a ⇒ ('a, 'b, 'c, 'd) tuple4 ⇒ ('a, 'b, 'c, 'd) tuple4› where ‹update_a x1 tuple4 = (case tuple4 of Tuple4 M x2 x3 x4 ⇒ let _ = M in Tuple4 x1 x2 x3 x4)› definition update_b :: ‹'b ⇒ ('a, 'b, 'c, 'd) tuple4 ⇒ ('a, 'b, 'c, 'd) tuple4› where ‹update_b x2 tuple4 = (case tuple4 of Tuple4 x1 M x3 x4 ⇒ let _ = M in Tuple4 x1 x2 x3 x4)› definition update_c :: ‹'c ⇒ ('a, 'b, 'c, 'd) tuple4 ⇒ ('a, 'b, 'c, 'd) tuple4› where ‹update_c x3 tuple4 = (case tuple4 of Tuple4 x1 x2 M x4 ⇒ let _ = M in Tuple4 x1 x2 x3 x4)› definition update_d :: ‹'d ⇒ ('a, 'b, 'c, 'd) tuple4 ⇒ ('a, 'b, 'c, 'd) tuple4› where ‹update_d x4 tuple4 = (case tuple4 of Tuple4 x1 x2 x3 M ⇒ let _ = M in Tuple4 x1 x2 x3 x4)› end lemma tuple4_assn_conv[simp]: "tuple4_assn P1 P2 P3 P4 (Tuple4 a1 a2 a3 a4) (Tuple4 a1' a2' a3' a4') = (P1 a1 a1' ∧* P2 a2 a2' ∧* P3 a3 a3' ∧* P4 a4 a4')" unfolding tuple4_assn.simps by auto lemma tuple4_assn_ctxt: ‹tuple4_assn P1 P2 P3 P4 (Tuple4 a1 a2 a3 a4) (Tuple4 a1' a2' a3' a4') = z ⟹ hn_ctxt (tuple4_assn P1 P2 P3 P4) (Tuple4 a1 a2 a3 a4) (Tuple4 a1' a2' a3' a4')= z› by (simp add: hn_ctxt_def) lemma hn_case_tuple4'[sepref_comb_rules]: assumes FR: ‹Γ ⊢ hn_ctxt (tuple4_assn P1 P2 P3 P4) p' p ** Γ1› assumes Pair: "⋀a1 a2 a3 a4 a1' a2' a3' a4'. ⟦p'=Tuple4 a1' a2' a3' a4'⟧ ⟹ hn_refine (hn_ctxt P1 a1' a1 ∧* hn_ctxt P2 a2' a2 ∧* hn_ctxt P3 a3' a3 ∧* hn_ctxt P4 a4' a4 ∧* Γ1) (f a1 a2 a3 a4 ) (Γ2 a1 a2 a3 a4 a1' a2' a3' a4') R (CP a1 a2 a3 a4 ) (f' a1' a2' a3' a4')" assumes FR2: ‹⋀a1 a2 a3 a4 a1' a2' a3' a4'. Γ2 a1 a2 a3 a4 a1' a2' a3' a4' ⊢ hn_ctxt P1' a1' a1 ** hn_ctxt P2' a2' a2 ** hn_ctxt P3' a3' a3 ** hn_ctxt P4' a4' a4 ** Γ1'› shows ‹hn_refine Γ (case_tuple4 f p) (hn_ctxt (tuple4_assn P1' P2' P3' P4') p' p ** Γ1') R (case_tuple4 CP p) (case_tuple4$(λ₂a1 a2 a3 a4 . f' a1 a2 a3 a4 )$p')› (is ‹?G Γ›) unfolding autoref_tag_defs PROTECT2_def apply1 (rule hn_refine_cons_pre[OF FR]) apply1 (cases p; cases p'; simp add: tuple4_assn_conv[THEN tuple4_assn_ctxt]) unfolding CP_SPLIT_def prod.simps apply (rule hn_refine_cons[OF _ Pair _ entails_refl]) applyS (simp add: hn_ctxt_def) applyS simp using FR2 by (simp add: hn_ctxt_def) lemma case_tuple4_arity[sepref_monadify_arity]: ‹case_tuple4 ≡ λ₂fp p. SP case_tuple4$(λ₂a b. fp$a$b)$p› by (simp_all only: SP_def APP_def PROTECT2_def RCALL_def) lemma case_tuple4_comb[sepref_monadify_comb]: ‹⋀fp p. case_tuple4$fp$p ≡ Refine_Basic.bind$(EVAL$p)$(λ₂p. (SP case_tuple4$fp$p))› by (simp_all) lemma case_tuple4_plain_comb[sepref_monadify_comb]: "EVAL$(case_tuple4$(λ₂a1 a2 a3 a4 . fp a1 a2 a3 a4 )$p) ≡ Refine_Basic.bind$(EVAL$p)$(λ₂p. case_tuple4$(λ₂a1 a2 a3 a4 . EVAL$(fp a1 a2 a3 a4 ))$p)" apply (rule eq_reflection, simp split: list.split prod.split option.split tuple4.split)+ done lemma ho_tuple4_move[sepref_preproc]: ‹case_tuple4 (λa1 a2 a3 a4 x. f x a1 a2 a3 a4 ) = (λp x. case_tuple4 (f x) p)› by (auto split: tuple4.splits) locale tuple4_state = tuple4_state_ops a_assn b_assn c_assn d_assn a_default a b_default b c_default c d_default d for a_assn :: ‹'a ⇒ 'xa ⇒ assn› and b_assn :: ‹'b ⇒ 'xb ⇒ assn› and c_assn :: ‹'c ⇒ 'xc ⇒ assn› and d_assn :: ‹'d ⇒ 'xd ⇒ assn› and a_default :: 'a and a :: ‹'xa llM› and b_default :: 'b and b :: ‹'xb llM› and c_default :: 'c and c :: ‹'xc llM› and d_default :: 'd and d :: ‹'xd llM› and a_free :: ‹'xa ⇒ unit llM› and b_free :: ‹'xb ⇒ unit llM› and c_free :: ‹'xc ⇒ unit llM› and d_free :: ‹'xd ⇒ unit llM› + assumes a: ‹(uncurry0 a, uncurry0 (RETURN a_default)) ∈ unit_assn^k →_a a_assn› and b: ‹(uncurry0 b, uncurry0 (RETURN b_default)) ∈ unit_assn^k →_a b_assn› and c: ‹(uncurry0 c, uncurry0 (RETURN c_default)) ∈ unit_assn^k →_a c_assn› and d: ‹(uncurry0 d, uncurry0 (RETURN d_default)) ∈ unit_assn^k →_a d_assn› and a_free: ‹MK_FREE a_assn a_free› and b_free: ‹MK_FREE b_assn b_free›and c_free: ‹MK_FREE c_assn c_free›and d_free: ‹MK_FREE d_assn d_free› notes [[sepref_register_adhoc a_default b_default c_default d_default]] begin lemmas [sepref_comb_rules] = hn_case_tuple4'[of _ a_assn b_assn c_assn d_assn, unfolded tuple4_int_assn_def[symmetric]] lemma ex_tuple4_iff: "(∃b :: (_,_,_,_)tuple4. P b) ⟷ (∃a b c d. P (Tuple4 a b c d))" apply auto apply (case_tac b) by force lemmas [sepref_frame_free_rules] = a_free b_free c_free d_free sepref_register ‹Tuple4› lemma [sepref_fr_rules]: ‹(uncurry3 (Mreturn oooo Tuple4), uncurry3 (RETURN oooo Tuple4)) ∈ a_assn^d *_a b_assn^d *_a c_assn^d *_a d_assn^d →_a tuple4_int_assn› unfolding tuple4_int_assn_def apply sepref_to_hoare apply vcg unfolding ex_tuple4_iff apply vcg' done lemma [sepref_frame_match_rules]: ‹ hn_ctxt (tuple4_assn (invalid_assn a_assn) (invalid_assn b_assn) (invalid_assn c_assn) (invalid_assn d_assn)) ax bx ⊢ hn_val UNIV ax bx› unfolding hn_ctxt_def invalid_assn_def tuple4_int_assn_def entails_def apply (auto split: prod.split tuple4.splits elim: is_pureE simp: sep_algebra_simps pure_part_pure_conj_eq) apply (auto simp: pure_part_def) apply (auto simp: pure_def pure_true_conv) done lemma RETURN_case_tuple4_inverse: ‹RETURN (let _ = M in ff) = (do {_ ← mop_free M; RETURN (ff)})› by (auto intro!: ext simp: mop_free_def split: tuple4.splits) sepref_definition update_a_code is ‹uncurry (RETURN oo update_a)› :: ‹a_assn^d *_a tuple4_int_assn^d →_a tuple4_int_assn› supply [[goals_limit=5]] unfolding update_a_def tuple4.case_distrib comp_def RETURN_case_tuple4_inverse by sepref sepref_definition update_b_code is ‹uncurry (RETURN oo update_b)› :: ‹b_assn^d *_a tuple4_int_assn^d →_a tuple4_int_assn› supply [[goals_limit=1]] unfolding update_b_def tuple4.case_distrib comp_def RETURN_case_tuple4_inverse by sepref sepref_definition update_c_code is ‹uncurry (RETURN oo update_c)› :: ‹c_assn^d *_a tuple4_int_assn^d →_a tuple4_int_assn› supply [[goals_limit=1]] unfolding update_c_def tuple4.case_distrib comp_def RETURN_case_tuple4_inverse by sepref sepref_definition update_d_code is ‹uncurry (RETURN oo update_d)› :: ‹d_assn^d *_a tuple4_int_assn^d →_a tuple4_int_assn› supply [[goals_limit=1]] unfolding update_d_def tuple4.case_distrib comp_def RETURN_case_tuple4_inverse by sepref lemma RETURN_case_tuple4_invers: ‹(RETURN ∘∘ case_tuple4) (λx1 x2 x3 x4. ff x1 x2 x3 x4) = case_tuple4 (λx1 x2 x3 x4. RETURN (ff x1 x2 x3 x4))› by (auto intro!: ext split: tuple4.splits) lemmas [sepref_fr_rules] = a b c d sepref_definition remove_a_code is ‹RETURN o remove_a› :: ‹ tuple4_int_assn^d →_a a_assn ×_a tuple4_int_assn› unfolding remove_a_def RETURN_case_tuple4_invers by sepref sepref_definition remove_b_code is ‹RETURN o remove_b› :: ‹ tuple4_int_assn^d →_a b_assn ×_a tuple4_int_assn› unfolding remove_b_def RETURN_case_tuple4_invers by sepref sepref_definition remove_c_code is ‹RETURN o remove_c› :: ‹ tuple4_int_assn^d →_a c_assn ×_a tuple4_int_assn› unfolding remove_c_def RETURN_case_tuple4_invers by sepref sepref_definition remove_d_code is ‹RETURN o remove_d› :: ‹ tuple4_int_assn^d →_a d_assn ×_a tuple4_int_assn› unfolding remove_d_def RETURN_case_tuple4_invers by sepref lemmas separation_rules = remove_a_code.refine remove_b_code.refine remove_c_code.refine remove_d_code.refine lemmas code_rules = remove_a_code_def remove_b_code_def remove_c_code_def remove_d_code_def lemmas setter_and_getters_def = update_a_def remove_a_def update_b_def remove_b_def update_c_def remove_c_def update_d_def remove_d_def end context tuple4_state begin lemma reconstruct_isasat[sepref_frame_match_rules]: ‹hn_ctxt (tuple4_assn (a_assn) (b_assn) (c_assn) (d_assn)) ax bx ⊢ hn_ctxt tuple4_int_assn ax bx› unfolding tuple4_int_assn_def apply (auto split: prod.split tuple4.splits elim: is_pureE simp: sep_algebra_simps pure_part_pure_conj_eq) done context fixes x_assn :: ‹'r ⇒ 'q ⇒ assn› and read_all_code :: ‹'xa ⇒ 'xb ⇒ 'xc ⇒ 'xd ⇒ 'q llM› and read_all :: ‹'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'r nres› begin definition read_all_st_code :: ‹_› where ‹read_all_st_code xi = (case xi of Tuple4 a1 a2 a3 a4 ⇒ read_all_code a1 a2 a3 a4 )› definition read_all_st :: ‹('a, 'b, 'c, 'd) tuple4 ⇒ _› where ‹read_all_st tuple4 = (case tuple4 of Tuple4 a1 a2 a3 a4 ⇒ read_all a1 a2 a3 a4)› context fixes P assumes trail_read[sepref_fr_rules]: ‹(uncurry3 read_all_code, uncurry3 read_all) ∈ [uncurry3 P]_a a_assn^k *_a b_assn^k *_a c_assn^k *_a d_assn^k → x_assn› notes [[sepref_register_adhoc read_all]] begin sepref_definition read_all_st_code_tmp is read_all_st :: ‹[case_tuple4 P]_a tuple4_int_assn^k → x_assn› unfolding read_all_st_def by sepref lemmas read_all_st_code_refine = read_all_st_code_tmp.refine[unfolded read_all_st_code_tmp_def read_all_st_code_def[symmetric]] end end end lemma Mreturn_comp_Tuple4: ‹(Mreturn oooo Tuple4) a b c d = Mreturn (Tuple4 a b c d)› by auto lemma tuple4_free[sepref_frame_free_rules]: assumes ‹MK_FREE A freea› ‹MK_FREE B freeb› ‹MK_FREE C freec› ‹MK_FREE D freed› shows ‹ MK_FREE (tuple4_assn A B C D) (λS. case S of Tuple4 a b c d ⇒ do_M { freea a; freeb b; freec c; freed d })› supply [vcg_rules] = assms[THEN MK_FREED] apply (rule)+ apply (clarsimp split: tuple4.splits) by vcg' end

Theory Tuple4_LLVM