From b6e5e7ae3e29e9e7f7dc5cc9096bb48c1261b1a7 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 3 Jul 2026 20:27:42 +0300 Subject: [PATCH 1/7] Kill the false "keccak/unstructured storage is unreachable" doctrine 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 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 --- composer/spec/cvl_generation.py | 58 ++++++++++++- composer/spec/feedback.py | 5 ++ composer/spec/prop_inference.py | 11 ++- .../templates/property_generation_prompt.j2 | 21 +++++ composer/templates/property_judge_prompt.j2 | 9 ++ .../templates/property_judge_system_prompt.j2 | 25 ++++-- tests/test_cvl_skips.py | 81 ++++++++++++++++- tests/test_template_render.py | 86 +++++++++++++++++++ 8 files changed, 286 insertions(+), 10 deletions(-) create mode 100644 tests/test_template_render.py diff --git a/composer/spec/cvl_generation.py b/composer/spec/cvl_generation.py index ba8da4b..aad33e2 100644 --- a/composer/spec/cvl_generation.py +++ b/composer/spec/cvl_generation.py @@ -7,6 +7,7 @@ """ import hashlib +import re from dataclasses import dataclass from typing import Annotated, Callable, Literal, NotRequired, override, Awaitable, Any, Protocol from typing_extensions import TypedDict @@ -305,6 +306,36 @@ async def run(self) -> Command: ) return tool_state_update(self.tool_call_id, msg) +# Skip gate: reasons of the shape "the state is hard to *access*" name a capability gap that +# CVL can bridge, not an expressiveness limit. Each entry pairs a trigger pattern (matched +# against the skip reason) with the capability that must be addressed in +# ``alternatives_considered`` and the evidence pattern used to detect that the capability was +# actually discussed. A skip whose reason fires a trigger is rejected until every triggered +# capability is addressed. +_SKIP_GATE_CHECKS: list[tuple[re.Pattern[str], str, re.Pattern[str]]] = [ + ( + re.compile(r"keccak|storage slot|unstructured", re.IGNORECASE), + "a precomputed keccak storage-slot constant (keccak256 is a built-in CVL function)", + re.compile(r"keccak|slot", re.IGNORECASE), + ), + ( + re.compile(r"keccak|storage slot|unstructured|cannot (access|observe)", re.IGNORECASE), + "Sload/Sstore storage hooks on the slot/path in question", + re.compile(r"sload|sstore|hook", re.IGNORECASE), + ), + ( + re.compile(r"no (public )?getter|cannot (access|observe)|unstructured", re.IGNORECASE), + "a harness getter/helper or direct storage access (currentContract.)", + re.compile(r"harness|getter|helper|currentContract|direct storage", re.IGNORECASE), + ), + ( + re.compile(r"cannot (access|observe)", re.IGNORECASE), + "ghost state mirroring the value via hooks or summaries", + re.compile(r"ghost", re.IGNORECASE), + ), +] + + @tool_display( lambda p: f"Skipping property `{p.get('property_title', '?')}`", suppress_ack("Skip result", ("Recorded skip",)), @@ -312,7 +343,8 @@ async def run(self) -> Command: class _RecordSkipSchema(WithInjectedState[CVLGenerationState], WithInjectedId, WithImplementation[Command]): """ Declare that you are skipping a property from the batch. - You must provide the property's title and a justification. + You must provide the property's title, a justification, and the alternative + mechanisms you considered before skipping. The feedback judge will evaluate whether your justification is valid. Only use this after genuinely attempting to formalize the property. """ @@ -322,6 +354,14 @@ class _RecordSkipSchema(WithInjectedState[CVLGenerationState], WithInjectedId, W reason: str = Field( description="Justification for why this property cannot be formalized" ) + alternatives_considered: list[str] = Field( + description=( + "The alternative CVL/verification mechanisms you considered before skipping, and why " + "each does not work for this property. Where applicable you MUST address: precomputed " + "keccak storage-slot constants (keccak256 is a built-in CVL function), Sload/Sstore " + "storage hooks, harness getters/helpers, and ghost mirroring of contract state." + ) + ) @override def run(self) -> Command: @@ -336,6 +376,22 @@ def run(self) -> Command: self.tool_call_id, "A non-empty justification is required when skipping a property.", ) + missing = [ + capability + for trigger, capability, evidence in _SKIP_GATE_CHECKS + if trigger.search(self.reason) + and not any(evidence.search(alt) for alt in self.alternatives_considered) + ] + if missing: + return tool_state_update( + self.tool_call_id, + "Skip REJECTED: the stated reason suggests the state is merely hard to *access*, " + "which is a capability gap CVL can bridge, not an expressiveness limit. Before " + "this skip can be recorded, `alternatives_considered` must address: " + + "; ".join(missing) + + ". Either attempt the applicable mechanism, or explain in " + "`alternatives_considered` why it does not apply to this property.", + ) skip = SkippedProperty( property_title=self.property_title, reason=self.reason, diff --git a/composer/spec/feedback.py b/composer/spec/feedback.py index 5f64d7b..e6d023b 100644 --- a/composer/spec/feedback.py +++ b/composer/spec/feedback.py @@ -46,6 +46,11 @@ class FeedbackInherentParams(TypedDict): class JudgeSystemParams(TypedDict): sort: Sort + # Whether the pipeline can (re)generate main-contract augmentation harnesses. When true, + # the judge template's "demand a harness getter/wrapper instead of accepting the skip" + # wording is rendered; the template defaults it to false, so pipelines without harness + # augmentation may simply omit it. + harness_augmentation: NotRequired[bool] # Judge system prompt, shared between the natspec and source-mode flows. The fs # primitives are always documented; ``sort`` drives the rest (the template diff --git a/composer/spec/prop_inference.py b/composer/spec/prop_inference.py index ee1d1bc..97e7103 100644 --- a/composer/spec/prop_inference.py +++ b/composer/spec/prop_inference.py @@ -88,8 +88,15 @@ class RefinementState(MessagesState): 1. Attack vectors or invariants that reference off-chain events (like 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., + "invalid signatures should be rejected"). NB: this exclusion is + narrow. `keccak256` is a built-in CVL function, and storage-slot + constants derived from it (ERC-7201 namespaces, EIP-1967 proxy + slots, `keccak256(name) - 1` patterns) are compile-time constants + that can be precomputed and hooked via `Sload`/`Sstore` slot hooks. + Unstructured storage is likewise reachable via such hooks or via + harness getters. NEVER reject a property merely because the state + it references lives in keccak-derived storage slots. 3. Event emission (not impossible, simply difficult and tedious) In addition, due to the advent of checked arithmetic, properties that diff --git a/composer/templates/property_generation_prompt.j2 b/composer/templates/property_generation_prompt.j2 index d96585c..3ee687c 100644 --- a/composer/templates/property_generation_prompt.j2 +++ b/composer/templates/property_generation_prompt.j2 @@ -107,6 +107,27 @@ within the generated summary, match the callee contract against known implemente For those callees, simply dispatch the call to the relevant implementation. For calls "outside" of the prover inputs, fall back on a sound model of the external behavior, using e.g., ghosts. + +Never conclude that contract state is "unreachable" (and never skip a property on that basis) merely because +the state lives in keccak-derived storage slots (ERC-7201 namespaced storage, EIP-1967 proxy slots, +`keccak256(name) - 1` patterns) or lacks a public getter. `keccak256` is a built-in CVL function, and these +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., + `definition IMPLEMENTATION_SLOT() returns uint256 = 0x360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc;` +* **`Sload`/`Sstore` hooks**: hook reads/writes of the storage in question to observe or constrain its value. + For state reached through named storage paths, use the named-path hook patterns with `KEY`, e.g., + `hook Sstore _balances[KEY address user] uint256 newVal { ... }`. +* **Ghost mirroring**: declare a ghost variable updated by an `Sstore` hook (and constrained by the matching + `Sload` hook), then reference the ghost in your rules/invariants. +* **Harness getters**: as a fallback, if the verification setup includes harness contracts, their external + view getters expose otherwise-private/unstructured state directly. + +Before concluding that any state is unreachable, search the knowledge base for "keccak storage slot" and +"unstructured storage hook" — these entries document the exact hook grammar and worked examples. + + ## Step 4 Once all non-skipped properties have been approved by the feedback judge, AND all rules that are not expected diff --git a/composer/templates/property_judge_prompt.j2 b/composer/templates/property_judge_prompt.j2 index 537b2af..d494843 100644 --- a/composer/templates/property_judge_prompt.j2 +++ b/composer/templates/property_judge_prompt.j2 @@ -168,6 +168,15 @@ Verify that the specification covers all {{ properties | length }} listed proper perform your own research (or examine any CVL Document references cited in their skip) and critically examine their claims about CVL expressivity when evaluating the skip. + Before accepting ANY skip justified as "not expressible in CVL" — in particular one claiming that state is + private, unstructured, keccak-addressed, or lacks a getter — you must verify that NONE of the following + mechanisms make the property expressible: + (a) a precomputed keccak storage-slot constant (`keccak256` is a built-in CVL function; ERC-7201 namespaces + and EIP-1967 slots are compile-time constants) combined with an `Sload`/`Sstore` hook on that slot; + (b) a harness getter or direct storage access (e.g., `currentContract.`); + (c) ghost state mirroring the value via storage hooks or function summaries. + If any of these mechanisms applies, reject the skip and name the applicable mechanism. + *Exception*: if the author has filed an empirical rebuttal (see Step 1) against a prior-round formalization you proposed, accept that rebuttal per the Step 1 evaluation rules — do not re-insist on the same proposal. If the rebuttal establishes that no working formalization was diff --git a/composer/templates/property_judge_system_prompt.j2 b/composer/templates/property_judge_system_prompt.j2 index 31e187b..2fefe4e 100644 --- a/composer/templates/property_judge_system_prompt.j2 +++ b/composer/templates/property_judge_system_prompt.j2 @@ -20,12 +20,27 @@ {% endwith %} {% if sort != "greenfield" %} -## No Source Changes +## No Protocol Source Changes -Do NOT provide any feedback suggesting the Solidity code under verification (including verification harnesses) -be modified. The Solidity code under verification is *immutable* and cannot be changed. If the only feedback you can provide -involves changing the source code, do *NOT* provide that feedback, it is *INVALID*. +Do NOT provide any feedback suggesting the *protocol* Solidity code under verification be modified. The protocol +code is *immutable* and cannot be changed. If the only feedback you can provide involves changing the protocol +source code, do *NOT* provide that feedback, it is *INVALID*. Note that this includes rejecting property skipping with feedback to the effect of "change the code". If the only way to formalize -and prove a property is to change the source code, then skipping that property *IS* acceptable. +and prove a property is to change the *protocol* source code, then skipping that property *IS* acceptable. + +Verification *harnesses* (contracts under `certora/harnesses/`) are NOT protocol code: they are verification +infrastructure, existing precisely to expose state and behavior the protocol does not surface publicly. +{# harness_augmentation is set only by pipelines that can actually (re)generate main-contract + augmentation harnesses; default(false) keeps the demand-wording a no-op everywhere else. #} +{% if harness_augmentation | default(false) %} +If a property is skipped only because state or behavior is not publicly exposed, do NOT accept the skip as +"not expressible in CVL". Instead, demand a harness augmentation (an external view getter or a thin wrapper +under `certora/harnesses/`) that exposes the needed state, and reject the skip until the property has been +attempted against the augmented harness. +{% else %} +If a property is skipped only because state or behavior is not publicly exposed, you must label the skip as +"missing harness support, not CVL inexpressibility" in your feedback — do NOT endorse claims that such +properties are beyond CVL's expressiveness. +{% endif %} {% endif %} diff --git a/tests/test_cvl_skips.py b/tests/test_cvl_skips.py index 85556bd..24acbc4 100644 --- a/tests/test_cvl_skips.py +++ b/tests/test_cvl_skips.py @@ -43,8 +43,15 @@ _RESULT_NAME = "result" _PUT_CVL = "put_cvl" -def _skip(property_title: str, reason: str) -> ToolCallDict: - return tool_call_raw(name=_RECORD_SKIP_NAME, property_title=property_title, reason=reason) +def _skip(property_title: str, reason: str, alternatives: list[str] | None = None) -> ToolCallDict: + # alternatives_considered is a required tool field; most tests use reasons that don't + # trigger the skip gate, so an empty list suffices unless a test exercises the gate. + return tool_call_raw( + name=_RECORD_SKIP_NAME, + property_title=property_title, + reason=reason, + alternatives_considered=alternatives if alternatives is not None else [], + ) def _unskip(property_title: str) -> ToolCallDict: return tool_call_raw(_UNSKIP_NAME, property_title=property_title) @@ -233,6 +240,76 @@ async def test_invalid_skip_reason(self): assert "A non-empty justification is" in msg +# ========================================================================= +# Skip gate: access-shaped reasons require alternatives_considered coverage +# ========================================================================= + +class TestSkipGate: + def gate_mapper(self, st: CVLTestState) -> tuple[str, list[SkippedProperty]]: + return ( + Scenario.last_single_tool(_RECORD_SKIP_NAME, st), + st["skipped"], + ) + + async def test_keccak_reason_without_alternatives_rejected(self): + (msg, skipped) = await scenario(1).turn( + _skip("p0", "the balance lives in a keccak-derived storage slot with no way to read it") + ).map(self.gate_mapper).run() + assert skipped == [] + assert msg.startswith("Skip REJECTED:") + assert "keccak storage-slot constant" in msg + assert "Sload/Sstore storage hooks" in msg + + async def test_keccak_reason_with_alternatives_accepted(self): + (msg, skipped) = await scenario(1).turn( + _skip( + "p0", + "the balance lives in a keccak-derived storage slot", + alternatives=[ + "precomputed the keccak slot constant, but the slot value depends on a runtime salt", + "an Sstore hook on the slot cannot fire because writes go through delegatecall", + ], + ) + ).map(self.gate_mapper).run() + assert msg.startswith("Recorded skip") + assert len(skipped) == 1 and skipped[0].property_title == "p0" + + async def test_trigger_matching_is_case_insensitive(self): + (msg, skipped) = await scenario(1).turn( + _skip("p0", "state is in Unstructured Storage and CANNOT ACCESS it from CVL") + ).map(self.gate_mapper).run() + assert skipped == [] + assert msg.startswith("Skip REJECTED:") + + async def test_no_getter_reason_requires_harness_capability(self): + (msg, skipped) = await scenario(1).turn( + _skip("p0", "there is no public getter for the internal accumulator") + ).map(self.gate_mapper).run() + assert skipped == [] + assert "harness getter/helper" in msg + + async def test_cannot_observe_reason_requires_ghost_capability(self): + (msg, skipped) = await scenario(1).turn( + _skip( + "p0", + "we cannot observe the intermediate value", + alternatives=[ + "Sload/Sstore hooks don't fire on memory values", + "a harness getter cannot expose transient memory", + ], + ) + ).map(self.gate_mapper).run() + assert skipped == [] + assert "ghost state mirroring" in msg + + async def test_unrelated_reason_passes_with_empty_alternatives(self): + (msg, skipped) = await scenario(1).turn( + _skip("p0", "requires quantifying over arbitrary-length arrays") + ).map(self.gate_mapper).run() + assert msg.startswith("Recorded skip") + assert len(skipped) == 1 + + # ========================================================================= # Validation stamping + check_completion via graph # ========================================================================= diff --git a/tests/test_template_render.py b/tests/test_template_render.py new file mode 100644 index 0000000..b5d2bf6 --- /dev/null +++ b/tests/test_template_render.py @@ -0,0 +1,86 @@ +""" +Render smoke tests for the prompt templates touched by the keccak/unstructured-storage +skip-gate work. These catch missing-variable regressions (a template referencing a +variable its callers don't supply) and pin the gating behavior of the judge system +prompt's `harness_augmentation` variable, which defaults to false in the template so +pipelines without harness augmentation can omit it entirely. +""" +import pytest + +from composer.templates.loader import load_jinja_template +from composer.spec.prop import PropertyFormulation + + +def _props() -> list[PropertyFormulation]: + return [ + PropertyFormulation( + title="total_supply_preserved", + methods="invariant", + sort="invariant", + description="the total supply is preserved by all operations", + ), + PropertyFormulation( + title="no_free_mint", + methods=["mint(address,uint256)"], + sort="attack_vector", + description="an attacker cannot mint tokens for free", + ), + ] + + +class TestJudgeSystemPrompt: + def test_renders_without_harness_augmentation(self): + # harness_augmentation omitted: the template's `default(false)` must render the + # fallback wording (label as missing harness support), not the demand wording. + out = load_jinja_template("property_judge_system_prompt.j2", sort="existing") + assert "No Protocol Source Changes" in out + assert "missing harness support, not CVL inexpressibility" in out + assert "demand a harness augmentation" not in out + + def test_renders_with_harness_augmentation(self): + out = load_jinja_template( + "property_judge_system_prompt.j2", sort="existing", harness_augmentation=True + ) + assert "demand a harness augmentation" in out + assert "missing harness support, not CVL inexpressibility" not in out + + def test_explicit_false_matches_omitted(self): + omitted = load_jinja_template("property_judge_system_prompt.j2", sort="existing") + explicit = load_jinja_template( + "property_judge_system_prompt.j2", sort="existing", harness_augmentation=False + ) + assert omitted == explicit + + def test_greenfield_has_no_source_change_section(self): + # The whole protocol-immutability section is gated on sort != greenfield + # (greenfield has no pre-existing source to protect). + out = load_jinja_template("property_judge_system_prompt.j2", sort="greenfield") + assert "No Protocol Source Changes" not in out + + +class TestJudgePrompt: + @pytest.mark.parametrize("sort", ["existing", "greenfield"]) + def test_criteria7_skip_checklist_renders(self, sort: str): + out = load_jinja_template( + "property_judge_prompt.j2", properties=_props(), sort=sort, context=None + ) + # The capability checklist the judge must run before accepting a + # "not expressible in CVL" skip lives inside Criteria 7. + assert "Before accepting ANY skip" in out + assert "precomputed keccak storage-slot constant" in out + assert "harness getter or direct storage access" in out + assert "ghost state mirroring" in out + + +class TestGenerationPrompt: + def test_storage_access_block_renders(self): + out = load_jinja_template( + "property_generation_prompt.j2", + contract_name="Widget", + properties=_props(), + resources=[], + context=None, + ) + assert "" in out + assert "Sload" in out and "Sstore" in out + assert "keccak storage slot" in out # the KB search pointer From 0f62a8676dee14602d83163d901613f662e1e2c0 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 3 Jul 2026 20:50:18 +0300 Subject: [PATCH 2/7] Address review: protocol-scope Criteria 7, judge-visible alternatives, 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 --- composer/spec/cvl_generation.py | 18 +++++++++++-- composer/spec/feedback.py | 4 +++ composer/templates/property_judge_prompt.j2 | 8 +++--- tests/test_cvl_skips.py | 28 +++++++++++++++++++++ tests/test_template_render.py | 11 ++++++++ 5 files changed, 64 insertions(+), 5 deletions(-) diff --git a/composer/spec/cvl_generation.py b/composer/spec/cvl_generation.py index aad33e2..afb3734 100644 --- a/composer/spec/cvl_generation.py +++ b/composer/spec/cvl_generation.py @@ -51,6 +51,11 @@ class SkippedProperty(BaseModel): """A property the agent explicitly decided not to formalize.""" property_title: str = Field(description="The unique snake_case title of the property from the batch listing") reason: str = Field(description="Justification for why this property was skipped") + # Defaulted for back-compat with cached instances that predate the field. + alternatives_considered: list[str] = Field( + default_factory=list, + description="The alternative mechanisms the author considered before skipping, and why each does not work", + ) class PropertyRuleMapping(BaseModel): @@ -152,6 +157,9 @@ def _compute_digest(curr_spec: str, skipped: list[SkippedProperty]) -> str: digester = hashlib.md5() digester.update(curr_spec.encode()) for s in skipped: + # alternatives_considered is deliberately excluded: the skip's identity is its + # title+reason, and including the (judge-visible but advisory) alternatives would + # stale-out validation stamps on cached pre-field skips. digester.update(f"{s.property_title}:{s.reason}".encode()) return digester.hexdigest() @@ -312,14 +320,19 @@ async def run(self) -> Command: # ``alternatives_considered`` and the evidence pattern used to detect that the capability was # actually discussed. A skip whose reason fires a trigger is rejected until every triggered # capability is addressed. +# +# A bare "keccak" also appears in the one hash-related skip that stays legitimate — reasoning +# 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]]] = [ ( - re.compile(r"keccak|storage slot|unstructured", re.IGNORECASE), + re.compile(rf"{_KECCAK_SLOT}|storage slot|unstructured", re.IGNORECASE), "a precomputed keccak storage-slot constant (keccak256 is a built-in CVL function)", re.compile(r"keccak|slot", re.IGNORECASE), ), ( - re.compile(r"keccak|storage slot|unstructured|cannot (access|observe)", re.IGNORECASE), + re.compile(rf"{_KECCAK_SLOT}|storage slot|unstructured|cannot (access|observe)", re.IGNORECASE), "Sload/Sstore storage hooks on the slot/path in question", re.compile(r"sload|sstore|hook", re.IGNORECASE), ), @@ -395,6 +408,7 @@ def run(self) -> Command: skip = SkippedProperty( property_title=self.property_title, reason=self.reason, + alternatives_considered=self.alternatives_considered, ) return tool_state_update( self.tool_call_id, diff --git a/composer/spec/feedback.py b/composer/spec/feedback.py index e6d023b..e4840b1 100644 --- a/composer/spec/feedback.py +++ b/composer/spec/feedback.py @@ -124,6 +124,10 @@ async def the_tool( input_parts.append("The following properties were explicitly skipped by the author:") for s in skipped: input_parts.append(f" Property {s.property_title}: {s.reason}") + # The alternatives the author claims to have ruled out are part of the skip's + # justification: surface them so the judge can audit their substance. + for alt in s.alternatives_considered: + input_parts.append(f" Alternative considered: {alt}") if rebuttals: input_parts.append( "The author has filed the following rebuttals against feedback from " diff --git a/composer/templates/property_judge_prompt.j2 b/composer/templates/property_judge_prompt.j2 index d494843..3f28cf8 100644 --- a/composer/templates/property_judge_prompt.j2 +++ b/composer/templates/property_judge_prompt.j2 @@ -182,9 +182,11 @@ Verify that the specification covers all {{ properties | length }} listed proper re-insist on the same proposal. If the rebuttal establishes that no working formalization was found, the skip is VALID on the grounds that your prior proposal proved unworkable. {% if sort != "greenfield" %} - 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. + 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: needing a harness getter or wrapper (mechanism (b) above) does + NOT make a skip valid under this rule. {% endif %} **Array quantification limitation**: The Certora Prover cannot universally quantify over diff --git a/tests/test_cvl_skips.py b/tests/test_cvl_skips.py index 24acbc4..3efd855 100644 --- a/tests/test_cvl_skips.py +++ b/tests/test_cvl_skips.py @@ -309,6 +309,34 @@ async def test_unrelated_reason_passes_with_empty_alternatives(self): assert msg.startswith("Recorded skip") assert len(skipped) == 1 + async def test_hash_collision_reason_passes_gate(self): + # Collision/inversion/preimage reasoning is the one keccak-related skip that stays + # legitimate: a bare "keccak" away from slot/storage must not fire the access gate. + (msg, skipped) = await scenario(1).turn( + _skip("p0", "requires reasoning about keccak collisions to forge a valid signature") + ).map(self.gate_mapper).run() + assert msg.startswith("Recorded skip") + assert len(skipped) == 1 + + async def test_alternatives_are_recorded_on_the_skip(self): + # The judge audits alternatives_considered, so the recorded SkippedProperty must + # carry them (not just gate on them and drop them). + alts = [ + "precomputed the keccak slot constant, but the slot depends on a runtime salt", + "an Sstore hook cannot fire because writes go through delegatecall", + ] + (msg, skipped) = await scenario(1).turn( + _skip("p0", "the balance lives in a keccak-derived storage slot", alternatives=alts) + ).map(self.gate_mapper).run() + assert msg.startswith("Recorded skip") + assert skipped[0].alternatives_considered == alts + + async def test_skipped_property_backcompat_without_alternatives(self): + # Cached SkippedProperty instances predate alternatives_considered; deserialization + # must default it rather than fail validation. + s = SkippedProperty.model_validate({"property_title": "p0", "reason": "too hard"}) + assert s.alternatives_considered == [] + # ========================================================================= # Validation stamping + check_completion via graph diff --git a/tests/test_template_render.py b/tests/test_template_render.py index b5d2bf6..2d567ef 100644 --- a/tests/test_template_render.py +++ b/tests/test_template_render.py @@ -71,6 +71,17 @@ def test_criteria7_skip_checklist_renders(self, sort: str): assert "harness getter or direct storage access" in out assert "ghost state mirroring" in out + def test_criteria7_immutability_is_protocol_scoped(self): + # The immutability carve-out must not contradict checklist item (b): only + # *protocol* code changes validate a skip; harness getters/wrappers do not. + out = load_jinja_template( + "property_judge_prompt.j2", properties=_props(), sort="existing", context=None + ) + assert "only with *protocol* Solidity code changes" in out + assert "NOT protocol code" in out + # The old blanket doctrine ("the Solidity code is IMMUTABLE", unqualified) is gone. + assert "The Solidity code is *IMMUTABLE*" not in out + class TestGenerationPrompt: def test_storage_access_block_renders(self): From 2b430e51f874bf7cd0239c8ed3b84ad58085d34e Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 3 Jul 2026 21:10:16 +0300 Subject: [PATCH 3/7] Gate Criteria 7's harness-skip rejection on harness_augmentation 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 --- composer/spec/feedback.py | 6 ++++ composer/templates/property_judge_prompt.j2 | 21 +++++++++-- tests/test_template_render.py | 39 +++++++++++++++++++++ 3 files changed, 64 insertions(+), 2 deletions(-) diff --git a/composer/spec/feedback.py b/composer/spec/feedback.py index e4840b1..445a37b 100644 --- a/composer/spec/feedback.py +++ b/composer/spec/feedback.py @@ -41,6 +41,12 @@ class FeedbackInherentParams(TypedDict): # ``existing`` — pre-existing codebase being verified as-is; target # has real immutable source. sort: Sort + # Mirrors JudgeSystemParams.harness_augmentation and must be bound consistently + # with it: it gates Criteria 7's "reject harness-shaped skips" directive so the + # judge only demands harness getters/wrappers in pipelines that can generate + # them. The template defaults it to false, so pipelines without harness + # augmentation may simply omit it. + harness_augmentation: NotRequired[bool] FeedbackTemplate = TypedTemplate[FeedbackInherentParams]("property_judge_prompt.j2") diff --git a/composer/templates/property_judge_prompt.j2 b/composer/templates/property_judge_prompt.j2 index 3f28cf8..cc7f5d8 100644 --- a/composer/templates/property_judge_prompt.j2 +++ b/composer/templates/property_judge_prompt.j2 @@ -175,7 +175,19 @@ Verify that the specification covers all {{ properties | length }} listed proper and EIP-1967 slots are compile-time constants) combined with an `Sload`/`Sstore` hook on that slot; (b) a harness getter or direct storage access (e.g., `currentContract.`); (c) ghost state mirroring the value via storage hooks or function summaries. +{# harness_augmentation mirrors the identically-named variable in property_judge_system_prompt.j2 and + must be bound consistently with it: only pipelines that can (re)generate main-contract augmentation + harnesses may instruct the judge to reject harness-shaped skips; everywhere else (default(false)) + such skips are accepted with the "missing harness support" label the system prompt mandates. #} +{% if harness_augmentation | default(false) %} If any of these mechanisms applies, reject the skip and name the applicable mechanism. +{% else %} + If mechanism (a) or (c) applies, or (b) applies via direct storage access, reject the skip and name the + applicable mechanism. If the property is expressible ONLY through a new harness getter or wrapper — + a mechanism that cannot be generated in this pipeline — do NOT reject the skip on those grounds; + accept it, but label it as "missing harness support, not CVL inexpressibility". Never endorse a claim + that such a property is beyond CVL's expressiveness. +{% endif %} *Exception*: if the author has filed an empirical rebuttal (see Step 1) against a prior-round formalization you proposed, accept that rebuttal per the Step 1 evaluation rules — do not @@ -185,8 +197,13 @@ Verify that the specification covers all {{ properties | length }} listed proper If the property being skipped could be formalized only with *protocol* Solidity code changes, the skip is VALID. 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: needing a harness getter or wrapper (mechanism (b) above) does - NOT make a skip valid under this rule. + `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 %} {% endif %} **Array quantification limitation**: The Certora Prover cannot universally quantify over diff --git a/tests/test_template_render.py b/tests/test_template_render.py index 2d567ef..cb07e12 100644 --- a/tests/test_template_render.py +++ b/tests/test_template_render.py @@ -82,6 +82,45 @@ def test_criteria7_immutability_is_protocol_scoped(self): # The old blanket doctrine ("the Solidity code is IMMUTABLE", unqualified) is gone. assert "The Solidity code is *IMMUTABLE*" not in out + def test_criteria7_fallback_labels_harness_skips(self): + # harness_augmentation omitted (default false): Criteria 7 must align with the + # system prompt's fallback — harness-shaped skips get the "missing harness + # support" label rather than a rejection the author has no tool to satisfy. + out = load_jinja_template( + "property_judge_prompt.j2", properties=_props(), sort="existing", context=None + ) + assert "missing harness support, not CVL inexpressibility" in out + assert "If any of these mechanisms applies, reject the skip" not in out + assert "does NOT make a skip valid under this rule" not in out + + def test_criteria7_augmentation_rejects_harness_skips(self): + # With harness_augmentation the judge may demand harness getters/wrappers: + # all three mechanisms trigger rejection and harness need does not validate + # a skip under the protocol-immutability carve-out. + out = load_jinja_template( + "property_judge_prompt.j2", + properties=_props(), + sort="existing", + context=None, + harness_augmentation=True, + ) + assert "If any of these mechanisms applies, reject the skip" in out + assert "does NOT make a skip valid under this rule" in out + assert "missing harness support, not CVL inexpressibility" not in out + + def test_criteria7_explicit_false_matches_omitted(self): + omitted = load_jinja_template( + "property_judge_prompt.j2", properties=_props(), sort="existing", context=None + ) + explicit = load_jinja_template( + "property_judge_prompt.j2", + properties=_props(), + sort="existing", + context=None, + harness_augmentation=False, + ) + assert omitted == explicit + class TestGenerationPrompt: def test_storage_access_block_renders(self): From c5a45cd917fe84e8a6573e04cdefa803bafef841 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 3 Jul 2026 21:46:15 +0300 Subject: [PATCH 4/7] Cover alternatives_considered in the validation digest; widen access-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 --- composer/spec/cvl_generation.py | 15 ++++---- tests/test_cvl_skips.py | 64 +++++++++++++++++++++++++++++++++ 2 files changed, 73 insertions(+), 6 deletions(-) diff --git a/composer/spec/cvl_generation.py b/composer/spec/cvl_generation.py index afb3734..d7e441b 100644 --- a/composer/spec/cvl_generation.py +++ b/composer/spec/cvl_generation.py @@ -157,10 +157,13 @@ def _compute_digest(curr_spec: str, skipped: list[SkippedProperty]) -> str: digester = hashlib.md5() digester.update(curr_spec.encode()) for s in skipped: - # alternatives_considered is deliberately excluded: the skip's identity is its - # title+reason, and including the (judge-visible but advisory) alternatives would - # stale-out validation stamps on cached pre-field skips. digester.update(f"{s.property_title}:{s.reason}".encode()) + # The judge audits alternatives_considered as part of the skip's justification + # (feedback.py surfaces them), so changing them must stale the validation stamp. + # An empty list contributes nothing, so digests of cached pre-field skips (which + # deserialize with the default empty list) keep their legacy value. + for alt in s.alternatives_considered: + digester.update(f"|alt:{alt}".encode()) return digester.hexdigest() @@ -332,17 +335,17 @@ async def run(self) -> Command: re.compile(r"keccak|slot", re.IGNORECASE), ), ( - re.compile(rf"{_KECCAK_SLOT}|storage slot|unstructured|cannot (access|observe)", re.IGNORECASE), + re.compile(rf"{_KECCAK_SLOT}|storage slot|unstructured|cannot (be )?(access|observ)", re.IGNORECASE), "Sload/Sstore storage hooks on the slot/path in question", re.compile(r"sload|sstore|hook", re.IGNORECASE), ), ( - re.compile(r"no (public )?getter|cannot (access|observe)|unstructured", re.IGNORECASE), + re.compile(r"no (public )?getter|cannot (be )?(access|observ)|unstructured", re.IGNORECASE), "a harness getter/helper or direct storage access (currentContract.)", re.compile(r"harness|getter|helper|currentContract|direct storage", re.IGNORECASE), ), ( - re.compile(r"cannot (access|observe)", re.IGNORECASE), + re.compile(r"cannot (be )?(access|observ)", re.IGNORECASE), "ghost state mirroring the value via hooks or summaries", re.compile(r"ghost", re.IGNORECASE), ), diff --git a/tests/test_cvl_skips.py b/tests/test_cvl_skips.py index 3efd855..1c68ae4 100644 --- a/tests/test_cvl_skips.py +++ b/tests/test_cvl_skips.py @@ -19,6 +19,7 @@ from composer.spec.cvl_generation import ( CVLGenerationExtra, SkippedProperty, + _compute_digest, check_completion, _FeedbackSchema, _RecordSkipSchema, @@ -302,6 +303,23 @@ async def test_cannot_observe_reason_requires_ghost_capability(self): assert skipped == [] assert "ghost state mirroring" in msg + async def test_passive_access_reason_triggers_gate(self): + # Passive phrasing ("cannot be accessed") must fire the same access-shaped + # triggers as the active form ("cannot access"). + (msg, skipped) = await scenario(1).turn( + _skip("p0", "the accumulated fee cannot be accessed from outside the contract") + ).map(self.gate_mapper).run() + assert skipped == [] + assert msg.startswith("Skip REJECTED:") + assert "ghost state mirroring" in msg + + async def test_passive_observe_reason_triggers_gate(self): + (msg, skipped) = await scenario(1).turn( + _skip("p0", "the pending reward cannot be observed by any external caller") + ).map(self.gate_mapper).run() + assert skipped == [] + assert "harness getter/helper" in msg + async def test_unrelated_reason_passes_with_empty_alternatives(self): (msg, skipped) = await scenario(1).turn( _skip("p0", "requires quantifying over arbitrary-length arrays") @@ -338,6 +356,35 @@ async def test_skipped_property_backcompat_without_alternatives(self): assert s.alternatives_considered == [] +# ========================================================================= +# Digest coverage: alternatives_considered is part of the skip's audited identity +# ========================================================================= + +class TestDigestCoversAlternatives: + def test_digest_changes_with_alternatives(self): + bare = SkippedProperty(property_title="p0", reason="r") + with_alts = SkippedProperty( + property_title="p0", reason="r", alternatives_considered=["tried ghost mirroring"] + ) + assert _compute_digest("spec", [bare]) != _compute_digest("spec", [with_alts]) + + def test_digest_changes_with_alternative_content(self): + a = SkippedProperty( + property_title="p0", reason="r", alternatives_considered=["tried ghost mirroring"] + ) + b = SkippedProperty( + property_title="p0", reason="r", alternatives_considered=["tried Sstore hooks"] + ) + assert _compute_digest("spec", [a]) != _compute_digest("spec", [b]) + + def test_empty_alternatives_preserve_legacy_digest(self): + # Cached pre-field skips deserialize with the default empty list; their digest + # must equal an explicitly-empty one so cached validation stamps stay fresh. + legacy = SkippedProperty.model_validate({"property_title": "p0", "reason": "r"}) + explicit = SkippedProperty(property_title="p0", reason="r", alternatives_considered=[]) + assert _compute_digest("spec", [legacy]) == _compute_digest("spec", [explicit]) + + # ========================================================================= # Validation stamping + check_completion via graph # ========================================================================= @@ -410,6 +457,23 @@ async def test_changed_reason_no_result(self): _result("I'm done") ).map_run(is_result_rejection.check_reason(unsat_feedback_message)) + async def test_changed_alternatives_no_result(self): + # Editing the judge-audited alternatives_considered after validation must stale + # the stamp just like editing the reason does. + reason = "the balance lives in a keccak-derived storage slot" + assert await scenario(1, curr_spec="whatever").turns( + _skip("p0", reason, alternatives=[ + "the keccak slot constant depends on a runtime salt", + "an Sstore hook cannot fire through delegatecall", + ]), + _feedback(), + _skip("p0", reason, alternatives=[ + "the slot constant is not computable at compile time here", + "storage hooks do not fire for delegatecall writes", + ]), + _result("I'm done") + ).map_run(is_result_rejection.check_reason(unsat_feedback_message)) + async def test_other_validation_key_unsat(self): assert await scenario(1, curr_spec="whatever", required=[FEEDBACK_VALIDATION_KEY, "something_else"]).turn( _feedback() From aef046a2d849d749288252f290b57f91325c9571 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 3 Jul 2026 21:46:15 +0300 Subject: [PATCH 5/7] Scope Criteria 7's missing-harness-support fallback to non-greenfield 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 --- composer/templates/property_judge_prompt.j2 | 12 ++++++++++-- tests/test_template_render.py | 11 +++++++++++ 2 files changed, 21 insertions(+), 2 deletions(-) diff --git a/composer/templates/property_judge_prompt.j2 b/composer/templates/property_judge_prompt.j2 index cc7f5d8..63f7285 100644 --- a/composer/templates/property_judge_prompt.j2 +++ b/composer/templates/property_judge_prompt.j2 @@ -178,8 +178,16 @@ Verify that the specification covers all {{ properties | length }} listed proper {# harness_augmentation mirrors the identically-named variable in property_judge_system_prompt.j2 and must be bound consistently with it: only pipelines that can (re)generate main-contract augmentation harnesses may instruct the judge to reject harness-shaped skips; everywhere else (default(false)) - such skips are accepted with the "missing harness support" label the system prompt mandates. #} -{% if harness_augmentation | default(false) %} + such skips are accepted with the "missing harness support" label the system prompt mandates. + Greenfield is checked first because harness pipelines (and the immutability rule the fallback + compensates for) only exist for pre-existing source: the greenfield author shapes the stub's API + themselves, so a missing getter is never a capability gap there. #} +{% if sort == "greenfield" %} + If any of these mechanisms applies, reject the skip and name the applicable mechanism. There is no + pre-existing implementation here: the author defines the contract API through the stub, so a skip + claiming state lacks a getter is invalid — reject it and advise exposing the state through a getter + in the stub. +{% elif harness_augmentation | default(false) %} If any of these mechanisms applies, reject the skip and name the applicable mechanism. {% else %} If mechanism (a) or (c) applies, or (b) applies via direct storage access, reject the skip and name the diff --git a/tests/test_template_render.py b/tests/test_template_render.py index cb07e12..7ba89b1 100644 --- a/tests/test_template_render.py +++ b/tests/test_template_render.py @@ -82,6 +82,17 @@ def test_criteria7_immutability_is_protocol_scoped(self): # The old blanket doctrine ("the Solidity code is IMMUTABLE", unqualified) is gone. assert "The Solidity code is *IMMUTABLE*" not in out + def test_criteria7_greenfield_rejects_getter_skips(self): + # In greenfield the author defines the contract API through the stub, so + # getter-shaped skips stay rejectable and the "missing harness support" + # fallback labeling must not render. + out = load_jinja_template( + "property_judge_prompt.j2", properties=_props(), sort="greenfield", context=None + ) + assert "If any of these mechanisms applies, reject the skip" in out + assert "exposing the state through a getter" in out + assert "missing harness support, not CVL inexpressibility" not in out + def test_criteria7_fallback_labels_harness_skips(self): # harness_augmentation omitted (default false): Criteria 7 must align with the # system prompt's fallback — harness-shaped skips get the "missing harness From b439d330ba090503fc15e1741c4b4f73643ad04f Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sat, 4 Jul 2026 02:46:29 +0300 Subject: [PATCH 6/7] Replace the regex skip gate with a structured reason_category enum MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- composer/spec/cvl_generation.py | 114 ++++++++------ composer/spec/feedback.py | 7 +- composer/templates/property_judge_prompt.j2 | 5 + tests/test_cvl_skips.py | 162 +++++++++++++------- 4 files changed, 177 insertions(+), 111 deletions(-) diff --git a/composer/spec/cvl_generation.py b/composer/spec/cvl_generation.py index d7e441b..600e924 100644 --- a/composer/spec/cvl_generation.py +++ b/composer/spec/cvl_generation.py @@ -7,7 +7,6 @@ """ import hashlib -import re from dataclasses import dataclass from typing import Annotated, Callable, Literal, NotRequired, override, Awaitable, Any, Protocol from typing_extensions import TypedDict @@ -47,6 +46,21 @@ def feedback(self) -> str: ... # Feedback types # --------------------------------------------------------------------------- +# The author's self-classification of a skip reason. ``storage_access`` names the one +# category that is a capability gap CVL can bridge (keccak slot constants, storage hooks, +# harness getters, ghost mirroring) rather than an expressiveness limit, so it is the only +# category the record_skip gate treats specially. The judge polices classification honesty +# (Criteria 7 in property_judge_prompt.j2 audits access-shaped reasons categorized +# otherwise as storage_access), so the enum is a declaration, not a trusted fact. +ReasonCategory = Literal[ + "storage_access", # the state exists on-chain but is hard to *read* from CVL + "hash_collision", # requires reasoning about collisions/preimages/inversion of a hash + "prover_limitation", # a documented prover limit (e.g. quantifying over unbounded arrays) + "environment", # depends on off-chain/environment behavior CVL cannot model + "other", +] + + class SkippedProperty(BaseModel): """A property the agent explicitly decided not to formalize.""" property_title: str = Field(description="The unique snake_case title of the property from the batch listing") @@ -56,6 +70,11 @@ class SkippedProperty(BaseModel): default_factory=list, description="The alternative mechanisms the author considered before skipping, and why each does not work", ) + # Defaulted for back-compat with cached instances that predate the field. + reason_category: ReasonCategory = Field( + default="other", + description="The author's self-classification of the skip reason", + ) class PropertyRuleMapping(BaseModel): @@ -158,6 +177,12 @@ def _compute_digest(curr_spec: str, skipped: list[SkippedProperty]) -> str: digester.update(curr_spec.encode()) for s in skipped: digester.update(f"{s.property_title}:{s.reason}".encode()) + # The judge audits reason_category as part of the skip's justification + # (feedback.py surfaces it), so changing it must stale the validation stamp. + # The default "other" contributes nothing, so digests of cached pre-field + # skips (which deserialize with the default) keep their legacy value. + if s.reason_category != "other": + digester.update(f"|cat:{s.reason_category}".encode()) # The judge audits alternatives_considered as part of the skip's justification # (feedback.py surfaces them), so changing them must stale the validation stamp. # An empty list contributes nothing, so digests of cached pre-field skips (which @@ -317,40 +342,14 @@ async def run(self) -> Command: ) return tool_state_update(self.tool_call_id, msg) -# Skip gate: reasons of the shape "the state is hard to *access*" name a capability gap that -# CVL can bridge, not an expressiveness limit. Each entry pairs a trigger pattern (matched -# against the skip reason) with the capability that must be addressed in -# ``alternatives_considered`` and the evidence pattern used to detect that the capability was -# actually discussed. A skip whose reason fires a trigger is rejected until every triggered -# capability is addressed. -# -# A bare "keccak" also appears in the one hash-related skip that stays legitimate — reasoning -# 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]]] = [ - ( - re.compile(rf"{_KECCAK_SLOT}|storage slot|unstructured", re.IGNORECASE), - "a precomputed keccak storage-slot constant (keccak256 is a built-in CVL function)", - re.compile(r"keccak|slot", re.IGNORECASE), - ), - ( - re.compile(rf"{_KECCAK_SLOT}|storage slot|unstructured|cannot (be )?(access|observ)", re.IGNORECASE), - "Sload/Sstore storage hooks on the slot/path in question", - re.compile(r"sload|sstore|hook", re.IGNORECASE), - ), - ( - re.compile(r"no (public )?getter|cannot (be )?(access|observ)|unstructured", re.IGNORECASE), - "a harness getter/helper or direct storage access (currentContract.)", - re.compile(r"harness|getter|helper|currentContract|direct storage", re.IGNORECASE), - ), - ( - re.compile(r"cannot (be )?(access|observ)", re.IGNORECASE), - "ghost state mirroring the value via hooks or summaries", - re.compile(r"ghost", re.IGNORECASE), - ), -] - +# Skip gate: the author self-classifies each skip via ``reason_category``. A +# ``storage_access`` skip ("the state is hard to *read*") names a capability gap that CVL +# can bridge — precomputed keccak slot constants, Sload/Sstore hooks, harness getters, +# ghost mirroring — not an expressiveness limit, so it cannot be recorded until +# ``alternatives_considered`` is non-empty. The gate is purely structural (enum value + +# non-empty field check); the judge audits the *substance* of the alternatives and +# polices classification honesty (an access-shaped reason categorized otherwise is +# audited as storage_access — see Criteria 7 in property_judge_prompt.j2). @tool_display( lambda p: f"Skipping property `{p.get('property_title', '?')}`", @@ -359,8 +358,8 @@ async def run(self) -> Command: class _RecordSkipSchema(WithInjectedState[CVLGenerationState], WithInjectedId, WithImplementation[Command]): """ Declare that you are skipping a property from the batch. - You must provide the property's title, a justification, and the alternative - mechanisms you considered before skipping. + You must provide the property's title, a justification, a category classifying + the justification, and the alternative mechanisms you considered before skipping. The feedback judge will evaluate whether your justification is valid. Only use this after genuinely attempting to formalize the property. """ @@ -370,10 +369,24 @@ class _RecordSkipSchema(WithInjectedState[CVLGenerationState], WithInjectedId, W reason: str = Field( description="Justification for why this property cannot be formalized" ) + reason_category: ReasonCategory = Field( + description=( + "Classify the skip reason: `storage_access` — the state exists on-chain but is hard " + "to READ from CVL (private/internal fields, unstructured or keccak-addressed storage, " + "no public getter); `hash_collision` — the property requires reasoning about " + "collisions, preimages, or inversion of a hash function itself; `prover_limitation` — " + "a documented prover limit (e.g. quantifying over arbitrary-length arrays); " + "`environment` — depends on off-chain/environment behavior that cannot be modeled; " + "`other` — anything else. The feedback judge audits this classification: an " + "access-shaped reason categorized as anything but `storage_access` will be re-audited " + "as `storage_access`." + ) + ) alternatives_considered: list[str] = Field( description=( "The alternative CVL/verification mechanisms you considered before skipping, and why " - "each does not work for this property. Where applicable you MUST address: precomputed " + "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 " "storage hooks, harness getters/helpers, and ghost mirroring of contract state." ) @@ -392,25 +405,24 @@ def run(self) -> Command: self.tool_call_id, "A non-empty justification is required when skipping a property.", ) - missing = [ - capability - for trigger, capability, evidence in _SKIP_GATE_CHECKS - if trigger.search(self.reason) - and not any(evidence.search(alt) for alt in self.alternatives_considered) - ] - if missing: + if self.reason_category == "storage_access" and not any( + alt.strip() for alt in self.alternatives_considered + ): return tool_state_update( self.tool_call_id, - "Skip REJECTED: the stated reason suggests the state is merely hard to *access*, " - "which is a capability gap CVL can bridge, not an expressiveness limit. Before " - "this skip can be recorded, `alternatives_considered` must address: " - + "; ".join(missing) - + ". Either attempt the applicable mechanism, or explain in " - "`alternatives_considered` why it does not apply to this property.", + "Skip REJECTED: a `storage_access` skip names a capability gap CVL can bridge, " + "not an expressiveness limit. Before this skip can be recorded, " + "`alternatives_considered` must address the applicable mechanisms among: a " + "precomputed keccak storage-slot constant (keccak256 is a built-in CVL function); " + "Sload/Sstore storage hooks on the slot/path in question; a harness getter/helper " + "or direct storage access (currentContract.); ghost state mirroring the " + "value via hooks or summaries. Either attempt the applicable mechanism, or explain " + "in `alternatives_considered` why it does not apply to this property.", ) skip = SkippedProperty( property_title=self.property_title, reason=self.reason, + reason_category=self.reason_category, alternatives_considered=self.alternatives_considered, ) return tool_state_update( diff --git a/composer/spec/feedback.py b/composer/spec/feedback.py index 445a37b..1d045b3 100644 --- a/composer/spec/feedback.py +++ b/composer/spec/feedback.py @@ -129,7 +129,12 @@ async def the_tool( if skipped: input_parts.append("The following properties were explicitly skipped by the author:") for s in skipped: - input_parts.append(f" Property {s.property_title}: {s.reason}") + # The author's self-classification is part of the skip's justification: + # Criteria 7 tells the judge to audit access-shaped reasons categorized + # as anything but storage_access as storage_access anyway. + input_parts.append( + f" Property {s.property_title} (reason category: {s.reason_category}): {s.reason}" + ) # The alternatives the author claims to have ruled out are part of the skip's # justification: surface them so the judge can audit their substance. for alt in s.alternatives_considered: diff --git a/composer/templates/property_judge_prompt.j2 b/composer/templates/property_judge_prompt.j2 index 63f7285..f51096f 100644 --- a/composer/templates/property_judge_prompt.j2 +++ b/composer/templates/property_judge_prompt.j2 @@ -175,6 +175,11 @@ Verify that the specification covers all {{ properties | length }} listed proper and EIP-1967 slots are compile-time constants) combined with an `Sload`/`Sstore` hook on that slot; (b) a harness getter or direct storage access (e.g., `currentContract.`); (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 + a getter — but categorized as anything other than `storage_access`, audit it as `storage_access` + anyway, running the full mechanism checklist above; the category is the author's claim, not a fact. {# harness_augmentation mirrors the identically-named variable in property_judge_system_prompt.j2 and must be bound consistently with it: only pipelines that can (re)generate main-contract augmentation harnesses may instruct the judge to reject harness-shaped skips; everywhere else (default(false)) diff --git a/tests/test_cvl_skips.py b/tests/test_cvl_skips.py index 1c68ae4..510904c 100644 --- a/tests/test_cvl_skips.py +++ b/tests/test_cvl_skips.py @@ -44,13 +44,20 @@ _RESULT_NAME = "result" _PUT_CVL = "put_cvl" -def _skip(property_title: str, reason: str, alternatives: list[str] | None = None) -> ToolCallDict: - # alternatives_considered is a required tool field; most tests use reasons that don't - # trigger the skip gate, so an empty list suffices unless a test exercises the gate. +def _skip( + property_title: str, + reason: str, + alternatives: list[str] | None = None, + category: str = "other", +) -> ToolCallDict: + # reason_category and alternatives_considered are required tool fields; the gate only + # fires for category "storage_access", so the "other" default plus an empty list + # suffices unless a test exercises the gate. return tool_call_raw( name=_RECORD_SKIP_NAME, property_title=property_title, reason=reason, + reason_category=category, alternatives_considered=alternatives if alternatives is not None else [], ) @@ -242,7 +249,7 @@ async def test_invalid_skip_reason(self): # ========================================================================= -# Skip gate: access-shaped reasons require alternatives_considered coverage +# Skip gate: storage_access skips require non-empty alternatives_considered # ========================================================================= class TestSkipGate: @@ -252,89 +259,84 @@ def gate_mapper(self, st: CVLTestState) -> tuple[str, list[SkippedProperty]]: st["skipped"], ) - async def test_keccak_reason_without_alternatives_rejected(self): + async def test_storage_access_without_alternatives_rejected(self): (msg, skipped) = await scenario(1).turn( - _skip("p0", "the balance lives in a keccak-derived storage slot with no way to read it") + _skip( + "p0", + "the balance lives in a keccak-derived storage slot with no way to read it", + category="storage_access", + ) ).map(self.gate_mapper).run() assert skipped == [] assert msg.startswith("Skip REJECTED:") assert "keccak storage-slot constant" in msg assert "Sload/Sstore storage hooks" in msg + assert "harness getter/helper" in msg + assert "ghost state mirroring" in msg - async def test_keccak_reason_with_alternatives_accepted(self): + async def test_storage_access_with_blank_alternatives_rejected(self): + # Whitespace-only entries must not satisfy the non-empty requirement. (msg, skipped) = await scenario(1).turn( _skip( "p0", - "the balance lives in a keccak-derived storage slot", - alternatives=[ - "precomputed the keccak slot constant, but the slot value depends on a runtime salt", - "an Sstore hook on the slot cannot fire because writes go through delegatecall", - ], + "the accumulator is private with no getter", + alternatives=[" ", ""], + category="storage_access", ) ).map(self.gate_mapper).run() - assert msg.startswith("Recorded skip") - assert len(skipped) == 1 and skipped[0].property_title == "p0" - - async def test_trigger_matching_is_case_insensitive(self): - (msg, skipped) = await scenario(1).turn( - _skip("p0", "state is in Unstructured Storage and CANNOT ACCESS it from CVL") - ).map(self.gate_mapper).run() assert skipped == [] assert msg.startswith("Skip REJECTED:") - async def test_no_getter_reason_requires_harness_capability(self): - (msg, skipped) = await scenario(1).turn( - _skip("p0", "there is no public getter for the internal accumulator") - ).map(self.gate_mapper).run() - assert skipped == [] - assert "harness getter/helper" in msg - - async def test_cannot_observe_reason_requires_ghost_capability(self): + async def test_storage_access_with_alternatives_accepted(self): (msg, skipped) = await scenario(1).turn( _skip( "p0", - "we cannot observe the intermediate value", + "the balance lives in a keccak-derived storage slot", alternatives=[ - "Sload/Sstore hooks don't fire on memory values", - "a harness getter cannot expose transient memory", + "precomputed the keccak slot constant, but the slot value depends on a runtime salt", + "an Sstore hook on the slot cannot fire because writes go through delegatecall", ], + category="storage_access", ) ).map(self.gate_mapper).run() - assert skipped == [] - assert "ghost state mirroring" in msg - - async def test_passive_access_reason_triggers_gate(self): - # Passive phrasing ("cannot be accessed") must fire the same access-shaped - # triggers as the active form ("cannot access"). - (msg, skipped) = await scenario(1).turn( - _skip("p0", "the accumulated fee cannot be accessed from outside the contract") - ).map(self.gate_mapper).run() - assert skipped == [] - assert msg.startswith("Skip REJECTED:") - assert "ghost state mirroring" in msg + assert msg.startswith("Recorded skip") + assert len(skipped) == 1 and skipped[0].property_title == "p0" - async def test_passive_observe_reason_triggers_gate(self): + async def test_hash_collision_passes_with_empty_alternatives(self): + # Collision/inversion/preimage reasoning is the one keccak-related skip that stays + # legitimate; it is not access-shaped, so no alternatives are structurally required + # (the judge still audits the classification's honesty). (msg, skipped) = await scenario(1).turn( - _skip("p0", "the pending reward cannot be observed by any external caller") + _skip( + "p0", + "requires reasoning about keccak collisions to forge a valid signature", + category="hash_collision", + ) ).map(self.gate_mapper).run() - assert skipped == [] - assert "harness getter/helper" in msg + assert msg.startswith("Recorded skip") + assert len(skipped) == 1 - async def test_unrelated_reason_passes_with_empty_alternatives(self): + @pytest.mark.parametrize("category", ["prover_limitation", "environment", "other"]) + async def test_non_access_categories_pass_with_empty_alternatives(self, category: str): (msg, skipped) = await scenario(1).turn( - _skip("p0", "requires quantifying over arbitrary-length arrays") + _skip("p0", "requires quantifying over arbitrary-length arrays", category=category) ).map(self.gate_mapper).run() assert msg.startswith("Recorded skip") assert len(skipped) == 1 - async def test_hash_collision_reason_passes_gate(self): - # Collision/inversion/preimage reasoning is the one keccak-related skip that stays - # legitimate: a bare "keccak" away from slot/storage must not fire the access gate. + async def test_category_is_recorded_on_the_skip(self): + # The judge audits reason_category, so the recorded SkippedProperty must carry it + # (not just gate on it and drop it). (msg, skipped) = await scenario(1).turn( - _skip("p0", "requires reasoning about keccak collisions to forge a valid signature") + _skip( + "p0", + "the balance lives in a keccak-derived storage slot", + alternatives=["the slot constant depends on a runtime salt"], + category="storage_access", + ) ).map(self.gate_mapper).run() assert msg.startswith("Recorded skip") - assert len(skipped) == 1 + assert skipped[0].reason_category == "storage_access" async def test_alternatives_are_recorded_on_the_skip(self): # The judge audits alternatives_considered, so the recorded SkippedProperty must @@ -344,16 +346,22 @@ async def test_alternatives_are_recorded_on_the_skip(self): "an Sstore hook cannot fire because writes go through delegatecall", ] (msg, skipped) = await scenario(1).turn( - _skip("p0", "the balance lives in a keccak-derived storage slot", alternatives=alts) + _skip( + "p0", + "the balance lives in a keccak-derived storage slot", + alternatives=alts, + category="storage_access", + ) ).map(self.gate_mapper).run() assert msg.startswith("Recorded skip") assert skipped[0].alternatives_considered == alts - async def test_skipped_property_backcompat_without_alternatives(self): - # Cached SkippedProperty instances predate alternatives_considered; deserialization - # must default it rather than fail validation. + async def test_skipped_property_backcompat_without_new_fields(self): + # Cached SkippedProperty instances predate alternatives_considered and + # reason_category; deserialization must default them rather than fail validation. s = SkippedProperty.model_validate({"property_title": "p0", "reason": "too hard"}) assert s.alternatives_considered == [] + assert s.reason_category == "other" # ========================================================================= @@ -385,6 +393,31 @@ def test_empty_alternatives_preserve_legacy_digest(self): assert _compute_digest("spec", [legacy]) == _compute_digest("spec", [explicit]) +# ========================================================================= +# Digest coverage: reason_category is part of the skip's audited identity +# ========================================================================= + +class TestDigestCoversCategory: + def test_digest_changes_with_category(self): + a = SkippedProperty(property_title="p0", reason="r", reason_category="storage_access", + alternatives_considered=["tried ghost mirroring"]) + b = SkippedProperty(property_title="p0", reason="r", reason_category="hash_collision", + alternatives_considered=["tried ghost mirroring"]) + assert _compute_digest("spec", [a]) != _compute_digest("spec", [b]) + + def test_non_default_category_changes_digest(self): + default = SkippedProperty(property_title="p0", reason="r") + classified = SkippedProperty(property_title="p0", reason="r", reason_category="environment") + assert _compute_digest("spec", [default]) != _compute_digest("spec", [classified]) + + def test_default_category_preserves_legacy_digest(self): + # Cached pre-field skips deserialize with the default "other"; their digest must + # equal an explicitly-"other" one so cached validation stamps stay fresh. + legacy = SkippedProperty.model_validate({"property_title": "p0", "reason": "r"}) + explicit = SkippedProperty(property_title="p0", reason="r", reason_category="other") + assert _compute_digest("spec", [legacy]) == _compute_digest("spec", [explicit]) + + # ========================================================================= # Validation stamping + check_completion via graph # ========================================================================= @@ -465,12 +498,23 @@ async def test_changed_alternatives_no_result(self): _skip("p0", reason, alternatives=[ "the keccak slot constant depends on a runtime salt", "an Sstore hook cannot fire through delegatecall", - ]), + ], category="storage_access"), _feedback(), _skip("p0", reason, alternatives=[ "the slot constant is not computable at compile time here", "storage hooks do not fire for delegatecall writes", - ]), + ], category="storage_access"), + _result("I'm done") + ).map_run(is_result_rejection.check_reason(unsat_feedback_message)) + + async def test_changed_category_no_result(self): + # Re-classifying a skip after validation must stale the stamp just like + # editing the reason does — the category is judge-audited. + reason = "requires reasoning about the hash function itself" + assert await scenario(1, curr_spec="whatever").turns( + _skip("p0", reason, category="hash_collision"), + _feedback(), + _skip("p0", reason, category="prover_limitation"), _result("I'm done") ).map_run(is_result_rejection.check_reason(unsat_feedback_message)) From b7cf58e861a4759fb78facda7e1ab7483493629e Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sat, 4 Jul 2026 02:47:19 +0300 Subject: [PATCH 7/7] Thread harness_augmentation once through property_feedback_judge 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 --- composer/spec/feedback.py | 35 +++++++++----- composer/templates/property_judge_prompt.j2 | 8 ++-- .../templates/property_judge_system_prompt.j2 | 6 ++- tests/test_template_render.py | 47 +++++++++++++++++++ 4 files changed, 79 insertions(+), 17 deletions(-) diff --git a/composer/spec/feedback.py b/composer/spec/feedback.py index 1d045b3..b449904 100644 --- a/composer/spec/feedback.py +++ b/composer/spec/feedback.py @@ -41,22 +41,11 @@ class FeedbackInherentParams(TypedDict): # ``existing`` — pre-existing codebase being verified as-is; target # has real immutable source. sort: Sort - # Mirrors JudgeSystemParams.harness_augmentation and must be bound consistently - # with it: it gates Criteria 7's "reject harness-shaped skips" directive so the - # judge only demands harness getters/wrappers in pipelines that can generate - # them. The template defaults it to false, so pipelines without harness - # augmentation may simply omit it. - harness_augmentation: NotRequired[bool] FeedbackTemplate = TypedTemplate[FeedbackInherentParams]("property_judge_prompt.j2") class JudgeSystemParams(TypedDict): sort: Sort - # Whether the pipeline can (re)generate main-contract augmentation harnesses. When true, - # the judge template's "demand a harness getter/wrapper instead of accepting the skip" - # wording is rendered; the template defaults it to false, so pipelines without harness - # augmentation may simply omit it. - harness_augmentation: NotRequired[bool] # Judge system prompt, shared between the natspec and source-mode flows. The fs # primitives are always documented; ``sort`` drives the rest (the template @@ -64,18 +53,37 @@ class JudgeSystemParams(TypedDict): # ``sort == "existing"``, the only mode that wires those tools). FeedbackSystemTemplate = TypedTemplate[JudgeSystemParams]("property_judge_system_prompt.j2") + +def _bind_harness_augmentation( + prompt: TemplateInstantiation, harness_augmentation: bool +) -> TemplateInstantiation: + """Inject the ``harness_augmentation`` flag into an already-instantiated template bind. + + Both judge templates gate their harness-skip policy on this variable; injecting it + from the single ``property_feedback_judge`` parameter into BOTH binds is what keeps + the system prompt and Criteria 7 in agreement. The templates' ``default(false)`` is + a render fail-safe only, never the mechanism that decides the value. + """ + return TemplateInstantiation( + prompt.template, + {**prompt.args, "harness_augmentation": harness_augmentation}, + ) + + def property_feedback_judge( ctx: WorkflowContext[CVLJudge], env: ServiceHost, prompt: InjectedTemplate[Properties] | TemplateInstantiation, props: list[PropertyFormulation], *, + harness_augmentation: bool = False, extra_inputs: list[str | dict] | Callable[[], list[str | dict]] | None = None, system_prompt: TemplateInstantiation | None = None, ) -> FeedbackToolContext: if system_prompt is None: system_prompt = FeedbackSystemTemplate.bind({"sort": env.sort}) + system_prompt = _bind_harness_augmentation(system_prompt, harness_augmentation) builder = env.builder_heavy().with_tools( env.all_tools @@ -99,7 +107,10 @@ def did_rough_draft_read(s: ST, _) -> str | None: mem = ctx.get_memory_tool() - final_prompt = prompt if isinstance(prompt, TemplateInstantiation) else prompt.inject({"properties": props}) + final_prompt = _bind_harness_augmentation( + prompt if isinstance(prompt, TemplateInstantiation) else prompt.inject({"properties": props}), + harness_augmentation, + ) workflow = bind_standard( builder, ST, validator=did_rough_draft_read diff --git a/composer/templates/property_judge_prompt.j2 b/composer/templates/property_judge_prompt.j2 index f51096f..1670e6e 100644 --- a/composer/templates/property_judge_prompt.j2 +++ b/composer/templates/property_judge_prompt.j2 @@ -180,9 +180,11 @@ Verify that the specification covers all {{ properties | length }} listed proper reason is access-shaped — state described as private, unstructured, keccak-addressed, or lacking a getter — but categorized as anything other than `storage_access`, audit it as `storage_access` anyway, running the full mechanism checklist above; the category is the author's claim, not a fact. -{# harness_augmentation mirrors the identically-named variable in property_judge_system_prompt.j2 and - must be bound consistently with it: only pipelines that can (re)generate main-contract augmentation - harnesses may instruct the judge to reject harness-shaped skips; everywhere else (default(false)) +{# harness_augmentation is injected by property_feedback_judge (composer/spec/feedback.py) into both + this template's bind and property_judge_system_prompt.j2's bind from one function parameter, so + the two templates always agree; default(false) is a render fail-safe only. Only pipelines that + can (re)generate main-contract augmentation harnesses may instruct the judge to reject + harness-shaped skips; everywhere else (the false default) such skips are accepted with the "missing harness support" label the system prompt mandates. Greenfield is checked first because harness pipelines (and the immutability rule the fallback compensates for) only exist for pre-existing source: the greenfield author shapes the stub's API diff --git a/composer/templates/property_judge_system_prompt.j2 b/composer/templates/property_judge_system_prompt.j2 index 2fefe4e..c431be5 100644 --- a/composer/templates/property_judge_system_prompt.j2 +++ b/composer/templates/property_judge_system_prompt.j2 @@ -31,8 +31,10 @@ and prove a property is to change the *protocol* source code, then skipping that Verification *harnesses* (contracts under `certora/harnesses/`) are NOT protocol code: they are verification infrastructure, existing precisely to expose state and behavior the protocol does not surface publicly. -{# harness_augmentation is set only by pipelines that can actually (re)generate main-contract - augmentation harnesses; default(false) keeps the demand-wording a no-op everywhere else. #} +{# harness_augmentation is injected by property_feedback_judge (composer/spec/feedback.py) into both + this template's bind and property_judge_prompt.j2's bind from one function parameter, so the two + templates always agree. It is set only by pipelines that can actually (re)generate main-contract + augmentation harnesses; default(false) keeps the demand-wording a no-op as a render fail-safe. #} {% if harness_augmentation | default(false) %} If a property is skipped only because state or behavior is not publicly exposed, do NOT accept the skip as "not expressible in CVL". Instead, demand a harness augmentation (an external view getter or a thin wrapper diff --git a/tests/test_template_render.py b/tests/test_template_render.py index 7ba89b1..cc9318a 100644 --- a/tests/test_template_render.py +++ b/tests/test_template_render.py @@ -8,6 +8,12 @@ import pytest from composer.templates.loader import load_jinja_template +from composer.spec.feedback import ( + FeedbackSystemTemplate, + FeedbackTemplate, + Properties, + _bind_harness_augmentation, +) from composer.spec.prop import PropertyFormulation @@ -119,6 +125,47 @@ def test_criteria7_augmentation_rejects_harness_skips(self): assert "does NOT make a skip valid under this rule" in out assert "missing harness support, not CVL inexpressibility" not in out + @pytest.mark.parametrize("flag", [True, False]) + def test_judge_templates_agree_on_harness_wording(self, flag: bool): + # The system prompt and Criteria 7 encode the same harness-skip policy; for a + # given flag value the harness wording must be present/absent in BOTH templates + # together, or the judge receives self-contradictory instructions. + sys_out = load_jinja_template( + "property_judge_system_prompt.j2", sort="existing", harness_augmentation=flag + ) + task_out = load_jinja_template( + "property_judge_prompt.j2", + properties=_props(), + sort="existing", + context=None, + harness_augmentation=flag, + ) + assert ("demand a harness augmentation" in sys_out) == flag + assert ("If any of these mechanisms applies, reject the skip" in task_out) == flag + assert ("missing harness support, not CVL inexpressibility" in sys_out) == (not flag) + assert ("missing harness support, not CVL inexpressibility" in task_out) == (not flag) + + @pytest.mark.parametrize("flag", [True, False]) + def test_property_feedback_judge_injection_binds_both_templates(self, flag: bool): + # property_feedback_judge threads its harness_augmentation parameter into both + # binds via _bind_harness_augmentation; render both through the same helper and + # assert the resulting prompts agree for both flag values. + task = _bind_harness_augmentation( + FeedbackTemplate.bind({"context": None, "sort": "existing"}) + .depends(Properties) + .inject({"properties": _props()}), + flag, + ) + sys_p = _bind_harness_augmentation( + FeedbackSystemTemplate.bind({"sort": "existing"}), flag + ) + task_out = task.render_to(load_jinja_template) + sys_out = sys_p.render_to(load_jinja_template) + assert ("demand a harness augmentation" in sys_out) == flag + assert ("If any of these mechanisms applies, reject the skip" in task_out) == flag + assert ("missing harness support, not CVL inexpressibility" in sys_out) == (not flag) + assert ("missing harness support, not CVL inexpressibility" in task_out) == (not flag) + def test_criteria7_explicit_false_matches_omitted(self): omitted = load_jinja_template( "property_judge_prompt.j2", properties=_props(), sort="existing", context=None