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

composer/templates/cvl_additions.j2

@@ -25,4 +25,29 @@ where necessary.
 <advice>
 Reverting behavior is reasoned about by using the `@withrevert` annotation and examining the value of the `lastReverted` flag.
 </advice>
+<advice>
+Multi-call properties can compare executions from a common starting state using storage snapshots: `storage init = lastStorage;`
+snapshots the current blockchain state (and non-persistent ghosts), and `f(e, args) at init;` runs `f` starting from that snapshot
+instead of the current state. The standard additivity idiom: run `g(x); g(y);` sequentially from a snapshot, then run `g(x + y) at init;`
+from the *same* snapshot, and compare the resulting end states (e.g., final balances or shares).
+</advice>
+<advice>
+For implication-shaped assertions (`assert A => B;`), consider a companion witness rule containing `satisfy A;`. A `satisfy`
+statement checks that at least one execution reaches it with the condition true — a single witness execution suffices. This
+guards against vacuously-true implications whose antecedent `A` can never actually hold. List the witness rule in the
+`property_rules` mapping under the same property as the implication rule it guards, so it is retained in the final report.
+</advice>
+<advice>
+Information that is never stored in contract state — such as how many times a function was called, or the cumulative amount
+transferred across calls — can be tracked with a ghost updated through an expression summary. For example:
+`function _.deposit() external => countDeposit() expect void;` where `countDeposit` is a CVL function that increments a ghost
+counter. Two caveats: an expression summary *replaces* the summarized function's implementation (so only use it on calls whose
+real effects are not otherwise under test, e.g. calls from contract code to external dependencies), and summaries never apply
+to functions invoked directly from CVL — a ghost counting the verified contract's own entry points called from a rule stays 0.
+Mark such counter ghosts `persistent` when they must survive reverted calls or `at`-snapshot restores (non-persistent ghosts
+are rolled back along with the blockchain state, which would silently reset the count); this is compatible with the
+persistent-ghost guideline, since a call counter does not mirror contract state.
+This does not conflict with the direct-storage-access guideline: that guideline is about mirroring values already
+present in contract storage, whereas this idiom tracks information never stored in contract state.
+</advice>
 </cvl_advice>

composer/templates/cvl_guidelines.j2

@@ -35,11 +35,19 @@
     19. CVL automatically promotes operands of comparison/arithmetic operations to `mathint`. Explicit `to_mathint` casts are
         rarely need.
     20. `persistent` ghosts should be used sparingly, and should *never* be used on ghosts which are intended to model/mirror
-        contract state.
+        contract state. However, ghosts tracking information never stored in contract state (e.g., call counters, cumulative transfer
+        amounts) are a legitimate use of `persistent`, and of expression summaries on calls to external dependencies.
     21. When referring to meaningful numerical constants in a specification (e.g., max fee percentage, asset expiry period, etc.) prefer using the `definition` feature of CVL
         to provide meaningful names to the constants.
     22. Instead of `forall $type i` in a invariant, invariant parameters should be used instead. That is, instead of `invariant foo() forall uint i.logical_predicate(i)` simply write
         `invariant foo(uint i) logical_predicate(i)`. The parameters of an invariant are implicitly universally quantified.
     23. Direct storage access should be used instead of mirroring contract state in ghosts via hooks. The only reason to use hooks and ghosts to reason about storage state is
-        if the ghost state is used for anything other than simply reading the values.
+        if the ghost state is used for anything other than simply reading the values. Hooks and ghosts are also appropriate when the information of interest is not stored in
+        contract state at all (e.g., counting how many times a function is called, or summing the amounts transferred across a sequence of calls).
+    24. A bare `require` that constrains contract state inside a rule or `preserved` block is a spec smell: the assumption may not actually hold in reachable states, silently
+        weakening the proof. The default discipline is to state the assumption as an `invariant`, prove it, and assume it via `requireInvariant`. Bare requires over contract
+        state are acceptable only when accompanied by a comment referencing a justification or a documented trust assumption. Exception: capacity/overflow-avoidance bounds on
+        supplies, balances, or timestamps (e.g. `require totalSupply() <= 2^128`) exist to keep the solver tractable, not to model contract behavior — they are a recognized
+        documented-trust-assumption class; a comment naming the bound's purpose suffices, and no invariant attempt is expected because such bounds are typically not preserved
+        by the contract. In `preserved` blocks the stricter standard applies — `requireInvariant` or verifiable outside evidence; a comment alone is insufficient.
 </cvl_guidelines>

composer/templates/property_analysis_prompt.j2

@@ -78,6 +78,19 @@ Security properties fall into one of three categories:
     Bad example: "The protocol could be hacked" (overly broad)
     Bad example: "The underlying EVM consensus layer could be compromised allowing attackers to set arbitrary storage states" (implausible)
 
+To achieve broad coverage, sweep the component through the following six lenses while brainstorming:
+1. Unit behavior: the effect of a single function in isolation, including its *complete* revert conditions (when it must revert, and when it must NOT revert).
+2. Valid state: representational invariants that hold in every reachable state.
+3. Variable transition: how an individual variable may change — who may change it, when, and how (e.g., monotonicity: a counter only increases; a fee only changes via an admin setter).
+4. State transition: legality of transitions between modes/phases of the contract lifecycle (e.g., paused/unpaused, uninitialized/initialized, auction open/closed) — which transitions are allowed and who may trigger them.
+5. Multi-call / high-level: properties spanning a *sequence* of calls, e.g., round-trips (deposit then withdraw yields no more than deposited), no-free-profit, additivity of split vs. batched operations (two calls with x and y vs. one call with x + y).
+6. Risk / attack: adversarial scenarios detrimental to the protocol.
+
+Every property you keep must still be reported under one of the three categories above (lenses 2 and 6 map directly to
+categories 1 and 3; the rest usually land in category 2). The lenses are a brainstorming discipline, NOT a quota: it is
+expected and normal for several lenses to yield nothing for a given component, and the standing rule against padding
+with low-value properties applies in full force.
+
 {{ backend_guidance }}
 
 Note: Safety properties can (and should) include properties describing the intended, normal behavior of the smart contract. In other words, the properties
