max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: make bv_decide error when the LRAT proof is invalid (#5676)

Browse source
This commit is contained in:
Henrik Böving 2024-10-11 17:04:23 +02:00 • committed by GitHub
parent e5bbda1c3d
commit 087219bf5d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 9 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean
View file

@ -197,13 +197,20 @@ def LratCert.toReflectionProof [ToExpr α] (cert : LratCert) (cfg : TacticContex
let auxValue := mkApp2 (mkConst verifier) reflectedExpr certExpr
mkAuxDecl cfg.reflectionDef auxValue (mkConst ``Bool)
let nativeProof :=
let auxType ← mkEq (mkConst cfg.reflectionDef) (toExpr true)
let auxProof :=
mkApp3
(mkConst ``Lean.ofReduceBool)
(mkConst cfg.reflectionDef)
(toExpr true)
(← mkEqRefl (toExpr true))
return mkApp3 (mkConst unsat_of_verifier_eq_true) reflectedExpr certExpr nativeProof
try
let auxLemma ←
withTraceNode `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