inductive Core.Statement.CondType : Type

• Requires : CondType
• Ensures : CondType

@[implicit_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) (old_var_subst : SubstMap) (c : Command) : Command × Env

Equations

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

@[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 (Core.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.funcDecl decl md) = false
• 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 (Core.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.funcDecl decl md) = []
• 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 (Core.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.funcDecl decl md) = []
• 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

def Core.Statement.captureFreevars (env : Env) (paramNames : List CoreIdent) (e : Expression.Expr) : Expression.Expr

Substitute free variables in an expression with their current values from the environment, excluding the given parameter names (which are bound by the function, not free). This implements value capture semantics for local function declarations (funcDecl).

Unlike global functions (which are evaluated at the top level with no local state), local functions capture the values of free variables at the point of declaration. Parameters are excluded because they are bound by the function definition and should not be substituted with values from the enclosing scope.

Equations

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

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.

@[irreducible]

def Core.Statement.evalAuxGo (steps : Nat) (old_var_subst : SubstMap) (Ewns : List EnvWithNext) (ss : Statements) (nextSplitId : Nat) : List EnvWithNext × Statistics × Nat

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) (old_var_subst : SubstMap) (Ewn : EnvWithNext) (cond cond' : Expression.Expr) (then_ss else_ss : Statements) (nextSplitId : Nat) : List EnvWithNext × Statistics × Nat

Equations

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

def Core.Statement.evalAux (E : Env) (old_var_subst : SubstMap) (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) (old_var_subst : SubstMap) (ss : Statements) : List Env × Statistics

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

The argument old_var_subst below is a substitution map from global variables to their pre-state value in the enclosing procedure of ss.

Equations

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

def Core.Statement.evalOne (E : Env) (old_var_subst : SubstMap) (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

• Core.Statement.Command.run fuel E (Core.CmdExt.cmd c_2) = Imperative.Cmd.run E c_2
• Core.Statement.Command.run fuel E (Core.CmdExt.call pname callArgs md) = Core.Statement.Command.runCall (Core.CallArg.getLhs callArgs) pname (Core.CallArg.getInputExprs callArgs) fuel E