fix: E501 messages render the precondition in call-site terms

CHANGELOG.md

@@ -12,6 +12,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
 - **[#727](https://github.com/aallan/vera/issues/727) — duplicate E501 diagnostics.**  A violating call site could be recorded once per translation pass: the primary body translation, the `@Nat`-subtraction walker's let-RHS environment rebuild, and the walker's operand discharge each re-translate the same call (a `@Nat`-subtraction operand in a `let` RHS recorded **three** identical E501s).  The SMT layer now dedups at recording time by (call node, precondition) identity, so every topology collapses to exactly one diagnostic and one `call_pre` obligation per violating site — while sites that only the walker ever translates — a violating call inside a `@Nat`-subtraction operand in statement position, checked via the walker's operand discharge — keep their single recording rather than being suppressed.  (Bare statement-position calls with no enclosing subtraction remain unchecked either way; that pre-existing gap is tracked as [#730](https://github.com/aallan/vera/issues/730).)  Translation behaviour is unchanged and the warm/cold differential oracle is untouched.
 - **[#728](https://github.com/aallan/vera/issues/728) — LSP diagnostics now carry the full instruction contract.**  The language server's diagnostic mapping put only the description into the LSP message, so editor hovers said what broke but not how to fix it.  The message now appends the rationale paragraph and the `Fix:` paragraph exactly as `--json` carries them; diagnostics without those fields map to the bare description, unchanged.
+- **E501 messages now speak in call-site terms.**  The precondition is rendered with the actual arguments substituted for the callee's parameter slots (`At this call site: string_length("") > 0`), and the `Fix:` text shows concrete code — the guard with the rendered call (`if string_length("") > 0 then { classify_sentiment("") } else { ... }`) and the exact `requires(...)` to add — instead of generic advice.  Substitution honours De Bruijn most-recent-first resolution; module-qualified callees and unmappable slots keep the generic wording.
 
 ## [0.0.169] - 2026-06-11
 

README.md

@@ -210,7 +210,7 @@ cp /path/to/vera/SKILL.md ~/.claude/skills/vera-language/SKILL.md
 
 ## Project status
 
-Vera is in **active development** at v0.0.170 — 810+ commits, 171 releases, 4,318 tests, 96% code coverage, 89 conformance programs, 35 examples, and a 13-chapter specification. See **[HISTORY.md](HISTORY.md)** for how the compiler was built.
+Vera is in **active development** at v0.0.170 — 810+ commits, 171 releases, 4,321 tests, 96% code coverage, 89 conformance programs, 35 examples, and a 13-chapter specification. See **[HISTORY.md](HISTORY.md)** for how the compiler was built.
 
 The reference compiler — parser, AST, type checker, contract verifier (Z3), WASM code generator, module system, browser runtime, and runtime contract insertion — is working. The language specification is in draft across [13 chapters](spec/).
 

ROADMAP.md

@@ -4,7 +4,7 @@ Where the project is going.  See [HISTORY.md](HISTORY.md) for what's been built
 
 ## Where we are
 
-4,318 tests, 89 conformance programs, 35 examples, 13 spec chapters.
+4,321 tests, 89 conformance programs, 35 examples, 13 spec chapters.
 
 ## What's next
 

TESTING.md

@@ -6,7 +6,7 @@ This is the single source of truth for Vera's testing infrastructure, coverage d
 
 | Metric | Value |
 |--------|-------|
-| **Tests** | 4,318 across 34 files (~55,721 lines of test code; 4,287 passed + 16 stress, 15 skipped) |
+| **Tests** | 4,321 across 34 files (~55,830 lines of test code; 4,290 passed + 16 stress, 15 skipped) |
 | **Compiler code coverage** | 96% of 15,149 statements (CI minimum: 80%) |
 | **Conformance programs** | 89 programs across 9 spec chapters, validating every language feature |
 | **Example programs** | 35, all validated through `vera check` + `vera verify` |
@@ -58,7 +58,7 @@ python scripts/fix_allowlists.py --fix               # auto-fix stale allowlists
 | `test_parser.py` | 129 | 968 | Grammar rules, operator precedence, parse errors |
 | `test_ast.py` | 128 | 1,130 | AST transformation, node structure, serialisation, string escape sequences, ability declarations |
 | `test_checker.py` | 521 | 5,939 | Type synthesis, slot resolution, effects, effect subtyping, contracts, exhaustiveness, cross-module typing, visibility, error codes, string built-ins, generic rejection, IO operation types, Markdown types, Regex types, abilities, Map collection, Set collection, Decimal type, Json type, Html type, Http effect, Inference effect, removed legacy name regression |
-| `test_obligations.py` | 263 | 772 | Reified proof obligations + warm `VerificationSession` (#222 Phase A): full-corpus differential oracle (warm session == cold `verify()` on diagnostics, summary, and obligation stream, plus warm-twice determinism, across all 35 examples and every verify/run-level conformance program), summary↔obligation tier-bookkeeping consistency, per-kind unit tests (requires / ensures / decreases / nat_sub / call_pre statuses, counterexamples, error codes), content-key stability + same-text-two-sites span disambiguation, session solver reuse, type-error short-circuit, ADT-registry resync between programs; plus the Phase B incremental suite — identical-source full replay, callee-body-edit replays callers while callee-contract-edit invalidates them, span-shift and ADT-edit conservative invalidation, cross-program isolation, timeout-status never cached (monkeypatched solver), FIFO eviction bound; plus the #727 dedup pin — a violating call in a let RHS records exactly one E501 diagnostic and one call_pre obligation |
+| `test_obligations.py` | 266 | 851 | Reified proof obligations + warm `VerificationSession` (#222 Phase A): full-corpus differential oracle (warm session == cold `verify()` on diagnostics, summary, and obligation stream, plus warm-twice determinism, across all 35 examples and every verify/run-level conformance program), summary↔obligation tier-bookkeeping consistency, per-kind unit tests (requires / ensures / decreases / nat_sub / call_pre statuses, counterexamples, error codes), content-key stability + same-text-two-sites span disambiguation, session solver reuse, type-error short-circuit, ADT-registry resync between programs; plus the Phase B incremental suite — identical-source full replay, callee-body-edit replays callers while callee-contract-edit invalidates them, span-shift and ADT-edit conservative invalidation, cross-program isolation, timeout-status never cached (monkeypatched solver), FIFO eviction bound; plus the #727 dedup pin — a violating call in a let RHS records exactly one E501 diagnostic and one call_pre obligation |
 | `test_verifier.py` | 146 | 2,128 | Z3 verification, counterexamples, tier classification, call-site preconditions, branch-aware preconditions, pipe operator, cross-module contracts, match/ADT verification, decreases verification, mutual recursion, refined Bool/String/Float64 param sorts, **@Nat subtraction underflow obligation** (#520 — Path-A obligation discharge via requires/path-conditions/path-aware Z3 refutation, pure-literal exclusion, Int-Int and Nat-Int → Int exemptions) |
 | `test_codegen.py` | 1,134 | 19,570 | WASM compilation, arithmetic, Float64, Byte, arrays (incl. compound element types), ADTs, match (incl. nested patterns), generics, State\<T\>, Exn\<E\> handlers, control flow, strings, string escape sequences, IO (read\_line, read\_file, write\_file, args, exit, get\_env, sleep, time, stderr), bounds checking, quantifiers, assert/assume, refinement type aliases, pipe operator, string built-ins, built-in shadowing, parse\_nat Result, GC, Markdown host bindings, Regex host bindings, Map collection, Set collection, Decimal type, Json type, Html type, Http effect, Inference effect, Random effect, example round-trips, GC shadow stack overflow, **WASM tail-call optimization** (#517 — `return_call` emission for tail-position calls, 50K- and 1M-iteration stress, structural assertions on `return_call`/plain `call` boundary, **GC-aware TCO for allocating fns (#549 — `$gc_sp` restore before each `return_call`)**, postcondition-fallback regression (still reverts to plain `call`), analyzer unit tests covering Block-trailing / IfExpr-both-branches / MatchExpr-arm-bodies / let-value-NOT-marked / call-args-NOT-marked / ExprStmt-statement-NOT-marked / IfExpr-condition-NOT-marked / MatchExpr-scrutinee-NOT-marked) |
 | `test_codegen_contracts.py` | 32 | 576 | Runtime pre/postconditions, contract fail messages, old/new state postconditions |
@@ -80,7 +80,7 @@ python scripts/fix_allowlists.py --fix               # auto-fix stale allowlists
 | `test_tester.py` | 17 | 445 | Contract-driven testing: tier classification, input generation, test execution, skip message content |
 | `test_tester_coverage.py` | 34 | 903 | Tester coverage gaps: String/Float64/ADT parameter input generation, Bool/Byte parameters, unsatisfiable preconditions, type expression edge cases |
 | `test_markdown.py` | 59 | 394 | Markdown parser: block/inline parsing, rendering, round-trips, edge cases |
-| `test_lsp.py` | 94 | 1205 | LSP transport + coordinate layer (#222 Phase C) and language features (#222 Phase D): parametrized code-point↔UTF-16 goldens incl. astral-plane fixtures and surrogate-pair snapping, Span (1-based, exclusive-end) and SourceLocation (0-based col) → LSP Range conversions, point→token-range widening, DocumentStore open/change/close + index invalidation, an in-process handler-drive test, and one stdio end-to-end round-trip against the real `vera lsp` subprocess (initialize → didOpen → shutdown → exit) pinning serverInfo + textDocumentSync capabilities; plus the Phase D feature suite — parse-error single-diagnostic path, type-error verification short-circuit, tier=3 in E520 diagnostic data, per-function tier Hint synthesis (and its suppression for functions with violated obligations), smallest-enclosing-span hover, De Bruijn slot goto (most-recent-parameter jump, out-of-range None, off-slot None), and typed-hole completion (inside/after hole, away-from-hole None); plus the Phase E speculativeEdit suite — identical-text all-unchanged, breaking edit surfaces newly_undischarged (violated nat_sub) with canonical state untouched, strengthening edit surfaces newly_discharged, parse/type errors report ok:false, deleted functions report removed, proof_delta purity; plus the Phase F1 proposeEdit suite — the apply gate (clean and strengthening edits apply, breaking and non-compiling edits refuse), force overriding both gates with the delta still reported, wiring against a structural fake server (apply round-trip with exact full-document replacement range, refuse touches no canonical state, unopened-URI clamp sentinel), and full-document-range goldens (trailing-newline virtual line, UTF-16 end column); plus the Phase F2 strengthenContract suite — splice goldens (first-clause-only replacement with byte-identical remainder, ensures variant, unknown-fn None), the call-site audit pin (tightened precondition refused with newly_undischarged call_pre items, canonical state untouched), provable-ensures strengthening applies, and the three splice-target refusal paths (no analysis, unparseable document, unknown function); plus the Phase F3 addEffect suite — transitive-caller closure goldens (diamond in declaration order, leaf, unknown-fn None, recursion appears once), effect-row rewrite goldens (pure to singleton set, source-preserving append, already-present None, base-name identity blocking State<Int> next to State<Bool>), diamond propagation applying one multi-site candidate with the bystander untouched, mixed append/replace rows with already-satisfied callers skipped, the fully-satisfied no-op shape, and the two refusal paths; plus the #728 instruction-contract suite — the LSP message carries description, rationale, and the Fix: paragraph (also pinning single E501 emission at the LSP surface), and a bare diagnostic maps to the description alone |
+| `test_lsp.py` | 94 | 1210 | LSP transport + coordinate layer (#222 Phase C) and language features (#222 Phase D): parametrized code-point↔UTF-16 goldens incl. astral-plane fixtures and surrogate-pair snapping, Span (1-based, exclusive-end) and SourceLocation (0-based col) → LSP Range conversions, point→token-range widening, DocumentStore open/change/close + index invalidation, an in-process handler-drive test, and one stdio end-to-end round-trip against the real `vera lsp` subprocess (initialize → didOpen → shutdown → exit) pinning serverInfo + textDocumentSync capabilities; plus the Phase D feature suite — parse-error single-diagnostic path, type-error verification short-circuit, tier=3 in E520 diagnostic data, per-function tier Hint synthesis (and its suppression for functions with violated obligations), smallest-enclosing-span hover, De Bruijn slot goto (most-recent-parameter jump, out-of-range None, off-slot None), and typed-hole completion (inside/after hole, away-from-hole None); plus the Phase E speculativeEdit suite — identical-text all-unchanged, breaking edit surfaces newly_undischarged (violated nat_sub) with canonical state untouched, strengthening edit surfaces newly_discharged, parse/type errors report ok:false, deleted functions report removed, proof_delta purity; plus the Phase F1 proposeEdit suite — the apply gate (clean and strengthening edits apply, breaking and non-compiling edits refuse), force overriding both gates with the delta still reported, wiring against a structural fake server (apply round-trip with exact full-document replacement range, refuse touches no canonical state, unopened-URI clamp sentinel), and full-document-range goldens (trailing-newline virtual line, UTF-16 end column); plus the Phase F2 strengthenContract suite — splice goldens (first-clause-only replacement with byte-identical remainder, ensures variant, unknown-fn None), the call-site audit pin (tightened precondition refused with newly_undischarged call_pre items, canonical state untouched), provable-ensures strengthening applies, and the three splice-target refusal paths (no analysis, unparseable document, unknown function); plus the Phase F3 addEffect suite — transitive-caller closure goldens (diamond in declaration order, leaf, unknown-fn None, recursion appears once), effect-row rewrite goldens (pure to singleton set, source-preserving append, already-present None, base-name identity blocking State<Int> next to State<Bool>), diamond propagation applying one multi-site candidate with the bystander untouched, mixed append/replace rows with already-satisfied callers skipped, the fully-satisfied no-op shape, and the two refusal paths; plus the #728 instruction-contract suite — the LSP message carries description, rationale, and the Fix: paragraph (also pinning single E501 emission at the LSP surface), and a bare diagnostic maps to the description alone |
 | `test_browser.py` | 102 | 1,990 | Browser parity: Python/wasmtime vs Node.js/JS-runtime output equivalence across IO, State, contracts, Markdown, Regex, and all compilable examples |
 | `test_conformance.py` | 445 | 102 | Parametrized conformance suite: parse, check, verify, run, format idempotency across 89 programs |
 | `test_prelude.py` | 24 | 422 | Prelude injection: Option/Result/array operation detection, combinator shadowing, type aliases, end-to-end compilation |

tests/test_lsp.py

@@ -1181,7 +1181,12 @@ def test_message_carries_rationale_and_fix(self) -> None:
         message = e501[0].message
         assert "may violate the callee's precondition" in message
         assert "Fix:" in message
-        assert "guard the call" in message
+        # The fix is concrete code in call-site terms, not generic
+        # advice: the guard renders the actual call and the
+        # substituted precondition.
+        assert "Guard the call so the precondition holds" in message
+        assert "if 0 > 0 then { need_pos(0) } else { ... }" in message
+        assert "requires(0 > 0)" in message
         # The rationale paragraph travels too.
         assert "SMT solver could not prove" in message
 

tests/test_obligations.py

@@ -474,6 +474,85 @@ def test_pipe_call_violation_records_once(self) -> None:
         ]
         assert len(call_pres) == 1
 
+    def test_e501_renders_precondition_in_call_site_terms(self) -> None:
+        """E501's message states the precondition with the actual
+        arguments substituted, and the fix shows concrete code — the
+        guard with the rendered call, and the requires() to add.
+        """
+        source = (
+            "private fn need_pos(@String -> @String)\n"
+            "  requires(string_length(@String.0) > 0)\n"
+            "  ensures(true)\n"
+            "  effects(pure)\n"
+            "{\n"
+            "  @String.0\n"
+            "}\n"
+            "\n"
+            "public fn caller(-> @Int)\n"
+            "  requires(true)\n"
+            "  ensures(true)\n"
+            "  effects(pure)\n"
+            "{\n"
+            '  let @String = need_pos("");\n'
+            "  0\n"
+            "}\n"
+        )
+        result = self._verify_source(source)
+        e501 = [d for d in result.diagnostics if d.error_code == "E501"]
+        assert len(e501) == 1
+        d = e501[0]
+        assert 'At this call site: string_length("") > 0' in d.description
+        assert d.fix is not None
+        assert (
+            'if string_length("") > 0 then { need_pos("") } else { ... }'
+            in d.fix
+        )
+        assert "requires(string_length(\"\") > 0)" in d.fix
+
+    def test_e501_substitution_resolves_de_bruijn_order(self) -> None:
+        """Slot substitution must honour De Bruijn most-recent-first:
+        for callee (@Int, @Int) with requires(@Int.1 > @Int.0),
+        @Int.1 is parameter 1 and @Int.0 is parameter 2."""
+        source = (
+            "private fn cmp(@Int, @Int -> @Int)\n"
+            "  requires(@Int.1 > @Int.0)\n"
+            "  ensures(true)\n"
+            "  effects(pure)\n"
+            "{\n"
+            "  @Int.0\n"
+            "}\n"
+            "\n"
+            "public fn caller(-> @Int)\n"
+            "  requires(true)\n"
+            "  ensures(true)\n"
+            "  effects(pure)\n"
+            "{\n"
+            "  let @Int = cmp(1, 2);\n"
+            "  @Int.0\n"
+            "}\n"
+        )
+        result = self._verify_source(source)
+        e501 = [d for d in result.diagnostics if d.error_code == "E501"]
+        assert len(e501) == 1
+        assert "At this call site: 1 > 2" in e501[0].description
+
+    def test_e501_unmappable_slot_keeps_generic_fix(self) -> None:
+        """When a precondition slot cannot be mapped to an argument,
+        the message keeps the generic wording instead of guessing."""
+        from vera import ast as A
+        from vera.verifier import ContractVerifier
+
+        v = ContractVerifier.__new__(ContractVerifier)
+        pre = A.Requires(
+            expr=A.SlotRef(
+                type_name="String", type_args=None, index=5, span=None,
+            ),
+            span=None,
+        )
+        call = A.FnCall(name="f", args=(), span=None)
+        out = v._pre_at_call_site((), call, pre)
+        assert out is None
+
     def test_content_key_stable_across_runs(self) -> None:
         source = (
             "public fn f(@Nat -> @Nat)\n"