structure Strata.SMT.Encoder.AbstractEncoderState (τ : Type) : Type

Encoder state for the abstract solver backend. Extends EncoderState with a cache of τ handles for declared variables, so that encodeTerm can look up handles by name instead of requiring a mkVar method on the solver.

• base : EncoderState

  The underlying encoder state (UF name mappings).

• varHandles : Std.HashMap String τ

  Maps declared variable/function names to their solver handles. Populated by encodeUF / declareFun; looked up by encodeTerm.

@[reducible, inline]

abbrev Strata.SMT.Encoder.AbstractEncoderM (τ : Type) (m : Type → Type) (α : Type) : Type

Encoder monad over an abstract solver backend. Parameterized by the underlying monad m and the solver's term type τ so the encoder is not tied to any particular solver backend.

Equations

• Strata.SMT.Encoder.AbstractEncoderM τ m = StateT (Strata.SMT.Encoder.AbstractEncoderState τ) m

@[irreducible]

def Strata.SMT.Encoder.AbstractEncoder.termTypeToSort {τ σ : Type} {m : Type → Type} [Monad m] [MonadExceptOf IO.Error m] (solver : AbstractSolver τ σ m) (ty : TermType) : m σ

Convert a TermType to the solver's sort type σ by dispatching on the sort primitives provided by the solver. This is the sort-level counterpart of encodeTerm: both convert a Strata representation to a solver-native handle by pattern-matching on constructors. Keeping this logic in the encoder (rather than in AbstractSolver) means backends only need to implement the one-liner sort primitives, not a full dispatching method.

Equations

• One or more equations did not get rendered due to their size.
• Strata.SMT.Encoder.AbstractEncoder.termTypeToSort solver (Strata.SMT.TermType.prim Strata.SMT.TermPrimType.bool) = solver.boolSort
• Strata.SMT.Encoder.AbstractEncoder.termTypeToSort solver (Strata.SMT.TermType.prim Strata.SMT.TermPrimType.int) = solver.intSort
• Strata.SMT.Encoder.AbstractEncoder.termTypeToSort solver (Strata.SMT.TermType.prim Strata.SMT.TermPrimType.real) = solver.realSort
• Strata.SMT.Encoder.AbstractEncoder.termTypeToSort solver (Strata.SMT.TermType.prim Strata.SMT.TermPrimType.string) = solver.stringSort
• Strata.SMT.Encoder.AbstractEncoder.termTypeToSort solver (Strata.SMT.TermType.prim Strata.SMT.TermPrimType.regex) = solver.regexSort
• Strata.SMT.Encoder.AbstractEncoder.termTypeToSort solver (Strata.SMT.TermType.prim (Strata.SMT.TermPrimType.bitvec n)) = solver.bitvecSort n
• Strata.SMT.Encoder.AbstractEncoder.termTypeToSort solver (Strata.SMT.TermType.prim Strata.SMT.TermPrimType.trigger) = solver.boolSort
• Strata.SMT.Encoder.AbstractEncoder.termTypeToSort solver inner.option = do let s ← Strata.SMT.Encoder.AbstractEncoder.termTypeToSort solver inner solver.constrSort "Option" [s]

def Strata.SMT.Encoder.AbstractEncoder.encodeUF {τ σ : Type} {m : Type → Type} [Monad m] [MonadExceptOf IO.Error m] (solver : AbstractSolver τ σ m) (uf : UF) : AbstractEncoderM τ m String

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def Strata.SMT.Encoder.AbstractEncoder.encodeTerm {τ σ : Type} {m : Type → Type} [Monad m] [MonadExceptOf IO.Error m] (solver : AbstractSolver τ σ m) (t : Term) : AbstractEncoderM τ m τ

Equations

• One or more equations did not get rendered due to their size.
• Strata.SMT.Encoder.AbstractEncoder.encodeTerm solver (Strata.SMT.Term.prim p) = liftM (solver.mkPrim p)

def Strata.SMT.Encoder.AbstractEncoder.encodeFunctionDef {τ σ : Type} {m : Type → Type} [Monad m] [MonadExceptOf IO.Error m] (solver : AbstractSolver τ σ m) (f : IF) : AbstractEncoderM τ m String

Equations

• One or more equations did not get rendered due to their size.

def Strata.SMT.Encoder.encodeDeclarationsAbstract {m : Type → Type} {τ σ : Type} [Monad m] [MonadExceptOf IO.Error m] (solver : AbstractSolver τ σ m) (ctx : Core.SMT.Context) (prelude : m Unit) (assumptionTerms : List Term) (obligationTerm : Term) (varDefinitions : List Core.VarDefinition := []) (varDeclarations : List Core.VarDeclaration := []) : m (τ × List String × EncoderState)

Encode declarations and assertions through the AbstractSolver API. Replaces encodeDeclarations for the incremental path — all commands go through AbstractSolver methods instead of SolverM.

Parameterized by the solver backend monad m and the solver's term/sort types τ/σ so any implementation of AbstractSolver τ σ m can be used (e.g. incremental SMT-LIB, cvc5 FFI).

prelude is a deferred monadic action (e.g. solver option settings) executed after setLogic but before declarations. The caller constructs it inside the solver session and passes it in as a callback.

Equations

• One or more equations did not get rendered due to their size.

def Strata.SMT.Encoder.encodeCore (ctx : Core.SMT.Context) (prelude : SolverM Unit) (assumptionTerms : List Term) (obligationTerm : Term) (md : Imperative.MetaData Core.Expression) (satisfiabilityCheck validityCheck : Bool) (label : String) (varDefinitions : List Core.VarDefinition := []) (varDeclarations : List Core.VarDeclaration := []) (pctx : Pipeline.PipelineContext) : SolverM (List String × EncoderState)

