From 680538158127cf53fb0c4191fb1583cbc0c6c77f Mon Sep 17 00:00:00 2001 From: Lim Jin Xing Date: Thu, 18 Jul 2024 20:43:33 +0800 Subject: [PATCH] Generate `_notExternalAddress` function in RecordedState (#701) * Generate `_notExternalAddress` function in RecordedState * Set Version: 0.1.356 * Minor fix * Set Version: 0.1.357 * Set Version: 0.1.360 * `make format` * Updated expected output * Reverted foundry.k.expected * Minor issue foundry.k.expected * Relocated a module in contracts.k.expected * minor issue in contracts.k.expected --------- Co-authored-by: devops --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- src/kontrol/state_record.py | 18 ++++++++++++++++++ .../test-data/foundry/src/LoadStateDiff.sol | 9 +++++++++ .../test-data/foundry/src/LoadStateDump.sol | 10 ++++++++++ .../test-data/show/contracts.k.expected | 18 ++++++++++++++++++ 7 files changed, 58 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index 8509341ee..785120566 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.359 +0.1.360 diff --git a/pyproject.toml b/pyproject.toml index 8818e7977..2badc9aa9 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.359" +version = "0.1.360" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 75fd4e5ae..2c1b1bfc2 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.359' +VERSION: Final = '0.1.360' diff --git a/src/kontrol/state_record.py b/src/kontrol/state_record.py index 327ed0eb0..c65647fd0 100644 --- a/src/kontrol/state_record.py +++ b/src/kontrol/state_record.py @@ -124,16 +124,21 @@ def generate_main_contract(self) -> list[str]: lines.append('') lines.append(f'contract {self.name} is {self.name}Code ' + '{') + # Appending the Test contract address + lines.append('\t// Test contract address, 0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496') + lines.append('\taddress private constant FOUNDRY_TEST_ADDRESS = 0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496;') # Appending the cheatcode address to be able to avoid extending `Test` lines.append('\t// Cheat code address, 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D') lines.append('\taddress private constant VM_ADDRESS = address(uint160(uint256(keccak256("hevm cheat code"))));') lines.append('\tVm private constant vm = Vm(VM_ADDRESS);\n') + # Appending variables for external addresses for acc_key in list(self.accounts): lines.append('\taddress internal constant ' + self.accounts[acc_key] + 'Address = ' + acc_key + ';') lines.append('\n') + # Appending `recreateState()` function that consists of calling `vm.etch` and `vm.store` to recreate state for external computation lines.append('\tfunction recreateState() public {') lines.append('\t\tbytes32 slot;') @@ -144,6 +149,19 @@ def generate_main_contract(self) -> list[str]: lines.append('\t}') + lines.append('\n') + + # Appending `_notExternalAddress(address user)` function that consists of `vm.assume(user !=
)` + lines.append('\tfunction _notExternalAddress(address user) public pure {') + + lines.append('\t\tvm.assume(user != FOUNDRY_TEST_ADDRESS);') + lines.append('\t\tvm.assume(user != VM_ADDRESS);') + + for acc_key in list(self.accounts): + lines.append('\t\tvm.assume(user != ' + self.accounts[acc_key] + 'Address);') + + lines.append('\t}') + lines.append('}') return lines diff --git a/src/tests/integration/test-data/foundry/src/LoadStateDiff.sol b/src/tests/integration/test-data/foundry/src/LoadStateDiff.sol index 3ad9193cb..e7fc3d131 100644 --- a/src/tests/integration/test-data/foundry/src/LoadStateDiff.sol +++ b/src/tests/integration/test-data/foundry/src/LoadStateDiff.sol @@ -8,6 +8,8 @@ import { Vm } from "forge-std/Vm.sol"; import { LoadStateDiffCode } from "./LoadStateDiffCode.sol"; contract LoadStateDiff is LoadStateDiffCode { + // Test contract address, 0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496 + address private constant FOUNDRY_TEST_ADDRESS = 0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496; // Cheat code address, 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D address private constant VM_ADDRESS = address(uint160(uint256(keccak256("hevm cheat code")))); Vm private constant vm = Vm(VM_ADDRESS); @@ -23,4 +25,11 @@ contract LoadStateDiff is LoadStateDiffCode { value = hex'0000000000000000000000000000000000000000000000000000000000000003'; vm.store(acc0Address, slot, value); } + + + function _notExternalAddress(address user) public pure { + vm.assume(user != FOUNDRY_TEST_ADDRESS); + vm.assume(user != VM_ADDRESS); + vm.assume(user != acc0Address); + } } \ No newline at end of file diff --git a/src/tests/integration/test-data/foundry/src/LoadStateDump.sol b/src/tests/integration/test-data/foundry/src/LoadStateDump.sol index f0a9e97fa..1a3a37958 100644 --- a/src/tests/integration/test-data/foundry/src/LoadStateDump.sol +++ b/src/tests/integration/test-data/foundry/src/LoadStateDump.sol @@ -8,6 +8,8 @@ import { Vm } from "forge-std/Vm.sol"; import { LoadStateDumpCode } from "./LoadStateDumpCode.sol"; contract LoadStateDump is LoadStateDumpCode { + // Test contract address, 0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496 + address private constant FOUNDRY_TEST_ADDRESS = 0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496; // Cheat code address, 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D address private constant VM_ADDRESS = address(uint160(uint256(keccak256("hevm cheat code")))); Vm private constant vm = Vm(VM_ADDRESS); @@ -30,4 +32,12 @@ contract LoadStateDump is LoadStateDumpCode { value = hex'0000000000000000000000000000000000000000000000000000000000000002'; vm.store(acc1Address, slot, value); } + + + function _notExternalAddress(address user) public pure { + vm.assume(user != FOUNDRY_TEST_ADDRESS); + vm.assume(user != VM_ADDRESS); + vm.assume(user != acc0Address); + vm.assume(user != acc1Address); + } } \ No newline at end of file diff --git a/src/tests/integration/test-data/show/contracts.k.expected b/src/tests/integration/test-data/show/contracts.k.expected index 4bf445f2a..67ebb93f8 100644 --- a/src/tests/integration/test-data/show/contracts.k.expected +++ b/src/tests/integration/test-data/show/contracts.k.expected @@ -6740,11 +6740,20 @@ module S2KsrcZModLoadStateDiff-CONTRACT syntax Bytes ::= S2KsrcZModLoadStateDiffContract "." S2KsrcZModLoadStateDiffMethod [function, symbol("method_src%LoadStateDiff")] + syntax S2KsrcZModLoadStateDiffMethod ::= "S2KZUndnotExternalAddress" "(" Int ":" "address" ")" [symbol("method_src%LoadStateDiff_S2KZUndnotExternalAddress_address")] + syntax S2KsrcZModLoadStateDiffMethod ::= "S2KrecreateState" "(" ")" [symbol("method_src%LoadStateDiff_S2KrecreateState_")] + rule ( S2KsrcZModLoadStateDiff . S2KZUndnotExternalAddress ( V0_user : address ) => #abiCallData ( "_notExternalAddress" , ( #address ( V0_user ) , .TypedArgs ) ) ) + ensures #rangeAddress ( V0_user ) + + rule ( S2KsrcZModLoadStateDiff . S2KrecreateState ( ) => #abiCallData ( "recreateState" , .TypedArgs ) ) + rule ( selector ( "_notExternalAddress(address)" ) => 2801087029 ) + + rule ( selector ( "recreateState()" ) => 1765761107 ) @@ -6768,11 +6777,20 @@ module S2KsrcZModLoadStateDump-CONTRACT syntax Bytes ::= S2KsrcZModLoadStateDumpContract "." S2KsrcZModLoadStateDumpMethod [function, symbol("method_src%LoadStateDump")] + syntax S2KsrcZModLoadStateDumpMethod ::= "S2KZUndnotExternalAddress" "(" Int ":" "address" ")" [symbol("method_src%LoadStateDump_S2KZUndnotExternalAddress_address")] + syntax S2KsrcZModLoadStateDumpMethod ::= "S2KrecreateState" "(" ")" [symbol("method_src%LoadStateDump_S2KrecreateState_")] + rule ( S2KsrcZModLoadStateDump . S2KZUndnotExternalAddress ( V0_user : address ) => #abiCallData ( "_notExternalAddress" , ( #address ( V0_user ) , .TypedArgs ) ) ) + ensures #rangeAddress ( V0_user ) + + rule ( S2KsrcZModLoadStateDump . S2KrecreateState ( ) => #abiCallData ( "recreateState" , .TypedArgs ) ) + rule ( selector ( "_notExternalAddress(address)" ) => 2801087029 ) + + rule ( selector ( "recreateState()" ) => 1765761107 )