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"

global_interpretation soliditytest2: statement_with_gas costs_ex testenv2 costs_min
  defines stmt2 = "soliditytest2.stmt"
      and lexp2 = soliditytest2.lexp 
      and expr2 = soliditytest2.expr
      and ssel2 = soliditytest2.ssel
      and rexp2 = soliditytest2.rexp
      and msel2 = soliditytest2.msel
      and load2 = soliditytest2.load
      and eval2 = soliditytest2.eval
  by unfold_locales auto

lemma "eval2 1000
            (ASSIGN (Id (STR ''v1'')) (CALL (STR ''m1'') []))
            (STR ''myaddr'')
            (STR ''mycontract'')
            EMPTY
            (STR ''0'')
            [(STR ''myaddr'', STR ''100'', EOA, 0)]
            [(STR ''v1'', (Value (TUInt 8), Stackint 0))]
       = STR ''v1==5⏎myaddr: balance==100 - EOA''"
  by (eval)

definition "testenv3 ≡ loadProc (STR ''mycontract'')
              ([(STR ''m1'',
                Function ([(STR ''v2'', Value (TSInt 8)), (STR ''v3'', Value (TSInt 8))],
                False,
                PLUS (LVAL (Id (STR ''v2''))) (LVAL (Id (STR ''v3'')))))],
                ([], SKIP),
              SKIP)
            fmempty"

global_interpretation soliditytest3: statement_with_gas costs_ex testenv3 costs_min
  defines stmt3 = "soliditytest3.stmt"
      and lexp3 = soliditytest3.lexp 
      and expr3 = soliditytest3.expr
      and ssel3 = soliditytest3.ssel
      and rexp3 = soliditytest3.rexp
      and msel3 = soliditytest3.msel
      and load3 = soliditytest3.load
      and eval3 = soliditytest3.eval
  by unfold_locales auto

lemma "eval3 1000
            (ASSIGN (Id (STR ''v1'')) (CALL (STR ''m1'') [E.INT 8 3, E.INT 8 4]))
            (STR ''myaddr'')
            (STR ''mycontract'')
            EMPTY
            (STR ''0'')
            [(STR ''myaddr'', STR ''100'', EOA, 0),(STR ''mya'', STR ''100'', EOA, 0)]
            [(STR ''v1'', (Value (TSInt 8), Stackint 0))]
       = STR ''v1==7⏎myaddr: balance==100 - EOA⏎mya: balance==100 - EOA''"
  by (eval)

definition "testenv4 ≡ loadProc (STR ''mycontract'')
              ([(STR ''m1'', Function ([(STR ''v2'', Value (TSInt 8)), (STR ''v3'', Value (TSInt 8))], True, PLUS (LVAL (Id (STR ''v2''))) (LVAL (Id (STR ''v3'')))))],
                ([], SKIP),
                SKIP)
            fmempty"

global_interpretation soliditytest4: statement_with_gas costs_ex testenv4 costs_min
  defines stmt4 = "soliditytest4.stmt"
      and lexp4 = soliditytest4.lexp 
      and expr4 = soliditytest4.expr
      and ssel4 = soliditytest4.ssel
      and rexp4 = soliditytest4.rexp
      and msel4 = soliditytest4.msel
      and load4 = soliditytest4.load
      and eval4 = soliditytest4.eval
  by unfold_locales auto

lemma "eval4 1000
            (ASSIGN (Id (STR ''v1'')) (ECALL (ADDRESS (STR ''extaddr'')) (STR ''m1'') [E.INT 8 3, E.INT 8 4]))
            (STR ''myaddr'')
            EMPTY
            EMPTY
            (STR ''0'')
            [(STR ''myaddr'', STR ''100'', EOA, 0), (STR ''extaddr'', STR ''100'', Contract (STR ''mycontract''), 0)]
            [(STR ''v1'', (Value (TSInt 8), Stackint 0))]
       = STR ''v1==7⏎myaddr: balance==100 - EOA⏎extaddr: balance==100 - mycontract()''"
  by (eval)

definition "testenv5 ≡ loadProc (STR ''mycontract'')
              ([], ([], SKIP), SKIP)
            fmempty"

