EVM uses bounded 256 bit integer words, and sometimes also bytes (8 bit words).
Here we provide the arithmetic of these words, as well as some data-structures over them.
Both are implemented using K's Int
.
requires "krypto.k"
module EVM-DATA
imports KRYPTO
imports STRING-BUFFER
imports MAP
imports COLLECTIONS
syntax KResult ::= Int
The JSON format is used extensively for communication in the Ethereum circles. Writing a JSON-ish parser in K takes 6 lines.
syntax JSONList ::= List{JSON,","}
syntax JSONKey ::= String | Int
syntax JSON ::= String
| JSONKey ":" JSON
| "{" JSONList "}"
| "[" JSONList "]"
// ------------------------------------
Some important numbers that are referred to often during execution.
These can be used for pattern-matching on the LHS of rules as well (macro
attribute expands all occurances of these in rules).
syntax Int ::= "pow256" /* 2 ^Int 256 */
| "pow255" /* 2 ^Int 255 */
| "pow160" /* 2 ^Int 160 */
| "pow16" /* 2 ^Int 16 */
// ----------------------------------------
rule pow256 => 115792089237316195423570985008687907853269984665640564039457584007913129639936 [macro]
rule pow255 => 57896044618658097711785492504343953926634992332820282019728792003956564819968 [macro]
rule pow160 => 1461501637330902918203684832716283019655932542976 [macro]
rule pow16 => 65536 [macro]
syntax Int ::= "minSInt128"
| "maxSInt128"
| "minUInt8"
| "maxUInt8"
| "minUInt48"
| "maxUInt48"
| "minUInt128"
| "maxUInt128"
| "minUInt160"
| "maxUInt160"
| "minSInt256"
| "maxSInt256"
| "minUInt256"
| "maxUInt256"
| "minSFixed128x10"
| "maxSFixed128x10"
| "minUFixed128x10"
| "maxUFixed128x10"
// --------------------------------
rule minSInt128 => -170141183460469231731687303715884105728 [macro] /* -2^127 */
rule maxSInt128 => 170141183460469231731687303715884105727 [macro] /* 2^127 - 1 */
rule minSFixed128x10 => -1701411834604692317316873037158841057280000000000 [macro] /* (-2^127 ) * 10^10 */
rule maxSFixed128x10 => 1701411834604692317316873037158841057270000000000 [macro] /* ( 2^127 - 1) * 10^10 */
rule minSInt256 => -57896044618658097711785492504343953926634992332820282019728792003956564819968 [macro] /* -2^255 */
rule maxSInt256 => 57896044618658097711785492504343953926634992332820282019728792003956564819967 [macro] /* 2^255 - 1 */
rule minUInt8 => 0 [macro]
rule maxUInt8 => 255 [macro]
rule minUInt48 => 0 [macro]
rule maxUInt48 => 281474976710655 [macro] /* 2^48 - 1 */
rule minUInt128 => 0 [macro]
rule maxUInt128 => 340282366920938463463374607431768211455 [macro] /* 2^128 - 1 */
rule minUFixed128x10 => 0 [macro]
rule maxUFixed128x10 => 3402823669209384634633746074317682114550000000000 [macro] /* ( 2^128 - 1) * 10^10 */
rule minUInt160 => 0 [macro]
rule maxUInt160 => 1461501637330902918203684832716283019655932542975 [macro] /* 2^160 - 1 */
rule minUInt256 => 0 [macro]
rule maxUInt256 => 115792089237316195423570985008687907853269984665640564039457584007913129639935 [macro] /* 2^256 - 1 */
- Range of types
syntax Bool ::= #rangeSInt ( Int , Int )
| #rangeUInt ( Int , Int )
| #rangeSFixed ( Int , Int , Int )
| #rangeUFixed ( Int , Int , Int )
| #rangeAddress ( Int )
| #rangeBytes ( Int , Int )
// -------------------------------------------
rule #rangeSInt ( 128 , X ) => #range ( minSInt128 <= X <= maxSInt128 ) [macro]
rule #rangeSInt ( 256 , X ) => #range ( minSInt256 <= X <= maxSInt256 ) [macro]
rule #rangeUInt ( 48 , X ) => #range ( minUInt48 <= X <= maxUInt48 ) [macro]
rule #rangeUInt ( 128 , X ) => #range ( minUInt128 <= X <= maxUInt128 ) [macro]
rule #rangeUInt ( 256 , X ) => #range ( minUInt256 <= X <= maxUInt256 ) [macro]
rule #rangeSFixed ( 128 , 10 , X ) => #range ( minSFixed128x10 <= X <= maxSFixed128x10 ) [macro]
rule #rangeUFixed ( 128 , 10 , X ) => #range ( minUFixed128x10 <= X <= maxUFixed128x10 ) [macro]
rule #rangeAddress ( X ) => #range ( minUInt160 <= X <= maxUInt160 ) [macro]
rule #rangeBytes ( 32 , X ) => #range ( minUInt256 <= X <= maxUInt256 ) [macro]
syntax Bool ::= "#range" "(" Int "<" Int "<" Int ")"
| "#range" "(" Int "<" Int "<=" Int ")"
| "#range" "(" Int "<=" Int "<" Int ")"
| "#range" "(" Int "<=" Int "<=" Int ")"
// ------------------------------------------------------
rule #range ( LB < X < UB ) => LB <Int X andBool X <Int UB [macro]
rule #range ( LB < X <= UB ) => LB <Int X andBool X <=Int UB [macro]
rule #range ( LB <= X < UB ) => LB <=Int X andBool X <Int UB [macro]
rule #range ( LB <= X <= UB ) => LB <=Int X andBool X <=Int UB [macro]
-
chop
interperets an integer modulo$2^256$ .
syntax Int ::= chop ( Int ) [function, smtlib(chop)]
// ----------------------------------------------------
rule chop ( I:Int ) => I modInt pow256 [concrete, smt-lemma]
Primitives provide the basic conversion from K's sorts Int
and Bool
to EVM's words.
bool2Word
interperets aBool
as aInt
.word2Bool
interperets aInt
as aBool
.
syntax Int ::= bool2Word ( Bool ) [function]
// --------------------------------------------
rule bool2Word( B:Bool ) => 1 requires B
rule bool2Word( B:Bool ) => 0 requires notBool B
syntax Bool ::= word2Bool ( Int ) [function]
// --------------------------------------------
rule word2Bool( W ) => false requires W ==Int 0
rule word2Bool( W ) => true requires W =/=Int 0
sgn
gives the twos-complement interperetation of the sign of a word.abs
gives the twos-complement interperetation of the magnitude of a word.
syntax Int ::= sgn ( Int ) [function]
| abs ( Int ) [function]
// -------------------------------------
rule sgn(I) => -1 requires I >=Int pow255
rule sgn(I) => 1 requires I <Int pow255
rule abs(I) => 0 -Word I requires sgn(I) ==Int -1
rule abs(I) => I requires sgn(I) ==Int 1
- #signed : uInt256 -> sInt256 (i.e., [minUInt256..maxUInt256] -> [minSInt256..maxSInt256])
- #unsigned : sInt256 -> uInt256 (i.e., [minSInt256..maxSInt256] -> [minUInt256..maxUInt256])
syntax Int ::= #signed ( Int ) [function]
// -----------------------------------------
rule #signed(DATA) => DATA
requires 0 <=Int DATA andBool DATA <=Int maxSInt256
rule #signed(DATA) => DATA -Int pow256
requires maxSInt256 <Int DATA andBool DATA <=Int maxUInt256
syntax Int ::= #unsigned ( Int ) [function]
// -----------------------------------------
rule #unsigned(DATA) => DATA
requires 0 <=Int DATA andBool DATA <=Int maxSInt256
rule #unsigned(DATA) => pow256 +Int DATA
requires minSInt256 <=Int DATA andBool DATA <Int 0
.Account
represents the case when an account ID is referenced in the yellowpaper, but the actual value of the account ID is the empty set. This is used, for example, when referring to the destination of a message which creates a new contract.
syntax Account ::= ".Account" | Int
#symbolicWord
generates a fresh existentially-bound symbolic word.
syntax Int ::= "#symbolicWord" [function]
// -----------------------------------------
rule #symbolicWord => chop ( ?X:Int )
up/Int
performs integer division but rounds up instead of down.
NOTE: Here, we choose to add I2 -Int 1
to the numerator beforing doing the division to mimic the C++ implementation.
You could alternatively calculate I1 modInt I2
, then add one to the normal integer division afterward depending on the result.
syntax Int ::= Int "up/Int" Int [function]
// ------------------------------------------
rule I1 up/Int 0 => 0
rule I1 up/Int 1 => I1
rule I1 up/Int I2 => (I1 +Int (I2 -Int 1)) /Int I2 requires I2 >Int 1
log256Int
returns the log base 256 (floored) of an integer.
syntax Int ::= log256Int ( Int ) [function]
// -------------------------------------------
rule log256Int(N) => log2Int(N) /Int 8
The corresponding <op>Word
operations automatically perform the correct modulus for EVM words.
syntax Int ::= Int "+Word" Int [function]
| Int "*Word" Int [function]
| Int "-Word" Int [function]
| Int "/Word" Int [function]
| Int "%Word" Int [function]
// -----------------------------------------
rule W0 +Word W1 => chop( W0 +Int W1 )
rule W0 -Word W1 => chop( W0 -Int W1 ) requires W0 >=Int W1
rule W0 -Word W1 => chop( (W0 +Int pow256) -Int W1 ) requires W0 <Int W1
rule W0 *Word W1 => chop( W0 *Int W1 )
rule W0 /Word W1 => 0 requires W1 ==Int 0
rule W0 /Word W1 => chop( W0 /Int W1 ) requires W1 =/=Int 0
rule W0 %Word W1 => 0 requires W1 ==Int 0
rule W0 %Word W1 => chop( W0 modInt W1 ) requires W1 =/=Int 0
Care is needed for ^Word
to avoid big exponentiation.
The helper powmod
is a totalization of the operator _^%Int__
(which comes with K).
_^%Int__
is not defined when the modulus (third argument) is zero, but powmod
is.
syntax Int ::= Int "^Word" Int [function]
syntax Int ::= powmod(Int, Int, Int) [function]
// -----------------------------------------------
rule W0 ^Word W1 => powmod(W0, W1, pow256)
rule powmod(W0, W1, W2) => W0 ^%Int W1 W2 requires W2 =/=Int 0
rule powmod(W0, W1, W2) => 0 requires W2 ==Int 0
/sWord
and %sWord
give the signed interperetations of /Word
and %Word
.
syntax Int ::= Int "/sWord" Int [function]
| Int "%sWord" Int [function]
// ------------------------------------------
rule W0 /sWord W1 => #sgnInterp(sgn(W0) *Int sgn(W1) , abs(W0) /Word abs(W1))
rule W0 %sWord W1 => #sgnInterp(sgn(W0) , abs(W0) %Word abs(W1))
syntax Int ::= #sgnInterp ( Int , Int ) [function]
// --------------------------------------------------
rule #sgnInterp( W0 , W1 ) => 0 requires W0 ==Int 0
rule #sgnInterp( W0 , W1 ) => W1 requires W0 >Int 0
rule #sgnInterp( W0 , W1 ) => 0 -Word W1 requires W0 <Int 0
The <op>Word
comparisons similarly lift K operators to EVM ones:
syntax Int ::= Int "<Word" Int [function]
| Int ">Word" Int [function]
| Int "<=Word" Int [function]
| Int ">=Word" Int [function]
| Int "==Word" Int [function]
// ------------------------------------------
rule W0 <Word W1 => bool2Word(W0 <Int W1)
rule W0 >Word W1 => bool2Word(W0 >Int W1)
rule W0 <=Word W1 => bool2Word(W0 <=Int W1)
rule W0 >=Word W1 => bool2Word(W0 >=Int W1)
rule W0 ==Word W1 => bool2Word(W0 ==Int W1)
s<Word
implements a less-than forWord
(with signed interperetation).
syntax Int ::= Int "s<Word" Int [function]
// ------------------------------------------
rule W0 s<Word W1 => W0 <Word W1 requires sgn(W0) ==K 1 andBool sgn(W1) ==K 1
rule W0 s<Word W1 => bool2Word(false) requires sgn(W0) ==K 1 andBool sgn(W1) ==K -1
rule W0 s<Word W1 => bool2Word(true) requires sgn(W0) ==K -1 andBool sgn(W1) ==K 1
rule W0 s<Word W1 => abs(W1) <Word abs(W0) requires sgn(W0) ==K -1 andBool sgn(W1) ==K -1
Bitwise logical operators are lifted from the integer versions.
syntax Int ::= "~Word" Int [function]
| Int "|Word" Int [function]
| Int "&Word" Int [function]
| Int "xorWord" Int [function]
// -------------------------------------------
rule ~Word W => chop( W xorInt (pow256 -Int 1) )
rule W0 |Word W1 => chop( W0 |Int W1 )
rule W0 &Word W1 => chop( W0 &Int W1 )
rule W0 xorWord W1 => chop( W0 xorInt W1 )
-
bit
gets bit$N$ (0 being MSB). -
byte
gets byte$N$ (0 being the MSB).
syntax Int ::= bit ( Int , Int ) [function]
| byte ( Int , Int ) [function]
// --------------------------------------------
rule bit (N, _) => 0 requires notBool (N >=Int 0 andBool N <Int 256)
rule byte(N, _) => 0 requires notBool (N >=Int 0 andBool N <Int 32)
rule bit (N, W) => bitRangeInt(W , (255 -Int N) , 1) requires N >=Int 0 andBool N <Int 256
rule byte(N, W) => bitRangeInt(W , ( 31 -Int N) *Int 8 , 8) requires N >=Int 0 andBool N <Int 32
-
#nBits
shifts in$N$ ones from the right. -
#nBytes
shifts in$N$ bytes of ones from the right. -
_<<Byte_
shifts an integer 8 bits to the left.
syntax Int ::= #nBits ( Int ) [function]
| #nBytes ( Int ) [function]
| Int "<<Byte" Int [function]
// ------------------------------------------
rule #nBits(N) => (1 <<Int N) -Int 1 requires N >=Int 0
rule #nBytes(N) => #nBits(N *Int 8) requires N >=Int 0
rule N <<Byte M => N <<Int (8 *Int M)
-
signextend(N, W)
sign-extends from byte$N$ of$W$ (0 being MSB).
syntax Int ::= signextend( Int , Int ) [function]
// -------------------------------------------------
rule signextend(N, W) => W requires N >=Int 32 orBool N <Int 0
rule signextend(N, W) => chop( (#nBytes(31 -Int N) <<Byte (N +Int 1)) |Int W ) requires N <Int 32 andBool N >=Int 0 andBool word2Bool(bit(256 -Int (8 *Int (N +Int 1)), W))
rule signextend(N, W) => chop( #nBytes(N +Int 1) &Int W ) requires N <Int 32 andBool N >=Int 0 andBool notBool word2Bool(bit(256 -Int (8 *Int (N +Int 1)), W))
keccak
serves as a wrapper around theKeccak256
inKRYPTO
.
syntax Int ::= keccak ( WordStack ) [function, smtlib(smt_keccak)]
// ------------------------------------------------------------------
rule keccak(WS) => #parseHexWord(Keccak256(#unparseByteStack(WS))) [concrete]
A cons-list is used for the EVM wordstack.
.WordStack
serves as the empty worstack, and_:_
serves as the "cons" operator.
syntax WordStack [flatPredicate]
syntax WordStack ::= ".WordStack" | Int ":" WordStack
// -----------------------------------------------------
-
_++_
acts asWordStack
append. -
#take(N , WS)
keeps the first$N$ elements of aWordStack
(passing with zeros as needed). -
#drop(N , WS)
removes the first$N$ elements of aWordStack
.
syntax WordStack ::= WordStack "++" WordStack [function, right]
// ---------------------------------------------------------------
rule .WordStack ++ WS' => WS'
rule (W : WS) ++ WS' => W : (WS ++ WS')
syntax WordStack ::= #take ( Int , WordStack ) [function]
// ---------------------------------------------------------
rule #take(0, WS) => .WordStack
rule #take(N, .WordStack) => 0 : #take(N -Int 1, .WordStack) requires N >Int 0
rule #take(N, (W : WS)) => W : #take(N -Int 1, WS) requires N >Int 0
syntax WordStack ::= #drop ( Int , WordStack ) [function]
// ---------------------------------------------------------
rule #drop(0, WS) => WS
rule #drop(N, .WordStack) => .WordStack
rule #drop(N, (W : WS)) => #drop(N -Int 1, WS) requires N >Int 0
-
WS [ N ]
accesses element$N$ of$WS$ . -
WS [ N .. W ]
access the range ofWS
beginning withN
of widthW
. -
WS [ N := W ]
sets element$N$ of$WS$ to$W$ (padding with zeros as needed).
syntax Int ::= WordStack "[" Int "]" [function]
// -----------------------------------------------
rule (W0 : WS) [N] => W0 requires N ==Int 0
rule (.WordStack)[N] => 0 requires N >Int 0
rule (W0 : WS) [N] => WS[N -Int 1] requires N >Int 0
syntax WordStack ::= WordStack "[" Int ".." Int "]" [function]
// --------------------------------------------------------------
rule WS [ START .. WIDTH ] => #take(WIDTH, #drop(START, WS))
syntax WordStack ::= WordStack "[" Int ":=" Int "]" [function]
// --------------------------------------------------------------
rule (W0 : WS) [ N := W ] => W : WS requires N ==Int 0
rule .WordStack [ N := W ] => 0 : (.WordStack [ N -Int 1 := W ]) requires N >Int 0
rule (W0 : WS) [ N := W ] => W0 : (WS [ N -Int 1 := W ]) requires N >Int 0
#sizeWordStack
calculates the size of aWordStack
._in_
determines if aInt
occurs in aWordStack
.
syntax Int ::= #sizeWordStack ( WordStack ) [function, smtlib(sizeWordStack)]
| #sizeWordStack ( WordStack , Int ) [function, klabel(sizeWordStackAux), smtlib(sizeWordStackAux)]
// ----------------------------------------------------------------------------------------------------------------
rule #sizeWordStack ( WS ) => #sizeWordStack(WS, 0)
rule #sizeWordStack ( .WordStack, SIZE ) => SIZE
rule #sizeWordStack ( W : WS, SIZE ) => #sizeWordStack(WS, SIZE +Int 1)
syntax Bool ::= Int "in" WordStack [function]
// ---------------------------------------------
rule W in .WordStack => false
rule W in (W' : WS) => (W ==K W') orElseBool (W in WS)
#padToWidth(N, WS)
and#padRightToWidth
make sure that aWordStack
is the correct size.
syntax WordStack ::= #padToWidth ( Int , WordStack ) [function]
// ---------------------------------------------------------------
rule #padToWidth(N, WS) => WS requires notBool #sizeWordStack(WS) <Int N [concrete]
rule #padToWidth(N, WS) => #padToWidth(N, 0 : WS) requires #sizeWordStack(WS) <Int N [concrete]
syntax WordStack ::= #padRightToWidth ( Int , WordStack ) [function]
// --------------------------------------------------------------------
rule #padRightToWidth(N, WS) => #padRightToWidthAux(N -Int #sizeWordStack(WS), WS, .WordStack)
syntax WordStack ::= #padRightToWidthAux ( Int , WordStack , WordStack ) [function]
// -----------------------------------------------------------------------------------
rule #padRightToWidthAux(0, WS, ZEROS) => WS ++ ZEROS
rule #padRightToWidthAux(N, WS, ZEROS) => #padRightToWidthAux(N -Int 1, WS, 0 : ZEROS)
requires N >Int 0
WordStack2List
converts a term of sortWordStack
to a term of sortList
.
syntax List ::= WordStack2List ( WordStack ) [function]
// -------------------------------------------------------
rule WordStack2List(.WordStack) => .List
rule WordStack2List(W : WS) => ListItem(W) WordStack2List(WS)
The local memory of execution is a byte-array (instead of a word-array).
#asWord
will interperet a stack of bytes as a single word (with MSB first).#asInteger
will interperet a stack of bytes as a single arbitrary-precision integer (with MSB first).#asAccount
will interpret a stack of bytes as a single account id (with MSB first). Differs from#asWord
only in that an empty stack represents the empty account, not account zero.#asByteStack
will split a single word up into aWordStack
where each word is a byte wide.
syntax Int ::= #asWord ( WordStack ) [function, smtlib(asWord)]
// ---------------------------------------------------------------
rule #asWord( .WordStack ) => 0 // [concrete]
rule #asWord( W : .WordStack ) => W // [concrete]
rule #asWord( W0 : W1 : WS ) => #asWord(((W0 *Word 256) +Word W1) : WS) [concrete]
syntax Int ::= #asInteger ( WordStack ) [function]
// --------------------------------------------------
rule #asInteger( .WordStack ) => 0
rule #asInteger( W : .WordStack ) => W
rule #asInteger( W0 : W1 : WS ) => #asInteger(((W0 *Int 256) +Int W1) : WS)
syntax Account ::= #asAccount ( WordStack ) [function]
// ------------------------------------------------------
rule #asAccount( .WordStack ) => .Account
rule #asAccount( W : WS ) => #asWord(W : WS)
syntax WordStack ::= #asByteStack ( Int ) [function]
| #asByteStack ( Int , WordStack ) [function, klabel(#asByteStackAux), smtlib(asByteStack)]
// --------------------------------------------------------------------------------------------------------------
rule #asByteStack( W ) => #asByteStack( W , .WordStack ) [concrete]
rule #asByteStack( 0 , WS ) => WS // [concrete]
rule #asByteStack( W , WS ) => #asByteStack( W /Int 256 , W modInt 256 : WS ) requires W =/=K 0 [concrete]
#addr
turns an Ethereum word into the corresponding Ethereum address (160 LSB).
syntax Int ::= #addr ( Int ) [function]
// ---------------------------------------
rule #addr(W) => W %Word pow160
#newAddr
computes the address of a new account given the address and nonce of the creating account.#sender
computes the sender of the transaction from its data and signature.
syntax Int ::= #newAddr ( Int , Int ) [function]
// ------------------------------------------------
rule #newAddr(ACCT, NONCE) => #addr(#parseHexWord(Keccak256(#rlpEncodeLength(#rlpEncodeBytes(ACCT, 20) +String #rlpEncodeWord(NONCE), 192))))
syntax Account ::= #sender ( Int , Int , Int , Account , Int , String , Int , WordStack , WordStack ) [function]
| #sender ( String , Int , String , String ) [function, klabel(#senderAux)]
| #sender ( String ) [function, klabel(#senderAux2)]
// -------------------------------------------------------------------------------------------------------------------------------------
rule #sender(TN, TP, TG, TT, TV, DATA, TW, TR, TS)
=> #sender(#unparseByteStack(#parseHexBytes(Keccak256(#rlpEncodeLength(#rlpEncodeWordStack(TN : TP : TG : .WordStack) +String #rlpEncodeAccount(TT) +String #rlpEncodeWord(TV) +String #rlpEncodeString(DATA), 192)))), TW, #unparseByteStack(TR), #unparseByteStack(TS))
rule #sender(HT, TW, TR, TS) => #sender(ECDSARecover(HT, TW, TR, TS))
rule #sender("") => .Account
rule #sender(STR) => #addr(#parseHexWord(Keccak256(STR))) requires STR =/=String ""
#blockHeaderHash
computes the hash of a block header given all the block data.
syntax Int ::= #blockHeaderHash( Int , Int , Int , Int , Int , Int , WordStack , Int , Int , Int , Int , Int , WordStack , Int , Int ) [function, klabel(blockHeaderHash), symbol]
| #blockHeaderHash(String, String, String, String, String, String, String, String, String, String, String, String, String, String, String) [function, klabel(#blockHashHeaderStr), symbol]
// -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
rule #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN)
=> #blockHeaderHash(#asWord(#parseByteStackRaw(HP)),
#asWord(#parseByteStackRaw(HO)),
#asWord(#parseByteStackRaw(HC)),
#asWord(#parseByteStackRaw(HR)),
#asWord(#parseByteStackRaw(HT)),
#asWord(#parseByteStackRaw(HE)),
#parseByteStackRaw(HB) ,
#asWord(#parseByteStackRaw(HD)),
#asWord(#parseByteStackRaw(HI)),
#asWord(#parseByteStackRaw(HL)),
#asWord(#parseByteStackRaw(HG)),
#asWord(#parseByteStackRaw(HS)),
#parseByteStackRaw(HX) ,
#asWord(#parseByteStackRaw(HM)),
#asWord(#parseByteStackRaw(HN)))
rule #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN)
=> #parseHexWord(Keccak256(#rlpEncodeLength( #rlpEncodeBytes(HP, 32)
+String #rlpEncodeBytes(HO, 32)
+String #rlpEncodeBytes(HC, 20)
+String #rlpEncodeBytes(HR, 32)
+String #rlpEncodeBytes(HT, 32)
+String #rlpEncodeBytes(HE, 32)
+String #rlpEncodeString(#unparseByteStack(HB))
+String #rlpEncodeWordStack(HD : HI : HL : HG : HS : .WordStack)
+String #rlpEncodeString(#unparseByteStack(HX))
+String #rlpEncodeBytes(HM, 32)
+String #rlpEncodeBytes(HN, 8),
192)))
Most of EVM data is held in finite maps.
We are using the polymorphic Map
sort for these word maps.
-
WM [ N := WS ]
assigns a contiguous chunk of$WM$ to$WS$ starting at position$W$ . -
#asMapWordStack
converts aWordStack
to aMap
. -
#range(M, START, WIDTH)
reads off$WIDTH$ elements from$WM$ beginning at position$START$ (padding with zeros as needed).
syntax Map ::= Map "[" Int ":=" WordStack "]" [function]
// --------------------------------------------------------
rule WM[ N := .WordStack ] => WM
rule WM[ N := W : WS ] => (WM[N <- W])[N +Int 1 := WS]
syntax Map ::= #asMapWordStack ( WordStack ) [function]
// -------------------------------------------------------
rule #asMapWordStack(WS:WordStack) => .Map [ 0 := WS ]
syntax WordStack ::= #range ( Map , Int , Int ) [function]
syntax WordStack ::= #range ( Map , Int , Int , WordStack) [function, klabel(#rangeAux)]
// ----------------------------------------------------------------------------------------
rule #range(WM, START, WIDTH) => #range(WM, START +Int WIDTH -Int 1, WIDTH, .WordStack)
rule #range(WM, END, WIDTH, WS) => WS requires WIDTH ==Int 0
rule #range(WM, END, WIDTH, WS) => #range(WM, END -Int 1, WIDTH -Int 1, 0 : WS) requires (WIDTH >Int 0) andBool notBool END in_keys(WM)
rule #range(END |-> W WM, END, WIDTH, WS) => #range(WM, END -Int 1, WIDTH -Int 1, W : WS) requires (WIDTH >Int 0)
#removeZeros
removes any entries in a map with zero values.
syntax Map ::= #removeZeros ( Map ) [function]
| #removeZeros ( List , Map ) [function, klabel(#removeZerosAux)]
// ------------------------------------------------------------------------------
rule #removeZeros( M ) => #removeZeros(Set2List(keys(M)), M)
rule #removeZeros( .List, .Map ) => .Map
rule #removeZeros( ListItem(KEY) L, KEY |-> 0 REST ) => #removeZeros(L, REST)
rule #removeZeros( ListItem(KEY) L, KEY |-> VALUE REST ) => KEY |-> VALUE #removeZeros(L, REST) requires VALUE =/=K 0
#lookup
looks up a key in a map and returns 0 if the key doesn't exist, otherwise returning its value.
syntax Int ::= #lookup ( Map , Int ) [function]
// -----------------------------------------------
rule #lookup( (KEY |-> VAL) M, KEY ) => VAL
rule #lookup( M, KEY ) => 0 requires notBool KEY in_keys(M)
The EVM test-sets are represented in JSON format with hex-encoding of the data and programs. Here we provide some standard parser/unparser functions for that format.
These parsers can interperet hex-encoded strings as Int
s, WordStack
s, and Map
s.
#parseHexWord
interperets a string as a single hex-encodedWord
.#parseHexBytes
interperets a string as a hex-encoded stack of bytes.#parseByteStack
interperets a string as a hex-encoded stack of bytes, but makes sure to remove the leading "0x".#parseByteStackRaw
inteprets a string as a stack of bytes.#parseWordStack
interperets a JSON list as a stack ofWord
.#parseMap
interperets a JSON key/value object as a map fromWord
toWord
.#parseAddr
interperets a string as a 160 bit hex-endcoded address.
syntax Int ::= #parseHexWord ( String ) [function]
| #parseWord ( String ) [function]
// --------------------------------------------------
rule #parseHexWord("") => 0
rule #parseHexWord("0x") => 0
rule #parseHexWord(S) => String2Base(replaceAll(S, "0x", ""), 16) requires (S =/=String "") andBool (S =/=String "0x")
rule #parseWord("") => 0
rule #parseWord(S) => #parseHexWord(S) requires lengthString(S) >=Int 2 andBool substrString(S, 0, 2) ==String "0x"
rule #parseWord(S) => String2Int(S) [owise]
syntax WordStack ::= #parseHexBytes ( String ) [function]
| #parseByteStack ( String ) [function]
| #parseByteStackRaw ( String ) [function]
// ----------------------------------------------------------
rule #parseByteStack(S) => #parseHexBytes(replaceAll(S, "0x", ""))
rule #parseHexBytes("") => .WordStack
rule #parseHexBytes(S) => #parseHexWord(substrString(S, 0, 2)) : #parseHexBytes(substrString(S, 2, lengthString(S))) requires lengthString(S) >=Int 2
rule #parseByteStackRaw(S) => ordChar(substrString(S, 0, 1)) : #parseByteStackRaw(substrString(S, 1, lengthString(S))) requires lengthString(S) >=Int 1
rule #parseByteStackRaw("") => .WordStack
syntax WordStack ::= #parseWordStack ( JSON ) [function]
// --------------------------------------------------------
rule #parseWordStack( [ .JSONList ] ) => .WordStack
rule #parseWordStack( [ (WORD:String) , REST ] ) => #parseHexWord(WORD) : #parseWordStack( [ REST ] )
syntax Map ::= #parseMap ( JSON ) [function]
// --------------------------------------------
rule #parseMap( { .JSONList } ) => .Map
rule #parseMap( { _ : (VALUE:String) , REST } ) => #parseMap({ REST }) requires #parseHexWord(VALUE) ==K 0
rule #parseMap( { KEY : (VALUE:String) , REST } ) => #parseMap({ REST }) [ #parseHexWord(KEY) <- #parseHexWord(VALUE) ] requires #parseHexWord(VALUE) =/=K 0
syntax Int ::= #parseAddr ( String ) [function]
// -----------------------------------------------
rule #parseAddr(S) => #addr(#parseHexWord(S))
We need to interperet a WordStack
as a String
again so that we can call Keccak256
on it from KRYPTO
.
#unparseByteStack
turns a stack of bytes (as aWordStack
) into aString
.#padByte
ensures that theString
interperetation of aInt
is wide enough.
syntax String ::= #unparseByteStack ( WordStack ) [function, klabel(unparseByteStack)]
| #unparseByteStack ( WordStack , StringBuffer ) [function, klabel(#unparseByteStackAux)]
// ---------------------------------------------------------------------------------------------------------
rule #unparseByteStack ( WS ) => #unparseByteStack(WS, .StringBuffer)
rule #unparseByteStack( .WordStack, BUFFER ) => StringBuffer2String(BUFFER)
rule #unparseByteStack( W : WS, BUFFER ) => #unparseByteStack(WS, BUFFER +String chrChar(W modInt (2 ^Int 8)))
syntax String ::= #padByte( String ) [function]
// -----------------------------------------------
rule #padByte( S ) => S requires lengthString(S) ==K 2
rule #padByte( S ) => "0" +String S requires lengthString(S) ==K 1
RLP encoding is used extensively for executing the blocks of a transaction. For details about RLP encoding, see the YellowPaper Appendix B.
#rlpEncodeWord
RLP encodes a single EVM word.#rlpEncodeString
RLP encodes a singleString
.
syntax String ::= #rlpEncodeWord ( Int ) [function]
| #rlpEncodeBytes ( Int , Int ) [function]
| #rlpEncodeWordStack ( WordStack ) [function]
| #rlpEncodeString ( String ) [function]
| #rlpEncodeAccount ( Account ) [function]
// --------------------------------------------------------------
rule #rlpEncodeWord(0) => "\x80"
rule #rlpEncodeWord(WORD) => chrChar(WORD) requires WORD >Int 0 andBool WORD <Int 128
rule #rlpEncodeWord(WORD) => #rlpEncodeLength(#unparseByteStack(#asByteStack(WORD)), 128) requires WORD >=Int 128
rule #rlpEncodeBytes(WORD, LEN) => #rlpEncodeString(#unparseByteStack(#padToWidth(LEN, #asByteStack(WORD))))
rule #rlpEncodeWordStack(.WordStack) => ""
rule #rlpEncodeWordStack(W : WS) => #rlpEncodeWord(W) +String #rlpEncodeWordStack(WS)
rule #rlpEncodeString(STR) => STR requires lengthString(STR) ==Int 1 andBool ordChar(STR) <Int 128
rule #rlpEncodeString(STR) => #rlpEncodeLength(STR, 128) [owise]
rule #rlpEncodeAccount(.Account) => "\x80"
rule #rlpEncodeAccount(ACCT) => #rlpEncodeBytes(ACCT, 20) requires ACCT =/=K .Account
syntax String ::= #rlpEncodeLength ( String , Int ) [function]
| #rlpEncodeLength ( String , Int , String ) [function, klabel(#rlpEncodeLengthAux)]
// ----------------------------------------------------------------------------------------------------
rule #rlpEncodeLength(STR, OFFSET) => chrChar(lengthString(STR) +Int OFFSET) +String STR requires lengthString(STR) <Int 56
rule #rlpEncodeLength(STR, OFFSET) => #rlpEncodeLength(STR, OFFSET, #unparseByteStack(#asByteStack(lengthString(STR)))) requires lengthString(STR) >=Int 56
rule #rlpEncodeLength(STR, OFFSET, BL) => chrChar(lengthString(BL) +Int OFFSET +Int 55) +String BL +String STR
#rlpDecode
RLP decodes a singleString
into aJSON
.#rlpDecodeList
RLP decodes a singleString
into aJSONList
, interpereting the string as the RLP encoding of a list.
syntax JSON ::= #rlpDecode(String) [function]
| #rlpDecode(String, LengthPrefix) [function, klabel(#rlpDecodeAux)]
// ----------------------------------------------------------------------------------
rule #rlpDecode(STR) => #rlpDecode(STR, #decodeLengthPrefix(STR, 0))
rule #rlpDecode(STR, #str(LEN, POS)) => substrString(STR, POS, POS +Int LEN)
rule #rlpDecode(STR, #list(LEN, POS)) => [#rlpDecodeList(STR, POS)]
syntax JSONList ::= #rlpDecodeList(String, Int) [function]
| #rlpDecodeList(String, Int, LengthPrefix) [function, klabel(#rlpDecodeListAux)]
// ---------------------------------------------------------------------------------------------------
rule #rlpDecodeList(STR, POS) => #rlpDecodeList(STR, POS, #decodeLengthPrefix(STR, POS)) requires POS <Int lengthString(STR)
rule #rlpDecodeList(STR, POS) => .JSONList [owise]
rule #rlpDecodeList(STR, POS, _:LengthPrefixType(L, P)) => #rlpDecode(substrString(STR, POS, L +Int P)) , #rlpDecodeList(STR, L +Int P)
syntax LengthPrefixType ::= "#str" | "#list"
syntax LengthPrefix ::= LengthPrefixType "(" Int "," Int ")"
| #decodeLengthPrefix ( String , Int ) [function]
| #decodeLengthPrefix ( String , Int , Int ) [function, klabel(#decodeLengthPrefixAux)]
| #decodeLengthPrefixLength ( LengthPrefixType , String , Int , Int ) [function]
| #decodeLengthPrefixLength ( LengthPrefixType , Int , Int , Int ) [function, klabel(#decodeLengthPrefixLengthAux)]
// --------------------------------------------------------------------------------------------------------------------------------------------
rule #decodeLengthPrefix(STR, START) => #decodeLengthPrefix(STR, START, ordChar(substrString(STR, START, START +Int 1)))
rule #decodeLengthPrefix(STR, START, B0) => #str(1, START) requires B0 <Int 128
rule #decodeLengthPrefix(STR, START, B0) => #str(B0 -Int 128, START +Int 1) requires B0 >=Int 128 andBool B0 <Int (128 +Int 56)
rule #decodeLengthPrefix(STR, START, B0) => #decodeLengthPrefixLength(#str, STR, START, B0) requires B0 >=Int (128 +Int 56) andBool B0 <Int 192
rule #decodeLengthPrefix(STR, START, B0) => #list(B0 -Int 192, START +Int 1) requires B0 >=Int 192 andBool B0 <Int 192 +Int 56
rule #decodeLengthPrefix(STR, START, B0) => #decodeLengthPrefixLength(#list, STR, START, B0) [owise]
rule #decodeLengthPrefixLength(#str, STR, START, B0) => #decodeLengthPrefixLength(#str, START, B0 -Int 128 -Int 56 +Int 1, #asWord(#parseByteStackRaw(substrString(STR, START +Int 1, START +Int 1 +Int (B0 -Int 128 -Int 56 +Int 1)))))
rule #decodeLengthPrefixLength(#list, STR, START, B0) => #decodeLengthPrefixLength(#list, START, B0 -Int 192 -Int 56 +Int 1, #asWord(#parseByteStackRaw(substrString(STR, START +Int 1, START +Int 1 +Int (B0 -Int 192 -Int 56 +Int 1)))))
rule #decodeLengthPrefixLength(TYPE, START, LL, L) => TYPE(L, START +Int 1 +Int LL)
endmodule