@@ -41,7 +41,7 @@ For verification purposes, it's much easier to specify a program in terms of its
4141To 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
515515The ` "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>
0 commit comments