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

[shellygr]

Some more guidance on property inference.

---

Part 5 of 6 (spec-quality series). Generated specs were ~80% unit-style rules; human specs concentrate on accounting invariants, multi-call sequences, and state-transition properties, and never assume state with bare requires.

What

• cvl_guidelines.j2 (read by author AND judge): new guideline 24 — a bare require over contract state is a spec smell; default is invariant + requireInvariant, bare requires only with a justification comment. Two carve-outs: 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 — a comment alone is insufficient). Guideline 23 amended with a ghost-counter carve-out (information never stored in contract state); guideline 20 now names persistent counter ghosts and expression summaries on external-dependency calls as legitimate for that same class.
• property_analysis_prompt.j2: 6-lens coverage checklist (unit / valid-state / variable-transition / state-transition / multi-call / risk) — explicitly a brainstorming discipline, not a quota; swept lenses recorded in reasoning. No PropertyType schema change (caches survive).
• property_generation_prompt.j2: the property_rules mapping instruction now requires supporting invariants and companion witness rules to be listed under the property they support — rules unreferenced by any property are silently dropped from the final report.
• cvl_additions.j2 (author-only): three <advice> entries — storage s = lastStorage / f(e,args) at s snapshot idiom (additivity/round-trip), satisfy-witness companion rules for implication antecedents (mapped in property_rules under the parent property), ghost counters via expression summaries (with persistent-ghost note and the caveats that summaries replace the callee and never apply to direct CVL calls).

Design revisions after architecture review

• Guideline 24 carve-out for capacity/overflow-avoidance bounds — they keep the solver tractable rather than model behavior, so no invariant attempt is expected.
• Guideline 24 preserved-block policy now defers to the stricter judge standard (Criteria 4), removing the internal conflict where a comment sufficed for the author but not the judge.
• Companion satisfy-witness rules and supporting invariants must be mapped in property_rules under their parent property — orphan rules are dropped from the report (confirmed by reviewers).
• Ghost-counter/persistent-ghost defense made judge-visible via guideline 20, so the judge shares the vocabulary the author advice uses.

🤖 Generated with Claude Code

[shellygr]

remove this test. does nothing

[jtoman]

my 2 c.

[jtoman]

we discussed this on zoom, but we already have guidance for both the judge and author to not use require as a "make the rule pass" magic. Repeating it a third time will not fix the problem imo. The instructions you provide here are almost verbatim in the author prompt. It would be useful if we could find the run where this happened and see what reasoning/thinking tricks the agent used to talk itself out of the rules it already knew about, rather than just repeating the rule one more time and hoping that one makes it stick.