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)

@[implicit_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

@[implicit_reducible]

instance CatCrypt.Tactic.ProofTermAudit.instBEqTag : BEq Tag

Equations

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

def CatCrypt.Tactic.ProofTermAudit.instInhabitedTag.default : Tag

Equations

• CatCrypt.Tactic.ProofTermAudit.instInhabitedTag.default = CatCrypt.Tactic.ProofTermAudit.Tag.vacuousBody

@[implicit_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).

Equations

• CatCrypt.Tactic.ProofTermAudit.Tag.vacuousBody.toString = "vacuous_body"
• CatCrypt.Tactic.ProofTermAudit.Tag.returnsAssumption.toString = "returns_assumption"
• CatCrypt.Tactic.ProofTermAudit.Tag.trivialConstructor.toString = "trivial_constructor"
• CatCrypt.Tactic.ProofTermAudit.Tag.fieldProjectionBody.toString = "field_projection_body"
• CatCrypt.Tactic.ProofTermAudit.Tag.proofBySubsingleton.toString = "proof_by_subsingleton"
• CatCrypt.Tactic.ProofTermAudit.Tag.proofByExfalso.toString = "proof_by_exfalso"
• (CatCrypt.Tactic.ProofTermAudit.Tag.ignoresParams a a_1).toString = toString "ignores_params(" ++ toString a ++ toString "/" ++ toString a_1 ++ toString ")"
• CatCrypt.Tactic.ProofTermAudit.Tag.customHypothesisInType.toString = "custom_hypothesis_in_type"

@[implicit_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.

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.