def Strata.SMT.Encoder.encodeCore (ctx : Core.SMT.Context) (prelude : SolverM Unit) (ts : List Term) : SolverM (List String × EncoderState)

Equations

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

@[reducible, inline]

abbrev Core.SMT.SMTModel : Type

Equations

• Core.SMT.SMTModel = Map (Lambda.IdentT Lambda.LMonoTy Core.Visibility) String

def Core.SMT.SMTModel.format (model : SMTModel) : Std.Format

Equations

• Core.SMT.SMTModel.format [] = Std.Format.text ""
• Core.SMT.SMTModel.format [((k, snd), v)] = Std.format "(" ++ Std.format k ++ Std.format ", " ++ Std.format v ++ Std.format ")"
• Core.SMT.SMTModel.format (((k, snd), v) :: rest) = Std.format "(" ++ Std.format k ++ Std.format ", " ++ Std.format v ++ Std.format ") " ++ Core.SMT.SMTModel.format rest

instance Core.SMT.instToFormatSMTModel : Std.ToFormat SMTModel

Equations

• Core.SMT.instToFormatSMTModel = { format := Core.SMT.SMTModel.format }

def Core.SMT.getSMTId (x : Lambda.IdentT Lambda.LMonoTy Visibility) (ctx : Context) (E : Strata.SMT.EncoderState) : Except Std.Format String

Find the Id for the SMT encoding of x.

Equations

• One or more equations did not get rendered due to their size.
• Core.SMT.getSMTId (var, none) ctx E = Except.error (Std.format "Expected variable " ++ Std.format var ++ Std.format " to be annotated with a type!")

def Core.SMT.getModel (m : String) : Except Std.Format (List Strata.SMT.CExParser.KeyValue)

Equations

• Core.SMT.getModel m = do let cex ← Strata.SMT.CExParser.parseCEx m pure cex.pairs

def Core.SMT.processModel (vars : List (Lambda.IdentT Lambda.LMonoTy Visibility)) (cexs : List Strata.SMT.CExParser.KeyValue) (ctx : Context) (E : Strata.SMT.EncoderState) : Except Std.Format SMTModel

Equations

• One or more equations did not get rendered due to their size.
• Core.SMT.processModel [] cexs ctx E = pure []

def Core.SMT.processModel.findModelValue (id : String) (cexs : List Strata.SMT.CExParser.KeyValue) : Except Std.Format String

Equations

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

inductive Core.SMT.Result : Type

• sat (m : SMTModel) : Result
• unsat : Result
• unknown : Result
• err (msg : String) : Result

instance Core.SMT.instDecidableEqResult : DecidableEq Result

Equations

• Core.SMT.instDecidableEqResult = Core.SMT.instDecidableEqResult.decEq

def Core.SMT.instDecidableEqResult.decEq (x✝ x✝¹ : Result) : Decidable (x✝ = x✝¹)

Equations

