This module contains the implementation of the reflection monad, used by all other components of this directory.

instance Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVBinOp : Lean.ToExpr Std.Tactic.BVDecide.BVBinOp

Equations

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

instance Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVUnOp : Lean.ToExpr Std.Tactic.BVDecide.BVUnOp

Equations

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

instance Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVExpr {w : Nat} : Lean.ToExpr (Std.Tactic.BVDecide.BVExpr w)

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVExpr.go {w : Nat} : Std.Tactic.BVDecide.BVExpr w → Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVExpr.go (Std.Tactic.BVDecide.BVExpr.var idx) = Lean.mkApp2 (Lean.mkConst `Std.Tactic.BVDecide.BVExpr.var) (Lean.toExpr w) (Lean.toExpr idx)
• Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVExpr.go (Std.Tactic.BVDecide.BVExpr.const val) = Lean.mkApp2 (Lean.mkConst `Std.Tactic.BVDecide.BVExpr.const) (Lean.toExpr w) (Lean.toExpr val)

instance Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVBinPred : Lean.ToExpr Std.Tactic.BVDecide.BVBinPred

Equations

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

instance Lean.Elab.Tactic.BVDecide.Frontend.instToExprGate : Lean.ToExpr Std.Tactic.BVDecide.Gate

Equations

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

instance Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVPred : Lean.ToExpr Std.Tactic.BVDecide.BVPred

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVPred.go : Std.Tactic.BVDecide.BVPred → Lean.Expr

Equations

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

instance Lean.Elab.Tactic.BVDecide.Frontend.instToExprBoolExpr {α : Type} [Lean.ToExpr α] : Lean.ToExpr (Std.Tactic.BVDecide.BoolExpr α)

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.instToExprBoolExpr.go {α : Type} [Lean.ToExpr α] : Std.Tactic.BVDecide.BoolExpr α → Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.BVDecide.Frontend.instToExprBoolExpr.go (Std.Tactic.BVDecide.BoolExpr.const b) = Lean.mkApp2 (Lean.mkConst `Std.Tactic.BVDecide.BoolExpr.const) (Lean.toTypeExpr α) (Lean.toExpr b)

structure Lean.Elab.Tactic.BVDecide.Frontend.Atom : Type

A BitVec atom.

• width : Nat

  The width of the BitVec that is being abstracted.

• atomNumber : Nat

  A unique numeric identifier for the atom.

• synthetic : Bool

  Whether the atom is synthetic. The effect of this is that values for this atom are not considered for the counter example deriviation. This is for example useful when we introduce an atom over an expression, together with additional lemmas that fully describe the behavior of the atom.

structure Lean.Elab.Tactic.BVDecide.Frontend.State : Type

The state of the reflection monad

• atoms : Std.HashMap Lean.Expr Lean.Elab.Tactic.BVDecide.Frontend.Atom

  The atoms encountered so far. Saved as a map from BitVec expressions to a (width, atomNumber) pair.

• atomsAssignmentCache : Lean.Expr

  A cache for atomsAssignment.

@[reducible, inline]

abbrev Lean.Elab.Tactic.BVDecide.Frontend.M (α : Type) : Type

The reflection monad, used to track BitVec variables that we see as we traverse the context.

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.M = StateRefT' IO.RealWorld Lean.Elab.Tactic.BVDecide.Frontend.State Lean.MetaM

structure Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr : Type

A reified version of an Expr representing a BVExpr.

• width : Nat
• bvExpr : Std.Tactic.BVDecide.BVExpr self.width

  The reified expression.

• evalsAtAtoms : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr

  A proof that bvExpr.eval atomsAssignment = originalBVExpr.

• expr : Lean.Expr

  A cache for toExpr bvExpr.

structure Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred : Type

A reified version of an Expr representing a BVPred.

• bvPred : Std.Tactic.BVDecide.BVPred

  The reified expression.

• evalsAtAtoms : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr

  A proof that bvPred.eval atomsAssignment = originalBVPredExpr.

• expr : Lean.Expr

  A cache for toExpr bvPred

structure Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical : Type

A reified version of an Expr representing a BVLogicalExpr.

• bvExpr : Std.Tactic.BVDecide.BVLogicalExpr

  The reified expression.

• evalsAtAtoms : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr

  A proof that bvExpr.eval atomsAssignment = originalBVLogicalExpr.

• expr : Lean.Expr

  A cache for toExpr bvExpr

structure Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical : Type

A reified version of an Expr representing a BVLogicalExpr that we know to be true.

• bvExpr : Std.Tactic.BVDecide.BVLogicalExpr

  The reified expression.

• satAtAtoms : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr

  A proof that bvExpr.eval atomsAssignment = true.

• expr : Lean.Expr

  A cache for toExpr bvExpr

def Lean.Elab.Tactic.BVDecide.Frontend.M.run {α : Type} (m : Lean.Elab.Tactic.BVDecide.Frontend.M α) : Lean.MetaM α

Run a reflection computation as a MetaM one.

Equations

• m.run = StateRefT'.run' m { atoms := ∅, atomsAssignmentCache := Lean.mkConst `List.nil [Lean.Level.zero] }

def Lean.Elab.Tactic.BVDecide.Frontend.M.atoms : Lean.Elab.Tactic.BVDecide.Frontend.M (List (Nat × Lean.Expr))

Retrieve the atoms as pairs of their width and expression.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.M.atomsAssignment : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr

Retrieve a BitVec.Assignment representing the atoms we found so far.

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.M.atomsAssignment = do let __do_lift ← getThe Lean.Elab.Tactic.BVDecide.Frontend.State pure __do_lift.atomsAssignmentCache

def Lean.Elab.Tactic.BVDecide.Frontend.M.lookup (e : Lean.Expr) (width : Nat) (synthetic : Bool) : Lean.Elab.Tactic.BVDecide.Frontend.M Nat

Look up an expression in the atoms, recording it if it has not previously appeared.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.M.lookup.updateAtomsAssignment : Lean.Elab.Tactic.BVDecide.Frontend.M Unit

Equations

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

structure Lean.Elab.Tactic.BVDecide.Frontend.LemmaState : Type

The state of the lemma reflection monad.

• lemmas : Array Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical

  The list of top level lemmas that got created on the fly during reflection.

@[reducible, inline]

abbrev Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (α : Type) : Type

The lemma reflection monad. It extends the usual reflection monad M by adding the ability to add additional top level lemmas on the fly.

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.LemmaM = StateRefT' IO.RealWorld Lean.Elab.Tactic.BVDecide.Frontend.LemmaState Lean.Elab.Tactic.BVDecide.Frontend.M

def Lean.Elab.Tactic.BVDecide.Frontend.LemmaM.run {α : Type} (m : Lean.Elab.Tactic.BVDecide.Frontend.LemmaM α) (state : Lean.Elab.Tactic.BVDecide.Frontend.LemmaState := { lemmas := #[] }) : Lean.Elab.Tactic.BVDecide.Frontend.M (α × Array Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical)

Equations

• m.run state = do let __discr ← StateRefT'.run m state match __discr with | (res, state) => pure (res, state.lemmas)

def Lean.Elab.Tactic.BVDecide.Frontend.LemmaM.addLemma (lemma : Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical) : Lean.Elab.Tactic.BVDecide.Frontend.LemmaM Unit

Add another top level lemma.

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.LemmaM.addLemma lemma = modify fun (s : Lean.Elab.Tactic.BVDecide.Frontend.LemmaState) => { lemmas := s.lemmas.push lemma }