From 722d82588487b5e91299a21599b6eddd0da5e556 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 3 Jul 2026 20:24:43 +0300 Subject: [PATCH 1/6] Add 8 CVL KB articles: storage-slot, harness, vacuity, and multi-call 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 --- composer/scripts/kb_populate.py | 238 ++++++++++++++++++++++++++++++++ tests/test_kb_populate.py | 53 +++++++ 2 files changed, 291 insertions(+) create mode 100644 tests/test_kb_populate.py diff --git a/composer/scripts/kb_populate.py b/composer/scripts/kb_populate.py index 01899c0..c6ddfdc 100644 --- a/composer/scripts/kb_populate.py +++ b/composer/scripts/kb_populate.py @@ -498,6 +498,244 @@ class KBMessage(TypedDict): "to the property being checked." ), }, + { + "title": "Keccak-derived / unstructured storage slots are verifiable — don't skip", + "symptom": "You are about to skip a property because the contract keeps state in keccak-derived storage slots (ERC-7201 namespaced storage, EIP-1967 proxy slots, assembly/`StorageSlot` access) and \"CVL cannot reason about hash functions\".", + "body": ( + "**Misconception:** The \"no reasoning about hashes\" limitation is about *collisions and " + "inversion* of hashes of unknown data. A keccak-derived storage *slot* is the hash of a " + "fixed string literal — a compile-time constant — and `keccak256` is a built-in CVL " + "function. Such state is fully in reach.\n\n" + "**Slot formulas:**\n" + "- 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 harness article). Prefer hooks for " + "tracking *writes*, getters for reading current values inside assertions." + ), + }, + { + "title": "Sload/Sstore hook grammar — paths, KEY/INDEX, ghost mirroring", + "symptom": "You need to observe storage reads/writes (a mapping entry, array element, struct field, or raw slot) to state a property, but are unsure of the hook pattern syntax or why your hook never fires.", + "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" + "**Why a hook may never fire:**\n" + "- Hooks are only triggered by *contract* code. Direct storage access from CVL does not " + "fire them (calling a Solidity function from CVL does — the store happens in contract " + "code).\n" + "- Hooks are not applied recursively: stores performed inside a hook body do not trigger " + "further hooks.\n" + "- Non-persistent ghosts are havoced together with storage on unresolved calls — mirror " + "values can be wiped even though the hook fired." + ), + }, + { + "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 " + "patterns, all in a `contract XHarness is X` under `certora/harnesses/` (verify the " + "harness instead of the base contract — inherited behavior is unchanged):\n\n" + "**1. Getter harness** for private/internal state:\n" + "```solidity\n" + "contract VaultHarness is Vault {\n" + " function getPendingFees() external view returns (uint256) {\n" + " return _pendingFees; // internal state, no public getter upstream\n" + " }\n" + "}\n" + "```\n\n" + "**2. Raw-slot getter** for unstructured/keccak-derived storage:\n" + "```solidity\n" + "function slotValue(bytes32 slot) external view returns (uint256 v) {\n" + " assembly { v := sload(slot) }\n" + "}\n" + "```\n\n" + "**3. Helper decomposition** of a monolithic external function: expose each internal step " + "as a thin wrapper (`helper1()`, `helper2()`, ...) so steps can be verified separately. " + "Wrappers must contain *no logic of their own* — each one only calls an existing internal " + "function; otherwise you verify the harness, not the protocol.\n\n" + "A harness is verification infrastructure, not a protocol change — needing one is not a " + "reason to skip a property." + ), + }, + { + "title": "Rule passes vacuously — a method always reverts under the model", + "symptom": "rule_sanity reports a rule vacuous (or `assert false` passes), or a parametric rule's instantiation for one method always reverts even though the method works on-chain.", + "body": ( + "**Root-cause checklist, in order of likelihood:**\n" + "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" + "2. **Conflicting `require`s** (including silent `require_*` casts) in the rule or a " + "preserved block.\n" + "3. **`loop_iter` too small:** with default (pessimistic) loop handling, executions " + "needing more iterations than `loop_iter` are cut off — possibly all of them.\n" + "4. **`lastReverted` overwritten** by a later call (see the dedicated article).\n\n" + "**Repair order — fix the root cause before filtering:**\n" + "1. Replace the bad summary with a sound one (expression summary / ghost model of the " + "callee).\n" + "2. Write a small mock contract and link it into the scene.\n" + "3. `\"optimistic_fallback\": true` if the offender is an unresolved raw ETH transfer " + "(see the optimistic_fallback article).\n" + "4. Only if 1–3 are impossible: a `filtered` block, with a comment documenting which " + "repairs were attempted and why they failed.\n\n" + "Filtering first hides the setup bug and silently unverifies *every* property on that " + "method." + ), + }, + { + "title": "Unresolved low-level call{value} havocs storage — optimistic_fallback vs DISPATCHER vs mock", + "symptom": "Call resolution shows an unresolved low-level `.call{value: ...}(\"\")` (or `send`/`transfer`) resolved as HAVOC; rules fail with arbitrary storage changes or become vacuous.", + "body": ( + "**Default behavior:** an unresolved external call with an empty input buffer havocs " + "storage — the Prover assumes the unknown receiver may call back and change anything.\n\n" + "**Options, weakest-assumption first:**\n" + "- **`\"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" + "- **`DISPATCHER(true)`**: when the call goes through a known interface and an " + "implementation exists in the scene; the Prover case-splits over scene implementations. " + "Sound relative to the scene, but fails at type-checking (CLI ≥7.7.0) if no " + "implementation is present, and doesn't apply to raw empty-calldata transfers.\n" + "- **Mock contract** linked into the scene: full control over counterparty behavior; " + "costs authoring effort and risks over-constraining (a too-friendly mock hides bugs).\n\n" + "Pick the weakest assumption that unblocks the rule and record the soundness trade-off in " + "a comment next to the flag or summary." + ), + }, + { + "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\")." + ), + }, + { + "title": "Implication rules can pass vacuously — add `satisfy` witness rules", + "symptom": "A rule whose assertion is an implication (`antecedent => consequent`) passes, and you suspect it only passes because the antecedent is never true on any reachable path.", + "body": ( + "**Semantics:** `assert p;` must hold on *all* reachable paths; `satisfy p;` checks that " + "*there exists* a reachable path where `p` holds, and fails if none does. A rule body " + "ends with either `assert` or `satisfy`.\n\n" + "`rule_sanity: basic` catches a fully unreachable assert, but NOT an implication whose " + "antecedent is never true — the assert is still reached and trivially passes. The fix is " + "a witness companion rule:\n" + "```cvl\n" + "rule pausedBlocksWithdraw(env e) {\n" + " bool paused = paused();\n" + " withdraw@withrevert(e);\n" + " assert paused => lastReverted;\n" + "}\n" + "\n" + "// companion witness: the interesting antecedent is actually reachable\n" + "rule pausedBlocksWithdraw_witness(env e) {\n" + " bool paused = paused();\n" + " withdraw@withrevert(e);\n" + " satisfy paused;\n" + "}\n" + "```\n\n" + "**Difference from `assert`:** a passing `satisfy` produces a concrete witness execution " + "in the report — it is a coverage/sanity check that the rule exercises the case you care " + "about, not a safety proof. Add witnesses for every implication-shaped or " + "heavily-`require`d rule." + ), + }, + { + "title": "Nonlinear arithmetic (mulDiv) times out — verify relational properties, summarize with abstractions", + "symptom": "Rules over share/asset conversions or ratio math (`x * y / z`, mulDiv, WAD/RAY operations) time out or exhaust the SMT solver.", + "body": ( + "**Principle — relational over exact:** do not restate the exact nonlinear formula in the " + "spec (that doubles the nonlinear reasoning burden). State the properties that actually " + "matter and are solver-friendly:\n" + "- monotonicity in each argument,\n" + "- bounds and rounding direction (`down <= up <= down + 1`),\n" + "- round-trip inequalities (converting and back never favors the user),\n" + "- zero/identity cases.\n\n" + "**Summarize the hotspot:** replace the exact `mulDiv` implementation with a relational " + "abstraction that keeps only such axioms. The `CVLMath.spec` summaries resource (under " + "`certora/specs/summaries/`, when present in the project) provides `mulDivDownAbstract`, " + "`mulDivUpAbstract`, and friends with monotonicity/zero/exactness axioms — import it and " + "route the implementation through it:\n" + "```cvl\n" + "import \"summaries/CVLMath.spec\";\n" + "\n" + "methods {\n" + " function MathLib.mulDiv(uint256 x, uint256 y, uint256 d) internal returns (uint256)\n" + " => mulDivDownAbstract(x, y, d);\n" + "}\n" + "```\n\n" + "**Trade-off:** the abstraction over-approximates the real function, so properties that " + "depend on exact values may get spurious counterexamples — keep exact summaries for " + "those rules only. Abstractions with axioms can also introduce vacuity if the axioms " + "conflict; keep `rule_sanity: basic` on to catch it." + ), + }, ] to_store : list[KnowledgeBaseArticle] = [ diff --git a/tests/test_kb_populate.py b/tests/test_kb_populate.py new file mode 100644 index 0000000..86f0f69 --- /dev/null +++ b/tests/test_kb_populate.py @@ -0,0 +1,53 @@ +""" +Static validation of the KB seed data in composer/scripts/kb_populate.py. + +The module initializes the indexed store at import time (requires Postgres), +so instead of importing it we extract the CVL_HELP_MESSAGES literal via AST +parsing and validate its shape: every entry has non-empty title/symptom/body +strings, and titles are unique (they are the store keys). +""" +import ast +from pathlib import Path + +KB_POPULATE_PATH = ( + Path(__file__).parent.parent / "composer" / "scripts" / "kb_populate.py" +) + +REQUIRED_KEYS = {"title", "symptom", "body"} + + +def _load_messages() -> list[dict[str, str]]: + tree = ast.parse(KB_POPULATE_PATH.read_text()) + for node in tree.body: + if ( + isinstance(node, ast.AnnAssign) + and isinstance(node.target, ast.Name) + and node.target.id == "CVL_HELP_MESSAGES" + ): + assert node.value is not None, "CVL_HELP_MESSAGES has no value" + # entries are pure literals (dicts of implicitly-concatenated + # string constants), so literal_eval reconstructs them exactly + return ast.literal_eval(node.value) + raise AssertionError("CVL_HELP_MESSAGES assignment not found in kb_populate.py") + + +def test_entries_are_well_formed(): + messages = _load_messages() + assert len(messages) > 0 + for entry in messages: + assert set(entry.keys()) == REQUIRED_KEYS, ( + f"entry {entry.get('title', '')!r} has keys {set(entry.keys())}" + ) + for key in REQUIRED_KEYS: + value = entry[key] + assert isinstance(value, str) and value.strip(), ( + f"entry {entry.get('title', '')!r} has empty {key!r}" + ) + + +def test_titles_are_unique(): + # titles are the store keys — a duplicate would silently shadow an article + titles = [entry["title"] for entry in _load_messages()] + assert len(titles) == len(set(titles)), ( + f"duplicate titles: {sorted(t for t in titles if titles.count(t) > 1)}" + ) From 4a09c8ecdce732d67e012f2210d1df13afaaff09 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 3 Jul 2026 20:36:28 +0300 Subject: [PATCH 2/6] Attribute vacuity from loop cut-off to optimistic_loop, not the pessimistic 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 --- composer/scripts/kb_populate.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/composer/scripts/kb_populate.py b/composer/scripts/kb_populate.py index c6ddfdc..743ca8d 100644 --- a/composer/scripts/kb_populate.py +++ b/composer/scripts/kb_populate.py @@ -605,8 +605,9 @@ class KBMessage(TypedDict): "touching that path becomes vacuous. Inspect the auto-generated summaries first.\n" "2. **Conflicting `require`s** (including silent `require_*` casts) in the rule or a " "preserved block.\n" - "3. **`loop_iter` too small:** with default (pessimistic) loop handling, executions " - "needing more iterations than `loop_iter` are cut off — possibly all of them.\n" + "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" "4. **`lastReverted` overwritten** by a later call (see the dedicated article).\n\n" "**Repair order — fix the root cause before filtering:**\n" "1. Replace the bad summary with a sound one (expression summary / ghost model of the " From 5512e905de57f81561d65eeac8954ca109981ff1 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sat, 4 Jul 2026 03:26:45 +0300 Subject: [PATCH 3/6] Rewrite mulDiv KB article against the single-source math tiers 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 --- composer/scripts/kb_populate.py | 39 +++++++++++++++++++++++++++------ 1 file changed, 32 insertions(+), 7 deletions(-) diff --git a/composer/scripts/kb_populate.py b/composer/scripts/kb_populate.py index 743ca8d..de3900e 100644 --- a/composer/scripts/kb_populate.py +++ b/composer/scripts/kb_populate.py @@ -719,22 +719,47 @@ class KBMessage(TypedDict): "- round-trip inequalities (converting and back never favors the user),\n" "- zero/identity cases.\n\n" "**Summarize the hotspot:** replace the exact `mulDiv` implementation with a relational " - "abstraction that keeps only such axioms. The `CVLMath.spec` summaries resource (under " - "`certora/specs/summaries/`, when present in the project) provides `mulDivDownAbstract`, " - "`mulDivUpAbstract`, and friends with monotonicity/zero/exactness axioms — import it and " - "route the implementation through it:\n" + "abstraction that keeps only such axioms. Generated projects always ship " + "`certora/specs/summaries/CVLMathAbstract.spec`, which provides `mulDivDownAbstract`, " + "`mulDivUpAbstract`, and friends (plus WAD/RAY definitions) with " + "zero/exactness/monotonicity axioms — import it and route the implementation through it:\n" "```cvl\n" - "import \"summaries/CVLMath.spec\";\n" + "import \"summaries/CVLMathAbstract.spec\";\n" "\n" "methods {\n" " function MathLib.mulDiv(uint256 x, uint256 y, uint256 d) internal returns (uint256)\n" " => mulDivDownAbstract(x, y, d);\n" "}\n" "```\n\n" + "**Exact tier:** rules that depend on exact values or the overflow revert should instead " + "use the `*Summary` functions from `certora/specs/summaries/Math.spec` (present either " + "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 " + "advertised resources) for which files the project actually has before importing.\n\n" + "**Fallback — neither file exists:** write the relational abstraction inline. A minimal " + "floor(x * y / d) model:\n" + "```cvl\n" + "ghost mapping(uint256 => mapping(uint256 => mapping(uint256 => uint256))) mulDivDownGhost;\n" + "\n" + "function mulDivDownAbstract(uint256 x, uint256 y, uint256 d) returns uint256 {\n" + " if (d == 0) revert();\n" + " uint256 result = mulDivDownGhost[x][y][d];\n" + " require (x == 0 || y == 0) => result == 0; // zero-preservation\n" + " require y == d => result == x; // exact when a factor equals the denominator\n" + " require x == d => result == y;\n" + " require y <= d => result <= x; // linear relaxation of result*d <= x*y\n" + " require y >= d => result >= x;\n" + " require x <= d => result <= y;\n" + " require x >= d => result >= y;\n" + " return result;\n" + "}\n" + "```\n\n" "**Trade-off:** the abstraction over-approximates the real function, so properties that " "depend on exact values may get spurious counterexamples — keep exact summaries for " - "those rules only. Abstractions with axioms can also introduce vacuity if the axioms " - "conflict; keep `rule_sanity: basic` on to catch it." + "those rules only. The abstract tier's constraints are `require`-based axioms and the " + "overflow revert is not modeled, so contradicting assumptions prune paths silently " + "(potential vacuity): keep `rule_sanity: basic` on and avoid these abstractions in " + "`satisfy` rules." ), }, ] From 2278ed7021662f41367108e3bc7575a6868e1811 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sat, 4 Jul 2026 03:30:22 +0300 Subject: [PATCH 4/6] Put literal failure tokens in the vacuity symptom; exact-title cross-refs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Article 4's symptom now quotes SANITY_FAILED / SANITY_FAILURE, the rule_not_vacuous sanity sub-rule, and the 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 ""' 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 --- composer/scripts/kb_populate.py | 40 ++++++++++++++++++++------------- tests/test_kb_populate.py | 24 ++++++++++++++++++++ 2 files changed, 48 insertions(+), 16 deletions(-) diff --git a/composer/scripts/kb_populate.py b/composer/scripts/kb_populate.py index de3900e..d05f008 100644 --- a/composer/scripts/kb_populate.py +++ b/composer/scripts/kb_populate.py @@ -396,7 +396,7 @@ class KBMessage(TypedDict): }, { "title": "Vacuity — rule passes but `assert false` also passes", - "symptom": "A rule verifies successfully, but something feels wrong. You add `assert false;` and it also verifies.", + "symptom": "A single rule verifies successfully, but something feels wrong. You add `assert false;` to that rule and it also verifies — the rule's own requires or calls make its assertions unreachable.", "body": ( "**Cause:** The rule is **vacuous** — the combination of `require` statements and/or implicit " "reverts makes it impossible for execution to reach the assertions. Common causes:\n" @@ -405,7 +405,11 @@ class KBMessage(TypedDict): "3. Overflow/underflow causing implicit reverts in Solidity ≥0.8.\n\n" "**Fix:** Always run with `\"rule_sanity\": \"basic\"` (this is now the default in recent " "versions). This checks whether each rule and assert is reachable. If the sanity check fails, " - "revisit your `require` statements." + "revisit your `require` statements.\n\n" + "**Scope:** this article covers vacuity local to one rule. If the report flags a *method* " + "as vacuous across many rules (SANITY_FAILED with a `` block), the " + "verification setup — not the rule — is the problem; see the article titled " + "\"Rule passes vacuously — a method always reverts under the model\"." ), }, { @@ -525,7 +529,8 @@ class KBMessage(TypedDict): "}\n" "```\n\n" "**Alternative — harness getter:** add `contract XHarness is X` with an `external view` " - "getter that `sload`s the slot constant (see the harness article). Prefer hooks for " + "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." ), }, @@ -554,14 +559,14 @@ class KBMessage(TypedDict): " balanceMirror[user] = v;\n" "}\n" "```\n\n" - "**Why a hook may never fire:**\n" - "- Hooks are only triggered by *contract* code. Direct storage access from CVL does not " - "fire them (calling a Solidity function from CVL does — the store happens in contract " - "code).\n" - "- Hooks are not applied recursively: stores performed inside a hook body do not trigger " - "further hooks.\n" - "- Non-persistent ghosts are havoced together with storage on unresolved calls — mirror " - "values can be wiped even though the hook fired." + "**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\"." ), }, { @@ -595,7 +600,7 @@ class KBMessage(TypedDict): }, { "title": "Rule passes vacuously — a method always reverts under the model", - "symptom": "rule_sanity reports a rule vacuous (or `assert false` passes), or a parametric rule's instantiation for one method always reverts even though the method works on-chain.", + "symptom": "The prover reports SANITY_FAILED / SANITY_FAILURE (the rule_not_vacuous sanity sub-rule fails), or the report contains a block flagging a method as vacuous across rules, or a parametric rule's instantiation for one method always reverts even though the method works on-chain.", "body": ( "**Root-cause checklist, in order of likelihood:**\n" "1. **`NONDET` summary on a payable or side-effecting callee.** Canonical case: the " @@ -604,17 +609,20 @@ class KBMessage(TypedDict): "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" "2. **Conflicting `require`s** (including silent `require_*` casts) in the rule or a " - "preserved block.\n" + "preserved block — when only one rule is vacuous, see the article titled " + "\"Vacuity — rule passes but `assert false` also passes\".\n" "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" - "4. **`lastReverted` overwritten** by a later call (see the dedicated article).\n\n" + "4. **`lastReverted` overwritten** by a later call — see the article titled " + "\"`lastReverted` is overwritten by subsequent calls\".\n\n" "**Repair order — fix the root cause before filtering:**\n" "1. Replace the bad summary with a sound one (expression summary / ghost model of the " "callee).\n" "2. Write a small mock contract and link it into the scene.\n" - "3. `\"optimistic_fallback\": true` if the offender is an unresolved raw ETH transfer " - "(see the optimistic_fallback article).\n" + "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" "4. Only if 1–3 are impossible: a `filtered` block, with a comment documenting which " "repairs were attempted and why they failed.\n\n" "Filtering first hides the setup bug and silently unverifies *every* property on that " diff --git a/tests/test_kb_populate.py b/tests/test_kb_populate.py index 86f0f69..34a2b1a 100644 --- a/tests/test_kb_populate.py +++ b/tests/test_kb_populate.py @@ -51,3 +51,27 @@ def test_titles_are_unique(): assert len(titles) == len(set(titles)), ( f"duplicate titles: {sorted(t for t in titles if titles.count(t) > 1)}" ) + + +# Bodies cross-reference other articles with the fixed phrase +# `article titled ""` so a following agent can KBGet by exact +# key. The marker + closing quote delimit the title verbatim (titles contain +# no double quotes, enforced below), so plain splitting recovers it exactly. +CROSS_REF_MARKER = 'article titled "' + + +def test_cross_references_resolve(): + messages = _load_messages() + titles = {entry["title"] for entry in messages} + for title in titles: + assert '"' not in title, ( + f"title {title!r} contains a double quote, breaking the " + f"cross-reference convention" + ) + for entry in messages: + for chunk in entry["body"].split(CROSS_REF_MARKER)[1:]: + referenced = chunk.split('"', 1)[0] + assert referenced in titles, ( + f"article {entry['title']!r} references unknown article " + f"{referenced!r}" + ) From 11a4b4356d921527f2f95f8b05a591ec9baeff36 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sat, 4 Jul 2026 03:30:56 +0300 Subject: [PATCH 5/6] Declare tier ownership atop the seeded KB articles 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 --- composer/scripts/kb_populate.py | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/composer/scripts/kb_populate.py b/composer/scripts/kb_populate.py index d05f008..0705a5e 100644 --- a/composer/scripts/kb_populate.py +++ b/composer/scripts/kb_populate.py @@ -10,6 +10,22 @@ class KBMessage(TypedDict): body: str symptom: str +# Canonical-source policy for guidance that also exists elsewhere: +# - Prompt templates (composer/templates/*.j2) own PHASE PROCEDURE and tool +# bindings — repair ladders, decision gates, references to concrete tools +# like write_mock/edit_config. They are always-on for the one phase that +# must act unprompted; do not shrink them to KB pointers. +# - These KB articles own SYMPTOM-INDEXED CONCEPT KNOWLEDGE: tool-agnostic, +# retrieved on demand by any agent (cex remediation, cvl_research, natspec). +# Only the symptom field is embedded for retrieval, so symptoms should quote +# the literal tokens agents see in prover output; bodies stay +# decision-centric (what to do and why, not phase mechanics). Articles +# reference each other with the phrase `article titled ""` +# (KBGet retrieves by exact title; tests/test_kb_populate.py checks the +# references resolve). +# - Public docs derive from these concepts and are reference material. +# When the same fact appears in more than one tier, edit the owning tier +# first and bring the other copies along. CVL_HELP_MESSAGES : list[KBMessage] = [ { "title": "Summary not being applied", From 99201e094db2670977d70d24ef68ff51669ee343 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sat, 4 Jul 2026 03:38:33 +0300 Subject: [PATCH 6/6] Declare the cross-reference graph as data instead of parsing prose MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- composer/scripts/kb_populate.py | 25 ++++++++++++++++++ tests/test_kb_populate.py | 47 ++++++++++++++++++++++----------- 2 files changed, 56 insertions(+), 16 deletions(-) diff --git a/composer/scripts/kb_populate.py b/composer/scripts/kb_populate.py index 0705a5e..0ab4b8b 100644 --- a/composer/scripts/kb_populate.py +++ b/composer/scripts/kb_populate.py @@ -788,6 +788,31 @@ class KBMessage(TypedDict): }, ] +# Cross-reference graph of the articles above, declared as data so the test +# suite (tests/test_kb_populate.py) can check that references resolve without +# parsing prose: each key is an article title, each value the exact titles its +# body cites with the `article titled ""` phrase. Keep this map in sync +# when editing a body's cross-references. +KB_CROSS_REFERENCES: dict[str, list[str]] = { + "Vacuity — rule passes but `assert false` also passes": [ + "Rule passes vacuously — a method always reverts under the model", + ], + "Keccak-derived / unstructured storage slots are verifiable — don't skip": [ + "No public getter for the state you need — write a harness", + ], + "Sload/Sstore hook grammar — paths, KEY/INDEX, ghost mirroring": [ + "Hook is not triggered by CVL code", + "Hook is not triggered recursively", + "Ghost variable has unexpected value after an external call", + ], + "Rule passes vacuously — a method always reverts under the model": [ + "Vacuity — rule passes but `assert false` also passes", + "`lastReverted` is overwritten by subsequent calls", + "Unresolved low-level call{value} havocs storage — " + "optimistic_fallback vs DISPATCHER vs mock", + ], +} + to_store : list[KnowledgeBaseArticle] = [ { "title": d["title"], diff --git a/tests/test_kb_populate.py b/tests/test_kb_populate.py index 34a2b1a..e3df0c1 100644 --- a/tests/test_kb_populate.py +++ b/tests/test_kb_populate.py @@ -16,19 +16,23 @@ REQUIRED_KEYS = {"title", "symptom", "body"} -def _load_messages() -> list[dict[str, str]]: +def _load_literal(name: str): tree = ast.parse(KB_POPULATE_PATH.read_text()) for node in tree.body: if ( isinstance(node, ast.AnnAssign) and isinstance(node.target, ast.Name) - and node.target.id == "CVL_HELP_MESSAGES" + and node.target.id == name ): - assert node.value is not None, "CVL_HELP_MESSAGES has no value" - # entries are pure literals (dicts of implicitly-concatenated - # string constants), so literal_eval reconstructs them exactly + assert node.value is not None, f"{name} has no value" + # the seed data is pure literals (dicts of implicitly-concatenated + # string constants), so literal_eval reconstructs it exactly return ast.literal_eval(node.value) - raise AssertionError("CVL_HELP_MESSAGES assignment not found in kb_populate.py") + raise AssertionError(f"{name} assignment not found in kb_populate.py") + + +def _load_messages() -> list[dict[str, str]]: + return _load_literal("CVL_HELP_MESSAGES") def test_entries_are_well_formed(): @@ -55,23 +59,34 @@ def test_titles_are_unique(): # Bodies cross-reference other articles with the fixed phrase # `article titled "<exact title>"` so a following agent can KBGet by exact -# key. The marker + closing quote delimit the title verbatim (titles contain -# no double quotes, enforced below), so plain splitting recovers it exactly. -CROSS_REF_MARKER = 'article titled "' - - +# key. The graph is declared as data (KB_CROSS_REFERENCES in kb_populate.py) +# rather than recovered from the prose, so the test only checks declared +# facts: every declared reference names an existing article and its citing +# phrase appears verbatim in the declaring body. A cross-reference added to a +# body without a matching map entry is not detected — keep the map in sync. def test_cross_references_resolve(): messages = _load_messages() - titles = {entry["title"] for entry in messages} + cross_refs: dict[str, list[str]] = _load_literal("KB_CROSS_REFERENCES") + bodies = {entry["title"]: entry["body"] for entry in messages} + titles = set(bodies) for title in titles: assert '"' not in title, ( f"title {title!r} contains a double quote, breaking the " f"cross-reference convention" ) - for entry in messages: - for chunk in entry["body"].split(CROSS_REF_MARKER)[1:]: - referenced = chunk.split('"', 1)[0] + for source, referenced_titles in cross_refs.items(): + assert source in titles, ( + f"KB_CROSS_REFERENCES declares unknown source article {source!r}" + ) + assert referenced_titles, ( + f"KB_CROSS_REFERENCES entry for {source!r} is empty — drop it" + ) + for referenced in referenced_titles: assert referenced in titles, ( - f"article {entry['title']!r} references unknown article " + f"article {source!r} declares a reference to unknown article " f"{referenced!r}" ) + assert f'article titled "{referenced}"' in bodies[source], ( + f"article {source!r} declares a reference to {referenced!r} " + f"but its body lacks the citing phrase" + )