Skip to content

Commit a978756

Browse files
ehildenbrv-jenkins
ehildenb
and
rv-jenkins
authored
Gas simplification for Csstore, named rules (#1560)
* include/evm: name various CALL rules * bin/kevm: pass --debug through to kevm-pyk * kevm-pyk/__main__: correct how logging levels are handled * tests/specs/functional/infinite-gas-spec: add failing gas comparison check for foundry * include/kframework/{infinite-gas,lemmas/int-simplification}: add lemmas for simplifying infinite gas query * include/kframework/evm: add named rule for when statusCode changes * include/kframework/evm: add names for various return cases from calls * include/evm: formatting * tests/specs/function/infinite-gas-spec: another failing test * include/{infinite-gas,lemmas/int-simplification}: more simplifications * kevm-pyk/kevm: correct way to get zero-byte code --------- Co-authored-by: rv-jenkins <[email protected]>
1 parent eb37959 commit a978756

File tree

7 files changed

+65
-34
lines changed

7 files changed

+65
-34
lines changed

‎bin/kevm

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,7 @@ run_kevm_pyk() {
5959
;;
6060
esac
6161
! ${verbose} || pyk_args+=(--verbose)
62+
! ${debug} || pyk_args+=(--debug)
6263
execute python3 -m kevm_pyk "${pyk_command}" "$@" "${pyk_args[@]}"
6364
}
6465

‎include/kframework/evm.md

Lines changed: 28 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -261,7 +261,8 @@ Control Flow
261261
```k
262262
syntax KItem ::= "#halt" | "#end" StatusCode
263263
// --------------------------------------------
264-
rule <k> #end SC => #halt ... </k>
264+
rule [end]:
265+
<k> #end SC => #halt ... </k>
265266
<statusCode> _ => SC </statusCode>
266267
267268
rule <k> #halt ~> (_:Int => .) ... </k>
@@ -290,11 +291,14 @@ OpCode Execution
290291
```k
291292
syntax KItem ::= "#execute"
292293
// ---------------------------
293-
rule [halt]: <k> #halt ~> (#execute => .) ... </k>
294-
rule [step]: <k> (. => #next [ #lookupOpCode(PGM, PCOUNT, SCHED) ]) ~> #execute ... </k>
295-
<program> PGM </program>
296-
<pc> PCOUNT </pc>
297-
<schedule> SCHED </schedule>
294+
rule [halt]:
295+
<k> #halt ~> (#execute => .) ... </k>
296+
297+
rule [step]:
298+
<k> (. => #next [ #lookupOpCode(PGM, PCOUNT, SCHED) ]) ~> #execute ... </k>
299+
<program> PGM </program>
300+
<pc> PCOUNT </pc>
301+
<schedule> SCHED </schedule>
298302
```
299303

300304
### Single Step
@@ -1398,14 +1402,16 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
13981402
13991403
syntax KItem ::= "#return" Int Int
14001404
// ----------------------------------
1401-
rule <statusCode> _:ExceptionalStatusCode </statusCode>
1405+
rule [return.exception]:
1406+
<statusCode> _:ExceptionalStatusCode </statusCode>
14021407
<k> #halt ~> #return _ _
14031408
=> #popCallStack ~> #popWorldState ~> 0 ~> #push
14041409
...
14051410
</k>
14061411
<output> _ => .ByteArray </output>
14071412
1408-
rule <statusCode> EVMC_REVERT </statusCode>
1413+
rule [return.revert]:
1414+
<statusCode> EVMC_REVERT </statusCode>
14091415
<k> #halt ~> #return RETSTART RETWIDTH
14101416
=> #popCallStack ~> #popWorldState
14111417
~> 0 ~> #push ~> #refund GAVAIL ~> #setLocalMem RETSTART RETWIDTH OUT
@@ -1414,7 +1420,8 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
14141420
<output> OUT </output>
14151421
<gas> GAVAIL </gas>
14161422
1417-
rule <statusCode> EVMC_SUCCESS </statusCode>
1423+
rule [return.success]:
1424+
<statusCode> EVMC_SUCCESS </statusCode>
14181425
<k> #halt ~> #return RETSTART RETWIDTH
14191426
=> #popCallStack ~> #dropWorldState
14201427
~> 1 ~> #push ~> #refund GAVAIL ~> #setLocalMem RETSTART RETWIDTH OUT
@@ -1442,7 +1449,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
14421449
```k
14431450
syntax CallOp ::= "CALL"
14441451
// ------------------------
1445-
rule <k> CALL _GCAP ACCTTO VALUE ARGSTART ARGWIDTH RETSTART RETWIDTH
1452+
rule [call]:
1453+
<k> CALL _GCAP ACCTTO VALUE ARGSTART ARGWIDTH RETSTART RETWIDTH
14461454
=> #checkCall ACCTFROM VALUE
14471455
~> #call ACCTFROM ACCTTO ACCTTO VALUE VALUE #range(LM, ARGSTART, ARGWIDTH) false
14481456
~> #return RETSTART RETWIDTH
@@ -1453,7 +1461,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
14531461
14541462
syntax CallOp ::= "CALLCODE"
14551463
// ----------------------------
1456-
rule <k> CALLCODE _GCAP ACCTTO VALUE ARGSTART ARGWIDTH RETSTART RETWIDTH
1464+
rule [callcode]:
1465+
<k> CALLCODE _GCAP ACCTTO VALUE ARGSTART ARGWIDTH RETSTART RETWIDTH
14571466
=> #checkCall ACCTFROM VALUE
14581467
~> #call ACCTFROM ACCTFROM ACCTTO VALUE VALUE #range(LM, ARGSTART, ARGWIDTH) false
14591468
~> #return RETSTART RETWIDTH
@@ -1464,7 +1473,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
14641473
14651474
syntax CallSixOp ::= "DELEGATECALL"
14661475
// -----------------------------------
1467-
rule <k> DELEGATECALL _GCAP ACCTTO ARGSTART ARGWIDTH RETSTART RETWIDTH
1476+
rule [delegatecall]:
1477+
<k> DELEGATECALL _GCAP ACCTTO ARGSTART ARGWIDTH RETSTART RETWIDTH
14681478
=> #checkCall ACCTFROM 0
14691479
~> #call ACCTAPPFROM ACCTFROM ACCTTO 0 VALUE #range(LM, ARGSTART, ARGWIDTH) false
14701480
~> #return RETSTART RETWIDTH
@@ -1477,7 +1487,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
14771487
14781488
syntax CallSixOp ::= "STATICCALL"
14791489
// ---------------------------------
1480-
rule <k> STATICCALL _GCAP ACCTTO ARGSTART ARGWIDTH RETSTART RETWIDTH
1490+
rule [staticcall]:
1491+
<k> STATICCALL _GCAP ACCTTO ARGSTART ARGWIDTH RETSTART RETWIDTH
14811492
=> #checkCall ACCTFROM 0
14821493
~> #call ACCTFROM ACCTTO ACCTTO 0 0 #range(LM, ARGSTART, ARGWIDTH) true
14831494
~> #return RETSTART RETWIDTH
@@ -1596,7 +1607,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
15961607
```k
15971608
syntax TernStackOp ::= "CREATE"
15981609
// -------------------------------
1599-
rule <k> CREATE VALUE MEMSTART MEMWIDTH
1610+
rule [create]:
1611+
<k> CREATE VALUE MEMSTART MEMWIDTH
16001612
=> #accessAccounts #newAddr(ACCT, NONCE)
16011613
~> #checkCall ACCT VALUE
16021614
~> #create ACCT #newAddr(ACCT, NONCE) VALUE #range(LM, MEMSTART, MEMWIDTH)
@@ -1617,7 +1629,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
16171629
```k
16181630
syntax QuadStackOp ::= "CREATE2"
16191631
// --------------------------------
1620-
rule <k> CREATE2 VALUE MEMSTART MEMWIDTH SALT
1632+
rule [create2]:
1633+
<k> CREATE2 VALUE MEMSTART MEMWIDTH SALT
16211634
=> #accessAccounts #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH))
16221635
~> #checkCall ACCT VALUE
16231636
~> #create ACCT #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH)) VALUE #range(LM, MEMSTART, MEMWIDTH)

‎include/kframework/infinite-gas.md

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -98,6 +98,18 @@ module INFINITE-GAS-COMMON
9898
rule 0 <=Int Csstore(_, _, _, _) => true [simplification]
9999
rule Csstore(_, _, _, _) <Int #gas(_) => true [simplification]
100100
101+
rule G <Int Csstore(SCHED, _, _, _) => false
102+
requires Gsload < SCHED > <=Int G
103+
andBool Gsstoreset < SCHED > <=Int G
104+
andBool Gsstorereset < SCHED > <=Int G
105+
[simplification]
106+
107+
rule Csstore(SCHED, _, _, _) <=Int G => true
108+
requires Gsload < SCHED > <=Int G
109+
andBool Gsstoreset < SCHED > <=Int G
110+
andBool Gsstorereset < SCHED > <=Int G
111+
[simplification]
112+
101113
rule 0 <=Int Cmem(_, N) => true requires 0 <=Int N [simplification]
102114
rule Cmem(_, N) <Int #gas(G) => true requires N <Int #gas(G) [simplification]
103115

‎include/kframework/lemmas/int-simplification.k

Lines changed: 16 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ module INT-SIMPLIFICATION-HASKELL [symbolic, kore]
3838
// associativity normalization
3939

4040
rule C1 +Int S2 => S2 +Int C1 [concrete(C1), symbolic(S2), simplification]
41-
41+
4242
rule S1 +Int (S2 +Int I3) => (S1 +Int S2) +Int I3 [symbolic(S1, S2), simplification]
4343
rule S1 +Int (S2 -Int I3) => (S1 +Int S2) -Int I3 [symbolic(S1, S2), simplification]
4444
rule S1 -Int (S2 +Int I3) => (S1 -Int S2) -Int I3 [symbolic(S1, S2), simplification]
@@ -64,6 +64,8 @@ module INT-SIMPLIFICATION-HASKELL [symbolic, kore]
6464
rule I1 +Int C <Int I2 => I1 <Int I2 -Int C [concrete(C), simplification]
6565
rule C1 <Int I2 +Int C3 => C1 -Int C3 <Int I2 [concrete(C1, C3), simplification]
6666
rule C1 <=Int I2 +Int C3 => C1 -Int C3 <=Int I2 [concrete(C1, C3), simplification]
67+
rule C1 -Int I2 <Int C3 => C1 -Int C3 <Int I2 [concrete(C1, C3), simplification]
68+
rule C1 <=Int C2 -Int I3 => I3 <=Int C2 -Int C1 [concrete(C1, C2), simplification]
6769

6870
endmodule
6971

@@ -101,9 +103,9 @@ module INT-SIMPLIFICATION-COMMON
101103
rule (C +Int (A -Int D)) +Int (B -Int A) => C +Int (B -Int D) [simplification]
102104
rule (((A -Int B) -Int C) -Int D) +Int B => (A -Int C) -Int D [simplification]
103105

104-
// ###########################################################################
106+
// ###########################################################################
105107
// mul
106-
// ###########################################################################
108+
// ###########################################################################
107109

108110
rule 1 *Int A => A [simplification]
109111
rule A *Int 1 => A [simplification]
@@ -114,9 +116,9 @@ module INT-SIMPLIFICATION-COMMON
114116

115117
rule (E *Int A) +Int B +Int C +Int D +Int (F *Int A) => ((E +Int F) *Int A) +Int B +Int C +Int D [simplification]
116118

117-
// ###########################################################################
119+
// ###########################################################################
118120
// div
119-
// ###########################################################################
121+
// ###########################################################################
120122

121123
rule A /Int 1 => A [simplification]
122124

@@ -129,37 +131,37 @@ module INT-SIMPLIFICATION-COMMON
129131

130132
rule (A *Int B) /Int C <=Int D => true requires 0 <=Int A andBool 0 <=Int B andBool 0 <Int C andBool A <=Int D andBool B <=Int C [simplification]
131133

132-
// ###########################################################################
134+
// ###########################################################################
133135
// inc-or
134136
// ###########################################################################
135137

136138
rule 0 |Int A => A [simplification]
137139
rule A |Int 0 => A [simplification]
138140
rule A |Int A => A [simplification]
139141

140-
// ###########################################################################
142+
// ###########################################################################
141143
// bit-and
142-
// ###########################################################################
144+
// ###########################################################################
143145

144146
rule 0 &Int _ => 0 [simplification]
145147
rule _ &Int 0 => 0 [simplification]
146148
rule A &Int A => A [simplification]
147149

148-
// ###########################################################################
150+
// ###########################################################################
149151
// mod
150-
// ###########################################################################
152+
// ###########################################################################
151153

152154
rule A modInt B => A requires 0 <=Int A andBool A <Int B [simplification]
153155

154-
// ###########################################################################
156+
// ###########################################################################
155157
// max, min
156-
// ###########################################################################
158+
// ###########################################################################
157159

158160
rule minInt(A, B) => A requires A <=Int B [simplification]
159161

160-
// ###########################################################################
162+
// ###########################################################################
161163
// inequality
162-
// ###########################################################################
164+
// ###########################################################################
163165

164166
rule A +Int B <Int A => false requires 0 <=Int B [simplification]
165167

@@ -181,7 +183,6 @@ module INT-SIMPLIFICATION-COMMON
181183
rule A <Int minInt(B, C) => true requires A <Int B andBool A <Int C [simplification]
182184
rule A <=Int minInt(B, C) => true requires A <=Int B andBool A <=Int C [simplification]
183185

184-
185186
rule A <=Int maxInt(B, C) => true requires A <=Int B orBool A <=Int C [simplification]
186187

187188
endmodule

‎kevm-pyk/src/kevm_pyk/__main__.py

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -912,12 +912,12 @@ def parse(s: str) -> List[T]:
912912

913913

914914
def _loglevel(args: Namespace) -> int:
915-
if args.verbose or args.profile:
916-
return logging.INFO
917-
918915
if args.debug:
919916
return logging.DEBUG
920917

918+
if args.verbose or args.profile:
919+
return logging.INFO
920+
921921
return logging.WARNING
922922

923923

‎kevm-pyk/src/kevm_pyk/kevm.py

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@
1212
from pyk.ktool import KProve, KRun
1313
from pyk.ktool.kompile import KompileBackend
1414
from pyk.ktool.kprint import SymbolTable, paren
15+
from pyk.prelude.bytes import bytesToken
1516
from pyk.prelude.kbool import notBool
1617
from pyk.prelude.kint import intToken, ltInt
1718
from pyk.prelude.ml import mlAnd, mlEqualsTrue
@@ -471,7 +472,7 @@ def account_CHEATCODE_ADDRESS(store_var: KInner) -> KApply: # noqa: N802
471472
return KEVM.account_cell(
472473
Foundry.address_CHEATCODE(), # Hardcoded for now
473474
intToken(0),
474-
KToken('b"\\x00"', 'Bytes'),
475+
bytesToken('\x00'),
475476
store_var,
476477
KApply('.Map'),
477478
intToken(0),

‎tests/specs/functional/infinite-gas-spec.k

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -117,6 +117,9 @@ module INFINITE-GAS-SPEC
117117
claim <k> runLemma(#if _:Int ==Int 0 #then #gas(VGas -Int Csstore(_, _, _,_)) #else #gas(VGas +Int -344) #fi <Int minInt(#if _ #then #gas(_) #else #gas(_) #fi, #gas(_))) => doneLemma(false) ... </k>
118118
claim <k> runLemma(minInt(#if _ #then #gas(_) #else #gas(_) #fi, #gas(_)) <=Int #if _:Int ==Int 0 #then #gas(VGas -Int Csstore(_, _, _,_)) #else #gas(VGas +Int -344) #fi) => doneLemma(true) ... </k>
119119

120+
claim [Csstore-1]: <k> runLemma(9223372036854696114 -Int Csstore(LONDON, _, _, _) <Int 8) => doneLemma(false) ... </k>
121+
claim [Csstore-2]: <k> runLemma(8 <=Int 9223372036854763220 -Int Csstore(LONDON, _, _, _)) => doneLemma(true) ... </k>
122+
120123
claim <k> runLemma(#allBut64th(#gas(_G)) <Int #gas(_G')) => doneLemma(false) ... </k>
121124

122125
claim <k> runLemma(Gverylow < _ > <=Int #gas(_)) => doneLemma(true) ... </k>

0 commit comments

Comments
 (0)