Theory Stack_Typing
section ‹More Stack Typing›
theory Stack_Typing
imports L2Defs Runs_To_VCG
begin
definition equal_upto:: "'a set ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'b) ⇒ bool" where
"equal_upto S f g = (∀x. x ∉ S ⟶ f x = g x)"
lemma equal_upto_refl[simp, intro]: "equal_upto S f f"
by (simp add: equal_upto_def)
lemma symp_equal_upto: "symp (equal_upto S)"
by (simp add: equal_upto_def symp_def)
lemma equal_upto_commute: "equal_upto S f g ⟷ equal_upto S g f"
using symp_equal_upto
by (metis sympE)
lemma equal_upto_trans[trans]: "equal_upto S f g ⟹ equal_upto S g h ⟹ equal_upto S f h"
by (simp add: equal_upto_def)
lemma equal_upto_mono: "S ⊆ T ⟹ equal_upto S f g ⟹ equal_upto T f g"
by (meson equal_upto_def subset_iff)
definition equal_on:: "'a set ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'b) ⇒ bool" where
"equal_on S f g = (∀x. x ∈ S ⟶ f x = g x)"
lemma equal_on_UNIV_iff[simp]: "equal_on UNIV f g ⟷ f = g"
by (auto simp add: equal_on_def)
lemma equal_on_refl [simp, intro]: "equal_on S f f"
by (auto simp add: equal_on_def)
lemma symp_equal_on: "symp (equal_on S)"
by (simp add: equal_on_def symp_def)
lemma equal_on_commute: "equal_on S f g ⟷ equal_on S g f"
using symp_equal_on
by (metis sympE)
lemma equal_on_trans[trans]: "equal_on S f g ⟹ equal_on S g h ⟹ equal_on S f h"
by (simp add: equal_on_def)
lemma equal_on_mono: "S ⊆ T ⟹ equal_on T f g ⟹ equal_on S f g"
by (meson equal_on_def subset_iff)
lemma equal_on_equal_upto_eq: "equal_on S f g ⟹ equal_upto S f g ⟹ f = g"
by (auto simp add: equal_on_def equal_upto_def)
named_theorems unchanged_typing_on_simps and unchanged_typing
declare mex_def [unchanged_typing_on_simps]
declare meq_def [unchanged_typing_on_simps]
ML ‹
structure Unchanged_Typing =
struct
fun unchanged_typing_tac splitter ctxt =
let
val unchanged_typing_on_simps = Named_Theorems.get ctxt @{named_theorems unchanged_typing_on_simps}
val unchanged_typing = Named_Theorems.get ctxt @{named_theorems unchanged_typing}
val vcg_attrs = map (Attrib.attribute ctxt) @{attributes [runs_to_vcg]}
val (_, ctxt) = ctxt |> fold_map (Thm.proof_attributes vcg_attrs) unchanged_typing
val ctxt = ctxt addsimps unchanged_typing_on_simps
val trace_tac = Runs_To_VCG.no_trace_tac
fun solver_tac ctxt = ALLGOALS (asm_full_simp_tac ctxt)
in
Runs_To_VCG.runs_to_vcg_tac splitter (~1) trace_tac
{do_nosplit = false, no_unsafe_hyp_subst = false} solver_tac ctxt
end
end
›
lemma stack_allocs_releases_equal_on_stack:
"(p, d2) ∈ stack_allocs n 𝒮 TYPE('a::mem_type) d1 ⟹
equal_on 𝒮 d2 d3 ⟹ equal_on 𝒮 d1 (stack_releases n p d3)"
by (smt (verit, best) equal_on_def stack_releases_footprint stack_releases_other
stack_releases_stack_allocs_inverse)
lemma stack_allocs_releases_equal_on_typing:
"(p, d2) ∈ stack_allocs n 𝒮 TYPE('a::mem_type) d1 ⟹
equal_on X d2 d3 ⟹ equal_on X d1 (stack_releases n p d3)"
by (smt (verit, best) equal_on_def stack_releases_footprint stack_releases_other
stack_releases_stack_allocs_inverse)
lemma stack_allocs_releases_equal_on_typing':
"(p, d2) ∈ stack_allocs n 𝒮 TYPE('a::mem_type) d1 ⟹
equal_on X' d2 d3 ⟹ X ⊆ X' ⟹ equal_on X d1 (stack_releases n p d3)"
using stack_allocs_releases_equal_on_typing
using equal_on_mono by blast
context heap_typing_state
begin
definition unchanged_typing_on:: "addr set ⇒ 's ⇒ 's ⇒ bool" where
"unchanged_typing_on S s t = equal_on S (htd s) (htd t)"
lemma unchanged_typing_on_UNIV_iff: "unchanged_typing_on UNIV s t ⟷ htd s = htd t"
by (auto simp add: unchanged_typing_on_def)
lemma unchanged_typing_on_UNIV_I: "htd s = htd t ⟹ unchanged_typing_on UNIV s t"
by (simp add: unchanged_typing_on_UNIV_iff)
lemma typing_eq_unchanged_typing_on: "htd s = htd t ⟹ unchanged_typing_on S s t"
by (auto simp add: unchanged_typing_on_def equal_on_def)
lemma unchanged_typing_on_relf[simp]: "unchanged_typing_on S s s"
by (auto simp add: unchanged_typing_on_def equal_on_def)
lemma unchanged_typing_on_conv[unchanged_typing_on_simps]: "unchanged_typing_on S s t ⟷ (∀a ∈ S. htd s a = htd t a)"
by (auto simp add: unchanged_typing_on_def equal_on_def)
lemma unchanged_typing_on_cong: "(⋀a. a ∈ S ⟹ htd s a = htd s' a) ⟹
(⋀a. a ∈ S ⟹ htd t a = htd t' a)
⟹ unchanged_typing_on S s t ⟷ unchanged_typing_on S s' t"
by (simp add: unchanged_typing_on_def equal_on_def)
lemma typing_eq_left_unchanged_typing_on: "htd s1 = htd s2 ⟹
unchanged_typing_on S s1 t ⟷ unchanged_typing_on S s2 t"
by (auto simp add: unchanged_typing_on_def equal_on_def)
lemma symp_unchanged_typing_on: "symp (unchanged_typing_on S)"
using symp_equal_on
by (metis symp_def unchanged_typing_on_def)
lemma unchanged_typing_on_commute: "unchanged_typing_on S s t ⟷ unchanged_typing_on S t s"
using symp_unchanged_typing_on
by (metis sympE)
lemma unchanged_typing_on_trans[trans]:
assumes s_t: "unchanged_typing_on S s t"
assumes t_u: "unchanged_typing_on S t u"
shows "unchanged_typing_on S s u"
by (meson equal_on_trans s_t t_u unchanged_typing_on_def)
lemma unchanged_typing_on_mono: "S ⊆ T ⟹ unchanged_typing_on T s t ⟹ unchanged_typing_on S s t"
using equal_on_mono
by (smt (verit) unchanged_typing_on_def)
lemma unchanged_typing_on_root_ptr_valid_preservation:
fixes p::"'a::mem_type ptr"
assumes "unchanged_typing_on S s t"
assumes "ptr_span p ⊆ S"
assumes "root_ptr_valid (htd s) p"
shows "root_ptr_valid (htd t) p"
using assms
by (simp add: equal_on_def root_ptr_valid_domain subset_iff unchanged_typing_on_def)
simproc_setup unchanged_typing_nondet (‹c ∙ s ?⦃λr t. unchanged_typing_on 𝒮 s t⦄›) = ‹
let
val prop_to_meta_eq = @{lemma ‹P ⟹ (P ≡ True)› for P by auto}
fun try_prove ctxt prop = try (Goal.prove_internal ctxt [] prop)
(fn _ => Unchanged_Typing.unchanged_typing_tac NONE ctxt)
in
fn phi => fn ctxt => fn ct =>
let
val _ = Utils.verbose_msg 3 ctxt (fn _ => "unchanged_typing_nondet invoked on: " ^ @{make_string} ct)
in
try_prove ctxt \<^instantiate>‹P = ct in cterm ‹Trueprop P› for P›
|> Option.map (fn thm => prop_to_meta_eq OF [thm])
end
end
›
declare [[simproc del: unchanged_typing_nondet]]
end
context stack_heap_state
begin
lemma with_fresh_stack_ptr_unchanged_typing[unchanged_typing]:
assumes f[runs_to_vcg]:"⋀p s. (f p) ∙ s ?⦃λr t. typing.unchanged_typing_on 𝒮 s t⦄"
shows "(with_fresh_stack_ptr n I (L2_VARS f nm)) ∙ s ?⦃λr t. typing.unchanged_typing_on 𝒮 s t⦄"
unfolding with_fresh_stack_ptr_def on_exit_def on_exit'_def L2_VARS_def
apply (runs_to_vcg)
subgoal for x d vs r t
thm typing.typing_eq_left_unchanged_typing_on
thm typing.typing_eq_left_unchanged_typing_on [of _ "(htd_upd (λ_. d) s)"]
apply (subst (asm) typing.typing_eq_left_unchanged_typing_on [of _ "(htd_upd (λ_. d) s)"])
apply simp
apply (simp add: typing.unchanged_typing_on_def stack_allocs_releases_equal_on_stack)
done
done
end
lemma override_on_merge: "override_on (override_on f g B) g A = override_on f g (A ∪ B)"
by (auto simp add: override_on_def fun_eq_iff)
lemma override_on_id [simp]: "override_on f f A = f"
by (auto simp add: override_on_def)
lemma override_cancel_snd [simp]: "override_on f (override_on g1 g0 A) A = override_on f g0 A"
by (auto simp add: override_on_def)
lemma override_cancel_subset_snd : "A ⊆ B ⟹ override_on f (override_on g1 g0 B) A = override_on f g0 A"
by (auto simp add: override_on_def fun_eq_iff)
lemma override_cancel_fst[simp] : "override_on (override_on f1 f0 A) g A = override_on f1 g A"
by (auto simp add: override_on_def fun_eq_iff)
lemma override_cancel_subset_fst : "A ⊆ B ⟹ override_on (override_on f1 f0 A) g B = override_on f1 g B"
by (auto simp add: override_on_def fun_eq_iff)
lemma equal_on_stack_free_preservation:
assumes eq: "equal_on S d2 d1"
assumes "stack_free d1 ⊆ S"
assumes "stack_free d2 ⊆ S"
shows "stack_free d2 = stack_free d1"
using assms
by (smt (verit, best) Abs_fnat_hom_0 Collect_cong One_nat_def add.right_neutral equal_on_def less_Suc0 mem_Collect_eq ptr_val.simps
root_ptr_valid_def size_of_stack_byte(3) stack_free_def subsetD valid_root_footprint_def)
lemma equal_upto_disjoint_h_val: "equal_upto P h' h ⟹
ptr_span p ∩ P = {} ⟹
h_val h' (p::'a::mem_type ptr) = h_val h p"
by (smt (verit, best) disjoint_iff equal_upto_def h_val_def heap_list_h_eq2)
context heap_state
begin
definition equal_upto_heap_on:: "addr set ⇒ 's ⇒ 's ⇒ bool" where
"equal_upto_heap_on S s t = (∃T H.
t = hmem_upd (λ_. H) (htd_upd (λ_. T) s) ∧
equal_upto S (hmem s) H ∧
equal_upto S (htd s) T)"
definition zero_heap_on:: "addr set ⇒ 's ⇒ 's" where
"zero_heap_on A s = hmem_upd (λh. override_on h zero_heap A) (htd_upd (λhtd. override_on htd stack_byte_typing A) s)"
lemma equal_upto_heap_on_equal_upto_htd: "equal_upto_heap_on S s t ⟹ equal_upto S (htd s) (htd t)"
by (auto simp add: equal_upto_heap_on_def)
lemma equal_upto_heap_on_equal_upto_hmem: "equal_upto_heap_on S s t ⟹ equal_upto S (hmem s) (hmem t)"
by (auto simp add: equal_upto_heap_on_def)
lemma zero_heap_on_empty[simp]: "zero_heap_on {} s = s"
by (auto simp add: zero_heap_on_def)
lemma equal_upto_heap_on_zero_heap_on_subset: "A ⊆ B ⟹ equal_upto_heap_on B s (zero_heap_on A s)"
apply (clarsimp simp add: zero_heap_on_def equal_upto_heap_on_def override_on_def)
by (smt (verit, best) equal_upto_def equal_upto_mono heap.upd_cong hmem_htd_upd typing.upd_cong)
lemma equal_upto_heap_on_zero_heap_on[simp]: "equal_upto_heap_on A s (zero_heap_on A s)"
by (simp add: equal_upto_heap_on_zero_heap_on_subset)
lemma equal_upto_heap_on_refl[simp, intro]: "equal_upto_heap_on S s s"
by (force simp add: equal_upto_heap_on_def)
lemma override_on_heap_update_other:
fixes p::"'a::mem_type ptr"
shows "ptr_span p ⊆ A ⟹ override_on (heap_update p v h) f A = override_on h f A"
apply (clarsimp simp add: override_on_def fun_eq_iff)
by (smt (verit, ccfv_SIG) CTypes.mem_type_simps(2) heap_list_length heap_update_def heap_update_nmem_same subsetD)
lemma override_on_heap_update_commute:
fixes p::"'a::mem_type ptr"
shows "ptr_span p ∩ A = {} ⟹
override_on (heap_update p v h) f A = heap_update p v (override_on h f A)"
apply (clarsimp simp add: override_on_def fun_eq_iff heap_update_def heap_update_nmem_same orthD2)
by (smt (verit, best) disjoint_iff heap_list_h_eq2 heap_list_length heap_update_list_value len max_size)
lemma override_on_heap_update_padding_other:
fixes p::"'a::mem_type ptr"
shows "ptr_span p ⊆ A ⟹ length bs = size_of TYPE('a) ⟹ override_on (heap_update_padding p v bs h) f A = override_on h f A"
apply (clarsimp simp add: override_on_def fun_eq_iff)
by (smt (verit) CTypes.mem_type_simps(2) heap_update_nmem_same heap_update_padding_def subsetD)
lemma zero_heap_on_heap_update_other:
fixes p::"'a::mem_type ptr"
shows "ptr_span p ⊆ A ⟹ zero_heap_on A (hmem_upd (heap_update p v) s) = zero_heap_on A s"
by (simp add: zero_heap_on_def heap_commute comp_def override_on_heap_update_other)
lemma override_on_stack_byte_typing_stack_allocs:
assumes alloc: "(p, d) ∈ stack_allocs n 𝒮 TYPE('a::mem_type) d0"
assumes subset: "stack_free d0 ⊆ A"
shows "override_on d stack_byte_typing A = override_on d0 stack_byte_typing A"
using alloc subset
apply (simp add: override_on_def fun_eq_iff)
by (meson in_mono stack_allocs_other stack_allocs_stack_subset_stack_free)
lemma zero_heap_on_stack_allocs:
assumes alloc: "(p, d) ∈ stack_allocs n 𝒮 TYPE('a::mem_type) (htd s)"
assumes subset: "stack_free (htd s) ⊆ A"
shows "zero_heap_on A (htd_upd (λ_. d) s) = zero_heap_on A s"
apply (simp add: zero_heap_on_def comp_def)
using override_on_stack_byte_typing_stack_allocs [OF alloc subset]
by (metis (no_types, lifting) typing.upd_cong)
lemma zero_heap_on_stack_releases:
fixes p:: "'a::mem_type ptr"
assumes subset: "{ptr_val p..+n * size_of TYPE('a::mem_type)} ⊆ A"
shows "zero_heap_on A (htd_upd (stack_releases n p) s) = zero_heap_on A s"
using subset
by (simp add: zero_heap_on_def comp_def stack_releases_def override_on_merge Un_absorb2 )
lemma zero_heap_on_stack_releases':
fixes p:: "'a::mem_type ptr"
assumes guard: "(⋀i. i < n ⟹ c_null_guard (p +⇩p int i))"
shows "zero_heap_on (stack_free (stack_releases n p (htd s)) ∪ A) (htd_upd (stack_releases n p) s) =
zero_heap_on (stack_free (htd s) ∪ {ptr_val p..+n * size_of TYPE('a)} ∪ A) s"
apply (subst stack_free_stack_releases)
apply (simp add: guard)
apply (subst zero_heap_on_stack_releases)
apply blast
apply (simp add: sup_commute)
done
text ‹We want to express that certain portions of the heap (typing and values) are 'irrelevant',
in particular regarding (free) stack space. The notion of 'irrelevant' is a bit vague, it means
that the behaviour of the program does not depend on those locations and also that it does not
modify those locations. Moreover, we prefer an abstraction function rather than an
relation between states to avoid admissibility issues for refinement.›
definition frame:: "addr set ⇒ 's ⇒ 's ⇒ 's" where
"frame A s⇩0 s =
hmem_upd (λh. override_on h (hmem s⇩0) (A ∪ stack_free (htd s)))
(htd_upd (λd. override_on d (htd s⇩0) (A - stack_free (htd s))) s)"
text ‹The standard use case we have in mind is @{term "A ∩ stack_free (htd s) = {}"}, hence
@{prop "A - stack_free (htd s) = A"}, but nevertheless the intuition is:
▪ stack free typing from \<^term>‹s› is preserved, the framed sate has at least as many stack free
addresses as the original one. So we can simulate any stack allocation.
▪ heap values for stack free and \<^term>‹A› are taken from reference state \<^term>‹s⇩0›, this
captures that we do not depend on the original values in \<^term>‹s› for those addresses.
▪ typing for allocations in \<^term>‹A› is taken from reference state \<^term>‹s⇩0›, this captures
that we do not depend on the original typing in \<^term>‹s› for those addresses.
By taking the same reference state \<^term>‹s⇩0› to frame two states \<^term>‹s› and \<^term>‹s'›,
we can express that the 'irrelevant' parts of the heap did not change in the respective
framed states \<^term>‹frame A s⇩0 s› and \<^term>‹frame A s⇩0 s'›.
›
definition raw_frame:: "addr set ⇒ 's ⇒ 's ⇒ 's" where
"raw_frame A s⇩0 s =
hmem_upd (λh. override_on h (hmem s⇩0) A)
(htd_upd (λd. override_on d (htd s⇩0) A) s)"
lemma frame_heap_independent_selector:
"(⋀f s. sel (hmem_upd f s) = sel s) ⟹ (⋀f s. sel (htd_upd f s) = sel s) ⟹
sel (frame A s⇩0 s) = sel s"
by (auto simp add: frame_def)
lemma frame_id[simp]: "frame A s s = s"
unfolding frame_def
by (simp add: heap.upd_same typing.upd_same)
lemma frame_hmem_UNIV[simp]: "hmem (frame UNIV s⇩0 s) = hmem s⇩0"
unfolding frame_def
by simp
lemma hmem_frame: "hmem (frame A s⇩0 s) = (λa. if a ∈ A ∪ stack_free (htd s) then hmem s⇩0 a else hmem s a)"
unfolding frame_def
by (auto simp add: fun_eq_iff)
lemma htd_frame: "htd (frame A s⇩0 s) = (λa. if a ∈ (A - stack_free (htd s)) then htd s⇩0 a else htd s a)"
unfolding frame_def
by (auto simp add: fun_eq_iff)
lemma stack_free_htd_frame: "stack_free (htd s) ⊆ stack_free (htd (frame A s⇩0 s))"
apply (clarsimp simp add: htd_frame stack_free_def root_ptr_valid_def)
by (smt (verit) One_nat_def add.right_neutral less_Suc0 mem_Collect_eq orthD2 semiring_1_class.of_nat_0 size_of_stack_byte(3) valid_root_footprint_def)
lemma stack_free_htd_frame': "stack_free (htd s⇩0) ∩ A = {} ⟹ stack_free (htd (frame A s⇩0 s)) = stack_free (htd s)"
by (auto simp add: htd_frame stack_free_def root_ptr_valid_def valid_root_footprint_def)
lemma equal_on_hmem_frame: "equal_on (A ∪ stack_free (htd s)) (hmem (frame A s⇩0 s)) (hmem s⇩0)"
by (auto simp add: equal_on_def frame_def equal_upto_def override_on_def fun_eq_iff)
lemma equal_upto_hmem_frame: "equal_upto (A ∪ stack_free (htd s)) (hmem (frame A s⇩0 s)) (hmem s)"
by (auto simp add: equal_on_def frame_def equal_upto_def override_on_def fun_eq_iff)
lemma equal_on_htd_frame: "stack_free (htd s) ∩ A = {} ⟹ equal_on A (htd (frame A s⇩0 s)) (htd s⇩0)"
by (auto simp add: equal_on_def frame_def equal_upto_def override_on_def fun_eq_iff)
lemma equal_on_htd_stack_free_frame: "stack_free (htd s) ∩ A = {} ⟹
equal_on (stack_free (htd s)) (htd (frame A s⇩0 s)) (htd s)"
by (auto simp add: equal_on_def frame_def equal_upto_def override_on_def fun_eq_iff)
lemma equal_upto_htd_frame: "equal_upto A (htd (frame A s⇩0 s)) (htd s)"
by (auto simp add: equal_on_def frame_def equal_upto_def override_on_def fun_eq_iff)
lemma equal_upto_heap_on_frame: "equal_upto_heap_on (A ∪ stack_free (htd s)) (frame A s⇩0 s) s"
apply (clarsimp simp add: equal_upto_heap_on_def frame_def equal_upto_def override_on_def fun_eq_iff)
by (smt (verit, ccfv_threshold) K_record_comp heap.upd_compose heap.upd_same heap_commute typing.upd_compose typing.upd_same)
lemma frame_heap_update:
fixes p::"'a::mem_type ptr"
shows "ptr_span p ⊆ A ⟹ frame A s⇩0 (hmem_upd (heap_update p v) s) = frame A s⇩0 s"
apply (clarsimp simp add: frame_def)
apply (subst heap_commute [symmetric])
apply (simp add: comp_def )
apply (subst override_on_heap_update_other)
apply auto
done
lemma frame_heap_update_disjoint:
fixes p::"'a::mem_type ptr"
shows "ptr_span p ∩ A = {} ⟹ ptr_span p ∩ stack_free (htd s) = {} ⟹
frame A s⇩0 (hmem_upd (heap_update p v) s) = hmem_upd (heap_update p v) (frame A s⇩0 s)"
apply (clarsimp simp add: frame_def)
apply (subst heap_commute [symmetric])
apply (simp add: comp_def)
apply (subst override_on_heap_update_commute)
apply blast
apply blast
done
lemma h_val_frame_disjoint':
fixes p::"'a::mem_type ptr"
shows "ptr_span p ∩ A = {} ⟹ ptr_span p ∩ stack_free (htd s) = {} ⟹
ptr_span p = ptr_span p' ⟹
h_val (hmem (frame A s⇩0 s)) p' = h_val (hmem s) p'"
apply (clarsimp simp add: frame_def override_on_def)
by (smt (verit, del_insts) disjoint_iff h_val_def heap_list_h_eq2 hmem_htd_upd)
lemma h_val_frame_disjoint:
fixes p::"'a::mem_type ptr"
shows "ptr_span p ∩ A = {} ⟹ ptr_span p ∩ stack_free (htd s) = {} ⟹
h_val (hmem (frame A s⇩0 s)) p = h_val (hmem s) p"
apply (erule (1) h_val_frame_disjoint')
by (rule refl)
lemma h_val_frame_disjoint_globals:
fixes p::"'a::mem_type ptr"
assumes "𝒢 ∩ A = {}" "𝒢 ∩ stack_free (htd s) = {}"
assumes "ptr_span p ⊆ 𝒢"
shows "h_val (hmem (frame A s⇩0 s)) p = h_val (hmem s) p"
apply (rule h_val_frame_disjoint)
subgoal using assms by blast
subgoal using assms by blast
done
lemma frame_heap_update_padding:
fixes p::"'a::mem_type ptr"
shows "ptr_span p ⊆ A ⟹ length bs = size_of TYPE('a) ==> frame A s⇩0 (hmem_upd (heap_update_padding p v bs) s) = frame A s⇩0 s"
apply (clarsimp simp add: frame_def)
apply (subst heap_commute [symmetric])
apply (simp add: comp_def )
apply (subst override_on_heap_update_padding_other)
apply auto
done
lemma frame_stack_alloc:
fixes p::"'a::mem_type ptr"
assumes subset: "ptr_span p ⊆ stack_free (htd s)"
assumes disjoint: "stack_free (htd s) ∩ A = {}"
assumes alloc: "stack_free (ptr_force_type p (htd s)) = stack_free (htd s) - ptr_span p"
shows
"frame (ptr_span p ∪ A) (htd_upd (λd. override_on d stack_byte_typing (ptr_span p)) t⇩0)
(htd_upd (λ_. ptr_force_type p (htd s)) s) = frame A t⇩0 s"
proof -
from alloc subset disjoint
have *: "ptr_span p ∪ A ∪ stack_free (ptr_force_type p (htd s)) = A ∪ stack_free (htd s)"
by auto
from subset disjoint alloc
have **:"override_on (ptr_force_type p (htd s))
(override_on (htd t⇩0) stack_byte_typing (ptr_span p)) (ptr_span p ∪ A - stack_free (ptr_force_type p (htd s))) = override_on (htd s) (htd t⇩0) (A - stack_free (htd s))"
apply (clarsimp simp add: override_on_def fun_eq_iff ptr_force_type_d)
by (smt (verit, ccfv_threshold) add.right_neutral mem_Collect_eq old.prod.exhaust
prod.sel(1) prod.sel(2) ptr_val.ptr_val_def root_ptr_valid_def semiring_1_class.of_nat_0 stack_byte_typing_footprint stack_free_def subset_iff valid_root_footprint_def)
show ?thesis
apply (clarsimp simp add: frame_def comp_def * **)
by (metis (no_types, lifting) typing.upd_cong)
qed
lemma frame_stack_release:
fixes p::"'a::mem_type ptr"
assumes disjoint_free: "ptr_span p ∩ stack_free (htd s) = {}"
assumes disjoint_old: "ptr_span p ∩ A = {}"
assumes c_null_guard: "c_null_guard p"
assumes lbs: "length bs = size_of TYPE ('a)"
shows "frame (ptr_span p ∪ A) (htd_upd (λd. override_on d stack_byte_typing (ptr_span p)) t⇩0) s =
frame A t⇩0 (hmem_upd (heap_update_list (ptr_val p) bs) (htd_upd (stack_releases (Suc 0) p) s))"
proof -
from disjoint_free c_null_guard
have *: "(ptr_span p ∪ A ∪ stack_free (htd s)) = A ∪ stack_free (stack_releases (Suc 0) p (htd s))"
by (metis (no_types, opaque_lifting) Un_assoc add.right_neutral mult_0 stack_free_stack_release
stack_release_def stack_releases_def sup_commute times_nat.simps(2))
from disjoint_free disjoint_old c_null_guard
have **: "override_on (htd s) (override_on (htd t⇩0) stack_byte_typing (ptr_span p)) (ptr_span p ∪ A - stack_free (htd s)) =
override_on (stack_releases (Suc 0) p (htd s)) (htd t⇩0) (A - stack_free (stack_releases (Suc 0) p (htd s)))"
apply (clarsimp simp add: override_on_def fun_eq_iff stack_byte_typing_footprint stack_releases_footprint stack_releases_other,
intro conjI impI)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (metis UnE add.right_neutral mult_is_0 stack_free_stack_release stack_release_def stack_releases_def times_nat.simps(2))
using stack_free_stack_releases_mono by blast
have ***: "override_on (heap_update_list (ptr_val p) bs (hmem s)) (hmem t⇩0) (A ∪ stack_free (stack_releases (Suc 0) p (htd s)))
=
override_on (hmem s) (hmem t⇩0) (A ∪ stack_free (stack_releases (Suc 0) p (htd s)))"
using disjoint_old lbs *
apply (clarsimp simp add: override_on_def fun_eq_iff stack_byte_typing_footprint stack_releases_footprint stack_releases_other)
by (metis Un_iff heap_update_nmem_same lbs)
show ?thesis
apply (simp add: frame_def comp_def * )
apply (simp add: heap_commute)
using ** ***
by (metis (no_types, lifting) heap.get_upd heap.upd_compose heap.upd_cong htd_hmem_upd
typing.get_upd typing.upd_compose typing.upd_cong)
qed
lemma frame_stack_release_keep:
fixes p::"'a::mem_type ptr"
assumes disjoint_free: "ptr_span p ∩ stack_free (htd s) = {}"
assumes disjoint_old: "ptr_span p ∩ A = {}"
assumes c_null_guard: "c_null_guard p"
assumes lbs: "length bs = size_of TYPE('a)"
shows "hmem_upd (heap_update_list (ptr_val p) (heap_list (hmem t⇩0) (size_of TYPE('a)) (ptr_val p)))
( htd_upd (stack_releases (Suc 0) p) (frame A t⇩0 s)) =
frame A t⇩0
(hmem_upd (heap_update_list (ptr_val p) bs)
(htd_upd (stack_releases (Suc 0) p) s))"
proof -
from disjoint_free c_null_guard
have *: "(ptr_span p ∪ A ∪ stack_free (htd s)) = A ∪ stack_free (stack_releases (Suc 0) p (htd s))"
by (metis (no_types, opaque_lifting) Un_assoc add.right_neutral mult_0 stack_free_stack_release
stack_release_def stack_releases_def sup_commute times_nat.simps(2))
from disjoint_free disjoint_old c_null_guard
have **: "stack_releases (Suc 0) p (override_on (htd s) (htd t⇩0) (A - stack_free (htd s))) =
override_on (stack_releases (Suc 0) p (htd s)) (htd t⇩0) (A - stack_free (stack_releases (Suc 0) p (htd s)))"
apply (clarsimp simp add: override_on_def fun_eq_iff stack_byte_typing_footprint stack_releases_footprint stack_releases_other,
intro conjI impI)
subgoal by (smt (verit, del_insts) Un_iff add.right_neutral mult_is_0 stack_free_stack_release
stack_release_def stack_release_other stack_releases_def times_nat.simps(2))
subgoal by (smt (verit, best) UnE less_Suc0 ptr_add_0_id semiring_1_class.of_nat_0 stack_free_stack_releases
stack_releases_footprint stack_releases_other)
done
have ***: "heap_update_list (ptr_val p) (heap_list (hmem t⇩0) (size_of TYPE('a)) (ptr_val p))
(override_on (hmem s) (hmem t⇩0) (A ∪ stack_free (htd s))) =
override_on (heap_update_list (ptr_val p) bs (hmem s)) (hmem t⇩0)
(A ∪ stack_free (stack_releases (Suc 0) p (htd s)))"
using lbs disjoint_old disjoint_free *
apply (clarsimp simp add: override_on_def fun_eq_iff heap_update_nmem_same orthD2 heap_update_list_value )
apply (smt (verit, ccfv_SIG) Un_iff heap_list_length heap_update_list_id' heap_update_list_value max_size)
done
show ?thesis
apply (simp add: frame_def comp_def * heap_commute )
using ** ***
by (metis (no_types, lifting) heap.upd_cong htd_hmem_upd lense.upd_cong typing.lense_axioms)
qed
lemma symp_equal_upto_heap_on: "symp (equal_upto_heap_on S)"
proof
fix s t
assume "equal_upto_heap_on S s t"
then obtain T H where
t: "t = hmem_upd (λ_. H) (htd_upd (λ_. T) s)" and
eq_H: "equal_upto S (hmem s) H" and
eq_T: "equal_upto S (htd s) T"
by (auto simp add: equal_upto_heap_on_def)
show "equal_upto_heap_on S t s"
proof -
define H' where "H' = hmem s"
define T' where "T' = htd s"
have "s = hmem_upd (λ_. H') (htd_upd (λ_. T') t)"
unfolding H'_def T'_def
apply (subst t)
apply (simp add: heap_commute heap.upd_same typing.upd_same)
done
moreover
from eq_H have "equal_upto S (hmem t) H'"
by (simp add: H'_def equal_upto_commute t)
moreover
from eq_T have "equal_upto S (htd t) T'"
by (simp add: T'_def equal_upto_commute t)
ultimately show ?thesis
by (auto simp add: equal_upto_heap_on_def)
qed
qed
lemma equal_upto_heap_on_commute: "equal_upto_heap_on S s t ⟷ equal_upto_heap_on S s t"
using symp_equal_upto_heap_on
by (metis sympE)
lemma equal_upto_heap_on_trans[trans]:
assumes s_t: "equal_upto_heap_on S s t"
assumes t_u: "equal_upto_heap_on S t u"
shows "equal_upto_heap_on S s u"
proof -
from s_t obtain T H where
t: "t = hmem_upd (λ_. H) (htd_upd (λ_. T) s)" and
eq_H: "equal_upto S (hmem s) H" and
eq_T: "equal_upto S (htd s) T"
by (auto simp add: equal_upto_heap_on_def)
from t_u obtain T' H' where
u: "u = hmem_upd (λ_. H') (htd_upd (λ_. T') t)" and
eq_H': "equal_upto S (hmem t) H'" and
eq_T': "equal_upto S (htd t) T'"
by (auto simp add: equal_upto_heap_on_def)
have "u = hmem_upd (λ_. H') (htd_upd (λ_. T') s)"
apply (subst u)
apply (subst t)
apply (simp add: heap_commute comp_def)
done
moreover
from eq_H'
have "equal_upto S (hmem s) H'"
apply -
apply (subst (asm) t)
apply simp
using eq_H equal_upto_trans by blast
moreover
from eq_T'
have "equal_upto S (htd s) T'"
apply -
apply (subst (asm) t)
apply simp
using eq_T equal_upto_trans by blast
ultimately show ?thesis
by (auto simp add: equal_upto_heap_on_def)
qed
lemma equal_upto_heap_on_mono: "S ⊆ T ⟹ equal_upto_heap_on S s t ⟹ equal_upto_heap_on T s t"
using equal_upto_mono
by (smt (verit) equal_upto_heap_on_def)
end
lemma runs_to_partial_L2_modify[runs_to_vcg]:
"(L2_modify f) ∙ s ?⦃λr t. r = Result () ∧ t = f s⦄"
unfolding L2_defs
apply runs_to_vcg
done
lemma runs_to_partial_L2_unknown[runs_to_vcg]:
"(⋀x. P (Result x) s) ⟹ (L2_unknown ns) ∙ s ?⦃P⦄"
unfolding L2_defs
apply runs_to_vcg
apply simp
done
lemma runs_to_partial_L2_seq[runs_to_vcg]:
"f ∙ s ?⦃ λr t. (∀a. r = Result a ⟶ g a ∙ t ?⦃ Q ⦄) ∧ (∀e. r = Exn e ⟶ Q (Exn e) t) ⦄ ⟹
(L2_seq f g) ∙ s ?⦃ Q ⦄"
unfolding L2_defs
apply runs_to_vcg
done
lemma (in heap_typing_state) runs_to_partial_L2_seq[unchanged_typing]:
assumes [runs_to_vcg]: "f ∙ s ?⦃λr t. unchanged_typing_on S s t⦄"
assumes [runs_to_vcg]: "⋀r s. (g r) ∙ s ?⦃λr t. unchanged_typing_on S s t⦄"
shows "(L2_seq f g) ∙ s ?⦃λr t. unchanged_typing_on S s t⦄"
by (runs_to_vcg) (auto simp add: unchanged_typing_on_simps)
lemma runs_to_partial_L2_gets[runs_to_vcg]:
"P (Result (f s)) s ⟹ (L2_gets f ns) ∙ s ?⦃ P ⦄"
unfolding L2_defs
apply runs_to_vcg
done
lemma runs_to_partial_L2_condition[runs_to_vcg]:
"(P s ⟹ f ∙ s ?⦃Q⦄) ⟹ (¬ P s ⟹ g ∙ s ?⦃Q⦄) ⟹ (L2_condition P f g) ∙ s ?⦃Q⦄"
unfolding L2_defs
apply runs_to_vcg
apply auto
done
lemma runs_to_partial_L2_catch[runs_to_vcg]:
assumes [runs_to_vcg]: "f ∙ s ?⦃ λr t. (∀e. r = Exn e ⟶ ((g e) ∙ t ?⦃ P ⦄)) ∧ (∀v'. r = Result v' ⟶ P (Result v') t) ⦄"
shows "(L2_catch f g) ∙ s ?⦃P ⦄"
unfolding L2_defs
using assms
apply runs_to_vcg
done
lemma (in heap_typing_state) runs_to_partial_L2_catch[unchanged_typing]:
assumes [runs_to_vcg]: "f ∙ s ?⦃λr t. unchanged_typing_on S s t⦄"
assumes [runs_to_vcg]: "⋀r s. (g r) ∙ s ?⦃λr t. unchanged_typing_on S s t⦄"
shows "(L2_catch f g) ∙ s ?⦃λr t. unchanged_typing_on S s t⦄"
by (runs_to_vcg) (auto simp add: unchanged_typing_on_simps)
lemma runs_to_partial_L2_try[runs_to_vcg]:
assumes [runs_to_vcg]:
"f ∙ s ?⦃ λr. Q (unnest_exn r) ⦄"
shows "(L2_try f) ∙ s ?⦃ Q ⦄"
unfolding L2_defs
apply runs_to_vcg
done
lemma (in heap_typing_state) runs_to_partial_L2_try[unchanged_typing]:
assumes [runs_to_vcg]: "f ∙ s ?⦃λr t. unchanged_typing_on S s t⦄"
shows "(L2_try f) ∙ s ?⦃λr t. unchanged_typing_on S s t⦄"
by (runs_to_vcg)
lemma runs_to_partial_L2_while:
assumes B: "⋀r s. I (Result r) s ⟹ C r s ⟹ (B r) ∙ s ?⦃I⦄"
assumes Qr: "⋀r s. I (Result r) s ⟹ ¬ C r s ⟹ Q (Result r) s"
assumes Ql: "⋀e s. I (Exn e) s ⟹ Q (Exn e) s"
assumes I: "I (Result r) s"
shows "(L2_while C B r ns) ∙ s ?⦃ Q ⦄"
unfolding L2_defs
by (rule runs_to_partial_whileLoop_exn [where I=I, OF I Qr Ql B])
lemma runs_to_partial_L2_while_same_post:
assumes B: "⋀r s. Q (Result r) s ⟹ C r s ⟹ (B r) ∙ s ?⦃Q⦄"
assumes I: "Q (Result r) s"
shows "(L2_while C B r ns) ∙ s ?⦃ Q ⦄"
using assms
by - (rule runs_to_partial_L2_while)
lemma (in heap_typing_state) runs_to_partial_L2_while_unchanged_typing[unchanged_typing]:
assumes B[runs_to_vcg]: "⋀r s. C r s ⟹ (B r) ∙ s ?⦃λr t. unchanged_typing_on S s t⦄"
shows "(L2_while C B r ns) ∙ s ?⦃λr t. unchanged_typing_on S s t⦄"
supply runs_to_partial_L2_while_same_post [runs_to_vcg]
apply (runs_to_vcg)
apply (auto simp add: unchanged_typing_on_simps)
done
lemma runs_to_partial_L2_throw[runs_to_vcg]:
assumes "P (Exn e) s"
shows "(L2_throw e ns) ∙ s ?⦃ P ⦄"
unfolding L2_defs
using assms
by (rule runs_to_partial_yield)
lemma runs_to_partial_L2_spec[runs_to_vcg]: "(L2_spec R) ∙ s ?⦃λr t. (s, t) ∈ R⦄"
unfolding L2_defs
by runs_to_vcg
lemma runs_to_partial_state_L2_assume[runs_to_vcg]:
"(L2_assume R) ∙ s ?⦃λr t. ∃x. r = Result x ∧ (x, t) ∈ R s⦄"
unfolding L2_defs
apply (runs_to_vcg)
done
lemma runs_to_partial_L2_guard[runs_to_vcg]:
shows "(L2_guard P) ∙ s ?⦃ λr t. r = Result () ∧ s = t ∧ P s⦄"
unfolding L2_defs
apply (runs_to_vcg)
done
definition GUARDED_ASSM :: "bool ⇒ bool" where [remove_ASSMs]: "GUARDED_ASSM P ⟷ P"
lemma GUARDED_ASSM_D: "GUARDED_ASSM P ⟹ P" by (simp add: GUARDED_ASSM_def)
lemma runs_to_partial_L2_guarded[runs_to_vcg]:
"(GUARDED_ASSM (P s) ⟹ c ∙ s ?⦃Q⦄) ⟹ (L2_guarded P c) ∙ s ?⦃Q⦄"
unfolding L2_guarded_def GUARDED_ASSM_def
by runs_to_vcg
lemma runs_to_partial_L2_fail_conv[simp]: "L2_fail ∙ s ?⦃ R ⦄ ⟷ True"
by (simp add: L2_fail_def)
lemma runs_to_partial_L2_fail[runs_to_vcg]: "L2_fail ∙ s ?⦃ R ⦄"
by simp
lemma runs_to_partial_L2_call[runs_to_vcg]:
assumes [runs_to_vcg]: "m ∙ s ?⦃ λr. Q (case r of Exn e ⇒ Exn (f e) | Result r ⇒ Result r) ⦄"
shows "(L2_call m f ns) ∙ s ?⦃ Q ⦄"
unfolding L2_call_def
apply runs_to_vcg
apply (simp add: map_exn_def)
done
end