Skip to content

Commit 0689688

Browse files
rv-auditorrv-auditor
committed
Merge remote-tracking branch 'origin/master' into release
2 parents 9b29a04 + 1e4dda8 commit 0689688

File tree

8 files changed

+159
-236
lines changed

8 files changed

+159
-236
lines changed

‎kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md‎

Lines changed: 50 additions & 55 deletions
Original file line numberDiff line numberDiff line change
@@ -380,33 +380,28 @@ Processing SetCode Transaction Authority Entries
380380
rule <statusCode> _:ExceptionalStatusCode </statusCode>
381381
<k> exception ~> clear => clear ... </k>
382382
383-
syntax EthereumCommand ::= "failure" String | "success"
384-
// -------------------------------------------------------
383+
syntax EthereumCommand ::= "success"
384+
// ------------------------------------
385385
rule <k> success => .K ... </k>
386386
<exit-code> _ => 0 </exit-code>
387387
<mode> _ => SUCCESS </mode>
388-
389-
rule <k> failure _ => .K ... </k>
390-
rule <k> #halt ~> failure _ => .K ... </k>
388+
rule <k> (#halt => .K) ~> success ... </k>
391389
```
392390

393391
### Running Tests
394392

395393
- `run` runs a given set of Ethereum tests (from the test-set).
396394

397-
Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`.
398-
399395
```k
400396
syntax EthereumCommand ::= "run" JSON
401-
// -------------------------------------
402-
rule <k> run { .JSONs } => .K ... </k>
403-
rule <k> run { TESTID : { TEST:JSONs } , TESTS }
404-
=> run ( TESTID : { TEST } )
405-
~> #if #hasPost?( { TEST } ) #then .K #else exception #fi
406-
~> clear
407-
~> run { TESTS }
408-
...
409-
</k>
397+
// --------------------------------------
398+
rule <k> run { .JSONs } => .K ... </k>
399+
rule <k> run { TESTID : { TEST:JSONs } } => run { TEST }
400+
~> #if #hasPost?( { TEST } ) #then .K #else exception #fi
401+
~> clear
402+
...
403+
</k>
404+
requires notBool TESTID in (#loadKeys #execKeys #checkKeys)
410405
411406
syntax Bool ::= "#hasPost?" "(" JSON ")" [function]
412407
// ---------------------------------------------------
@@ -421,7 +416,7 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
421416
// -------------------------------------
422417
rule #loadKeys => ( SetItem("env") SetItem("pre") SetItem("rlp") SetItem("genesisRLP") )
423418
424-
rule <k> run TESTID : { KEY : (VAL:JSON) , REST } => load KEY : VAL ~> run TESTID : { REST } ... </k>
419+
rule <k> run { KEY : (VAL:JSON) , REST } => load KEY : VAL ~> run { REST } ... </k>
425420
requires KEY in #loadKeys
426421
```
427422

@@ -432,31 +427,31 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
432427
// -------------------------------------
433428
rule #execKeys => ( SetItem("exec") SetItem("blocks") )
434429
435-
rule <k> run TESTID : { KEY : (VAL:JSON) , NEXT , REST } => run TESTID : { NEXT , KEY : VAL , REST } ... </k>
430+
rule <k> run { KEY : (VAL:JSON) , NEXT , REST } => run { NEXT , KEY : VAL , REST } ... </k>
436431
requires KEY in #execKeys
437432
438-
rule <k> run TESTID : { "blocks" : [ { BLOCK }, BLOCKS ] } => clearTX ~> clearBLOCK ~> process TESTID : { BLOCK } ~> run TESTID : { "blocks" : [ BLOCKS ] } ... </k>
439-
rule <k> run _TESTID : { "blocks" : [ .JSONs ] } => .K ... </k>
433+
rule <k> run { "blocks" : [ { BLOCK }, BLOCKS ] } => clearTX ~> clearBLOCK ~> process { BLOCK } ~> run { "blocks" : [ BLOCKS ] } ... </k>
434+
rule <k> run { "blocks" : [ .JSONs ] } => .K ... </k>
440435
441436
syntax EthereumCommand ::= "process" JSON
442437
// -----------------------------------------
443-
rule <k> process TESTID : { "expectException" : _ , REST } => exception ~> process TESTID : { REST } ... </k>
438+
rule <k> process { "expectException" : _ , REST } => exception ~> process { REST } ... </k>
444439
445-
rule <k> exception ~> process _TESTID : { "rlp_decoded" : { KEY : VAL , REST1 => REST1 }, (REST2 => KEY : VAL , REST2 ) } ... </k>
446-
rule <k> exception ~> process _TESTID : { "rlp_decoded" : { .JSONs } , REST => REST} ... </k>
440+
rule <k> exception ~> process { "rlp_decoded" : { KEY : VAL , REST1 => REST1 }, (REST2 => KEY : VAL , REST2 ) } ... </k>
441+
rule <k> exception ~> process { "rlp_decoded" : { .JSONs } , REST => REST} ... </k>
447442
448-
rule <k> exception ~> process TESTID : { KEY : VAL , REST } => load KEY : VAL ~> exception ~> process TESTID : { REST } ... </k> requires KEY in #loadKeys
449-
rule <k> exception ~> process TESTID : { KEY : VAL , REST } => exception ~> process TESTID : { REST } ~> check TESTID : {KEY : VAL} ... </k> requires KEY in #checkKeys
450-
rule <k> exception ~> process _TESTID : { .JSONs } => #startBlock ~> startTx ~> exception ... </k>
443+
rule <k> exception ~> process { KEY : VAL , REST } => load KEY : VAL ~> exception ~> process { REST } ... </k> requires KEY in #loadKeys
444+
rule <k> exception ~> process { KEY : VAL , REST } => exception ~> process { REST } ~> check {KEY : VAL} ... </k> requires KEY in #checkKeys
445+
rule <k> exception ~> process { .JSONs } => #startBlock ~> startTx ~> exception ... </k>
451446
452-
rule <k> process _TESTID : { "rlp_decoded" : { KEY : VAL , REST1 => REST1 }, (REST2 => KEY : VAL , REST2 ) } ... </k>
453-
rule <k> process _TESTID : { "rlp_decoded" : { .JSONs } , REST => REST} ... </k>
447+
rule <k> process { "rlp_decoded" : { KEY : VAL , REST1 => REST1 }, (REST2 => KEY : VAL , REST2 ) } ... </k>
448+
rule <k> process { "rlp_decoded" : { .JSONs } , REST => REST} ... </k>
454449
455-
rule <k> process TESTID : { KEY : VAL , REST } => load KEY : VAL ~> process TESTID : { REST } ... </k> requires KEY in #loadKeys
456-
rule <k> process TESTID : { KEY : VAL , REST } => process TESTID : { REST } ~> check TESTID : {KEY : VAL} ... </k> requires KEY in #checkKeys
457-
rule <k> process _TESTID : { .JSONs } => #startBlock ~> startTx ... </k>
450+
rule <k> process { KEY : VAL , REST } => load KEY : VAL ~> process { REST } ... </k> requires KEY in #loadKeys
451+
rule <k> process { KEY : VAL , REST } => process { REST } ~> check {KEY : VAL} ... </k> requires KEY in #checkKeys
452+
rule <k> process { .JSONs } => #startBlock ~> startTx ... </k>
458453
459-
rule <k> run _TESTID : { "exec" : (EXEC:JSON) } => loadCallState EXEC ~> start ~> flush ... </k>
454+
rule <k> run { "exec" : (EXEC:JSON) } => loadCallState EXEC ~> start ~> flush ... </k>
460455
461456
rule <k> load "exec" : J => loadCallState J ... </k>
462457
@@ -490,8 +485,8 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
490485
SetItem("genesisBlockHeader") SetItem("withdrawals") SetItem("blocknumber")
491486
)
492487
493-
rule <k> run TESTID : { KEY : (VAL:JSON) , REST } => run TESTID : { REST } ~> check TESTID : { "post" : VAL } ... </k> requires KEY in #allPostKeys
494-
rule <k> run TESTID : { KEY : (VAL:JSON) , REST } => run TESTID : { REST } ~> check TESTID : { KEY : VAL } ... </k> requires KEY in #checkKeys andBool notBool KEY in #allPostKeys
488+
rule <k> run { KEY : (VAL:JSON) , REST } => run { REST } ~> check { "post" : VAL } ... </k> requires KEY in #allPostKeys
489+
rule <k> run { KEY : (VAL:JSON) , REST } => run { REST } ~> check { KEY : VAL } ... </k> requires KEY in #checkKeys andBool notBool KEY in #allPostKeys
495490
```
496491

497492
- `driver.md` specific handling of state-utils commands
@@ -540,8 +535,8 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
540535
rule <k> check (KEY:String) : { JS:JSONs => qsortJSONs(JS) } ... </k>
541536
requires KEY in (SetItem("callcreates")) andBool notBool sortedJSONs(JS)
542537
543-
rule <k> check TESTID : { "post" : (POST:String) } => check "blockHeader" : { "stateRoot" : #parseWord(POST) } ~> failure TESTID ... </k>
544-
rule <k> check TESTID : { "post" : { POST } } => check "account" : { POST } ~> failure TESTID ... </k>
538+
rule <k> check { "post" : (POST:String) } => check "blockHeader" : { "stateRoot" : #parseWord(POST) } ... </k>
539+
rule <k> check { "post" : { POST } } => check "account" : { POST } ... </k>
545540
546541
rule <k> check "account" : { ACCTID:Int : { KEY : VALUE , REST } } => check "account" : { ACCTID : { KEY : VALUE } } ~> check "account" : { ACCTID : { REST } } ... </k>
547542
requires REST =/=K .JSONs
@@ -602,22 +597,22 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
602597
Here we check the other post-conditions associated with an EVM test.
603598

604599
```k
605-
rule <k> check TESTID : { "out" : OUT } => check "out" : OUT ~> failure TESTID ... </k>
606-
// ---------------------------------------------------------------------------------------
600+
rule <k> check { "out" : OUT } => check "out" : OUT ... </k>
601+
// ------------------------------------------------------------
607602
rule <k> check "out" : ((OUT:String) => #parseByteStack(OUT)) ... </k>
608603
rule <k> check "out" : OUT => .K ... </k> <output> OUT </output>
609604
610-
rule <k> check TESTID : { "logs" : LOGS } => check "logs" : LOGS ~> failure TESTID ... </k>
611-
// -------------------------------------------------------------------------------------------
605+
rule <k> check { "logs" : LOGS } => check "logs" : LOGS ... </k>
606+
// ----------------------------------------------------------------
612607
rule <k> check "logs" : HASH:String => .K ... </k> <log> SL </log> requires #parseHexBytes(Keccak256(#rlpEncodeLogs(SL))) ==K #parseByteStack(HASH)
613608
614-
rule <k> check TESTID : { "gas" : GLEFT } => check "gas" : GLEFT ~> failure TESTID ... </k>
615-
// -------------------------------------------------------------------------------------------
609+
rule <k> check { "gas" : GLEFT } => check "gas" : GLEFT ... </k>
610+
// ----------------------------------------------------------------
616611
rule <k> check "gas" : ((GLEFT:String) => #parseWord(GLEFT)) ... </k>
617612
rule <k> check "gas" : GLEFT => .K ... </k> <gas> GLEFT </gas>
618613
619-
rule check TESTID : { "blockHeader" : BLOCKHEADER } => check "blockHeader" : BLOCKHEADER ~> failure TESTID
620-
// ----------------------------------------------------------------------------------------------------------
614+
rule <k> check { "blockHeader" : BLOCKHEADER } => check "blockHeader" : BLOCKHEADER ... </k>
615+
// -------------------------------------------------------------------------------------------
621616
rule <k> check "blockHeader" : { KEY : VALUE , REST } => check "blockHeader" : { KEY : VALUE } ~> check "blockHeader" : { REST } ... </k>
622617
requires REST =/=K .JSONs
623618
@@ -682,8 +677,8 @@ Here we check the other post-conditions associated with an EVM test.
682677
orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR, UB, EB, BR) ==Int #asWord(HASH)
683678
orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR, UB, EB, BR, RR) ==Int #asWord(HASH)
684679
685-
rule check TESTID : { "genesisBlockHeader" : BLOCKHEADER } => check "genesisBlockHeader" : BLOCKHEADER ~> failure TESTID
686-
// ------------------------------------------------------------------------------------------------------------------------
680+
rule <k> check { "genesisBlockHeader" : BLOCKHEADER } => check "genesisBlockHeader" : BLOCKHEADER ... </k>
681+
// ---------------------------------------------------------------------------------------------------------
687682
rule <k> check "genesisBlockHeader" : { KEY : VALUE , REST } => check "genesisBlockHeader" : { KEY : VALUE } ~> check "genesisBlockHeader" : { REST } ... </k>
688683
requires REST =/=K .JSONs
689684
@@ -693,8 +688,8 @@ Here we check the other post-conditions associated with an EVM test.
693688
rule <k> check "genesisBlockHeader" : { "hash": HASH } => .K ... </k>
694689
<blockhashes> ... ListItem(HASH) ListItem(_) </blockhashes>
695690
696-
rule <k> check TESTID : { "transactions" : TRANSACTIONS } => check "transactions" : TRANSACTIONS ~> failure TESTID ... </k>
697-
// ---------------------------------------------------------------------------------------------------------------------------
691+
rule <k> check { "transactions" : TRANSACTIONS } => check "transactions" : TRANSACTIONS ... </k>
692+
// ------------------------------------------------------------------------------------------------
698693
rule <k> check "transactions" : [ .JSONs ] => .K ... </k> <txOrder> .List </txOrder>
699694
rule <k> check "transactions" : { .JSONs } => .K ... </k> <txOrder> ListItem(_) => .List ... </txOrder>
700695
@@ -759,7 +754,7 @@ Here we check the other post-conditions associated with an EVM test.
759754
760755
syntax Bool ::= isInAccessListStorage ( Int , JSON ) [symbol(isInAccessListStorage), function]
761756
| isInAccessList ( Account , Int , JSON ) [symbol(isInAccessList), function]
762-
// -------------------------------------------------------------------------------------------------
757+
// ------------------------------------------------------------------------------------------
763758
rule isInAccessList(_ , _ , [.JSONs ]) => false
764759
rule isInAccessList(ADDR, KEY, [[ACCT, [STRG:JSONs]], REST]) => #if ADDR ==K #asAccount(ACCT)
765760
#then isInAccessListStorage (KEY, [STRG]) orBool isInAccessList(ADDR, KEY, [REST])
@@ -774,14 +769,14 @@ Here we check the other post-conditions associated with an EVM test.
774769
TODO: case with nonzero ommers.
775770

