feat(core): Add CoreSMT verification pipeline with incremental solver and diagnosis

.github/workflows/ci.yml

@@ -108,6 +108,7 @@ jobs:
         run: |
           ./run_py_analyze.sh
           ./run_py_analyze.sh laurel
+          ./run_py_analyze.sh --incremental laurel
           python run_py_analyze_sarif.py
           python run_py_analyze_sarif.py --laurel
       - name: Run regex differential tests

Strata/Backends/CBMC/CoreToCBMC.lean

@@ -208,7 +208,8 @@ end
 
 def listToExpr (l: ListMap CoreLabel Core.Procedure.Check) : Core.Expression.Expr :=
   match l with
-  | _ => .true ()
+  -- CBMC does not track source locations; SourceRange.none is used for synthesized expressions.
+  | _ => .true Strata.SourceRange.none
 
 def createContractSymbolFromAST (func : Core.Procedure) : Except String CBMCSymbol := do
   let location : Location := {

Strata/DDM/Util/SourceRange.lean

@@ -25,14 +25,24 @@ structure SourceRange where
   start : String.Pos.Raw
   /-- One past the end of the range. -/
   stop : String.Pos.Raw
-deriving DecidableEq, Inhabited, Repr
+deriving DecidableEq, Inhabited
+
+/-- Compact repr: always displays as `()` to keep debug output readable.
+    Source location info is available via `SourceRange.format`. -/
+instance : Repr SourceRange where
+  reprPrec _ _ := "()"
 
 namespace SourceRange
 
 def none : SourceRange := { start := 0, stop := 0 }
 
 def isNone (loc : SourceRange) : Bool := loc.start = 0 ∧ loc.stop = 0
 
+/-- info: "()" -/
+#guard_msgs in #eval toString (reprPrec (none : SourceRange) 0)
+/-- info: "()" -/
+#guard_msgs in #eval toString (reprPrec ({ start := ⟨5⟩, stop := ⟨10⟩ } : SourceRange) 0)
+
 instance : Std.ToFormat SourceRange where
  format fr := f!"{fr.start}-{fr.stop}"
 

Strata/DL/SMT/SolverInterface.lean

@@ -0,0 +1,110 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.DL.SMT.Solver
+import Strata.DL.SMT.Term
+import Strata.DL.SMT.TermType
+import Strata.DL.SMT.DDMTransform.Translate
+import Strata.Languages.Core.Options
+
+/-!
+# SMT Solver Interface
+
+Abstract interface for SMT solvers using `Strata.SMT.Term` and `Strata.SMT.TermType`.
+Converts to SMT-LIB strings via `SMTDDM.toString` when communicating with solvers.
+
+The interface is a structure (not a type class) to allow runtime selection of
+different solver backends.
+-/
+
+namespace Strata.SMT
+
+open Strata.SMT
+
+/-- Abstract interface for SMT solvers.
+    Uses Strata.SMT.Term which can be converted to SMT-LIB strings via SMTDDM.toString -/
+structure SolverInterface where
+  /-- Push a new scope onto the solver stack -/
+  push : IO Unit
+  /-- Pop the top scope from the solver stack -/
+  pop : IO Unit
+  /-- Declare an uninterpreted sort -/
+  declareSort : String → Nat → IO Unit
+  /-- Declare an uninterpreted function -/
+  declareFun : String → List TermType → TermType → IO Unit
+  /-- Define a function with a body -/
+  defineFun : String → List (String × TermType) → TermType → Term → IO Unit
+  /-- Assert a term -/
+  assert : Term → IO Unit
+  /-- Check satisfiability -/
+  checkSat : IO Decision
+  /-- Check satisfiability with assumptions (check-sat-assuming) -/
+  checkSatAssuming : List Term → IO Decision
+  /-- Get model values for variables -/
+  getModel : List String → IO (List (String × String))
+  /-- Reset the solver state -/
+  reset : IO Unit
+
+/-- Helper to convert Term to SMT-LIB string -/
+private def termToString (t : Term) : Except String String :=
+  Strata.SMTDDM.termToString t
+
+/-- Helper to create an SMTSolverInterface from an initialized Solver -/
+def mkSolverInterfaceFromSolver (solver : Solver) : IO SolverInterface := do
+  let solverRef ← IO.mkRef solver
+  return {
+    push := do
+      let s ← solverRef.get
+      s.smtLibInput.putStr "(push 1)\n"
+      s.smtLibInput.flush
+    pop := do
+      let s ← solverRef.get
+      s.smtLibInput.putStr "(pop 1)\n"
+      s.smtLibInput.flush
+    declareSort := fun name arity => do
+      let _ ← (Solver.declareSort name arity).run (← solverRef.get)
+    declareFun := fun name argTypes retType => do
+      let _ ← (Solver.declareFun name argTypes retType).run (← solverRef.get)
+    defineFun := fun name args retType body => do
+      let _ ← (Solver.defineFunTerm name args retType body).run (← solverRef.get)
+    assert := fun term => do
+      let _ ← (Solver.assert term).run (← solverRef.get)
+    checkSat := do
+      (Solver.checkSat []).run (← solverRef.get) >>= fun (d, _) => pure d
+    checkSatAssuming := fun assumptions => do
+      let s ← solverRef.get
+      let assumptionStrs ← assumptions.mapM fun a =>
+        match termToString a with
+        | .ok str => pure str
+        | .error e => throw (IO.userError s!"Failed to convert term to string: {e}")
+      let assumptionsStr := String.intercalate " " assumptionStrs
+      s.smtLibInput.putStr s!"(check-sat-assuming ({assumptionsStr}))\n"
+      s.smtLibInput.flush
+      match s.smtLibOutput with
+      | .some stdout =>
+        let result := (← stdout.getLine).trimAscii.toString
+        match result with
+        | "sat"     => return .sat
+        | "unsat"   => return .unsat
+        | "unknown" => return .unknown
+        | other     => throw (IO.userError s!"Unrecognized solver output: {other}")
+      | .none => return .unsat  -- Buffer solver: assume proved (no diagnosis)
+    getModel := fun vars => do
+      let s ← solverRef.get
+      let varsStr := String.intercalate " " vars
+      s.smtLibInput.putStr s!"(get-value ({varsStr}))\n"
+      s.smtLibInput.flush
+      match s.smtLibOutput with
+      | .some stdout =>
+        let response ← stdout.getLine
+        return vars.map fun v => (v, response)
+      | .none => return []
+    reset := do
+      let _ ← (Solver.reset).run (← solverRef.get)
+      let _ ← (Solver.setLogic "ALL").run (← solverRef.get)
+  : SolverInterface }
+
+end Strata.SMT

Strata/DL/SMT/State.lean

@@ -0,0 +1,76 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.DL.SMT.SolverInterface
+import Strata.Languages.Core.Expressions
+
+/-!
+# SMT State and Context Management
+
+Defines the SMT solver state and context tracking. The state is returned from
+verify calls to enable reuse across multiple verification sessions.
+-/
+
+namespace Strata.SMT
+
+open Strata.SMT
+
+/-- A context item represents something added to the SMT solver state -/
+inductive ContextItem where
+  /-- An assumed expression (as SMT term) -/
+  | assumption : Term → ContextItem
+  /-- A declared sort (name, arity) -/
+  | sortDecl : String → Nat → ContextItem
+  /-- A declared function (name, arg types, return type) -/
+  | funcDecl : String → List TermType → TermType → ContextItem
+  /-- A defined function (name, args, return type, body) -/
+  | funcDef : String → List (String × TermType) → TermType → Term → ContextItem
+  /-- A declared variable (name, type) -/
+  | varDecl : String → TermType → ContextItem
+  /-- A defined variable (name, type, value) -/
+  | varDef : String → TermType → Term → ContextItem
+
+/-- A scope is a list of context items added at the same push level -/
+abbrev ContextScope := List ContextItem
+
+/-- Context stack: a stack of scopes, where each scope corresponds to a push level.
+    The head of the list is the current (innermost) scope. -/
+abbrev ContextStack := List ContextScope
+
+/-- Verification state that can be reused across calls -/
+structure VerifierState where
+  /-- The SMT solver interface -/
+  solver : SMT.SolverInterface
+  /-- Stack of context scopes (for push/pop support) -/
+  contextStack : ContextStack
+
+/-- Create initial state from a solver interface -/
+def VerifierState.init (solver : SMT.SolverInterface) : VerifierState :=
+  { solver, contextStack := [[]] }
+
+/-- Push a new scope onto the context stack -/
+def VerifierState.push (state : VerifierState) : IO VerifierState := do
+  state.solver.push
+  return { state with contextStack := [] :: state.contextStack }
+
+/-- Pop the top scope from the context stack -/
+def VerifierState.pop (state : VerifierState) : IO VerifierState := do
+  state.solver.pop
+  match state.contextStack with
+  | []          => return state
+  | _ :: rest   => return { state with contextStack := rest }
+
+/-- Add an item to the current scope -/
+def VerifierState.addItem (state : VerifierState) (item : ContextItem) : VerifierState :=
+  match state.contextStack with
+  | []            => { state with contextStack := [[item]] }
+  | scope :: rest => { state with contextStack := (item :: scope) :: rest }
+
+/-- Get all context items (flattened from all scopes) for error reporting -/
+def VerifierState.allContextItems (state : VerifierState) : List ContextItem :=
+  state.contextStack.flatten
+
+end Strata.SMT

Strata/Languages/B3/Format.lean

@@ -0,0 +1,49 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.Languages.B3.DDMTransform.Conversion
+import Strata.Languages.B3.DDMTransform.DefinitionAST
+
+/-!
+# B3 Formatting Utilities
+
+Helper functions for formatting B3 AST nodes to strings using DDM.
+-/
+
+namespace B3
+
+open Strata
+
+/-- Get metadata from B3 expression -/
+def getExpressionMetadata (expr : B3AST.Expression SourceRange) : SourceRange :=
+  match expr with
+  | .literal m _ => m
+  | .id m _ => m
+  | .ite m _ _ _ => m
+  | .binaryOp m _ _ _ => m
+  | .unaryOp m _ _ => m
+  | .functionCall m _ _ => m
+  | .labeledExpr m _ _ => m
+  | .letExpr m _ _ _ => m
+  | .quantifierExpr m _ _ _ _ => m
+
+/-- Format a DDM operation AST node to string -/
+private def formatOp (prog : Program) (op : Operation) : String :=
+  let fmtCtx := FormatContext.ofDialects prog.dialects prog.globalContext {}
+  let fmtState : FormatState := { openDialects := prog.dialects.toList.foldl (init := {}) fun a (dialect : Dialect) => a.insert dialect.name }
+  (mformat (ArgF.op op) fmtCtx fmtState).format.pretty.trimAscii.toString
+
+/-- Format B3 statement to string -/
+def formatStatement (prog : Program) (stmt : B3AST.Statement SourceRange) (ctx : ToCSTContext) : String :=
+  let (cstStmt, _) := B3.stmtToCST ctx stmt
+  formatOp prog cstStmt.toAst
+
+/-- Format B3 expression to string -/
+def formatExpression (prog : Program) (expr : B3AST.Expression SourceRange) (ctx : ToCSTContext) : String :=
+  let (cstExpr, _) := B3.expressionToCST ctx expr
+  formatOp prog cstExpr.toAst
+
+end B3