@[implicit_reducible]

instance Core.instToFormatExpressionMetadata : Std.ToFormat ExpressionMetadata

Equations

• Core.instToFormatExpressionMetadata = inferInstance

@[implicit_reducible]

instance Core.instToFormatExprExpression : Std.ToFormat Expression.Expr

Equations

• Core.instToFormatExprExpression = id inferInstance

def Core.formatScope (m : Map CoreIdent (Option Lambda.LMonoTy × Expression.Expr)) : Std.Format

Equations

• Core.formatScope [] = Std.Format.text ""
• Core.formatScope [(k, ty, v)] = Core.formatScope.go✝ k ty v
• Core.formatScope ((k, ty, v) :: rest) = Core.formatScope.go✝ k ty v ++ Std.Format.line ++ Core.formatScope rest

@[implicit_reducible]

instance Core.instToFormatMapCoreIdentProdOptionLMonoTyExprExpression : Std.ToFormat (Map CoreIdent (Option Lambda.LMonoTy × Expression.Expr))

Equations

• Core.instToFormatMapCoreIdentProdOptionLMonoTyExprExpression = { format := Core.formatScope }

@[implicit_reducible]

instance Core.instInhabitedExpressionMetadata : Inhabited ExpressionMetadata

Equations

• Core.instInhabitedExpressionMetadata = inferInstance

@[implicit_reducible]

instance Core.instTraceableEvalProvenanceExpressionMetadata : Lambda.Traceable Lambda.LExpr.EvalProvenance ExpressionMetadata

Equations

• Core.instTraceableEvalProvenanceExpressionMetadata = { combine := fun (x : List (Lambda.LExpr.EvalProvenance × Core.ExpressionMetadata)) => () }

@[implicit_reducible]

instance Core.instInhabitedLExprMkMkExpressionMetadataCoreIdent {LMonoTy : Type} : Inhabited (Lambda.LExpr { base := { Metadata := ExpressionMetadata, IDMeta := CoreIdent }, TypeType := LMonoTy })

Equations

• Core.instInhabitedLExprMkMkExpressionMetadataCoreIdent = inferInstance

def Core.PathCondition.format (p : Imperative.PathCondition Expression) : Std.Format

Equations

• Core.PathCondition.format [] = Std.Format.text ""
• Core.PathCondition.format [e] = Core.formatCoreEntry✝ e
• Core.PathCondition.format (e :: rest) = Std.format (Core.formatCoreEntry✝ e) ++ Std.format Std.Format.line ++ Core.PathCondition.format rest

def Core.PathConditions.format (ps : Imperative.PathConditions Expression) : Std.Format

Equations

• Core.PathConditions.format [] = Std.format ""
• Core.PathConditions.format (p :: prest) = Std.format (Core.PathCondition.format p) ++ Std.format Std.Format.line ++ Core.PathConditions.format prest

def Core.PathCondition.getVars (p : Imperative.PathCondition Expression) : List (Lambda.IdentT Lambda.LMonoTy Unit)

Equations

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

def Core.PathConditions.getVars (ps : Imperative.PathConditions Expression) : List (Lambda.IdentT Lambda.LMonoTy Unit)

Equations

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

def Core.ProofObligation.getVars (d : Imperative.ProofObligation Expression) : List (Lambda.IdentT Lambda.LMonoTy Unit)

Equations

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

def Core.ProofObligation.eraseTypes (d : Imperative.ProofObligation Expression) : Imperative.ProofObligation Expression

Equations

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

def Core.ProofObligations.eraseTypes (ds : Imperative.ProofObligations Expression) : Imperative.ProofObligations Expression

Equations

• Core.ProofObligations.eraseTypes ds = Array.map Core.ProofObligation.eraseTypes ds

@[implicit_reducible]

instance Core.instToFormatProofObligationExpression : Std.ToFormat (Imperative.ProofObligation Expression)

Equations

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

@[implicit_reducible]

