Skip to content

Commit

Permalink
integrate CREATEDACCOUNTS_CELL in the Kontrol initial state; update e…
Browse files Browse the repository at this point in the history 
…xpected output
  • Loading branch information
@anvacaru
anvacaru committed Jan 14, 2025
1 parent a982693 commit 1d8874a
Show file tree
Hide file tree
Showing 20 changed files with 637 additions and 0 deletions.
1 change: 1 addition & 0 deletions src/kontrol/prove.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1064,6 +1064,7 @@ def _init_cterm(
'ACCESSEDSTORAGE_CELL': map_empty(),
'INTERIMSTATES_CELL': list_empty(),
'TOUCHEDACCOUNTS_CELL': set_empty(),
'CREATEDACCOUNTS_CELL': set_empty(),
'STATIC_CELL': FALSE,
'ACCOUNTS_CELL': KEVM.accounts(init_account_list),
}
Expand Down
3 changes: 3 additions & 0 deletions src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -107,6 +107,9 @@ module SUMMARY-TEST%ACCOUNTPARAMSTEST.TESTDEALCONCRETE():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
...
</substate>
<origin>
Expand Down
3 changes: 3 additions & 0 deletions src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -108,6 +108,9 @@ module SUMMARY-TEST%ADDRTEST.TEST-ADDR-TRUE():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
...
</substate>
<origin>
Expand Down
15 changes: 15 additions & 0 deletions src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -141,6 +141,9 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
...
</substate>
<origin>
Expand Down Expand Up @@ -380,6 +383,9 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
...
</substate>
<origin>
Expand Down Expand Up @@ -618,6 +624,9 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
...
</substate>
<origin>
Expand Down Expand Up @@ -858,6 +867,9 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
...
</substate>
<origin>
Expand Down Expand Up @@ -1098,6 +1110,9 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
...
</substate>
<origin>
Expand Down
18 changes: 18 additions & 0 deletions src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -141,6 +141,9 @@ Node 10:
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
...
</substate>
<origin>
Expand Down Expand Up @@ -384,6 +387,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
...
</substate>
<origin>
Expand Down Expand Up @@ -623,6 +629,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
...
</substate>
<origin>
Expand Down Expand Up @@ -861,6 +870,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
...
</substate>
<origin>
Expand Down Expand Up @@ -1101,6 +1113,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
...
</substate>
<origin>
Expand Down Expand Up @@ -1341,6 +1356,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
...
</substate>
<origin>
Expand Down
69 changes: 69 additions & 0 deletions src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -227,6 +227,9 @@ Node 20:
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
...
</substate>
<origin>
Expand Down Expand Up @@ -475,6 +478,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
...
</substate>
<origin>
Expand Down Expand Up @@ -714,6 +720,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
...
</substate>
<origin>
Expand Down Expand Up @@ -952,6 +961,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
...
</substate>
<origin>
Expand Down Expand Up @@ -1192,6 +1204,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
...
</substate>
<origin>
Expand Down Expand Up @@ -1435,6 +1450,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
...
</substate>
<origin>
Expand Down Expand Up @@ -1682,6 +1700,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
...
</substate>
<origin>
Expand Down Expand Up @@ -1970,6 +1991,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
</substate> } ) )
</interimStates>
<touchedAccounts>
Expand Down Expand Up @@ -2024,6 +2048,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
</substate>
<origin>
ORIGIN_ID:Int
Expand Down Expand Up @@ -2309,6 +2336,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
</substate> } )
</interimStates>
<touchedAccounts>
Expand Down Expand Up @@ -2363,6 +2393,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
</substate>
<origin>
ORIGIN_ID:Int
Expand Down Expand Up @@ -2649,6 +2682,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
</substate> } )
</interimStates>
<touchedAccounts>
Expand Down Expand Up @@ -2703,6 +2739,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
</substate>
<origin>
ORIGIN_ID:Int
Expand Down Expand Up @@ -2992,6 +3031,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
</substate> } )
</interimStates>
<touchedAccounts>
Expand Down Expand Up @@ -3046,6 +3088,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
</substate>
<origin>
ORIGIN_ID:Int
Expand Down Expand Up @@ -3335,6 +3380,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
</substate> } )
</interimStates>
<touchedAccounts>
Expand Down Expand Up @@ -3389,6 +3437,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
</substate>
<origin>
ORIGIN_ID:Int
Expand Down Expand Up @@ -3681,6 +3732,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
</substate> } )
</interimStates>
<touchedAccounts>
Expand Down Expand Up @@ -3735,6 +3789,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
</substate>
<origin>
ORIGIN_ID:Int
Expand Down Expand Up @@ -4027,6 +4084,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
</substate> } ) => .List )
</interimStates>
<touchedAccounts>
Expand Down Expand Up @@ -4081,6 +4141,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
</substate>
<origin>
ORIGIN_ID:Int
Expand Down Expand Up @@ -4325,6 +4388,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
...
</substate>
<origin>
Expand Down Expand Up @@ -4570,6 +4636,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
<accessedStorage>
.Map
</accessedStorage>
<createdAccounts>
.Set
</createdAccounts>
...
</substate>
<origin>
Expand Down
Loading

0 comments on commit 1d8874a

Please sign in to comment.