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 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.emitDatatypesAbstract {m : Type → Type} {τ σ : Type} [Monad m] [MonadExceptOf IO.Error m] (solver : AbstractSolver τ σ m) (ctx : Core.SMT.Context) : m Unit

Emit datatype declarations through the AbstractSolver API.

Equations

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

def Strata.SMT.Encoder.declareContextAbstract {m : Type → Type} {τ σ : Type} [Monad m] [MonadExceptOf IO.Error m] (solver : AbstractSolver τ σ m) (ctx : Core.SMT.Context) (sorts : List DL.SMT.Sort) (datatypes : Std.HashSet String) (ufs : List UF) (ifs : List IF) (axms : List Term) (managed : Std.HashSet String) : AbstractEncoderM τ m Unit

Send part of an encoding context to a solver: the given sorts, datatypes, uninterpreted and defined functions, and axioms, in that order: sorts come first since a datatype's constructors may mention them (a heap holds a Map). A one-shot solve sends the whole context; a long-lived session sends only what it has not sent before.

A sort that ctx declares as a datatype is left to the datatype declaration, since strict solver APIs (e.g. cvc5 FFI) reject a redefinition. A function named in managed is a program variable: it is only registered here, because the caller declares or defines it with the rest of its path.

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) : SolverEncodingM (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.

def Core.SMT.typedVarToSMTFn (ctx : Context) (id : Expression.Ident) (ty : Expression.Ty) : Except Std.Format (String × Strata.SMT.TermType)

Map a Core typed identifier to its SMT name and sort.

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.solverPreludeOptions (solver : String) (solverOptions : Array (String × String)) : Array (String × String)

The set-options every solver starts from.

Equations

• Core.SMT.solverPreludeOptions "z3" solverOptions = #[("smt.mbqi", "false"), ("auto_config", "false")] ++ solverOptions
• Core.SMT.solverPreludeOptions solver solverOptions = #[] ++ solverOptions

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

Equations

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

@[reducible, inline, deprecated Core.SMT.setSolverPrelude (since := "2026-10-27")]

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

Equations

• Core.SMT.getSolverPrelude = Core.SMT.setSolverPrelude

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

Equations

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

structure Core.SMT.IncrementalLaunch : Type

How a live solver is started for --incremental, and what it is told once started. The tree walk and the one-shot incremental discharge both start their solvers from this, so a goal gets the same time limit, and an unknown at that limit the same reading, whichever of the two sends it.

• flags : Array String

  The command-line flags.

• prelude : Array (String × String)

  The set-options sent after the solver starts, and again after every (reset).

• timeLimitMs : Nat

  The limit, in milliseconds, at which a check's unknown reads as a timeout; 0 for never.

def Core.SMT.incrementalLaunch (options : VerifyOptions) : IncrementalLaunch

Launch flags per backend for a live solver. Model generation is requested on the command line, because a session resets its solver to cross to a branch it cannot extend, and (reset) clears options while launch flags survive it. Without it cvc5 answers (get-model) with "cannot get model unless model generation is enabled"; z3 produces models by default.

The timeout is per check: cvc5's --tlimit and z3's -T bound a whole run, which for a session shared by many checks would make a later check fail for having been preceded by others, so the verdict would depend on how many goals its worker happened to take. An obligation that asks both checks, satisfiability and validity, so gets up to twice --solver-timeout here, where the path that writes the query to a file gives both together one limit.

A solver started with a per-check limit (cvc5 and z3) keeps that limit as a bound. The user's own time option for that solver replaces it, so only the last such value is sent, and only when it is a positive number below the limit; the limit is sent in its place otherwise. A smaller user limit makes the solver give up first, so its unknown stands as on the per-obligation path; otherwise an unknown at the limit is a timeout. Without a limit (--solver-timeout 0) the user's options are sent as given.

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) (captured : Option Emitter.CapturedFile := 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) (factory : Lambda.Factory CoreLParams := Factory) : 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 and distinct constraints into the factory (needed for SMT encoding).