instance Core.instToFormatProofObligationsExpression : Std.ToFormat (Imperative.ProofObligations Expression)

Equations

• Core.instToFormatProofObligationsExpression = { format := fun (os : Imperative.ProofObligations Core.Expression) => Std.Format.joinSep (Array.map Std.format os).toList Std.Format.line }

def Core.ProofObligation.create (label : String) (propertyType : Imperative.PropertyType) (assumptions : Imperative.PathConditions Expression) (obligation : Procedure.Check) : Option (Imperative.ProofObligation Expression)

Equations

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

def Core.ProofObligations.createAssertions (assumptions : Imperative.PathConditions Expression) (obligations : ListMap String Procedure.Check) : Imperative.ProofObligations Expression

Equations

• One or more equations did not get rendered due to their size.
• Core.ProofObligations.createAssertions assumptions [] = #[]

@[reducible, inline]

abbrev Core.SubstMap : Type

A substitution map from variable identifiers to expressions.

Equations

• Core.SubstMap = Map Core.Expression.Ident Core.Expression.Expr

structure Core.Env : Type

• error : Option (Imperative.EvalError Expression)
• program : Program
• substMap : SubstMap
• exprEnv : Lambda.LState { Metadata := ExpressionMetadata, IDMeta := Unit }
• datatypes : Lambda.TypeFactory
• distinct : List (List Expression.Expr)
• pathConditions : Imperative.RevPathConditions Expression
• warnings : List (Imperative.EvalWarning Expression)
• deferred : Imperative.ProofObligations Expression
• pathCap : Option Nat
• collectAllAssertFailures : Bool

  When true, concrete execution records a failed assertion and keeps going instead of halting on the first failure, so multiple assertion failures can be collected in a single run. See assertFailures.

• assertFailures : List (String × Expression.Expr × Imperative.MetaData Expression)

  Assertion failures collected during concrete execution when collectAllAssertFailures is set, most recent first. Each entry carries the assert's label, its evaluated (false) condition, and the statement's metadata — the last of which resolves the failure's source location and property summary without consulting the label.

• ignoreAssumes : Bool

  When true, concrete execution treats assume statements as no-ops instead of enforcing them. See EvalContext.ignoreAssume.

def Core.Env.init (empty_factory : Bool := false) : Env

Equations

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

@[implicit_reducible]

instance Core.instEmptyCollectionEnv : EmptyCollection Env

Equations

• Core.instEmptyCollectionEnv = { emptyCollection := Core.Env.init true }

@[implicit_reducible]

instance Core.instInhabitedEnv : Inhabited Env

Equations

• Core.instInhabitedEnv = { default := Core.Env.init }

@[implicit_reducible]

instance Core.instToFormatEnv : Std.ToFormat Env

Equations

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

def Core.oldLocalVarSubst (E : Env) : SubstMap

Create a substitution map from all variables to their values.

Equations

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

def Core.oldVarSubst (subst : SubstMap) (E : Env) : SubstMap

Append subst map to a substitution map.

Equations

• Core.oldVarSubst subst E = subst ++ Core.oldLocalVarSubst E

def Core.Env.exprEval (E : Env) (e : Expression.Expr) : Expression.Expr

Equations

• E.exprEval e = (Lambda.LExpr.evalWithLState E.exprEnv.config.fuel E.exprEnv e).fst

def Core.Env.pushScope (E : Env) (scope : Lambda.Scope CoreLParams) : Env

Equations

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

def Core.Env.pushEmptyScope (E : Env) : Env

Equations

• E.pushEmptyScope = E.pushScope []

def Core.Env.popScope (E : Env) : Env

Equations

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

def Core.Env.factory (E : Env) : Lambda.Factory CoreLParams

Equations

• E.factory = E.exprEnv.config.factory

def Core.Env.addFactory (E : Env) (f : Lambda.Factory CoreLParams) : Except Strata.Message Env

Equations

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