Encode a verification condition into SMT-LIB format, including check-sat commands. Used by the batch pipeline.

Equations

• One or more equations did not get rendered due to their size.

def Core.SMT.sanitizeFilename (s : String) : String

Replace characters that are problematic on common filesystems (parens, quotes, spaces, path separators, and Windows-invalid characters such as < > : | ? *) with underscores or remove them. Single-pass over the string.

Equations

• One or more equations did not get rendered due to their size.

def Core.SMT.sanitizeFilenameCapped (s : String) (maxLen : Nat := 128) : String

Filesystem-safe filename component derived from an obligation label. First sanitizes illegal characters, then caps length: labels within maxLen pass through unchanged; longer ones are truncated to maxLen characters with a hex hash of the full label appended, so generated filenames stay within NAME_MAX while remaining unique and stable per label. Used only for filename derivation, never for report text.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Core.SMT.Result : Type

Equations

• Core.SMT.Result = Imperative.SMT.Result Core.Expression.Ident

def Core.SMT.getSolverPrelude (solver : String) (solverOptions : Array (String × String)) : Strata.SMT.SolverM Unit

Equations

• One or more equations did not get rendered due to their size.

def Core.SMT.getSolverFlags (options : VerifyOptions) : Array String

Equations

• One or more equations did not get rendered due to their size.

def Core.SMT.dischargeObligation (options : VerifyOptions) (vars : List Expression.TypedIdent) (md : Imperative.MetaData Expression) (filename : String) (assumptionTerms : List Strata.SMT.Term) (obligationTerm : Strata.SMT.Term) (ctx : Context) (satisfiabilityCheck validityCheck : Bool) (label : String) (varDefinitions : List VarDefinition := []) (varDeclarations : List VarDeclaration := []) (termCache : Option (IO.Ref (Std.HashMap Strata.SMT.Term String)) := none) (pctx : Strata.Pipeline.PipelineContext) : IO (Except Imperative.SMT.SolverError (Result × Result × Strata.SMT.EncoderState))

Equations

• One or more equations did not get rendered due to their size.

def Core.SMT.dischargeObligationIncremental (options : VerifyOptions) (vars : List Expression.TypedIdent) (_md : Imperative.MetaData Expression) (assumptionTerms : List Strata.SMT.Term) (obligationTerm : Strata.SMT.Term) (ctx : Context) (satisfiabilityCheck validityCheck : Bool) (_label : String) (varDefinitions : List VarDefinition := []) (varDeclarations : List VarDeclaration := []) : IO (Except Imperative.SMT.SolverError (Result × Result × Strata.SMT.EncoderState))

Discharge a proof obligation using the incremental solver backend. Spawns a live solver process, sends commands via stdin/stdout, and reads results interactively. Returns the same result triple as the batch dischargeObligation.

Equations

• One or more equations did not get rendered due to their size.

def Core.typeCheck (options : VerifyOptions) (program : Program) (moreFns : Lambda.Factory CoreLParams := Lambda.Factory.default) : Except Strata.Message Program

Equations

• One or more equations did not get rendered due to their size.

def Core.formatProofObligation (ob : Imperative.ProofObligation Expression) : Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Core.formatProofObligations (obs : Array (Imperative.ProofObligation Expression)) : Std.Format

Equations

• Core.formatProofObligations obs = Std.Format.joinSep (List.map Core.formatProofObligation obs.toList) (Std.Format.text "\n")

def Core.buildEnv (options : VerifyOptions) (program : Program) (factory : Lambda.Factory CoreLParams) (registerCustomFunctions : Bool := false) : Except Strata.Message (Env × Statistics)

Build an evaluation environment from a program. Loads the factory, datatypes, and processes all declarations. When registerCustomFunctions is true, also loads function declarations, distinct constraints, and local function declarations from procedure bodies into the factory (needed for SMT encoding).

Equations

• One or more equations did not get rendered due to their size.

def Core.generateRecursiveAxioms (tf : Lambda.TypeFactory) (exprEval : Expression.Expr → Expression.Expr) (func : Lambda.LFunc CoreLParams) : Except Strata.Message (Lambda.LFunc CoreLParams)

Pre-compute the per-constructor axioms for a recursive function with a @[cases] parameter and store them in the function's axioms field.

Previously these axioms were generated on the fly inside the SMT encoder (toSMTOp → Lambda.genRecursiveAxioms), which forced the encoder to carry an expression evaluator alongside the factory and datatypes. Generating them here — as part of building the obligation program — lets the encoder consume func.axioms directly and keeps it independent of transient evaluation state.

Non-recursive functions, recursive functions without @[cases] (e.g. int-recursive functions encoded as pure UFs), and functions that already carry these axioms are returned unchanged.

Equations

• One or more equations did not get rendered due to their size.

def Core.toCoreProofObligationProgram (options : VerifyOptions) (program : Program) (moreFns : Lambda.Factory CoreLParams := Lambda.Factory.default) : Except Strata.Message (Program × Statistics)

Proof obligation program construction: Program → Program. Runs symbolic execution and converts obligations to a program suitable for downstream phases (CSE, SMT encoding).

Equations

• One or more equations did not get rendered due to their size.

def Core.typeCheckAndBuildObligationProgram (options : VerifyOptions) (program : Program) (moreFns : Lambda.Factory CoreLParams := Lambda.Factory.default) : Except Strata.Message (Program × Statistics)

Convenience: type check then build obligation program.

Equations

• Core.typeCheckAndBuildObligationProgram options program moreFns = do let program ← Core.typeCheck options program moreFns Core.toCoreProofObligationProgram options program moreFns

