From 54676e63984b0d4c68e9ff0de4ee66e6ca4c2ae6 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 3 Jul 2026 20:21:58 +0300 Subject: [PATCH 1/6] Property portfolio: requireInvariant discipline, 6-lens checklist, technique advice MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - cvl_guidelines.j2: guideline 24 (bare state requires are a spec smell; default to invariant + requireInvariant, justify exceptions in a comment); guideline 23 carve-out for hooks/ghosts tracking information never stored in contract state. - property_analysis_prompt.j2: 6-lens coverage checklist (unit / valid-state / variable-transition / state-transition / multi-call / risk) after the 3-category block, explicitly a brainstorming discipline, not a quota; task steps ask the agent to record swept lenses in its reasoning. No PropertyType schema change. - cvl_additions.j2: three author-only advice entries — lastStorage/at storage snapshots with the additivity idiom, satisfy-witness companion rules for implication-shaped assertions, ghost counters via expression summaries. - tests/test_template_render.py: render smoke tests for the three templates. Co-Authored-By: Claude Fable 5 --- composer/templates/cvl_additions.j2 | 18 ++++ composer/templates/cvl_guidelines.j2 | 6 +- .../templates/property_analysis_prompt.j2 | 16 +++- tests/test_template_render.py | 84 +++++++++++++++++++ 4 files changed, 122 insertions(+), 2 deletions(-) create mode 100644 tests/test_template_render.py diff --git a/composer/templates/cvl_additions.j2 b/composer/templates/cvl_additions.j2 index c54edb6..a0c052b 100644 --- a/composer/templates/cvl_additions.j2 +++ b/composer/templates/cvl_additions.j2 @@ -25,4 +25,22 @@ where necessary. Reverting behavior is reasoned about by using the `@withrevert` annotation and examining the value of the `lastReverted` flag. + +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). + + +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. + + +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. 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. + \ No newline at end of file diff --git a/composer/templates/cvl_guidelines.j2 b/composer/templates/cvl_guidelines.j2 index a7a12df..6a3f16f 100644 --- a/composer/templates/cvl_guidelines.j2 +++ b/composer/templates/cvl_guidelines.j2 @@ -41,5 +41,9 @@ 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. \ No newline at end of file diff --git a/composer/templates/property_analysis_prompt.j2 b/composer/templates/property_analysis_prompt.j2 index 88f264b..ce5fe96 100644 --- a/composer/templates/property_analysis_prompt.j2 +++ b/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. diff --git a/tests/test_template_render.py b/tests/test_template_render.py new file mode 100644 index 0000000..ef4f076 --- /dev/null +++ b/tests/test_template_render.py @@ -0,0 +1,84 @@ +"""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 23 carve-out: hooks/ghosts for information never stored in contract state. + assert "not stored in" in out + assert out.strip().endswith("") + + +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. + assert "satisfy" in out + # Ghost counters via expression summaries. + assert "countDeposit() expect void" in out + assert out.strip().endswith("") + + +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", + sort="source", + 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="source", + prior_properties=prior, + ) + assert "solvency" in out + assert "looked at deposit accounting" in out From e989a5e0ee2baf2037eb6a6813d7c56c4b52afe9 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 3 Jul 2026 20:26:34 +0300 Subject: [PATCH 2/6] Clarify expression-summary caveats in ghost-counter advice Expression summaries replace the callee's implementation and never apply to direct CVL invocations; the advice now says so, so agents only use the idiom for external-dependency calls. Co-Authored-By: Claude Fable 5 --- composer/templates/cvl_additions.j2 | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/composer/templates/cvl_additions.j2 b/composer/templates/cvl_additions.j2 index a0c052b..4afbbfe 100644 --- a/composer/templates/cvl_additions.j2 +++ b/composer/templates/cvl_additions.j2 @@ -40,7 +40,10 @@ guards against vacuously-true implications whose antecedent `A` can never actual 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. This does not conflict with the direct-storage-access guideline: that guideline is about mirroring values already +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. +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. \ No newline at end of file From 8ec7d12ef0cf5653a3d2a37a446675c9fd8729f6 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 3 Jul 2026 20:46:18 +0300 Subject: [PATCH 3/6] Use a valid Sort value in template render tests "source" is not a member of Sort (Literal["greenfield", "existing", "update"] in composer/spec/service_host.py); "existing" exercises the same non-greenfield template branch with a value production can pass. Co-Authored-By: Claude Fable 5 --- tests/test_template_render.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/tests/test_template_render.py b/tests/test_template_render.py index ef4f076..365e31e 100644 --- a/tests/test_template_render.py +++ b/tests/test_template_render.py @@ -52,7 +52,9 @@ def test_property_analysis_prompt_render(): "property_analysis_prompt.j2", context=_fake_component_context(), backend_guidance="BACKEND_GUIDANCE_SENTINEL", - sort="source", + # 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. @@ -77,7 +79,7 @@ def test_property_analysis_prompt_render_with_prior_rounds(): "property_analysis_prompt.j2", context=_fake_component_context(), backend_guidance="", - sort="source", + sort="existing", prior_properties=prior, ) assert "solvency" in out From 146663fbc82779a9ae31b95eb3267afa9cacabd5 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 3 Jul 2026 21:08:23 +0300 Subject: [PATCH 4/6] Note persistent-ghost requirement in ghost-counter advice Non-persistent ghosts are rolled back by reverted calls and at-snapshot restores, so a counter combined with the lastStorage additivity idiom would silently reset. Marking counters persistent is consistent with the persistent-ghost guideline since they do not mirror contract state. Co-Authored-By: Claude Fable 5 --- composer/templates/cvl_additions.j2 | 3 +++ 1 file changed, 3 insertions(+) diff --git a/composer/templates/cvl_additions.j2 b/composer/templates/cvl_additions.j2 index 4afbbfe..f590569 100644 --- a/composer/templates/cvl_additions.j2 +++ b/composer/templates/cvl_additions.j2 @@ -43,6 +43,9 @@ transferred across calls — can be tracked with a ghost updated through an expr 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. From af8c61863135497b445b131fffc768bccb4df6d3 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sat, 4 Jul 2026 02:39:55 +0300 Subject: [PATCH 5/6] Carve out capacity bounds, map companion rules, judge-visible ghost defense Three template-level fixes from the architecture review of the property portfolio prompts: - Guideline 24: solver/capacity bounds (e.g. require totalSupply() <= 2^128) are a recognized documented-trust-assumption class needing no invariant attempt, and preserved blocks defer to the stricter judge standard (requireInvariant or verifiable outside evidence) instead of the comment-suffices rule, removing the conflict with judge Criteria 4. - Author instruction: companion satisfy-witness rules and supporting invariants must be listed in property_rules under their parent property, since rules unreferenced by any property are dropped from the report. - Guideline 20: persistent counter ghosts and expression summaries on external-dependency calls are legitimate for information never stored in contract state, so the judge shares the vocabulary the author advice uses. Co-Authored-By: Claude Fable 5 --- composer/templates/cvl_additions.j2 | 3 ++- composer/templates/cvl_guidelines.j2 | 8 ++++++-- composer/templates/property_generation_prompt.j2 | 3 ++- tests/test_template_render.py | 10 +++++++++- 4 files changed, 19 insertions(+), 5 deletions(-) diff --git a/composer/templates/cvl_additions.j2 b/composer/templates/cvl_additions.j2 index f590569..40cbe1e 100644 --- a/composer/templates/cvl_additions.j2 +++ b/composer/templates/cvl_additions.j2 @@ -34,7 +34,8 @@ from the *same* snapshot, and compare the resulting end states (e.g., final bala 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. +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. Information that is never stored in contract state — such as how many times a function was called, or the cumulative amount diff --git a/composer/templates/cvl_guidelines.j2 b/composer/templates/cvl_guidelines.j2 index 6a3f16f..bee22ee 100644 --- a/composer/templates/cvl_guidelines.j2 +++ b/composer/templates/cvl_guidelines.j2 @@ -35,7 +35,8 @@ 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 @@ -45,5 +46,8 @@ 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. + 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. \ No newline at end of file diff --git a/composer/templates/property_generation_prompt.j2 b/composer/templates/property_generation_prompt.j2 index d96585c..1cafe20 100644 --- a/composer/templates/property_generation_prompt.j2 +++ b/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. diff --git a/tests/test_template_render.py b/tests/test_template_render.py index 365e31e..976dba1 100644 --- a/tests/test_template_render.py +++ b/tests/test_template_render.py @@ -16,6 +16,13 @@ def test_cvl_guidelines_render(): # 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("") @@ -26,8 +33,9 @@ def test_cvl_additions_render(): # Storage snapshot / additivity idiom. assert "lastStorage" in out assert "at init" in out - # satisfy-witness companion rules. + # 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("") From e585b7d2a4f37b5b0d7a92a830eefd92fbfe95a8 Mon Sep 17 00:00:00 2001 From: shellygr Date: Sun, 5 Jul 2026 22:47:40 +0300 Subject: [PATCH 6/6] Apply suggestion from @shellygr --- composer/templates/cvl_additions.j2 | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/composer/templates/cvl_additions.j2 b/composer/templates/cvl_additions.j2 index 40cbe1e..4a2f81a 100644 --- a/composer/templates/cvl_additions.j2 +++ b/composer/templates/cvl_additions.j2 @@ -37,17 +37,4 @@ statement checks that at least one execution reaches it with the condition true 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. - -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. - \ No newline at end of file