Skip to content

Commit

Permalink
Add no-gas mode to kevm (#2207)
Browse files Browse the repository at this point in the history 
* add use-gas cell and option

* Set Version: 1.0.384

* override #deductGas

* update exected output for test_gst_to_kore

* Set Version: 1.0.386

* update output templates

* update failing expected files

* add <use-gas> cell to k claims

* integrate use-gas cell in optimization rules

* Set Version: 1.0.394

* typo

* temp, profiling

* Revert "temp, profiling"

This reverts commit 87dd5f5.

* fix typo in expected files

* Set Version: 1.0.396

* fix output templates

* fix static_callcodecallcodecall

* True => true

* Set Version: 1.0.397

* evm.md: disable refund, maintain accessStorage logic

* Set Version: 1.0.398

* renaming use-gas cell

* formatting optimizations

* rename <use-gas> to <useGas> in configuration files

* removing SCHED from no-gas optimizations

* fix formatting

* no-gas effects on non-main EVM files

* add noGas proof example

* de-duplicating rules

* rewrite constraints for optimizations

* Revert "rewrite constraints for optimizations"

This reverts commit e522615.

* Revert "de-duplicating rules"

This reverts commit af7c6d1.

* Set Version: 1.0.399

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Petar Maksimovic <[email protected]>
  • Loading branch information
@anvacaru @PetarMax
3 people authored Dec 19, 2023
1 parent 34e0352 commit b50a246
Show file tree
Hide file tree
Showing 143 changed files with 889 additions and 311 deletions.
2 changes: 1 addition & 1 deletion Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ test-prove-kprove: tests/specs/opcodes/evm-optimizations-spec.md poetry

# to generate optimizations.md, run: ./optimizer/optimize.sh &> output
tests/specs/opcodes/evm-optimizations-spec.md: kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
cat kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md | sed 's/^rule/claim/' | sed 's/EVM-OPTIMIZATIONS/EVM-OPTIMIZATIONS-SPEC/' | grep -v 'priority(40)' > $@
cat kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md | sed 's/^ rule/ claim/' | sed 's/EVM-OPTIMIZATIONS/EVM-OPTIMIZATIONS-SPEC/' | grep -v 'priority(40)' > $@


# Integration Tests
Expand Down
2 changes: 1 addition & 1 deletion kevm-pyk/pyproject.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "kevm-pyk"
version = "1.0.398"
version = "1.0.399"
description = ""
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
2 changes: 1 addition & 1 deletion kevm-pyk/src/kevm_pyk/__init__.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,4 +6,4 @@
from typing import Final


VERSION: Final = '1.0.398'
VERSION: Final = '1.0.399'
10 changes: 6 additions & 4 deletions kevm-pyk/src/kevm_pyk/__main__.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -594,6 +594,7 @@ def exec_run(
schedule: str,
mode: str,
chainid: int,
usegas: bool,
target: str | None = None,
save_directory: Path | None = None,
debugger: bool = False,
Expand All @@ -609,12 +610,12 @@ def exec_run(

try:
json_read = json.loads(input_file.read_text())
kore_pattern = gst_to_kore(json_read, schedule, mode, chainid)
kore_pattern = gst_to_kore(json_read, schedule, mode, chainid, usegas)
except json.JSONDecodeError:
pgm_token = KToken(input_file.read_text(), KSort('EthereumSimulation'))
kast_pgm = kevm.parse_token(pgm_token)
kore_pgm = kevm.kast_to_kore(kast_pgm, sort=KSort('EthereumSimulation'))
kore_pattern = kore_pgm_to_kore(kore_pgm, SORT_ETHEREUM_SIMULATION, schedule, mode, chainid)
kore_pattern = kore_pgm_to_kore(kore_pgm, SORT_ETHEREUM_SIMULATION, schedule, mode, chainid, usegas)

kevm.run(
kore_pattern,
Expand All @@ -633,6 +634,7 @@ def exec_kast(
schedule: str,
mode: str,
chainid: int,
usegas: bool,
target: str | None = None,
save_directory: Path | None = None,
**kwargs: Any,
Expand All @@ -647,12 +649,12 @@ def exec_kast(

try:
json_read = json.loads(input_file.read_text())
kore_pattern = gst_to_kore(json_read, schedule, mode, chainid)
kore_pattern = gst_to_kore(json_read, schedule, mode, chainid, usegas)
except json.JSONDecodeError:
pgm_token = KToken(input_file.read_text(), KSort('EthereumSimulation'))
kast_pgm = kevm.parse_token(pgm_token)
kore_pgm = kevm.kast_to_kore(kast_pgm)
kore_pattern = kore_pgm_to_kore(kore_pgm, SORT_ETHEREUM_SIMULATION, schedule, mode, chainid)
kore_pattern = kore_pgm_to_kore(kore_pgm, SORT_ETHEREUM_SIMULATION, schedule, mode, chainid, usegas)

output_text = kore_print(kore_pattern, definition_dir=kevm.definition_dir, output=output)
print(output_text)
Expand Down
3 changes: 3 additions & 0 deletions kevm-pyk/src/kevm_pyk/cli.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -134,6 +134,9 @@ def evm_chain_args(self) -> ArgumentParser:
default='NORMAL',
help="execution mode to use [{'|'.join(modes)}]",
)
args.add_argument(
'--no-gas', action='store_false', dest='usegas', default=True, help='omit gas cost computations'
)
return args

@cached_property
Expand Down
15 changes: 8 additions & 7 deletions kevm-pyk/src/kevm_pyk/gst_to_kore.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
from typing import TYPE_CHECKING

from pyk.cli.utils import file_path
from pyk.kore.prelude import INT, SORT_JSON, SORT_K_ITEM, inj, int_dv, json_to_kore, top_cell_initializer
from pyk.kore.prelude import BOOL, INT, SORT_JSON, SORT_K_ITEM, bool_dv, inj, int_dv, json_to_kore, top_cell_initializer
from pyk.kore.syntax import App, SortApp

from .cli import KEVMCLIArgs
Expand All @@ -29,16 +29,17 @@
SORT_ETHEREUM_SIMULATION: Final = SortApp('SortEthereumSimulation')


def gst_to_kore(gst_data: Any, schedule: str, mode: str, chainid: int) -> App:
return kore_pgm_to_kore(json_to_kore(gst_data), SORT_JSON, schedule, mode, chainid)
def gst_to_kore(gst_data: Any, schedule: str, mode: str, chainid: int, usegas: bool) -> App:
return kore_pgm_to_kore(json_to_kore(gst_data), SORT_JSON, schedule, mode, chainid, usegas)


def kore_pgm_to_kore(pgm: Pattern, pattern_sort: SortApp, schedule: str, mode: str, chainid: int) -> App:
def kore_pgm_to_kore(pgm: Pattern, pattern_sort: SortApp, schedule: str, mode: str, chainid: int, usegas: bool) -> App:
config = {
'$PGM': inj(pattern_sort, SORT_K_ITEM, pgm),
'$SCHEDULE': inj(SORT_SCHEDULE, SORT_K_ITEM, _schedule_to_kore(schedule)),
'$MODE': inj(SORT_MODE, SORT_K_ITEM, _mode_to_kore(mode)),
'$CHAINID': inj(INT, SORT_K_ITEM, int_dv(chainid)),
'$USEGAS': inj(BOOL, SORT_K_ITEM, bool_dv(usegas)),
}
return top_cell_initializer(config)

Expand All @@ -54,12 +55,12 @@ def _mode_to_kore(mode: str) -> App:
def main() -> None:
sys.setrecursionlimit(15000000)
args = _parse_args()
_exec_gst_to_kore(args.input_file, args.schedule, args.mode, args.chainid)
_exec_gst_to_kore(args.input_file, args.schedule, args.mode, args.chainid, args.usegas)


def _exec_gst_to_kore(input_file: Path, schedule: str, mode: str, chainid: int) -> None:
def _exec_gst_to_kore(input_file: Path, schedule: str, mode: str, chainid: int, usegas: bool) -> None:
gst_data = json.loads(input_file.read_text())
kore = gst_to_kore(gst_data, schedule, mode, chainid)
kore = gst_to_kore(gst_data, schedule, mode, chainid, usegas)
kore.write(sys.stdout)
sys.stdout.write('\n')
_LOGGER.info('Finished writing KORE')
Expand Down
8 changes: 4 additions & 4 deletions kevm-pyk/src/kevm_pyk/interpreter.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,8 @@
from pyk.kore.syntax import Pattern


def interpret(gst_data: Any, schedule: str, mode: str, chainid: int, *, check: bool = True) -> Pattern:
proc_res = _interpret(gst_data, schedule, mode, chainid)
def interpret(gst_data: Any, schedule: str, mode: str, chainid: int, usegas: bool, *, check: bool = True) -> Pattern:
proc_res = _interpret(gst_data, schedule, mode, chainid, usegas)

if check:
proc_res.check_returncode()
Expand All @@ -25,8 +25,8 @@ def interpret(gst_data: Any, schedule: str, mode: str, chainid: int, *, check: b
return kore


def _interpret(gst_data: Any, schedule: str, mode: str, chainid: int) -> CompletedProcess:
def _interpret(gst_data: Any, schedule: str, mode: str, chainid: int, usegas: bool) -> CompletedProcess:
interpreter = kdist.get('evm-semantics.llvm') / 'interpreter'
init_kore = gst_to_kore(gst_data, schedule, mode, chainid)
init_kore = gst_to_kore(gst_data, schedule, mode, chainid, usegas)
proc_res = run_process([str(interpreter), '/dev/stdin', '-1', '/dev/stdout'], input=init_kore.text, check=False)
return proc_res
2 changes: 2 additions & 0 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -301,6 +301,8 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
rule <k> loadCallState { "code" : (CODE:OpCodes), REST } => #loadProgram #asmOpCodes(CODE) ~> loadCallState { REST } ... </k>
rule <k> loadCallState { "usegas" : (USEGAS:Bool), REST => REST } ... </k> <useGas> _ => USEGAS </useGas>
rule <k> loadCallState { KEY : ((VAL:String) => #parseWord(VAL)), _ } ... </k>
requires KEY in (SetItem("gas") SetItem("gasPrice") SetItem("value"))
Expand Down
60 changes: 54 additions & 6 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@ In the comments next to each cell, we've marked which component of the YellowPap
<exit-code exit=""> 1 </exit-code>
<mode> $MODE:Mode </mode>
<schedule> $SCHEDULE:Schedule </schedule>
<useGas> $USEGAS:Bool </useGas>
<ethereum>
Expand Down Expand Up @@ -551,6 +552,7 @@ After executing a transaction, it's necessary to have the effect of the substate
<accessedStorage> _ => .Map </accessedStorage>
rule <k> #finalizeTx(false) ... </k>
<useGas> true </useGas>
<schedule> SCHED </schedule>
<gas> GAVAIL => G*(GAVAIL, GLIMIT, REFUND, SCHED) </gas>
<refund> REFUND => 0 </refund>
Expand All @@ -563,6 +565,7 @@ After executing a transaction, it's necessary to have the effect of the substate
requires REFUND =/=Int 0
rule <k> #finalizeTx(false => true) ... </k>
<useGas> true </useGas>
<baseFee> BFEE </baseFee>
<origin> ORG </origin>
<coinbase> MINER </coinbase>
Expand All @@ -589,6 +592,7 @@ After executing a transaction, it's necessary to have the effect of the substate
requires ORG =/=Int MINER
rule <k> #finalizeTx(false => true) ... </k>
<useGas> true </useGas>
<baseFee> BFEE </baseFee>
<origin> ACCT </origin>
<coinbase> ACCT </coinbase>
Expand All @@ -608,6 +612,14 @@ After executing a transaction, it's necessary to have the effect of the substate
...
</message>
rule <k> #finalizeTx(false => true) ... </k>
<useGas> false </useGas>
<txPending> ListItem(MsgId:Int) REST => REST </txPending>
<message>
<msgID> MsgId </msgID>
...
</message>
rule <k> (. => #deleteAccounts(Set2List(ACCTS))) ~> #finalizeTx(true) ... </k>
<selfDestruct> ACCTS => .Set </selfDestruct>
requires size(ACCTS) >Int 0
Expand Down Expand Up @@ -1243,7 +1255,7 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
</account>
requires VALUE <=Int BAL
rule <k> #checkDepthExceeded => #refund GCALL ~> #pushCallStack ~> #pushWorldState ~> #end EVMC_CALL_DEPTH_EXCEEDED ... </k>
rule <k> #checkDepthExceeded => #refund GCALL ~> #pushCallStack ~> #pushWorldState ~> #end EVMC_CALL_DEPTH_EXCEEDED ... </k>
<output> _ => .Bytes </output>
<callGas> GCALL </callGas>
<callDepth> CD </callDepth>
Expand Down Expand Up @@ -1299,6 +1311,7 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
=> #touchAccounts ACCTFROM ACCTTO ~> #accessAccounts ACCTFROM ACCTTO ~> #loadProgram BYTES ~> #initVM ~> #precompiled?(ACCTCODE, SCHED) ~> #execute
...
</k>
<useGas> true </useGas>
<callDepth> CD => CD +Int 1 </callDepth>
<callData> _ => ARGS </callData>
<callValue> _ => APPVALUE </callValue>
Expand All @@ -1309,6 +1322,19 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
<static> OLDSTATIC:Bool => OLDSTATIC orBool STATIC </static>
<schedule> SCHED </schedule>
rule <k> #mkCall ACCTFROM ACCTTO ACCTCODE BYTES APPVALUE ARGS STATIC:Bool
=> #touchAccounts ACCTFROM ACCTTO ~> #accessAccounts ACCTFROM ACCTTO ~> #loadProgram BYTES ~> #initVM ~> #precompiled?(ACCTCODE, SCHED) ~> #execute
...
</k>
<useGas> false </useGas>
<callDepth> CD => CD +Int 1 </callDepth>
<callData> _ => ARGS </callData>
<callValue> _ => APPVALUE </callValue>
<id> _ => ACCTTO </id>
<caller> _ => ACCTFROM </caller>
<static> OLDSTATIC:Bool => OLDSTATIC orBool STATIC </static>
<schedule> SCHED </schedule>
syntax InternalOp ::= "#precompiled?" "(" Int "," Schedule ")"
// --------------------------------------------------------------
rule <k> #precompiled?(ACCTCODE, SCHED) => #next [ #precompiled(ACCTCODE) ] ... </k> requires #isPrecompiledAccount(ACCTCODE, SCHED)
Expand Down Expand Up @@ -1343,7 +1369,7 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
<touchedAccounts> TOUCHED_ACCOUNTS => TOUCHED_ACCOUNTS |Set SetItem(ADDR) </touchedAccounts>
syntax KItem ::= "#accessStorage" Account Int
// --------------------------------------------
// ---------------------------------------------
rule <k> #accessStorage ACCT INDEX => . ... </k>
<accessedStorage> ... ACCT |-> (TS:Set => TS |Set SetItem(INDEX)) ... </accessedStorage>
rule <k> #accessStorage ACCT INDEX => . ... </k>
Expand All @@ -1354,7 +1380,7 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
| "#accessAccounts" Set
| "#accessAccounts" Account Account
| "#accessAccounts" Account Account Set
// -----------------------------------------------------
// ------------------------------------------------------
rule <k> #accessAccounts ADDR1:Account ADDR2:Account ADDRSET:Set => #accessAccounts ADDR1 ~> #accessAccounts ADDR2 ~> #accessAccounts ADDRSET ... </k>
rule <k> #accessAccounts ADDR1:Account ADDR2:Account => #accessAccounts ADDR1 ~> #accessAccounts ADDR2 ... </k>
Expand Down Expand Up @@ -1418,7 +1444,9 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
syntax InternalOp ::= "#refund" Gas
| "#setLocalMem" Int Int Bytes
// --------------------------------------------------
rule [refund]: <k> #refund G:Gas => . ... </k> <gas> GAVAIL => GAVAIL +Gas G </gas>
rule [refund]: <k> #refund G:Gas => . ... </k> <gas> GAVAIL => GAVAIL +Gas G </gas> <useGas> true </useGas>
rule [refund.noGas]: <k> #refund _ => . ... </k> <useGas> false </useGas>
rule <k> #setLocalMem START WIDTH WS => . ... </k>
<localMem> LM => LM [ START := #range(WS, 0, minInt(WIDTH, lengthBytes(WS))) ] </localMem>
Expand Down Expand Up @@ -1508,6 +1536,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
=> #touchAccounts ACCTFROM ACCTTO ~> #accessAccounts ACCTFROM ACCTTO ~> #loadProgram INITCODE ~> #initVM ~> #execute
...
</k>
<useGas> true </useGas>
<schedule> SCHED </schedule>
<id> _ => ACCTTO </id>
<gas> _ => GCALL </gas>
Expand All @@ -1522,6 +1551,22 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
...
</account>
rule <k> #mkCreate ACCTFROM ACCTTO VALUE INITCODE
=> #touchAccounts ACCTFROM ACCTTO ~> #accessAccounts ACCTFROM ACCTTO ~> #loadProgram INITCODE ~> #initVM ~> #execute
...
</k>
<useGas> false </useGas>
<id> _ => ACCTTO </id>
<caller> _ => ACCTFROM </caller>
<callDepth> CD => CD +Int 1 </callDepth>
<callData> _ => .Bytes </callData>
<callValue> _ => VALUE </callValue>
<account>
<acctID> ACCTTO </acctID>
<nonce> NONCE => NONCE +Int 1 </nonce>
...
</account>
rule <k> #incrementNonce ACCT => . ... </k>
<account>
<acctID> ACCT </acctID>
Expand Down Expand Up @@ -1850,6 +1895,8 @@ Overall Gas
~> #access [ OP , AOP ]
...
</k>
<useGas> true </useGas>
rule <k> #gas [ _ , _ ] => . ... </k> <useGas> false </useGas>
rule <k> #gas [ OP ] => #gasExec(SCHED, OP) ~> #deductGas ... </k>
<schedule> SCHED </schedule>
Expand All @@ -1867,8 +1914,9 @@ Overall Gas
<memoryUsed> MU => MU' </memoryUsed> <schedule> SCHED </schedule>
rule <k> _G:Gas ~> (#deductMemoryGas => #deductGas) ... </k> //Required for verification
rule <k> G:Gas ~> #deductGas => #end EVMC_OUT_OF_GAS ... </k> <gas> GAVAIL:Gas </gas> requires GAVAIL <Gas G
rule <k> G:Gas ~> #deductGas => . ... </k> <gas> GAVAIL:Gas => GAVAIL -Gas G </gas> requires G <=Gas GAVAIL
rule <k> G:Gas ~> #deductGas => #end EVMC_OUT_OF_GAS ... </k> <gas> GAVAIL:Gas </gas> <useGas> true </useGas> requires GAVAIL <Gas G
rule <k> G:Gas ~> #deductGas => . ... </k> <gas> GAVAIL:Gas => GAVAIL -Gas G </gas> <useGas> true </useGas> requires G <=Gas GAVAIL
rule <k> _:Gas ~> #deductGas => . ... </k> <useGas> false </useGas>
syntax Bool ::= #inStorage ( Map , Account , Int ) [function, total]
| #inStorageAux1 ( KItem , Int ) [function, total]
Expand Down
Loading

0 comments on commit b50a246

Please sign in to comment.