test: add symbolic tests for IdRegistry and KeyRegistry invariants #275
Conversation
|
Thanks for all the setup here, @daejunpark! Halmos has come a long way and this is a very useful example. |
.github/workflows/ci.yml
Outdated
| @@ -41,6 +41,26 @@ jobs: | |||
| - name: Check forge snapshots | |||
| run: forge snapshot --check --match-contract Gas | |||
|
|
|||
| symtest: | |||
There was a problem hiding this comment.
self: move to run only when merged to main
test/IdRegistry/IdRegistry.st.sol
Outdated
|
|
||
| import {IdRegistryHarness} from "../Utils.sol"; | ||
|
|
||
| contract IdRegistrySymTest is SymTest, Test { |
There was a problem hiding this comment.
self: can we use TestSuiteSetup here?
test/IdRegistry/IdRegistry.st.sol
Outdated
| // Setup IdRegistry | ||
| idRegistry = new IdRegistryHarness(address(0)); | ||
|
|
||
| trustedCaller = address(0x1000); |
There was a problem hiding this comment.
self: use the owner pattern that we use elsewhere, should get this for free if we can use TestSuiteSetup above
test/IdRegistry/IdRegistry.st.sol
Outdated
| } | ||
| } | ||
|
|
||
| // Verify the IdRegistry invariants |
There was a problem hiding this comment.
self: clarify what invariants we are asserting here
test/IdRegistry/IdRegistry.st.sol
Outdated
| // Verify invariant properties | ||
|
|
||
| // Ensure that there is no recovery address associated with fid 0. | ||
| assert(idRegistry.getRecoveryOf(0) == address(0)); |
There was a problem hiding this comment.
self: do we actually care about this invariant? whats the worst that happens if this occurs?
test/IdRegistry/IdRegistry.st.sol
Outdated
| assert(oldPaused == false); | ||
| assert(newIdCounter - oldIdCounter == 1); | ||
| assert(newIdX == oldIdX || oldIdX == 0); | ||
| assert(newIdX == oldIdX || newIdY == oldIdY); |
There was a problem hiding this comment.
@daejunpark I found these last two lines hard to reason about, and rewrote them as follows. From the POV of symbolic verification, is there any difference between what we are asserting here?
if (newIdX != oldIdX) {
assert(oldIdX == 0 && newIdX == newIdCounter);
assert(oldIdY == newIdY);
} else if (newIdY != oldIdY) {
assert(oldIdY == 0 && newIdY == newIdCounter);
assert(oldIdX == newIdX);
} else {
assert(oldIdX == newIdX && oldIdY == newIdY);
}
There was a problem hiding this comment.
they are implications. since solidity doesn't offer a logical implication operator, we use not A or B to specify A implies B.
so they mean:
- if
newIdX != oldIdX, thenoldIdX == 0should hold. - if
newIdX != oldIdX, thennewIdY == oldIdYshould hold.
which can be also written as follows (with no difference from the logical reasoning perspective):
if (newIdX != oldIdX) {
assert(oldIdX == 0);
assert(newIdY == oldIdY);
}
your rewritten version should also works, but note that:
- the assertion in the last
elsebranch cannot be violated, because of theif-then-elsesemantics. - the second
ifbranch is logically dual with the firstifbranch, asxandyare symmetric.
There was a problem hiding this comment.
very helpful thanks.
- Agree that the last branch is unnecessary, and can be removed.
- What are the implications of logical duality here? Does it imply that this code is testing different things than the original logic you specified?
test/IdRegistry/IdRegistry.st.sol
Outdated
| return abi.encodePacked(selector, args); | ||
| } | ||
|
|
||
| function check_transfer(address caller, address to, address other) public { |
There was a problem hiding this comment.
@daejunpark we test transfer in two ways - via this specific test for transfer, and more generically in check_invariant, though we do not assert much there.
we test register only in one way - in the general check invariant, where we assert a lot of specific stuff.
is there a rationale for this design? or is this something that could be standardizes where we have a general invariant assertion test and specific ones for each function including register?
There was a problem hiding this comment.
initially, i had put everything in a single check_invariant test, but it seemed too complicated to read, so i split it into two tests for readability.
for readability reasons, yes, i usually separate invariant tests (where you call an arbitrary function), from tests for individual functions.
| y = svm.createAddress("y"); | ||
| } | ||
|
|
||
| function verifyInvariants(bytes4 selector, address caller) public { |
There was a problem hiding this comment.
note that the default prefix for halmos test functions is check_. if you want to use a different prefix, then you need to provide an additional option --function <prefix> to halmos, which is --function verify in this case. otherwise these functions will be omitted from testing, as you can see in the last ci run:
https://github.com/farcasterxyz/contracts/actions/runs/5671611054/job/15369109292
horsefacts
force-pushed
the
test/halmos
branch
2 times, most recently
from
4977686
to
ae04294
Compare
|
Thanks for all your help here and on tg, @daejunpark and @karmacoma-eth! I'm working on updating the tests here to account for some contract changes and have bumped into a counterexample that I don't understand. I've updated the tests to account for a few changes to the key registry:
Since I updated the invariants to account for these new functions. Since there are now multiple add/remove functions, there's now an extra check inside each post-state to detect which function was called and make any function-specific assertions. For example, before: if (newStateX == KeyRegistry.KeyState.REMOVED) {
// For a transition to REMOVED, ensure that:
// - The previous state must be ADD.
// - The transition can only be made by remove(), where:
// - It must be called by the owner of fid x.
assert(oldStateX == KeyRegistry.KeyState.ADDED);
assert(selector == keyRegistry.remove.selector);
assert(oldCallerId == x);
} And after: if (newStateX == KeyRegistry.KeyState.REMOVED) {
// For a transition to REMOVED, ensure that:
// - The previous state must be ADD.
assert(oldStateX == KeyRegistry.KeyState.ADDED);
// - The transition can only be made by remove() or removeFor()
if (selector == keyRegistry.remove.selector) {
// - remove() must be called by the owner of fid x.
assert(oldCallerId == x);
} else if (selector == keyRegistry.removeFor.selector) {
// No assertion here yet
} else {
assert(false);
}
}However, introducing the The function selector here is If I'm reading the failure right, it indicates that Am I interpreting the counterexample correctly? Anything else look suspicious here? You can see a few more counterexamples in the CI output here. |
|
ngl this is a chonky test, this is why we need a16z/halmos#130 |
|
thanks for updating the tests! let me take a look at the failure. |
Ha, yes, and I'm afraid I made it chonkier. Not sure either of these are relevant, but I noticed two other things here: |
daejunpark
force-pushed
the
test/halmos
branch
from
641846c
to
c2b143c
Compare
|
it turned out that a known halmos bug was triggered by this test. i've temporarily adjusted the test to avoid the bug and will fix it quickly. will get back to this soon. |
No, this test is one of the good uses of halmos. What is now missing from halmos is the debugging info, such as the trace info mentioned by Karma. We will add it soon. |
daejunpark
force-pushed
the
test/halmos
branch
from
f742034
to
768421f
Compare
i fixed the halmos issue, and reverted the temporary adjustment to the test. i also rebased the pr on the main branch, and updated the test for the new interface. it should work again now. please let me know if you have any further questions. |
|
the tests passed locally, but seems too heavy for the github ci. let me try optimizing them. |
This reverts commit c2b143c.
horsefacts
force-pushed
the
test/halmos
branch
from
15ea810
to
137e885
Compare
|
Coverage after merging test/halmos into main will be
Coverage Report
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Motivation
The purpose of this PR is to illustrate and discuss the use of symbolic tests for verifying contract invariants. Symbolic tests offer several advantages over random testing (such as foundry fuzzing and invariant testing), and can be highly effective when used properly. The tests provided in this (draft) PR is not exhaustive, but should serve as a pointer to provide the idea of symbolic tests and help further discussion.
Change Summary
Merge Checklist
Choose all relevant options below by adding an
xnow or at any time before submitting for reviewPR-Codex overview
Focus of this PR:
This PR focuses on adding symbolic tests for the
IdRegistryandKeyRegistrycontracts.Detailed summary:
IdRegistrycontract.KeyRegistrycontract.