Re-check proofs

Every PASS is a Lean 4 file. You can check it with the same toolchain that checked it in the first place, independently of the engine, the Hub and us.

The easy way

theformalera cert verify release.cert.json --require L1 --pubkey release.pub --proofs

With --proofs, cert verify checks every proof file’s digest against the certificate. It then compiles the lemma closure (proofs/lemmas/) from source into a scratch directory, and runs lake env lean on every proof in the locked spec workspace.

By hand, with stock Lean

You need the spec package the certificate pins (predicate.spec_digest), built with lake build, and the release directory (release.cert.json, proofs/, proofs/lemmas/).

recheck.sh

#!/usr/bin/env bash
# Re-check a release's proofs with the standard Lean 4 toolchain only (no theformalera code).
set -euo pipefail
REL=$PWD
SPEC=/path/to/the/locked/spec/package/lean     # its digest is pinned by the certificate
OUT=$(mktemp -d)
cd "$SPEC"

# 1. the lemma dependency closure, compiled from the shipped Lean source
for f in $REL/proofs/lemmas/TFELemmas/*.lean; do
  m=$(basename "$f" .lean)
  mkdir -p $OUT/TFELemmas
  lake env lean --root=$REL/proofs/lemmas "$f" -o $OUT/TFELemmas/$m.olean
done
export LEAN_PATH=$OUT

# 2. every proof, with `#print axioms` of its main theorem appended
for f in $REL/proofs/*.lean; do
  ns=$(grep -m1 '^namespace' "$f" | cut -d' ' -f2)
  { cat "$f"; echo "#print axioms $ns.implements"; } > $OUT/check.lean
  echo "== $(basename "$f")"
  lake env lean $OUT/check.lean | grep -E "error|axioms" || true
done

A real run on a release of the example repository:

$ grep -c sorry proofs/*.lean proofs/lemmas/TFELemmas/*.lean | awk -F: '{s+=$2} END {print NR " files, " s " occurrences of sorry"}'
9 files, 0 occurrences of sorry
$ time ./recheck.sh
lemma closure compiled from source: TFELemmas.Pack_2f5f29ad9072
== rmsnorm_kernel__layers____input_norm__9d6f70d2a5.lean
'TFE.Cert.rmsnorm_kernel_input_norm_4ea45477.implements' depends on axioms: [propext, Classical.choice, Quot.sound]
== silu_mul_tanh_kernel__layers____mlp_act__156cd7f53b.lean
'TFE.Cert.silu_mul_tanh_kernel_mlp_act_f9d7de5b.implements' depends on axioms: [propext, Classical.choice, Quot.sound]

real	0m7.989s

Terminal: recheck.sh compiles the lemma closure and checks two proofs; each depends only on propext, Classical.choice and Quot.sound

What to look for

Lean must accept every file with no errors.
#print axioms of each implements theorem must list only propext, Classical.choice and Quot.sound. Any other axiom (sorryAx, a custom axiom, Lean.ofReduceBool from native_decide) means the proof does not count.
The theorem’s statement is Implements … (spec) for the Op Spec of the node in the certificate. Read the certificate’s header: it names the kernel and the Spec Key.

Reading a proof file

A proof file is self-contained apart from the spec library and the lemma closure. In order, it contains:

Args: the kernel’s global memory per pointer argument, and its scalar arguments;
one definition per Triton IR value, documented with the IR line and source location (norm.py:16);
the binding hypotheses Hyp: the layouts of your tensors, the scalars, and that outputs do not overlap inputs;
the theorem implements, and its proof.

The proof’s value subgoals end in tfe_close or tfe_replay "<tactic script>". When a lemma was hit, its module is imported from the closure.

Get started

Concepts

Guides

Model conformance

Case studies

Help

The easy way

By hand, with stock Lean

What to look for

Reading a proof file

​The easy way

​By hand, with stock Lean

​What to look for

​Reading a proof file

The easy way

By hand, with stock Lean

What to look for

Reading a proof file