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 (ShowLnat 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 (ShowLnat (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 (ShowLint i)) (hash loc' (ShowLint 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 (ShowLint i)) (hash loc' (ShowLint 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 (ShowLint 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 = ShowLnat (toploc mem);
         m = iter (λi m' . minitRec (hash l (ShowLint 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 ls ld (MTArray x t) ms md =
    (case accessStore ls ms of
      Some e 
        (case e of
          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)
    | None  None)"
| "cpm2mrec ls ld (MTValue t) ms md =
    (case accessStore ls ms of
      Some e  (case e of
          MValue v  Some (updateStore ld (MValue v) md)
        | _  None)
    | None  None)"
 
fun 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"

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 (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"

(*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 (ShowLint i)) (hash locm (ShowLint 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 (ShowLint i)) (hash locs (ShowLint 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 (ShowLint i)) (hash locs (ShowLint 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