Equations

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

def Core.evalProgramDecls (options : VerifyOptions) (program : Program) (moreFns : Lambda.Factory CoreLParams := Lambda.Factory.default) : Except Strata.Message (List Decl × Imperative.ProofObligations Expression × Statistics)

Symbolic evaluation of a program's declarations, as obligation generation runs it: the program and the factory moreFns extends, both without the unconditional inline attribute except on the functions whose expansion removes a lambda (Core.Simplify.lambdaCarriers), through buildEnv and Program.eval. Returns the program-level declarations of the obligation program (the program's type declarations, the functions evaluation added with their recursive axioms, the distinct declarations), the obligations evaluation deferred, and the statistics.

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.declObligationsProgram (options : VerifyOptions) (program : Program) (moreFns : Lambda.Factory CoreLParams := Lambda.Factory.default) : Except Strata.Message (Program × Statistics)

The declaration phase of a program (Core.WP.declObligationsProgramWith): the program-level declarations and the lemmas' obligations are those symbolic evaluation produces for the program without its procedures (evalProgramDecls, the evaluation symbolic mode runs, done once); the axioms and procedures are kept in place; each lemma becomes the obligation unit of its obligation.

Equations

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

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

The WP phase of a program (Core.WP.wpProcsProgram): each procedure that is not an obligation unit becomes a guarded procedure of the same name and header; every other declaration is kept. The names the procedures introduce avoid the names of the factory's functions and those the program declares.

Equations

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

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

The SSA phase of a program (Core.WP.ssaProgram): each guarded procedure becomes an obligation procedure of the same name; the names it introduces avoid the names of the factory's functions and those the program declares.

Equations

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

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

The declaration phase of a program, then its WP phase, then its SSA phase.

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

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

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.

@[instance_reducible]

instance Core.instReprSolverPhaseLog : Repr SolverPhaseLog

Equations

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

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

Equations

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

