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

@[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) : IO (Except Std.Format (Result × Result × Strata.SMT.EncoderState))

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

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

Equations

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

instance Core.instReprVCOutcome : Repr VCOutcome

Equations

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

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 cex, 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 cex => 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 cex, Imperative.SMT.Result.sat cex_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 cex, Imperative.SMT.Result.unknown => 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 => 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, Imperative.SMT.Result.sat cex => 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, 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, Imperative.SMT.Result.unknown => 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

Equations

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

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

Equations

• o.isSatisfiable = match o.satisfiabilityProperty with | Imperative.SMT.Result.sat cex => 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.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.

@[reducible, inline]

abbrev Core.LExprModel : Type

A counterexample model with values lifted to LExpr for display purposes. This is used for formatting counterexamples 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 (cex : 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.formatCexValue✝ e) ++ Std.format ")"

instance Core.instToFormatLExprModel : Std.ToFormat LExprModel

Equations

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

structure Core.VCResult : Type

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

• obligation : Imperative.ProofObligation Expression
• outcome : Except String 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 PE (partial evaluation) 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 PE also determined satisfiability, we mask it to .unknown.

Equations

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

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

Equations

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

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

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 a => true | Except.ok a => 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.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 Core.instToFormatVCResults : Std.ToFormat VCResults

Equations

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

instance Core.instToStringVCResults : ToString VCResults

Equations

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

def Core.preprocessObligation (obligation : Imperative.ProofObligation Expression) (p : Program) (options : VerifyOptions) (satisfiabilityCheck validityCheck : Bool) (axiomCache : Option IrrelevantAxioms.Cache := none) : EIO Strata.DiagnosticModel (Imperative.ProofObligation Expression × Option SMT.Result × Option SMT.Result)

Preprocess a proof obligation using partial evaluation (PE). Returns PE-determined results for satisfiability and validity independently. Each result is some r if PE can determine it, none if the solver is needed.

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) (counter : IO.Ref Nat) (tempDir : System.FilePath) (satisfiabilityCheck validityCheck : Bool) : 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 (pE : Program × Env) (options : VerifyOptions) (counter : IO.Ref Nat) (tempDir : System.FilePath) (axiomCache : Option IrrelevantAxioms.Cache := none) : EIO Strata.DiagnosticModel VCResults

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

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.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) : IO Core.VCResults

Equations

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

def Strata.toDiagnosticModel (vcr : Core.VCResult) : 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

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

Equations

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

instance Strata.instReprDiagnostic : Repr Diagnostic

Equations

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

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) : Option Diagnostic

Equations

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