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 <devops@runtimeverification.com>

package/version

@@ -1 +1 @@
-0.1.359
+0.1.360

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. <contact@runtimeverification.com>",

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'

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 != <address found in this contract>)`
+        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
 

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);
+	}
 }

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);
+	}
 }

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 )