global_interpretation soliditytest5: statement_with_gas costs_ex testenv5 costs_min
  defines stmt5 = "soliditytest5.stmt"
      and lexp5 = soliditytest5.lexp 
      and expr5 = soliditytest5.expr
      and ssel5 = soliditytest5.ssel
      and rexp5 = soliditytest5.rexp
      and msel5 = soliditytest5.msel
      and load5 = soliditytest5.load
      and eval5 = soliditytest5.eval
  by unfold_locales auto

lemma "eval5 1000
            (TRANSFER (ADDRESS (STR ''myaddr'')) (UINT 256 10))
            (STR ''089Be5381FcEa58aF334101414c04F993947C733'') 
            EMPTY
            EMPTY
            (STR ''0'')
            [(STR ''089Be5381FcEa58aF334101414c04F993947C733'', STR ''100'', EOA, 0), (STR ''myaddr'', STR ''100'', Contract (STR ''mycontract''), 0)] 
            []
       = STR ''089Be5381FcEa58aF334101414c04F993947C733: balance==90 - EOA⏎myaddr: balance==110 - mycontract()''"
  by (eval)

definition "testenv6 ≡ loadProc (STR ''Receiver'')
              ([(STR ''hello'', Var (STValue TBool))],
              ([], SKIP),
              ASSIGN (Id (STR ''hello'')) TRUE)
            fmempty"

global_interpretation soliditytest6: statement_with_gas costs_ex testenv6 costs_min
  defines stmt6 = "soliditytest6.stmt"
      and lexp6 = soliditytest6.lexp 
      and expr6 = soliditytest6.expr
      and ssel6 = soliditytest6.ssel
      and rexp6 = soliditytest6.rexp
      and msel6 = soliditytest6.msel
      and load6 = soliditytest6.load
      and eval6 = soliditytest6.eval
  by unfold_locales auto

lemma "eval6 1000
          (TRANSFER (ADDRESS (STR ''ReceiverAd'')) (UINT 256 10))
          (STR ''SenderAd'')
          EMPTY
          EMPTY
          (STR ''0'')
          [(STR ''ReceiverAd'', STR ''100'', Contract (STR ''Receiver''), 0), (STR ''SenderAd'', STR ''100'', EOA, 0)]
          []
       = STR ''ReceiverAd: balance==110 - Receiver(hello==true⏎)⏎SenderAd: balance==90 - EOA''"
  by (eval)

definition "testenv7 ≡ loadProc (STR ''mycontract'')
             ([], ([], SKIP), SKIP)
             fmempty"

global_interpretation soliditytest7: statement_with_gas costs_ex testenv7 costs_min
  defines stmt7 = "soliditytest7.stmt"
      and lexp7 = soliditytest7.lexp 
      and expr7 = soliditytest7.expr
      and ssel7 = soliditytest7.ssel
      and rexp7 = soliditytest7.rexp
      and msel7 = soliditytest7.msel
      and load7 = soliditytest7.load
      and eval7 = soliditytest7.eval
  by unfold_locales auto

lemma "eval7 1000
            (COMP(COMP(((ASSIGN (Id (STR ''x''))  (E.UINT 8 0))))(TRANSFER (ADDRESS (STR ''myaddr'')) (UINT 256 5)))(SKIP))
            (STR ''089Be5381FcEa58aF334101414c04F993947C733'')
            EMPTY
            EMPTY
            (STR ''0'')
            [(STR ''089Be5381FcEa58aF334101414c04F993947C733'', STR ''100'', EOA, 0), (STR ''myaddr'', STR ''100'', Contract (STR ''mycontract''),0)]
            [(STR ''x'', (Value (TUInt 8), Stackint 9))]
       = STR ''x==0⏎089Be5381FcEa58aF334101414c04F993947C733: balance==95 - EOA⏎myaddr: balance==105 - mycontract()''"
  by (eval)

subsection‹The Final Code Export›

consts ReadLS   :: "String.literal ⇒ S"
consts ReadLacc :: "String.literal ⇒ (String.literal × String.literal × atype × nat) list"
consts ReadLdat :: "String.literal ⇒ (String.literal × Type × DataEnvironment) list"
consts ReadLP :: "String.literal ⇒ DataP list"

code_printing 
   constant ReadLS  ⇀ (Haskell) "Prelude.read"
 | constant ReadLacc ⇀ (Haskell) "Prelude.read"
 | constant ReadLdat ⇀ (Haskell) "Prelude.read"
 | constant ReadLP ⇀ (Haskell) "Prelude.read"

