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_nat 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 (ShowL_nat (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_int i)) (hash l_d (ShowL_int 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_int i)) (hash l_d (ShowL_int 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_int 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_nat (toploc mem);
         m = iter (λi m' . minitRec (hash l (ShowL_int i)) t m') mem x
     in snd (allocate m))"

declare minit_def [solidity_symbex]

subsubsection ‹Example›

lemma "minit 2 (MTArray 2 (MTValue TBool)) emptyStore =
\<lparr>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_int i)) (hash l_d (ShowL_int 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_int i)) (hash l_d (ShowL_int 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_int i)) (hash locm (ShowL_int 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_int i)) (hash locm (ShowL_int 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_int i)) (hash locs (ShowL_int 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_int i)) (hash locs (ShowL_int 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