|
| 1 | +/- |
| 2 | + Copyright Strata Contributors |
| 3 | +
|
| 4 | + SPDX-License-Identifier: Apache-2.0 OR MIT |
| 5 | +-/ |
| 6 | +module |
| 7 | + |
| 8 | +public import Strata.MetaVerifier -- shake: keep |
| 9 | +public import StrataBoole.Verify |
| 10 | +meta import Lean.Meta.Eval |
| 11 | +import Lean.Meta.Eval -- shake: keep |
| 12 | +import Lean.Meta.Tactic.Rewrite -- shake: keep |
| 13 | +meta import Lean.Meta.Tactic.Rewrite |
| 14 | +import Lean.Meta.Tactic.Unfold -- shake: keep |
| 15 | +meta import Lean.Meta.Tactic.Unfold |
| 16 | + |
| 17 | +/-! |
| 18 | +# Boole MetaVerifier |
| 19 | +
|
| 20 | +Extends `Strata.MetaVerifier` with Boole dialect support for `genCoreVCs` and |
| 21 | +`smtVCsCorrect`. Test files in the `StrataBoole` package should import this |
| 22 | +module instead of `Strata.MetaVerifier` directly. |
| 23 | +-/ |
| 24 | + |
| 25 | +public section |
| 26 | + |
| 27 | +namespace Strata.Boole |
| 28 | + |
| 29 | +def genVCs (program : Strata.Boole.Program) (gctx : Strata.GlobalContext) (options : Core.VerifyOptions := .default) : Option Core.coreVCs := do |
| 30 | + let program ← (Strata.Boole.toCoreProgram program gctx).toOption |
| 31 | + Core.genVCs program options |
| 32 | + |
| 33 | +end Strata.Boole |
| 34 | + |
| 35 | +namespace Strata |
| 36 | + |
| 37 | +/-- |
| 38 | +Generate verification conditions for a `Strata.Program`, with Boole support. |
| 39 | +Extends `Strata.genCoreVCs` to handle the Boole dialect. |
| 40 | +-/ |
| 41 | +def genCoreVCsBoole (program : Program) : Option Core.coreVCs := do |
| 42 | + if program.dialect == "Boole" then |
| 43 | + match Boole.getProgram program with |
| 44 | + | .ok booleProgram => |
| 45 | + Boole.genVCs booleProgram program.globalContext { (default : Core.VerifyOptions) with verbose := .quiet : Core.VerifyOptions } |
| 46 | + | .error _ => none |
| 47 | + else |
| 48 | + genCoreVCs program |
| 49 | + |
| 50 | +/-- |
| 51 | +Generate SMT verification conditions for a `Strata.Program`, with Boole support. |
| 52 | +-/ |
| 53 | +def genSMTVCsBoole (program : Program) : Option SMT.SMTVCs := do |
| 54 | + let coreVCs ← genCoreVCsBoole program |
| 55 | + toSMTVCs coreVCs |
| 56 | + |
| 57 | +/-- |
| 58 | +State semantic correctness of the SMT verification conditions generated for a |
| 59 | +program, with Boole dialect support. |
| 60 | +-/ |
| 61 | +def smtVCsCorrectBoole (program : Program) : Prop := |
| 62 | + match genSMTVCsBoole program with |
| 63 | + | some vcs => (denoteQueries vcs).getD False |
| 64 | + | none => False |
| 65 | + |
| 66 | +end Strata |
| 67 | + |
| 68 | +namespace Strata.Meta |
| 69 | + |
| 70 | +open Lean hiding Options |
| 71 | + |
| 72 | +private unsafe def genSMTVCsBooleUnsafe (mv : MVarId) : MetaM (List MVarId) := do |
| 73 | + let type ← mv.getType |
| 74 | + let some program := type.app1? ``Strata.smtVCsCorrectBoole | throwError "Expected a Strata.smtVCsCorrectBoole goal" |
| 75 | + trace[debug] m!"Generating SMT VCs for {program}" |
| 76 | + let mv ← Meta.unfoldTarget mv ``Strata.smtVCsCorrectBoole |
| 77 | + let ovcs := .app (.const ``Strata.genSMTVCsBoole []) program |
| 78 | + let ovcsType := .app (.const ``Option [0]) (.const ``Strata.SMT.SMTVCs []) |
| 79 | + let some evcs ← Meta.evalExpr (Option Strata.SMT.SMTVCs) ovcsType ovcs |
| 80 | + | throwError "Failed to generate VCs" |
| 81 | + trace[debug] m!"Generated {repr evcs}" |
| 82 | + let rhs := toExpr (some evcs) |
| 83 | + let eqVCs := mkApp3 (.const ``Eq [1]) ovcsType ovcs rhs |
| 84 | + let hEQVCs ← nativeDecide eqVCs |
| 85 | + let r ← mv.rewrite (← mv.getType) hEQVCs |
| 86 | + let mv ← mv.replaceTargetEq r.eNew r.eqProof |
| 87 | + let mvs ← evcs.mapM SMT.createGoal |
| 88 | + trace[debug] m!"Created {mvs.length} SMT VC goals: {mvs}" |
| 89 | + let ps ← mvs.mapM MVarId.getType |
| 90 | + let hP := andNIntro (List.zip ps (mvs.map Expr.mvar)) |
| 91 | + mv.assign hP |
| 92 | + return mvs |
| 93 | + |
| 94 | +@[implemented_by genSMTVCsBooleUnsafe] |
| 95 | +meta opaque genSMTVCsBoole (mv : MVarId) : MetaM (List MVarId) |
| 96 | + |
| 97 | +end Strata.Meta |
| 98 | + |
| 99 | +namespace Strata.Tactic |
| 100 | + |
| 101 | +open Lean Elab Tactic in |
| 102 | +/-- |
| 103 | +Generate one Lean goal per SMT verification condition in a goal of the form |
| 104 | +`Strata.smtVCsCorrectBoole program`. Boole-aware variant of `gen_smt_vcs`. |
| 105 | +-/ |
| 106 | +syntax (name := genSMTVCsBoole) "gen_smt_vcs_boole" : tactic |
| 107 | + |
| 108 | +open Lean Elab Tactic in |
| 109 | +@[tactic genSMTVCsBoole] meta def evalGenSMTVCsBoole : Tactic := fun stx => do |
| 110 | + match stx with |
| 111 | + | `(tactic| gen_smt_vcs_boole) => |
| 112 | + let mvs ← Meta.genSMTVCsBoole (← Tactic.getMainGoal) |
| 113 | + Tactic.replaceMainGoal mvs |
| 114 | + | _ => throwUnsupportedSyntax |
| 115 | + |
| 116 | +end Strata.Tactic |
| 117 | + |
| 118 | +end -- public section |
0 commit comments