Per-invariant source ranges for loop-invariant diagnostics (#1361)

## Summary

Loop-invariant verification diagnostics (a failing `invariant(...)` in a
`while`/`for` loop) previously pointed at the **whole loop** instead of
the specific invariant that failed. This change threads each invariant's
source range through the loop's metadata so loop elimination can
attribute each invariant's verification condition to that invariant's
own source location.

This support is required for
[JVerify#437](strata-org/jverify#437)

## Problem

In Strata, loop-invariant proof obligations are synthesized by
`LoopElim` and were tagged with the loop-wide metadata `md`. The
per-invariant source range was lost earlier in the pipeline: Core loop
invariants are bare `(label, expr)` pairs and Core expressions are
`Unit`-annotated, so they carry no source range.

A front-end-only change does not help: the diagnostic location is driven
by the synthesized assert's metadata, not by anything attached to the
invariant expression. The fix therefore has to live in Strata.

## Solution

Thread each invariant's source range through the loop's existing
`MetaData` array and use it per-invariant in `LoopElim`. When a
per-invariant provenance is present, each invariant's generated
assert/assume is attributed to that invariant's own source location;
otherwise we fall back to the loop metadata `md`, so loops not
originating from Laurel (Core `.st`, C_Simp) are unchanged.


## Testing

`StrataTest/.../Fundamentals/T13_WhileLoopsError.lean` adds two
caret-annotated regression tests using the existing diagnostic harness
(`TestDiagnostics`, `matchesDiagnostic`), which checks the exact
start/end line and column of each diagnostic:

1. **`badInitialInvariant`** — a single `invariant i >= 0` that fails on
entry. The caret asserts the diagnostic lands on the invariant
expression, not the `while` loop.
2. **`secondInvariantFails`** — two invariants where the first holds on
entry but the second (`invariant j >= 0`) does not. The caret asserts
the diagnostic points specifically at the failing second invariant. This
is the case that distinguishes per-invariant attribution from loop-wide
attribution: before the fix the range would resolve to the loop, so the
carets would not match.

Verification:

- `lake build Strata` — compiles, no proof breakage.
- `lake build StrataTest` — all `#guard_msgs` tests pass, including the
new ones.
- The fallback to the loop `md` keeps existing Core `.st` and C_Simp
loop diagnostics unchanged.

Author: kadirayk

Strata/DL/Imperative/MetaData.lean

@@ -293,6 +293,27 @@ def MetaData.eraseAllElems {P : PureExpr} [BEq P.Ident]
     (md : MetaData P) (fld : MetaDataElem.Field P) : MetaData P :=
   md.filter (fun e => !(e.fld == fld))
 
+/-- Label for a per-loop-invariant source provenance. Loop lowering stores one
+    such element per invariant, in invariant order, so that loop elimination can
+    attribute each invariant's verification condition to the specific invariant's
+    source location rather than to the whole loop. -/
+def MetaData.invariantProvenanceLabel : String := "invariantProvenance"
+
+/-- Append a loop invariant's provenance to metadata. These are appended in
+    invariant order. Note this matches on the `.label` constructor directly, so
+    it needs no `BEq P.Ident` instance. -/
+def MetaData.pushInvariantProvenance {P : PureExpr} (md : MetaData P) (p : Provenance) : MetaData P :=
+  md.push { fld := .label MetaData.invariantProvenanceLabel, value := .provenance p }
+
+/-- Get all per-invariant provenances from metadata, in the order they were
+    pushed (matching the loop's invariant order). -/
+def MetaData.getInvariantProvenances {P : PureExpr} (md : MetaData P) : Array Provenance :=
+  md.filterMap fun elem =>
+    match elem.fld, elem.value with
+    | .label l, .provenance p =>
+      if l == MetaData.invariantProvenanceLabel then some p else none
+    | _, _ => none
+
 /-- Replace the primary provenance with a new one, shifting existing related
     provenances and prepending the old primary provenance. -/
 def MetaData.setCallSiteFileRange {P : PureExpr} [BEq P.Ident]

Strata/Languages/Laurel/LaurelAST.lean

@@ -418,11 +418,15 @@ def Condition.mapM [Monad m] (f : AstNode StmtExpr → m (AstNode StmtExpr)) (c
 def Condition.mapCondition (f : AstNode StmtExpr → AstNode StmtExpr) (c : Condition) : Condition :=
   { c with condition := f c.condition }
 
+/-- Build a provenance from an optional source location. -/
+def fileRangeToProvenance (source : Option FileRange) : Provenance :=
+  match source with
+  | some fr => Provenance.ofSourceRange fr.file fr.range
+  | none => .synthesized .laurel
+
 /-- Build Core metadata from an optional source location. -/
 def fileRangeToCoreMd (source : Option FileRange) : Imperative.MetaData Core.Expression :=
-  match source with
-  | some fr => Imperative.MetaData.ofSourceRange fr.file fr.range
-  | none => Imperative.MetaData.ofProvenance (.synthesized .laurel)
+  Imperative.MetaData.ofProvenance (fileRangeToProvenance source)
 
 /-- Build Core metadata from an AstNode's source location. -/
 def astNodeToCoreMd (node : AstNode α) : Imperative.MetaData Core.Expression :=

Strata/Languages/Laurel/LaurelToCoreTranslator.lean

@@ -502,7 +502,15 @@ def translateStmt (stmt : StmtExprMd)
       let invExprs ← invariants.mapM (fun i => do return ("", ← translateExpr i))
       let decreasingExprCore ← decreasesExpr.mapM (translateExpr)
       let bodyStmts ← translateStmt body
-      return [Imperative.Stmt.loop (.det condExpr) decreasingExprCore invExprs bodyStmts md]
+      -- Attach each invariant's source provenance to the loop metadata, in
+      -- invariant order, so loop elimination can point an invariant's
+      -- verification condition at the specific invariant rather than the whole
+      -- loop. (The Core loop IR stores invariants as `(label, expr)` pairs with
+      -- no per-invariant metadata slot, and Core expressions carry no source
+      -- range, so we thread the ranges through the loop metadata instead.)
+      let mdWithInvs := invariants.foldl
+        (fun acc i => acc.pushInvariantProvenance (fileRangeToProvenance i.source)) md
+      return [Imperative.Stmt.loop (.det condExpr) decreasingExprCore invExprs bodyStmts mdWithInvs]
   | .Exit target =>
       return [Imperative.Stmt.exit target md]
   | .Hole _ _ =>

Strata/Transform/LoopElim.lean

@@ -142,16 +142,34 @@ def Stmt.removeLoopsM
     -- reference to the source invariant.
     let invSuffix : Nat → String → String := fun i lbl =>
       if lbl.isEmpty then toString i else s!"{i}_{lbl}"
+    -- Per-invariant source provenance, threaded through the loop metadata by the
+    -- Laurel→Core translation (in invariant order). When present, each
+    -- invariant's generated assert/assume is attributed to that invariant's own
+    -- source location instead of the whole loop; otherwise we fall back to the
+    -- loop metadata `md` (e.g. for loops not originating from Laurel).
+    -- Contract: `invProvs` holds one provenance per invariant, in invariant
+    -- order, pushed by the Laurel→Core translation (`pushInvariantProvenance`).
+    -- When the sizes disagree (e.g. a loop not originating from Laurel, or a
+    -- future desync between push and retrieval) we fall back to the loop `md`
+    -- via the index lookup below, so a mismatch degrades gracefully rather than
+    -- mis-attributing ranges.
+    let invProvs := MetaData.getInvariantProvenances md
+    let invMd : Nat → MetaData P := fun i =>
+      -- Only real source locations (`.loc`) refine the diagnostic; a synthesized
+      -- provenance carries no usable range, so fall back to the loop `md`
+      match invProvs[i]? with
+      | some (p@(.loc ..)) => MetaData.ofProvenance p
+      | _ => md
     let entry_invariants := invariants.mapIdx fun i (lbl, inv) =>
-      Stmt.cmd (HasPassiveCmds.assert s!"entry_invariant_{loop_num}_{invSuffix i lbl}" inv md)
+      Stmt.cmd (HasPassiveCmds.assert s!"entry_invariant_{loop_num}_{invSuffix i lbl}" inv (invMd i))
     let entry_invariant_assumes := invariants.mapIdx fun i (lbl, inv) =>
-      Stmt.cmd (HasPassiveCmds.assume s!"assume_entry_invariant_{loop_num}_{invSuffix i lbl}" inv md)
+      Stmt.cmd (HasPassiveCmds.assume s!"assume_entry_invariant_{loop_num}_{invSuffix i lbl}" inv (invMd i))
     let first_iter_facts :=
       .block s!"first_iter_asserts_{loop_num}" (entry_invariants ++ entry_invariant_assumes) {}
     let inv_assumes := invariants.mapIdx fun i (lbl, inv) =>
-      Stmt.cmd (HasPassiveCmds.assume s!"{loopElimInvariantPrefix}{loop_num}_{invSuffix i lbl}" inv md)
+      Stmt.cmd (HasPassiveCmds.assume s!"{loopElimInvariantPrefix}{loop_num}_{invSuffix i lbl}" inv (invMd i))
     let maintain_invariants := invariants.mapIdx fun i (lbl, inv) =>
-      Stmt.cmd (HasPassiveCmds.assert s!"arbitrary_iter_maintain_invariant_{loop_num}_{invSuffix i lbl}" inv md)
+      Stmt.cmd (HasPassiveCmds.assert s!"arbitrary_iter_maintain_invariant_{loop_num}_{invSuffix i lbl}" inv (invMd i))
     -- Guard-specific parts: assume_guard, termination, not_guard
     let (guard_assumes, pre_termination, post_termination, exit_guard) ← match guard with
       | .det g => do
@@ -183,7 +201,7 @@ def Stmt.removeLoopsM
       ([havocd, arbitrary_iter_assumes] ++ pre_termination ++
        body_statements ++ maintain_invariants ++ post_termination) {}
     let invariant_assumes := invariants.mapIdx fun i (lbl, inv) =>
-      Stmt.cmd (HasPassiveCmds.assume s!"invariant_{loop_num}_{invSuffix i lbl}" inv md)
+      Stmt.cmd (HasPassiveCmds.assume s!"invariant_{loop_num}_{invSuffix i lbl}" inv (invMd i))
     let exit_state_assumes := [havocd] ++ exit_guard ++ invariant_assumes
     let loop_passive :=
       .ite guard (arbitrary_iter_facts :: exit_state_assumes) [] {}

StrataTest/Languages/Laurel/Examples/Fundamentals/T13_WhileLoopsError.lean

@@ -0,0 +1,68 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import StrataTest.Util.TestLaurel
+
+open StrataTest.Util
+open Strata
+
+/-! ## Loop-invariant failures point at the specific invariant
+
+These negative tests pin each failing loop invariant's diagnostic to that
+invariant's own source range (per-invariant source ranges threaded through
+loop elimination), rather than the whole loop. -/
+
+#eval testLaurel
+#strata
+program Laurel;
+procedure badInitialInvariant()
+  opaque
+{
+    var i: int := -1;
+    while(i < 10)
+      invariant i >= 0
+//              ^^^^^^ error: assertion does not hold
+    {
+        i := i + 1
+    }
+};
+#end
+
+#eval testLaurel
+#strata
+program Laurel;
+procedure secondInvariantFails()
+  opaque
+{
+    var i: int := 0;
+    var j: int := -1;
+    while(i < 10)
+      invariant i >= 0
+      invariant j >= 0
+//              ^^^^^^ error: assertion does not hold
+    {
+        i := i + 1;
+        j := j + 1
+    }
+};
+#end
+
+#eval testLaurel
+#strata
+program Laurel;
+procedure forSecondInvFails()
+  opaque
+{
+    var j: int := -1;
+    for(var i: int := 0; i < 10; i := i + 1)
+      invariant i >= 0
+      invariant j >= 0
+//              ^^^^^^ error: assertion does not hold
+    {
+        j := j + 1
+    }
+};
+#end