restate-check — does a human review survive a Mathlib bump?

A review is made against one environment. env_digest includes every package revision, so statement_stable is not_applicable across environments by construction — which means a single Mathlib or anchor bump invalidates 100% of human review simultaneously, and recovery costs the entire original review budget, per bump, at roughly two hours an entry.

This is the only thing standing between that and re-reviewing everything.

What it does

For each reviewed entry: take the statement as the human read it (reviewed_statement_pp), parse it, elaborate it in the current environment, and ask whether it is definitionally equal to what that declaration says now. If it is, the review survives the bump.

Three outcomes, and the third is not the second

• restated — elaborates and is defeq. The review survives.
• changed — elaborates, is not defeq. The statement moved; the review is invalidated and must be redone.
• not_checkable — could not be parsed or elaborated at all.

not_checkable must never be collapsed into changed. They differ in what a human must do: changed means re-review this statement, not_checkable means nobody knows whether it changed, and reporting the second as the first would send a reviewer to re-read a statement that may be perfectly fine while hiding that the tool failed.

reviewed_statement_pp is NOT type_pp

Reusing the emission's type_pp here is the trap this file exists to avoid. The emitter pins pp.explicit := false; under those options 5 of 76 declarations fail to elaborate with unresolved metavariables, and with implicits printed, 0. A check built on type_pp would report not_checkable on statements that are perfectly fine.

The message log is load-bearing

elabTerm logs errors rather than throwing them. A try/catch alone therefore returns success on a failed elaboration and leaks the error into the enclosing build's output. Observed directly while writing the spike.

So each attempt snapshots Core.State.messages, treats hasErrors as failure, and restores the log afterwards. Without this the check is both wrong and noisy.

Transparency is deliberately not touched

withTransparency .all rescues exactly zero cases — 339 both ways in the spike. Reaching for it would widen what counts as "the same statement" for no measured gain, and every widening here is a way for a review to survive a change it should not have survived.

inductive MathFormalContract.RestateOutcome : Type

What one reviewed statement did against the current environment.

• restated : RestateOutcome

  Elaborated, and definitionally equal to the declaration's current type.

• changed : RestateOutcome

  Elaborated, and NOT defeq. The statement moved.

• notCheckable : RestateOutcome

  Could not be parsed or elaborated. Nobody knows whether it changed.

@[implicit_reducible]

instance MathFormalContract.instInhabitedRestateOutcome : Inhabited RestateOutcome

Equations

• MathFormalContract.instInhabitedRestateOutcome = { default := MathFormalContract.instInhabitedRestateOutcome.default }

@[implicit_reducible]

instance MathFormalContract.instDecidableEqRestateOutcome : DecidableEq RestateOutcome

Equations

• MathFormalContract.instDecidableEqRestateOutcome x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def MathFormalContract.RestateOutcome.toString : RestateOutcome → String

Equations

• MathFormalContract.RestateOutcome.restated.toString = "restated"
• MathFormalContract.RestateOutcome.changed.toString = "changed"
• MathFormalContract.RestateOutcome.notCheckable.toString = "not_checkable"

structure MathFormalContract.RestateResult : Type

One entry's verdict, with the reason a not_checkable was not checkable.

The reason is not decoration: "parse failed" and "elaboration logged an error" send a reviewer to different places, and an outcome with no reason is one nobody can act on.

• key : String
• decl : Lean.Name
• outcome : RestateOutcome
• reason : String

@[implicit_reducible]

instance MathFormalContract.instInhabitedRestateResult : Inhabited RestateResult

Equations

• MathFormalContract.instInhabitedRestateResult = { default := MathFormalContract.instInhabitedRestateResult.default }

def MathFormalContract.elabStatement? (s : String) : Lean.Elab.TermElabM (Except String Lean.Expr)

Elaborate s as a term in the current environment, with the message log sandboxed.

Returns none when the statement could not be parsed or elaborated, together with why. The snapshot/restore around the attempt is what stops a logged elaboration error from both being mistaken for success AND appearing in the enclosing build's output.

Equations

• One or more equations did not get rendered due to their size.

def MathFormalContract.restateOne (key : String) (decl : Lean.Name) (statementPp : String) : Lean.Elab.TermElabM RestateResult

Check one reviewed statement against the declaration's current type.

Equations

• One or more equations did not get rendered due to their size.

def MathFormalContract.restateJson (results : Array RestateResult) (checkedAt : String) : Lean.Json

The restate/1.0 document.

Equations

• One or more equations did not get rendered due to their size.

The producer

restateOne is the check. This is what runs it over a work-list and writes the restate/1.0 artifact — the piece that was missing, and without which the check was reachable only from this package's own tests.

