# 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) "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 ⇒ '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 (ShowL⇩n⇩a⇩t ntop, s ⦇toploc := ntop⦈))"

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

definition 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))"

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 l⇩s l⇩d (STArray x t) sto =
iter' (λi s'. copyRec (hash l⇩s (ShowL⇩i⇩n⇩t i)) (hash l⇩d (ShowL⇩i⇩n⇩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 ⇒ int ⇒ STypes ⇒ StorageT ⇒ StorageT option"
where
"copy l⇩s l⇩d x t sto =
iter' (λi s'. copyRec (hash l⇩s (ShowL⇩i⇩n⇩t i)) (hash l⇩d (ShowL⇩i⇩n⇩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

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 (ShowL⇩i⇩n⇩t 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 = 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))"

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 l⇩s l⇩d (MTArray x t) m⇩s m⇩d =
(case accessStore l⇩s m⇩s of
Some (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)"
| "cpm2mrec l⇩s l⇩d (MTValue t) m⇩s m⇩d =
(case accessStore l⇩s m⇩s of
Some (MValue v) ⇒ Some (updateStore l⇩d (MValue v) m⇩d)
| _ ⇒ None)"

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

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

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

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 (ShowL⇩i⇩n⇩t i)) (hash locs (ShowL⇩i⇩n⇩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 ⇒ 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"

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
```