From c0cb1ba4d66942ec1c89f47d8346c5d28351491a Mon Sep 17 00:00:00 2001 From: Andrei Date: Tue, 10 Oct 2023 12:01:33 +0300 Subject: [PATCH 1/6] implement cut cheat code --- .../kevm_pyk/kproj/evm-semantics/foundry.md | 40 +++++++++++++++++++ kevm-pyk/src/kevm_pyk/utils.py | 2 +- kevm-pyk/src/kontrolx/foundry.py | 1 + tests/foundry/src/KEVMCheats.sol | 2 + 4 files changed, 44 insertions(+), 1 deletion(-) 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..98c8e392cb 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 ` .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)" ) ``` +#### `sign` - Signs a digest with private key + +``` +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 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..97cc2b917e 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': KApply('.Set'), } constraints = None 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 { From 8da64ebe0959a631e2db10f582b2c8700282d031 Mon Sep 17 00:00:00 2001 From: Andrei Date: Tue, 10 Oct 2023 12:02:29 +0300 Subject: [PATCH 2/6] typo --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/foundry.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 98c8e392cb..59b5913d23 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/foundry.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/foundry.md @@ -192,7 +192,7 @@ 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 From f7b7ab9a1febc3ef9ea0004c55729232019d41c8 Mon Sep 17 00:00:00 2001 From: Andrei Date: Tue, 10 Oct 2023 12:03:40 +0300 Subject: [PATCH 3/6] add description --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/foundry.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 59b5913d23..8ab69f28d9 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/foundry.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/foundry.md @@ -1087,7 +1087,7 @@ The `ECDSASign` function returns the signed data in [r,s,v] form, which we conve requires SELECTOR ==Int selector ( "sign(uint256,bytes32)" ) ``` -#### `sign` - Signs a digest with private key +#### `cut` - Adds a new KCFG node at the given program counter. ``` function cut(uint256 programCounter) external; From 8515d50bad0320d1a3531ccfcb158ecf524a2a85 Mon Sep 17 00:00:00 2001 From: Andrei Date: Tue, 10 Oct 2023 12:11:08 +0300 Subject: [PATCH 4/6] fix foundry.pc --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/foundry.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 8ab69f28d9..d79029ea48 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/foundry.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/foundry.md @@ -1467,7 +1467,7 @@ If the production is matched when no prank is active, it will be ignored. #pc [ OP ] => #cut ... PCOUNT => PCOUNT +Int #widthOp(OP) CPC - requires PCOUNT in CPC + requires (PCOUNT +Int #widthOp(OP)) in CPC [priority(40)] ``` From 6df8042f34c2c5531f59249b429c1350b20418b0 Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 10 Oct 2023 09:12:21 +0000 Subject: [PATCH 5/6] Set Version: 1.0.315 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) 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/package/version b/package/version index 7681bff51e..aeffd5170f 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.314 +1.0.315 From a8e269042c4362d92a64408a8178af4cf310c454 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andrei=20V=C4=83caru?= <16517508+anvacaru@users.noreply.github.com> Date: Thu, 19 Oct 2023 11:37:57 +0300 Subject: [PATCH 6/6] Update kevm-pyk/src/kontrolx/foundry.py --- kevm-pyk/src/kontrolx/foundry.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/kontrolx/foundry.py b/kevm-pyk/src/kontrolx/foundry.py index 97cc2b917e..cde387648d 100644 --- a/kevm-pyk/src/kontrolx/foundry.py +++ b/kevm-pyk/src/kontrolx/foundry.py @@ -1304,7 +1304,7 @@ def _init_cterm( 'ISSTORAGEWHITELISTACTIVE_CELL': FALSE, 'ADDRESSSET_CELL': KApply('.Set'), 'STORAGESLOTSET_CELL': KApply('.Set'), - 'CUTPC': KApply('.Set'), + 'CUTPC_CELL': KApply('.Set'), } constraints = None