@[reducible, inline]

abbrev Core.evalLoc : ExprSourceLoc

Location of expressions this file builds itself.

Equations

• Core.evalLoc = ExprSourceLoc.synthesized "eval"

inductive Core.Statement.CondType : Type

• Requires : CondType
• Ensures : CondType

@[instance_reducible]

instance Core.Statement.instToStringCondType : ToString CondType

Equations

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

@[reducible, inline]

abbrev Core.Statement.VarSubst : Type

Equations

• Core.Statement.VarSubst = List ((Core.Expression.Ident × Option Lambda.LMonoTy) × Core.Expression.Expr)

def Core.Statement.mkReturnSubst (proc : Procedure) (lhs : List Expression.Ident) (E : Env) : VarSubst × VarSubst × Env

Create fresh variables for return and LHS mapping.

Return mapping is used for postcondition substitution, i.e., to map procedure's return parameter names to fresh variables.

LHS mapping is used for environment updates, i.e., to map caller's LHS variable names to the same fresh variables as above.

For example, if we have call x := Inc(8) where Inc returns a variable named ret: Return mapping: [("ret", fresh_var)] LHS mapping: [("x", fresh_var)]

Equations

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

def Core.Statement.Command.inlineCallContract (E : Env) (lhs : List Expression.Ident) (pname : String) (args : List Expression.Expr) (md : Imperative.MetaData Expression) : Command × Env

Evaluate a procedure call by inlining its contract. args and lhs are matched positionally against proc.header.inputs and proc.header.outputs respectively.

Equations

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

def Core.Statement.Command.eval (E : Env) (c : Command) : Command × Env

Equations

• One or more equations did not get rendered due to their size.
• Core.Statement.Command.eval E (Imperative.CmdExt.cmd c_2) = match Imperative.Cmd.eval E c_2 with | (c, E) => (Imperative.CmdExt.cmd c, E)

@[irreducible]

def Core.Statement.Statement.containsCmd (predicate : Imperative.Cmd Expression → Bool) (s : Statement) : Bool

Generic function to check if a statement contains a specific command type.

Equations

• One or more equations did not get rendered due to their size.
• Core.Statement.Statement.containsCmd predicate (Imperative.Stmt.cmd (Imperative.CmdExt.cmd c)) = predicate c
• Core.Statement.Statement.containsCmd predicate (Imperative.Stmt.cmd cmd) = false
• Core.Statement.Statement.containsCmd predicate (Imperative.Stmt.block label inner_ss md) = Core.Statement.Statements.containsCmds predicate inner_ss
• Core.Statement.Statement.containsCmd predicate (Imperative.Stmt.loop guard measure invariants body_ss md) = Core.Statement.Statements.containsCmds predicate body_ss
• Core.Statement.Statement.containsCmd predicate (Imperative.Stmt.exit label md) = false
• Core.Statement.Statement.containsCmd predicate (Imperative.Stmt.typeDecl tc md) = false

@[irreducible]

def Core.Statement.Statements.containsCmds (predicate : Imperative.Cmd Expression → Bool) (ss : Statements) : Bool

Generic function to check if statements contain a specific command type.

Equations

• Core.Statement.Statements.containsCmds predicate [] = false
• Core.Statement.Statements.containsCmds predicate (s :: ss_2) = (Core.Statement.Statement.containsCmd predicate s || Core.Statement.Statements.containsCmds predicate ss_2)

def Core.Statement.Statements.containsCovers (ss : Statements) : Bool

Detect if statements contain any cover commands.

Equations

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

def Core.Statement.Statements.containsAsserts (ss : Statements) : Bool

Detect if statements contain any assert commands.

Equations

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

@[irreducible]

def Core.Statement.Statement.collectCovers (s : Statement) : List (String × Imperative.MetaData Expression)

Collect all cover commands from a statement s with their labels and metadata.

Equations

• Core.Statement.Statement.collectCovers (Imperative.Stmt.cmd (Imperative.CmdExt.cmd (Imperative.Cmd.cover label _expr md))) = [(label, md)]
• Core.Statement.Statement.collectCovers (Imperative.Stmt.cmd cmd) = []
• Core.Statement.Statement.collectCovers (Imperative.Stmt.block label inner_ss md) = Core.Statement.Statements.collectCovers inner_ss
• Core.Statement.Statement.collectCovers (Imperative.Stmt.ite cond then_ss else_ss md) = Core.Statement.Statements.collectCovers then_ss ++ Core.Statement.Statements.collectCovers else_ss
• Core.Statement.Statement.collectCovers (Imperative.Stmt.loop guard measure invariants body_ss md) = Core.Statement.Statements.collectCovers body_ss
• Core.Statement.Statement.collectCovers (Imperative.Stmt.exit label md) = []
• Core.Statement.Statement.collectCovers (Imperative.Stmt.typeDecl tc md) = []

@[irreducible]

def Core.Statement.Statements.collectCovers (ss : Statements) : List (String × Imperative.MetaData Expression)

Collect all cover commands from statements ss with their labels and metadata.

Equations

