Theory Storage
section‹Storage›
theory Storage
imports Valuetypes "HOL-Library.Finite_Map"
begin
fun hash :: "Location ⇒ String.literal ⇒ Location"
where "hash loc ix = ix + (STR ''.'' + loc)"
subsection ‹General Store›
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›