feat: add @[mvcgen_witness_type] attribute for extensible witness classification (#12882)

This PR adds an `@[mvcgen_witness_type]` tag attribute, analogous to `@[mvcgen_invariant_type]`, that allows users to mark types as witness types. Goals whose type is an application of a tagged type are classified as witnesses rather than verification conditions, and appear in a new `witnesses` section in the `mvcgen` tactic syntax (before `invariants`). Witnesses are concrete values the prover supplies (inspired by zero-knowledge proofs), as opposed to invariants (predicates maintained across iterations) or verification conditions (propositions to prove). The test uses a ZK-inspired example where a `SquareRootWitness` value must be provided by the prover, with the resulting constraint auto-discharged. Changes: - `src/Lean/Elab/Tactic/Do/Attr.lean`: register `@[mvcgen_witness_type]` tag attribute and `isMVCGenWitnessType` helper - `src/Lean/Elab/Tactic/Do/VCGen/Basic.lean`: add `witnesses` field to `State`, three-way classification in `addSubGoalAsVC` - `src/Std/Tactic/Do/Syntax.lean`: add `witnesses` section syntax (before `invariants`), extract shared `goalDotAlt`/`goalCaseAlt` syntax kinds - `src/Lean/Elab/Tactic/Do/VCGen.lean`: extract shared `elabGoalSection`, add `elabWitnesses`, wire up witness labeling and elaboration - `tests/elab/mvcgenWitnessType.lean`: end-to-end tests for witness-only, witness with `-leave`, and combined witness+invariant scenarios 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
2026-03-17 10:24:07 +00:00 · 2026-03-11 19:38:05 +08:00
parent e43b526363
commit a32be44f90
6 changed files with 233 additions and 59 deletions
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -2262,6 +2262,42 @@ 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<n>`).
+* A goal whose type is an application of a type tagged with `@[mvcgen_witness_type]` is classified
+  as a witness (`witness<n>`).
+* All other goals are classified as verification conditions (`vc<n>`).
+
 ### Invariant suggestions

 `mvcgen` will suggest invariants for you if you use the `invariants?` keyword.
--- a/src/Lean/Elab/Tactic/Do/Attr.lean
+++ b/src/Lean/Elab/Tactic/Do/Attr.lean
@@ -268,3 +268,24 @@ 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
--- a/src/Lean/Elab/Tactic/Do/VCGen.lean
+++ b/src/Lean/Elab/Tactic/Do/VCGen.lean
@@ -35,6 +35,7 @@ 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
@@ -45,10 +46,13 @@ 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, vcs := state.vcs }
+    return { invariants := state.invariants, witnesses := state.witnesses, vcs := state.vcs }
 where
  onFail (goal : MGoal) (name : Name) : VCGenM Expr := do
    -- trace[Elab.Tactic.Do.vcgen] "fail {goal.toExpr}"
@@ -351,60 +355,77 @@ 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}<n>` ({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
-      | `(invariantDotAlt| · $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<n>` ({invariants.size})."
-          continue
-        withRef rhs do
-        discard <| evalTacticAt (← `(tactic| exact $rhs)) mv
-      | `(invariantCaseAlt| | $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 `invariantDotAlt`, got {alt}"
-
    if let `(invariantsKW| invariants) := invariantsKW then
-      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}"
+      elabGoalSection invariants alts "inv" "invariant"
    else
-      -- Otherwise, we have `invariants?`. Suggest missing invariants.
+      -- 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)
      let mut suggestions := #[]
      for i in 0...invariants.size do
        let mv := invariants[i]!
        if ← mv.isAssigned then
          continue
        let invariant ← suggestInvariant mv
-        suggestions := suggestions.push (← `(invariantDotAlt| · $invariant))
+        suggestions := suggestions.push (← `(goalDotAlt| · $invariant))
      let alts' := alts ++ suggestions
      let stx' ← `(invariantAlts|invariants $alts'*)
      if suggestions.size > 0 then
@@ -456,8 +477,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, vcs } ← VCGen.genVCs goal ctx fuel
-  trace[Elab.Tactic.Do.vcgen] "after genVCs {← (invariants ++ vcs).mapM fun m => m.getTag}"
+  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 runOnVCs (tac : TSyntax `tactic) (extraMsg : MessageData) (vcs : Array MVarId) : TermElabM (Array MVarId) :=
    vcs.flatMapM fun vc =>
      tryCatchRuntimeEx
@@ -466,10 +487,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 elabInvariants {← (invariants ++ vcs).mapM fun m => m.getTag}"
-  elabInvariants stx[3] invariants (suggestInvariant vcs)
+  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)
  let invariants ← invariants.filterM (not <$> ·.isAssigned)
-  trace[Elab.Tactic.Do.vcgen] "before trying trivial VCs {← (invariants ++ vcs).mapM fun m => m.getTag}"
+  trace[Elab.Tactic.Do.vcgen] "before trying trivial VCs {← (invariants ++ witnesses ++ 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
@@ -477,17 +501,17 @@ 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 ++ vcs).mapM fun m => m.getTag}"
-  let vcs ← elabVCs stx[4] 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] "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] "replaced main goal, new: {← getGoals}"

@[builtin_tactic Lean.Parser.Tactic.mvcgenHint]
 def elabMVCGenHint : Tactic := fun stx => withMainContext do
  let stx' : TSyntax ``mvcgen := TSyntax.mk <| stx
    |>.setKind ``Lean.Parser.Tactic.mvcgen
-    |>.modifyArgs (·.set! 0 (mkAtom "mvcgen") |>.push (mkNullNode #[← `(invariantAlts| invariants?)]) |>.push mkNullNode)
+    |>.modifyArgs (·.set! 0 (mkAtom "mvcgen") |>.push mkNullNode |>.push (mkNullNode #[← `(invariantAlts| invariants?)]) |>.push mkNullNode)
  -- logInfo m!"{stx}\n{toString stx}\n{repr stx}"
  -- logInfo m!"{stx'}\n{toString stx'}\n{repr stx'}"
  Lean.Meta.Tactic.TryThis.addSuggestion stx stx'
--- a/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean
+++ b/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean
@@ -73,6 +73,10 @@ 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 := #[]
@@ -104,8 +108,11 @@ 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
-  if isMVCGenInvariantType (← getEnv) ty then
+  let env ← getEnv
+  if isMVCGenInvariantType env 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 }

--- a/src/Std/Tactic/Do/Syntax.lean
+++ b/src/Std/Tactic/Do/Syntax.lean
@@ -364,14 +364,29 @@ macro "mvcgen_trivial" : tactic =>
  )

 /--
-An invariant alternative of the form `· term`, one per invariant goal.
+A goal section alternative of the form `· term`, one per goal.
+Used by both `invariants` and `witnesses` sections.
 -/
-syntax invariantDotAlt := ppDedent(ppLine) cdotTk (colGe term)
+syntax goalDotAlt := ppDedent(ppLine) cdotTk (colGe term)

 /--
-An invariant alternative of the form `| inv<n> a b c => term`, one per invariant goal.
+A goal section alternative of the form `| label<n> a b c => term`, one per goal.
+Used by both `invariants` and `witnesses` sections.
 -/
-syntax invariantCaseAlt := ppDedent(ppLine) "| " caseArg " => " (colGe term)
+syntax goalCaseAlt := ppDedent(ppLine) "| " caseArg " => " (colGe term)
+
+/--
+The contextual keyword ` witnesses `.
+-/
+syntax witnessesKW := &"witnesses "
+
+/--
+After `mvcgen [...]`, there can be an optional `witnesses` followed by either
+* a bulleted list of witnesses `· term; · term`.
+* a labelled list of witnesses `| witness1 => term; witness2 a b c => term`, which is useful for
+  naming inaccessibles.
+-/
+syntax witnessAlts := witnessesKW withPosition((colGe (goalDotAlt <|> goalCaseAlt))*)

 /--
 Either the contextual keyword ` invariants ` or its tracing form ` invariants? ` which suggests
@@ -380,14 +395,14 @@ skeletons for missing invariants as a hint.
 syntax invariantsKW := &"invariants " <|> &"invariants? "

 /--
-After `mvcgen [...]`, there can be an optional `invariants` followed by either
+After `mvcgen [...] witnesses ...`, there can be an optional `invariants` followed by either
 * a bulleted list of invariants `· term; · term`.
 * a labelled list of invariants `| inv1 => term; inv2 a b c => term`, which is useful for naming
  inaccessibles.
 The tracing variant ` invariants? ` will suggest a skeleton for missing invariants; see the
 docstring for `mvcgen`.
 -/
-syntax invariantAlts := invariantsKW withPosition((colGe (invariantDotAlt <|> invariantCaseAlt))*)
+syntax invariantAlts := invariantsKW withPosition((colGe (goalDotAlt <|> goalCaseAlt))*)

 /--
 In induction alternative, which can have 1 or more cases on the left
@@ -404,7 +419,7 @@ syntax vcAlts := "with " (ppSpace colGt tactic)? withPosition((colGe vcAlt)*)
@[tactic_alt Lean.Parser.Tactic.mvcgenMacro]
 syntax (name := mvcgen) "mvcgen" optConfig
  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "] ")?
-  (invariantAlts)? (vcAlts)? : tactic
+  (witnessAlts)? (invariantAlts)? (vcAlts)? : tactic

 /--
 A hint tactic that expands to `mvcgen invariants?`.
--- a/tests/elab/mvcgenWitnessType.lean
+++ b/tests/elab/mvcgenWitnessType.lean
@@ -0,0 +1,71 @@
+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