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

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

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

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

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

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

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

source
def Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVExpr.go {w : Nat} :
Std.Tactic.BVDecide.BVExpr w → 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)

Instances For

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

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

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

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

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

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

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

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

Instances For

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

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

source
def Lean.Elab.Tactic.BVDecide.Frontend.instToExprBoolExpr.go {α : Type} [ToExpr α] :
Std.Tactic.BVDecide.BoolExpr α → 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)

Instances For

source
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 derivation. 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.

Instances For

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

The state of the reflection monad

- atoms : Std.HashMap Expr Atom

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

- atomsAssignmentCache : Option Expr

  A cache for `atomsAssignment`. If it is `none` the cache is currently invalidated as new atoms have been added since it was last updated, if it is `some` it must be consistent with the atoms contained in `atoms`.

- evalsAtCache : Std.HashMap Expr (Option Expr)

  Cached calls to `evalsAtAtoms` of various reflection structures. Whenever `atoms` is modified this cache is invalidated as `evalsAtAtoms` relies on `atoms`.

Instances For

source
@[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

Instances For

source
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.

- originalExpr : Expr

  The expression that was reflected, used for caching of `evalsAtAtoms`.

- evalsAtAtoms' : M (Option Expr)

  A proof that `bvExpr.eval atomsAssignment = originalExpr`, none if it holds by `rfl`.

- expr : Expr

  A cache for `toExpr bvExpr`.

Instances For

source
def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.evalsAtAtoms (reified : ReifiedBVExpr) :
M (Option Expr)
Equations

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

Instances For

source
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.

- originalExpr : Expr

  The expression that was reflected, usef for caching of `evalsAtAtoms`.

- evalsAtAtoms' : M (Option Expr)

  A proof that `bvPred.eval atomsAssignment = originalExpr`, none if it holds by `rfl`.

- expr : Expr

  A cache for `toExpr bvPred`

Instances For

source
def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred.evalsAtAtoms (reified : ReifiedBVPred) :
M (Option Expr)
Equations

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

Instances For

source
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.

- originalExpr : Expr

  The expression that was reflected, usef for caching of `evalsAtAtoms`.

- evalsAtAtoms' : M (Option Expr)

  A proof that `bvExpr.eval atomsAssignment = originalExpr`, none if it holds by `rfl`.

- expr : Expr

  A cache for `toExpr bvExpr`

Instances For

source
def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.evalsAtAtoms (reified : ReifiedBVLogical) :
M (Option Expr)
Equations

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

Instances For

source
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 : M Expr

  A proof that `bvExpr.eval atomsAssignment = true`.

- expr : Expr

  A cache for `toExpr bvExpr`

Instances For

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

Run a reflection computation as a `MetaM` one.

Equations

- m.run = StateRefT'.run' m { }

Instances For

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

Retrieve the atoms as pairs of their width and expression.

Equations

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

Instances For

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

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

Equations

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

Instances For

source
def Lean.Elab.Tactic.BVDecide.Frontend.M.lookup (e : Expr) (width : Nat) (synthetic : Bool) :
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.

Instances For

source
@[specialize #[]]
def Lean.Elab.Tactic.BVDecide.Frontend.M.simplifyBinaryProof' (mkFRefl : Expr → Expr) (fst : Expr) (fproof : Option Expr) (mkSRefl : Expr → Expr) (snd : Expr) (sproof : Option Expr) :
Option (Expr × Expr)
Equations

- Lean.Elab.Tactic.BVDecide.Frontend.M.simplifyBinaryProof' mkFRefl fst (some fproof_2) mkSRefl snd (some sproof_2) = some (fproof_2, sproof_2)
- Lean.Elab.Tactic.BVDecide.Frontend.M.simplifyBinaryProof' mkFRefl fst (some fproof_2) mkSRefl snd none = some (fproof_2, mkSRefl snd)
- Lean.Elab.Tactic.BVDecide.Frontend.M.simplifyBinaryProof' mkFRefl fst none mkSRefl snd (some sproof_2) = some (mkFRefl fst, sproof_2)
- Lean.Elab.Tactic.BVDecide.Frontend.M.simplifyBinaryProof' mkFRefl fst none mkSRefl snd none = none

Instances For

source
@[specialize #[]]
def Lean.Elab.Tactic.BVDecide.Frontend.M.simplifyBinaryProof (mkRefl : Expr → Expr) (fst : Expr) (fproof : Option Expr) (snd : Expr) (sproof : Option Expr) :
Option (Expr × Expr)
Equations

- Lean.Elab.Tactic.BVDecide.Frontend.M.simplifyBinaryProof mkRefl fst fproof snd sproof = Lean.Elab.Tactic.BVDecide.Frontend.M.simplifyBinaryProof' mkRefl fst fproof mkRefl snd sproof

Instances For

source
@[specialize #[]]
def Lean.Elab.Tactic.BVDecide.Frontend.M.simplifyTernaryProof (mkRefl : Expr → Expr) (fst : Expr) (fproof : Option Expr) (snd : Expr) (sproof : Option Expr) (thd : Expr) (tproof : Option Expr) :
Option (Expr × Expr × Expr)
Equations

- Lean.Elab.Tactic.BVDecide.Frontend.M.simplifyTernaryProof mkRefl fst (some fproof_2) snd sproof thd tproof = some (fproof_2, stproof)
- Lean.Elab.Tactic.BVDecide.Frontend.M.simplifyTernaryProof mkRefl fst (some fproof_2) snd sproof thd tproof = some (fproof_2, mkRefl snd, mkRefl thd)
- Lean.Elab.Tactic.BVDecide.Frontend.M.simplifyTernaryProof mkRefl fst none snd sproof thd tproof = some (mkRefl fst, stproof)
- Lean.Elab.Tactic.BVDecide.Frontend.M.simplifyTernaryProof mkRefl fst none snd sproof thd tproof = none

Instances For

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

The state of the lemma reflection monad.

- lemmas : Array SatAtBVLogical

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

- bvExprCache : Std.HashMap Expr (Option ReifiedBVExpr)

  Cache for reification of `BVExpr`.

- bvPredCache : Std.HashMap Expr (Option ReifiedBVPred)

  Cache for reification of `BVPred`.

- bvLogicalCache : Std.HashMap Expr (Option ReifiedBVLogical)

  Cache for reification of `BVLogicalExpr`.

Instances For

source
@[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

Instances For

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

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

Instances For

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

Add another top level lemma.

Equations

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

Instances For

source
@[specialize #[]]
def Lean.Elab.Tactic.BVDecide.Frontend.LemmaM.withBVExprCache (e : Expr) (f : Expr → LemmaM (Option ReifiedBVExpr)) :
LemmaM (Option ReifiedBVExpr)
Equations

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

Instances For

source
@[specialize #[]]
def Lean.Elab.Tactic.BVDecide.Frontend.LemmaM.withBVPredCache (e : Expr) (f : Expr → LemmaM (Option ReifiedBVPred)) :
LemmaM (Option ReifiedBVPred)
Equations

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

Instances For

source
@[specialize #[]]
def Lean.Elab.Tactic.BVDecide.Frontend.LemmaM.withBVLogicalCache (e : Expr) (f : Expr → LemmaM (Option ReifiedBVLogical)) :
LemmaM (Option ReifiedBVLogical)
Equations

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

Instances For