def Core.validateCasesTypes (funcs : List Function) (tf : Lambda.TypeFactory) : Except Strata.Message Unit

Validate that all @[cases] parameters in a recursive function block reference known datatypes. This is checked at evaluation time because it is an SMT backend limitation, not a type system constraint.

Equations

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

def Core.Env.addFactoryFunc (E : Env) (func : Lambda.LFunc CoreLParams) : Except Strata.Message Env

Add a function to the environment. For recursive functions, checks that the @[cases] attribute was provided (which sets inlineIfConstr), and rejects cases not yet supported for SMT verification (polymorphic recursive functions, missing @[cases] attribute).

Equations

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

def Core.Env.insertInContext (xt : Lambda.IdentT Lambda.LMonoTy Unit) (e : Expression.Expr) (E : Env) : Env

Equations

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

def Core.Env.addToContext (xs : Map (Lambda.IdentT Lambda.LMonoTy Unit) Expression.Expr) (E : Env) : Env

Insert each (x, v) in xs into the context.

Equations

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

def Core.Env.genSym (x : String) (c : Lambda.EvalConfig CoreLParams) : CoreIdent × Lambda.EvalConfig CoreLParams

Equations

• Core.Env.genSym x c = match Lambda.EvalConfig.genSym x c with | (new_var, c) => ({ name := new_var, metadata := () }, c)

def Core.Env.genVar' (x : String) (σ : Lambda.LState CoreLParams) : CoreIdent × Lambda.LState CoreLParams

Equations

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

def Core.Env.genVar (x : Expression.Ident) (E : Env) : Expression.Ident × Env

Equations

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

def Core.Env.genVars (xs : List String) (σ : Lambda.LState CoreLParams) : List CoreIdent × Lambda.LState CoreLParams

Equations

• Core.Env.genVars [] σ = ([], σ)
• Core.Env.genVars (x :: rest) σ = match Core.Env.genVar' x σ with | (x', σ) => match Core.Env.genVars rest σ with | (xrest', σ) => (x' :: xrest', σ)

def Core.Env.genFVar (E : Env) (xt : Lambda.IdentT Lambda.LMonoTy Unit) : Expression.Expr × Env

Generate a fresh variable using the base name and pre-existing type, if any, from xt.

Equations

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

def Core.Env.genFVars (E : Env) (xs : List (Lambda.IdentT Lambda.LMonoTy Unit)) : List Expression.Expr × Env

Generate fresh variables using the base names and any pre-existing types from xs.

Equations

• E.genFVars xs = Core.Env.genFVars.go✝ [] E xs

def Core.Env.insertFreeVarsInOldestScope (xs : List (Lambda.IdentT Lambda.LMonoTy Unit)) (E : Env) : Env

Insert (xi, .fvar xi), for each xi in xs, in the oldest scope in ss, only if xi is the identifier of a free variable, i.e., it is not in ss.

Equations

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

def Core.PathCondition.merge (cond : Expression.Expr) (pc1 pc2 : Imperative.PathCondition Expression) : Imperative.PathCondition Expression

Equations

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

def Core.Env.performMerge (cond : Expression.Expr) (E1 E2 : Env) (_h1 : E1.error.isNone = true) (_h2 : E2.error.isNone = true) : Env

Equations

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

def Core.Env.merge (cond : Expression.Expr) (E1 E2 : Env) : Env

Equations

• Core.Env.merge cond E1 E2 = if h1 : E1.error.isSome = true then E1 else if h2 : E2.error.isSome = true then E2 else Core.Env.performMerge cond E1 E2 ⋯ ⋯

def Core.Env.addMutualDatatype (E : Env) (block : Lambda.MutualDatatype Unit) : Except Strata.Message Env

Equations

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

def Core.Env.addDatatypes (E : Env) (blocks : List (Lambda.MutualDatatype Unit)) : Except Strata.Message Env

Equations

• E.addDatatypes blocks = List.foldlM Core.Env.addMutualDatatype E blocks