Theory HeapLift

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)


theory HeapLift
  imports
  In_Out_Parameters
  Split_Heap
  AbstractArrays
begin

section "Refinement Lemmas"

lemma ucast_ucast_id:
  "LENGTH('a) ≤ LENGTH('b) ⟹ ucast (ucast (x::'a::len word)::'b::len word) = x"
  by (auto intro: ucast_up_ucast_id simp: is_up_def source_size_def target_size_def word_size)

lemma lense_ucast_signed:
  "lense (unsigned :: 'a::len word ⇒ 'a signed word) (λv x. unsigned (v (unsigned x)))"
  by (rule lenseI_equiv) (simp_all add: ucast_ucast_id)

lemma pointer_lense_ucast_signed:
  fixes r :: "'h ⇒ 'a::len8 word ptr ⇒ 'a word"
  assumes "pointer_lense r w"
  shows "pointer_lense
    (λh p. UCAST('a → 'a signed) (r h (PTR_COERCE('a signed word → 'a word) p)))
    (λp m. w (PTR_COERCE('a signed word → 'a word) p)
      (λw. UCAST('a signed → 'a) (m (UCAST('a → 'a signed) w))))"
proof -
  interpret pointer_lense r w by fact
  note scast_ucast_norm[simp del]
  note ucast_ucast_id[simp]
  show ?thesis
    apply unfold_locales
    apply (simp add: read_write_same)
    apply (simp add: write_same)
    apply (simp add: comp_def)
    apply (simp add: write_other_commute typ_uinfo_t_signed_word_word_conv
                flip: size_of_tag typ_uinfo_size)
    done
qed

lemma (in xmem_type) length_to_bytes:
  "length (to_bytes (v::'a) bs) = size_of TYPE('a)"
  by (simp add: to_bytes_def lense.access_result_size)

lemma (in xmem_type) heap_update_padding_eq:
  "length bs = size_of TYPE('a) ⟹
    heap_update_padding p v bs h = heap_update p v (heap_update_list (ptr_val p) bs h)"
  using u.max_size
  by (simp add: heap_update_padding_def heap_update_def size_of_def
      heap_list_heap_update_list_id heap_update_list_overwrite)

lemma (in xmem_type) heap_update_padding_eq':
  "length bs = size_of TYPE('a) ⟹
    heap_update_padding p v bs = heap_update p v ∘ heap_update_list (ptr_val p) bs"
  by (simp add: fun_eq_iff heap_update_padding_eq)

lemma split_disj_asm: "P (x ∨ y) = (¬ (x ∧ ¬ P x ∨ ¬ x ∧ ¬ P y))"
  by (smt (verit, best))

lemma comp_commute_of_fold:
  assumes x: "x = fold f xs"
  assumes xs: "list_all (λx. f x o a = a o f x) xs"
  shows "x o a = a o x"
  unfolding x using xs by (induction xs) (simp_all add: fun_eq_iff)

definition padding_closed_under_all_fields where
  "padding_closed_under_all_fields t ⟷
    (∀s f n bs bs'. field_lookup t f 0 = Some (s, n) ⟶
      eq_upto_padding t bs bs' ⟶ eq_upto_padding s (take (size_td s) (drop n bs)) (take (size_td s) (drop n bs')))"

lemma padding_closed_under_all_fields_typ_uinfo_t:
  "padding_closed_under_all_fields (typ_uinfo_t TYPE('a::xmem_type))"
  unfolding padding_closed_under_all_fields_def