@[instance_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.

• axiomsDropped : Bool

  Set when directed pruning dropped axioms from the query; a sat then reports as unknown, see VCOutcome.withAxiomsDropped.

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

@[instance_reducible]

instance Core.instReprVCOutcome : Repr VCOutcome

Equations

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

@[instance_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 (some m)) (Imperative.SMT.Result.unknown candidateModel) = Imperative.SMT.Result.unknown (some m)
• Core.SMT.Result.merge (Imperative.SMT.Result.unknown candidateModel) (Imperative.SMT.Result.unknown (some m)) = Imperative.SMT.Result.unknown (some 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 ")"

@[instance_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

@[instance_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.

@[instance_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

@[instance_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.

@[instance_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.hasValidityUnknown (vr : VCResult) : Bool

Weaker gate than VCResult.isUnknown: triggers when the validity component is unknown, regardless of satisfiability. Used by requeryDropAxioms because nat VCs with bridge axioms land in satisfiableValidityUnknown (sat + unknown validity), which VCResult.isUnknown — requiring both components unknown — does not catch.

Equations

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

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

@[instance_reducible]

instance Core.instToFormatVCResults : Std.ToFormat VCResults

Equations

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

@[instance_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.modelOfResults (ctx : SMT.Context) (satResult validityResult : SMT.Result) : LExprModel

The counterexample a pair of check results carries: the satisfiability check's model first, then the validity check's, a candidate model from unknown counting too.

Equations

• Core.modelOfResults ctx (Imperative.SMT.Result.sat m) validityResult = Core.convertModel m ctx.getConstructorNames
• Core.modelOfResults ctx satResult (Imperative.SMT.Result.sat m) = Core.convertModel m ctx.getConstructorNames
• Core.modelOfResults ctx (Imperative.SMT.Result.unknown (some m)) validityResult = Core.convertModel m ctx.getConstructorNames
• Core.modelOfResults ctx satResult (Imperative.SMT.Result.unknown (some m)) = Core.convertModel m ctx.getConstructorNames
• Core.modelOfResults ctx satResult validityResult = []

def Core.checksFor (property : Imperative.PropertyType) (md : Imperative.MetaData Expression) (options : VerifyOptions) : Bool × Bool

Which of the two solver checks an obligation needs, shared by every back end so they agree on what a verdict means. It is asked per obligation: an obligation annotated for a full check always gets both, and in deductive mode a property that passes when unreachable is checked only for validity while one that does not is checked only for satisfiability.

Equations

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

inductive Core.PathConditionShape : Type

What evaluatorResults needs to know about a path condition, read in one pass over it.

• onlyDefinitions : PathConditionShape

  Every entry only declares or defines a variable. Such a path condition is satisfiable: each entry is sent to the solver as a declare-fun or a non-recursive define-fun, which some model always satisfies.

  The solver also receives axioms that are not entries of the path condition: those of the built-in functions the definitions use, such as mapConst's, and those attached to the program's own functions (func.axioms, and the per-constructor axioms of recursive functions). Taking the path condition to be satisfiable therefore assumes that these axioms are satisfiable together. If they are not, an assertion the solver would pass vacuously is reported failing; no assertion is ever reported passing because of this. Core.factoryInterp_axiomsSatisfied proves that the axioms of the polymorphic built-ins (Core.Factory) hold together in one model. Two steps are assumed rather than proved: that the specialized copies MonomorphizeFunctions makes of these built-ins, whose axioms are what the solver receives, inherit that model; and that the axioms of the program's own functions are satisfiable. The evaluator also decides before encoding, so a definition the encoder cannot encode is reported as this failure rather than as an analysis error.

• hasFalseAssumption : PathConditionShape

  Some assumption is literally false: the evaluator already knows the path is dead.

• other : PathConditionShape

  Anything else.

@[instance_reducible]

instance Core.instDecidableEqPathConditionShape : DecidableEq PathConditionShape

Equations

• Core.instDecidableEqPathConditionShape x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.pathConditionShape (obligation : Imperative.ProofObligation Expression) : PathConditionShape

The shape of obligation's path condition, read in one pass over its entries.

Equations

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

def Core.usesSatisfiablePathsPremise (obligation : Imperative.ProofObligation Expression) (checkMode : VerificationMode) (shape : PathConditionShape) : Bool

Whether the premise of deductiveAssumingSatisfiablePaths, that every path to an assertion can be taken, lets the evaluator decide that obligation, whose goal is literally false and whose path condition has shape shape, fails: its path condition, whatever it holds, is taken to be satisfiable without asking a solver. Covers are left to the solver, so they are reported as in deductive, and so is a path condition with a literally false assumption, which the evaluator already knows is dead.

Equations

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

def Core.evaluatorResults (obligation : Imperative.ProofObligation Expression) (checkMode : VerificationMode) (satisfiabilityCheck validityCheck : Bool) : Option SMT.Result × Option SMT.Result

The results the evaluator decides without a solver, for satisfiability and validity: some r when the obligation alone settles that check, none when a solver is needed. A check not asked for is unknown.

Equations

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

def Core.axiomCacheFor (mode : IrrelevantAxiomsMode) (prog : Program) : Option IrrelevantAxioms.Cache

The axiom-relevance cache that mode needs for prog, or none when pruning is off.

Equations

• Core.axiomCacheFor mode prog = if (mode == Core.IrrelevantAxiomsMode.Off) = true then none else some (Core.IrrelevantAxioms.Cache.build prog (mode == Core.IrrelevantAxiomsMode.Directed))

def Core.seedName (op : CoreIdent) : String

The name under which the axiom-relevance query knows the function op: its base name, with any monomorphization mangling removed. An obligation is post-MonomorphizeFunctions, so its function references carry mangled names ($__mono#f#int), whereas the axiom program, cache and call graph the query runs against are the pre-pipeline program, which names the base f. Without demangling, a specialized function's axiom would be deemed irrelevant and pruned, turning a valid goal into a false alarm. An unmangled name is returned unchanged. Every seed name, the goal's and the path's, goes through this function.

Equations

• Core.seedName op = Core.NameMangling.demangledBaseName op.toPretty

structure Core.ExprFacts : Type

What the per-obligation steps read off one expression of a path condition. Consecutive obligations share most of their path, by pointer, so these are computed once per expression (ExprFactsCache) instead of once per expression per obligation.

• ops: its function names, as the axiom-relevance seeds name them (seedName);
• opsLast: List.uniqKeepLast ops. uniqKeepLast of a concatenation is unchanged when each part is first replaced by its own uniqKeepLast: a name's last occurrence in the whole is its last occurrence in the last part that has it;
• vars: its free variables, each one's first occurrence only. Symmetrically, eraseDups of a concatenation is unchanged when each part is deduplicated first.

• ops : Thunk (List String)
• opsLast : Thunk (List String)
• vars : Thunk (List (Lambda.IdentT Lambda.LMonoTy Unit))

def Core.exprFacts (e : Expression.Expr) : ExprFacts

Equations

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

@[reducible, inline]

abbrev Core.ExprFactsCache : Type

exprFacts, memoized by the expression's address (see Strata.PtrCache).

Equations

• Core.ExprFactsCache = Strata.PtrCache.PtrCache Core.exprFacts

def Core.ExprFactsCache.empty : ExprFactsCache

Equations

• Core.ExprFactsCache.empty = Strata.PtrCache.PtrCache.empty

def Core.ExprFactsCache.facts (e : Expression.Expr) : StateM ExprFactsCache ExprFacts

Equations

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

def Core.ExprFactsCache.runIn {α : Type} (ref : IO.Ref ExprFactsCache) (m : StateM ExprFactsCache α) : BaseIO α

Run m against the cache in ref. The cache is taken out of the reference while m runs, so its table stays unshared and is updated in place.

Equations

• Core.ExprFactsCache.runIn ref m = ST.Ref.modifyGet ref fun (c : Core.ExprFactsCache) => StateT.run m c

def Core.seedExprs (assumptions : Imperative.PathConditions Expression) (axiomSet : Std.HashSet String) : Array Expression.Expr

The expressions of assumptions whose function names seed the relevance query, in order: every expression of every entry, except those of the assumptions labelled in axiomSet.

Equations

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

def Core.antecedentOpsCached (assumptions : Imperative.PathConditions Expression) (axiomSet : Std.HashSet String) : StateM ExprFactsCache (List String)

The function names of seedExprs, demangled, concatenated in order.

Equations

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

def Core.seedsKeepLastCached (consequentFns : List String) (assumptions : Imperative.PathConditions Expression) (axiomSet : Std.HashSet String) : StateM ExprFactsCache (List String)

List.uniqKeepLast (consequentFns ++ ops), where ops is antecedentOpsCached, built from the back without concatenating: the opsLast of seedExprs from the last expression to the first, then consequentFns, each name kept the first time it is met (List.keepLastStep), which is its last occurrence in the whole (ExprFacts).

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) (exprCache : Option (IO.Ref ExprFactsCache) := none) (relevanceMemo : Option (IO.Ref IrrelevantAxioms.RelevanceMemo) := none) : EIO Strata.Message (Imperative.ProofObligation Expression × Option SMT.Result × Option SMT.Result × List String)

Preprocess a proof obligation using symbolic simulation. Returns the symbolic results for satisfiability and validity independently (some r if the evaluator can determine it, none if the solver is needed), plus the labels of axiom assumptions found irrelevant to this obligation (empty when pruning is off or inapplicable). The returned obligation has the pruned axioms removed from its assumptions; the labels let a caller that needs the original assumptions (e.g. for cross-obligation sharing) apply the pruning at emission time instead.

Equations

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

def Core.transformPipelinePhases (options : VerifyOptions := VerifyOptions.default) : 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), filterProcedures appears twice, as an ordinary phase each time: a caller who does not filter simply leaves both out. All filter phases are model-preserving since they only remove information without introducing over-approximations.

The two occurrences do different work. The first restricts the program to the requested procedures, keeping their transitive callees because CallElim still needs the callees' contracts. The second, after CallElim, TermCheck and PrecondElim, discards those callees now that their contracts have been inlined; it names the requested procedures and drops the lemmas no declaration lists. The well-formedness and termination lemmas of a requested procedure or function survive because it lists them in its lemmas; those of other functions are pruned.

A single filter would suffice if the first pass kept each callee as its contract alone, with the body removed: CallElim would consume those declarations and they would fall away, leaving nothing for a second pass to collect. That requires changing what the filter produces.

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

assertWellFormedCalls comes first, so an ill-formed call is reported in every procedure, including ones the procedure filter then drops. The filter follows, and then assertNoCFGBodies, which turns a throw from inside runProgram into a rejection naming the fact, so every statement-level transform after it may rely on structured bodies.

Equations

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

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

Type-checking pipeline phase: runs Core.typeCheck on the program against factory (the full function set to type-check against; defaults to the pristine Core.Factory).

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.

Requires noNondetGuards, which NondetElim.nondetElimPipelinePhase establishes: Core.Statement.eval rejects a surviving nondeterministic guard.

Equations

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

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

The declaration pipeline phase, the first phase --vcgen wp runs: the program-level declarations symbolic evaluation produces for the program without its procedures (type declarations, functions, distinct declarations) replace the program's, every axiom and every procedure is kept unchanged, and each lemma becomes an obligation unit (a procedure asserting its obligation). It evaluates no procedure, so it requires nothing of them; it keeps every procedure, emits obligation units without loops, calls, contracts, type parameters or nondeterministic guards, and its functions are those symbolic evaluation emits.

Equations

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

def Core.wpPipelinePhase (moreFns : Lambda.Factory CoreLParams := Lambda.Factory.default) : PipelinePhase

The WP pipeline phase: each procedure that is not an obligation unit becomes a guarded procedure, every other declaration is kept (--vcgen wp runs it after declObligationsPipelinePhase, then ssaPipelinePhase). It requires a program without calls, since it rejects every call, and bodies whose every exit targets an enclosing block, which it checks of each procedure again (WP.checkLoopFree). It empties every contract, emits only guarded-form bodies whose every ite arm contains an obligation (Imperative.WP.wpEntry_armsHaveObl; each obligation unit it keeps is one assert or cover), emits no loop and no exit, keeps headers, touches no function and builds only annotated variables, literals and ites.

Equations

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

def Core.ssaPipelinePhase (moreFns : Lambda.Factory CoreLParams := Lambda.Factory.default) : PipelinePhase

The SSA pipeline phase: each guarded procedure becomes an obligation procedure. It emits only init, assume, assert, cover and ite *, and no set; it drops the procedures' specifications, so it requires none. The obligation program declares its variables in place, so it does not establish noInits, and commonSubexprElim, which requires noInits, cannot follow it. It requires every ite arm to contain an obligation: it drops an arm without one and inlines the other arm, so a run through the dropped arm would be replayed by running the other arm's definitions. It keeps every obligation and emits an ite * only when both arms are nonempty, so its output keeps that fact.

Equations

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

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

The phases --vcgen wp runs in place of symbolicEvalPipelinePhase: the declaration phase, the WP phase, the SSA phase, then the erasure of unread definitions.

Equations

• Core.wpVCGenPhases options moreFns = [Core.declObligationsPipelinePhase options moreFns, Core.wpPipelinePhase moreFns, Core.ssaPipelinePhase moreFns, Core.deadDefElimPipelinePhase]

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

The phases that run between transformPipelinePhases and symbolicEvalPipelinePhase: replace procedure and lemma type parameters by opaque types, type-check, monomorphize functions, and eliminate nondeterminism.

Factored out so genVCs in MetaVerifier can reuse them without pulling in the full transformPipelinePhases prefix (call elimination, precondition lifting, etc.), which is unnecessary for programs that already arrive call-free from the Boole→Core translation.

Equations

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

def Core.corePipelinePhases (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 (a pipeline that omits it is still sound, though solver outcomes may differ on individual obligations).

Equations

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

def Core.backEndRequiredFacts : ProgramFactSet

What the back end needs of the program the pipeline hands it, as opposed to what one phase asks of another. A phase list that does not deliver these is rejected the same way as one whose phases do not fit.

A CFG body is worse than an unsupported statement: obligation extraction returns no obligations at all for one, so every assertion in it would go unchecked and unreported.

noNondetGuards is absent because obligation extraction accepts ite *; hasObligationForm states what it does require.

noLoopInvariants and noLoopMeasures are absent because noLoops covers them; they are required by LoopElim, which is where they matter.

Equations

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

def Core.coreValidatedPipeline (options : VerifyOptions := VerifyOptions.default) (moreFns : Lambda.Factory CoreLParams := Lambda.Factory.default) : Except String (ValidatedPipeline ProgramFactSet.empty)

The Core pipeline, checked as it is assembled: the phase list built from options, validated against the phases' contracts and against what the back end requires. A phase list that does not compose never becomes a pipeline, so callers cannot run one.

A caller wanting a different order builds one with Core.validatePipeline (or Core.validatePipelineFrom) over a phase list of its own and passes the result to verify.

Equations

• Core.coreValidatedPipeline options moreFns = Core.ValidatedPipeline.ofListDelivering "the verification back end" Core.backEndRequiredFacts (Core.corePipelinePhases options moreFns)

def Core.coreAbstractedPhases (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 options as the corresponding corePipelinePhases run: the phase list's membership is options-dependent (proceduresToVerify), so a list computed with different options describes phases that did not actually run.

Equations

• Core.coreAbstractedPhases options moreFns = List.map (fun (x : Core.PipelinePhase) => x.phase) (Core.corePipelinePhases 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, [])

def Core.VCOutcome.withAxiomsDropped (o : VCOutcome) : VCOutcome

The outcome as reported. When axiomsDropped is set, a sat becomes unknown, keeping its model, because the model may violate a dropped axiom, so a real violation found this way also reports as unknown. An unsat stands: adding the dropped axioms back keeps the query unsatisfiable.

Equations

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

def Core.VCOutcome.afterPruning (mode : IrrelevantAxiomsMode) (dropped : List String) (o : VCOutcome) : VCOutcome

The outcome of a query from which pruning in mode dropped the axioms dropped. In directed mode it is marked and reported as withAxiomsDropped says; other modes keep the solver's answer.

Equations

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

def Core.VCResult.validateModels (r : VCResult) (phases : List AbstractedPhase) : VCResult

Pass a result's two verdicts through the phases' model validation, as the default back end does for each obligation it discharges, and record what each phase decided.

Equations

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

@[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 := []) (prunedAxiomLabels : List String := []) : 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.collectModelVarsCached (obligation : Imperative.ProofObligation Expression) (varDefinitions : List VarDefinition) (varDeclarations : List VarDeclaration) : StateM ExprFactsCache (List (Lambda.IdentT Lambda.LMonoTy Unit))

The variables a counterexample for obligation should report: those its goal and assumptions reach, through the managed definitions they use, that Core.SMT.isReportedName names. A variable the passive program declares (var x) is reported; one it defines (init x := e) is not, since its value follows from the others. A variable of a function type, such as one standing for a function in a generated lemma, is not reported: SMT-LIB's get-value takes only terms of a value sort, and a request naming it would lose the whole counterexample.

Each expression's free variables are read from ExprFactsCache, so the expressions a caller's obligations share are walked once. The variables come in the order of ProofObligation.getVars (each one's first occurrence: the goal's, then each expression's in order); its eraseDups of the concatenation is unchanged when each expression's variables come deduplicated (ExprFacts).

Equations

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

def Core.collectModelVars (obligation : Imperative.ProofObligation Expression) (varDefinitions : List VarDefinition) (varDeclarations : List VarDeclaration) : List (Lambda.IdentT Lambda.LMonoTy Unit)

collectModelVarsCached with a cache of its own, for a caller with one obligation.

Equations

• Core.collectModelVars obligation varDefinitions varDeclarations = StateT.run' (Core.collectModelVarsCached obligation varDefinitions varDeclarations) Core.ExprFactsCache.empty

def Core.cseDefinitions (obligation : Imperative.ProofObligation Expression) : List (String × Expression.Expr)

The CSE-generated definitions on the path of obligation, in order.

Equations

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

def Core.neededCSEDefinitions (obligation : Imperative.ProofObligation Expression) (definitions : List (String × Expression.Expr)) : Std.HashSet String

The names of the definitions of definitions, the CSE-generated definitions of obligation, that obligation uses: those its goal and its other path-condition entries reference, closed over the definitions' bodies (see pruneUnusedCSEDefinitions).

Equations

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

def Core.pruneUnusedCSEDefinitions (obligation : Imperative.ProofObligation Expression) : Imperative.ProofObligation Expression

Remove CSE-generated definitions that cannot affect this obligation.

Symbolic evaluation combines every deferred obligation into one synthetic procedure before CSE runs. CSE may therefore hoist a repeated expression above all obligation branches, making its init $__cse.* entry appear in every obligation even when only one branch references it. Such a definition must not reach an obligation that does not use it: it can mention a function the obligation does not, and so bring that function's axioms into its context. A recursive function's termination and well-formedness lemmas are stated without the function, and must be checked without its axioms, which may be contradictory when the function does not terminate. An unencodable literal in such a definition would also prevent unrelated obligations from reaching the solver.

Start from CSE variables referenced by the obligation and by non-CSE path-condition entries, close transitively over CSE definition bodies, and retain only those definitions. The original entry ordering is preserved, so every retained dependency is still emitted before its users.

Equations

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

def Core.dischargeObligations (E : Env) (obligations : Imperative.ProofObligations Expression) (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) : EIO Strata.Message (VCResults × Statistics)

Discharge obligations, in order, against the environment E built for the program they come from: each is asked of the solver mkDischarge gives, after the evaluator and the pruning the options ask for. verifySingleEnv sends a whole program's obligations through here; a back end that has already read the obligations sends one at a time.

Equations

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

def Core.obligationsOf (oblProgram : Program) : Except Strata.Message (Imperative.ProofObligations Expression)

The obligations extractObligations reads from a program, each without the CSE definitions it does not use (see pruneUnusedCSEDefinitions).

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 verifyPipeline when no custom solver is provided.

Equations

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

def Core.verifyPipeline (program : Program) (tempDir : System.FilePath) (options : VerifyOptions := VerifyOptions.default) (moreFns : Lambda.Factory CoreLParams := Lambda.Factory.default) (externalPhases : List AbstractedPhase := []) (entryFacts : ProgramFactSet := ProgramFactSet.empty) (pipeline : Option (ValidatedPipeline entryFacts) := none) (entryFactsHold : entryFacts.holds program := by exact _root_.Core.ProgramFactSet.empty_holds _) (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, on solver when given and otherwise one obligation at a time. Core.verify chooses solver, the obligation-tree walk under --incremental, and calls this. 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.

@[instance_reducible]

instance Strata.instReprDiagnostic : Repr Diagnostic

Equations

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

@[instance_reducible]

instance Strata.instBEqDiagnostic : BEq Diagnostic

Equations

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

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

@[instance_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.