776771
```k
777-
rule <k> check TESTID : { "uncleHeaders" : OMMERS } => check "ommerHeaders" : OMMERS ~> failure TESTID ... </k>
778-
// ---------------------------------------------------------------------------------------------------------------
772+
rule <k> check { "uncleHeaders" : OMMERS } => check "ommerHeaders" : OMMERS ... </k>
773+
// ------------------------------------------------------------------------------------
779774
rule <k> check "ommerHeaders" : [ .JSONs ] => .K ... </k> <ommerBlockHeaders> [ .JSONs ] </ommerBlockHeaders>
780775
```
781776

782777
```k
783-
rule <k> check TESTID : {"withdrawals" : WITHDRAWALS } => check "withdrawals" : WITHDRAWALS ~> failure TESTID ... </k>
784-
// ----------------------------------------------------------------------------------------------------------------------
778+
rule <k> check { "withdrawals" : WITHDRAWALS } => check "withdrawals" : WITHDRAWALS ... </k>
779+
// --------------------------------------------------------------------------------------------
785780
rule <k> check "withdrawals" : [ .JSONs ] => .K ... </k> <withdrawalsOrder> .List </withdrawalsOrder>
786781
rule <k> check "withdrawals" : { .JSONs } => .K ... </k> <withdrawalsOrder> ListItem(_) => .List ... </withdrawalsOrder>
787782
@@ -799,8 +794,8 @@ TODO: case with nonzero ommers.
799794
```
800795

801796
```k
802-
rule <k> check TESTID : { "blocknumber": BN } => check "blocknumber" : BN ~> failure TESTID ... </k>
803-
// ----------------------------------------------------------------------------------------------------
797+
rule <k> check { "blocknumber": BN } => check "blocknumber" : BN ... </k>
798+
// -------------------------------------------------------------------------
804799
rule <k> check "blocknumber" : (VALUE:String => #parseWord(VALUE)) ... </k>
805800
rule <k> check "blocknumber" : BN => .K ... </k> <number> BN </number>
806801
```

0 commit comments

Comments
 (0)