proof safe
  fix s f n bs bs' assume s_n: "field_lookup (typ_uinfo_t TYPE('a)) f 0 = Some (s, n)"
    and bs_bs': "eq_upto_padding (typ_uinfo_t TYPE('a)) bs bs'"
  then have len: "length bs = size_of TYPE('a)" "length bs' = size_of TYPE('a) "
    by (auto simp: eq_upto_padding_def size_of_def)

  from s_n[THEN field_lookup_uinfo_Some_rev] obtain k where
    k: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (k, n)" and k_s: "export_uinfo k = s"
    by auto
  have [simp]: "size_td k = size_td s" by (simp flip: k_s)
  from xmem_type_field_lookup_eq_upto_padding_focus[OF k len bs_bs']
  show "eq_upto_padding s (take (size_td s) (drop n bs)) (take (size_td s) (drop n bs'))"
    unfolding k_s by simp
qed

lemma (in open_types) plift_heap_update_list_eq_upto_padding:
  assumes t: "mem_type_u t" and t': "padding_closed_under_all_fields t"
  assumes a: "ptr_valid_u t (hrs_htd h) a"
  assumes bs_bs': "eq_upto_padding t bs bs'"
  shows "plift (hrs_mem_update (heap_update_list a bs) h) =
    (plift (hrs_mem_update (heap_update_list a bs') h)::'a::xmem_type ptr ⇒ 'a option)"
  apply (rule plift_eq_plift, simp_all add: h_val_def hrs_mem_update)
proof -
  from bs_bs' have [simp]: "length bs = size_td t" "length bs' = size_td t"
    by (simp_all add: eq_upto_padding_def)
  have [arith]: "size_td t < addr_card"
    using mem_type_u.max_size[OF t] by simp
  have a_bnd: "size_of TYPE('a) ≤ addr_card"
    using max_size[where 'a='a] by arith
  let ?A = "typ_uinfo_t TYPE('a)"

  fix p :: "'a ptr" assume p: "ptr_valid (hrs_htd h) p"
  from ptr_valid_u_cases_weak[OF t a this[unfolded ptr_valid_def]]
  show "from_bytes (heap_list (heap_update_list a bs (hrs_mem h)) (size_of TYPE('a)) (ptr_val p)) =
    (from_bytes (heap_list (heap_update_list a bs' (hrs_mem h)) (size_of TYPE('a)) (ptr_val p))::'a)"
  proof (elim disjE exE conjE)
    assume "disjnt {a..+size_td t} {ptr_val p..+size_td (typ_uinfo_t TYPE('a))}"
    with bs_bs' show ?thesis
      unfolding heap_upd_list_def
      by (subst (1 2) heap_list_update_disjoint_same; simp add: size_of_def disjnt_def)
  next
    fix path assume path: "addressable_field t path ?A" and
      p_eq: "ptr_val p = a + word_of_nat (field_offset_untyped t path)"
    let ?n = "field_offset_untyped t path"
    have sz: "size_of TYPE('a) + ?n ≤ size_td t"
      using field_lookup_offset_size'[OF addressable_fieldD_field_lookup'[OF path]]
      by (simp add: size_of_def)
    let ?s = "typ_uinfo_t TYPE('a)"
    from addressable_fieldD_field_lookup'[OF path] t' bs_bs' have *:
      "eq_upto_padding ?s (take (size_td ?s) (drop ?n bs)) (take (size_td ?s) (drop ?n bs'))"
      unfolding padding_closed_under_all_fields_def
      by (auto simp flip: typ_uinfo_size)

    show ?thesis unfolding p_eq
      using eq_upto_padding_from_bytes_eq[OF *] sz
      apply (subst (1 2) heap_list_update_list)
      apply (simp_all add: size_of_def)
      done
  next
    fix path assume path: "addressable_field ?A path t"
      and p_eq: "a = ptr_val p + word_of_nat (field_offset_untyped ?A path)"
    let ?n = "field_offset_untyped ?A path"
    have sz: "size_td t + ?n ≤ size_of TYPE('a)"
      using field_lookup_offset_size'[OF addressable_fieldD_field_lookup'[OF path]]
      by (simp add: size_of_def)
    from field_lookup_uinfo_Some_rev[OF addressable_fieldD_field_lookup'[OF path]] obtain k
      where k: "field_lookup (typ_info_t TYPE('a)) path 0 = Some (k, ?n)"
        and eq_t: "export_uinfo k = t" by blast
    then have [simp]: "size_td k = size_td t"
      by (simp flip: eq_t)

    have *: "eq_upto_padding (typ_uinfo_t TYPE('a))
      (super_update_bs bs (heap_list (hrs_mem h) (size_of TYPE('a)) (ptr_val p)) ?n)
      (super_update_bs bs' (heap_list (hrs_mem h) (size_of TYPE('a)) (ptr_val p)) ?n)"
      by (subst xmem_type_field_lookup_eq_upto_padding_super_update_bs[OF k(1)])
         (simp_all add: eq_t bs_bs')

    note 1 = c_guard_no_wrap'[OF ptr_valid_c_guard, OF p]
    show ?thesis unfolding p_eq using sz
      apply (subst (1 2) heap_update_list_super_update_bs_heap_list[OF 1])
      apply (simp_all add: heap_list_heap_update_list_id[OF a_bnd])
      apply (intro eq_upto_padding_from_bytes_eq[OF *])
      done
  qed
qed

lemma (in open_types) read_dedicated_heap_heap_update_list_eq_upto_padding[simp]:
  assumes t: "mem_type_u t" and t': "padding_closed_under_all_fields t"
  assumes a: "ptr_valid_u t (hrs_htd h) a"
  assumes bs_bs': "eq_upto_padding t bs bs'"
  shows "read_dedicated_heap (hrs_mem_update (heap_update_list a bs) h) =
    (read_dedicated_heap (hrs_mem_update (heap_update_list a bs') h)::'a::xmem_type ptr ⇒ 'a) ⟷ True"
  by (simp add: plift_heap_update_list_eq_upto_padding[OF assms] read_dedicated_heap_def fun_eq_iff)

definition "L2Tcorres st A C = corresXF st (λr _. r) (λr _. r) (λ_. True) A C"

lemma L2Tcorres_id:
  "L2Tcorres id C C"
  by (metis L2Tcorres_def corresXF_id)

lemma L2Tcorres_fail:
  "L2Tcorres st L2_fail X"
  apply (clarsimp simp: L2Tcorres_def L2_defs)
  apply (rule corresXF_fail)
  done

lemma admissible_nondet_ord_L2Tcorres [corres_admissible]:
  "ccpo.admissible Inf (≥) (λA. L2Tcorres st A C)"
  unfolding L2Tcorres_def
  apply (rule admissible_nondet_ord_corresXF)
  done

lemma L2Tcorres_top [corres_top]: "L2Tcorres st ⊤ C"
  by (auto simp add: L2Tcorres_def corresXF_def)

(* Abstraction predicates for inner expressions. *)
definition "abs_guard    st   A C ≡ ∀s. A (st s) ⟶ C s"
definition "abs_expr     st P A C ≡ ∀s. P (st s) ⟶ C s = A (st s)"
definition "abs_modifies st P A C ≡ ∀s. P (st s) ⟶ st (C s) = A (st s)"

(* Predicates to enable some transformations on the input expressions
   (namely, rewriting uses of field_lvalue) that are best done
   as a preprocessing stage (st = id).
   The corresTA rules should ensure that these are used to rewrite
   any inner expressions before handing off to the predicates above. *)
definition "struct_rewrite_guard      A C ≡ ∀s. A s ⟶ C s"
definition "struct_rewrite_expr     P A C ≡ ∀s. P s ⟶ C s = A s"
definition "struct_rewrite_modifies P A C ≡ ∀s. P s ⟶ C s = A s"


(* Standard heap abstraction rules. *)
named_theorems heap_abs
(* Rules that require first-order matching. *)
named_theorems heap_abs_fo

named_theorems derived_heap_defs and
 valid_array_defs and
 heap_upd_cong and
 valid_same_typ_descs

lemma deepen_heap_upd_cong: "f = f' ⟹ upd f s = upd f' s"
  by simp

lemma deepen_heap_map_cong: "f = f' ⟹ upd f p s = upd f' p s"
  by simp


(* fun_app2 is like fun_app, but it skips an abstraction.
 * We use this for terms like "λs a. Array.update a k (f s)".
 * fixme: ideally, the first order conversion code can skip abstractions. *)

lemma abs_expr_fun_app2 [heap_abs_fo]:
  "⟦ abs_expr st P f f';
     abs_expr st Q g g' ⟧ ⟹
   abs_expr st (λs. P s ∧ Q s) (λs a. f s a (g s a)) (λs a. f' s a $ g' s a)"
  by (simp add: abs_expr_def)

lemma abs_expr_fun_app [heap_abs_fo]:
  "⟦ abs_expr st Y x x'; abs_expr st X f f' ⟧ ⟹
      abs_expr st (λs. X s ∧ Y s) (λs. f s (x s)) (λs. f' s $ x' s)"
  apply (clarsimp simp: abs_expr_def)
  done

lemma abs_expr_Pair [heap_abs]: "
abs_expr st X f1 f1' ⟹ abs_expr st Y f2 f2' ⟹
abs_expr st  (λs. X s ∧ Y s)  (λs. (f1 s, f2 s)) (λs. (f1' s, f2' s))"
  apply (clarsimp simp: abs_expr_def)
  done

lemma abs_expr_constant [heap_abs]:
  "abs_expr st (λ_. True) (λs. a) (λs. a)"
  apply (clarsimp simp: abs_expr_def)
  done

lemma abs_guard_expr [heap_abs]:
  "abs_expr st P a' a ⟹ abs_guard st (λs. P s ∧ a' s) a"
  by (simp add: abs_expr_def abs_guard_def)

lemma abs_guard_constant [heap_abs]:
  "abs_guard st (λ_. P) (λ_. P)"
  by (clarsimp simp: abs_guard_def)

lemma abs_guard_conj [heap_abs]:
  "⟦ abs_guard st G G'; abs_guard st H H' ⟧
      ⟹ abs_guard st (λs. G s ∧ H s) (λs. G' s ∧ H' s)"
  by (clarsimp simp: abs_guard_def)


lemma L2Tcorres_modify [heap_abs]:
    "⟦ struct_rewrite_modifies P b c; abs_guard st P' P;
       abs_modifies st Q a b ⟧ ⟹
     L2Tcorres st (L2_seq (L2_guard (λs. P' s ∧ Q s)) (λ_. (L2_modify a))) (L2_modify c)"
  apply (auto intro!: refines_bind_guard_right refines_modify  
      simp: corresXF_refines_conv 
      L2Tcorres_def L2_defs abs_modifies_def abs_guard_def struct_rewrite_modifies_def struct_rewrite_guard_def)
  done

lemma L2Tcorres_gets [heap_abs]:
    "⟦ struct_rewrite_expr P b c; abs_guard st P' P;
       abs_expr st Q a b ⟧ ⟹
     L2Tcorres st (L2_seq (L2_guard (λs. P' s ∧ Q s)) (λ_. L2_gets a n)) (L2_gets c n)"
  apply (auto intro!: refines_bind_guard_right refines_gets   
      simp: corresXF_refines_conv L2Tcorres_def L2_defs abs_expr_def abs_guard_def struct_rewrite_expr_def struct_rewrite_guard_def)
  done

lemma L2Tcorres_gets_const [heap_abs]:
    "L2Tcorres st (L2_gets (λ_. a) n) (L2_gets (λ_. a) n)"
  apply (simp add: corresXF_refines_conv refines_gets L2Tcorres_def L2_defs)
  done

lemma L2Tcorres_guard [heap_abs]:
    "⟦ struct_rewrite_guard b c; abs_guard st a b ⟧ ⟹
     L2Tcorres st (L2_guard a) (L2_guard c)"
  apply (simp add: corresXF_def L2Tcorres_def L2_defs abs_guard_def struct_rewrite_guard_def)
  done

lemma L2Tcorres_while [heap_abs]:
  assumes body_corres [simplified THIN_def,rule_format]:
    "PROP THIN (⋀x. L2Tcorres st (B' x) (B x))"
  and cond_rewrite [simplified THIN_def,rule_format]:
    "PROP THIN (⋀r. struct_rewrite_expr (G r) (C' r) (C r))"
  and guard_abs[simplified THIN_def,rule_format]:
    "PROP THIN (⋀r. abs_guard st (G' r) (G r))"
  and guard_impl_cond[simplified THIN_def,rule_format]:
    "PROP THIN (⋀r. abs_expr st (H r) (C'' r) (C' r))"
  shows "L2Tcorres st (L2_guarded_while (λi s. G' i s ∧ H i s) C'' B' i n) (L2_while C B i n)"
proof -

  have cond_match: "⋀r s. G' r (st s) ∧ H r (st s) ⟹ C'' r (st s) = C r s"
    using cond_rewrite guard_abs guard_impl_cond
    by (clarsimp simp: abs_expr_def abs_guard_def struct_rewrite_expr_def)

  have "corresXF st (λr _. r) (λr _. r) (λ_. True)
           (do { _ ← guard (λs. G' i s ∧ H i s);
                     whileLoop C''
                       (λi. do { r ← B' i;
                                _ ← guard (λs. G' r s ∧ H r s);
                                return r
                       }) i
           })
     (whileLoop C B i)"
    apply (rule corresXF_guard_imp)
     apply (rule corresXF_guarded_while [where P="λ_ _. True" and P'="λ_ _. True"])
         apply (clarsimp cong: corresXF_cong)
         apply (rule corresXF_guard_imp)
          apply (rule body_corres [unfolded L2Tcorres_def])
         apply simp
        apply (clarsimp simp: cond_match)
       apply clarsimp
       apply (simp add: runs_to_partial_def_old split: xval_splits)
      apply simp
     apply simp
    apply simp
    done

  thus ?thesis
    by (clarsimp simp: L2Tcorres_def L2_defs gets_return top_fun_def)
qed


named_theorems abs_spec

definition "abs_spec st P (A :: ('a × 'a) set) (C :: ('c × 'c) set)
           ≡ (∀s t. P (st s) ⟶ (((s, t) ∈ C) ⟶ ((st s, st t) ∈ A)))
                              ∧ (∀s. P (st s) ⟶ (∃x. (st s, x) ∈ A) ⟶ (∃x. (s, x) ∈ C))"

lemma L2Tcorres_spec [heap_abs]:
  "⟦ abs_spec st P A C ⟧
     ⟹ L2Tcorres st (L2_seq (L2_guard P) (λ_. (L2_spec A))) (L2_spec C)"
  unfolding corresXF_refines_conv L2Tcorres_def L2_defs
  apply (clarsimp simp add: abs_spec_def)
  apply (intro refines_bind_guard_right refines_bind_bind_exn_wp refines_state_select)
   apply (force intro!: refines_select simp add: abs_spec_def split: xval_splits)
  apply blast
  done


definition "abs_assume st P (A :: 'a ⇒ ('b × 'a) set) (C :: 'c ⇒ ('b × 'c) set)
  ≡ (∀s t r. P (st s) ⟶ (((r, t) ∈ C s) ⟶ ((r, st t) ∈ A (st s))))"

(* FIXME: replace refines_assume_result_and_state in spec monad *)
lemma refines_assume_result_and_state': 
  "refines (assume_result_and_state P) (assume_result_and_state Q) s t R"
  if "sim_set (λ(v, s) (w, t). R (Result v, s) (Result w, t))  (P s) (Q t)"
  using that
  by (force simp: refines_def_old  sim_set_def rel_set_def  case_prod_unfold)


lemma L2Tcorres_assume [heap_abs]:
  "⟦ abs_assume st P A C ⟧
     ⟹ L2Tcorres st (L2_seq (L2_guard P) (λ_. (L2_assume A))) (L2_assume C)"
  unfolding corresXF_refines_conv L2Tcorres_def L2_defs
  apply (clarsimp simp add: abs_assume_def) thm  refines_mono [OF _ refines_assume_result_and_state]
  apply (intro refines_bind_guard_right refines_bind_bind_exn_wp refines_assume_result_and_state' )
  apply (auto simp add: sim_set_def)
  done

lemma abs_spec_constant [heap_abs]:
  "abs_spec st (λ_. True) {(a, b). C} {(a, b). C}"
  apply (clarsimp simp: abs_spec_def)
  done

lemma L2Tcorres_condition [heap_abs]:
  "⟦PROP THIN (Trueprop (L2Tcorres st L L'));
    PROP THIN (Trueprop (L2Tcorres st R R'));
    PROP THIN (Trueprop (struct_rewrite_expr P C' C));
    PROP THIN (Trueprop (abs_guard st P' P));
    PROP THIN (Trueprop (abs_expr st Q C'' C'))⟧ ⟹
   L2Tcorres st (L2_seq (L2_guard (λs. P' s ∧ Q s)) (λ_. L2_condition C'' L R)) (L2_condition C L' R')"
  unfolding THIN_def L2_defs L2Tcorres_def corresXF_refines_conv
  apply clarsimp
  apply (intro refines_bind_guard_right refines_condition)
  apply (auto simp add: abs_expr_def abs_guard_def struct_rewrite_expr_def struct_rewrite_guard_def)
  done

lemma L2Tcorres_seq [heap_abs]:
  "⟦PROP THIN (Trueprop (L2Tcorres st L' L)); PROP THIN (⋀r. L2Tcorres st (R' r) (R r)) ⟧
      ⟹ L2Tcorres st (L2_seq L' R') (L2_seq L R)"
  unfolding THIN_def L2_defs L2Tcorres_def corresXF_refines_conv
  apply clarsimp
  apply (intro refines_bind_bind_exn_wp)
  subgoal for t
    apply (erule_tac x=t in allE)
    apply (rule refines_weaken)
     apply assumption
    apply (auto split: xval_splits)
    done
  done


lemma L2Tcorres_guarded_simple [heap_abs]:
  assumes b_c: "struct_rewrite_guard b c"
  assumes a_b: "abs_guard st a b"
  assumes f_g: "⋀s s'. c s ⟹ s' = st s ⟹ L2Tcorres st f g"
  shows "L2Tcorres st (L2_guarded a f) (L2_guarded c g)"
  unfolding L2_guarded_def L2_defs L2Tcorres_def corresXF_refines_conv
  using b_c a_b f_g
  by (fastforce simp add: refines_def_old L2Tcorres_def corresXF_refines_conv reaches_bind succeeds_bind 
      struct_rewrite_guard_def abs_guard_def abs_expr_def split: xval_splits)

lemma L2Tcorres_catch [heap_abs]:
    "⟦PROP THIN (Trueprop (L2Tcorres st L L'));
      PROP THIN (⋀r. L2Tcorres st (R r) (R' r))
     ⟧ ⟹ L2Tcorres st (L2_catch L R) (L2_catch L' R')"
  unfolding THIN_def
  apply (clarsimp simp: L2Tcorres_def L2_defs)
  apply (rule corresXF_guard_imp)
   apply (erule corresXF_except [where P'="λx y s. x = y" and Q="λ_. True"])
     apply (simp add: corresXF_refines_conv)
    apply (simp add: runs_to_partial_def_old split: xval_splits)
   apply simp
  apply simp
  done

lemma corresXF_return_same:
  "corresXF st (λr _. r) (λr _. r) (λ_. True) (return e) (return e)"
  by (clarsimp simp add: corresXF_def)

lemma corresXF_yield_same:
  "corresXF st (λr _. r) (λr _. r) (λ_. True) (yield e) (yield e)"
 by (auto simp add: corresXF_refines_conv intro!: refines_yield split: xval_splits)

lemma L2_try_catch: "L2_try L = L2_catch L (λe. yield (to_xval e))"
  unfolding L2_defs
  apply (rule spec_monad_eqI)
  apply (clarsimp simp add: runs_to_iff)
  apply (auto simp add: runs_to_def_old unnest_exn_def to_xval_def split: xval_splits sum.splits )
  done

lemma L2Tcorres_try [heap_abs]:
    "⟦ L2Tcorres st L L'⟧ ⟹ L2Tcorres st (L2_try L) (L2_try L')"
  apply (simp add: L2_try_catch)
  apply (erule L2Tcorres_catch [simplified THIN_def])
  apply (unfold L2Tcorres_def top_fun_def top_bool_def)
  apply (rule corresXF_yield_same)
  done

lemma L2Tcorres_unknown [heap_abs]:
  "L2Tcorres st (L2_unknown ns) (L2_unknown ns)"
  apply (clarsimp simp: L2_unknown_def)
  apply (clarsimp simp: L2Tcorres_def)
  apply (auto intro!: corresXF_select_select)
  done

lemma L2Tcorres_throw [heap_abs]:
  "L2Tcorres st (L2_throw x n) (L2_throw x n)"
  apply (clarsimp simp: L2Tcorres_def L2_defs)
  apply (rule corresXF_throw)
  apply simp
  done

lemma L2Tcorres_split [heap_abs]:
  "⟦ ⋀x y. L2Tcorres st (P x y) (P' x y) ⟧ ⟹
    L2Tcorres st (case a of (x, y) ⇒ P x y) (case a of (x, y) ⇒ P' x y)"
  apply (clarsimp simp: split_def)
  done

lemma L2Tcorres_seq_unused_result [heap_abs]:
  "⟦PROP THIN (Trueprop (L2Tcorres st L L')); PROP THIN (Trueprop (L2Tcorres st R R')) ⟧
  ⟹ L2Tcorres st (L2_seq L (λ_. R)) (L2_seq L' (λ_. R'))"
  apply (rule L2Tcorres_seq, auto)
  done

lemma abs_expr_split [heap_abs]:
  "⟦ ⋀a b. abs_expr st (P a b) (A a b) (C a b) ⟧
       ⟹ abs_expr st (case r of (a, b) ⇒ P a b)
            (case r of (a, b) ⇒ A a b) (case r of (a, b) ⇒ C a b)"
  apply (auto simp: split_def)
  done

lemma abs_guard_split [heap_abs]:
  "⟦ ⋀a b. abs_guard st (A a b) (C a b) ⟧
       ⟹ abs_guard st (case r of (a, b) ⇒ A a b) (case r of (a, b) ⇒ C a b)"
  apply (auto simp: split_def)
  done

lemma L2Tcorres_abstract_fail [heap_abs]:
  "L2Tcorres st L2_fail L2_fail"
  apply (clarsimp simp: L2Tcorres_def L2_defs)
  apply (rule corresXF_fail)
  done

lemma abs_expr_id [heap_abs]:
  "abs_expr id (λ_. True) A A"
  apply (clarsimp simp: abs_expr_def)
  done

lemma abs_expr_lambda_null [heap_abs]:
  "abs_expr st P A C ⟹ abs_expr st P (λs r. A s) (λs r. C s)"
  apply (clarsimp simp: abs_expr_def)
  done

lemma abs_modify_id [heap_abs]:
  "abs_modifies id (λ_. True) A A"
  apply (clarsimp simp: abs_modifies_def)
  done

lemma corresXF_exec_concrete [intro?]:
  "corresXF id ret_xf ex_xf P A C ⟹ corresXF st ret_xf ex_xf P (exec_concrete st A) C"
  by (force simp add: corresXF_refines_conv refines_def_old reaches_exec_concrete succeeds_exec_concrete_iff split: xval_splits)

lemma L2Tcorres_exec_concrete [heap_abs]:
  "L2Tcorres id A C ⟹ L2Tcorres st (exec_concrete st (L2_call A emb ns)) (L2_call C emb ns)"
  apply (clarsimp simp: L2Tcorres_def L2_call_def map_exn_catch_conv)
  apply (rule corresXF_exec_concrete)
  apply (rule CorresXF.corresXF_except  [ where P' = "λx y s. x = y"])
     apply assumption
  subgoal 
    by (auto simp add: corresXF_refines_conv)
  subgoal
    by (auto simp add: runs_to_partial_def_old split: xval_splits)
  subgoal by simp
  done

lemma L2Tcorres_exec_concrete_simpl [heap_abs]:
  "L2Tcorres id A C ⟹ L2Tcorres st (exec_concrete st (L2_call_L1 arg_xf gs ret_xf A)) (L2_call_L1 arg_xf gs ret_xf C)"
  apply (clarsimp simp: L2Tcorres_def L2_call_L1_def)
  apply (rule corresXF_exec_concrete)
  apply (clarsimp simp add: corresXF_refines_conv)
  apply (rule refines_bind_bind_exn_wp)
  apply (clarsimp split: xval_splits)
  apply (rule refines_get_state)
  apply (clarsimp split: xval_splits)
  apply (rule refines_bind_bind_exn_wp)
  apply (clarsimp split: xval_splits)
  apply (rule refines_select)
  apply (clarsimp split: xval_splits)
  subgoal for x
    apply (rule exI[where x=x])
    apply (erule_tac x=x in allE)
    apply (clarsimp)
    apply (rule refines_run_bind)
    apply (clarsimp split: exception_or_result_splits)
    apply (erule refines_weaken)
    apply (clarsimp split: xval_splits)
    apply (rule refines_bind_bind_exn_wp)
    apply (clarsimp split: xval_splits)
    apply (rule refines_set_state)
    apply (clarsimp split: xval_splits)
    done
  done

lemma corresXF_exec_abstract [intro?]:
  "corresXF st ret_xf ex_xf P A C ⟹ corresXF id ret_xf ex_xf P (exec_abstract st A) C"
  by (force simp: corresXF_refines_conv refines_def_old reaches_exec_abstract split: xval_splits)

lemma L2Tcorres_exec_abstract [heap_abs]:
    "L2Tcorres st A C ⟹ L2Tcorres id (exec_abstract st (L2_call A emb ns)) (L2_call C emb ns)"
  apply (clarsimp simp: L2_call_def map_exn_catch_conv L2Tcorres_def)
  apply (rule corresXF_exec_abstract)
  apply (rule CorresXF.corresXF_except  [ where P' = "λx y s. x = y"])
     apply assumption
    subgoal by (auto simp add: corresXF_refines_conv)
    subgoal by (auto simp add: runs_to_partial_def_old split: xval_splits)
    subgoal by simp  
    done

lemma L2Tcorres_call [heap_abs]:
  "L2Tcorres st A C ⟹ L2Tcorres st (L2_call A emb ns) (L2_call C emb ns)"
  unfolding L2Tcorres_def L2_call_def map_exn_catch_conv
  apply (rule CorresXF.corresXF_except  [ where P' = "λx y s. x = y"])
    apply assumption
    subgoal by (auto simp add: corresXF_refines_conv)
    subgoal by (auto simp add: runs_to_partial_def_old split: xval_splits)
    subgoal by simp  
    done


named_theorems
valid_implies_c_guard and
read_commutes and
write_commutes  and
field_write_commutes and
write_valid_preservation and
lift_heap_update_padding_heap_update_conv

(*
 * Assert the given abstracted heap (accessed using "getter" and "setter") for type
 * "'a" is a valid abstraction w.r.t. the given state translation functions.
 *)



locale valid_implies_cguard =
  fixes st::"'s ⇒ 't"
  fixes v::"'t ⇒ 'a::c_type ptr ⇒ bool"
  assumes valid_implies_c_guard[valid_implies_c_guard]: "v (st s) p ⟹ c_guard p"

locale read_simulation =
  fixes st ::"'s ⇒ 't"
  fixes v ::"'t ⇒ 'a::c_type ptr ⇒ bool"
  fixes r :: "'t ⇒ 'a ptr ⇒ 'a"
  fixes t_hrs::"'s ⇒ heap_raw_state"
  assumes read_commutes[read_commutes]: "v (st s) p ⟹
              r (st s) p = h_val (hrs_mem (t_hrs s)) p"

locale write_simulation =
  heap_raw_state t_hrs t_hrs_upd
  for
    t_hrs :: "('s ⇒ heap_raw_state)" and
    t_hrs_upd::"(heap_raw_state ⇒ heap_raw_state) ⇒ 's ⇒ 's" +
  fixes st ::"'s ⇒ 't"
  fixes v ::"'t ⇒ 'a::mem_type ptr ⇒ bool"
  fixes w :: "'a ptr ⇒ ('a ⇒ 'a)  ⇒ 't ⇒ 't"

  assumes write_padding_commutes[write_commutes]: "v (st s) p ⟹ length bs = size_of TYPE('a) ⟹
           st (t_hrs_upd (hrs_mem_update (heap_update_padding p x bs)) s) =
                           w p (λ_. x)  (st s)"

begin
lemma write_commutes[write_commutes]:
  assumes valid: "v (st s) p"
  shows "st (t_hrs_upd (hrs_mem_update (heap_update p x)) s) =
                           w p (λ_. x) (st s)"
proof -
  have eq: "hrs_mem_update (heap_update p x) =
        hrs_mem_update (λh. heap_update_padding p x (heap_list h (size_of TYPE('a)) (ptr_val p)) h)"
    using heap_update_heap_update_padding_conv
    by metis

  show ?thesis
    apply (simp only: eq)
    apply (subst write_padding_commutes [symmetric,  where bs="heap_list (hrs_mem (t_hrs s)) (size_of TYPE('a)) (ptr_val p)"])
      apply (rule valid)
     apply clarsimp
    by (metis (no_types, lifting) heap.upd_cong)
qed

lemma lift_heap_update_padding_heap_update_conv[lift_heap_update_padding_heap_update_conv]:
  "v (st s) p ⟹ length bs = size_of TYPE('a) ⟹
           st (t_hrs_upd (hrs_mem_update (heap_update_padding p x bs)) s) =
           st (t_hrs_upd (hrs_mem_update (heap_update p x)) s)"
  using write_padding_commutes write_commutes by auto

lemma write_commutes_atomic: "∀s p x. v (st s) p ⟶
   st (t_hrs_upd (hrs_mem_update (heap_update p x)) s) =
                           w p (λ_. x) (st s)"
  using  write_commutes by blast

end


locale write_preserves_valid =
  fixes v ::"'t ⇒ 'a::c_type ptr ⇒ bool"
  fixes w :: "'a ptr ⇒ ('b ⇒ 'b) ⇒ 't ⇒ 't"
  assumes valid_preserved: "v (w p' f s) p = v s p"
begin
lemma valid_preserved_pointless[simp]: "v (w p' f s)  = v s"
  by (rule ext) (rule valid_preserved)
end


locale valid_only_typ_desc_dependent =
  fixes t_hrs :: "('s ⇒ heap_raw_state)"
  fixes st ::"'s ⇒ 't"
  fixes v ::"'t ⇒ 'a::c_type ptr ⇒ bool"
  assumes valid_same_typ_desc [valid_same_typ_descs]: "hrs_htd (t_hrs s) = hrs_htd (t_hrs t) ⟹ v (st s) p = v (st t) p"

locale heap_typing_simulation =
  open_types 𝒯 + t_hrs: heap_raw_state t_hrs t_hrs_upd + heap_typing_state heap_typing heap_typing_upd
  for
    𝒯 and
    t_hrs :: "('s ⇒ heap_raw_state)" and
    t_hrs_upd :: "(heap_raw_state ⇒ heap_raw_state) ⇒ ('s ⇒ 's)" and
    heap_typing :: "'t ⇒ heap_typ_desc" and
    heap_typing_upd :: "(heap_typ_desc ⇒ heap_typ_desc) ⇒ 't ⇒ 't" +
  fixes st ::"'s ⇒ 't"
  assumes heap_typing_commutes[simp]: "heap_typing (st s) = hrs_htd (t_hrs s)"
  assumes lift_heap_update_list_stack_byte_independent:
    "(⋀i. i < length bs ⟹ root_ptr_valid (hrs_htd (t_hrs s)) ((p::stack_byte ptr) +⇩p int i)) ⟹
     st (t_hrs_upd (hrs_mem_update (heap_update_list (ptr_val p) bs)) s) = st s"
  assumes st_eq_upto_padding:
    "mem_type_u t ⟹ padding_closed_under_all_fields t ⟹
      ptr_valid_u t (hrs_htd (t_hrs s)) a ⟹ eq_upto_padding t bs bs' ⟹
      st (t_hrs_upd (hrs_mem_update (heap_update_list a bs)) s) =
      st (t_hrs_upd (hrs_mem_update (heap_update_list a bs')) s)"
begin

lemma heap_typing_upd_commutes: "heap_typing (heap_typing_upd f (st s)) = hrs_htd (t_hrs (t_hrs_upd (hrs_htd_update f) s))"
  apply (simp add: hrs_htd_update)
  done

lemma write_simulation_alt:
  assumes v: "⋀s p. v (st s) p ⟹ ptr_valid (hrs_htd (t_hrs s)) p"
  assumes *: "⋀s (p::'a::xmem_type ptr) x. v (st s) p ⟹
    st (t_hrs_upd (hrs_mem_update (heap_update p x)) s) = w p (λ_. x)  (st s)"
  shows "write_simulation t_hrs t_hrs_upd st v w"
proof
  fix s p x and bs :: "byte list" assume p: "v (st s) p" and bs: "length bs = size_of TYPE('a)"

  have [simp]: "t_hrs_upd (hrs_mem_update (heap_update p x)) s =
    t_hrs_upd (hrs_mem_update (heap_update_list (ptr_val p)
      (to_bytes x (heap_list (hrs_mem (t_hrs s)) (size_of TYPE('a)) (ptr_val p))))) s"
    by (rule t_hrs.heap.upd_cong) (simp add: heap_update_def)

  show "st (t_hrs_upd (hrs_mem_update (heap_update_padding p x bs)) s) = w p (λ_. x) (st s)"
    apply (subst *[OF p, symmetric])
    apply (simp add: heap_update_padding_def[abs_def])
    apply (rule st_eq_upto_padding[where t="typ_uinfo_t TYPE('a)"])
    apply (rule typ_uinfo_t_mem_type)
    apply (rule padding_closed_under_all_fields_typ_uinfo_t)
    apply (subst ptr_valid_def[symmetric])
    apply (simp add: v p)
    unfolding to_bytes_def typ_uinfo_t_def
    apply (rule field_lookup_access_ti_eq_upto_padding[where f="[]" and 'b='a])
    apply (simp_all add: bs size_of_def)
    done
qed

end

locale typ_heap_simulation =
  heap_raw_state t_hrs t_hrs_update +
  read_simulation st v r t_hrs +
  write_simulation t_hrs t_hrs_update st v w  +
  write_preserves_valid v w +
  valid_implies_cguard st v +
  valid_only_typ_desc_dependent t_hrs st v +
  pointer_lense r w
  for
    st:: "'s ⇒ 't" and
    r:: "'t ⇒ ('a::xmem_type) ptr ⇒ 'a" and
    w:: "'a ptr ⇒ ('a ⇒ 'a) ⇒ 't ⇒ 't" and
    v:: "'t ⇒ ('a::xmem_type) ptr ⇒ bool" and
    t_hrs :: "'s ⇒ heap_raw_state" and
    t_hrs_update:: "(heap_raw_state ⇒ heap_raw_state) ⇒ 's ⇒ 's"
begin

lemma write_valid_preservation [write_valid_preservation]:
  shows "v (st (t_hrs_update (hrs_mem_update (heap_update q x)) s)) p = v (st s) p"
  by (metis hrs_htd_mem_update get_upd valid_same_typ_desc)

lemma write_padding_valid_preservation [write_valid_preservation]:
  shows "v (st (t_hrs_update (hrs_mem_update (heap_update_padding q x bs)) s)) p = v (st s) p"
  by (metis hrs_htd_mem_update get_upd valid_same_typ_desc)

end



locale stack_simulation =
  heap_typing_simulation 𝒯 t_hrs t_hrs_update heap_typing heap_typing_upd st +
  typ_heap_typing r w heap_typing heap_typing_upd 𝒮
  for
    𝒯 and
    st:: "'s ⇒ 't" and
    r:: "'t ⇒ ('a::xmem_type) ptr ⇒ 'a" and
    w:: "'a ptr ⇒ ('a ⇒ 'a) ⇒ 't ⇒ 't" and
    t_hrs :: "'s ⇒ heap_raw_state" and
    t_hrs_update:: "(heap_raw_state ⇒ heap_raw_state) ⇒ 's ⇒ 's" and
    heap_typing :: "'t ⇒ heap_typ_desc" and
    heap_typing_upd :: "(heap_typ_desc ⇒ heap_typ_desc) ⇒ 't ⇒ 't" and
    𝒮:: "addr set" +
assumes sim_stack_alloc:
  "⋀p d vs bs s n.
    (p, d) ∈ stack_allocs n 𝒮 TYPE('a) (hrs_htd (t_hrs s)) ⟹ length vs = n ⟹ length bs = n * size_of TYPE ('a) ⟹
      st (t_hrs_update (hrs_mem_update (fold (λi. heap_update_padding (p +⇩p int i) (vs!i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<n]) ∘ hrs_htd_update (λ_. d)) s) =
      (fold (λi. w (p +⇩p int i) (λ_. (vs ! i))) [0..<n]) (heap_typing_upd (λ_. d) (st s))"

assumes sim_stack_release: "⋀p s n. (⋀i. i < n ⟹ root_ptr_valid (hrs_htd (t_hrs s)) (p +⇩p int i)) ⟹
  length bs = n * size_of TYPE('a) ⟹
 st (t_hrs_update (hrs_mem_update (heap_update_list (ptr_val p) bs) ∘ hrs_htd_update (stack_releases n p)) s) =
         ((heap_typing_upd (stack_releases n p) (fold (λi. w (p +⇩p int i) (λ_. c_type_class.zero)) [0..<n] (st s))))"

assumes stack_byte_zero: "⋀p d i. (p, d) ∈ stack_allocs n 𝒮 TYPE('a) (hrs_htd (t_hrs s)) ⟹ i < n ⟹ r (st s) (p +⇩p int i) = ZERO('a)"


lemma (in typ_heap_simulation) L2Tcorres_IO_modify_paddingE [heap_abs]:
  assumes "abs_expr st P a c"
  shows "L2Tcorres st (L2_seq (L2_guard (λt. v t p ∧ P t)) (λ_. (L2_modify (λs. w p (λ_. a s) s)))) 
    (IO_modify_heap_paddingE (p::'a ptr) c)"
  using assms
  using length_to_bytes write_padding_commutes unfolding liftE_IO_modify_heap_padding
  by (auto simp add: abs_expr_def L2Tcorres_def corresXF_refines_conv L2_defs 
      IO_modify_heap_padding_def refines_def_old reaches_bind succeeds_bind split: xval_splits)



locale typ_heap_typing_stack_simulation =
  typ_heap_simulation st r w v t_hrs t_hrs_update +
  stack_simulation 𝒯 st r w t_hrs t_hrs_update heap_typing heap_typing_upd 𝒮
  for
    𝒯 and
    st:: "'s ⇒ 't" and
    r:: "'t ⇒ ('a::xmem_type) ptr ⇒ 'a" and
    w:: "'a ptr ⇒ ('a ⇒ 'a) ⇒ 't ⇒ 't" and
    v:: "'t ⇒ ('a::xmem_type) ptr ⇒ bool" and
    t_hrs :: "'s ⇒ heap_raw_state" and
    t_hrs_update:: "(heap_raw_state ⇒ heap_raw_state) ⇒ 's ⇒ 's" and
    heap_typing :: "'t ⇒ heap_typ_desc" and
    heap_typing_upd :: "(heap_typ_desc ⇒ heap_typ_desc) ⇒ 't ⇒ 't" and
    𝒮:: "addr set"
begin

sublocale monolithic: stack_heap_raw_state t_hrs t_hrs_update 𝒮
  by (unfold_locales)

definition "rel_split_heap ≡ λs⇩c s⇩a. s⇩a = st s⇩c"

lemma rel_split_heap_stack_free_eq:
  "rel_split_heap s⇩c s⇩a  ⟹ stack_free (hrs_htd (t_hrs s⇩c)) = stack_free (heap_typing s⇩a)"
  by (simp only: rel_split_heap_def heap_typing_commutes)

definition rel_stack_free_eq where
  "rel_stack_free_eq s⇩c s⇩a  ≡ stack_free (hrs_htd (t_hrs s⇩c)) = stack_free (heap_typing s⇩a)"

lemma rel_prod_rel_split_heap_conv:
  "rel_prod (=) rel_split_heap = (λ(v, t) (r, s).
             s = st t ∧ (case v of Exn x ⇒ r = Exn x | Result x ⇒ r = Result x)) "
  by (auto simp add: rel_split_heap_def rel_prod_conv fun_eq_iff split: prod.splits xval_splits)

lemma L2Tcorres_refines:
  "L2Tcorres st f⇩a f⇩c ⟹ refines f⇩c f⇩a s (st s) (rel_prod (=) rel_split_heap)"
  by (simp add: L2Tcorres_def corresXF_refines_conv rel_prod_rel_split_heap_conv)

lemma refines_L2Tcorres:
  assumes f: "⋀s. refines f⇩c f⇩a s (st s) (rel_prod (=) rel_split_heap)"
  shows "L2Tcorres st f⇩a f⇩c"
  using f
  by (simp add: L2Tcorres_def corresXF_refines_conv rel_prod_rel_split_heap_conv)

lemma L2Tcorres_refines_conv:
"L2Tcorres st f⇩a f⇩c ⟷ (∀s. refines f⇩c f⇩a s (st s) (rel_prod (=) rel_split_heap))"
  by (auto simp add: L2Tcorres_refines refines_L2Tcorres)

lemma sim_guard_with_fresh_stack_ptr:
  fixes f⇩c:: "'a ptr ⇒ ('b, 'c, 's) exn_monad"
  assumes init: "init⇩a (st s) = init⇩c s"
  assumes f: "⋀s p::'a ptr. refines (f⇩c p) (f⇩a p) s (st s) (rel_prod (=) rel_split_heap)"
  shows "refines
           (monolithic.with_fresh_stack_ptr n init⇩c f⇩c)
           (guard_with_fresh_stack_ptr n init⇩a f⇩a) s (st s)
           (rel_prod (=) rel_split_heap)"
  unfolding monolithic.with_fresh_stack_ptr_def guard_with_fresh_stack_ptr_def
                   stack_ptr_acquire_def stack_ptr_release_def assume_stack_alloc_def
  apply (rule refines_bind_bind_exn [where Q= "(rel_prod (=) rel_split_heap)"])
  subgoal
    apply (rule refines_assume_result_and_state')
    using sim_stack_alloc stack_byte_zero 
    by (fastforce simp add: sim_set_def rel_split_heap_def init split: xval_splits)
  apply simp
  apply simp
  apply simp
  apply (rule refines_rel_prod_guard_on_exit [where S'="rel_split_heap"])
   apply (subst (asm) rel_split_heap_def )
   apply simp
   apply (rule f)
  subgoal by (auto simp add: rel_split_heap_def sim_stack_release)
  subgoal by (simp add: Ex_list_of_length)
  done

lemma sim_with_fresh_stack_ptr:
  fixes f⇩c:: "'a ptr ⇒ ('b, 'c, 's) exn_monad"
  assumes init: "init⇩a (st s) = init⇩c s"
  assumes f: "⋀s p::'a ptr. refines (f⇩c p) (f⇩a p) s (st s) (rel_prod (=) rel_split_heap)"
  assumes typing_unchanged: "⋀s p::'a ptr. (f⇩c p) ∙ s ?⦃λr t. typing.unchanged_typing_on 𝒮 s t⦄"
  shows "refines
           (monolithic.with_fresh_stack_ptr n init⇩c f⇩c)
           (with_fresh_stack_ptr n init⇩a f⇩a) s (st s)
           (rel_prod (=) rel_split_heap)"
  apply (simp add: monolithic.with_fresh_stack_ptr_def with_fresh_stack_ptr_def
                   stack_ptr_acquire_def stack_ptr_release_def assume_stack_alloc_def)
  apply (rule refines_bind_bind_exn [where Q= "λ(r,t) (r',t').
           (rel_prod (=) rel_split_heap) (r,t) (r',t') ∧
          (∃p. r = Result p ∧ (∀i < n. ptr_span (p +⇩p int i) ⊆ 𝒮 ∧ root_ptr_valid (heap_typing t') (p +⇩p int i)))"], simp_all)

  subgoal
    apply (rule refines_assume_result_and_state')
    using sim_stack_alloc stack_byte_zero stack_allocs_𝒮 
    apply (clarsimp simp add: sim_set_def init rel_split_heap_def, safe)
      apply blast+
    by (smt (verit) hrs_htd_update stack_allocs_cases)
 
  subgoal for p t t'
    apply (rule refines_runs_to_partial_rel_prod_on_exit [where S'="rel_split_heap" and P="typing.unchanged_typing_on 𝒮 t"])
       apply (subst (asm) rel_split_heap_def )
       apply simp
       apply (rule f)
      apply (rule typing_unchanged)
    subgoal for s⇩c s⇩a t⇩c
      apply clarsimp
      apply (clarsimp simp add: rel_split_heap_def)
      apply (subst sim_stack_release)
      subgoal for bs i
        using typing.unchanged_typing_on_root_ptr_valid_preservation [where S=𝒮 and s=t and t=s⇩c and p=" (p +⇩p int i)"]
        by auto
      subgoal by auto
      subgoal by auto
      done
  subgoal by (simp add: Ex_list_of_length)
  done
  done

lemma sim_assume_with_fresh_stack_ptr:
  fixes f⇩c:: "'a ptr ⇒ ('b, 'c, 's) exn_monad"
  assumes init: "init⇩a (st s) = init⇩c s"
  assumes f: "⋀s p::'a ptr. refines (f⇩c p) (f⇩a p) s (st s) (rel_prod (=) rel_split_heap)"
  assumes typing_unchanged: "⋀s p::'a ptr. (f⇩c p) ∙ s ?⦃λr t. typing.unchanged_typing_on 𝒮 s t⦄"
  shows "refines
           (monolithic.with_fresh_stack_ptr n init⇩c f⇩c)
           (assume_with_fresh_stack_ptr n init⇩a f⇩a) s (st s)
           (rel_prod (=) rel_split_heap)"
  unfolding monolithic.with_fresh_stack_ptr_def assume_with_fresh_stack_ptr_def
                   stack_ptr_acquire_def stack_ptr_release_def assume_stack_alloc_def
  apply (rule refines_bind_bind_exn [where Q= "λ(r,t) (r',t').
           (rel_prod (=) rel_split_heap) (r,t) (r',t') ∧
          (∃p. r = Result p ∧ (∀i < n. ptr_span (p +⇩p int i) ⊆ 𝒮 ∧ root_ptr_valid (heap_typing t') (p +⇩p int i)))"])

  subgoal
    apply (rule refines_assume_result_and_state')
    using sim_stack_alloc stack_byte_zero stack_allocs_𝒮
    apply (clarsimp simp add: sim_set_def init rel_split_heap_def hrs_htd_update stack_allocs_root_ptr_valid_same)
     apply blast
    done
  apply simp
  apply simp
  apply simp
  subgoal for p q t t'
    apply (rule refines_runs_to_partial_rel_prod_assume_on_exit [where S'="rel_split_heap" and P="typing.unchanged_typing_on 𝒮 t"])
       apply (subst (asm) rel_split_heap_def )
       apply simp
       apply (rule f)
      apply (rule typing_unchanged)
    subgoal for s⇩c s⇩a t⇩c
      apply clarsimp
      apply (clarsimp simp add: rel_split_heap_def)
      apply (subst sim_stack_release)
      subgoal for bs i
        using typing.unchanged_typing_on_root_ptr_valid_preservation [where S=𝒮 and s=t and t=s⇩c and p=" (p +⇩p int i)"]
        by auto
      subgoal by auto
      subgoal by auto
      done
    subgoal by (simp add: Ex_list_of_length)
    subgoal for s⇩c s⇩a
      apply clarsimp
      apply (clarsimp simp add: rel_split_heap_def)
      subgoal for i
        using typing.unchanged_typing_on_root_ptr_valid_preservation [where S=𝒮 and s=t and t=s⇩c and p=" (p +⇩p int i)"]
        by auto
      done
    done
  done



lemma L2Tcorres_guard_with_fresh_stack_ptr [heap_abs]:
  assumes rew: "struct_rewrite_expr P init⇩c' init⇩c"
  assumes grd: "abs_guard st P' P"
  assumes expr: "abs_expr st Q init⇩a init⇩c'"
  assumes f[simplified THIN_def, rule_format]: "PROP THIN (⋀p::'a ptr. L2Tcorres st (f⇩a p) (f⇩c p))"
  shows "L2Tcorres st (L2_seq (L2_guard (λs. P' s ∧ Q s))
           (λ_. (guard_with_fresh_stack_ptr n init⇩a (L2_VARS f⇩a nm))))
           (monolithic.with_fresh_stack_ptr n init⇩c (L2_VARS f⇩c nm))"
  apply (rule refines_L2Tcorres)
  apply (simp add: L2_seq_def L2_guard_def  L2_VARS_def )
  apply (rule refines_bind_guard_right)
  apply clarsimp
  apply (rule sim_guard_with_fresh_stack_ptr)
  subgoal for s
    using rew grd expr
    by (auto simp add: struct_rewrite_expr_def abs_guard_def abs_expr_def)
  subgoal for s s' p
    apply (rule L2Tcorres_refines)
    apply (rule f)
    done
  done

lemma L2Tcorres_with_fresh_stack_ptr:
  assumes typing_unchanged: "⋀s p::'a ptr. (f⇩c p) ∙ s ?⦃λr t. typing.unchanged_typing_on 𝒮 s t⦄"
  assumes rew: "struct_rewrite_expr P init⇩c' init⇩c"
  assumes grd: "abs_guard st P' P"
  assumes expr: "abs_expr st Q init⇩a init⇩c'"
  assumes f[simplified THIN_def, rule_format]: "PROP THIN (⋀p::'a ptr. L2Tcorres st (f⇩a p) (f⇩c p))"
  shows "L2Tcorres st (L2_seq (L2_guard (λs. P' s ∧ Q s))
           (λ_. (with_fresh_stack_ptr n init⇩a (L2_VARS f⇩a nm))))
           (monolithic.with_fresh_stack_ptr n init⇩c (L2_VARS f⇩c nm))"
  apply (rule refines_L2Tcorres)
  apply (simp add: L2_seq_def L2_guard_def  L2_VARS_def)
  apply (rule refines_bind_guard_right)
  apply clarsimp
  apply (rule sim_with_fresh_stack_ptr)
  subgoal for s
    using rew grd expr
    by (auto simp add: struct_rewrite_expr_def abs_guard_def abs_expr_def)
  subgoal for s s' p
    apply (rule L2Tcorres_refines)
    apply (rule f)
    done
  using typing_unchanged by blast

lemma L2Tcorres_assume_with_fresh_stack_ptr[heap_abs]:
  assumes typing_unchanged: "⋀s p::'a ptr. (f⇩c p) ∙ s ?⦃λr t. typing.unchanged_typing_on 𝒮 s t⦄"
  assumes rew: "struct_rewrite_expr P init⇩c' init⇩c"
  assumes grd: "abs_guard st P' P"
  assumes expr: "abs_expr st Q init⇩a init⇩c'"
  assumes f[simplified THIN_def, rule_format]: "PROP THIN (⋀p::'a ptr. L2Tcorres st (f⇩a p) (f⇩c p))"
  shows "L2Tcorres st (L2_seq (L2_guard (λs. P' s ∧ Q s))
           (λ_. (assume_with_fresh_stack_ptr n init⇩a (L2_VARS f⇩a nm))))
           (monolithic.with_fresh_stack_ptr n init⇩c (L2_VARS f⇩c nm))"
  apply (rule refines_L2Tcorres)
  apply (simp add: L2_seq_def L2_guard_def L2_VARS_def)
  apply (rule refines_bind_guard_right)
  apply clarsimp
  apply (rule sim_assume_with_fresh_stack_ptr)
  subgoal for s
    using rew grd expr
    by (auto simp add: struct_rewrite_expr_def abs_guard_def abs_expr_def)
  subgoal for s s' p
    apply (rule L2Tcorres_refines)
    apply (rule f)
    done
  using typing_unchanged by blast


lemma unchanged_typing_commutes: "typing.unchanged_typing_on S s t ⟹ unchanged_typing_on S (st s) (st t)"
  using heap_typing_commutes [of s] heap_typing_commutes [of t]
  by (auto simp add: unchanged_typing_on_def typing.unchanged_typing_on_def)
end

(* The following lemmas help to establish that reading from stack_byte typed locations
   results in ZERO('a) *)

named_theorems read_stack_byte_ZERO_base
  and read_stack_byte_ZERO_step
  and read_stack_byte_ZERO_step_subst

lemma (in open_types) ptr_span_with_stack_byte_type_implies_ptr_invalid:
  fixes p :: "('a :: {mem_type, stack_type}) ptr"
  assumes *: "∀a ∈ ptr_span p. root_ptr_valid d (PTR (stack_byte) a)"
  shows "¬ ptr_valid_u (typ_uinfo_t TYPE('a)) d (ptr_val p)"
  by (metis assms disjoint_iff fold_ptr_valid' in_ptr_span_itself ptr_exhaust_eq
            ptr_valid_stack_byte_disjoint)

lemma (in open_types)
  ptr_span_with_stack_byte_type_implies_ZERO[read_stack_byte_ZERO_base]:
  fixes p :: "('a :: {mem_type, stack_type}) ptr"
  assumes "∀a ∈ ptr_span p. root_ptr_valid (hrs_htd d) (PTR (stack_byte) a)"
  shows "the_default (ZERO('a)) (plift d p) = ZERO('a)"
  using ptr_span_with_stack_byte_type_implies_ptr_invalid[OF assms]
  by (simp add: fold_ptr_valid' plift_None)

lemma ptr_span_array_ptr_index_subset_ptr_span:
  fixes p :: "(('a :: {array_outer_max_size})['b :: array_max_count]) ptr"
  assumes "i < CARD('b)"
  shows "ptr_span (array_ptr_index p c i) ⊆ ptr_span p"
  using assms
  apply (simp add: array_ptr_index_def ptr_add_def)
  apply (rule intvl_sub_offset)
  apply (rule order_trans[of _ "i * size_of TYPE('a) + size_of TYPE('a)"])
  apply (simp add: unat_le_helper)
  apply (simp add: add.commute less_le_mult_nat)
  done

lemma read_stack_byte_ZERO_array_intro[read_stack_byte_ZERO_step]:
  fixes q :: "('a :: {array_outer_max_size}['b :: array_max_count]) ptr"
  assumes ptr_span_has_stack_byte_type:
    "∀a∈ptr_span q. root_ptr_valid d (PTR(stack_byte) a)"
  assumes subtype_reads_ZERO:
    "⋀p :: 'a ptr. ∀a∈ptr_span p. root_ptr_valid d (PTR(stack_byte) a) ⟹ r s p = ZERO('a)"
  shows "(ARRAY i. r s (array_ptr_index q c i)) = ZERO('a['b])"
  apply (rule array_ext)
  apply (simp add: array_index_zero)
  apply (rule subtype_reads_ZERO)
  using ptr_span_has_stack_byte_type ptr_span_array_ptr_index_subset_ptr_span by blast

lemma read_stack_byte_ZERO_array_2dim_intro[read_stack_byte_ZERO_step]:
  fixes q :: "('a :: {array_inner_max_size}['b :: array_max_count]['c :: array_max_count]) ptr"
  assumes ptr_span_has_stack_byte_type:
    "∀a∈ptr_span q. root_ptr_valid d (PTR(stack_byte) a)"
  assumes subtype_reads_ZERO:
    "⋀p :: 'a ptr. ∀a∈ptr_span p. root_ptr_valid d (PTR(stack_byte) a) ⟹ r s p = ZERO('a)"
  shows "(ARRAY i j. r s (array_ptr_index (array_ptr_index q c i) c j)) = ZERO('a['b]['c])"
  apply (rule array_ext)
  apply (simp add: array_index_zero)
  apply (rule array_ext)
  apply (simp add: array_index_zero)
  apply (rule subtype_reads_ZERO)
  by (metis (no_types, opaque_lifting) subset_iff ptr_span_has_stack_byte_type
            ptr_span_array_ptr_index_subset_ptr_span)

lemma read_stack_byte_ZERO_field_intro[read_stack_byte_ZERO_step]:
  fixes q :: "'a :: mem_type ptr"
  assumes ptr_span_has_stack_byte_type:
    "∀a∈ptr_span q. root_ptr_valid d (PTR(stack_byte) a)"
  assumes subtype_reads_ZERO:
    "⋀p :: 'b :: mem_type ptr. ∀a∈ptr_span p. root_ptr_valid d (PTR(stack_byte) a) ⟹ r s p = ZERO('b)"
  assumes subtype_lookup:
    "field_lookup (typ_uinfo_t TYPE('a)) f 0 = Some (typ_uinfo_t TYPE('b), n)"
  shows "r s (PTR('b) (&(q→f))) = ZERO('b)"
proof -
  have "ptr_span (PTR('b) (&(q→f))) ⊆ ptr_span q"
    using TypHeapSimple.field_tag_sub'[OF subtype_lookup]
    by (simp, metis size_of_fold)
  thus ?thesis
    using ptr_span_has_stack_byte_type subtype_lookup subtype_reads_ZERO by blast
qed


context open_types
begin

lemma ptr_span_with_stack_byte_type_implies_read_dedicated_heap_ZERO[simp]:
  "∀a∈ptr_span p. root_ptr_valid (hrs_htd s) (PTR(stack_byte) a) ⟹
    read_dedicated_heap s p = ZERO('a::{stack_type, xmem_type})"
  unfolding read_dedicated_heap_def ptr_span_with_stack_byte_type_implies_ZERO[of p] merge_addressable_fields.idem ..

lemma write_simulationI:
  fixes R :: "'s ⇒ 'a::xmem_type ptr ⇒ 'a"
  assumes fs: "map_of 𝒯 (typ_uinfo_t TYPE('a)) = Some fs"
  assumes "heap_typing_simulation 𝒯 t_hrs t_hrs_update heap_typing heap_typing_update l"
    and l_w: "list_all2 (λf w. ∀t u n h (p::'a ptr) x.
        field_ti TYPE('a) f = Some t ⟶
        field_lookup (typ_uinfo_t TYPE('a)) f 0 = Some (u, n) ⟶
        ptr_valid_u u (hrs_htd (t_hrs h)) &(p→f) ⟶
        l (t_hrs_update (hrs_mem_update (heap_upd_list (size_td u) &(p→f) (access_ti t x))) h)
          = w p x (l h)) fs ws"
    and l_u: "⋀(p::'a ptr) (x::'a) (s::'b).
      ptr_valid (hrs_htd (t_hrs s)) p ⟹
      l (t_hrs_update (write_dedicated_heap p x) s) = u (upd_fun p (λold. merge_addressable_fields old x)) (l s)"
  assumes V:
    "⋀h p. V (l h) p ⟷ ptr_valid (hrs_htd (t_hrs h)) p"
  assumes W:
    "⋀p f h. W p f h =
      fold (λw. w p (f (R h p))) ws (u (upd_fun p (λold. merge_addressable_fields old (f (R h p)))) h)"
  shows "write_simulation t_hrs t_hrs_update l V W"
proof -
  interpret hrs: heap_typing_simulation 𝒯 t_hrs t_hrs_update heap_typing heap_typing_update l
    by fact

  have valid:
    "list_all (λf. ∀u n. field_lookup (typ_uinfo_t TYPE('a)) f 0 = Some (u, n) ⟶
      ptr_valid_u u h &(p→f)) fs"
    if *: "ptr_valid_u (typ_uinfo_t TYPE('a)) h (ptr_val p)" for h and p :: "'a ptr"
    using ptr_valid_u_step[OF fs _ _ *]
    by (auto simp: list_all_iff field_lvalue_def field_offset_def)

  have fold': "l (fold
        (λxa. t_hrs_update
                (hrs_mem_update
                  (heap_upd_list (size_td (the (field_ti TYPE('a) xa))) &(p→xa)
                    (access_ti (the (field_ti TYPE('a) xa)) x))))
        fs s) =
      fold (λw. w p x) ws (l s)"
    if p: "ptr_valid_u (typ_uinfo_t TYPE('a)) (hrs_htd (t_hrs s)) (ptr_val p)"
    for p x s
    using l_w wf_𝒯[OF fs] p[THEN valid]
  proof (induction arbitrary: s)
    case (Cons f fs w ws)
    from Cons.prems obtain u n where f_u :"field_lookup (typ_uinfo_t TYPE('a)) f 0 = Some (u, n)"
      and [simp]: "list_all (λf. ∃a b. field_lookup (typ_uinfo_t TYPE('a)) f 0 = Some (a, b)) fs"
      by auto
    from f_u[THEN field_lookup_uinfo_Some_rev] obtain k where
      "field_lookup (typ_info_t TYPE('a)) f 0 = Some (k, n)" and u_eq: "u = export_uinfo k"
      by auto
    then have [simp]: "field_ti TYPE('a) f = Some k" by (simp add: field_ti_def)
    have [simp]: "size_td k = size_td u"
      by (simp add: u_eq)
    have [simp]: "ptr_valid_u u (hrs_htd (t_hrs s)) &(p→f)"
      using Cons.prems(2) f_u by auto
    show ?case
      using Cons.prems Cons.hyps by (simp add: Cons.IH f_u)
  qed simp

  have fold:
    "l ((fold (t_hrs_update ∘
          (λ(f, u). hrs_mem_update (heap_upd_list (size_td u) &(p→f) (access_ti u x))))
        (addressable_fields TYPE('a)) ∘
      t_hrs_update (write_dedicated_heap p x)) s) =
    fold (λw. w p x) ws (u (upd_fun p (λold. merge_addressable_fields old x)) (l s))"
    if p: "ptr_valid_u (typ_uinfo_t TYPE('a)) (hrs_htd (t_hrs s)) (ptr_val p)"
    for p x s
    by (subst addressable_fields_def)
       (simp add: fs fold_map fold' p ptr_valid_def l_u cong: fold_cong)

  show ?thesis
    apply (rule hrs.write_simulation_alt)
    apply (simp add: V)
    apply (subst hrs_mem_update_heap_update')
    apply (subst W)
    apply (subst (asm) V)
    apply (subst (asm) ptr_valid_def)
    apply (subst hrs.t_hrs.upd_comp[symmetric])
    apply (subst hrs.t_hrs.upd_comp_fold)
    apply (subst fold)
    apply simp_all
    done
qed

end

locale stack_simulation_heap_typing =
  typ_heap_simulation st r w "λt p. open_types.ptr_valid 𝒯 (heap_typing t) p" t_hrs t_hrs_update +
  heap_typing_simulation 𝒯 t_hrs t_hrs_update heap_typing heap_typing_upd st +
  typ_heap_typing r w heap_typing heap_typing_upd 𝒮
  for
    st:: "'s ⇒ 't" and
    r:: "'t ⇒ ('a::{xmem_type, stack_type}) ptr ⇒ 'a" and
    w:: "'a ptr ⇒ ('a ⇒ 'a) ⇒ 't ⇒ 't" and
    t_hrs :: "'s ⇒ heap_raw_state" and
    t_hrs_update:: "(heap_raw_state ⇒ heap_raw_state) ⇒ 's ⇒ 's" and
    heap_typing :: "'t ⇒ heap_typ_desc" and
    heap_typing_upd :: "(heap_typ_desc ⇒ heap_typ_desc) ⇒ 't ⇒ 't" and
    𝒮:: "addr set" and
    𝒯:: "(typ_uinfo * qualified_field_name list) list" +

assumes sim_stack_alloc_heap_typing:
  "⋀p d s n.
    (p, d) ∈ stack_allocs n 𝒮 TYPE('a) (hrs_htd (t_hrs s)) ⟹
      st (t_hrs_update (hrs_mem_update (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n]) ∘ hrs_htd_update (λ_. d)) s) =
      (heap_typing_upd (λ_. d) (st s))"

assumes sim_stack_release_heap_typing:
"⋀(p::'a ptr) s n. (⋀i. i < n ⟹ root_ptr_valid (hrs_htd (t_hrs s)) (p +⇩p int i)) ⟹
  st (t_hrs_update (hrs_htd_update (stack_releases n p)) s) =
    heap_typing_upd (stack_releases n p)
     (st (t_hrs_update (hrs_mem_update (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n])) s))"

assumes sim_stack_stack_byte_zero[read_stack_byte_ZERO_step]:
  "⋀p s. ∀a∈ptr_span p. root_ptr_valid (hrs_htd (t_hrs s)) (PTR(stack_byte) a) ⟹ r (st s) p = ZERO('a)" (* " *)

begin

lemma fold_heap_update_simulation:
  assumes valid: "⋀i. i < n ⟹ ptr_valid (heap_typing (st s)) (p +⇩p int i)"
  shows "st (t_hrs_update (hrs_mem_update (fold (λi. heap_update (p +⇩p int i) (vs i)) [0..<n])) s) =
          fold (λi. w (p +⇩p int i) (λ_. vs i)) [0..<n] (st s)"
  using valid
proof (induct n arbitrary: vs s)
  case 0
  then show ?case
    by (simp add: case_prod_unfold hrs_mem_update_def)
next
  case (Suc n)
  from Suc.prems obtain
    valid: "⋀i. i < Suc n ⟹ ptr_valid (heap_typing (st s)) (p +⇩p int i)" by blast

  from valid have valid': "⋀i. i < n ⟹ ptr_valid (heap_typing (st s)) (p +⇩p int i)" by auto
  note hyp = Suc.hyps [OF valid']
  show ?case
    apply (simp add: hyp [symmetric])
    apply (subst write_commutes [symmetric])
    using valid
    apply simp
    using TypHeapSimple.hrs_mem_update_comp hrs_mem_update_def
    apply simp
    done
qed

lemma fold_heap_update_padding_simulation:
  assumes valid: "⋀i. i < n ⟹ ptr_valid (heap_typing (st s)) (p +⇩p int i)"
  assumes lbs: "length bs = n * size_of TYPE('a)"
  shows "st (t_hrs_update (hrs_mem_update (fold (λi. heap_update_padding (p +⇩p int i) (vs i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<n])) s) =
          fold (λi. w (p +⇩p int i) (λ_. vs i)) [0..<n] (st s)"
  using valid lbs
proof (induct n arbitrary: bs vs s )
  case 0
  then show ?case
    by (simp add: case_prod_unfold hrs_mem_update_def)
next
  case (Suc n)
  from Suc.prems obtain
    valid: "⋀i. i < Suc n ⟹ ptr_valid (heap_typing (st s)) (p +⇩p int i)" and
    lbs': "length (take (n * (size_of TYPE('a))) bs) = n * size_of TYPE('a)"
    by auto

  from valid have valid': "⋀i. i < n ⟹ ptr_valid (heap_typing (st s)) (p +⇩p int i)" by auto
  note hyp = Suc.hyps [OF valid' lbs']
  have take_eq: "⋀i. i < n ⟹ take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) (take (n * size_of TYPE('a)) bs)) =
        take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs)"
    by (metis Groups.mult_ac(2) mult_less_cancel1 not_less not_less_eq
        order_less_imp_le take_all take_drop_take times_nat.simps(2))

  have fold_eq: "⋀h. fold
              (λi. heap_update_padding (p +⇩p int i) (vs i)
                        (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) (take (n * size_of TYPE('a)) bs))))
              [0..<n] h =
            fold
              (λi. heap_update_padding (p +⇩p int i) (vs i)
                        (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs)))
                 [0..<n] h"

    apply (rule fold_cong)
      apply (rule refl)
     apply (rule refl)
    using take_eq
    apply simp
    done


  show ?case
    apply (simp add: hyp [symmetric])
    apply (subst write_padding_commutes [symmetric, where bs = "take (size_of TYPE('a)) (drop (n * size_of TYPE('a)) bs)"])
    subgoal using valid
      by simp
    subgoal using Suc.prems by simp
    subgoal
    using TypHeapSimple.hrs_mem_update_comp hrs_mem_update_def
      by (simp add: fold_eq)
    done
qed

lemma sim_stack_alloc':
  assumes alloc: "(p, d) ∈ stack_allocs n 𝒮 TYPE('a) (hrs_htd (t_hrs s))"
  assumes len: "length vs = n"
  assumes lbs: "length bs = n * size_of TYPE('a)"
  shows "st (t_hrs_update (hrs_mem_update (fold (λi. heap_update_padding (p +⇩p int i) (vs!i) (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs))) [0..<n]) ∘ hrs_htd_update (λ_. d)) s) =
            (fold (λi. w (p +⇩p int i) (λ_. (vs ! i))) [0..<n]) (heap_typing_upd (λ_. d) (st s))"
proof -
  {
    fix i
    assume i_bound: "i < n"
    have "ptr_valid (heap_typing (st (t_hrs_update
                 (hrs_mem_update (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n]) ∘
                  hrs_htd_update (λ_. d))
                 s)))
          (p +⇩p int i)"
    proof -
      from stack_allocs_cases [OF alloc] i_bound
      have ptr_valid: "ptr_valid d (p +⇩p int i)"
        using root_ptr_valid_ptr_valid by auto
      thus ?thesis
        using heap_typing_upd_commutes by (simp, metis)
    qed
  } note valids = this

  from stack_allocs_cases [OF alloc] obtain
    bound: "unat (ptr_val p) + n * size_of TYPE('a) ≤ addr_card" and
    not_null: "ptr_val p ≠ 0"
    by (metis Ptr_ptr_val c_guard_NULL_simp)

  show ?thesis
    apply (simp add: sim_stack_alloc_heap_typing [OF alloc, symmetric])
    apply (subst fold_heap_update_padding_simulation [OF valids lbs, symmetric])
      apply (simp)
     apply (simp add: len)
    apply (simp add: comp_def hrs_mem_update_comp')
    apply (subst fold_heap_update_padding_heap_update_collapse [OF bound not_null])
    using lbs
     apply (auto simp add: less_le_mult_nat nat_move_sub_le)
    done
qed

lemma sim_stack_release':
  fixes p :: "'a ptr"
  assumes roots: "⋀i. i < n ⟹ root_ptr_valid (hrs_htd (t_hrs s)) (p +⇩p int i)"
  shows "st (t_hrs_update (hrs_htd_update (stack_releases n p)) s) =
           ((heap_typing_upd (stack_releases n p) ((fold (λi. w (p +⇩p int i) (λ_. c_type_class.zero)) [0..<n]) (st s))))"
proof -
  from roots root_ptr_valid_ptr_valid heap_typing_commutes
  have valids: "⋀i . i < n ⟹ ptr_valid (heap_typing (st s)) (p +⇩p int i)"
    by metis
  note commutes = fold_heap_update_simulation [OF valids, symmetric, of n, simplified]
  show ?thesis
    apply (simp add: commutes )
    apply (simp add: sim_stack_release_heap_typing [OF roots])
    done
qed


lemma sim_stack_release'':
  fixes p :: "'a ptr"
  assumes roots: "⋀i. i < n ⟹ root_ptr_valid (hrs_htd (t_hrs s)) (p +⇩p int i)"
  assumes lbs: "length bs = n * size_of TYPE('a)"
  shows "st (t_hrs_update (hrs_mem_update (heap_update_list (ptr_val p) bs) o hrs_htd_update (stack_releases n p)) s) =
           ((heap_typing_upd (stack_releases n p) ((fold (λi. w (p +⇩p int i) (λ_. c_type_class.zero)) [0..<n]) (st s))))"
proof -
  {
    fix i
    assume bound_i: "i < length bs"
    have "root_ptr_valid (hrs_htd (t_hrs (t_hrs_update (hrs_htd_update (stack_releases n p)) s)))
            ((PTR_COERCE('a → stack_byte) p) +⇩p int i)"
    proof -
      have span: "ptr_val (((PTR_COERCE('a → stack_byte) p) +⇩p int i)) ∈ {ptr_val p..+n * size_of TYPE('a)}"
        using lbs bound_i intvlI by (auto simp add: ptr_add_def)
      from roots have "∀i<n. c_guard (p +⇩p int i)"
        using root_ptr_valid_c_guard by blast
      from stack_releases_root_ptr_valid_footprint [OF span this]
      show ?thesis
        using typing.get_upd by force
    qed
  } note sb = this

  show ?thesis
    apply (simp add:  lift_heap_update_list_stack_byte_independent [OF sb, simplified])
    apply (simp add: sim_stack_release' [OF roots])
    done
qed


lemma stack_byte_zero':
  assumes "(p, d) ∈ stack_allocs n 𝒮 TYPE('a) (hrs_htd (t_hrs s))"
  assumes "i < n"
  shows "r (st s) (p +⇩p int i) = ZERO('a)"
  by (rule sim_stack_stack_byte_zero)
     (meson assms stack_allocs_cases stack_allocs_contained subsetD)

sublocale stack_simulation
  using sim_stack_alloc' sim_stack_release'' stack_byte_zero'
  by (unfold_locales) auto

sublocale typ_heap_typing_stack_simulation 𝒯 st r w "λt p. open_types.ptr_valid 𝒯 (heap_typing t) p" t_hrs t_hrs_update heap_typing heap_typing_upd 𝒮
  by (unfold_locales)

end





(*
 * Assert the given field ("field_getter", "field_setter") of the given structure
 * can be abstracted into the heap, and then accessed as a HOL object.
 *)

(*
 * This can deal with nested structures, but they must be packed_types.
 * fixme: generalise this framework to mem_types
 *)

definition
  valid_struct_field
    :: "string list
           ⇒ (('p::xmem_type) ⇒ ('f::xmem_type))
           ⇒ (('f ⇒ 'f) ⇒ ('p ⇒ 'p))
           ⇒ ('s ⇒ heap_raw_state)
           ⇒ ((heap_raw_state ⇒ heap_raw_state) ⇒ 's ⇒ 's)
           ⇒ bool"
 where
  "valid_struct_field field_name field_getter field_setter t_hrs t_hrs_update ≡
     (lense field_getter field_setter
      ∧ field_ti TYPE('p) field_name =
          Some (adjust_ti (typ_info_t TYPE('f)) field_getter (field_setter ∘ (λx _. x)))
      ∧ (∀p :: 'p ptr. c_guard p ⟶ c_guard (Ptr &(p→field_name) :: 'f ptr))
      ∧ lense t_hrs t_hrs_update)"

lemma typ_heap_simulation_get_hvalD:
  "⟦ typ_heap_simulation st r w v
        t_hrs t_hrs_update; v (st s) p ⟧ ⟹
      h_val (hrs_mem (t_hrs s)) p = r (st s) p"
  by (clarsimp simp: read_simulation.read_commutes [OF typ_heap_simulation.axioms(2)])

lemma valid_struct_fieldI [intro]:
  fixes field_getter :: "('a::xmem_type) ⇒ ('f::xmem_type)"
  shows "⟦
     ⋀s f. f (field_getter s) = (field_getter s) ⟹ field_setter f s = s;
     ⋀s f f'. f (field_getter s) = f' (field_getter s) ⟹ field_setter f s = field_setter f' s;
     ⋀s f. field_getter (field_setter f s) = f (field_getter s);
     ⋀s f g. field_setter f (field_setter g s) = field_setter (f ∘ g) s;
     field_ti TYPE('a) field_name =
         Some (adjust_ti (typ_info_t TYPE('f)) field_getter (field_setter ∘ (λx _. x)));
     ⋀(p::'a ptr). c_guard p ⟹ c_guard (Ptr &(p→field_name) :: 'f ptr);
     ⋀s x. t_hrs (t_hrs_update x s) = x (t_hrs s);
     ⋀s f. f (t_hrs s) = t_hrs s ⟹ t_hrs_update f s = s;
     ⋀s f f'. f (t_hrs s) = f' (t_hrs s) ⟹ t_hrs_update f s = t_hrs_update f' s;
     ⋀s f g. t_hrs_update f (t_hrs_update g s) = t_hrs_update (λx. f (g x)) s
      ⟧ ⟹
    valid_struct_field field_name field_getter field_setter t_hrs t_hrs_update"
  apply (unfold valid_struct_field_def lense_def o_def)
  apply (safe | assumption | rule ext)+
  done

lemma typ_heap_simulation_t_hrs_updateD:
  "⟦ typ_heap_simulation st r w v
         t_hrs t_hrs_update; v (st s) p ⟧ ⟹
           st (t_hrs_update (hrs_mem_update (heap_update p v')) s) =
                           w p (λx. v') (st s)"
  by (clarsimp simp: write_simulation.write_commutes [OF typ_heap_simulation.axioms(3)])

lemma heap_abs_expr_guard [heap_abs]:
  "⟦ typ_heap_simulation st getter setter vgetter t_hrs t_hrs_update;
     abs_expr st P x' x ⟧ ⟹
     abs_guard st (λs. P s ∧ vgetter s (x' s)) (λs. (c_guard (x s :: ('a::xmem_type) ptr)))"
  apply (clarsimp simp: abs_expr_def abs_guard_def
                        simple_lift_def root_ptr_valid_def
                        valid_implies_cguard.valid_implies_c_guard [OF typ_heap_simulation.axioms(5)])
  done

lemma heap_abs_expr_h_val [heap_abs]:
  "⟦ typ_heap_simulation st r w v t_hrs t_hrs_update;
     abs_expr st P x' x ⟧ ⟹
      abs_expr st
       (λs. P s ∧ v s (x' s))
         (λs. (r s (x' s)))
         (λs. (h_val (hrs_mem (t_hrs s))) (x s))"
  apply (clarsimp simp: abs_expr_def simple_lift_def)
  apply (metis typ_heap_simulation_get_hvalD)
  done

lemma heap_abs_modifies_heap_update__unused:
  "⟦ typ_heap_simulation st r w v t_hrs t_hrs_update;
     abs_expr st Pb b' b;
     abs_expr st Pc c' c ⟧ ⟹
      abs_modifies st (λs. Pb s ∧ Pc s ∧ v s (b' s))
        (λs. w (b' s) (λx. (c' s)) s)
        (λs. t_hrs_update (hrs_mem_update (heap_update (b s :: ('a::xmem_type) ptr) (c s))) s)"
  apply (clarsimp simp: typ_simple_heap_simps abs_expr_def abs_modifies_def)
  apply (metis typ_heap_simulation_t_hrs_updateD)
  done

(* See comment for heap_lift__wrap_h_val. *)
definition "heap_lift__h_val ≡ h_val"

(* See the comment for struct_rewrite_modifies_field.
 * In this case we rely on nice unification for ?c.
 * The heap_abs_syntax generator also relies on this rule
 * and would need to be modified if the previous rule was used instead. *)
(*        (λs. setter (λx. x(b' s := c' (x (b' s)) s)) s) *)
lemma heap_abs_modifies_heap_update [heap_abs]:
  "⟦ typ_heap_simulation st r w v t_hrs t_hrs_update;
     abs_expr st Pb b' b;
     ⋀v. abs_expr st Pc (c' v) (c v) ⟧ ⟹
      abs_modifies st (λs. Pb s ∧ Pc s ∧ v s (b' s))
        (λs. w (b' s) (λ_. (c' (r s (b' s)) s)) s)
        (λs. t_hrs_update (hrs_mem_update
               (heap_update (b s :: ('a::xmem_type) ptr)
                            (c (heap_lift__h_val (hrs_mem (t_hrs s)) (b s)) s))) s)"
  apply (clarsimp simp: typ_simple_heap_simps abs_expr_def abs_modifies_def heap_lift__h_val_def)
  subgoal for s
    apply (rule subst[where t = "h_val (hrs_mem (t_hrs s)) (b' (st s))"
        and s = "r (st s) (b' (st s))"])
     apply (clarsimp simp: read_simulation.read_commutes [OF typ_heap_simulation.axioms(2)])
    apply (simp add: write_simulation.write_commutes [OF typ_heap_simulation.axioms(3)])
    done
  done


(*
 * struct_rewrite: remove uses of field_lvalue. (field_lvalue p a = &(p→a))
 * We do three transformations:
 *   c_guard (p→a)  ⟸  c_guard p
 *   h_val s (p→a)   =   p_C.a_C (h_val s p)
 *   heap_update (p→a) v s   =   heap_update p (p_C.a_C_update (λ_. v) (h_val s p)) s
 * However, an inner expression may nest h_vals arbitrarily.
 *
 * Any output of a struct_rewrite rule should be fully rewritten.
 * By doing this, each rule only needs to rewrite the parts of a term that it
 * introduces by itself.
 *)

(* struct_rewrite_guard rules *)

lemma struct_rewrite_guard_expr [heap_abs]:
  "struct_rewrite_expr P a' a ⟹ struct_rewrite_guard (λs. P s ∧ a' s) a"
  by (simp add: struct_rewrite_expr_def struct_rewrite_guard_def)

lemma struct_rewrite_guard_constant [heap_abs]:
  "struct_rewrite_guard (λ_. P) (λ_. P)"
  by (simp add: struct_rewrite_guard_def)

lemma struct_rewrite_guard_conj [heap_abs]:
  "⟦ struct_rewrite_guard b' b; struct_rewrite_guard a' a ⟧ ⟹
       struct_rewrite_guard (λs. a' s ∧ b' s) (λs. a s ∧ b s)"
  by (clarsimp simp: struct_rewrite_guard_def)

lemma struct_rewrite_guard_split [heap_abs]:
  "⟦ ⋀a b. struct_rewrite_guard (A a b) (C a b) ⟧
       ⟹ struct_rewrite_guard (case r of (a, b) ⇒ A a b) (case r of (a, b) ⇒ C a b)"
  apply (auto simp: split_def)
  done

lemma struct_rewrite_guard_c_guard_field [heap_abs]:
  "⟦ valid_struct_field field_name (field_getter :: ('a :: xmem_type) ⇒ ('f :: xmem_type)) field_setter t_hrs t_hrs_update;
     struct_rewrite_expr P p' p;
     struct_rewrite_guard Q (λs. c_guard (p' s)) ⟧ ⟹
   struct_rewrite_guard (λs. P s ∧ Q s)
     (λs. c_guard (Ptr (field_lvalue (p s :: 'a ptr) field_name) :: 'f ptr))"
  by (simp add: valid_struct_field_def struct_rewrite_expr_def struct_rewrite_guard_def)

lemma align_of_array: "align_of TYPE(('a :: array_outer_max_size)['b' :: array_max_count]) = align_of TYPE('a)"
  by (simp add: align_of_def align_td_array)


lemma c_guard_array:
  "⟦ 0 ≤ k; nat k < CARD('b); c_guard (p :: (('a::array_outer_max_size)['b::array_max_count]) ptr) ⟧
   ⟹ c_guard (ptr_coerce p +⇩p k :: 'a ptr)"
  apply (clarsimp simp: CTypesDefs.ptr_add_def c_guard_def c_null_guard_def)
  apply (rule conjI[rotated])
   apply (erule contrapos_nn)
   apply (clarsimp simp: intvl_def)
  subgoal for i
    apply (rule exI[where  x = "nat k * size_of TYPE('a) + i"])
    apply clarsimp
    apply (rule conjI)
     apply (simp add: field_simps)
    apply (rule less_le_trans[where y = "Suc (nat k) * size_of TYPE('a)"])
     apply simp
    apply (metis less_eq_Suc_le mult_le_mono2 mult.commute)
    done
  apply (subgoal_tac "ptr_aligned (ptr_coerce p :: 'a ptr)")
   apply (frule_tac p = "ptr_coerce p" and i = "k" in ptr_aligned_plus)
   apply (clarsimp simp: CTypesDefs.ptr_add_def)
  apply (clarsimp simp: ptr_aligned_def align_of_array)
  done

lemma struct_rewrite_guard_c_guard_Array_field [heap_abs]:
  "⟦ valid_struct_field field_name (field_getter :: ('a :: xmem_type) ⇒ ('f::array_outer_max_size ['n::array_max_count])) field_setter t_hrs t_hrs_update;
     struct_rewrite_expr P p' p;
     struct_rewrite_guard Q (λs. c_guard (p' s)) ⟧ ⟹
   struct_rewrite_guard (λs. P s ∧ Q s ∧ 0 ≤ k ∧ nat k < CARD('n))
     (λs. c_guard (ptr_coerce (Ptr (field_lvalue (p s :: 'a ptr) field_name) :: (('f['n]) ptr)) +⇩p k :: 'f ptr))"
  by (simp del: ptr_coerce.simps add: valid_struct_field_def struct_rewrite_expr_def struct_rewrite_guard_def c_guard_array)


(* struct_rewrite_expr rules *)

(* This is only used when heap lifting is turned off,
 * where we expect no rewriting to happen anyway.
 * TODO: it might be safe to enable this unconditionally,
 *       as long as it happens after heap_abs_fo. *)
lemma struct_rewrite_expr_id:
  "struct_rewrite_expr (λ_. True) A A"
  by (simp add: struct_rewrite_expr_def)


lemma struct_rewrite_expr_fun_app2 [heap_abs_fo]:
  "⟦ struct_rewrite_expr P f f';
     struct_rewrite_expr Q g g' ⟧ ⟹
   struct_rewrite_expr (λs. P s ∧ Q s) (λs a. f s a (g s a)) (λs a. f' s a $ g' s a)"
  by (simp add: struct_rewrite_expr_def)

lemma struct_rewrite_expr_fun_app [heap_abs_fo]:
  "⟦ struct_rewrite_expr Y x x'; struct_rewrite_expr X f f' ⟧ ⟹
       struct_rewrite_expr (λs. X s ∧ Y s) (λs. f s (x s)) (λs. f' s $ x' s)"
  by (clarsimp simp: struct_rewrite_expr_def)

lemma struct_rewrite_expr_constant [heap_abs]:
  "struct_rewrite_expr (λ_. True) (λ_. a) (λ_. a)"
  by (clarsimp simp: struct_rewrite_expr_def)

lemma struct_rewrite_expr_lambda_null [heap_abs]:
  "struct_rewrite_expr P A C ⟹ struct_rewrite_expr P (λs _. A s) (λs _. C s)"
  by (clarsimp simp: struct_rewrite_expr_def)

lemma struct_rewrite_expr_split [heap_abs]:
  "⟦ ⋀a b. struct_rewrite_expr (P a b) (A a b) (C a b) ⟧
       ⟹ struct_rewrite_expr (case r of (a, b) ⇒ P a b)
            (case r of (a, b) ⇒ A a b) (case r of (a, b) ⇒ C a b)"
  apply (auto simp: split_def)
  done

lemma struct_rewrite_expr_basecase_h_val [heap_abs]:
  "struct_rewrite_expr (λ_. True) (λs. h_val (h s) (p s)) (λs. h_val (h s) (p s))"
  by (simp add: struct_rewrite_expr_def)

lemma struct_rewrite_expr_indirect_h_val [heap_abs]:
  "struct_rewrite_expr P a c ⟹
   struct_rewrite_expr P (λs. h_val (h s) (a s)) (λs. h_val (h s) (c s))"
  by (simp add: struct_rewrite_expr_def)

lemma struct_rewrite_expr_field [heap_abs]:
  "⟦ valid_struct_field field_name (field_getter :: ('a :: xmem_type) ⇒ ('f :: xmem_type)) field_setter t_hrs t_hrs_update;
     struct_rewrite_expr P p' p;
     struct_rewrite_expr Q a (λs. h_val (hrs_mem (t_hrs s)) (p' s)) ⟧
   ⟹ struct_rewrite_expr (λs. P s ∧ Q s) (λs. field_getter (a s))
        (λs. h_val (hrs_mem (t_hrs s)) (Ptr (field_lvalue (p s) field_name)))"
  apply (clarsimp simp: valid_struct_field_def struct_rewrite_expr_def)
  apply (subst h_val_field_from_bytes')
    apply assumption
   apply (rule export_tag_adjust_ti(1)[rule_format])
    apply (simp add: lense.fg_cons)
   apply simp
  apply simp
  done

lemma abs_expr_field [heap_abs]:
  "⟦ valid_struct_field field_name (field_getter :: ('a :: xmem_type) ⇒ ('f :: xmem_type)) field_setter t_hrs t_hrs_update;
     abs_expr st P a c⟧
   ⟹ abs_expr st P (λs. field_getter (a s)) (λs. field_getter (c s))"
  by (clarsimp simp add: valid_struct_field_def abs_expr_def)

(* Descend into struct fields that are themselves arrays. *)
lemma struct_rewrite_expr_Array_field [heap_abs]:
  "⟦ valid_struct_field field_name
                        (field_getter :: ('a :: xmem_type) ⇒ 'f::array_outer_max_size ['n::array_max_count])
                        field_setter t_hrs t_hrs_update;
     struct_rewrite_expr P p' p;
     struct_rewrite_expr Q a (λs. h_val (hrs_mem (t_hrs s)) (p' s)) ⟧
   ⟹ struct_rewrite_expr (λs. P s ∧ Q s ∧ k ≥ 0 ∧ nat k < CARD('n))
        (λs. index (field_getter (a s)) (nat k))
        (λs. h_val (hrs_mem (t_hrs s))
               (ptr_coerce (Ptr (field_lvalue (p s) field_name) :: ('f['n]) ptr) +⇩p k))"
  apply (cases k)
   apply (clarsimp simp: struct_rewrite_expr_def simp del: ptr_coerce.simps)
  subgoal for n s
    apply (subst struct_rewrite_expr_field
        [unfolded struct_rewrite_expr_def, simplified, rule_format, symmetric,
          where field_getter = field_getter and P = P and Q = Q and p = p and p' = p'])
        apply assumption
       apply simp
      apply simp
     apply simp
    apply (rule subst[where s = "p s" and t = "p' s"])
     apply simp
    apply (rule heap_access_Array_element[symmetric])
    apply simp
    done
  apply (simp add: struct_rewrite_expr_def)
  done
declare struct_rewrite_expr_Array_field [unfolded ptr_coerce.simps, heap_abs]

(* struct_rewrite_modifies rules *)

lemma struct_rewrite_modifies_id [heap_abs]:
  "struct_rewrite_modifies (λ_. True) A A"
  by (simp add: struct_rewrite_modifies_def)

(* We need some typ_heap_simulation, but we're really only after t_hrs_update.
 * We artificially constrain the type of v to limit backtracking,
 * since specialisation of typ_heap_simulation will generate one rule per 'a. *)
lemma struct_rewrite_modifies_basecase [heap_abs]:
  "⟦ typ_heap_simulation st (getter :: 's ⇒ 'a ptr ⇒ ('a::xmem_type)) setter vgetter t_hrs t_hrs_update;
     struct_rewrite_expr P p' p;
     struct_rewrite_expr Q v' v ⟧ ⟹
   struct_rewrite_modifies (λs. P s ∧ Q s)
     (λs. t_hrs_update (hrs_mem_update (heap_update (p' s) (v' s :: 'a))) s)
     (λs. t_hrs_update (hrs_mem_update (heap_update (p s) (v s :: 'a))) s)"
  by (simp add: struct_rewrite_expr_def struct_rewrite_modifies_def)

(* ≈ heap_update_field.
 * We probably need this rule to generalise struct_rewrite_modifies_field. *)
lemma heap_update_field_unpacked:
  "⟦ field_ti TYPE('a::mem_type) f = Some (t :: 'a xtyp_info);
     c_guard (p :: 'a::mem_type ptr);
     export_uinfo t = export_uinfo (typ_info_t TYPE('b::mem_type)) ⟧ ⟹
   heap_update (Ptr &(p→f) :: 'b ptr) v hp =
   heap_update p (update_ti t (to_bytes_p v) (h_val hp p)) hp"
  oops

(* ≈ heap_update_Array_element. Would want this for struct_rewrite_modifies_Array_field. *)
lemma heap_update_Array_element_unpacked:
  "n < CARD('b::array_max_count) ⟹
   heap_update (ptr_coerce p' +⇩p int n) w hp =
   heap_update (p'::('a::array_outer_max_size['b::array_max_count]) ptr)
               (Arrays.update (h_val hp p') n w) hp"
  oops

(* helper *)
lemma read_write_valid_hrs_mem:
  "lense hrs_mem hrs_mem_update"
  by (clarsimp simp: hrs_mem_def hrs_mem_update_def lense_def)


(*
 * heap_update is a bit harder.
 * Recall that we want to rewrite
 *   "heap_update (ptr→a→b→c) val s" to
 *   "heap_update ptr (c_update (b_update (a_update (λ_. val))) (h_val s ptr)) s".
 * In the second term, c_update is the outer update even though
 * c is the innermost field.
 *
 * We introduce a schematic update function ?u that would eventually be
 * instantiated to be the chain "λf. c_update (b_update (a_update f))".
 * Observe that when we find another field "→d", we can instantiate
 *   ?u' = λf. ?u (d_update f)
 * so that u' is the correct update function for "ptr→a→b→c→d".
 *
 * This is a big hack because:
 *  - We rely on a particular behaviour of the unifier (see below).
 *  - We will have a chain of flex-flex pairs
 *      ?u1 =?= λf. ?u0 (a_update f)
 *      ?u2 =?= λf. ?u1 (b_update f)
 *      etc.
 *  - Because we are doing this transformation in steps, moving
 *    one component of "ptr→a→..." at a time, we end up invoking
 *    struct_rewrite_expr on the same subterms over and over again.
 * In case we find out this hack doesn't scale, we can avoid the schematic ?u
 * by traversing the chain and constructing ?u in a separate step.
 *)

(*
 * There's more. heap_update rewrites for "ptr→a→b := RHS" cause a
 * "h_val s ptr" to appear in the RHS.
 * When we lift to the typed heap, we want this h_val to be treated
 * differently to other "h_val s ptr" terms that were already in the RHS.
 * Thus we define heap_lift__h_val ≡ h_val to carry this information around.
 *)
definition "heap_lift__wrap_h_val ≡ (=)"

lemma heap_lift_wrap_h_val [heap_abs]:
  "heap_lift__wrap_h_val (heap_lift__h_val s p) (h_val s p)"
  by (simp add: heap_lift__h_val_def heap_lift__wrap_h_val_def)

lemma heap_lift_wrap_h_val_skip [heap_abs]:
  "heap_lift__wrap_h_val (h_val s (Ptr (field_lvalue p f))) (h_val s (Ptr (field_lvalue p f)))"
  by (simp add: heap_lift__wrap_h_val_def)

lemma heap_lift_wrap_h_val_skip_array [heap_abs]:
  "heap_lift__wrap_h_val (h_val s (ptr_coerce p +⇩p k))
                         (h_val s (ptr_coerce p +⇩p k))"
  by (simp add: heap_lift__wrap_h_val_def)

(* These are valid rules, but produce redundant output. *)
lemma struct_rewrite_modifies_field__unused:
  "⟦ valid_struct_field field_name (field_getter :: ('a::xmem_type) ⇒ ('f::xmem_type)) field_setter t_hrs t_hrs_update;
     struct_rewrite_expr P p' p;
     struct_rewrite_expr Q f' f;
     struct_rewrite_modifies R
       (λs. t_hrs_update (hrs_mem_update (heap_update (p'' s)
                (u s (field_setter (λ_. f' s))))) s)
       (λs. t_hrs_update (hrs_mem_update (heap_update (p' s)
                (field_setter (λ_. f' s) (h_val (hrs_mem (t_hrs s)) (p' s))))) s);
     struct_rewrite_guard S (λs. c_guard (p' s)) ⟧ ⟹
   struct_rewrite_modifies (λs. P s ∧ Q s ∧ R s ∧ S s)
     (λs. t_hrs_update (hrs_mem_update (heap_update (p'' s)
              (u s (field_setter (λ_. f' s))))) s)
     (λs. t_hrs_update (hrs_mem_update (heap_update (Ptr (field_lvalue (p s) field_name))
              (f s))) s)"
  apply (clarsimp simp: struct_rewrite_expr_def struct_rewrite_guard_def struct_rewrite_modifies_def valid_struct_field_def)
  apply (erule_tac x = s in allE)+
  apply (erule impE, assumption)+
  apply (erule_tac t = "t_hrs_update (hrs_mem_update (heap_update (p'' s)
                          (u s (field_setter (λ_. f' s))))) s"
               and s = "t_hrs_update (hrs_mem_update (heap_update (p' s)
                          (field_setter (λ_. f' s) (h_val (hrs_mem (t_hrs s)) (p' s))))) s"
                in subst)
  apply (rule lense.upd_cong[where get = t_hrs and upd = t_hrs_update])
   apply assumption
  apply (rule lense.upd_cong[OF read_write_valid_hrs_mem])
  apply (subst heap_update_field_root_conv''')
     apply assumption+
   apply (simp add: typ_uinfo_t_def lense.fg_cons)
  apply (subst update_ti_update_ti_t)
   apply (simp add: size_of_def)
  apply (subst update_ti_s_adjust_ti_to_bytes_p)
   apply (erule lense.fg_cons)
  apply simp
  done

lemma struct_rewrite_modifies_Array_field__unused:
  "⟦ valid_struct_field field_name (field_getter :: ('a::xmem_type) ⇒ (('f::array_outer_max_size)['n::array_max_count])) field_setter t_hrs t_hrs_update;
     struct_rewrite_expr P p' p;
     struct_rewrite_expr Q f' f;
     struct_rewrite_modifies R
       (λs. t_hrs_update (hrs_mem_update (heap_update (p'' s)
                (u s (field_setter (λa. Arrays.update a (nat k) (f' s)))))) s)
       (λs. t_hrs_update (hrs_mem_update (heap_update (p' s)
               (field_setter (λa. Arrays.update a (nat k) (f' s))
                  (h_val (hrs_mem (t_hrs s)) (p' s))))) s);
     struct_rewrite_guard S (λs. c_guard (p' s)) ⟧ ⟹
   struct_rewrite_modifies (λs. P s ∧ Q s ∧ R s ∧ S s ∧ 0 ≤ k ∧ nat k < CARD('n))
     (λs. t_hrs_update (hrs_mem_update (heap_update (p'' s)
              (u s (field_setter (λa. Arrays.update a (nat k) (f' s)))))) s)
     (λs. t_hrs_update (hrs_mem_update (heap_update
            (ptr_coerce (Ptr (field_lvalue (p s) field_name) :: ('f['n]) ptr) +⇩p k) (f s))) s)"
  using ptr_coerce.simps [simp del]
  apply (clarsimp simp: struct_rewrite_expr_def struct_rewrite_guard_def struct_rewrite_modifies_def valid_struct_field_def)
  subgoal for s
    apply (erule_tac x = s in allE)+
    apply (erule impE, assumption)+
    apply (erule_tac t = "t_hrs_update (hrs_mem_update (heap_update (p'' s)
                          (u s(field_setter (λa. Arrays.update a (nat k) (f' s)))))) s"
        and s = "t_hrs_update (hrs_mem_update (heap_update (p' s)
                          (field_setter (λa. Arrays.update a (nat k) (f' s))
                             (h_val (hrs_mem (t_hrs s)) (p' s))))) s"
        in subst)
    apply (rule lense.upd_cong[where get = t_hrs and upd = t_hrs_update])
     apply assumption
    apply (rule lense.upd_cong[OF read_write_valid_hrs_mem])
    apply (cases k, clarsimp)
     apply (subst heap_update_array_element[symmetric])
       apply assumption
      apply simp
     apply (subst heap_update_field_root_conv''')
        apply assumption+
      apply (simp add: typ_uinfo_t_def lense.fg_cons)
     apply (subst h_val_field_from_bytes')
       apply assumption+
      apply (simp add: lense.fg_cons)
     apply clarsimp
     apply (subst update_ti_update_ti_t)
      apply (simp add: size_of_def)
     apply (subst update_ti_s_adjust_ti_to_bytes_p)
      apply (erule lense.fg_cons)
     apply clarsimp
     apply (subst lense.upd_cong[of field_getter field_setter])
       apply auto
    done
  done


(*
 * These produce less redundant output (we avoid "t_update (λ_. foo (t x)) x"
 * where x is some huge term).
 * The catch: we rely on the unifier to produce a "greedy" instantiation for ?f.
 * Namely, if we are matching "?f s (h_val s p)" on
 *   "b_update (a_update (λ_. foo (h_val s p))) (h_val s p)",
 * we expect ?f to be instantiated to
 *   "λs v. b_update (a_update (λ_. foo v)) v"
 * even though there are other valid ones.
 * It just so happens that isabelle's unifier produces such an instantiation.
 * Are we lucky, or presumptuous?
 *)
lemma struct_rewrite_modifies_field [heap_abs]:
  "⟦ valid_struct_field field_name (field_getter :: ('a::xmem_type) ⇒ ('f::xmem_type)) field_setter t_hrs t_hrs_update;
     struct_rewrite_expr P p' p;
     struct_rewrite_expr Q f' f;
     ⋀s. heap_lift__wrap_h_val (h_val_p' s) (h_val (hrs_mem (t_hrs s)) (p' s));
     struct_rewrite_modifies R
       (λs. t_hrs_update (hrs_mem_update (heap_update (p'' s)
                (u s (field_setter (f' s))))) s)
       (λs. t_hrs_update (hrs_mem_update (heap_update (p' s)
                (field_setter (f' s) (h_val_p' s)))) s);
     struct_rewrite_guard S (λs. c_guard (p' s)) ⟧ ⟹
   struct_rewrite_modifies (λs. P s ∧ Q s ∧ R s ∧ S s)
     (λs. t_hrs_update (hrs_mem_update (heap_update (p'' s)
              (u s (field_setter (f' s))))) s)
     (λs. t_hrs_update (hrs_mem_update (heap_update (Ptr (field_lvalue (p s) field_name))
              (f s (h_val (hrs_mem (t_hrs s)) (Ptr (field_lvalue (p s) field_name)))))) s)"
  apply (clarsimp simp: struct_rewrite_expr_def struct_rewrite_guard_def struct_rewrite_modifies_def valid_struct_field_def heap_lift__wrap_h_val_def)
  apply (erule_tac x = s in allE)+
  apply (erule impE, assumption)+
  apply (erule_tac t = "t_hrs_update (hrs_mem_update (heap_update (p'' s)
                          (u s (field_setter (f' s))))) s"
               and s = "t_hrs_update (hrs_mem_update (heap_update (p' s)
                          (field_setter (f' s) (h_val (hrs_mem (t_hrs s)) (p' s))))) s"
                in subst)
  apply (rule lense.upd_cong[where get = t_hrs and upd = t_hrs_update])
   apply assumption
  apply (rule lense.upd_cong[OF read_write_valid_hrs_mem])
  apply (subst heap_update_field_root_conv''')
     apply assumption+
   apply (simp add: typ_uinfo_t_def lense.fg_cons)
   apply (subst h_val_field_from_bytes')
     apply assumption+
    apply (simp add: lense.fg_cons)
  apply (subst update_ti_update_ti_t)
   apply (simp add: size_of_def)
  apply (subst update_ti_s_adjust_ti_to_bytes_p)
   apply (erule lense.fg_cons)
  apply (subst lense.upd_cong[where get = field_getter and upd = field_setter])
    apply auto
  done

(* fixme: this is nearly a duplicate. Would a standalone array rule work instead? *)
lemma struct_rewrite_modifies_Array_field [heap_abs]:
  "⟦ valid_struct_field field_name (field_getter :: ('a::xmem_type) ⇒ (('f::array_outer_max_size)['n::array_max_count])) field_setter t_hrs t_hrs_update;
     struct_rewrite_expr P p' p;
     struct_rewrite_expr Q f' f;
     ⋀s. heap_lift__wrap_h_val (h_val_p' s) (h_val (hrs_mem (t_hrs s)) (p' s));
     struct_rewrite_modifies R
       (λs. t_hrs_update (hrs_mem_update (heap_update (p'' s)
                (u s (field_setter (λa. Arrays.update a (nat k) (f' s (index a (nat k)))))))) s)
       (λs. t_hrs_update (hrs_mem_update (heap_update (p' s)
               (field_setter (λa. Arrays.update a (nat k) (f' s (index a (nat k))))
                  (h_val_p' s)))) s);
     struct_rewrite_guard S (λs. c_guard (p' s)) ⟧ ⟹
   struct_rewrite_modifies (λs. P s ∧ Q s ∧ R s ∧ S s ∧ 0 ≤ k ∧ nat k < CARD('n))
     (λs. t_hrs_update (hrs_mem_update (heap_update (p'' s)
              (u s (field_setter (λa. Arrays.update a (nat k) (f' s (index a (nat k)))))))) s)
     (λs. t_hrs_update (hrs_mem_update (heap_update
            (ptr_coerce (Ptr (field_lvalue (p s) field_name) :: ('f['n]) ptr) +⇩p k)
                (f s (h_val (hrs_mem (t_hrs s)) (ptr_coerce (Ptr (field_lvalue (p s) field_name) :: ('f['n]) ptr) +⇩p k :: 'f ptr))))) s)"
  using ptr_coerce.simps[simp del]
  apply (clarsimp simp: struct_rewrite_expr_def struct_rewrite_guard_def struct_rewrite_modifies_def valid_struct_field_def heap_lift__wrap_h_val_def)
  subgoal for s
    apply (erule_tac x = s in allE)+
    apply (erule impE, assumption)+
    apply (erule_tac t = "t_hrs_update (hrs_mem_update (heap_update (p'' s)
                          (u s(field_setter (λa. Arrays.update a (nat k) (f' s (index a (nat k)))))))) s"
        and s = "t_hrs_update (hrs_mem_update (heap_update (p' s)
                          (field_setter (λa. Arrays.update a (nat k) (f' s (index a (nat k))))
                             (h_val (hrs_mem (t_hrs s)) (p' s))))) s"
        in subst)
    apply (rule lense.upd_cong[where get = t_hrs and upd = t_hrs_update])
     apply assumption
    apply (rule lense.upd_cong[OF read_write_valid_hrs_mem])
    apply (cases k, clarsimp)
     apply (subst heap_update_array_element[symmetric])
       apply assumption
      apply simp
     apply (subst heap_update_field_root_conv''')
        apply assumption+
      apply (simp add: typ_uinfo_t_def lense.fg_cons)
     apply (subst h_val_field_from_bytes')
       apply assumption+
      apply (simp add: lense.fg_cons)
     apply (subst heap_access_Array_element[symmetric])
      apply simp
     apply (subst h_val_field_from_bytes')
       apply assumption+
      apply (simp add: lense.fg_cons)
     apply clarsimp
     apply (subst update_ti_update_ti_t)
      apply (simp add: size_of_def)
     apply (subst update_ti_s_adjust_ti_to_bytes_p)
      apply (erule lense.fg_cons)
     apply clarsimp
     apply (subst lense.upd_cong[of field_getter field_setter])
       apply auto
    done
  done


(*
 * Convert gets/sets to global variables into gets/sets in the new globals record.
 *)

definition
  valid_globals_field :: "
     ('s ⇒ 't)
     ⇒ ('s ⇒ 'a)
     ⇒ (('a ⇒ 'a) ⇒ 's ⇒ 's)
     ⇒ ('t ⇒ 'a)
     ⇒ (('a ⇒ 'a) ⇒ 't ⇒ 't)
     ⇒ bool"
where
  "valid_globals_field st old_getter old_setter new_getter new_setter ≡
    (∀s. new_getter (st s) = old_getter s)
    ∧ (∀s v. new_setter v (st s) = st (old_setter v s))"

lemma abs_expr_globals_getter [heap_abs]:
  "⟦ valid_globals_field st old_getter old_setter new_getter new_setter ⟧
    ⟹ abs_expr st (λ_. True) new_getter old_getter"
  apply (clarsimp simp: valid_globals_field_def abs_expr_def)
  done

lemma abs_expr_globals_setter [heap_abs]:
  "⟦ valid_globals_field st old_getter old_setter new_getter new_setter;
     ⋀old. abs_expr st (P old) (v old) (v' old) ⟧
    ⟹ abs_modifies st (λs. ∀old. P old s) (λs. new_setter (λold. v old s) s) (λs. old_setter (λold. v' old s) s)"
  apply (clarsimp simp: valid_globals_field_def abs_expr_def abs_modifies_def)
  done

lemma struct_rewrite_expr_globals_getter [heap_abs]:
  "⟦ valid_globals_field st old_getter old_setter new_getter new_setter ⟧
    ⟹ struct_rewrite_expr (λ_. True) old_getter old_getter"
  apply (clarsimp simp: struct_rewrite_expr_def)
  done

lemma struct_rewrite_modifies_globals_setter [heap_abs]:
  "⟦ valid_globals_field st old_getter old_setter new_getter new_setter;
     ⋀old. struct_rewrite_expr (P old) (v' old) (v old) ⟧
    ⟹ struct_rewrite_modifies (λs. ∀old. P old s) (λs. old_setter (λold. v' old s) s) (λs. old_setter (λold. v old s) s)"
  apply (clarsimp simp: valid_globals_field_def struct_rewrite_expr_def struct_rewrite_modifies_def)
  done

(* Translate Hoare modifies specs generated by the C parser.
 * A modifies spec is of the form
 *   {(s, s'). ∃v1 v2 ... s' = s⦇field1 := v1, field2 := v2, ...⦈}
 * except using mex and meq instead of ∃ and =. *)
lemma abs_spec_may_not_modify_globals[heap_abs]:
  "abs_spec st (λ_. True) {(a, b). meq b a} {(a, b). meq b a}"
  apply (clarsimp simp: abs_spec_def meq_def)
  done

lemma abs_spec_modify_global[heap_abs]:
  "valid_globals_field st old_getter old_setter new_getter new_setter ⟹
   abs_spec st (λ_. True) {(a, b). C a b} {(a, b). C' a b} ⟹
   abs_spec st (λ_. True) {(a, b). mex (λx. C (new_setter (λ_. x) a) b)} {(a, b). mex (λx. C' (old_setter (λ_. x) a) b)}"
  apply (fastforce simp: abs_spec_def mex_def valid_globals_field_def)
  done
(* NB: Polish will unfold meq and mex. The reason is explained there. *)


(* Signed words are stored on the heap as unsigned words. *)

lemma uint_scast:
    "uint (scast x :: 'a word) = uint (x :: 'a::len signed word)"
  apply (subst down_cast_same [symmetric])
   apply (clarsimp simp: cast_simps)
  apply (subst uint_up_ucast)
   apply (clarsimp simp: cast_simps)
  apply simp
  done

lemma to_bytes_signed_word:
    "to_bytes (x :: 'a::len8 signed word) p = to_bytes (scast x :: 'a word) p"
  by (clarsimp simp: uint_scast to_bytes_def typ_info_word word_rsplit_def)

lemma from_bytes_signed_word:
    "length p = len_of TYPE('a) div 8 ⟹
           (from_bytes p :: 'a::len8 signed word) = ucast (from_bytes p :: 'a word)"
  by (clarsimp simp: from_bytes_def word_rcat_def scast_def cast_simps typ_info_word)

lemma hrs_mem_update_signed_word:
    "hrs_mem_update (heap_update (ptr_coerce p :: 'a::len8 word ptr) (scast val :: 'a::len8 word))
               = hrs_mem_update (heap_update p (val :: 'a::len8 signed word))"
  apply (rule ext)
  apply (clarsimp simp: hrs_mem_update_def split_def)
  apply (clarsimp simp: heap_update_def to_bytes_signed_word
             size_of_def typ_info_word)
  done

lemma h_val_signed_word:
    "(h_val a p :: 'a::len8 signed word) = ucast (h_val a (ptr_coerce p :: 'a word ptr))"
  apply (clarsimp simp: h_val_def)
  apply (subst from_bytes_signed_word)
   apply (clarsimp simp: size_of_def typ_info_word)
  apply (clarsimp simp: size_of_def typ_info_word)
  done


lemma align_of_signed_word:
  "align_of TYPE('a::len8 signed word) = align_of TYPE('a word)"
  by (clarsimp simp: align_of_def typ_info_word)

lemma size_of_signed_word:
  "size_of TYPE('a::len8 signed word) = size_of TYPE('a word)"
  by (clarsimp simp: size_of_def typ_info_word)

lemma c_guard_ptr_coerce:
  "⟦ align_of TYPE('a) = align_of TYPE('b);
     size_of TYPE('a) = size_of TYPE('b) ⟧ ⟹
        c_guard (ptr_coerce p :: ('b::c_type) ptr) = c_guard (p :: ('a::c_type) ptr)"
  apply (clarsimp simp: c_guard_def ptr_aligned_def c_null_guard_def)
  done

lemma word_rsplit_signed:
    "(word_rsplit (ucast v' :: ('a::len) signed word) :: 8 word list) = word_rsplit (v' :: 'a word)"
  apply (clarsimp simp: word_rsplit_def)
  apply (clarsimp simp: cast_simps)
  done

lemma heap_update_signed_word:
    "heap_update (ptr_coerce p :: 'a word ptr) (scast v) = heap_update (p :: ('a::len8) signed word ptr) v"
    "heap_update (ptr_coerce p' :: 'a signed word ptr) (ucast v') = heap_update (p' :: ('a::len8) word ptr) v'"
  apply (auto simp: heap_update_def to_bytes_def typ_info_word word_rsplit_def cast_simps uint_scast)
  done

lemma heap_update_padding_signed_word:
    "heap_update_padding (ptr_coerce p :: 'a word ptr) (scast v) bs  = heap_update_padding (p :: ('a::len8) signed word ptr) v bs"
    "heap_update_padding (ptr_coerce p' :: 'a signed word ptr) (ucast v') bs = heap_update_padding (p' :: ('a::len8) word ptr) v' bs"
  by (auto simp: heap_update_padding_def to_bytes_def typ_info_word word_rsplit_def cast_simps uint_scast)

lemma typ_heap_simulation_c_guard:
  "⟦ typ_heap_simulation st r w v t_hrs t_hrs_update;
           v (st s) p ⟧ ⟹ c_guard p"
  by (clarsimp simp: valid_implies_cguard.valid_implies_c_guard [OF typ_heap_simulation.axioms(5)])

abbreviation (input)
  scast_f :: "(('a::len) signed word ptr ⇒ 'a signed word)
            ⇒ ('a word ptr ⇒ 'a word)"
where
  "scast_f f ≡ (λp. scast (f (ptr_coerce p)))"

abbreviation (input)
  ucast_f :: "(('a::len) word ptr ⇒ 'a word)
            ⇒ ('a signed word ptr ⇒ 'a signed word)"
where
  "ucast_f f ≡ (λp. ucast (f (ptr_coerce p)))"

abbreviation (input)
  cast_f' :: "('a ptr ⇒ 'x) ⇒ ('b ptr ⇒ 'x)"
where
  "cast_f' f ≡ (λp. f (ptr_coerce p))"

lemma read_write_validE_weak:
  "⟦ lense r w;
      ⟦ ⋀f s. r (w f s) = f (r s);
        ⋀f s. f (r s) = (r s) ⟹ w f s = s ⟧ ⟹ R ⟧
        ⟹ R"
  apply atomize_elim
  apply (unfold lense_def)
  apply metis
  done

lemma lense_transcode:
  "⟦ lense r w; ⋀v. f' (f v) = v; ⋀v. f (f' v) = v  ⟧ ⟹
   lense (λs. f' (r s)) (λg s. w (λold. f (g (f' old))) s)"
  apply (unfold lense_def)
  apply (simp add:comp_def)
  done


(* fixme: This is a sublocale relation.*)
lemma typ_heap_simulation_signed_word:
  notes align_of_signed_word [simp]
        size_of_signed_word [simp]
        heap_update_signed_word [simp]
  shows
  "⟦ typ_heap_simulation st
        (r :: 's ⇒ ('a::len8) word ptr  ⇒ 'a word) w
              v t_hrs t_hrs_update ⟧
    ⟹ typ_heap_simulation st
              (λs p. ucast (r s (ptr_coerce p)) :: 'a signed word)
              (λp f.  (w (ptr_coerce p) ((λx. scast (f (ucast x)))) ))
              (λs p. v s (ptr_coerce p))
              t_hrs t_hrs_update"
  apply (clarsimp simp: typ_heap_simulation_def
          map.compositionality o_def c_guard_ptr_coerce)
  apply (intro conjI impI)
  subgoal
    apply (clarsimp simp add: read_simulation_def)
    apply (drule_tac x=s in spec)+
    apply (drule_tac x="ptr_coerce p" in spec)+
    by (simp add: h_val_signed_word)
  subgoal
    apply (clarsimp simp add: write_simulation_def write_simulation_axioms_def)
    subgoal for s p bs x
      apply (erule_tac x=s in allE)
      apply (erule_tac x="(PTR_COERCE('a signed word → 'a word) p)" in allE)
      apply clarsimp
      apply (erule_tac x=bs in allE)
      apply clarsimp
      apply (erule_tac x= " SCAST('a signed → 'a) x" in allE)
      using heap_update_padding_signed_word
      by (metis (mono_tags, lifting) hrs_mem_update_cong)
    done

  subgoal
    by (clarsimp simp add: write_preserves_valid_def)
  subgoal
    apply (clarsimp simp add: valid_implies_cguard_def)
    apply (drule spec, drule spec, erule (1) impE)+
    apply (subst (asm) c_guard_ptr_coerce, simp, simp)
    by blast
  subgoal
    apply (simp (no_asm_use) add: valid_only_typ_desc_dependent_def)
    by blast
  subgoal
    apply (simp (no_asm_use) add: pointer_lense_def)
    apply clarsimp
    by (metis comp_apply ucast_scast_id)
  done

lemma c_guard_ptr_ptr_coerce:
    "⟦ c_guard (a :: ('a::c_type) ptr ptr); ptr_val a = ptr_val b ⟧ ⟹
         c_guard (b :: ('b::c_type) ptr ptr)"
  by (clarsimp simp: c_guard_def ptr_aligned_def c_null_guard_def)

abbreviation (input)
  ptr_coerce_f :: "('a ptr ptr ⇒ 'a ptr) ⇒ ('b ptr ptr ⇒ 'b ptr)"
where
  "ptr_coerce_f f ≡ (λp. ptr_coerce (f (ptr_coerce p)))"

abbreviation (input)
  ptr_coerce_range_f :: "('a ptr  ⇒ bool) ⇒ ('b ptr ⇒ bool)"
where
  "ptr_coerce_range_f f ≡ (λp. (f (ptr_coerce p)))"

(* fixme: this is a sublocale *)
lemma typ_heap_simulation_ptr_coerce:
  "⟦ typ_heap_simulation st
        (r :: 's ⇒ ('a::c_type) ptr ptr  ⇒ 'a ptr) w
              v t_hrs t_hrs_update ⟧
    ⟹ typ_heap_simulation st
              (λs p. ptr_coerce (r s (ptr_coerce p)) :: ('b::c_type) ptr)
              (λp f.  (w (ptr_coerce p) ((λx. ptr_coerce (f (ptr_coerce x))))))
              (λs p. v s (ptr_coerce p))
              t_hrs t_hrs_update"
  apply (clarsimp simp: typ_heap_simulation_def fun_upd_def)
  apply (intro conjI impI)
  subgoal
    by (clarsimp simp: read_simulation_def h_val_def typ_info_ptr from_bytes_def)
  subgoal
    apply (clarsimp simp add: write_simulation_def write_simulation_axioms_def)
    apply (erule allE, erule allE, erule (1) impE)+
    apply (erule_tac x="bs" in allE)
    apply clarsimp
    apply (erule_tac x="ptr_coerce x" in allE)
    apply (clarsimp simp: heap_update_padding_def [abs_def] to_bytes_def typ_info_ptr)
    done
  subgoal
    apply (clarsimp simp add: write_preserves_valid_def)
    done
  subgoal
    apply (clarsimp simp add: valid_implies_cguard_def)
    apply (drule spec, drule spec, erule (1) impE)+
    apply (subst (asm) c_guard_ptr_coerce, simp, simp)
    by blast
  subgoal
    apply (simp (no_asm_use) add: valid_only_typ_desc_dependent_def)
    by blast
  subgoal
    apply (simp (no_asm_use) add: pointer_lense_def)
    apply clarsimp
    by (metis comp_apply ptr_coerce_id ptr_coerce_idem)
  done




(*
 * Nasty hack: Convert signed word pointers-to-pointers to word
 * pointers-to-pointers.
 *
 * The idea here is that types of the form:
 *
 *    int ***x;
 *
 * need to be converted to accesses of the "unsigned int ***" heap.
 *)
lemmas signed_typ_heap_simulations =
  typ_heap_simulation_signed_word
  typ_heap_simulation_ptr_coerce [where 'a="('x::len8) word"  and 'b="('x::len8) signed word"]
  typ_heap_simulation_ptr_coerce [where 'a="('x::len8) word ptr"  and 'b="('x::len8) signed word ptr"]
  typ_heap_simulation_ptr_coerce [where 'a="('x::len8) word ptr ptr"  and 'b="('x::len8) signed word ptr ptr"]
  typ_heap_simulation_ptr_coerce [where 'a="('x::len8) word ptr ptr ptr"  and 'b="('x::len8) signed word ptr ptr ptr"]

(*
 * The above lemmas generate a mess in its output, generating things
 * like:
 *
 * (heap_w32_update
 *    (λa b. scast
 *            (((λb. ucast (a (ptr_coerce b)))(a := 3))
 *              (ptr_coerce b))))
 *
 * This theorem cleans it up a little.
 *)
lemma ptr_coerce_eq:
  "(ptr_coerce x = ptr_coerce y) = (x = y)"
  by (cases x, cases y, auto)

lemma signed_word_heap_opt [L2opt]:
  "(scast (((λx. ucast (a (ptr_coerce x))) (p := v :: 'a::len signed word)) (b :: 'a signed word ptr)))
  = ((a(ptr_coerce p := (scast v :: 'a word))) ((ptr_coerce b) :: 'a word ptr))"
  by (auto simp: fun_upd_def ptr_coerce_eq)

lemma signed_word_heap_ptr_coerce_opt [L2opt]:
  "(ptr_coerce (((λx. ptr_coerce (a (ptr_coerce x))) (p := v :: 'a ptr)) (b :: 'a ptr ptr)))
  = ((a(ptr_coerce p := (ptr_coerce v :: 'b ptr))) ((ptr_coerce b) :: 'b ptr ptr))"
  by (auto simp: fun_upd_def ptr_coerce_eq)

declare ptr_coerce_idem [L2opt]
declare scast_ucast_id [L2opt]
declare ucast_scast_id [L2opt]

(* array rules *)
lemma heap_abs_expr_c_guard_array [heap_abs]:
  "⟦ typ_heap_simulation st r w v t_hrs t_hrs_update;
      abs_expr st P x' (λs. ptr_coerce (x s) :: 'a ptr) ⟧ ⟹
     abs_guard st
        (λs. P s ∧ (∀a ∈ set (array_addrs (x' s) CARD('b)). v s a))
        (λs. c_guard (x s :: ('a::array_outer_max_size, 'b::array_max_count) array ptr))"
  apply (clarsimp simp: abs_expr_def abs_guard_def simple_lift_def root_ptr_valid_def)
  apply (subgoal_tac "∀a∈set (array_addrs (x' (st s)) CARD('b)). c_guard a")
   apply (erule allE, erule (1) impE)
   apply (rule c_guard_array_c_guard)
   apply (subst (asm) (2) set_array_addrs)
   apply force
  apply clarsimp
  apply (erule (1) my_BallE)
  apply (drule (1) typ_heap_simulation_c_guard)
  apply simp
  done

(* begin machinery for heap_abs_array_update *)
lemma fold_over_st:
  "⟦ xs = ys; P s;
     ⋀s x. x ∈ set xs ∧ P s ⟹ P (g x s) ∧ f x (st s) = st (g x s)
   ⟧ ⟹ fold f xs (st s) = st (fold g ys s)"
  apply (erule subst)
  apply (induct xs arbitrary: s)
   apply simp
  apply simp
  done

lemma fold_lift_write:
  "⟦ xs = ys; lense r w
   ⟧ ⟹ fold (λi. w (f i)) xs s = w (fold f ys) s"
  apply (erule subst)
  apply (induct xs arbitrary: s)
   apply (simp add: lense.upd_same)
  apply (simp add: lense.upd_compose)
  done

(* cf. heap_update_nmem_same *)
lemma fold_heap_update_list_nmem_same:
  "⟦ n * size_of TYPE('a :: mem_type) < addr_card;
     n * size_of TYPE('a) ≤ k; k < addr_card;
     ⋀i h. length (pad i h) = size_of TYPE('a) ⟧ ⟹
     h (ptr_val (p :: 'a ptr) + of_nat k) =
     (fold (λi h. heap_update_list (ptr_val (p +⇩p int i))
                 (to_bytes (val i h :: 'a) (pad i h)) h) [0..<n] h) (ptr_val p + of_nat k)"
  apply (induct n arbitrary: k)
   apply simp
  apply (clarsimp simp: CTypesDefs.ptr_add_def simp del: mult_Suc)
  apply (subst heap_update_nmem_same)
   apply (subst len)
    apply simp
   apply (simp add: intvl_def)
   apply (intro allI impI)
   apply (subst (asm) of_nat_mult[symmetric] of_nat_add[symmetric])+
   apply (rename_tac j)
   apply (erule_tac Q = "of_nat k = of_nat (n * size_of TYPE('a) + j)" in contrapos_pn)
   apply (subst of_nat_inj)
     apply (subst len_of_addr_card)
     apply simp
    apply (subst len_of_addr_card)
    apply simp
   apply simp
  apply simp
  done

lemma heap_list_of_disjoint_fold_heap_update_list:
  "⟦ n * size_of TYPE('a :: mem_type) < addr_card;
     n * size_of TYPE('a) + k < addr_card;
     ⋀i h. length (pad i h) = size_of TYPE('a) ⟧ ⟹
   heap_list (fold (λi h. heap_update_list (ptr_val ((p :: 'a ptr) +⇩p int i))
                            (to_bytes (val i h :: 'a) (pad i h)) h) [0..<n] h)
             k (ptr_val (p +⇩p int n))
   = heap_list h k (ptr_val (p +⇩p int n))"
  apply (rule nth_equalityI, force)
  subgoal for i
    apply (clarsimp simp: heap_list_nth)
    apply (rule subst[where t = "ptr_val (p +⇩p int n) + of_nat i"
        and s = "ptr_val p + of_nat (n * size_of TYPE('a) + i)"])
     apply (clarsimp simp: CTypesDefs.ptr_add_def)
    apply (rule fold_heap_update_list_nmem_same[symmetric])
       apply simp_all
    done
  done

(* remove false dependency *)
lemma fold_heap_update_list:
  "n * size_of TYPE('a :: mem_type) < 2^addr_bitsize ⟹
   fold (λi h. heap_update_list (ptr_val ((p :: 'a ptr) +⇩p int i))
                 (to_bytes (val i :: 'a)
                   (heap_list h (size_of TYPE('a)) (ptr_val (p +⇩p int i)))) h)
        [0..<n] h =
   fold (λi. heap_update_list (ptr_val (p +⇩p int i))
               (to_bytes (val i)
                 (heap_list h (size_of TYPE('a)) (ptr_val (p +⇩p int i)))))
        [0..<n] h"
  apply (induct n)
   apply simp
  apply clarsimp
  apply (subst heap_list_of_disjoint_fold_heap_update_list)
     apply (simp add: len_of_addr_card[symmetric])+
  done

(* cf. access_ti_list_array *)
lemma access_ti_list_array_unpacked:
  "⟦ ∀n. size_td_tuple (f n) = v3; length xs = v3 * n;
     ∀m xs. length xs = v3 ∧ m < n ⟶
              access_ti_tuple (f m) (FCP g) xs = h m xs
   ⟧ ⟹
   access_ti_list (map f [0 ..< n]) (FCP g) xs
     = foldl (@) [] (map (λm. h m (take v3 (drop (v3 * m) xs))) [0 ..< n])"
  apply (subgoal_tac "∀ys. size_td_list (map f ys) = v3 * length ys")
   prefer 2
  subgoal
    apply (rule allI)
    subgoal for ys by (induct ys) auto
    done
  apply (induct n arbitrary: xs)
   apply simp
  apply (simp add: access_ti_append)
  apply (rule foldl_cong)
    apply simp
   apply (rule map_cong[OF refl])
   apply (subst take_drop)
   apply (subst take_take)
   apply (subst min_absorb1)
    apply clarsimp
    apply (metis Suc_leI mult_Suc_right nat_mult_le_cancel_disj)
   apply (subst take_drop[symmetric])
   apply (rule refl)
  apply simp
  done

lemma concat_nth_chunk:
  "⟦ ∀x ∈ set xs. length (f x) = chunk; n < length xs ⟧
   ⟹ take chunk (drop (n * chunk) (concat (map f xs))) = f (xs ! n)"
  apply (induct xs arbitrary: n, force)
  subgoal for x xs n
    apply (cases n)
     apply clarsimp
    apply clarsimp
    done
  done

(* fixme: proof should be much nicer when done within locale *)
lemma array_update_split:
  "⟦ typ_heap_simulation st (r :: 's ⇒ ('a::array_outer_max_size) ptr ⇒ 'a) w
                    v t_hrs t_hrs_update;
     ∀x ∈ set (array_addrs (ptr_coerce p) CARD('b::array_max_count)).
        v (st s) x
   ⟧ ⟹ st (t_hrs_update (hrs_mem_update (heap_update p (arr :: 'a['b]))) s) =
          fold (λi. w (ptr_coerce p +⇩p int i) (λx. index arr i))
               [0 ..< CARD('b)] (st s)"
  apply (clarsimp simp: typ_heap_simulation_def heap_raw_state_def valid_implies_cguard_def read_simulation_def write_preserves_valid_def)

  apply (drule write_simulation.write_commutes_atomic)

  (* unwrap st *)
  apply (subst fold_over_st[OF refl,
           where P = "λs. ∀x∈set (array_addrs (ptr_coerce p) CARD('b)). v (st s) x"
             and g = "λi. t_hrs_update (hrs_mem_update (heap_update
                            (ptr_coerce p +⇩p int i) (index arr i)))"])
    apply simp
  subgoal for sa x
    apply (subgoal_tac "v (st sa) (ptr_coerce p +⇩p int x)")
     apply clarsimp
    apply (clarsimp simp: set_array_addrs)
    apply metis
    done
  apply (rule arg_cong[where f = st])
  apply (subst hrs_mem_update_def)+

  (* unwrap t_hrs_update *)
  apply (subst fold_lift_write[OF refl, where w = t_hrs_update])
   apply assumption
  apply (rule arg_cong[where f = "λf. t_hrs_update f s"])
  apply (rule ext)
  apply (subst fold_lift_write[OF refl,
        where r = fst and w = "λf s. case s of (h, z) ⇒ (f h, z)"])
   apply (simp (no_asm) add: lense_def)
  apply clarsimp

  (* split up array update *)
  apply (clarsimp simp: heap_update_def[abs_def])
  apply (subst coerce_heap_update_to_heap_updates[unfolded foldl_conv_fold,
           where chunk = "size_of TYPE('a)" and m = "CARD('b)"])
    apply (rule size_of_array[simplified mult.commute])
   apply simp

  (* remove false dependency *)
  apply (subst fold_heap_update_list[OF array_count_size])
  apply (rule fold_cong[OF refl refl])
  subgoal for a x

    apply (clarsimp simp: CTypesDefs.ptr_add_def)
    apply (rule arg_cong[where f = "heap_update_list (ptr_val p + of_nat x * of_nat (size_of TYPE('a)))"])

    apply (subst fcp_eta[where g = arr, symmetric])
    apply (clarsimp simp: to_bytes_def typ_info_array array_tag_def array_tag_n_eq simp del: fcp_eta)
    apply (subst access_ti_list_array_unpacked)
       apply clarsimp
       apply (rule refl)
      apply (simp add: size_of_def)
     apply clarsimp
     apply (rule refl)
    apply (clarsimp simp: foldl_conv_concat)

  (* we need this later *)
    apply (subgoal_tac
        "⋀x. x < CARD('b) ⟹
          size_td (typ_info_t TYPE('a))
           ≤ CARD('b) * size_td (typ_info_t TYPE('a)) - size_td (typ_info_t TYPE('a)) * x")
     prefer 2
     apply (subst le_diff_conv2)
      apply simp
     apply (subst mult.commute, subst mult_Suc[symmetric])
     apply (rule mult_le_mono1)
     apply simp

    apply (subst concat_nth_chunk)
      apply clarsimp
      apply (subst fd_cons_length)
        apply simp
       apply (simp add: size_of_def)
      apply (simp add: size_of_def)
     apply simp
    apply (subst drop_heap_list_le)
     apply (simp add: size_of_def)
    apply (subst take_heap_list_le)
     apply (simp add: size_of_def)
    apply (clarsimp simp: size_of_def)
    apply (subst mult.commute, rule refl)
    done
  done

lemma fold_update_id:
  "⟦ lense getter setter;
     ∀i ∈ set xs. ∀j ∈ set xs. (i = j) = (ind i = ind j);
     ∀i ∈ set xs. val i = getter s (ind i)
  ⟧ ⟹ fold (λi. setter (λx. x(ind i := val i))) xs s = s"
  apply (induct xs)
   apply simp
  apply (rename_tac a xs)
  apply clarsimp
  apply (subgoal_tac "setter (λx. x(ind a := getter s (ind a))) s = s")
   apply simp
  apply (subst (asm) lense_def)
  apply simp
  done

lemma fold_update_id':
  "⟦ pointer_lense r w;
     ∀i ∈ set xs. ∀j ∈ set xs. (i = j) = (ind i = ind j);
     ∀i ∈ set xs. val i = r s (ind i)
  ⟧ ⟹ fold (λi. w (ind i) (λ_. val i)) xs s = s"
  apply (induct xs)
   apply simp
  apply (rename_tac a xs)
  apply clarsimp
  apply (subgoal_tac "w (ind a) (λx. r s (ind a)) s = s")
   apply simp
  apply (subst (asm) pointer_lense_def)
  apply simp
  done

lemma array_count_index:
  "⟦ i < CARD('b::array_max_count); j < CARD('b) ⟧
   ⟹ (i = j) =
        ((of_nat (i * size_of TYPE('a::array_outer_max_size)) :: addr)
          = of_nat (j * size_of TYPE('a)))"
  apply (rule subst[where t = "i = j" and s = "i * size_of TYPE('a) = j * size_of TYPE('a)"])
   apply clarsimp
  apply (subgoal_tac "⋀ i. i < CARD('b) ⟹ i * size_of TYPE('a) < 2 ^ LENGTH(addr_bitsize)")
   apply (rule of_nat_inj[symmetric]; force)  
  apply (rule subst[where t = "len_of TYPE(addr_bitsize)" and s = addr_bitsize], force)
  apply (rule less_trans)
   apply (erule_tac b = "CARD('b)" in mult_strict_right_mono)
   apply (rule sz_nzero)
  apply (rule array_count_size)
  done


(* end machinery for heap_abs_array_update *)

lemma le_outside_intvl: "p < a ⟹ 0 ∉ {a ..+b} ⟹ p ∉ {a ..+b}"
  apply (clarsimp simp: intvl_def not_le not_less)
  by (metis Word_Lemmas_Internal.word_wrap_of_natD add_increasing2 le0 le_iff_add less_le not_less)

lemma intvl_mult_split:
  "{p ..+ a * b} = (⋃i<b. {p + of_nat (i * a) ..+ a})"
proof cases
  assume a: "0 < a"
  note of_nat_add[simp del, symmetric, simp] of_nat_mult[simp del, symmetric, simp]
  show ?thesis using a
    apply (clarsimp simp: intvl_def, intro set_eqI iffI; clarsimp)
    subgoal for i
      by (intro bexI[of _ "i div a"] exI[of _ "i mod a"])
         (simp_all add: dme pos_mod_bound less_mult_imp_div_less ac_simps)
    subgoal for j k
      by (intro exI[of _ "j * a + k"]) (simp add: nat_index_bound)
    done
qed simp

lemma intvl_mul_disjnt:
  fixes n i :: "'a::len word"
  assumes n: "unat n < b" and i: "unat i < b" and b: "sz * b ≤ 2^LENGTH('a)"
  assumes ni: "n ≠ i"
  shows "{n * word_of_nat sz..+sz} ∩ {i * word_of_nat sz..+sz} = {}"
proof -
  { fix j l assume j: "j < sz" and l: "l < sz"
    assume "n * word_of_nat sz + word_of_nat j = i * word_of_nat sz + word_of_nat l"
    then have "(word_of_nat (unat n * sz + j) :: 'a word) = word_of_nat (unat i * sz + l)" by simp
    moreover have "unat n * sz + j < 2^LENGTH('a)"
      by (intro less_le_trans[OF nat_index_bound b] n j)
    moreover have "unat i * sz + l < 2^LENGTH('a)"
      by (intro less_le_trans[OF nat_index_bound b] i l)
    ultimately have "(unat n * sz + j) div sz = (unat i * sz + l) div sz"
      by (subst (asm) of_nat_inj) simp_all
    then have "unat n = unat i"
      using j l by simp
    with ni have False by simp }
  then show ?thesis
    by (auto simp: intvl_def)
qed

lemma array_disj_helper:
  fixes p :: "('a::mem_type['b]) ptr"
  assumes ni: "n < CARD('b)" "i < CARD('b)" "n ≠ i"
  assumes valid: "∀x∈set (array_addrs (PTR_COERCE('a['b] → 'a) p) CARD('b)). c_guard x"
  shows "{ptr_val p + word_of_nat n * word_of_nat (size_of TYPE('a))..+size_of TYPE('a)} ∩
    {ptr_val p + word_of_nat i * word_of_nat (size_of TYPE('a))..+size_of TYPE('a)} = {}"
proof -
  have [arith]: "CARD('b) ≤ size_of TYPE('a) * CARD('b)"
    using sz_nzero[where 'a='a, arith] by simp

  have "0 ∉ (⋃b<CARD('b). {ptr_val p + of_nat (b * size_of TYPE('a)) ..+ size_of TYPE('a)})"
    using valid
    apply (clarsimp simp: set_array_addrs c_guard_def c_null_guard_def)
    subgoal premises prems for b
      using prems(2-) prems(1)[rule_format, OF exI, of
        "Ptr (ptr_val p + word_of_nat b * word_of_nat (size_of TYPE('a)))" b]
      by (simp add: ptr_add_def)
    done
  then have "0 ∉ {ptr_val p ..+ size_of TYPE('a) * CARD('b)}"
    unfolding intvl_mult_split .
  from zero_not_in_intvl_no_overflow[OF this]
  have "size_of TYPE('a) * CARD('b) ≤ addr_card"
    by (simp add: addr_card)
  moreover note ni
  ultimately show ?thesis
    by (smt (verit, ccfv_SIG) ‹CARD('b) ≤ size_of TYPE('a) * CARD('b)› addr_card_len_of_conv
        intvl_disj_offset intvl_mul_disjnt order_less_le_trans unat_of_nat_len)
qed



theorem heap_abs_array_update [heap_abs]:
 "⟦ typ_heap_simulation st (r :: 's ⇒ 'a ptr ⇒ 'a) w
                   v t_hrs t_hrs_update;
    abs_expr st Pb b' b;
    abs_expr st Pn n' n;
    abs_expr st Pv y' y
  ⟧ ⟹
    abs_modifies st (λs. Pb s ∧ Pn s ∧ Pv s ∧ n' s < CARD('b) ∧
                         (∀ptr ∈ set (array_addrs (ptr_coerce (b' s)) CARD('b)). (v s ptr)))
      (λs. w (ptr_coerce (b' s) +⇩p int (n' s)) (λv. y' s)  s)
      (λs. t_hrs_update (hrs_mem_update (
              heap_update (b s) (Arrays.update ((h_val (hrs_mem (t_hrs s)) (b s))
                                 :: ('a::array_outer_max_size)['b::array_max_count]) (n s) (y s)))) s)"
  apply (clarsimp simp: abs_modifies_def abs_expr_def)
  subgoal for s
  (* rewrite heap_update of array *)
    apply (subst array_update_split
        [where st = st and t_hrs = t_hrs and t_hrs_update = t_hrs_update])
      apply assumption
     apply assumption
    apply (clarsimp simp: typ_heap_simulation_def valid_implies_cguard_def read_simulation_def write_preserves_valid_def)
    apply (drule write_simulation.write_commutes_atomic)
    apply (subst fold_cong[OF refl refl,
          where g = "λi. w  (ptr_coerce (b' (st s)) +⇩p int i) (λx.
                         if i = n' (st s) then y' (st s) else r (st s) (ptr_coerce (b' (st s)) +⇩p int i))"])
    subgoal for x 
      apply (cases "x = n' (st s)")
       apply simp
      apply (subst index_update2)
        apply simp
       apply simp
      apply (rule arg_cong[where x = "index (h_val (hrs_mem (t_hrs s)) (b' (st s))) x"])
      apply (subst heap_access_Array_element)
       apply simp
      apply (clarsimp simp: set_array_addrs)
      apply metis
      done

(* split away the indices that don't change *)
    apply (subst split_upt_on_n[where n = "n s"])
     apply simp
    apply clarsimp
    thm fold_update_id

(* [0..<n] doesn't change *)
    apply (subst fold_update_id'[where s = "st s"])
       apply assumption
      apply (clarsimp simp: CTypesDefs.ptr_add_def)
      apply (subst of_nat_mult[symmetric])+
      apply (rule array_count_index)
       apply (erule less_trans, assumption)+
     apply clarsimp

(* [Suc n..<CARD('b)] doesn't change *)
    apply (subst fold_update_id')
       apply assumption
      apply (clarsimp simp: CTypesDefs.ptr_add_def)
      apply (subst of_nat_mult[symmetric])+
      apply (erule array_count_index)
      apply assumption
     apply clarsimp
      (* index n is disjoint *)
     apply (subst pointer_lense.read_write_other[where r = r and w = w])
       apply assumption
      apply (clarsimp simp: CTypesDefs.ptr_add_def disjnt_def)
      apply (rule array_disj_helper)
         apply simp
        apply assumption
       apply simp
      apply blast
     apply (rule refl)
    apply (rule refl)
    done
  done



(* Array access, which is considerably simpler than updating. *)
lemma heap_abs_array_access[heap_abs]:
 "⟦ typ_heap_simulation st (r :: 's ⇒ ('a::xmem_type) ptr ⇒ 'a) w
                   v t_hrs t_hrs_update;
    abs_expr st Pb b' b;
    abs_expr st Pn n' n
  ⟧ ⟹
    abs_expr st (λs. Pb s ∧ Pn s ∧ n' s < CARD('b::finite) ∧ v s (ptr_coerce (b' s) +⇩p int (n' s)))
      (λs. r s (ptr_coerce (b' s) +⇩p int (n' s)))
      (λs. index (h_val (hrs_mem (t_hrs s)) (b s :: ('a['b]) ptr)) (n s))"
  apply (clarsimp simp: typ_heap_simulation_def abs_expr_def valid_implies_cguard_def read_simulation_def write_simulation_def write_preserves_valid_def)
  apply (subst heap_access_Array_element)
   apply simp
  apply (simp add: set_array_addrs)
  done


lemma the_fun_upd_lemma1:
    "(λx. the (f x))(p := v) = (λx. the ((f (p := Some v)) x))"
  by auto

lemma the_fun_upd_lemma2:
   "∃z. f p = Some z ⟹
       (λx. ∃z. (f (p := Some v)) x = Some z) =  (λx. ∃z. f x = Some z) "
  by auto

lemma the_fun_upd_lemma3:
    "((λx. the (f x))(p := v)) x = the ((f (p := Some v)) x)"
  by simp

lemma the_fun_upd_lemma4:
   "∃z. f p = Some z ⟹
       (∃z. (f (p := Some v)) x = Some z) =  (∃z. f x = Some z) "
  by simp

lemmas the_fun_upd_lemmas =
    the_fun_upd_lemma1
    the_fun_upd_lemma2
    the_fun_upd_lemma3
    the_fun_upd_lemma4


(* Used by heap_abs_syntax to simplify signed word updates. *)
lemma sword_update:
"⋀ptr :: ('a :: len) signed word ptr.
   (λ(x :: 'a word ptr ⇒ 'a word) p :: 'a word ptr.
     if ptr_coerce p = ptr then scast (n :: 'a signed word) else x (ptr_coerce p))
    =
   (λ(old :: 'a word ptr ⇒ 'a word) x :: 'a word ptr.
     if x = ptr_coerce ptr then scast n else old x)"
  by force

text ‹Proof taken from @{thm LemmaBucket_C.heap_update_Array_update}›
lemma (in array_outer_max_size) array_index_unat_conv:
  assumes x_bound: "x < CARD('b::array_max_count)"
  assumes k_bound: "k < size_of TYPE('a)"
  shows "unat (of_nat x * of_nat (size_of TYPE('a)) + (of_nat k :: addr))
                 = x * size_of TYPE('a) + k"
proof -
  have size: "CARD('b) * size_of TYPE('a ) < 2 ^ addr_bitsize"
    using array_count_size  by blast
  show ?thesis
    using size x_bound k_bound
    apply (cases "size_of TYPE('a)", simp_all)
    apply (cases "CARD('b)", simp_all)
    apply (subst unat_add_lem[THEN iffD1])
     apply (simp add: unat_word_ariths unat_of_nat less_Suc_eq_le)
     apply (subgoal_tac "Suc x * size_of TYPE('a) < 2 ^ addr_bitsize", simp_all)
     apply (erule order_le_less_trans[rotated], simp add: add_mono)
    apply (subst unat_mult_lem[THEN iffD1])
     apply (simp add: unat_of_nat unat_add_lem[THEN iffD1])
     apply (rule order_less_le_trans, erule order_le_less_trans[rotated],
            rule add_mono, simp+)
      apply (simp add: less_Suc_eq_le trans_le_add2)
     apply simp
    apply (simp add: unat_of_nat unat_add_lem[THEN iffD1])
    done
qed

lemma ptr_span_array_index_disj:
  fixes p::"('a::array_outer_max_size['b::array_max_count]) ptr"
  assumes n_bound: "n < CARD ('b)"
  assumes i_bound: "i < n"
  shows "disjnt (ptr_span (array_ptr_index p False n)) (ptr_span (array_ptr_index p False i))"
  using n_bound i_bound
  apply (clarsimp simp add: array_ptr_index_def ptr_add_def intvl_def disjnt_def)
  apply (intro set_eqI)
  apply clarsimp
  apply (drule word_unat.Rep_inject[THEN iffD2])
  apply (clarsimp simp: array_index_unat_conv [where 'b='b] nat_eq_add_iff1)
  by (metis mult.commute nat_index_bound not_add_less1)

lemma ptr_span_array_ptr_index_disj:
  fixes p::"('a::array_outer_max_size['b::array_max_count]) ptr"
  fixes q::"('a['b::array_max_count]) ptr"
  assumes n_bound: "n < CARD ('b)"
  assumes m_bound: "m < CARD ('b)"
  assumes disj:"disjnt (ptr_span p) (ptr_span q)"
  shows "disjnt (ptr_span (array_ptr_index p False n)) (ptr_span (array_ptr_index q False m))"
proof (rule ccontr)
  assume "¬disjnt (ptr_span (array_ptr_index p False n)) (ptr_span (array_ptr_index q False m))"

  then obtain k k' where
    k_bound: "k < size_of TYPE('a)" and
    k'_bound: "k' < size_of TYPE('a)" and
    eq: "ptr_val p + word_of_nat n * word_of_nat (size_of TYPE('a)) + word_of_nat k =
         ptr_val q + word_of_nat m * word_of_nat (size_of TYPE('a)) + word_of_nat k'"
    by (auto simp add: intvl_def array_ptr_index_def ptr_add_def disjnt_def)

  define i where "i = unat ((word_of_nat n::addr) * word_of_nat (size_of TYPE('a)) + word_of_nat k)"
  have i_bound: "i < CARD('b) * size_of TYPE('a)"
    using n_bound k_bound
    by(simp add: i_def array_index_unat_conv [OF n_bound k_bound]  mult.commute nat_index_bound)

  define j where "j = unat ((word_of_nat m::addr) * word_of_nat (size_of TYPE('a)) + word_of_nat k')"
  have j_bound: "j < CARD('b) * size_of TYPE('a)"
    using m_bound k'_bound
    by(simp add: j_def array_index_unat_conv [OF m_bound k'_bound]  mult.commute nat_index_bound)

  from i_bound j_bound disj have "ptr_val p + word_of_nat i ≠ ptr_val q + word_of_nat j"
    by (auto simp add: intvl_def disjnt_def)
  with eq show False
    by (simp add: i_def j_def add.commute add.left_commute)
qed

named_theorems select_conv and select_conv_independent and valid_conv and valid_array_conv and
  gen_update_commute and gen_outer_update_commute and update_commute

locale pointer_array_lense = pointer_lense r w
  for r:: "'s ⇒ 'a:: array_outer_max_size ptr ⇒ 'a"
  and w:: "'a ptr ⇒ ('a ⇒ 'a) ⇒ 's ⇒ 's"
begin

definition heap_array  ::"'s ⇒ ('a['b::array_max_count]) ptr ⇒ 'a['b]"  where
"heap_array s p = FCP (λi. r s (array_ptr_index p False i))"

lemmas [read_stack_byte_ZERO_step_subst] = heap_array_def

definition heap_array_map :: "('a['b]) ptr ⇒ ('a['b::array_max_count] ⇒ 'a['b]) ⇒  's ⇒ 's" where
"heap_array_map p f s ≡
  fold (λi. w (array_ptr_index p False i) (λ_. (f (heap_array s p)).[i])) [0..<CARD('b)] s"

lemma element_heap_eq_heap_array_eq [select_conv]: "r s = r s' ⟹ heap_array s = heap_array s'"
  apply (rule ext)
  apply (simp add: heap_array_def)
  done

lemma fold_write_independent_field:
  fixes p::"('a['b::array_max_count]) ptr"
  assumes field_independent: "(⋀p x s. f (w p (λ_. x) s) = f s)"
  assumes n_bound: "n ≤ CARD('b)"
  shows "f (fold (λi. w (array_ptr_index p False i) (λ_. g (heap_array s p).[i])) [0..<n] t) = f t"
  using n_bound
proof (induct n arbitrary: t)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case using field_independent
    by simp
qed


lemma heap_array_map_independent_field [select_conv_independent]:
  assumes field_independent: "(⋀p x s. f (w p (λ_. x) s) = f s)"
  shows "f (heap_array_map p g s) = f s"
  apply (simp add: heap_array_map_def)
  apply (rule fold_write_independent_field)
   apply (rule field_independent)
  apply simp
  done

lemma fold_write_independent_field_upd_commute:
  fixes p::"('a['b::array_max_count]) ptr"
  assumes write_commute: "⋀p x s. (f_upd (w p (λ_. x) s)) = w p (λ_. x) (f_upd s)"
  assumes n_bound: "n ≤ CARD('b)"
  shows "f_upd (fold (λi. w (array_ptr_index p False i) (λ_. g (heap_array s p).[i])) [0..<n] t) =
          fold (λi. w  (array_ptr_index p False i) (λ_. g (heap_array s p).[i])) [0..<n] (f_upd t)"
  using n_bound
proof (induct n arbitrary: t)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case using write_commute
    by simp
qed

lemma heap_array_map_independent_field_commute [gen_update_commute]:
  assumes read_independent: "⋀s. r (f_upd s) = r s"
  assumes write_independent: "⋀p x s. (f_upd (w p (λ_. x) s)) = w p (λ_. x) (f_upd s)"
  shows "f_upd (heap_array_map p g s) = (heap_array_map p g (f_upd s))"
  apply (simp add: heap_array_map_def element_heap_eq_heap_array_eq [OF read_independent])
  apply (rule fold_write_independent_field_upd_commute)
  apply (rule write_independent)
  apply simp
  done

lemma heap_array_index[simp]: "i < CARD('b) ⟹
  heap_array s (p::('a['b::array_max_count]) ptr).[i] = r s (array_ptr_index p False i)"
  by (simp add: heap_array_def)

lemma read_write_same_fold_aux:
  fixes p::"('a['b::array_max_count]) ptr"
  assumes n_bound: "n ≤ CARD ('b)"
  assumes i_bound: "i < n"
  shows "r (fold (λi. w (array_ptr_index p False i) (λ_. f (heap_array s p).[i])) [0..<n] s) (array_ptr_index p False i) = f (heap_array s p).[i]"
  using n_bound i_bound
proof (induct n arbitrary: i s)
  case 0
  then show ?case by simp
next
  case (Suc n)
  from Suc.prems obtain i_bound: "i < Suc n" and Suc_n_bound: "Suc n ≤ CARD ('b)" and
    n_bound: "n ≤ CARD('b)" and n_bound': "n < CARD('b)" by auto
  have size: "CARD('b) * size_of TYPE('a ) < 2 ^ addr_bitsize"
    using Padding_Equivalence.array_count_size by blast
  show ?case
  proof (cases "i=n")
    case True
    show ?thesis
      apply (simp add: True)
      apply (simp add: read_write_same)
      done
  next
    case False
    from False i_bound have i_bound': "i < n" by simp
    have disj: "disjnt (ptr_span (array_ptr_index p False n)) (ptr_span (array_ptr_index p False i))"
      by (rule ptr_span_array_index_disj [OF n_bound' i_bound'])
    show ?thesis
      apply (simp add: False)
      apply (simp add: read_write_other disj )
      apply (rule Suc.hyps [OF n_bound i_bound'])
      done
  qed
qed

lemma array_read_write_same: "heap_array (heap_array_map p f s) p = f (heap_array s p)"
  apply (subst cart_eq )
  apply clarsimp
  apply (simp add: heap_array_map_def)
  apply (rule read_write_same_fold_aux)
  by simp_all

lemma read_write_other_fold_aux:
  fixes p::"('a['b::array_max_count]) ptr"
  fixes p'::"('a['b::array_max_count]) ptr"
  assumes n_bound: "n ≤ CARD ('b)"
  assumes i_bound: "i < CARD ('b)"
  assumes disj:"disjnt (ptr_span p) (ptr_span p')"
  shows "r (fold (λi. w (array_ptr_index p False i) (λ_. f (heap_array s p).[i])) [0..<n] s) (array_ptr_index p' False i) =
         r s (array_ptr_index p' False i)"
  using n_bound i_bound
proof (induct n arbitrary: i s)
  case 0
  then show ?case by simp
next
  case (Suc n)
  from Suc.prems obtain  Suc_n_bound: "Suc n ≤ CARD ('b)" and
    n_bound: "n ≤ CARD('b)" and n_bound': "n < CARD('b)" and
    i_bound: "i < CARD('b)" by auto
  have size: "CARD('b) * size_of TYPE('a ) < 2 ^ addr_bitsize"
    using Padding_Equivalence.array_count_size by blast

  from ptr_span_array_ptr_index_disj [OF n_bound' i_bound disj]
  show ?case
    apply (simp add: read_write_other)
    apply (rule Suc.hyps [OF n_bound i_bound])
    done
qed

lemma array_read_write_other:
  fixes p::"('a['b::array_max_count]) ptr"
  fixes p'::"('a['b::array_max_count]) ptr"
  assumes disj:"disjnt (ptr_span p) (ptr_span p')"
  shows "heap_array (heap_array_map p f s) p' = heap_array s p'"
  apply (subst cart_eq )
  apply clarsimp
  apply (simp add: heap_array_map_def)
  apply (rule read_write_other_fold_aux [OF _ _ disj])
  by simp_all

lemma write_cong_fold_aux:
  fixes p::"('a['b::array_max_count]) ptr"
  assumes f_f': "f (heap_array s p) = f' (heap_array s p)"
  assumes n_bound: "n ≤ CARD('b)"
  shows "fold (λi. w (array_ptr_index p False i) (λ_. f (heap_array s p).[i])) [0..<n] s =
    fold (λi. w (array_ptr_index p False i) (λ_. f' (heap_array s p).[i])) [0..<n] s"
  using n_bound
proof (induct n arbitrary:)
  case 0
  then show ?case by simp
next
  case (Suc n)
  have suc_n_bound: "Suc n ≤ CARD('b)" using Suc.prems .

  define s' where "s' = (fold (λi. w (array_ptr_index p False i) (λ_. f' (heap_array s p).[i])) [0..<n] s)"

  from f_f' suc_n_bound
  have "(λ_. f (heap_array s p).[n]) =  (λ_. f' (heap_array s p).[n])"
    by auto
  hence eq: "(λ_. f (heap_array s p).[n]) (r s' (array_ptr_index p False n)) =
            (λ_. f' (heap_array s p).[n]) (r s' (array_ptr_index p False n))" by metis
  from Suc show ?case by (simp add: write_cong [OF eq])
qed


lemma array_write_cong:
  fixes p::"('a['b::array_max_count]) ptr"
  assumes eq: "f (heap_array s p) = f' (heap_array s p)"
  shows "heap_array_map p f s = heap_array_map p f' s"
  apply (simp add: heap_array_map_def)
  apply (rule write_cong_fold_aux)
  apply (rule eq)
  apply simp
  done

lemma array_write_same_triv[simp]:
  fixes p::"('a['b::array_max_count]) ptr"
  shows "heap_array_map p (λ_. f (heap_array s p)) s = heap_array_map p f s"
  using array_write_cong by fastforce

lemma array_write_fold_same_aux:
  fixes p::"('a['b::array_max_count]) ptr"
  assumes f_id: "f (heap_array s p) = heap_array s p"
  assumes n_bound: "n ≤ CARD('b)"
  shows "fold (λi. w (array_ptr_index p False i) (λ_. f (heap_array s p).[i])) [0..<n] s = s"
  using n_bound
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  from Suc.prems f_id
  have f_n_id: "f (heap_array s p).[n] = r s (array_ptr_index p False n)"
    by simp
  from Suc show ?case
    by (simp add: write_same f_n_id)
qed

lemma array_write_same:
  fixes p::"('a['b::array_max_count]) ptr"
  assumes f_id: "f (heap_array s p) = heap_array s p"
  shows "heap_array_map p f s = s"
  apply (simp add: heap_array_map_def)
  apply (rule array_write_fold_same_aux)
   apply (rule f_id)
  by simp

lemma array_write_triv [simp]:
  fixes p::"('a['b::array_max_count]) ptr"
  shows "heap_array_map p (λ_. heap_array s p) s = s" and "heap_array_map p (λx. x) s = s"
  by (simp_all add: array_write_same)



lemma write_fold_other_commute:
  fixes p::"nat ⇒ 'a ptr"
  and q:: "'a ptr"
assumes disj: "⋀i. i < n ⟹ disjnt (ptr_span q) (ptr_span (p i))"
  shows
  "w q f  (fold (λi. w (p i) (g i)) [0..<n] s) =
   fold (λi. w (p i) (g i) ) [0..<n] (w q f s)"
  using disj
proof (induct n arbitrary: s)
  case 0
  then show ?case by simp
next
  case (Suc n)
  from Suc.prems obtain
    q_n_disj: "disjnt (ptr_span q) (ptr_span (p n))" and
    disj': "⋀i. i < n ⟹ disjnt (ptr_span q) (ptr_span (p i))" by auto

  note n_commute =  write_other_commute[OF q_n_disj, symmetric]
  show ?case
    apply simp
    apply (subst n_commute)
    apply (subst Suc.hyps [OF disj'])
    apply (simp_all)
    done
qed

lemma write_fold_arr_commute:
  fixes p::"('a['b::array_max_count]) ptr"
  and arr:: "'a['b::array_max_count]"
assumes n_bound: "n < CARD('b)"
  shows
  "w (array_ptr_index p False n) (λ_. arr.[n])
    (fold (λi. w (array_ptr_index p False i) (λ_. arr.[i]))
       [0..<n] s) =
   fold
       (λi. w (array_ptr_index p False i) (λ_. arr.[i]))
       [0..<n] ( w (array_ptr_index p False n)  (λ_. arr.[n]) s)"
  apply (rule write_fold_other_commute)
  using n_bound
  by (simp add: ptr_span_array_index_disj)



lemma array_fold_fuse_aux:
  fixes p::"('a['b::array_max_count]) ptr"
  fixes f::"'a['b] ⇒ 'a['b]"
  fixes g::"'a['b] ⇒ 'a['b]"
  assumes n_bound: "n ≤ CARD('b)"
  shows "fold
     (λi. w (array_ptr_index p False i) (λ_. f (g (heap_array s p)).[i]))
     [0..<n]
     (fold
       (λi. w (array_ptr_index p False i) (λ_. g (heap_array s p).[i]))
       [0..<n] t) =
    fold
     (λi. w (array_ptr_index p False i) (λ_. f (g (heap_array s p)).[i]))
     [0..<n] t"
  using n_bound
proof (induct n arbitrary: t)
  case 0
  then show ?case by simp
next
  case (Suc n)
  from Suc.prems have n_bound: "n ≤ CARD('b)" and n_bound': "n < CARD('b)"
    by auto
    show ?case
      apply (simp add: )

      apply (subst (2) write_fold_arr_commute [OF n_bound'])
      apply (subst Suc.hyps [OF n_bound])
      apply (subst  write_fold_arr_commute [OF n_bound'])
      apply (subst write_comp)
      apply (subst (1) write_fold_arr_commute [OF n_bound'])
      by (meson comp_apply)
qed




lemma array_write_comp:
  fixes p::"('a['b::array_max_count]) ptr"
  shows "heap_array_map p f (heap_array_map p g s) = heap_array_map p (f o g) s"
proof -
  from  array_read_write_same [of p g s]
  have g_eq: "heap_array (heap_array_map p g s) p = g (heap_array s p)".
  show ?thesis
    apply (subst (1 3) heap_array_map_def)
    apply (simp add: g_eq)
    apply (subst (1) heap_array_map_def)
    apply (rule array_fold_fuse_aux)
    by simp
qed

lemma fold_fold_other_commute:
  fixes p::"nat ⇒ 'a ptr"
  and q:: "nat ⇒ 'a ptr"
assumes disj: "⋀i j. i < n ⟹ j < m ⟹ disjnt (ptr_span (p i)) (ptr_span (q j))"
  shows
  "fold (λi. w (p i) (f i)) [0..<n] (fold (λi. w (q i) (g i)) [0..<m] s) =
   fold (λi. w (q i) (g i)) [0..<m] (fold (λi. w (p i) (f i)) [0..<n] s)"
  using disj
proof (induct n arbitrary: m s)
  case 0
  then show ?case by simp
next
  case (Suc n)
  from Suc.prems obtain
    disj': "⋀i j. i < n ⟹ j < m ⟹ disjnt (ptr_span (p i)) (ptr_span (q j))" and
    m_disj: "⋀j. j < m ⟹ disjnt (ptr_span (p n)) (ptr_span (q j))"  by auto
  show ?case
    apply simp
    apply (subst  write_fold_other_commute [OF m_disj, symmetric])
    apply assumption
    apply (subst Suc.hyps [OF disj'])
      apply assumption
     apply assumption
    apply (rule refl)
    done
qed


lemma array_write_other_commute:
  fixes p::"('a['b::array_max_count]) ptr"
  fixes q::"('a['b::array_max_count]) ptr"
  assumes disj: "disjnt (ptr_span p) (ptr_span q)"
  shows "heap_array_map q g (heap_array_map p f s) = heap_array_map p f (heap_array_map q g s)"
proof -
  from array_read_write_other [OF disj]
  have g_eq: "g (heap_array (heap_array_map p f s) q) = g (heap_array s q)" by simp

  from  array_read_write_other disj
  have f_eq: "f (heap_array (heap_array_map q g s) p) = f (heap_array s p)"
    by (metis Int_commute disjnt_def)

  show ?thesis
    apply (subst (1 3) heap_array_map_def)
    apply (simp add: g_eq f_eq)
    apply (simp add: heap_array_map_def)
    apply (rule fold_fold_other_commute)
    using disj
    by (metis Int_commute ptr_span_array_ptr_index_disj disjnt_def)
qed

sublocale array: pointer_lense heap_array heap_array_map
  apply (unfold_locales)
      apply (rule array_read_write_same)
    apply (rule array_write_same, assumption)
   apply (rule array_write_comp)
  apply (rule array_write_other_commute, assumption)
  done

end

locale pointer_two_dimensional_array_lense = pointer_array_lense r w
  for r:: "'s ⇒ 'a:: array_inner_max_size ptr ⇒ 'a"
  and w:: "'a ptr ⇒ ('a ⇒ 'a) ⇒ 's ⇒ 's"
begin
sublocale outer: pointer_array_lense heap_array heap_array_map
  by (intro_locales)

lemmas outer.heap_array_map_independent_field_commute [gen_outer_update_commute]

end

locale valid_array_base =
  fixes vgetter:: "('t ⇒ 'a::array_outer_max_size ptr ⇒ bool)"
begin

definition valid_array ::"'t ⇒ ('a['b::array_max_count]) ptr ⇒ bool" where
 [valid_array_defs]: "valid_array s p = (∀i < CARD('b). vgetter s (array_ptr_index p False i))"

lemma element_vgetter_eq_valid_array_eq [valid_array_conv]: "vgetter s = vgetter s' ⟹ valid_array s = valid_array s'"
  apply (rule ext)
  apply (simp add: valid_array_def)
  done

end

locale valid_pointer_array_lense = pointer_array_lense r w +
  valid_array_base vgetter +
  write_preserves_valid vgetter w
  for r:: "'s ⇒ 'a:: array_outer_max_size ptr ⇒ 'a"
  and w:: "'a ptr ⇒ ('a ⇒ 'a) ⇒ 's ⇒ 's"
  and vgetter:: "('s ⇒ 'a ptr ⇒ bool)"
begin

lemma setter_fold_keeps_vgetter:
  fixes p':: "('a['b::array_max_count]) ptr"
  fixes p:: "'a ptr"
  assumes n_bound: "n ≤ CARD('b)"
  shows  "vgetter (fold (λi. w (array_ptr_index p' False i) (λ_. f (heap_array s p').[i])) [0..<n] s) p = vgetter s p"
  using n_bound
proof (induct n arbitrary: s)
  case 0
  then show ?case by (simp )
next
  case (Suc n)
  from Suc.prems obtain
    suc_n_bound: "Suc n ≤ CARD('b)" and
    n_bound: "n ≤ CARD('b)" by auto
  show ?case
    apply simp
    apply (rule Suc.hyps [OF n_bound])
    done
qed

lemma heap_array_map_keeps_vgetter:
  fixes p:: "('a['b::array_max_count]) ptr"
  fixes p':: "('a['b]) ptr"
  shows "valid_array (heap_array_map p' f s) p = valid_array s p"
  by (clarsimp simp add: valid_array_def heap_array_map_def setter_fold_keeps_vgetter)

sublocale array: write_preserves_valid valid_array heap_array_map
  apply (unfold_locales)
  apply (rule heap_array_map_keeps_vgetter)
  done

lemma heap_array_map_keeps_vgetter_element[simp]:
  fixes p':: "('a['b::array_max_count]) ptr"
  shows "vgetter (heap_array_map p' f s) = vgetter s"
  apply (rule ext)
  by (simp add: heap_array_map_def setter_fold_keeps_vgetter)

lemma getter_keeps_valid_array[simp]:
  fixes p':: "'a ptr"
  shows "(valid_array::'s ⇒ ('a['b::array_max_count]) ptr ⇒ bool) (w p' f s) = valid_array s"
  apply (rule ext)
  by (simp add: valid_array_def)

lemma getter_keeps_valid_array_pointwise[]:
  fixes p':: "'a ptr"
  fixes p :: "('a['b::array_max_count]) ptr"
  shows "(valid_array::'s ⇒ ('a['b::array_max_count]) ptr ⇒ bool) (w p' f s) p = valid_array s p"
  by (simp add: valid_array_def)
end


locale valid_pointer_two_dimensional_array_lense = pointer_two_dimensional_array_lense r w +
  valid_array_base vgetter +
  write_preserves_valid vgetter w
  for r:: "'s ⇒ 'a:: array_inner_max_size ptr ⇒ 'a"
  and w:: "'a ptr ⇒ ('a ⇒ 'a) ⇒ 's ⇒ 's"
  and vgetter:: "('s ⇒ 'a ptr ⇒ bool)"
begin
sublocale inner: valid_pointer_array_lense r w vgetter
  by (intro_locales)

sublocale outer: valid_pointer_array_lense heap_array heap_array_map valid_array
  by (intro_locales)

end

locale array_typ_heap_simulation =
  lense t_hrs t_hrs_update +
  read_simulation st v r t_hrs +
  write_simulation t_hrs t_hrs_update st v w +
  write_preserves_valid v w +
  valid_implies_cguard st v +
  valid_only_typ_desc_dependent t_hrs st v +
  pointer_array_lense r w +
  valid_array_base v
  for
    st:: "'s ⇒ 't" and
    r:: "'t ⇒ 'a::array_outer_max_size ptr ⇒ 'a" and
    w:: "'a ptr ⇒ ('a ⇒ 'a) ⇒ 't ⇒ 't" and
    v:: "'t ⇒ 'a ptr ⇒ bool" and
    t_hrs :: "'s ⇒ heap_raw_state" and
    t_hrs_update:: "(heap_raw_state ⇒ heap_raw_state) ⇒ 's ⇒ 's"
begin

sublocale typ_heap_simulation
  by (intro_locales)

sublocale valid_pointer_array_lense r w v
  by (intro_locales)

lemmas typ_heap_simulation = typ_heap_simulation_axioms


lemma valid_array_implies_safe: "valid_array (st s) p ⟹ c_guard p"
  using valid_implies_c_guard
  apply (simp add: valid_array_def)
  by (metis TypHeapSimple.c_guard_array_c_guard array_ptr_index_simps(1))

lemma heap_array_data_correct:
  assumes valid_arr: "valid_array (st s) p"
  shows "heap_array (st s) p = h_val (hrs_mem (t_hrs s)) p"
  apply (subst cart_eq)
  apply clarsimp
  apply (subst  heap_access_Array_element')
   apply simp
  using read_commutes valid_arr
  by (auto simp add: valid_array_def)

lemma write_fold_commutes:
  fixes p:: "('a['b::array_max_count]) ptr"
  assumes n_bound: "n ≤ CARD('b)"
  assumes valid: "valid_array (st s) p"
  shows "st (t_hrs_update (hrs_mem_update (fold (λi. heap_update (array_ptr_index p False i) (x.[i])) [0..<n])) s) =
    fold (λi. w (array_ptr_index p False i) (λ_. x.[i])) [0..<n] (st s)"
  using n_bound valid
proof (induct n arbitrary: s)
  case 0
  then show ?case
    by simp
next
  case (Suc n)
  from Suc.prems obtain  suc_n_bound: "Suc n ≤ CARD('b)" and n_bound: "n ≤ CARD('b)" and n_bound': "n < CARD('b)"
    and valid: "valid_array (st s) p" by auto

  have vgetter: "v (st (t_hrs_update (hrs_mem_update (fold (λi. heap_update (array_ptr_index p False i) (x.[i])) [0..<n])) s))
    (array_ptr_index p False n)"
    apply (subst Suc.hyps [OF n_bound valid] )
    apply (subst setter_fold_keeps_vgetter [OF n_bound])
    using valid n_bound' apply (simp add: valid_array_def)
    done
  show ?case
    apply simp
    apply (subst Suc.hyps[OF n_bound valid, symmetric])
    apply (subst write_commutes[symmetric])
     apply (rule vgetter)
    by (simp add: hrs_mem_update_def split_def comp_def)
qed

lemma heap_array_map_commutes:
  fixes p:: "('a['b::array_max_count]) ptr"
  assumes valid: "valid_array (st s) p"
  shows "st (t_hrs_update (hrs_mem_update (heap_update p x)) s) = heap_array_map p (λ_. x) (st s)"
proof -
  from valid_array_implies_safe [OF valid] have cgrd: "c_guard p" .
  show ?thesis
    apply (simp add: heap_array_map_def heap_update_array_pointless [OF cgrd])
    apply (rule write_fold_commutes)
    apply simp
    apply (rule valid)
    done
qed


lemma write_padding_fold_commutes:
  fixes p:: "('a['b::array_max_count]) ptr"
  assumes n_bound: "n ≤ CARD('b)"
  assumes valid: "valid_array (st s) p"
  assumes lbs: "length bs = CARD('b) * size_of TYPE('a)"
  shows "st (t_hrs_update
         (hrs_mem_update
           (fold
             (λi. heap_update_padding (array_ptr_index p False i) (x.[i])
                    (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs)))
             [0..<n]))
         s) =
    fold (λi. w (array_ptr_index p False i) (λ_. x.[i])) [0..<n] (st s)"
  using n_bound valid
proof (induct n arbitrary: s)
  case 0
  then show ?case
    by simp
next
  case (Suc n)
  from Suc.prems obtain  suc_n_bound: "Suc n ≤ CARD('b)" and n_bound: "n ≤ CARD('b)" and n_bound': "n < CARD('b)"
    and valid: "valid_array (st s) p" by auto

  from lbs suc_n_bound
  have lbs': "length (take (size_of TYPE('a)) (drop (n * size_of TYPE('a)) bs)) = size_of TYPE('a)"
    by (auto simp add: less_le_mult_nat nat_move_sub_le)


  have vgetter: "v (st (t_hrs_update
            (hrs_mem_update
              (λh. fold (λi. heap_update_padding (array_ptr_index p False i) (x.[i])
                               (take (size_of TYPE('a)) (drop (i * size_of TYPE('a)) bs)))
                     [0..<n] h))
            s))
     (array_ptr_index p False n)"
    apply (subst Suc.hyps [OF n_bound valid] )

    apply (subst setter_fold_keeps_vgetter [OF n_bound])
    using valid n_bound' apply (simp add: valid_array_def)
    done

  show ?case apply simp
    apply (subst Suc.hyps[OF n_bound valid, symmetric])

    apply (subst write_padding_commutes[where bs = ‹take (size_of TYPE('a)) (drop (n * size_of TYPE('a)) bs)›, OF vgetter lbs', symmetric])
    apply simp
    apply (simp only: hrs_mem_update_comp)
    apply (simp only: comp_def)
    done
qed


lemma heap_array_padding_map_commutes:
  fixes p:: "('a['b::array_max_count]) ptr"
  assumes valid: "valid_array (st s) p"
  assumes bound: "length bs = size_of TYPE('a['b])"
  shows "st (t_hrs_update (hrs_mem_update (heap_update_padding p x bs)) s) = heap_array_map p (λ_. x) (st s)"
proof -
  from valid_array_implies_safe [OF valid] have cgrd: "c_guard p" .
  from bound have bound': "length bs = CARD('b) * size_of TYPE('a)"
    by auto
  show ?thesis
    apply (simp add: heap_array_map_def heap_update_padding_array_pointless [OF cgrd bound'])
    apply (simp add: write_padding_fold_commutes [OF _ valid bound'])
    done
qed


lemma array_valid_same_typ_desc:
  fixes p:: "('a['b::array_max_count]) ptr"
  assumes typ_eq: "hrs_htd (t_hrs s) = hrs_htd (t_hrs t)"
  shows "valid_array (st s) p = valid_array (st t) p"
  apply (simp add: valid_array_def)
  using typ_eq valid_same_typ_desc by blast

sublocale array: typ_heap_simulation st heap_array heap_array_map valid_array t_hrs t_hrs_update
  apply (unfold_locales)
     apply (rule heap_array_data_correct, assumption)
    apply (rule heap_array_padding_map_commutes, assumption, assumption)
   apply (rule valid_array_implies_safe, assumption)
  apply (rule array_valid_same_typ_desc, assumption)
  done

end

locale two_dimensional_array_typ_heap_simulation =
  lense t_hrs t_hrs_update +
  read_simulation st v r t_hrs +
  write_simulation t_hrs t_hrs_update st v w  +
  write_preserves_valid v w +
  valid_implies_cguard st v +
  valid_only_typ_desc_dependent t_hrs st v +
  pointer_two_dimensional_array_lense r w
  for
    st:: "'s ⇒ 't" and
    r:: "'t ⇒ 'a::array_inner_max_size ptr ⇒ 'a" and
    w:: "'a ptr  ⇒ ('a ⇒ 'a) ⇒ 't ⇒ 't" and
    v:: "'t ⇒ 'a ptr ⇒ bool" and
    t_hrs :: "'s ⇒ heap_raw_state" and
    t_hrs_update:: "(heap_raw_state ⇒ heap_raw_state) ⇒ 's ⇒ 's"
begin

sublocale inner: array_typ_heap_simulation st r w v t_hrs t_hrs_update
  by (intro_locales)

lemmas inner_typ_heap_simulation = inner.typ_heap_simulation

sublocale outer: array_typ_heap_simulation st heap_array heap_array_map inner.valid_array t_hrs t_hrs_update
  by (intro_locales)

lemmas outer_typ_heap_simulation = outer.typ_heap_simulation


end

lemma root_ptr_valid_field_lvalue:
  fixes p::"'a::mem_type ptr"
  fixes q:: "'b::mem_type ptr"
  assumes root_p: "root_ptr_valid d p"
  assumes root_q: "root_ptr_valid d q"
  assumes fl: "field_lookup (typ_info_t TYPE('b)) f 0 = Some (t, k)"
  assumes other: "typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE('b)"
  shows "ptr_val p = &(q→f) ⟷ False"
proof
  assume p: "ptr_val p = &(q→f)"
  from field_tag_sub [OF fl] have "{&(q→f)..+size_td t} ⊆ ptr_span q".
  moreover
  from root_ptr_valid_cases [OF root_p root_q] other have "ptr_span p ∩ ptr_span q = {}" by blast
  ultimately
  show False
    using p
     by (metis (mono_tags, lifting) disjoint_iff field_lookup_wf_size_desc_gt fl intvl_inter
        intvl_start_inter mem_type_self subset_iff wf_size_desc)
qed simp

lemma root_ptr_valid_field_lvalue':
  fixes q:: "'b::mem_type ptr"
  assumes root_p: "root_ptr_valid d (PTR ('a::mem_type)(&(q→f)))"
  assumes root_q: "root_ptr_valid d q"
  assumes fl: "field_lookup (typ_info_t TYPE('b)) f 0 = Some (t, k)"
  assumes other: "typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE('b)"
  shows "False"
  using root_ptr_valid_field_lvalue [OF root_p root_q fl other]
  by simp


lemma root_ptr_valid_array_ptr_index_dim1:
  fixes q:: "('a::array_outer_max_size['c::array_max_count]) ptr"
  assumes root_p: "root_ptr_valid d (array_ptr_index q False i)"
  assumes root_q: "root_ptr_valid d q"
  assumes other: "typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE('a['c])"
  assumes i_bound: "i < CARD('c)"
  shows "False"
proof -
  from field_lookup_array [OF i_bound]
  obtain t k where
    fl: "field_lookup (typ_info_t TYPE('a['c])) [replicate i (CHR ''1'')] 0 = Some (t, k)"
    by blast
  from root_ptr_valid_field_lvalue [OF root_p root_q fl other] i_bound
  show ?thesis
    by (simp add: array_ptr_index_field_lvalue_conv)
qed


lemma root_ptr_valid_field_lvalue_array_ptr_index_dim1:
  fixes q:: "'b::mem_type ptr"
  assumes root_p: "root_ptr_valid d (array_ptr_index (PTR('a['c]) &(q→f)) False i)"
  assumes root_q: "root_ptr_valid d q"
  assumes other: "typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE('b)"
  assumes i_bound: "i < CARD('c)"
  assumes fl: "field_lookup (typ_info_t TYPE('b)) f 0 = Some (t, k)"
  assumes t: "export_uinfo t = typ_uinfo_t (TYPE('a::array_outer_max_size['c::array_max_count]))"
  shows False
proof -
  from field_lookup_array [OF i_bound]
  obtain s n where
    fl_i: "field_lookup (typ_info_t TYPE('a['c])) [replicate i (CHR ''1'')] k = Some (s, n)"
    by blast

  from fl_i t obtain s' n' where
    fl_i': "field_lookup t [replicate i (CHR ''1'')] k = Some (s', n')"
    by (metis (no_types, lifting) Padding_Equivalence.field_lookup_export_uinfo_Some_rev
        field_lookup_export_uinfo_Some fold_typ_uinfo_t)

  from field_lookup_prefix_Some''(1)[rule_format, where f="f" and g="[replicate i CHR ''1'']"
    and m=0, OF fl]
  have fl_app: "field_lookup (typ_info_t TYPE('b)) (f @ [replicate i CHR ''1'']) 0 = Some (s', n')"
    by (simp add: fl_update fl_i')
  have conv: "&(PTR('a['c]) &(q→f)→[replicate i CHR ''1'']) = &(q→f @[replicate i CHR ''1''] )"
    apply (subst field_lvalue_append)
       apply simp_all
      apply (rule field_lookup_field_ti')
      apply (rule fl)
     apply (simp add: typ_uinfo_t_def i_bound t)
    apply (rule field_lookup_field_ti')
    apply (rule field_lookup_array [OF i_bound])
    done

  from root_ptr_valid_field_lvalue [OF root_p root_q fl_app other] show False
    by (simp add: array_ptr_index_field_lvalue_conv i_bound conv)
qed

lemma root_ptr_valid_field_lvalue_array_ptr_index_dim1':
  fixes q:: "'b::mem_type ptr"
  assumes root_p: "root_ptr_valid d (array_ptr_index (PTR(('a::array_outer_max_size['c::array_max_count])) &(q→f)) False i)"
  assumes root_q: "root_ptr_valid d q"
  assumes other: "typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE('b)"
  assumes i_bound: "i < CARD('c)"
  assumes fl: "field_lookup (typ_info_t TYPE('b)) f 0 = Some (adjust_ti (typ_info_t (TYPE('a['c]))) acc upd, k)"
  assumes fg: "fg_cons acc upd"
  shows "False"
  using root_ptr_valid_field_lvalue_array_ptr_index_dim1 [OF root_p root_q other i_bound fl]
  by (simp add: fg)

lemma root_ptr_valid_array_ptr_index_dim2:
  fixes q:: "(('a::array_inner_max_size['c::array_max_count])['d::array_max_count]) ptr"
  assumes root_p: "root_ptr_valid d (array_ptr_index (array_ptr_index q False i) False j)"
  assumes root_q: "root_ptr_valid d q"
  assumes other: "typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE('a['c]['d])"
  assumes i_bound: "i < CARD('d)"
  assumes j_bound: "j < CARD('c)"
  shows "False"
proof -
  from field_lookup_array [OF i_bound, of 0, where 'a="'a['c]"]
  have fl_i: "field_lookup (typ_info_t TYPE(('a['c])['d])) [replicate i CHR ''1''] 0 =
                Some (adjust_ti (typ_info_t TYPE('a['c])) (λx. x.[i]) (λx f. Arrays.update f i x),
                 i * size_of TYPE('a['c]))" by simp
  from field_lookup_array [OF j_bound, of "i * size_of TYPE('a['c])", where 'a="'a"]
  have fl_j: "field_lookup (typ_info_t TYPE('a['c])) [replicate j CHR ''1''] (i * size_of TYPE('a['c])) =
               Some (adjust_ti (typ_info_t TYPE('a)) (λx. x.[j]) (λx f. Arrays.update f j x),
                i * size_of TYPE('a['c]) + j * size_of TYPE('a))" by simp

  have append: "&(PTR('a['c]) &(q→[replicate i CHR ''1''])→[replicate j CHR ''1'']) =
                  &(q→[replicate i CHR ''1'', replicate j CHR ''1''])"
    apply (subst field_lvalue_append)
       apply simp_all
      apply (rule field_lookup_field_ti')
      apply (rule fl_i)
     apply (simp add: typ_uinfo_t_def i_bound)
    apply (rule field_lookup_field_ti')
    apply (rule field_lookup_array [OF j_bound])
    done

  have sz_eq: "size_of TYPE('a['c]) = (CARD('c) * size_of TYPE('a))"
    using size_of_array by blast
  from field_lookup_prefix_Some''(1)[rule_format, where f="[replicate i CHR ''1'']" and g="[replicate j CHR ''1'']"
   and t =  "(typ_info_t TYPE(('a['c])['d]))" and m=0, OF fl_i]
  obtain t k
    where fl: "field_lookup (typ_info_t TYPE('a['c]['d])) [replicate i CHR ''1'', replicate j CHR ''1''] 0 = Some (t, k)"
    apply (simp add: i_bound)
    apply (simp add: fl_update sz_eq  )
    using fl_j [simplified sz_eq]
    apply simp
    done
  show ?thesis
    using root_ptr_valid_field_lvalue [OF root_p root_q fl other] i_bound j_bound
    apply (simp add: array_ptr_index_field_lvalue_conv append )
    done
qed

lemma root_ptr_valid_field_lvalue_array_ptr_index_dim2:
  fixes q:: "'b::mem_type ptr"
  assumes root_p: "root_ptr_valid d (array_ptr_index (array_ptr_index (PTR('a['c]['d]) &(q→f)) False i) False j)"
  assumes root_q: "root_ptr_valid d q"
  assumes other: "typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE('b)"
  assumes i_bound: "i < CARD('d)"
  assumes j_bound: "j < CARD('c)"
  assumes fl: "field_lookup (typ_info_t TYPE('b)) f 0 = Some (t, k)"
  assumes t: "export_uinfo t = typ_uinfo_t (TYPE(('a::array_inner_max_size['c::array_max_count])['d::array_max_count]))"
  shows "False"
proof -
  from field_lookup_array [OF i_bound]
  obtain s n where
    fl_i: "field_lookup (typ_info_t TYPE('a['c]['d])) [replicate i (CHR ''1'')] k = Some (s, n)" and
    s: "s = adjust_ti (typ_info_t TYPE('a['c])) (λx. x.[i]) (λx f. Arrays.update f i x)"
    by blast

  from fl_i t s obtain s' n' where
    fl_i': "field_lookup t [replicate i (CHR ''1'')] k = Some (s', n')" and
    s': "export_uinfo s' = typ_uinfo_t TYPE('a['c])"
    by (smt (verit, best) Padding_Equivalence.field_lookup_export_uinfo_Some_rev
       export_tag_adjust_ti(1) fg_cons_array field_lookup_array fold_typ_uinfo_t i_bound wf_fd field_lookup_typ_uinfo_t_Some)

  from field_lookup_prefix_Some''(1)[rule_format, where f="f" and g="[replicate i CHR ''1'']"
    and m=0, OF fl]
  have fl_app1: "field_lookup (typ_info_t TYPE('b)) (f @ [replicate i CHR ''1'']) 0 = Some (s', n')"
    by (simp add: fl_update fl_i')

  from field_lookup_array [OF j_bound]
  obtain s'' n'' where
    fl_j: "field_lookup (typ_info_t TYPE('a['c])) [replicate j (CHR ''1'')] n' = Some (s'', n'')"
    by blast

  from fl_j s' obtain s''' n''' where
    fl_j': "field_lookup s' [replicate j (CHR ''1'')] n' = Some (s''', n''')"
    by (metis (no_types, lifting) CTypes.field_lookup_export_uinfo_Some_rev field_lookup_export_uinfo_Some fold_typ_uinfo_t)

  from field_lookup_prefix_Some''(1)[rule_format, where f="f @ [replicate i CHR ''1'']" and g="[replicate j CHR ''1'']"
     and m=0, OF fl_app1]
  have fl_app2: "field_lookup (typ_info_t TYPE('b)) (f @ [replicate i CHR ''1'', replicate j CHR ''1'']) 0 = Some (s''', n''')"
    by (simp add: fl_update fl_j')

  have conv: "&(PTR('a['c]) &(PTR('a['c]['d]) &(q→f)→[replicate i CHR ''1''])→[replicate j CHR ''1'']) =
           &(q→f @ [replicate i CHR ''1'', replicate j CHR ''1''])"
    apply (subst field_lvalue_append)
       apply (rule field_lookup_field_ti')
       apply (rule fl)
      apply (simp add: typ_uinfo_t_def i_bound t)
     apply (rule field_lookup_field_ti')
     apply (rule field_lookup_offset_shift')
     apply (rule fl_i)

    apply (subst field_lvalue_append)
    apply (rule field_lookup_field_ti')
       apply (rule field_lookup_offset_shift')
       apply (rule fl_app1)
      apply (simp add: s')
     apply (rule field_lookup_field_ti')
     apply (rule field_lookup_offset_shift')
    apply (rule fl_j)
    apply simp
    done
  from root_ptr_valid_field_lvalue [OF root_p root_q fl_app2 other ] show False
    by (simp add: array_ptr_index_field_lvalue_conv i_bound j_bound conv)
qed

context open_types
begin

definition
  "typ_heap_simulation_of_field (st::'s ⇒ 't) t_hrs t_hrs_update heap_typing_upd f' r' w' ⟷
  (∀d p f. heap_typing_upd d o w' p f = w' p f o heap_typing_upd d) ∧
  (∀t u n.
    field_ti TYPE('a::mem_type) f' = Some t ⟶
    field_lookup (typ_uinfo_t TYPE('a)) f' 0 = Some (u, n) ⟶
    partial_pointer_lense (merge_ti t) r' w' ∧
    (∀(p::'a ptr) s. (∀a∈ptr_span p. root_ptr_valid (hrs_htd (t_hrs s)) (PTR(stack_byte) a)) ⟶
      r' (st s) p ZERO('a) = ZERO('a)) ∧
    (∀(p::'a ptr) x h. ptr_valid_u u (hrs_htd (t_hrs h)) &(p→f') ⟶
      st (t_hrs_update (hrs_mem_update (heap_upd_list (size_td u) &(p→f') (access_ti t x))) h) =
      w' p x (st h)))"

end

definition
  pointer_writer_disjnt ::
    "('a::c_type ptr ⇒ 't upd) ⇒ ('b::c_type ptr ⇒ 't upd) ⇒ bool"
where
  "pointer_writer_disjnt f g ⟷
    (∀p q. disjnt (ptr_span p) (ptr_span q) ⟶ f p ∘ g q = g q o f p)"

definition
  pointer_writer_disjnt_eq ::
    "('a::c_type ptr ⇒ 'x ⇒ 't upd) ⇒ ('b::c_type ptr ⇒ 'y ⇒ 't upd) ⇒ bool"
where
  "pointer_writer_disjnt_eq f g ⟷ (∀p q x y.
    disjnt (ptr_span p) (ptr_span q) ∨ ptr_val p = ptr_val q ⟶ f p x ∘ g q y = g q y o f p x)"

named_theorems pointer_writer_disjnt_intros

lemma pointer_writer_disjnt_eq:
  assumes nm: "∃n1 n2.
    field_lookup (typ_uinfo_t TYPE('a::mem_type)) f1 0 =
      Some (typ_uinfo_t TYPE('b::mem_type), n1) ∧
    field_lookup (typ_uinfo_t TYPE('a)) f2 0 = Some (typ_uinfo_t TYPE('c::mem_type), n2)"
  assumes w1_w2: "⋀x y. pointer_writer_disjnt (λp. w1 p x) (λq. w2 q y)"
  shows "disj_fn f1 f2 ⟶ pointer_writer_disjnt_eq
    (λ(p::'a ptr). w1 (PTR('b) &(p→f1)))
    (λ(p::'a ptr). w2 (PTR('c) &(p→f2)))" (is "?disj ⟶ ?goal")
proof
  assume ?disj
  from nm obtain n1 n2 where fl:
    "field_lookup (typ_uinfo_t TYPE('a::mem_type)) f1 0 =
      Some (typ_uinfo_t TYPE('b::mem_type), n1)"
    "field_lookup (typ_uinfo_t TYPE('a)) f2 0 = Some (typ_uinfo_t TYPE('c::mem_type), n2)"
    by auto
  from fl[THEN field_tag_sub']
  have "ptr_span (PTR('b) &(p→f1)) ⊆ ptr_span p ∧ ptr_span (PTR('c) &(q→f2)) ⊆ ptr_span q"
    for p q :: "'a ptr"
    by (auto intro: field_tag_sub' simp: size_of_def del: subsetI)
  then have ne[simp]: "disjnt (ptr_span p) (ptr_span q) ⟹
    disjnt (ptr_span (PTR('b) &(p→f1))) (ptr_span (PTR('c) &(q→f2)))" for p q :: "'a ptr"
    by (blast intro: disjnt_subset1 disjnt_subset2)
  moreover
  from fl obtain u1 u2 where fl_t:
      "field_lookup (typ_info_t TYPE('a)) f1 0 = Some (u1, n1)"
      "field_lookup (typ_info_t TYPE('a)) f2 0 = Some (u2, n2)"
    and export: "export_uinfo u1 = typ_uinfo_t TYPE('b)" "export_uinfo u2 = typ_uinfo_t TYPE('c)"
    by (auto dest!: field_lookup_export_uinfo_Some_rev simp: typ_uinfo_t_def)
  from fa_fu_lookup_disj_interD[OF fl_t ‹disj_fn f1 f2›]
  have "disjnt (ptr_span (PTR('b) &(p→f1))) (ptr_span (PTR('c) &(p→f2)))" for p :: "'a ptr"
    apply (simp add: size_of_fold disjnt_def)
    apply (simp add: size_of_def field_lvalue_def field_offset_def field_offset_untyped_def fl
                     intvl_disj_offset
                flip: typ_uinfo_size export)
    done
  ultimately show ?goal using w1_w2
    by (auto simp: pointer_writer_disjnt_def pointer_writer_disjnt_eq_def)
qed

lemma pointer_writer_disjnt_sym:
  "pointer_writer_disjnt f g ⟹ pointer_writer_disjnt g f"
  by (auto simp add: pointer_writer_disjnt_def disjnt_sym)

lemma pointer_writer_disjnt_id_left:
  "pointer_writer_disjnt (λp h. h) w"
  by (simp add: pointer_writer_disjnt_def fun_eq_iff)

lemma pointer_writer_disjnt_id_left':
  "pointer_writer_disjnt (λp. id) w"
  by (simp add: pointer_writer_disjnt_def fun_eq_iff)

lemma pointer_writer_disjnt_comp_left:
  "pointer_writer_disjnt w1 w ⟹ pointer_writer_disjnt w2 w ⟹
    pointer_writer_disjnt (λp h. w1 p (w2 p h)) w"
  by (simp add: pointer_writer_disjnt_def fun_eq_iff)

lemma pointer_writer_disjnt_comp_left':
  "pointer_writer_disjnt w1 w ⟹ pointer_writer_disjnt w2 w ⟹
    pointer_writer_disjnt (λp. w1 p ∘ w2 p) w"
  by (simp add: pointer_writer_disjnt_def fun_eq_iff)

lemma pointer_writer_disjnt_fold_left:
  "list_all (λw'. pointer_writer_disjnt (f w') w) ws ⟹
    pointer_writer_disjnt (λp. fold (λw. f w p) ws) w"
  by (induction ws) (auto intro: pointer_writer_disjnt_comp_left' pointer_writer_disjnt_id_left')

lemma pointer_writer_disjntI:
  "(⋀p q h. w1 p (w2 q h) = w2 q (w1 p h)) ⟹ pointer_writer_disjnt w1 w2"
  by (auto simp: pointer_writer_disjnt_def)

lemma pointer_writer_disjntD:
  "pointer_writer_disjnt w1 w2 ⟹ disjnt (ptr_span p) (ptr_span q) ⟹
    w1 p (w2 q h) = w2 q (w1 p h)"
  by (auto simp: pointer_writer_disjnt_def fun_eq_iff)

lemma pointer_writer_disjnt_ptr_map_left:
  fixes w1 :: "'a::mem_type ptr ⇒ 's upd" and w2 :: "'b::c_type ptr ⇒ 's upd"
  assumes w1_w2: "pointer_writer_disjnt w1 w2"
  assumes "⋀(p::'c::c_type ptr). ptr_span (F p) ⊆ ptr_span p"
  shows "pointer_writer_disjnt (λ(p::'c ptr). w1 (F p)) w2"
  using assms by (auto simp: pointer_writer_disjnt_def disjnt_subset1)

lemma pointer_writer_disjnt_ptr_left:
  fixes w1 :: "'a::mem_type ptr ⇒ 's upd" and w2 :: "'b::mem_type ptr ⇒ 's upd"
  assumes w1_w2: "pointer_writer_disjnt w1 w2"
  assumes n:
    "∃n. field_lookup (typ_uinfo_t TYPE('c::mem_type)) f 0 = Some (typ_uinfo_t TYPE('a), n)"
  shows "pointer_writer_disjnt (λ(p::'c ptr). w1 (PTR('a) &(p→f))) w2"
proof (rule pointer_writer_disjnt_ptr_map_left[OF w1_w2])
  show "ptr_span (PTR('a) &(p→f)) ⊆ ptr_span p" for p :: "'c ptr"
    using field_tag_sub'[where 'a='c, of f "typ_uinfo_t TYPE('a)" _ p] n
    by (auto simp: size_of_def)
qed

lemma pointer_writer_disjnt_ptr_corce:
  fixes w1 :: "'a::mem_type ptr ⇒ 's upd" and w2 :: "'b::mem_type ptr ⇒ 's upd"
  assumes w1_w2: "pointer_writer_disjnt w1 w2"
    and size: "size_of TYPE('a) ≤ size_of TYPE('c)"
  shows "pointer_writer_disjnt (λ(p::'c::c_type ptr). w1 (PTR_COERCE('c → 'a) p)) w2"
  by (rule pointer_writer_disjnt_ptr_map_left[OF w1_w2])
     (simp add: intvl_start_le size)

lemma pointer_writer_disjnt_ptr_corce_signed:
  fixes w1 :: "'a::len8 word ptr ⇒ 's upd" and w2 :: "'b::mem_type ptr ⇒ 's upd"
  assumes w1_w2: "pointer_writer_disjnt w1 w2"
  shows "pointer_writer_disjnt (λ(p::'a signed word ptr).
    w1 (PTR_COERCE('a signed word → 'a word) p)) w2"
  using w1_w2 by (rule pointer_writer_disjnt_ptr_corce) (simp add: size_of_signed_word)

lemma pointer_writer_disjnt_ptr_corce_signed':
  fixes w1 :: "'a::len8 word ptr ⇒ 's upd" and w2 :: "'b::mem_type ptr ⇒ 's upd"
  shows "pointer_writer_disjnt w2 w1 ⟹
    pointer_writer_disjnt w2 (λ(p::'a signed word ptr).
      w1 (PTR_COERCE('a signed word → 'a word) p))"
  using pointer_writer_disjnt_ptr_corce_signed[of w1 w2] by (simp add: pointer_writer_disjnt_sym)

lemma (in pointer_lense) pointer_writer_disjnt_replace_by_const:
  "(⋀x. pointer_writer_disjnt (λp. w p (λ_. x)) w') ⟹ pointer_writer_disjnt (λp. w p f) w'"
  by (auto simp add: pointer_writer_disjnt_def fun_eq_iff)
     (metis (no_types, lifting) read_write_same write_cong write_read)

lemma (in pointer_lense) read_commute_of_pointer_writer_disjnt:
  assumes w': "⋀f. pointer_writer_disjnt (λp. w p f) w'"
  assumes p_q: "disjnt (ptr_span p) (ptr_span q)"
  shows "r (w' q h) p = r h p"
  apply (subst write_same[of "λ_. r h p" h p, OF refl, symmetric])
  apply (subst pointer_writer_disjntD[OF w' p_q, symmetric])
  apply (subst read_write_same)
  apply (rule refl)
  done

lemma (in pointer_lense) read_commute_of_pointer_writer_disjnt':
  assumes w': "⋀f. pointer_writer_disjnt w' (λp. w p f)"
  assumes p_q: "disjnt (ptr_span p) (ptr_span q)"
  shows "r (w' q h) p = r h p"
  using read_commute_of_pointer_writer_disjnt[OF w'[THEN pointer_writer_disjnt_sym] p_q] .

lemma (in pointer_lense) read_commute_of_commute:
  assumes w': "⋀p f. w p f o w' = w' o w p f"
  shows "r (w' h) p = r h p"
  using read_write_same[of p "λ_. r h p" "w' h"] w'
  by (subst write_same[of "λ_. r h p" h p, OF refl, symmetric]) (simp add: fun_eq_iff)

lemma (in pointer_lense) read_commute_of_commute':
  assumes w': "⋀p f. w' o w p f = w p f o w'"
  shows "r (w' h) p = r h p"
  using read_commute_of_commute[OF w'[symmetric]] .

lemma (in lense) get_commute_of_commute:
  assumes w': "⋀f. w' o upd f = upd f o w'"
  shows "get (w' h) = get h"
  using get_upd[of "λ_. get h" "w' h"] w'[symmetric]
  by (subst upd_same[of "λ_. get h" h, OF refl, symmetric]) (simp add: fun_eq_iff del: get_upd)

lemma (in pointer_lense) pointer_writer_disjnt_replace_dep_by_const:
  assumes *: "⋀x. pointer_writer_disjnt (λp. w p x) w'"
  shows "pointer_writer_disjnt (λp s. w p (f (r s p)) s) w'"
  by (auto simp add: pointer_writer_disjnt_def fun_eq_iff
      read_commute_of_pointer_writer_disjnt[OF *]
      pointer_writer_disjntD[OF *])

lemma (in pointer_lense) pointer_writer_disjnt_upd[pointer_writer_disjnt_intros]:
  "pointer_writer_disjnt (λp. w p x) (λp. w p y)"
  by (simp add: pointer_writer_disjnt_def write_other_commute disjnt_def fun_eq_iff)

lemma (in partial_pointer_lense) read_commute_of_pointer_writer_disjnt:
  assumes w': "⋀f. pointer_writer_disjnt (λp. w p f) w'"
  assumes p_q: "disjnt (ptr_span p) (ptr_span q)"
  shows "r (w' q h) p y = r h p y"
  by (metis m_r p_q pointer_writer_disjntD r_w w' w_r)

lemma pointer_lense_upd_fun_of_lense:
  fixes get upd assumes "lense get upd"
  shows "pointer_lense get (λp f. upd (upd_fun p f))"
proof -
  interpret lense get upd by fact
  show ?thesis
  proof qed (simp_all add: upd_same upd_fun.upd_same disj_ptr_span_ptr_neq
      upd_fun_commute Int_commute disjnt_def)
qed

locale open_types_heap_typing_state = open_types 𝒯 +
  heap_typing_state heap_typing heap_typing_upd
  for
    𝒯 and
    heap_typing :: "'t ⇒ heap_typ_desc" and
    heap_typing_upd :: "(heap_typ_desc ⇒ heap_typ_desc) ⇒ 't ⇒ 't" 


locale typ_heap_simulation_open_types =
  typ_heap_simulation st r w v t_hrs t_hrs_update +
  open_types_heap_typing_state 𝒯 heap_typing heap_typing_upd
  for
    𝒯 and
    st:: "'s ⇒ 't" and
    r:: "'t ⇒ ('a::{xmem_type, stack_type}) ptr ⇒ 'a" and
    w:: "'a ptr ⇒ ('a ⇒ 'a) ⇒ 't ⇒ 't" and
    v:: "'t ⇒ 'a ptr ⇒ bool" and
    t_hrs :: "'s ⇒ heap_raw_state" and
    t_hrs_update:: "(heap_raw_state ⇒ heap_raw_state) ⇒ 's ⇒ 's" and
    heap_typing :: "'t ⇒ heap_typ_desc" and
    heap_typing_upd :: "(heap_typ_desc ⇒ heap_typ_desc) ⇒ 't ⇒ 't" +
  assumes heap_typing_commutes[simp]: "heap_typing (st s) = hrs_htd (t_hrs s)"
  assumes heap_typing_upd_write_commute:
    "⋀p f h d. heap_typing_upd d (w p f h) = w p f (heap_typing_upd d h)"
  assumes ptr_valid_imp_v: "⋀p h. ptr_valid (heap_typing h) p ⟹ v h p"
  assumes sim_stack_stack_byte_zero':
    "⋀p s. ∀a∈ptr_span p. root_ptr_valid (hrs_htd (t_hrs s)) (PTR(stack_byte) a) ⟹
      r (st s) p = ZERO('a)"
begin

lemma heap_typing_write[simp]: "heap_typing (w p f h) = heap_typing h"
  apply (subst upd_same[symmetric, of "λ_. heap_typing h", OF refl])
  apply (subst heap_typing_upd_write_commute[symmetric])
  apply (rule get_upd)
  done

lemma heap_typing_upd[simp]: "r (heap_typing_upd d h) = r h"
  apply (rule ext)
  subgoal for p
    apply (subst write_same[symmetric, of "λ_. r h p", OF refl])
    apply (subst heap_typing_upd_write_commute)
    apply (rule read_write_same)
    done
  done

lemma unchanged_typing_root_ptr_valid_preserved:
  "unchanged_typing_on A t1 t2 ⟹ ptr_span p ⊆ A 
  ⟹ root_ptr_valid (heap_typing t1) p = root_ptr_valid (heap_typing t2) p"
  by (simp add: unchanged_typing_on_def equal_on_def intvlI 
      root_ptr_valid_def size_of_tag subsetD valid_root_footprint_def)

lemma unchanged_typing_ptr_valid_preserved:
  assumes unch: "unchanged_typing_on UNIV t1 t2" 
  shows "ptr_valid (heap_typing t1) p = ptr_valid (heap_typing t2) p"
proof -
  from unch have "heap_typing t1 = heap_typing t2"
    by (simp add: fun_eq_iff unchanged_typing_on_def equal_on_def)
  thus ?thesis
    by simp
qed

lemma unchanged_typing_on_write [unchanged_typing_on_simps]: 
  "unchanged_typing_on A t (w p f t)"
  using heap_typing_upd_write_commute 
  by (simp add: unchanged_typing_on_def)

lemma heap_typing_fold_upd_write: "heap_typing (fold (λi. w (x i) (g i)) [0..<n] t) = heap_typing t"
proof (induct n)
  case 0
  then show ?case by (simp add: heap_typing_upd_write_commute)
next
  case (Suc n)
  then show ?case by (simp add: heap_typing_upd_write_commute)
qed


end

lemma distinct_prop_conj:
  "distinct_prop (λa b. R a b ∧ P a b) xs ⟷ distinct_prop R xs ∧ distinct_prop P xs"
  by (auto simp: distinct_prop_iff_nth)

lemma distinct_prop_zip_cons:
  "list_all (λ(c, d). P a b c d) (zip as bs) ⟹
    distinct_prop (λ(a, b) (c, d). P a b c d) (zip as bs) ⟹
    distinct_prop (λ(a, b) (c, d). P a b c d) (zip (a#as) (b#bs))"
  by (simp add: list_all_iff)

lemma distinct_prop_zip_nil:
  "distinct_prop (λ(a, b) (c, d). P a b c d) (zip [] [])"
  by (simp add: list_all_iff)

lemma list_all_zip_cons:
  "P a b ⟹ list_all (λ(a, b). P a b) (zip as bs) ⟹
    list_all (λ(a, b). P a b) (zip (a#as) (b#bs))"
  by simp

lemma list_all_zip_nil:
  "list_all (λ(a, b). P a b) (zip [] [])"
  by simp

named_theorems disjnt_heap_fields_comp

context open_types
begin

lemma typ_heap_simulationI_part_addressable:
  fixes R :: "'t ⇒ 'a::{xmem_type, stack_type} ptr ⇒ 'a"
  assumes hrs: "heap_typing_simulation 𝒯 hrs hrs_upd heap_typing heap_typing_upd l"
  assumes fs: "map_of 𝒯 (typ_uinfo_t TYPE('a)) = Some fs"
  assumes "lense g u"
  assumes len[simp]: "length rs = length fs" "length ws = length fs"
  assumes *:
      "list_all (λ(f, r, w). typ_heap_simulation_of_field l hrs hrs_upd heap_typing_upd f r w) (zip fs (zip rs ws))"
    and **: "distinct_prop (λ(f1, w1) (f2, w2).
      disj_fn f1 f2 ⟶ pointer_writer_disjnt_eq w1 w2)
      (zip fs ws)"
    and ws_u: "list_all (λw. ∀p a f. w p a ∘ u f = u f ∘ w p a) ws"
    and l_u: "⋀(p::'a ptr) (x::'a) (s::'b).
      PTR_VALID('a) (hrs_htd (hrs s)) p ⟹
      l (hrs_upd (write_dedicated_heap p x) s) = u (upd_fun p (λold. merge_addressable_fields old x)) (l s)"
    and r_stack:
      "⋀p s. ∀a∈ptr_span p. root_ptr_valid (hrs_htd (hrs s)) (PTR(stack_byte) a) ⟹
        g (l s) p = ZERO(_)"
    and heap_typing_u: "⋀x d h. heap_typing_upd d (u x h) = u x (heap_typing_upd d h)"
  assumes V:
    "⋀h p. V h p ⟷ PTR_VALID('a) (heap_typing h) p"
  assumes R:
    "⋀h p. R h p = fold (λr. r h p) rs (g h p)"
  assumes W:
    "⋀p f h. W p f h =
      fold (λw. w p (f (R h p))) ws (u (upd_fun p (λold. merge_addressable_fields old (f (R h p)))) h)"
  shows "typ_heap_simulation_open_types 𝒯 l R W V hrs hrs_upd heap_typing heap_typing_upd ∧
    (pointer_lense g (λp f. u (upd_fun p f))) ∧
    (∀w. (∀x. list_all (λw'. pointer_writer_disjnt (λp. w' p x) w) ws) ⟶
      (∀x. pointer_writer_disjnt (λp. u (upd_fun p (λ_. x))) w) ⟶
      (∀f. pointer_writer_disjnt (λp. W p f) w)) ∧
    (∀w p. (∀x. list_all (λw'. w' p x o w = w o w' p x) ws) ⟶
      (∀x. u (upd_fun p (λ_. x)) o w = w o u (upd_fun p (λ_. x))) ⟶
      (∀f. W p f o w = w o W p f))"
    (is "?t1 ∧ ?t3 ∧
      (∀w. ?ws w ⟶ ?u w ⟶ (∀f. ?t2 f w)) ∧
      (∀w p. ?ws2 w p ⟶ ?u2 w p ⟶ (∀f. ?t4 w p f))")
proof (intro conjI allI impI)
  interpret hrs: heap_typing_simulation 𝒯 hrs hrs_upd heap_typing heap_typing_upd l by fact
  interpret lense g u by fact

  have [simp]: "length (addressable_fields TYPE('a)) = length fs"
    by (simp add: addressable_fields_def fs)

  have "list_all (λf. ∃u n. field_lookup (typ_uinfo_t TYPE('a)) f 0 = Some (u, n))
    (map fst (zip fs (zip rs ws)))"
    using wf_𝒯[OF fs] by auto
  then have fs_exists:
    "list_all (λx. ∃u n. field_lookup (typ_uinfo_t TYPE('a)) (fst x) 0 = Some (u, n))
      (zip fs (zip rs ws))"
    by (simp add: list.pred_map comp_def del: len)

  have rs_ws:
    "list_all (λ(m, r, w). partial_pointer_lense m r w) (zip (map merge_ti (map snd (addressable_fields TYPE('a)))) (zip rs ws))"
    apply (simp add: zip_map1 list.pred_map addressable_fields_def fs split_beta' comp_def)
    using list_all_conj[OF * fs_exists]
    apply (rule list.pred_mono_strong)
    apply (auto simp: field_ti_def field_lookup_typ_uinfo_t_Some typ_heap_simulation_of_field_def
                dest!: field_lookup_uinfo_Some_rev)
    done

  have dist: "distinct_prop disj_fn fs"
    using 𝒯_distinct[OF fs] .

  interpret pointer_lense R W
    apply (rule pointer_lense_of_partials_cover[
      of g u "map merge_ti (map snd (addressable_fields TYPE('a)))" rs ws, OF ‹lense g u› _ _ _ _ _ _ R])
    subgoal by simp
    subgoal by simp
    subgoal by fact
    subgoal for a b c
      apply (simp add: distinct_prop_map addressable_fields_def fs)
      apply (rule distinct_prop_mono[OF _ dist])
      using wf_𝒯[OF fs]
      apply (intro disjnt_scene_merge_ti[THEN disjnt_sceneD,
        OF option.collapse[symmetric] option.collapse[symmetric]])
      apply (auto simp: list.pred_set field_ti_def disj_fn_def
                  dest!: field_lookup_uinfo_Some_rev)
      done
    subgoal
      using ws_u ** dist
      apply (clarsimp simp add: list_all_iff pointer_writer_disjnt_eq_def[abs_def])
      apply (clarsimp simp add: distinct_prop_iff_nth fun_eq_iff distinct_conv_nth
          disj_fn_def)
      apply metis
      done
    subgoal by (simp add: merge_ti_list_def fold_map comp_def)
    subgoal by (rule W)
    done

  have "list_all (λ(f, w). ∀t u n h p x.
        field_ti TYPE('a) f = Some t ⟶
        field_lookup (typ_uinfo_t TYPE('a)) f 0 = Some (u, n) ⟶
        ptr_valid_u u (hrs_htd (hrs h)) &(p→f) ⟶
        l (hrs_upd (hrs_mem_update (heap_upd_list (size_td u) &(p→f) (access_ti t x))) h) =
          w p x (l h))
     (map (λfrw. (fst frw, snd (snd frw))) (zip fs (zip rs ws)))"
    unfolding list.pred_map
    using * by (rule list.pred_mono_strong) (auto simp:  typ_heap_simulation_of_field_def)
  also have "map (λfrw. (fst frw, snd (snd frw))) (zip fs (zip rs ws)) = zip fs ws"
    by (simp add: list_eq_iff_nth_eq)
  finally have fs_ws: "list_all2 (λf w. ∀t u n h p x.
        field_ti TYPE('a) f = Some t ⟶
        field_lookup (typ_uinfo_t TYPE('a)) f 0 = Some (u, n) ⟶
        ptr_valid_u u (hrs_htd (hrs h)) &(p→f) ⟶
        l (hrs_upd (hrs_mem_update (heap_upd_list (size_td u) &(p→f) (access_ti t x))) h) =
          w p x (l h))
     fs ws"
    by (subst (asm) list_all_zip_iff_list_all2; simp)

  have V_l: "⋀h p. V (l h) p ⟷ PTR_VALID('a) (hrs_htd (hrs h)) p"
    by (simp add: V)

  interpret write_simulation hrs hrs_upd l V W
    apply (rule write_simulationI[OF fs hrs, of ws u V _ R])
    apply (rule fs_ws)
    apply (rule l_u)
    apply assumption
    apply (rule V_l)
    apply (rule W)
    done

  show ?t3
    by (rule pointer_lense_upd_fun_of_lense) fact
  then interpret u: pointer_lense g "λp f. u (upd_fun p f)" .

  show "?t2 f w" if *: "?ws w" "?u w" for w f
    by (rule pointer_writer_disjnt_replace_by_const)
       (use * in ‹auto simp add: W[abs_def]
        intro!: pointer_writer_disjnt_comp_left[OF pointer_writer_disjnt_fold_left
                u.pointer_writer_disjnt_replace_by_const]›)

  show disj: "?t4 w p f" if *: "?u2 w p" "?ws2 w p" for p f w
  proof (standard, unfold comp_def)
    fix h
    have w_ws: "w (fold (λw. w p c) ws h) = fold (λw. w p c) ws (w h)" for c h
      using *[rule_format, of c]
      by (induction ws arbitrary: h) (auto simp: fun_eq_iff)

    have w_u[simp]: "w (u (upd_fun p (λ_. c)) h) = u (upd_fun p (λ_. c)) (w h)" for c h
      using *(1) by (auto simp: fun_eq_iff)

    have g_w[simp]: "g (w h) p = g h p" for h
      by (subst u.write_same[of "λ_. g h p" h p, OF refl, symmetric])
         (simp add: u.read_write_same)

    have w_u'[simp]: "w (u (upd_fun p f) h) = u (upd_fun p f) (w h)" for f h
      by (subst (1 2) u.write_cong[where f'="λ_. f (g h p)"]) simp_all

    have w_W_const: "w (W p (λx. c) h) = W p (λx. c) (w h)" for c h
      by (simp add: W w_ws)

    have R_eq: "R (w h) p = R h p"
      apply (subst write_same[of "λ_. R h p" h p, OF refl, symmetric])
      apply (subst w_W_const)
      apply (subst read_write_same)
      apply (rule refl)
      done

    show "W p f (w h) = w (W p f h)"
      by (simp add: R_eq write_cong[of f _ _ "λ_. f (R h p)"] w_W_const)
  qed

  show ?t1
  proof
    fix h p assume V_p: "V (l h) p"
    then show "c_guard p" by (simp add: ptr_valid.ptr_valid_c_guard V)

    have l_h: "l h = W p (λx. h_val (hrs_mem (hrs h)) p) (l h)"
      apply (subst write_commutes[OF V_p, symmetric])
      apply (subst hrs.t_hrs.heap.upd_same)
      apply (cases "hrs h")
      apply (simp_all add: hrs_mem_update_def hrs_mem_def xmem_type_class.heap_update_id)
      done

    show "R (l h) p = h_val (hrs_mem (hrs h)) p"
      apply (subst l_h)
      apply (subst read_write_same)
      apply simp
      done
  next
    fix p :: "'a ptr" and s
    assume p: "∀a∈ptr_span p. root_ptr_valid (hrs_htd (hrs s)) (PTR(stack_byte) a)"
    moreover
    { fix f w and r :: "'t ⇒ 'a ptr ⇒ 'a ⇒ 'a" and u n
      assume "typ_heap_simulation_of_field l hrs hrs_upd heap_typing_upd f r w"
        "field_lookup (typ_uinfo_t TYPE('a)) f 0 = Some (u, n)"
      with p have "r (l s) p ZERO('a) = ZERO('a)"
        unfolding typ_heap_simulation_of_field_def
        by (auto simp: field_ti_def field_lookup_typ_uinfo_t_Some typ_heap_simulation_of_field_def
                 dest!: field_lookup_uinfo_Some_rev) }
    note this[simp]
    from * fs_exists len have "fold (λr. r (l s) p) rs ZERO('a) = ZERO('a)"
      by (induction fs arbitrary: rs ws)
         (auto simp: length_Suc_conv simp del: len)
    ultimately show "R (l s) p = ZERO('a)"
      unfolding R by (simp add: r_stack)
  next
    { fix d p f
      have "W p f o heap_typing_upd d = heap_typing_upd d o W p f"
        apply (rule disj)
        subgoal using heap_typing_u by (simp add: fun_eq_iff)
        using * len
        apply (induction fs arbitrary: ws rs)
        apply (auto simp add: length_Suc_conv typ_heap_simulation_of_field_def simp del: len)
        done
      then show "heap_typing_upd d (W p f h) = W p f (heap_typing_upd d h)" for h
        by (simp add: fun_eq_iff) }
    note heap_typing_W = this

    show "V (W p' f h) p = V h p" for p' f h p
      unfolding V
      apply (subst hrs.upd_same[symmetric, of "λ_. heap_typing h", OF refl])
      apply (subst heap_typing_W[symmetric])
      apply (subst hrs.get_upd)
      ..
  qed (simp_all add: V)
qed

lemma typ_heap_simulationI_no_addressable:
  fixes R :: "'t ⇒ 'a::{xmem_type, stack_type} ptr ⇒ 'a"
  assumes "heap_typing_simulation 𝒯 hrs hrs_upd heap_typing heap_typing_upd l"
  assumes R_u: "lense R u"
  assumes fs: "map_of 𝒯 (typ_uinfo_t TYPE('a)) = None"
    and l_u: "⋀(p::'a ptr) (x::'a) (s::'b).
      PTR_VALID('a) (hrs_htd (hrs s)) p ⟹
      l (hrs_upd (write_dedicated_heap p x) s) = u (upd_fun p (λold. merge_addressable_fields old x)) (l s)"
    and heap_typing_u: "⋀x d h. heap_typing_upd d (u x h) = u x (heap_typing_upd d h)"
    and r_stack:
      "⋀p s. ∀a∈ptr_span p. root_ptr_valid (hrs_htd (hrs s)) (PTR(stack_byte) a) ⟹
        R (l s) p = ZERO(_)"
  assumes V:
    "⋀h p. V h p ⟷ PTR_VALID('a) (heap_typing h) p"
  assumes W:
    "⋀p f h. W p f h = u (λh'. h'(p := f (h' p))) h"
  shows "typ_heap_simulation_open_types 𝒯 l R W V hrs hrs_upd heap_typing heap_typing_upd"
proof -
  interpret hrs: heap_typing_simulation 𝒯 hrs hrs_upd heap_typing heap_typing_upd l by fact
  interpret lense R u by fact

  have [simp]: "merge_addressable_fields = (λa b::'a. b)"
    by (simp add: fun_eq_iff addressable_fields_def fs)

  interpret pointer_lense R W
    using pointer_lense_of_lense_fld[where 'd='a, OF R_u, of "[]"]
    by (simp add: W[abs_def] upd_fun_def[abs_def])

  interpret write_simulation hrs hrs_upd l V W
    apply (rule hrs.write_simulation_alt)
    subgoal by (simp add: V)
    subgoal for h p x
      unfolding W V
      using l_u[of h p x]
      by (simp add: write_dedicated_heap_def heap_upd_const upd_fun_def[abs_def])
    done

  show ?thesis
  proof
    fix h p assume V_p: "V (l h) p"
    then show "c_guard p" by (simp add: ptr_valid.ptr_valid_c_guard V)

    have l_h: "l h = W p (λx. h_val (hrs_mem (hrs h)) p) (l h)"
      apply (subst write_commutes[OF V_p, symmetric])
      apply (subst hrs.t_hrs.heap.upd_same)
      apply (cases "hrs h")
      apply (simp_all add: hrs_mem_update_def hrs_mem_def xmem_type_class.heap_update_id)
      done

    show "R (l h) p = h_val (hrs_mem (hrs h)) p"
      apply (subst l_h)
      apply (subst read_write_same)
      apply simp
      done
  next
    show "V (W p' f h) p = V h p" for p' f h p
      unfolding W V
      apply (subst hrs.upd_same[symmetric, of "λ_. heap_typing h", OF refl])
      apply (subst heap_typing_u[symmetric])
      apply (subst hrs.get_upd)
      ..
  qed (simp_all add: V W heap_typing_u r_stack)
qed

lemma typ_heap_simulationI_all_addressable:
  fixes R :: "'t ⇒ 'a::{xmem_type, stack_type} ptr ⇒ 'a"
  assumes hrs: "heap_typing_simulation 𝒯 hrs hrs_upd heap_typing heap_typing_upd l"
  assumes fs: "map_of 𝒯 (typ_uinfo_t TYPE('a)) = Some fs"
  assumes len[simp]: "length rs = length fs" "length ws = length fs"
  assumes *:
    "list_all (λ(f, r, w). typ_heap_simulation_of_field l hrs hrs_upd heap_typing_upd f r w) (zip fs (zip rs ws))"
    and **: "distinct_prop (λ(f1, w1) (f2, w2).
        disj_fn f1 f2 ⟶ pointer_writer_disjnt_eq w1 w2)
      (zip fs ws)"
  assumes all: "⋀a b. fold (λx. merge_ti (the (field_ti TYPE('a) x)) a) fs b = a"
  assumes V:
    "⋀h p. V h p ⟷ PTR_VALID('a) (heap_typing h) p"
  assumes R:
    "⋀h p x. R h p = fold (λr. r h p) rs x"
  assumes W:
    "⋀p f h. W p f h = fold (λw. w p (f (R h p))) ws h"
  shows "typ_heap_simulation_open_types 𝒯 l R W V hrs hrs_upd heap_typing heap_typing_upd ∧
    (∀w. (∀x. list_all (λw'. pointer_writer_disjnt (λp. w' p x) w) ws) ⟶
      (∀f. pointer_writer_disjnt (λp. W p f) w)) ∧
    (∀(w::'t ⇒ 't) p.
      (∀x. list_all (λw'. w' p x ∘ w = w ∘ w' p x) ws) ⟶
      (∀f. W p f ∘ w = w ∘ W p f))"
    (is "?t1 ∧ (∀w. ?ws w ⟶ (∀f. ?t2 f w)) ∧ (∀w p. ?ws2 p w ⟶ (∀f. ?t3 p f w))")
proof (intro conjI allI impI)
  interpret hrs: heap_typing_simulation 𝒯 hrs hrs_upd heap_typing heap_typing_upd l by fact

  have [simp]: "length (addressable_fields TYPE('a)) = length fs"
    by (simp add: addressable_fields_def fs)

  have "list_all (λf. ∃u n. field_lookup (typ_uinfo_t TYPE('a)) f 0 = Some (u, n))
    (map fst (zip fs (zip rs ws)))"
    using wf_𝒯[OF fs] by auto
  then have fs_exists:
    "list_all (λx. ∃u n. field_lookup (typ_uinfo_t TYPE('a)) (fst x) 0 = Some (u, n))
      (zip fs (zip rs ws))"
    by (simp add: list.pred_map comp_def del: len)

  have coer_eq[simp]: "merge_addressable_fields = (λa b::'a. a)"
    by (simp add: merge_ti_list_def addressable_fields_def fold_map fs fun_eq_iff comp_def all)

  have dist: "distinct_prop disj_fn fs"
    using 𝒯_distinct[OF fs] .

  interpret pointer_lense R W
    apply (rule pointer_lense_of_partials[
      of "map merge_ti (map snd (addressable_fields TYPE('a)))" rs ws, OF _ _ _ _ _ _ R])
    subgoal by simp
    subgoal by simp
    subgoal
      apply (simp add: zip_map1 list.pred_map addressable_fields_def fs split_beta' comp_def)
      using list_all_conj[OF * fs_exists]
      apply (rule list.pred_mono_strong)
      apply (auto simp: field_ti_def field_lookup_typ_uinfo_t_Some typ_heap_simulation_of_field_def
                  dest!: field_lookup_uinfo_Some_rev)
      done
    subgoal for a b c
      apply (simp add: distinct_prop_map addressable_fields_def fs)
      apply (rule distinct_prop_mono[OF _ dist])
      using wf_𝒯[OF fs]
      apply (intro disjnt_scene_merge_ti[THEN disjnt_sceneD,
        OF option.collapse[symmetric] option.collapse[symmetric]])
      apply (auto simp: list.pred_set field_ti_def disj_fn_def
                  dest!: field_lookup_uinfo_Some_rev)
      done
    subgoal
      using ** dist
      apply (clarsimp simp add: distinct_prop_iff_nth fun_eq_iff pointer_writer_disjnt_eq_def[abs_def]
                             distinct_conv_nth disj_fn_def)
      apply metis
      done
    subgoal by (simp add: addressable_fields_def fs fold_map comp_def all)
    subgoal by (rule W)
    done

  have "list_all (λ(f, w). ∀t u n h p x.
        field_ti TYPE('a) f = Some t ⟶
        field_lookup (typ_uinfo_t TYPE('a)) f 0 = Some (u, n) ⟶
        ptr_valid_u u (hrs_htd (hrs h)) &(p→f) ⟶
        l (hrs_upd (hrs_mem_update (heap_upd_list (size_td u) &(p→f) (access_ti t x))) h) =
          w p x (l h))
     (map (λfrw. (fst frw, snd (snd frw))) (zip fs (zip rs ws)))"
    unfolding list.pred_map
    using * by (rule list.pred_mono_strong) (auto simp:  typ_heap_simulation_of_field_def)
  also have "map (λfrw. (fst frw, snd (snd frw))) (zip fs (zip rs ws)) = zip fs ws"
    by (simp add: list_eq_iff_nth_eq)
  finally have fs_ws: "list_all2 (λf w. ∀t u n h p x.
        field_ti TYPE('a) f = Some t ⟶
        field_lookup (typ_uinfo_t TYPE('a)) f 0 = Some (u, n) ⟶
        ptr_valid_u u (hrs_htd (hrs h)) &(p→f) ⟶
        l (hrs_upd (hrs_mem_update (heap_upd_list (size_td u) &(p→f) (access_ti t x))) h) =
          w p x (l h))
     fs ws"
    by (subst (asm) list_all_zip_iff_list_all2; simp)

  have V_l: "⋀h p. V (l h) p ⟷ PTR_VALID('a) (hrs_htd (hrs h)) p"
    by (simp add: V)

  interpret write_simulation hrs hrs_upd l V W
    apply (rule write_simulationI[OF fs hrs, of ws "λx y. y" V _ R])
    apply (rule fs_ws)
    apply (simp add: write_dedicated_heap_def heap_upd_id hrs_mem_update_id3 flip: id_def)
    apply (simp add: id_def)
    apply (rule V_l)
    apply (rule W)
    done

  show "?t2 f w" if *: "?ws w" for w f
    apply (rule pointer_writer_disjnt_replace_by_const)
    apply (simp add: W[abs_def])
    apply (intro pointer_writer_disjnt_fold_left *[rule_format])
    done

  show disj: "?t3 p f w" if *: "?ws2 p w" for p f w
  proof (standard, unfold comp_def)
    fix h
    have w_W_const: "w (W p (λx. c) h) = W p (λx. c) (w h)" for c h
      using *[rule_format, of c]
      apply (simp add: W)
      apply (induction ws arbitrary: h)
      apply (auto simp: fun_eq_iff)
      done
    have R_eq: "R (w h) p = R h p"
      apply (subst write_same[of "λ_. R h p" h p, OF refl, symmetric])
      apply (subst w_W_const)
      apply (subst read_write_same)
      apply (rule refl)
      done

    show "W p f (w h) = w (W p f h)"
      by (simp add: R_eq write_cong[of f _ _ "λ_. f (R h p)"] w_W_const)
  qed

  show ?t1
  proof
    fix h p assume V_p: "V (l h) p"
    then show "c_guard p" by (simp add: ptr_valid.ptr_valid_c_guard V)

    have l_h: "l h = W p (λx. h_val (hrs_mem (hrs h)) p) (l h)"
      apply (subst write_commutes[OF V_p, symmetric])
      apply (subst hrs.t_hrs.heap.upd_same)
      apply (cases "hrs h")
      apply (simp_all add: hrs_mem_update_def hrs_mem_def xmem_type_class.heap_update_id)
      done

    show "R (l h) p = h_val (hrs_mem (hrs h)) p"
      apply (subst l_h)
      apply (subst read_write_same)
      apply simp
      done
  next
    fix p :: "'a ptr" and s
    assume p: "∀a∈ptr_span p. root_ptr_valid (hrs_htd (hrs s)) (PTR(stack_byte) a)"
    moreover
    { fix f w and r :: "'t ⇒ 'a ptr ⇒ 'a ⇒ 'a" and u n
      assume "typ_heap_simulation_of_field l hrs hrs_upd heap_typing_upd f r w"
        "field_lookup (typ_uinfo_t TYPE('a)) f 0 = Some (u, n)"
      with p have "r (l s) p ZERO('a) = ZERO('a)"
        unfolding typ_heap_simulation_of_field_def
        by (auto simp: field_ti_def field_lookup_typ_uinfo_t_Some typ_heap_simulation_of_field_def
                 dest!: field_lookup_uinfo_Some_rev) }
    note this[simp]
    from * fs_exists len have "fold (λr. r (l s) p) rs ZERO('a) = ZERO('a)"
      by (induction fs arbitrary: rs ws)
         (auto simp: length_Suc_conv simp del: len)
    ultimately show "R (l s) p = ZERO('a)"
      unfolding R[of _ _ "ZERO('a)"] by simp
  next
    { fix p f d
      have "W p f o heap_typing_upd d = heap_typing_upd d o W p f"
        apply (rule disj)
        using * len
        apply (induction fs arbitrary: ws rs)
        apply (auto simp add: length_Suc_conv typ_heap_simulation_of_field_def simp del: len)
        done
      then show "heap_typing_upd d (W p f h) = W p f (heap_typing_upd d h)" for h
        by (simp add: fun_eq_iff) }
    note heap_typing_W = this

    show "V (W p' f h) p = V h p" for p' f h p
      unfolding V
      apply (subst hrs.upd_same[symmetric, of "λ_. heap_typing h", OF refl])
      apply (subst heap_typing_W[symmetric])
      apply (subst hrs.get_upd)
      ..
  qed (simp_all add: V)
qed

end

definition
  field_with_lense ::
    "qualified_field_name ⇒ ('a::c_type ⇒ 'b::c_type) ⇒ (('b ⇒ 'b) ⇒ 'a ⇒ 'a) ⇒ bool"
where
  "field_with_lense f g u ⟷
    field_ti TYPE('a) f = Some (adjust_ti (typ_info_t TYPE('b)) g (u o (λx _. x))) ∧
    lense g u"

lemma update_desc_id: "update_desc (λx. x) (λx _. x) = id"
  by (simp add: fun_eq_iff update_desc_def)

lemma field_with_lense_Nil: "field_with_lense [] (λx. x) (λf x. f x)"
  by (simp add: field_with_lense_def lense_def comp_def adjust_ti_def update_desc_id map_td_id(1))

lemma field_with_lense_Cons:
  fixes g :: "'a::mem_type ⇒ 'b::mem_type" and gs :: "'b ⇒ 'c::mem_type"
  assumes fs: "field_with_lense fs gs us"
  assumes f: "field_ti TYPE('a) [f] = Some (adjust_ti (typ_info_t TYPE('b)) g (u o (λx _. x)))"
  assumes g_u: "fg_cons g (u o (λx _. x))"
  assumes u: "⋀f x. u f x = u (λ_. f (g x)) x"
  shows "field_with_lense (f # fs) (λx. gs (g x)) (λf. u (us f))"
  unfolding field_with_lense_def
proof
  from fs obtain n where fs:
    "field_lookup (typ_info_t TYPE('b)) fs 0 =
      Some (adjust_ti (typ_info_t TYPE('c)) gs (us o (λx _. x)), n)"
    and gs_us: "lense gs us"
    by (auto simp add: field_with_lense_def field_ti_def split: option.splits)

  have g_u: "lense g u"
    using g_u
    apply (rule lense_of_fg_cons')
    apply (rule u)
    done
  then interpret lense g u .
  show "lense (λx. gs (g x)) (λf. u (us f))"
    using g_u gs_us by (rule lense_compose)

  have "(λx. gs (g x)) = gs ∘ g"
    "(λv x. u (λ_. us (λ_. v) (g x)) x) = (λf. u (us f)) ∘ (λx _. x)"
    by (simp_all add: fun_eq_iff cong: upd_cong)
  with field_ti_append_field_lookup[OF f, of fs 0]
  show "field_ti TYPE('a) (f # fs) =
    Some (adjust_ti (typ_info_t TYPE('c)) (λx. gs (g x)) ((λf. u (us f)) ∘ (λx _. x)))"
    unfolding field_lookup_adjust_ti2[OF fs]
    by (simp add: adjust_ti_adjust_ti)
qed

lemma (in typ_heap_simulation_open_types) typ_heap_simulation_of_field:
  assumes f: "field_with_lense f g u"
  assumes v: "⋀h p. PTR_VALID('a) (hrs_htd (t_hrs h)) p ⟹ v (st h) p"
  assumes g_zero: "g ZERO('x::mem_type) = ZERO('a)"
  shows "typ_heap_simulation_of_field st t_hrs t_hrs_update heap_typing_upd f
     (λh p. u (λ_. r h (PTR('a) &(p→f))))
     (λp x. w (PTR('a) &(p→f)) (λ_. g x))"
proof -
  have g_u: "lense g u" using f by (simp add: field_with_lense_def)
  then interpret lense g u .

  have [simp]: "fg_cons g (u ∘ (λx _. x))"
    by (rule fg_cons)
  obtain n where [simp]:
    "field_lookup (typ_uinfo_t TYPE('x)) f 0 = Some (typ_uinfo_t TYPE('a), n)"
    using f
    by (auto simp: field_ti_def field_lookup_typ_uinfo_t_Some field_with_lense_def
             split: option.splits)
  have sz: "size_td (typ_info_t TYPE('a)) = size_of TYPE('a)"
    by (simp add: size_of_def)

  have p_f_eq: "&(p→f) = ptr_val (PTR('c) &(p→f))" for p :: "'x ptr"
    by simp

  have ptr_span_subset: "ptr_span (PTR('a) &(p→f)) ⊆ ptr_span p" for  p :: "'x ptr"
    using field_tag_sub'[where 'a='x, of "f" _ _ p] by (simp add: size_of_def)

  have u_zero: "u (λ_. ZERO('a)) ZERO('x) = ZERO('x)"
    by (simp add: upd_same g_zero)

  show ?thesis using f
    apply (clarsimp simp: typ_heap_simulation_of_field_def field_with_lense_def, intro conjI allI impI)
    subgoal by (simp add: heap_typing_upd_write_commute fun_eq_iff)
    subgoal
      apply (rule partial_pointer_lenseI[OF g_u])
      apply (rule pointer_lense_field_lvalue)
      apply assumption
      apply (simp add: size_of_def)
      done
    subgoal for p
      using ptr_span_subset[of p]
      by (subst sim_stack_stack_byte_zero') (auto simp: u_zero)
    subgoal
      apply (subst sz)
      apply (subst p_f_eq)
      apply (subst heap_update_eq_heap_upd_list[symmetric])
      apply (rule write_commutes)
      apply (simp add: v ptr_valid_def)
      done
    done
qed

context pointer_array_lense
begin

lemma pointer_writer_disjnt_heap_array_map[pointer_writer_disjnt_intros]:
  assumes w': "⋀x. pointer_writer_disjnt (λp. w p x) w'"
  shows "pointer_writer_disjnt (λp. heap_array_map p x) w'"
  apply (rule array.pointer_writer_disjnt_replace_by_const)
  apply (simp only: heap_array_map_def[abs_def])
  apply (rule pointer_writer_disjnt_fold_left)
  apply (clarsimp simp add: list_all_iff)
  apply (rule pointer_writer_disjnt_ptr_map_left[OF w' ptr_span_array_ptr_index_subset_ptr_span])
  apply simp
  done

lemma pointer_writer_disjnt_heap_array_map_right[pointer_writer_disjnt_intros]:
  "(⋀x. pointer_writer_disjnt w' (λp. w p x)) ⟹ pointer_writer_disjnt w' (λp. heap_array_map p x)"
  by (metis pointer_writer_disjnt_heap_array_map pointer_writer_disjnt_sym)

lemma disjnt_comp_heap_array_map[disjnt_heap_fields_comp]:
  assumes w': "⋀q x. w q x ∘ w' = w' ∘ w q x"
  shows "heap_array_map p x ∘ w' = w' ∘ heap_array_map p x"
proof -
  have "heap_array_map p (λ_. c) ∘ w' = w' ∘ heap_array_map p (λ_. c)" for c
    apply (rule comp_commute_of_fold)
    apply (subst heap_array_map_def[abs_def], rule refl)
    apply (simp add: w' list_all_iff)
    done
  then have *: "w' (heap_array_map p (λ_. c) h) = heap_array_map p (λ_. c) (w' h)" for c h
    by (simp add: fun_eq_iff)

  have [simp]: "heap_array (w' h) p = heap_array h p" for h
    apply (subst array.write_same[symmetric, of "λ_. heap_array h p", OF refl])
    apply (subst *)
    apply (subst array.read_write_same)
    apply (rule refl)
    done
  show ?thesis
    apply (rule ext)
    subgoal for h
      apply (clarsimp simp add: fun_eq_iff)
      apply (subst (1 2) array.write_cong[where f'="λ_. x (heap_array h p)"])
      apply (simp_all flip: *)
      done
    done
qed

end

lemma (in open_types) valid_array_of_ptr_valid_arrayI:
  fixes r :: "'t ⇒ 'a::{xmem_type, array_outer_max_size} ptr ⇒ 'a"
  fixes p :: "('a['n::{finite, array_max_count}]) ptr"
  assumes f: "map_of 𝒯 (typ_uinfo_t TYPE('a['n])) = Some (array_fields CARD('n))"
  assumes p: "PTR_VALID('a['n]) h' p"
  assumes v: "⋀p. PTR_VALID('a) h' p ⟹ v h p"
  shows "valid_array_base.valid_array v h p"
  unfolding valid_array_base.valid_array_def
proof (intro allI impI v)
  fix n assume n: "n < CARD('n)"
  note fl_array = field_lookup_array[OF n, THEN field_lookup_typ_uinfo_t_Some]

  have "[replicate n CHR ''1''] ∈ set (array_fields CARD('n))"
    using n by (auto simp: array_fields_def)

  note * = ptr_valid_u_step[OF f this fl_array p[unfolded ptr_valid_def]]
  have "field_offset_untyped (typ_uinfo_t TYPE('a['n])) [replicate n CHR ''1''] =
    n * size_of TYPE('a)"
    by (simp add: field_offset_untyped_def fl_array)
  with * show "PTR_VALID('a) h' (array_ptr_index p False n)"
    by (simp add: n array_ptr_index_def ptr_add_def ptr_valid_def typ_uinfo_t_def)
qed

lemma (in open_types) valid_array_of_ptr_valid_array1[simp]:
  fixes r :: "'t ⇒ 'a::{xmem_type, array_outer_max_size} ptr ⇒ 'a"
  fixes p :: "('a['n::{finite, array_max_count}]) ptr"
  assumes f:
    "map_of 𝒯 (typ_uinfo_t TYPE('a['n])) = Some (array_fields CARD('n))"
  assumes p: "PTR_VALID('a['n]) (heap_typing h) p"
  shows "valid_array_base.valid_array (λh. PTR_VALID('a) (heap_typing h)) h p"
  by (rule valid_array_of_ptr_valid_arrayI[of "heap_typing h", OF f p])

lemma (in open_types) valid_array_of_ptr_valid_array2[simp]:
  fixes r :: "'t ⇒ 'a::{xmem_type, array_inner_max_size} ptr ⇒ 'a"
  fixes p :: "('a['n::{finite, array_max_count}]['m::{finite, array_max_count}]) ptr"
  assumes f2:
    "map_of 𝒯 (typ_uinfo_t TYPE('a['n]['m])) = Some (array_fields CARD('m))"
  assumes f1:
    "map_of 𝒯 (typ_uinfo_t TYPE('a['n])) = Some (array_fields CARD('n))"
  assumes p: "PTR_VALID('a['n]['m]) (heap_typing h) p"
  shows "valid_array_base.valid_array (valid_array_base.valid_array
    (λh. PTR_VALID('a) (heap_typing h))) h p"
  apply (rule valid_array_of_ptr_valid_arrayI[of "heap_typing h", OF f2 p])
  apply (rule valid_array_of_ptr_valid_array1[OF f1])
  apply assumption
  done

lemma (in open_types) ptr_valid_unsigned[simp]:
  "PTR_VALID('a::len8 signed word) h p ⟷
    PTR_VALID('a::len8 word) h (PTR_COERCE('a signed word → 'a word) p)"
  by (simp add: typ_uinfo_t_signed_word_word_conv ptr_valid_def)

lemma ucast_zero_word:
  "UCAST('a::len8 → 'a signed) ZERO('a word) = ZERO('a signed word)"
  using len8_bytes[where 'a='a]
  apply (simp add: zero_def)
  apply (subst from_bytes_signed_word)
  apply (simp_all add: size_of_def typ_info_word ucast_ucast_id)
  done

definition signed_heap:: 
  "('s ⇒ 'a::len word ptr ⇒ 'a word) ⇒ ('s ⇒ 'a signed word ptr ⇒ 'a signed word)" where
  "signed_heap h s = UCAST ('a::len → 'a signed) o (h s) o PTR_COERCE('a signed word → 'a word)"

lemma signed_heap_apply[simp]: 
  "signed_heap h s p = UCAST ('a::len → 'a signed) (h s (PTR_COERCE('a signed word → 'a word) p))"
  by (simp add: signed_heap_def)

lemma signed_typ_heap_simulation_of_typ_heap_simulation:
  fixes r :: "_ ⇒ _ ⇒ 'a::len8 word"
  assumes r:
    "typ_heap_simulation_open_types 𝒯 st r w v t_hrs t_hrs_update heap_typing heap_typing_upd"
  shows "typ_heap_simulation_open_types 𝒯 st
    (signed_heap r)
    (λp m. w (PTR_COERCE('a signed word → 'a word) p) (λw. UCAST('a signed → 'a) (m (UCAST('a → 'a signed) w))))
    (λh p. v h (PTR_COERCE('a signed word → 'a word) p))
    t_hrs t_hrs_update heap_typing heap_typing_upd"
proof -
  interpret typ_heap_simulation_open_types 𝒯 st r w v t_hrs t_hrs_update heap_typing heap_typing_upd
    by fact
  interpret cast: pointer_lense
    "signed_heap r"
    "λp m. w (PTR_COERCE('a signed word → 'a word) p)
      (λw. UCAST('a signed → 'a) (m (UCAST('a → 'a signed) w)))"
    unfolding signed_heap_def comp_def
    by (rule pointer_lense_ucast_signed) unfold_locales
  have [simp]: "c_guard p ⟷ c_guard (PTR_COERCE('a signed word → 'a word) p)" for p
    apply (intro c_guard_ptr_coerce[symmetric])
    apply (simp_all add: size_of_signed_word align_of_signed_word)
    done
  note scast_ucast_norm[simp del]
  note ucast_ucast_id[simp]
  show ?thesis
    apply unfold_locales 
    apply (simp_all add: ptr_valid_unsigned ptr_valid_imp_v
        read_commutes h_val_signed_word write_padding_commutes heap_typing_upd_write_commute)
    apply (subst heap_update_padding_signed_word(1)[symmetric])
    apply (subst write_padding_commutes)
    apply (simp_all add: size_of_signed_word scast_ucast_down_same valid_implies_c_guard)
    apply (rule valid_same_typ_desc, simp)
    apply (simp add: sim_stack_stack_byte_zero')
    apply (simp add: ucast_zero_word)
    done
qed

lemma array_typ_heap_simulation_of_typ_heap_simulation:
  fixes r :: "_ ⇒ _ ⇒ 'a::{stack_type, xmem_type, array_outer_max_size}"
  assumes "typ_heap_simulation_open_types 𝒯 st r w v t_hrs t_hrs_update heap_typing heap_typing_upd"
  assumes f: "map_of 𝒯 (typ_uinfo_t TYPE('a['n::{finite, array_max_count}])) =
    Some (array_fields CARD('n))"
  shows
    "typ_heap_simulation_open_types 𝒯 st
      (pointer_array_lense.heap_array r :: _ ⇒ ('a['n]) ptr ⇒ _)
      (pointer_array_lense.heap_array_map r w)
      (valid_array_base.valid_array v)
      t_hrs t_hrs_update heap_typing heap_typing_upd"
proof -
  interpret sim: typ_heap_simulation_open_types 𝒯 st r w v t_hrs t_hrs_update by fact
  interpret array_typ_heap_simulation st r w v t_hrs t_hrs_update ..
  show ?thesis
  proof
    fix p :: "('a['n]) ptr" and d f
    have "heap_array_map p f o heap_typing_upd d = heap_typing_upd d o heap_array_map p f"
      by (intro disjnt_comp_heap_array_map)
         (simp add: fun_eq_iff sim.heap_typing_upd_write_commute)
    then show "heap_typing_upd d (heap_array_map p f h) = heap_array_map p f (heap_typing_upd d h)" for h
      by (simp add: fun_eq_iff)
    show "heap_array (st s) p = ZERO(_)"
      if p: "∀a∈ptr_span p. root_ptr_valid (hrs_htd (t_hrs s)) (PTR(stack_byte) a)" for s
      apply (intro array_ext)
      apply (simp add: array_index_zero)
      apply (intro sim.sim_stack_stack_byte_zero')
      subgoal for i
        using ptr_span_array_ptr_index_subset_ptr_span[of i p False] p
        apply auto
        done
      done
    show "sim.ptr_valid (heap_typing h) p ⟹ valid_array h p" for h
      by (rule sim.valid_array_of_ptr_valid_arrayI[OF f, of "heap_typing h"])
         (simp_all add: sim.ptr_valid_imp_v)
  qed simp
qed

lemma (in typ_heap_simulation_open_types) stack_simulation_heap_typingI:
  assumes hrs: "heap_typing_simulation 𝒯 t_hrs t_hrs_update heap_typing heap_typing_upd st"
  assumes sim_stack_alloc_heap_typing:
    "⋀p d s n.
      (p, d) ∈ stack_allocs n 𝒮 TYPE('a) (hrs_htd (t_hrs s)) ⟹
        st (t_hrs_update (hrs_mem_update (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n]) ∘ hrs_htd_update (λ_. d)) s) =
        (heap_typing_upd (λ_. d) (st s))"
  assumes sim_stack_release_heap_typing:
    "⋀(p::'a ptr) s n. (⋀i. i < n ⟹ root_ptr_valid (hrs_htd (t_hrs s)) (p +⇩p int i)) ⟹
      st (t_hrs_update (hrs_htd_update (stack_releases n p)) s) =
        heap_typing_upd (stack_releases n p)
         (st (t_hrs_update (hrs_mem_update (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n])) s))"
  shows "stack_simulation_heap_typing st r w t_hrs t_hrs_update heap_typing heap_typing_upd 𝒮 𝒯"
proof -
  interpret hrs: heap_typing_simulation 𝒯 t_hrs t_hrs_update heap_typing heap_typing_upd st by fact
  interpret write_simulation t_hrs t_hrs_update st "λt p. open_types.ptr_valid 𝒯 (heap_typing t) p" w
    apply (rule hrs.write_simulation_alt)
    apply simp
    apply (simp_all add: ptr_valid.ptr_valid_c_guard ptr_valid_imp_v write_commutes read_commutes)
    done
  interpret typ_heap_simulation
    st r w "λt p. open_types.ptr_valid 𝒯 (heap_typing t) p" t_hrs t_hrs_update
    by unfold_locales
       (simp_all add: ptr_valid.ptr_valid_c_guard ptr_valid_imp_v write_commutes read_commutes)
  show ?thesis
  proof
  qed (simp_all add: sim_stack_stack_byte_zero' sim_stack_alloc_heap_typing sim_stack_release_heap_typing)
qed


end