fun main_stub :: "String.literal list ⇒ (int × String.literal)"
  where
   "main_stub [stm, saddr, name, raddr, val, acc, dat]
        = (0, eval0 1000 (ReadLS stm) saddr name raddr val (ReadLacc acc) (ReadLdat dat))"
 | "main_stub _ = (2, 
          STR ''solidity-evaluator [credit] \"Statement\" \"ContractAddress\" \"OriginAddress\" \"Value\"⏎''
        + STR ''  \"(Address * Balance) list\" \"(Address * ((Identifier * Member) list) * Statement)\" \"(Variable * Type * Value) list\"⏎''
        + STR ''⏎'')"

generate_file "code/solidity-evaluator/app/Main.hs" = ‹
module Main where
import System.Environment
import Solidity_Evaluator
import Prelude

main :: IO ()
main = do
  args <- getArgs
  Prelude.putStr(snd $ Solidity_Evaluator.main_stub args) 
›

export_generated_files _

export_code eval0 SKIP main_stub
            in Haskell module_name "Solidity_Evaluator" file_prefix "solidity-evaluator/src"  (string_classes)   

subsection‹Demonstrating the Symbolic Execution of Solidity›

subsubsection‹Simple Examples  › 
lemma "msel True (MTArray 5 (MTArray 6 (MTValue TBool))) (STR ''2'') [UINT 8 3] eempty emptyStore (mystate⦇gas:=1⦈) 1
= Normal ((STR ''3.2'', MTArray 6 (MTValue TBool)), 1)"  by Solidity_Symbex.solidity_symbex

lemma "msel True (MTArray 5 (MTArray 6 (MTValue TBool))) (STR ''2'') [UINT 8 3, UINT 8 4] eempty emptyStore (mystate⦇gas:=1,memory:=mymemory2⦈) 1
= Normal ((STR ''4.5'', MTValue TBool), 1)" by Solidity_Symbex.solidity_symbex

lemma "msel True (MTArray 5 (MTArray 6 (MTValue TBool))) (STR ''2'') [UINT 8 5] eempty emptyStore (mystate⦇gas:=1,memory:=mymemory2⦈) 1
= Exception (Err)" by Solidity_Symbex.solidity_symbex

subsubsection‹A More Complex Example Including Memory Copy› 

abbreviation P1::S
  where "P1 ≡ COMP (ASSIGN (Id (STR ''sa'')) (LVAL (Id (STR ''ma''))))
                   (ASSIGN (Ref (STR ''sa'') [UINT (8::nat) 0]) TRUE)"
abbreviation myenv::Environment
  where "myenv ≡ updateEnv (STR ''ma'') (Memory (MTArray 1 (MTValue TBool))) (Stackloc (STR ''1''))
                 (updateEnv (STR ''sa'') (Storage (STArray 1 (STValue TBool))) (Storeloc (STR ''1''))
                 (emptyEnv (STR ''ad'') EMPTY (STR ''ad'') (STR ''0'')))"
 
abbreviation mystack::Stack
  where "mystack ≡ updateStore (STR ''1'') (KMemptr (STR ''1'')) emptyStore"
 
abbreviation mystore::"Address ⇒ StorageT"
  where "mystore ≡ λ _ . fmempty"
 
abbreviation mymemory::MemoryT
  where "mymemory ≡ updateStore (STR ''0.1'') (MValue (STR ''False'')) emptyStore"
 
abbreviation mystorage::StorageT
  where "mystorage ≡ fmupd (STR ''0.1'') (STR ''True'') fmempty"

declare[[ML_print_depth = 10000]]
value ‹(stmt P1 myenv emptyStore ⦇accounts=emptyAccount, stack=mystack, memory=mymemory, storage=(mystore ((STR ''ad''):= mystorage)), gas=1000⦈)›  


lemma ‹(stmt P1 myenv emptyStore ⦇accounts=emptyAccount, stack=mystack, memory=mymemory, storage=(mystore ((STR ''ad''):= mystorage)), gas=1000⦈)
      = Normal ((), ⦇accounts = emptyAccount, stack = ⦇mapping = fmap_of_list [(STR ''1'', KMemptr STR ''1'')], toploc = 0⦈,
                   memory = ⦇mapping = fmap_of_list [(STR ''0.1'', MValue STR ''False'')], toploc = 0⦈, storage = (mystore ((STR ''ad''):= mystorage)), gas = 1000⦈) ›  
    by(solidity_symbex)

end