Skip to content

Gas simplification for Csstore, named rules #1560

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 13 commits into from
Feb 13, 2023
Merged

Gas simplification for Csstore, named rules #1560

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
d58bb36
include/evm: name various CALL rules
ehildenb Dec 16, 2022
10e2e92
bin/kevm: pass --debug through to kevm-pyk
ehildenb Jan 28, 2023
5ed27c3
kevm-pyk/__main__: correct how logging levels are handled
ehildenb Jan 28, 2023
8a7060d
tests/specs/functional/infinite-gas-spec: add failing gas comparison …
ehildenb Feb 12, 2023
b6f7b79
include/kframework/{infinite-gas,lemmas/int-simplification}: add lemm…
ehildenb Feb 12, 2023
8bd248e
include/kframework/evm: add named rule for when statusCode changes
ehildenb Feb 12, 2023
75db760
include/kframework/evm: add names for various return cases from calls
ehildenb Feb 12, 2023
26ef0e7
include/evm: formatting
ehildenb Feb 12, 2023
c394439
tests/specs/function/infinite-gas-spec: another failing test
ehildenb Feb 12, 2023
06f1fc5
include/{infinite-gas,lemmas/int-simplification}: more simplifications
ehildenb Feb 12, 2023
83661f1
kevm-pyk/kevm: correct way to get zero-byte code
ehildenb Dec 10, 2022
5a99a6b
Merge branch 'master' into gas-lemma
ehildenb Feb 12, 2023
ccbc04b
Merge branch 'master' into gas-lemma
rv-jenkins Feb 13, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions bin/kevm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,7 @@ run_kevm_pyk() {
;;
esac
! ${verbose} || pyk_args+=(--verbose)
! ${debug} || pyk_args+=(--debug)
execute python3 -m kevm_pyk "${pyk_command}" "$@" "${pyk_args[@]}"
}