def Core.typeCheckAndEval (options : VerifyOptions) (program : Program) (moreFns : Lambda.Factory CoreLParams := Lambda.Factory.default) : Except Strata.Message (List Env × Statistics)

Convenience: type check then symbolic eval. Returns the list of evaluation environments and statistics.

Equations

• One or more equations did not get rendered due to their size.

structure Core.SolverPhaseLog : Type

A solver log entry recording the SMT result after a specific pipeline phase.

• phase : String

  Name of the pipeline phase that produced this entry.

• result : SMT.Result

  The SMT result after this phase's validation.

def Core.instReprSolverPhaseLog.repr : SolverPhaseLog → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Core.instReprSolverPhaseLog : Repr SolverPhaseLog

Equations

• Core.instReprSolverPhaseLog = { reprPrec := Core.instReprSolverPhaseLog.repr }

@[implicit_reducible]

instance Core.instBEqSolverPhaseLog : BEq SolverPhaseLog

Equations

• Core.instBEqSolverPhaseLog = { beq := Core.instBEqSolverPhaseLog.beq }

def Core.instBEqSolverPhaseLog.beq : SolverPhaseLog → SolverPhaseLog → Bool

Equations

• Core.instBEqSolverPhaseLog.beq { phase := a, result := a_1 } { phase := b, result := b_1 } = (a == b && a_1 == b_1)
• Core.instBEqSolverPhaseLog.beq x✝¹ x✝ = false

def Core.AbstractedPhase.validateModel (phases : List AbstractedPhase) (result : SMT.Result) (obligation : Imperative.ProofObligation Expression) : SMT.Result × List SolverPhaseLog

Validate a model against all phases for a given obligation. Phases are recorded top-down, so we reverse them to validate from the last (innermost) phase first. Returns the adjusted result and a log of intermediate results per phase, ordered outermost-first (deepest phase closest to SMT at the end).

Each phase independently validates the model when it has a validator. A phase with modelToValidate can demote .sat m to .unknown (some m) (when the model fails validation) or promote .unknown (some m) back to .sat m (when the model passes validation against the pre-phase semantics). This means phases are not cascading — each validating phase makes its own decision based on the model.

Equations

• One or more equations did not get rendered due to their size.

structure Core.VCOutcome : Type

Analysis outcome of a verification condition based on two SMT queries:

• satisfiabilityProperty: result of checking P ∧ Q (is the property satisfiable given the path condition?)
• validityProperty: result of checking P ∧ ¬Q (can the property be false given the path condition?)

The 9 possible outcomes and their interpretations. For cover statements, any outcome where P ∧ Q is sat displays as ✅ (cover satisfied). Unreachable covers display as ❌ (error) instead of ⛔ (warning).

Emoji Label P ∧ Q P ∧ ¬Q Reachable Deductive BugFinding BugFinding+Complete Meaning

---

✅ always true and is reachable sat unsat yes pass pass pass Property always true, reachable from declaration entry ❌ always false and is reachable unsat sat yes error error error Property always false, reachable from declaration entry 🔶 can be both true and false and is reachable sat sat yes error note error Reachable, solver found models for both the property and its negation ⛔ unreachable in this context unsat unsat no warning error error Dead code, unreachable in this context ➕ can be true and is reachable sat unknown yes error note note Property can be true and is reachable, unknown if always true ✖️ always false if reached unsat unknown unknown error error error Property always false if reached, unknown if reachable ➖ can be false and is reachable unknown sat yes error note error Property can be false and is reachable, unknown if always false ✔️ always true if reached unknown unsat unknown pass pass pass Property always true if reached, unknown if reachable ❓ unknown unknown unknown unknown error note note Both checks inconclusive

• satisfiabilityProperty : SMT.Result
• validityProperty : SMT.Result
• solverLog : Array (Array SolverPhaseLog)

  Ordered log of solver results per path. Each inner array is one path's log: the raw solver results followed by per-phase adjusted results (e.g. sat→unknown when a phase cannot validate the model). When outcomes from multiple paths are merged, each path's log is preserved as a separate entry in the outer array. Consumed by future diagnostic and traceability tooling.

• mergedFrom : Array VCOutcome

  When this outcome was produced by merging multiple paths, stores the pre-merge per-path outcomes. Empty for unmerged (single-path) results. Used by the rendering phase to compute per-path classification summaries without storing rendering-mode-dependent strings.

@[implicit_reducible]

instance Core.instReprVCOutcome : Repr VCOutcome

Equations

• Core.instReprVCOutcome = { reprPrec := Core.instReprVCOutcome.repr }

partial def Core.instReprVCOutcome.repr : VCOutcome → Nat → Std.Format

@[implicit_reducible]

instance Core.instInhabitedVCOutcome : Inhabited VCOutcome

Equations

• Core.instInhabitedVCOutcome = { default := { satisfiabilityProperty := Imperative.SMT.Result.unknown, validityProperty := Imperative.SMT.Result.unknown } }

def Core.VCOutcome.passAndReachable (o : VCOutcome) : Bool

Equations

• o.passAndReachable = match o.satisfiabilityProperty, o.validityProperty with | Imperative.SMT.Result.sat model, Imperative.SMT.Result.unsat => true | x, x_1 => false

def Core.VCOutcome.alwaysFalseAndReachable (o : VCOutcome) : Bool

Equations

• o.alwaysFalseAndReachable = match o.satisfiabilityProperty, o.validityProperty with | Imperative.SMT.Result.unsat, Imperative.SMT.Result.sat model => true | x, x_1 => false

