ProofTermAudit — machine-checked shell / vacuity detection over proof terms

This module ports the deterministic (zero-LLM-token) core of facebookresearch/autoform-bot's autoform/eval/ subsystem to CatCrypt. autoform-bot grades autoformalizations by introspecting the compiled proof term rather than the surface syntax; we reuse the same idea to machine-check the project's shell-vs-genuine-reduction distinction.

CatCrypt's existing audit (scripts/audit_security.lean) detects "shell" theorems via a docstring-tag convention ((composition plumbing), (concurrent UC via ITreeN), …) and via text scanning of theorem signatures. Those are convention-dependent: a theorem mislabelled in its docstring, or whose body silently became trivial, slips through. This module inspects the elaborated Expr of a declaration's proof term and reports structural tags that no comment can fake.

Tags

Each tag is computed purely from the proof term e := value? of a declaration, after stripping leading fun-binders (stripLambdas). Let nl be the number of stripped binders (the declaration's parameters and hypotheses) and body the head-beta-reduced lambda body.

Tag	Detection (implemented)
vacuous_body	body's head constant is True.intro / trivial / And.intro of True.intros, or body is a rfl-proof (Eq.refl / rfl) at a propositionally trivial head — i.e. the proof carries no hypothesis-dependent content.
returns_assumption	body is exactly a bvar referring to one of the nl binders — the proof fun … hᵢ … => hᵢ directly returns a hypothesis.
trivial_constructor	body's head is a structure/inductive constructor (ConstructorVal) and the constructor has no explicit (non-instance, non-Prop-erased) data arguments derived from the binders — a content-free constructor application (e.g. ⟨⟩ : True, PUnit.unit, Unit.unit).
field_projection_body	body is a .proj, or its head is a projection function (Environment.getProjectionFnInfo?) — the proof is "read a field", not a derivation.
proof_by_subsingleton	body's head constant is Subsingleton.elim / Subsingleton.allEq / proof_irrel.
proof_by_exfalso	body's head constant is False.elim / absurd / False.rec / Empty.elim — goal derived from a contradiction on an assumption.
ignores_params	At least one of the nl stripped binders does not occur in body. (Reported with the used/total count.) This is the structural analogue of autoform-bot's "the proof does not use its premises" check. Note: a binder may legitimately appear only in the type of a later binder; this tag is advisory, surfaced together with the stronger returns_assumption / vacuous_body signals rather than failing on its own.

Stubbed / partial

Tag

Status

custom_hypothesis_in_type

Partial. Full autoform-bot semantics ("the statement carries a suspicious custom hypothesis that trivializes the goal") requires modelling which hypotheses are load-bearing for the conclusion — undecidable in general. We implement a conservative proxy: flag declarations whose type contains a hypothesis of the form (h : P) → P (an identity implication a returns_assumption body would discharge), or whose conclusion is defeq to True. Anything subtler is deferred.

Shell classification

shellTags is the subset that indicates a content-free proof: vacuous_body, returns_assumption, trivial_constructor. The audit driver treats a declaration as a potential undocumented shell when it carries a shell tag but its docstring lacks an honest (composition plumbing) / sdist_self marker, and as a docstring/body mismatch when the docstring claims a genuine result yet the body is vacuous_body / returns_assumption.

A genuine reduction (e.g. one that applys a composition lemma and then discharges its premise from the hypotheses, like UCEmulates_of_sdist followed by exact hkdf_sdist …) elaborates to a term whose head is the composition lemma applied to the binders, so it is not tagged — exactly the discrimination the feedback_no_genuine_reduction memory and the UC docstring convention are guarding.

Usage

• Interactive: #proof_term_tags <decl-name> logs the tags for one decl.
• Programmatic: ProofTermAudit.tagsFor (n : Name) : MetaM (Array Tag).
• Batch driver: see CatCrypt/Tactic/ProofTermAuditDriver.lean (the lake exe proofaudit executable), which scans every UCEmulates / *_uc_secure / reduction theorem in the environment and prints a report consumed by scripts/audit_security.lean.

Future work (NOT implemented this increment)

• Increment 2 — dependency-graph cone alerts. Walk the transitive getUsedConstants cone of each security theorem and alert when a "genuine"-tagged theorem's cone bottoms out in an axiom or sorryAx that is not on the sanctioned list. (autoform-bot's reachability check.)
• Increment 3 — LLM faithfulness jury. Grade whether the Lean statement faithfully renders the informal/RFC claim. This is the LLM-token path and is explicitly out of scope here.

inductive CatCrypt.Tactic.ProofTermAudit.Tag : Type

A structural tag computed from a declaration's proof term.

