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

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,14 +342,24 @@ 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",)),
 )
 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.<field>); 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,

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 "

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

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.
 
+<storage_access>
+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.
+</storage_access>
+
 ## Step 4
 
 Once all non-skipped properties have been approved by the feedback judge, AND all rules that are not expected

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.<field>`);
+  (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