def Core.VCOutcome.canBeTrueOrFalseAndIsReachable (o : VCOutcome) : Bool

Equations

• o.canBeTrueOrFalseAndIsReachable = match o.satisfiabilityProperty, o.validityProperty with | Imperative.SMT.Result.sat model, Imperative.SMT.Result.sat model_1 => true | x, x_1 => false

def Core.VCOutcome.unreachable (o : VCOutcome) : Bool

Equations

• o.unreachable = match o.satisfiabilityProperty, o.validityProperty with | Imperative.SMT.Result.unsat, Imperative.SMT.Result.unsat => true | x, x_1 => false

def Core.VCOutcome.satisfiableValidityUnknown (o : VCOutcome) : Bool

Equations

• o.satisfiableValidityUnknown = match o.satisfiabilityProperty, o.validityProperty with | Imperative.SMT.Result.sat model, Imperative.SMT.Result.unknown candidateModel => true | x, x_1 => false

def Core.VCOutcome.alwaysFalseReachabilityUnknown (o : VCOutcome) : Bool

Equations

• o.alwaysFalseReachabilityUnknown = match o.satisfiabilityProperty, o.validityProperty with | Imperative.SMT.Result.unsat, Imperative.SMT.Result.unknown candidateModel => true | x, x_1 => false

def Core.VCOutcome.canBeFalseAndIsReachable (o : VCOutcome) : Bool

Equations

• o.canBeFalseAndIsReachable = match o.satisfiabilityProperty, o.validityProperty with | Imperative.SMT.Result.unknown candidateModel, Imperative.SMT.Result.sat model => true | x, x_1 => false

def Core.VCOutcome.passReachabilityUnknown (o : VCOutcome) : Bool

Equations

• o.passReachabilityUnknown = match o.satisfiabilityProperty, o.validityProperty with | Imperative.SMT.Result.unknown candidateModel, Imperative.SMT.Result.unsat => true | x, x_1 => false

def Core.VCOutcome.unknown (o : VCOutcome) : Bool

Equations

• o.unknown = match o.satisfiabilityProperty, o.validityProperty with | Imperative.SMT.Result.unknown candidateModel, Imperative.SMT.Result.unknown candidateModel_1 => true | x, x_1 => false

def Core.VCOutcome.hasSMTError (o : VCOutcome) : Bool

True when either SMT property is .err (solver returned an error on a specific check, as opposed to the outer VCResult.outcome being .error due to an encoding failure).

Equations

• o.hasSMTError = match o.satisfiabilityProperty, o.validityProperty with | Imperative.SMT.Result.err msg, x => true | x, Imperative.SMT.Result.err msg => true | x, x_1 => false

def Core.VCOutcome.isPass (o : VCOutcome) : Bool

The assertion's validity is proven (validity = unsat). True for passAndReachable, unreachable, and passReachabilityUnknown. Note: this does NOT distinguish reachable passes from unreachable (dead-code) passes.

Equations

• o.isPass = match o.validityProperty with | Imperative.SMT.Result.unsat => true | x => false

def Core.VCOutcome.isSatisfiable (o : VCOutcome) : Bool

The assertion can be true (satisfiability = sat). True for passAndReachable, canBeTrueOrFalseAndIsReachable, and satisfiableValidityUnknown.

Equations

• o.isSatisfiable = match o.satisfiabilityProperty with | Imperative.SMT.Result.sat model => true | x => false

def Core.VCOutcome.isAlwaysFalse (o : VCOutcome) : Bool

Equations

• o.isAlwaysFalse = (o.alwaysFalseAndReachable || o.alwaysFalseReachabilityUnknown)

def Core.VCOutcome.isAlwaysTrue (o : VCOutcome) : Bool

Equations

• o.isAlwaysTrue = o.isPass

def Core.VCOutcome.isReachable (o : VCOutcome) : Bool

Equations

• o.isReachable = (o.passAndReachable || o.alwaysFalseAndReachable || o.canBeTrueOrFalseAndIsReachable)

def Core.VCOutcome.bugFindingSuccess (o : VCOutcome) : Bool

Success in bug-finding mode: the assertion is satisfiable (can be true on some reachable path), or provably always true with unknown reachability. Does NOT include unreachable paths — dead code in agent-generated code is worth flagging as a potential issue.

Equations

• o.bugFindingSuccess = (o.isSatisfiable || o.passReachabilityUnknown)

def Core.VCOutcome.bugFindingFailure (o : VCOutcome) : Bool

Failure in bug-finding mode: the assertion is always false (a definite bug), or the path is unreachable (dead code).

Equations

• o.bugFindingFailure = (o.alwaysFalseAndReachable || o.alwaysFalseReachabilityUnknown || o.unreachable)

def Core.VCOutcome.isPassAndReachable (o : VCOutcome) : Bool

Equations

• Core.VCOutcome.isPassAndReachable = Core.VCOutcome.passAndReachable

def Core.VCOutcome.isRefutedAndReachable (o : VCOutcome) : Bool

Equations

• Core.VCOutcome.isRefutedAndReachable = Core.VCOutcome.alwaysFalseAndReachable

def Core.VCOutcome.isCanBeTrueOrFalseAndIsReachable (o : VCOutcome) : Bool

Equations

• Core.VCOutcome.isCanBeTrueOrFalseAndIsReachable = Core.VCOutcome.canBeTrueOrFalseAndIsReachable

def Core.VCOutcome.isUnreachable (o : VCOutcome) : Bool

Equations

• Core.VCOutcome.isUnreachable = Core.VCOutcome.unreachable

def Core.VCOutcome.isSatisfiableValidityUnknown (o : VCOutcome) : Bool

Equations

