Per-invariant source ranges for loop-invariant diagnostics

[kadirayk]

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

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.

[fabiomadge]

LGTM, non-blocking comments (leaving as a comment, not a formal approval). Clean, well-scoped fix for the LoopElim whole-loop-range issue (jverify#437). Built and verified: build green, loop suite green (T13/T17/Core Loops), VCs unchanged — each invariant's expr, label, and property-type are untouched; only the per-invariant MetaData differs, and metadata drives diagnostics, not the VC.

Design is the right tradeoff. The Core loop IR stores invariants as (String × Expr) with no per-invariant metadata slot, and Core exprs are Unit-annotated. Threading provenances through the loop md is the correct localized choice (4 files, no IR/proof/backend churn):

• Metadata on the invariant tuple is cleaner but changes Stmt.loop + its induction principle → ripples into semantics proofs and the CBMC backend. Too invasive.
• Metadata on Core exprs needs a slot the Unit-annotated type lacks — the "front-end-only fix doesn't help" point, confirmed.
• It mirrors the existing relatedFileRange/getRelatedFileRanges pattern, so it's house idiom.

Main ask: add a for-loop test. For-loops work (verified: a failing 2nd for-loop invariant lands on the invariant expr, since for desugars to the same .While), but only while-loops are tested. Verified drop-in for T13_WhileLoopsError.lean:

def forSecondInvFailsProgram := r"
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
    }
};
"

#guard_msgs (drop info, error) in
#eval testInputWithOffset "ForSecondInvFails" forSecondInvFailsProgram 60 processLaurelFile

Good to merge once that's in. Remaining points inline.

[fabiomadge]

(duplicate of the review above — posted twice by mistake; see the other review for the full content)

[fabiomadge]

Thanks for the follow-ups — all four points from my earlier comments are addressed: the .loc gating (so a sourceless invariant falls back to the loop range instead of losing it), the fileRangeToCoreMd/fileRangeToProvenance de-dup, the documented invProvs[i] contract with graceful fallback, and the MetaData.getInvariantProvenances naming. The added for-loop test is a nice extra. Built T13_WhileLoopsError locally and the per-invariant caret annotations all match. LGTM.

[aqjune-aws]

Great patch :)