This PR reverts #12882 which added the `@[mvcgen_witness_type]` tag attribute and `witnesses` section to `mvcgen`. Théophile Wallez confirmed he doesn't need this feature and can get by with `invariants`, so there is no use in having it. The actual `mvcgen` syntax needs to be adjusted after a stage0 update in order for `elabMVCGen` to cope with both old and new syntax. Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
Sebastian Graf
GitHub
parent
4227765e2b
commit
40cdec76c5
6 changed files with 54 additions and 209 deletions
|
|
@ -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<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.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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}<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
|
||||
| `(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<n>` ({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]
|
||||
|
|
|
|||
|
|
@ -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 }
|
||||
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
Loading…
Add table
Reference in a new issue