• Core.VCOutcome.isSatisfiableValidityUnknown = Core.VCOutcome.satisfiableValidityUnknown

def Core.VCOutcome.isAlwaysFalseReachabilityUnknown (o : VCOutcome) : Bool

Equations

• Core.VCOutcome.isAlwaysFalseReachabilityUnknown = Core.VCOutcome.alwaysFalseReachabilityUnknown

def Core.VCOutcome.isCanBeFalseAndReachable (o : VCOutcome) : Bool

Equations

• Core.VCOutcome.isCanBeFalseAndReachable = Core.VCOutcome.canBeFalseAndIsReachable

def Core.VCOutcome.isPassReachabilityUnknown (o : VCOutcome) : Bool

Equations

• Core.VCOutcome.isPassReachabilityUnknown = Core.VCOutcome.passReachabilityUnknown

def Core.VCOutcome.isUnknown (o : VCOutcome) : Bool

Equations

• Core.VCOutcome.isUnknown = Core.VCOutcome.unknown

def Core.VCOutcome.isRefuted (o : VCOutcome) : Bool

Equations

• Core.VCOutcome.isRefuted = Core.VCOutcome.alwaysFalseAndReachable

def Core.VCOutcome.isRefutedIfReachable (o : VCOutcome) : Bool

Equations

• Core.VCOutcome.isRefutedIfReachable = Core.VCOutcome.alwaysFalseReachabilityUnknown

def Core.VCOutcome.isCanBeTrueOrFalse (o : VCOutcome) : Bool

Equations

• Core.VCOutcome.isCanBeTrueOrFalse = Core.VCOutcome.canBeTrueOrFalseAndIsReachable

def Core.VCOutcome.isAlwaysTrueIfReachable (o : VCOutcome) : Bool

Equations

• Core.VCOutcome.isAlwaysTrueIfReachable = Core.VCOutcome.passReachabilityUnknown

def Core.VCOutcome.isPassIfReachable (o : VCOutcome) : Bool

Equations

• Core.VCOutcome.isPassIfReachable = Core.VCOutcome.passReachabilityUnknown

def Core.VCOutcome.isAlwaysFalseIfReachable (o : VCOutcome) : Bool

Equations

• Core.VCOutcome.isAlwaysFalseIfReachable = Core.VCOutcome.alwaysFalseReachabilityUnknown

def Core.VCOutcome.isReachableAndCanBeFalse (o : VCOutcome) : Bool

Equations

• Core.VCOutcome.isReachableAndCanBeFalse = Core.VCOutcome.canBeFalseAndIsReachable

def Core.VCOutcome.label (o : VCOutcome) (property : Imperative.PropertyType) (checkLevel : CheckLevel) (checkMode : VerificationMode) : String

Equations

• One or more equations did not get rendered due to their size.

def Core.VCOutcome.emoji (o : VCOutcome) (property : Imperative.PropertyType) (checkLevel : CheckLevel) (checkMode : VerificationMode) : String

Equations

• One or more equations did not get rendered due to their size.

def Core.VCOutcome.pathSummary (o : VCOutcome) (property : Imperative.PropertyType) (checkLevel : CheckLevel) (checkMode : VerificationMode) : String

Compute a per-path classification summary for a merged outcome. Returns a parenthesized string like "(always true if reached on 1 path, always false if reached on 1 path)" when the merged result differs from individual paths. Returns the empty string for unmerged results or when all paths have the same classification as the merged result.

Equations

• One or more equations did not get rendered due to their size.

def Core.SMT.Result.merge (a b : Result) : Result

Merge two SMT results, where err dominates sat dominates unknown dominates unsat. If either result is an error, the merged result is an error. If either result is sat, the merged result is sat (keeping the first model). If either is unknown, the merged result is unknown. Only if both are unsat is the merged result unsat.

Equations

• Core.SMT.Result.merge (Imperative.SMT.Result.err e) b = Imperative.SMT.Result.err e
• a.merge (Imperative.SMT.Result.err e) = Imperative.SMT.Result.err e
• Core.SMT.Result.merge (Imperative.SMT.Result.sat m) b = Imperative.SMT.Result.sat m
• a.merge (Imperative.SMT.Result.sat m) = Imperative.SMT.Result.sat m
• Core.SMT.Result.merge (Imperative.SMT.Result.unknown m) b = Imperative.SMT.Result.unknown m
• a.merge (Imperative.SMT.Result.unknown m) = Imperative.SMT.Result.unknown m
• Core.SMT.Result.merge Imperative.SMT.Result.unsat Imperative.SMT.Result.unsat = Imperative.SMT.Result.unsat

def Core.VCOutcome.merge (a b : VCOutcome) : VCOutcome

Merge two VCOutcomes from different paths to the same assertion. For each SMT check (satisfiability and validity), sat dominates: if the assertion is satisfiable on any path, the merged result is sat. Each path's solverLog is preserved as a separate entry. Pre-merge per-path outcomes are stored in mergedFrom for rendering.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Core.LExprModel : Type

A model with values lifted to LExpr for display purposes. This is used for formatting models in a human-readable way using Core's expression formatter and for future use as program metadata.

Equations

• Core.LExprModel = List (Core.Expression.Ident × Lambda.LExpr Core.CoreLParams.mono)

def Core.LExprModel.format (model : LExprModel) : Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Core.LExprModel.format [] = Std.Format.text ""
• Core.LExprModel.format [(id, e)] = Std.format "(" ++ Std.format id ++ Std.format ", " ++ Std.format (Core.formatModelValue✝ e) ++ Std.format ")"

@[implicit_reducible]

instance Core.instToFormatLExprModel : Std.ToFormat LExprModel