• vacuousBody : Tag
• returnsAssumption : Tag
• trivialConstructor : Tag
• fieldProjectionBody : Tag
• proofBySubsingleton : Tag
• proofByExfalso : Tag
• ignoresParams (used total : Nat) : Tag

  carries (used, total) binder counts

• customHypothesisInType : Tag

  partial detector (see module doc)

@[instance_reducible]

instance CatCrypt.Tactic.ProofTermAudit.instReprTag : Repr Tag

Equations

• CatCrypt.Tactic.ProofTermAudit.instReprTag = { reprPrec := CatCrypt.Tactic.ProofTermAudit.instReprTag.repr }

def CatCrypt.Tactic.ProofTermAudit.instReprTag.repr : Tag → Nat → Std.Format

Equations

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

def CatCrypt.Tactic.ProofTermAudit.instBEqTag.beq : Tag → Tag → Bool

Equations

• CatCrypt.Tactic.ProofTermAudit.instBEqTag.beq CatCrypt.Tactic.ProofTermAudit.Tag.vacuousBody CatCrypt.Tactic.ProofTermAudit.Tag.vacuousBody = true
• CatCrypt.Tactic.ProofTermAudit.instBEqTag.beq CatCrypt.Tactic.ProofTermAudit.Tag.returnsAssumption CatCrypt.Tactic.ProofTermAudit.Tag.returnsAssumption = true
• CatCrypt.Tactic.ProofTermAudit.instBEqTag.beq CatCrypt.Tactic.ProofTermAudit.Tag.trivialConstructor CatCrypt.Tactic.ProofTermAudit.Tag.trivialConstructor = true
• CatCrypt.Tactic.ProofTermAudit.instBEqTag.beq CatCrypt.Tactic.ProofTermAudit.Tag.fieldProjectionBody CatCrypt.Tactic.ProofTermAudit.Tag.fieldProjectionBody = true
• CatCrypt.Tactic.ProofTermAudit.instBEqTag.beq CatCrypt.Tactic.ProofTermAudit.Tag.proofBySubsingleton CatCrypt.Tactic.ProofTermAudit.Tag.proofBySubsingleton = true
• CatCrypt.Tactic.ProofTermAudit.instBEqTag.beq CatCrypt.Tactic.ProofTermAudit.Tag.proofByExfalso CatCrypt.Tactic.ProofTermAudit.Tag.proofByExfalso = true
• CatCrypt.Tactic.ProofTermAudit.instBEqTag.beq (CatCrypt.Tactic.ProofTermAudit.Tag.ignoresParams a a_1) (CatCrypt.Tactic.ProofTermAudit.Tag.ignoresParams b b_1) = (a == b && a_1 == b_1)
• CatCrypt.Tactic.ProofTermAudit.instBEqTag.beq CatCrypt.Tactic.ProofTermAudit.Tag.customHypothesisInType CatCrypt.Tactic.ProofTermAudit.Tag.customHypothesisInType = true
• CatCrypt.Tactic.ProofTermAudit.instBEqTag.beq x✝¹ x✝ = false

@[instance_reducible]

instance CatCrypt.Tactic.ProofTermAudit.instBEqTag : BEq Tag

Equations

• CatCrypt.Tactic.ProofTermAudit.instBEqTag = { beq := CatCrypt.Tactic.ProofTermAudit.instBEqTag.beq }

@[instance_reducible]

instance CatCrypt.Tactic.ProofTermAudit.instInhabitedTag : Inhabited Tag

Equations

• CatCrypt.Tactic.ProofTermAudit.instInhabitedTag = { default := CatCrypt.Tactic.ProofTermAudit.instInhabitedTag.default }

def CatCrypt.Tactic.ProofTermAudit.Tag.toString : Tag → String

Human-readable, stable string form (matches the module-doc table).

@[instance_reducible]

instance CatCrypt.Tactic.ProofTermAudit.Tag.instToString : ToString Tag

Equations

• CatCrypt.Tactic.ProofTermAudit.Tag.instToString = { toString := CatCrypt.Tactic.ProofTermAudit.Tag.toString }

def CatCrypt.Tactic.ProofTermAudit.Tag.isShell : Tag → Bool

Tags indicating a content-free proof body (the "shell" set).

Equations

• CatCrypt.Tactic.ProofTermAudit.Tag.vacuousBody.isShell = true
• CatCrypt.Tactic.ProofTermAudit.Tag.returnsAssumption.isShell = true
• CatCrypt.Tactic.ProofTermAudit.Tag.trivialConstructor.isShell = true
• x✝.isShell = false

def CatCrypt.Tactic.ProofTermAudit.Tag.shellTags (ts : Array Tag) : Array Tag

