Add support for most 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]:
@@ -378,20 +378,67 @@ 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]:
+         <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 will match when the `randomUint()` cheat code function is called.
+This 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]
+```
+
+The following rule will match when the `randomUint(uint256,uint256)` cheat code function is called.
+This rule returns a symbolic integer of 256 bytes which is greater than or equal to the first argument and less than or equal to the second argument.
+
+```{.k .symbolic}
+    rule [cheatcode.call.randomUint256Range]:
+         <k> #cheatcode_call SELECTOR ARGS => .K ... </k>
+         <output> _ => #buf(32, ?WORD) </output>
+      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}
     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 +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,24 +463,53 @@ 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> _ =>
+            ?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> _ =>
+            ?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 +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 )

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()

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