diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index dccfd26d8f..3436613800 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -2259,42 +2259,6 @@ with grind ``` This is more convenient than the equivalent `· by rename_i _ acc _; exact I1 acc`. -### Witnesses - -When a specification has a parameter whose type is tagged with `@[mvcgen_witness_type]`, `mvcgen` -classifies the corresponding goal as a *witness* rather than a verification condition. -Witnesses are concrete values that the user must provide (inspired by zero-knowledge proofs), -as opposed to invariants (predicates maintained across loop iterations) or verification conditions -(propositions to prove). - -Witness goals are labelled `witness1`, `witness2`, etc. and can be provided in a `witnesses` section -that appears before the `invariants` section: -``` -mvcgen [...] witnesses -· W1 -· W2 -invariants -· I1 -with grind -``` -Like invariants, witnesses support case label syntax: -``` -mvcgen [...] witnesses -| witness1 => W1 -``` - -See the `@[mvcgen_witness_type]` attribute for how to register custom witness types. - -### Invariant and witness type attributes - -The `@[mvcgen_invariant_type]` and `@[mvcgen_witness_type]` tag attributes control how `mvcgen` -classifies subgoals: -* A goal whose type is an application of a type tagged with `@[mvcgen_invariant_type]` is classified - as an invariant (`inv`). -* A goal whose type is an application of a type tagged with `@[mvcgen_witness_type]` is classified - as a witness (`witness`). -* All other goals are classified as verification conditions (`vc`). - ### Invariant suggestions `mvcgen` will suggest invariants for you if you use the `invariants?` keyword. diff --git a/src/Lean/Elab/Tactic/Do/Attr.lean b/src/Lean/Elab/Tactic/Do/Attr.lean index d3e994622d..2d0040d874 100644 --- a/src/Lean/Elab/Tactic/Do/Attr.lean +++ b/src/Lean/Elab/Tactic/Do/Attr.lean @@ -268,24 +268,3 @@ def isMVCGenInvariantType (env : Environment) (ty : Expr) : Bool := mvcgenInvariantAttr.hasTag env name else false - -/-- -Marks a type as a witness type for the `mvcgen` tactic. -Goals whose type is an application of a tagged type will be classified -as witnesses rather than verification conditions. -In the spirit of zero-knowledge proofs, witnesses are concrete values that the user -must provide, as opposed to invariants (predicates maintained across iterations) -or verification conditions (propositions to prove). --/ -builtin_initialize mvcgenWitnessTypeAttr : TagAttribute ← - registerTagAttribute `mvcgen_witness_type - "marks a type as a witness type for the `mvcgen` tactic" - -/-- -Returns `true` if `ty` is an application of a type tagged with `@[mvcgen_witness_type]`. --/ -def isMVCGenWitnessType (env : Environment) (ty : Expr) : Bool := - if let .const name .. := ty.getAppFn then - mvcgenWitnessTypeAttr.hasTag env name - else - false diff --git a/src/Lean/Elab/Tactic/Do/VCGen.lean b/src/Lean/Elab/Tactic/Do/VCGen.lean index 7e0cd596e6..6788400d23 100644 --- a/src/Lean/Elab/Tactic/Do/VCGen.lean +++ b/src/Lean/Elab/Tactic/Do/VCGen.lean @@ -35,7 +35,6 @@ namespace VCGen structure Result where invariants : Array MVarId - witnesses : Array MVarId vcs : Array MVarId partial def genVCs (goal : MVarId) (ctx : Context) (fuel : Fuel) : MetaM Result := do @@ -46,13 +45,10 @@ partial def genVCs (goal : MVarId) (ctx : Context) (fuel : Fuel) : MetaM Result for h : idx in *...state.invariants.size do let mv := state.invariants[idx] mv.setTag (Name.mkSimple ("inv" ++ toString (idx + 1))) - for h : idx in *...state.witnesses.size do - let mv := state.witnesses[idx] - mv.setTag (Name.mkSimple ("witness" ++ toString (idx + 1))) for h : idx in *...state.vcs.size do let mv := state.vcs[idx] mv.setTag (Name.mkSimple ("vc" ++ toString (idx + 1)) ++ (← mv.getTag).eraseMacroScopes) - return { invariants := state.invariants, witnesses := state.witnesses, vcs := state.vcs } + return { invariants := state.invariants, vcs := state.vcs } where onFail (goal : MGoal) (name : Name) : VCGenM Expr := do -- trace[Elab.Tactic.Do.vcgen] "fail {goal.toExpr}" @@ -356,70 +352,53 @@ where end VCGen -/-- Shared implementation for elaborating goal sections (invariants, witnesses). - `tagPrefix` is `"inv"` or `"witness"`, used to parse labels like `inv1` or `witness2`. - `label` is `"invariant"` or `"witness"`, used in error messages. - When `requireAll` is true, an error is thrown if fewer alts are provided than goals. -/ -private def elabGoalSection (goals : Array MVarId) (alts : Array Syntax) - (tagPrefix : String) (label : String) (requireAll := true) : TacticM Unit := do - let goals ← goals.filterM (not <$> ·.isAssigned) - let mut dotOrCase := LBool.undef -- .true => dot - for h : n in 0...alts.size do - let alt := alts[n] - match alt with - | `(goalDotAlt| · $rhs) => - if dotOrCase matches .false then - logErrorAt alt m!"Alternation between labelled and bulleted {label}s is not supported." - break - dotOrCase := .true - let some mv := goals[n]? | do - logErrorAt alt m!"More {label}s have been defined ({alts.size}) than there were unassigned {label} goals `{tagPrefix}` ({goals.size})." - continue - withRef rhs do - discard <| evalTacticAt (← `(tactic| exact $rhs)) mv - | `(goalCaseAlt| | $tag $args* => $rhs) => - if dotOrCase matches .true then - logErrorAt alt m!"Alternation between labelled and bulleted {label}s is not supported." - break - dotOrCase := .false - let n? : Option Nat := do - let `(binderIdent| $tag:ident) := tag | some n -- fall back to ordinal - let .str .anonymous s := tag.getId | none - s.dropPrefix? tagPrefix >>= String.Slice.toNat? - let some mv := do goals[(← n?) - 1]? | do - logErrorAt alt m!"No {label} with label {tag} {repr tag}." - continue - if ← mv.isAssigned then - logErrorAt alt m!"{label} {n?.get!} is already assigned." - continue - withRef rhs do - discard <| evalTacticAt (← `(tactic| rename_i $args*; exact $rhs)) mv - | _ => logErrorAt alt m!"Expected `goalDotAlt`, got {alt}" - if requireAll && alts.size < goals.size then - let missingTypes ← goals[alts.size:].toArray.mapM (·.getType) - throwError "Lacking definitions for the following {label}s.\n{toMessageList missingTypes}" - -def elabWitnesses (stx : Syntax) (witnesses : Array MVarId) : TacticM Unit := do - let some stx := stx.getOptional? | return () - let stx : TSyntax ``witnessAlts := ⟨stx⟩ - withRef stx do - match stx with - | `(witnessAlts| witnesses $alts*) => - elabGoalSection witnesses alts "witness" "witness" - | _ => logErrorAt stx m!"Expected witnessAlts, got {stx}" - def elabInvariants (stx : Syntax) (invariants : Array MVarId) (suggestInvariant : MVarId → TacticM Term) : TacticM Unit := do let some stx := stx.getOptional? | return () let stx : TSyntax ``invariantAlts := ⟨stx⟩ withRef stx do match stx with | `(invariantAlts| $invariantsKW $alts*) => + let invariants ← invariants.filterM (not <$> ·.isAssigned) + + let mut dotOrCase := LBool.undef -- .true => dot + for h : n in 0...alts.size do + let alt := alts[n] + match alt with + | `(goalDotAlt| · $rhs) => + if dotOrCase matches .false then + logErrorAt alt m!"Alternation between labelled and bulleted invariants is not supported." + break + dotOrCase := .true + let some mv := invariants[n]? | do + logErrorAt alt m!"More invariants have been defined ({alts.size}) than there were unassigned invariants goals `inv` ({invariants.size})." + continue + withRef rhs do + discard <| evalTacticAt (← `(tactic| exact $rhs)) mv + | `(goalCaseAlt| | $tag $args* => $rhs) => + if dotOrCase matches .true then + logErrorAt alt m!"Alternation between labelled and bulleted invariants is not supported." + break + dotOrCase := .false + let n? : Option Nat := do + let `(binderIdent| $tag:ident) := tag | some n -- fall back to ordinal + let .str .anonymous s := tag.getId | none + s.dropPrefix? "inv" >>= String.Slice.toNat? + let some mv := do invariants[(← n?) - 1]? | do + logErrorAt alt m!"No invariant with label {tag} {repr tag}." + continue + if ← mv.isAssigned then + logErrorAt alt m!"Invariant {n?.get!} is already assigned." + continue + withRef rhs do + discard <| evalTacticAt (← `(tactic| rename_i $args*; exact $rhs)) mv + | _ => logErrorAt alt m!"Expected `goalDotAlt`, got {alt}" + if let `(invariantsKW| invariants) := invariantsKW then - elabGoalSection invariants alts "inv" "invariant" + if alts.size < invariants.size then + let missingTypes ← invariants[alts.size:].toArray.mapM (·.getType) + throwErrorAt stx m!"Lacking definitions for the following invariants.\n{toMessageList missingTypes}" else - -- We have `invariants?`. First elaborate any user-provided alts, then suggest the rest. - elabGoalSection invariants alts "inv" "invariant" (requireAll := false) - let invariants ← invariants.filterM (not <$> ·.isAssigned) + -- Otherwise, we have `invariants?`. Suggest missing invariants. let mut suggestions := #[] for i in 0...invariants.size do let mv := invariants[i]! @@ -478,8 +457,8 @@ def elabMVCGen : Tactic := fun stx => withMainContext do | none => .unlimited let goal ← getMainGoal let goal ← if ctx.config.elimLets then elimLets goal else pure goal - let { invariants, witnesses, vcs } ← VCGen.genVCs goal ctx fuel - trace[Elab.Tactic.Do.vcgen] "after genVCs {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}" + let { invariants, vcs } ← VCGen.genVCs goal ctx fuel + trace[Elab.Tactic.Do.vcgen] "after genVCs {← (invariants ++ vcs).mapM fun m => m.getTag}" let runOnVCs (tac : TSyntax `tactic) (extraMsg : MessageData) (vcs : Array MVarId) : TermElabM (Array MVarId) := vcs.flatMapM fun vc => tryCatchRuntimeEx @@ -488,13 +467,13 @@ def elabMVCGen : Tactic := fun stx => withMainContext do (fun ex => throwError "Error while running {tac} on {vc}Message: {indentD ex.toMessageData}\n{extraMsg}") let invariants ← if ctx.config.leave then runOnVCs (← `(tactic| try mleave)) "Try again with -leave." invariants else pure invariants - trace[Elab.Tactic.Do.vcgen] "before elabWitnesses {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}" - elabWitnesses stx[3] witnesses - let witnesses ← witnesses.filterM (not <$> ·.isAssigned) - trace[Elab.Tactic.Do.vcgen] "before elabInvariants {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}" - elabInvariants stx[4] invariants (suggestInvariant vcs) + trace[Elab.Tactic.Do.vcgen] "before elabInvariants {← (invariants ++ vcs).mapM fun m => m.getTag}" + -- TODO: This is a vestige from removing the witnesses section (stx[3]) introduced in #12882. + -- After stage0 update, nargs will be constantly 5 again, as it used to. + let nargs := stx.getNumArgs + elabInvariants stx[nargs-2] invariants (suggestInvariant vcs) let invariants ← invariants.filterM (not <$> ·.isAssigned) - trace[Elab.Tactic.Do.vcgen] "before trying trivial VCs {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}" + trace[Elab.Tactic.Do.vcgen] "before trying trivial VCs {← (invariants ++ vcs).mapM fun m => m.getTag}" let vcs ← do let vcs ← if ctx.config.trivial then runOnVCs (← `(tactic| try mvcgen_trivial)) "Try again with -trivial." vcs else pure vcs let vcs ← if ctx.config.leave then runOnVCs (← `(tactic| try mleave)) "Try again with -leave." vcs else pure vcs @@ -502,10 +481,10 @@ def elabMVCGen : Tactic := fun stx => withMainContext do -- Eliminating lets here causes some metavariables in `mkFreshPair_triple` to become nonassignable -- so we don't do it. Presumably some weird delayed assignment thing is going on. -- let vcs ← if ctx.config.elimLets then liftMetaM <| vcs.mapM elimLets else pure vcs - trace[Elab.Tactic.Do.vcgen] "before elabVCs {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}" - let vcs ← elabVCs stx[5] vcs - trace[Elab.Tactic.Do.vcgen] "before replacing main goal {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}" - replaceMainGoal (invariants ++ witnesses ++ vcs).toList + trace[Elab.Tactic.Do.vcgen] "before elabVCs {← (invariants ++ vcs).mapM fun m => m.getTag}" + let vcs ← elabVCs stx[nargs-1] vcs + trace[Elab.Tactic.Do.vcgen] "before replacing main goal {← (invariants ++ vcs).mapM fun m => m.getTag}" + replaceMainGoal (invariants ++ vcs).toList -- trace[Elab.Tactic.Do.vcgen] "replaced main goal, new: {← getGoals}" @[builtin_tactic Lean.Parser.Tactic.mvcgenHint] diff --git a/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean b/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean index 61e1b17941..3b189f5e98 100644 --- a/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean +++ b/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean @@ -73,10 +73,6 @@ structure State where -/ invariants : Array MVarId := #[] /-- - Holes of witness type that have been generated so far. - -/ - witnesses : Array MVarId := #[] - /-- The verification conditions that have been generated so far. -/ vcs : Array MVarId := #[] @@ -108,11 +104,8 @@ def addSubGoalAsVC (goal : MVarId) : VCGenM PUnit := do -- VC to the user as-is, without abstracting any variables in the local context. -- This only makes sense for synthetic opaque metavariables. goal.setKind .syntheticOpaque - let env ← getEnv - if isMVCGenInvariantType env ty then + if isMVCGenInvariantType (← getEnv) ty then modify fun s => { s with invariants := s.invariants.push goal } - else if isMVCGenWitnessType env ty then - modify fun s => { s with witnesses := s.witnesses.push goal } else modify fun s => { s with vcs := s.vcs.push goal } diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index e444447049..aa2e6fd6e0 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -22,6 +22,7 @@ options get_default_options() { opts = opts.update({"quotPrecheck"}, true); opts = opts.update({"pp", "rawOnError"}, true); + // force stage0 update // Temporary, core-only flags for editing (i.e. must be part of stage0/bin/lean). Must be synced // with `LEAN_EXTRA_MAKE_OPTS` build flags in src/CMakeLists.txt. diff --git a/tests/elab/mvcgenWitnessType.lean b/tests/elab/mvcgenWitnessType.lean deleted file mode 100644 index 323249b390..0000000000 --- a/tests/elab/mvcgenWitnessType.lean +++ /dev/null @@ -1,71 +0,0 @@ -import Std.Tactic.Do -import Std -set_option backward.do.legacy false - -open Std Do - -set_option grind.warning false -set_option mvcgen.warning false - --- Test that `@[mvcgen_witness_type]` works end-to-end. --- --- In zero-knowledge proofs, a witness is a concrete value the prover privately knows --- (e.g. a field element), as opposed to an invariant (a predicate maintained across --- iterations) or a verification condition (a proposition to prove). --- --- We model this by axiomatizing a circuit-like computation that requires a concrete --- witness value. The `mvcgen` tactic classifies the witness goal as `witness1` and --- the constraint as `vc1`. - --- A witness type: a concrete value the prover supplies (not a predicate). -@[mvcgen_witness_type] -structure SquareRootWitness where - root : Nat - --- An axiomatized circuit that verifies a square root claim. -opaque checkSquareRoot (n : Nat) : Id Bool - --- Spec: given a witness w whose root squares to n, the circuit returns true. --- When mvcgen applies this spec, `w` becomes a metavariable of witness type, --- and the precondition `w.root * w.root = n` becomes a verification condition. -@[spec] -axiom checkSquareRoot_spec {n : Nat} (w : SquareRootWitness) : - Triple (checkSquareRoot n) ⌜w.root * w.root = n⌝ (⇓ r => ⌜r = true⌝) - -def verifySquareRoot : Id Bool := do - checkSquareRoot 9 - --- mvcgen produces: --- witness1 : SquareRootWitness (concrete value to provide) --- vc1 : 3 * 3 = 9 (constraint, auto-solved after witness instantiation) --- The prover supplies ⟨3⟩ as the witness; the constraint is then trivially true. -theorem verifySquareRoot_correct : - ⦃⌜True⌝⦄ verifySquareRoot ⦃⇓ r => ⌜r = true⌝⦄ := by - mvcgen [verifySquareRoot] witnesses - · ⟨3⟩ - --- With -leave, the VC remains for manual discharge. -theorem verifySquareRoot_manual : - ⦃⌜True⌝⦄ verifySquareRoot ⦃⇓ r => ⌜r = true⌝⦄ := by - mvcgen -leave [verifySquareRoot] witnesses - · ⟨3⟩ - with omega - --- Demonstrate that witnesses and invariants can coexist, with witnesses first. - --- A program that first checks a witness and then loops over a list. -def witnessAndLoop (xs : List Nat) : Id Nat := do - let mut s := 0 - let _ ← checkSquareRoot 9 - for x in xs do - s := s + x - pure s - --- Both witnesses (before invariants) in the mvcgen syntax. -theorem witnessAndLoop_correct (xs : List Nat) : - ⦃⌜True⌝⦄ witnessAndLoop xs ⦃⇓ _ => ⌜True⌝⦄ := by - mvcgen [witnessAndLoop] witnesses - · ⟨3⟩ - invariants - · ⇓ _ => ⌜True⌝ - with grind