# Theory Solidity_Evaluator

```section‹ Solidty Evaluator and Code Generator Setup›

theory
Solidity_Evaluator
imports
Solidity_Main
"HOL-Library.Code_Target_Numeral"
"HOL-Library.Sublist"
"HOL-Library.Finite_Map"
begin

paragraph‹Generalized Unit Tests›

lemma  "createSInt 8 500 = STR ''-12''"
by(eval)

lemma "STR ''-92134039538802366542421159375273829975''
= createSInt 128 45648483135649456465465452123894894554654654654654646999465"
by(eval)

lemma "STR ''-128'' = createSInt 8 (-128)"
by(eval)

lemma "STR ''244'' = (createUInt 8 500)"
by(eval)

lemma "STR ''220443428915524155977936330922349307608''
= (createUInt 128 4564848313564945646546545212389489455465465465465464699946544654654654654168)"
by(eval)

lemma "less (TUInt 144) (TSInt 160) (STR ''5'') (STR ''8'') = Some(STR ''True'', TBool) "
by(eval)

subsection‹Code Generator Setup and Local Tests›

subsubsection‹Utils›

definition EMPTY::"String.literal" where "EMPTY = STR ''''"

definition FAILURE::"String.literal" where "FAILURE = STR ''Failure''"

fun intersperse :: "String.literal ⇒ String.literal list ⇒ String.literal" where
"intersperse s [] = EMPTY"
| "intersperse s [x] = x"
| "intersperse s (x # xs) = x + s + intersperse s xs"

definition splitAt::"nat ⇒ String.literal ⇒ String.literal × String.literal" where
"splitAt n xs = (String.implode(take n (String.explode xs)), String.implode(drop n (String.explode xs)))"

fun splitOn':: "'a ⇒ 'a list ⇒ 'a list ⇒ 'a list list" where
"splitOn' x [] acc = [rev acc]"
| "splitOn' x (y#ys) acc = (if x = y then (rev acc)#(splitOn' x ys [])
else splitOn' x ys (y#acc))"

fun splitOn::"'a  ⇒ 'a list ⇒ 'a list list" where
"splitOn x xs = splitOn' x xs []"

definition isSuffixOf::"String.literal ⇒ String.literal ⇒ bool" where
"isSuffixOf s x = suffix (String.explode s) (String.explode x)"

definition tolist :: "Location ⇒ String.literal list" where
"tolist s = map String.implode (splitOn (CHR ''.'') (String.explode s))"

abbreviation convert :: "Location ⇒ Location"
where "convert loc ≡ (if loc= STR ''True'' then STR ''true'' else
if loc=STR ''False'' then STR ''false'' else loc)"

definition ‹sorted_list_of_set' ≡ map_fun id id (folding_on.F insort [])›

lemma sorted_list_of_fset'_def': ‹sorted_list_of_set' = sorted_list_of_set›
apply(rule ext)
by (simp add: sorted_list_of_set'_def sorted_list_of_set_def sorted_key_list_of_set_def)

lemma sorted_list_of_set_sort_remdups' [code]:
‹sorted_list_of_set' (set xs) = sort (remdups xs)›
using sorted_list_of_fset'_def' sorted_list_of_set_sort_remdups
by metis

definition  locations_map :: "Location ⇒ (Location, 'v) fmap ⇒ Location list" where
"locations_map loc = (filter (isSuffixOf ((STR ''.'')+loc))) ∘  sorted_list_of_set' ∘ fset ∘ fmdom"

definition  locations :: "Location ⇒ 'v Store ⇒ Location list" where
"locations loc = locations_map loc ∘ mapping"

subsubsection‹Valuetypes›

fun dump⇩V⇩a⇩l⇩u⇩e⇩t⇩y⇩p⇩e⇩s::"Types ⇒ Valuetype ⇒ String.literal" where
"dump⇩V⇩a⇩l⇩u⇩e⇩t⇩y⇩p⇩e⇩s (TSInt _) n = n"
| "dump⇩V⇩a⇩l⇩u⇩e⇩t⇩y⇩p⇩e⇩s (TUInt _) n = n"
| "dump⇩V⇩a⇩l⇩u⇩e⇩t⇩y⇩p⇩e⇩s TBool b = (if b = (STR ''True'') then  STR ''true'' else STR ''false'')"
| "dump⇩V⇩a⇩l⇩u⇩e⇩t⇩y⇩p⇩e⇩s TAddr ad = ad"

subsubsection‹Memory›

datatype Data⇩M⇩e⇩m⇩o⇩r⇩y = MArray "Data⇩M⇩e⇩m⇩o⇩r⇩y list"
| MBool bool
| MInt int
| MAddress Address

fun loadRec⇩M⇩e⇩m⇩o⇩r⇩y :: "Location ⇒ Data⇩M⇩e⇩m⇩o⇩r⇩y ⇒ MemoryT ⇒ MemoryT" and
iterateM :: "Location ⇒ MemoryT × nat ⇒ Data⇩M⇩e⇩m⇩o⇩r⇩y ⇒ MemoryT × nat" where
"loadRec⇩M⇩e⇩m⇩o⇩r⇩y loc (MArray dat) mem = fst (foldl (iterateM loc) (updateStore loc (MPointer loc) mem,0) dat)"
| "loadRec⇩M⇩e⇩m⇩o⇩r⇩y loc (MBool b) mem = updateStore loc ((MValue ∘ ShowL⇩b⇩o⇩o⇩l) b) mem "
| "loadRec⇩M⇩e⇩m⇩o⇩r⇩y loc (MInt i) mem = updateStore loc ((MValue ∘ ShowL⇩i⇩n⇩t) i) mem "
| "loadRec⇩M⇩e⇩m⇩o⇩r⇩y loc (MAddress ad) mem = updateStore loc (MValue ad) mem"
| "iterateM loc (mem,x) d = (loadRec⇩M⇩e⇩m⇩o⇩r⇩y (hash loc (ShowL⇩n⇩a⇩t x)) d mem, Suc x)"

definition load⇩M⇩e⇩m⇩o⇩r⇩y :: "Data⇩M⇩e⇩m⇩o⇩r⇩y list ⇒ MemoryT ⇒ MemoryT" where
"load⇩M⇩e⇩m⇩o⇩r⇩y dat mem = (let loc   = ShowL⇩n⇩a⇩t (toploc mem);
(m, _) = foldl (iterateM loc) (mem, 0) dat
in (snd ∘ allocate) m)"

fun dumprec⇩M⇩e⇩m⇩o⇩r⇩y:: "Location ⇒ MTypes ⇒ MemoryT ⇒ String.literal ⇒ String.literal ⇒ String.literal" where
"dumprec⇩M⇩e⇩m⇩o⇩r⇩y loc tp mem ls str =
(case accessStore loc mem of
Some (MPointer l) ⇒
(case tp of
(MTArray x t) ⇒ iter (λi str' . dumprec⇩M⇩e⇩m⇩o⇩r⇩y ((hash l o ShowL⇩i⇩n⇩t) i) t mem
(ls + (STR ''['') + (ShowL⇩i⇩n⇩t i) + (STR '']'')) str') str x
| _ ⇒ FAILURE)
| Some (MValue v) ⇒
(case tp of
MTValue t ⇒ str + ls + (STR ''=='') + dump⇩V⇩a⇩l⇩u⇩e⇩t⇩y⇩p⇩e⇩s t v + (STR ''⏎'')
| _ ⇒ FAILURE)
| None ⇒ FAILURE)"

definition dump⇩M⇩e⇩m⇩o⇩r⇩y :: "Location ⇒ int ⇒ MTypes ⇒ MemoryT ⇒ String.literal ⇒String.literal ⇒String.literal" where
"dump⇩M⇩e⇩m⇩o⇩r⇩y loc x t mem ls str = iter (λi. dumprec⇩M⇩e⇩m⇩o⇩r⇩y ((hash loc (ShowL⇩i⇩n⇩t i))) t mem (ls + STR ''['' + (ShowL⇩i⇩n⇩t i + STR '']''))) str x"

subsubsection‹Storage›

datatype Data⇩S⇩t⇩o⇩r⇩a⇩g⇩e =
SArray "Data⇩S⇩t⇩o⇩r⇩a⇩g⇩e list"
| SMap "(String.literal × Data⇩S⇩t⇩o⇩r⇩a⇩g⇩e) list"
| SBool bool
| SInt int
| SAddress Address

fun go⇩S⇩t⇩o⇩r⇩a⇩g⇩e :: "Location ⇒ (String.literal ×  STypes) ⇒ (String.literal × STypes)" where
"go⇩S⇩t⇩o⇩r⇩a⇩g⇩e l (s, STArray _ t) = (s + (STR ''['') + (convert l) + (STR '']''), t)"
| "go⇩S⇩t⇩o⇩r⇩a⇩g⇩e l (s, STMap _ t) = (s + (STR ''['') + (convert l) + (STR '']''), t)"
| "go⇩S⇩t⇩o⇩r⇩a⇩g⇩e l (s, STValue t) = (s + (STR ''['') + (convert l) + (STR '']''), STValue t)"

fun dumpSingle⇩S⇩t⇩o⇩r⇩a⇩g⇩e :: "StorageT ⇒ String.literal ⇒ STypes ⇒ (Location × Location) ⇒ String.literal ⇒ String.literal" where
"dumpSingle⇩S⇩t⇩o⇩r⇩a⇩g⇩e sto id' tp (loc,l) str =
(case foldr go⇩S⇩t⇩o⇩r⇩a⇩g⇩e (tolist loc) (str + id', tp) of
(s, STValue t) ⇒
(case sto \$\$ (loc + l) of
Some v ⇒ s + (STR ''=='') + dump⇩V⇩a⇩l⇩u⇩e⇩t⇩y⇩p⇩e⇩s t v
| None ⇒ FAILURE)
| _ ⇒ FAILURE)"

definition iterate where
"iterate loc t id' sto s l = dumpSingle⇩S⇩t⇩o⇩r⇩a⇩g⇩e sto id' t (splitAt (length (String.explode l) - length (String.explode loc) - 1) l) s + (STR ''⏎'')"

fun dump⇩S⇩t⇩o⇩r⇩a⇩g⇩e ::  "StorageT ⇒ Location ⇒ String.literal ⇒ STypes ⇒ String.literal ⇒ String.literal" where
"dump⇩S⇩t⇩o⇩r⇩a⇩g⇩e sto loc id' (STArray _ t) str = foldl (iterate loc t id' sto) str (locations_map loc sto)"
| "dump⇩S⇩t⇩o⇩r⇩a⇩g⇩e sto loc id' (STMap _ t) str = foldl (iterate loc t id' sto) str (locations_map loc sto)"
| "dump⇩S⇩t⇩o⇩r⇩a⇩g⇩e sto loc id' (STValue t) str =
(case sto \$\$ loc of
Some v ⇒ str + id' + (STR ''=='') + dump⇩V⇩a⇩l⇩u⇩e⇩t⇩y⇩p⇩e⇩s t v + (STR ''⏎'')
| _ ⇒ str)"

fun loadRec⇩S⇩t⇩o⇩r⇩a⇩g⇩e :: "Location ⇒ Data⇩S⇩t⇩o⇩r⇩a⇩g⇩e ⇒ StorageT ⇒ StorageT" and
iterateSA :: "Location ⇒ StorageT × nat ⇒ Data⇩S⇩t⇩o⇩r⇩a⇩g⇩e ⇒ StorageT × nat" and
iterateSM :: "Location ⇒ String.literal × Data⇩S⇩t⇩o⇩r⇩a⇩g⇩e ⇒ StorageT ⇒ StorageT" where
"loadRec⇩S⇩t⇩o⇩r⇩a⇩g⇩e loc (SArray dat) sto = fst (foldl (iterateSA loc) (sto,0) dat)"
| "loadRec⇩S⇩t⇩o⇩r⇩a⇩g⇩e loc (SMap dat) sto  = foldr (iterateSM loc) dat sto"
| "loadRec⇩S⇩t⇩o⇩r⇩a⇩g⇩e loc (SBool b) sto = fmupd loc (ShowL⇩b⇩o⇩o⇩l b) sto"
| "loadRec⇩S⇩t⇩o⇩r⇩a⇩g⇩e loc (SInt i)  sto = fmupd loc (ShowL⇩i⇩n⇩t i) sto"
| "loadRec⇩S⇩t⇩o⇩r⇩a⇩g⇩e loc (SAddress ad) sto = fmupd loc ad sto"
| "iterateSA loc (s', x) d = (loadRec⇩S⇩t⇩o⇩r⇩a⇩g⇩e (hash loc (ShowL⇩n⇩a⇩t x)) d s', Suc x)"
| "iterateSM loc (k, v) s' = loadRec⇩S⇩t⇩o⇩r⇩a⇩g⇩e (hash loc k) v s'"

subsubsection‹Environment›

datatype Data⇩E⇩n⇩v⇩i⇩r⇩o⇩n⇩m⇩e⇩n⇩t =
Memarr "Data⇩M⇩e⇩m⇩o⇩r⇩y list" |
CDarr "Data⇩M⇩e⇩m⇩o⇩r⇩y list" |
Stoarr "Data⇩S⇩t⇩o⇩r⇩a⇩g⇩e list"|
Stomap "(String.literal × Data⇩S⇩t⇩o⇩r⇩a⇩g⇩e) list" |
Stackbool bool |
Stobool bool |
Stackint int |
Stoint int |
Stackaddr Address |
Stoaddr Address

fun astore :: "Identifier ⇒ Type ⇒ Valuetype ⇒ StorageT * Environment ⇒ StorageT * Environment"
where "astore i t v (s, e) = (fmupd i v s, (updateEnv i t (Storeloc i) e))"

fun loadsimple⇩E⇩n⇩v⇩i⇩r⇩o⇩n⇩m⇩e⇩n⇩t :: "(Stack × CalldataT × MemoryT × StorageT × Environment)
⇒ (Identifier × Type × Data⇩E⇩n⇩v⇩i⇩r⇩o⇩n⇩m⇩e⇩n⇩t) ⇒ (Stack × CalldataT × MemoryT × StorageT × Environment)"
where
"loadsimple⇩E⇩n⇩v⇩i⇩r⇩o⇩n⇩m⇩e⇩n⇩t (k, c, m, s, e) (id', tp, d) = (case d of
Stackbool b ⇒
let (k', e') = astack id' tp (KValue (ShowL⇩b⇩o⇩o⇩l b)) (k, e)
in (k', c, m, s, e')
| Stobool b ⇒
let (s', e') = astore id' tp (ShowL⇩b⇩o⇩o⇩l b) (s, e)
in (k, c, m, s', e')
|  Stackint n ⇒
let (k', e') = astack id' tp (KValue (ShowL⇩i⇩n⇩t n)) (k, e)
in (k', c, m, s, e')
|  Stoint n ⇒
let (s', e') = astore id' tp (ShowL⇩i⇩n⇩t n) (s, e)
in (k, c, m, s', e')
|  Stackaddr ad ⇒
let (k', e') = astack id' tp (KValue ad) (k, e)
in (k', c, m, s, e')
|  Stoaddr ad ⇒
let (s', e') = astore id' tp ad (s, e)
in (k, c, m, s', e')
|  CDarr a ⇒
let l = ShowL⇩n⇩a⇩t (toploc c);
c' = load⇩M⇩e⇩m⇩o⇩r⇩y a c;
(k', e') = astack id' tp (KCDptr l) (k, e)
in (k', c', m, s, e')
|  Memarr a ⇒
let l = ShowL⇩n⇩a⇩t (toploc m);
m' = load⇩M⇩e⇩m⇩o⇩r⇩y a m;
(k', e') = astack id' tp (KMemptr l) (k, e)
in (k', c, m', s, e')
|  Stoarr a ⇒
let s' = loadRec⇩S⇩t⇩o⇩r⇩a⇩g⇩e id' (SArray a) s;
e' = updateEnv id' tp (Storeloc id') e
in (k, c, m, s', e')
|  Stomap mp ⇒
let s' = loadRec⇩S⇩t⇩o⇩r⇩a⇩g⇩e id' (SMap mp) s;
e' = updateEnv id' tp (Storeloc id') e
in (k, c, m, s', e')
)"

definition getValue⇩E⇩n⇩v⇩i⇩r⇩o⇩n⇩m⇩e⇩n⇩t :: "Stack ⇒ CalldataT ⇒ MemoryT ⇒ StorageT ⇒ Environment ⇒ Identifier ⇒ String.literal ⇒ String.literal"
where
"getValue⇩E⇩n⇩v⇩i⇩r⇩o⇩n⇩m⇩e⇩n⇩t k c m s e i txt = (case fmlookup (denvalue e) i of
Some (tp, Stackloc l) ⇒ (case accessStore l k of
Some (KValue v) ⇒ (case tp of
Value t ⇒ (txt + i + (STR ''=='') + dump⇩V⇩a⇩l⇩u⇩e⇩t⇩y⇩p⇩e⇩s t v + (STR ''⏎''))
|  _ ⇒ FAILURE)
| Some (KCDptr p) ⇒ (case tp of
Calldata (MTArray x t) ⇒ dump⇩M⇩e⇩m⇩o⇩r⇩y p x t c i txt
| _ ⇒ FAILURE)
| Some (KMemptr p) ⇒ (case tp of
Memory (MTArray x t) ⇒ dump⇩M⇩e⇩m⇩o⇩r⇩y p x t m i txt
| _ ⇒ FAILURE)
| Some (KStoptr p) ⇒ (case tp of
Storage t ⇒ dump⇩S⇩t⇩o⇩r⇩a⇩g⇩e s p i t txt
| _ ⇒ FAILURE))
| Some (Storage t, Storeloc l) ⇒ dump⇩S⇩t⇩o⇩r⇩a⇩g⇩e s l i t txt
| _ ⇒ FAILURE
)"

definition dump⇩E⇩n⇩v⇩i⇩r⇩o⇩n⇩m⇩e⇩n⇩t :: "Stack  ⇒ CalldataT ⇒ MemoryT ⇒ StorageT ⇒ Environment ⇒ Identifier list ⇒ String.literal"
where "dump⇩E⇩n⇩v⇩i⇩r⇩o⇩n⇩m⇩e⇩n⇩t k c m s e sl = foldr (getValue⇩E⇩n⇩v⇩i⇩r⇩o⇩n⇩m⇩e⇩n⇩t k c m s e) sl EMPTY"

subsubsection‹Accounts›

fun load⇩A⇩c⇩c⇩o⇩u⇩n⇩t⇩s :: "Accounts ⇒ (Address × Balance × atype × nat) list ⇒ Accounts" where
"load⇩A⇩c⇩c⇩o⇩u⇩n⇩t⇩s acc []             = acc"
| "load⇩A⇩c⇩c⇩o⇩u⇩n⇩t⇩s acc ((ad, b, t, c)#as) = load⇩A⇩c⇩c⇩o⇩u⇩n⇩t⇩s (acc (ad:=⦇bal=b, type=Some t, contracts=c⦈)) as"

fun dumpStorage::"StorageT ⇒ (Identifier × Member) ⇒ String.literal" where
"dumpStorage s (i, Var x) = dump⇩S⇩t⇩o⇩r⇩a⇩g⇩e s i i x EMPTY"
| "dumpStorage s (i, Function x) = FAILURE"
| "dumpStorage s (i, Method x) = FAILURE"

fun dumpMembers :: "atype option ⇒ Environment⇩P ⇒ StorageT ⇒ String.literal" where
"dumpMembers None ep s = FAILURE"
| "dumpMembers (Some EOA) _ _ = STR ''EOA''"
| "dumpMembers (Some (Contract name)) ep s =
(case ep \$\$ name of
Some (ct, _) ⇒ name + STR ''('' + (intersperse (STR '','') (map (dumpStorage s) (filter (is_Var ∘ snd) (sorted_list_of_fmap ct)))) + STR '')''
| None ⇒ FAILURE)"

(*
The first parameter is just to guarantee termination
*)
fun dump⇩A⇩c⇩c⇩o⇩u⇩n⇩t :: "nat ⇒ Environment⇩P ⇒ State ⇒ Address ⇒ String.literal"
where "dump⇩A⇩c⇩c⇩o⇩u⇩n⇩t 0 _ _ _ = FAILURE"
| "dump⇩A⇩c⇩c⇩o⇩u⇩n⇩t (Suc c) ep st a = a + STR '': '' +
STR ''balance=='' + bal (accounts st a) +
STR '' - '' + dumpMembers (type (accounts st a)) ep (storage st a) +
iter (λx s. s + STR ''⏎'' + dump⇩A⇩c⇩c⇩o⇩u⇩n⇩t c ep st (hash a (ShowL⇩i⇩n⇩t x))) EMPTY (int (contracts (accounts st a)))"

definition dump⇩A⇩c⇩c⇩o⇩u⇩n⇩t⇩s :: "Environment⇩P ⇒ State ⇒ Address list ⇒ String.literal"
where "dump⇩A⇩c⇩c⇩o⇩u⇩n⇩t⇩s ep st al = intersperse (STR ''⏎'') (map (dump⇩A⇩c⇩c⇩o⇩u⇩n⇩t 1000 ep st) al)"

definition init⇩A⇩c⇩c⇩o⇩u⇩n⇩t::"(Address × Balance × atype × nat) list => Accounts" where
"init⇩A⇩c⇩c⇩o⇩u⇩n⇩t = load⇩A⇩c⇩c⇩o⇩u⇩n⇩t⇩s emptyAccount"

type_synonym Data⇩P = "(Identifier × Member) list × ((Identifier × Type) list × S) × S"

fun loadProc::"Identifier ⇒ Data⇩P ⇒ Environment⇩P ⇒ Environment⇩P"
where "loadProc i (xs, fb) = fmupd i (fmap_of_list xs, fb)"

subsection‹Test Setup›

definition(in statement_with_gas) eval::"Gas ⇒ S ⇒ Address ⇒ Identifier ⇒ Address ⇒ Valuetype ⇒ (Address × Balance × atype × nat) list
⇒ (String.literal × Type × Data⇩E⇩n⇩v⇩i⇩r⇩o⇩n⇩m⇩e⇩n⇩t) list
⇒ String.literal"
where "eval g stm addr name adest aval acc dat
= (let (k,c,m,s,e) = foldl loadsimple⇩E⇩n⇩v⇩i⇩r⇩o⇩n⇩m⇩e⇩n⇩t (emptyStore, emptyStore, emptyStore, fmempty, emptyEnv addr name adest aval) dat;
a         = init⇩A⇩c⇩c⇩o⇩u⇩n⇩t acc;
s'        = emptyStorage (addr := s);
z         = ⦇accounts=a,stack=k,memory=m,storage=s',gas=g⦈
in (
case (stmt stm e c z) of
Normal ((), z') ⇒ (dump⇩E⇩n⇩v⇩i⇩r⇩o⇩n⇩m⇩e⇩n⇩t (stack z') c (memory z') (storage z' addr) e (map (λ (a,b,c). a) dat))
+ (dump⇩A⇩c⇩c⇩o⇩u⇩n⇩t⇩s ep z' (map fst acc))
| Exception Err   ⇒ STR ''Exception''
| Exception Gas   ⇒ STR ''OutOfGas''))"

global_interpretation soliditytest0: statement_with_gas costs_ex "fmap_of_list []" costs_min
defines stmt0 = "soliditytest0.stmt"
and lexp0 = soliditytest0.lexp
and expr0 = soliditytest0.expr
and ssel0 = soliditytest0.ssel
and rexp0 = soliditytest0.rexp
and msel0 = soliditytest0.msel
and load0 = soliditytest0.load
and eval0 = soliditytest0.eval
by unfold_locales auto

lemma "eval0 1000
SKIP
(STR ''089Be5381FcEa58aF334101414c04F993947C733'')
EMPTY
EMPTY
(STR ''0'')
[(STR ''089Be5381FcEa58aF334101414c04F993947C733'', STR ''100'', EOA, 0), (STR ''115f6e2F70210C14f7DB1AC69737a3CC78435d49'', STR ''100'', EOA, 0)]
[(STR ''v1'', (Value TBool, Stackbool True))]
= STR ''v1==true⏎089Be5381FcEa58aF334101414c04F993947C733: balance==100 - EOA⏎115f6e2F70210C14f7DB1AC69737a3CC78435d49: balance==100 - EOA''"
by(eval)

lemma "eval0 1000
SKIP
(STR ''089Be5381FcEa58aF334101414c04F993947C733'')
EMPTY
EMPTY
(STR ''0'')
[(STR ''089Be5381FcEa58aF334101414c04F993947C733'', STR ''100'', EOA, 0), (STR ''115f6e2F70210C14f7DB1AC69737a3CC78435d49'', STR ''100'', EOA, 0)]
[(STR ''v1'',(Memory (MTArray 5 (MTValue TBool)), Memarr [MBool True, MBool False, MBool True, MBool False, MBool True]))]
= STR ''v1[0]==true⏎v1[1]==false⏎v1[2]==true⏎v1[3]==false⏎v1[4]==true⏎089Be5381FcEa58aF334101414c04F993947C733: balance==100 - EOA⏎115f6e2F70210C14f7DB1AC69737a3CC78435d49: balance==100 - EOA''"
by(eval)

lemma "eval0 1000
(ITE FALSE (ASSIGN (Id (STR ''x'')) TRUE) (ASSIGN (Id (STR ''y'')) TRUE))
(STR ''089Be5381FcEa58aF334101414c04F993947C733'')
EMPTY
EMPTY
(STR ''0'')
[(STR ''089Be5381FcEa58aF334101414c04F993947C733'', STR ''100'', EOA, 0), (STR ''115f6e2F70210C14f7DB1AC69737a3CC78435d49'', STR ''100'', EOA, 0)]
[(STR ''x'', (Value TBool, Stackbool False)), (STR ''y'', (Value TBool, Stackbool False))]
= STR ''y==true⏎x==false⏎089Be5381FcEa58aF334101414c04F993947C733: balance==100 - EOA⏎115f6e2F70210C14f7DB1AC69737a3CC78435d49: balance==100 - EOA''"
by(eval)

lemma "eval0 1000
(BLOCK ((STR ''v2'', Value TBool), None) (ASSIGN (Id (STR ''v1'')) (LVAL (Id (STR ''v2'')))))
(STR ''089Be5381FcEa58aF334101414c04F993947C733'')
EMPTY
EMPTY
(STR ''0'')
[(STR ''089Be5381FcEa58aF334101414c04F993947C733'', STR ''100'', EOA, 0), (STR ''115f6e2F70210C14f7DB1AC69737a3CC78435d49'', STR ''100'', EOA, 0)]
[(STR ''v1'', (Value TBool, Stackbool True))]
= STR ''v1==false⏎089Be5381FcEa58aF334101414c04F993947C733: balance==100 - EOA⏎115f6e2F70210C14f7DB1AC69737a3CC78435d49: balance==100 - EOA''"
by(eval)

lemma "eval0 1000
(ASSIGN (Id (STR ''a_s120_21_m8'')) (LVAL (Id (STR ''a_s120_21_s8''))))
(STR ''089Be5381FcEa58aF334101414c04F993947C733'')
EMPTY
EMPTY
(STR ''0'')
[(STR ''089Be5381FcEa58aF334101414c04F993947C733'', STR ''100'', EOA, 0)]
[((STR ''a_s120_21_s8''), Storage (STArray 1 (STArray 2 (STValue (TSInt 120)))), Stoarr [SArray [SInt 347104507864064359095275590289383142, SInt 565831699297331399489670920129618233]]),
((STR ''a_s120_21_m8''), Memory (MTArray 1 (MTArray 2 (MTValue (TSInt 120)))), Memarr [MArray [MInt (290845675805142398428016622247257774), MInt ((-96834026877269277170645294669272226))]])]
= STR ''a_s120_21_m8[0][0]==347104507864064359095275590289383142⏎a_s120_21_m8[0][1]==565831699297331399489670920129618233⏎a_s120_21_s8[0][0]==347104507864064359095275590289383142⏎a_s120_21_s8[0][1]==565831699297331399489670920129618233⏎089Be5381FcEa58aF334101414c04F993947C733: balance==100 - EOA''"
by(eval)

lemma "eval0 1000
(ASSIGN (Ref (STR ''a_s8_32_m0'') [UINT 8 1]) (LVAL (Ref (STR ''a_s8_31_s7'') [UINT 8 0])))
(STR ''089Be5381FcEa58aF334101414c04F993947C733'')
EMPTY
EMPTY
(STR ''0'')
[(STR ''089Be5381FcEa58aF334101414c04F993947C733'', STR ''100'', EOA, 0)]
[(STR ''a_s8_31_s7'', (Storage (STArray 1 (STArray 3 (STValue (TSInt 8)))), Stoarr [SArray [SInt ((98)), SInt ((-23)), SInt (36)]])),
(STR ''a_s8_32_m0'', (Memory (MTArray 2 (MTArray 3 (MTValue (TSInt 8)))), Memarr [MArray [MInt ((-64)), MInt ((39)), MInt ((-125))], MArray [MInt ((-32)), MInt ((-82)), MInt ((-105))]]))]
= STR ''a_s8_32_m0[0][0]==-64⏎a_s8_32_m0[0][1]==39⏎a_s8_32_m0[0][2]==-125⏎a_s8_32_m0[1][0]==98⏎a_s8_32_m0[1][1]==-23⏎a_s8_32_m0[1][2]==36⏎a_s8_31_s7[0][0]==98⏎a_s8_31_s7[0][1]==-23⏎a_s8_31_s7[0][2]==36⏎089Be5381FcEa58aF334101414c04F993947C733: balance==100 - EOA''"
by(eval)

lemma "eval0 1000
SKIP
(STR ''089Be5381FcEa58aF334101414c04F993947C733'')
EMPTY
EMPTY
(STR ''0'')
[(STR ''089Be5381FcEa58aF334101414c04F993947C733'', STR ''100'', EOA, 0), (STR ''115f6e2F70210C14f7DB1AC69737a3CC78435d49'', STR ''100'', EOA, 0)]
[(STR ''v1'', (Storage (STMap (TUInt 32) (STValue (TUInt 8))), Stomap [(STR ''2129136830'', SInt (247))]))]
= STR ''v1[2129136830]==247⏎089Be5381FcEa58aF334101414c04F993947C733: balance==100 - EOA⏎115f6e2F70210C14f7DB1AC69737a3CC78435d49: balance==100 - EOA''"
by(eval)

definition "testenv1 ≡ loadProc (STR ''mycontract'')
([(STR ''v1'', Var (STValue TBool)),
(STR ''m1'', Method ([], True, (ASSIGN (Id (STR ''v1'')) FALSE)))],
([], SKIP),
SKIP)
fmempty"

global_interpretation soliditytest1: statement_with_gas costs_ex testenv1 costs_min
defines stmt1 = "soliditytest1.stmt"
and lexp1 = soliditytest1.lexp
and expr1 = soliditytest1.expr
and ssel1 = soliditytest1.ssel
and rexp1 = soliditytest1.rexp
and msel1 = soliditytest1.msel
and load1 = soliditytest1.load
and eval1 = soliditytest1.eval
by unfold_locales auto

lemma "eval1 1000
(EXTERNAL (ADDRESS (STR ''myaddr'')) (STR ''m1'') [] (UINT 256 0))
(STR ''local'')
EMPTY
(STR ''mycontract'')
(STR ''0'')
[(STR ''local'', STR ''100'', EOA, 0), (STR ''myaddr'', STR ''100'', Contract (STR ''mycontract''), 0)]
[]
= STR ''local: balance==100 - EOA⏎myaddr: balance==100 - mycontract(v1==false⏎)''"
by (eval)

lemma "eval1 1000
(NEW (STR ''mycontract'') [] (UINT 256 10))
(STR ''local'')
EMPTY
(STR ''mycontract'')
(STR ''0'')
[(STR ''local'', STR ''100'', EOA, 0), (STR ''myaddr'', STR ''100'', Contract (STR ''mycontract''), 0)]
[]
= STR ''local: balance==90 - EOA⏎0.local: balance==10 - mycontract()⏎myaddr: balance==100 - mycontract()''"
by eval

lemma "eval1 1000
(
COMP
(NEW (STR ''mycontract'') [] (UINT 256 10))
(EXTERNAL CONTRACTS (STR ''m1'') [] (UINT 256 0))
)
(STR ''local'')
EMPTY
(STR ''mycontract'')
(STR ''0'')
[(STR ''local'', STR ''100'', EOA, 0), (STR ''myaddr'', STR ''100'', Contract (STR ''mycontract''), 0)]
[]
= STR ''local: balance==90 - EOA⏎0.local: balance==10 - mycontract(v1==false⏎)⏎myaddr: balance==100 - mycontract()''"
by eval

definition "testenv2 ≡ loadProc (STR ''mycontract'')
([(STR ''m1'', Function ([], False, UINT 8 5))],
([], SKIP),
SKIP)
fmempty"

```