Fix early return soundness in Laurel: replace assume false with exit

Strata/Languages/Laurel/LaurelToCoreTranslator.lean

@@ -355,11 +355,9 @@ def translateStmt (env : TypeEnv) (outputParams : List Parameter) (stmt : StmtEx
           let ident := ⟨outParam.name, ()⟩
           let coreExpr ← translateExpr env value
           let assignStmt := Core.Statement.set ident coreExpr md
-          let noFallThrough := Core.Statement.assume "return" (.const () (.boolConst false)) .empty
-          return (env, [assignStmt, noFallThrough])
+          return (env, [assignStmt, .exit (some "$body") md])
       | none, _ =>
-          let noFallThrough := Core.Statement.assume "return" (.const () (.boolConst false)) .empty
-          return (env, [noFallThrough])
+          return (env, [.exit (some "$body") md])
       | some _, none =>
           panic! "Return statement with value but procedure has no output parameters"
   | .While cond invariants decreasesExpr body =>
@@ -422,11 +420,13 @@ def translateProcedure (proc : Procedure) : TranslateM Core.Procedure := do
         translateChecks initEnv postconds "postcondition"
     | _ => pure []
   let modifies : List Core.Expression.Ident := []
-  let body : List Core.Statement ←
+  let bodyStmts : List Core.Statement ←
     match proc.body with
     | .Transparent bodyExpr => (·.2) <$> translateStmt initEnv proc.outputs bodyExpr
     | .Opaque _postconds (some impl) _ => (·.2) <$> translateStmt initEnv proc.outputs impl
     | _ => pure [Core.Statement.assume "no_body" (.const () (.boolConst false)) .empty]
+  -- Wrap body in a labeled block so early returns (exit) work correctly.
+  let body : List Core.Statement := [.block "$body" bodyStmts .empty]
   let spec : Core.Procedure.Spec := { modifies, preconditions, postconditions }
   return { header, spec, body }
 

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

@@ -41,6 +41,9 @@ procedure dag(a: int) returns (r: int)
   }
   assert if (a > 0) { b == 1 } else { true };
     assert if (a > 0) { b == 2 } else { true };
+//  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
+// duplicates due to VCG path duplication (#419):
+//  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
 //  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
   return b;
 }

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

@@ -0,0 +1,41 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import StrataTest.Util.TestDiagnostics
+import StrataTest.Languages.Laurel.TestExamples
+
+open StrataTest.Util
+open Strata
+
+namespace Strata.Laurel
+
+def program := r"
+procedure earlyReturnCorrect(x: int) returns (r: int)
+  ensures r >= 0
+{
+  if (x < 0) {
+    return -x;
+  }
+  return x;
+}
+
+procedure earlyReturnBuggy(x: int) returns (r: int)
+  ensures r >= 0
+//        ^^^^^^ error: assertion does not hold
+// duplicate due to VCG path duplication (#419):
+//        ^^^^^^ error: assertion does not hold
+{
+  if (x < 0) {
+    return x;
+  }
+  return x;
+}
+"
+
+#guard_msgs (drop info, error) in
+#eval testInputWithOffset "EarlyReturn" program 14 processLaurelFile
+
+end Strata.Laurel

StrataTest/Util/TestDiagnostics.lean

@@ -51,10 +51,13 @@ def parseDiagnosticExpectations (content : String) : List DiagnosticExpectation
           let caretColStart := commentPrefix + caretStart.offset.byteIdx
           let caretColEnd := commentPrefix + currentCaret.offset.byteIdx
 
-          -- The diagnostic is on the previous line
+          -- The diagnostic is on the nearest previous non-comment line
           if i > 0 then
+            let mut targetLine := i
+            while targetLine > 0 && lines[targetLine - 1]!.trimAsciiStart.startsWith "//" do
+              targetLine := targetLine - 1
             expectations := expectations.append [{
-              line := i,  -- 1-indexed line number (the line before the comment)
+              line := targetLine,
               colStart := caretColStart,
               colEnd := caretColEnd,
               level := level,