KB: 8 articles on storage-slot access, harnessing, vacuity repair, and multi-call idioms#44
Open
shellygr wants to merge 6 commits into
Open
KB: 8 articles on storage-slot access, harnessing, vacuity repair, and multi-call idioms#44shellygr wants to merge 6 commits into
shellygr wants to merge 6 commits into
Conversation
… idioms Seed CVL_HELP_MESSAGES with decision-guidance articles covering: keccak-derived storage slot constants + slot hooks, Sload/Sstore hook grammar, harness getters/helper decomposition, the vacuous-method root-cause checklist and repair ladder, optimistic_fallback vs DISPATCHER vs mock for unresolved low-level calls, lastStorage/`at` multi-call templates, satisfy-witness rules, and relational abstraction of nonlinear math (CVLMath.spec). kb_populate.py needs Postgres at import time, so validate the seed data with an AST-based test (well-formed entries, unique titles). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…mistic default The pessimistic default fails loudly with an unwinding violation; only optimistic_loop silently assumes away paths beyond loop_iter. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
shellygr
commented
Jul 3, 2026
| "title": "No public getter for the state you need — write a harness", | ||
| "symptom": "The property needs a private/internal variable, an unstructured storage slot, or an intermediate step of a monolithic function, and the contract exposes no getter for it.", | ||
| "body": ( | ||
| "Missing getters are a *harness* problem, not a CVL-expressibility problem. Three " |
Contributor
Author
There was a problem hiding this comment.
here we need to mention that it is relevant if direct storage access is also not applicable, for whatever reason
Article 8 now points at the always-installed CVLMathAbstract.spec for the relational tier, names Math.spec as the exact *Summary tier, tells the agent to check the certora/specs/summaries/ listing before importing, and carries an inline mulDivDownAbstract fallback plus the require-based vacuity caveat for projects that predate the shipped assets. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…refs
- Article 4's symptom now quotes SANITY_FAILED / SANITY_FAILURE, the
rule_not_vacuous sanity sub-rule, and the <vacuity_alert> block —
the literal tokens an agent pastes from prover output — so embedding
retrieval matches the failure text.
- The two vacuity articles no longer compete on near-identical symptoms:
the older one is scoped to single-rule require-conflict vacuity, the
new one to method-level setup vacuity, and they link to each other.
- All informal cross-references ("the harness article", "the dedicated
article", "the optimistic_fallback article") now use the fixed phrase
'article titled "<exact title>"' so a following agent can KBGet by
exact key; article 2's hook-troubleshooting section shrinks to one-line
pointers at the three pre-existing hook/ghost articles instead of
restating them.
- New test asserts every such reference names an existing article.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Comment states which copy of duplicated guidance is authoritative: prompts own phase procedure and tool bindings, KB articles own symptom-indexed tool-agnostic concept knowledge, public docs derive from the concepts. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The drift-guard test recovered cross-referenced titles by splitting bodies on the citing phrase — string-ops the repo policy reserves for confirmed cases. The graph now lives as a KB_CROSS_REFERENCES literal next to the articles; the test checks declared facts only: every declared reference names an existing article and its exact citing phrase appears in the declaring body. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Contributor
Author
|
Delta since the previous version (post architecture review, 4 new commits):
🤖 Generated with Claude Code |
jtoman
requested changes
Jul 6, 2026
Comment on lines
+556
to
+585
| "body": ( | ||
| "**Pattern grammar by example:**\n" | ||
| "```cvl\n" | ||
| "hook Sload address o owner { ... } // read of a named variable\n" | ||
| "hook Sstore totalSupply uint256 ts (uint256 old_ts) { ... } // old value in parens\n" | ||
| "hook Sstore balances[KEY address user] uint256 v { ... } // mapping entry\n" | ||
| "hook Sstore entries[INDEX uint256 i] uint256 e { ... } // array element\n" | ||
| "hook Sstore owner.balance uint256 b { ... } // struct field\n" | ||
| "hook Sstore (slot 1).(offset 2) uint16 b { ... } // raw slot + offset\n" | ||
| "```\n" | ||
| "`KEY` binds the mapping key, `INDEX` the array index; paths compose " | ||
| "(`m[KEY address a].field[INDEX uint256 i]`).\n\n" | ||
| "**Ghost mirroring** — the standard way to make hooked state visible to rules and " | ||
| "invariants:\n" | ||
| "```cvl\n" | ||
| "ghost mapping(address => uint256) balanceMirror {\n" | ||
| " init_state axiom forall address a. balanceMirror[a] == 0;\n" | ||
| "}\n" | ||
| "hook Sstore balances[KEY address user] uint256 v {\n" | ||
| " balanceMirror[user] = v;\n" | ||
| "}\n" | ||
| "```\n\n" | ||
| "**If the hook never fires, or the mirror value is unexpectedly wiped**, the usual " | ||
| "causes have dedicated articles:\n" | ||
| "- hooks fire only on *contract* code — see the article titled " | ||
| "\"Hook is not triggered by CVL code\";\n" | ||
| "- stores inside a hook body do not re-trigger hooks — see the article titled " | ||
| "\"Hook is not triggered recursively\";\n" | ||
| "- non-persistent ghost mirrors are havoced together with storage — see the article " | ||
| "titled \"Ghost variable has unexpected value after an external call\"." |
Contributor
There was a problem hiding this comment.
this almost directly contradicts advice elsewhere saying to use direct storage access where possible (ghosts/hooks which purely mirror storage state is cruft that serves no purpose over just doing direct storage access)
Contributor
Author
There was a problem hiding this comment.
We have exemplars on solc0.4. Good luck to the agent then. Agree the solution is not in kb articles
Contributor
There was a problem hiding this comment.
I guess my claim is that if direct storage access doesn't work, hooks won't work either, unless they get lucky and all the state they need is in constant slots.
| }, | ||
| { | ||
| "title": "No public getter for the state you need — write a harness", | ||
| "symptom": "The property needs a private/internal variable, an unstructured storage slot, or an intermediate step of a monolithic function, and the contract exposes no getter for it.", |
Contributor
There was a problem hiding this comment.
again, direct storage access should be fine for private or internal variables!
Comment on lines
+622
to
+626
| "1. **`NONDET` summary on a payable or side-effecting callee.** Canonical case: the " | ||
| "contract forwards ETH to a summarized `deposit()` (e.g. the beacon-chain deposit " | ||
| "contract). The `NONDET` summary erases the callee's state effects, so checks downstream " | ||
| "of the call fail on every path and the caller always reverts in the model — every rule " | ||
| "touching that path becomes vacuous. Inspect the auto-generated summaries first.\n" |
Contributor
There was a problem hiding this comment.
this is such a special case from your recent experience, calling it a "canonical" example is a huge stretch.
A better phrasing is to say the following:
A summary does not capture a side effect a later computation relies on. For example, whitelistUser(address) is summarized as NONDET, but the contract code contains:
whilelistUser(someUser);
performTrade(someUser); // <- always reverts, whitelists not updated
Comment on lines
+655
to
+658
| "- **`\"optimistic_fallback\": true`** (conf flag): unresolved empty-calldata calls no " | ||
| "longer havoc the caller's storage. The right fix when the call is a *pure ETH transfer* " | ||
| "to an arbitrary address. Unsound exactly when the receiver could reenter the protocol — " | ||
| "reentrancy is what the flag assumes away, so don't use it for reentrancy properties.\n" |
Contributor
There was a problem hiding this comment.
no agent can currently act on this; if we put this we will have agents spin out trying to figure out how to add this flag. Don't mention a remediation that the agent can't use imo
Comment on lines
+639
to
+641
| "3. `\"optimistic_fallback\": true` if the offender is an unresolved raw ETH transfer — " | ||
| "see the article titled \"Unresolved low-level call{value} havocs storage — " | ||
| "optimistic_fallback vs DISPATCHER vs mock\".\n" |
Contributor
There was a problem hiding this comment.
so objection below about unusable mitigations
Contributor
Author
There was a problem hiding this comment.
I tend to disagree here that it cannot act upon it if receiving this from the cex analyzer?
Contributor
There was a problem hiding this comment.
the agent has no way to change the prover config to add "optimistic_fallback" I mean. dispatcher vs mock, sure!
Comment on lines
+630
to
+632
| "3. **`optimistic_loop: true` with `loop_iter` too small:** paths needing more " | ||
| "iterations than `loop_iter` are silently assumed away — possibly all of them. (The " | ||
| "pessimistic default instead fails loudly with a loop-unwinding violation.)\n" |
Comment on lines
+670
to
+703
| "title": "Verifying properties across a sequence of calls — `lastStorage` and `at`", | ||
| "symptom": "The property compares outcomes of different call sequences from the same starting state (additivity, round-trip/inverse, split-vs-whole operations), and single-call rules can't express it.", | ||
| "body": ( | ||
| "**Idiom:** snapshot the state with `storage s = lastStorage;` and replay an alternative " | ||
| "sequence from the snapshot with `f(e, args) at s;`.\n\n" | ||
| "**Additivity template** (split vs. whole):\n" | ||
| "```cvl\n" | ||
| "rule depositAdditive(env e, uint256 x, uint256 y) {\n" | ||
| " storage init = lastStorage;\n" | ||
| " deposit(e, x);\n" | ||
| " deposit(e, y);\n" | ||
| " uint256 split = balanceOf(e.msg.sender);\n" | ||
| "\n" | ||
| " deposit(e, require_uint256(x + y)) at init; // replay from the snapshot\n" | ||
| " uint256 whole = balanceOf(e.msg.sender);\n" | ||
| "\n" | ||
| " assert split == whole; // rounding may require: split <= whole (or a ±1 bound)\n" | ||
| "}\n" | ||
| "```\n\n" | ||
| "**Round-trip template** (inverse operations restore state):\n" | ||
| "```cvl\n" | ||
| "rule depositWithdrawRoundTrip(env e, uint256 amount) {\n" | ||
| " storage init = lastStorage;\n" | ||
| " uint256 shares = deposit(e, amount);\n" | ||
| " withdraw(e, shares);\n" | ||
| " assert lastStorage[currentContract] == init[currentContract];\n" | ||
| "}\n" | ||
| "```\n" | ||
| "Whole-storage comparison (`==` on `storage` variables, optionally restricted per contract " | ||
| "with `s[c]`) is supported.\n\n" | ||
| "**Caveat:** rounding usually breaks exact equalities — prefer inequalities in the " | ||
| "direction that protects the protocol (\"the user never gains from split/round-trip\")." | ||
| ), | ||
| }, |
Contributor
There was a problem hiding this comment.
I don't think this should be in the KB, not as the prompting around it is. Searching on a "symptom" of "how do I ... ?" just doesn't make sense. We should either add a sister tool for this kind of "how to do X" for various, common X patterns with richer search (FTS, full vector search) instead of trying to rephrase everything the agent needs to know as a "symptom".
Put another way, trying to express "here's how to do X" as an symptom: "I don't know how to do X" is not a natural way to find knowledge.
Comment on lines
+760
to
+761
| "because AutoSetup's curated summaries shipped it or because the pipeline installed the " | ||
| "same canonical file). Check the `certora/specs/summaries/` directory listing (or the " |
Contributor
There was a problem hiding this comment.
agent has no idea what autosetup is
Comment on lines
+530
to
+550
| "- EIP-1967: `bytes32(uint256(keccak256(\"eip1967.proxy.implementation\")) - 1)`\n" | ||
| "- ERC-7201: `keccak256(abi.encode(uint256(keccak256(id)) - 1)) & ~bytes32(uint256(0xff))`\n\n" | ||
| "Compute the constant once (from the contract source, or with `cast keccak`/`chisel`) and " | ||
| "embed it as a `definition`:\n" | ||
| "```cvl\n" | ||
| "// bytes32(uint256(keccak256(\"eip1967.proxy.implementation\")) - 1)\n" | ||
| "definition IMPL_SLOT() returns uint256 =\n" | ||
| " 0x360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc;\n" | ||
| "\n" | ||
| "ghost address implMirror;\n" | ||
| "\n" | ||
| "// the (slot ...) hook pattern takes a numeric literal; keep the derivation as a comment\n" | ||
| "hook Sstore (slot 0x360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc)\n" | ||
| " address newImpl {\n" | ||
| " implMirror = newImpl;\n" | ||
| "}\n" | ||
| "```\n\n" | ||
| "**Alternative — harness getter:** add `contract XHarness is X` with an `external view` " | ||
| "getter that `sload`s the slot constant — see the article titled " | ||
| "\"No public getter for the state you need — write a harness\". Prefer hooks for " | ||
| "tracking *writes*, getters for reading current values inside assertions." |
Contributor
There was a problem hiding this comment.
except this doesn't help if this is used for anything but a single slot. We really don't want the agent trying to reason about these raw storage slots. Honest solution is to add the magic eip-7201 annotations and/or use the editor to make the computed storage slot eip-7201 compliant.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Part 6 of 6 (spec-quality series). The knowledge base had no coverage of the CVL capabilities the generated specs wrongly deemed impossible; these symptom-indexed articles make retrieval surface them at decision time.
What
Eight additive entries to
CVL_HELP_MESSAGES({title, symptom, body}format, matching existing style), plus a declared cross-reference graph (KB_CROSS_REFERENCES) and a tier-ownership policy comment atop the article list:optimistic_loop); symptom quotes the literal prover failure tokens (SANITY_FAILED/SANITY_FAILURE,rule_not_vacuous,<vacuity_alert>) so embedding retrieval matches pasted output; scoped to method-level setup vacuity, with the pre-existing require-conflict vacuity article cross-linked rather than competed with.call{value}HAVOC (optimistic_fallbackvs DISPATCHER vs mock trade-offs)lastStorage/atidioms)CVLMathAbstract.specfor the relational tier,Math.specfor the exact*Summarytier, checkcertora/specs/summaries/before importing, inlinemulDivDownAbstractfallback for projects predating the shipped assetsDesign revisions after architecture review
Math.spec/CVLMathAbstract.spec, noCVLMath.speccopy) — merge Ship CVLMath relational math library; prefer relational properties over formula mirroring #42 before this PR.article titled "<exact title>"so a following agent can KBGet by exact key.KB_CROSS_REFERENCESdata literal; the drift-guard test checks declared facts instead of parsing prose (repo no-string-ops policy).CVL_HELP_MESSAGES: prompts own phase procedure, KB owns symptom-indexed concept knowledge, public docs derive from the concepts.Notes for review
python -m composer.scripts.kb_populateneeds local Postgres and was not run here; the AST-based test validates shape/uniqueness. Please reseed once after merge.Tests
tests/test_kb_populate.py: 3 passed (shape/uniqueness, plus cross-reference integrity: every declared reference names an existing article and its citing phrase appears in the declaring body). Diff is essentially additive (+407 / −2).🤖 Generated with Claude Code