Compute log bloom and gas used (#453)

* data, driver, krypto, web3: add Int to JSON type in data.md * data: M3:2048 function * driver, evm: move block finalization to evm.md * evm: bloom filter function * driver, evm: actually compute gas used and logs bloom * data: don't use #fun * data: better naming of bloom filter stuff
runtimeverification · Aug 22, 2019 · d938b30 · d938b30
1 parent 133d028
commit d938b30
Show file tree

Hide file tree

Showing 5 changed files with 90 additions and 44 deletions.
diff --git a/data.md b/data.md
@@ -29,7 +29,7 @@ Writing a JSON-ish parser in K takes 6 lines.
 ```k
     syntax JSONList ::= List{JSON,","}
     syntax JSONKey  ::= String | Int
-    syntax JSON     ::= String
+    syntax JSON     ::= String | Int
                       | JSONKey ":" JSON
                       | "{" JSONList "}"
                       | "[" JSONList "]"
@@ -655,6 +655,22 @@ Addresses
 
 ```
 
+- `M3:2048` computes the 2048-bit hash of a log entry in which exactly 3 bits are set. This is used to compute the Bloom filter of a log entry.
+
+```k
+    syntax Int ::= "M3:2048" "(" ByteArray ")" [function]
+ // -----------------------------------------------------
+    rule M3:2048(WS) => setBloomFilterBits(#parseByteStack(Keccak256(#unparseByteStack(WS))))
+
+    syntax Int ::= setBloomFilterBits(ByteArray) [function]
+ // -------------------------------------------------------
+    rule setBloomFilterBits(HASH) => (1 <<Int getBloomFilterBit(HASH, 0)) |Int (1 <<Int getBloomFilterBit(HASH, 2)) |Int (1 <<Int getBloomFilterBit(HASH, 4))
+
+    syntax Int ::= getBloomFilterBit(ByteArray, Int) [function]
+ // -----------------------------------------------------------
+    rule getBloomFilterBit(X, I) => #asInteger(X [ I .. 2 ]) %Int 2048
+```
+
 Word Map
 --------
 

diff --git a/driver.md b/driver.md
@@ -43,8 +43,8 @@ For verification purposes, it's much easier to specify a program in terms of its
 To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a "pretti-fication" to the nicer input form.
 
 ```{.k .standalone}
-    syntax JSON ::= Int | ByteArray | OpCodes | Map | Call | SubstateLogEntry | Account
- // -----------------------------------------------------------------------------------
+    syntax JSON ::= ByteArray | OpCodes | Map | Call | SubstateLogEntry | Account
+ // -----------------------------------------------------------------------------
 
     syntax JSONList ::= #sortJSONList ( JSONList )            [function]
                       | #sortJSONList ( JSONList , JSONList ) [function, klabel(#sortJSONListAux)]
@@ -202,44 +202,6 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
       requires TT =/=K .Account
 ```
 
--   `#finalizeBlock` is used to signal that block finalization procedures should take place (after transactions have executed).
--   `#rewardOmmers(_)` pays out the reward to uncle blocks so that blocks are orphaned less often in Ethereum.
-
-```{.k .standalone}
-    syntax EthereumCommand ::= "#finalizeBlock" | #rewardOmmers ( JSONList )
- // ------------------------------------------------------------------------
-    rule <k> #finalizeBlock => #rewardOmmers(OMMERS) ... </k>
-         <schedule> SCHED </schedule>
-         <ommerBlockHeaders> [ OMMERS ] </ommerBlockHeaders>
-         <coinbase> MINER </coinbase>
-         <account>
-           <acctID> MINER </acctID>
-           <balance> MINBAL => MINBAL +Int Rb < SCHED > </balance>
-           ...
-         </account>
-
-    rule <k> (.K => #newAccount MINER) ~> #finalizeBlock ... </k>
-         <coinbase> MINER </coinbase>
-         <activeAccounts> ACCTS </activeAccounts>
-      requires notBool MINER in ACCTS
-
-    rule <k> #rewardOmmers(.JSONList) => . ... </k>
-    rule <k> #rewardOmmers([ _ , _ , OMMER , _ , _ , _ , _ , _ , OMMNUM , _ ] , REST) => #rewardOmmers(REST) ... </k>
-         <schedule> SCHED </schedule>
-         <coinbase> MINER </coinbase>
-         <number> CURNUM </number>
-         <account>
-           <acctID> MINER </acctID>
-           <balance> MINBAL => MINBAL +Int Rb < SCHED > /Int 32 </balance>
-          ...
-         </account>
-         <account>
-           <acctID> OMMER </acctID>
-           <balance> OMMBAL => OMMBAL +Int Rb < SCHED > +Int (OMMNUM -Int CURNUM) *Int (Rb < SCHED > /Int 8) </balance>
-          ...
-         </account>
-```
-
 -   `exception` only clears from the `<k>` cell if there is an exception preceding it.
 -   `failure_` holds the name of a test that failed if a test does fail.
 -   `success` sets the `<exit-code>` to `0` and the `<mode>` to `SUCCESS`.
@@ -311,7 +273,7 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
       requires KEY in #execKeys
 
     rule <k> run TESTID : { "exec" : (EXEC:JSON) } => load "exec" : EXEC ~> start ~> flush ... </k>
-    rule <k> run TESTID : { "lastblockhash" : (HASH:String) } => startTx                   ... </k>
+    rule <k> run TESTID : { "lastblockhash" : (HASH:String) } => #startBlock ~> startTx    ... </k>
 ```
 
 -   `#postKeys` are a subset of `#checkKeys` which correspond to post-state account checks.

diff --git a/evm.md b/evm.md
@@ -576,6 +576,7 @@ After executing a transaction, it's necessary to have the effect of the substate
          <origin> ORG </origin>
          <coinbase> MINER </coinbase>
          <gas> GAVAIL </gas>
+         <gasUsed> GUSED => GUSED +Int GLIMIT -Int GAVAIL </gasUsed>
          <refund> 0 </refund>
          <account>
            <acctID> ORG </acctID>
@@ -599,6 +600,8 @@ After executing a transaction, it's necessary to have the effect of the substate
     rule <k> #finalizeTx(false => true) ... </k>
          <origin> ACCT </origin>
          <coinbase> ACCT </coinbase>
+         <gas> GAVAIL </gas>
+         <gasUsed> GUSED => GUSED +Int GLIMIT -Int GAVAIL </gasUsed>
          <refund> 0 </refund>
          <account>
            <acctID> ACCT </acctID>
@@ -632,6 +635,71 @@ After executing a transaction, it's necessary to have the effect of the substate
     rule <k> #deleteAccounts(.List) => . ... </k>
 ```
 
+### Block processing
+
+-   `#startBlock` is used to signal that we are about to start mining a block and block initialization should take place (before transactions are executed).
+-   `#finalizeBlock` is used to signal that block finalization procedures should take place (after transactions have executed).
+-   `#rewardOmmers(_)` pays out the reward to uncle blocks so that blocks are orphaned less often in Ethereum.
+
+```{.k .standalone}
+    syntax EthereumCommand ::= "#startBlock"
+ // ----------------------------------------
+    rule <k> #startBlock => . ... </k>
+         <gasUsed> _ => 0 </gasUsed>
+         <log> _ => .List </log>
+         <logsBloom> _ => #padToWidth(256, .ByteArray) </logsBloom>
+
+    syntax EthereumCommand ::= "#finalizeBlock" | #rewardOmmers ( JSONList )
+ // ------------------------------------------------------------------------
+    rule <k> #finalizeBlock => #rewardOmmers(OMMERS) ... </k>
+         <schedule> SCHED </schedule>
+         <ommerBlockHeaders> [ OMMERS ] </ommerBlockHeaders>
+         <coinbase> MINER </coinbase>
+         <account>
+           <acctID> MINER </acctID>
+           <balance> MINBAL => MINBAL +Int Rb < SCHED > </balance>
+           ...
+         </account>
+         <log> LOGS </log>
+         <logsBloom> _ => #bloomFilter(LOGS) </logsBloom>
+
+    rule <k> (.K => #newAccount MINER) ~> #finalizeBlock ... </k>
+         <coinbase> MINER </coinbase>
+         <activeAccounts> ACCTS </activeAccounts>
+      requires notBool MINER in ACCTS
+
+    rule <k> #rewardOmmers(.JSONList) => . ... </k>
+    rule <k> #rewardOmmers([ _ , _ , OMMER , _ , _ , _ , _ , _ , OMMNUM , _ ] , REST) => #rewardOmmers(REST) ... </k>
+         <schedule> SCHED </schedule>
+         <coinbase> MINER </coinbase>
+         <number> CURNUM </number>
+         <account>
+           <acctID> MINER </acctID>
+           <balance> MINBAL => MINBAL +Int Rb < SCHED > /Int 32 </balance>
+          ...
+         </account>
+         <account>
+           <acctID> OMMER </acctID>
+           <balance> OMMBAL => OMMBAL +Int Rb < SCHED > +Int (OMMNUM -Int CURNUM) *Int (Rb < SCHED > /Int 8) </balance>
+          ...
+         </account>
+
+    syntax ByteArray ::= #bloomFilter(List)      [function]
+                       | #bloomFilter(List, Int) [function, klabel(#bloomFilterAux)]
+ // --------------------------------------------------------------------------------
+    rule #bloomFilter(L) => #bloomFilter(L, 0)
+
+    rule #bloomFilter(.List, B) => #padToWidth(256, #asByteStack(B))
+    rule #bloomFilter(ListItem({ ACCT | TOPICS | _ }) L, B) => #bloomFilter(ListItem(#padToWidth(20, #asByteStack(ACCT))) listAsByteArrays(TOPICS) L, B)
+
+    syntax List ::= listAsByteArrays(List) [function]
+ // -------------------------------------------------
+    rule listAsByteArrays(.List) => .List
+    rule listAsByteArrays(ListItem(TOPIC) L) => ListItem(#padToWidth(32, #asByteStack(TOPIC))) listAsByteArrays(L)
+
+    rule #bloomFilter(ListItem(WS:ByteArray) L, B) => #bloomFilter(L, B |Int M3:2048(WS))
+```
+
 EVM Programs
 ============
 

diff --git a/krypto.md b/krypto.md
@@ -36,7 +36,7 @@ The BN128 elliptic curve is defined over 2-dimensional points over the fields of
 -   `isValidPoint` takes a point in either G1 or G2 and validates that it actually falls on the respective elliptic curve.
 
 ```k
-    syntax G1Point ::= "(" Int "," Int ")"
+    syntax G1Point ::= "(" Int "," Int ")" [prefer]
     syntax G2Point ::= "(" Int "x" Int "," Int "x" Int ")"
     syntax G1Point ::= BN128Add(G1Point, G1Point) [function, hook(KRYPTO.bn128add)]
                      | BN128Mul(G1Point, Int)     [function, hook(KRYPTO.bn128mul)]

diff --git a/web3.md b/web3.md
@@ -30,7 +30,7 @@ module WEB3
         <web3response> .List </web3response>
       </kevm-client>
 
-    syntax JSON ::= Int | Bool | "null" | "undef"
+    syntax JSON ::= Bool | "null" | "undef"
                   | #getJSON ( JSONKey , JSON ) [function]
  // ------------------------------------------------------
     rule #getJSON( KEY, { KEY : J, _ } )     => J