Equations

• Core.instToFormatLExprModel = { format := Core.LExprModel.format }

inductive Core.VCError : Type

Classifies errors that prevent a verification condition from being resolved.

• encoding (msg : String) : VCError
• solverTimeout (msg : String) : VCError
• solverCrash (msg : String) : VCError

@[implicit_reducible]

instance Core.instReprVCError : Repr VCError

Equations

• Core.instReprVCError = { reprPrec := Core.instReprVCError.repr }

def Core.instReprVCError.repr : VCError → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Core.instBEqVCError : BEq VCError

Equations

• Core.instBEqVCError = { beq := Core.instBEqVCError.beq }

def Core.instBEqVCError.beq : VCError → VCError → Bool

Equations

• Core.instBEqVCError.beq (Core.VCError.encoding a) (Core.VCError.encoding b) = (a == b)
• Core.instBEqVCError.beq (Core.VCError.solverTimeout a) (Core.VCError.solverTimeout b) = (a == b)
• Core.instBEqVCError.beq (Core.VCError.solverCrash a) (Core.VCError.solverCrash b) = (a == b)
• Core.instBEqVCError.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Core.instToStringVCError : ToString VCError

Equations

• One or more equations did not get rendered due to their size.

structure Core.VCResult : Type

A collection of all information relevant to a verification condition's analysis.

• obligation : Imperative.ProofObligation Expression
• outcome : Except VCError VCOutcome
• estate : Strata.SMT.EncoderState
• verbose : VerboseMode
• checkLevel : CheckLevel
• checkMode : VerificationMode
• lexprModel : LExprModel

  model with values converted from SMT.Term to Core LExpr. The contents must be consistent with the outcome, if the outcome was a failure.

def Core.maskOutcome (outcome : VCOutcome) (satisfiabilityCheck validityCheck : Bool) : VCOutcome

Mask outcome properties that were not requested. When the evaluator resolves a check that wasn't requested by the check mode/level, we set it to .unknown so the label function displays the appropriate message for the checks that were actually requested. For example, in minimal deductive mode we only request validity, so if evaluator also determined satisfiability, we mask it to .unknown.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Core.instToFormatVCResult : Std.ToFormat VCResult

Equations

• One or more equations did not get rendered due to their size.

def Core.VCResult.formatOutcome (r : VCResult) : String

Compact single-line outcome string: emoji + label (e.g. "✅ pass", "❌ fail"). Uses the property, check level, and check mode stored in the result.

Equations

• One or more equations did not get rendered due to their size.

def Core.VCResult.isSuccess (vr : VCResult) : Bool

Deductive-mode success: the assertion's validity is proven (isPass). Includes unreachable paths (vacuously true). For bug-finding mode, use isBugFindingSuccess instead.

Equations

• vr.isSuccess = match vr.outcome with | Except.ok o => o.isPass | Except.error a => false

def Core.VCResult.isFailure (vr : VCResult) : Bool

Deductive-mode failure: the assertion can be false on some reachable path. For bug-finding mode, use isBugFindingFailure instead.

Equations

• One or more equations did not get rendered due to their size.

def Core.VCResult.isUnknown (vr : VCResult) : Bool

Equations

• vr.isUnknown = match vr.outcome with | Except.ok o => o.isUnknown | Except.error a => false

def Core.VCResult.isImplementationError (vr : VCResult) : Bool

Equations

• vr.isImplementationError = match vr.outcome with | Except.error (Core.VCError.encoding msg) => true | Except.error (Core.VCError.solverCrash msg) => true | x => false

def Core.VCResult.isTimeout (vr : VCResult) : Bool

Equations

• vr.isTimeout = match vr.outcome with | Except.error (Core.VCError.solverTimeout msg) => true | x => false

def Core.VCResult.isNotSuccess (vcResult : VCResult) : Bool

Equations

• vcResult.isNotSuccess = !vcResult.isSuccess

def Core.VCResult.isUnreachable (vr : VCResult) : Bool

Equations

• vr.isUnreachable = match vr.outcome with | Except.ok o => o.unreachable | Except.error a => false

def Core.VCResult.isBugFindingSuccess (vr : VCResult) : Bool

Equations

• vr.isBugFindingSuccess = match vr.outcome with | Except.ok o => o.bugFindingSuccess | Except.error a => false

def Core.VCResult.isBugFindingFailure (vr : VCResult) : Bool

Equations

• vr.isBugFindingFailure = match vr.outcome with | Except.ok o => o.bugFindingFailure | Except.error a => false

def Core.VCResult.hasSMTError (vr : VCResult) : Bool

True when either SMT property inside a successful outcome is .err. Complements isImplementationError, which covers the outer .error case.

Equations

• vr.hasSMTError = match vr.outcome with | Except.ok o => o.hasSMTError | Except.error a => false

@[reducible, inline]

abbrev Core.VCResults : Type

Equations

• Core.VCResults = Array Core.VCResult

def Core.VCResults.format (rs : VCResults) : Std.Format

Equations

• rs.format = Std.Format.joinSep (Array.map (fun (r : Core.VCResult) => Std.format Std.Format.line ++ Std.format r) rs).toList Std.Format.line

@[implicit_reducible]

instance Core.instToFormatVCResults : Std.ToFormat VCResults

Equations

• Core.instToFormatVCResults = { format := Core.VCResults.format }

@[implicit_reducible]

instance Core.instToStringVCResults : ToString VCResults

Equations

• Core.instToStringVCResults = { toString := fun (rs : Core.VCResults) => toString rs.format }

def Core.VCResult.merge (a b : VCResult) : VCResult

