Core Expression metadata

.github/scripts/checkNoSourceRangeNone.sh

@@ -0,0 +1,96 @@
+#!/bin/bash
+# Check that new code does not introduce net-new SourceRange.none or ExprSourceLoc.none
+# without justification.
+#
+# Suppression:
+#   Per-line:  add "-- nosourcerange: <explanation>" on the same line
+#   Per-file:  add "-- nosourcerange-file: <explanation>" anywhere in the file
+#
+# The explanation must be non-empty and must not consist solely of "ok".
+
+set -euo pipefail
+
+BASE_REF="${1:-origin/main}"
+
+# Patterns to check. If any of these are renamed, the safety check below will
+# detect that the pattern no longer appears anywhere in the codebase and fail,
+# forcing the developer to update this list.
+NONE_PATTERNS=("SourceRange.none" "ExprSourceLoc.none")
+
+# Safety check: every pattern must appear at least once in the tracked Lean
+# files. If a pattern disappears entirely (e.g. due to a rename), this script
+# must be updated to track the new name.
+for pat in "${NONE_PATTERNS[@]}"; do
+  if ! git ls-files '*.lean' | xargs grep -qF "$pat" 2>/dev/null; then
+    echo "ERROR: Pattern '$pat' not found in any tracked .lean file."
+    echo "It may have been renamed. Update NONE_PATTERNS in this script."
+    exit 1
+  fi
+done
+
+MERGE_BASE=$(git merge-base HEAD "$BASE_REF" 2>/dev/null || echo "$BASE_REF")
+
+# Build a grep -F pattern file from the array
+GREP_PATTERNS=$(printf '%s\n' "${NONE_PATTERNS[@]}")
+
+# Get all new lines matching any none-pattern (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 -f <(echo "$GREP_PATTERNS") | \
+      grep -v -P -- '-- nosourcerange(-file)?:\s*(?!ok\s*$)\S'; 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 / ExprSourceLoc.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 -qP -- '-- nosourcerange-file:\s*(?!ok\s*$)\S' "$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 occurrences are suppressed."
+  exit 0
+fi
+
+ADDED=$(echo "$FILTERED" | wc -l | tr -d ' ')
+
+# Count removed lines matching any none-pattern from the same diff
+REMOVED=$(git diff "$MERGE_BASE"...HEAD --unified=0 --diff-filter=ACMR -- '*.lean' \
+  | grep -E '^-[^-]' \
+  | grep -cF -f <(echo "$GREP_PATTERNS") || true)
+
+NET=$((ADDED - REMOVED))
+
+if [ "$NET" -gt 0 ]; then
+  echo "ERROR: Net increase of $NET unsuppressed SourceRange.none / ExprSourceLoc.none occurrence(s)."
+  echo "  (added: $ADDED, removed: $REMOVED)"
+  echo ""
+  echo "Each occurrence should either propagate real source metadata or"
+  echo "be suppressed with one of:"
+  echo "  -- nosourcerange: <explanation>       (on the same line)"
+  echo "  -- nosourcerange-file: <explanation>  (anywhere in the file, covers all occurrences)"
+  echo ""
+  echo "The explanation must be non-empty and must not consist solely of \"ok\"."
+  echo ""
+  echo "$FILTERED"
+  exit 1
+fi
+
+echo "OK: No net increase in unsuppressed usage (added: $ADDED, removed: $REMOVED)."

.github/workflows/ci.yml

@@ -43,7 +43,7 @@ jobs:
                 echo "Unsupported architecture: $ARCH"
                 exit 1
               fi
-              wget https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.1/cvc5-Linux-${ARCH_NAME}-static.zip
+              wget --tries=3 --retry-connrefused --waitretry=5 https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.1/cvc5-Linux-${ARCH_NAME}-static.zip
               unzip cvc5-Linux-${ARCH_NAME}-static.zip
               chmod +x cvc5-Linux-${ARCH_NAME}-static/bin/cvc5
               echo "$GITHUB_WORKSPACE/cvc5-Linux-${ARCH_NAME}-static/bin/" >> $GITHUB_PATH
@@ -53,11 +53,11 @@ jobs:
               ARCH=$(uname -m)
               if [ "$ARCH" = "x86_64" ]; then
                 ARCH_NAME="x86_64"
-                wget https://github.com/Z3Prover/z3/releases/download/z3-4.15.2/z3-4.15.2-x64-glibc-2.39.zip
+                wget --tries=3 --retry-connrefused --waitretry=5 https://github.com/Z3Prover/z3/releases/download/z3-4.15.2/z3-4.15.2-x64-glibc-2.39.zip
                 ARCHIVE_NAME="z3-4.15.2-x64-glibc-2.39"
               elif [ "$ARCH" = "aarch64" ] || [ "$ARCH" = "arm64" ]; then
                 ARCH_NAME="arm64"
-                wget https://github.com/Z3Prover/z3/releases/download/z3-4.15.2/z3-4.15.2-arm64-glibc-2.34.zip
+                wget --tries=3 --retry-connrefused --waitretry=5 https://github.com/Z3Prover/z3/releases/download/z3-4.15.2/z3-4.15.2-arm64-glibc-2.34.zip
                 ARCHIVE_NAME="z3-4.15.2-arm64-win"
               else
                 echo "Unsupported architecture: $ARCH"
@@ -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

@@ -694,6 +694,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
 
@@ -720,30 +721,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]
@@ -757,13 +758,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
@@ -772,7 +773,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
@@ -785,13 +786,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
@@ -842,32 +843,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
@@ -876,15 +877,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
@@ -893,37 +894,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