diff --git a/src/kontrol/kdist/cheatcodes.md b/src/kontrol/kdist/cheatcodes.md index 4b77a78ec..35892fc00 100644 --- a/src/kontrol/kdist/cheatcodes.md +++ b/src/kontrol/kdist/cheatcodes.md @@ -121,7 +121,7 @@ function deal(address who, uint256 newBalance) external; ``` `cheatcode.call.deal` will match when the `deal` cheat code function is called. -The rule then takes from the function call data the target account, using `#asWord(#range(ARGS, 0, 32)`, and the new balance, using `#asWord(#range(ARGS, 32, 32))`, and forwards them to the `#setBalance` production which updates the account accordingly. +The rule then takes from the function call data the target account, using `#asWord(#range(ARGS, 0, 32))`, and the new balance, using `#asWord(#range(ARGS, 32, 32))`, and forwards them to the `#setBalance` production which updates the account accordingly. ```k rule [cheatcode.call.deal]: @@ -378,13 +378,59 @@ This rule returns a symbolic integer of up to the bit width that was sent as an [preserves-definedness] ``` +#### `randomUint` - Returns a single symbolic unsigned integer of a given size. + +``` +function randomUint() external returns (uint256); +function randomUint(uint256) external returns (uint256); +function randomUint(uint256,uint256) external returns (uint256); +``` + +`cheatcode.call.randomUintWidth` will match when the `randomUint(uint256)` cheat code function is called. +This rule returns a symbolic integer of up to the bit width that was sent as an argument. + +```{.k .symbolic} + rule [cheatcode.call.randomUintWidth]: + #cheatcode_call SELECTOR ARGS => .K ... + _ => #buf(32, ?WORD) + requires 0 #cheatcode_call SELECTOR _ => .K ... + _ => #buf(32, ?WORD) + requires SELECTOR ==Int selector ( "randomUint()" ) + ensures 0 <=Int ?WORD andBool ?WORD #cheatcode_call SELECTOR ARGS => .K ... + _ => #buf(32, ?WORD) + requires SELECTOR ==Int selector ( "randomUint(uint256,uint256)" ) + ensures #asWord(#range(ARGS, 0, 32)) <=Int ?WORD andBool ?WORD <=Int #asWord(#range(ARGS, 32, 32)) + [preserves-definedness] +``` + #### `freshBool` - Returns a single symbolic boolean. ``` function freshBool() external returns (bool); +function randomBool() external returns (bool); ``` -`cheatcode.call.freshBool` will match when the `freshBool` cheat code function is called. +`cheatcode.call.freshBool` will match when the `freshBool` or `randomBool` cheat code function is called. This rule returns a symbolic boolean value being either 0 (false) or 1 (true). ```{.k .symbolic} @@ -392,6 +438,7 @@ This rule returns a symbolic boolean value being either 0 (false) or 1 (true). #cheatcode_call SELECTOR _ => .K ... _ => #buf(32, ?WORD) requires SELECTOR ==Int selector ( "freshBool()" ) + orBool SELECTOR ==Int selector ( "randomBool()" ) ensures #rangeBool(?WORD) [preserves-definedness] ``` @@ -400,9 +447,12 @@ This rule returns a symbolic boolean value being either 0 (false) or 1 (true). ``` function freshBytes(uint256) external returns (bytes memory); +function randomBytes(uint256) external returns (bytes memory); +function randomBytes4() external view returns (bytes4); +function randomBytes8() external view returns (bytes8); ``` -`cheatcode.call.freshBytes` will match when the `freshBytes` cheat code function is called. +`cheatcode.call.freshBytes` will match when the `freshBytes` or `randomBytes` cheat code function is called. This rule returns a fully symbolic byte array value of the given length. ```{.k .symbolic} @@ -413,7 +463,34 @@ This rule returns a fully symbolic byte array value of the given length. +Bytes #buf ( ( ( notMaxUInt5 &Int ( #asWord(ARGS) +Int maxUInt5 ) ) -Int #asWord(ARGS) ) , 0 ) requires SELECTOR ==Int selector ( "freshBytes(uint256)" ) - ensures lengthBytes(?BYTES) ==Int #asWord(ARGS) + orBool SELECTOR ==Int selector ( "randomBytes(uint256)" ) + ensures lengthBytes(?BYTES) ==Int #asWord(ARGS) + [preserves-definedness] +``` + +This rule returns a fully symbolic byte array value of length 4. + +```{.k .symbolic} + rule [cheatcode.call.randomBytes4]: + #cheatcode_call SELECTOR _ => .K ... + _ => + ?BYTES +Bytes #buf ( 28 , 0 ) + + requires SELECTOR ==Int selector ( "randomBytes4()" ) + ensures lengthBytes(?BYTES) ==Int 4 + [preserves-definedness] +``` + +This rule returns a fully symbolic byte array value of length 8. + +```{.k .symbolic} + rule [cheatcode.call.randomBytes8]: + #cheatcode_call SELECTOR _ => .K ... + _ => + ?BYTES +Bytes #buf ( 24 , 0 ) + + requires SELECTOR ==Int selector ( "randomBytes8()" ) + ensures lengthBytes(?BYTES) ==Int 8 [preserves-definedness] ``` @@ -421,9 +498,10 @@ This rule returns a fully symbolic byte array value of the given length. ``` function freshAddress() external returns (address); +function randomAddress() external returns (address); ``` -`foundry.call.freshAddress` will match when the `freshAddress` cheat code function is called. +`foundry.call.freshAddress` will match when the `freshAddress` or `randomAddress` cheat code function is called. This rule returns a symbolic address value. ```{.k .symbolic} @@ -431,6 +509,7 @@ This rule returns a symbolic address value. #cheatcode_call SELECTOR _ => .K ... _ => #buf(32, ?WORD) requires SELECTOR ==Int selector ( "freshAddress()" ) + orBool SELECTOR ==Int selector ( "randomAddress()" ) ensures #rangeAddress(?WORD) andBool ?WORD =/=Int #address(FoundryTest) andBool ?WORD =/=Int #address(FoundryCheat) [preserves-definedness] ``` @@ -1592,9 +1671,17 @@ Selectors for **implemented** cheat code functions. rule ( selector ( "symbolicStorage(address)" ) => 769677742 ) rule ( selector ( "setArbitraryStorage(address)" ) => 3781367863 ) rule ( selector ( "freshUInt(uint8)" ) => 625253732 ) + rule ( selector ( "randomUint(uint256)" ) => 3481396892 ) + rule ( selector ( "randomUint()" ) => 621954864 ) + rule ( selector ( "randomUint(uint256,uint256)" ) => 3592095003 ) rule ( selector ( "freshBool()" ) => 2935720297 ) + rule ( selector ( "randomBool()" ) => 3451987645 ) rule ( selector ( "freshBytes(uint256)" ) => 1389402351 ) + rule ( selector ( "randomBytes(uint256)" ) => 1818047145 ) + rule ( selector ( "randomBytes4()" ) => 2608649593 ) + rule ( selector ( "randomBytes8()" ) => 77050021 ) rule ( selector ( "freshAddress()" ) => 2363359817 ) + rule ( selector ( "randomAddress()" ) => 3586058741 ) rule ( selector ( "prank(address)" ) => 3395723175 ) rule ( selector ( "prank(address,address)" ) => 1206193358 ) rule ( selector ( "allowCallsToAddress(address)" ) => 1850795572 ) diff --git a/src/tests/integration/test-data/end-to-end-prove-all b/src/tests/integration/test-data/end-to-end-prove-all index 4e4c53ec1..18565c4ce 100644 --- a/src/tests/integration/test-data/end-to-end-prove-all +++ b/src/tests/integration/test-data/end-to-end-prove-all @@ -1,4 +1,12 @@ CounterTest.test_Increment() +RandomVarTest.test_randomBool() +RandomVarTest.test_randomAddress() +RandomVarTest.test_randomUint() +RandomVarTest.test_randomUint_192() +RandomVarTest.test_randomUint_Range(uint256,uint256) +RandomVarTest.test_randomBytes_length(uint256) +RandomVarTest.test_randomBytes4_length() +RandomVarTest.test_randomBytes8_length() TransientStorageTest.testTransientStoreLoad(uint256,uint256) UnitTest.test_assertEq_address_err() UnitTest.test_assertEq_bool_err() diff --git a/src/tests/integration/test-data/src/RandomVar.t.sol b/src/tests/integration/test-data/src/RandomVar.t.sol new file mode 100644 index 000000000..59b4970cd --- /dev/null +++ b/src/tests/integration/test-data/src/RandomVar.t.sol @@ -0,0 +1,56 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.13; + +import {Test, console} from "forge-std/Test.sol"; + +contract RandomVarTest is Test { + uint256 constant length_limit = 72; + + function test_randomBool() public view { + bool freshBool = vm.randomBool(); + vm.assume(freshBool); + } + + function test_randomAddress() public { + address freshAddress = vm.randomAddress(); + assertNotEq(freshAddress, address(this)); + assertNotEq(freshAddress, address(vm)); + } + + function test_randomBytes_length(uint256 len) public view { + vm.assume(0 < len); + vm.assume(len <= length_limit); + bytes memory freshBytes = vm.randomBytes(len); + assertEq(freshBytes.length, len); + } + + function test_randomBytes4_length() public view { + bytes4 freshBytes = vm.randomBytes4(); + assertEq(freshBytes.length, 4); + } + + function test_randomBytes8_length() public view { + bytes8 freshBytes = vm.randomBytes8(); + assertEq(freshBytes.length, 8); + } + + function test_randomUint_192() public { + uint256 randomUint192 = vm.randomUint(192); + + assert(0 <= randomUint192); + assert(randomUint192 <= type(uint192).max); + } + + function test_randomUint_Range(uint256 min, uint256 max) public { + vm.assume(max >= min); + uint256 rand = vm.randomUint(min, max); + assertTrue(rand >= min, "rand >= min"); + assertTrue(rand <= max, "rand <= max"); + } + + function test_randomUint() public { + uint256 rand = vm.randomUint(); + assertTrue(rand >= type(uint256).min); + assertTrue(rand <= type(uint256).max); + } +} \ No newline at end of file