Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/master' into release
Browse files Browse the repository at this point in the history
  • Loading branch information
rv-jenkins committed Nov 20, 2024
2 parents 577e6ce + 5f496c3 commit 9bd8ae7
Show file tree
Hide file tree
Showing 3 changed files with 156 additions and 5 deletions.
97 changes: 92 additions & 5 deletions src/kontrol/kdist/cheatcodes.md
Original file line number Diff line number Diff line change
Expand Up @@ -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]:
Expand Down Expand Up @@ -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]
```
Expand All @@ -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}
Expand All @@ -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]
```
Expand Down Expand Up @@ -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 )
Expand Down
8 changes: 8 additions & 0 deletions src/tests/integration/test-data/end-to-end-prove-all
Original file line number Diff line number Diff line change
@@ -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()
Expand Down
56 changes: 56 additions & 0 deletions src/tests/integration/test-data/src/RandomVar.t.sol
Original file line number Diff line number Diff line change
@@ -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);
}
}

0 comments on commit 9bd8ae7

Please sign in to comment.