Theory Storage

section‹Storage›

theory Storage
imports Valuetypes "Finite-Map-Extras.Finite_Map_Extras"

begin

subsection ‹Hashing›

definition hash :: "location ⇒ String.literal ⇒ location"
  where "hash loc ix = ix + (STR ''.'' + loc)"

declare hash_def [solidity_symbex]

text ‹Hash function which uses - for contract version/instance number›
definition hash_version :: "location ⇒ String.literal ⇒ location"
  where "hash_version loc ix = ix + (STR ''-'' + loc)"

lemma explode_dot[simp]: "literal.explode STR ''.'' = [CHR ''.'']" 
  by (simp add: Literal.rep_eq zero_literal.rep_eq)

lemma example: "hash (STR ''1.0'') (STR ''2'') = hash (STR ''0'') (STR ''2.1'')" by eval

lemma hash_explode:
  "String.explode (hash l i) = String.explode i @ (String.explode (STR ''.'') @ String.explode l)"
  unfolding hash_def by (simp add: plus_literal.rep_eq)

lemma hash_dot:
  "String.explode (hash l i) ! length (String.explode i) = CHR ''.''"
  unfolding hash_def by (simp add: Literal.rep_eq plus_literal.rep_eq)

lemma hash_injective:
  assumes "hash l i = hash l' i'"
    and "CHR ''.'' ∉ set (String.explode i)"
    and "CHR ''.'' ∉ set (String.explode i')"
  shows "l = l' ∧ i = i'"
proof (rule ccontr)
  assume "¬ (l = l' ∧ i = i')" 
  then consider (1) "i≠i'" | (2) "i=i' ∧ l≠l'" by auto
  then have "String.explode (hash l i) ≠ String.explode (hash l' i')"
  proof cases
    case 1
    then have neq: "(String.explode i) ≠ (String.explode i')" by (metis literal.explode_inverse)

    consider (1) "length (String.explode i) = length (String.explode i')" | (2) "length (String.explode i) < length (String.explode i')" | (3) "length (String.explode i) > length (String.explode i')" by linarith
    then show ?thesis
    proof (cases)
      case 1
      then obtain j where "String.explode i ! j ≠ String.explode i' ! j" using neq nth_equalityI by auto
      then show ?thesis using 1 plus_literal.rep_eq unfolding hash_def by force
    next
      case 2
      then have "String.explode i' ! length (String.explode i) ≠ CHR ''.''" using assms(3) by (metis nth_mem)
      then have "String.explode (hash l' i') ! length (String.explode i) ≠ CHR ''.''" using 2 hash_explode[of l' i'] by (simp add: nth_append)
      moreover have "String.explode (hash l i) ! length (String.explode i) = CHR ''.''" using hash_dot by simp
      ultimately show ?thesis by auto
    next
      case 3
      then have "String.explode i ! length (String.explode i') ≠ CHR ''.''" using assms(2) by (metis nth_mem)
      then have "String.explode (hash l i) ! length (String.explode i') ≠ CHR ''.''" using 3 hash_explode[of l i] by (simp add: nth_append)
      moreover have "String.explode (hash l' i') ! length (String.explode i') = CHR ''.''" using hash_dot by simp
      ultimately show ?thesis by auto
    qed
  next
    case 2
    then show ?thesis using hash_explode literal.explode_inject by force
  qed
  then show False using assms(1) by simp
qed

subsection ‹General store›

record 'v store =
  Mapping :: "(location,'v) fmap"
  Toploc :: nat 

definition accessStore :: "location ⇒ ('a, 'v) store_scheme ⇒ 'a option"
where "accessStore loc st = fmlookup (Mapping st) loc"

declare accessStore_def[solidity_symbex]

definition emptyStore :: "'v store"
  where "emptyStore = ⦇ Mapping=fmempty, Toploc=0 ⦈"

declare emptyStore_def [solidity_symbex]

definition allocate :: "('a, 'v) store_scheme ⇒ location * ('a, 'v) store_scheme"
where "allocate s = (let ntop = Suc(Toploc s) in (ShowL⇩n⇩a⇩t ntop, s ⦇Toploc := ntop⦈))"


lemma allocateMapping:
  assumes "∃t. (t, s') = allocate s"
  shows "Mapping s = Mapping s'" using assms unfolding allocate_def by auto

lemma accessAllocate:
  assumes "∃t. (t, s') = allocate s"
  shows "∀l. accessStore l s' = accessStore l s" 
  using assms allocateMapping unfolding accessStore_def by force

lemma allocateSameAccess:
  shows "∀loc. accessStore loc m = accessStore loc (snd (allocate m))" 
  unfolding allocate_def accessStore_def by simp


definition updateStore :: "location ⇒ 'v ⇒ ('v, 'a) store_scheme ⇒ ('v, 'a) store_scheme"
where "updateStore loc val s = s ⦇ Mapping := fmupd loc val (Mapping s)⦈"

declare updateStore_def [solidity_symbex]

lemma accessStore_updateStore[simp]: "accessStore l (updateStore l v st) = Some v" unfolding updateStore_def accessStore_def by auto

lemma accessStore_non_changed:
  assumes "updateStore l v st = st'"
  shows "∀l'. l'≠l ⟶ accessStore l' st = accessStore l' st'" 
  using assms unfolding updateStore_def accessStore_def by auto


definition push :: "'v ⇒ ('v, 'a) store_scheme ⇒ ('v, 'a) store_scheme"
  where "push val sto = (let s = updateStore (ShowL⇩n⇩a⇩t (Toploc sto)) val sto in snd (allocate s))"

declare push_def [solidity_symbex]

subsection ‹stack›
                                
datatype (discs_sels) stackvalue = KValue valuetype
                    | KCDptr location
                    | KMemptr location
                    | KStoptr location

type_synonym stack = "stackvalue store"

subsection ‹Storage›

subsubsection ‹Definition›

type_synonym storagevalue = valuetype

type_synonym storageT = "(location,storagevalue) fmap"

datatype (discs_sels) stypes
  = STArray nat stypes
  | STMap types stypes
  | STValue types

subsubsection ‹Example›

abbreviation mystorage::storageT
where "mystorage ≡ (fmap_of_list
  [(STR ''0.0.0'', STR ''False''),
   (STR ''1.1.0'', STR ''True'')])"

subsubsection ‹Access storage›

definition accessStorage :: "types ⇒ location ⇒ storageT ⇒ storagevalue"
where
  "accessStorage t loc sto =
    (case sto $$ loc of
      Some v ⇒ v
    | None ⇒ ival t)"

declare accessStorage_def [solidity_symbex]

subsubsection ‹Copy from storage to storage›

primrec copyRec :: "location ⇒ location ⇒ stypes ⇒ storageT ⇒ storageT option"
where
  "copyRec l⇩s l⇩d (STArray x t) sto =
    iter' (λi s'. copyRec (hash l⇩s (ShowL⇩n⇩a⇩t i)) (hash l⇩d (ShowL⇩n⇩a⇩t i)) t s') sto x"
| "copyRec l⇩s l⇩d (STValue t) sto =
    (let e = accessStorage t l⇩s sto in Some (fmupd l⇩d e sto))"
| "copyRec _ _ (STMap _ _) _ = None"
 
definition copy :: "location ⇒ location ⇒ nat ⇒ stypes ⇒ storageT ⇒ storageT option"
where
  "copy l⇩s l⇩d x t sto =
    iter' (λi s'. copyRec (hash l⇩s (ShowL⇩n⇩a⇩t i)) (hash l⇩d (ShowL⇩n⇩a⇩t i)) t s') sto x"

declare copy_def [solidity_symbex]


abbreviation mystorage2::storageT
where "mystorage2 ≡ (fmap_of_list
  [(STR ''0.0.0'', STR ''False''),
   (STR ''1.1.0'', STR ''True''),
   (STR ''0.5'', STR ''False''),
   (STR ''1.5'', STR ''True'')])"

lemma "copy (STR ''1.0'') (STR ''5'') 2 (STValue TBool) mystorage = Some mystorage2"
  by eval

subsection ‹Memory and Calldata›

subsubsection ‹Definition›

datatype memoryvalue =
  MValue valuetype
  | MPointer location

datatype (discs_sels) mtypes =
  MTArray nat mtypes
  | MTValue types

subsection ‹Typed Store›

record ('t, 'v) typedstore = "'v store" +
  Typed_Mapping :: "(location, 't) fmap"

text ‹Use the inherited accessStore for values, add new functions for type management›

definition accessTypeStore :: "location ⇒ ('t, 'v) typedstore ⇒ 't option"
where "accessTypeStore loc st = fmlookup (Typed_Mapping st) loc"

declare accessTypeStore_def [solidity_symbex]

definition updateTypeStore :: "location ⇒ 't ⇒ ('t, 'v) typedstore ⇒ ('t, 'v) typedstore"
where "updateTypeStore loc typ st = st ⦇ Typed_Mapping := fmupd loc typ (Typed_Mapping st) ⦈"

declare updateTypeStore_def [solidity_symbex]

definition updateTypedStore :: "location ⇒ 'v ⇒ 't ⇒ ('t, 'v) typedstore ⇒ ('t, 'v) typedstore"
where "updateTypedStore loc val typ st = updateTypeStore loc typ (updateStore loc val st)"

definition emptyTypedStore :: "('t, 'v) typedstore"
  where "emptyTypedStore = ⦇ Mapping=fmempty, Toploc=0, Typed_Mapping=fmempty ⦈"

declare emptyTypedStore_def [solidity_symbex]

definition pushTyped :: "'v ⇒ 't ⇒ ('t, 'v) typedstore ⇒ ('t, 'v) typedstore"
  where "pushTyped val typ sto = (let s = updateTypedStore (ShowL⇩n⇩a⇩t (Toploc sto)) val typ sto in snd (allocate s))"

declare pushTyped_def [solidity_symbex]

lemma "accessStore l (updateTypedStore l v t (emptyTypedStore)) = Some v" 
  unfolding updateTypedStore_def updateTypeStore_def accessStore_def updateStore_def by simp

lemma "accessTypeStore l (updateTypedStore l v t (emptyTypedStore)) = Some t" 
  unfolding updateTypedStore_def updateTypeStore_def accessTypeStore_def updateStore_def by simp

lemma allocateTypeSameAccess:
  shows "∀loc. accessTypeStore loc m = accessTypeStore loc (snd (allocate m))" 
  unfolding allocate_def accessStore_def accessTypeStore_def by simp

type_synonym memoryT = "(mtypes,memoryvalue) typedstore"

type_synonym calldataT = memoryT

subsubsection ‹Example›

abbreviation mymemory::memoryT
  where "mymemory ≡
    ⦇Mapping = fmap_of_list
      [(STR ''1.1.0'', MValue STR ''False''),
       (STR ''0.1.0'', MValue STR ''True''),
       (STR ''1.0'', MPointer STR ''1.0''),
       (STR ''1.0.0'', MValue STR ''False''),
       (STR ''0.0.0'', MValue STR ''True''),
       (STR ''0.0'', MPointer STR ''0.0'')],
     Toploc = 1,
     Typed_Mapping = fmap_of_list
      [(STR ''1.1.0'', MTValue TBool),
       (STR ''0.1.0'', MTValue TBool),
       (STR ''1.0'', MTArray 2 (MTValue TBool)),
       (STR ''1.0.0'', MTValue TBool),
       (STR ''0.0.0'', MTValue TBool),
       (STR ''0.0'', MTArray 2 (MTValue TBool))]⦈"

subsubsection ‹Initialization›

subsubsection ‹Definition›

primrec minitRec :: "location ⇒ mtypes ⇒ memoryT ⇒ memoryT"
where
  "minitRec loc (MTArray x t) = (λmem.
    let m = updateTypedStore loc (MPointer loc) (MTArray x t) mem
    in iter (λi m' . minitRec (hash loc (ShowL⇩n⇩a⇩t i)) t m') m x)"
| "minitRec loc (MTValue t) = updateTypedStore loc (MValue (ival t)) (MTValue t)"

definition minit :: "nat ⇒ mtypes ⇒ memoryT ⇒ memoryT"
where
  "minit x t mem =
    (let l = ShowL⇩n⇩a⇩t (Toploc mem);
         m = iter (λi m' . minitRec (hash l (ShowL⇩n⇩a⇩t i)) t m') mem x
     in snd (allocate m))"

declare minit_def [solidity_symbex]

primrec arraysGreaterZero::"mtypes ⇒ bool"
  where "arraysGreaterZero (MTValue v) = True"
       | "arraysGreaterZero (MTArray x t) = (x>0 ∧ arraysGreaterZero t)"

subsubsection ‹Example›

lemma "minit 2 (MTArray 2 (MTValue TBool)) emptyTypedStore =
⦇Mapping = fmap_of_list
  [(STR ''0.0'', MPointer STR ''0.0''), 
   (STR ''0.0.0'', MValue STR ''False''),
   (STR ''1.0.0'', MValue STR ''False''), 
   (STR ''1.0'', MPointer STR ''1.0''),
   (STR ''0.1.0'', MValue STR ''False''), 
   (STR ''1.1.0'', MValue STR ''False'')],
  Toploc = 1,
  Typed_Mapping = fmap_of_list
  [(STR ''0.0'', MTArray 2 (MTValue TBool)), 
   (STR ''0.0.0'', MTValue TBool),
   (STR ''1.0.0'', MTValue TBool), 
   (STR ''1.0'', MTArray 2 (MTValue TBool)),
   (STR ''0.1.0'', MTValue TBool), 
   (STR ''1.1.0'', MTValue TBool)]⦈" by eval



subsubsection ‹Copy from memory to memory›

subsubsection ‹Definition›

primrec cpm2mrec :: "location ⇒ location ⇒ mtypes ⇒ memoryT ⇒ memoryT ⇒ memoryT option"
where
  "cpm2mrec l⇩s l⇩d (MTArray x t) m⇩s m⇩d =
    (case accessStore l⇩s m⇩s of
      Some (MPointer l) ⇒
        (let m = updateTypedStore l⇩d (MPointer l⇩d) (MTArray x t) m⇩d
          in iter' (λi m'. cpm2mrec (hash l (ShowL⇩n⇩a⇩t i)) (hash l⇩d (ShowL⇩n⇩a⇩t i)) t m⇩s m') m x)
    | _ ⇒ None)"
| "cpm2mrec l⇩s l⇩d (MTValue t) m⇩s m⇩d =
    (case accessStore l⇩s m⇩s of
      Some (MValue v) ⇒ Some (updateTypedStore l⇩d (MValue v) (MTValue t) m⇩d)
    | _ ⇒ None)"

definition cpm2m :: "location ⇒ location ⇒ nat ⇒ mtypes ⇒ memoryT ⇒ memoryT ⇒ memoryT option"
where
  "cpm2m l⇩s l⇩d x t m⇩s m⇩d = iter' (λi m. cpm2mrec (hash l⇩s (ShowL⇩n⇩a⇩t i)) (hash l⇩d (ShowL⇩n⇩a⇩t i)) t m⇩s m) m⇩d x"

declare cpm2m_def [solidity_symbex]

subsubsection ‹Example›

lemma "cpm2m (STR ''0'') (STR ''0'') 2 (MTArray 2 (MTValue TBool)) mymemory (snd (allocate emptyTypedStore)) = Some mymemory"
  by eval 

abbreviation mymemory2::memoryT
  where "mymemory2 ≡
    ⦇Mapping = fmap_of_list
      [(STR ''0.5'', MValue STR ''True''),
       (STR ''1.5'', MValue STR ''False'')],
     Toploc = 0,
     Typed_Mapping = fmap_of_list
      [(STR ''0.5'', MTValue TBool),
       (STR ''1.5'', MTValue TBool)]⦈"

lemma "cpm2m (STR ''1.0'') (STR ''5'') 2 (MTValue TBool) mymemory emptyTypedStore = Some mymemory2" by eval

subsection ‹Copy from storage to memory›

subsubsection ‹Definition›

fun cps2mTypeConvert:: "stypes ⇒ mtypes option"
  where
  "cps2mTypeConvert (STValue t) = Some (MTValue t)"
| "cps2mTypeConvert (STArray len t) = (case (cps2mTypeConvert t) of Some t' ⇒ Some (MTArray len t')
                                                                   | None ⇒ None)"
| "cps2mTypeConvert _ = None"

primrec cps2mrec :: "location ⇒ location ⇒ stypes ⇒ storageT ⇒ memoryT ⇒ memoryT option"
where
  "cps2mrec locs locm (STArray x t) sto mem =
    (case cps2mTypeConvert t of
      Some t' ⇒ 
        (let m = updateTypedStore locm (MPointer locm) (MTArray x t') mem
         in iter' (λi m'. cps2mrec (hash locs (ShowL⇩n⇩a⇩t i)) (hash locm (ShowL⇩n⇩a⇩t i)) t sto m') m x)
    | None ⇒ None)"
| "cps2mrec locs locm (STValue t) sto mem =
    (let v = accessStorage t locs sto
    in Some (updateTypedStore locm (MValue v) (MTValue t) mem))"
| "cps2mrec _ _ (STMap _ _) _ _ = None"

definition cps2m :: "location ⇒ location ⇒ nat ⇒ stypes ⇒ storageT ⇒ memoryT ⇒ memoryT option"
where
  "cps2m locs locm x t sto mem =
    iter' (λi m'. cps2mrec (hash locs (ShowL⇩n⇩a⇩t i)) (hash locm (ShowL⇩n⇩a⇩t i)) t sto m') mem x"

declare cps2m_def [solidity_symbex]

subsubsection ‹Example›

abbreviation mystorage3::storageT
where "mystorage3 ≡ (fmap_of_list
  [(STR ''0.0.1'', STR ''True''),
   (STR ''1.0.1'', STR ''False''),
   (STR ''0.1.1'', STR ''True''),
   (STR ''1.1.1'', STR ''False'')])"

lemma "cps2m (STR ''1'') (STR ''0'') 2 (STArray 2 (STValue TBool)) mystorage3 (snd (allocate emptyTypedStore)) = Some mymemory"
  by eval

fun cps2mTypeCompatible:: "stypes ⇒ mtypes ⇒ bool"
  where
  "cps2mTypeCompatible (STValue t) (MTValue t') = (t = t')"
| "cps2mTypeCompatible (STArray len t) (MTArray len' t') = (len' > 0 ∧ len = len' ∧ cps2mTypeCompatible t t')"
| "cps2mTypeCompatible _ _ = False"

subsection ‹Copy from memory to storage›

subsubsection ‹Definition›
primrec cpm2srec :: "location ⇒ location ⇒ mtypes ⇒ memoryT ⇒ storageT ⇒ storageT option"
where
  "cpm2srec locm locs (MTArray x t) mem sto =
    (case accessStore locm mem of
      Some (MPointer l) ⇒
        iter' (λi s'. cpm2srec (hash l (ShowL⇩n⇩a⇩t i)) (hash locs (ShowL⇩n⇩a⇩t i)) t mem s') sto x
    | _ ⇒ None)"
| "cpm2srec locm locs (MTValue t) mem sto =
    (case accessStore locm mem of
      Some (MValue v) ⇒ Some (fmupd locs v sto)
    | _ ⇒ None)"

definition cpm2s :: "location ⇒ location ⇒ nat ⇒ mtypes ⇒ memoryT ⇒ storageT ⇒ storageT option"
where
  "cpm2s locm locs x t mem sto =
    iter' (λi s'. cpm2srec (hash locm (ShowL⇩n⇩a⇩t i)) (hash locs (ShowL⇩n⇩a⇩t i)) t mem s') sto x"

declare cpm2s_def [solidity_symbex]

subsubsection ‹Example›

lemma "cpm2s (STR ''0'') (STR ''1'') 2 (MTArray 2 (MTValue TBool)) mymemory fmempty = Some mystorage3"
  by eval

declare copyRec.simps [simp del, solidity_symbex add]
declare minitRec.simps [simp del, solidity_symbex add]
declare cpm2mrec.simps [simp del, solidity_symbex add]
declare cps2mrec.simps [simp del, solidity_symbex add]
declare cpm2srec.simps [simp del, solidity_symbex add]

end