From 54dfbc00849e3e4619aa75cbc4fa4aab53479e40 Mon Sep 17 00:00:00 2001
From: Dwight Guth <dwight.guth@pi2.network>
Date: Mon, 2 Dec 2024 13:26:47 -0600
Subject: [PATCH] remove some nondeterminism in driver.md (#22)

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).
---
 kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md      | 7 -------
 kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md | 2 ++
 2 files changed, 2 insertions(+), 7 deletions(-)

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
index 0caa9574ff..745e50f037 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
@@ -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>
-      requires REST =/=K .JSONs
-
     rule <k> check "blockHeader" : { _KEY : (VALUE:String => #parseByteStack(VALUE)) } ... </k>
 
     rule <k> check "blockHeader" : {  KEY : (VALUE:Bytes => #asWord(VALUE)) } ... </k>
@@ -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>
-      requires REST =/=K .JSONs
-
     rule <k> check "genesisBlockHeader" : { KEY : _ } => .K ... </k> requires KEY =/=String "hash"
 
     rule <k> check "genesisBlockHeader" : { "hash": (HASH:String => #asWord(#parseByteStack(HASH))) } ... </k>
@@ -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>
     rule <k> check "transactions" : { .JSONs } => .K ... </k> <txOrder> ListItem(_) => .List ... </txOrder>
 
     rule <k> check "transactions" : [ TRANSACTION , REST ] => check "transactions" : TRANSACTION   ~> check "transactions" : [ REST ] ... </k>
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md
index f3e53c7b90..bd5ac3807e 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md
@@ -336,9 +336,11 @@ The `"rlp"` key loads the block information.
 
     rule <k> loadTransaction TXID { "r" : TR:Bytes, REST => REST } ... </k>
          <message> <msgID> TXID </msgID> <sigR> _ => TR </sigR> ... </message>
+      requires lengthBytes(TR) ==Int 32
 
     rule <k> loadTransaction TXID { "s" : TS:Bytes, REST => REST } ... </k>
          <message> <msgID> TXID </msgID> <sigS> _ => TS </sigS> ... </message>
+      requires lengthBytes(TS) ==Int 32
 
     rule <k> loadTransaction TXID { "type" : T:Int, REST => REST } ... </k>
          <message> <msgID> TXID </msgID> <txType> _ => #asmTxPrefix(T) </txType> ... </message>