From 4f02bd16307001bf93786343680c4ec2d8c9ba07 Mon Sep 17 00:00:00 2001 From: Andrei Date: Wed, 8 Nov 2023 08:58:05 +0200 Subject: [PATCH 1/2] add support for cut cheat code --- src/kontrol/kdist/foundry.md | 41 +++++++++++++++++++ src/kontrol/prove.py | 8 +++- .../test-data/foundry/src/KEVMCheats.sol | 2 + 3 files changed, 50 insertions(+), 1 deletion(-) diff --git a/src/kontrol/kdist/foundry.md b/src/kontrol/kdist/foundry.md index 10dbb9a4c..0ce2d6b7b 100644 --- a/src/kontrol/kdist/foundry.md +++ b/src/kontrol/kdist/foundry.md @@ -119,6 +119,8 @@ The configuration of the Foundry Cheat Codes is defined as follwing: - `` flags if the whitelist mode is enabled for storage changes. - `` - stores the address whitelist. - `` - stores the storage whitelist containing pairs of addresses and storage indexes. +6. The `` cell stores a set of program counters inserted using the `cut` cheat code. +Each program counter in the set will end up creating a new node in the KCFG. ```k module FOUNDRY-CHEAT-CODES @@ -163,6 +165,7 @@ module FOUNDRY-CHEAT-CODES .Set .Set + .Set ``` @@ -1035,6 +1038,24 @@ The `ECDSASign` function returns the signed data in [r,s,v] form, which we conve requires SELECTOR ==Int selector ( "sign(uint256,bytes32)" ) ``` + +#### `cut` - Adds a new KCFG node at the given program counter. + +``` +function cut(uint256 programCounter) external; +``` + +`foundry.call.cut` will match when the `cut` cheat code function is called. +This rule will add the `programCounter` argument to the `cutPC` set. + +```k + rule [foundry.call.cut]: + #call_foundry SELECTOR ARGS => . ... + CPC => CPC SetItem(#asWord(#range(ARGS, 0, 32))) + requires SELECTOR ==Int selector ( "cut(uint256)" ) + ``` + + Otherwise, throw an error for any other call to the Foundry contract. ```k @@ -1421,6 +1442,25 @@ If the production is matched when no prank is active, it will be ignored. ``` +- `foundry.pc` triggers the `#cut` rule when a program counter that is in the `cutPC` set is executed. + +```k + rule [foundry.pc]: + #pc [ OP ] => #cut ... + PCOUNT => PCOUNT +Int #widthOp(OP) + CPC + requires (PCOUNT +Int #widthOp(OP)) in CPC + [priority(40)] +``` + +- `foundry_cut` is an empty rule used to create a node in the KCFG. + +```k + syntax KItem ::= "#cut" [klabel(foundry_cut)] + // --------------------------------------------- + rule [foundry.cut]: #cut => . ... +``` + - selectors for cheat code functions. ```k @@ -1460,6 +1500,7 @@ If the production is matched when no prank is active, it will be ignored. rule ( selector ( "allowChangesToStorage(address,uint256)" ) => 4207417100 ) rule ( selector ( "infiniteGas()" ) => 3986649939 ) rule ( selector ( "setGas(uint256)" ) => 3713137314 ) + rule ( selector ( "cut(uint256)" ) => 153488823 ) ``` - selectors for unimplemented cheat code functions. diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 0c5fa7d5a..cd621ddf6 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -204,13 +204,16 @@ def init_and_run_proof(test: FoundryTest) -> Proof: run_constructor=options.run_constructor, ) + cut_point_rules = ['FOUNDRY.foundry.cut'] + cut_point_rules.extend(KEVMSemantics.cut_point_rules(options.break_on_jumpi, options.break_on_calls)) + run_prover( foundry.kevm, proof, kcfg_explore, max_depth=options.max_depth, max_iterations=options.max_iterations, - cut_point_rules=KEVMSemantics.cut_point_rules(options.break_on_jumpi, options.break_on_calls), + cut_point_rules=cut_point_rules, terminal_rules=KEVMSemantics.terminal_rules(options.break_every_step), ) return proof @@ -467,6 +470,7 @@ def _init_cterm( 'ISSTORAGEWHITELISTACTIVE_CELL': FALSE, 'ADDRESSSET_CELL': KApply('.Set'), 'STORAGESLOTSET_CELL': KApply('.Set'), + 'CUTPC_CELL': KApply('.Set'), } constraints = None @@ -543,6 +547,7 @@ def _final_term(empty_config: KInner, contract_name: str, use_init_code: bool = 'ISSTORAGEWHITELISTACTIVE_CELL': KVariable('ISSTORAGEWHITELISTACTIVE_FINAL'), 'ADDRESSSET_CELL': KVariable('ADDRESSSET_FINAL'), 'STORAGESLOTSET_CELL': KVariable('STORAGESLOTSET_FINAL'), + 'CUTPC_CELL': KVariable('CUTPC_FINAL'), } return abstract_cell_vars( Subst(final_subst)(empty_config), @@ -557,5 +562,6 @@ def _final_term(empty_config: KInner, contract_name: str, use_init_code: bool = KVariable('ISSTORAGEWHITELISTACTIVE_FINAL'), KVariable('ADDRESSSET_FINAL'), KVariable('STORAGESLOTSET_FINAL'), + KVariable('CUTPC_FINAL'), ], ) diff --git a/src/tests/integration/test-data/foundry/src/KEVMCheats.sol b/src/tests/integration/test-data/foundry/src/KEVMCheats.sol index 451892628..d3ee57b87 100644 --- a/src/tests/integration/test-data/foundry/src/KEVMCheats.sol +++ b/src/tests/integration/test-data/foundry/src/KEVMCheats.sol @@ -31,6 +31,8 @@ interface KEVMCheatsBase { function freshUInt(uint8) external returns (uint256); // Returns a symbolic boolean value function freshBool() external returns (uint256); + // Adds a new KCFG node at the given program counter. + function cut(uint256) external; } abstract contract KEVMCheats { From c4f65e026363f98f742c82a1934e43ac06a1660d Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 8 Nov 2023 07:00:13 +0000 Subject: [PATCH 2/2] Set Version: 0.1.54 --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index a4c528cd5..7b300677b 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.53 +0.1.54 diff --git a/pyproject.toml b/pyproject.toml index 09e4c813b..1f3778d7a 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.53" +version = "0.1.54" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index bc4acf12c..70964acd7 100644 --- a/src/kontrol/__init__.py +++ b/src/kontrol/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '0.1.53' +VERSION: Final = '0.1.54'