perf: more sharing and caching in bv_decide's reflection (#7698)
This PR adds more sharing and caching procedures to bv_decide's reflection step. In particular we cache the reflection proof better, enforce better term sharing in the reflected term, which in turn speeds up bitblasting as bitblaster cache lookups can be checked with pointer equality. This PR was motivated by SMTLIB problem `QF_BV/Sage2/bench_7415.smt2`
This commit is contained in:
Henrik Böving
GitHub
parent
17c18752ff
commit
060b2fe46f
9 changed files with 226 additions and 161 deletions
|
|
@ -35,15 +35,15 @@ def mkContext (lratPath : System.FilePath) (cfg : BVDecideConfig) : TermElabM Ta
|
|||
/--
|
||||
Prepare an `Expr` that proves `bvExpr.unsat` using `ofReduceBool`.
|
||||
-/
|
||||
def lratChecker (ctx : TacticContext) (bvExpr : BVLogicalExpr) : MetaM Expr := do
|
||||
def lratChecker (ctx : TacticContext) (reflectionResult : ReflectionResult) : MetaM Expr := do
|
||||
let cert ← LratCert.ofFile ctx.lratPath ctx.config.trimProofs
|
||||
cert.toReflectionProof ctx bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
|
||||
cert.toReflectionProof ctx reflectionResult
|
||||
|
||||
@[inherit_doc Lean.Parser.Tactic.bvCheck]
|
||||
def bvCheck (g : MVarId) (ctx : TacticContext) : MetaM Unit := do
|
||||
let unsatProver : UnsatProver := fun _ reflectionResult _ => do
|
||||
withTraceNode `Meta.Tactic.sat (fun _ => return "Preparing LRAT reflection term") do
|
||||
let proof ← lratChecker ctx reflectionResult.bvExpr
|
||||
let proof ← lratChecker ctx reflectionResult
|
||||
return .ok ⟨proof, ""⟩
|
||||
let _ ← closeWithBVReflection g unsatProver
|
||||
return ()
|
||||
|
|
|
|||
|
|
@ -79,9 +79,22 @@ def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Ar
|
|||
return finalMap
|
||||
|
||||
structure ReflectionResult where
|
||||
/--
|
||||
The reflected expression.
|
||||
-/
|
||||
bvExpr : BVLogicalExpr
|
||||
/--
|
||||
Function to prove `False` given a satisfiability proof of `bvExpr`
|
||||
-/
|
||||
proveFalse : Expr → M Expr
|
||||
/--
|
||||
Set of unused hypotheses for diagnostic purposes.
|
||||
-/
|
||||
unusedHypotheses : Std.HashSet FVarId
|
||||
/--
|
||||
A cache for `toExpr bvExpr`.
|
||||
-/
|
||||
expr : Expr
|
||||
|
||||
/--
|
||||
A counter example generated from the bitblaster.
|
||||
|
|
@ -257,6 +270,54 @@ def explainCounterExampleQuality (counterExample : CounterExample) : MetaM Messa
|
|||
err := diagnosis.derivedEquations.foldl (init := err) folder
|
||||
return err
|
||||
|
||||
/--
|
||||
Turn an `LratCert` into a proof that some `reflectedExpr` is UNSAT.
|
||||
-/
|
||||
def LratCert.toReflectionProof (cert : LratCert) (cfg : TacticContext)
|
||||
(reflectionResult : ReflectionResult) : MetaM Expr := do
|
||||
withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling expr term") do
|
||||
mkAuxDecl cfg.exprDef reflectionResult.expr (mkConst ``BVLogicalExpr)
|
||||
|
||||
withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling proof certificate term") do
|
||||
mkAuxDecl cfg.certDef (toExpr cert) (mkConst ``String)
|
||||
|
||||
let reflectedExpr := mkConst cfg.exprDef
|
||||
let certExpr := mkConst cfg.certDef
|
||||
|
||||
withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling reflection proof term") do
|
||||
let auxValue := mkApp2 (mkConst ``verifyBVExpr) reflectedExpr certExpr
|
||||
mkAuxDecl cfg.reflectionDef auxValue (mkConst ``Bool)
|
||||
|
||||
let auxType ← mkEq (mkConst cfg.reflectionDef) (toExpr true)
|
||||
let auxProof :=
|
||||
mkApp3
|
||||
(mkConst ``Lean.ofReduceBool)
|
||||
(mkConst cfg.reflectionDef)
|
||||
(toExpr true)
|
||||
(← mkEqRefl (toExpr true))
|
||||
try
|
||||
let auxLemma ←
|
||||
-- disable async TC so we can catch its exceptions
|
||||
withOptions (Elab.async.set · false) do
|
||||
withTraceNode `Meta.Tactic.sat (fun _ => return "Verifying LRAT certificate") do
|
||||
mkAuxLemma [] auxType auxProof
|
||||
return mkApp3 (mkConst ``unsat_of_verifyBVExpr_eq_true) reflectedExpr certExpr (mkConst auxLemma)
|
||||
catch e =>
|
||||
throwError m!"Failed to check the LRAT certificate in the kernel:\n{e.toMessageData}"
|
||||
where
|
||||
/--
|
||||
Add an auxiliary declaration. Only used to create constants that appear in our reflection proof.
|
||||
-/
|
||||
mkAuxDecl (name : Name) (value type : Expr) : CoreM Unit :=
|
||||
addAndCompile <| .defnDecl {
|
||||
name := name,
|
||||
levelParams := [],
|
||||
type := type,
|
||||
value := value,
|
||||
hints := .abbrev,
|
||||
safety := .safe
|
||||
}
|
||||
|
||||
def lratBitblaster (goal : MVarId) (ctx : TacticContext) (reflectionResult : ReflectionResult)
|
||||
(atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) :
|
||||
MetaM (Except CounterExample UnsatProver.Result) := do
|
||||
|
|
@ -287,14 +348,13 @@ def lratBitblaster (goal : MVarId) (ctx : TacticContext) (reflectionResult : Ref
|
|||
match res with
|
||||
| .ok cert =>
|
||||
trace[Meta.Tactic.sat] "SAT solver found a proof."
|
||||
let proof ← cert.toReflectionProof ctx bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
|
||||
let proof ← cert.toReflectionProof ctx reflectionResult
|
||||
return .ok ⟨proof, cert⟩
|
||||
| .error assignment =>
|
||||
trace[Meta.Tactic.sat] "SAT solver found a counter example."
|
||||
let equations := reconstructCounterExample map assignment aigSize atomsAssignment
|
||||
return .error { goal, unusedHypotheses := reflectionResult.unusedHypotheses, equations }
|
||||
|
||||
|
||||
def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do
|
||||
let hyps ← getPropHyps
|
||||
let mut sats := #[]
|
||||
|
|
@ -314,12 +374,12 @@ def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do
|
|||
else
|
||||
let sat := sats[1:].foldl (init := sats[0]) SatAtBVLogical.and
|
||||
return {
|
||||
bvExpr := sat.bvExpr,
|
||||
bvExpr := ShareCommon.shareCommon sat.bvExpr,
|
||||
proveFalse := sat.proveFalse,
|
||||
unusedHypotheses := unusedHypotheses
|
||||
unusedHypotheses := unusedHypotheses,
|
||||
expr := sat.expr
|
||||
}
|
||||
|
||||
|
||||
def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
|
||||
MetaM (Except CounterExample LratCert) := M.run do
|
||||
g.withContext do
|
||||
|
|
|
|||
|
|
@ -142,6 +142,11 @@ structure State where
|
|||
contained in `atoms`.
|
||||
-/
|
||||
atomsAssignmentCache : Option Expr := none
|
||||
/--
|
||||
Cached calls to `evalsAtAtoms` of various reflection structures. Whenever `atoms` is modified
|
||||
this cache is invalidated as `evalsAtAtoms` relies on `atoms`.
|
||||
-/
|
||||
evalsAtCache : Std.HashMap Expr (Option Expr) := {}
|
||||
|
||||
/--
|
||||
The reflection monad, used to track `BitVec` variables that we see as we traverse the context.
|
||||
|
|
@ -158,14 +163,26 @@ structure ReifiedBVExpr where
|
|||
-/
|
||||
bvExpr : BVExpr width
|
||||
/--
|
||||
A proof that `bvExpr.eval atomsAssignment = originalBVExpr`, none if it holds by `rfl`.
|
||||
The expression that was reflected, used for caching of `evalsAtAtoms`.
|
||||
-/
|
||||
evalsAtAtoms : M (Option Expr)
|
||||
originalExpr : Expr
|
||||
/--
|
||||
A proof that `bvExpr.eval atomsAssignment = originalExpr`, none if it holds by `rfl`.
|
||||
-/
|
||||
evalsAtAtoms' : M (Option Expr)
|
||||
/--
|
||||
A cache for `toExpr bvExpr`.
|
||||
-/
|
||||
expr : Expr
|
||||
|
||||
def ReifiedBVExpr.evalsAtAtoms (reified : ReifiedBVExpr) : M (Option Expr) := do
|
||||
match (← get).evalsAtCache[reified.originalExpr]? with
|
||||
| some hit => return hit
|
||||
| none =>
|
||||
let proof? ← reified.evalsAtAtoms'
|
||||
modify fun s => { s with evalsAtCache := s.evalsAtCache.insert reified.originalExpr proof? }
|
||||
return proof?
|
||||
|
||||
/--
|
||||
A reified version of an `Expr` representing a `BVPred`.
|
||||
-/
|
||||
|
|
@ -175,14 +192,26 @@ structure ReifiedBVPred where
|
|||
-/
|
||||
bvPred : BVPred
|
||||
/--
|
||||
A proof that `bvPred.eval atomsAssignment = originalBVPredExpr`, none if it holds by `rfl`.
|
||||
The expression that was reflected, usef for caching of `evalsAtAtoms`.
|
||||
-/
|
||||
evalsAtAtoms : M (Option Expr)
|
||||
originalExpr : Expr
|
||||
/--
|
||||
A proof that `bvPred.eval atomsAssignment = originalExpr`, none if it holds by `rfl`.
|
||||
-/
|
||||
evalsAtAtoms' : M (Option Expr)
|
||||
/--
|
||||
A cache for `toExpr bvPred`
|
||||
-/
|
||||
expr : Expr
|
||||
|
||||
def ReifiedBVPred.evalsAtAtoms (reified : ReifiedBVPred) : M (Option Expr) := do
|
||||
match (← get).evalsAtCache[reified.originalExpr]? with
|
||||
| some hit => return hit
|
||||
| none =>
|
||||
let proof? ← reified.evalsAtAtoms'
|
||||
modify fun s => { s with evalsAtCache := s.evalsAtCache.insert reified.originalExpr proof? }
|
||||
return proof?
|
||||
|
||||
/--
|
||||
A reified version of an `Expr` representing a `BVLogicalExpr`.
|
||||
-/
|
||||
|
|
@ -192,14 +221,26 @@ structure ReifiedBVLogical where
|
|||
-/
|
||||
bvExpr : BVLogicalExpr
|
||||
/--
|
||||
A proof that `bvExpr.eval atomsAssignment = originalBVLogicalExpr`, none if it holds by `rfl`.
|
||||
The expression that was reflected, usef for caching of `evalsAtAtoms`.
|
||||
-/
|
||||
evalsAtAtoms : M (Option Expr)
|
||||
originalExpr : Expr
|
||||
/--
|
||||
A proof that `bvExpr.eval atomsAssignment = originalExpr`, none if it holds by `rfl`.
|
||||
-/
|
||||
evalsAtAtoms' : M (Option Expr)
|
||||
/--
|
||||
A cache for `toExpr bvExpr`
|
||||
-/
|
||||
expr : Expr
|
||||
|
||||
def ReifiedBVLogical.evalsAtAtoms (reified : ReifiedBVLogical) : M (Option Expr) := do
|
||||
match (← get).evalsAtCache[reified.originalExpr]? with
|
||||
| some hit => return hit
|
||||
| none =>
|
||||
let proof? ← reified.evalsAtAtoms'
|
||||
modify fun s => { s with evalsAtCache := s.evalsAtCache.insert reified.originalExpr proof? }
|
||||
return proof?
|
||||
|
||||
/--
|
||||
A reified version of an `Expr` representing a `BVLogicalExpr` that we know to be true.
|
||||
-/
|
||||
|
|
@ -266,7 +307,15 @@ def lookup (e : Expr) (width : Nat) (synthetic : Bool) : M Nat := do
|
|||
trace[Meta.Tactic.bv] "New atom of width {width}, synthetic? {synthetic}: {e}"
|
||||
let ident ← modifyGetThe State fun s =>
|
||||
let newAtom := { width, synthetic, atomNumber := s.atoms.size}
|
||||
(s.atoms.size, { s with atoms := s.atoms.insert e newAtom, atomsAssignmentCache := none })
|
||||
let newAtomNumber := s.atoms.size
|
||||
let s := {
|
||||
s with
|
||||
atoms := s.atoms.insert e newAtom,
|
||||
-- must clear the caches as they depend on `atoms`.
|
||||
atomsAssignmentCache := none
|
||||
evalsAtCache := {}
|
||||
}
|
||||
(newAtomNumber, s)
|
||||
return ident
|
||||
|
||||
@[specialize]
|
||||
|
|
|
|||
|
|
@ -39,7 +39,7 @@ def mkAtom (e : Expr) (width : Nat) (synthetic : Bool) : M ReifiedBVExpr := do
|
|||
let expr := mkApp2 (mkConst ``BVExpr.var) (toExpr width) (toExpr ident)
|
||||
-- This is safe because this proof always holds definitionally.
|
||||
let proof := pure none
|
||||
return ⟨width, .var ident, proof, expr⟩
|
||||
return ⟨width, .var ident, expr, proof, expr⟩
|
||||
|
||||
/--
|
||||
Parse `expr` as a `Nat` or `BitVec` constant depending on `ty`.
|
||||
|
|
@ -71,7 +71,7 @@ def mkBVConst (val : BitVec w) : M ReifiedBVExpr := do
|
|||
let expr := mkApp2 (mkConst ``BVExpr.const) (toExpr w) (toExpr val)
|
||||
-- This is safe because this proof always holds definitionally.
|
||||
let proof := pure none
|
||||
return ⟨w, bvExpr, proof, expr⟩
|
||||
return ⟨w, bvExpr, toExpr val, proof, expr⟩
|
||||
|
||||
end ReifiedBVExpr
|
||||
|
||||
|
|
|
|||
|
|
@ -33,8 +33,9 @@ Construct a `ReifiedBVLogical` from `ReifiedBVPred` by wrapping it as an atom.
|
|||
def ofPred (bvPred : ReifiedBVPred) : M ReifiedBVLogical := do
|
||||
let boolExpr := .literal bvPred.bvPred
|
||||
let expr := mkApp2 (mkConst ``BoolExpr.literal) (mkConst ``BVPred) bvPred.expr
|
||||
-- important: This must be the same proof as the bvPred one in order for the cache to be correct
|
||||
let proof := bvPred.evalsAtAtoms
|
||||
return ⟨boolExpr, proof, expr⟩
|
||||
return ⟨boolExpr, bvPred.originalExpr, proof, expr⟩
|
||||
|
||||
/--
|
||||
Construct an uninterrpeted `Bool` atom from `t`.
|
||||
|
|
@ -51,14 +52,14 @@ def mkBoolConst (val : Bool) : M ReifiedBVLogical := do
|
|||
let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr val)
|
||||
-- This is safe because this proof always holds definitionally.
|
||||
let proof := pure none
|
||||
return ⟨boolExpr, proof, expr⟩
|
||||
return ⟨boolExpr, toExpr val, proof, expr⟩
|
||||
|
||||
/--
|
||||
Construct the reified version of applying the gate in `gate` to `lhs` and `rhs`.
|
||||
This function assumes that `lhsExpr` and `rhsExpr` are the corresponding expressions to `lhs`
|
||||
and `rhs`.
|
||||
-/
|
||||
def mkGate (lhs rhs : ReifiedBVLogical) (lhsExpr rhsExpr : Expr) (gate : Gate) :
|
||||
def mkGate (lhs rhs : ReifiedBVLogical) (lhsExpr rhsExpr : Expr) (gate : Gate) (origExpr : Expr) :
|
||||
M ReifiedBVLogical := do
|
||||
let congrThm := congrThmOfGate gate
|
||||
let boolExpr := .gate gate lhs.bvExpr rhs.bvExpr
|
||||
|
|
@ -84,7 +85,7 @@ def mkGate (lhs rhs : ReifiedBVLogical) (lhsExpr rhsExpr : Expr) (gate : Gate) :
|
|||
lhsExpr rhsExpr
|
||||
lhsEvalExpr rhsEvalExpr
|
||||
lhsProof rhsProof
|
||||
return ⟨boolExpr, proof, expr⟩
|
||||
return ⟨boolExpr, origExpr, proof, expr⟩
|
||||
where
|
||||
congrThmOfGate (gate : Gate) : Name :=
|
||||
match gate with
|
||||
|
|
@ -97,7 +98,7 @@ where
|
|||
Construct the reified version of `Bool.not subExpr`.
|
||||
This function assumes that `subExpr` is the expression corresponding to `sub`.
|
||||
-/
|
||||
def mkNot (sub : ReifiedBVLogical) (subExpr : Expr) : M ReifiedBVLogical := do
|
||||
def mkNot (sub : ReifiedBVLogical) (subExpr : Expr) (origExpr : Expr) : M ReifiedBVLogical := do
|
||||
let boolExpr := .not sub.bvExpr
|
||||
let expr := mkApp2 (mkConst ``BoolExpr.not) (mkConst ``BVPred) sub.expr
|
||||
let proof := do
|
||||
|
|
@ -105,14 +106,14 @@ def mkNot (sub : ReifiedBVLogical) (subExpr : Expr) : M ReifiedBVLogical := do
|
|||
let some subProof ← sub.evalsAtAtoms | return none
|
||||
let subEvalExpr ← ReifiedBVLogical.mkEvalExpr sub.expr
|
||||
return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof
|
||||
return ⟨boolExpr, proof, expr⟩
|
||||
return ⟨boolExpr, origExpr, proof, expr⟩
|
||||
|
||||
/--
|
||||
Construct the reified version of `if discrExpr then lhsExpr else rhsExpr`.
|
||||
This function assumes that `discrExpr`, lhsExpr` and `rhsExpr` are the corresponding expressions to
|
||||
`discr`, `lhs` and `rhs`.
|
||||
-/
|
||||
def mkIte (discr lhs rhs : ReifiedBVLogical) (discrExpr lhsExpr rhsExpr : Expr) :
|
||||
def mkIte (discr lhs rhs : ReifiedBVLogical) (discrExpr lhsExpr rhsExpr : Expr) (origExpr : Expr) :
|
||||
M ReifiedBVLogical := do
|
||||
let boolExpr := .ite discr.bvExpr lhs.bvExpr rhs.bvExpr
|
||||
let expr :=
|
||||
|
|
@ -140,7 +141,7 @@ def mkIte (discr lhs rhs : ReifiedBVLogical) (discrExpr lhsExpr rhsExpr : Expr)
|
|||
discrExpr lhsExpr rhsExpr
|
||||
discrEvalExpr lhsEvalExpr rhsEvalExpr
|
||||
discrProof lhsProof rhsProof
|
||||
return ⟨boolExpr, proof, expr⟩
|
||||
return ⟨boolExpr, origExpr, proof, expr⟩
|
||||
|
||||
end ReifiedBVLogical
|
||||
|
||||
|
|
|
|||
|
|
@ -19,9 +19,9 @@ open Lean.Meta
|
|||
namespace ReifiedBVPred
|
||||
|
||||
/--
|
||||
Construct an uninterpreted `Bool` atom from `t`.
|
||||
Construct an uninterpreted `Bool` atom from `origExpr`.
|
||||
-/
|
||||
def boolAtom (t : Expr) : M (Option ReifiedBVPred) := do
|
||||
def boolAtom (origExpr : Expr) : M (Option ReifiedBVPred) := do
|
||||
/-
|
||||
Idea: we have t : Bool here, let's construct:
|
||||
BitVec.ofBool t : BitVec 1
|
||||
|
|
@ -29,9 +29,9 @@ def boolAtom (t : Expr) : M (Option ReifiedBVPred) := do
|
|||
BitVec.getLsb (BitVec.ofBool t) 0 : Bool
|
||||
We can prove that this is equivalent to `t`. This allows us to have boolean variables in BVPred.
|
||||
-/
|
||||
let ty ← inferType t
|
||||
let ty ← inferType origExpr
|
||||
let_expr Bool := ty | return none
|
||||
let atom ← ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) t) 1 false
|
||||
let atom ← ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) origExpr) 1 false
|
||||
let bvExpr : BVPred := .getLsbD atom.bvExpr 0
|
||||
let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr 1) atom.expr (toExpr 0)
|
||||
let proof := do
|
||||
|
|
@ -41,18 +41,18 @@ def boolAtom (t : Expr) : M (Option ReifiedBVPred) := do
|
|||
let atomProof := (← atom.evalsAtAtoms).getD (ReifiedBVExpr.mkBVRefl atom.width atomEval)
|
||||
return mkApp3
|
||||
(mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.ofBool_congr)
|
||||
t
|
||||
origExpr
|
||||
atomEval
|
||||
atomProof
|
||||
return some ⟨bvExpr, proof, expr⟩
|
||||
return some ⟨bvExpr, origExpr, proof, expr⟩
|
||||
|
||||
/--
|
||||
Construct the reified version of applying the predicate in `pred` to `lhs` and `rhs`.
|
||||
This function assumes that `lhsExpr` and `rhsExpr` are the corresponding expressions to `lhs`
|
||||
and `rhs`.
|
||||
-/
|
||||
def mkBinPred (lhs rhs : ReifiedBVExpr) (lhsExpr rhsExpr : Expr) (pred : BVBinPred) :
|
||||
M (Option ReifiedBVPred) := do
|
||||
def mkBinPred (lhs rhs : ReifiedBVExpr) (lhsExpr rhsExpr : Expr) (pred : BVBinPred)
|
||||
(origExpr : Expr) : M (Option ReifiedBVPred) := do
|
||||
if h : lhs.width = rhs.width then
|
||||
let congrThm := congrThmofBinPred pred
|
||||
let bvExpr : BVPred := .bin (w := lhs.width) lhs.bvExpr pred (h ▸ rhs.bvExpr)
|
||||
|
|
@ -79,7 +79,7 @@ def mkBinPred (lhs rhs : ReifiedBVExpr) (lhsExpr rhsExpr : Expr) (pred : BVBinPr
|
|||
lhsExpr rhsExpr lhsEval rhsEval
|
||||
lhsProof
|
||||
rhsProof
|
||||
return some ⟨bvExpr, proof, expr⟩
|
||||
return some ⟨bvExpr, origExpr, proof, expr⟩
|
||||
else
|
||||
return none
|
||||
where
|
||||
|
|
@ -92,7 +92,8 @@ where
|
|||
Construct the reified version of `BitVec.getLsbD subExpr idx`.
|
||||
This function assumes that `subExpr` is the expression corresponding to `sub`.
|
||||
-/
|
||||
def mkGetLsbD (sub : ReifiedBVExpr) (subExpr : Expr) (idx : Nat) : M ReifiedBVPred := do
|
||||
def mkGetLsbD (sub : ReifiedBVExpr) (subExpr : Expr) (idx : Nat) (origExpr : Expr) :
|
||||
M ReifiedBVPred := do
|
||||
let bvExpr : BVPred := .getLsbD sub.bvExpr idx
|
||||
let idxExpr := toExpr idx
|
||||
let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr sub.width) sub.expr idxExpr
|
||||
|
|
@ -107,7 +108,7 @@ def mkGetLsbD (sub : ReifiedBVExpr) (subExpr : Expr) (idx : Nat) : M ReifiedBVPr
|
|||
subExpr
|
||||
subEval
|
||||
subProof
|
||||
return ⟨bvExpr, proof, expr⟩
|
||||
return ⟨bvExpr, origExpr, proof, expr⟩
|
||||
|
||||
end ReifiedBVPred
|
||||
|
||||
|
|
|
|||
|
|
@ -37,15 +37,16 @@ where
|
|||
let resValExpr := lhs
|
||||
let lemmaName := ``Std.Tactic.BVDecide.Reflect.BitVec.cond_true
|
||||
|
||||
|
||||
let notDiscrExpr := mkApp (mkConst ``Bool.not) discrExpr
|
||||
let notDiscr ← ReifiedBVLogical.mkNot discr discrExpr
|
||||
let notDiscr ← ReifiedBVLogical.mkNot discr discrExpr notDiscrExpr
|
||||
|
||||
let eqBVExpr ← mkAppM ``BEq.beq #[atomExpr, resExpr]
|
||||
let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq | return none
|
||||
let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq eqBVExpr
|
||||
| return none
|
||||
let eqBV ← ReifiedBVLogical.ofPred eqBVPred
|
||||
|
||||
let imp ← ReifiedBVLogical.mkGate notDiscr eqBV notDiscrExpr eqBVExpr .or
|
||||
let orExpr := mkApp2 (mkConst ``Bool.or) notDiscrExpr eqBVExpr
|
||||
let imp ← ReifiedBVLogical.mkGate notDiscr eqBV notDiscrExpr eqBVExpr .or orExpr
|
||||
|
||||
let proof := do
|
||||
let evalExpr ← ReifiedBVLogical.mkEvalExpr imp.expr
|
||||
|
|
@ -70,10 +71,12 @@ where
|
|||
let lemmaName := ``Std.Tactic.BVDecide.Reflect.BitVec.cond_false
|
||||
|
||||
let eqBVExpr ← mkAppM ``BEq.beq #[atomExpr, resExpr]
|
||||
let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq | return none
|
||||
let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq eqBVExpr
|
||||
| return none
|
||||
let eqBV ← ReifiedBVLogical.ofPred eqBVPred
|
||||
|
||||
let imp ← ReifiedBVLogical.mkGate discr eqBV discrExpr eqBVExpr .or
|
||||
let orExpr := mkApp2 (mkConst ``Bool.or) discrExpr eqBVExpr
|
||||
let imp ← ReifiedBVLogical.mkGate discr eqBV discrExpr eqBVExpr .or orExpr
|
||||
|
||||
let proof := do
|
||||
let evalExpr ← ReifiedBVLogical.mkEvalExpr imp.expr
|
||||
|
|
|
|||
|
|
@ -24,29 +24,29 @@ Reify an `Expr` that's a constant-width `BitVec`.
|
|||
Unless this function is called on something that is not a constant-width `BitVec` it is always
|
||||
going to return `some`.
|
||||
-/
|
||||
partial def ReifiedBVExpr.of (x : Expr) : LemmaM (Option ReifiedBVExpr) := do
|
||||
goOrAtom x
|
||||
partial def ReifiedBVExpr.of (origExpr : Expr) : LemmaM (Option ReifiedBVExpr) := do
|
||||
goOrAtom origExpr
|
||||
where
|
||||
/--
|
||||
Reify `x`, returns `none` if the reification procedure failed.
|
||||
-/
|
||||
go (x : Expr) : LemmaM (Option ReifiedBVExpr) := do
|
||||
match_expr x with
|
||||
| BitVec.ofNat _ _ => goBvLit x
|
||||
go (origExpr : Expr) : LemmaM (Option ReifiedBVExpr) := do
|
||||
match_expr origExpr with
|
||||
| BitVec.ofNat _ _ => goBvLit origExpr
|
||||
| HAnd.hAnd _ _ _ _ lhsExpr rhsExpr =>
|
||||
binaryReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.BitVec.and_congr
|
||||
binaryReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.BitVec.and_congr origExpr
|
||||
| HXor.hXor _ _ _ _ lhsExpr rhsExpr =>
|
||||
binaryReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.BitVec.xor_congr
|
||||
binaryReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.BitVec.xor_congr origExpr
|
||||
| HAdd.hAdd _ _ _ _ lhsExpr rhsExpr =>
|
||||
binaryReflection lhsExpr rhsExpr .add ``Std.Tactic.BVDecide.Reflect.BitVec.add_congr
|
||||
binaryReflection lhsExpr rhsExpr .add ``Std.Tactic.BVDecide.Reflect.BitVec.add_congr origExpr
|
||||
| HMul.hMul _ _ _ _ lhsExpr rhsExpr =>
|
||||
binaryReflection lhsExpr rhsExpr .mul ``Std.Tactic.BVDecide.Reflect.BitVec.mul_congr
|
||||
binaryReflection lhsExpr rhsExpr .mul ``Std.Tactic.BVDecide.Reflect.BitVec.mul_congr origExpr
|
||||
| HDiv.hDiv _ _ _ _ lhsExpr rhsExpr =>
|
||||
binaryReflection lhsExpr rhsExpr .udiv ``Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr
|
||||
binaryReflection lhsExpr rhsExpr .udiv ``Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr origExpr
|
||||
| HMod.hMod _ _ _ _ lhsExpr rhsExpr =>
|
||||
binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr
|
||||
binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr origExpr
|
||||
| Complement.complement _ _ innerExpr =>
|
||||
unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr
|
||||
unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr origExpr
|
||||
| HShiftLeft.hShiftLeft _ β _ _ innerExpr distanceExpr =>
|
||||
let distance? ← ReifiedBVExpr.getNatOrBvValue? β distanceExpr
|
||||
if distance?.isSome then throwError "internal error: constant shift should have been eliminated."
|
||||
|
|
@ -57,6 +57,7 @@ where
|
|||
.shiftLeft
|
||||
``BVExpr.shiftLeft
|
||||
``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeft_congr
|
||||
origExpr
|
||||
| HShiftRight.hShiftRight _ β _ _ innerExpr distanceExpr =>
|
||||
let distance? ← ReifiedBVExpr.getNatOrBvValue? β distanceExpr
|
||||
if distance?.isSome then throwError "internal error: constant shift should have been eliminated."
|
||||
|
|
@ -67,6 +68,7 @@ where
|
|||
.shiftRight
|
||||
``BVExpr.shiftRight
|
||||
``Std.Tactic.BVDecide.Reflect.BitVec.shiftRight_congr
|
||||
origExpr
|
||||
| BitVec.sshiftRight _ innerExpr distanceExpr =>
|
||||
let some distance ← getNatValue? distanceExpr | return none
|
||||
shiftConstLikeReflection
|
||||
|
|
@ -75,6 +77,7 @@ where
|
|||
.arithShiftRightConst
|
||||
``BVUnOp.arithShiftRightConst
|
||||
``Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRightNat_congr
|
||||
origExpr
|
||||
| BitVec.sshiftRight' _ _ innerExpr distanceExpr =>
|
||||
shiftReflection
|
||||
distanceExpr
|
||||
|
|
@ -82,6 +85,7 @@ where
|
|||
.arithShiftRight
|
||||
``BVExpr.arithShiftRight
|
||||
``Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRight_congr
|
||||
origExpr
|
||||
| HAppend.hAppend _ _ _ _ lhsExpr rhsExpr =>
|
||||
let some lhs ← goOrAtom lhsExpr | return none
|
||||
let some rhs ← goOrAtom rhsExpr | return none
|
||||
|
|
@ -109,7 +113,7 @@ where
|
|||
lhsExpr lhsEval
|
||||
rhsExpr rhsEval
|
||||
lhsProof rhsProof
|
||||
return some ⟨lhs.width + rhs.width, bvExpr, proof, expr⟩
|
||||
return some ⟨lhs.width + rhs.width, bvExpr, origExpr, proof, expr⟩
|
||||
| BitVec.replicate _ nExpr innerExpr =>
|
||||
let some inner ← goOrAtom innerExpr | return none
|
||||
let some n ← getNatValue? nExpr | return none
|
||||
|
|
@ -132,7 +136,7 @@ where
|
|||
innerExpr
|
||||
innerEval
|
||||
innerProof
|
||||
return some ⟨inner.width * n, bvExpr, proof, expr⟩
|
||||
return some ⟨inner.width * n, bvExpr, origExpr, proof, expr⟩
|
||||
| BitVec.extractLsb' _ startExpr lenExpr innerExpr =>
|
||||
let some start ← getNatValue? startExpr | return none
|
||||
let some len ← getNatValue? lenExpr | return none
|
||||
|
|
@ -154,7 +158,7 @@ where
|
|||
innerExpr
|
||||
innerEval
|
||||
innerProof
|
||||
return some ⟨len, bvExpr, proof, expr⟩
|
||||
return some ⟨len, bvExpr, origExpr, proof, expr⟩
|
||||
| BitVec.rotateLeft _ innerExpr distanceExpr =>
|
||||
rotateReflection
|
||||
distanceExpr
|
||||
|
|
@ -162,6 +166,7 @@ where
|
|||
.rotateLeft
|
||||
``BVUnOp.rotateLeft
|
||||
``Std.Tactic.BVDecide.Reflect.BitVec.rotateLeft_congr
|
||||
origExpr
|
||||
| BitVec.rotateRight _ innerExpr distanceExpr =>
|
||||
rotateReflection
|
||||
distanceExpr
|
||||
|
|
@ -169,29 +174,30 @@ where
|
|||
.rotateRight
|
||||
``BVUnOp.rotateRight
|
||||
``Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr
|
||||
origExpr
|
||||
| cond _ discrExpr lhsExpr rhsExpr =>
|
||||
let some atom ← ReifiedBVExpr.bitVecAtom x true | return none
|
||||
let some atom ← ReifiedBVExpr.bitVecAtom origExpr true | return none
|
||||
let some discr ← ReifiedBVLogical.of discrExpr | return none
|
||||
let some lhs ← goOrAtom lhsExpr | return none
|
||||
let some rhs ← goOrAtom rhsExpr | return none
|
||||
addCondLemmas discr atom lhs rhs discrExpr x lhsExpr rhsExpr
|
||||
addCondLemmas discr atom lhs rhs discrExpr origExpr lhsExpr rhsExpr
|
||||
return some atom
|
||||
| _ => return none
|
||||
|
||||
/--
|
||||
Reify `x` or abstract it as an atom.
|
||||
Reify `origExpr` or abstract it as an atom.
|
||||
Unless this function is called on something that is not a fixed-width `BitVec` it is always going
|
||||
to return `some`.
|
||||
-/
|
||||
goOrAtom (x : Expr) : LemmaM (Option ReifiedBVExpr) := do
|
||||
LemmaM.withBVExprCache x fun x => do
|
||||
let res ← go x
|
||||
goOrAtom (origExpr : Expr) : LemmaM (Option ReifiedBVExpr) := do
|
||||
LemmaM.withBVExprCache origExpr fun origExpr => do
|
||||
let res ← go origExpr
|
||||
match res with
|
||||
| some exp => return some exp
|
||||
| none => ReifiedBVExpr.bitVecAtom x false
|
||||
| none => ReifiedBVExpr.bitVecAtom origExpr false
|
||||
|
||||
shiftConstLikeReflection (distance : Nat) (innerExpr : Expr) (shiftOp : Nat → BVUnOp)
|
||||
(shiftOpName : Name) (congrThm : Name) :
|
||||
(shiftOpName : Name) (congrThm : Name) (origExpr : Expr) :
|
||||
LemmaM (Option ReifiedBVExpr) := do
|
||||
let some inner ← goOrAtom innerExpr | return none
|
||||
let bvExpr : BVExpr inner.width := .un (shiftOp distance) inner.bvExpr
|
||||
|
|
@ -206,17 +212,17 @@ where
|
|||
(mkConst congrThm)
|
||||
(toExpr distance)
|
||||
let proof := unaryCongrProof inner innerExpr congrProof
|
||||
return some ⟨inner.width, bvExpr, proof, expr⟩
|
||||
return some ⟨inner.width, bvExpr, origExpr, proof, expr⟩
|
||||
|
||||
rotateReflection (distanceExpr : Expr) (innerExpr : Expr) (rotateOp : Nat → BVUnOp)
|
||||
(rotateOpName : Name) (congrThm : Name) :
|
||||
(rotateOpName : Name) (congrThm : Name) (origExpr : Expr) :
|
||||
LemmaM (Option ReifiedBVExpr) := do
|
||||
let some distance ← getNatValue? distanceExpr | return none
|
||||
shiftConstLikeReflection distance innerExpr rotateOp rotateOpName congrThm
|
||||
shiftConstLikeReflection distance innerExpr rotateOp rotateOpName congrThm origExpr
|
||||
|
||||
shiftReflection (distanceExpr : Expr) (innerExpr : Expr)
|
||||
(shiftOp : {m n : Nat} → BVExpr m → BVExpr n → BVExpr m) (shiftOpName : Name)
|
||||
(congrThm : Name) :
|
||||
(congrThm : Name) (origExpr : Expr) :
|
||||
LemmaM (Option ReifiedBVExpr) := do
|
||||
let some inner ← goOrAtom innerExpr | return none
|
||||
let some distance ← goOrAtom distanceExpr | return none
|
||||
|
|
@ -234,9 +240,9 @@ where
|
|||
(toExpr inner.width)
|
||||
(toExpr distance.width)
|
||||
let proof := binaryCongrProof inner distance innerExpr distanceExpr congrProof
|
||||
return some ⟨inner.width, bvExpr, proof, expr⟩
|
||||
return some ⟨inner.width, bvExpr, origExpr, proof, expr⟩
|
||||
|
||||
binaryReflection (lhsExpr rhsExpr : Expr) (op : BVBinOp) (congrThm : Name) :
|
||||
binaryReflection (lhsExpr rhsExpr : Expr) (op : BVBinOp) (congrThm : Name) (origExpr : Expr) :
|
||||
LemmaM (Option ReifiedBVExpr) := do
|
||||
let some lhs ← goOrAtom lhsExpr | return none
|
||||
let some rhs ← goOrAtom rhsExpr | return none
|
||||
|
|
@ -245,7 +251,7 @@ where
|
|||
let expr := mkApp4 (mkConst ``BVExpr.bin) (toExpr lhs.width) lhs.expr (toExpr op) rhs.expr
|
||||
let congrThm := mkApp (mkConst congrThm) (toExpr lhs.width)
|
||||
let proof := binaryCongrProof lhs rhs lhsExpr rhsExpr congrThm
|
||||
return some ⟨lhs.width, bvExpr, proof, expr⟩
|
||||
return some ⟨lhs.width, bvExpr, origExpr, proof, expr⟩
|
||||
else
|
||||
return none
|
||||
|
||||
|
|
@ -262,13 +268,13 @@ where
|
|||
rhsEval rhsProof? | return none
|
||||
return mkApp6 congrThm lhsExpr rhsExpr lhsEval rhsEval lhsProof rhsProof
|
||||
|
||||
unaryReflection (innerExpr : Expr) (op : BVUnOp) (congrThm : Name) :
|
||||
unaryReflection (innerExpr : Expr) (op : BVUnOp) (congrThm : Name) (origExpr : Expr) :
|
||||
LemmaM (Option ReifiedBVExpr) := do
|
||||
let some inner ← goOrAtom innerExpr | return none
|
||||
let bvExpr := .un op inner.bvExpr
|
||||
let expr := mkApp3 (mkConst ``BVExpr.un) (toExpr inner.width) (toExpr op) inner.expr
|
||||
let proof := unaryCongrProof inner innerExpr (mkConst congrThm)
|
||||
return some ⟨inner.width, bvExpr, proof, expr⟩
|
||||
return some ⟨inner.width, bvExpr, origExpr, proof, expr⟩
|
||||
|
||||
unaryCongrProof (inner : ReifiedBVExpr) (innerExpr : Expr) (congrProof : Expr) : M (Option Expr) := do
|
||||
let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
|
||||
|
|
@ -283,82 +289,83 @@ where
|
|||
Reify an `Expr` that is a predicate about `BitVec`.
|
||||
Unless this function is called on something that is not a `Bool` it is always going to return `some`.
|
||||
-/
|
||||
partial def ReifiedBVPred.of (t : Expr) : LemmaM (Option ReifiedBVPred) := do
|
||||
LemmaM.withBVPredCache t fun t => do
|
||||
match ← go t with
|
||||
partial def ReifiedBVPred.of (origExpr : Expr) : LemmaM (Option ReifiedBVPred) := do
|
||||
LemmaM.withBVPredCache origExpr fun origExpr => do
|
||||
match ← go origExpr with
|
||||
| some pred => return some pred
|
||||
| none => ReifiedBVPred.boolAtom t
|
||||
| none => ReifiedBVPred.boolAtom origExpr
|
||||
where
|
||||
/--
|
||||
Reify `t`, returns `none` if the reification procedure failed.
|
||||
Reify `origExpr`, returns `none` if the reification procedure failed.
|
||||
-/
|
||||
go (t : Expr) : LemmaM (Option ReifiedBVPred) := do
|
||||
match_expr t with
|
||||
go (origExpr : Expr) : LemmaM (Option ReifiedBVPred) := do
|
||||
match_expr origExpr with
|
||||
| BEq.beq α _ lhsExpr rhsExpr =>
|
||||
let_expr BitVec _ := α | return none
|
||||
binaryReflection lhsExpr rhsExpr .eq
|
||||
binaryReflection lhsExpr rhsExpr .eq origExpr
|
||||
| BitVec.ult _ lhsExpr rhsExpr =>
|
||||
binaryReflection lhsExpr rhsExpr .ult
|
||||
binaryReflection lhsExpr rhsExpr .ult origExpr
|
||||
| BitVec.getLsbD _ subExpr idxExpr =>
|
||||
let some sub ← ReifiedBVExpr.of subExpr | return none
|
||||
let some idx ← getNatValue? idxExpr | return none
|
||||
return some (← ReifiedBVPred.mkGetLsbD sub subExpr idx)
|
||||
return some (← ReifiedBVPred.mkGetLsbD sub subExpr idx origExpr)
|
||||
| _ => return none
|
||||
|
||||
binaryReflection (lhsExpr rhsExpr : Expr) (pred : BVBinPred) : LemmaM (Option ReifiedBVPred) := do
|
||||
binaryReflection (lhsExpr rhsExpr : Expr) (pred : BVBinPred) (origExpr : Expr) :
|
||||
LemmaM (Option ReifiedBVPred) := do
|
||||
let some lhs ← ReifiedBVExpr.of lhsExpr | return none
|
||||
let some rhs ← ReifiedBVExpr.of rhsExpr | return none
|
||||
ReifiedBVPred.mkBinPred lhs rhs lhsExpr rhsExpr pred
|
||||
ReifiedBVPred.mkBinPred lhs rhs lhsExpr rhsExpr pred origExpr
|
||||
|
||||
/--
|
||||
Reify an `Expr` that is a boolean expression containing predicates about `BitVec` as atoms.
|
||||
Unless this function is called on something that is not a `Bool` it is always going to return `some`.
|
||||
-/
|
||||
partial def ReifiedBVLogical.of (t : Expr) : LemmaM (Option ReifiedBVLogical) := do
|
||||
goOrAtom t
|
||||
partial def ReifiedBVLogical.of (origExpr : Expr) : LemmaM (Option ReifiedBVLogical) := do
|
||||
goOrAtom origExpr
|
||||
where
|
||||
/--
|
||||
Reify `t`, returns `none` if the reification procedure failed.
|
||||
-/
|
||||
go (t : Expr) : LemmaM (Option ReifiedBVLogical) := do
|
||||
match_expr t with
|
||||
go (origExpr : Expr) : LemmaM (Option ReifiedBVLogical) := do
|
||||
match_expr origExpr with
|
||||
| Bool.true => ReifiedBVLogical.mkBoolConst true
|
||||
| Bool.false => ReifiedBVLogical.mkBoolConst false
|
||||
| Bool.not subExpr =>
|
||||
let some sub ← goOrAtom subExpr | return none
|
||||
return some (← ReifiedBVLogical.mkNot sub subExpr)
|
||||
| Bool.and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and
|
||||
| Bool.xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor
|
||||
return some (← ReifiedBVLogical.mkNot sub subExpr origExpr)
|
||||
| Bool.and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and origExpr
|
||||
| Bool.xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor origExpr
|
||||
| BEq.beq α _ lhsExpr rhsExpr =>
|
||||
match_expr α with
|
||||
| Bool => gateReflection lhsExpr rhsExpr .beq
|
||||
| BitVec _ => goPred t
|
||||
| Bool => gateReflection lhsExpr rhsExpr .beq origExpr
|
||||
| BitVec _ => goPred origExpr
|
||||
| _ => return none
|
||||
| cond _ discrExpr lhsExpr rhsExpr =>
|
||||
let some discr ← goOrAtom discrExpr | return none
|
||||
let some lhs ← goOrAtom lhsExpr | return none
|
||||
let some rhs ← goOrAtom rhsExpr | return none
|
||||
return some (← ReifiedBVLogical.mkIte discr lhs rhs discrExpr lhsExpr rhsExpr)
|
||||
| _ => goPred t
|
||||
return some (← ReifiedBVLogical.mkIte discr lhs rhs discrExpr lhsExpr rhsExpr origExpr)
|
||||
| _ => goPred origExpr
|
||||
|
||||
/--
|
||||
Reify `t` or abstract it as an atom.
|
||||
Unless this function is called on something that is not a `Bool` it is always going to return `some`.
|
||||
-/
|
||||
goOrAtom (t : Expr) : LemmaM (Option ReifiedBVLogical) := do
|
||||
LemmaM.withBVLogicalCache t fun t => do
|
||||
match ← go t with
|
||||
goOrAtom (origExpr : Expr) : LemmaM (Option ReifiedBVLogical) := do
|
||||
LemmaM.withBVLogicalCache origExpr fun origExpr => do
|
||||
match ← go origExpr with
|
||||
| some boolExpr => return some boolExpr
|
||||
| none => ReifiedBVLogical.boolAtom t
|
||||
| none => ReifiedBVLogical.boolAtom origExpr
|
||||
|
||||
gateReflection (lhsExpr rhsExpr : Expr) (gate : Gate) :
|
||||
gateReflection (lhsExpr rhsExpr : Expr) (gate : Gate) (origExpr : Expr) :
|
||||
LemmaM (Option ReifiedBVLogical) := do
|
||||
let some lhs ← goOrAtom lhsExpr | return none
|
||||
let some rhs ← goOrAtom rhsExpr | return none
|
||||
ReifiedBVLogical.mkGate lhs rhs lhsExpr rhsExpr gate
|
||||
ReifiedBVLogical.mkGate lhs rhs lhsExpr rhsExpr gate origExpr
|
||||
|
||||
goPred (t : Expr) : LemmaM (Option ReifiedBVLogical) := do
|
||||
let some pred ← ReifiedBVPred.of t | return none
|
||||
goPred (origExpr : Expr) : LemmaM (Option ReifiedBVLogical) := do
|
||||
let some pred ← ReifiedBVPred.of origExpr | return none
|
||||
ReifiedBVLogical.ofPred pred
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -148,61 +148,5 @@ def runExternal (cnf : CNF Nat) (solver : System.FilePath) (lratPath : System.Fi
|
|||
|
||||
return .ok lratProof
|
||||
|
||||
/--
|
||||
Add an auxiliary declaration. Only used to create constants that appear in our reflection proof.
|
||||
-/
|
||||
def mkAuxDecl (name : Name) (value type : Expr) : CoreM Unit :=
|
||||
addAndCompile <| .defnDecl {
|
||||
name := name,
|
||||
levelParams := [],
|
||||
type := type,
|
||||
value := value,
|
||||
hints := .abbrev,
|
||||
safety := .safe
|
||||
}
|
||||
|
||||
/--
|
||||
Turn an `LratCert` into a proof that some `reflected` expression is UNSAT by providing a `verifier`
|
||||
function together with a correctness theorem for it.
|
||||
|
||||
- `verifier` is expected to have type `α → LratCert → Bool`
|
||||
- `unsat_of_verifier_eq_true` is expected to have type
|
||||
`∀ (b : α) (c : LratCert), verifier b c = true → unsat b`
|
||||
-/
|
||||
def LratCert.toReflectionProof [ToExpr α] (cert : LratCert) (cfg : TacticContext) (reflected : α)
|
||||
(verifier : Name) (unsat_of_verifier_eq_true : Name) : MetaM Expr := do
|
||||
withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling expr term") do
|
||||
mkAuxDecl cfg.exprDef (toExpr reflected) (toTypeExpr α)
|
||||
|
||||
let certType := toTypeExpr LratCert
|
||||
|
||||
withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling proof certificate term") do
|
||||
mkAuxDecl cfg.certDef (toExpr cert) certType
|
||||
|
||||
let reflectedExpr := mkConst cfg.exprDef
|
||||
let certExpr := mkConst cfg.certDef
|
||||
|
||||
withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling reflection proof term") do
|
||||
let auxValue := mkApp2 (mkConst verifier) reflectedExpr certExpr
|
||||
mkAuxDecl cfg.reflectionDef auxValue (mkConst ``Bool)
|
||||
|
||||
let auxType ← mkEq (mkConst cfg.reflectionDef) (toExpr true)
|
||||
let auxProof :=
|
||||
mkApp3
|
||||
(mkConst ``Lean.ofReduceBool)
|
||||
(mkConst cfg.reflectionDef)
|
||||
(toExpr true)
|
||||
(← mkEqRefl (toExpr true))
|
||||
try
|
||||
let auxLemma ←
|
||||
-- disable async TC so we can catch its exceptions
|
||||
withOptions (Elab.async.set · false) do
|
||||
withTraceNode `Meta.Tactic.sat (fun _ => return "Verifying LRAT certificate") do
|
||||
mkAuxLemma [] auxType auxProof
|
||||
return mkApp3 (mkConst unsat_of_verifier_eq_true) reflectedExpr certExpr (mkConst auxLemma)
|
||||
catch e =>
|
||||
throwError m!"Failed to check the LRAT certificate in the kernel:\n{e.toMessageData}"
|
||||
|
||||
|
||||
end Frontend
|
||||
end Lean.Elab.Tactic.BVDecide
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue