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]

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) "ii'" | (2) "i=i'  ll'" 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  'v Store  'v 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 :: "'v Store  Location * ('v Store)"
where "allocate s = (let ntop = Suc(toploc s) in (ShowLnat ntop, s toploc := ntop))"



definition updateStore :: "Location  'v  'v Store  'v Store"
where "updateStore loc val s = s  mapping := fmupd loc val (mapping s)"

declare updateStore_def [solidity_symbex]

definition push :: "'v  'v Store  'v Store"
  where "push val sto = (let s = updateStore (ShowLnat (toploc sto)) val sto in snd (allocate s))"

declare push_def [solidity_symbex]

subsection ‹Stack›

datatype 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 STypes = STArray int 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 ls ld (STArray x t) sto =
    iter' (λi s'. copyRec (hash ls (ShowLint i)) (hash ld (ShowLint i)) t s') sto x"
| "copyRec ls ld (STValue t) sto =
    (let e = accessStorage t ls sto in Some (fmupd ld e sto))"
| "copyRec _ _ (STMap _ _) _ = None"
 
definition copy :: "Location  Location  int  STypes  StorageT  StorageT option"
where
  "copy ls ld x t sto =
    iter' (λi s'. copyRec (hash ls (ShowLint i)) (hash ld (ShowLint 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

type_synonym MemoryT = "Memoryvalue Store"

type_synonym CalldataT = MemoryT

datatype MTypes =
  MTArray int MTypes
  | MTValue Types

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"

subsubsection ‹Initialization›

subsubsection ‹Definition›

primrec minitRec :: "Location  MTypes  MemoryT  MemoryT"
where
  "minitRec loc (MTArray x t) = (λmem.
    let m = updateStore loc (MPointer loc) mem
    in iter (λi m' . minitRec (hash loc (ShowLint i)) t m') m x)"
| "minitRec loc (MTValue t) = updateStore loc (MValue (ival t))"

definition minit :: "int  MTypes  MemoryT  MemoryT"
where
  "minit x t mem =
    (let l = ShowLnat (toploc mem);
         m = iter (λi m' . minitRec (hash l (ShowLint i)) t m') mem x
     in snd (allocate m))"

declare minit_def [solidity_symbex]

subsubsection ‹Example›

lemma "minit 2 (MTArray 2 (MTValue TBool)) emptyStore =
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" by eval

subsubsection ‹Copy from memory to memory›

subsubsection ‹Definition›

primrec cpm2mrec :: "Location  Location  MTypes  MemoryT  MemoryT  MemoryT option"
where
  "cpm2mrec ls ld (MTArray x t) ms md =
    (case accessStore ls ms of
      Some (MPointer l) 
        (let m = updateStore ld (MPointer ld) md
          in iter' (λi m'. cpm2mrec (hash ls (ShowLint i)) (hash ld (ShowLint i)) t ms m') m x)
    | _  None)"
| "cpm2mrec ls ld (MTValue t) ms md =
    (case accessStore ls ms of
      Some (MValue v)  Some (updateStore ld (MValue v) md)
    | _  None)"

definition cpm2m :: "Location  Location  int  MTypes  MemoryT  MemoryT  MemoryT option"
where
  "cpm2m ls ld x t ms md = iter' (λi m. cpm2mrec (hash ls (ShowLint i)) (hash ld (ShowLint i)) t ms m) md x"

declare cpm2m_def [solidity_symbex]

subsubsection ‹Example›

lemma "cpm2m (STR ''0'') (STR ''0'') 2 (MTArray 2 (MTValue TBool)) mymemory (snd (allocate emptyStore)) = 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"

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

subsection ‹Copy from storage to memory›

subsubsection ‹Definition›

primrec cps2mrec :: "Location  Location  STypes  StorageT  MemoryT  MemoryT option"
where
  "cps2mrec locs locm (STArray x t) sto mem =
    (let m = updateStore locm (MPointer locm) mem
    in iter' (λi m'. cps2mrec (hash locs (ShowLint i)) (hash locm (ShowLint i)) t sto m') m x)"
| "cps2mrec locs locm (STValue t) sto mem =
    (let v = accessStorage t locs sto
    in Some (updateStore locm (MValue v) mem))"
| "cps2mrec _ _ (STMap _ _) _ _ = None"

definition cps2m :: "Location  Location  int  STypes  StorageT  MemoryT  MemoryT option"
where
  "cps2m locs locm x t sto mem =
    iter' (λi m'. cps2mrec (hash locs (ShowLint i)) (hash locm (ShowLint 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 emptyStore)) = Some mymemory"
  by eval

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 locm (ShowLint i)) (hash locs (ShowLint 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  int  MTypes  MemoryT  StorageT  StorageT option"
where
  "cpm2s locm locs x t mem sto =
    iter' (λi s'. cpm2srec (hash locm (ShowLint i)) (hash locs (ShowLint 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