remove some nondeterminism in driver.md #22
Conversation
| @@ -547,7 +541,6 @@ Here we check the other post-conditions associated with an EVM test. | |||
|
|
|||
| rule <k> check TESTID : { "transactions" : TRANSACTIONS } => check "transactions" : TRANSACTIONS ~> failure TESTID ... </k> | |||
| // --------------------------------------------------------------------------------------------------------------------------- | |||
| rule <k> check "transactions" : [ .JSONs ] => .K ... </k> <txOrder> .List </txOrder> | |||
There was a problem hiding this comment.
Superceded by this rule: rule <k> check DATA : [ .JSONs ] => .K ... </k> requires DATA =/=String "ommerHeaders"
| @@ -536,9 +533,6 @@ Here we check the other post-conditions associated with an EVM test. | |||
|
|
|||
| rule check TESTID : { "genesisBlockHeader" : BLOCKHEADER } => check "genesisBlockHeader" : BLOCKHEADER ~> failure TESTID | |||
| // ------------------------------------------------------------------------------------------------------------------------ | |||
| rule <k> check "genesisBlockHeader" : { KEY : VALUE , REST } => check "genesisBlockHeader" : { KEY : VALUE } ~> check "genesisBlockHeader" : { REST } ... </k> | |||
There was a problem hiding this comment.
Superceded by this rule: rule <k> check DATA : { (KEY:String) : VALUE , REST } => check DATA : { KEY : VALUE } ~> check DATA : { REST } ... </k> requires REST =/=K .JSONs andBool notBool DATA in (SetItem("callcreates") SetItem("transactions"))
| @@ -473,9 +473,6 @@ Here we check the other post-conditions associated with an EVM test. | |||
|
|
|||
| rule check TESTID : { "blockHeader" : BLOCKHEADER } => check "blockHeader" : BLOCKHEADER ~> failure TESTID | |||
| // ---------------------------------------------------------------------------------------------------------- | |||
| rule <k> check "blockHeader" : { KEY : VALUE , REST } => check "blockHeader" : { KEY : VALUE } ~> check "blockHeader" : { REST } ... </k> | |||
There was a problem hiding this comment.
Superceded by this rule: rule <k> check DATA : { (KEY:String) : VALUE , REST } => check DATA : { KEY : VALUE } ~> check DATA : { REST } ... </k> requires REST =/=K .JSONs andBool notBool DATA in (SetItem("callcreates") SetItem("transactions"))
There was a problem hiding this comment.
Looks good! Approved!
One minor note: the rule deleted on line 476 was clearly intended to constrain the test configuration in a way that the replacement rule does not.
That said, I don't know if the deleted rule ever effectively constrained anything --- due to its overlap with the replacement rule --- which does not have the constraint.
For completeness, the intended constraint was:
The number of JSON objects in the transactions array in the JSON blob should be the same as the number of list elements in the <txOrder> cell.
There are a few rules in driver.md that conflict with each other or which conflict with rules in state-utils.md. It is pretty straightforward to modify the semantics so that this is no longer the case. We do this in order to test that the EVM semantics is actually 100% deterministic (which it is).
There are a few rules in driver.md that conflict with each other or which conflict with rules in state-utils.md. It is pretty straightforward to modify the semantics so that this is no longer the case. We do this in order to test that the EVM semantics is actually 100% deterministic (which it is).
There are a few rules in driver.md that conflict with each other or which conflict with rules in state-utils.md. It is pretty straightforward to modify the semantics so that this is no longer the case. We do this in order to test that the EVM semantics is actually 100% deterministic (which it is).
There are a few rules in driver.md that conflict with each other or which conflict with rules in state-utils.md. It is pretty straightforward to modify the semantics so that this is no longer the case. We do this in order to test that the EVM semantics is actually 100% deterministic (which it is).
There are a few rules in driver.md that conflict with each other or which conflict with rules in state-utils.md. It is pretty straightforward to modify the semantics so that this is no longer the case. We do this in order to test that the EVM semantics is actually 100% deterministic (which it is).
There are a few rules in driver.md that conflict with each other or which conflict with rules in state-utils.md. It is pretty straightforward to modify the semantics so that this is no longer the case. We do this in order to test that the EVM semantics is actually 100% deterministic (which it is).