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 b8 500 = STR ''-12''" by eval

lemma "STR ''-92134039538802366542421159375273829975'' 
      = createSInt b128 45648483135649456465465452123894894554654654654654646999465"
  by eval

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

lemma "STR ''244'' = createUInt b8 500" by eval

lemma "STR ''220443428915524155977936330922349307608'' 
      = createUInt b128 4564848313564945646546545212389489455465465465465464699946544654654654654168"
  by eval

lemma "less (TUInt b144) (TSInt b160) (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 ShowLnat) i) t mem 
                              (ls + (STR ''['') + (ShowLnat 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 ⇒ nat ⇒ mtypes ⇒ memoryT ⇒ String.literal ⇒String.literal ⇒String.literal" where
"dumpMemory loc x t mem ls str = iter (λi. dumprecMemory ((hash loc (ShowLnat i))) t mem (ls + STR ''['' + (ShowLnat 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
            type.Memory (MTArray x t) ⇒ dumpMemory p x t m i txt
            | _ ⇒ FAILURE)
      | Some (KStoptr p) ⇒ (case tp of
            type.Storage t ⇒ dumpStorage s p i t txt
            | _ ⇒ FAILURE))
   | Some (type.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 (atype.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_version a (ShowLnat x))) EMPTY ((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, emptyTypedStore, emptyTypedStore, 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'',(type.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''), type.Storage (STArray 1 (STArray 2 (STValue (TSInt b120)))), Stoarr [SArray [SInt 347104507864064359095275590289383142, SInt 565831699297331399489670920129618233]]),
             ((STR ''a_s120_21_m8''), type.Memory (MTArray 1 (MTArray 2 (MTValue (TSInt b120)))), 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 b8 1]) (LVAL (Ref (STR ''a_s8_31_s7'') [UINT b8 0]))) 
            (STR ''089Be5381FcEa58aF334101414c04F993947C733'')
            EMPTY
            EMPTY
            (STR ''0'')
            [(STR ''089Be5381FcEa58aF334101414c04F993947C733'', STR ''100'', EOA, 0)]
            [(STR ''a_s8_31_s7'', type.Storage (STArray 1 (STArray 3 (STValue (TSInt b8)))), Stoarr [SArray [SInt ((98)), SInt ((-23)), SInt (36)]]),
             (STR ''a_s8_32_m0'', type.Memory (MTArray 2 (MTArray 3 (MTValue (TSInt b8)))), 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'', type.Storage (STMap (TUInt b32) (STValue (TUInt b8))), 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 b256 0))
            (STR ''local'')
            EMPTY
            (STR ''mycontract'')
            (STR ''0'')
            [(STR ''local'', STR ''100'', EOA, 0), (STR ''myaddr'', STR ''100'', atype.Contract (STR ''mycontract''), 0)]
            []
        = STR ''local: balance==100 - EOA⏎myaddr: balance==100 - mycontract(v1==false⏎)''"
  by (eval)

lemma "eval1 1000
            (NEW (STR ''mycontract'') [] (UINT b256 10))
            (STR ''local'')
            EMPTY
            (STR ''mycontract'')
            (STR ''0'')
            [(STR ''local'', STR ''100'', EOA, 0), (STR ''myaddr'', STR ''100'', atype.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 b256 10))
                (EXTERNAL CONTRACTS (STR ''m1'') [] (UINT b256 0))
            )
            (STR ''local'')
            EMPTY
            (STR ''mycontract'')
            (STR ''0'')
            [(STR ''local'', STR ''100'', EOA, 0), (STR ''myaddr'', STR ''100'', atype.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 b8 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 b8), Stackint 0))]
       = STR ''v1==5⏎myaddr: balance==100 - EOA''"
  by (eval)

definition "testenv3 ≡ loadProc (STR ''mycontract'')
              ([(STR ''m1'',
                Function ([(STR ''v2'', Value (TSInt b8)), (STR ''v3'', Value (TSInt b8))],
                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 b8 3, e.INT b8 4]))
            (STR ''myaddr'')
            (STR ''mycontract'')
            EMPTY
            (STR ''0'')
            [(STR ''myaddr'', STR ''100'', EOA, 0),(STR ''mya'', STR ''100'', EOA, 0)]
            [(STR ''v1'', (Value (TSInt b8), 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 b8)), (STR ''v3'', Value (TSInt b8))], 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 b8 3, e.INT b8 4]))
            (STR ''myaddr'')
            EMPTY
            EMPTY
            (STR ''0'')
            [(STR ''myaddr'', STR ''100'', EOA, 0), (STR ''extaddr'', STR ''100'', atype.Contract (STR ''mycontract''), 0)]
            [(STR ''v1'', (Value (TSInt b8), 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 b256 10))
            (STR ''089Be5381FcEa58aF334101414c04F993947C733'') 
            EMPTY
            EMPTY
            (STR ''0'')
            [(STR ''089Be5381FcEa58aF334101414c04F993947C733'', STR ''100'', EOA, 0), (STR ''myaddr'', STR ''100'', atype.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 b256 10))
          (STR ''SenderAd'')
          EMPTY
          EMPTY
          (STR ''0'')
          [(STR ''ReceiverAd'', STR ''100'', atype.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 b8 0))))(TRANSFER (ADDRESS (STR ''myaddr'')) (UINT b256 5)))(SKIP))
            (STR ''089Be5381FcEa58aF334101414c04F993947C733'')
            EMPTY
            EMPTY
            (STR ''0'')
            [(STR ''089Be5381FcEa58aF334101414c04F993947C733'', STR ''100'', EOA, 0), (STR ''myaddr'', STR ''100'', atype.Contract (STR ''mycontract''),0)]
            [(STR ''x'', (Value (TUInt b8), 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 b8 3] eempty emptyTypedStore (mystate⦇state.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 b8 3, UINT b8 4] eempty emptyTypedStore (mystate⦇state.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 b8 5] eempty emptyTypedStore (mystate⦇state.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 b8 0]) TRUE)"
abbreviation myenv::environment
  where "myenv ≡ updateEnv (STR ''ma'') (type.Memory (MTArray 1 (MTValue TBool))) (Stackloc (STR ''1''))
                 (updateEnv (STR ''sa'') (type.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 ≡ updateTypeStore (STR ''0.1'') (MTValue TBool) (updateStore (STR ''0.1'') (MValue (STR ''False'')) emptyTypedStore)"

abbreviation mystorage::storageT
  where "mystorage ≡ fmupd (STR ''0.1'') (STR ''True'') fmempty"

declare[[ML_print_depth = 10000]]
value ‹(stmt P1 myenv emptyTypedStore ⦇Accounts=emptyAccount, Stack=mystack, Memory=mymemory, Storage=(mystore ((STR ''ad''):= mystorage)), state.Gas=1000⦈)›  


lemma ‹(stmt P1 myenv emptyTypedStore ⦇Accounts=emptyAccount, Stack=mystack, Memory=mymemory, Storage=(mystore ((STR ''ad''):= mystorage)), state.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, Typed_Mapping= fmap_of_list [(STR ''0.1'', MTValue TBool)]⦈, Storage = (mystore ((STR ''ad''):= mystorage)), state.Gas = 1000⦈) ›  
    by(solidity_symbex)

end