Skip to content

Bound MIXHASH_CELL to rangeUInt256 #1111

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
anvacaru merged 5 commits into from
Dec 8, 2025
Merged

Bound MIXHASH_CELL to rangeUInt256 #1111

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
df36db3
add new unit test
anvacaru Nov 28, 2025
322b92c
Merge branch 'master' into mixhash_rangeUInt256
anvacaru Nov 29, 2025
d8196ee
Update expected output files
rv-auditor Nov 29, 2025
9cba786
Merge branch 'master' into mixhash_rangeUInt256
anvacaru Dec 1, 2025
20057ae
Merge branch 'master' into mixhash_rangeUInt256
anvacaru Dec 5, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions src/kontrol/utils.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -306,6 +306,7 @@ def replace_k_words(text: str) -> str:
'#Equals': '==',
'NUMBER_CELL': 'block.number',
'TIMESTAMP_CELL': 'block.timestamp',
'MIXHASH_CELL': 'block.prevrandao',
':Int': '',
':Bytes': '',
}
Expand Down
3 changes: 2 additions & 1 deletion src/tests/integration/test-data/end-to-end-prove-all
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,4 +56,5 @@ UnitTest.test_assertNotEq(bytes32,bytes32)
UnitTest.test_assertNotEq(int256,int256)
UnitTest.test_assertTrue_err()
UnitTest.test_assertTrue(bool)
UnitTest.test_checkInitialBalance(uint256)
UnitTest.test_checkInitialBalance(uint256)
UnitTest.test_prevrandao_nonnegative()
22 changes: 11 additions & 11 deletions src/tests/integration/test-data/show/UnitTest.test_checkInitialBalance(uint256).expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,13 +4,13 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
│ src: test/Unit.t.sol:6:458
│ src: test/Unit.t.sol:6:462
│ method: test%UnitTest.test_checkInitialBalance(uint256)
│
│ (880 steps)
├─ 3
│ k: #consoleLog 3054400204 b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0 ...
│ pc: 16676
│ pc: 16687
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
│ src: lib/forge-std/src/console.sol:11:22
Expand All @@ -19,7 +19,7 @@
│ (1 step)
├─ 4
│ k: #refund 0 ~> 1 ~> #push ~> #setLocalMem 0 0 b"" ~> #pc [ STATICCALL ] ~> #execut ...
│ pc: 16676
│ pc: 16687
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
│ src: lib/forge-std/src/console.sol:11:22
Expand All @@ -28,7 +28,7 @@
│ (646 steps)
├─ 5
│ k: #consoleLog 3054400204 b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0 ...
│ pc: 16676
│ pc: 16687
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
│ src: lib/forge-std/src/console.sol:11:22
Expand All @@ -37,7 +37,7 @@
│ (1 step)
├─ 6
│ k: #refund 0 ~> 1 ~> #push ~> #setLocalMem 0 0 b"" ~> #pc [ STATICCALL ] ~> #execut ...
│ pc: 16676
│ pc: 16687
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
│ src: lib/forge-std/src/console.sol:11:22
Expand All @@ -46,7 +46,7 @@
│ (205 steps)
├─ 7 (terminal)
│ k: #halt ~> CONTINUATION:K
│ pc: 1038
│ pc: 1049
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
│ src: test/Unit.t.sol:135:139
Expand Down Expand Up @@ -115,7 +115,7 @@ module SUMMARY-TEST%UNITTEST.TEST-CHECKINITIALBALANCE(UINT256):0
0
</callValue>
<wordStack>
( .WordStack => ( #address ( FoundryConsole ) : ( 192 : ( 2095 : ( 192 : ( 2280 : ( maxUInt96 : ( 128 : ( 10324 : ( maxUInt96 : ( KV0_amount:Int : ( 1037 : ( 3050190935 : .WordStack ) ) ) ) ) ) ) ) ) ) ) ) )
( .WordStack => ( #address ( FoundryConsole ) : ( 192 : ( 2106 : ( 192 : ( 2291 : ( maxUInt96 : ( 128 : ( 10335 : ( maxUInt96 : ( KV0_amount:Int : ( 1048 : ( 3050190935 : .WordStack ) ) ) ) ) ) ) ) ) ) ) ) )
</wordStack>
<localMem>
( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01d\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x84\xb6\x0er\xcc\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" )
Expand Down Expand Up @@ -341,7 +341,7 @@ module SUMMARY-TEST%UNITTEST.TEST-CHECKINITIALBALANCE(UINT256):0
0
</callValue>
<wordStack>
( #address ( FoundryConsole ) : ( 192 : ( 2095 : ( 192 : ( 2280 : ( maxUInt96 : ( 128 : ( 10324 : ( maxUInt96 : ( KV0_amount:Int : ( 1037 : ( 3050190935 : .WordStack ) ) ) ) ) ) ) ) ) ) ) )
( #address ( FoundryConsole ) : ( 192 : ( 2106 : ( 192 : ( 2291 : ( maxUInt96 : ( 128 : ( 10335 : ( maxUInt96 : ( KV0_amount:Int : ( 1048 : ( 3050190935 : .WordStack ) ) ) ) ) ) ) ) ) ) ) )
</wordStack>
<localMem>
b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01d\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x84\xb6\x0er\xcc\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"
Expand Down Expand Up @@ -567,7 +567,7 @@ module SUMMARY-TEST%UNITTEST.TEST-CHECKINITIALBALANCE(UINT256):0
0
</callValue>
<wordStack>
( #address ( FoundryConsole ) : ( ( 192 => 420 ) : ( 2095 : ( ( 192 => 420 ) : ( 2280 : ( ( maxUInt96 => KV0_amount:Int ) : ( ( 128 => 356 ) : ( ( 10324 => 10372 ) : ( maxUInt96 : ( KV0_amount:Int : ( 1037 : ( 3050190935 : .WordStack ) ) ) ) ) ) ) ) ) ) ) )
( #address ( FoundryConsole ) : ( ( 192 => 420 ) : ( 2106 : ( ( 192 => 420 ) : ( 2291 : ( ( maxUInt96 => KV0_amount:Int ) : ( ( 128 => 356 ) : ( ( 10335 => 10383 ) : ( maxUInt96 : ( KV0_amount:Int : ( 1048 : ( 3050190935 : .WordStack ) ) ) ) ) ) ) ) ) ) ) )
</wordStack>
<localMem>
( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01d\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x84\xb6\x0er\xcc\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02H\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x84\xb6\x0er\xcc\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0eSymbolic value\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x84\xb6\x0er\xcc\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , KV0_amount:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0eSymbolic value\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" )
Expand Down Expand Up @@ -793,7 +793,7 @@ module SUMMARY-TEST%UNITTEST.TEST-CHECKINITIALBALANCE(UINT256):0
0
</callValue>
<wordStack>
( #address ( FoundryConsole ) : ( 420 : ( 2095 : ( 420 : ( 2280 : ( KV0_amount:Int : ( 356 : ( 10372 : ( maxUInt96 : ( KV0_amount:Int : ( 1037 : ( 3050190935 : .WordStack ) ) ) ) ) ) ) ) ) ) ) )
( #address ( FoundryConsole ) : ( 420 : ( 2106 : ( 420 : ( 2291 : ( KV0_amount:Int : ( 356 : ( 10383 : ( maxUInt96 : ( KV0_amount:Int : ( 1048 : ( 3050190935 : .WordStack ) ) ) ) ) ) ) ) ) ) ) )
</wordStack>
<localMem>
b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02H\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x84\xb6\x0er\xcc\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0eSymbolic value\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x84\xb6\x0er\xcc\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , KV0_amount:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0eSymbolic value\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"
Expand Down Expand Up @@ -1021,7 +1021,7 @@ module SUMMARY-TEST%UNITTEST.TEST-CHECKINITIALBALANCE(UINT256):0
0
</callValue>
<wordStack>
( ( #address ( FoundryConsole ) => 3050190935 ) : ( ( 420 : ( 2095 : ( 420 : ( 2280 : ( KV0_amount:Int : ( 356 : ( 10372 : ( maxUInt96 : ( KV0_amount:Int : ( 1037 : ( 3050190935 : .WordStack ) ) ) ) ) ) ) ) ) ) ) => .WordStack ) )
( ( #address ( FoundryConsole ) => 3050190935 ) : ( ( 420 : ( 2106 : ( 420 : ( 2291 : ( KV0_amount:Int : ( 356 : ( 10383 : ( maxUInt96 : ( KV0_amount:Int : ( 1048 : ( 3050190935 : .WordStack ) ) ) ) ) ) ) ) ) ) ) => .WordStack ) )
</wordStack>
<localMem>
b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02H\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x84\xb6\x0er\xcc\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16Test contract balance:\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0eSymbolic value\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x84\xb6\x0er\xcc\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , KV0_amount:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0eSymbolic value\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"
Expand Down
10 changes: 7 additions & 3 deletions src/tests/integration/test-data/show/UnitTestCounterexampleTest.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -400,7 +400,7 @@ contract UnitTest is Test {
val1[2] = 0; val2[2] = 0;
string memory err = "throw test";
string memory err_output = "throw test: [-1, 2, 0] != [1, -2, 0]";
vm.expectRevert(bytes(err_output));
vm.expectRevert(bytes(err_output));
assertEq(val1, val2, err);
}

Expand All @@ -425,9 +425,9 @@ contract UnitTest is Test {
val1[2] = 2; val2[2] = 12;
val1[3] = 3; val2[3] = 13;
val1[4] = 4; val2[4] = 14;
string memory err = "throw test";
string memory err = "throw test";
string memory err_output = "throw test: [0, 1, 2, 3, 4] != [10, 11, 12, 13, 14]";
vm.expectRevert(bytes(err_output));
vm.expectRevert(bytes(err_output));
assertEq(val1, val2, err);
}

Expand All @@ -444,6 +444,10 @@ contract UnitTest is Test {
assert(value != 10);
}

function test_prevrandao_nonnegative() public view {
assert(block.prevrandao >= 0);
}

/****************************
* Internal helper functions *
*****************************/
Expand Down
10 changes: 7 additions & 3 deletions src/tests/integration/test-data/test/Unit.t.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -400,7 +400,7 @@ contract UnitTest is Test {
val1[2] = 0; val2[2] = 0;
string memory err = "throw test";
string memory err_output = "throw test: [-1, 2, 0] != [1, -2, 0]";
vm.expectRevert(bytes(err_output));
vm.expectRevert(bytes(err_output));
assertEq(val1, val2, err);
}

Expand All @@ -425,9 +425,9 @@ contract UnitTest is Test {
val1[2] = 2; val2[2] = 12;
val1[3] = 3; val2[3] = 13;
val1[4] = 4; val2[4] = 14;
string memory err = "throw test";
string memory err = "throw test";
string memory err_output = "throw test: [0, 1, 2, 3, 4] != [10, 11, 12, 13, 14]";
vm.expectRevert(bytes(err_output));
vm.expectRevert(bytes(err_output));
assertEq(val1, val2, err);
}

Expand All @@ -444,6 +444,10 @@ contract UnitTest is Test {
assert(value != 10);
}

function test_prevrandao_nonnegative() public view {
assert(block.prevrandao >= 0);
}

/****************************
* Internal helper functions *
*****************************/
Expand Down