evm, driver, tests/{*.out,proofs}: remove <callLog> cell for VMTests mode, disable checking callcreates keys

Author: Everett Hildenbrandt

driver.md

@@ -315,7 +315,7 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
  // -------------------------------------------------------------------------------------------
     rule #postKeys    => ( SetItem("post") SetItem("postState") )
     rule #allPostKeys => ( #postKeys SetItem("expect") SetItem("export") SetItem("expet") )
-    rule #checkKeys   => ( #allPostKeys SetItem("logs") SetItem("callcreates") SetItem("out") SetItem("gas")
+    rule #checkKeys   => ( #allPostKeys SetItem("logs") SetItem("out") SetItem("gas")
                            SetItem("blockHeader") SetItem("transactions") SetItem("uncleHeaders") SetItem("genesisBlockHeader")
                          )
 
@@ -328,7 +328,7 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
 ```{.k .standalone}
     syntax Set ::= "#discardKeys" [function]
  // ----------------------------------------
-    rule #discardKeys => ( SetItem("//") SetItem("_info") )
+    rule #discardKeys => ( SetItem("//") SetItem("_info") SetItem("callcreates") )
 
     rule <k> run TESTID : { KEY : _ , REST } => run TESTID : { REST } ... </k> requires KEY in #discardKeys
 ```
@@ -354,7 +354,6 @@ State Manipulation
          <memoryUsed>      _ => 0          </memoryUsed>
          <callDepth>       _ => 0          </callDepth>
          <callStack>       _ => .List      </callStack>
-         <callLog>         _ => .Set       </callLog>
          <program>         _ => .Map       </program>
          <programBytes>    _ => .WordStack </programBytes>
          <id>              _ => 0          </id>
@@ -718,14 +717,6 @@ Here we check the other post-conditions associated with an EVM test.
     rule <k> check "gas" : ((GLEFT:String) => #parseWord(GLEFT)) ... </k>
     rule <k> check "gas" : GLEFT => . ... </k> <gas> GLEFT </gas>
 
-    rule <k> check TESTID : { "callcreates" : CCREATES } => check "callcreates" : CCREATES ~> failure TESTID ... </k>
- // -----------------------------------------------------------------------------------------------------------------
-    rule <k> check "callcreates" : { ("data" : (DATA:String)) , ("destination" : (ACCTTO:String)) , ("gasLimit" : (GLIMIT:String)) , ("value" : (VAL:String)) , .JSONList }
-          => check "callcreates" : { #parseAddr(ACCTTO) | #parseWord(GLIMIT) | #parseWord(VAL) | #parseByteStack(DATA) }
-         ...
-         </k>
-    rule <k> check "callcreates" : C:Call => . ... </k> <callLog> CL </callLog> requires C in CL
-
     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>

evm.md

@@ -45,7 +45,6 @@ In the comments next to each cell, we've marked which component of the YellowPap
           <output>          .WordStack </output>            // H_RETURN
           <callStack>       .List      </callStack>
           <interimStates>   .List      </interimStates>
-          <callLog>         .Set       </callLog>
           <touchedAccounts> .Set       </touchedAccounts>
 
           <callState>

tests/interactive/gas-analysis/sumTo10.evm.out

@@ -29,9 +29,6 @@
       <interimStates>
         .List
       </interimStates>
-      <callLog>
-        .Set
-      </callLog>
       <touchedAccounts>
         .Set
       </touchedAccounts>

tests/proofs

@@ -25,9 +25,6 @@
       <interimStates>
         .List
       </interimStates>
-      <callLog>
-        .Set
-      </callLog>
       <touchedAccounts>
         .Set
       </touchedAccounts>