Tags that mark the proof body as content-free.

Equations

• CatCrypt.Tactic.ProofTermAudit.Tag.shellTags ts = Array.filter CatCrypt.Tactic.ProofTermAudit.Tag.isShell ts

Term-inspection helpers

partial def CatCrypt.Tactic.ProofTermAudit.stripLambdas : Lean.Expr → Nat × Lean.Expr

Strip leading fun-binders, returning their count and the body.

partial def CatCrypt.Tactic.ProofTermAudit.usedBinders (e : Lean.Expr) (extra : Nat) (acc : Std.HashSet Nat) : Std.HashSet Nat

Collect the de-Bruijn indices (relative to the body, i.e. counting the stripped lambdas as the outermost binders) of every free bvar occurrence. extra tracks binders introduced inside body.

def CatCrypt.Tactic.ProofTermAudit.countUsedBinders (nl : Nat) (body : Lean.Expr) : Nat

Count how many of the nl outermost binders occur in body.

Equations

• CatCrypt.Tactic.ProofTermAudit.countUsedBinders nl body = (List.filter (fun (k : Nat) => (CatCrypt.Tactic.ProofTermAudit.usedBinders body 0 ∅).contains k) (List.range nl)).length

def CatCrypt.Tactic.ProofTermAudit.isVacuousHead (n : Lean.Name) : Bool

Is n one of the recognised "vacuous proof" head constants?

Equations

• CatCrypt.Tactic.ProofTermAudit.isVacuousHead n = (n == `True.intro || n == `trivial || n == `id)

def CatCrypt.Tactic.ProofTermAudit.isSubsingletonHead (n : Lean.Name) : Bool

Is n a subsingleton-elimination head?

Equations

• CatCrypt.Tactic.ProofTermAudit.isSubsingletonHead n = (n == `Subsingleton.elim || n == `Subsingleton.allEq || n == `proof_irrel)

def CatCrypt.Tactic.ProofTermAudit.isExfalsoHead (n : Lean.Name) : Bool

Is n an ex-falso head?

Equations

• CatCrypt.Tactic.ProofTermAudit.isExfalsoHead n = (n == `False.elim || n == `absurd || n == `False.rec || n == `Empty.elim || n == `False.casesOn || n == `Empty.casesOn)

def CatCrypt.Tactic.ProofTermAudit.isReflHead (n : Lean.Name) : Bool

Is n a recognised content-free rfl-proof head? Eq.refl / rfl / HEq.refl / Iff.rfl — these carry no hypothesis-dependent content.

Equations

