Documentation

Blaster.StateMachine.KInduction

source
def Blaster.StateMachine.kIndStrategy (smInst : Lean.Expr) :
Optimize.TranslateEnvT Unit

Given smInst an instance of StateMachine, perform the k-induction strategy for invariant satisfaction up to to Depth maxDepth. In particular, considering k = maxDepth, try to incrementally check if the following propositional formulae are satisfied: kIndStrategy(smInst) ≡ - base(k) = st₀ = init in₀ → (∀ i ∈ [0, k-1], assumptions inᵢ stᵢ ∧ stᵢ₊₁ = next inᵢ stᵢ) → assumptions inₖ stₖ → invariants inₖ stₖ -- base case satisfied - contradiction(k) - ∀ i ∈ [0, k], ¬ assumptions inᵢ stᵢ -- absence of contradiction

- step(k) =
   (∀ i ∈ [0, k-1], assumptions inᵢ stᵢ ∧ stᵢ₊₁ = next inᵢ stᵢ ∧ invariants inᵢ stᵢ) →
   assumptions inₖ stₖ →
   invariants inₖ stₖ -- induction step
  • A counterexample to induction is generated when step(k) is not satisfied for a given depth k
  • A counterexample is generated when base(k) is not satisfied. where: inᵢ : set of input variables at step ᵢ stᵢ : set of state variables at step ᵢ

Trigger an error when smInst is not an instance of StateMachine.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    partial def Blaster.StateMachine.kIndStrategy.visit (smInst : Lean.Expr) (prevState : Option Lean.Expr) :
    StateMachineEnvT Unit
    source
    def Blaster.StateMachine.kIndStrategy.withDeclState (smInst iVar : Lean.Expr) (pState : Option Lean.Expr) (f : Lean.Expr → StateMachineEnvT Unit) :
    StateMachineEnvT Unit
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[inline]
      def Blaster.StateMachine.kIndStrategy.invariantAtDepth (smInst iVar state : Lean.Expr) :
      StateMachineEnvT Lean.Expr
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Blaster.StateMachine.kIndStrategy.analysisAtDepth (invExpr : Lean.Expr) :
        StateMachineEnvT (Option Smt.Result)
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Blaster.StateMachine.kind :
          Lean.ParserDescr
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Blaster.StateMachine.kIndCommand (sOpts : Options.BlasterOptions) (stx : Lean.Syntax) :
            Lean.Elab.TermElabM Unit
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Blaster.StateMachine.kIndImp :
              Lean.Elab.Command.CommandElab
              Equations
              Instances For