Module accept 

Accept predicate for replayed proof attempts.

A passing lake lean exit code alone is gameable: an attempt can weaken the statement it claims to prove, smuggle in sorry, or pin an extra axiom, and still exit zero. This module turns “the file compiled” into “the file compiled and the thing it proved is the thing we asked for” through a small set of guards, each of which returns a typed rejection carrying its own trace. It is not a proof of soundness: it raises the bar against the known bypass classes below. See “Known limitations”.

Live guards (run on every passing compile):

1. STATEMENT-UNCHANGED. The declaration signature (everything up to the := that opens the proof body) must be byte-identical before and after the edit. This guards against silent statement-weakening.
2. AXIOM-WHITELIST. #print axioms <decl> must report a subset of {propext, Classical.choice, Quot.sound}. A sorry warning on the compile, or any axiom outside the set, is a rejection. The axiom set is read from a probe bracketed by per-run sentinels, so a top-level command in the edited file cannot forge the result, and an anonymous declaration (example) is aliased to a named probe rather than skipped. This guards against sorry/admit and extra-axiom passes.
3. REVERSE-DEP. lake build of the edited module (and its direct importers when they are cheap to find) must succeed, so a weakened shared lemma cannot stay green on a stale olean.

Guard 4 (NEGATIVE-CONTROL) is wired but stubbed. See check_negative_control.

Known limitations: these guards catch known bypass classes; they are not a proof that no bypass exists. The axiom probe assumes the edit is a proof body, so a replacement that introduces a top-level command (#eval, #print, import, set_option, macro, elab, open) is refused at patch time (see crate::patch); that restriction is what keeps the probe trustworthy.

Structs

AcceptOutcome

Result of running the accept predicate over one patched, passing compile.

AcceptReport

Per-guard outcomes for one accept evaluation.

AcceptRequest

Everything the accept predicate needs for one attempt.

NegativeControl

Negation manifest for the negative-control guard.

Enums

GuardStatus

Outcome of one guard inside an AcceptReport.

RejectReason

Why the accept predicate refused to certify a passing compile.

Constants

AXIOM_WHITELIST

Axioms a certified proof may depend on without weakening trust.

Functions

check_negative_control

Guard 4. Compile the formal negation of the claim and require it to fail; if both the claim and its negation pass, the claim is vacuous and is rejected.

evaluate

Run the live guards in order and return the first rejection, if any.