From 873fd61185af32b9253c2707152d44cb78bf0df0 Mon Sep 17 00:00:00 2001
From: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com>
Date: Tue, 5 May 2026 13:41:08 +0000
Subject: [PATCH 1/4] Improve block formatting and diagnostic reporting

Formatting improvements:
- Change block formatting to use indent(2) with newlines for vertical layout
  instead of single-line '{ ... }' format
- Update semicolon separator to use newlines instead of spaces

Debugging improvements:
- Replace boolean 'coreProgramHasSuperfluousErrors' with 'coreDiagnostics' list
  that records why the Core program was suppressed, enabling better error surfacing
- Add source location and reason parameters to 'invalidCoreType' for more
  informative diagnostics
- Surface core diagnostics when no other diagnostics explain program suppression
- Add 'processLaurelFileKeepIntermediates' test helper for writing intermediate
  pipeline files to Build/ directory
- Add Build/ to .gitignore

Test updates:
- Update all expected outputs to match new block formatting
- Add 'opaque' keyword to test procedures that need it for the new formatting
- Fix #guard_msgs whitespace formatting
---
 .gitignore                                    |   3 +-
 Strata/DDM/Format.lean                        |   2 +-
 .../Laurel/Grammar/LaurelGrammar.lean         |   2 +-
 .../Languages/Laurel/Grammar/LaurelGrammar.st |   4 +-
 .../Laurel/LaurelCompilationPipeline.lean     |   7 +-
 .../Laurel/LaurelToCoreTranslator.lean        |  28 +--
 .../AbstractToConcreteTreeTranslatorTest.lean |  78 ++++++---
 .../Laurel/ConstrainedTypeElimTest.lean       |  54 ++++--
 .../Laurel/DivisionByZeroCheckTest.lean       |   2 +-
 .../Fundamentals/T10_ConstrainedTypes.lean    |   2 +-
 .../Fundamentals/T15_ShortCircuit.lean        |   2 +-
 .../Laurel/LiftExpressionAssignmentsTest.lean |  13 +-
 .../Languages/Laurel/LiftHolesTest.lean       | 164 +++++++++++++-----
 StrataTest/Languages/Laurel/TestExamples.lean |  10 ++
 .../Languages/Python/PySpecArgTypeTest.lean   |   7 +-
 15 files changed, 282 insertions(+), 96 deletions(-)

