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

[shellygr]

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

[shellygr]

claude, have you THOUGHT LONG AND HARD ABOUT THIS?

[shellygr]

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]

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]

to adapt to John's edit agent

[shellygr]

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