Merge two VCResults from different paths to the same assertion. Outcomes are merged at the VCOutcome level (sat dominates). The first result's obligation metadata is preserved. The model from the result with a sat outcome is preferred.

Equations

• One or more equations did not get rendered due to their size.

def Core.VCResults.mergeByAssertion (rs : VCResults) : VCResults

Merge VCResults that originate from the same assertion (identified by source location + related locations from inlining). Outcomes are merged at the VCOutcome level: if a proposition is sat on any path, the merged result is sat. Preserves first-occurrence order. When the file range is unknown, each VCResult is kept as-is.

Equations

• One or more equations did not get rendered due to their size.

def Core.preprocessObligation (obligation : Imperative.ProofObligation Expression) (p : Program) (options : VerifyOptions) (satisfiabilityCheck validityCheck : Bool) (axiomCache : Option IrrelevantAxioms.Cache := none) (axiomNames : List String := []) (axiomProgram : Option Program := none) : EIO Strata.Message (Imperative.ProofObligation Expression × Option SMT.Result × Option SMT.Result)

Preprocess a proof obligation using symbolic simulation. Returns the symbolic results for satisfiability and validity independently. Each result is some r if evaluator can determine it, none if the solver is needed.

Equations

• One or more equations did not get rendered due to their size.

def Core.transformPipelinePhases (procs : Option (List String) := none) : List PipelinePhase

The Core verification pipeline phases. Each entry pairs a program transformation with its per-obligation model validation. The pipeline extracts transforms from this list, and the validation extracts phases, ensuring they stay in sync.

Call elimination always runs as a standalone program-to-program pass. When procs is provided (targeted verification), the pipeline also includes filtering and post-transform filter phases. All filter phases are model-preserving since they only remove information without introducing over-approximations.

A second FilterProcedures pass runs after CallElim and PrecondElim to prune any procedures that became unreachable after transforms. This pass explicitly lists the target procedures and their WF procedures (via PrecondElim.wfProcName) as targets, and disables noFilter so that WF procedures for prelude functions are correctly pruned.

loopElimPipelinePhase is placed last because loop elimination happens during evaluation (not as a program-to-program pass), making it the closest phase to SMT.

Equations

• One or more equations did not get rendered due to their size.

def Core.typeCheckPipelinePhase (options : VerifyOptions := VerifyOptions.default) (moreFns : Lambda.Factory CoreLParams := Lambda.Factory.default) : PipelinePhase

Type-checking pipeline phase: runs Core.typeCheck on the program.

Equations

• One or more equations did not get rendered due to their size.

def Core.symbolicEvalPipelinePhase (options : VerifyOptions := VerifyOptions.default) (moreFns : Lambda.Factory CoreLParams := Lambda.Factory.default) : PipelinePhase

Symbolic-evaluation pipeline phase: partially evaluates the program into the passive proof-obligation form consumed by obligation extraction.

Equations

• One or more equations did not get rendered due to their size.

def Core.corePipelinePhases (procs : Option (List String) := none) (options : VerifyOptions := VerifyOptions.default) (moreFns : Lambda.Factory CoreLParams := Lambda.Factory.default) : List PipelinePhase

The full pipeline phases for program-to-program transforms, including type checking, symbolic evaluation, and common subexpression elim. CSE runs after symbolic evaluation to extract common subexpressions introduced by partial evaluation inlining; it is model-preserving (skipping it via options.disableCSE is sound, though solver outcomes may differ on individual obligations).

Equations

• One or more equations did not get rendered due to their size.

def Core.coreAbstractedPhases (procs : Option (List String) := none) (options : VerifyOptions := VerifyOptions.default) (moreFns : Lambda.Factory CoreLParams := Lambda.Factory.default) : List AbstractedPhase

The abstracted phases derived from the Core pipeline phases.

Must be called with the same procs/options as the corresponding corePipelinePhases run: the phase list's membership is options-dependent (disableCSE), so a list computed with different options describes phases that did not actually run.

Equations

• Core.coreAbstractedPhases procs options moreFns = List.map (fun (x : Core.PipelinePhase) => x.phase) (Core.corePipelinePhases procs options moreFns)

def Core.SMT.Result.adjustForPhases (r : Result) (phases : List AbstractedPhase) (obligation : Imperative.ProofObligation Expression) : Result × List SolverPhaseLog

Adjust an SMT result through pipeline phase validation. A .sat result may be demoted to .unknown if a phase cannot validate the model, and an .unknown result may be promoted back to .sat if a phase can validate the model. Returns the adjusted result and a log of intermediate results per phase.

Equations

• One or more equations did not get rendered due to their size.
• Core.SMT.Result.adjustForPhases (Imperative.SMT.Result.sat model) phases obligation = Core.AbstractedPhase.validateModel phases (Imperative.SMT.Result.sat model) obligation
• r.adjustForPhases phases obligation = (r, [])

@[reducible, inline]

abbrev Core.DischargeFn : Type

A discharge function encapsulates the solver backend. It takes assumption terms, the obligation term, the SMT context, and the satisfiability/validity check flags, and returns the solver results. The pipeline is parametrized by this function so it does not know about SMT-LIB or any specific solver.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Core.CoreSMTSolver : Type

A CoreSMTSolver encapsulates the strategy for discharging all proof obligations extracted from a CoreSMT program. The pipeline is parametrized by this function so that the solver backend can be swapped — e.g. for a parallel solver that dispatches obligations concurrently, or an incremental solver that shares path-condition state across assertions.

