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 dumpValuetypes::"Types  Valuetype  String.literal" where
   "dumpValuetypes (TSInt _) n = n"
 | "dumpValuetypes (TUInt _) n = n"
 | "dumpValuetypes TBool b = (if b = (STR ''True'') then  STR ''true'' else STR ''false'')"
 | "dumpValuetypes TAddr ad = ad"

subsubsection‹Memory›

datatype DataMemory = MArray "DataMemory list"
                   | MBool bool
                   | MInt int
                   | MAddress Address

fun loadRecMemory :: "Location  DataMemory  MemoryT  MemoryT" and
        iterateM :: "Location  MemoryT × nat  DataMemory  MemoryT × nat" where
  "loadRecMemory loc (MArray dat) mem = fst (foldl (iterateM loc) (updateStore loc (MPointer loc) mem,0) dat)"
| "loadRecMemory loc (MBool b) mem = updateStore loc ((MValue  ShowLbool) b) mem "
| "loadRecMemory loc (MInt i) mem = updateStore loc ((MValue  ShowLint) i) mem "
| "loadRecMemory loc (MAddress ad) mem = updateStore loc (MValue ad) mem"
| "iterateM loc (mem,x) d = (loadRecMemory (hash loc (ShowLnat x)) d mem, Suc x)"

definition loadMemory :: "DataMemory list  MemoryT  MemoryT" where
"loadMemory dat mem = (let loc   = ShowLnat (toploc mem);
                         (m, _) = foldl (iterateM loc) (mem, 0) dat
                       in (snd  allocate) m)"
                          
