Stop false 'keccak/unstructured storage is unreachable' skips; gate skip justifications by shellygr · Pull Request #39 · Certora/AutoProver

shellygr · 2026-07-03T19:27:37Z

Part 1 of 6 related spec-quality PRs derived from comparing generated specs against hand-written specs from a recent customer engagement (generated specs skipped properties claiming keccak-derived storage slots are unreachable in CVL — they are not).

What

prop_inference.py CERTORA_BACKEND_GUIDANCE: hash collision/inversion reasoning remains out of scope, but keccak-derived storage slots are compile-time constants — hookable via Sload/Sstore and exposable via harness getters.
property_generation_prompt.j2: new <storage_access> block (slot-constant definitions, slot hooks, ghost mirroring, harness getters, KB pointers).
property_judge_system_prompt.j2: "No Source Changes" → "No Protocol Source Changes"; harnesses are verification infrastructure. Harness-augmentation wording is injected by property_feedback_judge(harness_augmentation: bool = False) into both judge templates through one bind helper (no-op until the main-harness PR flips the argument).
property_judge_prompt.j2 Criteria 7: judge must check slot-hook / harness-getter / ghost+summary expressibility before accepting a "not expressible" skip, and audits access-shaped skip reasons whose declared category isn't storage_access; greenfield keeps unconditional rejection (author controls the stubs).
cvl_generation.py _RecordSkipSchema: required reason_category: Literal["storage_access", "hash_collision", "prover_limitation", "environment", "other"] plus required alternatives_considered. The gate is purely structural: a storage_access skip cannot be recorded until alternatives_considered is non-empty — no text matching over LLM prose. Category and alternatives are surfaced verbatim to the judge and covered by the validation digest (mutating them stales the stamp; default "other" category and empty alternatives hash like legacy for cache back-compat).

Design revisions after architecture review

Regex skip gate (_SKIP_GATE_CHECKS/_KECCAK_SLOT) deleted — NLP-in-regex over LLM prose was brittle; the author now self-classifies via the reason_category enum and the gate checks structure only.
Classification honesty moved to the judge — Criteria 7 gained one line auditing access-shaped reasons categorized as anything other than storage_access (judge polices semantics, not a regex).
reason_category joins _compute_digest only when non-default, so cached pre-field skips keep their legacy digests and stamps.
Mirrored NotRequired harness_augmentation fields on FeedbackInherentParams/JudgeSystemParams (aligned only by comments) removed — the flag now threads once through property_feedback_judge into both template binds, so the two judge prompts cannot disagree.
Render tests assert harness wording is present/absent in both judge templates together for flag true and false, including through the injection helper itself.

Cross-PR interactions

