strata-org · MikaelMayer · Apr 28, 2026 · Apr 28, 2026 · Apr 28, 2026 · Apr 28, 2026
@@ -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 := {

@@ -25,10 +25,11 @@ 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, DecidableEq, BEq
 
 namespace SourceRange
 
+@[expose]
 def none : SourceRange := { start := 0, stop := 0 }
 
 def isNone (loc : SourceRange) : Bool := loc.start = 0 ∧ loc.stop = 0

@@ -49,6 +49,9 @@ class HasBool (P : PureExpr) where
   ff : P.Expr
   tt_is_not_ff: tt ≠ ff
   boolTy : P.Ty
+  /-- Check if an expression represents `true`. Defaults to `e == tt` but
+      implementations may override to ignore metadata. -/
+  isTt : [BEq P.Expr] → P.Expr → Bool := fun e => e == tt
 
 class HasNot (P : PureExpr) extends HasBool P where
   not : P.Expr → P.Expr

@@ -61,7 +61,7 @@ def runStep [BEq P.Expr] [HasBool P]
     | .det e =>
       match ops.evalExpr ρ e with
       | some v =>
-        if v == HasBool.tt then .stmts tss ρ
+        if HasBool.isTt v then .stmts tss ρ
         else .stmts ess ρ
       | none => .terminal (ops.addError ρ "ITE condition did not reduce to bool")
 
@@ -71,7 +71,7 @@ def runStep [BEq P.Expr] [HasBool P]
     | .det g =>
       match ops.evalExpr ρ g with
       | some v =>
-        if v == HasBool.tt then .stmts (body ++ [s]) ρ
+        if HasBool.isTt v then .stmts (body ++ [s]) ρ
         else .terminal ρ
       | none => .terminal (ops.addError ρ "Loop guard did not reduce to bool")
 

@@ -231,6 +231,21 @@ instance {T: LExprParamsT} [DecidableEq T.base.Metadata] [DecidableEq T.TypeType
     else
       isFalse (fun heq => h (LExpr.beq_eq e1 e2 |>.mpr heq))
 
+/-- Structural equality ignoring metadata fields. Does not allocate intermediate expressions. -/
+def LExpr.beqIgnoringMetadata [BEq T.TypeType] [BEq (Identifier T.base.IDMeta)] : LExpr T → LExpr T → Bool
+  | .const _ c1, .const _ c2 => c1 == c2
+  | .op _ o1 ty1, .op _ o2 ty2 => o1 == o2 && ty1 == ty2
+  | .bvar _ i1, .bvar _ i2 => i1 == i2
+  | .fvar _ n1 ty1, .fvar _ n2 ty2 => n1 == n2 && ty1 == ty2
+  | .abs _ name1 ty1 e1, .abs _ name2 ty2 e2 => name1 == name2 && ty1 == ty2 && beqIgnoringMetadata e1 e2
+  | .quant _ k1 name1 ty1 tr1 e1, .quant _ k2 name2 ty2 tr2 e2 =>
+    k1 == k2 && name1 == name2 && ty1 == ty2 && beqIgnoringMetadata tr1 tr2 && beqIgnoringMetadata e1 e2
+  | .app _ fn1 e1, .app _ fn2 e2 => beqIgnoringMetadata fn1 fn2 && beqIgnoringMetadata e1 e2
+  | .ite _ c1 t1 f1, .ite _ c2 t2 f2 =>
+    beqIgnoringMetadata c1 c2 && beqIgnoringMetadata t1 t2 && beqIgnoringMetadata f1 f2
+  | .eq _ e1a e1b, .eq _ e2a e2b => beqIgnoringMetadata e1a e2a && beqIgnoringMetadata e1b e2b
+  | _, _ => false
+
 def LExpr.noTrigger {T : LExprParamsT} (m : T.base.Metadata) : LExpr T := .bvar m 0
 def LExpr.allTr {T : LExprParamsT} (m : T.base.Metadata) (name : String) (ty : Option T.TypeType) := @LExpr.quant T m .all name ty
 def LExpr.all {T : LExprParamsT} (m : T.base.Metadata) (name : String) (ty : Option T.TypeType) := @LExpr.quant T m .all name ty (LExpr.noTrigger m)
@@ -694,6 +709,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 +736,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 +773,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 +788,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 +801,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 +858,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 +892,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 +909,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

@@ -74,7 +74,7 @@ def Scope.merge (cond : LExpr T.mono) (m1 m2 : Scope T) : Scope T :=
         (k, (ty1, mkIte cond e1 e2)) ::
       Scope.merge cond rest (m2.erase k)
   where mkIte (cond tru fals : LExpr T.mono) : LExpr T.mono :=
-    if tru == fals then tru
+    if tru.beqIgnoringMetadata fals then tru
     else (LExpr.ite (default : T.Metadata) cond tru fals)