Theory CTypesDefs

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

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

(* Definitions supporting the extremely long CTypes.thy *)

theory CTypesDefs
imports
  CTypesBase
begin

section "C types setup"

type_synonym field_name = string
type_synonym qualified_field_name = "field_name list"

type_synonym typ_name = string


text ‹A ‹typ_desc› wraps a ‹typ_struct› with a typ name.
        A ‹typ_struct› is either a Scalar, with size, alignment and either a
        field description (for ‹typ_info›) or a 'normalisor'
        (for ‹typ_uinfo›), or an Aggregate, with a list of ‹typ_desc›,
        field name, and field descripton (for the complete sub-structure) or unit
        (for ‹typ_uinfo›). The field description for aggregates is an extension of
        the original work of H. Tuch. It is used to make the construction of a new structure from
        nested structures / arrays more efficient. Properties like commutation of fields can
        be expressed and proven for the toplevel fields only, without having to re-examine the
        nested leafs of the tree.
›

datatype
         ('a,'b) typ_desc   = TypDesc nat "('a, 'b) typ_struct" typ_name
    and  ('a,'b) typ_struct = TypScalar nat nat "'a" |
                         TypAggregate "(('a, 'b) typ_desc, field_name, 'b) dt_tuple list"

datatype_compat dt_tuple
datatype_compat typ_desc typ_struct
print_theorems
(* These recreate the precise order of subgoals of the old datatype package *)
lemma typ_desc_induct:
  "⟦⋀nat typ_struct list. P2 typ_struct ⟹ P1 (TypDesc nat typ_struct list); ⋀nat1 nat2 a. P2 (TypScalar nat1 nat2 a);
       ⋀list. P3 list ⟹ P2 (TypAggregate list); P3 []; ⋀dt_tuple list. ⟦P4 dt_tuple; P3 list⟧ ⟹ P3 (dt_tuple # list);
       ⋀typ_desc list b. P1 typ_desc ⟹ P4 (DTuple typ_desc list b)⟧
      ⟹ P1 typ_desc"
   by (rule compat_typ_desc.induct)

lemma typ_struct_induct:
    "⟦⋀nat typ_struct list. P2 typ_struct ⟹ P1 (TypDesc nat typ_struct list); ⋀nat1 nat2 a. P2 (TypScalar nat1 nat2 a);
       ⋀list. P3 list ⟹ P2 (TypAggregate list); P3 []; ⋀dt_tuple list. ⟦P4 dt_tuple; P3 list⟧ ⟹ P3 (dt_tuple # list);
       ⋀typ_desc list b. P1 typ_desc ⟹ P4 (DTuple typ_desc list b)⟧
      ⟹ P2 typ_struct"
   by (rule compat_typ_struct.induct)

lemma typ_list_induct:
    "⟦⋀nat typ_struct list. P2 typ_struct ⟹ P1 (TypDesc nat typ_struct list); ⋀nat1 nat2 a. P2 (TypScalar nat1 nat2 a);
      ⋀list. P3 list ⟹ P2 (TypAggregate list); P3 []; ⋀dt_tuple list. ⟦P4 dt_tuple; P3 list⟧ ⟹ P3 (dt_tuple # list);
      ⋀typ_desc list b. P1 typ_desc ⟹ P4 (DTuple typ_desc list b)⟧
     ⟹ P3 list"
   by (rule compat_typ_desc_char_list_dt_tuple_list.induct)

lemma typ_dt_tuple_induct:
    "⟦⋀nat typ_struct list. P2 typ_struct ⟹ P1 (TypDesc nat typ_struct list); ⋀nat1 nat2 a. P2 (TypScalar nat1 nat2 a);
      ⋀list. P3 list ⟹ P2 (TypAggregate list); P3 []; ⋀dt_tuple list. ⟦P4 dt_tuple; P3 list⟧ ⟹ P3 (dt_tuple # list);
      ⋀typ_desc list b. P1 typ_desc ⟹ P4 (DTuple typ_desc list b)⟧
     ⟹ P4 dt_tuple"
   by (rule compat_typ_desc_char_list_dt_tuple.induct)

― ‹Declare as default induct rule with old case names›
lemmas typ_desc_typ_struct_inducts [case_names
  TypDesc TypScalar TypAggregate Nil_typ_desc Cons_typ_desc DTuple_typ_desc, induct type] =
  typ_desc_induct typ_struct_induct typ_list_induct typ_dt_tuple_induct

― ‹Make sure list induct rule is tried first›
declare list.induct [induct type]

type_synonym ('a, 'b) typ_tuple = "(('a, 'b) typ_desc,field_name, 'b) dt_tuple"

type_synonym typ_uinfo = "(normalisor, unit) typ_desc"
type_synonym typ_uinfo_struct = "(normalisor, unit) typ_struct"
type_synonym typ_uinfo_tuple = "(normalisor, unit) typ_tuple"

record 'a field_desc =
  field_access :: "'a ⇒ byte list ⇒ byte list"
  field_update :: "byte list ⇒ 'a ⇒ 'a"
  field_sz :: nat

type_synonym ('a, 'b) typ_info = "('a field_desc, 'b) typ_desc"
type_synonym ('a, 'b) typ_info_struct = "('a field_desc, 'b) typ_struct"
type_synonym ('a, 'b) typ_info_tuple = "('a field_desc, 'b) typ_tuple"

type_synonym 'a xtyp_tuple = "('a, 'a) typ_tuple"
type_synonym 'a xtyp_info = "('a field_desc, 'a field_desc) typ_desc"
type_synonym 'a xtyp_info_struct = "('a field_desc, 'a field_desc) typ_struct"
type_synonym 'a xtyp_info_tuple = "'a field_desc xtyp_tuple"

definition fu_commutes :: "('b ⇒ 'a ⇒ 'a) ⇒ ('c ⇒ 'a ⇒ 'a) ⇒ bool" where
  "fu_commutes f g ≡ ∀v bs bs'. f bs (g bs' v) = g bs' (f bs v)"


text ‹‹size_td› returns the sum of the sizes of all Scalar fields
        comprising a ‹typ_desc› i.e. the overall size of the type›

(* Could express this and many other typ_desc primrecs as tree fold/map
   combos, but the intuition this way is clearer for anything non-trivial *)
primrec
  size_td :: "('a, 'b) typ_desc ⇒ nat" and
  size_td_struct :: "('a, 'b) typ_struct ⇒ nat" and
  size_td_list :: "('a, 'b) typ_tuple list ⇒ nat" and
  size_td_tuple :: "('a, 'b) typ_tuple ⇒ nat"
where
  tz0: "size_td (TypDesc algn st nm) = size_td_struct st"

| tz1: "size_td_struct (TypScalar n algn d) = n"
| tz2: "size_td_struct (TypAggregate xs) = size_td_list xs"

| tz3: "size_td_list [] = 0"
| tz4: "size_td_list (x#xs) = size_td_tuple x + size_td_list xs"

| tz5: "size_td_tuple (DTuple t n d) = size_td t"


text ‹‹access_ti› overlays the byte-wise representation of an object
        on a given byte list, given the ‹typ_info› (i.e. the layout)›

primrec
  access_ti :: "('a, 'b) typ_info ⇒ ('a ⇒ byte list ⇒ byte list)" and
  access_ti_struct :: "('a, 'b) typ_info_struct ⇒
    ('a ⇒ byte list ⇒ byte list)" and
  access_ti_list :: "('a,  'b) typ_info_tuple list ⇒
    ('a ⇒ byte list ⇒ byte list)" and
  access_ti_tuple :: "('a, 'b) typ_info_tuple ⇒ ('a ⇒ byte list ⇒ byte list)"
where
  fa0: "access_ti (TypDesc algn st nm) = access_ti_struct st"

| fa1: "access_ti_struct (TypScalar n algn d) = field_access d"
| fa2: "access_ti_struct (TypAggregate xs) = access_ti_list xs"

| fa3: "access_ti_list [] = (λv bs. [])"
| fa4: "access_ti_list (x#xs) =
         (λv bs. access_ti_tuple x v (take (size_td_tuple x) bs) @
                 access_ti_list xs v (drop (size_td_tuple x) bs))"

| fa5: "access_ti_tuple (DTuple t nm d) = access_ti t"

text ‹@{text access_ti⇩0} overlays the representation of an object on a
        list of zero bytes›

definition access_ti⇩0 :: "('a, 'b) typ_info ⇒ ('a ⇒ byte list)" where
  "access_ti⇩0 t ≡ λv. access_ti t v (replicate (size_td t) 0)"

text ‹‹update_ti› updates an object, given a list of bytes (the
        representation of the new value), and the ‹typ_info››

primrec
  update_ti :: "('a, 'b) typ_info ⇒ (byte list ⇒ 'a ⇒ 'a)" and
  update_ti_struct :: "('a, 'b) typ_info_struct ⇒ (byte list ⇒ 'a ⇒ 'a)" and
  update_ti_list :: "('a, 'b) typ_info_tuple list ⇒ (byte list ⇒ 'a ⇒ 'a)" and
  update_ti_tuple :: "('a, 'b) typ_info_tuple ⇒ (byte list ⇒ 'a ⇒ 'a)"
where
  fu0: "update_ti (TypDesc algn st nm) = update_ti_struct st"

| fu1: "update_ti_struct (TypScalar n algn d) = field_update d"
| fu2: "update_ti_struct (TypAggregate xs) = update_ti_list xs"

| fu3: "update_ti_list [] = (λbs. id)"
| fu4: "update_ti_list (x#xs) = (λbs v.
         update_ti_tuple x (take (size_td_tuple x) bs)
             (update_ti_list xs (drop (size_td_tuple x) bs) v))"

| fu5: "update_ti_tuple (DTuple t nm d) = update_ti t"


text ‹‹update_ti_t› updates an object only if the length of the
        supplied representation equals the object size›

definition update_ti_t :: "('a, 'b) typ_info ⇒ (byte list ⇒ 'a ⇒ 'a)" where
  "update_ti_t t ≡ λbs. if length bs = size_td t then
      update_ti t bs else id"

definition update_ti_struct_t :: "('a, 'b) typ_info_struct ⇒ (byte list ⇒ 'a ⇒ 'a)" where
  "update_ti_struct_t t ≡ λbs. if length bs = size_td_struct t then
      update_ti_struct t bs else id"

definition update_ti_list_t :: "('a, 'b) typ_info_tuple list  ⇒ (byte list ⇒ 'a ⇒ 'a)" where
  "update_ti_list_t t ≡ λbs. if length bs = size_td_list t then
      update_ti_list t bs else id"

definition update_ti_tuple_t :: "('a, 'b) typ_info_tuple ⇒ (byte list ⇒ 'a ⇒ 'a)" where
  "update_ti_tuple_t t ≡ λbs. if length bs = size_td_tuple t then
      update_ti_tuple t bs else id"

lemma update_ti_t_struct_t [simp]: "update_ti_t (TypDesc algn st nm) = update_ti_struct_t st"
  apply (rule ext)
  apply (simp add: update_ti_t_def update_ti_struct_t_def)
  done

lemma update_ti_update_ti_t:
  "length bs = size_td s ⟹ update_ti s bs v = update_ti_t s bs v"
  unfolding update_ti_t_def by simp

text ‹‹field_desc› generates the access/update pair for a field,
        given the field's ‹type_desc››

definition field_desc :: "('a,  'b) typ_info ⇒ 'a field_desc" where
  "field_desc t ≡ ⦇ field_access = access_ti t,
      field_update = update_ti_t t, field_sz = size_td t ⦈"

declare field_desc_def [simp add]

definition field_desc_struct :: "('a, 'b) typ_info_struct ⇒ 'a field_desc" where
  "field_desc_struct t ≡ ⦇ field_access = access_ti_struct t,
      field_update = update_ti_struct_t t, field_sz = size_td_struct t ⦈"

declare field_desc_struct_def [simp add]

definition field_desc_list :: "('a, 'b) typ_info_tuple list ⇒ 'a field_desc"
where
  "field_desc_list t ≡ ⦇ field_access = access_ti_list t,
      field_update = update_ti_list_t t, field_sz = size_td_list t ⦈"

declare field_desc_list_def [simp add]

definition field_desc_tuple :: "('a, 'b) typ_info_tuple ⇒ 'a field_desc"
where
  "field_desc_tuple t ≡ ⦇ field_access = access_ti_tuple t,
      field_update = update_ti_tuple_t t, field_sz = size_td_tuple t ⦈"

declare field_desc_tuple_def [simp add]


primrec
  map_td :: "(nat ⇒ nat ⇒ 'a ⇒ 'b) ⇒ ('c ⇒ 'd) ⇒ ('a, 'c) typ_desc ⇒ ('b, 'd) typ_desc" and
  map_td_struct :: "(nat ⇒ nat ⇒ 'a ⇒ 'b) ⇒ ('c ⇒ 'd) ⇒ ('a, 'c) typ_struct  ⇒ ('b, 'd) typ_struct" and
  map_td_list :: "(nat ⇒ nat ⇒ 'a ⇒ 'b) ⇒ ('c ⇒ 'd) ⇒ ('a, 'c) typ_tuple list ⇒
    ('b, 'd) typ_tuple list" and
  map_td_tuple :: "(nat ⇒ nat ⇒ 'a  ⇒ 'b) ⇒ ('c ⇒ 'd) ⇒ ('a, 'c) typ_tuple ⇒ ('b, 'd) typ_tuple"
where
  mat0: "map_td f g (TypDesc algn st nm) = TypDesc algn (map_td_struct f g st) nm"

| mat1: "map_td_struct f g (TypScalar n algn d) = TypScalar n algn (f n algn d)"
| mat2: "map_td_struct f g (TypAggregate xs) = TypAggregate (map_td_list f g xs)"

| mat3: "map_td_list f g [] = []"
| mat4: "map_td_list f g (x#xs) = map_td_tuple f g x # map_td_list f g xs"

| mat5: "map_td_tuple f g (DTuple t n d) = DTuple (map_td f g t) n (g d)"

definition field_norm :: "nat ⇒ nat ⇒ ('a,'b) field_desc_scheme ⇒ (byte list ⇒ byte list)"
where
  "field_norm ≡ λn algn d bs.
      if length bs = n then
          field_access d (field_update d bs undefined) (replicate n 0) else
          []"

definition export_uinfo :: "('a, 'b) typ_info ⇒ typ_uinfo" where
  "export_uinfo t ≡ map_td field_norm (λ_. ()) t"


primrec
  wf_desc :: "('a, 'b) typ_desc ⇒ bool" and
  wf_desc_struct :: "('a, 'b) typ_struct ⇒ bool" and
  wf_desc_list :: "('a, 'b) typ_tuple list ⇒ bool" and
  wf_desc_tuple :: "('a, 'b) typ_tuple ⇒ bool"
where
  wfd0: "wf_desc (TypDesc algn ts n) = wf_desc_struct ts"

| wfd1: "wf_desc_struct (TypScalar n algn d) = True"
| wfd2: "wf_desc_struct (TypAggregate ts) = wf_desc_list ts"

| wfd3: "wf_desc_list [] = True"
| wfd4: "wf_desc_list (x#xs) = (wf_desc_tuple x ∧ ¬ dt_snd x ∈ dt_snd ` set xs ∧
          wf_desc_list xs)"

| wfd5: "wf_desc_tuple (DTuple x n d) = wf_desc x"


primrec
  wf_size_desc :: "('a, 'b) typ_desc ⇒ bool" and
  wf_size_desc_struct :: "('a, 'b) typ_struct ⇒ bool" and
  wf_size_desc_list :: "('a, 'b) typ_tuple list ⇒ bool" and
  wf_size_desc_tuple :: "('a, 'b) typ_tuple ⇒ bool"
where
  wfsd0: "wf_size_desc (TypDesc algn ts n) = wf_size_desc_struct ts"

| wfsd1: "wf_size_desc_struct (TypScalar n algn d) = (0 < n)"
| wfsd2: "wf_size_desc_struct (TypAggregate ts) =
           (ts ≠ [] ∧ wf_size_desc_list ts)"

| wfsd3: "wf_size_desc_list [] = True"
| wfsd4: "wf_size_desc_list (x#xs) =
           (wf_size_desc_tuple x ∧ wf_size_desc_list xs)"

| wfsd5: "wf_size_desc_tuple (DTuple x n d) = wf_size_desc x"


definition
  typ_struct :: "('a, 'b) typ_desc ⇒ ('a, 'b) typ_struct"
where
  "typ_struct t = (case t of TypDesc algn st sz ⇒ st)"

lemma typ_struct [simp]:
  "typ_struct (TypDesc algn st sz) = st"
  by (simp add: typ_struct_def)

primrec
  typ_name :: "('a, 'b) typ_desc ⇒ typ_name"
where
  "typ_name (TypDesc algn st nm) = nm"


primrec
  norm_tu :: "typ_uinfo ⇒ normalisor" and
  norm_tu_struct :: "typ_uinfo_struct ⇒ normalisor" and
  norm_tu_list :: "typ_uinfo_tuple list ⇒ normalisor" and
  norm_tu_tuple :: "typ_uinfo_tuple ⇒ normalisor"
where
  tn0: "norm_tu (TypDesc algn st nm) = norm_tu_struct st"

| tn1: "norm_tu_struct (TypScalar n aln f) = f"
| tn2: "norm_tu_struct (TypAggregate xs) = norm_tu_list xs"

| tn3: "norm_tu_list [] = (λbs. [])"
| tn4: "norm_tu_list (x#xs) = (λbs.
         norm_tu_tuple x (take (size_td_tuple x) bs) @
         norm_tu_list xs (drop (size_td_tuple x) bs))"

| tn5: "norm_tu_tuple (DTuple t n d) = norm_tu t"

class c_type_name =
  fixes
    typ_name_itself :: "'a itself ⇒ typ_name"

class c_type = c_type_name +
  fixes
    typ_info_t :: "'a itself ⇒ 'a xtyp_info"
  assumes type_name_itself_typ_name: "typ_name_itself T = typ_name (typ_info_t T)"

instance c_type ⊆ type ..


definition (in c_type) typ_uinfo_t :: "'a itself ⇒ typ_uinfo" where
  "typ_uinfo_t t ≡ export_uinfo (typ_info_t TYPE('a))"

definition (in c_type) to_bytes :: "'a ⇒ byte list ⇒ byte list" where
  "to_bytes v ≡ access_ti (typ_info_t TYPE('a)) v"


(* from_bytes is now total - all partial C types 'a need to be instantiated
   as c_types using 'a option and the parser needs to do some work
   extracting the value and generating guards for non-None when these are
   used. Luckily for us in our work we never use them. *)
definition (in c_type) from_bytes :: "byte list ⇒ 'a" where
  "from_bytes bs ≡
      field_update (field_desc (typ_info_t TYPE('a))) bs undefined"


type_synonym ('a, 'b) flr = "(('a, 'b) typ_desc × nat) option"

primrec
  field_lookup :: "('a, 'b) typ_desc ⇒ qualified_field_name ⇒ nat ⇒ ('a, 'b) flr" and
  field_lookup_struct :: "('a, 'b) typ_struct ⇒ qualified_field_name ⇒ nat ⇒
    ('a, 'b) flr" and
  field_lookup_list :: "('a, 'b) typ_tuple list ⇒ qualified_field_name ⇒ nat ⇒
    ('a, 'b) flr" and
  field_lookup_tuple :: "('a, 'b) typ_tuple ⇒ qualified_field_name ⇒ nat ⇒ ('a, 'b) flr"
where
  fl0: "field_lookup (TypDesc algn st nm) f m =
         (if f=[] then Some (TypDesc algn st nm,m) else field_lookup_struct st f m)"

| fl1: "field_lookup_struct (TypScalar n algn d) f m = None"
| fl2: "field_lookup_struct (TypAggregate xs) f m = field_lookup_list xs f m"

| fl3: "field_lookup_list [] f m = None"
| fl4: "field_lookup_list (x#xs) f m = (
         case field_lookup_tuple x f m of
           None ⇒ field_lookup_list xs f (m + size_td (dt_fst x)) |
           Some y ⇒ Some y)"

| fl5: "field_lookup_tuple (DTuple t nm d) f m =
         (if nm=hd f ∧ f ≠ [] then field_lookup t (tl f) m else None)"


lemma field_lookup_wf_desc_pres:
  fixes t::"('a, 'b) typ_desc"
  and st::"('a, 'b) typ_struct"
  and ts::"('a, 'b) typ_tuple list"
  and x::"('a, 'b) typ_tuple"
shows
"wf_desc t ⟹ field_lookup t f n = Some (s, m) ⟹ wf_desc s"
"wf_desc_struct st ⟹ field_lookup_struct st f n = Some (s, m) ⟹ wf_desc s"
"wf_desc_list ts ⟹ field_lookup_list ts f n = Some (s, m) ⟹ wf_desc s"
"wf_desc_tuple x ⟹ field_lookup_tuple x f n = Some (s, m) ⟹ wf_desc s"
by (induct t and st and ts and x arbitrary: n s m f and n s m f  and n s m f and n s m f)
   (auto split: if_split_asm option.splits)

definition map_td_flr :: "(nat ⇒ nat ⇒ 'a ⇒ 'b) ⇒ ('c ⇒ 'd) ⇒
  (('a,'c) typ_desc × nat) option ⇒ ('b, 'd) flr"
where
  "map_td_flr f g ≡ case_option None (λ(s,n). Some (map_td f g s,n))"


definition
  import_flr :: "(nat ⇒ nat ⇒ 'b ⇒ 'a) ⇒ ('d ⇒ 'c) ⇒  ('a, 'c) flr ⇒ (('b,'d) typ_desc × nat) option ⇒ bool"
where
  "import_flr f g s k ≡ case_option (k=None)
      (λ(s,m). case_option False (λ(t,n). n=m ∧ map_td f g t=s) k )
      s"

definition
  field_offset_untyped :: "('a, 'b) typ_desc ⇒ qualified_field_name ⇒ nat"
where
  "field_offset_untyped t n ≡ snd (the (field_lookup t n 0))"

definition (in c_type)
  field_offset :: "'a itself ⇒ qualified_field_name ⇒ nat"
where
  "field_offset t n ≡ field_offset_untyped (typ_uinfo_t TYPE('a)) n"

definition (in c_type)
  field_ti :: "'a itself ⇒ qualified_field_name ⇀ 'a xtyp_info"
where
  "field_ti t n ≡ case_option None (Some ∘ fst)
      (field_lookup (typ_info_t TYPE('a)) n 0)"


definition (in c_type)
  field_size :: "'a itself ⇒ qualified_field_name ⇒ nat"
where
  "field_size t n ≡ size_td (the (field_ti t n))"

definition (in c_type)
  field_lvalue :: "'a ptr ⇒ qualified_field_name ⇒ addr"
    (‹(‹open_block notation=‹mixfix field_lvalue››&'(_→_'))›)
where
  "&(p→f) ≡ ptr_val (p::'a ptr) + of_nat (field_offset TYPE('a) f)"

definition (in c_type)
  size_of :: "'a itself ⇒ nat" where
  "size_of t ≡ size_td (typ_info_t TYPE('a))"

lemma (in c_type) size_of_fold: "size_td (typ_info_t TYPE('a)) = size_of TYPE('a)"
  by (simp add: size_of_def)

definition (in c_type)
  norm_bytes :: "'a itself ⇒ normalisor" where
  "norm_bytes t ≡ norm_tu (export_uinfo (typ_info_t t))"

definition (in c_type) to_bytes_p :: "'a ⇒ byte list" where
  "to_bytes_p v ≡ to_bytes v (replicate (size_of TYPE('a)) 0)"

definition (in c_type) zero ::"'a" where
  "zero ≡ from_bytes (replicate (size_of TYPE('a)) 0)"

hide_const (open) zero ― ‹mandatory qualifier: \<^const>‹c_type_class.zero››

syntax
  "_zero" :: "type ⇒ logic"  (‹(‹indent=1 notation=‹mixfix ZERO››ZERO/(1'(_')))›)
syntax_consts
  "_zero" == c_type_class.zero
translations
  "ZERO('a)" => "CONST c_type_class.zero :: ('a)"

typed_print_translation ‹
let
  val show_zero_types = Attrib.setup_config_bool @{binding show_zero_types} (K true);

  fun zero_tr' ctxt typ _ =
    if Config.get ctxt show_zero_types then
      Syntax.const @{syntax_const "_zero"} $ Syntax_Phases.term_of_typ ctxt typ
    else
      raise Match;

in [(@{const_syntax c_type_class.zero}, zero_tr' )]
end›

primrec
  align_td_wo_align :: "('a, 'b) typ_desc ⇒ nat" and
  align_td_wo_align_struct :: "('a, 'b) typ_struct ⇒ nat" and
  align_td_wo_align_list :: "('a, 'b) typ_tuple list ⇒ nat" and
  align_td_wo_align_tuple :: "('a, 'b) typ_tuple ⇒ nat"
where
  al0:  "align_td_wo_align (TypDesc algn st nm) = align_td_wo_align_struct st"

| al1:  "align_td_wo_align_struct (TypScalar n algn d) = algn"
| al2:  "align_td_wo_align_struct (TypAggregate xs) = align_td_wo_align_list xs"

| al3:  "align_td_wo_align_list [] = 0"
| al4:  "align_td_wo_align_list (x#xs) = max (align_td_wo_align_tuple x) (align_td_wo_align_list xs)"

| al5:  "align_td_wo_align_tuple (DTuple t n d) = align_td_wo_align t"

primrec
  align_td :: "('a, 'b) typ_desc ⇒ nat" and
  align_td_struct :: "('a, 'b) typ_struct ⇒ nat" and
  align_td_list :: "('a, 'b) typ_tuple list ⇒ nat" and
  align_td_tuple :: "('a, 'b) typ_tuple ⇒ nat"
where
  al0:  "align_td (TypDesc algn st nm) = algn"

| al1:  "align_td_struct (TypScalar n algn d) = algn"
| al2:  "align_td_struct (TypAggregate xs) = align_td_list xs"

| al3:  "align_td_list [] = 0"
| al4:  "align_td_list (x#xs) = max (align_td_tuple x) (align_td_list xs)"

| al5:  "align_td_tuple (DTuple t n d) = align_td t"


primrec
  wf_align :: "('a, 'b) typ_desc ⇒ bool" and
  wf_align_struct :: "('a, 'b) typ_struct ⇒ bool" and
  wf_align_list :: "('a, 'b) typ_tuple list ⇒ bool" and
  wf_align_tuple :: "('a, 'b) typ_tuple ⇒ bool"
where
  wfal0: "wf_align (TypDesc algn ts n) = (align_td_wo_align_struct ts ≤ algn ∧
                                          align_td_struct ts ≤ algn ∧
                                          wf_align_struct ts)"

| wfal1: "wf_align_struct (TypScalar n algn d) = True"
| wfal2: "wf_align_struct (TypAggregate ts) = (wf_align_list ts)"

| wfal3: "wf_align_list [] = True"
| wfal4: "wf_align_list (x#xs) =
           (wf_align_tuple x ∧ wf_align_list xs)"

| wfal5: "wf_align_tuple (DTuple x n d) = wf_align x"



definition (in c_type) align_of :: "'a itself ⇒ nat" where
  "align_of t ≡ 2^(align_td (typ_info_t TYPE('a)))"

lemma align_td_wo_align_le_align_td:
  fixes t::"('a,'b) typ_info" and
   st::"('a,'b) typ_info_struct" and
   fs::"('a,'b) typ_info_tuple list" and
   f::"('a,'b) typ_info_tuple"
 shows
 "wf_align t ⟹ align_td_wo_align t ≤ align_td t"
 "wf_align_struct st ⟹ align_td_wo_align_struct st ≤ align_td_struct st"
 "wf_align_list fs ⟹ align_td_wo_align_list fs ≤ align_td_list fs"
 "wf_align_tuple f ⟹ align_td_wo_align_tuple f ≤ align_td_tuple f"
     apply (induct t and st and fs and f rule: typ_desc_typ_struct_inducts)
       apply auto
  done

lemma (in c_type) align_td_wo_align_le_align_of:
  assumes wf: "wf_align (typ_info_t TYPE('a))"
  shows "2^(align_td_wo_align (typ_info_t TYPE('a))) ≤ align_of (TYPE('a))"
  using align_td_wo_align_le_align_td (1) [OF wf]
  by (simp add: align_of_def)

definition (in c_type)
  ptr_add :: "'a ptr ⇒ int ⇒ 'a ptr" (infixl ‹+⇩p› 65)
where
  "ptr_add (a :: 'a ptr) w ≡
     Ptr (ptr_val a + of_int w * of_nat (size_of (TYPE('a))))"

lemma (in c_type) ptr_add_def':
  "ptr_add (Ptr p :: ('a) ptr) n
      = (Ptr (p + of_int n * of_nat (size_of TYPE('a))))"
  by (cases p, auto simp: ptr_add_def scast_id)

definition (in c_type)
  ptr_sub :: "'a ptr ⇒ 'a ptr ⇒ addr_bitsize signed word" (infixl ‹-⇩p› 65)
where
  "ptr_sub (a :: 'a ptr) p ≡
     ucast (ptr_val a - ptr_val p) div of_nat (size_of (TYPE('a)))"

definition (in c_type) ptr_aligned :: "'a ptr ⇒ bool" where
  "ptr_aligned p ≡ align_of TYPE('a) dvd unat (ptr_val (p::'a ptr))"

type_synonym 'a ptr_guard = "'a ptr ⇒ bool"

definition (in c_type) c_null_guard :: "'a ptr_guard" where
  "c_null_guard ≡ λp. 0 ∉ {ptr_val p..+size_of TYPE('a)}"

definition (in c_type) c_guard :: "'a ptr_guard" where
   "c_guard ≡ λp. ptr_aligned p ∧ c_null_guard p"

primrec
  td_set :: "('a, 'b) typ_desc ⇒ nat ⇒ (('a, 'b) typ_desc × nat) set" and
  td_set_struct :: "('a, 'b) typ_struct ⇒ nat ⇒ (('a, 'b) typ_desc × nat) set" and
  td_set_list :: "('a, 'b) typ_tuple list ⇒ nat ⇒ (('a,'b) typ_desc × nat) set" and
  td_set_tuple :: "('a, 'b) typ_tuple ⇒ nat ⇒ (('a, 'b) typ_desc × nat) set"
where
  ts0:  "td_set (TypDesc algn st nm) m = {(TypDesc algn st nm,m)} ∪ td_set_struct st m"

| ts1:  "td_set_struct (TypScalar n algn d) m = {}"
| ts2:  "td_set_struct (TypAggregate xs) m = td_set_list xs m"

| ts3:  "td_set_list [] m = {}"
| ts4:  "td_set_list (x#xs) m = td_set_tuple x m ∪ td_set_list xs (m + size_td (dt_fst x))"

| ts5:  "td_set_tuple (DTuple t nm d) m = td_set t m"


instantiation typ_desc :: (type, type) ord
begin

definition
  typ_tag_le_def:  "s ≤ (t::('a, 'b) typ_desc) ≡ (∃n. (s,n) ∈ td_set t 0)"
definition
  typ_tag_lt_def: "s < (t::('a, 'b) typ_desc) ≡ s ≤ t ∧ s ≠ t"
instance ..

end


definition
  fd_cons_double_update :: "('a, 'x) field_desc_scheme ⇒ bool"
where
  "fd_cons_double_update d ≡
      (∀v bs bs'. length bs = length bs' ⟶ field_update d bs (field_update d bs' v) = field_update d bs v)"

definition
  fd_cons_update_access :: "('a, 'x) field_desc_scheme ⇒ nat ⇒ bool"
where
  "fd_cons_update_access d n ≡
      (∀v bs. length bs = n ⟶ field_update d (field_access d v bs) v = v)"

definition
  norm_desc  :: "('a, 'x) field_desc_scheme ⇒ nat ⇒ (byte list ⇒ byte list)"
where
  "norm_desc d n ≡ λbs. field_access d (field_update d bs undefined) (replicate n 0)"

definition
  fd_cons_length :: "('a, 'x) field_desc_scheme ⇒ nat ⇒ bool"
where
  "fd_cons_length d n ≡ ∀v bs. length bs = n ⟶ length (field_access d v bs) = n"

definition
  fd_cons_access_update :: "('a, 'x) field_desc_scheme ⇒ nat ⇒ bool"
where
  "fd_cons_access_update d n ≡ ∀bs bs' v v'. length bs = n ⟶
      length bs' = n ⟶
      field_access d (field_update d bs v) bs' = field_access d (field_update d bs v') bs'"


definition
  fd_cons_update_normalise :: "('a, 'x) field_desc_scheme ⇒ nat ⇒ bool"
where
  "fd_cons_update_normalise d n  ≡
      (∀v bs. length bs=n ⟶ field_update d (norm_desc d n bs) v = field_update d bs v)"


definition
  fd_cons_desc :: "('a,'x) field_desc_scheme ⇒ nat ⇒ bool"
where
  "fd_cons_desc d n ≡ fd_cons_double_update d ∧
      fd_cons_update_access d n ∧
      fd_cons_access_update d n ∧
      fd_cons_length d n"

definition
  fd_cons :: "('a, 'b) typ_info ⇒ bool"
where
  "fd_cons t ≡ fd_cons_desc (field_desc t) (size_td t)"

definition
  fd_cons_struct :: "('a, 'b) typ_info_struct ⇒ bool"
where
  "fd_cons_struct t ≡ fd_cons_desc (field_desc_struct t) (size_td_struct t)"

definition
  fd_cons_list :: "('a, 'b) typ_info_tuple list ⇒ bool"
where
  "fd_cons_list t ≡ fd_cons_desc (field_desc_list t) (size_td_list t)"

definition
  fd_cons_tuple :: "('a,  'b) typ_info_tuple ⇒ bool"
where
  "fd_cons_tuple t ≡ fd_cons_desc (field_desc_tuple t) (size_td_tuple t)"


definition
  fa_fu_ind :: "'a field_desc ⇒ 'a field_desc ⇒ nat ⇒ nat ⇒bool"
where
  "fa_fu_ind d d' n n' ≡ ∀v bs bs'. length bs = n ⟶ length bs' = n' ⟶
      field_access d (field_update d' bs v) bs' = field_access d v bs'"

definition
  wf_fdp :: "(('a, 'b) typ_info × qualified_field_name) set ⇒ bool"
where
  "wf_fdp t ≡ ∀x m. (x,m) ∈ t ⟶ (fd_cons x ∧ (∀y n. (y,n) ∈ t ∧ ¬ m ≤ n ∧ ¬ n ≤ m
      ⟶ fu_commutes (field_update (field_desc x)) (field_update (field_desc y)) ∧
          fa_fu_ind (field_desc x) (field_desc y) (size_td y) (size_td x)))"

lemma wf_fdp_list:
  "wf_fdp (xs ∪ ys) ⟹ wf_fdp xs ∧ wf_fdp ys"
  by (auto simp: wf_fdp_def)


primrec
  wf_fd :: "('a, 'b) typ_info ⇒ bool" and
  wf_fd_struct :: "('a, 'b) typ_info_struct ⇒ bool" and
  wf_fd_list :: "('a, 'b) typ_info_tuple list ⇒ bool" and
  wf_fd_tuple :: "('a, 'b) typ_info_tuple ⇒ bool"
where
  wffd0:  "wf_fd (TypDesc algn ts n) = (wf_fd_struct ts)"

| wffd1:  "wf_fd_struct (TypScalar n algn d) = fd_cons_struct (TypScalar n algn d::('a,'b) typ_info_struct)"
| wffd2:  "wf_fd_struct (TypAggregate ts) = wf_fd_list ts"

| wffd3:  "wf_fd_list [] = True"
| wffd4:  "wf_fd_list (x#xs) = (wf_fd_tuple x ∧ wf_fd_list xs ∧
      fu_commutes (update_ti_tuple_t x) (update_ti_list_t xs) ∧
      fa_fu_ind (field_desc_tuple x) (field_desc_list xs) (size_td_list xs) (size_td_tuple x)∧
      fa_fu_ind (field_desc_list xs) (field_desc_tuple x) (size_td_tuple x) (size_td_list xs))"

| wffd5:  "wf_fd_tuple (DTuple x n d) = wf_fd x"


definition
  tf_set :: "('a, 'b) typ_info ⇒ (('a, 'b) typ_info × qualified_field_name) set"
where
  "tf_set td ≡ {(s,f) | s f. ∃n. field_lookup td f 0 = Some (s,n)}"

definition
  tf_set_struct :: "('a, 'b) typ_info_struct ⇒ (('a, 'b) typ_info × qualified_field_name) set"
where
  "tf_set_struct td ≡ {(s,f) | s f. ∃n. field_lookup_struct td f 0 = Some (s,n)}"

definition
  tf_set_list :: "('a, 'b) typ_info_tuple list ⇒ (('a, 'b) typ_info × qualified_field_name) set"
where
  "tf_set_list td ≡ {(s,f) | s f. ∃n. field_lookup_list td f 0 = Some (s,n)}"

definition
  tf_set_tuple :: "('a, 'b) typ_info_tuple ⇒ (('a, 'b) typ_info × qualified_field_name) set"
where
  "tf_set_tuple td ≡ {(s,f) | s f. ∃n. field_lookup_tuple td f 0 = Some (s,n)}"


record 'a leaf_desc =
  lf_fd :: "'a field_desc"
  lf_sz :: nat
  lf_fn :: qualified_field_name


primrec
  lf_set :: "('a, 'b) typ_info ⇒ qualified_field_name ⇒ 'a leaf_desc set" and
  lf_set_struct :: "('a, 'b) typ_info_struct ⇒ qualified_field_name ⇒ 'a leaf_desc set" and
  lf_set_list :: "('a, 'b) typ_info_tuple list ⇒ qualified_field_name ⇒ 'a leaf_desc set" and
  lf_set_tuple :: "('a, 'b) typ_info_tuple ⇒ qualified_field_name ⇒ 'a leaf_desc set"
where
  fds0:  "lf_set (TypDesc algn st nm) fn = lf_set_struct st fn"

| fds1:  "lf_set_struct (TypScalar n algn d) fn = {(⦇ lf_fd = d, lf_sz = n, lf_fn = fn ⦈)}"
| fds2:  "lf_set_struct (TypAggregate xs) fn = lf_set_list xs fn"

| fds3:  "lf_set_list [] fn = {}"
| fds4:  "lf_set_list (x#xs) fn = lf_set_tuple x fn ∪ lf_set_list xs fn"

| fds5:  "lf_set_tuple (DTuple t n d) fn = lf_set t (fn@[n])"


definition
  wf_lf :: "'a leaf_desc set ⇒ bool"
where
  "wf_lf D ≡ ∀x. x ∈ D ⟶ (fd_cons_desc (lf_fd x) (lf_sz x) ∧ (∀y. y ∈ D ⟶ lf_fn y ≠ lf_fn x
      ⟶ fu_commutes (field_update (lf_fd x)) (field_update (lf_fd y)) ∧
          fa_fu_ind (lf_fd x) (lf_fd y) (lf_sz y) (lf_sz x)))"

definition
  ti_ind :: "'a leaf_desc set ⇒ 'a leaf_desc set ⇒ bool"
where
  "ti_ind X Y ≡ ∀x y. x ∈ X ∧ y ∈ Y ⟶ (
      fu_commutes (field_update (lf_fd x)) (field_update (lf_fd y)) ∧
          fa_fu_ind (lf_fd x) (lf_fd y) (lf_sz y) (lf_sz x) ∧
          fa_fu_ind (lf_fd y) (lf_fd x) (lf_sz x) (lf_sz y))"


definition
  t2d :: "(('a, 'b) typ_info × qualified_field_name) ⇒ 'a leaf_desc"
where
  "t2d x ≡ ⦇ lf_fd = field_desc (fst x), lf_sz = size_td (fst x), lf_fn = snd x⦈"


definition
  fd_consistent :: "('a, 'b) typ_info ⇒ bool"
where
  "fd_consistent t ≡ ∀f s n. field_lookup t f 0 = Some (s,n)
      ⟶ fd_cons s"

class wf_type = c_type +
  assumes wf_desc [simp]: "wf_desc (typ_info_t TYPE('a))"
  assumes wf_size_desc [simp]: "wf_size_desc (typ_info_t TYPE('a))"
  assumes wf_lf [simp]: "wf_lf (lf_set (typ_info_t TYPE('a)) [])"

definition
  super_update_bs :: "byte list ⇒ byte list ⇒ nat ⇒ byte list"
where
  "super_update_bs v bs n ≡ take n bs @ v @
      drop (n + length v) bs"

definition
  disj_fn :: "qualified_field_name ⇒ qualified_field_name ⇒ bool"
where
  "disj_fn s t ≡ ¬ s ≤ t ∧ ¬ t ≤ s"

definition
  fs_path :: "qualified_field_name list ⇒ qualified_field_name set"
where
  "fs_path xs ≡ {x. ∃k. k ∈ set xs ∧ x ≤ k} ∪ {x. ∃k. k ∈ set xs ∧ k ≤ x}"

definition
  field_names :: "('a, 'b) typ_desc ⇒ qualified_field_name set"
where
  "field_names t ≡ {f. field_lookup t f 0 ≠ None}"

definition
  align_field :: "('a, 'b) typ_desc ⇒ bool"
where
  "align_field ti ≡ ∀f s n. field_lookup ti f 0 = Some (s,n) ⟶
      2^(align_td s) dvd n"

class mem_type_sans_size = wf_type +
  assumes upd:
     "length bs = size_of TYPE('a) ⟶
      update_ti_t (typ_info_t TYPE('a)) bs v
          = update_ti_t (typ_info_t TYPE('a)) bs w"
  assumes align_size_of: "align_of (TYPE('a)) dvd size_of TYPE('a)"
  assumes align_field: "align_field (typ_info_t TYPE('a))"
  assumes wf_align: "wf_align (typ_info_t TYPE('a))"


class mem_type = mem_type_sans_size +
  assumes max_size: "size_of (TYPE('a)) < addr_card"


primrec
  aggregate :: "('a, 'b) typ_desc ⇒ bool" and
  aggregate_struct :: "('a, 'b) typ_struct ⇒ bool"
where
  "aggregate (TypDesc algn st tn) = aggregate_struct st"

| "aggregate_struct (TypScalar n algn d) = False"
| "aggregate_struct (TypAggregate ts) = True"

class simple_mem_type = mem_type +
  assumes simple_tag: "¬ aggregate (typ_info_t TYPE('a))"

definition
  field_of :: "addr ⇒ ('a, 'b) typ_desc ⇒ ('a, 'b) typ_desc ⇒ bool"
where
  "field_of q s t ≡ (s,unat q) ∈ td_set t 0"

definition (in c_type)
  field_of_t :: "'a ptr ⇒ 'b::c_type ptr ⇒ bool"
where
  "field_of_t p q ≡ field_of (ptr_val p - ptr_val q) (typ_uinfo_t TYPE('a))
      (typ_uinfo_t TYPE('b))"

definition (in c_type)
  h_val :: "heap_mem ⇒ 'a ptr ⇒ 'a"
where
  "h_val h ≡ λp. from_bytes (heap_list h (size_of TYPE ('a))
      (ptr_val (p::'a ptr)))"

primrec
  heap_update_list :: "addr ⇒ byte list ⇒ heap_mem ⇒ heap_mem"
where
  heap_update_list_base: "heap_update_list p [] h = h"
| heap_update_list_rec:
  "heap_update_list p (x#xs) h = heap_update_list (p + 1) xs (h(p:= x))"

type_synonym 'a typ_heap_g = "'a ptr ⇒ 'a"

(* fixme: now redundant with h_val *)
definition (in c_type)
  lift :: "heap_mem ⇒ 'a typ_heap_g"
where
  "lift h ≡ h_val h"

definition (in c_type)
  heap_update :: "'a ptr ⇒ 'a ⇒ heap_mem ⇒ heap_mem"
where
  "heap_update p v h ≡ heap_update_list (ptr_val p) (to_bytes v (heap_list h (size_of TYPE('a)) (ptr_val p))) h"

definition (in c_type)
  heap_update_padding :: "'a ptr ⇒ 'a ⇒ byte list ⇒ heap_mem ⇒ heap_mem" where
"heap_update_padding p v bs h =
  heap_update_list (ptr_val p) (to_bytes v bs) h"

lemma (in c_type) heap_update_heap_update_padding_conv:
  "heap_update p v h = heap_update_padding p v (heap_list h (size_of TYPE('a)) (ptr_val p)) h"
  by (simp add: heap_update_def heap_update_padding_def)

definition (in c_type) heap_upd where
  "heap_upd p f s = heap_update p (f (h_val s p)) s"

definition heap_upd_list :: "nat ⇒ addr ⇒ (byte list ⇒ byte list) ⇒ heap_mem ⇒ heap_mem" where
  "heap_upd_list n p f h = heap_update_list p (f (heap_list h n p)) h"

fun
  fold_td' :: "(typ_name ⇒ ('a × field_name) list ⇒ 'a) × ('a, 'b) typ_desc ⇒ 'a"
where
fot0: "fold_td' (f,TypDesc algn st nm) = (case st of
           TypScalar n algn d ⇒ d |
           TypAggregate ts ⇒ f nm (map (λx. case x of DTuple t n d ⇒ (fold_td' (f,t),n)) ts))"


definition
  fold_td :: "(typ_name ⇒ ('a × field_name) list ⇒ 'a) ⇒ ('a, 'b) typ_desc ⇒ 'a"
where
  "fold_td ≡ λf t. fold_td' (f,t)"

declare fold_td_def [simp]

definition
  fold_td_struct :: "typ_name ⇒ (typ_name ⇒ ('a × field_name) list ⇒ 'a) ⇒ ('a, 'b) typ_struct ⇒ 'a"
where
  "fold_td_struct tn f st ≡ (case st of
           TypScalar n algn d ⇒ d |
           TypAggregate ts ⇒ f tn (map (λx. case x of DTuple t n d ⇒ (fold_td' (f,t),n)) ts))"

declare fold_td_struct_def [simp]

definition
  fold_td_list :: "typ_name ⇒ (typ_name ⇒ ('a × field_name) list ⇒ 'a) ⇒ ('a, 'b) typ_tuple list ⇒ 'a"
where
  "fold_td_list tn f ts ≡ f tn (map (λx. case x of DTuple t n d ⇒ (fold_td' (f,t),n)) ts)"

declare fold_td_list_def [simp]

definition
  fold_td_tuple :: "(typ_name ⇒ ('a × field_name) list ⇒ 'a) ⇒ ('a, 'b) typ_tuple ⇒ 'a"
where
  "fold_td_tuple f x ≡ (case x of DTuple t n d ⇒ fold_td' (f,t))"

declare fold_td_tuple_def [simp]

fun
  map_td' :: "((nat ⇒ nat ⇒ 'a ⇒ 'b) × ('c ⇒ 'd)) × ('a, 'c) typ_desc ⇒ ('b, 'd) typ_desc"
where
  "map_td' ((f,g),TypDesc algn st nm) = (TypDesc algn (case st of
           TypScalar n algn d ⇒ TypScalar n algn (f n algn d) |
           TypAggregate ts ⇒ TypAggregate (map (λx. case x of DTuple t n d ⇒ DTuple (map_td' ((f,g),t)) n (g d)) ts)) nm)"

definition
  tnSum :: "typ_name ⇒ (nat × field_name) list ⇒ nat"
where
  "tnSum ≡ λtn ts. foldr ((+) o fst) ts 0"

definition
  tnMax :: "typ_name ⇒ (nat × field_name) list ⇒ nat"
where
  "tnMax ≡ λtn ts. foldr (λx y. max (fst x) y) ts 0"

definition
  wfd :: "typ_name ⇒ (bool × field_name) list ⇒ bool"
where
  "wfd ≡ λtn ts. distinct (map snd ts) ∧ foldr (∧) (map fst ts) True"

definition
  wfsd :: "typ_name ⇒ (bool × field_name) list ⇒ bool"
where
  "wfsd ≡ λtn ts. ts ≠ [] ∧ foldr (∧) (map fst ts) True"


definition "component_desc_tuple t ≡ case t of (DTuple t n d) ⇒ d"

lemma component_desc_tuple_simp [simp]: "component_desc_tuple (DTuple t n d) = d"
  by (simp add: component_desc_tuple_def)

primrec split_list:: "nat list ⇒ 'a list ⇒ 'a list list" where
  "split_list [] bs = [bs]"
| "split_list (n#ns) bs = take n bs # split_list ns (drop n bs)"


lemma concat_split [simp]: "concat (split_list ns bs) = bs"
  by (induct ns arbitrary: bs) auto

primrec split_map':: "('b ⇒ nat) ⇒ ('b ⇒ 'a list ⇒ 'c) ⇒ 'b list ⇒ 'a list ⇒ 'c list" where
  "split_map' n f [] bs = []"
| "split_map' n f (x#xs) bs = f x (take (n x) bs) # split_map' n f xs (drop (n x) bs)"


lemma length_split_map' [simp]: "length (split_map' n f xs bs) = length xs"
  by (induct xs arbitrary: bs) auto

lemma "split_map' n f xs bs = map (λ(f',bs'). f' bs') (zip (map f xs) (split_list (map n xs) bs))"
  by (induct xs arbitrary: bs) auto

primrec split_map:: "('b ⇒ 'a list ⇒ 'c list) ⇒ 'b list ⇒ 'a list ⇒ 'c list list" where
  "split_map f [] bs = []"
| "split_map f (x#xs) bs = f x bs # split_map f xs (drop (length (f x bs)) bs)"

lemma length_split_map [simp]: "length (split_map f xs bs) = length xs"
  by (induct xs arbitrary: bs) auto

primrec split_fold:: "('b ⇒ 'a list ⇒ 'd  ⇒ ('d × 'a list)) ⇒ 'b list ⇒ 'a list ⇒ 'd ⇒ ('d × 'a list)"  where
  "split_fold f [] bs s = (s, bs)"
| "split_fold f (x#xs) bs s = (let (s', bs') = f x bs s in split_fold f xs bs' s')"


definition apply_field_update::"'a field_desc ⇒ byte list ⇒ 'a ⇒ ('a × byte list)" where
  "apply_field_update d bs s ≡ (field_update d bs s, drop (field_sz d) bs)"

definition apply_field_updates :: "'a field_desc list ⇒ byte list ⇒ 'a ⇒ ('a × byte list)" where
  "apply_field_updates ≡ split_fold apply_field_update"

lemma apply_field_updates_Nil [simp]: "apply_field_updates [] bs s = (s, bs)"
  by (simp add: apply_field_updates_def)

lemma apply_field_updates_Cons [simp]: "apply_field_updates (d#ds) bs s =
  apply_field_updates ds (drop (field_sz d) bs) (field_update d bs s)"
  by (simp add: apply_field_updates_def apply_field_update_def)


definition "component_access_tuple v t bs ≡ case t of (DTuple t n d) ⇒ field_access d v bs"

lemma component_access_tuple_simp [simp]: "component_access_tuple v (DTuple t n d) = field_access d v"
  by (auto simp add: component_access_tuple_def)


definition "component_access_struct st v bs =
  (case st of TypScalar _ _ d ⇒ field_access d v bs
   | TypAggregate fs ⇒ concat (split_map (component_access_tuple v) fs bs))"

lemma component_access_struct_scalar [simp]:
  "component_access_struct (TypScalar sz align d) = field_access d"
  apply (rule ext)
  apply (rule ext)
  apply (simp add: component_access_struct_def)
  done

lemma component_access_struct_aggregate [simp]:
  "component_access_struct (TypAggregate fs) v bs = concat (split_map (component_access_tuple v) fs bs)"
  by (simp add: component_access_struct_def)

lemma component_access_struct_aggregate_nil [simp]:
"component_access_struct (TypAggregate []) = (λv bs. [])"
  apply (rule ext)
  apply (rule ext)
  apply simp
  done


definition "component_update_tuple t bs ≡ case t of (DTuple t n d) ⇒ field_update d bs"

lemma component_update_tuple_simp [simp]: "component_update_tuple (DTuple t n d) = field_update d"
  by (auto simp add: component_update_tuple_def)


definition "component_update_struct st bs v =
  (case st of TypScalar _ _ d ⇒ field_update d bs v
   | TypAggregate fs ⇒ fst (apply_field_updates (map dt_trd fs) bs v))"

lemma component_update_struct_scalar [simp]:
  "component_update_struct (TypScalar sz align d) = field_update d"
  apply (rule ext)
  apply (rule ext)
  apply (simp add: component_update_struct_def)
  done

lemma component_update_struct_aggregate [simp]:
  "component_update_struct (TypAggregate fs) bs v = fst (apply_field_updates (map dt_trd fs) bs v)"
  by (simp add: component_update_struct_def)

lemma component_update_struct_aggregate_nil [simp]:
"component_update_struct (TypAggregate []) = (λbs. id)"
  apply (rule ext)
  apply (rule ext)
  apply simp
  done


definition "component_sz_struct st =
  (case st of TypScalar _ _ d ⇒ field_sz d
   | TypAggregate fs ⇒ foldl (+) 0 (map (field_sz o dt_trd) fs))"

lemma component_sz_struct_scalar [simp]:
  "component_sz_struct (TypScalar sz align d) = field_sz d"
  by (simp add: component_sz_struct_def)


lemma component_sz_struct_aggregate [simp]:
  "component_sz_struct (TypAggregate fs) = foldl (+) 0 (map (field_sz o dt_trd) fs)"
  by (simp add: component_sz_struct_def)



definition "component_desc_struct st =
  ⦇field_access = component_access_struct st,
   field_update = component_update_struct st,
   field_sz = component_sz_struct st⦈"

lemma component_desc_struct_simps [simp]:
  "field_access (component_desc_struct st) = component_access_struct st"
  "field_update (component_desc_struct st) = component_update_struct st"
  "field_sz (component_desc_struct st) = component_sz_struct st"
  "component_desc_struct (TypScalar sz align d) = d"
  by (auto simp add: component_desc_struct_def)


definition "component_desc t ≡ case t of TypDesc algn st n ⇒ component_desc_struct st"

lemma component_desc_simps [simp]: "component_desc (TypDesc algn st n) = component_desc_struct st"
  by (simp add: component_desc_def)


definition (in c_type) xto_bytes :: "'a ⇒ byte list ⇒ byte list" where
  "xto_bytes ≡ field_access (component_desc (typ_info_t TYPE('a)))"

definition (in c_type) xfrom_bytes  :: "byte list ⇒ 'a" where
  "xfrom_bytes bs ≡ field_update (component_desc (typ_info_t TYPE('a))) bs undefined"

primrec
  toplevel_field_descs :: "'a xtyp_info ⇒ 'a field_desc list" and
  toplevel_field_descs_struct :: "'a xtyp_info_struct ⇒ 'a field_desc list" and
  toplevel_field_descs_list :: "'a xtyp_info_tuple list ⇒ 'a field_desc list" and
  toplevel_field_descs_tuple :: "'a xtyp_info_tuple ⇒ 'a field_desc list"
where
  tfd0: "toplevel_field_descs (TypDesc algn st nm) = toplevel_field_descs_struct st"

| tfd1: "toplevel_field_descs_struct (TypScalar n algn d) = [d]"
| tfd2: "toplevel_field_descs_struct (TypAggregate xs) = toplevel_field_descs_list xs"

| tfd3: "toplevel_field_descs_list [] = []"
| tfd4: "toplevel_field_descs_list (x#xs) = toplevel_field_descs_tuple x @ toplevel_field_descs_list xs"

| tfd5: "toplevel_field_descs_tuple (DTuple t nm d) = [d]"

locale padding_base =
  fixes acc::"'a ⇒ byte list ⇒ byte list"
  fixes upd:: "byte list ⇒ 'a ⇒ 'a"
  fixes sz::nat
begin
  definition eq_padding::"byte list ⇒ byte list ⇒ bool" where
    "eq_padding bs bs' ≡ length bs = sz ∧ length bs' = sz ∧ (∀v. acc v bs = acc v bs')"
  definition eq_upto_padding::"byte list ⇒ byte list ⇒ bool" where
    "eq_upto_padding bs bs' ≡ length bs = sz ∧ length bs' = sz ∧ (∀v. upd bs v = upd bs' v)"


definition is_padding_byte::"nat ⇒ bool" where
    "is_padding_byte i ≡ i < sz ∧ (∀v bs. length bs = sz ⟶
          (acc v bs ! i  = bs ! i) ∧
          (∀b. upd bs v = upd (bs[i:=b]) v))"


definition is_value_byte::"nat ⇒ bool" where
    "is_value_byte i ≡ i < sz ∧ (∀v bs. length bs = sz ⟶
       (∀bs'. length bs' = sz ⟶ (acc (upd bs v) bs' ! i) = bs ! i) ∧
       (∀b. acc v bs = acc v (bs[i:=b])))"

lemma is_padding_byteI:
  assumes "i < sz"
  assumes "⋀v bs. i < sz ⟹ length bs = sz ⟹ acc v bs ! i = bs ! i"
  assumes "⋀v bs b. i < sz ⟹ length bs = sz ⟹ upd bs v = upd (bs[i:=b]) v"
  shows "is_padding_byte i"
  using assms
  by  (simp add: is_padding_byte_def)

lemma is_value_byteI:
  assumes "i < sz"
  assumes "⋀v bs bs'. i < sz ⟹ length bs = sz ⟹ length bs' = sz ⟹
              (acc (upd bs v) bs' ! i) = bs ! i"
  assumes "⋀v bs b. i < sz ⟹ length bs = sz ⟹ acc v bs = acc v (bs[i:=b])"
  shows "is_value_byte i"
  using assms
  by  (simp add: is_value_byte_def)

lemma is_padding_byte_acc_id: "
    is_padding_byte i ⟹ length bs = sz