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

subsection‹Code Generator Setup and Local Tests›


subsubsection‹Utils›

definition FAILURE::"String.literal" where "FAILURE = STR ''Failure''"
definition "inta_of_int = int o nat_of_integer"
definition "nat_of_int  = nat_of_integer"

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))"

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"

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)


subsubsection‹Load: Accounts›

fun loadAccounts :: "Accounts ⇒ (Address × Balance) list ⇒ Accounts" where 
   "loadAccounts acc []             = acc"
 | "loadAccounts acc ((ad, bal)#as) = loadAccounts (updateBalance ad bal acc) as"

definition dumpAccounts :: "Accounts ⇒ Address list ⇒ String.literal"
where
  "dumpAccounts acc = foldl (λ t a . String.implode (    (String.explode t) 
                                                     @ (String.explode a) 
                                                     @ ''.balance'' 
                                                     @ ''=='' 
                                                     @ String.explode (accessBalance acc a) 
                                                     @ ''⏎'')) 
                          (STR '''')"

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


subsubsection‹Load: Store›

type_synonym DataStore = "(Location × String.literal) list"

fun showStore::"'a Store ⇒ 'a fset" where
    "showStore s = (fmran (mapping s))"

subsubsection‹Load: Memory›

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

fun 
 loadRecMemory :: "Location ⇒ DataMemory ⇒ MemoryT ⇒ MemoryT" where
"loadRecMemory loc (MArray dat) mem = 
(fst (foldl (λ S d . let (s',x) = S in  (loadRecMemory (hash loc (ShowLnat x)) d s', Suc x)) (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"

definition loadMemory :: "DataMemory list ⇒ MemoryT ⇒ MemoryT" where
"loadMemory dat mem = (let l     = ShowLnat (toploc mem);
                         (m, _) = foldl (λ (m',x) d . (loadRecMemory (((hash l) ∘ ShowLnat) x) d m', Suc x)) (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

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)"

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 fmlookup sto (loc + l) of
            Some v ⇒ s + (STR ''=='') + dumpValuetypes t v
           | None ⇒ FAILURE)
        | _ ⇒ FAILURE)"

                            
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"

fun dumpStorage ::  "StorageT ⇒ Location ⇒ String.literal ⇒ STypes ⇒ String.literal ⇒ String.literal"
where
"dumpStorage sto loc id' (STArray _ t) str = foldl 
      (λ s l . dumpSingleStorage sto id' t ((splitAt (length (String.explode l) - length (String.explode loc) - 1) l)) s 
           + (STR ''⏎'')) str (locations_map loc sto)"
| "dumpStorage sto loc id' (STMap _ t) str = 
   foldl (λ s l . dumpSingleStorage sto id' t (splitAt (length (String.explode l) - length (String.explode loc) - 1) l) s + (STR ''⏎'')) str 
(locations_map loc sto)"
  | "dumpStorage sto loc id' (STValue t) str = (case fmlookup sto loc of
      Some v ⇒ str + id' + (STR ''=='') + dumpValuetypes t v + (STR ''⏎'')
    | _ ⇒ str)"


fun loadRecStorage :: "Location ⇒ DataStorage ⇒ StorageT ⇒ StorageT" where
"loadRecStorage loc (SArray dat) sto = fst (foldl (λ S d . let (s', x) = S in (loadRecStorage (hash loc (ShowLnat x)) d s', Suc x)) (sto,0) dat)"
| "loadRecStorage loc (SMap dat) sto  = ( foldr (λ (k, v) s'. loadRecStorage (hash loc k) v s') 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"

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 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 loadEnvironment::"(Stack × CalldataT × MemoryT × StorageT × Environment) ⇒ (Identifier × Type × DataEnvironment) list
                       ⇒ (Stack × CalldataT × MemoryT × StorageT × Environment)"
  where
"loadEnvironment = foldl loadsimpleEnvironment"

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
)"

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

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  (STR '''')"

fun loadProc::"EnvironmentP ⇒ DataP ⇒ EnvironmentP"
  where "loadProc eP (ad, (xs, fb)) = fmupd ad (fmap_of_list xs, fb) eP"

fun initStorage::"(Address × Balance) list ⇒ (Address, StorageT) fmap ⇒ (Address, StorageT) fmap"
  where "initStorage [] m = m"
  | "initStorage (x # xs) m = fmupd (fst x) (fmempty) m"

subsection‹Test Setup›

definition eval::"Gas ⇒ (S ⇒ EnvironmentP ⇒ Environment ⇒ CalldataT ⇒ (unit, Ex, State) state_monad)
                 ⇒ S ⇒ Address ⇒ Address ⇒ Valuetype ⇒ (Address × Balance) list 
                 ⇒ DataP list
                 ⇒ (String.literal × Type × DataEnvironment) list
          ⇒ String.literal"
  where "eval g stmteval stm addr adest aval acc d dat
        = (let (k,c,m,s,e) = loadEnvironment (emptyStore, emptyStore, emptyStore, fmempty, emptyEnv addr adest aval) dat;
               ep        = foldl loadProc fmempty d;
               a         = initAccount acc;
               s'        = fmupd addr s (initStorage acc fmempty);
               z         = ⦇accounts=a,stack=k,memory=m,storage=s',gas=g⦈ 
           in (
             case (stmteval stm ep e c z) of
              Normal ((), z') ⇒ (dumpEnvironment (stack z') c (memory z') (the (fmlookup (storage z') addr)) e (map (λ (a,b,c). a) dat))
                             + (dumpAccounts (accounts z') (map fst acc))
             | Exception Err   ⇒ STR ''Exception''
             | Exception Gas   ⇒ STR ''OutOfGas''))"