Expand Down
43 changes: 28 additions & 15 deletions include/kframework/evm.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -261,7 +261,8 @@ Control Flow
```k
syntax KItem ::= "#halt" | "#end" StatusCode
// --------------------------------------------
rule <k> #end SC => #halt ... </k>
rule [end]:
<k> #end SC => #halt ... </k>
<statusCode> _ => SC </statusCode>
rule <k> #halt ~> (_:Int => .) ... </k>
Expand Down Expand Up @@ -290,11 +291,14 @@ OpCode Execution
```k
syntax KItem ::= "#execute"
// ---------------------------
rule [halt]: <k> #halt ~> (#execute => .) ... </k>
rule [step]: <k> (. => #next [ #lookupOpCode(PGM, PCOUNT, SCHED) ]) ~> #execute ... </k>
<program> PGM </program>
<pc> PCOUNT </pc>
<schedule> SCHED </schedule>
rule [halt]:
<k> #halt ~> (#execute => .) ... </k>
rule [step]:
<k> (. => #next [ #lookupOpCode(PGM, PCOUNT, SCHED) ]) ~> #execute ... </k>
<program> PGM </program>
<pc> PCOUNT </pc>
<schedule> SCHED </schedule>
```

### Single Step
Expand Down Expand Up @@ -1398,14 +1402,16 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
syntax KItem ::= "#return" Int Int
// ----------------------------------
rule <statusCode> _:ExceptionalStatusCode </statusCode>
rule [return.exception]:
<statusCode> _:ExceptionalStatusCode </statusCode>
<k> #halt ~> #return _ _
=> #popCallStack ~> #popWorldState ~> 0 ~> #push
...
</k>
<output> _ => .ByteArray </output>
rule <statusCode> EVMC_REVERT </statusCode>
rule [return.revert]:
<statusCode> EVMC_REVERT </statusCode>
<k> #halt ~> #return RETSTART RETWIDTH
=> #popCallStack ~> #popWorldState
~> 0 ~> #push ~> #refund GAVAIL ~> #setLocalMem RETSTART RETWIDTH OUT
Expand All @@ -1414,7 +1420,8 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
<output> OUT </output>
<gas> GAVAIL </gas>
rule <statusCode> EVMC_SUCCESS </statusCode>
rule [return.success]:
<statusCode> EVMC_SUCCESS </statusCode>
<k> #halt ~> #return RETSTART RETWIDTH
=> #popCallStack ~> #dropWorldState
~> 1 ~> #push ~> #refund GAVAIL ~> #setLocalMem RETSTART RETWIDTH OUT
Expand Down Expand Up @@ -1442,7 +1449,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
```k
syntax CallOp ::= "CALL"
// ------------------------
rule <k> CALL _GCAP ACCTTO VALUE ARGSTART ARGWIDTH RETSTART RETWIDTH
rule [call]:
<k> CALL _GCAP ACCTTO VALUE ARGSTART ARGWIDTH RETSTART RETWIDTH
=> #checkCall ACCTFROM VALUE
~> #call ACCTFROM ACCTTO ACCTTO VALUE VALUE #range(LM, ARGSTART, ARGWIDTH) false
~> #return RETSTART RETWIDTH
Expand All @@ -1453,7 +1461,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
syntax CallOp ::= "CALLCODE"
// ----------------------------
rule <k> CALLCODE _GCAP ACCTTO VALUE ARGSTART ARGWIDTH RETSTART RETWIDTH
rule [callcode]:
<k> CALLCODE _GCAP ACCTTO VALUE ARGSTART ARGWIDTH RETSTART RETWIDTH
=> #checkCall ACCTFROM VALUE
~> #call ACCTFROM ACCTFROM ACCTTO VALUE VALUE #range(LM, ARGSTART, ARGWIDTH) false
~> #return RETSTART RETWIDTH
Expand All @@ -1464,7 +1473,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
syntax CallSixOp ::= "DELEGATECALL"
// -----------------------------------
rule <k> DELEGATECALL _GCAP ACCTTO ARGSTART ARGWIDTH RETSTART RETWIDTH
rule [delegatecall]:
<k> DELEGATECALL _GCAP ACCTTO ARGSTART ARGWIDTH RETSTART RETWIDTH
=> #checkCall ACCTFROM 0
~> #call ACCTAPPFROM ACCTFROM ACCTTO 0 VALUE #range(LM, ARGSTART, ARGWIDTH) false
~> #return RETSTART RETWIDTH
Expand All @@ -1477,7 +1487,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
syntax CallSixOp ::= "STATICCALL"
// ---------------------------------
rule <k> STATICCALL _GCAP ACCTTO ARGSTART ARGWIDTH RETSTART RETWIDTH
rule [staticcall]:
<k> STATICCALL _GCAP ACCTTO ARGSTART ARGWIDTH RETSTART RETWIDTH
=> #checkCall ACCTFROM 0
~> #call ACCTFROM ACCTTO ACCTTO 0 0 #range(LM, ARGSTART, ARGWIDTH) true
~> #return RETSTART RETWIDTH
Expand Down Expand Up @@ -1596,7 +1607,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
```k
syntax TernStackOp ::= "CREATE"
// -------------------------------
rule <k> CREATE VALUE MEMSTART MEMWIDTH
rule [create]:
<k> CREATE VALUE MEMSTART MEMWIDTH
=> #accessAccounts #newAddr(ACCT, NONCE)
~> #checkCall ACCT VALUE
~> #create ACCT #newAddr(ACCT, NONCE) VALUE #range(LM, MEMSTART, MEMWIDTH)
Expand All @@ -1617,7 +1629,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
```k
syntax QuadStackOp ::= "CREATE2"
// --------------------------------
rule <k> CREATE2 VALUE MEMSTART MEMWIDTH SALT
rule [create2]:
<k> CREATE2 VALUE MEMSTART MEMWIDTH SALT
=> #accessAccounts #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH))
~> #checkCall ACCT VALUE
~> #create ACCT #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH)) VALUE #range(LM, MEMSTART, MEMWIDTH)
Expand Down
12 changes: 12 additions & 0 deletions include/kframework/infinite-gas.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,6 +98,18 @@ module INFINITE-GAS-COMMON
rule 0 <=Int Csstore(_, _, _, _) => true [simplification]
rule Csstore(_, _, _, _) <Int #gas(_) => true [simplification]
rule G <Int Csstore(SCHED, _, _, _) => false
requires Gsload < SCHED > <=Int G
andBool Gsstoreset < SCHED > <=Int G
andBool Gsstorereset < SCHED > <=Int G
[simplification]
rule Csstore(SCHED, _, _, _) <=Int G => true
requires Gsload < SCHED > <=Int G
andBool Gsstoreset < SCHED > <=Int G
andBool Gsstorereset < SCHED > <=Int G
[simplification]
rule 0 <=Int Cmem(_, N) => true requires 0 <=Int N [simplification]
rule Cmem(_, N) <Int #gas(G) => true requires N <Int #gas(G) [simplification]
Expand Down
31 changes: 16 additions & 15 deletions include/kframework/lemmas/int-simplification.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ module INT-SIMPLIFICATION-HASKELL [symbolic, kore]
// associativity normalization

rule C1 +Int S2 => S2 +Int C1 [concrete(C1), symbolic(S2), simplification]

rule S1 +Int (S2 +Int I3) => (S1 +Int S2) +Int I3 [symbolic(S1, S2), simplification]
rule S1 +Int (S2 -Int I3) => (S1 +Int S2) -Int I3 [symbolic(S1, S2), simplification]
rule S1 -Int (S2 +Int I3) => (S1 -Int S2) -Int I3 [symbolic(S1, S2), simplification]
Expand All @@ -64,6 +64,8 @@ module INT-SIMPLIFICATION-HASKELL [symbolic, kore]
rule I1 +Int C <Int I2 => I1 <Int I2 -Int C [concrete(C), simplification]
rule C1 <Int I2 +Int C3 => C1 -Int C3 <Int I2 [concrete(C1, C3), simplification]
rule C1 <=Int I2 +Int C3 => C1 -Int C3 <=Int I2 [concrete(C1, C3), simplification]
rule C1 -Int I2 <Int C3 => C1 -Int C3 <Int I2 [concrete(C1, C3), simplification]
rule C1 <=Int C2 -Int I3 => I3 <=Int C2 -Int C1 [concrete(C1, C2), simplification]

endmodule

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

// ###########################################################################
// ###########################################################################
// mul
// ###########################################################################
// ###########################################################################

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

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]

// ###########################################################################
// ###########################################################################
// div
// ###########################################################################
// ###########################################################################

rule A /Int 1 => A [simplification]

Expand All @@ -129,37 +131,37 @@ module INT-SIMPLIFICATION-COMMON

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]

