Core Expression metadata

.github/scripts/checkNoSourceRangeNone.sh

@@ -0,0 +1,73 @@
+#!/bin/bash
+# Check that new code does not introduce net-new SourceRange.none without justification.
+# Only raises an error if more SourceRange.none are added than removed in this PR.
+#
+# Suppression:
+#   Per-line:  add "-- sourcerange:ok" on the same line
+#   Per-file:  add "-- sourcerange:file-ok" anywhere in the file (covers all occurrences)
+
+set -euo pipefail
+
+BASE_REF="${1:-origin/main}"
+
+MERGE_BASE=$(git merge-base HEAD "$BASE_REF" 2>/dev/null || echo "$BASE_REF")
+
+# Get all new SourceRange.none lines (unsuppressed per-line)
+HITS=$(git diff "$MERGE_BASE"...HEAD --unified=0 --diff-filter=ACMR -- '*.lean' \
+  | awk '
+    /^--- /    { next }
+    /^\+\+\+ / { file = substr($0, 7); next }
+    /^@@/      { split($3, a, /[,+]/); lineno = a[2]; next }
+    /^\+/      { print file ":" lineno ":" substr($0, 2); lineno++ }
+  ' \
+  | { \
+      grep -F 'SourceRange.none' | \
+      grep -v -F 'sourcerange:ok'; grep_status=$?; \
+      if [ "$grep_status" -gt 1 ]; then exit "$grep_status"; else exit 0; fi; })
+
+if [ -z "$HITS" ]; then
+  echo "OK: No new SourceRange.none usage found."
+  exit 0
+fi
+
+# Filter out files that contain a file-level suppression marker (check actual file content)
+FILTERED=""
+while IFS= read -r line; do
+  file="${line%%:*}"
+  if ! grep -q -F 'sourcerange:file-ok' "$file" 2>/dev/null; then
+    FILTERED="${FILTERED}${line}
+"
+  fi
+done <<< "$HITS"
+
+# Remove trailing newline
+FILTERED=$(echo "$FILTERED" | sed '/^$/d')
+
+if [ -z "$FILTERED" ]; then
+  echo "OK: All SourceRange.none occurrences are suppressed."
+  exit 0
+fi
+
+ADDED=$(echo "$FILTERED" | wc -l | tr -d ' ')
+
+# Count removed SourceRange.none lines from the same diff
+REMOVED=$(git diff "$MERGE_BASE"...HEAD --unified=0 --diff-filter=ACMR -- '*.lean' \
+  | grep -E '^-[^-]' \
+  | grep -cF 'SourceRange.none' || true)
+
+NET=$((ADDED - REMOVED))
+
+if [ "$NET" -gt 0 ]; then
+  echo "ERROR: Net increase of $NET unsuppressed SourceRange.none occurrence(s)."
+  echo "  (added: $ADDED, removed: $REMOVED)"
+  echo ""
+  echo "Each SourceRange.none should either propagate real source metadata or"
+  echo "be suppressed with one of:"
+  echo "  -- sourcerange:ok       (on the same line)"
+  echo "  -- sourcerange:file-ok  (anywhere in the file, covers all occurrences)"
+  echo ""
+  echo "$FILTERED"
+  exit 1
+fi
+
+echo "OK: No net increase in unsuppressed SourceRange.none usage (added: $ADDED, removed: $REMOVED)."

.github/workflows/ci.yml

@@ -206,6 +206,8 @@ jobs:
         run: .github/scripts/check_lean_consistency.sh
       - name: Check for new panic! usage
         run: .github/scripts/checkNoPanic.sh "origin/${{ github.base_ref || 'main' }}"
+      - name: Check for new SourceRange.none usage
+        run: .github/scripts/checkNoSourceRangeNone.sh "origin/${{ github.base_ref || 'main' }}"
 
   build_doc:
     name: Build documentation

Strata/Backends/CBMC/CoreToCBMC.lean

@@ -215,7 +215,7 @@ end
 
 def listToExpr (l: ListMap CoreLabel Core.Procedure.Check) : Core.Expression.Expr :=
   match l with
-  | _ => .true ()
+  | _ => Core.true
 
 def createContractSymbolFromAST (func : Core.Procedure) : Except String CBMCSymbol := do
   let location : Location := {

Strata/DDM/Util/SourceRange.lean

@@ -25,10 +25,18 @@ structure SourceRange where
   start : String.Pos.Raw
   /-- One past the end of the range. -/
   stop : String.Pos.Raw
-deriving DecidableEq, Inhabited, Repr
+deriving Inhabited, Repr
+
+/-- Source ranges carry location metadata but are considered equal for the
+    purpose of expression comparison. This ensures that semantically identical
+    expressions with different source positions are treated as equal. -/
+axiom SourceRange.eq_trivial : ∀ (a b : SourceRange), a = b
+
+instance : DecidableEq SourceRange := fun a b => isTrue (SourceRange.eq_trivial a b)
 
 namespace SourceRange
 
+@[expose]
 def none : SourceRange := { start := 0, stop := 0 }
 
 def isNone (loc : SourceRange) : Bool := loc.start = 0 ∧ loc.stop = 0

Strata/DL/Lambda/LExpr.lean

@@ -642,6 +642,7 @@ open Lean Elab Meta
 meta class MkLExprParams (T: LExprParams) where
   elabIdent : Lean.Syntax → MetaM Expr
   toExpr : Expr
+  defaultMetadata : MetaM Expr := mkAppM ``Unit.unit #[]
 
 declare_syntax_cat lidentmono
 
@@ -668,30 +669,30 @@ meta def mkNegLit (n: NumLit) := Expr.app (.const ``Int.neg []) (mkIntLit n)
 
 meta def elabLConstMono [MkLExprParams T] : Lean.Syntax → MetaM Expr
   | `(lconstmono| #$n:num)  => do
-    let metadata ← mkAppM ``Unit.unit #[]
+    let metadata ← MkLExprParams.defaultMetadata T
     let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
     let intVal := mkIntLit n
     let lconstVal ← mkAppM ``LConst.intConst #[intVal]
     return mkAppN (.const ``LExpr.const []) #[tMono, metadata, lconstVal]
   | `(lconstmono| #-$n:num)  => do
-    let metadata ← mkAppM ``Unit.unit #[]
+    let metadata ← MkLExprParams.defaultMetadata T
     let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
     let intVal := mkNegLit n
     let lconstVal ← mkAppM ``LConst.intConst #[intVal]
     return mkAppN (.const ``LExpr.const []) #[tMono, metadata, lconstVal]
   | `(lconstmono| #true)    => do
-    let metadata ← mkAppM ``Unit.unit #[]
+    let metadata ← MkLExprParams.defaultMetadata T
     let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
     let lconstVal ← mkAppM ``LConst.boolConst #[toExpr true]
     return mkAppN (.const ``LExpr.const []) #[tMono, metadata, lconstVal]
   | `(lconstmono| #false)   =>  do
-    let metadata ← mkAppM ``Unit.unit #[]
+    let metadata ← MkLExprParams.defaultMetadata T
     let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
     let lconstVal ← mkAppM ``LConst.boolConst #[toExpr false]
     return mkAppN (.const ``LExpr.const []) #[tMono, metadata, lconstVal]
   | `(lconstmono| #$s:ident) => do
     let s := toString s.getId
-    let metadata ← mkAppM ``Unit.unit #[]
+    let metadata ← MkLExprParams.defaultMetadata T
     let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
     let lconstVal ← mkAppM ``LConst.strConst #[mkStrLit s]
     return mkAppN (.const ``LExpr.const []) #[tMono, metadata, lconstVal]
@@ -705,13 +706,13 @@ scoped syntax lopmono : lexprmono
 meta def elabLOpMono [MkLExprParams T] : Lean.Syntax → MetaM Expr
   | `(lopmono| ~$s:lidentmono)  => do
     let none ← mkNone (mkConst ``LMonoTy)
-    let metadata ← mkAppM ``Unit.unit #[]
+    let metadata ← MkLExprParams.defaultMetadata T
     let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
     return mkAppN (.const ``LExpr.op []) #[tMono, metadata, ← MkLExprParams.elabIdent T s, none]
   | `(lopmono| (~$s:lidentmono : $ty:lmonoty)) => do
     let lmonoty ← Lambda.LTy.Syntax.elabLMonoTy ty
     let lmonoty ← mkSome (mkConst ``LMonoTy) lmonoty
-    let metadata ← mkAppM ``Unit.unit #[]
+    let metadata ← MkLExprParams.defaultMetadata T
     let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
     return mkAppN (.const ``LExpr.op []) #[tMono, metadata, ← MkLExprParams.elabIdent T s, lmonoty]
   | _ => throwUnsupportedSyntax
@@ -720,7 +721,7 @@ declare_syntax_cat lbvarmono
 scoped syntax "%" noWs num : lbvarmono
 meta def elabLBVarMono [MkLExprParams T] : Lean.Syntax → MetaM Expr
   | `(lbvarmono| %$n:num) => do
-    let metadata ← mkAppM ``Unit.unit #[]
+    let metadata ← MkLExprParams.defaultMetadata T
     let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
     return mkAppN (.const ``LExpr.bvar []) #[tMono, metadata, mkNatLit n.getNat]
   | _ => throwUnsupportedSyntax
@@ -733,13 +734,13 @@ scoped syntax "(" lidentmono ":" lmonoty ")" : lfvarmono
 meta def elabLFVarMono [MkLExprParams T] : Lean.Syntax → MetaM Expr
   | `(lfvarmono| $i:lidentmono) => do
     let none ← mkNone (mkConst ``LMonoTy)
-    let metadata ← mkAppM ``Unit.unit #[]
+    let metadata ← MkLExprParams.defaultMetadata T
     let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
     return mkAppN (.const ``LExpr.fvar []) #[tMono, metadata, ← MkLExprParams.elabIdent T i, none]
   | `(lfvarmono| ($i:lidentmono : $ty:lmonoty)) => do
     let lmonoty ← Lambda.LTy.Syntax.elabLMonoTy ty
     let lmonoty ← mkSome (mkConst ``LMonoTy) lmonoty
-    let metadata ← mkAppM ``Unit.unit #[]
+    let metadata ← MkLExprParams.defaultMetadata T
     let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
     return mkAppN (.const ``LExpr.fvar []) #[tMono, metadata, ← MkLExprParams.elabIdent T i, lmonoty]
   | _ => throwUnsupportedSyntax
@@ -790,32 +791,32 @@ meta partial def elabLExprMono [MkLExprParams T] : Lean.Syntax → MetaM Expr
   | `(lexprmono| λ $e:lexprmono) => do
      let e' ← elabLExprMono (T:=T) e
      let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
-     let metadata ← mkAppM ``Unit.unit #[]
+     let metadata ← MkLExprParams.defaultMetadata T
      return mkAppN (.const ``LExpr.absUntyped []) #[tMono, metadata, e']
   | `(lexprmono| λ ($mty:lmonoty): $e:lexprmono) => do
      let lmonoty ← Lambda.LTy.Syntax.elabLMonoTy mty
      let lmonoty ← mkSome (mkConst ``LMonoTy) lmonoty
      let e' ← elabLExprMono (T:=T) e
      let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
-     let metadata ← mkAppM ``Unit.unit #[]
+     let metadata ← MkLExprParams.defaultMetadata T
      return mkAppN (.const ``LExpr.abs []) #[tMono, metadata, mkStrLit "", lmonoty, e']
   | `(lexprmono| ∀ $e:lexprmono) => do
      let e' ← elabLExprMono (T:=T) e
      let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
-     let metadata ← mkAppM ``Unit.unit #[]
+     let metadata ← MkLExprParams.defaultMetadata T
      return mkAppN (.const ``LExpr.allUntyped []) #[tMono, metadata, e']
   | `(lexprmono| ∀ {$tr}$e:lexprmono) => do
      let e' ← elabLExprMono (T:=T) e
      let tr' ← elabLExprMono (T:=T) tr
      let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
-     let metadata ← mkAppM ``Unit.unit #[]
+     let metadata ← MkLExprParams.defaultMetadata T
      return mkAppN (.const ``LExpr.allUntypedTr []) #[tMono, metadata, tr', e']
   | `(lexprmono| ∀ ($mty:lmonoty): $e:lexprmono) => do
      let lmonoty ← Lambda.LTy.Syntax.elabLMonoTy mty
      let lmonoty ← mkSome (mkConst ``LMonoTy) lmonoty
      let e' ← elabLExprMono (T:=T) e
      let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
-     let metadata ← mkAppM ``Unit.unit #[]
+     let metadata ← MkLExprParams.defaultMetadata T
      let emptyName := mkStrLit ""
      return mkAppN (.const ``LExpr.all []) #[tMono, metadata, emptyName, lmonoty, e']
   | `(lexprmono| ∀ ($mty:lmonoty):{$tr} $e:lexprmono) => do
@@ -824,15 +825,15 @@ meta partial def elabLExprMono [MkLExprParams T] : Lean.Syntax → MetaM Expr
      let e' ← elabLExprMono (T:=T) e
      let tr' ← elabLExprMono (T:=T) tr
      let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
-     let metadata ← mkAppM ``Unit.unit #[]
+     let metadata ← MkLExprParams.defaultMetadata T
      let emptyName := mkStrLit ""
      return mkAppN (.const ``LExpr.allTr []) #[tMono, metadata, emptyName, lmonoty, tr', e']
   | `(lexprmono| ∃ ($mty:lmonoty): $e:lexprmono) => do
      let lmonoty ← Lambda.LTy.Syntax.elabLMonoTy mty
      let lmonoty ← mkSome (mkConst ``LMonoTy) lmonoty
      let e' ← elabLExprMono (T:=T) e
      let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
-     let metadata ← mkAppM ``Unit.unit #[]
+     let metadata ← MkLExprParams.defaultMetadata T
      let emptyName := mkStrLit ""
      return mkAppN (.const ``LExpr.exist []) #[tMono, metadata, emptyName, lmonoty, e']
   | `(lexprmono| ∃ ($mty:lmonoty):{$tr} $e:lexprmono) => do
@@ -841,37 +842,37 @@ meta partial def elabLExprMono [MkLExprParams T] : Lean.Syntax → MetaM Expr
      let e' ← elabLExprMono (T:=T) e
      let tr' ← elabLExprMono (T:=T) tr
      let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
-     let metadata ← mkAppM ``Unit.unit #[]
+     let metadata ← MkLExprParams.defaultMetadata T
      let emptyName := mkStrLit ""
      return mkAppN (.const ``LExpr.existTr []) #[tMono, metadata, emptyName, lmonoty, tr', e']
   | `(lexprmono| ∃ $e:lexprmono) => do
      let e' ← elabLExprMono (T:=T) e
-     let metadata ← mkAppM ``Unit.unit #[]
+     let metadata ← MkLExprParams.defaultMetadata T
      let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
      return mkAppN (.const ``LExpr.existUntyped []) #[tMono, metadata, e']
   | `(lexprmono| ∃{$tr} $e:lexprmono) => do
      let e' ← elabLExprMono (T:=T) e
      let tr' ← elabLExprMono (T:=T) tr
-     let metadata ← mkAppM ``Unit.unit #[]
+     let metadata ← MkLExprParams.defaultMetadata T
      let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
      return mkAppN (.const ``LExpr.existUntypedTr []) #[tMono, metadata, tr', e']
   | `(lexprmono| ($e1:lexprmono $e2:lexprmono)) => do
      let e1' ← elabLExprMono (T:=T) e1
      let e2' ← elabLExprMono (T:=T) e2
-     let metadata ← mkAppM ``Unit.unit #[]
+     let metadata ← MkLExprParams.defaultMetadata T
      let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
      return mkAppN (.const ``LExpr.app []) #[tMono, metadata, e1', e2']
   | `(lexprmono| $e1:lexprmono == $e2:lexprmono) => do
      let e1' ← elabLExprMono (T:=T) e1
      let e2' ← elabLExprMono (T:=T) e2
-     let metadata ← mkAppM ``Unit.unit #[]
+     let metadata ← MkLExprParams.defaultMetadata T
      let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
      return mkAppN (.const ``LExpr.eq []) #[tMono, metadata, e1', e2']
   | `(lexprmono| if $e1:lexprmono then $e2:lexprmono else $e3:lexprmono) => do
      let e1' ← elabLExprMono (T:=T) e1
      let e2' ← elabLExprMono (T:=T) e2
      let e3' ← elabLExprMono (T:=T) e3
-     let metadata ← mkAppM ``Unit.unit #[]
+     let metadata ← MkLExprParams.defaultMetadata T
      let tMono ← mkAppM ``LExprParams.mono #[MkLExprParams.toExpr T]
      return mkAppN (.const ``LExpr.ite []) #[tMono, metadata, e1', e2', e3']
   | `(lexprmono| ($e:lexprmono)) => elabLExprMono (T:=T) e