Theory Storage

section‹Storage›

theory Storage
imports Valuetypes "HOL-Library.Finite_Map"

begin

(*Covered*)
fun hash :: "Location ⇒ String.literal ⇒ Location"
where "hash loc ix = ix + (STR ''.'' + loc)"

subsection ‹General Store›

(*Covered*)
record 'v Store =
  mapping :: "(Location,'v) fmap"
  toploc :: nat 

fun accessStore :: "Location ⇒ 'v Store ⇒ 'v option"
where "accessStore loc st = fmlookup (mapping st) loc"

definition emptyStore :: "'v Store"
where "emptyStore = ⦇ mapping=fmempty, toploc=0 ⦈"

declare emptyStore_def [solidity_symbex]

fun allocate :: "'v Store ⇒ Location * ('v Store)"
where "allocate s = (let ntop = Suc(toploc s) in (ShowL⇩n⇩a⇩t ntop, s ⦇toploc := ntop⦈))"

fun updateStore :: "Location ⇒ 'v ⇒ 'v Store ⇒ 'v Store"
where "updateStore loc val s = s ⦇ mapping := fmupd loc val (mapping s)⦈"

fun push :: "'v ⇒ 'v Store ⇒ 'v Store"
  where "push val sto = (let s = updateStore (ShowL⇩n⇩a⇩t (toploc sto)) val sto in snd (allocate s))"

subsection ‹Stack›
(*Covered*)
datatype Stackvalue = KValue Valuetype
                    | KCDptr Location
                    | KMemptr Location
                    | KStoptr Location

(*Covered*)
type_synonym Stack = "Stackvalue Store"

subsection ‹Storage›

subsubsection ‹Definition›

type_synonym Storagevalue = Valuetype

(*Covered*)
type_synonym StorageT = "(Location,Storagevalue) fmap"

(*Covered*)
datatype STypes = STArray int STypes
                | STMap Types STypes
                | STValue Types

subsubsection ‹Example›

abbreviation mystorage::StorageT
where "mystorage ≡ (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'')])"

subsubsection ‹Access storage›

(*Covered*)
fun accessStorage :: "Types ⇒ Location ⇒ StorageT ⇒ Storagevalue"
where
  "accessStorage t loc sto =
    (case fmlookup sto loc of
      Some v ⇒ v
    | None ⇒ ival t)"

subsubsection ‹Copy from storage to storage›

fun copyRec :: "Location ⇒ Location ⇒ STypes ⇒ StorageT ⇒ StorageT option"
where
  "copyRec loc loc' (STArray x t) sto =
    iter' (λi s'. copyRec (hash loc (ShowL⇩i⇩n⇩t i)) (hash loc' (ShowL⇩i⇩n⇩t i)) t s') sto x"
| "copyRec loc loc' (STValue t) sto =
    (let e = accessStorage t loc sto in Some (fmupd loc' e sto))"
| "copyRec _ _ (STMap _ _) _ = None"
 
fun copy :: "Location ⇒ Location ⇒ int ⇒ STypes ⇒ StorageT ⇒ StorageT option"
where
  "copy loc loc' x t sto =
    iter' (λi s'. copyRec (hash loc (ShowL⇩i⇩n⇩t i)) (hash loc' (ShowL⇩i⇩n⇩t i)) t s') sto x"

subsection ‹Memory and Calldata›

subsubsection ‹Definition›

(*Covered*)
datatype Memoryvalue =
  MValue Valuetype
  | MPointer Location
(*Covered*)
type_synonym MemoryT = "Memoryvalue Store"
(*Covered*)
type_synonym CalldataT = MemoryT
(*Covered*)
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›

(*Covered*)
fun 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 (ShowL⇩i⇩n⇩t i)) t m') m x)"
| "minitRec loc (MTValue t) = updateStore loc (MValue (ival t))"

(*Covered*)
fun minit :: "int ⇒ MTypes ⇒ MemoryT ⇒ MemoryT"
where
  "minit x t mem =
    (let l = ShowL⇩n⇩a⇩t (toploc mem);
         m = iter (λi m' . minitRec (hash l (ShowL⇩i⇩n⇩t i)) t m') mem x
     in snd (allocate m))"

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›

fun 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 e ⇒
        (case e of
          MPointer l ⇒ (let m = updateStore l⇩d (MPointer l⇩d) m⇩d
             in iter' (λi m'. cpm2mrec (hash l⇩s (ShowL⇩i⇩n⇩t i)) (hash l⇩d (ShowL⇩i⇩n⇩t i)) t m⇩s m') m x)
        | _ ⇒ None)
    | None ⇒ None)"
| "cpm2mrec l⇩s l⇩d (MTValue t) m⇩s m⇩d =
    (case accessStore l⇩s m⇩s of
      Some e ⇒ (case e of
          MValue v ⇒ Some (updateStore l⇩d (MValue v) m⇩d)
        | _ ⇒ None)
    | None ⇒ None)"
 
fun cpm2m :: "Location ⇒ Location ⇒ int ⇒ 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⇩i⇩n⇩t i)) (hash l⇩d (ShowL⇩i⇩n⇩t i)) t m⇩s m) m⇩d x"

subsubsection ‹Example›

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

subsection ‹Copy from storage to memory›

subsubsection ‹Definition›

(*Covered*)
fun 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 (ShowL⇩i⇩n⇩t i)) (hash locm (ShowL⇩i⇩n⇩t 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"

(*Covered*)
fun cps2m :: "Location ⇒ Location ⇒ int ⇒ STypes ⇒ StorageT ⇒ MemoryT ⇒ MemoryT option"
where
  "cps2m locs locm x t sto mem =
    iter' (λi m'. cps2mrec (hash locs (ShowL⇩i⇩n⇩t i)) (hash locm (ShowL⇩i⇩n⇩t i)) t sto m') mem x"

subsubsection ‹Example›

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

subsection ‹Copy from memory to storage›

subsubsection ‹Definition›

(*covered*)
fun cpm2srec :: "Location ⇒ Location ⇒ MTypes ⇒ MemoryT ⇒ StorageT ⇒ StorageT option"
where
  "cpm2srec locm locs (MTArray x t) mem sto =
    (case accessStore locm mem of
      Some e ⇒
        (case e of
          MPointer l ⇒ iter' (λi s'. cpm2srec (hash locm (ShowL⇩i⇩n⇩t i)) (hash locs (ShowL⇩i⇩n⇩t i)) t mem s') sto x
        | _ ⇒ None)
    | None ⇒ None)"
| "cpm2srec locm locs (MTValue t) mem sto =
    (case accessStore locm mem of
      Some e ⇒ (case e of
          MValue v ⇒ Some (fmupd locs v sto)
        | _ ⇒ None)
    | None ⇒ None)"

(*covered*)
fun cpm2s :: "Location ⇒ Location ⇒ int ⇒ MTypes ⇒ MemoryT ⇒ StorageT ⇒ StorageT option"
where
  "cpm2s locm locs x t mem sto =
    iter' (λi s'. cpm2srec (hash locm (ShowL⇩i⇩n⇩t i)) (hash locs (ShowL⇩i⇩n⇩t i)) t mem s') sto x"

subsubsection ‹Example›

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

end