From 3ce25882ffa4e8bc0c14c93409b04729087b7be5 Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Fri, 8 Nov 2024 15:15:29 +0700 Subject: [PATCH] Support `random*` cheatcodes except for `randomInt` for signed ints --- src/kontrol/kdist/cheatcodes.md | 54 +++++++++++++++---- .../test-data/end-to-end-prove-all | 1 + .../integration/test-data/src/RandomVar.t.sol | 12 +++++ 3 files changed, 57 insertions(+), 10 deletions(-) create mode 100644 src/tests/integration/test-data/src/RandomVar.t.sol diff --git a/src/kontrol/kdist/cheatcodes.md b/src/kontrol/kdist/cheatcodes.md index 4b77a78ec..31e95b6a9 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]: @@ -362,19 +362,42 @@ This rule then takes the two addresses using `#asWord(#range(ARGS, 0, 32))` and #### `freshUInt` - Returns a single symbolic unsigned integer. ``` -function freshUInt(uint8) external returns (uint256); +function freshUInt(uint256) external returns (uint256); +function randomUInt(uint256) external returns (uint256); ``` -`cheatcode.call.freshUInt` will match when the `freshUInt` cheat code function is called. +`cheatcode.call.freshUInt` will match when the `freshUInt` or `randomUInt` 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.freshUInt]: #cheatcode_call SELECTOR ARGS => .K ... _ => #buf(32, ?WORD) - requires SELECTOR ==Int selector ( "freshUInt(uint8)" ) - andBool 0 #cheatcode_call SELECTOR ARGS => .K ... + _ => #buf(32, ?WORD) + requires SELECTOR ==Int 3592095003 // selector ( "randomUint(uint256,uint256)" ) + andBool 0 #cheatcode_call SELECTOR _ => .K ... _ => #buf(32, ?WORD) requires SELECTOR ==Int selector ( "freshBool()" ) + orBool SELECTOR ==Int selector ( "randomBool()" ) ensures #rangeBool(?WORD) [preserves-definedness] ``` @@ -400,9 +425,10 @@ 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); ``` -`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,6 +439,7 @@ 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)" ) + orBool SELECTOR ==Int selector ( "randomBytes(uint256)" ) ensures lengthBytes(?BYTES) ==Int #asWord(ARGS) [preserves-definedness] ``` @@ -421,9 +448,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 +459,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] ``` @@ -1591,10 +1620,15 @@ Selectors for **implemented** cheat code functions. rule ( selector ( "sign(uint256,bytes32)" ) => 3812747940 ) rule ( selector ( "symbolicStorage(address)" ) => 769677742 ) rule ( selector ( "setArbitraryStorage(address)" ) => 3781367863 ) - rule ( selector ( "freshUInt(uint8)" ) => 625253732 ) + rule ( selector ( "freshUInt(uint256)" ) => 1430414212 ) + rule ( selector ( "randomUInt(uint256)" ) => 3628412988 ) + 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 ( "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..cbcdb278f 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,5 @@ CounterTest.test_Increment() +RandomVarTest.test_randomBool() 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..8fe6bc4bf --- /dev/null +++ b/src/tests/integration/test-data/src/RandomVar.t.sol @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.13; + +import {Test, console} from "forge-std/Test.sol"; + +contract RandomVarTest is Test { + function test_randomBool() public { + uint256 fresh_uint256 = vm.randomBool(); + assertGe(fresh_uint256, 0); + assertLe(fresh_uint256, 1); + } +} \ No newline at end of file