Skip to content

Commit 5f496c3

Browse files
palinatolmachanvacaru
palinatolmach
and
anvacaru
authored
Add support for most random cheatcodes (#877)
* Support `random*` cheatcodes except for `randomInt` for signed ints * `randomUInt` signature fix * Add remaining `random*` cheatcodes * Add `random*` tests to end-to-end tests * Fix capitalization in `randomUInt` * Fix `bytes` rules, fix `randomInt` test typo * Fix `uint8` signature * Update `randomBytes` implementation, leave passing tests for the first PR * Add `test_randomUint_Range` * Add `randomUint(uint256,uint256)` implementation * Fix implementation for `randomUint256Range` * Fix `test_randomUint_192` name in `end-to-end-prove-all` * Minor cleanup in `cheatcodes.md` * Add a test for `vm.randomUint()` * Fix `test_randomUint_Range(uint256,uint256)` signature * Fix whitespaces in rules one Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> * Fix whitespaces in rules two Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> * Rename `randomUintWidth` rule, add descriptions for other rules --------- Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com>
1 parent 75bcce3 commit 5f496c3

File tree

3 files changed

+156
-5
lines changed

3 files changed

+156
-5
lines changed

‎src/kontrol/kdist/cheatcodes.md

Lines changed: 92 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -121,7 +121,7 @@ function deal(address who, uint256 newBalance) external;
121121
```
122122

123123
`cheatcode.call.deal` will match when the `deal` cheat code function is called.
124-
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.
124+
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.
125125

126126
```k
127127
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
378378
[preserves-definedness]
379379
```
380380

381+
#### `randomUint` - Returns a single symbolic unsigned integer of a given size.
382+
383+
```
384+
function randomUint() external returns (uint256);
385+
function randomUint(uint256) external returns (uint256);
386+
function randomUint(uint256,uint256) external returns (uint256);
387+
```
388+
389+
`cheatcode.call.randomUintWidth` will match when the `randomUint(uint256)` cheat code function is called.
390+
This rule returns a symbolic integer of up to the bit width that was sent as an argument.
391+
392+
```{.k .symbolic}
393+
rule [cheatcode.call.randomUintWidth]:
394+
<k> #cheatcode_call SELECTOR ARGS => .K ... </k>
395+
<output> _ => #buf(32, ?WORD) </output>
396+
requires 0 <Int #asWord(ARGS) andBool #asWord(ARGS) <=Int 256
397+
andBool SELECTOR ==Int selector ( "randomUint(uint256)" )
398+
ensures 0 <=Int ?WORD andBool ?WORD <Int 2 ^Int #asWord(ARGS)
399+
[preserves-definedness]
400+
```
401+
402+
The following rule will match when the `randomUint()` cheat code function is called.
403+
This rule returns a symbolic integer of 256 bytes.
404+
405+
```{.k .symbolic}
406+
rule [cheatcode.call.randomUint256]:
407+
<k> #cheatcode_call SELECTOR _ => .K ... </k>
408+
<output> _ => #buf(32, ?WORD) </output>
409+
requires SELECTOR ==Int selector ( "randomUint()" )
410+
ensures 0 <=Int ?WORD andBool ?WORD <Int 2 ^Int 256
411+
[preserves-definedness]
412+
```
413+
414+
The following rule will match when the `randomUint(uint256,uint256)` cheat code function is called.
415+
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.
416+
417+
```{.k .symbolic}
418+
rule [cheatcode.call.randomUint256Range]:
419+
<k> #cheatcode_call SELECTOR ARGS => .K ... </k>
420+
<output> _ => #buf(32, ?WORD) </output>
421+
requires SELECTOR ==Int selector ( "randomUint(uint256,uint256)" )
422+
ensures #asWord(#range(ARGS, 0, 32)) <=Int ?WORD andBool ?WORD <=Int #asWord(#range(ARGS, 32, 32))
423+
[preserves-definedness]
424+
```
425+
381426
#### `freshBool` - Returns a single symbolic boolean.
382427

383428
```
384429
function freshBool() external returns (bool);
430+
function randomBool() external returns (bool);
385431
```
386432

387-
`cheatcode.call.freshBool` will match when the `freshBool` cheat code function is called.
433+
`cheatcode.call.freshBool` will match when the `freshBool` or `randomBool` cheat code function is called.
388434
This rule returns a symbolic boolean value being either 0 (false) or 1 (true).
389435

390436
```{.k .symbolic}
391437
rule [cheatcode.call.freshBool]:
392438
<k> #cheatcode_call SELECTOR _ => .K ... </k>
393439
<output> _ => #buf(32, ?WORD) </output>
394440
requires SELECTOR ==Int selector ( "freshBool()" )
441+
orBool SELECTOR ==Int selector ( "randomBool()" )
395442
ensures #rangeBool(?WORD)
396443
[preserves-definedness]
397444
```
@@ -400,9 +447,12 @@ This rule returns a symbolic boolean value being either 0 (false) or 1 (true).
400447

401448
```
402449
function freshBytes(uint256) external returns (bytes memory);
450+
function randomBytes(uint256) external returns (bytes memory);
451+
function randomBytes4() external view returns (bytes4);
452+
function randomBytes8() external view returns (bytes8);
403453
```
404454

405-
`cheatcode.call.freshBytes` will match when the `freshBytes` cheat code function is called.
455+
`cheatcode.call.freshBytes` will match when the `freshBytes` or `randomBytes` cheat code function is called.
406456
This rule returns a fully symbolic byte array value of the given length.
407457

408458
```{.k .symbolic}
@@ -413,24 +463,53 @@ This rule returns a fully symbolic byte array value of the given length.
413463
+Bytes #buf ( ( ( notMaxUInt5 &Int ( #asWord(ARGS) +Int maxUInt5 ) ) -Int #asWord(ARGS) ) , 0 )
414464
</output>
415465
requires SELECTOR ==Int selector ( "freshBytes(uint256)" )
416-
ensures lengthBytes(?BYTES) ==Int #asWord(ARGS)
466+
orBool SELECTOR ==Int selector ( "randomBytes(uint256)" )
467+
ensures lengthBytes(?BYTES) ==Int #asWord(ARGS)
468+
[preserves-definedness]
469+
```
470+
471+
This rule returns a fully symbolic byte array value of length 4.
472+
473+
```{.k .symbolic}
474+
rule [cheatcode.call.randomBytes4]:
475+
<k> #cheatcode_call SELECTOR _ => .K ... </k>
476+
<output> _ =>
477+
?BYTES +Bytes #buf ( 28 , 0 )
478+
</output>
479+
requires SELECTOR ==Int selector ( "randomBytes4()" )
480+
ensures lengthBytes(?BYTES) ==Int 4
481+
[preserves-definedness]
482+
```
483+
484+
This rule returns a fully symbolic byte array value of length 8.
485+
486+
```{.k .symbolic}
487+
rule [cheatcode.call.randomBytes8]:
488+
<k> #cheatcode_call SELECTOR _ => .K ... </k>
489+
<output> _ =>
490+
?BYTES +Bytes #buf ( 24 , 0 )
491+
</output>
492+
requires SELECTOR ==Int selector ( "randomBytes8()" )
493+
ensures lengthBytes(?BYTES) ==Int 8
417494
[preserves-definedness]
418495
```
419496

420497
#### `freshAddress` - Returns a single symbolic address.
421498

422499
```
423500
function freshAddress() external returns (address);
501+
function randomAddress() external returns (address);
424502
```
425503

426-
`foundry.call.freshAddress` will match when the `freshAddress` cheat code function is called.
504+
`foundry.call.freshAddress` will match when the `freshAddress` or `randomAddress` cheat code function is called.
427505
This rule returns a symbolic address value.
428506

429507
```{.k .symbolic}
430508
rule [foundry.call.freshAddress]:
431509
<k> #cheatcode_call SELECTOR _ => .K ... </k>
432510
<output> _ => #buf(32, ?WORD) </output>
433511
requires SELECTOR ==Int selector ( "freshAddress()" )
512+
orBool SELECTOR ==Int selector ( "randomAddress()" )
434513
ensures #rangeAddress(?WORD) andBool ?WORD =/=Int #address(FoundryTest) andBool ?WORD =/=Int #address(FoundryCheat)
435514
[preserves-definedness]
436515
```
@@ -1592,9 +1671,17 @@ Selectors for **implemented** cheat code functions.
15921671
rule ( selector ( "symbolicStorage(address)" ) => 769677742 )
15931672
rule ( selector ( "setArbitraryStorage(address)" ) => 3781367863 )
15941673
rule ( selector ( "freshUInt(uint8)" ) => 625253732 )
1674+
rule ( selector ( "randomUint(uint256)" ) => 3481396892 )
1675+
rule ( selector ( "randomUint()" ) => 621954864 )
1676+
rule ( selector ( "randomUint(uint256,uint256)" ) => 3592095003 )
15951677
rule ( selector ( "freshBool()" ) => 2935720297 )
1678+
rule ( selector ( "randomBool()" ) => 3451987645 )
15961679
rule ( selector ( "freshBytes(uint256)" ) => 1389402351 )
1680+
rule ( selector ( "randomBytes(uint256)" ) => 1818047145 )
1681+
rule ( selector ( "randomBytes4()" ) => 2608649593 )
1682+
rule ( selector ( "randomBytes8()" ) => 77050021 )
15971683
rule ( selector ( "freshAddress()" ) => 2363359817 )
1684+
rule ( selector ( "randomAddress()" ) => 3586058741 )
15981685
rule ( selector ( "prank(address)" ) => 3395723175 )
15991686
rule ( selector ( "prank(address,address)" ) => 1206193358 )
16001687
rule ( selector ( "allowCallsToAddress(address)" ) => 1850795572 )

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,12 @@
11
CounterTest.test_Increment()
2+
RandomVarTest.test_randomBool()
3+
RandomVarTest.test_randomAddress()
4+
RandomVarTest.test_randomUint()
5+
RandomVarTest.test_randomUint_192()
6+
RandomVarTest.test_randomUint_Range(uint256,uint256)
7+
RandomVarTest.test_randomBytes_length(uint256)
8+
RandomVarTest.test_randomBytes4_length()
9+
RandomVarTest.test_randomBytes8_length()
210
TransientStorageTest.testTransientStoreLoad(uint256,uint256)
311
UnitTest.test_assertEq_address_err()
412
UnitTest.test_assertEq_bool_err()

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

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
// SPDX-License-Identifier: UNLICENSED
2+
pragma solidity ^0.8.13;
3+
4+
import {Test, console} from "forge-std/Test.sol";
5+
6+
contract RandomVarTest is Test {
7+
uint256 constant length_limit = 72;
8+
9+
function test_randomBool() public view {
10+
bool freshBool = vm.randomBool();
11+
vm.assume(freshBool);
12+
}
13+
14+
function test_randomAddress() public {
15+
address freshAddress = vm.randomAddress();
16+
assertNotEq(freshAddress, address(this));
17+
assertNotEq(freshAddress, address(vm));
18+
}
19+
20+
function test_randomBytes_length(uint256 len) public view {
21+
vm.assume(0 < len);
22+
vm.assume(len <= length_limit);
23+
bytes memory freshBytes = vm.randomBytes(len);
24+
assertEq(freshBytes.length, len);
25+
}
26+
27+
function test_randomBytes4_length() public view {
28+
bytes4 freshBytes = vm.randomBytes4();
29+
assertEq(freshBytes.length, 4);
30+
}
31+
32+
function test_randomBytes8_length() public view {
33+
bytes8 freshBytes = vm.randomBytes8();
34+
assertEq(freshBytes.length, 8);
35+
}
36+
37+
function test_randomUint_192() public {
38+
uint256 randomUint192 = vm.randomUint(192);
39+
40+
assert(0 <= randomUint192);
41+
assert(randomUint192 <= type(uint192).max);
42+
}
43+
44+
function test_randomUint_Range(uint256 min, uint256 max) public {
45+
vm.assume(max >= min);
46+
uint256 rand = vm.randomUint(min, max);
47+
assertTrue(rand >= min, "rand >= min");
48+
assertTrue(rand <= max, "rand <= max");
49+
}
50+
51+
function test_randomUint() public {
52+
uint256 rand = vm.randomUint();
53+
assertTrue(rand >= type(uint256).min);
54+
assertTrue(rand <= type(uint256).max);
55+
}
56+
}

0 commit comments

Comments
 (0)