harness_augmentation is flipped to true by the ap-main-harness PR (Main-contract augmentation harness: unstructured-storage getters, helper decomposition, verify-target threading #40) changing exactly one Python argument at the property_feedback_judge call site; safe to merge in either order.
The reason_category + structural gate + digest coverage + judge-audit design is the shared "structured exception ledger" pattern that Vacuity detection + repair ladder: fix setup root causes instead of filtering methods #41 (vacuity repair) reuses for acknowledge_vacuous_method; Vacuity detection + repair ladder: fix setup root causes instead of filtering methods #41 rebases on this PR's _compute_digest and judge-input plumbing.
Touches property_generation_prompt.j2/property_judge_prompt.j2 in disjoint sections from ap-vacuity-repair and ap-cvlmath; later-merging PR rebases mechanically.

Tests

uv run pytest tests/ -q -m "not expensive" --ignore=tests/test_rag_db.py --ignore=tests/test_token_usage.py → 137 passed, 3 skipped, 3 deselected (ignored files fail identically on master: Postgres testcontainer / model-registry env). tests/test_cvl_skips.py rewritten for the enum gate (structural gating, digest back-compat, judge surfacing); tests/test_template_render.py gained the cross-template agreement tests. Pyright on changed files: 0 errors.

🤖 Generated with Claude Code

Generated specs skipped properties whose state lives in keccak-derived storage slots, citing CVL inexpressibility. Keccak slots are compile-time constants reachable via Sload/Sstore hooks, ghosts, or harness getters; five coordinated changes stop both the author and the judge from blessing such skips: - prop_inference.py: narrow backend-guidance item 2 to hash collisions/inversion; keccak-derived slot constants and unstructured storage are explicitly in scope. - property_generation_prompt.j2: new <storage_access> block (slot-constant definitions, Sload/Sstore hooks incl. KEY patterns, ghost mirroring, harness getters, KB search pointer). - property_judge_system_prompt.j2: "No Source Changes" becomes "No Protocol Source Changes" -- harnesses are verification infrastructure. The demand-a-harness wording is gated on harness_augmentation (default(false), a no-op until harness augmentation lands); the fallback labels such skips "missing harness support, not CVL inexpressibility". - property_judge_prompt.j2 Criteria 7: capability checklist (slot constant + hook, harness getter/direct storage, ghost + summary) the judge must run before accepting a "not expressible" skip. - cvl_generation.py: _RecordSkipSchema requires alternatives_considered; access-shaped skip reasons (keccak/storage slot/unstructured/no getter/cannot access|observe) are rejected until each triggered capability is addressed. Adds render smoke tests for the modified templates (with/without harness_augmentation) and skip-gate acceptance/rejection tests. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…, collision carve-out Three review findings on the skip-gate change: - property_judge_prompt.j2: the Criteria 7 immutability carve-out still blessed any skip fixable "with Solidity code changes", contradicting the checklist item (b) six lines above and the protocol-vs-harness system prompt. It is now scoped to *protocol* code only, and explicitly states that needing a harness getter/wrapper does not validate a skip. - SkippedProperty carries alternatives_considered (defaulted for cached pre-field instances) and the property_feedback_judge input renders each alternative under the skip line, so the judge audits their substance instead of the gate keyword-matching them and dropping the text. The field stays out of _compute_digest (skip identity remains title+reason). - The bare "keccak" gate trigger fired on collision/inversion/preimage skips, which the guidance keeps legitimate; the trigger now requires keccak near "slot"/"storage" (the access-shaped usage the gate targets). Adds tests: collision reason passes the gate, alternatives land on the recorded skip, back-compat deserialization without the new field, and a render pin that the old blanket immutability wording is gone. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Review finding: the Criteria 7 directives ("if any of these mechanisms applies, reject the skip"; "needing a harness getter or wrapper does NOT make a skip valid") told the judge to reject harness-requiring skips even in pipelines where the author has no tool to create harnesses, tensioning with the system prompt's harness_augmentation=false fallback and burning author/judge rounds until the rebuttal escape hatch fired. Criteria 7 now branches on the same harness_augmentation variable as the system prompt (default false): the fallback keeps rejection for the always-available mechanisms (slot constant + hook, direct storage access, ghost mirroring) but accepts harness-getter-only skips with the "missing harness support, not CVL inexpressibility" label, matching the system prompt wording. FeedbackInherentParams gains the NotRequired param so PR 2 can bind both templates consistently; current call sites omit it. Render tests pin both branches and omitted==explicit-false equivalence. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…shaped skip triggers The judge audits alternatives_considered (feedback.py surfaces them), so mutating them after validation must stale the PROVER stamp; empty lists contribute nothing, keeping cached pre-field digests valid. Also widen the skip-gate triggers to `cannot (be )?(access|observ)` so passive phrasings ("cannot be accessed/observed") no longer bypass the gate. Tests pin both. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

In greenfield the author defines the contract API through the stub, so a missing getter is never a capability gap: getter-shaped skips stay rejectable there instead of being accepted with the fallback label. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

shellygr · 2026-07-03T20:05:49Z

+# about collisions/inversion/preimages of the hash function itself — so the keccak trigger
+# requires the word near "slot"/"storage", the access-shaped usage this gate targets.
+_KECCAK_SLOT = r"keccak\S*.{0,40}(?:slot|storage)|(?:slot|storage).{0,40}keccak"
+_SKIP_GATE_CHECKS: list[tuple[re.Pattern[str], str, re.Pattern[str]]] = [


claude, have you THOUGHT LONG AND HARD ABOUT THIS?

The record_skip gate no longer does NLP-in-regex over LLM prose (_SKIP_GATE_CHECKS/_KECCAK_SLOT are gone). The author instead self-classifies every skip via a required reason_category Literal on the tool schema; the gate is purely structural: a storage_access skip cannot be recorded until alternatives_considered is non-empty. The judge polices classification honesty — the category is surfaced in its input and Criteria 7 instructs it to audit access-shaped reasons categorized otherwise as storage_access. SkippedProperty defaults the category to "other" for cache back-compat, and only non-default categories join _compute_digest (the same empty-contributes-nothing scheme as alternatives_considered), so cached pre-field skips keep their legacy digests and validation stamps. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

The mirrored NotRequired harness_augmentation fields on FeedbackInherentParams/JudgeSystemParams (aligned only by comments) are gone. property_feedback_judge now takes harness_augmentation: bool = False and injects it into BOTH the task-prompt and system-prompt binds via one helper, so the two judge templates cannot disagree; a pipeline that gains harness augmentation flips exactly one Python argument. The templates' default(false) remains as a render fail-safe only. Render tests assert the harness wording is present/absent in both templates together for flag true and false, including through the _bind_harness_augmentation injection path itself. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

shellygr · 2026-07-03T23:55:23Z

Reworked per the architecture review — delta since the previous version (aef046a → b7cf58e):

The regex skip gate is gone: _SKIP_GATE_CHECKS/_KECCAK_SLOT deleted from cvl_generation.py. The author now declares a required reason_category enum (storage_access / hash_collision / prover_limitation / environment / other) on _RecordSkipSchema.
The gate is purely structural: a storage_access skip is rejected until alternatives_considered is non-empty — no text matching over LLM prose.
The judge polices classification honesty: reason_category is surfaced in its input, and Criteria 7 now audits access-shaped skip reasons categorized as anything else as if they were storage_access.
Cache back-compat: category defaults to "other" and only non-default values join _compute_digest, so pre-field cached skips keep their legacy digests and validation stamps.
The mirrored NotRequired harness_augmentation fields in feedback.py are removed; the flag threads once through property_feedback_judge(harness_augmentation: bool = False) into both judge-template binds, with render tests asserting the two templates agree for both flag values.
tests/test_cvl_skips.py rewritten for the enum gate; suite: 137 passed, 3 skipped, 3 deselected.

shellygr · 2026-07-04T15:32:31Z

   key compromising, phishing, etc.)
-2. Reasoning about hash function behavior or hash collisions (e.g.,
-   "invalid signatures should be rejected")
+2. Reasoning about hash function *collisions or inversion* (e.g.,


We need to see how this updated section interacts with proper erc-7201 annotations. It may apply in cases where proper annotations do not exist or that we failed to parse them.

shellygr · 2026-07-04T15:38:51Z

-  If the property being skipped could be formalized with Solidity code changes, the skip is VALID. Do *NOT* reject
-  skips with advice to change the Solidity code. The Solidity code is *IMMUTABLE* and suggestions to change the Solidity
-  code are INVALID.
+  If the property being skipped could be formalized only with *protocol* Solidity code changes, the skip is VALID.


to adapt to John's edit agent

shellygr · 2026-07-04T15:39:48Z


 {% if sort != "greenfield" %}
-## No Source Changes
+## No Protocol Source Changes


n.b. protocol source changes means we do not change the original files, but source changes involving harnesses are allowed

jtoman · 2026-07-06T22:17:16Z

+            "to READ from CVL (private/internal fields, unstructured or keccak-addressed storage, "
+            "no public getter); `hash_collision` — the property requires reasoning about "


again, private/internal fields are eminently readable from cvl via direct storage access, and this tool text will land in the attention window of the agent before it ever sees the CVL research articles about this being possible. This will make the problem worse, not better, the agent will start out thinking that private/internal storage fields can't be read and this is a problem to be overcome.

jtoman · 2026-07-06T22:19:51Z

+            "The alternative CVL/verification mechanisms you considered before skipping, and why "
+            "each does not work for this property. Required (non-empty) when `reason_category` is "
+            "`storage_access`, where you MUST address the applicable mechanisms among: precomputed "
+            "keccak storage-slot constants (keccak256 is a built-in CVL function), Sload/Sstore "


this is true (keccak256 is built in), but doing keccak256("whatever.namespace") in cvl won't yield the same value as the (likely precomputed) constant generated by the solidity compiler. Further, there's no way to do storage[keccak256("whatever")], the only way keccak256 would help you here is if you wrote a raw storage acccess hook and did conditional branching on slot == keccak256("..."). But, again, this doesn't work, because the value computed by keccak256 doesn't actually match whatever concrete value is being computed by the solidity compiler.

the solution is to allow munging/editing around unstructured storage so our existing (and quite robust!) support for eip-7201 makes this problem go away.

For reference, on some project (I forget which), once I got the eip-7201 annotations in the right place (in autosetup) the cvl author was able to use the names we generated just fine.

So: I agree we should reject skips around unstructured storage, but the fix mechanism does not (and cannot) exist spec side.

jtoman · 2026-07-06T22:22:48Z

+  (c) ghost state mirroring the value via storage hooks or function summaries.
+
+  The author self-classifies each skip with a reason category (shown alongside the skip): if the
+  reason is access-shaped — state described as private, unstructured, keccak-addressed, or lacking


I will note the "private" restriction is, again, totally invented by claude here, and trust all future such "limitations" are cleaned up rather than continuing to point them out

jtoman · 2026-07-06T22:23:27Z

+  Do *NOT* reject skips with advice to change the protocol Solidity code. The *protocol* Solidity code is
+  *IMMUTABLE* and suggestions to change the protocol code are INVALID. Verification *harnesses* (contracts under
+  `certora/harnesses/`) are NOT protocol code:
+  {% if harness_augmentation | default(false) %}
+  needing a harness getter or wrapper (mechanism (b) above) does NOT make a skip valid under this rule.
+  {% else %}
+  a skip needing only a harness getter or wrapper is NOT validated by this rule — it falls under the
+  "missing harness support" labeling above.
+  {% endif %}


this advice will collide with my editor agent advice soon

jtoman · 2026-07-06T22:26:25Z

+slots are compile-time constants. The available mechanisms are:
+
+* **Slot-constant `definition`s**: compute the concrete 32-byte slot value *once* (from the constant declared
+  in the source, or by evaluating the keccak expression yourself) and bind it with a CVL `definition`, e.g.,


evaluating the keccak expression yourself

We think claude can reliably simulate the sha3 algorithm???

Not sure about the API we use but the chatbots get it right. But those are probably highly engineered behind the scene to write sandboxed code and execute it

shellygr and others added 5 commits July 3, 2026 20:27

shellygr commented Jul 3, 2026

View reviewed changes

shellygr mentioned this pull request Jul 3, 2026

Property portfolio: requireInvariant discipline, 6-lens coverage checklist, multi-call techniques #43

Open

shellygr and others added 2 commits July 4, 2026 02:46

shellygr mentioned this pull request Jul 3, 2026

Ship CVLMath relational math library; prefer relational properties over formula mirroring #42

Draft

This was referenced Jul 4, 2026

Main-contract augmentation harness: unstructured-storage getters, helper decomposition, verify-target threading #40

Draft

Vacuity detection + repair ladder: fix setup root causes instead of filtering methods #41

Draft

shellygr added the autoprover label Jul 4, 2026

shellygr mentioned this pull request Jul 4, 2026

KB: 8 articles on storage-slot access, harnessing, vacuity repair, and multi-call idioms #44

Open

shellygr commented Jul 4, 2026

View reviewed changes

jtoman reviewed Jul 6, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Stop false 'keccak/unstructured storage is unreachable' skips; gate skip justifications#39

Stop false 'keccak/unstructured storage is unreachable' skips; gate skip justifications#39
shellygr wants to merge 7 commits into
masterfrom
shelly/ap-keccak-skip-gate

shellygr commented Jul 3, 2026 •

edited

Loading

Uh oh!

shellygr Jul 3, 2026

Uh oh!

shellygr commented Jul 3, 2026

Uh oh!

shellygr Jul 4, 2026

Uh oh!

shellygr Jul 4, 2026

Uh oh!

shellygr Jul 4, 2026

Uh oh!

jtoman Jul 6, 2026

Uh oh!

jtoman Jul 6, 2026

Uh oh!

jtoman Jul 6, 2026

Uh oh!

jtoman Jul 6, 2026

Uh oh!

jtoman Jul 6, 2026

Uh oh!

jtoman Jul 6, 2026

Uh oh!

shellygr Jul 6, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

		"to READ from CVL (private/internal fields, unstructured or keccak-addressed storage, "
		"no public getter); `hash_collision` — the property requires reasoning about "

Uh oh!

Conversation

shellygr commented Jul 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What

Design revisions after architecture review

Cross-PR interactions

Tests

Uh oh!

Choose a reason for hiding this comment

Uh oh!

shellygr commented Jul 3, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

shellygr commented Jul 3, 2026 •

edited

Loading