fun dumprecMemory:: "Location  MTypes  MemoryT  String.literal  String.literal  String.literal" where
"dumprecMemory loc tp mem ls str =
  (case accessStore loc mem of
    Some (MPointer l) 
      (case tp of
        (MTArray x t)  iter (λi str' . dumprecMemory ((hash l o ShowLint) i) t mem 
                              (ls + (STR ''['') + (ShowLint i) + (STR '']'')) str') str x
                  | _  FAILURE)
  | Some (MValue v) 
      (case tp of
        MTValue t  str + ls + (STR ''=='') + dumpValuetypes t v + (STR ''⏎'')
              | _  FAILURE)
  | None  FAILURE)"

definition dumpMemory :: "Location  int  MTypes  MemoryT  String.literal String.literal String.literal" where
"dumpMemory loc x t mem ls str = iter (λi. dumprecMemory ((hash loc (ShowLint i))) t mem (ls + STR ''['' + (ShowLint i + STR '']''))) str x"

subsubsection‹Storage›

datatype DataStorage =
    SArray "DataStorage list"
  | SMap "(String.literal × DataStorage) list"
  | SBool bool
  | SInt int
  | SAddress Address

fun goStorage :: "Location  (String.literal ×  STypes)  (String.literal × STypes)" where
  "goStorage l (s, STArray _ t) = (s + (STR ''['') + (convert l) + (STR '']''), t)"
| "goStorage l (s, STMap _ t) = (s + (STR ''['') + (convert l) + (STR '']''), t)"
| "goStorage l (s, STValue t) = (s + (STR ''['') + (convert l) + (STR '']''), STValue t)"

fun dumpSingleStorage :: "StorageT  String.literal  STypes  (Location × Location)  String.literal  String.literal" where
"dumpSingleStorage sto id' tp (loc,l) str =
    (case foldr goStorage (tolist loc) (str + id', tp) of
      (s, STValue t) 
        (case sto $$ (loc + l) of
           Some v  s + (STR ''=='') + dumpValuetypes t v
         | None  FAILURE)
     | _  FAILURE)"

definition iterate where
"iterate loc t id' sto s l = dumpSingleStorage sto id' t (splitAt (length (String.explode l) - length (String.explode loc) - 1) l) s + (STR ''⏎'')"

fun dumpStorage ::  "StorageT  Location  String.literal  STypes  String.literal  String.literal" where
  "dumpStorage sto loc id' (STArray _ t) str = foldl (iterate loc t id' sto) str (locations_map loc sto)"
| "dumpStorage sto loc id' (STMap _ t) str = foldl (iterate loc t id' sto) str (locations_map loc sto)"
| "dumpStorage sto loc id' (STValue t) str =
    (case sto $$ loc of
      Some v  str + id' + (STR ''=='') + dumpValuetypes t v + (STR ''⏎'')
    | _  str)"

fun loadRecStorage :: "Location  DataStorage  StorageT  StorageT" and
    iterateSA :: "Location  StorageT × nat  DataStorage  StorageT × nat" and
    iterateSM :: "Location  String.literal × DataStorage  StorageT  StorageT" where
  "loadRecStorage loc (SArray dat) sto = fst (foldl (iterateSA loc) (sto,0) dat)"
| "loadRecStorage loc (SMap dat) sto  = foldr (iterateSM loc) dat sto"
| "loadRecStorage loc (SBool b) sto = fmupd loc (ShowLbool b) sto"
| "loadRecStorage loc (SInt i)  sto = fmupd loc (ShowLint i) sto"
| "loadRecStorage loc (SAddress ad) sto = fmupd loc ad sto"
| "iterateSA loc (s', x) d = (loadRecStorage (hash loc (ShowLnat x)) d s', Suc x)"
| "iterateSM loc (k, v) s' = loadRecStorage (hash loc k) v s'"

subsubsection‹Environment›

datatype DataEnvironment =
    Memarr "DataMemory list" |
    CDarr "DataMemory list" |
    Stoarr "DataStorage list"|
    Stomap "(String.literal × DataStorage) 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 loadsimpleEnvironment :: "(Stack × CalldataT × MemoryT × StorageT × Environment) 
                     (Identifier × Type × DataEnvironment)  (Stack × CalldataT × MemoryT × StorageT × Environment)"
  where
"loadsimpleEnvironment (k, c, m, s, e) (id', tp, d) = (case d of
    Stackbool b 
        let (k', e') = astack id' tp (KValue (ShowLbool b)) (k, e)
        in (k', c, m, s, e')
  | Stobool b 
        let (s', e') = astore id' tp (ShowLbool b) (s, e)
        in (k, c, m, s', e')
  |  Stackint n 
        let (k', e') = astack id' tp (KValue (ShowLint n)) (k, e)
        in (k', c, m, s, e')
  |  Stoint n 
        let (s', e') = astore id' tp (ShowLint 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 = ShowLnat (toploc c);
            c' = loadMemory a c;
            (k', e') = astack id' tp (KCDptr l) (k, e)
        in (k', c', m, s, e')
  |  Memarr a 
        let l = ShowLnat (toploc m);
            m' = loadMemory a m;
            (k', e') = astack id' tp (KMemptr l) (k, e)
        in (k', c, m', s, e')
  |  Stoarr a 
        let s' = loadRecStorage id' (SArray a) s;
            e' = updateEnv id' tp (Storeloc id') e
        in (k, c, m, s', e')
  |  Stomap mp 
        let s' = loadRecStorage id' (SMap mp) s;
            e' = updateEnv id' tp (Storeloc id') e
        in (k, c, m, s', e')
)"

definition getValueEnvironment :: "Stack  CalldataT  MemoryT  StorageT  Environment  Identifier  String.literal  String.literal"
  where 
"getValueEnvironment 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 ''=='') + dumpValuetypes t v + (STR ''⏎''))
          |  _  FAILURE)
      | Some (KCDptr p)  (case tp of
            Calldata (MTArray x t)  dumpMemory p x t c i txt
            | _  FAILURE)
      | Some (KMemptr p)  (case tp of
            Memory (MTArray x t)  dumpMemory p x t m i txt
            | _  FAILURE)
      | Some (KStoptr p)  (case tp of
            Storage t  dumpStorage s p i t txt
            | _  FAILURE))
   | Some (Storage t, Storeloc l)  dumpStorage s l i t txt
   | _  FAILURE
)"

definition dumpEnvironment :: "Stack   CalldataT  MemoryT  StorageT  Environment  Identifier list  String.literal" 
  where "dumpEnvironment k c m s e sl = foldr (getValueEnvironment k c m s e) sl EMPTY"

subsubsection‹Accounts›

fun loadAccounts :: "Accounts  (Address × Balance × atype × nat) list  Accounts" where 
   "loadAccounts acc []             = acc"
 | "loadAccounts acc ((ad, b, t, c)#as) = loadAccounts (acc (ad:=bal=b, type=Some t, contracts=c)) as"

fun dumpStorage::"StorageT  (Identifier × Member)  String.literal" where
  "dumpStorage s (i, Var x) = dumpStorage s i i x EMPTY"
| "dumpStorage s (i, Function x) = FAILURE"
| "dumpStorage s (i, Method x) = FAILURE"

fun dumpMembers :: "atype option  EnvironmentP  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 dumpAccount :: "nat  EnvironmentP  State  Address  String.literal"
  where "dumpAccount 0 _ _ _ = FAILURE"
  | "dumpAccount (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 ''⏎'' + dumpAccount c ep st (hash a (ShowLint x))) EMPTY (int (contracts (accounts st a)))"

definition dumpAccounts :: "EnvironmentP  State  Address list  String.literal"
  where "dumpAccounts ep st al = intersperse (STR ''⏎'') (map (dumpAccount 1000 ep st) al)"

definition initAccount::"(Address × Balance × atype × nat) list => Accounts" where 
  "initAccount = loadAccounts emptyAccount"

type_synonym DataP = "(Identifier × Member) list × ((Identifier × Type) list × S) × S"

fun loadProc::"Identifier  DataP  EnvironmentP  EnvironmentP"
  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 × DataEnvironment) list
           String.literal"
  where "eval g stm addr name adest aval acc dat
        = (let (k,c,m,s,e) = foldl loadsimpleEnvironment (emptyStore, emptyStore, emptyStore, fmempty, emptyEnv addr name adest aval) dat;
               a         = initAccount 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')  (dumpEnvironment (stack z') c (memory z') (storage z' addr) e (map (λ (a,b,c). a) dat))
                             + (dumpAccounts 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"