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 := []) : SolverM (List String × EncoderState)

Encode a verification condition into SMT-LIB format.

This function encodes the path conditions (P) and obligation (Q) into SMT, then emits check-sat commands to determine satisfiability and/or validity.

When both checks are requested, uses check-sat-assuming for efficiency:

• Satisfiability: (check-sat-assuming (Q)) tests if P ∧ Q is satisfiable
• Validity: (check-sat-assuming ((not Q))) tests if P ∧ ¬Q is satisfiable

When only one check is requested, uses assert + check-sat:

• For satisfiability: (assert Q) (check-sat) tests P ∧ Q
• For validity: (assert (not Q)) (check-sat) tests P ∧ ¬Q

Note: The obligation term Q is encoded without negation. Negation is applied when needed for the validity check (line 64 for check-sat-assuming, line 77 for assert).

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.

@[reducible, inline]

abbrev Core.SMT.Result : Type

Equations

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

def Core.SMT.getSolverPrelude : String → Strata.SMT.SolverM Unit

Equations

• Core.SMT.getSolverPrelude "z3" = do Strata.SMT.Solver.setOption "smt.mbqi" "false" Strata.SMT.Solver.setOption "auto_config" "false"
• Core.SMT.getSolverPrelude "cvc5" = pure ()
• Core.SMT.getSolverPrelude x✝ = pure ()

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 := []) : IO (Except Imperative.SMT.SolverError (Result × Result × Strata.SMT.EncoderState))

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.

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

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

@[implicit_reducible]

instance Core.instBEqSolverPhaseLog : BEq SolverPhaseLog

Equations

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

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 unsat unsat no warning error error Dead code, path unreachable ➕ 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.

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.instBEqVCError : BEq VCError

Equations

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

@[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.DiagnosticModel (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.
• Core.transformPipelinePhases = [] ++ [Core.callElimPipelinePhase] ++ [Core.termCheckPipelinePhase] ++ [Core.precondElimPipelinePhase] ++ [] ++ [Core.loopElimPipelinePhase]

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 ANF encoding. ANF encoding runs after symbolic evaluation to extract common subexpressions introduced by partial evaluation inlining.

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.

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, [])

def Core.getObligationResult (assumptionTerms : List Strata.SMT.Term) (obligationTerm : Strata.SMT.Term) (ctx : SMT.Context) (obligation : Imperative.ProofObligation Expression) (p : Program) (options : VerifyOptions) (counter : IO.Ref Nat) (tempDir : System.FilePath) (satisfiabilityCheck validityCheck : Bool) (phases : List AbstractedPhase) (varDefinitions : List VarDefinition := []) (varDeclarations : List VarDeclaration := []) : EIO Strata.DiagnosticModel 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.verifySingleEnv (oblProgram : Program) (moreFns : Lambda.Factory CoreLParams := Lambda.Factory.default) (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) : EIO Strata.DiagnosticModel (VCResults × Statistics)

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 := []) (keepAllFilesPrefix : Option String := none) : EIO Strata.DiagnosticModel 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 keepAllFilesPrefix is provided, the program state after each pipeline phase is written to {prefix}.{n}.{phaseName}.core.st (numbered from 1).

Equations

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

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

Equations

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

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

Equations

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

def Strata.frontEndPhase : Core.AbstractedPhase

Front-end phase: any translation from a source language to Core may introduce over-approximations. Until front-ends can validate models or determine that an assertion is unaffected, all sat results are converted to unknown.

Equations

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

def Strata.verify (env : Program) (ictx : Parser.InputContext := default) (proceduresToVerify : Option (List String) := none) (options : Core.VerifyOptions := Core.VerifyOptions.default) (moreFns : Lambda.Factory Core.CoreLParams := Lambda.Factory.default) (externalPhases : List Core.AbstractedPhase := []) (keepAllFilesPrefix : Option String := none) : IO Core.VCResults

Equations

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

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

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 : DiagnosticType

@[implicit_reducible]

instance Strata.instReprDiagnostic : Repr Diagnostic

Equations

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

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.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

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

Equations

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

def Strata.Core.VCResult.toDiagnostic (files : Map Uri Lean.FileMap) (vcr : Core.VCResult) (phases : List Core.AbstractedPhase := []) : Option Diagnostic

Equations

• Strata.Core.VCResult.toDiagnostic files vcr phases = Option.map (fun (dm : Strata.DiagnosticModel) => Strata.DiagnosticModel.toDiagnostic files dm) (Strata.toDiagnosticModel vcr phases)