Theory AutoCorres2.HeapRawState

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

 *)

(* License: BSD, terms see file ./LICENSE *)

theory HeapRawState
imports CTypes
begin

type_synonym typ_base = bool
datatype s_heap_index = SIndexVal | SIndexTyp nat
datatype s_heap_value = SValue byte | STyp "typ_uinfo × typ_base"

primrec (nonexhaustive) s_heap_tag :: "s_heap_value ⇒ typ_uinfo × typ_base" where
  "s_heap_tag (STyp t) = t"

type_synonym typ_slice = "nat ⇀ typ_uinfo × typ_base"
(*  heap_typ_desc = "addr ⇒ tag_ladder"*)
type_synonym s_addr = "addr × s_heap_index"
type_synonym heap_state = "s_addr ⇀ s_heap_value"
type_synonym heap_typ_desc = "addr ⇒ bool × typ_slice"
type_synonym heap_raw_state = "heap_mem × heap_typ_desc"

(* Used in the C parser to avoid loss of information about the relative
   ordering of heap_updates and ptr_tags, as this order conveys the intention
   of the type of a memory location that can be helpful when reducing over
   multiple updates of both the heap memory state and heap type description
*)

definition hrs_mem :: "heap_raw_state ⇒ heap_mem" where
  "hrs_mem ≡ fst"

definition hrs_mem_update :: "(heap_mem ⇒ heap_mem) ⇒ heap_raw_state ⇒ heap_raw_state" where
  "hrs_mem_update f ≡ λ(h,d). (f h,d)"

definition hrs_htd :: "heap_raw_state ⇒ heap_typ_desc" where
  "hrs_htd ≡ snd"

definition hrs_htd_update :: "(heap_typ_desc ⇒ heap_typ_desc) ⇒ heap_raw_state ⇒ heap_raw_state"
  where
  "hrs_htd_update f ≡ λ(h,d). (h,f d)"


lemma hrs_comm:
  "hrs_htd_update d (hrs_mem_update h s) = hrs_mem_update h (hrs_htd_update d s)"
  by (simp add: hrs_htd_update_def hrs_mem_update_def split_def)

lemma hrs_htd_update_htd_update:
  "(λs. hrs_htd_update d (hrs_htd_update d' s)) = hrs_htd_update (d ∘ d')"
  by (simp add: hrs_htd_update_def split_def)

lemma hrs_htd_mem_update [simp]:
  "hrs_htd (hrs_mem_update f s) = hrs_htd s"
  by (simp add: hrs_mem_update_def hrs_htd_def split_def)

lemma hrs_mem_htd_update [simp]:
  "hrs_mem (hrs_htd_update f s) = hrs_mem s"
  by (simp add: hrs_htd_update_def hrs_mem_def split_def)

lemma hrs_mem_update:
  "hrs_mem (hrs_mem_update f s) = (f (hrs_mem s))"
  by (simp add: hrs_mem_update_def hrs_mem_def split_def)

lemma hrs_htd_update:
  "hrs_htd (hrs_htd_update f s) = (f (hrs_htd s))"
  by (simp add: hrs_htd_update_def hrs_htd_def split_def)

lemmas hrs_update = hrs_mem_update hrs_htd_update

lemma hrs_htd_update_comp: "hrs_htd_update f ∘ hrs_htd_update g = hrs_htd_update (f o g)"
  by (auto simp add: hrs_htd_update_def split: prod.splits)

lemma hrs_mem_update_comp: "hrs_mem_update f ∘ hrs_mem_update g = hrs_mem_update (f o g)"
  by (auto simp add: hrs_mem_update_def split: prod.splits)

lemma hrs_update_commute: 
  "hrs_mem_update f ∘ hrs_htd_update g = hrs_htd_update g o hrs_mem_update f"
  by (auto simp add: hrs_mem_update_def hrs_htd_update_def split: prod.splits)

end