Theory LLVM_Shallow_RS
section ‹LLVM Shallow Embedding --- Reasoning Setup›
theory LLVM_Shallow_RS
imports
"../basic/LLVM_Basic_Main"
LLVM_Memory_RS
begin
subsection ‹Monadification Setup for VCG›
ML ‹
structure LLVM_VCG_Monadify = struct
structure Monadify = Gen_Monadify_Cong (
fun mk_return x = @{mk_term "return ?x ::_ llM"}
fun mk_bind m f = @{mk_term "bind ?m ?f ::_ llM"}
fun dest_return @{mpat "return ?x ::_ llM"} = SOME x | dest_return _ = NONE
fun dest_bind @{mpat "bind ?m ?f ::_ llM"} = SOME (m,f) | dest_bind _ = NONE
fun dest_monadT (Type (@{type_name M},[T,@{typ unit},@{typ cost},@{typ llvm_memory},@{typ err}])) = SOME T | dest_monadT _ = NONE
val bind_return_thm = @{lemma "bind m return = m" by simp}
val return_bind_thm = @{lemma "bind (return x) f = f x" by simp}
val bind_bind_thm = @{lemma "bind (bind m (λx. f x)) g = bind m (λx. bind (f x) g)" by simp}
)
val _ = Theory.setup
(Attrib.setup \<^binding>‹vcg_const›
(Args.term >> (fn t => Thm.declaration_attribute (K (Monadify.prepare_add_const_decl t))))
"declaration of new vcg-constant")
fun monadify_all_tac ctxt = CONVERSION (Conv.top_sweep_conv (Monadify.monadify_conv) ctxt)
end
›
named_theorems vcg_monadify_xforms
method_setup vcg_monadify_raw = ‹Scan.succeed (SIMPLE_METHOD' o LLVM_VCG_Monadify.monadify_all_tac)›
method vcg_monadify_xform_raw = (simp only: vcg_monadify_xforms)?
method vcg_monadify uses simp =
vcg_monadify_xform_raw; ((changed ‹vcg_monadify_raw; vcg_monadify_xform_raw›)+)?
declare llvm_inline_bind_laws[vcg_monadify_xforms]
subsection ‹Abbreviations for VCG›
type_synonym ll_astate = "llvm_amemory × ecost"
type_synonym ll_assn = "(ll_astate ⇒ bool)"
definition "ll_α ≡ lift_α_cost llvm_α"
abbreviation llvm_htriple
:: "ll_assn ⇒ 'a llM ⇒ ('a ⇒ ll_assn) ⇒ bool"
where "llvm_htriple ≡ htriple_gc GC ll_α"
abbreviation "llSTATE ≡ STATE ll_α"
abbreviation "llPOST ≡ POSTCOND ll_α"
abbreviation (input) ll_cost_assn ("$$") where "ll_cost_assn ≡ λname n. $lift_acost (cost name n)"
locale llvm_prim_setup begin
end
subsection ‹General VCG Setup›
lemma fri_extract_prod_case[fri_extract_simps]: "(case p of (a,b) ⇒ (P a b :: ll_assn)) = (EXS a b. ↑(p=(a,b)) ** P a b)"
apply (cases p) apply (rule ext)
apply (auto simp: sep_algebra_simps pred_lift_extract_simps)
done
lemma norm_prod_case[vcg_normalize_simps]:
"wp (case p of (a,b) ⇒ f a b) Q s ⟷ (∀a b. p=(a,b) ⟶ wp (f a b) Q s)"
by (auto split: prod.split)
lemmas ll_notime_htriple_eq = notime_htriple_eq[of llvm_α _ "_::_ llM", folded ll_α_def]
lemma ll_consume_rule[vcg_rules]: "llvm_htriple ($lift_acost c) (consume c) (λ_. □)"
unfolding ll_α_def using consume_rule
by (simp)
subsection ‹Assertions›
typedef ('a,'c) dr_assn = "UNIV :: ('a ⇒ 'c ⇒ ll_assn) set" by simp
setup_lifting type_definition_dr_assn
lemma dr_assn_inverses[simp]:
"Abs_dr_assn (Rep_dr_assn A) = A"
"Rep_dr_assn (Abs_dr_assn B) = B"
using Rep_dr_assn_inverse Abs_dr_assn_inverse by auto
definition dr_assn_prefix :: "('a, 'b) dr_assn ⇒ 'a ⇒ 'b ⇒ ll_assn" ("↿_" [1000] 1000) where
"↿A a c ≡ Rep_dr_assn A a c"
definition "is_pure A ≡ ∀a c. sep_is_pure_assn (↿A a c)"
definition dr_assn_pure_prefix ("↿⇩p_" [1000] 1000) where
"↿⇩pA a c ≡ ↑pure_part (↿A a c)"
definition dr_assn_pure_asm_prefix ("♭⇩p_" [1000] 1000) where
"♭⇩pA a c ≡ pure_part (↿A a c) ∧ is_pure A"
lemma pure_fri_rule[fri_rules]: "PRECOND (SOLVE_ASM (♭⇩pA a c)) ⟹ □ ⊢ ↿⇩pA a c"
unfolding vcg_tag_defs entails_def dr_assn_pure_prefix_def dr_assn_pure_asm_prefix_def
is_pure_def
apply clarsimp
apply (subst pure_part_pure_eq[symmetric])
apply (auto simp: sep_algebra_simps)
done
lemma prepare_pure_assn[named_ss fri_prepare_simps]: "↿A a c = ↿⇩pA a c" if "is_pure A"
using that
by (simp add: dr_assn_pure_prefix_def is_pure_def)
lemma extract_pure_assn[fri_extract_simps]: "↿A a c = ↑♭⇩pA a c" if "is_pure A"
using that
unfolding vcg_tag_defs entails_def dr_assn_pure_asm_prefix_def is_pure_def
apply (auto simp: sep_algebra_simps)
done
attribute_setup is_pure_rule = ‹Attrib.add_del
(VCG_Lib.chained_decl_attr @{context} @{attributes [named_ss fri_prepare_simps, fri_extract_simps]})
(VCG_Lib.chained_decl_attr @{context} @{attributes [named_ss fri_prepare_simps del, fri_extract_simps del]})
›
‹Rules to introduce pure assertions›
text ‹This rule is to be overloaded by later rules›
lemma pure_part_pureD[vcg_prep_ext_rules]: "pure_part (↑Φ) ⟹ Φ" by simp
lemma prep_ext_state[vcg_prep_ext_rules]:
"llSTATE P s ⟹ pure_part P"
unfolding STATE_def by (blast intro: pure_partI)
lemma prep_ext_pure_part_pure[vcg_prep_ext_rules]:
"pure_part (↿⇩pA a c) ⟹ pure_part (↿A a c)"
unfolding dr_assn_pure_prefix_def by simp
lemma thin_dr_pure_asm[vcg_prep_ext_rules]: "(♭⇩pA a c) ⟹ pure_part (↿A a c)"
unfolding dr_assn_pure_asm_prefix_def by simp
definition "mk_assn ≡ Abs_dr_assn"
definition "mk_pure_assn A ≡ mk_assn (λa c. ↑A a c)"
lemma is_pure_mk_pure[simp]: "is_pure (mk_pure_assn A)"
unfolding is_pure_def mk_pure_assn_def mk_assn_def dr_assn_prefix_def
by (auto)
lemma sel_mk_assn[simp]: "↿(mk_assn A) a c = A a c"
by (auto simp: mk_assn_def dr_assn_prefix_def)
lemma sel_mk_pure_assn[simp]:
"↿(mk_pure_assn A) a c = ↑(A a c)"
"↿⇩p(mk_pure_assn A) a c = ↑(A a c)"
"♭⇩p(mk_pure_assn A) a c = A a c"
apply (auto simp: mk_pure_assn_def dr_assn_pure_prefix_def dr_assn_pure_asm_prefix_def)
apply (auto simp: mk_assn_def is_pure_def dr_assn_prefix_def sep_algebra_simps)
done
lemma mk_pure_assn_extractI:
assumes "pure_part (↿(mk_pure_assn A) a c)"
assumes "A a c ⟹ Φ a c"
shows "Φ a c"
using assms
by auto
lemma mk_assn_extractI:
assumes "pure_part (↿(mk_assn A) a c)"
assumes "A a c ⊢ ↑Φ a c ** sep_true"
shows "Φ a c"
using assms
apply (cases "Φ a c"; simp)
using entails_eqI by fastforce
lemma mk_assn_extractI':
assumes "pure_part (↿(mk_assn A) a c)"
assumes "FRAME (A a c) (↑Φ a c) F"
shows "Φ a c"
apply (rule mk_assn_extractI[OF assms(1)])
using assms(2) unfolding FRAME_def
by (metis (no_types, lifting) entails_def entails_mp sep_conj_commute)
lemma pure_part_mk_assnD[vcg_prep_ext_rules]:
"pure_part (↿(mk_assn f) a c) ⟹ pure_part (f a c)"
by auto
lemma fri_abs_cong_rl: "PRECOND (SOLVE_AUTO (a=a')) ⟹ ↿A a c ⊢ ↿A a' c"
unfolding vcg_tag_defs by auto
subsection ‹Memory Reasoning›
locale llvm_prim_mem_setup begin
sublocale llvm_prim_setup .
end
subsubsection ‹Pointers›
text ‹Assertion for pointer to single value›
definition ll_pto :: "('a::llvm_rep, 'a ptr) dr_assn"
where "ll_pto ≡ mk_assn (λv p. FST (llvm_pto (to_val v) (the_raw_ptr p)))"
instantiation ptr :: (llvm_rep) addr_algebra begin
definition "abase ≡ abase o the_raw_ptr"
definition "acompat a b ≡ acompat (the_raw_ptr a) (the_raw_ptr b)"
definition "adiff a b ≡ adiff (the_raw_ptr a) (the_raw_ptr b)"
definition aidx_ptr :: "'a ptr ⇒ int ⇒ 'a ptr" where "aidx a i ≡ PTR (aidx (the_raw_ptr a) i)"
instance
apply standard
apply (intro part_equivpI sympI transpI)
unfolding abase_ptr_def acompat_ptr_def adiff_ptr_def aidx_ptr_def
apply (metis acompat_equiv part_equivp_def ptr.sel)
apply (auto intro: acompat_sym acompat_trans simp: acompat_dom)
done
end
text ‹Assertion to range of array›
definition "ll_range I ≡ mk_assn (λf p. ↑(abase p) ** (⋃*i∈I. ↿ll_pto (f i) (p +⇩a i)))"
lemma ll_range_preep_pure[vcg_prep_ext_rules]:
"pure_part (↿(ll_range I) f p) ⟹ abase p"
unfolding ll_range_def
apply (erule mk_assn_extractI')
by vcg_try_solve
lemma ll_range_not_base: "¬abase p ⟹ ↿(ll_range I) f p = sep_false"
unfolding ll_range_def by auto
lemma null_not_base[simp]: "¬abase null"
apply (auto simp: abase_ptr_def null_def)
apply (auto simp: abase_llvm_ptr_def llvm_null_def)
done
lemma ll_range_not_null[simp]: "↿(ll_range I) f null = sep_false"
by (simp add: ll_range_not_base)
lemma ll_pto_not_same: "(↿ll_pto x p ** ↿ll_pto y p) = sep_false"
apply (rule ext)
apply (auto simp: ll_pto_def llvm_pto_def ab.ba.pto_def split: rptr.splits addr.splits)
apply (auto simp: sep_algebra_simps sep_conj_def)
apply (auto simp: sep_disj_llvm_amemory_def sep_algebra_simps ab.pto_def split: baddr.splits)
apply (auto simp: vpto_assn_def)
done
lemma ll_range_merge: "I⇩1∩I⇩2={} ⟹ (↿(ll_range I⇩1) f p ** ↿(ll_range I⇩2) f p) = ↿(ll_range (I⇩1∪I⇩2)) f p"
unfolding ll_range_def
by (auto simp: sep_algebra_simps)
lemma ll_range_bogus_upd[simp]: "x∉I ⟹ ↿(ll_range I) (f(x:=v)) p = ↿(ll_range I) f p"
unfolding ll_range_def
apply (cases "abase p"; simp add: sep_algebra_simps)
by (rule sep_set_img_cong) (auto)
lemma open_ll_range: "i∈I ⟹ ↿(ll_range I) f p = (↑abase p ** ↿ll_pto (f i) (p +⇩a i) ** ↿(ll_range (I-{i})) f p)"
unfolding ll_range_def
apply (cases "abase p"; simp add: sep_algebra_simps)
by (auto simp: sep_set_img_remove)
lemma
assumes "I∩I'≠{}"
assumes "F ⊢ ↿(ll_range (I'-I)) f p ** F'"
shows "↿(ll_range I) f p ** F ⊢ ↿(ll_range I') f p ** ↿(ll_range (I-I')) f p ** F'"
proof -
have "↿(ll_range I) f p ** F ⊢ ↿(ll_range I) f p ** ↿(ll_range (I'-I)) f p ** F'"
using assms(2) conj_entails_mono by blast
also have "… = (↿(ll_range (I ∪ (I'-I))) f p ** F')"
apply (subst ll_range_merge[symmetric])
by auto
also have "… = ((↿(ll_range I') f p ** ↿(ll_range (I-I')) f p) ** F')"
apply (rewrite in "_=⌑" ll_range_merge)
apply (auto simp: Un_commute)
done
finally show ?thesis by simp
qed
thm vcg_normalize_simps
lemma FST_pure[sep_algebra_simps, vcg_normalize_simps]: "FST (↑φ) = ↑φ"
unfolding FST_def by (simp add: fun_eq_iff pred_lift_extract_simps sep_algebra_simps)
lemma FST_extract_pure[sep_algebra_simps, vcg_normalize_simps]: "FST (↑φ ** Q) = (↑φ ** FST Q)"
unfolding FST_def by (simp add: fun_eq_iff pred_lift_extract_simps sep_algebra_simps)
text ‹Frame inference setup to consume excess credits when solving entailments›
lemma GC_move_left[named_ss fri_prepare_simps]:
"NO_MATCH GC P ⟹ (P ** GC) = (GC ** P)"
"NO_MATCH GC Q ⟹ (Q ** GC ** P) = (GC ** Q ** P)"
"(GC ** GC) = GC"
"(GC ** GC ** P) = (GC ** P)"
"FRAME_INFER P (GC ** Q) □ = FRAME_INFER P Q GC"
by (simp_all add: sep_algebra_simps sep_conj_c FRAME_INFER_def)
lemmas [fri_end_rules] = empty_ent_GC entails_GC
lemma consume_credits_fri_end_rule[fri_end_rules]: "P⊢GC ⟹ $c**P ⊢ GC"
using conj_entails_mono entails_GC by fastforce
print_named_simpset fri_prepare_simps
subsubsection ‹Load and Store›
context llvm_prim_mem_setup begin
lemma checked_from_val_rule[vcg_rules]: "llvm_htriple □ (checked_from_val (to_val x)) (λr. ↑(r=x))"
unfolding checked_from_val_def
supply [fri_rules] = empty_ent_GC
by vcg
lemmas [vcg_rules] = ll_notime_htriple_eq[THEN iffD1, OF llvm_load_rule]
lemmas [vcg_rules] = ll_notime_htriple_eq[THEN iffD1, OF llvm_store_rule]
text ‹Standard rules for load and store from pointer›
lemma ll_load_rule[vcg_rules]: "llvm_htriple ($$ ''load'' 1 ** ↿ll_pto x p) (ll_load p) (λr. ↑(r=x) ** ↿ll_pto x p)"
unfolding ll_load_def ll_pto_def
by vcg
lemma ll_store_rule[vcg_rules]: "llvm_htriple ($$ ''store'' 1 ** ↿ll_pto xx p) (ll_store x p) (λ_. ↿ll_pto x p)"
unfolding ll_store_def ll_pto_def
by vcg
text ‹Rules for load and store from indexed pointer, wrt. range›
lemmas [fri_extract_simps] = sep_conj_assoc
find_theorems htriple EXTRACT
thm vcg_decomp_rules
lemma ll_load_rule_range[vcg_rules]:
shows "llvm_htriple ($$ ''load'' 1 ** ↿(ll_range I) a p ** ↑⇩!( p' ~⇩a p ∧ p' -⇩a p ∈ I )) (ll_load p') (λr. ↑(r = a (p' -⇩a p)) ** ↿(ll_range I) a p)"
unfolding vcg_tag_defs
apply (rule htriple_vcgI')
apply fri_extract_basic
apply (simp add: open_ll_range)
apply fri_extract
apply vcg
done
lemma ll_store_rule_range[vcg_rules]:
shows "llvm_htriple ($$ ''store'' 1 ** ↿(ll_range I) a p ** ↑⇩!( p' ~⇩a p ∧ p' -⇩a p ∈ I )) (ll_store x p') (λ_. ↿(ll_range I) (a(p' -⇩a p := x)) p)"
unfolding vcg_tag_defs
apply (rule htriple_vcgI')
apply fri_extract_basic
apply (simp add: open_ll_range)
apply fri_extract
by vcg
subsubsection ‹Offsetting Pointers›
lemmas [vcg_rules] = ll_notime_htriple_eq[THEN iffD1, OF llvm_checked_idx_ptr_rule]
text ‹Rule for indexing pointer. Note, the new target address must exist›
lemma ll_ofs_ptr_rule[vcg_rules]:
"llvm_htriple
($$ ''ofs_ptr'' 1 ** ↿ll_pto v (p +⇩a (sint i)) ** ↑⇩!(abase p))
(ll_ofs_ptr p i)
(λr. ↑(r= p +⇩a (sint i)) ** ↿ll_pto v (p +⇩a (sint i)))"
unfolding ll_ofs_ptr_def ll_pto_def abase_ptr_def aidx_ptr_def
by vcg
text ‹Rule for indexing pointer into range. Note, the new target address must exist›
lemma ll_ofs_ptr_rule'[vcg_rules]:
shows "llvm_htriple
($$ ''ofs_ptr'' 1 ** ↿(ll_range I) x p ** ↑⇩!(p ~⇩a p' ∧ (p' +⇩a sint i) -⇩a p ∈ I))
(ll_ofs_ptr p' i)
(λr. ↑(r= p' +⇩a sint i) ** ↿(ll_range I) x p)"
unfolding vcg_tag_defs
supply [named_ss fri_prepare_simps] = open_ll_range
by vcg
subsubsection ‹Allocate and Free›
lemma FST_empty[sep_algebra_simps, vcg_normalize_simps]: "FST □ = □"
unfolding FST_def by (auto simp: sep_algebra_simps)
lemmas [vcg_rules] = ll_notime_htriple_eq[THEN iffD1, OF llvm_allocn_rule, unfolded FST_empty]
lemma FST_distrib_img[sep_algebra_simps, vcg_normalize_simps, named_ss fri_prepare_simps]:
"FST (⋃*i∈I. P i) = (⋃*i∈I. FST (P i))"
proof (cases "finite I")
case True
then show ?thesis by(induct rule: finite_induct) (simp_all add: FST_empty FST_conj_conv[symmetric])
next
case False
then show ?thesis by (auto simp add: FST_def)
qed
text ‹Memory allocation tag, which expresses ownership of an allocated block.›
definition ll_malloc_tag :: "int ⇒ 'a::llvm_rep ptr ⇒ _"
where "ll_malloc_tag n p ≡ $$ ''free'' 1 ** ↑(n≥0) ** FST (llvm_malloc_tag n (the_raw_ptr p))"
text ‹Allocation returns an array-base pointer to an initialized range,
as well as an allocation tag›
lemma ll_malloc_rule[vcg_rules]:
"llvm_htriple
($$ ''malloc'' (unat n) ** $$ ''free'' 1 ** ↑(n≠0))
(ll_malloc TYPE('a::llvm_rep) n)
(λr. ↿(ll_range {0..< uint n}) (λ_. init) r ** ll_malloc_tag (uint n) r)"
unfolding ll_malloc_def ll_pto_def ll_malloc_tag_def ll_range_def
supply [simp] = list_conj_eq_sep_set_img abase_ptr_def aidx_ptr_def unat_gt_0
supply [vcg_normalize_simps] = FST_conj_conv[symmetric]
apply vcg
done
lemmas [vcg_rules] = ll_notime_htriple_eq[THEN iffD1, OF llvm_free_rule]
lemma FST_EXS_conv[sep_algebra_simps, named_ss fri_prepare_simps, vcg_normalize_simps]: "FST (EXS x. P x) = (EXS x. FST (P x))"
by (auto simp: FST_def sep_algebra_simps)
text ‹Free takes a range and the matching allocation tag›
lemma ll_free_rule[vcg_rules]:
"llvm_htriple
(↿(ll_range {0..<n}) blk p ** ll_malloc_tag n p)
(ll_free p)
(λ_. □)
"
unfolding ll_free_def ll_pto_def ll_malloc_tag_def ll_range_def vcg_tag_defs
supply [simp] = list_conj_eq_sep_set_img abase_ptr_def aidx_ptr_def
supply [named_ss fri_prepare_simps] = sep_set_img_pull_EXS FST_conj_conv[symmetric]
supply [vcg_normalize_simps] = FST_conj_conv[symmetric]
by vcg
end
subsection ‹Arithmetic Instructions›
text ‹Tag for arithmetic bounds check proof obligations›
definition [vcg_tag_defs]: "WBOUNDS Φ ⟷ Φ"
lemma WBOUNDSI: "Φ ⟹ WBOUNDS Φ" by (simp add: WBOUNDS_def)
lemma WBOUNDSD: "WBOUNDS Φ ⟹ Φ" by (simp add: WBOUNDS_def)
declaration ‹K (Basic_VCG.add_solver (@{thms WBOUNDSI},@{binding solve_wbounds},fn ctxt => SELECT_GOAL (auto_tac ctxt)))›
abbreviation "in_srange op (a::'a::len word) (b::'a word) ≡ op (sint a) (sint b) ∈ sints (LENGTH ('a))"
lemma udivrem_is_undef_word_conv:
fixes a b :: "'a::len word"
shows "udivrem_is_undef (word_to_lint a) (word_to_lint b) ⟷ b=0"
by (auto simp: udivrem_is_undef_def word_to_lint_to_uint_0_iff)
lemma sdivrem_is_undef_word_conv:
fixes a b :: "'a::len word"
shows "sdivrem_is_undef (word_to_lint a) (word_to_lint b) ⟷ b=0 ∨ ¬in_srange (sdiv) a b"
by (auto simp: sdivrem_is_undef_def sdivrem_ovf_def word_to_lint_to_sint_conv)
subsubsection ‹VCG Simplifications and Rules›
text ‹
Most of the rules for arithmetic are set up as simplifications.
For operations with side-conditions, we have both,
a conditional simplification rule and a Hoare-rule.
Note that the Hoare-rule will only be tried if the simplification rule did not
succeed.
›
abbreviation ll_consume :: "cost ⇒ unit llM" where "ll_consume ≡ consume"
context llvm_prim_setup begin
abbreviation "consume1r n v ≡ doM {ll_consume (cost n 1); return v}"
lemma cond_llvm_htripleI: "x = consume1r n y ⟹ llvm_htriple ($$ n 1) x (λr. ↑(r=y))" by vcg
end
locale llvm_prim_arith_setup begin
sublocale llvm_prim_setup .
context
notes [simp] = op_lift_arith2'_def op_lift_arith2_def
op_lift_cmp_def op_lift_ptr_cmp_def op_lift_iconv_def
notes [simp] = word_to_lint_convs[symmetric]
notes [simp] = from_bool_lint_conv udivrem_is_undef_word_conv sdivrem_is_undef_word_conv
notes [simp] = word_to_lint_to_uint_conv word_to_lint_to_sint_conv
begin
paragraph ‹Arithmetic›
lemma ll_add_simp[vcg_normalize_simps]: "ll_add a b = consume1r ''add'' (a + b)" by (auto simp: ll_add_def)
lemma ll_sub_simp[vcg_normalize_simps]: "ll_sub a b = consume1r ''sub'' (a - b)" by (auto simp: ll_sub_def)
lemma ll_mul_simp[vcg_normalize_simps]: "ll_mul a b = consume1r ''mul'' (a * b)" by (auto simp: ll_mul_def)
lemma ll_udiv_simp[vcg_normalize_simps]: "b≠0 ⟹ ll_udiv a b = consume1r ''udiv'' (a div b)" by (auto simp: ll_udiv_def)
lemma ll_urem_simp[vcg_normalize_simps]: "b≠0 ⟹ ll_urem a b = consume1r ''urem'' (a mod b)" by (auto simp: ll_urem_def)
lemma ll_sdiv_simp[vcg_normalize_simps]: "⟦b≠0; in_srange (sdiv) a b⟧ ⟹ ll_sdiv a b = consume1r ''sdiv'' (a sdiv b)"
by (auto simp: ll_sdiv_def Let_def)
lemma ll_srem_simp[vcg_normalize_simps]: "⟦b≠0; in_srange (sdiv) a b⟧ ⟹ ll_srem a b = consume1r ''srem'' (a smod b)"
by (auto simp: ll_srem_def)
lemma ll_udiv_rule[vcg_rules]: "WBOUNDS (b≠0) ⟹ llvm_htriple ($$ ''udiv'' 1) (ll_udiv a b) (λr. ↑(r = a div b))"
unfolding vcg_tag_defs by vcg
lemma ll_urem_rule[vcg_rules]: "WBOUNDS (b≠0) ⟹ llvm_htriple ($$ ''urem'' 1) (ll_urem a b) (λr. ↑(r = a mod b))"
unfolding vcg_tag_defs by vcg
lemma ll_sdiv_rule[vcg_rules]: "⟦WBOUNDS (b≠0); WBOUNDS (in_srange (sdiv) a b)⟧ ⟹ llvm_htriple ($$ ''sdiv'' 1) (ll_sdiv a b) (λr. ↑(r = a sdiv b))"
unfolding vcg_tag_defs by vcg
lemma ll_srem_rule[vcg_rules]: "⟦WBOUNDS (b≠0); WBOUNDS (in_srange (sdiv) a b)⟧ ⟹ llvm_htriple ($$ ''srem'' 1) (ll_srem a b) (λr. ↑(r = a smod b))"
unfolding vcg_tag_defs by vcg
paragraph ‹Comparison›
lemma ll_icmp_simps[vcg_normalize_simps]:
"ll_icmp_eq a b = consume1r ''icmp_eq'' (from_bool (a = b))"
"ll_icmp_ne a b = consume1r ''icmp_ne'' (from_bool (a ≠ b))"
"ll_icmp_sle a b = consume1r ''icmp_sle'' (from_bool (a <=s b))"
"ll_icmp_slt a b = consume1r ''icmp_slt'' (from_bool (a <s b))"
"ll_icmp_ule a b = consume1r ''icmp_ule'' (from_bool (a ≤ b))"
"ll_icmp_ult a b = consume1r ''icmp_ult'' (from_bool (a < b))"
unfolding ll_icmp_eq_def ll_icmp_ne_def ll_icmp_sle_def ll_icmp_slt_def ll_icmp_ule_def ll_icmp_ult_def
by auto
lemma ll_ptrcmp_simps[vcg_normalize_simps]:
"ll_ptrcmp_eq a b = consume1r ''ptrcmp_eq'' (from_bool (a = b))"
"ll_ptrcmp_ne a b = consume1r ''ptrcmp_ne'' (from_bool (a ≠ b))"
unfolding ll_ptrcmp_eq_def ll_ptrcmp_ne_def
by auto
paragraph ‹Bitwise›
lemma ll_and_simp[vcg_normalize_simps]: "ll_and a b = consume1r ''and'' (a AND b)" by (auto simp: ll_and_def)
lemma ll_or_simp[vcg_normalize_simps]: "ll_or a b = consume1r ''or'' (a OR b)" by (auto simp: ll_or_def)
lemma ll_xor_simp[vcg_normalize_simps]: "ll_xor a b = consume1r ''xor'' (a XOR b)" by (auto simp: ll_xor_def)
lemma ll_shl_simp[vcg_normalize_simps]: "unat b < LENGTH ('a) ⟹ ll_shl (a::'a::len word) b = consume1r ''shl'' (a << unat b)"
by (auto simp: ll_shl_def Let_def shift_ovf_def bitSHL'_def)
lemma ll_lshr_simp[vcg_normalize_simps]: "unat b < LENGTH ('a) ⟹ ll_lshr (a::'a::len word) b = consume1r ''lshr'' (a >> unat b)"
by (auto simp: ll_lshr_def Let_def shift_ovf_def bitLSHR'_def)
lemma ll_ashr_simp[vcg_normalize_simps]: "unat b < LENGTH ('a) ⟹ ll_ashr (a::'a::len word) b = consume1r ''ashr'' (a >>> unat b)"
by (auto simp: ll_ashr_def Let_def shift_ovf_def bitASHR'_def)
lemma [vcg_rules]:
fixes a b :: "'a::len word"
assumes "WBOUNDS (unat b < LENGTH ('a))"
shows ll_shl_rule: "llvm_htriple ($$ ''shl'' 1) (ll_shl a b) (λr. ↑(r=a<<unat b))"
and ll_lshr_rule: "llvm_htriple ($$ ''lshr'' 1) (ll_lshr a b) (λr. ↑(r=a>>unat b))"
and ll_ashr_rule: "llvm_htriple ($$ ''ashr'' 1) (ll_ashr a b) (λr. ↑(r=a>>>unat b))"
using assms unfolding vcg_tag_defs
by vcg
paragraph ‹Conversion›
lemma ll_trunc_simp[vcg_normalize_simps]: "is_down' UCAST ('a→'b) ⟹ ll_trunc (a::'a::len word) TYPE('b::len word) = consume1r ''trunc'' (UCAST ('a→'b) a)"
by (auto simp: ll_trunc_def llb_trunc_def Let_def)
lemma ll_zext_simp[vcg_normalize_simps]: "is_up' UCAST ('a→'b) ⟹ ll_zext (a::'a::len word) TYPE('b::len word) = consume1r ''zext'' (UCAST ('a→'b) a)"
by (auto simp: ll_zext_def llb_zext_def Let_def)
lemma ll_sext_simp[vcg_normalize_simps]: "is_up' SCAST ('a→'b) ⟹ ll_sext (a::'a::len word) TYPE('b::len word) = consume1r ''sext'' (SCAST ('a→'b) a)"
by (auto simp: ll_sext_def llb_sext_def Let_def)
lemmas ll_trunc_rule[vcg_rules] = cond_llvm_htripleI[OF ll_trunc_simp, OF WBOUNDSD]
lemmas ll_zext_rule[vcg_rules] = cond_llvm_htripleI[OF ll_zext_simp, OF WBOUNDSD]
lemmas ll_sext_rule[vcg_rules] = cond_llvm_htripleI[OF ll_sext_simp, OF WBOUNDSD]
end
end
subsection ‹Control Flow›
locale llvm_prim_ctrl_setup begin
sublocale llvm_prim_setup .
text ‹The if command is handled by a set of normalization rules.
Note that the VCG will split on the introduced conjunction automatically.
›
lemma llc_if_simps[vcg_normalize_simps]:
"llc_if 1 t e = doM {consume (cost ''if'' 1); t}"
"r≠0 ⟹ llc_if r t e = doM {consume (cost ''if'' 1); t}"
"llc_if 0 t e = doM {consume (cost ''if'' 1); e}"
by (auto simp: llc_if_def)
lemma llc_if_simp[vcg_normalize_simps]: "wp (llc_if b t e) Q s ⟷ wp (ll_consume (cost ''if'' 1)) (λ_ s. (to_bool b ⟶ wp t Q s) ∧ (¬to_bool b ⟶ wp e Q s)) s"
unfolding llc_if_def
by (auto simp add: vcg_normalize_simps)
lemma if_simp: "wp (If b t e) Q s ⟷ (b ⟶ wp t Q s) ∧ (¬b ⟶ wp e Q s)"
by simp
end
text ‹The while command is handled by a standard invariant/variant rule.›
lemma llc_while_unfold: "llc_while b f σ = doM { ll_consume (cost ''call'' 1); ctd ← b σ; llc_if ctd (doM { σ←f σ; llc_while b f σ}) (return σ)}"
unfolding llc_while_def
apply (rewrite REC'_unfold[OF reflexive], pf_mono_prover)
by (simp add: ll_call_def)
definition llc_while_annot :: "('σ::llvm_rep ⇒ 't ⇒ ll_astate ⇒ bool) ⇒ ('t×'t) set ⇒ ('σ⇒1 word llM) ⇒ _"
where [llvm_inline]: "llc_while_annot I R ≡ llc_while"
declare [[vcg_const "llc_while_annot I R"]]
lemma annotate_llc_while: "llc_while = llc_while_annot I R" by (simp add: llc_while_annot_def)
lemma "mwp (run (doM { r←m; consume c; return r }) s) N (λ_. N) E S = mwp (run (doM {consume c; m}) s) N (λ_. N) E S"
unfolding mwp_def bind_def consume_def
apply (auto split: mres.split simp: run_simps)
oops
lemma "mwp (run (doM { r←m; consume (c::_::comm_monoid_add); return r }) s) N (λ_. N) bot S = mwp (run (doM {consume c; m}) s) N (λ_. N) bot S"
unfolding mwp_def bind_def consume_def
by (auto split: mres.split simp: run_simps algebra_simps)
lemma "mwp (run (doM { r←m; consume (c::_::comm_monoid_add); return r }) s) bot bot bot S = mwp (run (doM {consume c; m}) s) bot bot bot S"
unfolding mwp_def bind_def consume_def
by (auto split: mres.split simp: run_simps algebra_simps)
lemma wp_consume_bind_commute: "wp (doM { r←m; consume c; f r }) Q = wp (doM {consume c; r←m; f r}) Q"
unfolding wp_def mwp_def bind_def consume_def
by (auto split: mres.split simp: run_simps algebra_simps fun_eq_iff)
lemma wp_consume_bind_commute_simp: "NO_MATCH (consume X) m ⟹ wp (doM { r←m; consume c; f r }) Q = wp (doM {consume c; r←m; f r}) Q"
by (rule wp_consume_bind_commute)
context llvm_prim_ctrl_setup begin
lemma basic_while_rule:
assumes "wf R"
assumes "llSTATE (I σ t) s"
assumes STEP: "⋀σ t s. ⟦ llSTATE (I σ t) s ⟧ ⟹ wp (doM {ll_consume (cost ''call'' 1); ctd ← b σ; ll_consume (cost ''if'' 1); return ctd}) (λctd s⇩1.
(to_bool ctd ⟶ wp (f σ) (λσ' s⇩2. llSTATE (EXS t'. I σ' t' ** ↑((t',t)∈R)) s⇩2) s⇩1)
∧ (¬to_bool ctd ⟶ Q σ s⇩1)
) s"
shows "wp (llc_while b f σ) Q s"
using assms(1,2)
proof (induction t arbitrary: σ s)
case (less t)
note STEP = STEP[simplified vcg_normalize_simps]
show ?case
apply (subst llc_while_unfold)
apply (simp only: vcg_normalize_simps)
apply (rule wp_monoI[OF STEP])
apply fact
subgoal for uu s⇩0
apply (simp add: vcg_normalize_simps)
apply (erule wp_monoI)
subgoal for r s⇩1
apply (cases "to_bool r"; simp add: vcg_normalize_simps)
subgoal
apply (erule wp_monoI; clarsimp simp: vcg_normalize_simps)
apply (erule wp_monoI; clarsimp; fri_extract)
apply (rule less.IH; assumption)
done
subgoal
apply (erule wp_monoI; clarsimp simp: vcg_normalize_simps)
done
done
done
done
qed
definition "enat_less_than ≡ {(a,b::enat). a<b}"
lemma wf_enat_less_than[simp, intro!]: "wf enat_less_than" unfolding enat_less_than_def by (rule wellorder_class.wf)
lemma wp_weaken_cost:
assumes "wp c (λr s'. (the_acost (snd s') ≤ the_acost (snd s)) ⟶ Q r s') s"
shows "wp c Q s"
using assms unfolding wp_def mwp_def
apply (auto simp: run_simps split: mres.splits)
by (smt acost.sel add.commute add_diff_cancel_enat enat.distinct(1) le_cost_ecost_def le_funI le_iff_add minus_ecost_cost_def)
lemma wp_weaken_cost_monoI:
assumes 1: "wp c Q' s"
assumes 2: "⋀r s'. ⟦ the_acost (snd s') ≤ the_acost (snd s); Q' r s' ⟧ ⟹ Q r s'"
shows "wp c Q s"
using assms
by (blast intro: wp_weaken_cost wp_monoI)
lemma wp_weaken_cost_monoI_STATE:
assumes 1: "wp c Q' s"
assumes 2: "⋀r s'. ⟦ the_acost (snd s') ≤ the_acost (snd s); Q' r s' ⟧ ⟹ Q r s'"
shows "wp c Q s"
using assms
by (blast intro: wp_weaken_cost wp_monoI)
text ‹
Standard while rule.
Note that the second parameter of the invariant is the termination measure, which must
decrease wrt. a well-founded relation. It is initialized as a schematic variable, and must be
derivable via frame inference. In practice, the invariant will contain a ‹↑(t=…)› part.
›
lemma llc_while_annot_rule[vcg_decomp_erules]:
assumes "llSTATE P s"
assumes "FRAME P (I σ t) F"
assumes WF: "SOLVE_AUTO_DEFER (wf R)"
assumes STEP: "⋀σ t s. ⟦ llSTATE ((I σ t ** F)) s ⟧ ⟹ EXTRACT (wp (doM {ll_consume (cost ''call'' 1); ctd ← b σ; ll_consume (cost ''if'' 1); return ctd}) (λctd s⇩1.
(to_bool ctd ⟶ wp (f σ) (λσ' s⇩2. llPOST (EXS t'. I σ' t' ** ↑((t',t)∈R) ** F) s⇩2) s⇩1)
∧ (¬to_bool ctd ⟶ Q σ s⇩1)
) s)"
shows "wp (llc_while_annot I R b f σ) Q s"
proof -
from ‹llSTATE P s› ‹FRAME P (I σ t) F› have PRE: "llSTATE (I σ t ** F) s"
unfolding FRAME_def STATE_def entails_def
by (simp del: split_paired_All)
show ?thesis
unfolding llc_while_annot_def
apply (rule basic_while_rule[where I="λσ t. I σ t ** F" and R=R])
subgoal using WF unfolding vcg_tag_defs .
apply (rule PRE)
using STEP unfolding vcg_tag_defs
apply (simp add: sep_algebra_simps)
done
qed
end
subsection ‹LLVM Code Generator Setup›
lemma elim_higher_order_return[llvm_inline]: "doM { x::_⇒_ ← return f; m x } = m f" by simp
text ‹Useful shortcuts›
subsubsection ‹Direct Arithmetic›
subsubsection ‹Boolean Operations›
lemma (in llvm_prim_arith_setup) llvm_from_bool_inline[llvm_inline]:
"from_bool (a∧b) = (from_bool a AND from_bool b)"
"from_bool (a∨b) = (from_bool a OR from_bool b)"
"(from_bool (¬a)::1 word) = (1 - (from_bool a :: 1 word))"
subgoal by (metis and.idem and_zero_eq bit.conj_zero_left from_bool_eq_if')
subgoal by (smt (z3) from_bool_0 or.idem word_bw_comms(2) word_log_esimps(3))
subgoal by (metis (full_types) cancel_comm_monoid_add_class.diff_cancel diff_zero from_bool_eq_if')
done
subsubsection ‹Products›
lemma inline_prod_case[llvm_inline]: "(λ(a,b). f a b) = (λx. doM { a←prod_extract_fst x; b ← prod_extract_snd x; f a b })"
by (auto simp: prod_ops_simp)
lemma inline_return_prod_case[llvm_inline]:
"return (case x of (a,b) ⇒ f a b) = (case x of (a,b) ⇒ return (f a b))" by (rule prod.case_distrib)
lemma inline_return_prod[llvm_inline]: "return (a,b) = doM { x ← prod_insert_fst init a; x ← prod_insert_snd x b; return x }"
by (auto simp: prod_ops_simp)
context begin
interpretation llvm_prim_setup .
lemma ll_extract_pair_pair:
"ll_extract_fst (a,b) = return a"
"ll_extract_snd (a,b) = return b"
unfolding ll_extract_fst_def ll_extract_snd_def checked_split_pair_def checked_from_val_def
by auto
end
subsubsection ‹Marking of constants›
definition "ll_const x ≡ return x"
lemma ll_const_inline[llvm_inline]: "bind (ll_const x) f = f x" by (auto simp: ll_const_def)
declare [[vcg_const "numeral a"]]
declare [[vcg_const "ll_const c"]]
section ‹Data Refinement›
locale standard_opr_abstraction =
fixes α :: "'c ⇒ 'a"
and I :: "'c ⇒ bool"
and dflt_PRE1 :: "('a⇒'a) ⇒ 'c itself ⇒ 'a ⇒ bool"
and dflt_PRE2 :: "('a⇒'a⇒'a) ⇒ 'c itself ⇒ 'a ⇒ 'a ⇒ bool"
and dflt_EPURE :: "'a ⇒ 'c ⇒ bool"
assumes dflt_EPURE_correct: "⋀c. I c ⟹ dflt_EPURE (α c) c"
begin
interpretation llvm_prim_setup .
definition "assn ≡ mk_pure_assn (λa c. I c ∧ a=α c)"
lemma assn_pure[is_pure_rule]: "is_pure assn"
by (auto simp: assn_def)
lemma vcg_prep_delete_assn[vcg_prep_ext_rules]:
"pure_part (↿assn a c) ⟹ dflt_EPURE a c"
by (auto simp: assn_def dflt_EPURE_correct)
definition "is_un_op name PRE cop mop aop ≡
(∀a::'c. I a ∧ PRE TYPE('c) (α a) ⟶ I (mop a) ∧ α (mop a) = aop (α a) ∧ cop a = consume1r name (mop a))"
definition "is_bin_op name PRE cop mop aop ≡
(∀a b::'c. I a ∧ I b ∧ PRE TYPE('c) (α a) (α b) ⟶ I (mop a b) ∧ α (mop a b) = aop (α a) (α b) ∧ cop a b = consume1r name (mop a b))"
abbreviation "is_un_op' name cop mop aop ≡ is_un_op name (dflt_PRE1 aop) cop mop aop"
abbreviation "is_bin_op' name cop mop aop ≡ is_bin_op name (dflt_PRE2 aop) cop mop aop"
lemma is_un_opI[intro?]:
assumes "⋀a. ⟦I a; PRE TYPE('c) (α a)⟧ ⟹ cop a = consume1r name (mop a)"
assumes "⋀a. ⟦I a; PRE TYPE('c) (α a)⟧ ⟹ I (mop a)"
assumes "⋀a. ⟦I a; PRE TYPE('c) (α a)⟧ ⟹ α (mop a) = aop (α a)"
shows "is_un_op name PRE cop mop aop"
using assms unfolding is_un_op_def by blast
lemma is_bin_opI[intro?]:
assumes "⋀a b. ⟦I a; I b; PRE TYPE('c) (α a) (α b)⟧ ⟹ cop a b = consume1r name (mop a b)"
assumes "⋀a b. ⟦I a; I b; PRE TYPE('c) (α a) (α b)⟧ ⟹ I (mop a b)"
assumes "⋀a b. ⟦I a; I b; PRE TYPE('c) (α a) (α b)⟧ ⟹ α (mop a b) = aop (α a) (α b)"
shows "is_bin_op name PRE cop mop aop"
using assms unfolding is_bin_op_def by blast
lemma un_op_tmpl:
fixes w :: "'c"
assumes A: "is_un_op name PRE cop mop aop"
shows "llvm_htriple
($$ name 1 ** ↿assn i w ** ↑⇩d(PRE TYPE('c) i))
(cop w)
(λr. ↿assn (aop i) r ** ↿assn i w)
"
proof -
interpret llvm_prim_arith_setup .
show ?thesis
using A
unfolding is_un_op_def assn_def apply clarsimp
by vcg
qed
lemma bin_op_tmpl:
fixes w⇩1 w⇩2 :: "'c"
assumes A: "is_bin_op name PRE cop mop aop"
shows "llvm_htriple
($$name 1 ** ↿assn i⇩1 w⇩1 ** ↿assn i⇩2 w⇩2 ** ↑⇩d(PRE TYPE('c) i⇩1 i⇩2))
(cop w⇩1 w⇩2)
(λr. ↿assn (aop i⇩1 i⇩2) r ** ↿assn i⇩1 w⇩1 ** ↿assn i⇩2 w⇩2)
"
proof -
interpret llvm_prim_arith_setup .
show ?thesis
using A
unfolding is_bin_op_def assn_def apply clarsimp
by vcg
qed
end
interpretation bool: standard_opr_abstraction "to_bool::1 word ⇒ bool" "λ_. True" ‹λ_ _ _. True› ‹λ_ _ _ _. True› "λ_ _. True"
by standard auto
context standard_opr_abstraction begin
interpretation llvm_prim_setup .
definition "is_cmp_op name cop mop aop ≡
(∀a b. I a ∧ I b ⟶ (cop a b = consume1r name (from_bool (mop a b)) ∧ (mop a b ⟷ aop (α a) (α b))))"
lemma is_cmp_opI[intro?]:
assumes "⋀a b. ⟦I a; I b⟧ ⟹ cop a b = consume1r name (from_bool (mop a b))"
assumes "⋀a b. ⟦I a; I b⟧ ⟹ mop a b ⟷ aop (α a) (α b)"
shows "is_cmp_op name cop mop aop"
using assms unfolding is_cmp_op_def by blast
lemma cmp_op_tmpl:
fixes w⇩1 w⇩2 :: "'c"
assumes "is_cmp_op name cop mop aop"
shows "llvm_htriple
($$ name 1 ** ↿assn i⇩1 w⇩1 ** ↿assn i⇩2 w⇩2)
(cop w⇩1 w⇩2)
(λr. ↿bool.assn (aop i⇩1 i⇩2) r ** ↿assn i⇩1 w⇩1 ** ↿assn i⇩2 w⇩2)
"
using assms unfolding is_cmp_op_def assn_def bool.assn_def apply clarsimp
by vcg
end
subsection ‹Booleans›
lemma to_bool_logics:
fixes a b :: "1 word"
shows "to_bool (a&&b) ⟷ to_bool a ∧ to_bool b"
and "to_bool (a||b) ⟷ to_bool a ∨ to_bool b"
and "to_bool (a XOR b) ⟷ to_bool a ≠ to_bool b"
and "to_bool (NOT a) ⟷ ¬to_bool a"
apply (cases a; cases b; simp; fail)
apply (cases a; cases b; simp; fail)
apply (cases a; cases b; simp; fail)
apply (cases a; simp; fail)
done
context begin
interpretation llvm_prim_arith_setup .
abbreviation ll_not1 :: "1 word ⇒ 1 word llM" where "ll_not1 x ≡ ll_add x 1"
lemma bool_bin_ops:
"bool.is_bin_op' ''and'' ll_and (AND) (∧)"
"bool.is_bin_op' ''or'' ll_or (OR) (∨)"
"bool.is_bin_op' ''xor'' ll_xor (XOR) (≠)"
apply (all ‹rule›)
apply (simp_all only: to_bool_logics)
apply (all ‹vcg_normalize?›)
done
lemma bool_un_ops:
"bool.is_un_op' ''add'' ll_not1 (NOT) Not"
apply (all ‹rule›)
apply (simp_all only: to_bool_logics)
apply (all ‹vcg_normalize?›)
apply (simp_all add: word1_NOT_eq)
done
lemmas bool_op_rules[vcg_rules] =
bool_bin_ops[THEN bool.bin_op_tmpl]
bool_un_ops[THEN bool.un_op_tmpl]
end
subsection ‹Control Flow›
definition "ABSTRACT c ty P s ≡ ∃F a. llSTATE (↿ty a c ** F) s ∧ P a"
lemma ABSTRACT_pure: "is_pure A ⟹ ABSTRACT c A P h ⟷ (∃a. ♭⇩pA a c ∧ P a)"
unfolding ABSTRACT_def
apply (cases h)
apply (auto simp only: STATE_def dr_assn_pure_asm_prefix_def sep_conj_def
pure_part_def ll_α_def lift_α_cost_def)
by (metis disjoint_zero_sym extract_pure_assn pred_lift_extract_simps(1) sep_add_zero_sym)
lemma ABSTRACT_erule[vcg_decomp_erules]:
assumes "llSTATE P s"
assumes "FRAME P (↿ty a c) F"
assumes "llSTATE (↿ty a c ** F) s ⟹ EXTRACT (Q a)"
shows "ABSTRACT c ty Q s"
using assms
by (auto simp: FRAME_def ABSTRACT_def STATE_def entails_def vcg_tag_defs simp del: split_paired_All)
context begin
interpretation llvm_prim_arith_setup + llvm_prim_ctrl_setup .
lemma dr_normalize_llc_if[vcg_normalize_simps]:
"♭⇩pbool.assn b bi ⟹ wp (llc_if bi t e) Q s ⟷ wp (consume1r ''if'' ()) (λ_ s. (b ⟶ wp t Q s) ∧ (¬b⟶wp e Q s)) s"
unfolding bool.assn_def by vcg_normalize
lemma llc_while_annot_dr_rule[vcg_decomp_erules]:
assumes "llSTATE P s"
assumes "FRAME P (I σ t) F"
assumes WF: "SOLVE_AUTO_DEFER (wf R)"
assumes STEP: "⋀σ t s. ⟦ llSTATE ((I σ t ** F)) s ⟧ ⟹ EXTRACT (wp (doM {ll_consume (cost ''call'' 1); ctd ← b σ; ll_consume (cost ''if'' 1); return ctd}) (λctdi s⇩1.
ABSTRACT ctdi bool.assn (λctd.
(ctd ⟶ wp (f σ) (λσ' s⇩2. llPOST (EXS t'. I σ' t' ** ↑⇩d((t',t)∈R) ** F) s⇩2) s⇩1)
∧ (¬ctd ⟶ Q σ s⇩1)
) s⇩1
) s)"
shows "wp (llc_while_annot I R b f σ) Q s"
using assms(1) apply -
apply vcg_rl
apply fact
apply fact
apply (drule STEP)
apply (simp add: fri_extract_simps ABSTRACT_pure vcg_tag_defs bool.assn_def)
done
end
end