• CatCrypt.Tactic.ProofTermAudit.isReflHead n = (n == `Eq.refl || n == `rfl || n == `HEq.refl || n == `Iff.refl || n == `Iff.rfl)

def CatCrypt.Tactic.ProofTermAudit.isTrivialConstructorApp (env : Lean.Environment) (nl : Nat) (body : Lean.Expr) : Bool

Does body's head resolve to a structure/inductive constructor with no explicit data argument that comes from a binder? Such an application (e.g. PUnit.unit, ⟨⟩ : True) is a trivial constructor.

Equations

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

def CatCrypt.Tactic.ProofTermAudit.isFieldProjection (env : Lean.Environment) (body : Lean.Expr) : Bool

Is body (or its head) a structure-field projection?

Equations

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

Type-side (partial) detector

partial def CatCrypt.Tactic.ProofTermAudit.piTelescopeSyntactic : Lean.Expr → List Lean.Expr × Lean.Expr

Walk a forall-telescope syntactically (no whnf/isDefEq), returning the list of binder domains and the final conclusion. Cheap and total — deliberately avoids the reduction cost that makes a MetaM telescope blow heartbeats on heavy crypto types.

def CatCrypt.Tactic.ProofTermAudit.typeHasCustomTrivialiser (type : Lean.Expr) : Bool

Conservative, syntactic custom_hypothesis_in_type proxy: scan the type's pi-telescope for a hypothesis binder whose domain is structurally identical to the conclusion (an (h : P) → … → P identity implication a returns_assumption body would discharge), or a conclusion that is the constant True. Purely syntactic so it never reduces (and never blows heartbeats); subtler defeq cases are deferred (see module doc).

Equations

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

The tagger

def CatCrypt.Tactic.ProofTermAudit.tagsFor (n : Lean.Name) : Lean.MetaM (Array Tag)

Compute the structural tags for declaration n. Returns #[] for declarations with no inspectable value (axioms, opaques) — they are not the subject of this audit.

Equations

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

Statement-level detectors

The tags above read a proof term. The three detectors here read a statement, so they apply to axioms (which have no term) and to theorems whatever their proof.

• statementFromBinders — the conclusion is definitionally the type of a hypothesis binder, or of a Prop-valued field of a structure-typed binder. For an axiom this means the axiom is provable (fun P => P.field) and asserts nothing while adding a name to every downstream #print axioms. For a theorem it is the self-hypothesis shape, detected after unfolding, so a hypothesis wrapped in a named Prop (h : Bound P with Bound P := …) is caught as well.
• isNominalStatement — a theorem whose conclusion and at least one hypothesis are propositions about numbers only: every local occurs either with a numeric type or as the argument of a projection with a numeric result type, after unfolding Prop-valued definitions from the CatCrypt namespaces, and an opaque constant of numeric type counts as a number. Such a theorem relates named quantities to named quantities; no game, adversary or scheme constrains it. A statement whose type mentions no CatCrypt constant at all is plain arithmetic and is not reported.

def CatCrypt.Tactic.ProofTermAudit.isNumericTypeName (n : Lean.Name) : Bool

Types whose values the nominal-bound detector treats as numbers.

Equations

• CatCrypt.Tactic.ProofTermAudit.isNumericTypeName n = [`Nat, `Int, `Real, `ENNReal, `NNReal, `Rat].contains n

def CatCrypt.Tactic.ProofTermAudit.isNumericType (t : Lean.Expr) : Lean.MetaM Bool

Is t (up to reducible unfolding) one of the numeric carrier types?

Equations

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

def CatCrypt.Tactic.ProofTermAudit.isCatCryptName (n : Lean.Name) : Bool

Is n in a CatCrypt namespace (dev or core)?

Equations

• CatCrypt.Tactic.ProofTermAudit.isCatCryptName n = (n.getRoot == `CatCrypt || n.getRoot == `CatCryptCore)

def CatCrypt.Tactic.ProofTermAudit.typeMentionsCatCrypt (n : Lean.Name) : Lean.MetaM Bool

Does the type of n mention a constant from a CatCrypt namespace?

Equations

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

def CatCrypt.Tactic.ProofTermAudit.isDefEqCapped (a b : Lean.Expr) : Lean.MetaM Bool

isDefEq under a heartbeat cap, with failures read as false.

Equations

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

def CatCrypt.Tactic.ProofTermAudit.projectionMatchingConcl (x concl : Lean.Expr) : Lean.MetaM (Option Lean.Name)

The Prop-valued fields of the structure-typed local x whose type is definitionally concl; the first such field name.

Equations

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

def CatCrypt.Tactic.ProofTermAudit.statementFromBinders (n : Lean.Name) (reducibleOnly : Bool) : Lean.MetaM (Option String)

For a declaration of type ∀ xs, C with C : Prop: a witness that C is definitionally the type of a hypothesis binder, or of a Prop-valued field of a structure-typed binder. reducibleOnly restricts unfolding to reducible definitions (the syntactic tier); otherwise definitions unfold, which is the tier that sees through a named-Prop wrapper.

Equations

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

partial def CatCrypt.Tactic.ProofTermAudit.unfoldCatCryptProp (e : Lean.Expr) (fuel : Nat) : Lean.MetaM Lean.Expr

Unfold the head of e while it is a definition from a CatCrypt namespace whose value is a proposition, at most fuel times.

partial def CatCrypt.Tactic.ProofTermAudit.nominalExpr (xs : Array Lean.Expr) (e : Lean.Expr) : Lean.MetaM Bool

Is e a proposition about numbers only, relative to the locals xs? Every local occurrence must be numeric-typed or the argument of a projection with a numeric result type; an application of an opaque constant with a numeric result type is a number; binders inside e are not admitted.

def CatCrypt.Tactic.ProofTermAudit.isNominalStatement (n : Lean.Name) : Lean.MetaM Bool

Is theorem n a nominal-bound statement: a Prop-typed declaration whose type mentions a CatCrypt constant, whose conclusion is a proposition about numbers only, and at least one of whose hypothesis binders is too?

Equations

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

def CatCrypt.Tactic.ProofTermAudit.summaryFor (n : Lean.Name) : Lean.MetaM String

Pretty one-line summary of a decl's tags ("" if clean).

Equations

• CatCrypt.Tactic.ProofTermAudit.summaryFor n = do let ts ← CatCrypt.Tactic.ProofTermAudit.tagsFor n pure (", ".intercalate (List.map CatCrypt.Tactic.ProofTermAudit.Tag.toString ts.toList))

Interactive command

def CatCrypt.Tactic.ProofTermAudit.«command#proof_term_tags_» : Lean.ParserDescr

#proof_term_tags foo logs the structural shell/vacuity tags of foo.

Equations

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