inductive Core.Statement.CondType : Type

• Requires : CondType
• Ensures : CondType

instance Core.Statement.instToStringCondType : ToString CondType

Equations

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

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

Evaluate a procedure call lhs := pname(args).

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.
• Core.Statement.Command.eval E old_var_subst (Core.CmdExt.call lhs pname args md) = Core.Statement.Command.evalCall E old_var_subst lhs pname args md

@[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 invariant 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.goto label 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 invariant body_ss md) = Core.Statement.Statements.collectCovers body_ss
• Core.Statement.Statement.collectCovers (Imperative.Stmt.funcDecl decl md) = []
• Core.Statement.Statement.collectCovers (Imperative.Stmt.goto label 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 invariant body_ss md) = Core.Statement.Statements.collectAsserts body_ss
• Core.Statement.Statement.collectAsserts (Imperative.Stmt.funcDecl decl md) = []
• Core.Statement.Statement.collectAsserts (Imperative.Stmt.goto label 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.createFailingCoverObligations (covers : List (String × Imperative.MetaData Expression)) : Imperative.ProofObligations Expression

Equations

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

def Core.Statement.createPassingAssertObligations (asserts : List (String × Imperative.MetaData Expression)) : Imperative.ProofObligations Expression

Equations

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

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.

@[reducible, inline]

abbrev Core.Statement.StmtsStack : Type

Equations

• Core.Statement.StmtsStack = List Core.Statements

def Core.Statement.StmtsStack.push (stk : StmtsStack) (ss : Statements) : StmtsStack

Equations

• stk.push ss = ss.eraseTypes :: stk

def Core.Statement.StmtsStack.pop (stk : StmtsStack) : StmtsStack

Equations

• Core.Statement.StmtsStack.pop [] = []
• Core.Statement.StmtsStack.pop (head :: rst) = rst

def Core.Statement.StmtsStack.top (stk : StmtsStack) : Statements

Equations

• Core.Statement.StmtsStack.top [] = []
• Core.Statement.StmtsStack.top (head :: rst) = head

def Core.Statement.StmtsStack.appendToTop (stk : StmtsStack) (ss : Statements) : StmtsStack

Equations

• stk.appendToTop ss = (stk.top ++ ss.eraseTypes) :: stk.pop

structure Core.Statement.EnvWithNext : Type

A new environment with an optional next label to execute and transformed statements (i.e., statements that have already been evaluated).

• env : Env
• nextLabel : Option String
• stk : StmtsStack

def Core.Statement.processGoto : Statements → Option String → Statements × Option String

Drop statements up to the given label, and indicate whether goto needs to propagate up.

NOTE: We only allow forward-gotos right now.

Equations

• Core.Statement.processGoto x✝ none = (x✝, none)
• Core.Statement.processGoto x✝ (some l) = match List.dropWhile (fun (s : Core.Statement) => !Imperative.Stmt.hasLabel l s) x✝ with | [] => ([], some l) | rest' => (rest', none)

@[irreducible]

def Core.Statement.evalAuxGo (steps : Nat) (old_var_subst : SubstMap) (Ewn : EnvWithNext) (ss : Statements) (optLabel : Option String) : List EnvWithNext

Equations

• One or more equations did not get rendered due to their size.
• Core.Statement.evalAuxGo steps✝ old_var_subst Ewn ss optLabel = [{ env := Ewn.env, stk := Ewn.stk }]

@[irreducible]

def Core.Statement.processIteBranches (steps : Nat) (old_var_subst : SubstMap) (Ewn : EnvWithNext) (cond cond' : Expression.Expr) (then_ss else_ss : Statements) (md : Imperative.MetaData Expression) (orig_stk : StmtsStack) : List EnvWithNext

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) (optLabel : Option String) : List EnvWithNext

Equations

• Core.Statement.evalAux E old_var_subst ss optLabel = Core.Statement.evalAuxGo (Imperative.Block.sizeOf ss) old_var_subst { env := E } ss optLabel

def Core.Statement.gotoToError : EnvWithNext → Statements × Env

Equations

• One or more equations did not get rendered due to their size.
• Core.Statement.gotoToError { env := env, stk := stk } = (List.flatten stk, env)

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

Partial evaluator for statements yielding a list of environments and transformed statements.

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 = List.map Core.Statement.gotoToError (Core.Statement.evalAux E old_var_subst ss none)

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

Partial evaluator for statements yielding one environment and transformed statements.

Equations

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