@@ -95,7 +108,8 @@ Review your rough draft. For each property/invariant in your rough draft, make s
 attention for properties/invariants explicitly described as being uninteresting or impossible to verify in the downstream verification tool.
 
 ## Step 4
-Output the results of your analysis using the result tool.
+Output the results of your analysis using the result tool. In the reasoning you record, note which of the six coverage
+lenses you swept and which of them yielded nothing for this component.
 </task>
 
 <guidance>

composer/templates/property_generation_prompt.j2

@@ -119,7 +119,8 @@ The `result` tool *also* requires a `property_rules` mapping: for every property
 its unique snake_case title from the batch listing above), list the name(s) of the rule(s)/invariant(s) in your
 spec that verify it. Every non-skipped property must appear in this mapping with at least one rule; skipped
 properties must NOT appear. The result tool will be rejected if this mapping is incomplete or references a
-skipped or unknown property title.
+skipped or unknown property title. Supporting invariants and companion witness rules must also be listed under
+the property they support: rules not referenced by any property are silently dropped from the final report.
 
 To clarify: for your result to be accepted, all verification results from the prover must either be
 VERIFIED *or* that rule must be explicitly marked as "expected to fail" using the `expect_rule_failure` tool.

tests/test_template_render.py

@@ -0,0 +1,94 @@
+"""Render smoke tests for prompt templates.
+
+These templates are plain-jinja prompt fragments consumed by the property analysis /
+generation / judge agents. The tests render them with minimal stand-in objects (jinja
+only does attribute lookups, so `SimpleNamespace` suffices) and assert the load-bearing
+content is present — a missing template variable or a broken include fails fast here
+instead of mid-agent-run.
+"""
+from types import SimpleNamespace
+
+from composer.templates.loader import load_jinja_template
+
+
+def test_cvl_guidelines_render():
+    out = load_jinja_template("cvl_guidelines.j2")
+    # Guideline 24: requireInvariant discipline over bare state requires.
+    assert "requireInvariant" in out
+    assert "spec smell" in out
+    # Guideline 24 carve-out: solver-capacity bounds need no invariant attempt.
+    assert "keep the solver tractable" in out
+    # Guideline 24 defers preserved blocks to the stricter (judge Criteria 4) standard.
+    assert "stricter standard" in out
+    # Guideline 20 carve-out: persistent counter ghosts are legitimate (judge-visible
+    # counterpart of the ghost-counter advice in cvl_additions.j2).
+    assert "never stored in contract state" in out
+    # Guideline 23 carve-out: hooks/ghosts for information never stored in contract state.
+    assert "not stored in" in out
+    assert out.strip().endswith("</cvl_guidelines>")
+
+
+def test_cvl_additions_render():
+    out = load_jinja_template("cvl_additions.j2")
+    # Storage snapshot / additivity idiom.
+    assert "lastStorage" in out
+    assert "at init" in out
+    # satisfy-witness companion rules, mapped under their parent property.
+    assert "satisfy" in out
+    assert "property_rules" in out
+    # Ghost counters via expression summaries.
+    assert "countDeposit() expect void" in out
+    assert out.strip().endswith("</cvl_advice>")
+
+
+def _fake_component_context() -> SimpleNamespace:
+    """Minimal stand-in for ContractComponentInstance as accessed by the template."""
+    contract = SimpleNamespace(name="Vault", solidity_identifier="Vault")
+    component = SimpleNamespace(
+        name="Deposits",
+        description="Handles user deposits",
+        requirements=["Users receive shares proportional to deposits"],
+        interactions=[],
+    )
+    app = SimpleNamespace(application_type="an ERC4626 vault")
+    return SimpleNamespace(component=component, contract=contract, app=app,
+                           ommer_contracts=[])
+
+
+def test_property_analysis_prompt_render():
+    out = load_jinja_template(
+        "property_analysis_prompt.j2",
+        context=_fake_component_context(),
+        backend_guidance="BACKEND_GUIDANCE_SENTINEL",
+        # A valid Sort value (see composer/spec/service_host.py) exercising the
+        # non-greenfield template branch.
+        sort="existing",
+        prior_properties=[],
+    )
+    # The context and backend guidance are threaded through.
+    assert "Deposits" in out
+    assert "BACKEND_GUIDANCE_SENTINEL" in out
+    # 6-lens coverage checklist, framed as brainstorming discipline, not a quota.
+    assert "Unit behavior" in out
+    assert "Variable transition" in out
+    assert "Multi-call / high-level" in out
+    assert "NOT a quota" in out
+    # Task steps ask for a record of swept lenses.
+    assert "which of the six coverage" in out
+
+
+def test_property_analysis_prompt_render_with_prior_rounds():
+    prior = [SimpleNamespace(
+        items=[SimpleNamespace(sort="invariant", title="solvency",
+                               description="assets cover shares")],
+        reasoning="looked at deposit accounting",
+    )]
+    out = load_jinja_template(
+        "property_analysis_prompt.j2",
+        context=_fake_component_context(),
+        backend_guidance="",
+        sort="existing",
+        prior_properties=prior,
+    )
+    assert "solvency" in out
+    assert "looked at deposit accounting" in out