diff --git a/composer/spec/cvl_generation.py b/composer/spec/cvl_generation.py index ba8da4b..600e924 100644 --- a/composer/spec/cvl_generation.py +++ b/composer/spec/cvl_generation.py @@ -46,10 +46,35 @@ 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") 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", + ) + # 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): @@ -152,6 +177,18 @@ 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 + # 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() @@ -305,6 +342,15 @@ async def run(self) -> Command: ) return tool_state_update(self.tool_call_id, msg) +# 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', '?')}`", suppress_ack("Skip result", ("Recorded skip",)), @@ -312,7 +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 and a justification. + 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. """ @@ -322,6 +369,28 @@ 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. 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." + ) + ) @override def run(self) -> Command: @@ -336,9 +405,25 @@ def run(self) -> Command: self.tool_call_id, "A non-empty justification is required when skipping a property.", ) + 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: 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( self.tool_call_id, diff --git a/composer/spec/feedback.py b/composer/spec/feedback.py index 5f64d7b..b449904 100644 --- a/composer/spec/feedback.py +++ b/composer/spec/feedback.py @@ -53,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 @@ -88,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 @@ -118,7 +140,16 @@ 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: + 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/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..1670e6e 100644 --- a/composer/templates/property_judge_prompt.j2 +++ b/composer/templates/property_judge_prompt.j2 @@ -168,14 +168,57 @@ 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. + + 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 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 + 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 + 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 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: + {% 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/composer/templates/property_judge_system_prompt.j2 b/composer/templates/property_judge_system_prompt.j2 index 31e187b..c431be5 100644 --- a/composer/templates/property_judge_system_prompt.j2 +++ b/composer/templates/property_judge_system_prompt.j2 @@ -20,12 +20,29 @@ {% 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 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 +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..510904c 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, @@ -43,8 +44,22 @@ _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, + 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 [], + ) def _unskip(property_title: str) -> ToolCallDict: return tool_call_raw(_UNSKIP_NAME, property_title=property_title) @@ -233,6 +248,176 @@ async def test_invalid_skip_reason(self): assert "A non-empty justification is" in msg +# ========================================================================= +# Skip gate: storage_access skips require non-empty alternatives_considered +# ========================================================================= + +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_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", + 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_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 accumulator is private with no getter", + alternatives=[" ", ""], + category="storage_access", + ) + ).map(self.gate_mapper).run() + assert skipped == [] + assert msg.startswith("Skip REJECTED:") + + async def test_storage_access_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", + ], + 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_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", + "requires reasoning about keccak collisions to forge a valid signature", + category="hash_collision", + ) + ).map(self.gate_mapper).run() + assert msg.startswith("Recorded skip") + assert len(skipped) == 1 + + @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", category=category) + ).map(self.gate_mapper).run() + assert msg.startswith("Recorded skip") + assert len(skipped) == 1 + + 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", + "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 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 + # 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, + 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_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" + + +# ========================================================================= +# 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]) + + +# ========================================================================= +# 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 # ========================================================================= @@ -305,6 +490,34 @@ 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", + ], 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)) + async def test_other_validation_key_unsat(self): assert await scenario(1, curr_spec="whatever", required=[FEEDBACK_VALIDATION_KEY, "something_else"]).turn( _feedback() diff --git a/tests/test_template_render.py b/tests/test_template_render.py new file mode 100644 index 0000000..cc9318a --- /dev/null +++ b/tests/test_template_render.py @@ -0,0 +1,194 @@ +""" +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.feedback import ( + FeedbackSystemTemplate, + FeedbackTemplate, + Properties, + _bind_harness_augmentation, +) +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 + + 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 + + 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 + # 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 + + @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 + ) + 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): + 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