diff --git a/.gitignore b/.gitignore
index 3776616d98..9f5babd9ab 100644
--- a/.gitignore
+++ b/.gitignore
@@ -12,4 +12,5 @@ vcs/*.smt2
 *.py.ion
 *.py.ion.core.st
 
-Strata.code-workspace
\ No newline at end of file
+Strata.code-workspace
+Build/
\ No newline at end of file
diff --git a/Strata/DDM/Format.lean b/Strata/DDM/Format.lean
index 613a726135..4d97f30839 100644
--- a/Strata/DDM/Format.lean
+++ b/Strata/DDM/Format.lean
@@ -453,7 +453,7 @@ private partial def ArgF.mformatM {α} : ArgF α → FormatM PrecFormat
     if z : entries.size = 0 then
       pure (.atom .nil)
     else do
-      let f i q s := return s ++ "; " ++ (← entries[i].mformatM).format
+      let f i q s := return s ++ ";\n" ++ (← entries[i].mformatM).format
       let a := (← entries[0].mformatM).format
       .atom <$> entries.size.foldlM f (start := 1) a
 
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
index 02e2159643..c185d90edc 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
@@ -9,7 +9,7 @@ module
 -- Laurel dialect definition, loaded from LaurelGrammar.st
 -- NOTE: Changes to LaurelGrammar.st are not automatically tracked by the build system.
 -- Update this file (e.g. this comment) to trigger a recompile after modifying LaurelGrammar.st.
--- Last grammar change: multiAssign supports field access targets, added opaque keyword.
+-- Last grammar change: block format uses indent(2) with leading spaces for vertical layout.
 public import Strata.DDM.Integration.Lean
 public meta import Strata.DDM.Integration.Lean
 
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
index b81b0d8b11..5ddc8609f5 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
@@ -106,8 +106,8 @@ op ifThenElse (cond: StmtExpr, thenBranch: StmtExpr, elseBranch: Option ElseBran
 op assert (cond : StmtExpr, errorMessage: Option ErrorSummary) : StmtExpr => @[prec(0)] "assert " cond:0 errorMessage:0;
 op assume (cond : StmtExpr) : StmtExpr => @[prec(0)] "assume " cond:0;
 op return (value : StmtExpr) : StmtExpr => @[prec(0)] "return " value:0;
-op block (stmts : SemicolonSepBy StmtExpr) : StmtExpr => @[prec(1000)] "{ " stmts " }";
-op labelledBlock (stmts : SemicolonSepBy StmtExpr, label : Ident) : StmtExpr => @[prec(1000)] "{ " stmts " }" label;
+op block (stmts : SemicolonSepBy StmtExpr) : StmtExpr => @[prec(1000)] "{\n  " indent(2, stmts) "\n}";
+op labelledBlock (stmts : SemicolonSepBy StmtExpr, label : Ident) : StmtExpr => @[prec(1000)] "{\n  " indent(2, stmts) "\n}" label;
 op exit (label : Ident) : StmtExpr => @[prec(0)] "exit " label;
 
 // While loops
diff --git a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
index c6984120fe..61db034a52 100644
--- a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
+++ b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
@@ -211,8 +211,13 @@ def translateWithLaurel (options : LaurelTranslateOptions) (program : Program)
     if let some coreProgram := coreProgramOption then
       emit "CoreProgram" "core.st" coreProgram
     let mut allDiagnostics := passDiags ++ translateState.diagnostics
+
+    if translateState.coreDiagnostics.length > 0 && allDiagnostics.isEmpty then
+      -- The program was suppressed but no diagnostics explain why — report the core diagnostics.
+      allDiagnostics := allDiagnostics ++ translateState.coreDiagnostics
+
     let coreProgramOption :=
-      if translateState.coreProgramHasSuperfluousErrors then none else coreProgramOption
+      if !translateState.coreDiagnostics.isEmpty then none else coreProgramOption
     return (coreProgramOption, allDiagnostics, program, stats)
 
 /--
diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
index cccf8ab011..8983f69e82 100644
--- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
+++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
@@ -62,8 +62,11 @@ structure TranslateState where
   model : SemanticModel
   /-- Overflow check configuration -/
   overflowChecks : Core.OverflowChecks := {}
-  /-- Do not process the produces Core program, since it has superfluous errors -/
-  coreProgramHasSuperfluousErrors: Bool := false
+  /-- Diagnostics that indicate the Core program should not be processed further.
+      When non-empty, the produced Core program is suppressed. Each entry records
+      why the program was deemed invalid so that if no other diagnostics explain
+      the suppression, these can be surfaced to the user. -/
+  coreDiagnostics : List DiagnosticModel := []
 
 /-- The translation monad: state over Except, allowing both accumulated diagnostics and hard failures -/
 @[expose] abbrev TranslateM := OptionT (StateM TranslateState)
@@ -72,8 +75,9 @@ structure TranslateState where
 def emitDiagnostic (d : DiagnosticModel) : TranslateM Unit :=
   modify fun s => { s with diagnostics := s.diagnostics ++ [d] }
 
-private def invalidCoreType : TranslateM LMonoTy := do
-  modify fun s => { s with coreProgramHasSuperfluousErrors := true }
+private def invalidCoreType (source : Option FileRange := none) (reason : String := "Type could not be translated to Core (resolution error placeholder)") : TranslateM LMonoTy := do
+  modify fun s => { s with coreDiagnostics := s.coreDiagnostics ++
+    [diagnosticFromSource source reason DiagnosticType.StrataBug] }
   return .tcons s!"LaurelResolutionErrorPlaceholder" []
 
 /-
@@ -97,14 +101,15 @@ def translateType (ty : HighTypeMd) : TranslateM LMonoTy := do
     | some (.datatypeDefinition dt) => return .tcons dt.name.text []
     | some (.datatypeConstructor typeName _) => return .tcons typeName.text []
     | _ => do -- resolution should have already emitted a diagnostic
-      modify fun s => { s with coreProgramHasSuperfluousErrors := true }
+      modify fun s => { s with coreDiagnostics := s.coreDiagnostics ++
+        [diagnosticFromSource ty.source s!"UserDefined type could not be resolved to a composite or datatype" DiagnosticType.StrataBug] }
       return .tcons "Composite" []
   | .TCore s => return .tcons s []
   | .TReal => return LMonoTy.real
-  | .Unknown => invalidCoreType
+  | .Unknown => invalidCoreType ty.source "Unknown type encountered during Core translation"
   | _ => do
     emitDiagnostic (diagnosticFromSource ty.source "cannot translate type to Core: not supported yet" DiagnosticType.StrataBug)
-    invalidCoreType
+    invalidCoreType ty.source s!"cannot translate type to Core: not supported yet"
 
 termination_by ty.val
 decreasing_by all_goals (first | (cases elementType; term_by_mem) | (cases keyType; term_by_mem) | (cases valueType; term_by_mem))
@@ -129,7 +134,7 @@ private def freshId : TranslateM Nat := do
 /-- Throw a hard diagnostic error, aborting the current translation -/
 def throwExprDiagnostic (d : DiagnosticModel): TranslateM Core.Expression.Expr := do
   emitDiagnostic d
-  modify fun s => { s with coreProgramHasSuperfluousErrors := true }
+  modify fun s => { s with coreDiagnostics := s.coreDiagnostics ++ [d] }
   let id ← freshId
   return LExpr.fvar () (⟨s!"DUMMY_VAR_{id}", ()⟩) none
 
@@ -345,7 +350,7 @@ private def exprAsUnusedInit (expr : StmtExprMd) (md : Imperative.MetaData Core.
 
 def throwStmtDiagnostic (d : DiagnosticModel): TranslateM (List Core.Statement) := do
   emitDiagnostic d
-  modify fun s => { s with coreProgramHasSuperfluousErrors := true }
+  modify fun s => { s with coreDiagnostics := s.coreDiagnostics ++ [d] }
   return []
 
 /--
@@ -493,8 +498,9 @@ def translateStmt (stmt : StmtExprMd)
       | none =>
           return [.exit (some "$body") md]
       | some _ =>
-          emitDiagnostic $ md.toDiagnostic "Return statement with value should have been eliminated by EliminateValueReturns pass" DiagnosticType.StrataBug
-          modify fun s => { s with coreProgramHasSuperfluousErrors := true }
+          let d := md.toDiagnostic "Return statement with value should have been eliminated by EliminateValueReturns pass" DiagnosticType.StrataBug
+          emitDiagnostic d
+          modify fun s => { s with coreDiagnostics := s.coreDiagnostics ++ [d] }
           return [.exit (some "$body") md]
   | .While cond invariants decreasesExpr body =>
       let condExpr ← translateExpr cond
diff --git a/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean b/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean
index 701405b362..5134de4f39 100644
--- a/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean
+++ b/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean
@@ -58,21 +58,30 @@ private def roundtrip (input : String) : IO String := do
 
 /--
 info: procedure foo()
-{ assert true; assert false };
+  opaque
+{
+  assert true;
+  assert false
+};
 -/
 #guard_msgs in
-#eval do IO.println (← roundtrip r"procedure foo() { assert true; assert false };")
+#eval do IO.println (← roundtrip r"procedure foo() opaque { assert true; assert false };")
 
 /--
 info: procedure add(x: int, y: int): int
-{ x + y };
+  opaque
+{
+  x + y
+};
 -/
 #guard_msgs in
-#eval do IO.println (← roundtrip r"procedure add(x: int, y: int): int { x + y };")
+#eval do IO.println (← roundtrip r"procedure add(x: int, y: int): int opaque { x + y };")
 
 /--
 info: function aFunction(x: int): int
-{ x };
+{
+  x
+};
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"function aFunction(x: int): int { x };")
@@ -90,17 +99,22 @@ composite Point {
 
 /--
 info: procedure test(x: int): int
-{ if x > 0 then x else 0 - x };
+  opaque
+{
+  if x > 0 then x else 0 - x
+};
 -/
 #guard_msgs in
-#eval do IO.println (← roundtrip r"procedure test(x: int): int { if x > 0 then x else 0 - x };")
+#eval do IO.println (← roundtrip r"procedure test(x: int): int opaque { if x > 0 then x else 0 - x };")
 
 /--
 info: procedure divide(x: int, y: int): int
   requires y != 0
   opaque
   ensures result >= 0
-{ x / y };
+{
+  x / y
+};
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"
@@ -113,11 +127,15 @@ procedure divide(x: int, y: int): int
 
 /--
 info: procedure test()
-{ assert forall(x: int) => x == x; assert exists(y: int) => y > 0 };
+  opaque
+{
+  assert forall(x: int) => x == x;
+  assert exists(y: int) => y > 0
+};
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"
-procedure test() {
+procedure test() opaque {
     assert forall(x: int) => x == x;
     assert exists(y: int) => y > 0
 };
@@ -127,7 +145,12 @@ procedure test() {
 info: composite Point { var x: int var y: int }
 
 procedure test(): int
-{ var p: Point := new Point; p#x := 5; p#x };
+  opaque
+{
+  var p: Point := new Point;
+  p#x := 5;
+  p#x
+};
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"
@@ -135,7 +158,7 @@ composite Point {
   var x: int
   var y: int
 }
-procedure test(): int {
+procedure test(): int opaque {
     var p: Point := new Point;
     p#x := 5;
     p#x
@@ -160,25 +183,34 @@ info: composite Animal { }
 composite Dog extends Animal { }
 
 procedure test(a: Animal): bool
-{ a is Dog };
+  opaque
+{
+  a is Dog
+};
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"
 composite Animal {}
 composite Dog extends Animal {}
-procedure test(a: Animal): bool { a is Dog };
+procedure test(a: Animal): bool opaque { a is Dog };
 ")
 
 -- Additional coverage: while loops
 
 /--
 info: procedure test()
-{ var x: int := 0; while(x < 10)
-  invariant x >= 0 { x := x + 1 } };
+  opaque
+{
+  var x: int := 0;
+  while(x < 10)
+    invariant x >= 0 {
+    x := x + 1
+  }
+};
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"
-procedure test() {
+procedure test() opaque {
     var x: int := 0;
     while(x < 10)
       invariant x >= 0
@@ -203,7 +235,10 @@ procedure modify(c: Container)
   opaque
   ensures true
   modifies c
-{ c#value := c#value + 1; true };
+{
+  c#value := c#value + 1;
+  true
+};
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"
@@ -219,9 +254,12 @@ procedure modify(c: Container)
 
 /--
 info: procedure test(): int
-{ <??> };
+  opaque
+{
+  <??>
+};
 -/
 #guard_msgs in
-#eval do IO.println (← roundtrip r"procedure test(): int { <??> };")
+#eval do IO.println (← roundtrip r"procedure test(): int opaque { <??> };")
 
 end Strata.Laurel
diff --git a/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean b/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean
index 86ce51e683..bf333e569c 100644
--- a/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean
+++ b/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean
@@ -44,15 +44,25 @@ def parseLaurelAndElim (input : String) : IO Program := do
 
 /--
 info: function nat$constraint(x: int): bool
-{ x >= 0 };
+{
+  x >= 0
+};
 procedure test(n: int)
   returns (r: int)
   requires nat$constraint(n)
   opaque
   ensures nat$constraint(r)
-{ assert r >= 0; var y: int := n; assert nat$constraint(y); return y };
+{
+  assert r >= 0;
+  var y: int := n;
+  assert nat$constraint(y);
+  return y
+};
 procedure $witness_nat()
-{ var $witness: int := 0; assert nat$constraint($witness) };
+{
+  var $witness: int := 0;
+  assert nat$constraint($witness)
+};
 -/
 #guard_msgs in
 #eval! do
@@ -76,11 +86,25 @@ procedure test(b: bool) {
 
 /--
 info: function pos$constraint(v: int): bool
-{ v > 0 };
+{
+  v > 0
+};
 procedure test(b: bool)
-{ if b then { var x: int := 1; assert pos$constraint(x) }; { var x: int := -5; x := -10 } };
+{
+  if b then {
+    var x: int := 1;
+    assert pos$constraint(x)
+  };
+  {
+    var x: int := -5;
+    x := -10
+  }
+};
 procedure $witness_pos()
-{ var $witness: int := 1; assert pos$constraint($witness) };
+{
+  var $witness: int := 1;
+  assert pos$constraint($witness)
+};
 -/
 #guard_msgs in
 #eval! do
@@ -92,7 +116,7 @@ procedure $witness_pos()
 -- The variable has no known value, only the type constraint is assumed.
 def uninitProgram : String := r"
 constrained posint = x: int where x > 0 witness 1
-procedure f() {
+procedure f() opaque {
   var x: posint;
   assert x == 1
 };
@@ -100,11 +124,21 @@ procedure f() {
 
 /--
 info: function posint$constraint(x: int): bool
-{ x > 0 };
+{
+  x > 0
+};
 procedure f()
-{ var x: int; assume posint$constraint(x); assert x == 1 };
+  opaque
+{
+  var x: int;
+  assume posint$constraint(x);
+  assert x == 1
+};
 procedure $witness_posint()
-{ var $witness: int := 1; assert posint$constraint($witness) };
+{
+  var $witness: int := 1;
+  assert posint$constraint($witness)
+};
 -/
 #guard_msgs in
 #eval! do
diff --git a/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean b/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean
index 40e8a9112d..e58d25cea1 100644
--- a/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean
+++ b/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean
@@ -59,7 +59,7 @@ procedure callPureDivUnsafe(x: int)
 };
 "
 
-#guard_msgs(drop info, error) in
+#guard_msgs (drop info, error) in
 #eval testInputWithOffset "DivByZeroE2E" e2eProgram 22 processLaurelFile
 
 end Laurel
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean
index 80d21eb4d6..3bad996cd3 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean
@@ -196,7 +196,7 @@ procedure captureTest(y: haslarger)
 };
 "
 
-#guard_msgs(drop info, error) in
+#guard_msgs (drop info, error) in
 #eval testInputWithOffset "ConstrainedTypes" program 14 processLaurelFile
 
 end Laurel
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean
index 2e5b46a8ab..30737832d6 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean
@@ -91,7 +91,7 @@ procedure testImpliesProc()
 };
 "
 
-#guard_msgs(drop info) in
+#guard_msgs (drop info) in
 #eval testInputWithOffset "ShortCircuit" shortCircuitProgram 15 processLaurelFile
 
 end Laurel
diff --git a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean
index f3a3acbd6f..98e1706a3f 100644
--- a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean
+++ b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean
@@ -23,6 +23,7 @@ namespace Strata.Laurel
 
 def blockStmtLiftingProgram : String := r"
 procedure assertInBlockExpr()
+  opaque
 {
   var x: int := 0;
   var y: int := { assert x == 0; x := 1; x };
@@ -44,7 +45,17 @@ def parseLaurelAndLift (input : String) : IO Program := do
 
 /--
 info: procedure assertInBlockExpr()
-{ var x: int := 0; assert x == 0; var $x_0: int := x; x := 1; var y: int := { x }; assert y == 1 };
+  opaque
+{
+  var x: int := 0;
+  assert x == 0;
+  var $x_0: int := x;
+  x := 1;
+  var y: int := {
+    x
+  };
+  assert y == 1
+};
 -/
 #guard_msgs in
 #eval! do
diff --git a/StrataTest/Languages/Laurel/LiftHolesTest.lean b/StrataTest/Languages/Laurel/LiftHolesTest.lean
index 14d25a4416..08966a3321 100644
--- a/StrataTest/Languages/Laurel/LiftHolesTest.lean
+++ b/StrataTest/Languages/Laurel/LiftHolesTest.lean
@@ -46,11 +46,14 @@ info: function $hole_0()
   returns ($result: int)
   opaque;
 procedure test()
-{ var x: int := 1 + $hole_0() };
+  opaque
+{
+  var x: int := 1 + $hole_0()
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var x: int := 1 + <?> };
+procedure test() opaque { var x: int := 1 + <?> };
 "
 
 -- Bare Hole as Assign Declare initializer → replaced with call (no longer preserved as havoc).
@@ -59,11 +62,14 @@ info: function $hole_0()
   returns ($result: int)
   opaque;
 procedure test()
-{ var x: int := $hole_0() };
+  opaque
+{
+  var x: int := $hole_0()
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var x: int := <?> };
+procedure test() opaque { var x: int := <?> };
 "
 
 -- Hole in comparison arg inside assert → int (inferred from sibling literal).
@@ -72,11 +78,14 @@ info: function $hole_0()
   returns ($result: int)
   opaque;
 procedure test()
-{ assert $hole_0() > 0 };
+  opaque
+{
+  assert $hole_0() > 0
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { assert <?> > 0 };
+procedure test() opaque { assert <?> > 0 };
 "
 
 -- Hole directly as assert condition → bool.
@@ -85,11 +94,14 @@ info: function $hole_0()
   returns ($result: bool)
   opaque;
 procedure test()
-{ assert $hole_0() };
+  opaque
+{
+  assert $hole_0()
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { assert <?> };
+procedure test() opaque { assert <?> };
 "
 
 -- Hole directly as assume condition → bool.
@@ -98,11 +110,14 @@ info: function $hole_0()
   returns ($result: bool)
   opaque;
 procedure test()
-{ assume $hole_0() };
+  opaque
+{
+  assume $hole_0()
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { assume <?> };
+procedure test() opaque { assume <?> };
 "
 
 -- Hole as if-then-else condition → bool.
@@ -111,11 +126,16 @@ info: function $hole_0()
   returns ($result: bool)
   opaque;
 procedure test()
-{ if $hole_0() then { assert true } };
+  opaque
+{
+  if $hole_0() then {
+    assert true
+  }
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { if <?> then { assert true } };
+procedure test() opaque { if <?> then { assert true } };
 "
 
 -- Hole in then-branch of if-then-else inside typed local variable → int.
@@ -124,11 +144,14 @@ info: function $hole_0()
   returns ($result: int)
   opaque;
 procedure test()
-{ var x: int := if true then $hole_0() else 0 };
+  opaque
+{
+  var x: int := if true then $hole_0() else 0
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var x: int := if true then <?> else 0 };
+procedure test() opaque { var x: int := if true then <?> else 0 };
 "
 
 -- Hole as while-loop condition → bool.
@@ -137,11 +160,16 @@ info: function $hole_0()
   returns ($result: bool)
   opaque;
 procedure test()
-{ while($hole_0()) {  } };
+  opaque
+{
+  while($hole_0()) {
+    ⏎
+  }
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { while(<?>) {} };
+procedure test() opaque { while(<?>) {} };
 "
 
 -- Hole as while-loop invariant → bool.
@@ -150,12 +178,17 @@ info: function $hole_0()
   returns ($result: bool)
   opaque;
 procedure test()
-{ while(true)
-  invariant $hole_0() {  } };
+  opaque
+{
+  while(true)
+    invariant $hole_0() {
+    ⏎
+  }
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { while(true) invariant <?> {} };
+procedure test() opaque { while(true) invariant <?> {} };
 "
 
 /-! ## Operators -/
@@ -166,11 +199,14 @@ info: function $hole_0()
   returns ($result: bool)
   opaque;
 procedure test()
-{ assert true && $hole_0() };
+  opaque
+{
+  assert true && $hole_0()
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { assert true && <?> };
+procedure test() opaque { assert true && <?> };
 "
 
 -- Hole in Neg inside typed local variable → int.
@@ -179,11 +215,14 @@ info: function $hole_0()
   returns ($result: int)
   opaque;
 procedure test()
-{ var x: int := -$hole_0() };
+  opaque
+{
+  var x: int := -$hole_0()
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var x: int := -<?> };
+procedure test() opaque { var x: int := -<?> };
 "
 
 -- Hole in StrConcat inside typed local variable → string.
@@ -192,11 +231,14 @@ info: function $hole_0()
   returns ($result: string)
   opaque;
 procedure test()
-{ var s: string := "hello" ++ $hole_0() };
+  opaque
+{
+  var s: string := "hello" ++ $hole_0()
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint
-  "procedure test() { var s: string := \"hello\" ++ <?> };"
+  "procedure test() opaque { var s: string := \"hello\" ++ <?> };"
 
 /-! ## Multiple holes -/
 
@@ -209,11 +251,14 @@ function $hole_1()
   returns ($result: int)
   opaque;
 procedure test()
-{ var x: int := $hole_0() + $hole_1() };
+  opaque
+{
+  var x: int := $hole_0() + $hole_1()
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var x: int := <?> + <?> };
+procedure test() opaque { var x: int := <?> + <?> };
 "
 
 -- Holes across statements: Mul arg (int) then assert condition (bool).
@@ -225,11 +270,15 @@ function $hole_1()
   returns ($result: bool)
   opaque;
 procedure test()
-{ var x: int := 2 * $hole_0(); assert $hole_1() };
+  opaque
+{
+  var x: int := 2 * $hole_0();
+  assert $hole_1()
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var x: int := 2 * <?>; assert <?> };
+procedure test() opaque { var x: int := 2 * <?>; assert <?> };
 "
 
 /-! ## Combinations: holes in nested contexts -/
@@ -240,11 +289,16 @@ info: function $hole_0()
   returns ($result: int)
   opaque;
 procedure test()
-{ if 1 + $hole_0() > 0 then { assert true } };
+  opaque
+{
+  if 1 + $hole_0() > 0 then {
+    assert true
+  }
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { if 1 + <?> > 0 then { assert true } };
+procedure test() opaque { if 1 + <?> > 0 then { assert true } };
 "
 
 -- Hole in Implies inside while invariant → bool.
@@ -253,12 +307,18 @@ info: function $hole_0()
   returns ($result: bool)
   opaque;
 procedure test()
-{ var p: bool; while(true)
-  invariant p ==> $hole_0() {  } };
+  opaque
+{
+  var p: bool;
+  while(true)
+    invariant p ==> $hole_0() {
+    ⏎
+  }
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var p: bool; while(true) invariant p ==> <?> {} };
+procedure test() opaque { var p: bool; while(true) invariant p ==> <?> {} };
 "
 
 -- Hole in Mul inside typed local variable with real type → real.
@@ -267,11 +327,14 @@ info: function $hole_0()
   returns ($result: real)
   opaque;
 procedure test()
-{ var r: real := 3.14 * $hole_0() };
+  opaque
+{
+  var r: real := 3.14 * $hole_0()
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var r: real := 3.14 * <?> };
+procedure test() opaque { var r: real := 3.14 * <?> };
 "
 
 /-! ## Call argument and return type inference -/
@@ -282,11 +345,14 @@ info: function $hole_0(n: int)
   returns ($result: int)
   opaque;
 procedure test(n: int)
-{ assert n > $hole_0(n) };
+  opaque
+{
+  assert n > $hole_0(n)
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test(n: int) { assert n > <?> };
+procedure test(n: int) opaque { assert n > <?> };
 "
 
 /-! ## Holes in functions -/
@@ -297,11 +363,14 @@ info: function $hole_0(x: int)
   returns ($result: int)
   opaque;
 function test(x: int): int
-{ $hole_0(x) };
+  opaque
+{
+  $hole_0(x)
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-function test(x: int): int { <?> };
+function test(x: int): int opaque { <?> };
 "
 
 /-! ## Nondeterministic holes (<??>) -/
@@ -309,11 +378,14 @@ function test(x: int): int { <?> };
 -- Nondet hole in procedure → preserved after eliminateHoles (lifted by liftExpressionAssignments).
 /--
 info: procedure test()
-{ assert <??> };
+  opaque
+{
+  assert <??>
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { assert <??> };
+procedure test() opaque { assert <??> };
 "
 
 -- Mixed: det hole eliminated, nondet hole preserved.
@@ -322,11 +394,15 @@ info: function $hole_0()
   returns ($result: int)
   opaque;
 procedure test()
-{ var x: int := $hole_0(); assert <??> };
+  opaque
+{
+  var x: int := $hole_0();
+  assert <??>
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var x: int := <?>; assert <??> };
+procedure test() opaque { var x: int := <?>; assert <??> };
 "
 
 -- Nondet hole in function → should be rejected (not tested here since
diff --git a/StrataTest/Languages/Laurel/TestExamples.lean b/StrataTest/Languages/Laurel/TestExamples.lean
index 5affbb2813..781cc366fd 100644
--- a/StrataTest/Languages/Laurel/TestExamples.lean
+++ b/StrataTest/Languages/Laurel/TestExamples.lean
@@ -36,4 +36,14 @@ def processLaurelFileWithOptions (options : LaurelVerifyOptions) (input : InputC
 def processLaurelFile (input : InputContext) : IO (Array Diagnostic) :=
   processLaurelFileWithOptions default input
 
+/-- Project-root-relative path to the `Build/` directory for intermediate files.
+    Resolved from the current working directory so it works on any machine. -/
+def buildDir : IO String := do
+  let cwd ← IO.currentDir
+  return s!"{cwd}/Build/"
+
+def processLaurelFileKeepIntermediates (input : InputContext) : IO (Array Diagnostic) := do
+  let dir ← buildDir
+  processLaurelFileWithOptions { translateOptions := { keepAllFilesPrefix := dir}} input
+
 end Laurel
diff --git a/StrataTest/Languages/Python/PySpecArgTypeTest.lean b/StrataTest/Languages/Python/PySpecArgTypeTest.lean
index d921aaab9c..ff30813ef9 100644
--- a/StrataTest/Languages/Python/PySpecArgTypeTest.lean
+++ b/StrataTest/Languages/Python/PySpecArgTypeTest.lean
@@ -97,7 +97,12 @@ preconditions redundant. -/
 info: procedure typed_func(x: Any, y: Any): Any
   opaque
   modifies *
-{ result := <??>; assert Any..isfrom_int(x); assert Any..isfrom_str(y); assume Any..isfrom_float(result) };
+{
+  result := <??>;
+  assert Any..isfrom_int(x);
+  assert Any..isfrom_str(y);
+  assume Any..isfrom_float(result)
+};
 -/
 #guard_msgs in
 #eval! do

From efcc50c8e42a14dc6269a3bff1a9fe829469385d Mon Sep 17 00:00:00 2001
From: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com>
Date: Tue, 5 May 2026 14:31:05 +0000
Subject: [PATCH 2/4] Fix: only surface coreDiagnostics with known source
 locations

Diagnostics with FileRange.unknown are not actionable for users and
can arise from pre-existing resolution limitations (e.g., variables
in multi-assign with field targets losing their uniqueId). Filter
these out when surfacing suppression reasons to avoid spurious errors.
---
 Strata/Languages/Laurel/LaurelCompilationPipeline.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
index 61db034a52..3d3faa7457 100644
--- a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
+++ b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
@@ -213,8 +213,10 @@ def translateWithLaurel (options : LaurelTranslateOptions) (program : Program)
     let mut allDiagnostics := passDiags ++ translateState.diagnostics
 
     if translateState.coreDiagnostics.length > 0 && allDiagnostics.isEmpty then
-      -- The program was suppressed but no diagnostics explain why — report the core diagnostics.
-      allDiagnostics := allDiagnostics ++ translateState.coreDiagnostics
+      -- The program was suppressed but no diagnostics explain why — report the core diagnostics
+      -- that have a known source location (those without one are not actionable for the user).
+      let locatedDiags := translateState.coreDiagnostics.filter (·.fileRange != FileRange.unknown)
+      allDiagnostics := allDiagnostics ++ locatedDiags
 
     let coreProgramOption :=
       if !translateState.coreDiagnostics.isEmpty then none else coreProgramOption

From 44f1248741b6e5958dc6f6e58cb6661b1a7d4eee Mon Sep 17 00:00:00 2001
From: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com>
Date: Tue, 5 May 2026 15:08:43 +0000
Subject: [PATCH 3/4] Fix benchmark CI: use github.repository for CodeBuild
 source location

The CodeBuild source location was hardcoded to strata-org/Strata.git,
which fails when the commit only exists in keyboardDrummer/Strata.
Use github.server_url/github.repository so it resolves to the correct
repo dynamically.
---
 .github/workflows/ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index d01fc1ed7c..8e59e9b9e8 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -342,7 +342,7 @@ jobs:
           BUILD_ID=$(aws codebuild start-build \
             --project-name strata-benchmarks \
             --source-type-override GITHUB \
-            --source-location-override https://github.com/strata-org/Strata.git \
+            --source-location-override ${{ github.server_url }}/${{ github.repository }}.git \
             --source-version ${{ github.event.pull_request.head.sha || github.sha }} \
             --query 'build.id' --output text \
             --region us-east-2)

From bfe799ceb89773c419e3d49e22ebb542b3c7e6b0 Mon Sep 17 00:00:00 2001
From: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com>
Date: Tue, 5 May 2026 15:35:03 +0000
Subject: [PATCH 4/4] Fix benchmark CI: skip on forks, restore hardcoded source
 URL

The CodeBuild project has credentials for strata-org/Strata only.
On forks like keyboardDrummer/Strata, the job cannot access the source.
Add an 'if' condition to skip the benchmark on non-upstream repos,
and restore the hardcoded source URL that CodeBuild expects.
---
 .github/workflows/ci.yml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 8e59e9b9e8..87c3f2190d 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -324,6 +324,7 @@ jobs:
 
   strata-benchmarks:
     name: Run internal benchmarks of Strata
+    if: github.repository == 'strata-org/Strata'
     runs-on: ubuntu-latest
     permissions:
       id-token: write
@@ -342,7 +343,7 @@ jobs:
           BUILD_ID=$(aws codebuild start-build \
             --project-name strata-benchmarks \
             --source-type-override GITHUB \
-            --source-location-override ${{ github.server_url }}/${{ github.repository }}.git \
+            --source-location-override https://github.com/strata-org/Strata.git \
             --source-version ${{ github.event.pull_request.head.sha || github.sha }} \
             --query 'build.id' --output text \
             --region us-east-2)