Skip to content

Commit a51ccb7

Browse files
author
dwightguth
authored
Use Bytes type for concrete backends (#414)
* deps/k: update submodule * delete some unused functions * data, driver, evm-node, evm: rename WordStack to ByteArray everywhere * don't use #take or #drop in evm.md * data: ByteStack implementation * evm: split implementation of #dasmOpCodes and G0 * deps/plugin: update submodule * edsl: WordStack => ByteArray * tests/failing, tests/interactive: update test file syntax * deps/k: update submodule * deps/k: update submodule * tests/failing: fix \n->\r issue * data, evm: formatting * data, evm: formatting * data: fix copy paste error
1 parent db2cc0d commit a51ccb7

File tree

10 files changed

+312
-206
lines changed

10 files changed

+312
-206
lines changed

‎data.md‎

Lines changed: 147 additions & 81 deletions
Large diffs are not rendered by default.

‎deps/k‎

Submodule k updated from ec2e4e7 to 3f1b114

‎driver.md‎

Lines changed: 18 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ For verification purposes, it's much easier to specify a program in terms of its
4141
To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a "pretti-fication" to the nicer input form.
4242

4343
```{.k .standalone}
44-
syntax JSON ::= Int | WordStack | OpCodes | Map | Call | SubstateLogEntry | Account
44+
syntax JSON ::= Int | ByteArray | OpCodes | Map | Call | SubstateLogEntry | Account
4545
// -----------------------------------------------------------------------------------
4646
4747
syntax JSONList ::= #sortJSONList ( JSONList ) [function]
@@ -354,15 +354,15 @@ State Manipulation
354354
syntax EthereumCommand ::= "clearTX"
355355
// ------------------------------------
356356
rule <k> clearTX => . ... </k>
357-
<output> _ => .WordStack </output>
357+
<output> _ => .ByteArray </output>
358358
<memoryUsed> _ => 0 </memoryUsed>
359359
<callDepth> _ => 0 </callDepth>
360360
<callStack> _ => .List </callStack>
361361
<program> _ => .Map </program>
362-
<programBytes> _ => .WordStack </programBytes>
362+
<programBytes> _ => .ByteArray </programBytes>
363363
<id> _ => 0 </id>
364364
<caller> _ => 0 </caller>
365-
<callData> _ => .WordStack </callData>
365+
<callData> _ => .ByteArray </callData>
366366
<callValue> _ => 0 </callValue>
367367
<wordStack> _ => .WordStack </wordStack>
368368
<localMem> _ => .Map </localMem>
@@ -385,13 +385,13 @@ State Manipulation
385385
<stateRoot> _ => 0 </stateRoot>
386386
<transactionsRoot> _ => 0 </transactionsRoot>
387387
<receiptsRoot> _ => 0 </receiptsRoot>
388-
<logsBloom> _ => .WordStack </logsBloom>
388+
<logsBloom> _ => .ByteArray </logsBloom>
389389
<difficulty> _ => 0 </difficulty>
390390
<number> _ => 0 </number>
391391
<gasLimit> _ => 0 </gasLimit>
392392
<gasUsed> _ => 0 </gasUsed>
393393
<timestamp> _ => 0 </timestamp>
394-
<extraData> _ => .WordStack </extraData>
394+
<extraData> _ => .ByteArray </extraData>
395395
<mixHash> _ => 0 </mixHash>
396396
<blockNonce> _ => 0 </blockNonce>
397397
<ommerBlockHeaders> _ => [ .JSONList ] </ommerBlockHeaders>
@@ -453,7 +453,7 @@ The individual fields of the accounts are dealt with here.
453453
...
454454
</account>
455455
456-
rule <k> load "account" : { ACCT : { "code" : (CODE:WordStack) } } => . ... </k>
456+
rule <k> load "account" : { ACCT : { "code" : (CODE:ByteArray) } } => . ... </k>
457457
<account>
458458
<acctID> ACCT </acctID>
459459
<code> _ => CODE </code>
@@ -507,9 +507,9 @@ Here we load the environmental information.
507507
508508
rule <k> load "exec" : { "data" : ((DATA:String) => #parseByteStack(DATA)) } ... </k>
509509
// -------------------------------------------------------------------------------------
510-
rule <k> load "exec" : { "data" : (DATA:WordStack) } => . ... </k> <callData> _ => DATA </callData>
510+
rule <k> load "exec" : { "data" : (DATA:ByteArray) } => . ... </k> <callData> _ => DATA </callData>
511511
rule <k> load "exec" : { "code" : (CODE:OpCodes) } => . ... </k> <program> _ => #asMapOpCodes(CODE) </program>
512-
rule <k> load "exec" : { "code" : (CODE:WordStack) } => . ... </k> <program> _ => #asMapOpCodes(#dasmOpCodes(CODE, SCHED)) </program> <programBytes> _ => CODE </programBytes> <schedule> SCHED </schedule>
512+
rule <k> load "exec" : { "code" : (CODE:ByteArray) } => . ... </k> <program> _ => #asMapOpCodes(#dasmOpCodes(CODE, SCHED)) </program> <programBytes> _ => CODE </programBytes> <schedule> SCHED </schedule>
513513
```
514514

515515
The `"network"` key allows setting the fee schedule inside the test.
@@ -618,16 +618,16 @@ The `"rlp"` key loads the block information.
618618
rule <k> load "transaction" : { TXID : { "to" : TT:Account } } => . ... </k>
619619
<message> <msgID> TXID </msgID> <to> _ => TT </to> ... </message>
620620
621-
rule <k> load "transaction" : { TXID : { "data" : TI:WordStack } } => . ... </k>
621+
rule <k> load "transaction" : { TXID : { "data" : TI:ByteArray } } => . ... </k>
622622
<message> <msgID> TXID </msgID> <data> _ => TI </data> ... </message>
623623
624624
rule <k> load "transaction" : { TXID : { "v" : TW:Int } } => . ... </k>
625625
<message> <msgID> TXID </msgID> <sigV> _ => TW </sigV> ... </message>
626626
627-
rule <k> load "transaction" : { TXID : { "r" : TR:WordStack } } => . ... </k>
627+
rule <k> load "transaction" : { TXID : { "r" : TR:ByteArray } } => . ... </k>
628628
<message> <msgID> TXID </msgID> <sigR> _ => TR </sigR> ... </message>
629629
630-
rule <k> load "transaction" : { TXID : { "s" : TS:WordStack } } => . ... </k>
630+
rule <k> load "transaction" : { TXID : { "s" : TS:ByteArray } } => . ... </k>
631631
<message> <msgID> TXID </msgID> <sigS> _ => TS </sigS> ... </message>
632632
```
633633

@@ -689,7 +689,7 @@ The `"rlp"` key loads the block information.
689689
</account>
690690
requires #removeZeros(ACCTSTORAGE) ==K STORAGE
691691
692-
rule <k> check "account" : { ACCT : { "code" : (CODE:WordStack) } } => . ... </k>
692+
rule <k> check "account" : { ACCT : { "code" : (CODE:ByteArray) } } => . ... </k>
693693
<account>
694694
<acctID> ACCT </acctID>
695695
<code> CODE </code>
@@ -731,7 +731,7 @@ Here we check the other post-conditions associated with an EVM test.
731731
732732
rule <k> check "blockHeader" : { KEY : (VALUE:String => #parseByteStack(VALUE)) } ... </k>
733733
734-
rule <k> check "blockHeader" : { KEY : (VALUE:WordStack => #asWord(VALUE)) } ... </k>
734+
rule <k> check "blockHeader" : { KEY : (VALUE:ByteArray => #asWord(VALUE)) } ... </k>
735735
requires KEY in ( SetItem("coinbase") SetItem("difficulty") SetItem("gasLimit") SetItem("gasUsed")
736736
SetItem("mixHash") SetItem("nonce") SetItem("number") SetItem("parentHash")
737737
SetItem("receiptTrie") SetItem("stateRoot") SetItem("timestamp")
@@ -754,7 +754,7 @@ Here we check the other post-conditions associated with an EVM test.
754754
rule <k> check "blockHeader" : { "transactionsTrie" : VALUE } => . ... </k> <transactionsRoot> VALUE </transactionsRoot>
755755
rule <k> check "blockHeader" : { "uncleHash" : VALUE } => . ... </k> <ommersHash> VALUE </ommersHash>
756756
757-
rule <k> check "blockHeader" : { "hash": HASH:WordStack } => . ...</k>
757+
rule <k> check "blockHeader" : { "hash": HASH:ByteArray } => . ...</k>
758758
<previousHash> HP </previousHash>
759759
<ommersHash> HO </ommersHash>
760760
<coinbase> HC </coinbase>
@@ -792,9 +792,9 @@ Here we check the other post-conditions associated with an EVM test.
792792
rule <k> check "transactions" : { KEY : VALUE , REST } => check "transactions" : (KEY : VALUE) ~> check "transactions" : { REST } ... </k>
793793
794794
rule <k> check "transactions" : (KEY : (VALUE:String => #parseByteStack(VALUE))) ... </k>
795-
rule <k> check "transactions" : ("to" : (VALUE:WordStack => #asAccount(VALUE))) ... </k>
796-
rule <k> check "transactions" : (KEY : (VALUE:WordStack => #padToWidth(32, VALUE))) ... </k> requires KEY in (SetItem("r") SetItem("s")) andBool #sizeWordStack(VALUE) <Int 32
797-
rule <k> check "transactions" : (KEY : (VALUE:WordStack => #asWord(VALUE))) ... </k> requires KEY in (SetItem("gasLimit") SetItem("gasPrice") SetItem("nonce") SetItem("v") SetItem("value"))
795+
rule <k> check "transactions" : ("to" : (VALUE:ByteArray => #asAccount(VALUE))) ... </k>
796+
rule <k> check "transactions" : (KEY : (VALUE:ByteArray => #padToWidth(32, VALUE))) ... </k> requires KEY in (SetItem("r") SetItem("s")) andBool #sizeByteArray(VALUE) <Int 32
797+
rule <k> check "transactions" : (KEY : (VALUE:ByteArray => #asWord(VALUE))) ... </k> requires KEY in (SetItem("gasLimit") SetItem("gasPrice") SetItem("nonce") SetItem("v") SetItem("value"))
798798
799799
rule <k> check "transactions" : ("data" : VALUE) => . ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <data> VALUE </data> ... </message>
800800
rule <k> check "transactions" : ("gasLimit" : VALUE) => . ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txGasLimit> VALUE </txGasLimit> ... </message>

‎edsl.md‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -44,15 +44,15 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of
4444
| #int128 ( Int )
4545
| #bytes32 ( Int )
4646
| #bool ( Int )
47-
| #bytes ( WordStack )
47+
| #bytes ( ByteArray )
4848
| #string ( String )
4949
| #array ( TypedArg , Int , TypedArgs )
5050
// -----------------------------------------------------------
5151
5252
syntax TypedArgs ::= List{TypedArg, ","} [klabel(typedArgs)]
5353
// ------------------------------------------------------------
5454
55-
syntax WordStack ::= #abiCallData ( String , TypedArgs ) [function]
55+
syntax ByteArray ::= #abiCallData ( String , TypedArgs ) [function]
5656
// -------------------------------------------------------------------
5757
rule #abiCallData( FNAME , ARGS )
5858
=> #parseByteStack(substrString(Keccak256(#generateSignature(FNAME, ARGS)), 0, 8))
@@ -83,8 +83,8 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of
8383
rule #typeName( #string( _ )) => "string"
8484
rule #typeName( #array(T, _, _)) => #typeName(T) +String "[]"
8585
86-
syntax WordStack ::= #encodeArgs ( TypedArgs ) [function]
87-
syntax WordStack ::= #encodeArgsAux ( TypedArgs , Int , WordStack , WordStack ) [function]
86+
syntax ByteArray ::= #encodeArgs ( TypedArgs ) [function]
87+
syntax ByteArray ::= #encodeArgsAux ( TypedArgs , Int , ByteArray , ByteArray ) [function]
8888
// ------------------------------------------------------------------------------------------
8989
rule #encodeArgs(ARGS) => #encodeArgsAux(ARGS, #lenOfHeads(ARGS), .WordStack, .WordStack)
9090
@@ -152,7 +152,7 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of
152152
153153
rule #sizeOfDynamicTypeAux(.TypedArgs) => 0
154154
155-
syntax WordStack ::= #enc ( TypedArg ) [function]
155+
syntax ByteArray ::= #enc ( TypedArg ) [function]
156156
// -------------------------------------------------
157157
// static Type
158158
rule #enc(#uint160( DATA )) => #buf(32, #getValue(#uint160( DATA )))
@@ -171,13 +171,13 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of
171171
rule #enc(#array(_, N, DATA)) => #enc(#uint256(N)) ++ #encodeArgs(DATA)
172172
rule #enc( #string(STR)) => #enc(#bytes(#parseByteStackRaw(STR)))
173173
174-
syntax WordStack ::= #encBytes ( Int , WordStack ) [function]
174+
syntax ByteArray ::= #encBytes ( Int , WordStack ) [function]
175175
// -------------------------------------------------------------
176176
rule #encBytes(N, WS) => #enc(#uint256(N)) ++ WS ++ #buf(#ceil32(N) -Int N, 0)
177177
178178
//Byte array buffer. Lemmas defined in evm-data-symbolic.k
179179
// SIZE, DATA // left zero padding
180-
syntax WordStack ::= #buf ( Int , Int ) [function, smtlib(buf)]
180+
syntax ByteArray ::= #buf ( Int , Int ) [function, smtlib(buf)]
181181
// ---------------------------------------------------------------
182182
183183
syntax Int ::= #getValue ( TypedArg ) [function]
@@ -278,7 +278,7 @@ where `1003892871367861763272476045097431689001461395759728643661426852242313133
278278
rule #getIndexedArgs(_:TypedArg, ES) => #getIndexedArgs(ES)
279279
rule #getIndexedArgs(.EventArgs) => .List
280280
281-
syntax WordStack ::= #getEventData ( EventArgs ) [function]
281+
syntax ByteArray ::= #getEventData ( EventArgs ) [function]
282282
// -----------------------------------------------------------
283283
rule #getEventData(#indexed(_), ES) => #getEventData(ES)
284284
rule #getEventData(E:TypedArg, ES) => #enc(E) ++ #getEventData(ES)
@@ -329,7 +329,7 @@ Specifically, `#hashedLocation` is defined as follows, capturing the storage lay
329329
// --------------------------------------------------
330330
rule keccakIntList(VS) => keccak(intList2ByteStack(VS)) [concrete]
331331
332-
syntax WordStack ::= intList2ByteStack( IntList ) [function]
332+
syntax ByteArray ::= intList2ByteStack( IntList ) [function]
333333
// ------------------------------------------------------------
334334
rule intList2ByteStack(.IntList) => .WordStack
335335
rule intList2ByteStack(V VS) => #padToWidth(32, #asByteStack(V)) ++ intList2ByteStack(VS)

‎evm-node.md‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ Because the same account may be loaded more than once, implementations of this i
5252
=> <account>
5353
<acctID> ACCT </acctID>
5454
<balance> #getBalance(ACCT) </balance>
55-
<code> #if #isCodeEmpty(ACCT) #then .WordStack #else #unloaded(#getCodeHash(ACCT)) #fi </code>
55+
<code> #if #isCodeEmpty(ACCT) #then .ByteArray #else #unloaded(#getCodeHash(ACCT)) #fi </code>
5656
<storage> .Map </storage>
5757
<origStorage> .Map </origStorage>
5858
<nonce> #getNonce(ACCT) </nonce>
@@ -110,7 +110,7 @@ Because the same account may be loaded more than once, implementations of this i
110110
rule <k> #lookupCode ACCT => . ... </k>
111111
<account>
112112
<acctID> ACCT </acctID>
113-
<code> _:WordStack </code>
113+
<code> _:ByteArray </code>
114114
...
115115
</account>
116116
@@ -206,7 +206,7 @@ Because the same account may be loaded more than once, implementations of this i
206206
// ----------------------------------------
207207
rule <statusCode> _:ExceptionalStatusCode </statusCode>
208208
<k> #halt ~> #endVM => #popCallStack ~> #popWorldState ~> 0 </k>
209-
<output> _ => .WordStack </output>
209+
<output> _ => .ByteArray </output>
210210
211211
rule <statusCode> EVMC_REVERT </statusCode>
212212
<k> #halt ~> #endVM => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 </k>

0 commit comments

Comments
 (0)