Skip to content

Commit d938b30

Browse files
dwightguthehildenb
dwightguth
authored and
ehildenb
committed
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
1 parent 133d028 commit d938b30

File tree

5 files changed

+90
-44
lines changed

5 files changed

+90
-44
lines changed

‎data.md

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ Writing a JSON-ish parser in K takes 6 lines.
2929
```k
3030
syntax JSONList ::= List{JSON,","}
3131
syntax JSONKey ::= String | Int
32-
syntax JSON ::= String
32+
syntax JSON ::= String | Int
3333
| JSONKey ":" JSON
3434
| "{" JSONList "}"
3535
| "[" JSONList "]"
@@ -655,6 +655,22 @@ Addresses
655655
656656
```
657657

658+
- `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.
659+
660+
```k
661+
syntax Int ::= "M3:2048" "(" ByteArray ")" [function]
662+
// -----------------------------------------------------
663+
rule M3:2048(WS) => setBloomFilterBits(#parseByteStack(Keccak256(#unparseByteStack(WS))))
664+
665+
syntax Int ::= setBloomFilterBits(ByteArray) [function]
666+
// -------------------------------------------------------
667+
rule setBloomFilterBits(HASH) => (1 <<Int getBloomFilterBit(HASH, 0)) |Int (1 <<Int getBloomFilterBit(HASH, 2)) |Int (1 <<Int getBloomFilterBit(HASH, 4))
668+
669+
syntax Int ::= getBloomFilterBit(ByteArray, Int) [function]
670+
// -----------------------------------------------------------
671+
rule getBloomFilterBit(X, I) => #asInteger(X [ I .. 2 ]) %Int 2048
672+
```
673+
658674
Word Map
659675
--------
660676

‎driver.md

Lines changed: 3 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -43,8 +43,8 @@ For verification purposes, it's much easier to specify a program in terms of its
4343
To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a "pretti-fication" to the nicer input form.
4444

4545
```{.k .standalone}
46-
syntax JSON ::= Int | ByteArray | OpCodes | Map | Call | SubstateLogEntry | Account
47-
// -----------------------------------------------------------------------------------
46+
syntax JSON ::= ByteArray | OpCodes | Map | Call | SubstateLogEntry | Account
47+
// -----------------------------------------------------------------------------
4848
4949
syntax JSONList ::= #sortJSONList ( JSONList ) [function]
5050
| #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
202202
requires TT =/=K .Account
203203
```
204204

205-
- `#finalizeBlock` is used to signal that block finalization procedures should take place (after transactions have executed).
206-
- `#rewardOmmers(_)` pays out the reward to uncle blocks so that blocks are orphaned less often in Ethereum.
207-
208-
```{.k .standalone}
209-
syntax EthereumCommand ::= "#finalizeBlock" | #rewardOmmers ( JSONList )
210-
// ------------------------------------------------------------------------
211-
rule <k> #finalizeBlock => #rewardOmmers(OMMERS) ... </k>
212-
<schedule> SCHED </schedule>
213-
<ommerBlockHeaders> [ OMMERS ] </ommerBlockHeaders>
214-
<coinbase> MINER </coinbase>
215-
<account>
216-
<acctID> MINER </acctID>
217-
<balance> MINBAL => MINBAL +Int Rb < SCHED > </balance>
218-
...
219-
</account>
220-
221-
rule <k> (.K => #newAccount MINER) ~> #finalizeBlock ... </k>
222-
<coinbase> MINER </coinbase>
223-
<activeAccounts> ACCTS </activeAccounts>
224-
requires notBool MINER in ACCTS
225-
226-
rule <k> #rewardOmmers(.JSONList) => . ... </k>
227-
rule <k> #rewardOmmers([ _ , _ , OMMER , _ , _ , _ , _ , _ , OMMNUM , _ ] , REST) => #rewardOmmers(REST) ... </k>
228-
<schedule> SCHED </schedule>
229-
<coinbase> MINER </coinbase>
230-
<number> CURNUM </number>
231-
<account>
232-
<acctID> MINER </acctID>
233-
<balance> MINBAL => MINBAL +Int Rb < SCHED > /Int 32 </balance>
234-
...
235-
</account>
236-
<account>
237-
<acctID> OMMER </acctID>
238-
<balance> OMMBAL => OMMBAL +Int Rb < SCHED > +Int (OMMNUM -Int CURNUM) *Int (Rb < SCHED > /Int 8) </balance>
239-
...
240-
</account>
241-
```
242-
243205
- `exception` only clears from the `<k>` cell if there is an exception preceding it.
244206
- `failure_` holds the name of a test that failed if a test does fail.
245207
- `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"`
311273
requires KEY in #execKeys
312274
313275
rule <k> run TESTID : { "exec" : (EXEC:JSON) } => load "exec" : EXEC ~> start ~> flush ... </k>
314-
rule <k> run TESTID : { "lastblockhash" : (HASH:String) } => startTx ... </k>
276+
rule <k> run TESTID : { "lastblockhash" : (HASH:String) } => #startBlock ~> startTx ... </k>
315277
```
316278

317279
- `#postKeys` are a subset of `#checkKeys` which correspond to post-state account checks.

‎evm.md

Lines changed: 68 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -576,6 +576,7 @@ After executing a transaction, it's necessary to have the effect of the substate
576576
<origin> ORG </origin>
577577
<coinbase> MINER </coinbase>
578578
<gas> GAVAIL </gas>
579+
<gasUsed> GUSED => GUSED +Int GLIMIT -Int GAVAIL </gasUsed>
579580
<refund> 0 </refund>
580581
<account>
581582
<acctID> ORG </acctID>
@@ -599,6 +600,8 @@ After executing a transaction, it's necessary to have the effect of the substate
599600
rule <k> #finalizeTx(false => true) ... </k>
600601
<origin> ACCT </origin>
601602
<coinbase> ACCT </coinbase>
603+
<gas> GAVAIL </gas>
604+
<gasUsed> GUSED => GUSED +Int GLIMIT -Int GAVAIL </gasUsed>
602605
<refund> 0 </refund>
603606
<account>
604607
<acctID> ACCT </acctID>
@@ -632,6 +635,71 @@ After executing a transaction, it's necessary to have the effect of the substate
632635
rule <k> #deleteAccounts(.List) => . ... </k>
633636
```
634637

638+
### Block processing
639+
640+
- `#startBlock` is used to signal that we are about to start mining a block and block initialization should take place (before transactions are executed).
641+
- `#finalizeBlock` is used to signal that block finalization procedures should take place (after transactions have executed).
642+
- `#rewardOmmers(_)` pays out the reward to uncle blocks so that blocks are orphaned less often in Ethereum.
643+
644+
```{.k .standalone}
645+
syntax EthereumCommand ::= "#startBlock"
646+
// ----------------------------------------
647+
rule <k> #startBlock => . ... </k>
648+
<gasUsed> _ => 0 </gasUsed>
649+
<log> _ => .List </log>
650+
<logsBloom> _ => #padToWidth(256, .ByteArray) </logsBloom>
651+
652+
syntax EthereumCommand ::= "#finalizeBlock" | #rewardOmmers ( JSONList )
653+
// ------------------------------------------------------------------------
654+
rule <k> #finalizeBlock => #rewardOmmers(OMMERS) ... </k>
655+
<schedule> SCHED </schedule>
656+
<ommerBlockHeaders> [ OMMERS ] </ommerBlockHeaders>
657+
<coinbase> MINER </coinbase>
658+
<account>
659+
<acctID> MINER </acctID>
660+
<balance> MINBAL => MINBAL +Int Rb < SCHED > </balance>
661+
...
662+
</account>
663+
<log> LOGS </log>
664+
<logsBloom> _ => #bloomFilter(LOGS) </logsBloom>
665+
666+
rule <k> (.K => #newAccount MINER) ~> #finalizeBlock ... </k>
667+
<coinbase> MINER </coinbase>
668+
<activeAccounts> ACCTS </activeAccounts>
669+
requires notBool MINER in ACCTS
670+
671+
rule <k> #rewardOmmers(.JSONList) => . ... </k>
672+
rule <k> #rewardOmmers([ _ , _ , OMMER , _ , _ , _ , _ , _ , OMMNUM , _ ] , REST) => #rewardOmmers(REST) ... </k>
673+
<schedule> SCHED </schedule>
674+
<coinbase> MINER </coinbase>
675+
<number> CURNUM </number>
676+
<account>
677+
<acctID> MINER </acctID>
678+
<balance> MINBAL => MINBAL +Int Rb < SCHED > /Int 32 </balance>
679+
...
680+
</account>
681+
<account>
682+
<acctID> OMMER </acctID>
683+
<balance> OMMBAL => OMMBAL +Int Rb < SCHED > +Int (OMMNUM -Int CURNUM) *Int (Rb < SCHED > /Int 8) </balance>
684+
...
685+
</account>
686+
687+
syntax ByteArray ::= #bloomFilter(List) [function]
688+
| #bloomFilter(List, Int) [function, klabel(#bloomFilterAux)]
689+
// --------------------------------------------------------------------------------
690+
rule #bloomFilter(L) => #bloomFilter(L, 0)
691+
692+
rule #bloomFilter(.List, B) => #padToWidth(256, #asByteStack(B))
693+
rule #bloomFilter(ListItem({ ACCT | TOPICS | _ }) L, B) => #bloomFilter(ListItem(#padToWidth(20, #asByteStack(ACCT))) listAsByteArrays(TOPICS) L, B)
694+
695+
syntax List ::= listAsByteArrays(List) [function]
696+
// -------------------------------------------------
697+
rule listAsByteArrays(.List) => .List
698+
rule listAsByteArrays(ListItem(TOPIC) L) => ListItem(#padToWidth(32, #asByteStack(TOPIC))) listAsByteArrays(L)
699+
700+
rule #bloomFilter(ListItem(WS:ByteArray) L, B) => #bloomFilter(L, B |Int M3:2048(WS))
701+
```
702+
635703
EVM Programs
636704
============
637705

‎krypto.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ The BN128 elliptic curve is defined over 2-dimensional points over the fields of
3636
- `isValidPoint` takes a point in either G1 or G2 and validates that it actually falls on the respective elliptic curve.
3737

3838
```k
39-
syntax G1Point ::= "(" Int "," Int ")"
39+
syntax G1Point ::= "(" Int "," Int ")" [prefer]
4040
syntax G2Point ::= "(" Int "x" Int "," Int "x" Int ")"
4141
syntax G1Point ::= BN128Add(G1Point, G1Point) [function, hook(KRYPTO.bn128add)]
4242
| BN128Mul(G1Point, Int) [function, hook(KRYPTO.bn128mul)]

‎web3.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ module WEB3
3030
<web3response> .List </web3response>
3131
</kevm-client>
3232
33-
syntax JSON ::= Int | Bool | "null" | "undef"
33+
syntax JSON ::= Bool | "null" | "undef"
3434
| #getJSON ( JSONKey , JSON ) [function]
3535
// ------------------------------------------------------
3636
rule #getJSON( KEY, { KEY : J, _ } ) => J

0 commit comments

Comments
 (0)