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,322 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,322 tests, 89 conformance programs, 35 examples, 13 spec chapters.
 
 ## What's next
 

scripts/check_changelog_updated.py

@@ -172,18 +172,23 @@ def is_substantive(path: str) -> bool:
 def _changelog_has_new_entry(base: str) -> bool:
     """Return True if the CHANGELOG.md diff adds a new entry.
 
-    A "new entry" is either:
+    A "new entry" is any of:
 
     1. An added line introducing a new version heading (``+## [X.Y.Z]``
        or ``+## [Unreleased]``).
     2. An added bullet (``+- ...``) that appears *inside* the
        ``[Unreleased]`` section.
+    3. An added bullet inside the LATEST released section (the first
+       version heading after ``[Unreleased]``) — the tag-move fold-in
+       pattern: a follow-up PR amends the most recent release's
+       section and the tag moves to its merge commit, so bullets
+       there are release-notes-bearing.
 
     Section-tracking is necessary because CHANGELOG.md commonly has
     prose edits (typo fixes, wording tweaks) inside released-version
-    entries.  Those edits sometimes add bulleted lines, but they
-    shouldn't count as "adding a new entry" for the purposes of this
-    check — only bullets under ``[Unreleased]`` do.
+    entries.  Those edits sometimes add bulleted lines; for sections
+    OLDER than the latest release they don't count as "adding a new
+    entry" — that history is frozen.
 
     Pure whitespace or cosmetic changes to CHANGELOG.md don't count.
     """
@@ -205,6 +210,7 @@ def _changelog_has_new_entry(base: str) -> bool:
     # lines (prefixed with ``+``); we update current_section on both
     # so the tracker reflects the post-diff state of the file.
     current_section: str | None = None
+    latest_release: str | None = None
     for line in diff.splitlines():
         if line.startswith("+++") or line.startswith("---"):
             # File headers — ignore entirely.
@@ -231,6 +237,14 @@ def _changelog_has_new_entry(base: str) -> bool:
             end = content.find("]", 4)
             if end > 4:
                 current_section = content[4:end]
+                # The first versioned heading in file order is the
+                # most recent release (the diff spans the whole file
+                # via --unified=9999, so diff order == file order).
+                if (
+                    latest_release is None
+                    and current_section != "Unreleased"
+                ):
+                    latest_release = current_section
             # An *added* versioned heading (e.g. ``+## [0.0.114]``) is
             # itself a new entry — that's the release-cutting pattern.
             # But a bare ``+## [Unreleased]`` heading is just structural
@@ -241,10 +255,17 @@ def _changelog_has_new_entry(base: str) -> bool:
                 return True
             continue
 
-        # Added bullets only count inside the [Unreleased] section.
+        # Added bullets count inside [Unreleased], or inside the
+        # latest released section (the fold-in pattern; see the
+        # docstring).
         if line.startswith("+") and content.startswith("- "):
             if current_section == "Unreleased":
                 return True
+            if (
+                current_section is not None
+                and current_section == latest_release
+            ):
+                return True
 
     return False
 

tests/test_check_changelog_updated.py

@@ -270,34 +270,59 @@ def test_ignores_cosmetic_changes(
         monkeypatch.setattr(_mod, "_run", lambda cmd: diff)
         assert _mod._changelog_has_new_entry("origin/main") is False
 
-    def test_bullet_outside_unreleased_does_not_count(
+    def test_bullet_in_older_released_section_does_not_count(
         self, monkeypatch: pytest.MonkeyPatch,
     ) -> None:
-        """Added bullets inside a *released* version entry are not new entries.
+        """Added bullets inside sections OLDER than the latest release
+        are not new entries — that history is frozen.
 
-        A prose fix that inserts a bullet into an existing version's
-        description isn't "adding a new entry" — only bullets under the
-        [Unreleased] section (or a new ``## [X.Y.Z]`` heading) count.
-
-        Regression test: prior to the fix, any added ``+- `` line
-        counted, so editing v0.0.111's description would have satisfied
-        the check for any substantive change on the branch.
+        (Bullets in the LATEST released section DO count — the
+        tag-move fold-in pattern; see the companion test below.)
         """
         diff = textwrap.dedent("""\
             diff --git a/CHANGELOG.md b/CHANGELOG.md
-            @@ -5,7 +5,10 @@
+            @@ -5,7 +5,12 @@
              ## [Unreleased]
 
+             ## [0.0.112] - 2026-04-11
+
+             ### Added
+
+             - The latest release's existing bullet.
+
              ## [0.0.111] - 2026-04-10
 
              ### Fixed
             +
-            +- Additional clarification bullet on an existing fix.
+            +- Additional clarification bullet on an old fix.
              - **SMT translator: String/Float64 parameters**...
             """)
         monkeypatch.setattr(_mod, "_run", lambda cmd: diff)
         assert _mod._changelog_has_new_entry("origin/main") is False
 
+    def test_bullet_in_latest_released_section_counts(
+        self, monkeypatch: pytest.MonkeyPatch,
+    ) -> None:
+        """Added bullets in the FIRST version section after
+        [Unreleased] count: the tag-move fold-in pattern amends the
+        most recent release's section and re-releases it."""
+        diff = textwrap.dedent("""\
+            diff --git a/CHANGELOG.md b/CHANGELOG.md
+            @@ -5,7 +5,10 @@
+             ## [Unreleased]
+
+             ## [0.0.112] - 2026-04-11
+
+             ### Fixed
+            +
+            +- Fold-in bullet for the re-released version.
+             - An existing bullet.
+
+             ## [0.0.111] - 2026-04-10
+            """)
+        monkeypatch.setattr(_mod, "_run", lambda cmd: diff)
+        assert _mod._changelog_has_new_entry("origin/main") is True
+
     def test_bullet_under_unreleased_counts(
         self, monkeypatch: pytest.MonkeyPatch,
     ) -> None:

tests/test_lsp.py

@@ -1180,8 +1180,14 @@ def test_message_carries_rationale_and_fix(self) -> None:
         assert len(e501) == 1  # also pins #727 at the LSP surface
         message = e501[0].message
         assert "may violate the callee's precondition" in message
+        assert "At this call site:" 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"