structure Blaster.StateMachine.Invariant (α β : Type) : Type

Internal Invariant representation for state machine

• property : α → β → Prop

  property to be satisified

• label : String

  property label

• status : Smt.Result

  property status

class Blaster.StateMachine.StateMachine (α β : Type) : Type

Internal state machine representation where:

• α : specifies the input type
• β : specifies the state type

• init : α → β

  function to define the initial state

• next : α → β → β

  function to define the next state

• assumptions : α → β → Prop

  function to define any assumption about the input events and state

• invariants : α → β → Prop

  function to define any properties to be satisfied

structure Blaster.StateMachine.StateMachineEnv : Type

• inputType : Lean.Expr
• stateType : Lean.Expr
• smName : Lean.Name
• initFlag : Option Smt.SmtTerm

instance Blaster.StateMachine.instInhabitedStateMachineEnv : Inhabited StateMachineEnv

Equations

• Blaster.StateMachine.instInhabitedStateMachineEnv = { default := Blaster.StateMachine.instInhabitedStateMachineEnv.default }

def Blaster.StateMachine.instInhabitedStateMachineEnv.default : StateMachineEnv

Equations

• Blaster.StateMachine.instInhabitedStateMachineEnv.default = { inputType := default, stateType := default, smName := default, initFlag := default }

@[reducible, inline]

abbrev Blaster.StateMachine.StateMachineEnvT (α : Type) : Type

Equations

• Blaster.StateMachine.StateMachineEnvT = StateRefT' IO.RealWorld Blaster.StateMachine.StateMachineEnv Blaster.Optimize.TranslateEnvT

def Blaster.StateMachine.mkStateMachineConst : Optimize.TranslateEnvT Lean.Expr

Return StateMachine const expression and cache result.

Equations

• Blaster.StateMachine.mkStateMachineConst = Blaster.Optimize.mkExpr (Lean.mkConst `Blaster.StateMachine.StateMachine [Lean.levelZero])

def Blaster.StateMachine.mkInvariants : Optimize.TranslateEnvT Lean.Expr

Return Blaster.StateMachine.StateMachine.invariants const expression and cache result.

Equations

• Blaster.StateMachine.mkInvariants = Blaster.Optimize.mkExpr (Lean.mkConst `Blaster.StateMachine.StateMachine.invariants)

def Blaster.StateMachine.mkAssumptions : Optimize.TranslateEnvT Lean.Expr

Return Blaster.StateMachine.StateMachine.assumptions const expression and cache result.

Equations

• Blaster.StateMachine.mkAssumptions = Blaster.Optimize.mkExpr (Lean.mkConst `Blaster.StateMachine.StateMachine.assumptions)

def Blaster.StateMachine.mkInit : Optimize.TranslateEnvT Lean.Expr

Return Blaster.StateMachine.StateMachine.init const expression and cache result.

Equations

• Blaster.StateMachine.mkInit = Blaster.Optimize.mkExpr (Lean.mkConst `Blaster.StateMachine.StateMachine.init)

def Blaster.StateMachine.mkNext : Optimize.TranslateEnvT Lean.Expr

Return Blaster.StateMachine.StateMachine.next const expression and cache result.

Equations

• Blaster.StateMachine.mkNext = Blaster.Optimize.mkExpr (Lean.mkConst `Blaster.StateMachine.StateMachine.next)

def Blaster.StateMachine.incDepth : Optimize.TranslateEnvT Unit

Increment analysis depth

Equations

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

def Blaster.StateMachine.maxDepthReached : Optimize.TranslateEnvT Bool

Equations

• Blaster.StateMachine.maxDepthReached = do let env ← get pure (decide (env.optEnv.options.mcDepth > env.optEnv.options.solverOptions.maxDepth))

def Blaster.StateMachine.getMaxDepth : Optimize.TranslateEnvT Nat

Equations

• Blaster.StateMachine.getMaxDepth = do let __do_lift ← get pure __do_lift.optEnv.options.solverOptions.maxDepth

def Blaster.StateMachine.nameAtDepth (smName : Lean.Name) (suffix : String) : Optimize.TranslateEnvT Lean.Name

Equations

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

def Blaster.StateMachine.logDepthProgress (header : String) : Optimize.TranslateEnvT Unit

Equations

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

def Blaster.StateMachine.defineSmtInitFlag : Optimize.TranslateEnvT Smt.SmtTerm

Equations

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

def Blaster.StateMachine.defineInvAtDepth (inv : Smt.SmtTerm) : Optimize.TranslateEnvT Smt.SmtTerm

Equations

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

def Blaster.StateMachine.defineSmtDepthFlag : Optimize.TranslateEnvT Smt.SmtTerm

Equations

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

def Blaster.StateMachine.logNotInductiveAtDepth : Optimize.TranslateEnvT Unit

Equations

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

def Blaster.StateMachine.logNoCexAtDepth : Optimize.TranslateEnvT Unit

Equations

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

def Blaster.StateMachine.logUndeterminedAtDepth : Optimize.TranslateEnvT Unit

Equations

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

def Blaster.StateMachine.logCexAtDepth (r : Smt.Result) : Optimize.TranslateEnvT Unit

Equations

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

def Blaster.StateMachine.logCtiAtDepth (r : Smt.Result) : Optimize.TranslateEnvT Unit

Equations

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

def Blaster.StateMachine.logContradictionAtDepth : Optimize.TranslateEnvT Unit

Equations

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

def Blaster.StateMachine.getSMTypes (smInst : Lean.Expr) : Optimize.TranslateEnvT StateMachineEnv

Determine if smInst corresponds to a StateMachine instance and return a StateMachineEnv instance as result. Trigger an error when smInst is not a StateMachine instance.

Equations

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

def Blaster.StateMachine.assertAssumptions (smInst iVar state : Lean.Expr) : StateMachineEnvT Bool

Given smInst an instance of StateMachine, iVar input at step k and state at step k,

• assert assumptions iVar state
• check if current smt context is contradictory Return true if context is contradictory

Equations

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

def Blaster.StateMachine.assertAssumptions.translateAxioms (currDepth : Nat) : Optimize.TranslateEnvT Unit

Translate local axioms only when current depth is zero

Equations

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

def Blaster.StateMachine.assertAssumptions.checkContradiction (initFlag : Option Smt.SmtTerm) : Optimize.TranslateEnvT Smt.Result

Equations

• Blaster.StateMachine.assertAssumptions.checkContradiction none = Blaster.Smt.checkSat
• Blaster.StateMachine.assertAssumptions.checkContradiction (some iflag) = Blaster.Smt.checkSatAssuming #[iflag]