Theory AutoCorres2.Stack_Typing

(*
 * Copyright (c) 2023 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

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 s0 s =
     hmem_upd (λh. override_on h (hmem s0) (A ∪ stack_free (htd s))) 
      (htd_upd (λd. override_on d (htd s0) (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‹s0›, 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‹s0›, this captures
  that we do not depend on the original typing in term‹s› for those addresses.

By taking the same reference state term‹s0› 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 s0 s› and term‹frame A s0 s'›.
›

definition raw_frame:: "addr set ⇒ 's ⇒ 's ⇒ 's" where
  "raw_frame A s0 s =
     hmem_upd (λh. override_on h (hmem s0) A) 
      (htd_upd (λd. override_on d (htd s0) 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 s0 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 s0 s) = hmem s0"
  unfolding frame_def
  by simp


lemma hmem_frame: "hmem (frame A s0 s) = (λa. if a ∈ A ∪ stack_free (htd s) then hmem s0 a else hmem s a)"
  unfolding frame_def
  by (auto simp add: fun_eq_iff)

lemma htd_frame: "htd (frame A s0 s) = (λa. if a ∈ (A - stack_free (htd s)) then htd s0 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 s0 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 s0) ∩ A = {} ⟹ stack_free (htd (frame A s0 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 s0 s)) (hmem s0)"
  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 s0 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 s0 s)) (htd s0)"
  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 s0 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 s0 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 s0 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 s0 (hmem_upd (heap_update p v) s) = frame A s0 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 s0 (hmem_upd (heap_update p v) s) = hmem_upd (heap_update p v) (frame A s0 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 s0 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 s0 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 s0 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 s0 (hmem_upd (heap_update_padding p v bs) s) = frame A s0 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)) t0)
     (htd_upd (λ_. ptr_force_type p (htd s)) s) = frame A t0 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 t0) stack_byte_typing (ptr_span p)) (ptr_span p ∪ A - stack_free (ptr_force_type p (htd s))) = override_on (htd s) (htd t0) (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)) t0) s =
          frame A t0 (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 t0) stack_byte_typing (ptr_span p)) (ptr_span p ∪ A - stack_free (htd s)) = 
            override_on (stack_releases (Suc 0) p (htd s)) (htd t0) (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 t0) (A ∪ stack_free (stack_releases (Suc 0) p (htd s)))  
         = 
        override_on (hmem s) (hmem t0) (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 t0) (size_of TYPE('a)) (ptr_val p))) 
              ( htd_upd (stack_releases (Suc 0) p) (frame A t0 s)) =
          frame A t0 
             (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 t0) (A - stack_free (htd s))) = 
            override_on (stack_releases (Suc 0) p (htd s)) (htd t0) (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 t0) (size_of TYPE('a)) (ptr_val p))
              (override_on (hmem s) (hmem t0) (A ∪ stack_free (htd s))) =
           override_on (heap_update_list (ptr_val p) bs (hmem s)) (hmem t0) 
              (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