Add support for random cheatcodes

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]:
@@ -372,26 +372,89 @@ This rule returns a symbolic integer of up to the bit width that was sent as an
     rule [cheatcode.call.freshUInt]:
          <k> #cheatcode_call SELECTOR ARGS => .K ... </k>
          <output> _ => #buf(32, ?WORD) </output>
-      requires SELECTOR ==Int selector ( "freshUInt(uint8)" )
-       andBool 0 <Int #asWord(ARGS) andBool #asWord(ARGS) <=Int 32
+      requires 0 <Int #asWord(ARGS) andBool #asWord(ARGS) <=Int 32
+       andBool SELECTOR ==Int selector ( "freshUInt(uint8)" )
        ensures 0 <=Int ?WORD andBool ?WORD <Int 2 ^Int (8 *Int #asWord(ARGS))
        [preserves-definedness]
 ```
 
+#### `randomUint` - Returns a single symbolic unsigned integer of a given size.
+
+```
+function randomUint() external returns (uint256);
+function randomUint(uint256) external returns (uint256);
+```
+
+`cheatcode.call.randomUint` will match when the `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.randomUint]:
+         <k> #cheatcode_call SELECTOR ARGS => .K ... </k>
+         <output> _ => #buf(32, ?WORD) </output>
+      requires 0 <Int #asWord(ARGS) andBool #asWord(ARGS) <=Int 256
+       andBool SELECTOR ==Int selector ( "randomUint(uint256)" )
+       ensures 0 <=Int ?WORD andBool ?WORD <Int 2 ^Int #asWord(ARGS)
+       [preserves-definedness]
+```
+
+The following rule returns a symbolic integer of 256 bytes.
+
+```{.k .symbolic}
+    rule [cheatcode.call.randomUint256]:
+         <k> #cheatcode_call SELECTOR _ => .K ... </k>
+         <output> _ => #buf(32, ?WORD) </output>
+      requires SELECTOR ==Int selector ( "randomUint()" )
+       ensures 0 <=Int ?WORD andBool ?WORD <Int 2 ^Int 256
+       [preserves-definedness]
+```
+
+#### `randomInt` - Returns a single symbolic int256 value.
+
+```
+function randomInt(uint256) external returns (int256)
+function randomInt() external returns (int256)
+```
+
+`cheatcode.call.randomInt` will match when the `randomInt()` or `randomInt()` cheat code function is called.
+This rule returns a symbolic signed integer.
+
+```{.k .symbolic}
+    rule [cheatcode.call.randomInt256]:
+         <k> #cheatcode_call SELECTOR _ => .K ... </k>
+         <output> _ => #buf(32, ?WORD) </output>
+      requires SELECTOR ==Int selector ( "randomInt()" )
+       ensures -2 ^Int 255 <=Int ?WORD andBool ?WORD <Int 2 ^Int 255
+              [preserves-definedness]
+```
+
+```{.k .symbolic}
+    rule [cheatcode.call.randomInt]:
+         <k> #cheatcode_call SELECTOR ARGS => .K ... </k>
+         <output> _ => #buf(32, ?WORD) </output>
+      requires SELECTOR ==Int selector ( "randomInt(uint256)" )
+       andBool 0 <Int #asWord(ARGS) andBool #asWord(ARGS) <=Int 256
+       ensures -2 ^Int (#asWord(ARGS) -Int 1) <=Int ?WORD
+        andBool ?WORD <Int 2 ^Int (#asWord(ARGS) -Int 1)
+       [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}
     rule [cheatcode.call.freshBool]:
          <k> #cheatcode_call SELECTOR _ => .K ... </k>
          <output> _ => #buf(32, ?WORD) </output>
       requires SELECTOR ==Int selector ( "freshBool()" )
+         orBool SELECTOR ==Int selector ( "randomBool()" )
        ensures #rangeBool(?WORD)
        [preserves-definedness]
 ```
@@ -400,9 +463,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,24 +479,55 @@ 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 )
          </output>
       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]:
+         <k> #cheatcode_call SELECTOR _ => .K ... </k>
+         <output> _ =>
+            #buf( 32, 32 ) +Bytes #buf( 32, 4 ) +Bytes ?BYTES
+            +Bytes #buf ( 28 , 0 )
+         </output>
+      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]:
+         <k> #cheatcode_call SELECTOR _ => .K ... </k>
+         <output> _ =>
+            #buf( 32, 32 ) +Bytes #buf( 32, 8 ) +Bytes ?BYTES
+            +Bytes #buf ( 24 , 0 )
+         </output>
+      requires SELECTOR ==Int selector ( "randomBytes8()" )
+       ensures lengthBytes(?BYTES) ==Int 8
       [preserves-definedness]
 ```
 
 #### `freshAddress` - Returns a single symbolic address.
 
 ```
 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}
     rule [foundry.call.freshAddress]:
          <k> #cheatcode_call SELECTOR _ => .K ... </k>
          <output> _ => #buf(32, ?WORD) </output>
       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 +1689,19 @@ 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 ( "randomInt(uint256)" )                       => 310663526  )
+    rule ( selector ( "randomInt()" )                              => 287248898  )
     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 )

src/tests/integration/test-data/end-to-end-prove-all

@@ -1,4 +1,13 @@
 CounterTest.test_Increment()
+RandomVarTest.test_randomBool()
+RandomVarTest.test_randomAddress()
+RandomVarTest.test_randomUint()
+RandomVarTest.test_randomUint(uint256)
+RandomVarTest.test_randomInt()
+RandomVarTest.test_randomInt(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()

src/tests/integration/test-data/src/RandomVar.t.sol

@@ -0,0 +1,73 @@
+// 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_randomUint(uint256 x) public view {
+        vm.assume(0 < x);
+        vm.assume(x <= 256);
+        uint256 freshUint = vm.randomUint(x);
+
+        assert(0 <= freshUint);
+        assert(freshUint <= 2 ** x - 1);
+    }
+
+    function test_randomUint() public {
+        uint256 freshUint = vm.randomUint();
+
+        assert(0 <= freshUint);
+        assert(freshUint <= 2 ** 256 - 1);
+    }
+
+    function test_randomInt(uint256 x) public view {
+        vm.assume(0 < x);
+        vm.assume(x <= 256);
+
+        int256 minInt256 = -2 ** (x - 1);
+        int256 maxInt256 = int256(2 ** (x - 1) - 1);
+
+        int256 freshInt = vm.randomInt(x);
+
+        assert(minInt256 <= freshInt);
+        assert(freshInt <= maxInt256);
+    }
+
+    function test_randomInt() public view {
+        int256 freshInt = vm.randomInt();
+
+        assert(-2 ** 255 <= freshInt);
+        assert(freshInt <= 2 ** 255 - 1);
+    }
+
+    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 {
+        bytes8 freshBytes = vm.randomBytes4();
+        assertEq(freshBytes.length, 4);
+    }
+
+    function test_randomBytes8_length() public view {
+        bytes8 fresh_bytes = vm.randomBytes8();
+        assertEq(fresh_bytes.length, 8);
+    }
+}