From a32be44f909683a2f5dff4bb955dfa986bbc9b1c Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Wed, 11 Mar 2026 19:38:05 +0800 Subject: [PATCH] feat: add `@[mvcgen_witness_type]` attribute for extensible witness classification (#12882) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- src/Init/Tactics.lean | 36 +++++++ src/Lean/Elab/Tactic/Do/Attr.lean | 21 ++++ src/Lean/Elab/Tactic/Do/VCGen.lean | 126 ++++++++++++++--------- src/Lean/Elab/Tactic/Do/VCGen/Basic.lean | 9 +- src/Std/Tactic/Do/Syntax.lean | 29 ++++-- tests/elab/mvcgenWitnessType.lean | 71 +++++++++++++ 6 files changed, 233 insertions(+), 59 deletions(-) create mode 100644 tests/elab/mvcgenWitnessType.lean diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 6d64e968cc..abfdebfa7f 100644 --- 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`). +* 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 2d0040d874..d3e994622d 100644 --- 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 diff --git a/src/Lean/Elab/Tactic/Do/VCGen.lean b/src/Lean/Elab/Tactic/Do/VCGen.lean index c8011c2d8d..96af434f41 100644 --- 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}` ({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` ({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' diff --git a/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean b/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean index 3b189f5e98..61e1b17941 100644 --- 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 } diff --git a/src/Std/Tactic/Do/Syntax.lean b/src/Std/Tactic/Do/Syntax.lean index 35b7bcc843..b4229d1931 100644 --- 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 a b c => term`, one per invariant goal. +A goal section alternative of the form `| label 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?`. diff --git a/tests/elab/mvcgenWitnessType.lean b/tests/elab/mvcgenWitnessType.lean new file mode 100644 index 0000000000..323249b390 --- /dev/null +++ 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