Theory CHERI_C_Concrete_Memory_Model

theory CHERI_C_Concrete_Memory_Model
  imports "Preliminary_Library"
          "Separation_Algebra.Separation_Algebra"
          "Containers.Containers"
          "HOL-Library.Mapping"
          "HOL-Library.Code_Target_Numeral"
begin

section ‹CHERI-C Error System›
text ‹In this section, we formalise the error system used by the memory model.›
text ‹Below are coprocessor 2 excessptions thrown by the hardware. 
      BadAddressViolation is not a coprocessor 2 exception but remains one given by the hardware. 
      This corresponds to CapErr in the paper~\cite{park_2022}.›
datatype c2errtype = 
  TagViolation
  | PermitLoadViolation
  | PermitStoreViolation
  | PermitStoreCapViolation
  | PermitStoreLocalCapViolation
  | LengthViolation
  | BadAddressViolation

text ‹These are logical errors produced by the language. In practice, Some of these errors would never
      be caught due to the inherent spatial safety guarantees given by capabilities. 
      This corresponds to LogicErr in the paper~\cite{park_2022}. \\
      NOTE: Unhandled corresponds to a custom error not mentioned in \emph{logicerrtype}. One can provide
      the custom error as a string, but here, for custom errors, we leave it empty to simplify the
      proof. Ultimately, the important point is that the memory model can still catch custom errors.›
datatype logicerrtype =
  UseAfterFree
  | BufferOverrun
  | MissingResource
  | WrongMemVal
  | MemoryNotFreed
  | Unhandled "String.literal"

text ‹We make the distinction between the error types. This corresponds to Err in the paper~\cite{park_2022}.›
datatype errtype = 
  C2Err c2errtype
  | LogicErr logicerrtype

text ‹Finally, we have the `return' type $\mathcal{R}\ \rho$ in the paper~\cite{park_2022}.›
datatype 'a result =
  Success (res: 'a)
  | Error (err: errtype)

text ‹In this theory, we concretise the notion of blocks›
― ‹While we can use int as blocks, integer makes it more efficient for code execution›
type_synonym block = integer
type_synonym memcap = "block mem_capability"
type_synonym cap = "block capability"

text ‹Because \texttt{sizeof} depends on the architecture, it shall be given via the memory model. We also
      use uncompressed capabilities.›
definition sizeof :: "cctype ⇒ nat" ("|_|⇩τ")
  where
  "sizeof τ ≡ case τ of
     Uint8  ⇒ 1
   | Sint8  ⇒ 1
   | Uint16 ⇒ 2
   | Sint16 ⇒ 2
   | Uint32 ⇒ 4
   | Sint32 ⇒ 4
   | Uint64 ⇒ 8
   | Sint64 ⇒ 8
   | Cap ⇒ 32"

text ‹We provide some helper lemmas›
lemma size_type_align:
  assumes "|t|⇩τ = x"
  shows "∃ n. 2 ^ n = x"
proof (cases t)
  case Uint8
  then show ?thesis 
    using assms 
    unfolding sizeof_def 
    by fastforce
next
  case Sint8
  then show ?thesis
    using assms 
    unfolding sizeof_def 
    by fastforce
next
  case Uint16
  then show ?thesis 
    using assms 
    unfolding sizeof_def 
    by (rule_tac x=1 in exI) fastforce
next
  case Sint16
  then show ?thesis 
    using assms 
    unfolding sizeof_def 
    by (rule_tac x=1 in exI) fastforce
next
  case Uint32
  then show ?thesis
    using assms 
    unfolding sizeof_def 
    by (rule_tac x=2 in exI) fastforce
next
  case Sint32
  then show ?thesis
    using assms 
    unfolding sizeof_def 
    by (rule_tac x=2 in exI) fastforce
next
  case Uint64
  then show ?thesis 
    using assms 
    unfolding sizeof_def 
    by (rule_tac x=3 in exI) fastforce
next
  case Sint64
  then show ?thesis 
    using assms 
    unfolding sizeof_def 
    by (rule_tac x=3 in exI) fastforce
next
  case Cap
  then show ?thesis 
    using assms 
    unfolding sizeof_def 
    by (rule_tac x=5 in exI) fastforce
qed

lemma memval_size_u8:
  "|memval_type (Uint8_v v)|⇩τ = 1"
  unfolding sizeof_def 
  by fastforce

lemma memval_size_s8:
  "|memval_type (Sint8_v v)|⇩τ = 1"
  unfolding sizeof_def 
  by fastforce

lemma memval_size_u16:
  "|memval_type (Uint16_v v)|⇩τ = 2"
  unfolding sizeof_def 
  by fastforce

lemma memval_size_s16:
  "|memval_type (Sint16_v v)|⇩τ = 2"
  unfolding sizeof_def 
  by fastforce

lemma memval_size_u32:
  "|memval_type (Uint32_v v)|⇩τ = 4"
  unfolding sizeof_def 
  by fastforce

lemma memval_size_s32:
  "|memval_type (Sint32_v v)|⇩τ = 4"
  unfolding sizeof_def 
  by fastforce

lemma memval_size_u64:
  "|memval_type (Uint64_v v)|⇩τ = 8"
  unfolding sizeof_def 
  by fastforce

lemma memval_size_s64:
  "|memval_type (Sint64_v v)|⇩τ = 8"
  unfolding sizeof_def 
  by fastforce

lemma memval_size_cap:
  "|memval_type (Cap_v v)|⇩τ = 32"
  unfolding sizeof_def 
  by fastforce

lemmas memval_size_types = memval_size_u8 memval_size_s8 memval_size_u16 memval_size_s16 memval_size_u32 memval_size_s32 memval_size_u64 memval_size_s64 memval_size_cap

corollary memval_size_u16_eq_word_split_len:
  assumes "val = Uint16_v v"
  shows "|memval_type val|⇩τ = length (u16_split v)"
  using assms memval_size_u16 flatten_u16_length 
  by force

corollary memval_size_s16_eq_word_split_len:
  assumes "val = Sint16_v v"
  shows "|memval_type val|⇩τ = length (s16_split v)"
  using assms memval_size_s16 flatten_s16_length 
  by force

corollary memval_size_u32_eq_word_split_len:
  assumes "val = Uint32_v v"
  shows "|memval_type val|⇩τ = length (flatten_u32 v)"
  using assms memval_size_u32 flatten_u32_length
  by force

corollary memval_size_s32_eq_word_split_len:
  assumes "val = Sint32_v v"
  shows "|memval_type val|⇩τ = length (flatten_s32 v)"
  using assms memval_size_s32 flatten_s32_length 
  by force

corollary memval_size_u64_eq_word_split_len:
  assumes "val = Uint64_v v"
  shows "|memval_type val|⇩τ = length (flatten_u64 v)"
  using assms memval_size_u64 flatten_u64_length
  by force

corollary memval_size_s64_eq_word_split_len:
  assumes "val = Sint64_v v"
  shows "|memval_type val|⇩τ = length (flatten_s64 v)"
  using assms memval_size_s64 flatten_s64_length 
  by force

lemma sizeof_nonzero:
  "|t|⇩τ > 0"
  by (simp add: sizeof_def split: cctype.split)

text ‹We prove that integer is a countable type.›
instance int :: comp_countable ..

lemma integer_encode_eq: "(int_encode ∘ int_of_integer) x = (int_encode ∘ int_of_integer) y ⟷ x = y"
  using int_encode_eq integer_eq_iff 
  by auto

instance integer :: countable
  by (rule countable_classI[of "int_encode ∘ int_of_integer"]) (simp only: integer_encode_eq)

instance integer :: comp_countable ..

section ‹Memory›
text ‹In this section, we formalise the heap and prove some initial properties.›
subsection ‹Definitions›

text ‹First, we provide $\mathcal{V}_\mathcal{M}$---refer to ~\cite{park_2022} for the definition. 
      We note that this representation allows us to make the distinction between what is a 
      capability and what is a primitive value stored in memory. We can define a 
      tag-preserving \texttt{memcpy} by checking ahead whether there are valid capabilities stored 
      in memory or whether there are simply bytes. The downside to this approach is that overwriting
      primitive values to where capabilities were stored---and vice versa---will lead to an undefined 
      load operation. However, this tends not to be a big problem, as (1) overwritten capabilities 
      are tag-invalidated anyway, so the capabilities cannot be dereferenced even if the user 
      obtained the capability somehow, and (2) for legacy C programs that do not have access to 
      CHERI library functions, there is no way to access the metadata of the invalidated 
      capabilities. For compatibility purposes, this imposes hardly any problems.›
datatype memval =
  Byte (of_byte: "8 word")
  | ACap (of_cap: "memcap") (of_nth: "nat")

text ‹In general, the bound is irrelevant, as capability bound ensures spatial safety. We add bounds
      in the heap so that we can incorporate \textit{hybrid} CHERI C programs in the future, where 
      pointers and capabilities co-exist, but strictly speaking, this is not required in 
      \textit{purecap} CHERI C programs, which is what this memory model is based on. Ultimately, 
      this is the pair of mapping defined in the paper~\cite{park_2022}.›
record object =
  bounds :: "nat × nat"
  content :: "(nat, memval) mapping"
  tags :: "(nat, bool) mapping"

text ‹t is the datatype that allows us to make the distinction between blocks that are freed and 
      blocks that are valid.›
datatype t = 
  Freed
  | Map (the_map: "object")

text ‹heap\_map in heap is essentially $\mathcal{H}$ defined in the paper~\cite{park_2022}. We 
      extend the structure and keep track of the next block for the allocator for efficiency---much
      like how CompCert's C memory model does this~\cite{leroy_2012}.›
record heap =
  next_block :: "block"
  heap_map :: "(block, t) mapping"

definition memval_is_byte :: "memval ⇒ bool"
  where
  "memval_is_byte m ≡ case m of Byte _ ⇒ True | ACap _ _ ⇒ False"

abbreviation memval_is_cap :: "memval ⇒ bool"
  where
  "memval_is_cap m ≡ ¬ memval_is_byte m"

lemma memval_byte:
  "memval_is_byte m ⟹ ∃ b. m = Byte b"
  by (simp add: memval_is_byte_def split: memval.split_asm)

lemma memval_byte_not_memcap:
  "memval_is_byte m ⟹ m ≠ ACap c n"
  by (simp add: memval_is_byte_def split: memval.split_asm)

lemma memval_memcap:
  "memval_is_cap m ⟹ ∃ c n. m = ACap c n"
  by (simp add: memval_is_byte_def split: memval.split_asm)

lemma memval_memcap_not_byte:
  "memval_is_cap m ⟹ m ≠ Byte b"
  by (simp add: memval_is_byte_def split: memval.split_asm)

subsection ‹Properties›
text ‹We prove that the heap is an instance of separation algebra.›
instantiation unit :: cancellative_sep_algebra
begin
definition "0 ≡ ()"
definition "u1 + u2 = ()"
definition "(u1::unit) ## u2 ≡ True"
instance 
  by (standard; (blast | simp add: sep_disj_unit_def))
end

instantiation nat :: cancellative_sep_algebra
begin
definition "(n1::nat) ## n2 ≡ True"
instance 
  by (standard; (blast | simp add: sep_disj_nat_def))
end

text ‹This proof ultimately shows that heap\_map forms a separation algebra.›
instantiation mapping :: (type, type) cancellative_sep_algebra
begin

definition zero_map_def: "0 ≡ Mapping.empty"
definition plus_map_def: "m1 + m2 ≡ Mapping ((Mapping.lookup m1) ++ (Mapping.lookup m2))"
definition sep_disj_map_def: "m1 ## m2 ≡ Mapping.keys m1 ∩ Mapping.keys m2 = {}"

instance
proof
  show "⋀x :: ('a, 'b) mapping. x ## 0"
    by (simp add: sep_disj_map_def zero_map_def)
next
  show "⋀x :: ('a, 'b) mapping. x + 0 = x"
    by (simp add: sep_disj_map_def Mapping.keys_def zero_map_def plus_map_def Mapping.empty.abs_eq Mapping.lookup.abs_eq mapping_eqI)
next
  show "⋀x y :: ('a, 'b) mapping. x ## y ⟹ y ## x"
    using sep_disj_map_def 
    by auto
next 
  show "⋀x y :: ('a, 'b) mapping. x ## y ⟹ x + y = y + x"
    using map_add_comm
    by (fastforce simp add: sep_disj_map_def Mapping.keys_def zero_map_def plus_map_def Mapping.lookup_def)
next
  show "⋀x y z :: ('a, 'b) mapping. ⟦x ## y; y ## z; x ## z⟧ ⟹ x + y + z = x + (y + z)"
    by (simp add: sep_disj_map_def Mapping.keys_def zero_map_def plus_map_def Mapping.lookup_def Mapping_inverse)
next 
  show "⋀x y z :: ('a, 'b) mapping. ⟦x ## y + z; y ## z⟧ ⟹ x ## y"
    by (simp add: sep_disj_map_def Mapping.keys_def zero_map_def plus_map_def Mapping.lookup_def map_add_comm) 
      (metis (no_types, opaque_lifting) Mapping.keys.abs_eq Mapping.keys.rep_eq disjoint_iff domIff map_add_dom_app_simps(3))
next
  show "⋀x y z :: ('a, 'b) mapping. ⟦x ## y + z; y ## z⟧ ⟹ x + y ## z"
    by (simp add: sep_disj_map_def Mapping.keys_def zero_map_def plus_map_def Mapping.lookup_def map_add_comm Mapping_inverse inf_commute inf_sup_distrib1)
next 
  show "⋀x z y :: ('a, 'b) mapping. ⟦x + z = y + z; x ## z; y ## z⟧ ⟹ x = y"
    by (simp add: plus_map_def sep_disj_map_def)
      (metis (mono_tags, opaque_lifting) Mapping.keys.abs_eq Mapping.lookup.abs_eq disjoint_iff domIff map_add_dom_app_simps(3) mapping_eqI)
qed
end

instantiation heap_ext :: (cancellative_sep_algebra) cancellative_sep_algebra 
begin
definition "0 :: 'a heap_scheme ≡ ⦇ next_block = 0, heap_map = Mapping.empty, … = 0 ⦈"
definition "(m1 :: 'a heap_scheme) + (m2 :: 'a heap_scheme) ≡ 
              ⦇ next_block = next_block m1 + next_block m2,
                heap_map = Mapping ((Mapping.lookup (heap_map m1)) ++ (Mapping.lookup (heap_map m2))), 
                … = heap.more m1 + heap.more m2 ⦈" 
definition "(m1 :: 'a heap_scheme) ## (m2 :: 'a heap_scheme) ≡ 
              Mapping.keys (heap_map m1) ∩ Mapping.keys (heap_map m2) = {}
              ∧ heap.more m1 ## heap.more m2" 
instance 
proof
  show "⋀x :: 'a heap_scheme. x ## 0"
    by (simp add: plus_heap_ext_def sep_disj_heap_ext_def zero_heap_ext_def)
next
  show "⋀x y :: 'a heap_scheme. x ## y ⟹ y ## x"
    by (simp add: plus_heap_ext_def sep_disj_heap_ext_def zero_heap_ext_def inf_commute sep_disj_commute)
next
  show "⋀x :: 'a heap_scheme. x + 0 = x"
    by (simp add: plus_heap_ext_def sep_disj_heap_ext_def zero_heap_ext_def inf_commute sep_disj_commute Mapping.empty_def Mapping.lookup.abs_eq)
      (simp add: Mapping.lookup.rep_eq rep_inverse)
next
  show "⋀x y :: 'a heap_scheme. x ## y ⟹ x + y = y + x"
    by (simp add: plus_heap_ext_def sep_disj_heap_ext_def zero_heap_ext_def)
      (metis keys_dom_lookup map_add_comm sep_add_commute)
next 
  show "⋀x y z :: 'a heap_scheme. ⟦x ## y; y ## z; x ## z⟧ ⟹ x + y + z = x + (y + z)"
    by (simp add: plus_heap_ext_def sep_disj_heap_ext_def zero_heap_ext_def Mapping.lookup.abs_eq sep_add_assoc)
next 
  show "⋀x y z :: 'a heap_scheme. ⟦x ## y + z; y ## z⟧ ⟹ x ## y"
    by (simp add: plus_heap_ext_def sep_disj_heap_ext_def zero_heap_ext_def)
      (metis plus_map_def sep_disj_addD sep_disj_map_def)
next
  show "⋀x y z :: 'a heap_scheme. ⟦x ## y + z; y ## z⟧ ⟹ x + y ## z"
    by (simp add: plus_heap_ext_def sep_disj_heap_ext_def zero_heap_ext_def Mapping.lookup.abs_eq disjoint_iff keys_dom_lookup sep_disj_addI1)
next 
  show "⋀x z y :: 'a heap_scheme. ⟦x + z = y + z; x ## z; y ## z⟧ ⟹ x = y "
    by (simp add: plus_heap_ext_def sep_disj_heap_ext_def zero_heap_ext_def)
      (metis  heap.equality plus_map_def sep_add_cancel sep_disj_map_def)
qed
end

instantiation mem_capability_ext :: (comp_countable, zero) zero
begin
definition "0 :: ('a, 'b) mem_capability_scheme ≡ 
          ⦇ block_id = 0, 
            offset = 0,
            base = 0, 
            len = 0, 
            perm_load = False, 
            perm_cap_load = False, 
            perm_store = False,
            perm_cap_store = False,
            perm_cap_store_local = False,
            perm_global = False,
            … =  0⦈"
instance ..
end

subclass (in comp_countable) zero .

instantiation capability_ext :: (zero) zero
begin
definition "0 ≡ ⦇ tag = False, … = 0⦈"
instance ..
end

text ‹Section 4.5 of CHERI C/C++ Programming Guide defines what a \texttt{NULL} capability is~\cite{watson_cc_2019}.›
definition null_capability :: "cap" ("NULL")
  where
  "NULL ≡ 0"

context 
  notes null_capability_def[simp]
begin

lemma null_capability_block_id[simp]: 
  "block_id NULL = 0"
  by (simp add: zero_mem_capability_ext_def) 

lemma null_capability_offset[simp]:
  "offset NULL = 0"
  by (simp add: zero_mem_capability_ext_def)

lemma null_capability_base[simp]:
  "base NULL = 0"
  by (simp add: zero_mem_capability_ext_def)

lemma null_capability_len[simp]:
  "len NULL = 0"
  by (simp add: zero_mem_capability_ext_def)

lemma null_capability_perm_load[simp]:
  "perm_load NULL = False"
  by (simp add: zero_mem_capability_ext_def)

lemma null_capability_perm_cap_load[simp]:
  "perm_cap_load NULL = False"
  by (simp add: zero_mem_capability_ext_def)

lemma null_capability_perm_store[simp]:
  "perm_store NULL = False"
  by (simp add: zero_mem_capability_ext_def)

lemma null_capability_perm_cap_store[simp]:
  "perm_cap_store NULL = False"
  by (simp add: zero_mem_capability_ext_def)

lemma null_capability_perm_cap_store_local[simp]:
  "perm_cap_store_local NULL = False"
  by (simp add: zero_mem_capability_ext_def)

lemma null_capability_tag[simp]:
  "tag NULL = False"
  by (simp add: zero_capability_ext_def zero_mem_capability_ext_def)

end

text ‹Here, we define the initial heap.›
definition init_heap :: "heap"
  where
  "init_heap ≡ 0 ⦇ next_block := 1 ⦈"

abbreviation cap_offset :: "nat ⇒ nat"
  where
  "cap_offset p ≡ if p mod |Cap|⇩τ = 0 then p else p - p mod |Cap|⇩τ"

text ‹We state the well-formedness property $\mathcal{W}^\mathcal{C}_f$ stated in the paper~\cite{park_2022}.›
definition wellformed :: "(block, t) mapping ⇒ bool" ("𝒲⇩𝔣/(_/)")
  where
  "𝒲⇩𝔣(h) ≡ 
     ∀ b obj. Mapping.lookup h b = Some (Map obj) 
     ⟶ Set.filter (λx. x mod |Cap|⇩τ ≠ 0) (Mapping.keys (tags obj)) = {}"

lemma init_heap_empty:
  "Mapping.keys (heap_map init_heap) = {}"
  unfolding init_heap_def zero_heap_ext_def
  by simp

text ‹Below shows $\mathcal{W}^\mathcal{C}_f(\mu_0)$›
lemma init_wellformed:
  "𝒲⇩𝔣(heap_map init_heap)"
  unfolding init_heap_def wellformed_def zero_heap_ext_def
  by simp

lemma mapping_lookup_disj1:
  "m1 ## m2 ⟹ Mapping.lookup m1 n = Some x ⟹ Mapping.lookup (m1 + m2) n = Some x"
  by (metis Mapping.keys.rep_eq Mapping.lookup.abs_eq Mapping.lookup.rep_eq disjoint_iff is_none_simps(2) keys_is_none_rep map_add_dom_app_simps(3) plus_map_def sep_disj_map_def)

lemma mapping_lookup_disj2:
  "m1 ## m2 ⟹ Mapping.lookup m2 n = Some x ⟹ Mapping.lookup (m1 + m2) n = Some x"
  by (metis Mapping.keys.rep_eq Mapping.lookup.abs_eq Mapping.lookup.rep_eq disjoint_iff is_none_simps(2) keys_is_none_rep map_add_dom_app_simps(2) plus_map_def sep_disj_map_def)

text ‹Below shows that well-formedness is composition-compatible›
lemma "heap_map h1 ## heap_map h2 ⟹ 𝒲⇩𝔣(heap_map h1 + heap_map h2) 
   ⟹ 𝒲⇩𝔣(heap_map h1) ∧ 𝒲⇩𝔣(heap_map h2)"
  unfolding wellformed_def
  by (safe, erule_tac x=b in allE, erule_tac x=obj in allE)
    (fastforce intro: mapping_lookup_disj1 mapping_lookup_disj2)+

section ‹Helper functions and lemmas›
primrec is_memval_defined :: "(nat, memval) mapping ⇒ nat ⇒ nat ⇒ bool"
  where
  "is_memval_defined _ _ 0 = True"
| "is_memval_defined m off (Suc siz) = ((off ∈ Mapping.keys m) ∧ is_memval_defined m (Suc off) siz)"

primrec is_contiguous_bytes :: "(nat, memval) mapping ⇒ nat ⇒ nat ⇒ bool"
  where
  "is_contiguous_bytes _ _ 0 = True"
| "is_contiguous_bytes m off (Suc siz) = ((off ∈ Mapping.keys m) 
                                         ∧ memval_is_byte (the (Mapping.lookup m off))
                                         ∧ is_contiguous_bytes m (Suc off) siz)"

definition get_cap :: "(nat, memval) mapping ⇒ nat ⇒ memcap"
  where
  "get_cap m off = of_cap (the (Mapping.lookup m off))"

fun is_cap :: "(nat, memval) mapping ⇒ nat ⇒ bool"
  where
  "is_cap m off = (off ∈ Mapping.keys m ∧ memval_is_cap (the (Mapping.lookup m off)))"

primrec is_contiguous_cap :: "(nat, memval) mapping ⇒ memcap ⇒ nat ⇒ nat ⇒ bool"
  where
  "is_contiguous_cap _ _ _ 0 = True"
| "is_contiguous_cap m c off (Suc siz) = ((off ∈ Mapping.keys m)
                                         ∧ memval_is_cap (the (Mapping.lookup m off))
                                         ∧ of_cap (the (Mapping.lookup m off)) = c
                                         ∧ of_nth (the (Mapping.lookup m off)) = siz
                                         ∧ is_contiguous_cap m c (Suc off) siz)"

primrec is_contiguous_zeros_prim :: "(nat, memval) mapping ⇒ nat ⇒ nat ⇒ bool"
  where
  "is_contiguous_zeros_prim _ _ 0 = True"
| "is_contiguous_zeros_prim m off (Suc siz) = (Mapping.lookup m off = Some (Byte 0)
                                              ∧ is_contiguous_zeros_prim m (Suc off) siz)"

definition is_contiguous_zeros :: "(nat, memval) mapping ⇒ nat ⇒ nat ⇒ bool"
  where
  "is_contiguous_zeros m off siz ≡ ∀ ofs ≥ off. ofs < off + siz ⟶ Mapping.lookup m ofs = Some (Byte 0)"

lemma is_contiguous_zeros_code[code]:
  "is_contiguous_zeros m off siz = is_contiguous_zeros_prim m off siz"
proof safe
  show "is_contiguous_zeros m off siz ⟹ is_contiguous_zeros_prim m off siz"
    unfolding is_contiguous_zeros_def
  proof (induct siz arbitrary: off)
    case 0
    thus ?case by simp
  next
    case (Suc siz)
    thus ?case
      by fastforce
  qed
next
  show "is_contiguous_zeros_prim m off siz ⟹ is_contiguous_zeros m off siz"
    unfolding is_contiguous_zeros_def
  proof (induct siz arbitrary: off)
    case 0
    thus ?case
      by auto
  next
    case (Suc siz)
    have alt: "is_contiguous_zeros_prim m (Suc off) siz"
      using Suc(2) is_contiguous_zeros_prim.simps(2)[where ?m=m and ?off=off and ?siz=siz]
      by blast
    have add_simp: "Suc off + siz = off + Suc siz" 
      by simp
    show ?case 
      using Suc(1)[where ?off="Suc off", OF alt, simplified add_simp le_eq_less_or_eq Suc_le_eq] 
        Suc(2) Suc_le_eq le_eq_less_or_eq 
      by auto
  qed
qed

  

primrec retrieve_bytes :: "(nat, memval) mapping ⇒ nat ⇒ nat ⇒ 8 word list"
  where
  "retrieve_bytes m _ 0 = []"
| "retrieve_bytes m off (Suc siz) = of_byte (the (Mapping.lookup m off)) # retrieve_bytes m (Suc off) siz"

primrec is_same_cap :: "(nat, memval) mapping ⇒ memcap ⇒ nat ⇒ nat ⇒ bool"
  where
  "is_same_cap _ _ _ 0 = True"
| "is_same_cap m c off (Suc siz) = (of_cap (the (Mapping.lookup m off)) = c ∧ is_same_cap m c (Suc off) siz)"

(* tag retrieval must be based on offset now *)
definition retrieve_tval :: "object ⇒ nat ⇒ cctype ⇒ bool ⇒ block ccval"
  where
  "retrieve_tval obj off typ pcl ≡ 
     if is_contiguous_bytes (content obj) off |typ|⇩τ then
       (case typ of 
          Uint8  ⇒ Uint8_v  (decode_u8_list (retrieve_bytes (content obj) off |typ|⇩τ))
        | Sint8  ⇒ Sint8_v  (decode_s8_list (retrieve_bytes (content obj) off |typ|⇩τ))
        | Uint16 ⇒ Uint16_v (cat_u16 (retrieve_bytes (content obj) off |typ|⇩τ))
        | Sint16 ⇒ Sint16_v (cat_s16 (retrieve_bytes (content obj) off |typ|⇩τ))
        | Uint32 ⇒ Uint32_v (cat_u32 (retrieve_bytes (content obj) off |typ|⇩τ))
        | Sint32 ⇒ Sint32_v (cat_s32 (retrieve_bytes (content obj) off |typ|⇩τ))
        | Uint64 ⇒ Uint64_v (cat_u64 (retrieve_bytes (content obj) off |typ|⇩τ))
        | Sint64 ⇒ Sint64_v (cat_s64 (retrieve_bytes (content obj) off |typ|⇩τ))
        | Cap    ⇒ if is_contiguous_zeros (content obj) off |typ|⇩τ then Cap_v NULL else Undef)
     else if is_cap (content obj) off then
       let cap = get_cap (content obj) off in
       let tv = the (Mapping.lookup (tags obj) (cap_offset off)) in
       let t = (case pcl of False ⇒ False | True ⇒ tv) in
       let cv = mem_capability.extend cap ⦇ tag = t ⦈ in
       let nth_frag = of_nth (the (Mapping.lookup (content obj) off)) in 
       (case typ of 
          Uint8 ⇒ Cap_v_frag (mem_capability.extend cap ⦇ tag = False ⦈) nth_frag
        | Sint8 ⇒ Cap_v_frag (mem_capability.extend cap ⦇ tag = False ⦈) nth_frag
        | Cap   ⇒ if is_contiguous_cap (content obj) cap off |typ|⇩τ then Cap_v cv else Undef
        | _     ⇒ Undef)
     else Undef"

primrec store_bytes :: "(nat, memval) mapping ⇒ nat ⇒ 8 word list ⇒ (nat, memval) mapping"
  where
  "store_bytes obj _ [] = obj"
| "store_bytes obj off (v # vs) = store_bytes (Mapping.update off (Byte v) obj) (Suc off) vs"

primrec store_cap :: "(nat, memval) mapping ⇒ nat ⇒ cap ⇒ nat ⇒ (nat, memval) mapping"
  where
  "store_cap obj _ _ 0 = obj"
| "store_cap obj off cap (Suc n) = store_cap (Mapping.update off (ACap (mem_capability.truncate cap) n) obj) (Suc off) cap n"

abbreviation store_tag :: "(nat, bool) mapping ⇒ nat ⇒ bool ⇒ (nat, bool) mapping"
  where
  "store_tag obj off tg ≡ Mapping.update off tg obj"
                                                             
definition store_tval :: "object ⇒ nat ⇒ block ccval ⇒ object"
  where
  "store_tval obj off val ≡ 
     case val of Uint8_v  v     ⇒ obj ⦇ content := store_bytes (content obj) off (encode_u8_list v), 
                                         tags := store_tag (tags obj) (cap_offset off) False ⦈
               | Sint8_v  v     ⇒ obj ⦇ content := store_bytes (content obj) off (encode_s8_list v), 
                                         tags := store_tag (tags obj) (cap_offset off) False ⦈
               | Uint16_v v     ⇒ obj ⦇ content := store_bytes (content obj) off (u16_split v), 
                                         tags := store_tag (tags obj) (cap_offset off) False ⦈
               | Sint16_v v     ⇒ obj ⦇ content := store_bytes (content obj) off (s16_split v), 
                                         tags := store_tag (tags obj) (cap_offset off) False ⦈
               | Uint32_v v     ⇒ obj ⦇ content := store_bytes (content obj) off (flatten_u32 v), 
                                         tags := store_tag (tags obj) (cap_offset off) False ⦈
               | Sint32_v v     ⇒ obj ⦇ content := store_bytes (content obj) off (flatten_s32 v), 
                                         tags := store_tag (tags obj) (cap_offset off) False ⦈
               | Uint64_v v     ⇒ obj ⦇ content := store_bytes (content obj) off (flatten_u64 v), 
                                         tags := store_tag (tags obj) (cap_offset off) False ⦈
               | Sint64_v v     ⇒ obj ⦇ content := store_bytes (content obj) off (flatten_s64 v), 
                                         tags := store_tag (tags obj) (cap_offset off) False ⦈
               | Cap_v    c     ⇒ obj ⦇ content := store_cap (content obj) off c |Cap|⇩τ, 
                                         tags := store_tag (tags obj) (cap_offset off) (tag c) ⦈
               | Cap_v_frag c n ⇒ obj ⦇ content := Mapping.update off (ACap (mem_capability.truncate c) n) (content obj),
                                         tags := store_tag (tags obj) (cap_offset off) False⦈"

lemma stored_bytes_prev:
  assumes "x < off"
  shows "Mapping.lookup (store_bytes obj off vs) x = Mapping.lookup obj x"
  using assms 
  by (induct vs arbitrary: obj off) fastforce+

lemma stored_tags_prev:
  assumes "x < off"
  shows "Mapping.lookup (store_tag obj off vs) x = Mapping.lookup obj x"
  using assms 
  by force

lemma stored_cap_prev:
  assumes "x < off"
  shows "Mapping.lookup (store_cap obj off cap siz) x = Mapping.lookup obj x"
  using assms 
  by (induct siz arbitrary: obj off) fastforce+

lemma stored_bytes_instant_correctness:
  "Mapping.lookup (store_bytes obj off (v # vs)) off = Some (Byte v)"
proof (induct vs arbitrary: obj off)
  case Nil
  thus ?case by force
next 
  case (Cons a vs)
  thus ?case using stored_bytes_prev Suc_eq_plus1 lessI store_bytes.simps(2)
    by metis
qed

lemma stored_cap_instant_correctness:
  "Mapping.lookup (store_cap obj off cap (Suc siz)) off = Some (ACap (mem_capability.truncate cap) siz)"
proof (induct siz arbitrary: obj off)
  case 0
  thus ?case by force
next 
  case (Suc siz)
  thus ?case using stored_cap_prev Suc_eq_plus1 lessI store_cap.simps(2) lookup_update
    by metis
qed

lemma numeral_4_eq_4: "4 = Suc (Suc (Suc (Suc 0)))"
  by (simp add: eval_nat_numeral)

lemma numeral_5_eq_5: "5 = Suc (Suc (Suc (Suc (Suc 0))))"
  by (simp add: eval_nat_numeral)

lemma numeral_6_eq_6: "6 = Suc (Suc (Suc (Suc (Suc (Suc 0)))))"
  by (simp add: eval_nat_numeral)

lemma numeral_7_eq_7: "7 = Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))"
  by (simp add: eval_nat_numeral)

lemma numeral_8_eq_8: "8 = Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))"
  by (simp add: eval_nat_numeral)

lemma list_length_2_realise:
  "length ls = 2 ⟹ ∃ n0 n1. ls = [n0, n1]"
  by (metis One_nat_def Suc_length_conv add_diff_cancel_right' len_gt_0 len_of_finite_2_def 
      list.size(4) list_exhaust_size_eq0 list_exhaust_size_gt0 one_add_one)

lemma list_length_4_realise: 
  "length ls = 4 ⟹ ∃ n0 n1 n2 n3. ls = [n0, n1, n2, n3]"
  by (metis list_exhaust_size_eq0 list_exhaust_size_gt0 numeral_4_eq_4 size_Cons_lem_eq zero_less_Suc)

lemma list_length_8_realise:
  "length ls = 8 ⟹ ∃ n0 n1 n2 n3 n4 n5 n6 n7. ls = [n0, n1, n2, n3, n4, n5, n6, n7]"
  using list_exhaust_size_eq0 list_exhaust_size_gt0 numeral_8_eq_8 size_Cons_lem_eq zero_less_Suc
  by smt

lemma u16_split_realise:
  "∃ b0 b1. u16_split v = [b0, b1]" 
  using list_length_2_realise[where ?ls="u16_split v", OF flatten_u16_length[where ?vs=v]]
  by assumption

lemma s16_split_realise:
  "∃ b0 b1. s16_split v = [b0, b1]"
  using list_length_2_realise[where ?ls="s16_split v", OF flatten_s16_length[where ?vs=v]]
  by assumption

lemma u32_split_realise:
  "∃ b0 b1 b2 b3. flatten_u32 v = [b0, b1, b2, b3]"
  using list_length_4_realise[where ?ls="flatten_u32 v", OF flatten_u32_length[where ?vs=v]]
  by assumption

lemma s32_split_realise:
  "∃ b0 b1 b2 b3. flatten_s32 v = [b0, b1, b2, b3]"
  using list_length_4_realise[where ?ls="flatten_s32 v", OF flatten_s32_length[where ?vs=v]]
  by assumption

lemma u64_split_realise:
  "∃ b0 b1 b2 b3 b4 b5 b6 b7. flatten_u64 v = [b0, b1, b2, b3, b4, b5, b6, b7]"
  using list_length_8_realise[where ?ls="flatten_u64 v", OF flatten_u64_length[where ?vs=v]]
  by assumption

lemma s64_split_realise:
  "∃ b0 b1 b2 b3 b4 b5 b6 b7. flatten_s64 v = [b0, b1, b2, b3, b4, b5, b6, b7]"
  using list_length_8_realise[where ?ls="flatten_s64 v", OF flatten_s64_length[where ?vs=v]]
  by assumption

lemma store_bytes_u16:
  shows "off ∈ Mapping.keys (store_bytes m off (u16_split v))"
    and "Suc off ∈ Mapping.keys (store_bytes m off (u16_split v))"
    and "∃ b0. Mapping.lookup (store_bytes m off (u16_split v)) off = Some (Byte b0)"
    and "∃ b1. Mapping.lookup (store_bytes m off (u16_split v)) (Suc off) = Some (Byte b1)" 
proof -
  show "off ∈ Mapping.keys (store_bytes m off (u16_split v))"
    by (metis (no_types, opaque_lifting) domIff u16_split_realise handy_if_lemma keys_dom_lookup 
        stored_bytes_instant_correctness)
next
  show "Suc off ∈ Mapping.keys (store_bytes m off (u16_split v))"
    by (metis (mono_tags, opaque_lifting) domIff u16_split_realise handy_if_lemma keys_dom_lookup 
        store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "∃ b0. Mapping.lookup (store_bytes m off (u16_split v)) off = Some (Byte b0)"
    by (metis u16_split_realise stored_bytes_instant_correctness)
next
  show "∃ b1. Mapping.lookup (store_bytes m off (u16_split v)) (Suc off) = Some (Byte b1)"
    by (metis u16_split_realise store_bytes.simps(2) stored_bytes_instant_correctness)
qed

lemma store_bytes_s16:
  shows "off ∈ Mapping.keys (store_bytes m off (s16_split v))"
    and "Suc off ∈ Mapping.keys (store_bytes m off (s16_split v))"
    and "∃ b0. Mapping.lookup (store_bytes m off (s16_split v)) off = Some (Byte b0)"
    and "∃ b1. Mapping.lookup (store_bytes m off (s16_split v)) (Suc off) = Some (Byte b1)" 
proof -
  show "off ∈ Mapping.keys (store_bytes m off (s16_split v))"
    by (metis (no_types, opaque_lifting) domIff s16_split_realise handy_if_lemma keys_dom_lookup 
        stored_bytes_instant_correctness)
next
  show "Suc off ∈ Mapping.keys (store_bytes m off (s16_split v))"
    by (metis (mono_tags, opaque_lifting) domIff s16_split_realise handy_if_lemma keys_dom_lookup 
        store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "∃ b0. Mapping.lookup (store_bytes m off (s16_split v)) off = Some (Byte b0)"
    by (metis s16_split_realise stored_bytes_instant_correctness)
next
  show "∃ b1. Mapping.lookup (store_bytes m off (s16_split v)) (Suc off) = Some (Byte b1)"
    by (metis s16_split_realise store_bytes.simps(2) stored_bytes_instant_correctness)
qed

lemma store_bytes_u32:
  shows "off ∈ Mapping.keys (store_bytes m off (flatten_u32 v))"
    and "Suc off ∈ Mapping.keys (store_bytes m off (flatten_u32 v))"
    and "Suc (Suc off) ∈ Mapping.keys (store_bytes m off (flatten_u32 v))"
    and "Suc (Suc (Suc off)) ∈ Mapping.keys (store_bytes m off (flatten_u32 v))"
    and "∃ b0. Mapping.lookup (store_bytes m off (flatten_u32 v)) off = Some (Byte b0)"
    and "∃ b1. Mapping.lookup (store_bytes m off (flatten_u32 v)) (Suc off) = Some (Byte b1)"
    and "∃ b2. Mapping.lookup (store_bytes m off (flatten_u32 v)) (Suc (Suc off)) = Some (Byte b2)"
    and "∃ b3. Mapping.lookup (store_bytes m off (flatten_u32 v)) (Suc (Suc (Suc off))) = Some (Byte b3)" 
proof -
  show "off ∈ Mapping.keys (store_bytes m off (flatten_u32 v))" 
    by (metis (no_types, opaque_lifting) domIff handy_if_lemma keys_dom_lookup 
        stored_bytes_instant_correctness u32_split_realise)
next
  show "Suc off ∈ Mapping.keys (store_bytes m off (flatten_u32 v))" 
    by (metis (mono_tags, opaque_lifting) domIff u32_split_realise handy_if_lemma keys_dom_lookup 
        store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "Suc (Suc off) ∈ Mapping.keys (store_bytes m off (flatten_u32 v))"
    by (metis (mono_tags, opaque_lifting) domIff u32_split_realise handy_if_lemma keys_dom_lookup 
        store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "Suc (Suc (Suc off)) ∈ Mapping.keys (store_bytes m off (flatten_u32 v))"
    by (metis (mono_tags, opaque_lifting) domIff u32_split_realise handy_if_lemma keys_dom_lookup 
        store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "∃ b0. Mapping.lookup (store_bytes m off (flatten_u32 v)) off = Some (Byte b0)"
    by (metis u32_split_realise stored_bytes_instant_correctness)
next
  show "∃ b1. Mapping.lookup (store_bytes m off (flatten_u32 v)) (Suc off) = Some (Byte b1)"
    by (metis u32_split_realise store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "∃ b2. Mapping.lookup (store_bytes m off (flatten_u32 v)) (Suc (Suc off)) = Some (Byte b2)"
    by (metis u32_split_realise store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "∃ b3. Mapping.lookup (store_bytes m off (flatten_u32 v)) (Suc (Suc (Suc off))) = Some (Byte b3)" 
    by (metis u32_split_realise store_bytes.simps(2) stored_bytes_instant_correctness)
qed

lemma store_bytes_s32:
  shows "off ∈ Mapping.keys (store_bytes m off (flatten_s32 v))"
    and "Suc off ∈ Mapping.keys (store_bytes m off (flatten_s32 v))"
    and "Suc (Suc off) ∈ Mapping.keys (store_bytes m off (flatten_s32 v))"
    and "Suc (Suc (Suc off)) ∈ Mapping.keys (store_bytes m off (flatten_s32 v))"
    and "∃ b0. Mapping.lookup (store_bytes m off (flatten_s32 v)) off = Some (Byte b0)"
    and "∃ b1. Mapping.lookup (store_bytes m off (flatten_s32 v)) (Suc off) = Some (Byte b1)"
    and "∃ b2. Mapping.lookup (store_bytes m off (flatten_s32 v)) (Suc (Suc off)) = Some (Byte b2)"
    and "∃ b3. Mapping.lookup (store_bytes m off (flatten_s32 v)) (Suc (Suc (Suc off))) = Some (Byte b3)" 
proof -
  show "off ∈ Mapping.keys (store_bytes m off (flatten_s32 v))" 
    by (metis (no_types, opaque_lifting) domIff handy_if_lemma keys_dom_lookup 
        stored_bytes_instant_correctness s32_split_realise)
next
  show "Suc off ∈ Mapping.keys (store_bytes m off (flatten_s32 v))" 
    by (metis (mono_tags, opaque_lifting) domIff s32_split_realise handy_if_lemma keys_dom_lookup 
        store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "Suc (Suc off) ∈ Mapping.keys (store_bytes m off (flatten_s32 v))"
    by (metis (mono_tags, opaque_lifting) domIff s32_split_realise handy_if_lemma keys_dom_lookup 
        store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "Suc (Suc (Suc off)) ∈ Mapping.keys (store_bytes m off (flatten_s32 v))"
    by (metis (mono_tags, opaque_lifting) domIff s32_split_realise handy_if_lemma keys_dom_lookup 
        store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "∃ b0. Mapping.lookup (store_bytes m off (flatten_s32 v)) off = Some (Byte b0)"
    by (metis s32_split_realise stored_bytes_instant_correctness)
next
  show "∃ b1. Mapping.lookup (store_bytes m off (flatten_s32 v)) (Suc off) = Some (Byte b1)"
    by (metis s32_split_realise store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "∃ b2. Mapping.lookup (store_bytes m off (flatten_s32 v)) (Suc (Suc off)) = Some (Byte b2)"
    by (metis s32_split_realise store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "∃ b3. Mapping.lookup (store_bytes m off (flatten_s32 v)) (Suc (Suc (Suc off))) = Some (Byte b3)" 
    by (metis s32_split_realise store_bytes.simps(2) stored_bytes_instant_correctness)
qed

lemma store_bytes_u64:
  shows "off ∈ Mapping.keys (store_bytes m off (flatten_u64 v))"
    and "Suc off ∈ Mapping.keys (store_bytes m off (flatten_u64 v))"
    and "Suc (Suc off) ∈ Mapping.keys (store_bytes m off (flatten_u64 v))"
    and "Suc (Suc (Suc off)) ∈ Mapping.keys (store_bytes m off (flatten_u64 v))"
    and "Suc (Suc (Suc (Suc off))) ∈ Mapping.keys (store_bytes m off (flatten_u64 v))"
    and "Suc (Suc (Suc (Suc (Suc off)))) ∈ Mapping.keys (store_bytes m off (flatten_u64 v))"
    and "Suc (Suc (Suc (Suc (Suc (Suc off))))) ∈ Mapping.keys (store_bytes m off (flatten_u64 v))"
    and "Suc (Suc (Suc (Suc (Suc (Suc (Suc off)))))) ∈ Mapping.keys (store_bytes m off (flatten_u64 v))"
    and "∃ b0. Mapping.lookup (store_bytes m off (flatten_u64 v)) off = Some (Byte b0)"
    and "∃ b1. Mapping.lookup (store_bytes m off (flatten_u64 v)) (Suc off) = Some (Byte b1)"
    and "∃ b2. Mapping.lookup (store_bytes m off (flatten_u64 v)) (Suc (Suc off)) = Some (Byte b2)"
    and "∃ b3. Mapping.lookup (store_bytes m off (flatten_u64 v)) (Suc (Suc (Suc off))) = Some (Byte b3)"
    and "∃ b0. Mapping.lookup (store_bytes m off (flatten_u64 v)) (Suc (Suc (Suc (Suc off)))) = Some (Byte b0)"
    and "∃ b1. Mapping.lookup (store_bytes m off (flatten_u64 v)) (Suc (Suc (Suc (Suc (Suc off))))) = Some (Byte b1)"
    and "∃ b2. Mapping.lookup (store_bytes m off (flatten_u64 v)) (Suc (Suc (Suc (Suc (Suc (Suc off)))))) = Some (Byte b2)"
    and "∃ b3. Mapping.lookup (store_bytes m off (flatten_u64 v)) (Suc (Suc (Suc (Suc (Suc (Suc (Suc off))))))) = Some (Byte b3)"
proof -
  show "off ∈ Mapping.keys (store_bytes m off (flatten_u64 v))"
    by (metis (no_types, opaque_lifting) domIff handy_if_lemma keys_dom_lookup 
        stored_bytes_instant_correctness u64_split_realise)
next
  show "Suc off ∈ Mapping.keys (store_bytes m off (flatten_u64 v))" 
    by (metis (mono_tags, opaque_lifting) domIff u64_split_realise handy_if_lemma keys_dom_lookup 
        store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "Suc (Suc off) ∈ Mapping.keys (store_bytes m off (flatten_u64 v))"
    by (metis (mono_tags, opaque_lifting) domIff u64_split_realise handy_if_lemma keys_dom_lookup 
        store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "Suc (Suc (Suc off)) ∈ Mapping.keys (store_bytes m off (flatten_u64 v))"
    by (metis (mono_tags, opaque_lifting) domIff u64_split_realise handy_if_lemma keys_dom_lookup 
        store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "Suc (Suc (Suc (Suc off))) ∈ Mapping.keys (store_bytes m off (flatten_u64 v))"
    by (metis (mono_tags, opaque_lifting) domIff u64_split_realise handy_if_lemma keys_dom_lookup 
        store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "Suc (Suc (Suc (Suc (Suc off)))) ∈ Mapping.keys (store_bytes m off (flatten_u64 v))"
    by (metis (mono_tags, opaque_lifting) domIff u64_split_realise handy_if_lemma keys_dom_lookup 
        store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "Suc (Suc (Suc (Suc (Suc (Suc off))))) ∈ Mapping.keys (store_bytes m off (flatten_u64 v))"
    by (metis (mono_tags, opaque_lifting) domIff u64_split_realise handy_if_lemma keys_dom_lookup 
        store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "Suc (Suc (Suc (Suc (Suc (Suc (Suc off)))))) ∈ Mapping.keys (store_bytes m off (flatten_u64 v))"
    by (metis (mono_tags, opaque_lifting) domIff u64_split_realise handy_if_lemma keys_dom_lookup 
        store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "∃ b0. Mapping.lookup (store_bytes m off (flatten_u64 v)) off = Some (Byte b0)"
    by (metis u64_split_realise stored_bytes_instant_correctness)
next
  show "∃ b1. Mapping.lookup (store_bytes m off (flatten_u64 v)) (Suc off) = Some (Byte b1)"
    by (metis u64_split_realise store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "∃ b2. Mapping.lookup (store_bytes m off (flatten_u64 v)) (Suc (Suc off)) = Some (Byte b2)"
    by (metis u64_split_realise store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "∃ b3. Mapping.lookup (store_bytes m off (flatten_u64 v)) (Suc (Suc (Suc off))) = Some (Byte b3)" 
    by (metis u64_split_realise store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "∃ b0. Mapping.lookup (store_bytes m off (flatten_u64 v)) (Suc (Suc (Suc (Suc off)))) = Some (Byte b0)"
    by (metis u64_split_realise store_bytes.simps(2) stored_bytes_instant_correctness)
next 
  show"∃ b1. Mapping.lookup (store_bytes m off (flatten_u64 v)) (Suc (Suc (Suc (Suc (Suc off))))) = Some (Byte b1)"
    by (metis u64_split_realise store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "∃ b2. Mapping.lookup (store_bytes m off (flatten_u64 v)) (Suc (Suc (Suc (Suc (Suc (Suc off)))))) = Some (Byte b2)"
    by (metis u64_split_realise store_bytes.simps(2) stored_bytes_instant_correctness)
next 
  show "∃ b3. Mapping.lookup (store_bytes m off (flatten_u64 v)) (Suc (Suc (Suc (Suc (Suc (Suc (Suc off))))))) = Some (Byte b3)"
    by (metis u64_split_realise store_bytes.simps(2) stored_bytes_instant_correctness)
qed

lemma store_bytes_s64:
  shows "off ∈ Mapping.keys (store_bytes m off (flatten_s64 v))"
    and "Suc off ∈ Mapping.keys (store_bytes m off (flatten_s64 v))"
    and "Suc (Suc off) ∈ Mapping.keys (store_bytes m off (flatten_s64 v))"
    and "Suc (Suc (Suc off)) ∈ Mapping.keys (store_bytes m off (flatten_s64 v))"
    and "Suc (Suc (Suc (Suc off))) ∈ Mapping.keys (store_bytes m off (flatten_s64 v))"
    and "Suc (Suc (Suc (Suc (Suc off)))) ∈ Mapping.keys (store_bytes m off (flatten_s64 v))"
    and "Suc (Suc (Suc (Suc (Suc (Suc off))))) ∈ Mapping.keys (store_bytes m off (flatten_s64 v))"
    and "Suc (Suc (Suc (Suc (Suc (Suc (Suc off)))))) ∈ Mapping.keys (store_bytes m off (flatten_s64 v))"
    and "∃ b0. Mapping.lookup (store_bytes m off (flatten_s64 v)) off = Some (Byte b0)"
    and "∃ b1. Mapping.lookup (store_bytes m off (flatten_s64 v)) (Suc off) = Some (Byte b1)"
    and "∃ b2. Mapping.lookup (store_bytes m off (flatten_s64 v)) (Suc (Suc off)) = Some (Byte b2)"
    and "∃ b3. Mapping.lookup (store_bytes m off (flatten_s64 v)) (Suc (Suc (Suc off))) = Some (Byte b3)"
    and "∃ b0. Mapping.lookup (store_bytes m off (flatten_s64 v)) (Suc (Suc (Suc (Suc off)))) = Some (Byte b0)"
    and "∃ b1. Mapping.lookup (store_bytes m off (flatten_s64 v)) (Suc (Suc (Suc (Suc (Suc off))))) = Some (Byte b1)"
    and "∃ b2. Mapping.lookup (store_bytes m off (flatten_s64 v)) (Suc (Suc (Suc (Suc (Suc (Suc off)))))) = Some (Byte b2)"
    and "∃ b3. Mapping.lookup (store_bytes m off (flatten_s64 v)) (Suc (Suc (Suc (Suc (Suc (Suc (Suc off))))))) = Some (Byte b3)"
proof -
  show "off ∈ Mapping.keys (store_bytes m off (flatten_s64 v))"
    by (metis (no_types, opaque_lifting) domIff handy_if_lemma keys_dom_lookup 
        stored_bytes_instant_correctness s64_split_realise)
next
  show "Suc off ∈ Mapping.keys (store_bytes m off (flatten_s64 v))" 
    by (metis (mono_tags, opaque_lifting) domIff s64_split_realise handy_if_lemma keys_dom_lookup 
        store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "Suc (Suc off) ∈ Mapping.keys (store_bytes m off (flatten_s64 v))"
    by (metis (mono_tags, opaque_lifting) domIff s64_split_realise handy_if_lemma keys_dom_lookup 
        store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "Suc (Suc (Suc off)) ∈ Mapping.keys (store_bytes m off (flatten_s64 v))"
    by (metis (mono_tags, opaque_lifting) domIff s64_split_realise handy_if_lemma keys_dom_lookup 
        store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "Suc (Suc (Suc (Suc off))) ∈ Mapping.keys (store_bytes m off (flatten_s64 v))"
    by (metis (mono_tags, opaque_lifting) domIff s64_split_realise handy_if_lemma keys_dom_lookup 
        store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "Suc (Suc (Suc (Suc (Suc off)))) ∈ Mapping.keys (store_bytes m off (flatten_s64 v))"
    by (metis (mono_tags, opaque_lifting) domIff s64_split_realise handy_if_lemma keys_dom_lookup 
        store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "Suc (Suc (Suc (Suc (Suc (Suc off))))) ∈ Mapping.keys (store_bytes m off (flatten_s64 v))"
    by (metis (mono_tags, opaque_lifting) domIff s64_split_realise handy_if_lemma keys_dom_lookup 
        store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "Suc (Suc (Suc (Suc (Suc (Suc (Suc off)))))) ∈ Mapping.keys (store_bytes m off (flatten_s64 v))"
    by (metis (mono_tags, opaque_lifting) domIff s64_split_realise handy_if_lemma keys_dom_lookup 
        store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "∃ b0. Mapping.lookup (store_bytes m off (flatten_s64 v)) off = Some (Byte b0)"
    by (metis s64_split_realise stored_bytes_instant_correctness)
next
  show "∃ b1. Mapping.lookup (store_bytes m off (flatten_s64 v)) (Suc off) = Some (Byte b1)"
    by (metis s64_split_realise store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "∃ b2. Mapping.lookup (store_bytes m off (flatten_s64 v)) (Suc (Suc off)) = Some (Byte b2)"
    by (metis s64_split_realise store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "∃ b3. Mapping.lookup (store_bytes m off (flatten_s64 v)) (Suc (Suc (Suc off))) = Some (Byte b3)" 
    by (metis s64_split_realise store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "∃ b0. Mapping.lookup (store_bytes m off (flatten_s64 v)) (Suc (Suc (Suc (Suc off)))) = Some (Byte b0)"
    by (metis s64_split_realise store_bytes.simps(2) stored_bytes_instant_correctness)
next 
  show"∃ b1. Mapping.lookup (store_bytes m off (flatten_s64 v)) (Suc (Suc (Suc (Suc (Suc off))))) = Some (Byte b1)"
    by (metis s64_split_realise store_bytes.simps(2) stored_bytes_instant_correctness)
next
  show "∃ b2. Mapping.lookup (store_bytes m off (flatten_s64 v)) (Suc (Suc (Suc (Suc (Suc (Suc off)))))) = Some (Byte b2)"
    by (metis s64_split_realise store_bytes.simps(2) stored_bytes_instant_correctness)
next 
  show "∃ b3. Mapping.lookup (store_bytes m off (flatten_s64 v)) (Suc (Suc (Suc (Suc (Suc (Suc (Suc off))))))) = Some (Byte b3)"
    by (metis s64_split_realise store_bytes.simps(2) stored_bytes_instant_correctness)
qed

corollary u16_store_bytes_imp_is_contiguous_bytes:
  "is_contiguous_bytes (store_bytes m off (u16_split v)) off 2"
  by (metis One_nat_def Suc_1 is_contiguous_bytes.simps(1) is_contiguous_bytes.simps(2) memval_memcap_not_byte option.sel store_bytes_u16)

corollary s16_store_bytes_imp_is_contiguous_bytes:
  "is_contiguous_bytes (store_bytes m off (s16_split v)) off 2"
  by (metis One_nat_def Suc_1 is_contiguous_bytes.simps(1) is_contiguous_bytes.simps(2) memval_memcap_not_byte option.sel store_bytes_s16)

corollary u32_store_bytes_imp_is_contiguous_bytes:
  "is_contiguous_bytes (store_bytes m off (flatten_u32 v)) off 4" 
  by(simp add: numeral_4_eq_4, safe) 
    (simp add: store_bytes_u32, metis memval_memcap_not_byte option.sel store_bytes_u32)+ 

corollary s32_store_bytes_imp_is_contiguous_bytes:
  "is_contiguous_bytes (store_bytes m off (flatten_s32 v)) off 4" 
  by(simp add: numeral_4_eq_4, safe) 
    (simp add: store_bytes_s32, metis memval_memcap_not_byte option.sel store_bytes_s32)+

corollary u64_store_bytes_imp_is_contiguous_bytes:
  "is_contiguous_bytes (store_bytes m off (flatten_u64 v)) off 8" 
  by(simp add: numeral_8_eq_8, safe) 
    (simp add: store_bytes_u64, metis memval_memcap_not_byte option.sel store_bytes_u64)+ 

corollary s64_store_bytes_imp_is_contiguous_bytes:
  "is_contiguous_bytes (store_bytes m off (flatten_s64 v)) off 8" 
  by(simp add: numeral_8_eq_8, safe) 
    (simp add: store_bytes_s64, metis memval_memcap_not_byte option.sel store_bytes_s64)+ 

lemma stored_tval_contiguous_bytes:
  assumes "val ≠ Undef"
    and "∀ v. val ≠ Cap_v v"
    and "∀ v n. val ≠ Cap_v_frag v n"
  shows "is_contiguous_bytes (content (store_tval obj off val)) off |memval_type val|⇩τ"
  unfolding sizeof_def
  by (simp add: assms store_tval_def memval_is_byte_def split: ccval.split) (presburger add: s16_store_bytes_imp_is_contiguous_bytes s32_store_bytes_imp_is_contiguous_bytes s64_store_bytes_imp_is_contiguous_bytes u16_store_bytes_imp_is_contiguous_bytes u32_store_bytes_imp_is_contiguous_bytes u64_store_bytes_imp_is_contiguous_bytes)

lemma suc_of_32: 
  "32 = Suc 31"
  by simp

lemma store_cap_correct_dom:
  shows "off      ∈ Mapping.keys (store_cap m off cap 32)"
    and "off + 1  ∈ Mapping.keys (store_cap m off cap 32)"
    and "off + 2  ∈ Mapping.keys (store_cap m off cap 32)"
    and "off + 3  ∈ Mapping.keys (store_cap m off cap 32)"
    and "off + 4  ∈ Mapping.keys (store_cap m off cap 32)"
    and "off + 5  ∈ Mapping.keys (store_cap m off cap 32)"
    and "off + 6  ∈ Mapping.keys (store_cap m off cap 32)"
    and "off + 7  ∈ Mapping.keys (store_cap m off cap 32)"
    and "off + 8  ∈ Mapping.keys (store_cap m off cap 32)"
    and "off + 9  ∈ Mapping.keys (store_cap m off cap 32)"
    and "off + 10 ∈ Mapping.keys (store_cap m off cap 32)"
    and "off + 11 ∈ Mapping.keys (store_cap m off cap 32)"
    and "off + 12 ∈ Mapping.keys (store_cap m off cap 32)"
    and "off + 13 ∈ Mapping.keys (store_cap m off cap 32)"
    and "off + 14 ∈ Mapping.keys (store_cap m off cap 32)"
    and "off + 15 ∈ Mapping.keys (store_cap m off cap 32)"
    and "off + 16 ∈ Mapping.keys (store_cap m off cap 32)"
    and "off + 17 ∈