The work-list arrives as JSON, and that is not an accident

The reviews live in attest/review.yaml. Lean cannot read YAML, and it is not going to learn: this package's zero-dependency property is the argued exception that lets it into a topic repo's environment at all, and spending it on a YAML parser would end the argument.

So mfc restate-plan reads the reviews and writes [{key, decl, statement_pp}]. That is the same split the contract makes everywhere else — elaboration is Lean's, reading the verdict is mfc's — and it keeps this file free of a format it has no business parsing.

A missing statement is not_checkable, never a missing row

An entry whose statement_pp is null still appears in the results, as not_checkable with a reason. Dropping it would be T-01's hole exactly: a run that silently omits an entry looks identical to one where that entry was fine, and the omission is invisible in the counts because the counts are computed from the rows that are there.

maxHeartbeats is finite on purpose

An explicit rendering of a real statement runs to several kilobytes, so the default budget is raised. It is not set to 0: an unbounded elaboration that hangs stops CI with no artifact and no diagnosis, while an exhausted budget surfaces through elabStatement? as not_checkable with the reason attached — which is a worse verdict and a far better failure.

@[implicit_reducible]

instance MathFormalContract.instInhabitedPlanEntry : Inhabited MathFormalContract.PlanEntry✝

Equations

• MathFormalContract.instInhabitedPlanEntry = { default := MathFormalContract.instInhabitedPlanEntry.default }

@[implemented_by _private.MathFormalContract.RestateCheck.0.MathFormalContract.restateToFileImpl]

opaque MathFormalContract.restateToFile (rootLib : Lean.Name) (additionalRoots : List Lean.Name) (planPath outPath : System.FilePath) : IO UInt32

Import, check every reviewed statement, write restate/1.0.

opaque over an unsafe implementation for the same reason emitToFileForRoots is: importModules is unsafe, and unsafe def main would push that into the handful of lines a topic repo generates.

Capturing the statement a reviewer records

reviewed_statement_pp is the string a review's survival depends on, and every way of getting it wrong is SILENT: the field looks captured, mfc validate passes, and the failure surfaces at the next dependency bump as not_checkable, which reads like a broken tool rather than a bad capture.

Capturing the first one by hand took three attempts, with the schema, this file, and the emitter all open:

• Elision. pp.explicit alone left a ⋯ inside a proof argument. Unparseable. pp.proofs, pp.deepTerms and a raised pp.maxSteps close it — which is why this builds on Emit.ppOpts rather than its own list.
• Invented universe names. Rendering via #check @Decl instantiates the constant with FRESH universe metavariables and prints them u_1, u_2, u_3. The declaration's levelParams were [w, u, u'], so restateOne reported unknown universe level u_2. ci.type carries the declaration's own names; the term does not.
• A verification easier than the real check. Both bad renderings were checked with a universe u_1 u_2 u_3 command above an example, which supplies by hand the level context restateOne does not have.

So the capture proves itself

captureStatement renders, then puts the result through restateOne — the same parse, the same elabTerm, the same isDefEq, the same withLevelNames — and returns the string ONLY on restated. All three failures above produce a rendering that fails that check, so none of them can reach review.yaml through this path.

A capture that cannot pass the check it exists to feed is not a capture.

def MathFormalContract.capturePpOpts : Lean.Options

Emit.ppOpts with pp.explicit := true.

The one deliberate difference. The emitter renders at pp.explicit := false because type_pp is for reading; a reviewer's statement is for RE-ELABORATING, and implicit arguments that a human infers an elaborator must be told.

Equations

• MathFormalContract.capturePpOpts = MathFormalContract.ppOpts.setBool `pp.explicit true

def MathFormalContract.captureStatement (decl : Lean.Name) : Lean.Elab.TermElabM (Except String String)

Render decl's type as a reviewer would record it, and verify it.

Equations

• One or more equations did not get rendered due to their size.

@[implemented_by _private.MathFormalContract.RestateCheck.0.MathFormalContract.captureToFileImpl]

opaque MathFormalContract.captureToFile (rootLib : Lean.Name) (additionalRoots : List Lean.Name) (decl : Lean.Name) (outPath : Option System.FilePath) : IO UInt32

def MathFormalContract.restateMainForRoots (rootLib : Lean.Name) (additionalRoots : List Lean.Name) (args : List String) : IO UInt32

The entry point a topic repo calls. Mirrors emitMainForRoots.

Equations

• One or more equations did not get rendered due to their size.

def MathFormalContract.restateMain (rootLib : Lean.Name) (args : List String) : IO UInt32

Single-root topic repos.

Equations

• MathFormalContract.restateMain rootLib args = MathFormalContract.restateMainForRoots rootLib [] args