// ###########################################################################
// ###########################################################################
// inc-or
// ###########################################################################

rule 0 |Int A => A [simplification]
rule A |Int 0 => A [simplification]
rule A |Int A => A [simplification]

// ###########################################################################
// ###########################################################################
// bit-and
// ###########################################################################
// ###########################################################################

rule 0 &Int _ => 0 [simplification]
rule _ &Int 0 => 0 [simplification]
rule A &Int A => A [simplification]

// ###########################################################################
// ###########################################################################
// mod
// ###########################################################################
// ###########################################################################

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

// ###########################################################################
// ###########################################################################
// max, min
// ###########################################################################
// ###########################################################################

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

// ###########################################################################
// ###########################################################################
// inequality
// ###########################################################################
// ###########################################################################

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

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


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

endmodule
6 changes: 3 additions & 3 deletions kevm-pyk/src/kevm_pyk/__main__.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -912,12 +912,12 @@ def parse(s: str) -> List[T]:


def _loglevel(args: Namespace) -> int:
if args.verbose or args.profile:
return logging.INFO

if args.debug:
return logging.DEBUG

if args.verbose or args.profile:
return logging.INFO

return logging.WARNING


Expand Down
3 changes: 2 additions & 1 deletion kevm-pyk/src/kevm_pyk/kevm.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@
from pyk.ktool import KProve, KRun
from pyk.ktool.kompile import KompileBackend
from pyk.ktool.kprint import SymbolTable, paren
from pyk.prelude.bytes import bytesToken
from pyk.prelude.kbool import notBool
from pyk.prelude.kint import intToken, ltInt
from pyk.prelude.ml import mlAnd, mlEqualsTrue
Expand Down Expand Up @@ -471,7 +472,7 @@ def account_CHEATCODE_ADDRESS(store_var: KInner) -> KApply: # noqa: N802
return KEVM.account_cell(
Foundry.address_CHEATCODE(), # Hardcoded for now
intToken(0),
KToken('b"\\x00"', 'Bytes'),
bytesToken('\x00'),
store_var,
KApply('.Map'),
intToken(0),
Expand Down
3 changes: 3 additions & 0 deletions tests/specs/functional/infinite-gas-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,6 +117,9 @@ module INFINITE-GAS-SPEC
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>
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>

claim [Csstore-1]: <k> runLemma(9223372036854696114 -Int Csstore(LONDON, _, _, _) <Int 8) => doneLemma(false) ... </k>
claim [Csstore-2]: <k> runLemma(8 <=Int 9223372036854763220 -Int Csstore(LONDON, _, _, _)) => doneLemma(true) ... </k>

claim <k> runLemma(#allBut64th(#gas(_G)) <Int #gas(_G')) => doneLemma(false) ... </k>

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