The solver receives the fully-built factory (Core's built-ins plus any custom functions from external phases, e.g. RuntimeFactory, already threaded through the transformation pipeline) and the obligation program (in CoreSMT format after all pipeline transformations), and returns verification results together with statistics. Because the factory is already complete, a custom solver must pass it to buildEnv as-is and must NOT call Core.Factory.addFactory on it — doing so would re-add Core's built-ins and fail with duplicate-function errors.

Equations

• Core.CoreSMTSolver = (Lambda.Factory Core.CoreLParams → Core.Program → EIO Strata.Message (Core.VCResults × Statistics))

@[reducible, inline]

abbrev Core.MkDischargeFn : Type

Factory for discharge functions. Called once per obligation with the obligation's typed variables, metadata, and label. A custom implementation can replace the default (batch/incremental SMT-LIB) backend.

Equations

• One or more equations did not get rendered due to their size.

def Core.mkDischargeFn : MkDischargeFn

Construct a DischargeFn from verification options. Selects the incremental (abstract solver) backend or the batch (SMT-LIB file) backend based on options.incremental and options.alwaysGenerateSMT.

Equations

• One or more equations did not get rendered due to their size.

def Core.getObligationResult (assumptionTerms : List Strata.SMT.Term) (obligationTerm : Strata.SMT.Term) (ctx : SMT.Context) (obligation : Imperative.ProofObligation Expression) (p : Program) (options : VerifyOptions) (discharge : DischargeFn) (satisfiabilityCheck validityCheck : Bool) (phases : List AbstractedPhase) (varDefinitions : List VarDefinition := []) (varDeclarations : List VarDeclaration := []) : EIO Strata.Message VCResult

Invoke a backend engine and get the analysis result for a given proof obligation.

Equations

• One or more equations did not get rendered due to their size.

def Core.mkDefaultCoreSMTSolver (options : VerifyOptions) (counter : IO.Ref Nat) (tempDir : System.FilePath) (axiomCache : Option IrrelevantAxioms.Cache := none) (axiomNames : List String := []) (axiomProgram : Option Program := none) (externalPhases : List AbstractedPhase := []) (corePhases : List AbstractedPhase := coreAbstractedPhases) (mkDischarge : MkDischargeFn := mkDischargeFn) (pctx : Strata.Pipeline.PipelineContext) : CoreSMTSolver

Construct the default CoreSMTSolver that discharges obligations sequentially using the batch or incremental SMT-LIB backend (selected by options.incremental). This is the standard solver used by verify when no custom solver is provided.

Equations

• One or more equations did not get rendered due to their size.

def Core.verify (program : Program) (tempDir : System.FilePath) (proceduresToVerify : Option (List String) := none) (options : VerifyOptions := VerifyOptions.default) (moreFns : Lambda.Factory CoreLParams := Lambda.Factory.default) (externalPhases : List AbstractedPhase := []) (prefixPhases : List PipelinePhase := []) (solver : Option CoreSMTSolver := none) (mkDischarge : MkDischargeFn := mkDischargeFn) (pipelineCtx : Option Strata.Pipeline.PipelineContext := none) : EIO Strata.Message VCResults

Run the Strata Core verification pipeline on a program: transform, type-check, partially evaluate, and discharge proof obligations via SMT. All program-wide transformations that occur before any analyses (including type inference) should be placed here.

When options.keepAllFilesPrefix is set, the program state after each pipeline phase is written to {prefix}.{n}.{phaseName}.core.st (numbered from 1).

When pipelineCtx is provided, its outputMode — not options.profile — drives all profiling output. Callers that want profiling should supply a context whose outputMode showsProfiling; options.profile only decides the outputMode of the context created internally when pipelineCtx is none.

Equations

• One or more equations did not get rendered due to their size.

def Strata.typeCheck (ictx : Lean.Parser.InputContext) (env : StrataDDM.Program) (options : Core.VerifyOptions := Core.VerifyOptions.default) (moreFns : Lambda.Factory Core.CoreLParams := Lambda.Factory.default) : Except Message Core.Program

Equations

• One or more equations did not get rendered due to their size.

def Strata.Core.getProgram (p : StrataDDM.Program) (ictx : Lean.Parser.InputContext := default) : Core.Program × Array String

Equations

• Strata.Core.getProgram p ictx = Strata.TransM.run ictx (Strata.translateProgram p)

def Strata.toMessage (vcr : Core.VCResult) (phases : List Core.AbstractedPhase := []) : Option Message

Equations

• One or more equations did not get rendered due to their size.

structure Strata.Diagnostic : Type

• start : Lean.Position
• ending : Lean.Position
• message : String
• type : MessageKind

def Strata.instReprDiagnostic.repr : Diagnostic → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Strata.instReprDiagnostic : Repr Diagnostic

Equations

• Strata.instReprDiagnostic = { reprPrec := Strata.instReprDiagnostic.repr }

def Strata.instBEqDiagnostic.beq : Diagnostic → Diagnostic → Bool

Equations

• One or more equations did not get rendered due to their size.
• Strata.instBEqDiagnostic.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Strata.instBEqDiagnostic : BEq Diagnostic

Equations

• Strata.instBEqDiagnostic = { beq := Strata.instBEqDiagnostic.beq }

@[implicit_reducible]

instance Strata.instToExprDiagnostic : Lean.ToExpr Diagnostic

Equations

• Strata.instToExprDiagnostic = { toExpr := Strata.instToExprDiagnostic.toExpr, toTypeExpr := Lean.Expr.const `Strata.Diagnostic [] }

def Strata.instToExprDiagnostic.toExpr : Diagnostic → Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def Strata.Pipeline.Message.toDiagnostic (files : Map Uri Lean.FileMap) (dm : Message) : Diagnostic

Equations

• One or more equations did not get rendered due to their size.