diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 88a4c15ced..c621f3d85b 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.314" +version = "1.0.315" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 2e92eddbaa..af8df6f2ff 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.314' +VERSION: Final = '1.0.315' diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/foundry.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/foundry.md index e705e13854..d79029ea48 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/foundry.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/foundry.md @@ -192,6 +192,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 @@ -236,6 +238,7 @@ module FOUNDRY-CHEAT-CODES .Set .Set + .Set ``` @@ -1084,6 +1087,23 @@ 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(#range(ARGS, 0, 32)) + requires SELECTOR ==Int selector ( "cut(uint256)" ) +``` + + Otherwise, throw an error for any other call to the Foundry contract. ```k @@ -1440,6 +1460,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 @@ -1479,6 +1518,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/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py index 712f746779..00b1f6f6b4 100644 --- a/kevm-pyk/src/kevm_pyk/utils.py +++ b/kevm-pyk/src/kevm_pyk/utils.py @@ -103,7 +103,7 @@ def kevm_prove( ) -> bool: proof = proof terminal_rules = ['EVM.halt'] - cut_point_rules = [] + cut_point_rules = ['FOUNDRY.foundry.cut'] if break_every_step: terminal_rules.append('EVM.step') if break_on_jumpi: diff --git a/kevm-pyk/src/kontrolx/foundry.py b/kevm-pyk/src/kontrolx/foundry.py index b6798fc22c..cde387648d 100644 --- a/kevm-pyk/src/kontrolx/foundry.py +++ b/kevm-pyk/src/kontrolx/foundry.py @@ -1304,6 +1304,7 @@ def _init_cterm( 'ISSTORAGEWHITELISTACTIVE_CELL': FALSE, 'ADDRESSSET_CELL': KApply('.Set'), 'STORAGESLOTSET_CELL': KApply('.Set'), + 'CUTPC_CELL': KApply('.Set'), } constraints = None diff --git a/package/version b/package/version index 7681bff51e..aeffd5170f 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.314 +1.0.315 diff --git a/tests/foundry/src/KEVMCheats.sol b/tests/foundry/src/KEVMCheats.sol index 14e3aef982..0e5f3bc3c6 100644 --- a/tests/foundry/src/KEVMCheats.sol +++ b/tests/foundry/src/KEVMCheats.sol @@ -29,6 +29,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 SymbolicWords {