value "eval 1
            stmt
            SKIP 
            (STR ''089Be5381FcEa58aF334101414c04F993947C733'')
            (STR '''')
            (STR ''0'')
            [(STR ''089Be5381FcEa58aF334101414c04F993947C733'', STR ''100''),(STR ''115f6e2F70210C14f7DB1AC69737a3CC78435d49'', STR ''100'')] 
            []
            [(STR ''v1'', (Value TBool, Stackbool True))]"

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

value "eval 1000
            stmt
            SKIP
            (STR ''089Be5381FcEa58aF334101414c04F993947C733'')
            (STR '''')
            (STR ''0'')
            [(STR ''089Be5381FcEa58aF334101414c04F993947C733'', STR ''100''), (STR ''115f6e2F70210C14f7DB1AC69737a3CC78435d49'', STR ''100'')] 
            []
            [(STR ''v1'', (Storage (STArray 5 (STValue TBool)), Stoarr [SBool True, SBool False, SBool True, SBool False, SBool True]))]"


lemma "eval 1000
            stmt
            SKIP 
            (STR ''089Be5381FcEa58aF334101414c04F993947C733'')
            (STR '''')
            (STR ''0'')
            [(STR ''089Be5381FcEa58aF334101414c04F993947C733'', STR ''100''), (STR ''115f6e2F70210C14f7DB1AC69737a3CC78435d49'', STR ''100'')] 
            []
            [(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⏎115f6e2F70210C14f7DB1AC69737a3CC78435d49.balance==100⏎''"
  by(eval)

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

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

lemma "eval 1000
            stmt
            (ASSIGN (Id (STR ''a_s120_21_m8'')) (LVAL (Id (STR ''a_s120_21_s8''))))
            (STR ''089Be5381FcEa58aF334101414c04F993947C733'')
            (STR '''')
            (STR ''0'')
            [(STR ''089Be5381FcEa58aF334101414c04F993947C733'', STR ''100'')]
            []
            [((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⏎''"
  by(eval)

lemma "eval 1000
            stmt
            (ASSIGN (Ref (STR ''a_s8_32_m0'') [UINT 8 1]) (LVAL (Ref (STR ''a_s8_31_s7'') [UINT 8 0]))) 
            (STR ''089Be5381FcEa58aF334101414c04F993947C733'')
            (STR '''')
            (STR ''0'')
            [(STR ''089Be5381FcEa58aF334101414c04F993947C733'', STR ''100'')]
            []
            [(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⏎''"
  by(eval)


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

value "eval 1000
            stmt
            (INVOKE (STR ''m1'') [])
            (STR ''myaddr'')
            (STR '''')
            (STR ''0'')
            [(STR ''myaddr'', STR ''100'')]
            [
              (STR ''myaddr'',
                ([(STR ''m1'', Method ([], SKIP, None))],
                SKIP))
            ]
            [(STR ''x'', (Value TBool, Stackbool True))]"

lemma "eval 1000
            stmt
            (ASSIGN (Id (STR ''v1'')) (CALL (STR ''m1'') []))
            (STR ''myaddr'')
            (STR '''')
            (STR ''0'')
            [(STR ''myaddr'', STR ''100'')]
            [
              (STR ''myaddr'',
                ([(STR ''m1'', Method ([], SKIP, Some (UINT 8 5)))],
                SKIP))
            ]
            [(STR ''v1'', (Value (TUInt 8), Stackint 0))]
      = STR ''v1==5⏎myaddr.balance==100⏎''"
  by (eval)

lemma "eval 1000
            stmt
            (ASSIGN (Id (STR ''v1'')) (CALL (STR ''m1'') [E.INT 8 3, E.INT 8 4]))
            (STR ''myaddr'')
            (STR '''')
            (STR ''0'')
            [(STR ''myaddr'', STR ''100'')]
            [
              (STR ''myaddr'',
                ([(STR ''m1'', Method ([(STR ''v2'', Value (TSInt 8)), (STR ''v3'', Value (TSInt 8))], SKIP, Some (PLUS (LVAL (Id (STR ''v2''))) (LVAL (Id (STR ''v3''))))))],
                SKIP))
            ]
            [(STR ''v1'', (Value (TSInt 8), Stackint 0))]
      = STR ''v1==7⏎myaddr.balance==100⏎''"
  by (eval)

lemma "eval 1000
            stmt
            (ASSIGN (Id (STR ''v1'')) (ECALL (ADDRESS (STR ''extaddr'')) (STR ''m1'') [E.INT 8 3, E.INT 8 4] (E.UINT 8 0)))
            (STR ''myaddr'')
            (STR '''')
            (STR ''0'')
            [(STR ''myaddr'', STR ''100'')]
            [
              (STR ''extaddr'',
                ([(STR ''m1'', Method ([(STR ''v2'', Value (TSInt 8)), (STR ''v3'', Value (TSInt 8))], SKIP, Some (PLUS (LVAL (Id (STR ''v2''))) (LVAL (Id (STR ''v3''))))))],
                SKIP))
            ]
            [(STR ''v1'', (Value (TSInt 8), Stackint 0))]
       = STR ''v1==7⏎myaddr.balance==100⏎''"
  by (eval)

lemma "eval 1000
            stmt
            (TRANSFER (ADDRESS (STR ''myaddr'')) (UINT 256 10))
            (STR ''089Be5381FcEa58aF334101414c04F993947C733'') 
            (STR '''')
            (STR ''0'')
            [(STR ''089Be5381FcEa58aF334101414c04F993947C733'', STR ''100''), (STR ''0x2d5F6f401c770eEAdd68deB348948ed4504c4676'', STR ''100'')] 
            [
              (STR ''myaddr'',
                ([], SKIP))
            ]
            []
      = STR ''089Be5381FcEa58aF334101414c04F993947C733.balance==90⏎0x2d5F6f401c770eEAdd68deB348948ed4504c4676.balance==100⏎''"
  by (eval)

value "eval 1000
            stmt
            (TRANSFER (ADDRESS (STR ''myaddr'')) (UINT 256 10))
            (STR ''089Be5381FcEa58aF334101414c04F993947C733'') 
            (STR '''')
            (STR ''0'')
            [(STR ''089Be5381FcEa58aF334101414c04F993947C733'', STR ''100''), (STR ''0x2d5F6f401c770eEAdd68deB348948ed4504c4676'', STR ''100'')] 
            [
              (STR ''myaddr'',
                ([], SKIP))
            ]
            []"

lemma "eval 1000
            stmt
            (COMP(COMP(((ASSIGN (Id (STR ''x''))  (E.UINT 8 0))))(TRANSFER (ADDRESS (STR ''myaddr'')) (UINT 256 5)))(SKIP))
            (STR ''089Be5381FcEa58aF334101414c04F993947C733'')
            (STR '''')
            (STR ''0'')
            [(STR ''089Be5381FcEa58aF334101414c04F993947C733'', STR ''100''), (STR ''115f6e2F70210C14f7DB1AC69737a3CC78435d49'', STR ''100'')]
            [
              (STR ''myaddr'',
                ([], SKIP))
            ]
            [(STR ''x'', (Value (TUInt 8), Stackint 9))]
      = STR ''x==0⏎089Be5381FcEa58aF334101414c04F993947C733.balance==95⏎115f6e2F70210C14f7DB1AC69737a3CC78435d49.balance==100⏎''"
  by (eval)

value "eval 1000
            stmt
            (EXTERNAL (ADDRESS (STR ''Victim'')) (STR ''withdraw'') [] (E.UINT 8 0))
            (STR ''Victim'')
            (STR '''')
            (STR ''0'')
            [(STR ''Victim'', STR ''100''), (STR ''Attacker'', STR ''100'')]
            [
              (STR ''Attacker'',
                [(STR ''withdraw'', Method ([], EXTERNAL (ADDRESS (STR ''Victim'')) (STR ''withdraw'') [] (E.UINT 8 0), None))],
                SKIP),
              (STR ''Victim'',
                [(STR ''withdraw'', Method ([], EXTERNAL (ADDRESS (STR ''Attacker'')) (STR ''withdraw'') [] (E.UINT 8 0), None))],
                SKIP)
            ]
            []"

value "eval 1000
            stmt
            (INVOKE (STR ''withdraw'') [])
            (STR ''Victim'')
            (STR '''')
            (STR ''0'')
            [(STR ''Victim'', STR ''100''), (STR ''Attacker'', STR ''100'')]
            [
              (STR ''Victim'',
                [(STR ''withdraw'', Method ([], INVOKE (STR ''withdraw'') [], None))],
                SKIP)
            ]
            []"

subsection‹The Final Code Export›

consts ReadLS   :: "String.literal ⇒ S"
consts ReadLacc :: "String.literal ⇒ (String.literal × String.literal) 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 [credit, stm, saddr, raddr, val, acc, pr, dat]
        = (0, eval (ReadLnat credit) stmt (ReadLS stm) saddr raddr val (ReadLacc acc) (ReadLP pr) (ReadLdat dat))"
 | "main_stub [stm, saddr, raddr, val, acc, pr, dat]
        = (0, eval 1000 stmt (ReadLS stm) saddr raddr val (ReadLacc acc) (ReadLP pr) (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 eval SKIP main_stub
            in Haskell module_name "Solidity_Evaluator" file_prefix "solidity-evaluator/src"  (string_classes)   

subsection‹Demonstrating the Symbolic Execution of Solidity›

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'') (STR ''ad'') (STR ''0'')))"
 
abbreviation mystack::Stack
  where "mystack ≡ updateStore (STR ''1'') (KMemptr (STR ''1'')) emptyStore"
 
abbreviation mystore::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"


lemma "( stmt P1 fmempty myenv emptyStore ⦇accounts=emptyAccount, stack=mystack, memory=mymemory, storage=fmupd (STR ''ad'') mystorage fmempty, gas=1000⦈ ) =
  (Normal ((), ⦇accounts=emptyAccount, stack=mystack, memory=mymemory, storage=fmupd (STR ''ad'') mystorage fmempty, gas=1000⦈ ))"
  by(solidity_symbex)

end