• Core.Statement.Statements.collectCovers [] = []
• Core.Statement.Statements.collectCovers (s :: ss_2) = Core.Statement.Statement.collectCovers s ++ Core.Statement.Statements.collectCovers ss_2

@[irreducible]

def Core.Statement.Statement.collectAsserts (s : Statement) : List (String × Imperative.MetaData Expression)

Collect all assert commands from a statement s with their labels and metadata.

Equations

• Core.Statement.Statement.collectAsserts (Imperative.Stmt.cmd (Imperative.CmdExt.cmd (Imperative.Cmd.assert label _expr md))) = [(label, md)]
• Core.Statement.Statement.collectAsserts (Imperative.Stmt.cmd cmd) = []
• Core.Statement.Statement.collectAsserts (Imperative.Stmt.block label inner_ss md) = Core.Statement.Statements.collectAsserts inner_ss
• Core.Statement.Statement.collectAsserts (Imperative.Stmt.ite cond then_ss else_ss md) = Core.Statement.Statements.collectAsserts then_ss ++ Core.Statement.Statements.collectAsserts else_ss
• Core.Statement.Statement.collectAsserts (Imperative.Stmt.loop guard measure invariants body_ss md) = Core.Statement.Statements.collectAsserts body_ss
• Core.Statement.Statement.collectAsserts (Imperative.Stmt.exit label md) = []
• Core.Statement.Statement.collectAsserts (Imperative.Stmt.typeDecl tc md) = []

@[irreducible]

def Core.Statement.Statements.collectAsserts (ss : Statements) : List (String × Imperative.MetaData Expression)

Collect all assert commands from statements ss with their labels and metadata.

Equations

• Core.Statement.Statements.collectAsserts [] = []
• Core.Statement.Statements.collectAsserts (s :: ss_2) = Core.Statement.Statement.collectAsserts s ++ Core.Statement.Statements.collectAsserts ss_2

structure Core.Statement.EnvWithNext : Type

An environment with an optional exit label.

• env : Env
• exitLabel : Option (Option String)

  none = no exit active; some none = exit nearest block; some (some l) = exit block l

• splitConds : Array (Nat × Expression.Expr × Bool)

  Stack of unmerged split conditions. Each entry is (splitId, cond, side) where splitId uniquely identifies the split origin (both paths from the same split get the same splitId), cond is the branch condition expression, and side distinguishes the branches (true = then, false = else for ITE splits). Last element is the most recent (innermost) unmerged split.

  Key invariant: both sides of a split always share the same splitId and cond; only side differs. Entries are only pushed in processIteBranches when pathCap is active. mergeCondPairs relies on this to correctly pair and merge paths.

structure Core.Statement.SharedEvalState : Type

What statement evaluation passes from each path to the next, in evaluation order: the next split id, and the name supply, so that no two paths generate the same name. During statement evaluation, an env holds an empty name supply except while one of its commands runs.

• nextSplitId : Nat
• names : Lambda.NameSupply

@[irreducible]

def Core.Statement.evalAuxGo (steps : Nat) (Ewns : List EnvWithNext) (ss : Statements) (shared : SharedEvalState) : List EnvWithNext × Statistics × SharedEvalState

Batch symbolic evaluator: evaluates a statement list for all input paths simultaneously. Between each statement, enforces the path cap by merging continuing (.none exit) paths.

Equations

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

@[irreducible]

def Core.Statement.processIteBranches (steps : Nat) (Ewn : EnvWithNext) (cond cond' : Expression.Expr) (then_ss else_ss : Statements) (shared : SharedEvalState) : List EnvWithNext × Statistics × SharedEvalState

Equations

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

def Core.Statement.evalAux (E : Env) (ss : Statements) (optExit : Option (Option String)) : List EnvWithNext × Statistics

Equations

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

def Core.Statement.exitToError : EnvWithNext → Env

Equations

• One or more equations did not get rendered due to their size.
• Core.Statement.exitToError { env := env, splitConds := splitConds } = env

def Core.Statement.eval (E : Env) (ss : Statements) : List Env × Statistics

A symbolic simulator for statements yielding a list of resulting environments.

Equations

• Core.Statement.eval E ss = match Core.Statement.evalAux E ss none with | (ewns, stats) => (List.map Core.Statement.exitToError ewns, stats)

def Core.Statement.evalOne (E : Env) (ss : Statements) : Env

A symbolic simulator for statements yielding one environment.

Equations

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

@[irreducible]

def Core.Statement.Command.runCall (lhs : List Expression.Ident) (procName : String) (args : List Expression.Expr) (fuel : Nat) (E : Env) : Env

Interpret a single procedure call.

Importantly, this creates a separate Env to execute the body of the procedure with, which initially only contains input/output variables. The resulting Env is the original passed in Env with the output variables copied back into it.

Equations

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

@[irreducible]

def Core.Statement.Command.run (fuel : Nat) (E : Env) (c : Command) : Env

Equations

• One or more equations did not get rendered due to their size.
• Core.Statement.Command.run fuel E (Imperative.CmdExt.cmd c_2) = Imperative.Cmd.run E c_2