• Core.SMT.instDecidableEqResult.decEq (Core.SMT.Result.sat a) (Core.SMT.Result.sat b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Core.SMT.instDecidableEqResult.decEq (Core.SMT.Result.sat m) Core.SMT.Result.unsat = isFalse ⋯
• Core.SMT.instDecidableEqResult.decEq (Core.SMT.Result.sat m) Core.SMT.Result.unknown = isFalse ⋯
• Core.SMT.instDecidableEqResult.decEq (Core.SMT.Result.sat m) (Core.SMT.Result.err msg) = isFalse ⋯
• Core.SMT.instDecidableEqResult.decEq Core.SMT.Result.unsat (Core.SMT.Result.sat m) = isFalse ⋯
• Core.SMT.instDecidableEqResult.decEq Core.SMT.Result.unsat Core.SMT.Result.unsat = isTrue ⋯
• Core.SMT.instDecidableEqResult.decEq Core.SMT.Result.unsat Core.SMT.Result.unknown = isFalse Core.SMT.instDecidableEqResult.decEq._proof_8
• Core.SMT.instDecidableEqResult.decEq Core.SMT.Result.unsat (Core.SMT.Result.err msg) = isFalse ⋯
• Core.SMT.instDecidableEqResult.decEq Core.SMT.Result.unknown (Core.SMT.Result.sat m) = isFalse ⋯
• Core.SMT.instDecidableEqResult.decEq Core.SMT.Result.unknown Core.SMT.Result.unsat = isFalse Core.SMT.instDecidableEqResult.decEq._proof_11
• Core.SMT.instDecidableEqResult.decEq Core.SMT.Result.unknown Core.SMT.Result.unknown = isTrue ⋯
• Core.SMT.instDecidableEqResult.decEq Core.SMT.Result.unknown (Core.SMT.Result.err msg) = isFalse ⋯
• Core.SMT.instDecidableEqResult.decEq (Core.SMT.Result.err msg) (Core.SMT.Result.sat m) = isFalse ⋯
• Core.SMT.instDecidableEqResult.decEq (Core.SMT.Result.err msg) Core.SMT.Result.unsat = isFalse ⋯
• Core.SMT.instDecidableEqResult.decEq (Core.SMT.Result.err msg) Core.SMT.Result.unknown = isFalse ⋯
• Core.SMT.instDecidableEqResult.decEq (Core.SMT.Result.err a) (Core.SMT.Result.err b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Core.SMT.instReprResult.repr : Result → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Core.SMT.instReprResult.repr Core.SMT.Result.unsat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.SMT.Result.unsat")).group prec✝
• Core.SMT.instReprResult.repr Core.SMT.Result.unknown prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.SMT.Result.unknown")).group prec✝

instance Core.SMT.instReprResult : Repr Result

Equations

• Core.SMT.instReprResult = { reprPrec := Core.SMT.instReprResult.repr }

def Core.SMT.Result.isSat (r : Result) : Bool

Equations

• (Core.SMT.Result.sat m).isSat = true
• r.isSat = false

def Core.SMT.Result.formatWithVerbose (r : Result) (verbose : Bool) : Std.Format

Equations

• (Core.SMT.Result.sat a).formatWithVerbose verbose = if (!verbose || Map.isEmpty a) = true then Std.format "sat" else Std.format "sat\nModel: " ++ Std.format a
• Core.SMT.Result.unsat.formatWithVerbose verbose = Std.format "unsat"
• Core.SMT.Result.unknown.formatWithVerbose verbose = Std.format "unknown"
• (Core.SMT.Result.err a).formatWithVerbose verbose = Std.format "err " ++ Std.format a

instance Core.SMT.instToFormatResult : Std.ToFormat Result

Equations

• Core.SMT.instToFormatResult = { format := fun (r : Core.SMT.Result) => r.formatWithVerbose true }

def Core.SMT.Result.formatModelIfSat (r : Result) (verbose : Bool) : Std.Format

Equations

• (Core.SMT.Result.sat m).formatModelIfSat verbose = if (!verbose || Map.isEmpty m) = true then Std.format "" else Std.format "\nModel:\n" ++ Std.format m
• r.formatModelIfSat verbose = Std.format ""

def Core.SMT.runSolver (solver : String) (args : Array String) : IO IO.Process.Output

Equations

• Core.SMT.runSolver solver args = do let output ← IO.Process.output { cmd := solver, args := args } pure output

def Core.SMT.solverResult (vars : List (Lambda.IdentT Lambda.LMonoTy Visibility)) (output : IO.Process.Output) (ctx : Context) (E : Strata.SMT.EncoderState) (smtsolver : String) : Except Std.Format Result

Equations

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

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 : Options) : Array String

Equations

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

def Core.SMT.addLocationInfo (solver : Strata.SMT.Solver) (md : Imperative.MetaData Expression) : IO Unit

Equations

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

def Core.SMT.dischargeObligation (options : Options) (vars : List (Lambda.IdentT Lambda.LMonoTy Visibility)) (md : Imperative.MetaData Expression) (filename : String) (terms : List Strata.SMT.Term) (ctx : Context) : IO (Except Std.Format (Result × Strata.SMT.EncoderState))

Equations

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

inductive Core.Outcome : Type

Analysis outcome of a verification condition.

• pass : Outcome
• fail : Outcome
• unknown : Outcome
• implementationError (e : String) : Outcome

def Core.instReprOutcome.repr : Outcome → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Core.instReprOutcome.repr Core.Outcome.pass prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Outcome.pass")).group prec✝
• Core.instReprOutcome.repr Core.Outcome.fail prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Outcome.fail")).group prec✝
• Core.instReprOutcome.repr Core.Outcome.unknown prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Outcome.unknown")).group prec✝

instance Core.instReprOutcome : Repr Outcome

Equations

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

instance Core.instInhabitedOutcome : Inhabited Outcome

Equations

• Core.instInhabitedOutcome = { default := Core.instInhabitedOutcome.default }

def Core.instInhabitedOutcome.default : Outcome

Equations

• Core.instInhabitedOutcome.default = Core.Outcome.pass

instance Core.instDecidableEqOutcome : DecidableEq Outcome

Equations

• Core.instDecidableEqOutcome = Core.instDecidableEqOutcome.decEq

def Core.instDecidableEqOutcome.decEq (x✝ x✝¹ : Outcome) : Decidable (x✝ = x✝¹)

Equations

• Core.instDecidableEqOutcome.decEq Core.Outcome.pass Core.Outcome.pass = isTrue ⋯
• Core.instDecidableEqOutcome.decEq Core.Outcome.pass Core.Outcome.fail = isFalse Core.instDecidableEqOutcome.decEq._proof_1
• Core.instDecidableEqOutcome.decEq Core.Outcome.pass Core.Outcome.unknown = isFalse Core.instDecidableEqOutcome.decEq._proof_2
• Core.instDecidableEqOutcome.decEq Core.Outcome.pass (Core.Outcome.implementationError e) = isFalse ⋯
• Core.instDecidableEqOutcome.decEq Core.Outcome.fail Core.Outcome.pass = isFalse Core.instDecidableEqOutcome.decEq._proof_4
• Core.instDecidableEqOutcome.decEq Core.Outcome.fail Core.Outcome.fail = isTrue ⋯
• Core.instDecidableEqOutcome.decEq Core.Outcome.fail Core.Outcome.unknown = isFalse Core.instDecidableEqOutcome.decEq._proof_5
• Core.instDecidableEqOutcome.decEq Core.Outcome.fail (Core.Outcome.implementationError e) = isFalse ⋯
• Core.instDecidableEqOutcome.decEq Core.Outcome.unknown Core.Outcome.pass = isFalse Core.instDecidableEqOutcome.decEq._proof_7
• Core.instDecidableEqOutcome.decEq Core.Outcome.unknown Core.Outcome.fail = isFalse Core.instDecidableEqOutcome.decEq._proof_8
• Core.instDecidableEqOutcome.decEq Core.Outcome.unknown Core.Outcome.unknown = isTrue ⋯
• Core.instDecidableEqOutcome.decEq Core.Outcome.unknown (Core.Outcome.implementationError e) = isFalse ⋯
• Core.instDecidableEqOutcome.decEq (Core.Outcome.implementationError e) Core.Outcome.pass = isFalse ⋯
• Core.instDecidableEqOutcome.decEq (Core.Outcome.implementationError e) Core.Outcome.fail = isFalse ⋯
• Core.instDecidableEqOutcome.decEq (Core.Outcome.implementationError e) Core.Outcome.unknown = isFalse ⋯
• Core.instDecidableEqOutcome.decEq (Core.Outcome.implementationError a) (Core.Outcome.implementationError b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Core.instToFormatOutcome : Std.ToFormat Outcome

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
• smtResult : SMT.Result
• result : Outcome
• estate : Strata.SMT.EncoderState
• verbose : VerboseMode

def Core.smtResultToOutcome (r : SMT.Result) (isCover : Bool) : Outcome

Map the result from an SMT backend engine to an Outcome.

Equations

• Core.smtResultToOutcome Core.SMT.Result.unknown isCover = Core.Outcome.unknown
• Core.smtResultToOutcome Core.SMT.Result.unsat isCover = if isCover = true then Core.Outcome.fail else Core.Outcome.pass
• Core.smtResultToOutcome (Core.SMT.Result.sat m) isCover = if isCover = true then Core.Outcome.pass else Core.Outcome.fail
• Core.smtResultToOutcome (Core.SMT.Result.err e) isCover = Core.Outcome.implementationError e

instance Core.instToFormatVCResult : Std.ToFormat VCResult

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.result with | Core.Outcome.pass => true | x => false

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

Equations

• vr.isFailure = match vr.result with | Core.Outcome.fail => true | x => false

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

Equations

• vr.isUnknown = match vr.result with | Core.Outcome.unknown => true | x => false

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

Equations

• vr.isImplementationError = match vr.result with | Core.Outcome.implementationError e => true | x => false

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

Equations

• vcResult.isNotSuccess = !vcResult.isSuccess

@[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 : Options) : EIO Strata.DiagnosticModel (Imperative.ProofObligation Expression × Option VCResult)

Preprocess a proof obligation before handing it off to a backend engine.

Equations

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

def Core.getObligationResult (terms : List Strata.SMT.Term) (ctx : SMT.Context) (obligation : Imperative.ProofObligation Expression) (p : Program) (options : Options) (counter : IO.Ref Nat) (tempDir : System.FilePath) : 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 : Options) (counter : IO.Ref Nat) (tempDir : System.FilePath) : 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 : Options := Options.default) (moreFns : Lambda.Factory CoreLParams := Lambda.Factory.default) : EIO Strata.DiagnosticModel VCResults

Equations

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

def Strata.typeCheck (ictx : Parser.InputContext) (env : Program) (options : Options := Options.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 : Options := Options.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

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

• Strata.instBEqDiagnostic.beq { start := a, ending := a_1, message := a_2 } { start := b, ending := b_1, message := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• 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)