2026-07-02 12:17:44 +00:00
#!/usr/bin/env bash
# ─────────────────────────────────────────────────────────────────────────────
# check.sh — THE button. Compiles EVERY shipped .lean file and axiom-audits
# EVERY layer certificate. If a file is in this repo, this script checks it;
# if this script doesn't check it, it must not be in the repo.
#
# Phases:
# 0. resource + source-integrity guards
# 1. stub audit: no `by trivial` specs, no True-target theorems, and — the
# anti-axiom-smuggling gate — ZERO `axiom` declarations under Proofs/
# (external models in gen/ are the only sanctioned axiom site)
# 2. compile gen/ + Proofs/ in dependency order (explicit -o, capped cores,
# per-file timeout). Any "declaration uses 'sorry'" warning is a FAILURE
# (this catches sorry robustly — text greps can't, comments mention it).
verification: kernel-side axiom-declaration gate (Phase 2b) + self-test
Phase 1's anti-smuggling check reads source text. Measured today on Lean
v4.30.0-rc2, four distinct declarations compile cleanly and slip past its
anchored pattern:
` axiom cheat : ...` one leading space
`@[simp] axiom cheat : ...` line starts with the attribute
`unsafe axiom cheat : ...` `unsafe` absent from the modifier list
`axiom` <newline> ` cheat` no space follows the keyword
Any of them yields a repository that proves False while the button prints
ALL GREEN. Only the tab variant is blocked, and by Lean, not by us.
Hardening the pattern would fix the exhibited syntax rather than the class,
which is the mistake this estate has made before. Phase 2b stops parsing text
and asks the kernel instead: it reads every compiled Proofs/*.olean with
readModuleData and rejects any declaration that is an axiom.
Design notes:
- reads compiled artifacts rather than importing the modules, because
Proofs.Basic and Proofs.ConstSpecs deliberately reuse `zero_spec` and a
whole-corpus import is impossible by construction;
- membership is self-deriving from the filesystem, so Scalar* and
AxiomCheck are covered too — both are skipped by the CERTS audit and by
the dead-file gate;
- fails closed on absence: a missing .olean would make the scan vacuous, so
the count of compiled modules must equal the count of shipped sources;
- removes its temp source AND artifact on both paths, since a bare `rm`
after the call never runs under `set -e` when the gate goes red — exactly
how this repo accumulated 101 orphan .olean files;
- ~3 s for the whole corpus, against ~53 s for one module-importing run.
Phase 1's grep stays as a fast first line of defence. Phase 2b is the gate
that is load-bearing.
selftest-axgate.sh attacks the shipping gate, lifted out of check.sh at run
time rather than copied. It asserts the specific diagnostic, so a rejection
for an unrelated reason fails too, and it was itself negative-tested: with
the gate's throwError removed, the self-test goes red on exactly that case.
No proof, statement, specification or certificate is touched. No attested
commit is altered — the log binds specific commit hashes, all of which remain
ancestors of HEAD.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-28 16:24:18 +00:00
# 2b. kernel-side axiom-declaration gate: read every compiled Proofs/*.olean
# and reject ANY axiom declared there. Phase 1's grep reads source text
# and is evadable four ways (see the phase header); this one asks the
# kernel, derives its scope from the filesystem, and fails closed if the
# set of compiled modules does not match the set of shipped sources.
2026-07-02 12:17:44 +00:00
# 3. axiom audit: #print axioms for every certificate in CERTS; each must
# report exactly [propext, Classical.choice, Quot.sound]
verification: bind the statements, the specifications, and the model (P1-a)
Phases 3/3b establish what each certificate RESTS ON. Neither says what it
SAYS, nor what it is ABOUT. A certificate gutted to a tautology of the same
axiom cone passes both; so does one whose reference definition has been
redefined to BE the extracted code, at which point the theorem reads
`loop = loop` and every cone is byte-identical.
Phase 3c closes that. Proofs/Audit.lean emits a canonical block holding the
policy constants, every certificate's fully-elaborated statement (pp.all, so
implicit arguments, instances and universe levels are visible), and the body
of every specification constant transitively reachable from those statements.
Its SHA-256 is pinned in check.sh and the block itself is committed as
AUDIT-MANIFEST.txt, so a mismatch is DIFFED, not merely reported. 31
certificates, 68 specification constants per repository.
Two tiers, not one. These forks have an arithmetic tier that must stay
oracle-free and an apex tier carrying this fork's hash and wire-format axioms,
and the apex boundary genuinely differs per fork (dalek 8 extra names, anza 4,
risc0 and betrusted 5). One shared constant would have widened the arithmetic
tier to accept hash oracles, which is the most valuable property these repos
have. Each auditor is generated from its own repository's policy.
Phase 0b pins the extracted model. This was not a precaution: risc0 and
betrusted were observed emitting BYTE-IDENTICAL audit-manifest digests
(6c821b8e…) while shipping demonstrably different extracted models, their
point-doubling routines differing in operation order. A statement names an
extracted function; it does not contain that function's body. Binding
statements is not binding the subject. Membership derives from the filesystem,
so a new model file fails closed.
selftest-statements.sh attacks both phases with ten cases, each asserting a
specific diagnostic: an edited model body, an unlisted model file, a widened
policy, a hand-edited committed block, a certificate dropped from the auditor
WITH the digest refreshed to match, and a gutted statement whose cone is
unchanged. It lifts the phases out of check.sh at run time, so it attacks the
shipping gate rather than a copy.
Two bugs found and fixed during that testing, both mine: Phase 3c read `$0`
after `cd "$AENEAS_LEAN"`, and $0 is the caller's relative path; and the
axgate self-test compared the tree against a pristine checkout rather than
against how it found it. A third expectation was wrong rather than the code —
widening the apex boundary is caught by the exact-cone requirement before the
digest ever runs, which is a stronger rejection, and the test now says so.
All sixteen runs green at these commits: four main buttons, four axgate
self-tests, four binding self-tests, four scalar buttons.
TRUSTED-BASE.md records what this binds and, at equal length, what it does
not: a digest binds identity, not meaning; an author can rotate the pins in
one commit and is caught by review, not by the script; and pinning the model
says nothing about whether Charon and Aeneas translated the Rust faithfully.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-28 22:38:17 +00:00
# 3b. signature-apex audit: the four apex certificates against this fork's
# documented SHA-512 + wire-format boundary, exactly.
# 3c. statement + specification binding: Proofs/Audit.lean emits a canonical
# block of the policy constants, every certificate's fully-elaborated
# statement, and the body of every specification constant reachable from
# those statements. Its SHA-256 is pinned here and the block itself is
# committed, so a mismatch is diffable. This is the phase that makes a
# gutted statement, or a reference definition redefined to BE the
# extracted code, fail — neither moves any axiom cone.
2026-07-02 12:17:44 +00:00
# ─────────────────────────────────────────────────────────────────────────────
set -euo pipefail
source ~/aeneas-toolchain/env.sh
HERE = " $( cd " $( dirname " $0 " ) " && pwd ) "
AENEAS_LEAN = " $AENEAS_HOME /backends/lean "
TIMEOUT = " ${ LEAN_TIMEOUT :- 300 } "
2026-07-03 10:54:26 +00:00
export LEAN_MEM_MB = " ${ LEAN_MEM_MB :- 8192 } " # 8192: ReduceSpec exceeds 6144 (coherence pass 2)
2026-07-02 12:17:44 +00:00
CORES = " ${ LEAN_MAX_CORES :- 0 -3 } "
verification: --audit-only mode, and the guard that keeps it from becoming evidence (T1)
Gate work dominates this estate's wall-clock: on 2026-07-29, 3.9 hours of a
session went to Lean re-elaborating proofs nobody had edited while the audit
phases themselves took about fifteen seconds. --audit-only runs every gate
against the artifacts a previous full run left behind: ~60s against ~1280s.
IT IS SAFE ONLY BECAUSE IT REFUSES.
- It requires every shipped .lean to be BYTE-IDENTICAL to a basis recorded by
a previous full run. Not mtimes: `touch` defeats those, and a stale-artifact
check that fails open is worse than no shortcut at all, because a green
button would then describe a corpus that is no longer on disk.
- The basis is gitignored build state, so a fresh clone cannot inherit
permission to skip compiling.
- The closing banner differs and says in words that the run is not evidence.
selftest-auditonly.sh exercises seven cases: no basis, an edited comment
character, a deleted source, a new source, a missing artifact, a truncated
basis, and — asserted as a PASS — every source's mtime touched with bytes
unchanged, which pins the bytes-not-mtimes decision rather than leaving it
implicit. Negative-tested: with the basis comparison disabled a changed source
is wrongly accepted, exit 0 and zero refusals, so the guard is load-bearing.
A PHASE TERMINATOR, because this broke twice. Every self-test lifts a phase
from check.sh by scanning to the next phase marker. The last phase had no
marker after it, so a lift ran to end-of-file and swallowed whatever was
appended later — first Phase 2c into the axgate lift, then T1's tail into the
binding lift, where it referenced $AUDIT_ONLY and died under `set -u`. Both
surfaced as the BASELINE case failing: a self-test blaming a gate for its own
extraction bug. The phases now end at an explicit sentinel and both lifters
stop there, so nothing appended below can silently become part of the last
phase from a lifter's point of view.
TRUSTED-BASE.md records what an audit-only transcript does and does not
establish, and — because it cost a confusing red run today — that lean-guard's
memory clamp presents as `FAIL: Proofs/<module>` while being a resource
condition, not a broken proof.
Verified green: 8 full button runs (four check.sh, four check-scalar.sh) and 20
self-tests across the four repositories, zero red. One earlier run failed on
the memory clamp because the author ran a test suite concurrently; re-run on a
quiet machine, green.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-30 17:16:17 +00:00
# ── Mode selection ──────────────────────────────────────────────────────────
# --audit-only runs every gate EXCEPT the compile, against the .olean files a
# previous full run left behind. It exists because gate work dominates this
# estate's wall-clock: on 2026-07-29, 3.9 hours of a session went to Lean
# re-elaborating proofs nobody had edited, while the audit phases themselves
# take about fifteen seconds.
#
# IT MUST BE IMPOSSIBLE TO MISUSE, so:
# · it refuses to run unless a previous FULL run recorded a basis of source
# hashes AND every source still matches it byte-for-byte. Not mtimes —
# `touch` defeats those, and a stale-artifact check that fails open is
# worse than no shortcut at all, because a green button would then
# describe a corpus that is no longer on disk;
# · the basis file is build state, never committed, so a fresh clone cannot
# inherit permission to skip compiling;
# · the final banner DIFFERS, and says in words that the run is not evidence.
# A transcript must never be mistakable for a full one.
AUDIT_ONLY = 0
for arg in " $@ " ; do
case " $arg " in
--audit-only) AUDIT_ONLY = 1 ; ;
--help| -h) echo "usage: check.sh [--audit-only]" ; exit 0 ; ;
*) echo " unknown argument: $arg (see --help) " ; exit 1 ; ;
esac
done
BASIS = " $HERE /.audit-basis " # gitignored build state, written by full runs
# Every .lean this repository ships, with its hash: the exact set whose
# recompilation --audit-only proposes to skip.
source_basis( ) {
{ find " $HERE /Proofs " -name '*.lean' -type f -printf '%P\n' | sed 's|^|Proofs/|'
find " $HERE /gen " -name '*.lean' -type f -printf '%P\n' | sed 's|^|gen/|' ; } \
| LC_ALL = C sort | while read -r f; do printf '%s %s\n' " $( sha256sum " $HERE / $f " | cut -d' ' -f1) " " $f " ; done
}
2026-07-02 12:17:44 +00:00
# Layer manifests (extended as the pyramid grows; ORDER = import order).
GEN_MODULES = (
CurveField/TypesExternal
CurveField/Types
CurveField/FunsExternal
CurveField/Funs
THE SIGNATURE APEX: the EdDSA verification equation, proven and audited
`Proofs/SigApexSpec.lean`:
- `verify_loop_full` — the extracted 32-byte comparison loop returns exactly
the byte-equality of the two arrays (induction; axiom cone = exactly
[propext, Classical.choice, Quot.sound]).
- `verify_accepts_iff` — THE APEX: for a signature that parses, the
extracted RustCrypto verifier accepts IFF the recomputed compressed point
compress( [s]·B − [k]·A )
equals the signature's R byte-for-byte. The recomputation is grounded in
the PROVEN curve model (every curve and scalar call is a certified
definition); k is whatever scalar the SHA-512 oracle produces — the
honest EdDSA acceptance criterion with the hash opaque.
Boundary hygiene forced by the audit itself:
- The public vartime_double_scalar_mul_basepoint dispatch pulled the AVX2
vector-backend axiom into the apex cone. Fixed at the build level:
extract.sh pins RUSTFLAGS --cfg curve25519_dalek_backend="serial", so the
SIMD arm compiles out; BackendKind has only Serial and
get_selected_backend becomes a real definition (ok Serial).
- subtle.Choice.unwrap_u8 upgraded from axiom to the documented model
definition (Choice := U8; unwrap_u8 = self.0) — it sits on the verify
path via compress → is_negative.
- CurveSig modules added to GEN_MODULES (stale-olean incoherence otherwise).
check.sh grows Phase 3b: the apex certificate's axiom cone must equal
EXACTLY
[propext, Classical.choice, Quot.sound,
ed25519.Signature, sha2.Sha512,
sha512_new, sha512_update, sha512_finalize_bytes,
ed25519.Signature.to_bytes, signature.error.Error, Error.new]
— the SHA-512 hash oracle plus the opaque wire-format types. NO curve
axioms, NO scalar axioms, NO backend axioms, enforced on every button press.
Full check.sh green: 16 standard certificates + the apex audit.
Phase 2 (the point-level equation [s]B − [k]A = decompress R, needing
to_bytes canonicity and decompress) remains deferred and documented.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-04 17:45:55 +00:00
CurveSig/TypesExternal
CurveSig/Types
CurveSig/FunsExternal
CurveSig/Funs
2026-07-02 12:17:44 +00:00
)
PROOFS = (
Basic
Denote
P25519
ReduceSpec
SubNegSpec
ConstSpecs
AddSpec
MulSpec
SquareSpec
Square2Spec
Field
InvertSpec
FieldMain
FeQ
2026-07-02 12:50:42 +00:00
EdCurve
EdDenote
EdDouble
EdAddProjNiels
EdAddAffNiels
EdConvert
EdMain
2026-07-04 13:30:18 +00:00
DsmTableSpec
DsmStepSpec
DsmLoopSpec
DsmNafLoadSpec
DsmNafMath
NAF encoder proven end-to-end + the phase-1 double-scalar-mul apex
The complete non_adjacent_form(5) verification (four stages):
- `Proofs/DsmNafLoadSpec.lean` (generated) — the LE byte-to-word load.
- `Proofs/DsmNafMath.lean` — the digit loop's arithmetic core: window-read
lemmas (single/cross-word), the exact ZZ invariant steps (Nat.mod_mul
telescope), the carry-kill argument from V < 2^253, and the exit theorem.
- `Proofs/DsmNafLoopSpec.lean` — the w=5 digit loop by induction on the
remaining-bits measure: per-step 64-bit window read (4-way word split),
digit write via hcast/wrapping_sub (exact value window - 32*carry',
oddness, |d| < 16), invariant carried through even/odd steps.
- `Proofs/DsmNafSpec.lean` — the public spec: both entry masserts
DISCHARGED; the digits satisfy the NAF conditions and
sum naf[k]*2^k = V EXACTLY (integers, no modular slack)
for any scalar whose LE byte value V is below 2^253.
And the campaign's brick 4, `Proofs/DsmMulSpec.lean`:
- `run_basepoint` — the transpiled ED25519_BASEPOINT_POINT is the standard
base point: valid extended coordinates (X*Y = Z*T) and the curve equation,
kernel-checked via denominator-free 121666-scaled witnesses. Includes the
generic witness lemmas fp_mul_eq_of_witness / onCurve_of_witness.
- `vartime_double_base_mul_spec` — THE PHASE-1 COMPUTATIONAL SPEC of
vartime_double_base::mul: for canonical scalars and a valid on-curve A,
the result is valid, on-curve, and denotes
dsmFold (naf a) (naf b) (edPt A) edBasePt edId 256
with both digit arrays proven exact NAF encodings. Phase 2 (group
semantics [a]A + [b]B) requires Edwards associativity — deferred and
documented; nothing assumes it.
Also: removed a vestigial pre-re-extraction axiom stub
(backend.serial.scalar_mul.vartime_double_base.mul) from FunsExternal —
a root-level leftover that shadowed the real namespaced definition during
name resolution in proof files. Never referenced by any certificate (the
#print-axioms audit guards against that); deleted for hygiene.
CERTS += naf_load_spec, naf_exit, naf_digit_loop_spec,
non_adjacent_form_spec, run_basepoint, vartime_double_base_mul_spec —
each audited to exactly [propext, Classical.choice, Quot.sound].
Full check.sh green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-04 14:52:06 +00:00
DsmNafLoopSpec
DsmNafSpec
DsmMulSpec
Phase 2, brick 1a: to_bytes canonicity proven (to_bytes_spec, kernel-audited)
The load-bearing brick of the point-level apex equation:
FieldElement51::to_bytes always succeeds and its 32 output bytes denote
EXACTLY the represented residue - bytesVal s = feVal a mod p. Since the
canonical residue determines the bytes, this is simultaneously
canonicity ("output is the canonical encoding") and the injectivity
compress needs ("equal residues iff equal bytes").
- Proofs/ToBytesMath.lean: the context-free ℕ mathematics (METHOD 4) -
the 5-rung carry telescope (div_rung/q_telescope), the q-trick facts
(q = (h+19)/2^255 is a bit, fires iff h >= p), q_mod_p (adding 19q and
discarding bit 255 subtracts pq exactly), carry_pack (the masked-limb
assembly mod 2^255), five per-limb byte-chunk splits, and bytes_pack
(the 32-byte little-endian reassembly, closed by one zify +
linear_combination over the five splits).
- Proofs/ToBytesSpec.lean: the symbolic execution - at ~150 machine ops
the longest walk in the repo, loop-free: weak reduce (reduce_spec),
the q pass, the fold + carry pass, 32 byte extractions (the four
limb-boundary bytes turn disjoint ORs into additions via
Nat.two_pow_add_eq_or_of_lt), and the trailing top-bit debug-assert
DISCHARGED (b31 = f4/2^44 < 2^7), not assumed.
- check.sh: ToBytesMath/ToBytesSpec in PROOFS, to_bytes_spec in CERTS
(exact standard-three audit) - full button green fresh.
Walk lessons (for the control repo, next push): rw index-equations into
their consumers instead of subst (subst eliminates the wrong side or
dies on dependent do-motives); never rw [Nat.mod_eq_of_lt (by omega)]
(metavariable goal reaches omega) - state the bound with show.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-05 11:10:43 +00:00
ToBytesMath
ToBytesSpec
Phase 2, brick 1 complete: ed_compress_spec - compress emits the canonical
encoding of the denoted affine point (kernel-audited)
CurveFieldProofs.ed_compress_spec: for any valid extended point Pt
(ExtValid - the invariant every certified curve op guarantees),
compress Pt = ok s with
bytesVal s = (edY Pt).val + ((edX Pt).val % 2) * 2^255
- the 32 wire bytes are the canonical little-endian y-residue with the
x-parity bit at position 255. Compress semantics AND canonicity in one
statement, because to_bytes_spec pins the bytes to the residue itself.
Supporting certificates in Proofs/CompressSpec.lean:
- is_negative_spec: the sign read is the parity of the CANONICAL residue
(bit 0 of to_bytes) - (feVal x mod p) mod 2.
- Bytes32.exists_bytes: the 32-byte destructuring device (the
Fe.exists_limbs idiom, 32-wide).
- to_bytes_spec': premise-free restatement of the canonicity brick.
- xor_top_bit (ToBytesMath): setting a clear top bit by XOR is addition -
proven from xor_div_two_pow + and_xor_distrib_right, no bit-blasting.
The chain is entirely certified code: invert (Fermat), two muls, to_bytes
(canonicity), is_negative, and the sign-bit XOR. Axiom cone of
ed_compress_spec: exactly [propext, Classical.choice, Quot.sound].
check.sh: CompressSpec in PROOFS, ed_compress_spec in CERTS - full button
green fresh.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-05 11:33:58 +00:00
CompressSpec
2026-07-05 12:10:09 +00:00
ScalarPackSpec
THE SIGNATURE APEX: the EdDSA verification equation, proven and audited
`Proofs/SigApexSpec.lean`:
- `verify_loop_full` — the extracted 32-byte comparison loop returns exactly
the byte-equality of the two arrays (induction; axiom cone = exactly
[propext, Classical.choice, Quot.sound]).
- `verify_accepts_iff` — THE APEX: for a signature that parses, the
extracted RustCrypto verifier accepts IFF the recomputed compressed point
compress( [s]·B − [k]·A )
equals the signature's R byte-for-byte. The recomputation is grounded in
the PROVEN curve model (every curve and scalar call is a certified
definition); k is whatever scalar the SHA-512 oracle produces — the
honest EdDSA acceptance criterion with the hash opaque.
Boundary hygiene forced by the audit itself:
- The public vartime_double_scalar_mul_basepoint dispatch pulled the AVX2
vector-backend axiom into the apex cone. Fixed at the build level:
extract.sh pins RUSTFLAGS --cfg curve25519_dalek_backend="serial", so the
SIMD arm compiles out; BackendKind has only Serial and
get_selected_backend becomes a real definition (ok Serial).
- subtle.Choice.unwrap_u8 upgraded from axiom to the documented model
definition (Choice := U8; unwrap_u8 = self.0) — it sits on the verify
path via compress → is_negative.
- CurveSig modules added to GEN_MODULES (stale-olean incoherence otherwise).
check.sh grows Phase 3b: the apex certificate's axiom cone must equal
EXACTLY
[propext, Classical.choice, Quot.sound,
ed25519.Signature, sha2.Sha512,
sha512_new, sha512_update, sha512_finalize_bytes,
ed25519.Signature.to_bytes, signature.error.Error, Error.new]
— the SHA-512 hash oracle plus the opaque wire-format types. NO curve
axioms, NO scalar axioms, NO backend axioms, enforced on every button press.
Full check.sh green: 16 standard certificates + the apex audit.
Phase 2 (the point-level equation [s]B − [k]A = decompress R, needing
to_bytes canonicity and decompress) remains deferred and documented.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-04 17:45:55 +00:00
SigApexSpec
2026-07-05 12:36:03 +00:00
PointLiftSpec
2026-07-05 16:27:25 +00:00
PointEqSpec
2026-07-05 18:08:21 +00:00
DecompressSpec
2026-07-05 20:55:18 +00:00
FromBytesSpec
PHASE 2 COMPLETE ON DALEK: THE FULL POINT-LEVEL LIFT
(verify_accepts_iff_decompress, button-enforced)
THE THEOREM: under the apex hypotheses, the signature's R bytes
DECOMPRESS to a valid on-curve point Pt, and
verifier accepts <=> Pt = [k]*(-A) + [s]*B (as points)
- accept iff decompress(R) equals the recomputed point. Every link of
the chain (byte comparison <-> canonical-encoding equality <-> point
equality <-> decompressed-point equality) is machine-checked over the
extracted code. Axiom cone EXACTLY the SHA-512 + wire-format boundary;
Phase 3b now enforces FOUR certificate tiers (byte apex, half-lift,
point equation, full lift).
Proofs/DecompressMain.lean:
- edwards_d_denote: the extracted EDWARDS_D constant denotes THE curve
d (edwards_d_spec + edD_char cancelled by 121666 nonzero).
- decompress_of_canonical (standard three axioms): canonical encodings
of valid on-curve points decompress to them - from_bytes recovers the
y-residue exactly (sign bit discarded), Q's own x witnesses the
square so sqrt_ratio_i returns the even root, the sign bit (Q's
x-parity, from byte 31) selects +/-root, and the parity-injectivity
argument pins the selection to edX Q; the assembled {X,Y,1,X*Y} is
ExtValid and on-curve.
- verify_accepts_iff_decompress: the capstone composition.
Full button green fresh. Remaining: replicate x3, coherence pass 4.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-05 22:05:55 +00:00
DecompressMain
verification: build hygiene, and the hidden dependency it exposed (P0-a)
Phase 0a purges every .olean before compiling, bans stray Lean files at the
verification root (LEAN_PATH contains $PWD, so they join the build unaudited),
and requires gen/ to be exactly the model manifest plus its pinned templates.
The templates are KEPT, unlike SLH-DSA which deletes them: extract.sh directs
the operator to diff the hand-written external models against them, so they are
the reference for that comparison and P2-c will enforce it.
The purge is skipped under --audit-only, which exists to audit the artifacts a
previous full run produced. Those two features would otherwise destroy each
other, and it is a further reason an audit-only transcript is not evidence: it
has not had this hygiene applied.
WHAT THE PURGE EXPOSED, and it is the point of the whole item:
This button had never compiled the corpus from nothing. The signature apex
rests on scalar arithmetic — PointLiftSpec -> ScalarPackSpec ->
ScalarFromBytesSpec, and SigApexSpec -> ScalarDenote — and TWELVE of the scalar
layer's thirteen modules are transitive prerequisites of this manifest. They
were never compiled here. The button worked because check-scalar.sh had run at
some earlier point and left its .olean files behind. .olean is gitignored, so
no git status could ever have shown that the verdict rested on untracked
artifacts produced by a different script.
Nothing about the proofs was wrong. The evidence was resting on something
invisible, for the entire life of these repositories, and it surfaced the
moment something finally cleaned up before verifying.
Those twelve are now compiled here as PREREQ — BORROWED, NOT OWNED.
check-scalar.sh still audits them; Phase 1b asserts every borrowed name belongs
to the other manifest and to neither twice, so the list cannot become a second
ownership claim.
Two consequences fixed along the way, both the spelling-versus-membership error
that ScalarPackSpec has now taught four times:
- Phase 2b globbed Proofs/*.olean and would have demanded artifacts this
button never builds. It now scans its manifest by membership and fails
closed on a missing one.
- The three inventory drivers were exempted from the dead-file gate and
compiled in a later phase; after a purge they were absent when Phase 2b
ran. They are now in the manifest like everything else, and three
exemptions are gone.
The sweep runner now reports RESOURCE rather than RED when it sees a
memory_exception: lean-guard's clamp is not a broken proof, and it has misled
the operator once and the author once.
Verified green: 8 full runs from completely purged trees — four check.sh, four
check-scalar.sh — zero red, zero resource. Every artifact rebuilt from
committed source. These are the first runs in this repository's history whose
verdict provably depends on nothing but the bytes in git.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-30 20:54:00 +00:00
Audit # imports the certificate corpus and runs the audit
InventoryCore # inventory machinery (imports only Lean)
Inventory # inventory driver: main chain
InventoryBasic # inventory driver: Proofs.Basic (kept separate: name collision)
)
# Modules this button must COMPILE but does not OWN.
#
# The signature apex rests on scalar arithmetic: PointLiftSpec needs
# ScalarPackSpec which needs ScalarFromBytesSpec, and SigApexSpec needs
# ScalarDenote. Twelve of the scalar layer's thirteen modules are
# transitive prerequisites of this manifest.
#
# Until Phase 0a began purging, this button appeared to work without them:
# it silently consumed .olean files that a previous check-scalar.sh run had
# left lying about. The verdict depended on untracked build state produced
# by a DIFFERENT script — precisely the condition build hygiene exists to
# expose, and it stayed invisible for as long as nothing ever cleaned up.
#
# OWNERSHIP IS UNCHANGED: check-scalar.sh audits these — their cones, their
# declaration inventory, their axiom gate. This button only builds them so
# that running it alone is self-contained. Phase 1b asserts that every name
# here belongs to the OTHER manifest, so this list can never quietly become
# a second claim of ownership.
PREREQ = (
ScalarDenote
ScalarLoop
ScalarSubSpec
ScalarAddSpec
ScalarMulSpec
ScalarMontSpec
ScalarReduceSpec
ScalarFullMulSpec
ScalarWideSpec
ScalarBytesSpec
ScalarUnpackSpec
ScalarFromBytesSpec
2026-07-02 12:17:44 +00:00
)
# Fully-qualified certificate names; each must be axiom-clean.
CERTS = (
CurveFieldProofs.fieldImplementation
2026-07-02 12:50:42 +00:00
CurveFieldProofs.edwardsImplementation
2026-07-04 13:30:18 +00:00
CurveFieldProofs.naf_table_spec
CurveFieldProofs.naf_select_spec
CurveFieldProofs.proj_double_law
CurveFieldProofs.compl_as_projective_law
CurveFieldProofs.dsm_step_p_law
CurveFieldProofs.dsm_step_b_law
CurveFieldProofs.dsm_loop_spec
CurveFieldProofs.naf_load_spec
CurveFieldProofs.naf_exit
NAF encoder proven end-to-end + the phase-1 double-scalar-mul apex
The complete non_adjacent_form(5) verification (four stages):
- `Proofs/DsmNafLoadSpec.lean` (generated) — the LE byte-to-word load.
- `Proofs/DsmNafMath.lean` — the digit loop's arithmetic core: window-read
lemmas (single/cross-word), the exact ZZ invariant steps (Nat.mod_mul
telescope), the carry-kill argument from V < 2^253, and the exit theorem.
- `Proofs/DsmNafLoopSpec.lean` — the w=5 digit loop by induction on the
remaining-bits measure: per-step 64-bit window read (4-way word split),
digit write via hcast/wrapping_sub (exact value window - 32*carry',
oddness, |d| < 16), invariant carried through even/odd steps.
- `Proofs/DsmNafSpec.lean` — the public spec: both entry masserts
DISCHARGED; the digits satisfy the NAF conditions and
sum naf[k]*2^k = V EXACTLY (integers, no modular slack)
for any scalar whose LE byte value V is below 2^253.
And the campaign's brick 4, `Proofs/DsmMulSpec.lean`:
- `run_basepoint` — the transpiled ED25519_BASEPOINT_POINT is the standard
base point: valid extended coordinates (X*Y = Z*T) and the curve equation,
kernel-checked via denominator-free 121666-scaled witnesses. Includes the
generic witness lemmas fp_mul_eq_of_witness / onCurve_of_witness.
- `vartime_double_base_mul_spec` — THE PHASE-1 COMPUTATIONAL SPEC of
vartime_double_base::mul: for canonical scalars and a valid on-curve A,
the result is valid, on-curve, and denotes
dsmFold (naf a) (naf b) (edPt A) edBasePt edId 256
with both digit arrays proven exact NAF encodings. Phase 2 (group
semantics [a]A + [b]B) requires Edwards associativity — deferred and
documented; nothing assumes it.
Also: removed a vestigial pre-re-extraction axiom stub
(backend.serial.scalar_mul.vartime_double_base.mul) from FunsExternal —
a root-level leftover that shadowed the real namespaced definition during
name resolution in proof files. Never referenced by any certificate (the
#print-axioms audit guards against that); deleted for hygiene.
CERTS += naf_load_spec, naf_exit, naf_digit_loop_spec,
non_adjacent_form_spec, run_basepoint, vartime_double_base_mul_spec —
each audited to exactly [propext, Classical.choice, Quot.sound].
Full check.sh green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-04 14:52:06 +00:00
CurveFieldProofs.naf_digit_loop_spec
CurveFieldProofs.non_adjacent_form_spec
CurveFieldProofs.run_basepoint
CurveFieldProofs.vartime_double_base_mul_spec
THE SIGNATURE APEX: the EdDSA verification equation, proven and audited
`Proofs/SigApexSpec.lean`:
- `verify_loop_full` — the extracted 32-byte comparison loop returns exactly
the byte-equality of the two arrays (induction; axiom cone = exactly
[propext, Classical.choice, Quot.sound]).
- `verify_accepts_iff` — THE APEX: for a signature that parses, the
extracted RustCrypto verifier accepts IFF the recomputed compressed point
compress( [s]·B − [k]·A )
equals the signature's R byte-for-byte. The recomputation is grounded in
the PROVEN curve model (every curve and scalar call is a certified
definition); k is whatever scalar the SHA-512 oracle produces — the
honest EdDSA acceptance criterion with the hash opaque.
Boundary hygiene forced by the audit itself:
- The public vartime_double_scalar_mul_basepoint dispatch pulled the AVX2
vector-backend axiom into the apex cone. Fixed at the build level:
extract.sh pins RUSTFLAGS --cfg curve25519_dalek_backend="serial", so the
SIMD arm compiles out; BackendKind has only Serial and
get_selected_backend becomes a real definition (ok Serial).
- subtle.Choice.unwrap_u8 upgraded from axiom to the documented model
definition (Choice := U8; unwrap_u8 = self.0) — it sits on the verify
path via compress → is_negative.
- CurveSig modules added to GEN_MODULES (stale-olean incoherence otherwise).
check.sh grows Phase 3b: the apex certificate's axiom cone must equal
EXACTLY
[propext, Classical.choice, Quot.sound,
ed25519.Signature, sha2.Sha512,
sha512_new, sha512_update, sha512_finalize_bytes,
ed25519.Signature.to_bytes, signature.error.Error, Error.new]
— the SHA-512 hash oracle plus the opaque wire-format types. NO curve
axioms, NO scalar axioms, NO backend axioms, enforced on every button press.
Full check.sh green: 16 standard certificates + the apex audit.
Phase 2 (the point-level equation [s]B − [k]A = decompress R, needing
to_bytes canonicity and decompress) remains deferred and documented.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-04 17:45:55 +00:00
CurveFieldProofs.verify_loop_full
Phase 2, brick 1a: to_bytes canonicity proven (to_bytes_spec, kernel-audited)
The load-bearing brick of the point-level apex equation:
FieldElement51::to_bytes always succeeds and its 32 output bytes denote
EXACTLY the represented residue - bytesVal s = feVal a mod p. Since the
canonical residue determines the bytes, this is simultaneously
canonicity ("output is the canonical encoding") and the injectivity
compress needs ("equal residues iff equal bytes").
- Proofs/ToBytesMath.lean: the context-free ℕ mathematics (METHOD 4) -
the 5-rung carry telescope (div_rung/q_telescope), the q-trick facts
(q = (h+19)/2^255 is a bit, fires iff h >= p), q_mod_p (adding 19q and
discarding bit 255 subtracts pq exactly), carry_pack (the masked-limb
assembly mod 2^255), five per-limb byte-chunk splits, and bytes_pack
(the 32-byte little-endian reassembly, closed by one zify +
linear_combination over the five splits).
- Proofs/ToBytesSpec.lean: the symbolic execution - at ~150 machine ops
the longest walk in the repo, loop-free: weak reduce (reduce_spec),
the q pass, the fold + carry pass, 32 byte extractions (the four
limb-boundary bytes turn disjoint ORs into additions via
Nat.two_pow_add_eq_or_of_lt), and the trailing top-bit debug-assert
DISCHARGED (b31 = f4/2^44 < 2^7), not assumed.
- check.sh: ToBytesMath/ToBytesSpec in PROOFS, to_bytes_spec in CERTS
(exact standard-three audit) - full button green fresh.
Walk lessons (for the control repo, next push): rw index-equations into
their consumers instead of subst (subst eliminates the wrong side or
dies on dependent do-motives); never rw [Nat.mod_eq_of_lt (by omega)]
(metavariable goal reaches omega) - state the bound with show.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-05 11:10:43 +00:00
CurveFieldProofs.to_bytes_spec
Phase 2, brick 1 complete: ed_compress_spec - compress emits the canonical
encoding of the denoted affine point (kernel-audited)
CurveFieldProofs.ed_compress_spec: for any valid extended point Pt
(ExtValid - the invariant every certified curve op guarantees),
compress Pt = ok s with
bytesVal s = (edY Pt).val + ((edX Pt).val % 2) * 2^255
- the 32 wire bytes are the canonical little-endian y-residue with the
x-parity bit at position 255. Compress semantics AND canonicity in one
statement, because to_bytes_spec pins the bytes to the residue itself.
Supporting certificates in Proofs/CompressSpec.lean:
- is_negative_spec: the sign read is the parity of the CANONICAL residue
(bit 0 of to_bytes) - (feVal x mod p) mod 2.
- Bytes32.exists_bytes: the 32-byte destructuring device (the
Fe.exists_limbs idiom, 32-wide).
- to_bytes_spec': premise-free restatement of the canonicity brick.
- xor_top_bit (ToBytesMath): setting a clear top bit by XOR is addition -
proven from xor_div_two_pow + and_xor_distrib_right, no bit-blasting.
The chain is entirely certified code: invert (Fermat), two muls, to_bytes
(canonicity), is_negative, and the sign-bit XOR. Axiom cone of
ed_compress_spec: exactly [propext, Classical.choice, Quot.sound].
check.sh: CompressSpec in PROOFS, ed_compress_spec in CERTS - full button
green fresh.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-05 11:33:58 +00:00
CurveFieldProofs.ed_compress_spec
2026-07-05 12:10:09 +00:00
ScalarProofs.from_bytes_mod_order_wide_spec
2026-07-05 12:36:03 +00:00
CurveFieldProofs.vartime_dsm_basepoint_spec
2026-07-05 16:27:25 +00:00
CurveFieldProofs.enc_point_inj
2026-07-05 18:08:21 +00:00
CurveFieldProofs.pow_p58_spec
CurveFieldProofs.fe_ct_eq_spec
2026-07-05 19:16:05 +00:00
CurveFieldProofs.sqrt_core
Phase 2, decompress part 2b: THE SQUARE-ROOT WALK PROVEN
(sqrt_ratio_i_sq_spec, kernel-audited)
The largest single proof of the decompress chain: for square u/v
(witness x, v nonzero), the extracted sqrt_ratio_i returns choice 1 and
the even-parity root - Bnd r (2^52), r^2 * v = u, r's canonical residue
even. The walk composes every previously certified piece: the
square/mul/pow_p58 candidate chain, sqrt_m1_spec, fe_ct_eq_spec x3 (the
three constant-time residue checks), neg_spec, the Choice bitor, and
fe_cond_assign_spec twice (root flip by sqrt(-1), then sign
normalization via is_negative).
Case analysis: sqrt_core's disjunction (v*r^2 = +/-u) against the check
flags - u = 0 collapses everything to the zero root; u != 0 with
v*r^2 = u kills both flip flags (u = -u forces u = 0 in odd
characteristic; u = -u*i forces u*(1+i) = 0 with 1+i nonzero); with
v*r^2 = -u the flip fires and (i*r)^2 * v = -(-u) = u. Parity: the odd-
prime negation flip (ZMod.neg_val), zero-root edge included. New
helpers: eq_neg_self_iff_zero, one_add_i_ne_zero.
Certificate exact standard three; full button green fresh. Remaining:
from_bytes walk, decompress_of_canonical, replication, pass 4.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-05 20:03:57 +00:00
CurveFieldProofs.sqrt_ratio_i_sq_spec
2026-07-05 20:55:18 +00:00
CurveFieldProofs.from_bytes_spec
PHASE 2 COMPLETE ON DALEK: THE FULL POINT-LEVEL LIFT
(verify_accepts_iff_decompress, button-enforced)
THE THEOREM: under the apex hypotheses, the signature's R bytes
DECOMPRESS to a valid on-curve point Pt, and
verifier accepts <=> Pt = [k]*(-A) + [s]*B (as points)
- accept iff decompress(R) equals the recomputed point. Every link of
the chain (byte comparison <-> canonical-encoding equality <-> point
equality <-> decompressed-point equality) is machine-checked over the
extracted code. Axiom cone EXACTLY the SHA-512 + wire-format boundary;
Phase 3b now enforces FOUR certificate tiers (byte apex, half-lift,
point equation, full lift).
Proofs/DecompressMain.lean:
- edwards_d_denote: the extracted EDWARDS_D constant denotes THE curve
d (edwards_d_spec + edD_char cancelled by 121666 nonzero).
- decompress_of_canonical (standard three axioms): canonical encodings
of valid on-curve points decompress to them - from_bytes recovers the
y-residue exactly (sign bit discarded), Q's own x witnesses the
square so sqrt_ratio_i returns the even root, the sign bit (Q's
x-parity, from byte 31) selects +/-root, and the parity-injectivity
argument pins the selection to edX Q; the assembled {X,Y,1,X*Y} is
ExtValid and on-curve.
- verify_accepts_iff_decompress: the capstone composition.
Full button green fresh. Remaining: replicate x3, coherence pass 4.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-05 22:05:55 +00:00
CurveFieldProofs.decompress_of_canonical
2026-07-02 12:17:44 +00:00
)
# Imports needed so every certificate in CERTS is in scope for the audit.
AUDIT_IMPORTS = (
Proofs.FieldMain
2026-07-02 12:50:42 +00:00
Proofs.EdMain
2026-07-04 13:30:18 +00:00
Proofs.DsmTableSpec
Proofs.DsmStepSpec
Proofs.DsmLoopSpec
Proofs.DsmNafLoadSpec
Proofs.DsmNafMath
NAF encoder proven end-to-end + the phase-1 double-scalar-mul apex
The complete non_adjacent_form(5) verification (four stages):
- `Proofs/DsmNafLoadSpec.lean` (generated) — the LE byte-to-word load.
- `Proofs/DsmNafMath.lean` — the digit loop's arithmetic core: window-read
lemmas (single/cross-word), the exact ZZ invariant steps (Nat.mod_mul
telescope), the carry-kill argument from V < 2^253, and the exit theorem.
- `Proofs/DsmNafLoopSpec.lean` — the w=5 digit loop by induction on the
remaining-bits measure: per-step 64-bit window read (4-way word split),
digit write via hcast/wrapping_sub (exact value window - 32*carry',
oddness, |d| < 16), invariant carried through even/odd steps.
- `Proofs/DsmNafSpec.lean` — the public spec: both entry masserts
DISCHARGED; the digits satisfy the NAF conditions and
sum naf[k]*2^k = V EXACTLY (integers, no modular slack)
for any scalar whose LE byte value V is below 2^253.
And the campaign's brick 4, `Proofs/DsmMulSpec.lean`:
- `run_basepoint` — the transpiled ED25519_BASEPOINT_POINT is the standard
base point: valid extended coordinates (X*Y = Z*T) and the curve equation,
kernel-checked via denominator-free 121666-scaled witnesses. Includes the
generic witness lemmas fp_mul_eq_of_witness / onCurve_of_witness.
- `vartime_double_base_mul_spec` — THE PHASE-1 COMPUTATIONAL SPEC of
vartime_double_base::mul: for canonical scalars and a valid on-curve A,
the result is valid, on-curve, and denotes
dsmFold (naf a) (naf b) (edPt A) edBasePt edId 256
with both digit arrays proven exact NAF encodings. Phase 2 (group
semantics [a]A + [b]B) requires Edwards associativity — deferred and
documented; nothing assumes it.
Also: removed a vestigial pre-re-extraction axiom stub
(backend.serial.scalar_mul.vartime_double_base.mul) from FunsExternal —
a root-level leftover that shadowed the real namespaced definition during
name resolution in proof files. Never referenced by any certificate (the
#print-axioms audit guards against that); deleted for hygiene.
CERTS += naf_load_spec, naf_exit, naf_digit_loop_spec,
non_adjacent_form_spec, run_basepoint, vartime_double_base_mul_spec —
each audited to exactly [propext, Classical.choice, Quot.sound].
Full check.sh green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-04 14:52:06 +00:00
Proofs.DsmNafSpec
Proofs.DsmMulSpec
Phase 2, brick 1a: to_bytes canonicity proven (to_bytes_spec, kernel-audited)
The load-bearing brick of the point-level apex equation:
FieldElement51::to_bytes always succeeds and its 32 output bytes denote
EXACTLY the represented residue - bytesVal s = feVal a mod p. Since the
canonical residue determines the bytes, this is simultaneously
canonicity ("output is the canonical encoding") and the injectivity
compress needs ("equal residues iff equal bytes").
- Proofs/ToBytesMath.lean: the context-free ℕ mathematics (METHOD 4) -
the 5-rung carry telescope (div_rung/q_telescope), the q-trick facts
(q = (h+19)/2^255 is a bit, fires iff h >= p), q_mod_p (adding 19q and
discarding bit 255 subtracts pq exactly), carry_pack (the masked-limb
assembly mod 2^255), five per-limb byte-chunk splits, and bytes_pack
(the 32-byte little-endian reassembly, closed by one zify +
linear_combination over the five splits).
- Proofs/ToBytesSpec.lean: the symbolic execution - at ~150 machine ops
the longest walk in the repo, loop-free: weak reduce (reduce_spec),
the q pass, the fold + carry pass, 32 byte extractions (the four
limb-boundary bytes turn disjoint ORs into additions via
Nat.two_pow_add_eq_or_of_lt), and the trailing top-bit debug-assert
DISCHARGED (b31 = f4/2^44 < 2^7), not assumed.
- check.sh: ToBytesMath/ToBytesSpec in PROOFS, to_bytes_spec in CERTS
(exact standard-three audit) - full button green fresh.
Walk lessons (for the control repo, next push): rw index-equations into
their consumers instead of subst (subst eliminates the wrong side or
dies on dependent do-motives); never rw [Nat.mod_eq_of_lt (by omega)]
(metavariable goal reaches omega) - state the bound with show.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-05 11:10:43 +00:00
Proofs.ToBytesSpec
Phase 2, brick 1 complete: ed_compress_spec - compress emits the canonical
encoding of the denoted affine point (kernel-audited)
CurveFieldProofs.ed_compress_spec: for any valid extended point Pt
(ExtValid - the invariant every certified curve op guarantees),
compress Pt = ok s with
bytesVal s = (edY Pt).val + ((edX Pt).val % 2) * 2^255
- the 32 wire bytes are the canonical little-endian y-residue with the
x-parity bit at position 255. Compress semantics AND canonicity in one
statement, because to_bytes_spec pins the bytes to the residue itself.
Supporting certificates in Proofs/CompressSpec.lean:
- is_negative_spec: the sign read is the parity of the CANONICAL residue
(bit 0 of to_bytes) - (feVal x mod p) mod 2.
- Bytes32.exists_bytes: the 32-byte destructuring device (the
Fe.exists_limbs idiom, 32-wide).
- to_bytes_spec': premise-free restatement of the canonicity brick.
- xor_top_bit (ToBytesMath): setting a clear top bit by XOR is addition -
proven from xor_div_two_pow + and_xor_distrib_right, no bit-blasting.
The chain is entirely certified code: invert (Fermat), two muls, to_bytes
(canonicity), is_negative, and the sign-bit XOR. Axiom cone of
ed_compress_spec: exactly [propext, Classical.choice, Quot.sound].
check.sh: CompressSpec in PROOFS, ed_compress_spec in CERTS - full button
green fresh.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-05 11:33:58 +00:00
Proofs.CompressSpec
2026-07-05 12:10:09 +00:00
Proofs.ScalarPackSpec
THE SIGNATURE APEX: the EdDSA verification equation, proven and audited
`Proofs/SigApexSpec.lean`:
- `verify_loop_full` — the extracted 32-byte comparison loop returns exactly
the byte-equality of the two arrays (induction; axiom cone = exactly
[propext, Classical.choice, Quot.sound]).
- `verify_accepts_iff` — THE APEX: for a signature that parses, the
extracted RustCrypto verifier accepts IFF the recomputed compressed point
compress( [s]·B − [k]·A )
equals the signature's R byte-for-byte. The recomputation is grounded in
the PROVEN curve model (every curve and scalar call is a certified
definition); k is whatever scalar the SHA-512 oracle produces — the
honest EdDSA acceptance criterion with the hash opaque.
Boundary hygiene forced by the audit itself:
- The public vartime_double_scalar_mul_basepoint dispatch pulled the AVX2
vector-backend axiom into the apex cone. Fixed at the build level:
extract.sh pins RUSTFLAGS --cfg curve25519_dalek_backend="serial", so the
SIMD arm compiles out; BackendKind has only Serial and
get_selected_backend becomes a real definition (ok Serial).
- subtle.Choice.unwrap_u8 upgraded from axiom to the documented model
definition (Choice := U8; unwrap_u8 = self.0) — it sits on the verify
path via compress → is_negative.
- CurveSig modules added to GEN_MODULES (stale-olean incoherence otherwise).
check.sh grows Phase 3b: the apex certificate's axiom cone must equal
EXACTLY
[propext, Classical.choice, Quot.sound,
ed25519.Signature, sha2.Sha512,
sha512_new, sha512_update, sha512_finalize_bytes,
ed25519.Signature.to_bytes, signature.error.Error, Error.new]
— the SHA-512 hash oracle plus the opaque wire-format types. NO curve
axioms, NO scalar axioms, NO backend axioms, enforced on every button press.
Full check.sh green: 16 standard certificates + the apex audit.
Phase 2 (the point-level equation [s]B − [k]A = decompress R, needing
to_bytes canonicity and decompress) remains deferred and documented.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-04 17:45:55 +00:00
Proofs.SigApexSpec
2026-07-05 12:36:03 +00:00
Proofs.PointLiftSpec
2026-07-05 16:27:25 +00:00
Proofs.PointEqSpec
2026-07-05 18:08:21 +00:00
Proofs.DecompressSpec
2026-07-05 20:55:18 +00:00
Proofs.FromBytesSpec
PHASE 2 COMPLETE ON DALEK: THE FULL POINT-LEVEL LIFT
(verify_accepts_iff_decompress, button-enforced)
THE THEOREM: under the apex hypotheses, the signature's R bytes
DECOMPRESS to a valid on-curve point Pt, and
verifier accepts <=> Pt = [k]*(-A) + [s]*B (as points)
- accept iff decompress(R) equals the recomputed point. Every link of
the chain (byte comparison <-> canonical-encoding equality <-> point
equality <-> decompressed-point equality) is machine-checked over the
extracted code. Axiom cone EXACTLY the SHA-512 + wire-format boundary;
Phase 3b now enforces FOUR certificate tiers (byte apex, half-lift,
point equation, full lift).
Proofs/DecompressMain.lean:
- edwards_d_denote: the extracted EDWARDS_D constant denotes THE curve
d (edwards_d_spec + edD_char cancelled by 121666 nonzero).
- decompress_of_canonical (standard three axioms): canonical encodings
of valid on-curve points decompress to them - from_bytes recovers the
y-residue exactly (sign bit discarded), Q's own x witnesses the
square so sqrt_ratio_i returns the even root, the sign bit (Q's
x-parity, from byte 31) selects +/-root, and the parity-injectivity
argument pins the selection to edX Q; the assembled {X,Y,1,X*Y} is
ExtValid and on-curve.
- verify_accepts_iff_decompress: the capstone composition.
Full button green fresh. Remaining: replicate x3, coherence pass 4.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-05 22:05:55 +00:00
Proofs.DecompressMain
2026-07-02 12:17:44 +00:00
)
# ── Phase 0: resource + integrity guards ────────────────────────────────────
free -m | awk '/Mem:/{if($7<2048){print "FATAL: <2GB RAM available — refusing to compile"; exit 1}}'
echo "=== Phase 0: source integrity ==="
for f in " $HERE " /gen/CurveField/*.lean " $HERE " /Proofs/*.lean; do
[ -f " $f " ] || continue
if ! grep -qE '^(/-|import |namespace |theorem |def |open |set_option |--)' " $f " ; then
echo " CORRUPTED: $f is not Lean source (olean clobber?). Restore: git checkout HEAD -- $f "
exit 1
fi
done
echo " all sources valid"
verification: build hygiene, and the hidden dependency it exposed (P0-a)
Phase 0a purges every .olean before compiling, bans stray Lean files at the
verification root (LEAN_PATH contains $PWD, so they join the build unaudited),
and requires gen/ to be exactly the model manifest plus its pinned templates.
The templates are KEPT, unlike SLH-DSA which deletes them: extract.sh directs
the operator to diff the hand-written external models against them, so they are
the reference for that comparison and P2-c will enforce it.
The purge is skipped under --audit-only, which exists to audit the artifacts a
previous full run produced. Those two features would otherwise destroy each
other, and it is a further reason an audit-only transcript is not evidence: it
has not had this hygiene applied.
WHAT THE PURGE EXPOSED, and it is the point of the whole item:
This button had never compiled the corpus from nothing. The signature apex
rests on scalar arithmetic — PointLiftSpec -> ScalarPackSpec ->
ScalarFromBytesSpec, and SigApexSpec -> ScalarDenote — and TWELVE of the scalar
layer's thirteen modules are transitive prerequisites of this manifest. They
were never compiled here. The button worked because check-scalar.sh had run at
some earlier point and left its .olean files behind. .olean is gitignored, so
no git status could ever have shown that the verdict rested on untracked
artifacts produced by a different script.
Nothing about the proofs was wrong. The evidence was resting on something
invisible, for the entire life of these repositories, and it surfaced the
moment something finally cleaned up before verifying.
Those twelve are now compiled here as PREREQ — BORROWED, NOT OWNED.
check-scalar.sh still audits them; Phase 1b asserts every borrowed name belongs
to the other manifest and to neither twice, so the list cannot become a second
ownership claim.
Two consequences fixed along the way, both the spelling-versus-membership error
that ScalarPackSpec has now taught four times:
- Phase 2b globbed Proofs/*.olean and would have demanded artifacts this
button never builds. It now scans its manifest by membership and fails
closed on a missing one.
- The three inventory drivers were exempted from the dead-file gate and
compiled in a later phase; after a purge they were absent when Phase 2b
ran. They are now in the manifest like everything else, and three
exemptions are gone.
The sweep runner now reports RESOURCE rather than RED when it sees a
memory_exception: lean-guard's clamp is not a broken proof, and it has misled
the operator once and the author once.
Verified green: 8 full runs from completely purged trees — four check.sh, four
check-scalar.sh — zero red, zero resource. Every artifact rebuilt from
committed source. These are the first runs in this repository's history whose
verdict provably depends on nothing but the bytes in git.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-30 20:54:00 +00:00
# ── Phase 0a: build hygiene ─────────────────────────────────────────────────
# The verdict must depend on COMMITTED BYTES, never on build state left behind
# by an earlier run. An orphan .olean with no source still satisfies an import,
# and .olean is gitignored, so `git status` shows a clean tree while the
# compiler happily reads a module nobody can review.
#
# NOT RUN UNDER --audit-only, for the obvious reason: that mode exists to audit
# the artifacts a previous full run produced, and purging them would make the
# two features destroy each other. That is also why an audit-only transcript is
# not evidence — it has not had this hygiene applied.
if [ " $AUDIT_ONLY " = 0 ] ; then
echo "=== Phase 0a: build hygiene ==="
find " $HERE " -name '*.olean' -delete 2>/dev/null || true
echo " purged every .olean under verification/ — this run compiles from source"
else
echo "=== Phase 0a: SKIPPED (--audit-only keeps the artifacts it audits) ==="
fi
# Stray Lean files at the verification/ root join the build through LEAN_PATH,
# which contains $PWD. gen/ and Proofs/ are the only sanctioned locations.
STRAY = $( find " $HERE " -maxdepth 1 \( -name '*.lean' -o -name '*.olean' \) -printf '%f\n' 2>/dev/null || true )
if [ -n " $STRAY " ] ; then
echo " $STRAY " | sed 's/^/ STRAY Lean file outside gen\/ and Proofs\/: /'
echo "These join the build via LEAN_PATH and are audited by nothing."
exit 1
fi
# gen/ as a SET, not as a list of names: every .lean under gen/ must be either
# a compiled model module or an Aeneas *_Template.lean. The templates are KEPT
# here, unlike the companion SLH-DSA repo which deletes them: extract.sh directs
# the operator to diff the hand-written external models against them, so they
# are the reference for that comparison and deleting them would destroy it.
GENFAIL = 0
while read -r f; do
[ -z " $f " ] && continue
case " $f " in *_Template.lean) continue ; ; esac
b = " ${ f %.lean } "
case " ${ GEN_MODULES [*] } " in ( *" $b " *) ; ; ( *) echo " DEAD MODEL FILE: gen/ $f is in no manifest " ; GENFAIL = 1; ; esac
done < <( cd " $HERE /gen " && find . -name '*.lean' -printf '%P\n' | sort)
for m in " ${ GEN_MODULES [@] } " ; do
[ -f " $HERE /gen/ $m .lean " ] || { echo " MISSING MODEL FILE: gen/ $m .lean is in the manifest but absent " ; GENFAIL = 1; }
done
[ " $GENFAIL " = 0 ] || { echo "MODEL-SET CHECK FAILED" ; exit 1; }
echo " gen/ is exactly the manifest plus its pinned templates"
verification: bind the statements, the specifications, and the model (P1-a)
Phases 3/3b establish what each certificate RESTS ON. Neither says what it
SAYS, nor what it is ABOUT. A certificate gutted to a tautology of the same
axiom cone passes both; so does one whose reference definition has been
redefined to BE the extracted code, at which point the theorem reads
`loop = loop` and every cone is byte-identical.
Phase 3c closes that. Proofs/Audit.lean emits a canonical block holding the
policy constants, every certificate's fully-elaborated statement (pp.all, so
implicit arguments, instances and universe levels are visible), and the body
of every specification constant transitively reachable from those statements.
Its SHA-256 is pinned in check.sh and the block itself is committed as
AUDIT-MANIFEST.txt, so a mismatch is DIFFED, not merely reported. 31
certificates, 68 specification constants per repository.
Two tiers, not one. These forks have an arithmetic tier that must stay
oracle-free and an apex tier carrying this fork's hash and wire-format axioms,
and the apex boundary genuinely differs per fork (dalek 8 extra names, anza 4,
risc0 and betrusted 5). One shared constant would have widened the arithmetic
tier to accept hash oracles, which is the most valuable property these repos
have. Each auditor is generated from its own repository's policy.
Phase 0b pins the extracted model. This was not a precaution: risc0 and
betrusted were observed emitting BYTE-IDENTICAL audit-manifest digests
(6c821b8e…) while shipping demonstrably different extracted models, their
point-doubling routines differing in operation order. A statement names an
extracted function; it does not contain that function's body. Binding
statements is not binding the subject. Membership derives from the filesystem,
so a new model file fails closed.
selftest-statements.sh attacks both phases with ten cases, each asserting a
specific diagnostic: an edited model body, an unlisted model file, a widened
policy, a hand-edited committed block, a certificate dropped from the auditor
WITH the digest refreshed to match, and a gutted statement whose cone is
unchanged. It lifts the phases out of check.sh at run time, so it attacks the
shipping gate rather than a copy.
Two bugs found and fixed during that testing, both mine: Phase 3c read `$0`
after `cd "$AENEAS_LEAN"`, and $0 is the caller's relative path; and the
axgate self-test compared the tree against a pristine checkout rather than
against how it found it. A third expectation was wrong rather than the code —
widening the apex boundary is caught by the exact-cone requirement before the
digest ever runs, which is a stronger rejection, and the test now says so.
All sixteen runs green at these commits: four main buttons, four axgate
self-tests, four binding self-tests, four scalar buttons.
TRUSTED-BASE.md records what this binds and, at equal length, what it does
not: a digest binds identity, not meaning; an author can rotate the pins in
one commit and is caught by review, not by the script; and pinning the model
says nothing about whether Charon and Aeneas translated the Rust faithfully.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-28 22:38:17 +00:00
# ── Phase 0b: pin the extracted model ───────────────────────────────────────
# WHY. The certificates are stated ABOUT the extracted model in gen/. Phase 3c
# binds their statements and the specification definitions those statements are
# stated against — but a statement mentions an extracted function BY NAME, so
# editing that function's BODY changes what the theorem is about while leaving
# every statement, every cone and the audit digest byte-identical.
#
# This is not hypothetical. On 2026-07-28 the risc0 and betrusted repositories
# were observed to produce byte-identical AUDIT-MANIFEST digests despite
# shipping demonstrably different extracted models (a different operation order
# in the point-doubling routine). The statements could not tell them apart.
# Only a byte pin can.
#
# Membership is derived from the filesystem, not from a list: every .lean under
# gen/ must appear in GEN-MODEL.sha256 and vice versa, so adding a model file
# fails closed rather than passing unnoticed.
echo "=== Phase 0b: extracted-model byte pin ==="
if [ ! -s " $HERE /GEN-MODEL.sha256 " ] ; then
echo "FATAL: GEN-MODEL.sha256 is missing or empty — the extracted model is unpinned."
exit 1
fi
GEN_OBSERVED = $( cd " $HERE /gen " && find . -name '*.lean' -type f | sed 's|^\./||' | sort)
GEN_PINNED = $( awk '{print $2}' " $HERE /GEN-MODEL.sha256 " | sort)
if [ " $GEN_OBSERVED " != " $GEN_PINNED " ] ; then
echo "FATAL: the set of extracted-model files does not match GEN-MODEL.sha256."
echo " (< pinned, > present on disk)"
diff <( echo " $GEN_PINNED " ) <( echo " $GEN_OBSERVED " ) | sed 's/^/ /'
exit 1
fi
if ! ( cd " $HERE /gen " && sha256sum -c --quiet " $HERE /GEN-MODEL.sha256 " ) ; then
echo "FATAL: an extracted-model file does not match its pin. The proofs are"
echo "about a model that is no longer the one that was reviewed."
exit 1
fi
echo " $( wc -l < " $HERE /GEN-MODEL.sha256 " ) extracted-model files match their pins "
verification: pin the harness, the audit drivers and the policy files (P1-c)
Every gate this repository has was executed by scripts that nothing pinned.
Round-5 review of the companion SLH-DSA repository stubbed the compiler
wrapper alone and its button printed ALL GREEN in 3.6 seconds over
deliberately destroyed proofs; flipping two guards in the audit driver
disabled every check with the digest byte-identical. Depth of checking is
worth nothing if the thing doing the checking is unbound — and every gate
added this week made that gap more valuable to an attacker, not less.
Phase 0c requires every harness file to match HARNESS.sha256. Two design
points carry the weight:
- WHICH files must be pinned is POLICY and lives in check.sh, never in the
map being consulted. If the required set were read from the pin file,
deleting an entry would silently un-pin that file. It is instead derived
from the filesystem, so a deleted entry is a set mismatch and a build
failure. That is the exact defect SLH-DSA round-6 found, closed here by
construction.
- Membership self-derives from the executable bit: anything this script can
shell out to must be pinned, so a NEW script fails closed until someone
pins it deliberately. Load-bearing files that are not executable — the
audit driver, the committed manifests, the policy tables — cannot be
discovered that way and are listed explicitly.
lean-guard is inside the set, which finally makes the standing "lean-guard
stays hash-pinned" rule a property of the repository rather than a convention.
selftest-harness.sh replays five cases, each asserting a specific diagnostic:
an edited lean-guard, a new unpinned executable, a deleted pin entry, a
missing pin file, and a positive control. It was itself negative-tested — with
the hash comparison removed it goes red on exactly that case while cheerfully
reporting "10 harness files match their pins".
TRUSTED-BASE.md states the limit at equal length to the claim: pinning a
harness from inside that harness is circular, and an author who edits a script
and refreshes its pin in the same commit passes every phase. What the pin
changes is that the edit can no longer be SILENT — it must appear in the diff
at the commit being reviewed. A green button says "this is the apparatus that
was reviewed", never "this apparatus is trustworthy".
Also fixed, found by this sweep: both self-tests compared the working tree
against its starting state with `diff <(echo "$VAR") <(command)`, which is
asymmetric — for a clean tree the variable is empty and `echo` emits a blank
line the command does not. It reported a difference precisely when nothing was
wrong, and only surfaced once P1-a was committed and Proofs/ became clean.
Both now compare as strings.
Verified green: 20 runs across the four ed25519 repositories (four buttons,
four harness self-tests, four axiom-gate self-tests, four binding self-tests,
four scalar buttons), zero red.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-29 18:12:57 +00:00
# ── Phase 0c: harness integrity ─────────────────────────────────────────────
# WHY. Every gate in this script is executed by a script that, until now,
# nothing pinned. Round-5 review of the companion SLH-DSA repository stubbed
# the compiler wrapper alone and the button printed ALL GREEN in 3.6 seconds
# over deliberately destroyed proofs; flipping two guards in the audit driver
# disabled every check with the digest byte-identical. Depth of checking is
# worth nothing if the thing doing the checking is unbound.
#
# WHICH files must be pinned is POLICY, and policy lives here — in the root of
# trust — never inside the map being consulted. If the required set were read
# from HARNESS.sha256, deleting an entry would silently un-pin the file rather
# than failing the build.
#
# The set is SELF-DERIVING from the executable bit: anything this script can
# shell out to must be pinned, so a NEW script fails closed until someone pins
# it deliberately. Non-executable files that are nonetheless load-bearing —
# the audit driver, the committed manifests, the policy tables — cannot be
# discovered that way and are listed explicitly.
HARNESS_EXTRA = (
verification: pin the whole declaration surface (P1-b)
Phase 2b asks the kernel whether any AXIOM is declared under Proofs/. Phase 3
pins the cones of the named certificates. Between them sat every other
declaration in the corpus — around three thousand of them — and a helper lemma
quietly acquiring a hash oracle in its cone moved nothing either phase looked
at.
Phase 2c closes that. Ported from ltl-accumulator-verified, where a nine-attack
self-test proved a source-regex enumerator evadable by attributed, private,
indented and `instance` declarations and by a nested-namespace basename
collision. Reading the compiled environment sees what the kernel saw; no name
shape hides. Every constant contributes module, name, kind and full axiom cone,
and the observed set must equal inventory-allowlist.txt exactly in BOTH
directions, with a count trailer so a truncated run cannot pass as an empty
diff.
FOUR THINGS THIS BUILD GOT WRONG, each caught by a check rather than by review:
- The number of inventory drivers is a per-repo FACT, not an assumption.
dalek and anza cannot import their corpus as one environment (Proofs.Basic
and Proofs.ConstSpecs both declare CurveFieldProofs.zero_spec); risc0 and
betrusted have no Proofs.Basic at all. Determined by compiling a probe.
check.sh now DISCOVERS its drivers from the filesystem instead of naming
two, and the generator refuses to split out a module the repo lacks.
- The split let one real declaration hide behind another's entry. Keyed on
name alone, the two zero_specs produced byte-identical records, so 3022
declarations were covered by 3021 allowlist entries. Caught by the count
trailer. Every record now carries its originating module.
- The gate's success line said "single sanctioned axiom", inherited from the
accumulator's policy. This corpus permits NONE. A success message
describing a different rule is how an assertion stops meaning anything.
- selftest-axgate.sh lifted Phase 2b with a range ending at "Phase 3", so
inserting Phase 2c between them made it swallow the new phase and die on
variables only check.sh defines — surfacing as the BASELINE case failing,
a self-test blaming a gate for its own extraction bug. Both self-tests now
stop at the next phase marker whatever it is called, and refuse to run if
they capture more than one phase. The guard is the fix; the range was the
symptom.
WHAT THIS IS NOT, recorded in TRUSTED-BASE.md at the same length as the claim:
- No independent cone walker. The accumulator cross-checks collectAxioms
against a hand-written walker. Ported here it was wrong in BOTH directions
on mathlib's inductive shapes: EdPoint gave [] against the kernel's three
axioms, and once extended, ProjPoint gave three against the kernel's none.
Two implementations disagreeing both ways are a second wrong answer, not a
check. These cones rest on collectAxioms alone.
- Thirteen Proofs/Scalar* modules are inventoried by nothing — the
second-button seam, still open. Phase 2c names every uncovered module on
every run so the omission is visible rather than inferred.
selftest-inventory.sh exercises the shipping gate with six cases, each
asserting a specific diagnostic, including the one that matters: a cone
widened by one oracle while name, module and kind stay put. Negative-tested by
disabling the gate's diff, which turns two cases red including one for the
wrong reason, correctly reported as such.
Verified green: 20 runs across the four repositories (four buttons, four
harness, four inventory, four axgate, four binding self-tests), zero red. The
four check-scalar.sh greens from the preceding sweep stand: that script neither
reads the pin file nor changed.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-29 23:20:15 +00:00
AUDIT-MANIFEST.txt # the statement block Phase 3c's digest is taken over
GEN-MODEL.sha256 # the extracted-model pins Phase 0b enforces
P2-c: classify and pin the extraction boundary
Aeneas emits a *_Template.lean naming everything the extracted code needs
from outside itself — the extraction's own statement of its boundary.
extract.sh has always said, in prose, "after regenerating, diff the template
against the hand-written file". Prose is not a gate, and the diff cannot be
one: the two files legitimately differ in almost every line, holes and
Aeneas comments against real definitions and modeling policy.
MEASURING FIRST CHANGED WHAT THIS ITEM SHOULD BE. The TODO offered two
options — enforce the diff, or pin both files — and the answer turned out to
be neither. Both files were ALREADY byte-pinned by Phase 0b. And two further
things stand here: the generated Funs.lean imports the model and CALLS these
externals, so the Lean compiler enforces their TYPES wherever the extracted
code uses them; and the per-certificate exact cones catch any external that
becomes, or stops being, an assumption anything depends on.
What none of those three sees is the CLASSIFICATION: for each name the
extraction asks for, whether this repository answers with an ASSUMPTION or
with a PROOF. That is the tier-A/B claim the documents make in prose — the
curve calls and the three curve types resolve to proven definitions rather
than axioms, because gen/CurveField/Funs.lean opens `namespace
curve25519_dalek` and so defines the very names Aeneas asks for. Nothing
checked it. A regeneration that renamed one, or a model that quietly
answered one with an axiom instead, would have left the documents claiming a
proof where the repository had an assumption.
Phase 0d recomputes the classification with model-correspondence.py
(namespace-aware, so a definition inside a namespace counts under its full
name) and requires equality with the committed MODEL-CORRESPONDENCE.txt.
UNRESOLVED — the extraction asking for something nothing here provides — is
a hard failure.
dalek 43 MODEL 8 PROVEN 3 EXTRA
anza 38 MODEL 0 PROVEN 4 EXTRA (no CurveSig crate)
risc0 36 MODEL 8 PROVEN 4 EXTRA
betrusted 35 MODEL 8 PROVEN 4 EXTRA
selftest-correspondence.sh, five cases, negative-tested by disabling the
comparison. The case that matters is 2: a PROVEN external answered by an
axiom instead. No name changes anywhere, every byte pin still matches, and
it compiles, because the signature is unchanged — before Phase 0d nothing in
the button could tell.
Trap recorded for whoever extends it: case 3 first deleted the PROVEN rows,
which was VACUOUS on anza, since anza has none — it removed nothing, the
table still matched, and the case passed while testing nothing. It now
deletes the first row whatever its verdict AND asserts the file changed.
extract.sh now points at the gate instead of asking a human to look.
Certified by a full sweep: both buttons, all four forks, purged trees,
machine otherwise idle. 8/8 green.
2026-07-31 15:53:31 +00:00
MODEL-CORRESPONDENCE.txt # the extraction boundary Phase 0d recomputes
verification: pin the whole declaration surface (P1-b)
Phase 2b asks the kernel whether any AXIOM is declared under Proofs/. Phase 3
pins the cones of the named certificates. Between them sat every other
declaration in the corpus — around three thousand of them — and a helper lemma
quietly acquiring a hash oracle in its cone moved nothing either phase looked
at.
Phase 2c closes that. Ported from ltl-accumulator-verified, where a nine-attack
self-test proved a source-regex enumerator evadable by attributed, private,
indented and `instance` declarations and by a nested-namespace basename
collision. Reading the compiled environment sees what the kernel saw; no name
shape hides. Every constant contributes module, name, kind and full axiom cone,
and the observed set must equal inventory-allowlist.txt exactly in BOTH
directions, with a count trailer so a truncated run cannot pass as an empty
diff.
FOUR THINGS THIS BUILD GOT WRONG, each caught by a check rather than by review:
- The number of inventory drivers is a per-repo FACT, not an assumption.
dalek and anza cannot import their corpus as one environment (Proofs.Basic
and Proofs.ConstSpecs both declare CurveFieldProofs.zero_spec); risc0 and
betrusted have no Proofs.Basic at all. Determined by compiling a probe.
check.sh now DISCOVERS its drivers from the filesystem instead of naming
two, and the generator refuses to split out a module the repo lacks.
- The split let one real declaration hide behind another's entry. Keyed on
name alone, the two zero_specs produced byte-identical records, so 3022
declarations were covered by 3021 allowlist entries. Caught by the count
trailer. Every record now carries its originating module.
- The gate's success line said "single sanctioned axiom", inherited from the
accumulator's policy. This corpus permits NONE. A success message
describing a different rule is how an assertion stops meaning anything.
- selftest-axgate.sh lifted Phase 2b with a range ending at "Phase 3", so
inserting Phase 2c between them made it swallow the new phase and die on
variables only check.sh defines — surfacing as the BASELINE case failing,
a self-test blaming a gate for its own extraction bug. Both self-tests now
stop at the next phase marker whatever it is called, and refuse to run if
they capture more than one phase. The guard is the fix; the range was the
symptom.
WHAT THIS IS NOT, recorded in TRUSTED-BASE.md at the same length as the claim:
- No independent cone walker. The accumulator cross-checks collectAxioms
against a hand-written walker. Ported here it was wrong in BOTH directions
on mathlib's inductive shapes: EdPoint gave [] against the kernel's three
axioms, and once extended, ProjPoint gave three against the kernel's none.
Two implementations disagreeing both ways are a second wrong answer, not a
check. These cones rest on collectAxioms alone.
- Thirteen Proofs/Scalar* modules are inventoried by nothing — the
second-button seam, still open. Phase 2c names every uncovered module on
every run so the omission is visible rather than inferred.
selftest-inventory.sh exercises the shipping gate with six cases, each
asserting a specific diagnostic, including the one that matters: a cone
widened by one oracle while name, module and kind stay put. Negative-tested by
disabling the gate's diff, which turns two cases red including one for the
wrong reason, correctly reported as such.
Verified green: 20 runs across the four repositories (four buttons, four
harness, four inventory, four axgate, four binding self-tests), zero red. The
four check-scalar.sh greens from the preceding sweep stand: that script neither
reads the pin file nor changed.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-29 23:20:15 +00:00
inventory-allowlist.txt # the audit surface Phase 2c diffs against
verification: close the two-button seam and level up the scalar button (P0-b)
THE SEAM. This repository is checked by two scripts, and until now neither
asserted anything about the other's scope. check.sh's dead-file gate simply
SKIPPED anything named Scalar*, so a new Proofs/ScalarX.lean was gated by
nothing at all: absent from one manifest by exemption, from the other by
omission, compiled by neither, inventoried by neither. Each button now reads
the other's manifest and requires every shipped proof source to belong to
EXACTLY ONE of them — neither orphaned nor double-claimed, both directions,
plus a phantom check on entries naming files that do not exist. Negative-tested
four ways, including the exact hole this item names.
THE SCALAR BUTTON. Closing the seam exposed it as the estate's weakest link,
having been left behind by every hardening round while the main button gained
five phases. 45 lines to 227:
- source-integrity check over its sources;
- harness-pin verification, so running THIS button alone is protected and not
only running it after check.sh;
- a kernel-side axiom-declaration gate over the compiled artifacts, replacing
a source-text grep that is evadable four ways on v4.30.0-rc2;
- a declaration inventory of ~1880 constants against its own allowlist,
diffed both directions with a count trailer. These 13 modules were the only
part of the proof corpus with no inventory: check.sh Phase 2c named them as
uncovered on every run, and now names the button that covers them instead;
- per-certificate exact-cone assertions replacing `-eq 13` over matching
output lines. A count cannot say WHICH certificate is clean and passes just
as happily if one cone is reported twice.
Every fork-specific fact was read from the existing script rather than assumed:
risc0 and betrusted audit sub_loop1_one_spec where dalek and anza audit
cond_add_l_one_spec, untouched.
THREE BUGS, ONE ROOT CAUSE, all found by the gates rather than by review. Each
reasoned about how a thing is SPELLED instead of what it BELONGS TO, and the
corpus punished each: Proofs/ScalarPackSpec.lean is named like the scalar layer
and owned by the main button.
- the scalar dead-file gate globbed Scalar* and demanded ScalarPackSpec be
scalar-owned. REMOVED rather than special-cased: the seam check tests
membership in exactly one manifest, which is strictly stronger than any
prefix;
- the scalar axiom gate scanned Scalar*.olean, reporting "14 modules" for a
13-module manifest. On a tree where check.sh had not run that artifact is
absent and the button would have failed for a false reason. It now scans
the manifest by membership and fails closed on a missing artifact;
- Phase 2c's driver discovery globbed Inventory*.lean and claimed the other
button's driver, then correctly complained its own manifest lacked those
modules.
This is the family the campaign began with: a source-text axiom grep reasoning
about spelling. Recorded in TRUSTED-BASE.md because it generalises.
Also fixed: the first negative test of the scalar gate's absence check passed
for the wrong reason — the button recompiles before the gate runs, so removing
an artifact merely caused it to be rebuilt. Retested against the lifted phase,
where absence is a persistent condition.
Verified green: 24 runs across the four repositories — four main buttons, four
scalar buttons, and sixteen self-tests — zero red.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-30 10:30:26 +00:00
inventory-allowlist-scalar.txt # the scalar layer's audit surface (second button)
verification: pin the whole declaration surface (P1-b)
Phase 2b asks the kernel whether any AXIOM is declared under Proofs/. Phase 3
pins the cones of the named certificates. Between them sat every other
declaration in the corpus — around three thousand of them — and a helper lemma
quietly acquiring a hash oracle in its cone moved nothing either phase looked
at.
Phase 2c closes that. Ported from ltl-accumulator-verified, where a nine-attack
self-test proved a source-regex enumerator evadable by attributed, private,
indented and `instance` declarations and by a nested-namespace basename
collision. Reading the compiled environment sees what the kernel saw; no name
shape hides. Every constant contributes module, name, kind and full axiom cone,
and the observed set must equal inventory-allowlist.txt exactly in BOTH
directions, with a count trailer so a truncated run cannot pass as an empty
diff.
FOUR THINGS THIS BUILD GOT WRONG, each caught by a check rather than by review:
- The number of inventory drivers is a per-repo FACT, not an assumption.
dalek and anza cannot import their corpus as one environment (Proofs.Basic
and Proofs.ConstSpecs both declare CurveFieldProofs.zero_spec); risc0 and
betrusted have no Proofs.Basic at all. Determined by compiling a probe.
check.sh now DISCOVERS its drivers from the filesystem instead of naming
two, and the generator refuses to split out a module the repo lacks.
- The split let one real declaration hide behind another's entry. Keyed on
name alone, the two zero_specs produced byte-identical records, so 3022
declarations were covered by 3021 allowlist entries. Caught by the count
trailer. Every record now carries its originating module.
- The gate's success line said "single sanctioned axiom", inherited from the
accumulator's policy. This corpus permits NONE. A success message
describing a different rule is how an assertion stops meaning anything.
- selftest-axgate.sh lifted Phase 2b with a range ending at "Phase 3", so
inserting Phase 2c between them made it swallow the new phase and die on
variables only check.sh defines — surfacing as the BASELINE case failing,
a self-test blaming a gate for its own extraction bug. Both self-tests now
stop at the next phase marker whatever it is called, and refuse to run if
they capture more than one phase. The guard is the fix; the range was the
symptom.
WHAT THIS IS NOT, recorded in TRUSTED-BASE.md at the same length as the claim:
- No independent cone walker. The accumulator cross-checks collectAxioms
against a hand-written walker. Ported here it was wrong in BOTH directions
on mathlib's inductive shapes: EdPoint gave [] against the kernel's three
axioms, and once extended, ProjPoint gave three against the kernel's none.
Two implementations disagreeing both ways are a second wrong answer, not a
check. These cones rest on collectAxioms alone.
- Thirteen Proofs/Scalar* modules are inventoried by nothing — the
second-button seam, still open. Phase 2c names every uncovered module on
every run so the omission is visible rather than inferred.
selftest-inventory.sh exercises the shipping gate with six cases, each
asserting a specific diagnostic, including the one that matters: a cone
widened by one oracle while name, module and kind stay put. Negative-tested by
disabling the gate's diff, which turns two cases red including one for the
wrong reason, correctly reported as such.
Verified green: 20 runs across the four repositories (four buttons, four
harness, four inventory, four axgate, four binding self-tests), zero red. The
four check-scalar.sh greens from the preceding sweep stand: that script neither
reads the pin file nor changed.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-29 23:20:15 +00:00
Proofs/Audit.lean # the audit driver: it computes the digest it is judged by
audit: bind the scalar statements, and make the accounting identity mean audit
Closes four round-7/8 findings. Certified by the round-12 sweep: five
repositories, both buttons and every self-test, 48/48 GREEN.
── `scalar-statements-unbound` (gpt, round 7, CRITICAL) ────────────────────
The main button bound its 31 certificates' elaborated statements and reachable
specification bodies. This button bound NONE of its thirteen, while
TRUSTED-BASE item 8 said the audit covers "every certificate" — false across
the 44-certificate surface. The finding was raised in round 7, lost from the
round-8 work list by an F-number collision between two reviewers, and re-raised
in round 8.
Proofs/ScalarAudit.lean is generated from each fork's OWN Audit.lean, so the
canonicalisation is provably the same code: pp.all rendering, whitespace
normalisation, transitive specification closure. check-scalar.sh Phase 3c pins
the block's digest, requires the committed copy to match byte-for-byte so a
mismatch can be DIFFED, and cross-checks the auditor's certificate set against
the button's CERTS array.
dalek ecf3a3f8 · anza 0d942e47 · risc0 4b550a61 · betrusted 4b550a61
risc0 and betrusted share a digest and that is correct, not a collision: their
ScalarSubSpec.lean differs only in doc prose and in `black_box` entries inside
`simp only [...]` lists AFTER `:= by`. Proof scripts. They bind the same
statements over the same specifications, which is the documented scope.
selftest-scalar-statements.sh ships the two attacks the reviewer asked for:
ok gutted statement caught (cone unchanged)
ok rewritten specification body caught (name and cone unchanged)
The second rewrites a reachable reference body to `id (…)` — DEFINITIONALLY
EQUAL, so the corpus compiles and every proof typechecks and the cone is
byte-identical. Every earlier phase is blind to it.
── `drv-surface-no-cones` + `accounting-certifies-enumeration` (claude) ────
The round-7 accounting identity proved every kernel constant was ENUMERATED.
The reviewer showed enumeration is not audit: their planted claim WAS
enumerated, as DRV|LTLAccAudit.bait.smuggled|theorem with a real cone, and
nothing examined it — rows had no cone, no allowlist covered them, the
statement digest does not reach instruments, and Phase 2b gates DECLARED
AXIOMS, a different question. "Progress of one step, not two."
DRV rows now carry their axiom cone and are pinned in driver-allowlist.txt by
inventory_gate.sh with a DRV tag — the same implementation that pins the
corpus, in both directions, because a second copy of a coverage gate is a
second thing to drift. The axiom policy is per-surface and enforced per
surface: the corpus admits exactly the sanctioned boundary, the instruments
admit none, and an instrument axiom fails EVEN WHEN ALLOWLISTED.
Verified with the reviewer's own payload, both placements:
before the walk -> UNCLASSIFIED: DRV|…|bait.smuggled|theorem|Classical.choice,Quot.sound,propext
after the walk -> ACCOUNTING FAILED names it (kernel-side)
── `drv-naming-heuristic` (claude, round 7) ────────────────────────────────
Retired as load-bearing rather than patched. The rule admits a theorem whose
name extends a constant declared alongside it, and "breaks in one line" —
declare `def bait`, then `theorem bait.smuggled` walks through. It stays as a
fast readable first check; membership in a committed allowlist is what now
carries the weight, and a new row fails closed whatever it is called.
── what round 11 caught, which was mine ───────────────────────────────────
DRV rows first shipped WITHOUT their originating driver. dalek and anza run
two drivers, each declaring its own `corpus`; keyed on name alone those two
distinct declarations produced one byte-identical row, `sort -u` collapsed
them, and the trailers summed to 37 against 36. The estate had already learned
this on the corpus walk — INV rows carry their module because two modules both
declare CurveFieldProofs.zero_spec — and I rebuilt the record without it.
Rows now carry their driver, and the gate FAILS CLOSED ON DUPLICATE RECORDS
naming the collision: two declarations sharing one entry means one is covered
by the other's, which is exactly how a real declaration hides. The trailer
now checks what the drivers EMITTED, not what survives de-duplication —
conflating "the run was truncated" with "two rows were identical" is what let
a record-format defect present itself as an arithmetic complaint.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-03 10:15:26 +00:00
driver-allowlist.txt # the INSTRUMENTS' own declaration surface, with cones.
# Not executable, so it would otherwise sit outside the
# harness set — and an allowlist an attacker may rewrite
# pins nothing.
Proofs/ScalarAudit.lean # the scalar audit driver, likewise
SCALAR-AUDIT-MANIFEST.txt # the block the scalar digest is taken over, committed
# so a mismatch can be DIFFED and not merely reported
verification: pin the whole declaration surface (P1-b)
Phase 2b asks the kernel whether any AXIOM is declared under Proofs/. Phase 3
pins the cones of the named certificates. Between them sat every other
declaration in the corpus — around three thousand of them — and a helper lemma
quietly acquiring a hash oracle in its cone moved nothing either phase looked
at.
Phase 2c closes that. Ported from ltl-accumulator-verified, where a nine-attack
self-test proved a source-regex enumerator evadable by attributed, private,
indented and `instance` declarations and by a nested-namespace basename
collision. Reading the compiled environment sees what the kernel saw; no name
shape hides. Every constant contributes module, name, kind and full axiom cone,
and the observed set must equal inventory-allowlist.txt exactly in BOTH
directions, with a count trailer so a truncated run cannot pass as an empty
diff.
FOUR THINGS THIS BUILD GOT WRONG, each caught by a check rather than by review:
- The number of inventory drivers is a per-repo FACT, not an assumption.
dalek and anza cannot import their corpus as one environment (Proofs.Basic
and Proofs.ConstSpecs both declare CurveFieldProofs.zero_spec); risc0 and
betrusted have no Proofs.Basic at all. Determined by compiling a probe.
check.sh now DISCOVERS its drivers from the filesystem instead of naming
two, and the generator refuses to split out a module the repo lacks.
- The split let one real declaration hide behind another's entry. Keyed on
name alone, the two zero_specs produced byte-identical records, so 3022
declarations were covered by 3021 allowlist entries. Caught by the count
trailer. Every record now carries its originating module.
- The gate's success line said "single sanctioned axiom", inherited from the
accumulator's policy. This corpus permits NONE. A success message
describing a different rule is how an assertion stops meaning anything.
- selftest-axgate.sh lifted Phase 2b with a range ending at "Phase 3", so
inserting Phase 2c between them made it swallow the new phase and die on
variables only check.sh defines — surfacing as the BASELINE case failing,
a self-test blaming a gate for its own extraction bug. Both self-tests now
stop at the next phase marker whatever it is called, and refuse to run if
they capture more than one phase. The guard is the fix; the range was the
symptom.
WHAT THIS IS NOT, recorded in TRUSTED-BASE.md at the same length as the claim:
- No independent cone walker. The accumulator cross-checks collectAxioms
against a hand-written walker. Ported here it was wrong in BOTH directions
on mathlib's inductive shapes: EdPoint gave [] against the kernel's three
axioms, and once extended, ProjPoint gave three against the kernel's none.
Two implementations disagreeing both ways are a second wrong answer, not a
check. These cones rest on collectAxioms alone.
- Thirteen Proofs/Scalar* modules are inventoried by nothing — the
second-button seam, still open. Phase 2c names every uncovered module on
every run so the omission is visible rather than inferred.
selftest-inventory.sh exercises the shipping gate with six cases, each
asserting a specific diagnostic, including the one that matters: a cone
widened by one oracle while name, module and kind stay put. Negative-tested by
disabling the gate's diff, which turns two cases red including one for the
wrong reason, correctly reported as such.
Verified green: 20 runs across the four repositories (four buttons, four
harness, four inventory, four axgate, four binding self-tests), zero red. The
four check-scalar.sh greens from the preceding sweep stand: that script neither
reads the pin file nor changed.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-29 23:20:15 +00:00
Proofs/InventoryCore.lean # inventory machinery
verification: close the two-button seam and level up the scalar button (P0-b)
THE SEAM. This repository is checked by two scripts, and until now neither
asserted anything about the other's scope. check.sh's dead-file gate simply
SKIPPED anything named Scalar*, so a new Proofs/ScalarX.lean was gated by
nothing at all: absent from one manifest by exemption, from the other by
omission, compiled by neither, inventoried by neither. Each button now reads
the other's manifest and requires every shipped proof source to belong to
EXACTLY ONE of them — neither orphaned nor double-claimed, both directions,
plus a phantom check on entries naming files that do not exist. Negative-tested
four ways, including the exact hole this item names.
THE SCALAR BUTTON. Closing the seam exposed it as the estate's weakest link,
having been left behind by every hardening round while the main button gained
five phases. 45 lines to 227:
- source-integrity check over its sources;
- harness-pin verification, so running THIS button alone is protected and not
only running it after check.sh;
- a kernel-side axiom-declaration gate over the compiled artifacts, replacing
a source-text grep that is evadable four ways on v4.30.0-rc2;
- a declaration inventory of ~1880 constants against its own allowlist,
diffed both directions with a count trailer. These 13 modules were the only
part of the proof corpus with no inventory: check.sh Phase 2c named them as
uncovered on every run, and now names the button that covers them instead;
- per-certificate exact-cone assertions replacing `-eq 13` over matching
output lines. A count cannot say WHICH certificate is clean and passes just
as happily if one cone is reported twice.
Every fork-specific fact was read from the existing script rather than assumed:
risc0 and betrusted audit sub_loop1_one_spec where dalek and anza audit
cond_add_l_one_spec, untouched.
THREE BUGS, ONE ROOT CAUSE, all found by the gates rather than by review. Each
reasoned about how a thing is SPELLED instead of what it BELONGS TO, and the
corpus punished each: Proofs/ScalarPackSpec.lean is named like the scalar layer
and owned by the main button.
- the scalar dead-file gate globbed Scalar* and demanded ScalarPackSpec be
scalar-owned. REMOVED rather than special-cased: the seam check tests
membership in exactly one manifest, which is strictly stronger than any
prefix;
- the scalar axiom gate scanned Scalar*.olean, reporting "14 modules" for a
13-module manifest. On a tree where check.sh had not run that artifact is
absent and the button would have failed for a false reason. It now scans
the manifest by membership and fails closed on a missing artifact;
- Phase 2c's driver discovery globbed Inventory*.lean and claimed the other
button's driver, then correctly complained its own manifest lacked those
modules.
This is the family the campaign began with: a source-text axiom grep reasoning
about spelling. Recorded in TRUSTED-BASE.md because it generalises.
Also fixed: the first negative test of the scalar gate's absence check passed
for the wrong reason — the button recompiles before the gate runs, so removing
an artifact merely caused it to be rebuilt. Retested against the lifted phase,
where absence is a persistent condition.
Verified green: 24 runs across the four repositories — four main buttons, four
scalar buttons, and sixteen self-tests — zero red.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-30 10:30:26 +00:00
Proofs/InventoryScalar.lean # inventory driver: the scalar layer
verification: pin the whole declaration surface (P1-b)
Phase 2b asks the kernel whether any AXIOM is declared under Proofs/. Phase 3
pins the cones of the named certificates. Between them sat every other
declaration in the corpus — around three thousand of them — and a helper lemma
quietly acquiring a hash oracle in its cone moved nothing either phase looked
at.
Phase 2c closes that. Ported from ltl-accumulator-verified, where a nine-attack
self-test proved a source-regex enumerator evadable by attributed, private,
indented and `instance` declarations and by a nested-namespace basename
collision. Reading the compiled environment sees what the kernel saw; no name
shape hides. Every constant contributes module, name, kind and full axiom cone,
and the observed set must equal inventory-allowlist.txt exactly in BOTH
directions, with a count trailer so a truncated run cannot pass as an empty
diff.
FOUR THINGS THIS BUILD GOT WRONG, each caught by a check rather than by review:
- The number of inventory drivers is a per-repo FACT, not an assumption.
dalek and anza cannot import their corpus as one environment (Proofs.Basic
and Proofs.ConstSpecs both declare CurveFieldProofs.zero_spec); risc0 and
betrusted have no Proofs.Basic at all. Determined by compiling a probe.
check.sh now DISCOVERS its drivers from the filesystem instead of naming
two, and the generator refuses to split out a module the repo lacks.
- The split let one real declaration hide behind another's entry. Keyed on
name alone, the two zero_specs produced byte-identical records, so 3022
declarations were covered by 3021 allowlist entries. Caught by the count
trailer. Every record now carries its originating module.
- The gate's success line said "single sanctioned axiom", inherited from the
accumulator's policy. This corpus permits NONE. A success message
describing a different rule is how an assertion stops meaning anything.
- selftest-axgate.sh lifted Phase 2b with a range ending at "Phase 3", so
inserting Phase 2c between them made it swallow the new phase and die on
variables only check.sh defines — surfacing as the BASELINE case failing,
a self-test blaming a gate for its own extraction bug. Both self-tests now
stop at the next phase marker whatever it is called, and refuse to run if
they capture more than one phase. The guard is the fix; the range was the
symptom.
WHAT THIS IS NOT, recorded in TRUSTED-BASE.md at the same length as the claim:
- No independent cone walker. The accumulator cross-checks collectAxioms
against a hand-written walker. Ported here it was wrong in BOTH directions
on mathlib's inductive shapes: EdPoint gave [] against the kernel's three
axioms, and once extended, ProjPoint gave three against the kernel's none.
Two implementations disagreeing both ways are a second wrong answer, not a
check. These cones rest on collectAxioms alone.
- Thirteen Proofs/Scalar* modules are inventoried by nothing — the
second-button seam, still open. Phase 2c names every uncovered module on
every run so the omission is visible rather than inferred.
selftest-inventory.sh exercises the shipping gate with six cases, each
asserting a specific diagnostic, including the one that matters: a cone
widened by one oracle while name, module and kind stay put. Negative-tested by
disabling the gate's diff, which turns two cases red including one for the
wrong reason, correctly reported as such.
Verified green: 20 runs across the four repositories (four buttons, four
harness, four inventory, four axgate, four binding self-tests), zero red. The
four check-scalar.sh greens from the preceding sweep stand: that script neither
reads the pin file nor changed.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-29 23:20:15 +00:00
Proofs/Inventory.lean # inventory driver: main chain
Proofs/InventoryBasic.lean # inventory driver: Proofs.Basic
verification: pin the harness, the audit drivers and the policy files (P1-c)
Every gate this repository has was executed by scripts that nothing pinned.
Round-5 review of the companion SLH-DSA repository stubbed the compiler
wrapper alone and its button printed ALL GREEN in 3.6 seconds over
deliberately destroyed proofs; flipping two guards in the audit driver
disabled every check with the digest byte-identical. Depth of checking is
worth nothing if the thing doing the checking is unbound — and every gate
added this week made that gap more valuable to an attacker, not less.
Phase 0c requires every harness file to match HARNESS.sha256. Two design
points carry the weight:
- WHICH files must be pinned is POLICY and lives in check.sh, never in the
map being consulted. If the required set were read from the pin file,
deleting an entry would silently un-pin that file. It is instead derived
from the filesystem, so a deleted entry is a set mismatch and a build
failure. That is the exact defect SLH-DSA round-6 found, closed here by
construction.
- Membership self-derives from the executable bit: anything this script can
shell out to must be pinned, so a NEW script fails closed until someone
pins it deliberately. Load-bearing files that are not executable — the
audit driver, the committed manifests, the policy tables — cannot be
discovered that way and are listed explicitly.
lean-guard is inside the set, which finally makes the standing "lean-guard
stays hash-pinned" rule a property of the repository rather than a convention.
selftest-harness.sh replays five cases, each asserting a specific diagnostic:
an edited lean-guard, a new unpinned executable, a deleted pin entry, a
missing pin file, and a positive control. It was itself negative-tested — with
the hash comparison removed it goes red on exactly that case while cheerfully
reporting "10 harness files match their pins".
TRUSTED-BASE.md states the limit at equal length to the claim: pinning a
harness from inside that harness is circular, and an author who edits a script
and refreshes its pin in the same commit passes every phase. What the pin
changes is that the edit can no longer be SILENT — it must appear in the diff
at the commit being reviewed. A green button says "this is the apparatus that
was reviewed", never "this apparatus is trustworthy".
Also fixed, found by this sweep: both self-tests compared the working tree
against its starting state with `diff <(echo "$VAR") <(command)`, which is
asymmetric — for a clean tree the variable is empty and `echo` emits a blank
line the command does not. It reported a difference precisely when nothing was
wrong, and only surfaced once P1-a was committed and Proofs/ became clean.
Both now compare as strings.
Verified green: 20 runs across the four ed25519 repositories (four buttons,
four harness self-tests, four axiom-gate self-tests, four binding self-tests,
four scalar buttons), zero red.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-29 18:12:57 +00:00
)
echo "=== Phase 0c: harness integrity ==="
if [ ! -s " $HERE /HARNESS.sha256 " ] ; then
echo "FATAL: HARNESS.sha256 is missing or empty — the harness is unpinned."
exit 1
fi
# NOTE ON check.sh ITSELF: it is pinned like everything else. That catches
# drift and accident. It does NOT stop an author who edits this script and
# refreshes its pin in the same commit — nothing executed by the harness can.
# The defence there is that both changes appear in the diff at the pinned
# commit, which is why TRUSTED-BASE.md says the consumer's check is review.
HARNESS_REQUIRED = $( { find " $HERE " -type f -executable -not -path '*/.git/*' -printf '%P\n'
printf '%s\n' " ${ HARNESS_EXTRA [@] } " ; } | sort -u )
HARNESS_PINNED = $( awk '{print $2}' " $HERE /HARNESS.sha256 " | sort -u)
if [ " $HARNESS_REQUIRED " != " $HARNESS_PINNED " ] ; then
echo "FATAL: the set of harness files does not match HARNESS.sha256."
echo " (< pinned, > present and requiring a pin)"
diff <( echo " $HARNESS_PINNED " ) <( echo " $HARNESS_REQUIRED " ) | sed 's/^/ /'
exit 1
fi
if ! ( cd " $HERE " && sha256sum -c --quiet HARNESS.sha256 ) ; then
echo "FATAL: a harness file does not match its pin. The button you are"
echo "running is not the button that was reviewed."
exit 1
fi
echo " $( wc -l < " $HERE /HARNESS.sha256 " ) harness files match their pins "
P2-c: classify and pin the extraction boundary
Aeneas emits a *_Template.lean naming everything the extracted code needs
from outside itself — the extraction's own statement of its boundary.
extract.sh has always said, in prose, "after regenerating, diff the template
against the hand-written file". Prose is not a gate, and the diff cannot be
one: the two files legitimately differ in almost every line, holes and
Aeneas comments against real definitions and modeling policy.
MEASURING FIRST CHANGED WHAT THIS ITEM SHOULD BE. The TODO offered two
options — enforce the diff, or pin both files — and the answer turned out to
be neither. Both files were ALREADY byte-pinned by Phase 0b. And two further
things stand here: the generated Funs.lean imports the model and CALLS these
externals, so the Lean compiler enforces their TYPES wherever the extracted
code uses them; and the per-certificate exact cones catch any external that
becomes, or stops being, an assumption anything depends on.
What none of those three sees is the CLASSIFICATION: for each name the
extraction asks for, whether this repository answers with an ASSUMPTION or
with a PROOF. That is the tier-A/B claim the documents make in prose — the
curve calls and the three curve types resolve to proven definitions rather
than axioms, because gen/CurveField/Funs.lean opens `namespace
curve25519_dalek` and so defines the very names Aeneas asks for. Nothing
checked it. A regeneration that renamed one, or a model that quietly
answered one with an axiom instead, would have left the documents claiming a
proof where the repository had an assumption.
Phase 0d recomputes the classification with model-correspondence.py
(namespace-aware, so a definition inside a namespace counts under its full
name) and requires equality with the committed MODEL-CORRESPONDENCE.txt.
UNRESOLVED — the extraction asking for something nothing here provides — is
a hard failure.
dalek 43 MODEL 8 PROVEN 3 EXTRA
anza 38 MODEL 0 PROVEN 4 EXTRA (no CurveSig crate)
risc0 36 MODEL 8 PROVEN 4 EXTRA
betrusted 35 MODEL 8 PROVEN 4 EXTRA
selftest-correspondence.sh, five cases, negative-tested by disabling the
comparison. The case that matters is 2: a PROVEN external answered by an
axiom instead. No name changes anywhere, every byte pin still matches, and
it compiles, because the signature is unchanged — before Phase 0d nothing in
the button could tell.
Trap recorded for whoever extends it: case 3 first deleted the PROVEN rows,
which was VACUOUS on anza, since anza has none — it removed nothing, the
table still matched, and the case passed while testing nothing. It now
deletes the first row whatever its verdict AND asserts the file changed.
extract.sh now points at the gate instead of asking a human to look.
Certified by a full sweep: both buttons, all four forks, purged trees,
machine otherwise idle. 8/8 green.
2026-07-31 15:53:31 +00:00
# ── Phase 0d: template/model correspondence ─────────────────────────────────
# WHAT AENEAS'S TEMPLATE IS. When Aeneas extracts the Rust it also emits, for
# each crate, a *_Template.lean naming everything the extracted code needs from
# OUTSIDE itself. That template is the extraction's own statement of its
# boundary. The hand-written *External.lean beside it is our answer to that
# statement, and `extract.sh` has always said, in prose, "after regenerating,
# diff the template against the hand-written file". Prose is not a gate.
#
# WHAT THIS ADDS, given that three other things already stand here. Phase 0b
# byte-pins both files, so neither can drift from its pin unnoticed. The
# generated Funs.lean imports the model and CALLS these externals, so the Lean
# compiler already enforces their types wherever the extracted code uses them.
# The per-certificate exact cones catch any external that becomes — or stops
# being — an assumption anything depends on. What none of those three sees is
# the CLASSIFICATION: for each name the extraction asks for, whether this
# repository answers with an assumption or with a proof.
#
# That distinction is the tier-A/B claim, and it was prose until 2026-07-31.
# The docs say the curve calls (compress, as_bytes,
# vartime_double_scalar_mul_basepoint, from_bytes_mod_order{,_wide}) and the
# three curve TYPES resolve to the PROVEN model's own definitions rather than
# to axioms — because gen/CurveField/Funs.lean opens `namespace
# curve25519_dalek`, so the names Aeneas asks for are the names it defines.
# Nothing checked it. A regeneration that renamed one of those, or a model that
# quietly answered one with an axiom instead, would have left the documents
# claiming a proof where the repository now had an assumption.
#
# model-correspondence.py recomputes the classification from the files —
# namespace-aware, so a definition inside `namespace curve25519_dalek` counts
# under its full name — and the result must equal the committed table exactly.
# UNRESOLVED is a hard failure in the tool itself: the extraction asking for
# something this repository does not provide at all.
echo "=== Phase 0d: template/model correspondence ==="
CORR_FILE = " $HERE /MODEL-CORRESPONDENCE.txt "
if [ ! -s " $CORR_FILE " ] ; then
echo "FATAL: MODEL-CORRESPONDENCE.txt is missing or empty — the extraction boundary is unpinned."
exit 1
fi
CORR_OBSERVED = $( cd " $HERE " && python3 model-correspondence.py .) || {
echo " $CORR_OBSERVED " | grep UNRESOLVED | sed 's/^/ /'
echo "MODEL CORRESPONDENCE FAILED: the extraction declares an external that neither"
echo "the hand-written model nor the proven corpus provides."
exit 1
}
if ! diff -u " $CORR_FILE " <( printf '%s\n' " $CORR_OBSERVED " ) > /tmp/corr-diff.$$ 2>& 1; then
echo " MODEL CORRESPONDENCE DRIFT (< committed, > observed):"
sed -n '4,24p' /tmp/corr-diff.$$ | sed 's/^/ /'
rm -f /tmp/corr-diff.$$
echo "MODEL CORRESPONDENCE FAILED: an external changed how it is answered."
exit 1
fi
rm -f /tmp/corr-diff.$$
echo " $( grep -c '|MODEL$' " $CORR_FILE " ) externals answered by the hand-written model (assumptions) "
echo " $( grep -c '|PROVEN$' " $CORR_FILE " ) answered by PROVEN definitions in the extracted corpus "
echo " $( grep -c '|EXTRA$' " $CORR_FILE " ) model declarations beyond what the extraction asks for "
echo ""
2026-07-02 12:17:44 +00:00
# ── Phase 1: stub + axiom-smuggling audit ───────────────────────────────────
echo "=== Phase 1: stub audit ==="
if grep -rn 'by trivial' " $HERE " /Proofs/*Spec*.lean 2>/dev/null; then
echo "STUB DETECTED: 'by trivial' in spec files" ; exit 1; fi
if grep -rn ' : True :=' " $HERE " /Proofs/*.lean 2>/dev/null; then
echo "STUB DETECTED: True-target theorem" ; exit 1; fi
if grep -rnE '^(private |protected |noncomputable )*axiom ' " $HERE " /Proofs/*.lean 2>/dev/null; then
echo "AXIOM SMUGGLING DETECTED: axiom declaration under Proofs/ — forbidden."
echo "External models belong in gen/*/FunsExternal.lean and must stay outside"
echo "every certificate's dependency cone (Phase 3 verifies that)."
exit 1
fi
echo " clean: no trivial stubs, no True targets, no axioms outside gen/"
verification: close the two-button seam and level up the scalar button (P0-b)
THE SEAM. This repository is checked by two scripts, and until now neither
asserted anything about the other's scope. check.sh's dead-file gate simply
SKIPPED anything named Scalar*, so a new Proofs/ScalarX.lean was gated by
nothing at all: absent from one manifest by exemption, from the other by
omission, compiled by neither, inventoried by neither. Each button now reads
the other's manifest and requires every shipped proof source to belong to
EXACTLY ONE of them — neither orphaned nor double-claimed, both directions,
plus a phantom check on entries naming files that do not exist. Negative-tested
four ways, including the exact hole this item names.
THE SCALAR BUTTON. Closing the seam exposed it as the estate's weakest link,
having been left behind by every hardening round while the main button gained
five phases. 45 lines to 227:
- source-integrity check over its sources;
- harness-pin verification, so running THIS button alone is protected and not
only running it after check.sh;
- a kernel-side axiom-declaration gate over the compiled artifacts, replacing
a source-text grep that is evadable four ways on v4.30.0-rc2;
- a declaration inventory of ~1880 constants against its own allowlist,
diffed both directions with a count trailer. These 13 modules were the only
part of the proof corpus with no inventory: check.sh Phase 2c named them as
uncovered on every run, and now names the button that covers them instead;
- per-certificate exact-cone assertions replacing `-eq 13` over matching
output lines. A count cannot say WHICH certificate is clean and passes just
as happily if one cone is reported twice.
Every fork-specific fact was read from the existing script rather than assumed:
risc0 and betrusted audit sub_loop1_one_spec where dalek and anza audit
cond_add_l_one_spec, untouched.
THREE BUGS, ONE ROOT CAUSE, all found by the gates rather than by review. Each
reasoned about how a thing is SPELLED instead of what it BELONGS TO, and the
corpus punished each: Proofs/ScalarPackSpec.lean is named like the scalar layer
and owned by the main button.
- the scalar dead-file gate globbed Scalar* and demanded ScalarPackSpec be
scalar-owned. REMOVED rather than special-cased: the seam check tests
membership in exactly one manifest, which is strictly stronger than any
prefix;
- the scalar axiom gate scanned Scalar*.olean, reporting "14 modules" for a
13-module manifest. On a tree where check.sh had not run that artifact is
absent and the button would have failed for a false reason. It now scans
the manifest by membership and fails closed on a missing artifact;
- Phase 2c's driver discovery globbed Inventory*.lean and claimed the other
button's driver, then correctly complained its own manifest lacked those
modules.
This is the family the campaign began with: a source-text axiom grep reasoning
about spelling. Recorded in TRUSTED-BASE.md because it generalises.
Also fixed: the first negative test of the scalar gate's absence check passed
for the wrong reason — the button recompiles before the gate runs, so removing
an artifact merely caused it to be rebuilt. Retested against the lifted phase,
where absence is a persistent condition.
Verified green: 24 runs across the four repositories — four main buttons, four
scalar buttons, and sixteen self-tests — zero red.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-30 10:30:26 +00:00
# ── Phase 1b: the two-button seam ───────────────────────────────────────────
# WHY. This repository is checked by TWO buttons: this script covers the field,
# curve and signature layers, and check-scalar.sh covers the scalar layer.
# Until 2026-07-30 neither asserted anything about the other's scope, and this
# script's dead-file gate simply SKIPPED anything named Scalar*. A new
# Proofs/ScalarX.lean was therefore gated by nothing at all: absent from this
# manifest by exemption, absent from the other by omission, compiled by
# neither, inventoried by neither.
#
# The fix is mutual: each button reads the OTHER's manifest and asserts that
# every shipped proof source belongs to exactly one of them. Both directions,
# so a file can neither fall between the two nor be claimed by both.
echo "=== Phase 1b: two-button seam ==="
SEAMFAIL = 0
SCALAR_SH = " $HERE /check-scalar.sh "
if [ ! -f " $SCALAR_SH " ] ; then
echo " FATAL: check-scalar.sh is absent — half the corpus would go unchecked."
exit 1
fi
SCALAR_MANIFEST = $( grep -m1 '^PROOFS=(' " $SCALAR_SH " | sed 's/^PROOFS=(//; s/).*$//' | tr ' ' '\n' | sed '/^$/d' | sort -u)
if [ -z " $SCALAR_MANIFEST " ] ; then
echo " FATAL: could not read check-scalar.sh's manifest; refusing to guess its scope."
exit 1
fi
MAIN_MANIFEST = $( printf '%s\n' " ${ PROOFS [@] } " | sort -u)
# 1. Every shipped proof source belongs to exactly one manifest.
for f in " $HERE " /Proofs/*.lean; do
b = $( basename " $f " .lean)
case " $b " in AxiomCheck| Inventory| InventoryBasic| InventoryCore| InventoryScalar) continue ; ; esac
inm = 0; ins = 0
grep -qx " $b " <<< " $MAIN_MANIFEST " && inm = 1
grep -qx " $b " <<< " $SCALAR_MANIFEST " && ins = 1
if [ $(( inm + ins)) -eq 0 ] ; then
echo " ORPHAN: Proofs/ $b .lean is in NEITHER manifest — compiled and audited by no button " ; SEAMFAIL = 1
elif [ $(( inm + ins)) -eq 2 ] ; then
echo " DOUBLE-CLAIMED: Proofs/ $b .lean is in BOTH manifests — the buttons disagree about scope " ; SEAMFAIL = 1
fi
done
# 2. Neither manifest may name a file that does not exist.
while read -r m; do
[ -z " $m " ] && continue
[ -f " $HERE /Proofs/ $m .lean " ] || { echo " PHANTOM: check-scalar.sh lists $m , which does not exist " ; SEAMFAIL = 1; }
done <<< " $SCALAR_MANIFEST "
verification: build hygiene, and the hidden dependency it exposed (P0-a)
Phase 0a purges every .olean before compiling, bans stray Lean files at the
verification root (LEAN_PATH contains $PWD, so they join the build unaudited),
and requires gen/ to be exactly the model manifest plus its pinned templates.
The templates are KEPT, unlike SLH-DSA which deletes them: extract.sh directs
the operator to diff the hand-written external models against them, so they are
the reference for that comparison and P2-c will enforce it.
The purge is skipped under --audit-only, which exists to audit the artifacts a
previous full run produced. Those two features would otherwise destroy each
other, and it is a further reason an audit-only transcript is not evidence: it
has not had this hygiene applied.
WHAT THE PURGE EXPOSED, and it is the point of the whole item:
This button had never compiled the corpus from nothing. The signature apex
rests on scalar arithmetic — PointLiftSpec -> ScalarPackSpec ->
ScalarFromBytesSpec, and SigApexSpec -> ScalarDenote — and TWELVE of the scalar
layer's thirteen modules are transitive prerequisites of this manifest. They
were never compiled here. The button worked because check-scalar.sh had run at
some earlier point and left its .olean files behind. .olean is gitignored, so
no git status could ever have shown that the verdict rested on untracked
artifacts produced by a different script.
Nothing about the proofs was wrong. The evidence was resting on something
invisible, for the entire life of these repositories, and it surfaced the
moment something finally cleaned up before verifying.
Those twelve are now compiled here as PREREQ — BORROWED, NOT OWNED.
check-scalar.sh still audits them; Phase 1b asserts every borrowed name belongs
to the other manifest and to neither twice, so the list cannot become a second
ownership claim.
Two consequences fixed along the way, both the spelling-versus-membership error
that ScalarPackSpec has now taught four times:
- Phase 2b globbed Proofs/*.olean and would have demanded artifacts this
button never builds. It now scans its manifest by membership and fails
closed on a missing one.
- The three inventory drivers were exempted from the dead-file gate and
compiled in a later phase; after a purge they were absent when Phase 2b
ran. They are now in the manifest like everything else, and three
exemptions are gone.
The sweep runner now reports RESOURCE rather than RED when it sees a
memory_exception: lean-guard's clamp is not a broken proof, and it has misled
the operator once and the author once.
Verified green: 8 full runs from completely purged trees — four check.sh, four
check-scalar.sh — zero red, zero resource. Every artifact rebuilt from
committed source. These are the first runs in this repository's history whose
verdict provably depends on nothing but the bytes in git.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-30 20:54:00 +00:00
# PREREQ is a borrowing, not a claim: every name in it must belong to the
# OTHER manifest. Without this the list could silently grow into a second
# ownership claim over modules this button never audits.
for m in " ${ PREREQ [@] } " ; do
grep -qx " $m " <<< " $SCALAR_MANIFEST " || { echo " PREREQ NOT OWNED BY THE SCALAR BUTTON: $m " ; SEAMFAIL = 1; }
grep -qx " $m " <<< " $MAIN_MANIFEST " && { echo " PREREQ ALSO CLAIMED HERE: $m " ; SEAMFAIL = 1; }
done
[ " $SEAMFAIL " = 0 ] && echo " ${# PREREQ [@] } prerequisites borrowed from check-scalar.sh, which audits them "
verification: close the two-button seam and level up the scalar button (P0-b)
THE SEAM. This repository is checked by two scripts, and until now neither
asserted anything about the other's scope. check.sh's dead-file gate simply
SKIPPED anything named Scalar*, so a new Proofs/ScalarX.lean was gated by
nothing at all: absent from one manifest by exemption, from the other by
omission, compiled by neither, inventoried by neither. Each button now reads
the other's manifest and requires every shipped proof source to belong to
EXACTLY ONE of them — neither orphaned nor double-claimed, both directions,
plus a phantom check on entries naming files that do not exist. Negative-tested
four ways, including the exact hole this item names.
THE SCALAR BUTTON. Closing the seam exposed it as the estate's weakest link,
having been left behind by every hardening round while the main button gained
five phases. 45 lines to 227:
- source-integrity check over its sources;
- harness-pin verification, so running THIS button alone is protected and not
only running it after check.sh;
- a kernel-side axiom-declaration gate over the compiled artifacts, replacing
a source-text grep that is evadable four ways on v4.30.0-rc2;
- a declaration inventory of ~1880 constants against its own allowlist,
diffed both directions with a count trailer. These 13 modules were the only
part of the proof corpus with no inventory: check.sh Phase 2c named them as
uncovered on every run, and now names the button that covers them instead;
- per-certificate exact-cone assertions replacing `-eq 13` over matching
output lines. A count cannot say WHICH certificate is clean and passes just
as happily if one cone is reported twice.
Every fork-specific fact was read from the existing script rather than assumed:
risc0 and betrusted audit sub_loop1_one_spec where dalek and anza audit
cond_add_l_one_spec, untouched.
THREE BUGS, ONE ROOT CAUSE, all found by the gates rather than by review. Each
reasoned about how a thing is SPELLED instead of what it BELONGS TO, and the
corpus punished each: Proofs/ScalarPackSpec.lean is named like the scalar layer
and owned by the main button.
- the scalar dead-file gate globbed Scalar* and demanded ScalarPackSpec be
scalar-owned. REMOVED rather than special-cased: the seam check tests
membership in exactly one manifest, which is strictly stronger than any
prefix;
- the scalar axiom gate scanned Scalar*.olean, reporting "14 modules" for a
13-module manifest. On a tree where check.sh had not run that artifact is
absent and the button would have failed for a false reason. It now scans
the manifest by membership and fails closed on a missing artifact;
- Phase 2c's driver discovery globbed Inventory*.lean and claimed the other
button's driver, then correctly complained its own manifest lacked those
modules.
This is the family the campaign began with: a source-text axiom grep reasoning
about spelling. Recorded in TRUSTED-BASE.md because it generalises.
Also fixed: the first negative test of the scalar gate's absence check passed
for the wrong reason — the button recompiles before the gate runs, so removing
an artifact merely caused it to be rebuilt. Retested against the lifted phase,
where absence is a persistent condition.
Verified green: 24 runs across the four repositories — four main buttons, four
scalar buttons, and sixteen self-tests — zero red.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-30 10:30:26 +00:00
[ " $SEAMFAIL " = 0 ] && echo " every proof source belongs to exactly one button ( $( grep -c . <<< " $MAIN_MANIFEST " ) here, $( grep -c . <<< " $SCALAR_MANIFEST " ) scalar) "
[ " $SEAMFAIL " = 0 ] || { echo "SEAM CHECK FAILED" ; exit 1; }
2026-07-02 12:17:44 +00:00
# ── Phase 2: compile everything shipped ─────────────────────────────────────
verification: --audit-only mode, and the guard that keeps it from becoming evidence (T1)
Gate work dominates this estate's wall-clock: on 2026-07-29, 3.9 hours of a
session went to Lean re-elaborating proofs nobody had edited while the audit
phases themselves took about fifteen seconds. --audit-only runs every gate
against the artifacts a previous full run left behind: ~60s against ~1280s.
IT IS SAFE ONLY BECAUSE IT REFUSES.
- It requires every shipped .lean to be BYTE-IDENTICAL to a basis recorded by
a previous full run. Not mtimes: `touch` defeats those, and a stale-artifact
check that fails open is worse than no shortcut at all, because a green
button would then describe a corpus that is no longer on disk.
- The basis is gitignored build state, so a fresh clone cannot inherit
permission to skip compiling.
- The closing banner differs and says in words that the run is not evidence.
selftest-auditonly.sh exercises seven cases: no basis, an edited comment
character, a deleted source, a new source, a missing artifact, a truncated
basis, and — asserted as a PASS — every source's mtime touched with bytes
unchanged, which pins the bytes-not-mtimes decision rather than leaving it
implicit. Negative-tested: with the basis comparison disabled a changed source
is wrongly accepted, exit 0 and zero refusals, so the guard is load-bearing.
A PHASE TERMINATOR, because this broke twice. Every self-test lifts a phase
from check.sh by scanning to the next phase marker. The last phase had no
marker after it, so a lift ran to end-of-file and swallowed whatever was
appended later — first Phase 2c into the axgate lift, then T1's tail into the
binding lift, where it referenced $AUDIT_ONLY and died under `set -u`. Both
surfaced as the BASELINE case failing: a self-test blaming a gate for its own
extraction bug. The phases now end at an explicit sentinel and both lifters
stop there, so nothing appended below can silently become part of the last
phase from a lifter's point of view.
TRUSTED-BASE.md records what an audit-only transcript does and does not
establish, and — because it cost a confusing red run today — that lean-guard's
memory clamp presents as `FAIL: Proofs/<module>` while being a resource
condition, not a broken proof.
Verified green: 8 full button runs (four check.sh, four check-scalar.sh) and 20
self-tests across the four repositories, zero red. One earlier run failed on
the memory clamp because the author ran a test suite concurrently; re-run on a
quiet machine, green.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-30 17:16:17 +00:00
if [ " $AUDIT_ONLY " = 1 ] ; then
echo "=== Phase 2: SKIPPED (--audit-only) ==="
if [ ! -s " $BASIS " ] ; then
echo " REFUSING: no basis from a previous full run ( $BASIS absent). "
echo " --audit-only may only follow a full green run in this working tree."
echo " Run ./check.sh with no arguments first."
exit 1
fi
if ! diff -q <( source_basis) " $BASIS " >/dev/null 2>& 1; then
echo "REFUSING: the sources no longer match the basis of the last full run."
echo " The .olean files on disk describe a corpus that has changed, so every"
echo " audit below would be judging artifacts that no source produces."
echo " Differences (< basis, > now):"
diff <( source_basis) " $BASIS " | head -20 | sed 's/^/ /'
echo " Run ./check.sh with no arguments."
exit 1
fi
# Fail closed on absence too: a source with no artifact cannot be audited.
MISSING = 0
for m in " ${ PROOFS [@] } " ; do
[ -f " $HERE /Proofs/ $m .olean " ] || { echo " MISSING ARTIFACT: Proofs/ $m .olean " ; MISSING = 1; }
done
for m in " ${ GEN_MODULES [@] } " ; do
[ -f " $HERE /gen/ $m .olean " ] || { echo " MISSING ARTIFACT: gen/ $m .olean " ; MISSING = 1; }
done
[ " $MISSING " = 0 ] || { echo "REFUSING: run ./check.sh with no arguments." ; exit 1; }
echo " sources byte-identical to the last full run's basis; $( grep -c . " $BASIS " ) files "
else
2026-07-02 12:17:44 +00:00
echo "=== Phase 2: compile ==="
LOG = $( mktemp /tmp/check-compile-XXXX.log)
cd " $AENEAS_LEAN "
lake env bash -c "
set -euo pipefail
cd '$HERE/gen' && export LEAN_PATH = \" \$ LEAN_PATH:\$ PWD:$HERE \"
compile( ) {
echo \" · \$ 1\"
2026-07-02 14:10:55 +00:00
LEAN_TIMEOUT = $TIMEOUT LEAN_MAX_CORES = $CORES '$HERE/lean-guard' \" \$ { 1} .lean\" 2>& 1 | tee -a '$LOG' || { echo \" FAIL: \$ 1\" ; exit 1; }
2026-07-02 12:17:44 +00:00
}
for m in ${ GEN_MODULES [*] } ; do compile \" \$ m\" ; done
cd '$HERE'
verification: build hygiene, and the hidden dependency it exposed (P0-a)
Phase 0a purges every .olean before compiling, bans stray Lean files at the
verification root (LEAN_PATH contains $PWD, so they join the build unaudited),
and requires gen/ to be exactly the model manifest plus its pinned templates.
The templates are KEPT, unlike SLH-DSA which deletes them: extract.sh directs
the operator to diff the hand-written external models against them, so they are
the reference for that comparison and P2-c will enforce it.
The purge is skipped under --audit-only, which exists to audit the artifacts a
previous full run produced. Those two features would otherwise destroy each
other, and it is a further reason an audit-only transcript is not evidence: it
has not had this hygiene applied.
WHAT THE PURGE EXPOSED, and it is the point of the whole item:
This button had never compiled the corpus from nothing. The signature apex
rests on scalar arithmetic — PointLiftSpec -> ScalarPackSpec ->
ScalarFromBytesSpec, and SigApexSpec -> ScalarDenote — and TWELVE of the scalar
layer's thirteen modules are transitive prerequisites of this manifest. They
were never compiled here. The button worked because check-scalar.sh had run at
some earlier point and left its .olean files behind. .olean is gitignored, so
no git status could ever have shown that the verdict rested on untracked
artifacts produced by a different script.
Nothing about the proofs was wrong. The evidence was resting on something
invisible, for the entire life of these repositories, and it surfaced the
moment something finally cleaned up before verifying.
Those twelve are now compiled here as PREREQ — BORROWED, NOT OWNED.
check-scalar.sh still audits them; Phase 1b asserts every borrowed name belongs
to the other manifest and to neither twice, so the list cannot become a second
ownership claim.
Two consequences fixed along the way, both the spelling-versus-membership error
that ScalarPackSpec has now taught four times:
- Phase 2b globbed Proofs/*.olean and would have demanded artifacts this
button never builds. It now scans its manifest by membership and fails
closed on a missing one.
- The three inventory drivers were exempted from the dead-file gate and
compiled in a later phase; after a purge they were absent when Phase 2b
ran. They are now in the manifest like everything else, and three
exemptions are gone.
The sweep runner now reports RESOURCE rather than RED when it sees a
memory_exception: lean-guard's clamp is not a broken proof, and it has misled
the operator once and the author once.
Verified green: 8 full runs from completely purged trees — four check.sh, four
check-scalar.sh — zero red, zero resource. Every artifact rebuilt from
committed source. These are the first runs in this repository's history whose
verdict provably depends on nothing but the bytes in git.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-30 20:54:00 +00:00
# Prerequisites first: owned and audited by check-scalar.sh, built here so
# this run does not depend on artifacts another script may have left behind.
for m in ${ PREREQ [*] } ; do
[ -f \" Proofs/\$ m.lean\" ] || { echo \" MISSING PREREQ: Proofs/\$ m.lean\" ; exit 1; }
compile \" Proofs/\$ m\"
done
2026-07-02 12:17:44 +00:00
for m in ${ PROOFS [*] } ; do
[ -f \" Proofs/\$ m.lean\" ] || { echo \" MISSING: Proofs/\$ m.lean listed in manifest\" ; exit 1; }
compile \" Proofs/\$ m\"
done
# every shipped proof file must be in the manifest (no dead files)
for f in Proofs/*.lean; do
b = \$ ( basename \" \$ f\" .lean)
[ \" \$ b\" = AxiomCheck ] && continue
verification: build hygiene, and the hidden dependency it exposed (P0-a)
Phase 0a purges every .olean before compiling, bans stray Lean files at the
verification root (LEAN_PATH contains $PWD, so they join the build unaudited),
and requires gen/ to be exactly the model manifest plus its pinned templates.
The templates are KEPT, unlike SLH-DSA which deletes them: extract.sh directs
the operator to diff the hand-written external models against them, so they are
the reference for that comparison and P2-c will enforce it.
The purge is skipped under --audit-only, which exists to audit the artifacts a
previous full run produced. Those two features would otherwise destroy each
other, and it is a further reason an audit-only transcript is not evidence: it
has not had this hygiene applied.
WHAT THE PURGE EXPOSED, and it is the point of the whole item:
This button had never compiled the corpus from nothing. The signature apex
rests on scalar arithmetic — PointLiftSpec -> ScalarPackSpec ->
ScalarFromBytesSpec, and SigApexSpec -> ScalarDenote — and TWELVE of the scalar
layer's thirteen modules are transitive prerequisites of this manifest. They
were never compiled here. The button worked because check-scalar.sh had run at
some earlier point and left its .olean files behind. .olean is gitignored, so
no git status could ever have shown that the verdict rested on untracked
artifacts produced by a different script.
Nothing about the proofs was wrong. The evidence was resting on something
invisible, for the entire life of these repositories, and it surfaced the
moment something finally cleaned up before verifying.
Those twelve are now compiled here as PREREQ — BORROWED, NOT OWNED.
check-scalar.sh still audits them; Phase 1b asserts every borrowed name belongs
to the other manifest and to neither twice, so the list cannot become a second
ownership claim.
Two consequences fixed along the way, both the spelling-versus-membership error
that ScalarPackSpec has now taught four times:
- Phase 2b globbed Proofs/*.olean and would have demanded artifacts this
button never builds. It now scans its manifest by membership and fails
closed on a missing one.
- The three inventory drivers were exempted from the dead-file gate and
compiled in a later phase; after a purge they were absent when Phase 2b
ran. They are now in the manifest like everything else, and three
exemptions are gone.
The sweep runner now reports RESOURCE rather than RED when it sees a
memory_exception: lean-guard's clamp is not a broken proof, and it has misled
the operator once and the author once.
Verified green: 8 full runs from completely purged trees — four check.sh, four
check-scalar.sh — zero red, zero resource. Every artifact rebuilt from
committed source. These are the first runs in this repository's history whose
verdict provably depends on nothing but the bytes in git.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-30 20:54:00 +00:00
# InventoryScalar belongs to the other button; the rest are in PROOFS above.
case \" \$ b\" in InventoryScalar) continue ; ; esac
2026-07-03 10:54:26 +00:00
case \" \$ b\" in Scalar*) continue ; ; esac # scalar layer: checked by check-scalar.sh (coherence pass 2)
2026-07-02 12:17:44 +00:00
case \" ${ PROOFS [*] } \" in ( *\" \$ b \" *) ; ; ( *) echo \" DEAD FILE: \$ f not in check manifest\" ; exit 1; ; esac
done
"
if grep -q "uses 'sorry'" " $LOG " ; then
echo "STUB DETECTED: a compiled declaration uses 'sorry'" ; exit 1; fi
rm -f " $LOG "
verification: --audit-only mode, and the guard that keeps it from becoming evidence (T1)
Gate work dominates this estate's wall-clock: on 2026-07-29, 3.9 hours of a
session went to Lean re-elaborating proofs nobody had edited while the audit
phases themselves took about fifteen seconds. --audit-only runs every gate
against the artifacts a previous full run left behind: ~60s against ~1280s.
IT IS SAFE ONLY BECAUSE IT REFUSES.
- It requires every shipped .lean to be BYTE-IDENTICAL to a basis recorded by
a previous full run. Not mtimes: `touch` defeats those, and a stale-artifact
check that fails open is worse than no shortcut at all, because a green
button would then describe a corpus that is no longer on disk.
- The basis is gitignored build state, so a fresh clone cannot inherit
permission to skip compiling.
- The closing banner differs and says in words that the run is not evidence.
selftest-auditonly.sh exercises seven cases: no basis, an edited comment
character, a deleted source, a new source, a missing artifact, a truncated
basis, and — asserted as a PASS — every source's mtime touched with bytes
unchanged, which pins the bytes-not-mtimes decision rather than leaving it
implicit. Negative-tested: with the basis comparison disabled a changed source
is wrongly accepted, exit 0 and zero refusals, so the guard is load-bearing.
A PHASE TERMINATOR, because this broke twice. Every self-test lifts a phase
from check.sh by scanning to the next phase marker. The last phase had no
marker after it, so a lift ran to end-of-file and swallowed whatever was
appended later — first Phase 2c into the axgate lift, then T1's tail into the
binding lift, where it referenced $AUDIT_ONLY and died under `set -u`. Both
surfaced as the BASELINE case failing: a self-test blaming a gate for its own
extraction bug. The phases now end at an explicit sentinel and both lifters
stop there, so nothing appended below can silently become part of the last
phase from a lifter's point of view.
TRUSTED-BASE.md records what an audit-only transcript does and does not
establish, and — because it cost a confusing red run today — that lean-guard's
memory clamp presents as `FAIL: Proofs/<module>` while being a resource
condition, not a broken proof.
Verified green: 8 full button runs (four check.sh, four check-scalar.sh) and 20
self-tests across the four repositories, zero red. One earlier run failed on
the memory clamp because the author ran a test suite concurrently; re-run on a
quiet machine, green.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-30 17:16:17 +00:00
fi
2026-07-02 12:17:44 +00:00
verification: kernel-side axiom-declaration gate (Phase 2b) + self-test
Phase 1's anti-smuggling check reads source text. Measured today on Lean
v4.30.0-rc2, four distinct declarations compile cleanly and slip past its
anchored pattern:
` axiom cheat : ...` one leading space
`@[simp] axiom cheat : ...` line starts with the attribute
`unsafe axiom cheat : ...` `unsafe` absent from the modifier list
`axiom` <newline> ` cheat` no space follows the keyword
Any of them yields a repository that proves False while the button prints
ALL GREEN. Only the tab variant is blocked, and by Lean, not by us.
Hardening the pattern would fix the exhibited syntax rather than the class,
which is the mistake this estate has made before. Phase 2b stops parsing text
and asks the kernel instead: it reads every compiled Proofs/*.olean with
readModuleData and rejects any declaration that is an axiom.
Design notes:
- reads compiled artifacts rather than importing the modules, because
Proofs.Basic and Proofs.ConstSpecs deliberately reuse `zero_spec` and a
whole-corpus import is impossible by construction;
- membership is self-deriving from the filesystem, so Scalar* and
AxiomCheck are covered too — both are skipped by the CERTS audit and by
the dead-file gate;
- fails closed on absence: a missing .olean would make the scan vacuous, so
the count of compiled modules must equal the count of shipped sources;
- removes its temp source AND artifact on both paths, since a bare `rm`
after the call never runs under `set -e` when the gate goes red — exactly
how this repo accumulated 101 orphan .olean files;
- ~3 s for the whole corpus, against ~53 s for one module-importing run.
Phase 1's grep stays as a fast first line of defence. Phase 2b is the gate
that is load-bearing.
selftest-axgate.sh attacks the shipping gate, lifted out of check.sh at run
time rather than copied. It asserts the specific diagnostic, so a rejection
for an unrelated reason fails too, and it was itself negative-tested: with
the gate's throwError removed, the self-test goes red on exactly that case.
No proof, statement, specification or certificate is touched. No attested
commit is altered — the log binds specific commit hashes, all of which remain
ancestors of HEAD.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-28 16:24:18 +00:00
# ── Phase 2b: kernel-side axiom-declaration gate ────────────────────────────
# WHY THIS EXISTS. Phase 1's anti-smuggling check reads SOURCE TEXT, and a
# source-text grep is the wrong instrument. Measured on Lean v4.30.0-rc2
# (2026-07-28), each of the following compiles cleanly and slips past it:
# ` axiom cheat : ...` (one leading space — the pattern is anchored)
# `@[simp] axiom cheat : ...` (line starts with the attribute)
# `unsafe axiom cheat : ...` (`unsafe` is not in the modifier alternation)
# `axiom` <newline> ` cheat` (no space follows the keyword)
# Only the tab variant is blocked, and by Lean itself, not by us. Hardening the
# pattern would fix the exhibited syntax rather than the class; the class fix is
# to stop parsing text and ask the kernel, which is what this phase does.
# Ported from fips205-slhdsa-verified/verification/Proofs/Audit.lean.
#
# Phase 1's grep is kept as a fast, readable first line of defence. THIS is the
# gate that is load-bearing.
echo "=== Phase 2b: kernel-side axiom-declaration gate ==="
# dot-prefixed and inside $HERE: `lean` refuses a file outside the root
# directory, and a leading dot keeps it out of every *.lean glob.
# The gate reads the COMPILED ARTIFACTS directly (readModuleData) rather than
# importing the modules. Two reasons, both load-bearing:
# · Proofs.Basic and Proofs.ConstSpecs deliberately reuse the name
# `zero_spec` (they are never imported together), so a whole-corpus import
# is impossible by construction — it fails with "environment already
# contains". Reading oleans merges nothing, so collisions cannot arise.
# · Membership is then SELF-DERIVING from the filesystem: every .olean under
# Proofs/ is scanned, including Scalar* and AxiomCheck, which the CERTS
# audit and the dead-file gate both skip. Nothing is on a hand-kept list.
# Cost is ~3 s for the whole corpus (no mathlib import), against ~53 s for a
# single module-importing invocation.
verification: build hygiene, and the hidden dependency it exposed (P0-a)
Phase 0a purges every .olean before compiling, bans stray Lean files at the
verification root (LEAN_PATH contains $PWD, so they join the build unaudited),
and requires gen/ to be exactly the model manifest plus its pinned templates.
The templates are KEPT, unlike SLH-DSA which deletes them: extract.sh directs
the operator to diff the hand-written external models against them, so they are
the reference for that comparison and P2-c will enforce it.
The purge is skipped under --audit-only, which exists to audit the artifacts a
previous full run produced. Those two features would otherwise destroy each
other, and it is a further reason an audit-only transcript is not evidence: it
has not had this hygiene applied.
WHAT THE PURGE EXPOSED, and it is the point of the whole item:
This button had never compiled the corpus from nothing. The signature apex
rests on scalar arithmetic — PointLiftSpec -> ScalarPackSpec ->
ScalarFromBytesSpec, and SigApexSpec -> ScalarDenote — and TWELVE of the scalar
layer's thirteen modules are transitive prerequisites of this manifest. They
were never compiled here. The button worked because check-scalar.sh had run at
some earlier point and left its .olean files behind. .olean is gitignored, so
no git status could ever have shown that the verdict rested on untracked
artifacts produced by a different script.
Nothing about the proofs was wrong. The evidence was resting on something
invisible, for the entire life of these repositories, and it surfaced the
moment something finally cleaned up before verifying.
Those twelve are now compiled here as PREREQ — BORROWED, NOT OWNED.
check-scalar.sh still audits them; Phase 1b asserts every borrowed name belongs
to the other manifest and to neither twice, so the list cannot become a second
ownership claim.
Two consequences fixed along the way, both the spelling-versus-membership error
that ScalarPackSpec has now taught four times:
- Phase 2b globbed Proofs/*.olean and would have demanded artifacts this
button never builds. It now scans its manifest by membership and fails
closed on a missing one.
- The three inventory drivers were exempted from the dead-file gate and
compiled in a later phase; after a purge they were absent when Phase 2b
ran. They are now in the manifest like everything else, and three
exemptions are gone.
The sweep runner now reports RESOURCE rather than RED when it sees a
memory_exception: lean-guard's clamp is not a broken proof, and it has misled
the operator once and the author once.
Verified green: 8 full runs from completely purged trees — four check.sh, four
check-scalar.sh — zero red, zero resource. Every artifact rebuilt from
committed source. These are the first runs in this repository's history whose
verdict provably depends on nothing but the bytes in git.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-30 20:54:00 +00:00
# MEMBERSHIP, not a glob. Phase 0a purges every .olean and this button
# rebuilds only its own manifest; the scalar layer's artifacts belong to the
# other button. Counting Proofs/*.lean here would demand artifacts this run
# never makes — the spelling-versus-ownership error ScalarPackSpec exposed.
PROOF_OLEANS = $( printf '"%s.olean", ' " ${ PROOFS [@] } " | sed 's/, $//' )
verification: kernel-side axiom-declaration gate (Phase 2b) + self-test
Phase 1's anti-smuggling check reads source text. Measured today on Lean
v4.30.0-rc2, four distinct declarations compile cleanly and slip past its
anchored pattern:
` axiom cheat : ...` one leading space
`@[simp] axiom cheat : ...` line starts with the attribute
`unsafe axiom cheat : ...` `unsafe` absent from the modifier list
`axiom` <newline> ` cheat` no space follows the keyword
Any of them yields a repository that proves False while the button prints
ALL GREEN. Only the tab variant is blocked, and by Lean, not by us.
Hardening the pattern would fix the exhibited syntax rather than the class,
which is the mistake this estate has made before. Phase 2b stops parsing text
and asks the kernel instead: it reads every compiled Proofs/*.olean with
readModuleData and rejects any declaration that is an axiom.
Design notes:
- reads compiled artifacts rather than importing the modules, because
Proofs.Basic and Proofs.ConstSpecs deliberately reuse `zero_spec` and a
whole-corpus import is impossible by construction;
- membership is self-deriving from the filesystem, so Scalar* and
AxiomCheck are covered too — both are skipped by the CERTS audit and by
the dead-file gate;
- fails closed on absence: a missing .olean would make the scan vacuous, so
the count of compiled modules must equal the count of shipped sources;
- removes its temp source AND artifact on both paths, since a bare `rm`
after the call never runs under `set -e` when the gate goes red — exactly
how this repo accumulated 101 orphan .olean files;
- ~3 s for the whole corpus, against ~53 s for one module-importing run.
Phase 1's grep stays as a fast first line of defence. Phase 2b is the gate
that is load-bearing.
selftest-axgate.sh attacks the shipping gate, lifted out of check.sh at run
time rather than copied. It asserts the specific diagnostic, so a rejection
for an unrelated reason fails too, and it was itself negative-tested: with
the gate's throwError removed, the self-test goes red on exactly that case.
No proof, statement, specification or certificate is touched. No attested
commit is altered — the log binds specific commit hashes, all of which remain
ancestors of HEAD.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-28 16:24:18 +00:00
GATE = $( mktemp " $HERE /.axgate-XXXX.lean " )
{
echo "import Lean"
echo "open Lean"
verification: build hygiene, and the hidden dependency it exposed (P0-a)
Phase 0a purges every .olean before compiling, bans stray Lean files at the
verification root (LEAN_PATH contains $PWD, so they join the build unaudited),
and requires gen/ to be exactly the model manifest plus its pinned templates.
The templates are KEPT, unlike SLH-DSA which deletes them: extract.sh directs
the operator to diff the hand-written external models against them, so they are
the reference for that comparison and P2-c will enforce it.
The purge is skipped under --audit-only, which exists to audit the artifacts a
previous full run produced. Those two features would otherwise destroy each
other, and it is a further reason an audit-only transcript is not evidence: it
has not had this hygiene applied.
WHAT THE PURGE EXPOSED, and it is the point of the whole item:
This button had never compiled the corpus from nothing. The signature apex
rests on scalar arithmetic — PointLiftSpec -> ScalarPackSpec ->
ScalarFromBytesSpec, and SigApexSpec -> ScalarDenote — and TWELVE of the scalar
layer's thirteen modules are transitive prerequisites of this manifest. They
were never compiled here. The button worked because check-scalar.sh had run at
some earlier point and left its .olean files behind. .olean is gitignored, so
no git status could ever have shown that the verdict rested on untracked
artifacts produced by a different script.
Nothing about the proofs was wrong. The evidence was resting on something
invisible, for the entire life of these repositories, and it surfaced the
moment something finally cleaned up before verifying.
Those twelve are now compiled here as PREREQ — BORROWED, NOT OWNED.
check-scalar.sh still audits them; Phase 1b asserts every borrowed name belongs
to the other manifest and to neither twice, so the list cannot become a second
ownership claim.
Two consequences fixed along the way, both the spelling-versus-membership error
that ScalarPackSpec has now taught four times:
- Phase 2b globbed Proofs/*.olean and would have demanded artifacts this
button never builds. It now scans its manifest by membership and fails
closed on a missing one.
- The three inventory drivers were exempted from the dead-file gate and
compiled in a later phase; after a purge they were absent when Phase 2b
ran. They are now in the manifest like everything else, and three
exemptions are gone.
The sweep runner now reports RESOURCE rather than RED when it sees a
memory_exception: lean-guard's clamp is not a broken proof, and it has misled
the operator once and the author once.
Verified green: 8 full runs from completely purged trees — four check.sh, four
check-scalar.sh — zero red, zero resource. Every artifact rebuilt from
committed source. These are the first runs in this repository's history whose
verdict provably depends on nothing but the bytes in git.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-30 20:54:00 +00:00
echo " def expected : List String := [ $PROOF_OLEANS ] "
verification: kernel-side axiom-declaration gate (Phase 2b) + self-test
Phase 1's anti-smuggling check reads source text. Measured today on Lean
v4.30.0-rc2, four distinct declarations compile cleanly and slip past its
anchored pattern:
` axiom cheat : ...` one leading space
`@[simp] axiom cheat : ...` line starts with the attribute
`unsafe axiom cheat : ...` `unsafe` absent from the modifier list
`axiom` <newline> ` cheat` no space follows the keyword
Any of them yields a repository that proves False while the button prints
ALL GREEN. Only the tab variant is blocked, and by Lean, not by us.
Hardening the pattern would fix the exhibited syntax rather than the class,
which is the mistake this estate has made before. Phase 2b stops parsing text
and asks the kernel instead: it reads every compiled Proofs/*.olean with
readModuleData and rejects any declaration that is an axiom.
Design notes:
- reads compiled artifacts rather than importing the modules, because
Proofs.Basic and Proofs.ConstSpecs deliberately reuse `zero_spec` and a
whole-corpus import is impossible by construction;
- membership is self-deriving from the filesystem, so Scalar* and
AxiomCheck are covered too — both are skipped by the CERTS audit and by
the dead-file gate;
- fails closed on absence: a missing .olean would make the scan vacuous, so
the count of compiled modules must equal the count of shipped sources;
- removes its temp source AND artifact on both paths, since a bare `rm`
after the call never runs under `set -e` when the gate goes red — exactly
how this repo accumulated 101 orphan .olean files;
- ~3 s for the whole corpus, against ~53 s for one module-importing run.
Phase 1's grep stays as a fast first line of defence. Phase 2b is the gate
that is load-bearing.
selftest-axgate.sh attacks the shipping gate, lifted out of check.sh at run
time rather than copied. It asserts the specific diagnostic, so a rejection
for an unrelated reason fails too, and it was itself negative-tested: with
the gate's throwError removed, the self-test goes red on exactly that case.
No proof, statement, specification or certificate is touched. No attested
commit is altered — the log binds specific commit hashes, all of which remain
ancestors of HEAD.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-28 16:24:18 +00:00
cat <<'LEANGATE'
run_cmd do
let dir : System.FilePath := "Proofs"
let mut errs : Array String := #[]
let mut nMod := 0
let mut nConst := 0
2026-08-04 01:17:05 +00:00
let mut seen : Std.HashSet ( String × ) := { }
verification: build hygiene, and the hidden dependency it exposed (P0-a)
Phase 0a purges every .olean before compiling, bans stray Lean files at the
verification root (LEAN_PATH contains $PWD, so they join the build unaudited),
and requires gen/ to be exactly the model manifest plus its pinned templates.
The templates are KEPT, unlike SLH-DSA which deletes them: extract.sh directs
the operator to diff the hand-written external models against them, so they are
the reference for that comparison and P2-c will enforce it.
The purge is skipped under --audit-only, which exists to audit the artifacts a
previous full run produced. Those two features would otherwise destroy each
other, and it is a further reason an audit-only transcript is not evidence: it
has not had this hygiene applied.
WHAT THE PURGE EXPOSED, and it is the point of the whole item:
This button had never compiled the corpus from nothing. The signature apex
rests on scalar arithmetic — PointLiftSpec -> ScalarPackSpec ->
ScalarFromBytesSpec, and SigApexSpec -> ScalarDenote — and TWELVE of the scalar
layer's thirteen modules are transitive prerequisites of this manifest. They
were never compiled here. The button worked because check-scalar.sh had run at
some earlier point and left its .olean files behind. .olean is gitignored, so
no git status could ever have shown that the verdict rested on untracked
artifacts produced by a different script.
Nothing about the proofs was wrong. The evidence was resting on something
invisible, for the entire life of these repositories, and it surfaced the
moment something finally cleaned up before verifying.
Those twelve are now compiled here as PREREQ — BORROWED, NOT OWNED.
check-scalar.sh still audits them; Phase 1b asserts every borrowed name belongs
to the other manifest and to neither twice, so the list cannot become a second
ownership claim.
Two consequences fixed along the way, both the spelling-versus-membership error
that ScalarPackSpec has now taught four times:
- Phase 2b globbed Proofs/*.olean and would have demanded artifacts this
button never builds. It now scans its manifest by membership and fails
closed on a missing one.
- The three inventory drivers were exempted from the dead-file gate and
compiled in a later phase; after a purge they were absent when Phase 2b
ran. They are now in the manifest like everything else, and three
exemptions are gone.
The sweep runner now reports RESOURCE rather than RED when it sees a
memory_exception: lean-guard's clamp is not a broken proof, and it has misled
the operator once and the author once.
Verified green: 8 full runs from completely purged trees — four check.sh, four
check-scalar.sh — zero red, zero resource. Every artifact rebuilt from
committed source. These are the first runs in this repository's history whose
verdict provably depends on nothing but the bytes in git.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-30 20:54:00 +00:00
for name in expected do
let p := dir / name
-- FAIL CLOSED ON ABSENCE: a manifest module whose artifact is missing makes
-- this gate vacuous for that module. It must be an error, never a skip.
unless ( ← p.pathExists) do
throwError "COVERAGE: {name} is in the compile manifest but its artifact is absent"
nMod := nMod + 1
let ( mod, _) ← readModuleData p
2026-08-04 01:17:05 +00:00
-- THE MODULE IS PART OF THE RECORD. Round-9 review ( Claude, N2) : this gate
-- emitted KERNEL-NAME| <name>, and check.sh compared it against allowlists
-- keyed on module| name — keys that carry the module PRECISELY BECAUSE A
-- NAME IS NOT UNIQUE. This corpus still holds two distinct declarations
-- both called CurveFieldProofs.zero_spec ( Proofs.Basic and
-- Proofs.ConstSpecs) , which is why the module column was added to INV rows
-- in the first place. Keyed on name alone the identity certified " every
-- declaration NAME the kernel saw is accounted for ", not " every
-- declaration" — the same defect as the round-11 DRV regression, sitting
-- inside the check that caught it.
let modName := "Proofs." ++ ( name.dropRight 6) -- strip ".olean"
verification: build hygiene, and the hidden dependency it exposed (P0-a)
Phase 0a purges every .olean before compiling, bans stray Lean files at the
verification root (LEAN_PATH contains $PWD, so they join the build unaudited),
and requires gen/ to be exactly the model manifest plus its pinned templates.
The templates are KEPT, unlike SLH-DSA which deletes them: extract.sh directs
the operator to diff the hand-written external models against them, so they are
the reference for that comparison and P2-c will enforce it.
The purge is skipped under --audit-only, which exists to audit the artifacts a
previous full run produced. Those two features would otherwise destroy each
other, and it is a further reason an audit-only transcript is not evidence: it
has not had this hygiene applied.
WHAT THE PURGE EXPOSED, and it is the point of the whole item:
This button had never compiled the corpus from nothing. The signature apex
rests on scalar arithmetic — PointLiftSpec -> ScalarPackSpec ->
ScalarFromBytesSpec, and SigApexSpec -> ScalarDenote — and TWELVE of the scalar
layer's thirteen modules are transitive prerequisites of this manifest. They
were never compiled here. The button worked because check-scalar.sh had run at
some earlier point and left its .olean files behind. .olean is gitignored, so
no git status could ever have shown that the verdict rested on untracked
artifacts produced by a different script.
Nothing about the proofs was wrong. The evidence was resting on something
invisible, for the entire life of these repositories, and it surfaced the
moment something finally cleaned up before verifying.
Those twelve are now compiled here as PREREQ — BORROWED, NOT OWNED.
check-scalar.sh still audits them; Phase 1b asserts every borrowed name belongs
to the other manifest and to neither twice, so the list cannot become a second
ownership claim.
Two consequences fixed along the way, both the spelling-versus-membership error
that ScalarPackSpec has now taught four times:
- Phase 2b globbed Proofs/*.olean and would have demanded artifacts this
button never builds. It now scans its manifest by membership and fails
closed on a missing one.
- The three inventory drivers were exempted from the dead-file gate and
compiled in a later phase; after a purge they were absent when Phase 2b
ran. They are now in the manifest like everything else, and three
exemptions are gone.
The sweep runner now reports RESOURCE rather than RED when it sees a
memory_exception: lean-guard's clamp is not a broken proof, and it has misled
the operator once and the author once.
Verified green: 8 full runs from completely purged trees — four check.sh, four
check-scalar.sh — zero red, zero resource. Every artifact rebuilt from
committed source. These are the first runs in this repository's history whose
verdict provably depends on nothing but the bytes in git.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-30 20:54:00 +00:00
for ci in mod.constants do
nConst := nConst + 1
2026-08-04 01:17:05 +00:00
seen := seen.insert ( modName, ci.name)
verification: build hygiene, and the hidden dependency it exposed (P0-a)
Phase 0a purges every .olean before compiling, bans stray Lean files at the
verification root (LEAN_PATH contains $PWD, so they join the build unaudited),
and requires gen/ to be exactly the model manifest plus its pinned templates.
The templates are KEPT, unlike SLH-DSA which deletes them: extract.sh directs
the operator to diff the hand-written external models against them, so they are
the reference for that comparison and P2-c will enforce it.
The purge is skipped under --audit-only, which exists to audit the artifacts a
previous full run produced. Those two features would otherwise destroy each
other, and it is a further reason an audit-only transcript is not evidence: it
has not had this hygiene applied.
WHAT THE PURGE EXPOSED, and it is the point of the whole item:
This button had never compiled the corpus from nothing. The signature apex
rests on scalar arithmetic — PointLiftSpec -> ScalarPackSpec ->
ScalarFromBytesSpec, and SigApexSpec -> ScalarDenote — and TWELVE of the scalar
layer's thirteen modules are transitive prerequisites of this manifest. They
were never compiled here. The button worked because check-scalar.sh had run at
some earlier point and left its .olean files behind. .olean is gitignored, so
no git status could ever have shown that the verdict rested on untracked
artifacts produced by a different script.
Nothing about the proofs was wrong. The evidence was resting on something
invisible, for the entire life of these repositories, and it surfaced the
moment something finally cleaned up before verifying.
Those twelve are now compiled here as PREREQ — BORROWED, NOT OWNED.
check-scalar.sh still audits them; Phase 1b asserts every borrowed name belongs
to the other manifest and to neither twice, so the list cannot become a second
ownership claim.
Two consequences fixed along the way, both the spelling-versus-membership error
that ScalarPackSpec has now taught four times:
- Phase 2b globbed Proofs/*.olean and would have demanded artifacts this
button never builds. It now scans its manifest by membership and fails
closed on a missing one.
- The three inventory drivers were exempted from the dead-file gate and
compiled in a later phase; after a purge they were absent when Phase 2b
ran. They are now in the manifest like everything else, and three
exemptions are gone.
The sweep runner now reports RESOURCE rather than RED when it sees a
memory_exception: lean-guard's clamp is not a broken proof, and it has misled
the operator once and the author once.
Verified green: 8 full runs from completely purged trees — four check.sh, four
check-scalar.sh — zero red, zero resource. Every artifact rebuilt from
committed source. These are the first runs in this repository's history whose
verdict provably depends on nothing but the bytes in git.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-30 20:54:00 +00:00
if ci matches .axiomInfo _ then
errs := errs.push s!" {name}: {ci.name}"
verification: kernel-side axiom-declaration gate (Phase 2b) + self-test
Phase 1's anti-smuggling check reads source text. Measured today on Lean
v4.30.0-rc2, four distinct declarations compile cleanly and slip past its
anchored pattern:
` axiom cheat : ...` one leading space
`@[simp] axiom cheat : ...` line starts with the attribute
`unsafe axiom cheat : ...` `unsafe` absent from the modifier list
`axiom` <newline> ` cheat` no space follows the keyword
Any of them yields a repository that proves False while the button prints
ALL GREEN. Only the tab variant is blocked, and by Lean, not by us.
Hardening the pattern would fix the exhibited syntax rather than the class,
which is the mistake this estate has made before. Phase 2b stops parsing text
and asks the kernel instead: it reads every compiled Proofs/*.olean with
readModuleData and rejects any declaration that is an axiom.
Design notes:
- reads compiled artifacts rather than importing the modules, because
Proofs.Basic and Proofs.ConstSpecs deliberately reuse `zero_spec` and a
whole-corpus import is impossible by construction;
- membership is self-deriving from the filesystem, so Scalar* and
AxiomCheck are covered too — both are skipped by the CERTS audit and by
the dead-file gate;
- fails closed on absence: a missing .olean would make the scan vacuous, so
the count of compiled modules must equal the count of shipped sources;
- removes its temp source AND artifact on both paths, since a bare `rm`
after the call never runs under `set -e` when the gate goes red — exactly
how this repo accumulated 101 orphan .olean files;
- ~3 s for the whole corpus, against ~53 s for one module-importing run.
Phase 1's grep stays as a fast first line of defence. Phase 2b is the gate
that is load-bearing.
selftest-axgate.sh attacks the shipping gate, lifted out of check.sh at run
time rather than copied. It asserts the specific diagnostic, so a rejection
for an unrelated reason fails too, and it was itself negative-tested: with
the gate's throwError removed, the self-test goes red on exactly that case.
No proof, statement, specification or certificate is touched. No attested
commit is altered — the log binds specific commit hashes, all of which remain
ancestors of HEAD.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-28 16:24:18 +00:00
unless errs.isEmpty do
throwError "AXIOM DECLARED under Proofs/ (kernel-side gate):\n{String.intercalate " \n " errs.toList}"
-- FAIL CLOSED ON ABSENCE: an empty result and a clean result must not share
-- a code path. A deleted .olean would make the scan above vacuous; an extra
-- one is orphan litter with no shipped source.
verification: build hygiene, and the hidden dependency it exposed (P0-a)
Phase 0a purges every .olean before compiling, bans stray Lean files at the
verification root (LEAN_PATH contains $PWD, so they join the build unaudited),
and requires gen/ to be exactly the model manifest plus its pinned templates.
The templates are KEPT, unlike SLH-DSA which deletes them: extract.sh directs
the operator to diff the hand-written external models against them, so they are
the reference for that comparison and P2-c will enforce it.
The purge is skipped under --audit-only, which exists to audit the artifacts a
previous full run produced. Those two features would otherwise destroy each
other, and it is a further reason an audit-only transcript is not evidence: it
has not had this hygiene applied.
WHAT THE PURGE EXPOSED, and it is the point of the whole item:
This button had never compiled the corpus from nothing. The signature apex
rests on scalar arithmetic — PointLiftSpec -> ScalarPackSpec ->
ScalarFromBytesSpec, and SigApexSpec -> ScalarDenote — and TWELVE of the scalar
layer's thirteen modules are transitive prerequisites of this manifest. They
were never compiled here. The button worked because check-scalar.sh had run at
some earlier point and left its .olean files behind. .olean is gitignored, so
no git status could ever have shown that the verdict rested on untracked
artifacts produced by a different script.
Nothing about the proofs was wrong. The evidence was resting on something
invisible, for the entire life of these repositories, and it surfaced the
moment something finally cleaned up before verifying.
Those twelve are now compiled here as PREREQ — BORROWED, NOT OWNED.
check-scalar.sh still audits them; Phase 1b asserts every borrowed name belongs
to the other manifest and to neither twice, so the list cannot become a second
ownership claim.
Two consequences fixed along the way, both the spelling-versus-membership error
that ScalarPackSpec has now taught four times:
- Phase 2b globbed Proofs/*.olean and would have demanded artifacts this
button never builds. It now scans its manifest by membership and fails
closed on a missing one.
- The three inventory drivers were exempted from the dead-file gate and
compiled in a later phase; after a purge they were absent when Phase 2b
ran. They are now in the manifest like everything else, and three
exemptions are gone.
The sweep runner now reports RESOURCE rather than RED when it sees a
memory_exception: lean-guard's clamp is not a broken proof, and it has misled
the operator once and the author once.
Verified green: 8 full runs from completely purged trees — four check.sh, four
check-scalar.sh — zero red, zero resource. Every artifact rebuilt from
committed source. These are the first runs in this repository's history whose
verdict provably depends on nothing but the bytes in git.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-30 20:54:00 +00:00
logInfo s!" kernel confirms: {nConst} declarations across {nMod} compiled modules (this button's manifest, by membership), none is an axiom"
2026-08-04 01:17:05 +00:00
for ( m, n) in seen do IO.println s!"KERNEL-NAME|{m}|{n}"
verification: kernel-side axiom-declaration gate (Phase 2b) + self-test
Phase 1's anti-smuggling check reads source text. Measured today on Lean
v4.30.0-rc2, four distinct declarations compile cleanly and slip past its
anchored pattern:
` axiom cheat : ...` one leading space
`@[simp] axiom cheat : ...` line starts with the attribute
`unsafe axiom cheat : ...` `unsafe` absent from the modifier list
`axiom` <newline> ` cheat` no space follows the keyword
Any of them yields a repository that proves False while the button prints
ALL GREEN. Only the tab variant is blocked, and by Lean, not by us.
Hardening the pattern would fix the exhibited syntax rather than the class,
which is the mistake this estate has made before. Phase 2b stops parsing text
and asks the kernel instead: it reads every compiled Proofs/*.olean with
readModuleData and rejects any declaration that is an axiom.
Design notes:
- reads compiled artifacts rather than importing the modules, because
Proofs.Basic and Proofs.ConstSpecs deliberately reuse `zero_spec` and a
whole-corpus import is impossible by construction;
- membership is self-deriving from the filesystem, so Scalar* and
AxiomCheck are covered too — both are skipped by the CERTS audit and by
the dead-file gate;
- fails closed on absence: a missing .olean would make the scan vacuous, so
the count of compiled modules must equal the count of shipped sources;
- removes its temp source AND artifact on both paths, since a bare `rm`
after the call never runs under `set -e` when the gate goes red — exactly
how this repo accumulated 101 orphan .olean files;
- ~3 s for the whole corpus, against ~53 s for one module-importing run.
Phase 1's grep stays as a fast first line of defence. Phase 2b is the gate
that is load-bearing.
selftest-axgate.sh attacks the shipping gate, lifted out of check.sh at run
time rather than copied. It asserts the specific diagnostic, so a rejection
for an unrelated reason fails too, and it was itself negative-tested: with
the gate's throwError removed, the self-test goes red on exactly that case.
No proof, statement, specification or certificate is touched. No attested
commit is altered — the log binds specific commit hashes, all of which remain
ancestors of HEAD.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-28 16:24:18 +00:00
LEANGATE
} > " $GATE "
cd " $AENEAS_LEAN "
# The temp source AND its compiled artifact are removed on BOTH paths. Under
# `set -e` a bare `rm` after the call never runs when the gate goes red, which
# is exactly how this repo accumulated 101 orphan .olean files (fixed today).
GATE_RC = 0
Account for every constant the kernel sees, by set containment
THE GAP. The capability matrix in the control repo — built after the author
answered a capability question by grepping for a FILENAME rather than for the
property, three times in one session — asked whether each repository's auditor
enumerates itself. The four ed25519 forks answered no. Following that up found
something larger: `Proofs/Audit.lean`, the statement-binding driver from P1-a,
is compiled, is a member of the manifest, and was enumerated by NOTHING. The
kernel counted 3058 declarations where the inventory accounted for 3022, and
26 of the 36 missing were its.
THE PROPERTY, now enforced: every constant the kernel sees under this button's
manifest must appear, BY NAME, in either the corpus inventory or the
instruments' own surface. `emitDrivers` in InventoryCore walks the audit
modules and fails closed on an axiom (which would widen the trusted base
outside every cone) or on a standalone claim (which no certificate covers and
no allowlist pins), while admitting the obligations the elaborator generates
for a definition declared alongside it.
TWO WRONG FORMULATIONS FIRST, both recorded because the second is instructive:
· `kernel = corpus + instruments + N_DRIVERS`, where the last term was
justified as a per-driver "self-observation blind spot". It fitted dalek
and anza (2 drivers, residual 2) and broke on risc0 and betrusted
(1 driver, residual 2). The residual is 2 everywhere and has nothing to do
with drivers. This was curve-fitting from a sample of one, and it was named
as the highest-risk claim in the round-7 self-assessment BEFORE the data
refuted it.
· distinct-by-name counting, which collapses `CurveFieldProofs.zero_spec` —
a name that genuinely denotes two different declarations, in Proofs.Basic
and Proofs.ConstSpecs, walked by two drivers with separate environments.
THE MEASURED CAUSE of the residual. Lean materialises equation lemmas lazily,
when something forces an unfold, and each module that forces one gets its own
copy in its object file. `CurveFieldProofs.denote.eq_1` sits in both
SubNegSpec.olean and ConstSpecs.olean; `CurveFieldProofs.limbsVal.eq_1` in both
ReduceSpec.olean and ConstSpecs.olean. The kernel gate reads object files and
counts both copies; the environment holds one constant per name. Counts cannot
relate those two views in either direction — so the check compares SETS, which
is the idiom the rest of this estate already uses, and no constant remains that
could be widened to make a red run green.
Negative-tested: with the instrument walk disabled, the check names
Proofs.Audit's declarations as unaccounted.
ANZA also lacked one allowlist row, `subtle.Choice...from.eq_1`, the same
lazy-materialisation effect seen from the other side. Verified rather than
assumed before adding it: the parent is declared in gen/CurveField/
FunsExternal.lean — the model, pinned by bytes and not inventoried by
declaration — the lemma materialised in Proofs.CompressSpec which forced the
unfold, and all three other forks carry the lemma row while none carries the
parent.
CONSEQUENCE WORTH DISCLOSING: the audited declaration surface is not purely a
function of the corpus source. It depends on which proofs forced which
unfolds. This is now a known gap in the round-7 kit.
Also corrected here: Proofs/Inventory.lean's header claimed the audit drivers
were excluded from the compile manifest. They are lines 42-44 of PROOFS.
Certified by a full sweep: both buttons, all four forks, purged trees. 8/8.
2026-08-01 14:10:59 +00:00
# Kept, not just printed: Phase 2c needs the kernel's own declaration count to
# check that the two inventory walks account for every declaration it saw.
KERNLOG = $( mktemp /tmp/check-kernel-XXXX.log)
verification: kernel-side axiom-declaration gate (Phase 2b) + self-test
Phase 1's anti-smuggling check reads source text. Measured today on Lean
v4.30.0-rc2, four distinct declarations compile cleanly and slip past its
anchored pattern:
` axiom cheat : ...` one leading space
`@[simp] axiom cheat : ...` line starts with the attribute
`unsafe axiom cheat : ...` `unsafe` absent from the modifier list
`axiom` <newline> ` cheat` no space follows the keyword
Any of them yields a repository that proves False while the button prints
ALL GREEN. Only the tab variant is blocked, and by Lean, not by us.
Hardening the pattern would fix the exhibited syntax rather than the class,
which is the mistake this estate has made before. Phase 2b stops parsing text
and asks the kernel instead: it reads every compiled Proofs/*.olean with
readModuleData and rejects any declaration that is an axiom.
Design notes:
- reads compiled artifacts rather than importing the modules, because
Proofs.Basic and Proofs.ConstSpecs deliberately reuse `zero_spec` and a
whole-corpus import is impossible by construction;
- membership is self-deriving from the filesystem, so Scalar* and
AxiomCheck are covered too — both are skipped by the CERTS audit and by
the dead-file gate;
- fails closed on absence: a missing .olean would make the scan vacuous, so
the count of compiled modules must equal the count of shipped sources;
- removes its temp source AND artifact on both paths, since a bare `rm`
after the call never runs under `set -e` when the gate goes red — exactly
how this repo accumulated 101 orphan .olean files;
- ~3 s for the whole corpus, against ~53 s for one module-importing run.
Phase 1's grep stays as a fast first line of defence. Phase 2b is the gate
that is load-bearing.
selftest-axgate.sh attacks the shipping gate, lifted out of check.sh at run
time rather than copied. It asserts the specific diagnostic, so a rejection
for an unrelated reason fails too, and it was itself negative-tested: with
the gate's throwError removed, the self-test goes red on exactly that case.
No proof, statement, specification or certificate is touched. No attested
commit is altered — the log binds specific commit hashes, all of which remain
ancestors of HEAD.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-28 16:24:18 +00:00
lake env bash -c "
set -euo pipefail
cd '$HERE/gen' && export LEAN_PATH = \" \$ LEAN_PATH:\$ PWD:$HERE \"
cd '$HERE'
LEAN_TIMEOUT = $TIMEOUT LEAN_MAX_CORES = $CORES '$HERE/lean-guard' '$GATE'
Account for every constant the kernel sees, by set containment
THE GAP. The capability matrix in the control repo — built after the author
answered a capability question by grepping for a FILENAME rather than for the
property, three times in one session — asked whether each repository's auditor
enumerates itself. The four ed25519 forks answered no. Following that up found
something larger: `Proofs/Audit.lean`, the statement-binding driver from P1-a,
is compiled, is a member of the manifest, and was enumerated by NOTHING. The
kernel counted 3058 declarations where the inventory accounted for 3022, and
26 of the 36 missing were its.
THE PROPERTY, now enforced: every constant the kernel sees under this button's
manifest must appear, BY NAME, in either the corpus inventory or the
instruments' own surface. `emitDrivers` in InventoryCore walks the audit
modules and fails closed on an axiom (which would widen the trusted base
outside every cone) or on a standalone claim (which no certificate covers and
no allowlist pins), while admitting the obligations the elaborator generates
for a definition declared alongside it.
TWO WRONG FORMULATIONS FIRST, both recorded because the second is instructive:
· `kernel = corpus + instruments + N_DRIVERS`, where the last term was
justified as a per-driver "self-observation blind spot". It fitted dalek
and anza (2 drivers, residual 2) and broke on risc0 and betrusted
(1 driver, residual 2). The residual is 2 everywhere and has nothing to do
with drivers. This was curve-fitting from a sample of one, and it was named
as the highest-risk claim in the round-7 self-assessment BEFORE the data
refuted it.
· distinct-by-name counting, which collapses `CurveFieldProofs.zero_spec` —
a name that genuinely denotes two different declarations, in Proofs.Basic
and Proofs.ConstSpecs, walked by two drivers with separate environments.
THE MEASURED CAUSE of the residual. Lean materialises equation lemmas lazily,
when something forces an unfold, and each module that forces one gets its own
copy in its object file. `CurveFieldProofs.denote.eq_1` sits in both
SubNegSpec.olean and ConstSpecs.olean; `CurveFieldProofs.limbsVal.eq_1` in both
ReduceSpec.olean and ConstSpecs.olean. The kernel gate reads object files and
counts both copies; the environment holds one constant per name. Counts cannot
relate those two views in either direction — so the check compares SETS, which
is the idiom the rest of this estate already uses, and no constant remains that
could be widened to make a red run green.
Negative-tested: with the instrument walk disabled, the check names
Proofs.Audit's declarations as unaccounted.
ANZA also lacked one allowlist row, `subtle.Choice...from.eq_1`, the same
lazy-materialisation effect seen from the other side. Verified rather than
assumed before adding it: the parent is declared in gen/CurveField/
FunsExternal.lean — the model, pinned by bytes and not inventoried by
declaration — the lemma materialised in Proofs.CompressSpec which forced the
unfold, and all three other forks carry the lemma row while none carries the
parent.
CONSEQUENCE WORTH DISCLOSING: the audited declaration surface is not purely a
function of the corpus source. It depends on which proofs forced which
unfolds. This is now a known gap in the round-7 kit.
Also corrected here: Proofs/Inventory.lean's header claimed the audit drivers
were excluded from the compile manifest. They are lines 42-44 of PROOFS.
Certified by a full sweep: both buttons, all four forks, purged trees. 8/8.
2026-08-01 14:10:59 +00:00
" 2>&1 | tee " $KERNLOG " || GATE_RC= ${ PIPESTATUS [0] }
verification: kernel-side axiom-declaration gate (Phase 2b) + self-test
Phase 1's anti-smuggling check reads source text. Measured today on Lean
v4.30.0-rc2, four distinct declarations compile cleanly and slip past its
anchored pattern:
` axiom cheat : ...` one leading space
`@[simp] axiom cheat : ...` line starts with the attribute
`unsafe axiom cheat : ...` `unsafe` absent from the modifier list
`axiom` <newline> ` cheat` no space follows the keyword
Any of them yields a repository that proves False while the button prints
ALL GREEN. Only the tab variant is blocked, and by Lean, not by us.
Hardening the pattern would fix the exhibited syntax rather than the class,
which is the mistake this estate has made before. Phase 2b stops parsing text
and asks the kernel instead: it reads every compiled Proofs/*.olean with
readModuleData and rejects any declaration that is an axiom.
Design notes:
- reads compiled artifacts rather than importing the modules, because
Proofs.Basic and Proofs.ConstSpecs deliberately reuse `zero_spec` and a
whole-corpus import is impossible by construction;
- membership is self-deriving from the filesystem, so Scalar* and
AxiomCheck are covered too — both are skipped by the CERTS audit and by
the dead-file gate;
- fails closed on absence: a missing .olean would make the scan vacuous, so
the count of compiled modules must equal the count of shipped sources;
- removes its temp source AND artifact on both paths, since a bare `rm`
after the call never runs under `set -e` when the gate goes red — exactly
how this repo accumulated 101 orphan .olean files;
- ~3 s for the whole corpus, against ~53 s for one module-importing run.
Phase 1's grep stays as a fast first line of defence. Phase 2b is the gate
that is load-bearing.
selftest-axgate.sh attacks the shipping gate, lifted out of check.sh at run
time rather than copied. It asserts the specific diagnostic, so a rejection
for an unrelated reason fails too, and it was itself negative-tested: with
the gate's throwError removed, the self-test goes red on exactly that case.
No proof, statement, specification or certificate is touched. No attested
commit is altered — the log binds specific commit hashes, all of which remain
ancestors of HEAD.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-28 16:24:18 +00:00
rm -f " $GATE " " ${ GATE %.lean } .olean "
if [ " $GATE_RC " -ne 0 ] ; then
echo "AXIOM SMUGGLING GATE FAILED (kernel-side) — see the error above."
exit 1
fi
verification: pin the whole declaration surface (P1-b)
Phase 2b asks the kernel whether any AXIOM is declared under Proofs/. Phase 3
pins the cones of the named certificates. Between them sat every other
declaration in the corpus — around three thousand of them — and a helper lemma
quietly acquiring a hash oracle in its cone moved nothing either phase looked
at.
Phase 2c closes that. Ported from ltl-accumulator-verified, where a nine-attack
self-test proved a source-regex enumerator evadable by attributed, private,
indented and `instance` declarations and by a nested-namespace basename
collision. Reading the compiled environment sees what the kernel saw; no name
shape hides. Every constant contributes module, name, kind and full axiom cone,
and the observed set must equal inventory-allowlist.txt exactly in BOTH
directions, with a count trailer so a truncated run cannot pass as an empty
diff.
FOUR THINGS THIS BUILD GOT WRONG, each caught by a check rather than by review:
- The number of inventory drivers is a per-repo FACT, not an assumption.
dalek and anza cannot import their corpus as one environment (Proofs.Basic
and Proofs.ConstSpecs both declare CurveFieldProofs.zero_spec); risc0 and
betrusted have no Proofs.Basic at all. Determined by compiling a probe.
check.sh now DISCOVERS its drivers from the filesystem instead of naming
two, and the generator refuses to split out a module the repo lacks.
- The split let one real declaration hide behind another's entry. Keyed on
name alone, the two zero_specs produced byte-identical records, so 3022
declarations were covered by 3021 allowlist entries. Caught by the count
trailer. Every record now carries its originating module.
- The gate's success line said "single sanctioned axiom", inherited from the
accumulator's policy. This corpus permits NONE. A success message
describing a different rule is how an assertion stops meaning anything.
- selftest-axgate.sh lifted Phase 2b with a range ending at "Phase 3", so
inserting Phase 2c between them made it swallow the new phase and die on
variables only check.sh defines — surfacing as the BASELINE case failing,
a self-test blaming a gate for its own extraction bug. Both self-tests now
stop at the next phase marker whatever it is called, and refuse to run if
they capture more than one phase. The guard is the fix; the range was the
symptom.
WHAT THIS IS NOT, recorded in TRUSTED-BASE.md at the same length as the claim:
- No independent cone walker. The accumulator cross-checks collectAxioms
against a hand-written walker. Ported here it was wrong in BOTH directions
on mathlib's inductive shapes: EdPoint gave [] against the kernel's three
axioms, and once extended, ProjPoint gave three against the kernel's none.
Two implementations disagreeing both ways are a second wrong answer, not a
check. These cones rest on collectAxioms alone.
- Thirteen Proofs/Scalar* modules are inventoried by nothing — the
second-button seam, still open. Phase 2c names every uncovered module on
every run so the omission is visible rather than inferred.
selftest-inventory.sh exercises the shipping gate with six cases, each
asserting a specific diagnostic, including the one that matters: a cone
widened by one oracle while name, module and kind stay put. Negative-tested by
disabling the gate's diff, which turns two cases red including one for the
wrong reason, correctly reported as such.
Verified green: 20 runs across the four repositories (four buttons, four
harness, four inventory, four axgate, four binding self-tests), zero red. The
four check-scalar.sh greens from the preceding sweep stand: that script neither
reads the pin file nor changed.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-29 23:20:15 +00:00
# ── Phase 2c: environment-derived declaration inventory ─────────────────────
# WHAT THIS ADDS over Phase 2b. Phase 2b asks the kernel whether any AXIOM is
# declared under Proofs/. It says nothing about the ~3000 other declarations:
# a `def` or `theorem` whose cone quietly acquired an oracle, a declaration
# renamed, added or removed, or a compiler-generated auxiliary that changed
# shape, all pass 2b unremarked.
#
# This phase pins the whole surface. Every constant originating in an audited
# module contributes NAME, MODULE, KIND and full AXIOM CONE, and the observed
# set must equal inventory-allowlist.txt EXACTLY, both directions:
# UNCLASSIFIED (in the environment, not allowlisted) and STALE (allowlisted,
# not in the environment) are both build failures.
#
# PORTED from ltl-accumulator-verified, where a nine-attack self-test proved a
# source-regex enumerator evadable by attributed, private, indented and
# `instance` declarations and by a nested-namespace basename collision.
#
# TWO DRIVERS, because this corpus cannot be imported as one environment:
# Proofs.Basic and Proofs.ConstSpecs both declare CurveFieldProofs.zero_spec.
# The records carry their originating module precisely so those two remain
# distinct entries — keyed on name alone they were byte-identical, and the
# merged allowlist covered 3022 declarations with 3021 entries.
echo "=== Phase 2c: environment-derived declaration inventory ==="
INVFAIL = 0
INVLOG = $( mktemp /tmp/check-inv-XXXX.log)
cd " $AENEAS_LEAN "
# The DRIVERS are discovered, not listed: whether this corpus needs one or two
# is a per-repo fact (dalek and anza cannot import Proofs.Basic together with
# Proofs.ConstSpecs; risc0 and betrusted have no Proofs.Basic at all). A
# hardcoded pair would silently look for a file that does not exist here.
DRIVERS = $( ls " $HERE " /Proofs/Inventory*.lean 2>/dev/null | xargs -r -n1 basename \
verification: close the two-button seam and level up the scalar button (P0-b)
THE SEAM. This repository is checked by two scripts, and until now neither
asserted anything about the other's scope. check.sh's dead-file gate simply
SKIPPED anything named Scalar*, so a new Proofs/ScalarX.lean was gated by
nothing at all: absent from one manifest by exemption, from the other by
omission, compiled by neither, inventoried by neither. Each button now reads
the other's manifest and requires every shipped proof source to belong to
EXACTLY ONE of them — neither orphaned nor double-claimed, both directions,
plus a phantom check on entries naming files that do not exist. Negative-tested
four ways, including the exact hole this item names.
THE SCALAR BUTTON. Closing the seam exposed it as the estate's weakest link,
having been left behind by every hardening round while the main button gained
five phases. 45 lines to 227:
- source-integrity check over its sources;
- harness-pin verification, so running THIS button alone is protected and not
only running it after check.sh;
- a kernel-side axiom-declaration gate over the compiled artifacts, replacing
a source-text grep that is evadable four ways on v4.30.0-rc2;
- a declaration inventory of ~1880 constants against its own allowlist,
diffed both directions with a count trailer. These 13 modules were the only
part of the proof corpus with no inventory: check.sh Phase 2c named them as
uncovered on every run, and now names the button that covers them instead;
- per-certificate exact-cone assertions replacing `-eq 13` over matching
output lines. A count cannot say WHICH certificate is clean and passes just
as happily if one cone is reported twice.
Every fork-specific fact was read from the existing script rather than assumed:
risc0 and betrusted audit sub_loop1_one_spec where dalek and anza audit
cond_add_l_one_spec, untouched.
THREE BUGS, ONE ROOT CAUSE, all found by the gates rather than by review. Each
reasoned about how a thing is SPELLED instead of what it BELONGS TO, and the
corpus punished each: Proofs/ScalarPackSpec.lean is named like the scalar layer
and owned by the main button.
- the scalar dead-file gate globbed Scalar* and demanded ScalarPackSpec be
scalar-owned. REMOVED rather than special-cased: the seam check tests
membership in exactly one manifest, which is strictly stronger than any
prefix;
- the scalar axiom gate scanned Scalar*.olean, reporting "14 modules" for a
13-module manifest. On a tree where check.sh had not run that artifact is
absent and the button would have failed for a false reason. It now scans
the manifest by membership and fails closed on a missing artifact;
- Phase 2c's driver discovery globbed Inventory*.lean and claimed the other
button's driver, then correctly complained its own manifest lacked those
modules.
This is the family the campaign began with: a source-text axiom grep reasoning
about spelling. Recorded in TRUSTED-BASE.md because it generalises.
Also fixed: the first negative test of the scalar gate's absence check passed
for the wrong reason — the button recompiles before the gate runs, so removing
an artifact merely caused it to be rebuilt. Retested against the lifted phase,
where absence is a persistent condition.
Verified green: 24 runs across the four repositories — four main buttons, four
scalar buttons, and sixteen self-tests — zero red.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-30 10:30:26 +00:00
| sed 's/\.lean$//' | grep -vE '^(InventoryCore|InventoryScalar)$' | sort)
# InventoryScalar belongs to check-scalar.sh, which compiles the modules it
# covers. Globbing Inventory*.lean swept it in here, after which this phase
# correctly complained that its own manifest lacks the scalar modules.
verification: pin the whole declaration surface (P1-b)
Phase 2b asks the kernel whether any AXIOM is declared under Proofs/. Phase 3
pins the cones of the named certificates. Between them sat every other
declaration in the corpus — around three thousand of them — and a helper lemma
quietly acquiring a hash oracle in its cone moved nothing either phase looked
at.
Phase 2c closes that. Ported from ltl-accumulator-verified, where a nine-attack
self-test proved a source-regex enumerator evadable by attributed, private,
indented and `instance` declarations and by a nested-namespace basename
collision. Reading the compiled environment sees what the kernel saw; no name
shape hides. Every constant contributes module, name, kind and full axiom cone,
and the observed set must equal inventory-allowlist.txt exactly in BOTH
directions, with a count trailer so a truncated run cannot pass as an empty
diff.
FOUR THINGS THIS BUILD GOT WRONG, each caught by a check rather than by review:
- The number of inventory drivers is a per-repo FACT, not an assumption.
dalek and anza cannot import their corpus as one environment (Proofs.Basic
and Proofs.ConstSpecs both declare CurveFieldProofs.zero_spec); risc0 and
betrusted have no Proofs.Basic at all. Determined by compiling a probe.
check.sh now DISCOVERS its drivers from the filesystem instead of naming
two, and the generator refuses to split out a module the repo lacks.
- The split let one real declaration hide behind another's entry. Keyed on
name alone, the two zero_specs produced byte-identical records, so 3022
declarations were covered by 3021 allowlist entries. Caught by the count
trailer. Every record now carries its originating module.
- The gate's success line said "single sanctioned axiom", inherited from the
accumulator's policy. This corpus permits NONE. A success message
describing a different rule is how an assertion stops meaning anything.
- selftest-axgate.sh lifted Phase 2b with a range ending at "Phase 3", so
inserting Phase 2c between them made it swallow the new phase and die on
variables only check.sh defines — surfacing as the BASELINE case failing,
a self-test blaming a gate for its own extraction bug. Both self-tests now
stop at the next phase marker whatever it is called, and refuse to run if
they capture more than one phase. The guard is the fix; the range was the
symptom.
WHAT THIS IS NOT, recorded in TRUSTED-BASE.md at the same length as the claim:
- No independent cone walker. The accumulator cross-checks collectAxioms
against a hand-written walker. Ported here it was wrong in BOTH directions
on mathlib's inductive shapes: EdPoint gave [] against the kernel's three
axioms, and once extended, ProjPoint gave three against the kernel's none.
Two implementations disagreeing both ways are a second wrong answer, not a
check. These cones rest on collectAxioms alone.
- Thirteen Proofs/Scalar* modules are inventoried by nothing — the
second-button seam, still open. Phase 2c names every uncovered module on
every run so the omission is visible rather than inferred.
selftest-inventory.sh exercises the shipping gate with six cases, each
asserting a specific diagnostic, including the one that matters: a cone
widened by one oracle while name, module and kind stay put. Negative-tested by
disabling the gate's diff, which turns two cases red including one for the
wrong reason, correctly reported as such.
Verified green: 20 runs across the four repositories (four buttons, four
harness, four inventory, four axgate, four binding self-tests), zero red. The
four check-scalar.sh greens from the preceding sweep stand: that script neither
reads the pin file nor changed.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-29 23:20:15 +00:00
if [ -z " $DRIVERS " ] ; then
echo " NO INVENTORY DRIVER FOUND — the audit surface would go unchecked." ; exit 1
fi
N_DRIVERS = $( printf '%s\n' " $DRIVERS " | grep -c .)
for drv in $DRIVERS ; do
lake env bash -c "
set -uo pipefail
cd '$HERE/gen' && export LEAN_PATH = \" \$ LEAN_PATH:\$ PWD:$HERE \"
cd '$HERE'
LEAN_TIMEOUT = $TIMEOUT LEAN_MEM_MB = 8192 '$HERE/lean-guard' Proofs/$drv .lean
" >> " $INVLOG " 2>&1 || { cat " $INVLOG "; echo " INVENTORY COMPILE FAILED ( $drv ) "; rm -f " $INVLOG " ; exit 1; }
done
# Reconcile the two trailers into one. Summing them and comparing against the
# lines actually collected preserves the integrity property in the presence of
# the split: truncation in EITHER driver shows up as a mismatch.
N_TRAILERS = $( grep -c '^INV-COUNT|' " $INVLOG " )
if [ " $N_TRAILERS " -ne " $N_DRIVERS " ] ; then
echo " INVENTORY INCOMPLETE: expected a count trailer from each of the $N_DRIVERS driver(s), saw $N_TRAILERS "
INVFAIL = 1
fi
SUM = $( grep '^INV-COUNT|' " $INVLOG " | cut -d'|' -f2 | paste -sd+ - | bc)
OBS = $( mktemp /tmp/check-inv-obs-XXXX.log)
grep '^INV|' " $INVLOG " > " $OBS "
echo " INV-COUNT| ${ SUM :- 0 } " >> " $OBS "
" $HERE /inventory_gate.sh " " $OBS " " $HERE /inventory-allowlist.txt " || INVFAIL = 1
Account for every constant the kernel sees, by set containment
THE GAP. The capability matrix in the control repo — built after the author
answered a capability question by grepping for a FILENAME rather than for the
property, three times in one session — asked whether each repository's auditor
enumerates itself. The four ed25519 forks answered no. Following that up found
something larger: `Proofs/Audit.lean`, the statement-binding driver from P1-a,
is compiled, is a member of the manifest, and was enumerated by NOTHING. The
kernel counted 3058 declarations where the inventory accounted for 3022, and
26 of the 36 missing were its.
THE PROPERTY, now enforced: every constant the kernel sees under this button's
manifest must appear, BY NAME, in either the corpus inventory or the
instruments' own surface. `emitDrivers` in InventoryCore walks the audit
modules and fails closed on an axiom (which would widen the trusted base
outside every cone) or on a standalone claim (which no certificate covers and
no allowlist pins), while admitting the obligations the elaborator generates
for a definition declared alongside it.
TWO WRONG FORMULATIONS FIRST, both recorded because the second is instructive:
· `kernel = corpus + instruments + N_DRIVERS`, where the last term was
justified as a per-driver "self-observation blind spot". It fitted dalek
and anza (2 drivers, residual 2) and broke on risc0 and betrusted
(1 driver, residual 2). The residual is 2 everywhere and has nothing to do
with drivers. This was curve-fitting from a sample of one, and it was named
as the highest-risk claim in the round-7 self-assessment BEFORE the data
refuted it.
· distinct-by-name counting, which collapses `CurveFieldProofs.zero_spec` —
a name that genuinely denotes two different declarations, in Proofs.Basic
and Proofs.ConstSpecs, walked by two drivers with separate environments.
THE MEASURED CAUSE of the residual. Lean materialises equation lemmas lazily,
when something forces an unfold, and each module that forces one gets its own
copy in its object file. `CurveFieldProofs.denote.eq_1` sits in both
SubNegSpec.olean and ConstSpecs.olean; `CurveFieldProofs.limbsVal.eq_1` in both
ReduceSpec.olean and ConstSpecs.olean. The kernel gate reads object files and
counts both copies; the environment holds one constant per name. Counts cannot
relate those two views in either direction — so the check compares SETS, which
is the idiom the rest of this estate already uses, and no constant remains that
could be widened to make a red run green.
Negative-tested: with the instrument walk disabled, the check names
Proofs.Audit's declarations as unaccounted.
ANZA also lacked one allowlist row, `subtle.Choice...from.eq_1`, the same
lazy-materialisation effect seen from the other side. Verified rather than
assumed before adding it: the parent is declared in gen/CurveField/
FunsExternal.lean — the model, pinned by bytes and not inventoried by
declaration — the lemma materialised in Proofs.CompressSpec which forced the
unfold, and all three other forks carry the lemma row while none carries the
parent.
CONSEQUENCE WORTH DISCLOSING: the audited declaration surface is not purely a
function of the corpus source. It depends on which proofs forced which
unfolds. This is now a known gap in the round-7 kit.
Also corrected here: Proofs/Inventory.lean's header claimed the audit drivers
were excluded from the compile manifest. They are lines 42-44 of PROOFS.
Certified by a full sweep: both buttons, all four forks, purged trees. 8/8.
2026-08-01 14:10:59 +00:00
verification: derive lift dependencies instead of hand-keeping them
Round-9 swept all ten instruments per fork instead of only the two buttons,
and found selftest-axgate.sh red in all four. Root cause, identical to the
KERNLOG defect fixed the day before: a self-test lifts one phase out of
check.sh and supplies its variables from a HAND-WRITTEN preamble, and the
phase later grew a dependency nobody told the preamble about.
Phase 2b stopped globbing Proofs/*.olean and started reading $PROOFS by
membership. Bash does not error on an unset array under `set -u` — it
expands to nothing — so the gate silently received
expected := [".olean"]
one entry with an empty name, and rejected the baseline via its own
fail-closed absence check. Exit code right, reason wrong.
· lift-guard.sh (new, pinned): derives every variable the lifted payload
reads, subtracts what the driver defines, and fails AT LIFT TIME naming
the remainder. Wired into all five lifting self-tests; selftest-shapes.sh
drops its inline copy. One implementation, not five, since drifting out
of sync is the entire failure mode.
· selftest-axgate.sh: lifts PROOFS verbatim, and its case 2 now poisons a
MANIFESTED leaf module rather than adding a stray file. The stray-file
attack was a no-op against membership semantics — that is the dead-file
gate's job, proven by selftest-harness case 8 — and it is also the
weaker attack, since adding files to Proofs/ must clear a gate that
editing an already-manifested module does not.
· Phase 2c's accounting identity moves behind its own marker with its own
ACCTFAIL verdict, so the phase is liftable by construction rather than
by a self-test knowing where to stop. Truncating the lift range alone
would have dropped Phase 2c's own verdict and left the test unable to fail.
· The other four lifting self-tests assert on the PAYLOAD rather than the
assembled driver, so a marker in the preamble cannot satisfy a check
meant to prove the lift landed.
Certified: 8/8 self-tests green in all four forks (~212 assertions, none
failing); check.sh bytes unchanged and still matching the pin written before
the 3h08m round-9 sweep, whose 36 GREEN button rows therefore stand.
--audit-only re-run against the new HARNESS.sha256 in every fork.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-02 11:07:28 +00:00
# The drivers' corpus lists must together BE the compile manifest, minus the
# audit infrastructure and the scalar layer. Checked in both directions so a
# module cannot fall between the two drivers, and NO SILENT TRUNCATION: what
# this phase does not cover is named on stdout every run.
COVERED = $( for d in $DRIVERS ; do grep -ohE '`Proofs\.[A-Za-z0-9]+' " $HERE /Proofs/ $d .lean " ; done \
| sed 's/`Proofs\.//' | sort -u)
for m in " ${ PROOFS [@] } " ; do
case " $m " in Audit| Inventory| InventoryBasic| InventoryCore) continue ; ; esac
grep -qx " $m " <<< " $COVERED " || { echo " UNINVENTORIED: $m is compiled by this script but no driver covers it " ; INVFAIL = 1; }
done
while read -r m; do
[ -z " $m " ] && continue
case " ${ PROOFS [*] } " in ( *" $m " *) ; ; ( *) echo " PHANTOM: driver claims $m , which this script does not compile " ; INVFAIL = 1; ; esac
done <<< " $COVERED "
for f in " $HERE " /Proofs/*.lean; do
b = $( basename " $f " .lean)
case " $b " in Audit| Inventory| InventoryBasic| InventoryCore| InventoryScalar) continue ; ; esac
# Since P0-b the scalar layer IS inventoried, by check-scalar.sh Phase 2c
# against inventory-allowlist-scalar.txt. Say which button covers it rather
# than only that this one does not: "not here" reads like a gap when it is a
# division of labour, and read like a gap it would eventually be treated as one.
if ! grep -qx " $b " <<< " $COVERED " ; then
if grep -qx " $b " <<< " $SCALAR_MANIFEST " ; then
echo " covered by check-scalar.sh Phase 2c: Proofs/ $b .lean "
else
echo " NOT INVENTORIED BY ANY BUTTON: Proofs/ $b .lean " ; INVFAIL = 1
fi
fi
done
[ " $INVFAIL " = 0 ] || { echo "INVENTORY COVERAGE FAILED" ; exit 1; }
# ── Phase 2c-accounting: every kernel constant is accounted for ─────────────
# SEPARATED FROM PHASE 2c DELIBERATELY, and the reason is a self-test that
# could not pass (round-7 finding F5). This block reads $KERNLOG, created one
# phase earlier in Phase 2b. selftest-shapes.sh lifts "Phase 2c" by text marker
# and runs it standalone; once this block lived inside that range, the lifted
# driver died on its first `$KERNLOG` expansion under `set -u`. The test failed
# loudly in all four forks from the moment the block was added — so the shapes
# property went unverified, though it never produced a false green.
#
# Truncating the lift is NOT the fix: Phase 2c's own verdict
# (`INVENTORY COVERAGE FAILED`) sits after this block, so a shorter range drops
# the phase's ability to fail at all. Instead the block gets its own marker and
# its own verdict, which makes Phase 2c liftable BY CONSTRUCTION rather than by
# the self-test knowing where to stop.
Account for every constant the kernel sees, by set containment
THE GAP. The capability matrix in the control repo — built after the author
answered a capability question by grepping for a FILENAME rather than for the
property, three times in one session — asked whether each repository's auditor
enumerates itself. The four ed25519 forks answered no. Following that up found
something larger: `Proofs/Audit.lean`, the statement-binding driver from P1-a,
is compiled, is a member of the manifest, and was enumerated by NOTHING. The
kernel counted 3058 declarations where the inventory accounted for 3022, and
26 of the 36 missing were its.
THE PROPERTY, now enforced: every constant the kernel sees under this button's
manifest must appear, BY NAME, in either the corpus inventory or the
instruments' own surface. `emitDrivers` in InventoryCore walks the audit
modules and fails closed on an axiom (which would widen the trusted base
outside every cone) or on a standalone claim (which no certificate covers and
no allowlist pins), while admitting the obligations the elaborator generates
for a definition declared alongside it.
TWO WRONG FORMULATIONS FIRST, both recorded because the second is instructive:
· `kernel = corpus + instruments + N_DRIVERS`, where the last term was
justified as a per-driver "self-observation blind spot". It fitted dalek
and anza (2 drivers, residual 2) and broke on risc0 and betrusted
(1 driver, residual 2). The residual is 2 everywhere and has nothing to do
with drivers. This was curve-fitting from a sample of one, and it was named
as the highest-risk claim in the round-7 self-assessment BEFORE the data
refuted it.
· distinct-by-name counting, which collapses `CurveFieldProofs.zero_spec` —
a name that genuinely denotes two different declarations, in Proofs.Basic
and Proofs.ConstSpecs, walked by two drivers with separate environments.
THE MEASURED CAUSE of the residual. Lean materialises equation lemmas lazily,
when something forces an unfold, and each module that forces one gets its own
copy in its object file. `CurveFieldProofs.denote.eq_1` sits in both
SubNegSpec.olean and ConstSpecs.olean; `CurveFieldProofs.limbsVal.eq_1` in both
ReduceSpec.olean and ConstSpecs.olean. The kernel gate reads object files and
counts both copies; the environment holds one constant per name. Counts cannot
relate those two views in either direction — so the check compares SETS, which
is the idiom the rest of this estate already uses, and no constant remains that
could be widened to make a red run green.
Negative-tested: with the instrument walk disabled, the check names
Proofs.Audit's declarations as unaccounted.
ANZA also lacked one allowlist row, `subtle.Choice...from.eq_1`, the same
lazy-materialisation effect seen from the other side. Verified rather than
assumed before adding it: the parent is declared in gen/CurveField/
FunsExternal.lean — the model, pinned by bytes and not inventoried by
declaration — the lemma materialised in Proofs.CompressSpec which forced the
unfold, and all three other forks carry the lemma row while none carries the
parent.
CONSEQUENCE WORTH DISCLOSING: the audited declaration surface is not purely a
function of the corpus source. It depends on which proofs forced which
unfolds. This is now a known gap in the round-7 kit.
Also corrected here: Proofs/Inventory.lean's header claimed the audit drivers
were excluded from the compile manifest. They are lines 42-44 of PROOFS.
Certified by a full sweep: both buttons, all four forks, purged trees. 8/8.
2026-08-01 14:10:59 +00:00
# ── THE ACCOUNTING IDENTITY ───────────────────────────────────────────────
# Every declaration the kernel saw must be accounted for by exactly one walk:
# the corpus inventory, or the instruments' own surface. Until 2026-07-31 the
# two numbers were never compared — the kernel reported 3058 across this
# button's manifest, the inventory accounted for 3022, and the 36-declaration
# difference was the audit drivers' own machinery, covered by no allowlist row
# and by no other check. It was not a soundness hole (the drivers ARE in the
# manifest, so Phase 2b's kernel gate rejects an axiom in one whatever its
# indentation) but it was an unexamined remainder, and an unexamined remainder
# is where the next defect hides.
#
# Stating it as an IDENTITY rather than as two separate counts is what makes it
# fail closed: a declaration that slipped out of both walks leaves the sum
# short, and one counted twice leaves it long.
#
# COUNT DISTINCT CONSTANTS, NOT PHYSICAL DECLARATIONS. The two sides of this
# identity were, at first, counting different things, and the gap was papered
# over with a `+ N_DRIVERS` term justified as a "self-observation blind spot".
# That explanation was WRONG. It fitted dalek and anza (2 drivers, residual 2)
# and broke on risc0 and betrusted (1 driver, residual 2) — the residual is 2
# everywhere and has nothing to do with drivers.
#
# The measured cause: Lean materialises equation lemmas LAZILY, when something
# forces an unfold, and each module that forces one gets its own copy in its
# object file. On every fork, `CurveFieldProofs.denote.eq_1` sits in both
# `SubNegSpec.olean` and `ConstSpecs.olean`, and `CurveFieldProofs.limbsVal.eq_1`
# in both `ReduceSpec.olean` and `ConstSpecs.olean`. The kernel gate reads each
# object file separately and counts both copies; the environment holds one
# constant per name and the inventory sees it once. Hence exactly 2.
#
# So the gate now reports DISTINCT names and the fudge term is gone. This still
# fails closed: a declaration missing from both walks leaves the sum short, and
# one counted twice leaves it long. A future mismatch must be explained — as
# this one finally was — never absorbed into a constant.
audit: bind the scalar statements, and make the accounting identity mean audit
Closes four round-7/8 findings. Certified by the round-12 sweep: five
repositories, both buttons and every self-test, 48/48 GREEN.
── `scalar-statements-unbound` (gpt, round 7, CRITICAL) ────────────────────
The main button bound its 31 certificates' elaborated statements and reachable
specification bodies. This button bound NONE of its thirteen, while
TRUSTED-BASE item 8 said the audit covers "every certificate" — false across
the 44-certificate surface. The finding was raised in round 7, lost from the
round-8 work list by an F-number collision between two reviewers, and re-raised
in round 8.
Proofs/ScalarAudit.lean is generated from each fork's OWN Audit.lean, so the
canonicalisation is provably the same code: pp.all rendering, whitespace
normalisation, transitive specification closure. check-scalar.sh Phase 3c pins
the block's digest, requires the committed copy to match byte-for-byte so a
mismatch can be DIFFED, and cross-checks the auditor's certificate set against
the button's CERTS array.
dalek ecf3a3f8 · anza 0d942e47 · risc0 4b550a61 · betrusted 4b550a61
risc0 and betrusted share a digest and that is correct, not a collision: their
ScalarSubSpec.lean differs only in doc prose and in `black_box` entries inside
`simp only [...]` lists AFTER `:= by`. Proof scripts. They bind the same
statements over the same specifications, which is the documented scope.
selftest-scalar-statements.sh ships the two attacks the reviewer asked for:
ok gutted statement caught (cone unchanged)
ok rewritten specification body caught (name and cone unchanged)
The second rewrites a reachable reference body to `id (…)` — DEFINITIONALLY
EQUAL, so the corpus compiles and every proof typechecks and the cone is
byte-identical. Every earlier phase is blind to it.
── `drv-surface-no-cones` + `accounting-certifies-enumeration` (claude) ────
The round-7 accounting identity proved every kernel constant was ENUMERATED.
The reviewer showed enumeration is not audit: their planted claim WAS
enumerated, as DRV|LTLAccAudit.bait.smuggled|theorem with a real cone, and
nothing examined it — rows had no cone, no allowlist covered them, the
statement digest does not reach instruments, and Phase 2b gates DECLARED
AXIOMS, a different question. "Progress of one step, not two."
DRV rows now carry their axiom cone and are pinned in driver-allowlist.txt by
inventory_gate.sh with a DRV tag — the same implementation that pins the
corpus, in both directions, because a second copy of a coverage gate is a
second thing to drift. The axiom policy is per-surface and enforced per
surface: the corpus admits exactly the sanctioned boundary, the instruments
admit none, and an instrument axiom fails EVEN WHEN ALLOWLISTED.
Verified with the reviewer's own payload, both placements:
before the walk -> UNCLASSIFIED: DRV|…|bait.smuggled|theorem|Classical.choice,Quot.sound,propext
after the walk -> ACCOUNTING FAILED names it (kernel-side)
── `drv-naming-heuristic` (claude, round 7) ────────────────────────────────
Retired as load-bearing rather than patched. The rule admits a theorem whose
name extends a constant declared alongside it, and "breaks in one line" —
declare `def bait`, then `theorem bait.smuggled` walks through. It stays as a
fast readable first check; membership in a committed allowlist is what now
carries the weight, and a new row fails closed whatever it is called.
── what round 11 caught, which was mine ───────────────────────────────────
DRV rows first shipped WITHOUT their originating driver. dalek and anza run
two drivers, each declaring its own `corpus`; keyed on name alone those two
distinct declarations produced one byte-identical row, `sort -u` collapsed
them, and the trailers summed to 37 against 36. The estate had already learned
this on the corpus walk — INV rows carry their module because two modules both
declare CurveFieldProofs.zero_spec — and I rebuilt the record without it.
Rows now carry their driver, and the gate FAILS CLOSED ON DUPLICATE RECORDS
naming the collision: two declarations sharing one entry means one is covered
by the other's, which is exactly how a real declaration hides. The trailer
now checks what the drivers EMITTED, not what survives de-duplication —
conflating "the run was truncated" with "two rows were identical" is what let
a record-format defect present itself as an arithmetic complaint.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-03 10:15:26 +00:00
# PIN THE INSTRUMENTS' OWN SURFACE, in both directions, with the SAME gate the
# corpus uses (round-8 review, Claude, register keys `drv-surface-no-cones`,
# `accounting-certifies-enumeration`, and it retires `drv-naming-heuristic` as
# load-bearing).
#
# The accounting identity below proves every kernel constant is ENUMERATED by
# one of the two walks. The reviewer demonstrated that enumeration is not
# audit: their planted claim WAS enumerated, carried a real axiom cone, and
# nothing examined it — DRV rows had no cone and no allowlist covered them.
# They now carry the cone, and this gate pins them exactly as the corpus is, so
# a claim smuggled into an instrument is a NEW ROW and a new row fails closed
# whatever it is called.
" $HERE /inventory_gate.sh " " $INVLOG " " $HERE /driver-allowlist.txt " DRV || ACCTFAIL = 1
Account for every constant the kernel sees, by set containment
THE GAP. The capability matrix in the control repo — built after the author
answered a capability question by grepping for a FILENAME rather than for the
property, three times in one session — asked whether each repository's auditor
enumerates itself. The four ed25519 forks answered no. Following that up found
something larger: `Proofs/Audit.lean`, the statement-binding driver from P1-a,
is compiled, is a member of the manifest, and was enumerated by NOTHING. The
kernel counted 3058 declarations where the inventory accounted for 3022, and
26 of the 36 missing were its.
THE PROPERTY, now enforced: every constant the kernel sees under this button's
manifest must appear, BY NAME, in either the corpus inventory or the
instruments' own surface. `emitDrivers` in InventoryCore walks the audit
modules and fails closed on an axiom (which would widen the trusted base
outside every cone) or on a standalone claim (which no certificate covers and
no allowlist pins), while admitting the obligations the elaborator generates
for a definition declared alongside it.
TWO WRONG FORMULATIONS FIRST, both recorded because the second is instructive:
· `kernel = corpus + instruments + N_DRIVERS`, where the last term was
justified as a per-driver "self-observation blind spot". It fitted dalek
and anza (2 drivers, residual 2) and broke on risc0 and betrusted
(1 driver, residual 2). The residual is 2 everywhere and has nothing to do
with drivers. This was curve-fitting from a sample of one, and it was named
as the highest-risk claim in the round-7 self-assessment BEFORE the data
refuted it.
· distinct-by-name counting, which collapses `CurveFieldProofs.zero_spec` —
a name that genuinely denotes two different declarations, in Proofs.Basic
and Proofs.ConstSpecs, walked by two drivers with separate environments.
THE MEASURED CAUSE of the residual. Lean materialises equation lemmas lazily,
when something forces an unfold, and each module that forces one gets its own
copy in its object file. `CurveFieldProofs.denote.eq_1` sits in both
SubNegSpec.olean and ConstSpecs.olean; `CurveFieldProofs.limbsVal.eq_1` in both
ReduceSpec.olean and ConstSpecs.olean. The kernel gate reads object files and
counts both copies; the environment holds one constant per name. Counts cannot
relate those two views in either direction — so the check compares SETS, which
is the idiom the rest of this estate already uses, and no constant remains that
could be widened to make a red run green.
Negative-tested: with the instrument walk disabled, the check names
Proofs.Audit's declarations as unaccounted.
ANZA also lacked one allowlist row, `subtle.Choice...from.eq_1`, the same
lazy-materialisation effect seen from the other side. Verified rather than
assumed before adding it: the parent is declared in gen/CurveField/
FunsExternal.lean — the model, pinned by bytes and not inventoried by
declaration — the lemma materialised in Proofs.CompressSpec which forced the
unfold, and all three other forks carry the lemma row while none carries the
parent.
CONSEQUENCE WORTH DISCLOSING: the audited declaration surface is not purely a
function of the corpus source. It depends on which proofs forced which
unfolds. This is now a known gap in the round-7 kit.
Also corrected here: Proofs/Inventory.lean's header claimed the audit drivers
were excluded from the compile manifest. They are lines 42-44 of PROOFS.
Certified by a full sweep: both buttons, all four forks, purged trees. 8/8.
2026-08-01 14:10:59 +00:00
N_DRV = $( grep -c '^DRV|' " $INVLOG " || true )
DRV_TRAILERS = $( grep -c '^DRV-COUNT|' " $INVLOG " || true )
DRV_SUM = $( grep '^DRV-COUNT|' " $INVLOG " | cut -d'|' -f2 | paste -sd+ - | bc)
KERN_NAMES = $( mktemp /tmp/check-kernnames-XXXX.txt)
ACCT_NAMES = $( mktemp /tmp/check-acctnames-XXXX.txt)
2026-08-04 01:17:05 +00:00
LC_ALL = C grep '^KERNEL-NAME|' " $KERNLOG " | cut -d'|' -f3 | LC_ALL = C sort -u > " $KERN_NAMES "
Account for every constant the kernel sees, by set containment
THE GAP. The capability matrix in the control repo — built after the author
answered a capability question by grepping for a FILENAME rather than for the
property, three times in one session — asked whether each repository's auditor
enumerates itself. The four ed25519 forks answered no. Following that up found
something larger: `Proofs/Audit.lean`, the statement-binding driver from P1-a,
is compiled, is a member of the manifest, and was enumerated by NOTHING. The
kernel counted 3058 declarations where the inventory accounted for 3022, and
26 of the 36 missing were its.
THE PROPERTY, now enforced: every constant the kernel sees under this button's
manifest must appear, BY NAME, in either the corpus inventory or the
instruments' own surface. `emitDrivers` in InventoryCore walks the audit
modules and fails closed on an axiom (which would widen the trusted base
outside every cone) or on a standalone claim (which no certificate covers and
no allowlist pins), while admitting the obligations the elaborator generates
for a definition declared alongside it.
TWO WRONG FORMULATIONS FIRST, both recorded because the second is instructive:
· `kernel = corpus + instruments + N_DRIVERS`, where the last term was
justified as a per-driver "self-observation blind spot". It fitted dalek
and anza (2 drivers, residual 2) and broke on risc0 and betrusted
(1 driver, residual 2). The residual is 2 everywhere and has nothing to do
with drivers. This was curve-fitting from a sample of one, and it was named
as the highest-risk claim in the round-7 self-assessment BEFORE the data
refuted it.
· distinct-by-name counting, which collapses `CurveFieldProofs.zero_spec` —
a name that genuinely denotes two different declarations, in Proofs.Basic
and Proofs.ConstSpecs, walked by two drivers with separate environments.
THE MEASURED CAUSE of the residual. Lean materialises equation lemmas lazily,
when something forces an unfold, and each module that forces one gets its own
copy in its object file. `CurveFieldProofs.denote.eq_1` sits in both
SubNegSpec.olean and ConstSpecs.olean; `CurveFieldProofs.limbsVal.eq_1` in both
ReduceSpec.olean and ConstSpecs.olean. The kernel gate reads object files and
counts both copies; the environment holds one constant per name. Counts cannot
relate those two views in either direction — so the check compares SETS, which
is the idiom the rest of this estate already uses, and no constant remains that
could be widened to make a red run green.
Negative-tested: with the instrument walk disabled, the check names
Proofs.Audit's declarations as unaccounted.
ANZA also lacked one allowlist row, `subtle.Choice...from.eq_1`, the same
lazy-materialisation effect seen from the other side. Verified rather than
assumed before adding it: the parent is declared in gen/CurveField/
FunsExternal.lean — the model, pinned by bytes and not inventoried by
declaration — the lemma materialised in Proofs.CompressSpec which forced the
unfold, and all three other forks carry the lemma row while none carries the
parent.
CONSEQUENCE WORTH DISCLOSING: the audited declaration surface is not purely a
function of the corpus source. It depends on which proofs forced which
unfolds. This is now a known gap in the round-7 kit.
Also corrected here: Proofs/Inventory.lean's header claimed the audit drivers
were excluded from the compile manifest. They are lines 42-44 of PROOFS.
Certified by a full sweep: both buttons, all four forks, purged trees. 8/8.
2026-08-01 14:10:59 +00:00
{ LC_ALL = C awk -F'|' '/^INV\|/{print $3}' " $HERE /inventory-allowlist.txt "
audit: bind the scalar statements, and make the accounting identity mean audit
Closes four round-7/8 findings. Certified by the round-12 sweep: five
repositories, both buttons and every self-test, 48/48 GREEN.
── `scalar-statements-unbound` (gpt, round 7, CRITICAL) ────────────────────
The main button bound its 31 certificates' elaborated statements and reachable
specification bodies. This button bound NONE of its thirteen, while
TRUSTED-BASE item 8 said the audit covers "every certificate" — false across
the 44-certificate surface. The finding was raised in round 7, lost from the
round-8 work list by an F-number collision between two reviewers, and re-raised
in round 8.
Proofs/ScalarAudit.lean is generated from each fork's OWN Audit.lean, so the
canonicalisation is provably the same code: pp.all rendering, whitespace
normalisation, transitive specification closure. check-scalar.sh Phase 3c pins
the block's digest, requires the committed copy to match byte-for-byte so a
mismatch can be DIFFED, and cross-checks the auditor's certificate set against
the button's CERTS array.
dalek ecf3a3f8 · anza 0d942e47 · risc0 4b550a61 · betrusted 4b550a61
risc0 and betrusted share a digest and that is correct, not a collision: their
ScalarSubSpec.lean differs only in doc prose and in `black_box` entries inside
`simp only [...]` lists AFTER `:= by`. Proof scripts. They bind the same
statements over the same specifications, which is the documented scope.
selftest-scalar-statements.sh ships the two attacks the reviewer asked for:
ok gutted statement caught (cone unchanged)
ok rewritten specification body caught (name and cone unchanged)
The second rewrites a reachable reference body to `id (…)` — DEFINITIONALLY
EQUAL, so the corpus compiles and every proof typechecks and the cone is
byte-identical. Every earlier phase is blind to it.
── `drv-surface-no-cones` + `accounting-certifies-enumeration` (claude) ────
The round-7 accounting identity proved every kernel constant was ENUMERATED.
The reviewer showed enumeration is not audit: their planted claim WAS
enumerated, as DRV|LTLAccAudit.bait.smuggled|theorem with a real cone, and
nothing examined it — rows had no cone, no allowlist covered them, the
statement digest does not reach instruments, and Phase 2b gates DECLARED
AXIOMS, a different question. "Progress of one step, not two."
DRV rows now carry their axiom cone and are pinned in driver-allowlist.txt by
inventory_gate.sh with a DRV tag — the same implementation that pins the
corpus, in both directions, because a second copy of a coverage gate is a
second thing to drift. The axiom policy is per-surface and enforced per
surface: the corpus admits exactly the sanctioned boundary, the instruments
admit none, and an instrument axiom fails EVEN WHEN ALLOWLISTED.
Verified with the reviewer's own payload, both placements:
before the walk -> UNCLASSIFIED: DRV|…|bait.smuggled|theorem|Classical.choice,Quot.sound,propext
after the walk -> ACCOUNTING FAILED names it (kernel-side)
── `drv-naming-heuristic` (claude, round 7) ────────────────────────────────
Retired as load-bearing rather than patched. The rule admits a theorem whose
name extends a constant declared alongside it, and "breaks in one line" —
declare `def bait`, then `theorem bait.smuggled` walks through. It stays as a
fast readable first check; membership in a committed allowlist is what now
carries the weight, and a new row fails closed whatever it is called.
── what round 11 caught, which was mine ───────────────────────────────────
DRV rows first shipped WITHOUT their originating driver. dalek and anza run
two drivers, each declaring its own `corpus`; keyed on name alone those two
distinct declarations produced one byte-identical row, `sort -u` collapsed
them, and the trailers summed to 37 against 36. The estate had already learned
this on the corpus walk — INV rows carry their module because two modules both
declare CurveFieldProofs.zero_spec — and I rebuilt the record without it.
Rows now carry their driver, and the gate FAILS CLOSED ON DUPLICATE RECORDS
naming the collision: two declarations sharing one entry means one is covered
by the other's, which is exactly how a real declaration hides. The trailer
now checks what the drivers EMITTED, not what survives de-duplication —
conflating "the run was truncated" with "two rows were identical" is what let
a record-format defect present itself as an arithmetic complaint.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-03 10:15:26 +00:00
LC_ALL = C grep '^DRV|' " $INVLOG " | cut -d'|' -f3
Account for every constant the kernel sees, by set containment
THE GAP. The capability matrix in the control repo — built after the author
answered a capability question by grepping for a FILENAME rather than for the
property, three times in one session — asked whether each repository's auditor
enumerates itself. The four ed25519 forks answered no. Following that up found
something larger: `Proofs/Audit.lean`, the statement-binding driver from P1-a,
is compiled, is a member of the manifest, and was enumerated by NOTHING. The
kernel counted 3058 declarations where the inventory accounted for 3022, and
26 of the 36 missing were its.
THE PROPERTY, now enforced: every constant the kernel sees under this button's
manifest must appear, BY NAME, in either the corpus inventory or the
instruments' own surface. `emitDrivers` in InventoryCore walks the audit
modules and fails closed on an axiom (which would widen the trusted base
outside every cone) or on a standalone claim (which no certificate covers and
no allowlist pins), while admitting the obligations the elaborator generates
for a definition declared alongside it.
TWO WRONG FORMULATIONS FIRST, both recorded because the second is instructive:
· `kernel = corpus + instruments + N_DRIVERS`, where the last term was
justified as a per-driver "self-observation blind spot". It fitted dalek
and anza (2 drivers, residual 2) and broke on risc0 and betrusted
(1 driver, residual 2). The residual is 2 everywhere and has nothing to do
with drivers. This was curve-fitting from a sample of one, and it was named
as the highest-risk claim in the round-7 self-assessment BEFORE the data
refuted it.
· distinct-by-name counting, which collapses `CurveFieldProofs.zero_spec` —
a name that genuinely denotes two different declarations, in Proofs.Basic
and Proofs.ConstSpecs, walked by two drivers with separate environments.
THE MEASURED CAUSE of the residual. Lean materialises equation lemmas lazily,
when something forces an unfold, and each module that forces one gets its own
copy in its object file. `CurveFieldProofs.denote.eq_1` sits in both
SubNegSpec.olean and ConstSpecs.olean; `CurveFieldProofs.limbsVal.eq_1` in both
ReduceSpec.olean and ConstSpecs.olean. The kernel gate reads object files and
counts both copies; the environment holds one constant per name. Counts cannot
relate those two views in either direction — so the check compares SETS, which
is the idiom the rest of this estate already uses, and no constant remains that
could be widened to make a red run green.
Negative-tested: with the instrument walk disabled, the check names
Proofs.Audit's declarations as unaccounted.
ANZA also lacked one allowlist row, `subtle.Choice...from.eq_1`, the same
lazy-materialisation effect seen from the other side. Verified rather than
assumed before adding it: the parent is declared in gen/CurveField/
FunsExternal.lean — the model, pinned by bytes and not inventoried by
declaration — the lemma materialised in Proofs.CompressSpec which forced the
unfold, and all three other forks carry the lemma row while none carries the
parent.
CONSEQUENCE WORTH DISCLOSING: the audited declaration surface is not purely a
function of the corpus source. It depends on which proofs forced which
unfolds. This is now a known gap in the round-7 kit.
Also corrected here: Proofs/Inventory.lean's header claimed the audit drivers
were excluded from the compile manifest. They are lines 42-44 of PROOFS.
Certified by a full sweep: both buttons, all four forks, purged trees. 8/8.
2026-08-01 14:10:59 +00:00
} | LC_ALL = C sort -u > " $ACCT_NAMES "
2026-08-04 01:17:05 +00:00
# TWO QUESTIONS, NOT ONE — round-9 review (Claude, N2), and the measurement
# that answered it.
#
# The reviewer was right that keying this identity on NAME ALONE is weaker than
# it reads: the allowlists are keyed module|name precisely because a name is not
# unique, and this corpus holds two distinct CurveFieldProofs.zero_spec
# declarations. So the pair is the right key — and keying on it revealed why the
# straightforward fix is not available.
#
# 36 kernel pairs in this fork do not match a walk pair, and EVERY ONE of them
# has its name accounted for under a DIFFERENT module. Example:
# kernel: Proofs.ConstSpecs|CurveFieldProofs.denote.eq_1
# kernel: Proofs.SubNegSpec|CurveFieldProofs.denote.eq_1 <- same name twice
# walk: Proofs.SubNegSpec|CurveFieldProofs.denote.eq_1
# That is GPT-5.6's round-7 F8: lazy equation lemmas are materialised PER
# MODULE, so every module forcing an unfold gets its own copy in its object
# file. The kernel reads object files and sees both copies; the environment walk
# reads one merged environment and sees the name once. Both views are correct
# about different things, so a pair mismatch here is not evidence of an
# unexamined declaration, and suppressing it with an exception list would be the
# fudge term four-fork data already refuted once.
#
# So the phase asks both questions and answers them separately:
# UNACCOUNTED a name the kernel holds that NO walk mentions -> FAILS
# MULTI-MODULE a pair that differs only in module attribution -> COUNTED and
# REPORTED, never silently dropped, so the F8 phenomenon is
# visible every run and a change in it is a change a reader sees
KERN_PAIRS = $( mktemp /tmp/check-kernpairs-XXXX.txt)
ACCT_PAIRS = $( mktemp /tmp/check-acctpairs-XXXX.txt)
LC_ALL = C grep '^KERNEL-NAME|' " $KERNLOG " | cut -d'|' -f2,3 | LC_ALL = C sort -u > " $KERN_PAIRS "
{ LC_ALL = C awk -F'|' '/^INV\|/{print $2"|"$3}' " $HERE /inventory-allowlist.txt "
LC_ALL = C grep '^DRV|' " $INVLOG " | cut -d'|' -f2,3
} | LC_ALL = C sort -u > " $ACCT_PAIRS "
MULTIMOD = $( LC_ALL = C comm -23 " $KERN_PAIRS " " $ACCT_PAIRS " | wc -l)
Account for every constant the kernel sees, by set containment
THE GAP. The capability matrix in the control repo — built after the author
answered a capability question by grepping for a FILENAME rather than for the
property, three times in one session — asked whether each repository's auditor
enumerates itself. The four ed25519 forks answered no. Following that up found
something larger: `Proofs/Audit.lean`, the statement-binding driver from P1-a,
is compiled, is a member of the manifest, and was enumerated by NOTHING. The
kernel counted 3058 declarations where the inventory accounted for 3022, and
26 of the 36 missing were its.
THE PROPERTY, now enforced: every constant the kernel sees under this button's
manifest must appear, BY NAME, in either the corpus inventory or the
instruments' own surface. `emitDrivers` in InventoryCore walks the audit
modules and fails closed on an axiom (which would widen the trusted base
outside every cone) or on a standalone claim (which no certificate covers and
no allowlist pins), while admitting the obligations the elaborator generates
for a definition declared alongside it.
TWO WRONG FORMULATIONS FIRST, both recorded because the second is instructive:
· `kernel = corpus + instruments + N_DRIVERS`, where the last term was
justified as a per-driver "self-observation blind spot". It fitted dalek
and anza (2 drivers, residual 2) and broke on risc0 and betrusted
(1 driver, residual 2). The residual is 2 everywhere and has nothing to do
with drivers. This was curve-fitting from a sample of one, and it was named
as the highest-risk claim in the round-7 self-assessment BEFORE the data
refuted it.
· distinct-by-name counting, which collapses `CurveFieldProofs.zero_spec` —
a name that genuinely denotes two different declarations, in Proofs.Basic
and Proofs.ConstSpecs, walked by two drivers with separate environments.
THE MEASURED CAUSE of the residual. Lean materialises equation lemmas lazily,
when something forces an unfold, and each module that forces one gets its own
copy in its object file. `CurveFieldProofs.denote.eq_1` sits in both
SubNegSpec.olean and ConstSpecs.olean; `CurveFieldProofs.limbsVal.eq_1` in both
ReduceSpec.olean and ConstSpecs.olean. The kernel gate reads object files and
counts both copies; the environment holds one constant per name. Counts cannot
relate those two views in either direction — so the check compares SETS, which
is the idiom the rest of this estate already uses, and no constant remains that
could be widened to make a red run green.
Negative-tested: with the instrument walk disabled, the check names
Proofs.Audit's declarations as unaccounted.
ANZA also lacked one allowlist row, `subtle.Choice...from.eq_1`, the same
lazy-materialisation effect seen from the other side. Verified rather than
assumed before adding it: the parent is declared in gen/CurveField/
FunsExternal.lean — the model, pinned by bytes and not inventoried by
declaration — the lemma materialised in Proofs.CompressSpec which forced the
unfold, and all three other forks carry the lemma row while none carries the
parent.
CONSEQUENCE WORTH DISCLOSING: the audited declaration surface is not purely a
function of the corpus source. It depends on which proofs forced which
unfolds. This is now a known gap in the round-7 kit.
Also corrected here: Proofs/Inventory.lean's header claimed the audit drivers
were excluded from the compile manifest. They are lines 42-44 of PROOFS.
Certified by a full sweep: both buttons, all four forks, purged trees. 8/8.
2026-08-01 14:10:59 +00:00
UNACCOUNTED = $( LC_ALL = C comm -23 " $KERN_NAMES " " $ACCT_NAMES " )
if [ " $DRV_TRAILERS " -ne " $N_DRIVERS " ] ; then
echo " DRIVER SURFACE INCOMPLETE: expected a trailer from each of the $N_DRIVERS driver(s), saw $DRV_TRAILERS "
verification: derive lift dependencies instead of hand-keeping them
Round-9 swept all ten instruments per fork instead of only the two buttons,
and found selftest-axgate.sh red in all four. Root cause, identical to the
KERNLOG defect fixed the day before: a self-test lifts one phase out of
check.sh and supplies its variables from a HAND-WRITTEN preamble, and the
phase later grew a dependency nobody told the preamble about.
Phase 2b stopped globbing Proofs/*.olean and started reading $PROOFS by
membership. Bash does not error on an unset array under `set -u` — it
expands to nothing — so the gate silently received
expected := [".olean"]
one entry with an empty name, and rejected the baseline via its own
fail-closed absence check. Exit code right, reason wrong.
· lift-guard.sh (new, pinned): derives every variable the lifted payload
reads, subtracts what the driver defines, and fails AT LIFT TIME naming
the remainder. Wired into all five lifting self-tests; selftest-shapes.sh
drops its inline copy. One implementation, not five, since drifting out
of sync is the entire failure mode.
· selftest-axgate.sh: lifts PROOFS verbatim, and its case 2 now poisons a
MANIFESTED leaf module rather than adding a stray file. The stray-file
attack was a no-op against membership semantics — that is the dead-file
gate's job, proven by selftest-harness case 8 — and it is also the
weaker attack, since adding files to Proofs/ must clear a gate that
editing an already-manifested module does not.
· Phase 2c's accounting identity moves behind its own marker with its own
ACCTFAIL verdict, so the phase is liftable by construction rather than
by a self-test knowing where to stop. Truncating the lift range alone
would have dropped Phase 2c's own verdict and left the test unable to fail.
· The other four lifting self-tests assert on the PAYLOAD rather than the
assembled driver, so a marker in the preamble cannot satisfy a check
meant to prove the lift landed.
Certified: 8/8 self-tests green in all four forks (~212 assertions, none
failing); check.sh bytes unchanged and still matching the pin written before
the 3h08m round-9 sweep, whose 36 GREEN button rows therefore stand.
--audit-only re-run against the new HARNESS.sha256 in every fork.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-02 11:07:28 +00:00
ACCTFAIL = 1
Account for every constant the kernel sees, by set containment
THE GAP. The capability matrix in the control repo — built after the author
answered a capability question by grepping for a FILENAME rather than for the
property, three times in one session — asked whether each repository's auditor
enumerates itself. The four ed25519 forks answered no. Following that up found
something larger: `Proofs/Audit.lean`, the statement-binding driver from P1-a,
is compiled, is a member of the manifest, and was enumerated by NOTHING. The
kernel counted 3058 declarations where the inventory accounted for 3022, and
26 of the 36 missing were its.
THE PROPERTY, now enforced: every constant the kernel sees under this button's
manifest must appear, BY NAME, in either the corpus inventory or the
instruments' own surface. `emitDrivers` in InventoryCore walks the audit
modules and fails closed on an axiom (which would widen the trusted base
outside every cone) or on a standalone claim (which no certificate covers and
no allowlist pins), while admitting the obligations the elaborator generates
for a definition declared alongside it.
TWO WRONG FORMULATIONS FIRST, both recorded because the second is instructive:
· `kernel = corpus + instruments + N_DRIVERS`, where the last term was
justified as a per-driver "self-observation blind spot". It fitted dalek
and anza (2 drivers, residual 2) and broke on risc0 and betrusted
(1 driver, residual 2). The residual is 2 everywhere and has nothing to do
with drivers. This was curve-fitting from a sample of one, and it was named
as the highest-risk claim in the round-7 self-assessment BEFORE the data
refuted it.
· distinct-by-name counting, which collapses `CurveFieldProofs.zero_spec` —
a name that genuinely denotes two different declarations, in Proofs.Basic
and Proofs.ConstSpecs, walked by two drivers with separate environments.
THE MEASURED CAUSE of the residual. Lean materialises equation lemmas lazily,
when something forces an unfold, and each module that forces one gets its own
copy in its object file. `CurveFieldProofs.denote.eq_1` sits in both
SubNegSpec.olean and ConstSpecs.olean; `CurveFieldProofs.limbsVal.eq_1` in both
ReduceSpec.olean and ConstSpecs.olean. The kernel gate reads object files and
counts both copies; the environment holds one constant per name. Counts cannot
relate those two views in either direction — so the check compares SETS, which
is the idiom the rest of this estate already uses, and no constant remains that
could be widened to make a red run green.
Negative-tested: with the instrument walk disabled, the check names
Proofs.Audit's declarations as unaccounted.
ANZA also lacked one allowlist row, `subtle.Choice...from.eq_1`, the same
lazy-materialisation effect seen from the other side. Verified rather than
assumed before adding it: the parent is declared in gen/CurveField/
FunsExternal.lean — the model, pinned by bytes and not inventoried by
declaration — the lemma materialised in Proofs.CompressSpec which forced the
unfold, and all three other forks carry the lemma row while none carries the
parent.
CONSEQUENCE WORTH DISCLOSING: the audited declaration surface is not purely a
function of the corpus source. It depends on which proofs forced which
unfolds. This is now a known gap in the round-7 kit.
Also corrected here: Proofs/Inventory.lean's header claimed the audit drivers
were excluded from the compile manifest. They are lines 42-44 of PROOFS.
Certified by a full sweep: both buttons, all four forks, purged trees. 8/8.
2026-08-01 14:10:59 +00:00
elif [ " ${ DRV_SUM :- 0 } " != " $N_DRV " ] ; then
echo " DRIVER SURFACE TRUNCATED: trailers sum to ${ DRV_SUM :- 0 } , observed $N_DRV lines "
verification: derive lift dependencies instead of hand-keeping them
Round-9 swept all ten instruments per fork instead of only the two buttons,
and found selftest-axgate.sh red in all four. Root cause, identical to the
KERNLOG defect fixed the day before: a self-test lifts one phase out of
check.sh and supplies its variables from a HAND-WRITTEN preamble, and the
phase later grew a dependency nobody told the preamble about.
Phase 2b stopped globbing Proofs/*.olean and started reading $PROOFS by
membership. Bash does not error on an unset array under `set -u` — it
expands to nothing — so the gate silently received
expected := [".olean"]
one entry with an empty name, and rejected the baseline via its own
fail-closed absence check. Exit code right, reason wrong.
· lift-guard.sh (new, pinned): derives every variable the lifted payload
reads, subtracts what the driver defines, and fails AT LIFT TIME naming
the remainder. Wired into all five lifting self-tests; selftest-shapes.sh
drops its inline copy. One implementation, not five, since drifting out
of sync is the entire failure mode.
· selftest-axgate.sh: lifts PROOFS verbatim, and its case 2 now poisons a
MANIFESTED leaf module rather than adding a stray file. The stray-file
attack was a no-op against membership semantics — that is the dead-file
gate's job, proven by selftest-harness case 8 — and it is also the
weaker attack, since adding files to Proofs/ must clear a gate that
editing an already-manifested module does not.
· Phase 2c's accounting identity moves behind its own marker with its own
ACCTFAIL verdict, so the phase is liftable by construction rather than
by a self-test knowing where to stop. Truncating the lift range alone
would have dropped Phase 2c's own verdict and left the test unable to fail.
· The other four lifting self-tests assert on the PAYLOAD rather than the
assembled driver, so a marker in the preamble cannot satisfy a check
meant to prove the lift landed.
Certified: 8/8 self-tests green in all four forks (~212 assertions, none
failing); check.sh bytes unchanged and still matching the pin written before
the 3h08m round-9 sweep, whose 36 GREEN button rows therefore stand.
--audit-only re-run against the new HARNESS.sha256 in every fork.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-02 11:07:28 +00:00
ACCTFAIL = 1
Account for every constant the kernel sees, by set containment
THE GAP. The capability matrix in the control repo — built after the author
answered a capability question by grepping for a FILENAME rather than for the
property, three times in one session — asked whether each repository's auditor
enumerates itself. The four ed25519 forks answered no. Following that up found
something larger: `Proofs/Audit.lean`, the statement-binding driver from P1-a,
is compiled, is a member of the manifest, and was enumerated by NOTHING. The
kernel counted 3058 declarations where the inventory accounted for 3022, and
26 of the 36 missing were its.
THE PROPERTY, now enforced: every constant the kernel sees under this button's
manifest must appear, BY NAME, in either the corpus inventory or the
instruments' own surface. `emitDrivers` in InventoryCore walks the audit
modules and fails closed on an axiom (which would widen the trusted base
outside every cone) or on a standalone claim (which no certificate covers and
no allowlist pins), while admitting the obligations the elaborator generates
for a definition declared alongside it.
TWO WRONG FORMULATIONS FIRST, both recorded because the second is instructive:
· `kernel = corpus + instruments + N_DRIVERS`, where the last term was
justified as a per-driver "self-observation blind spot". It fitted dalek
and anza (2 drivers, residual 2) and broke on risc0 and betrusted
(1 driver, residual 2). The residual is 2 everywhere and has nothing to do
with drivers. This was curve-fitting from a sample of one, and it was named
as the highest-risk claim in the round-7 self-assessment BEFORE the data
refuted it.
· distinct-by-name counting, which collapses `CurveFieldProofs.zero_spec` —
a name that genuinely denotes two different declarations, in Proofs.Basic
and Proofs.ConstSpecs, walked by two drivers with separate environments.
THE MEASURED CAUSE of the residual. Lean materialises equation lemmas lazily,
when something forces an unfold, and each module that forces one gets its own
copy in its object file. `CurveFieldProofs.denote.eq_1` sits in both
SubNegSpec.olean and ConstSpecs.olean; `CurveFieldProofs.limbsVal.eq_1` in both
ReduceSpec.olean and ConstSpecs.olean. The kernel gate reads object files and
counts both copies; the environment holds one constant per name. Counts cannot
relate those two views in either direction — so the check compares SETS, which
is the idiom the rest of this estate already uses, and no constant remains that
could be widened to make a red run green.
Negative-tested: with the instrument walk disabled, the check names
Proofs.Audit's declarations as unaccounted.
ANZA also lacked one allowlist row, `subtle.Choice...from.eq_1`, the same
lazy-materialisation effect seen from the other side. Verified rather than
assumed before adding it: the parent is declared in gen/CurveField/
FunsExternal.lean — the model, pinned by bytes and not inventoried by
declaration — the lemma materialised in Proofs.CompressSpec which forced the
unfold, and all three other forks carry the lemma row while none carries the
parent.
CONSEQUENCE WORTH DISCLOSING: the audited declaration surface is not purely a
function of the corpus source. It depends on which proofs forced which
unfolds. This is now a known gap in the round-7 kit.
Also corrected here: Proofs/Inventory.lean's header claimed the audit drivers
were excluded from the compile manifest. They are lines 42-44 of PROOFS.
Certified by a full sweep: both buttons, all four forks, purged trees. 8/8.
2026-08-01 14:10:59 +00:00
elif [ ! -s " $KERN_NAMES " ] ; then
echo " ACCOUNTING FAILED: Phase 2b reported no constant names — the scan was vacuous"
verification: derive lift dependencies instead of hand-keeping them
Round-9 swept all ten instruments per fork instead of only the two buttons,
and found selftest-axgate.sh red in all four. Root cause, identical to the
KERNLOG defect fixed the day before: a self-test lifts one phase out of
check.sh and supplies its variables from a HAND-WRITTEN preamble, and the
phase later grew a dependency nobody told the preamble about.
Phase 2b stopped globbing Proofs/*.olean and started reading $PROOFS by
membership. Bash does not error on an unset array under `set -u` — it
expands to nothing — so the gate silently received
expected := [".olean"]
one entry with an empty name, and rejected the baseline via its own
fail-closed absence check. Exit code right, reason wrong.
· lift-guard.sh (new, pinned): derives every variable the lifted payload
reads, subtracts what the driver defines, and fails AT LIFT TIME naming
the remainder. Wired into all five lifting self-tests; selftest-shapes.sh
drops its inline copy. One implementation, not five, since drifting out
of sync is the entire failure mode.
· selftest-axgate.sh: lifts PROOFS verbatim, and its case 2 now poisons a
MANIFESTED leaf module rather than adding a stray file. The stray-file
attack was a no-op against membership semantics — that is the dead-file
gate's job, proven by selftest-harness case 8 — and it is also the
weaker attack, since adding files to Proofs/ must clear a gate that
editing an already-manifested module does not.
· Phase 2c's accounting identity moves behind its own marker with its own
ACCTFAIL verdict, so the phase is liftable by construction rather than
by a self-test knowing where to stop. Truncating the lift range alone
would have dropped Phase 2c's own verdict and left the test unable to fail.
· The other four lifting self-tests assert on the PAYLOAD rather than the
assembled driver, so a marker in the preamble cannot satisfy a check
meant to prove the lift landed.
Certified: 8/8 self-tests green in all four forks (~212 assertions, none
failing); check.sh bytes unchanged and still matching the pin written before
the 3h08m round-9 sweep, whose 36 GREEN button rows therefore stand.
--audit-only re-run against the new HARNESS.sha256 in every fork.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-02 11:07:28 +00:00
ACCTFAIL = 1
Account for every constant the kernel sees, by set containment
THE GAP. The capability matrix in the control repo — built after the author
answered a capability question by grepping for a FILENAME rather than for the
property, three times in one session — asked whether each repository's auditor
enumerates itself. The four ed25519 forks answered no. Following that up found
something larger: `Proofs/Audit.lean`, the statement-binding driver from P1-a,
is compiled, is a member of the manifest, and was enumerated by NOTHING. The
kernel counted 3058 declarations where the inventory accounted for 3022, and
26 of the 36 missing were its.
THE PROPERTY, now enforced: every constant the kernel sees under this button's
manifest must appear, BY NAME, in either the corpus inventory or the
instruments' own surface. `emitDrivers` in InventoryCore walks the audit
modules and fails closed on an axiom (which would widen the trusted base
outside every cone) or on a standalone claim (which no certificate covers and
no allowlist pins), while admitting the obligations the elaborator generates
for a definition declared alongside it.
TWO WRONG FORMULATIONS FIRST, both recorded because the second is instructive:
· `kernel = corpus + instruments + N_DRIVERS`, where the last term was
justified as a per-driver "self-observation blind spot". It fitted dalek
and anza (2 drivers, residual 2) and broke on risc0 and betrusted
(1 driver, residual 2). The residual is 2 everywhere and has nothing to do
with drivers. This was curve-fitting from a sample of one, and it was named
as the highest-risk claim in the round-7 self-assessment BEFORE the data
refuted it.
· distinct-by-name counting, which collapses `CurveFieldProofs.zero_spec` —
a name that genuinely denotes two different declarations, in Proofs.Basic
and Proofs.ConstSpecs, walked by two drivers with separate environments.
THE MEASURED CAUSE of the residual. Lean materialises equation lemmas lazily,
when something forces an unfold, and each module that forces one gets its own
copy in its object file. `CurveFieldProofs.denote.eq_1` sits in both
SubNegSpec.olean and ConstSpecs.olean; `CurveFieldProofs.limbsVal.eq_1` in both
ReduceSpec.olean and ConstSpecs.olean. The kernel gate reads object files and
counts both copies; the environment holds one constant per name. Counts cannot
relate those two views in either direction — so the check compares SETS, which
is the idiom the rest of this estate already uses, and no constant remains that
could be widened to make a red run green.
Negative-tested: with the instrument walk disabled, the check names
Proofs.Audit's declarations as unaccounted.
ANZA also lacked one allowlist row, `subtle.Choice...from.eq_1`, the same
lazy-materialisation effect seen from the other side. Verified rather than
assumed before adding it: the parent is declared in gen/CurveField/
FunsExternal.lean — the model, pinned by bytes and not inventoried by
declaration — the lemma materialised in Proofs.CompressSpec which forced the
unfold, and all three other forks carry the lemma row while none carries the
parent.
CONSEQUENCE WORTH DISCLOSING: the audited declaration surface is not purely a
function of the corpus source. It depends on which proofs forced which
unfolds. This is now a known gap in the round-7 kit.
Also corrected here: Proofs/Inventory.lean's header claimed the audit drivers
were excluded from the compile manifest. They are lines 42-44 of PROOFS.
Certified by a full sweep: both buttons, all four forks, purged trees. 8/8.
2026-08-01 14:10:59 +00:00
elif [ -n " $UNACCOUNTED " ] ; then
echo " ACCOUNTING FAILED: the kernel holds constants that neither walk accounts for:"
printf '%s\n' " $UNACCOUNTED " | head -20 | sed 's/^/ /'
verification: derive lift dependencies instead of hand-keeping them
Round-9 swept all ten instruments per fork instead of only the two buttons,
and found selftest-axgate.sh red in all four. Root cause, identical to the
KERNLOG defect fixed the day before: a self-test lifts one phase out of
check.sh and supplies its variables from a HAND-WRITTEN preamble, and the
phase later grew a dependency nobody told the preamble about.
Phase 2b stopped globbing Proofs/*.olean and started reading $PROOFS by
membership. Bash does not error on an unset array under `set -u` — it
expands to nothing — so the gate silently received
expected := [".olean"]
one entry with an empty name, and rejected the baseline via its own
fail-closed absence check. Exit code right, reason wrong.
· lift-guard.sh (new, pinned): derives every variable the lifted payload
reads, subtracts what the driver defines, and fails AT LIFT TIME naming
the remainder. Wired into all five lifting self-tests; selftest-shapes.sh
drops its inline copy. One implementation, not five, since drifting out
of sync is the entire failure mode.
· selftest-axgate.sh: lifts PROOFS verbatim, and its case 2 now poisons a
MANIFESTED leaf module rather than adding a stray file. The stray-file
attack was a no-op against membership semantics — that is the dead-file
gate's job, proven by selftest-harness case 8 — and it is also the
weaker attack, since adding files to Proofs/ must clear a gate that
editing an already-manifested module does not.
· Phase 2c's accounting identity moves behind its own marker with its own
ACCTFAIL verdict, so the phase is liftable by construction rather than
by a self-test knowing where to stop. Truncating the lift range alone
would have dropped Phase 2c's own verdict and left the test unable to fail.
· The other four lifting self-tests assert on the PAYLOAD rather than the
assembled driver, so a marker in the preamble cannot satisfy a check
meant to prove the lift landed.
Certified: 8/8 self-tests green in all four forks (~212 assertions, none
failing); check.sh bytes unchanged and still matching the pin written before
the 3h08m round-9 sweep, whose 36 GREEN button rows therefore stand.
--audit-only re-run against the new HARNESS.sha256 in every fork.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-02 11:07:28 +00:00
ACCTFAIL = 1
Account for every constant the kernel sees, by set containment
THE GAP. The capability matrix in the control repo — built after the author
answered a capability question by grepping for a FILENAME rather than for the
property, three times in one session — asked whether each repository's auditor
enumerates itself. The four ed25519 forks answered no. Following that up found
something larger: `Proofs/Audit.lean`, the statement-binding driver from P1-a,
is compiled, is a member of the manifest, and was enumerated by NOTHING. The
kernel counted 3058 declarations where the inventory accounted for 3022, and
26 of the 36 missing were its.
THE PROPERTY, now enforced: every constant the kernel sees under this button's
manifest must appear, BY NAME, in either the corpus inventory or the
instruments' own surface. `emitDrivers` in InventoryCore walks the audit
modules and fails closed on an axiom (which would widen the trusted base
outside every cone) or on a standalone claim (which no certificate covers and
no allowlist pins), while admitting the obligations the elaborator generates
for a definition declared alongside it.
TWO WRONG FORMULATIONS FIRST, both recorded because the second is instructive:
· `kernel = corpus + instruments + N_DRIVERS`, where the last term was
justified as a per-driver "self-observation blind spot". It fitted dalek
and anza (2 drivers, residual 2) and broke on risc0 and betrusted
(1 driver, residual 2). The residual is 2 everywhere and has nothing to do
with drivers. This was curve-fitting from a sample of one, and it was named
as the highest-risk claim in the round-7 self-assessment BEFORE the data
refuted it.
· distinct-by-name counting, which collapses `CurveFieldProofs.zero_spec` —
a name that genuinely denotes two different declarations, in Proofs.Basic
and Proofs.ConstSpecs, walked by two drivers with separate environments.
THE MEASURED CAUSE of the residual. Lean materialises equation lemmas lazily,
when something forces an unfold, and each module that forces one gets its own
copy in its object file. `CurveFieldProofs.denote.eq_1` sits in both
SubNegSpec.olean and ConstSpecs.olean; `CurveFieldProofs.limbsVal.eq_1` in both
ReduceSpec.olean and ConstSpecs.olean. The kernel gate reads object files and
counts both copies; the environment holds one constant per name. Counts cannot
relate those two views in either direction — so the check compares SETS, which
is the idiom the rest of this estate already uses, and no constant remains that
could be widened to make a red run green.
Negative-tested: with the instrument walk disabled, the check names
Proofs.Audit's declarations as unaccounted.
ANZA also lacked one allowlist row, `subtle.Choice...from.eq_1`, the same
lazy-materialisation effect seen from the other side. Verified rather than
assumed before adding it: the parent is declared in gen/CurveField/
FunsExternal.lean — the model, pinned by bytes and not inventoried by
declaration — the lemma materialised in Proofs.CompressSpec which forced the
unfold, and all three other forks carry the lemma row while none carries the
parent.
CONSEQUENCE WORTH DISCLOSING: the audited declaration surface is not purely a
function of the corpus source. It depends on which proofs forced which
unfolds. This is now a known gap in the round-7 kit.
Also corrected here: Proofs/Inventory.lean's header claimed the audit drivers
were excluded from the compile manifest. They are lines 42-44 of PROOFS.
Certified by a full sweep: both buttons, all four forks, purged trees. 8/8.
2026-08-01 14:10:59 +00:00
else
2026-08-04 01:17:05 +00:00
echo " accounting: every one of $( wc -l < " $KERN_NAMES " ) kernel constant names is covered by the corpus inventory or the instrument surface "
echo " multi-module: $MULTIMOD kernel record(s) differ from a walk only in module attribution (lazy equation lemmas materialised per module — GPT-5.6 round-7 F8, reported not suppressed) "
Account for every constant the kernel sees, by set containment
THE GAP. The capability matrix in the control repo — built after the author
answered a capability question by grepping for a FILENAME rather than for the
property, three times in one session — asked whether each repository's auditor
enumerates itself. The four ed25519 forks answered no. Following that up found
something larger: `Proofs/Audit.lean`, the statement-binding driver from P1-a,
is compiled, is a member of the manifest, and was enumerated by NOTHING. The
kernel counted 3058 declarations where the inventory accounted for 3022, and
26 of the 36 missing were its.
THE PROPERTY, now enforced: every constant the kernel sees under this button's
manifest must appear, BY NAME, in either the corpus inventory or the
instruments' own surface. `emitDrivers` in InventoryCore walks the audit
modules and fails closed on an axiom (which would widen the trusted base
outside every cone) or on a standalone claim (which no certificate covers and
no allowlist pins), while admitting the obligations the elaborator generates
for a definition declared alongside it.
TWO WRONG FORMULATIONS FIRST, both recorded because the second is instructive:
· `kernel = corpus + instruments + N_DRIVERS`, where the last term was
justified as a per-driver "self-observation blind spot". It fitted dalek
and anza (2 drivers, residual 2) and broke on risc0 and betrusted
(1 driver, residual 2). The residual is 2 everywhere and has nothing to do
with drivers. This was curve-fitting from a sample of one, and it was named
as the highest-risk claim in the round-7 self-assessment BEFORE the data
refuted it.
· distinct-by-name counting, which collapses `CurveFieldProofs.zero_spec` —
a name that genuinely denotes two different declarations, in Proofs.Basic
and Proofs.ConstSpecs, walked by two drivers with separate environments.
THE MEASURED CAUSE of the residual. Lean materialises equation lemmas lazily,
when something forces an unfold, and each module that forces one gets its own
copy in its object file. `CurveFieldProofs.denote.eq_1` sits in both
SubNegSpec.olean and ConstSpecs.olean; `CurveFieldProofs.limbsVal.eq_1` in both
ReduceSpec.olean and ConstSpecs.olean. The kernel gate reads object files and
counts both copies; the environment holds one constant per name. Counts cannot
relate those two views in either direction — so the check compares SETS, which
is the idiom the rest of this estate already uses, and no constant remains that
could be widened to make a red run green.
Negative-tested: with the instrument walk disabled, the check names
Proofs.Audit's declarations as unaccounted.
ANZA also lacked one allowlist row, `subtle.Choice...from.eq_1`, the same
lazy-materialisation effect seen from the other side. Verified rather than
assumed before adding it: the parent is declared in gen/CurveField/
FunsExternal.lean — the model, pinned by bytes and not inventoried by
declaration — the lemma materialised in Proofs.CompressSpec which forced the
unfold, and all three other forks carry the lemma row while none carries the
parent.
CONSEQUENCE WORTH DISCLOSING: the audited declaration surface is not purely a
function of the corpus source. It depends on which proofs forced which
unfolds. This is now a known gap in the round-7 kit.
Also corrected here: Proofs/Inventory.lean's header claimed the audit drivers
were excluded from the compile manifest. They are lines 42-44 of PROOFS.
Certified by a full sweep: both buttons, all four forks, purged trees. 8/8.
2026-08-01 14:10:59 +00:00
fi
2026-08-04 01:17:05 +00:00
rm -f " $KERN_NAMES " " $ACCT_NAMES " " $KERN_PAIRS " " $ACCT_PAIRS "
verification: derive lift dependencies instead of hand-keeping them
Round-9 swept all ten instruments per fork instead of only the two buttons,
and found selftest-axgate.sh red in all four. Root cause, identical to the
KERNLOG defect fixed the day before: a self-test lifts one phase out of
check.sh and supplies its variables from a HAND-WRITTEN preamble, and the
phase later grew a dependency nobody told the preamble about.
Phase 2b stopped globbing Proofs/*.olean and started reading $PROOFS by
membership. Bash does not error on an unset array under `set -u` — it
expands to nothing — so the gate silently received
expected := [".olean"]
one entry with an empty name, and rejected the baseline via its own
fail-closed absence check. Exit code right, reason wrong.
· lift-guard.sh (new, pinned): derives every variable the lifted payload
reads, subtracts what the driver defines, and fails AT LIFT TIME naming
the remainder. Wired into all five lifting self-tests; selftest-shapes.sh
drops its inline copy. One implementation, not five, since drifting out
of sync is the entire failure mode.
· selftest-axgate.sh: lifts PROOFS verbatim, and its case 2 now poisons a
MANIFESTED leaf module rather than adding a stray file. The stray-file
attack was a no-op against membership semantics — that is the dead-file
gate's job, proven by selftest-harness case 8 — and it is also the
weaker attack, since adding files to Proofs/ must clear a gate that
editing an already-manifested module does not.
· Phase 2c's accounting identity moves behind its own marker with its own
ACCTFAIL verdict, so the phase is liftable by construction rather than
by a self-test knowing where to stop. Truncating the lift range alone
would have dropped Phase 2c's own verdict and left the test unable to fail.
· The other four lifting self-tests assert on the PAYLOAD rather than the
assembled driver, so a marker in the preamble cannot satisfy a check
meant to prove the lift landed.
Certified: 8/8 self-tests green in all four forks (~212 assertions, none
failing); check.sh bytes unchanged and still matching the pin written before
the 3h08m round-9 sweep, whose 36 GREEN button rows therefore stand.
--audit-only re-run against the new HARNESS.sha256 in every fork.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-02 11:07:28 +00:00
ACCTFAIL = ${ ACCTFAIL :- 0 }
[ " $ACCTFAIL " = 0 ] || { echo "ACCOUNTING FAILED" ; rm -f " $INVLOG " " $OBS " " $KERNLOG " ; exit 1; }
Account for every constant the kernel sees, by set containment
THE GAP. The capability matrix in the control repo — built after the author
answered a capability question by grepping for a FILENAME rather than for the
property, three times in one session — asked whether each repository's auditor
enumerates itself. The four ed25519 forks answered no. Following that up found
something larger: `Proofs/Audit.lean`, the statement-binding driver from P1-a,
is compiled, is a member of the manifest, and was enumerated by NOTHING. The
kernel counted 3058 declarations where the inventory accounted for 3022, and
26 of the 36 missing were its.
THE PROPERTY, now enforced: every constant the kernel sees under this button's
manifest must appear, BY NAME, in either the corpus inventory or the
instruments' own surface. `emitDrivers` in InventoryCore walks the audit
modules and fails closed on an axiom (which would widen the trusted base
outside every cone) or on a standalone claim (which no certificate covers and
no allowlist pins), while admitting the obligations the elaborator generates
for a definition declared alongside it.
TWO WRONG FORMULATIONS FIRST, both recorded because the second is instructive:
· `kernel = corpus + instruments + N_DRIVERS`, where the last term was
justified as a per-driver "self-observation blind spot". It fitted dalek
and anza (2 drivers, residual 2) and broke on risc0 and betrusted
(1 driver, residual 2). The residual is 2 everywhere and has nothing to do
with drivers. This was curve-fitting from a sample of one, and it was named
as the highest-risk claim in the round-7 self-assessment BEFORE the data
refuted it.
· distinct-by-name counting, which collapses `CurveFieldProofs.zero_spec` —
a name that genuinely denotes two different declarations, in Proofs.Basic
and Proofs.ConstSpecs, walked by two drivers with separate environments.
THE MEASURED CAUSE of the residual. Lean materialises equation lemmas lazily,
when something forces an unfold, and each module that forces one gets its own
copy in its object file. `CurveFieldProofs.denote.eq_1` sits in both
SubNegSpec.olean and ConstSpecs.olean; `CurveFieldProofs.limbsVal.eq_1` in both
ReduceSpec.olean and ConstSpecs.olean. The kernel gate reads object files and
counts both copies; the environment holds one constant per name. Counts cannot
relate those two views in either direction — so the check compares SETS, which
is the idiom the rest of this estate already uses, and no constant remains that
could be widened to make a red run green.
Negative-tested: with the instrument walk disabled, the check names
Proofs.Audit's declarations as unaccounted.
ANZA also lacked one allowlist row, `subtle.Choice...from.eq_1`, the same
lazy-materialisation effect seen from the other side. Verified rather than
assumed before adding it: the parent is declared in gen/CurveField/
FunsExternal.lean — the model, pinned by bytes and not inventoried by
declaration — the lemma materialised in Proofs.CompressSpec which forced the
unfold, and all three other forks carry the lemma row while none carries the
parent.
CONSEQUENCE WORTH DISCLOSING: the audited declaration surface is not purely a
function of the corpus source. It depends on which proofs forced which
unfolds. This is now a known gap in the round-7 kit.
Also corrected here: Proofs/Inventory.lean's header claimed the audit drivers
were excluded from the compile manifest. They are lines 42-44 of PROOFS.
Certified by a full sweep: both buttons, all four forks, purged trees. 8/8.
2026-08-01 14:10:59 +00:00
rm -f " $INVLOG " " $OBS " " $KERNLOG "
Round-7 F1: make model/template correspondence SEMANTIC, and fail closed
THE DEFECT, as found. GPT-5.6 showed the textual classifier could report
PROVEN for a name Lean resolves to an axiom: a definition appearing only
inside a `/- -/` comment was read as real. Repairing that exposed something
larger and already live. Aeneas wraps long declarations:
axiom
curve25519_dalek.edwards.EdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg
The old scanner required keyword and name on one physical line, so it matched
nothing there and SILENTLY DROPPED the declaration — no MODEL row, no PROVEN
row, no failure. Nine to ten externals per fork had no row at all, and the
tier-A/B `neg` was missing from every committed table while the trust
documents claimed that class was machine-checked. Four pinned tables were
wrong, in four repositories, with the buttons green over them. No attacker
was required; Aeneas's own formatting did it.
The lesson is not "write a better regex". The scanner was FAIL-OPEN: input it
could not parse produced silence instead of a stop. A gate that drops what it
cannot read is worse than no gate, because the green covers a gap that is
invisible in the diff.
THE REPAIR, in three layers that each do only what they honestly can.
· DISCOVERY stays textual, because the template cannot be imported — it
declares the same names as the model and they would clash. It now strips
NESTED `/- -/` blocks, reads a name that wraps to a later line, tracks
namespace/section/end, and FAILS CLOSED: an unparseable keyword exits 2
naming file and line.
· Phase 0d keeps the cheap pre-compile comparison against the table.
· Phase 2d is new and authoritative. After compilation it generates a temp
Lean driver (the Phase 2b idiom, so no permanent module and no manifest
churn), imports every non-template gen module, and asks env.find? what
each external IS: kind and originating module. Model module -> MODEL;
non-axiom in a generated module -> PROVEN; an axiom outside the model, or
a name that does not resolve, is a failure. Lean's verdict must equal the
committed table's, and the answer count must equal the question count so
a truncated resolver cannot pass.
THE TABLES were regenerated and verified three ways before being committed:
an independently written second scanner agreed on 228/228 rows across the
four forks; all 47 changed rows carry file:line evidence; and the PROVEN row
was put to Lean directly — kind = def, module = CurveField.Funs.
dalek 54 -> 64 rows anza 42 -> 51 risc0 48 -> 57 betrusted 47 -> 56
Also corrected: `from_residual` was recorded EXTRA in every fork; the
template does demand it, so it is MODEL. anza carried a spurious `hash|EXTRA`
row from a mis-parse.
NEGATIVE-TESTED. With Phase 0d neutered so Phase 2d was the gate under test,
a PROVEN row edited to MODEL produces:
SEMANTIC DRIFT: ...neg — table says MODEL, Lean says PROVEN
selftest-correspondence.sh grew 4 cases -> 7: GPT's comment counterexample,
the wrapped declaration that was actually live, and a fail-closed check.
WHAT THIS DOES NOT CLOSE. Phase 2d resolves names in the environment built
from gen/. It establishes what a name IS — assumption or proof, and where —
not that the extraction faithfully represents the Rust. That remains the
Charon/Aeneas trust assumption and no gate here can close it.
Certified: both buttons, all four forks, purged trees. 8/8 green, with
62/48/53/52 externals resolved by Lean and every verdict matching.
2026-08-02 00:24:15 +00:00
# ── Phase 2d: SEMANTIC model/template correspondence ────────────────────────
# Phase 0d asks a text scanner what the extraction's boundary looks like. This
# phase asks LEAN what it actually is, and requires the two to agree.
#
# WHY BOTH. Round-7 review (GPT-5.6, finding F1) showed the textual classifier
# could be made to report PROVEN for a name Lean resolves to an axiom — a
# definition inside a `/- -/` comment was read as real. Worse, and found while
# repairing that: Aeneas wraps long declarations, and the old scanner required
# keyword and name on one physical line, so it SILENTLY DROPPED them. Nine to
# ten externals per fork had no row at all, and one — the tier-A/B `neg` — was
# missing from every committed table while the docs claimed that class was
# machine-checked.
#
# A source scanner cannot decide this question. Whether a name resolves to an
# assumption or to a proof is a property of the elaborated ENVIRONMENT: it turns
# on imports, namespaces, `export`, aliases and shadowing, none of which are
# visible to a regex. So the scanner's job is now only DISCOVERY — what does the
# template ask for — and even that fails closed. The verdict comes from Lean.
#
# The template itself is deliberately not imported: it declares the same names
# as the hand-written model and the two would clash. Discovery is therefore
# unavoidably textual, which is exactly why `model-correspondence.py` must stop
# rather than skip on anything it cannot parse.
echo "=== Phase 2d: semantic model/template correspondence ==="
SEMNAMES = $( mktemp /tmp/check-semnames-XXXX.txt)
SEMOUT = $( mktemp /tmp/check-semout-XXXX.txt)
python3 " $HERE /model-correspondence.py " --names " $HERE " > " $SEMNAMES " || {
echo "MODEL CORRESPONDENCE FAILED: could not enumerate the extraction's externals."
rm -f " $SEMNAMES " " $SEMOUT " ; exit 1; }
SEM = $( mktemp " $HERE /.semcheck-XXXX.lean " )
{
# Import every generated module that is not a template. There are no name
# clashes between crates (verified), and the crate roots transitively pull
# their own models, so this is the same environment the proofs are built on.
for m in $( cd " $HERE /gen " && find . -name '*.lean' -not -name '*_Template.lean' \
| sed 's|^\./||; s|\.lean$||; s|/|.|g' | sort) ; do
echo " import $m "
done
cat <<'LEANSEM'
open Lean in
#eval show CoreM Unit from do
let env ← getEnv
let path := System.FilePath.mk ( ← IO.getEnv "SEMNAMES" ) .get!
for line in ( ← IO.FS.lines path) do
let parts := line.splitOn "|"
if h : parts.length = 2 then
let rel := parts[ 0] !
let nm := parts[ 1] !.toName
match env.find? nm with
| none = > IO.println s!"SEM|{rel}|{parts[1]!}|ABSENT|-"
| some ci = >
let kind := match ci with
| .axiomInfo _ = > "axiom"
| .defnInfo _ = > "def"
| .thmInfo _ = > "theorem"
| .opaqueInfo _ = > "opaque"
| .inductInfo _ = > "inductive"
| .ctorInfo _ = > "ctor"
| .recInfo _ = > "recursor"
| .quotInfo _ = > "quot"
let mdl := match env.getModuleIdxFor? nm with
| some i = > toString env.header.moduleNames[ i] !
| none = > "<current>"
IO.println s!"SEM|{rel}|{parts[1]!}|{kind}|{mdl}"
LEANSEM
} > " $SEM "
cd " $AENEAS_LEAN "
SEM_RC = 0
SEMNAMES = " $SEMNAMES " lake env bash -c "
set -uo pipefail
cd '$HERE/gen' && export LEAN_PATH = \" \$ LEAN_PATH:\$ PWD:$HERE \"
cd '$HERE'
LEAN_TIMEOUT = $TIMEOUT LEAN_MAX_CORES = $CORES '$HERE/lean-guard' '$SEM'
" > " $SEMOUT " 2>&1 || SEM_RC= $?
cd " $HERE "
rm -f " $SEM " " ${ SEM %.lean } .olean "
if [ " $SEM_RC " -ne 0 ] ; then
echo "SEMANTIC CORRESPONDENCE FAILED: the resolver did not run."
tail -12 " $SEMOUT " | sed 's/^/ /'
rm -f " $SEMNAMES " " $SEMOUT " ; exit 1
fi
# Every name the extraction asks for must have been resolved, and its Lean
# verdict must equal the committed table's. The mapping is deliberately strict:
# resolves into the hand-written model module -> MODEL
# resolves to a NON-AXIOM in a generated module -> PROVEN
# anything else -> failure
SEMFAIL = 0
NSEM = $( grep -c '^SEM|' " $SEMOUT " || true )
NWANT = $( grep -c '|' " $SEMNAMES " || true )
if [ " $NSEM " -ne " $NWANT " ] ; then
echo " SEMANTIC CORRESPONDENCE TRUNCATED: asked about $NWANT externals, Lean answered for $NSEM "
SEMFAIL = 1
fi
while IFS = '|' read -r _tag rel name kind mdl; do
[ " $_tag " = SEM ] || continue
want = $( awk -F'|' -v r = " $rel " -v n = " $name " '$1==r && $2==n {print $3}' " $HERE /MODEL-CORRESPONDENCE.txt " )
case " $kind : $mdl " in
axiom:" ${ rel // \/ /. } " ) got = MODEL ; ;
*:" ${ rel // \/ /. } " ) got = MODEL ; ;
axiom:*) got = AXIOM-OUTSIDE-MODEL ; ;
ABSENT:*) got = UNRESOLVED ; ;
*) got = PROVEN ; ;
esac
if [ -z " $want " ] ; then
echo " SEMANTIC DRIFT: $rel | $name resolves ( $kind in $mdl ) but has NO ROW in MODEL-CORRESPONDENCE.txt "
SEMFAIL = 1
elif [ " $want " != " $got " ] ; then
echo " SEMANTIC DRIFT: $rel | $name — table says $want , Lean says $got ( $kind in $mdl ) "
SEMFAIL = 1
fi
done < " $SEMOUT "
rm -f " $SEMNAMES " " $SEMOUT "
if [ " $SEMFAIL " != 0 ] ; then
echo "SEMANTIC CORRESPONDENCE FAILED: the committed table does not match what Lean resolves."
exit 1
fi
echo " $NWANT externals resolved by Lean; every verdict matches the committed table "
echo ""
2026-07-02 12:17:44 +00:00
# ── Phase 3: axiom audit of every certificate ───────────────────────────────
echo "=== Phase 3: axiom audit ==="
EXPECTED = "[propext, Classical.choice, Quot.sound]"
cd " $AENEAS_LEAN "
lake env bash -c "
set -euo pipefail
cd '$HERE/gen' && export LEAN_PATH = \" \$ LEAN_PATH:\$ PWD:$HERE \"
cd '$HERE'
2026-07-03 10:54:26 +00:00
AUD = \$ ( mktemp '$HERE/.audit-XXXX.lean' )
2026-07-02 12:17:44 +00:00
{
for i in ${ AUDIT_IMPORTS [*] } ; do echo \" import \$ i\" ; done
for c in ${ CERTS [*] } ; do echo \" #print axioms \$c\"; done
} > \" \$ AUD\"
2026-07-03 10:54:26 +00:00
OUT = \$ ( LEAN_TIMEOUT = $TIMEOUT LEAN_MEM_MB = 4096 '$HERE/lean-guard' \" \$ AUD\" 2>& 1)
2026-07-02 12:17:44 +00:00
echo \" \$ OUT\"
2026-07-28 15:31:54 +00:00
rm -f \" \$ AUD\" \" \$ { AUD%.lean} .olean\"
2026-07-02 12:17:44 +00:00
N_CLEAN = \$ ( echo \" \$ OUT\" | grep -cF \" depends on axioms: $EXPECTED \" || true )
if [ \" \$ N_CLEAN\" -ne ${# CERTS [@] } ] ; then
echo \" AXIOM AUDIT FAILED: \$ N_CLEAN/${# CERTS [@] } certificates clean\"
exit 1
fi
"
THE SIGNATURE APEX: the EdDSA verification equation, proven and audited
`Proofs/SigApexSpec.lean`:
- `verify_loop_full` — the extracted 32-byte comparison loop returns exactly
the byte-equality of the two arrays (induction; axiom cone = exactly
[propext, Classical.choice, Quot.sound]).
- `verify_accepts_iff` — THE APEX: for a signature that parses, the
extracted RustCrypto verifier accepts IFF the recomputed compressed point
compress( [s]·B − [k]·A )
equals the signature's R byte-for-byte. The recomputation is grounded in
the PROVEN curve model (every curve and scalar call is a certified
definition); k is whatever scalar the SHA-512 oracle produces — the
honest EdDSA acceptance criterion with the hash opaque.
Boundary hygiene forced by the audit itself:
- The public vartime_double_scalar_mul_basepoint dispatch pulled the AVX2
vector-backend axiom into the apex cone. Fixed at the build level:
extract.sh pins RUSTFLAGS --cfg curve25519_dalek_backend="serial", so the
SIMD arm compiles out; BackendKind has only Serial and
get_selected_backend becomes a real definition (ok Serial).
- subtle.Choice.unwrap_u8 upgraded from axiom to the documented model
definition (Choice := U8; unwrap_u8 = self.0) — it sits on the verify
path via compress → is_negative.
- CurveSig modules added to GEN_MODULES (stale-olean incoherence otherwise).
check.sh grows Phase 3b: the apex certificate's axiom cone must equal
EXACTLY
[propext, Classical.choice, Quot.sound,
ed25519.Signature, sha2.Sha512,
sha512_new, sha512_update, sha512_finalize_bytes,
ed25519.Signature.to_bytes, signature.error.Error, Error.new]
— the SHA-512 hash oracle plus the opaque wire-format types. NO curve
axioms, NO scalar axioms, NO backend axioms, enforced on every button press.
Full check.sh green: 16 standard certificates + the apex audit.
Phase 2 (the point-level equation [s]B − [k]A = decompress R, needing
to_bytes canonicity and decompress) remains deferred and documented.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-04 17:45:55 +00:00
echo ""
echo "=== Phase 3b: signature-apex audit (SHA-512 + wire-format boundary) ==="
# The verification-equation apex is grounded in the PROVEN curve model; its
# only axioms beyond the standard three are the deliberate, documented
# boundary: the SHA-512 hash oracle and the opaque wire-format types.
# NO curve axioms, NO scalar axioms, NO backend-dispatch axioms.
cd " $AENEAS_LEAN "
lake env bash -c "
set -euo pipefail
cd '$HERE/gen' && export LEAN_PATH = \" \$ LEAN_PATH:\$ PWD:$HERE \"
cd '$HERE'
ALLOWED = '[propext, Classical.choice, Quot.sound, ed25519.Signature, sha2.Sha512, verifying.sha512_finalize_bytes, verifying.sha512_new, verifying.sha512_update, ed25519.Signature.to_bytes, signature.error.Error, signature.error.Error.new]'
AUD = \$ ( mktemp '$HERE/.apex-XXXX.lean' )
PHASE 2 COMPLETE ON DALEK: THE FULL POINT-LEVEL LIFT
(verify_accepts_iff_decompress, button-enforced)
THE THEOREM: under the apex hypotheses, the signature's R bytes
DECOMPRESS to a valid on-curve point Pt, and
verifier accepts <=> Pt = [k]*(-A) + [s]*B (as points)
- accept iff decompress(R) equals the recomputed point. Every link of
the chain (byte comparison <-> canonical-encoding equality <-> point
equality <-> decompressed-point equality) is machine-checked over the
extracted code. Axiom cone EXACTLY the SHA-512 + wire-format boundary;
Phase 3b now enforces FOUR certificate tiers (byte apex, half-lift,
point equation, full lift).
Proofs/DecompressMain.lean:
- edwards_d_denote: the extracted EDWARDS_D constant denotes THE curve
d (edwards_d_spec + edD_char cancelled by 121666 nonzero).
- decompress_of_canonical (standard three axioms): canonical encodings
of valid on-curve points decompress to them - from_bytes recovers the
y-residue exactly (sign bit discarded), Q's own x witnesses the
square so sqrt_ratio_i returns the even root, the sign bit (Q's
x-parity, from byte 31) selects +/-root, and the parity-injectivity
argument pins the selection to edX Q; the assembled {X,Y,1,X*Y} is
ExtValid and on-curve.
- verify_accepts_iff_decompress: the capstone composition.
Full button green fresh. Remaining: replicate x3, coherence pass 4.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-05 22:05:55 +00:00
{ echo 'import Proofs.SigApexSpec' ; echo 'import Proofs.PointLiftSpec' ; echo 'import Proofs.PointEqSpec' ; echo 'import Proofs.DecompressMain' ; echo '#print axioms CurveFieldProofs.verify_accepts_iff' ; echo '#print axioms CurveFieldProofs.verify_accepts_iff_point' ; echo '#print axioms CurveFieldProofs.verify_accepts_iff_point_eq' ; echo '#print axioms CurveFieldProofs.verify_accepts_iff_decompress' ; } > \" \$ AUD\"
THE SIGNATURE APEX: the EdDSA verification equation, proven and audited
`Proofs/SigApexSpec.lean`:
- `verify_loop_full` — the extracted 32-byte comparison loop returns exactly
the byte-equality of the two arrays (induction; axiom cone = exactly
[propext, Classical.choice, Quot.sound]).
- `verify_accepts_iff` — THE APEX: for a signature that parses, the
extracted RustCrypto verifier accepts IFF the recomputed compressed point
compress( [s]·B − [k]·A )
equals the signature's R byte-for-byte. The recomputation is grounded in
the PROVEN curve model (every curve and scalar call is a certified
definition); k is whatever scalar the SHA-512 oracle produces — the
honest EdDSA acceptance criterion with the hash opaque.
Boundary hygiene forced by the audit itself:
- The public vartime_double_scalar_mul_basepoint dispatch pulled the AVX2
vector-backend axiom into the apex cone. Fixed at the build level:
extract.sh pins RUSTFLAGS --cfg curve25519_dalek_backend="serial", so the
SIMD arm compiles out; BackendKind has only Serial and
get_selected_backend becomes a real definition (ok Serial).
- subtle.Choice.unwrap_u8 upgraded from axiom to the documented model
definition (Choice := U8; unwrap_u8 = self.0) — it sits on the verify
path via compress → is_negative.
- CurveSig modules added to GEN_MODULES (stale-olean incoherence otherwise).
check.sh grows Phase 3b: the apex certificate's axiom cone must equal
EXACTLY
[propext, Classical.choice, Quot.sound,
ed25519.Signature, sha2.Sha512,
sha512_new, sha512_update, sha512_finalize_bytes,
ed25519.Signature.to_bytes, signature.error.Error, Error.new]
— the SHA-512 hash oracle plus the opaque wire-format types. NO curve
axioms, NO scalar axioms, NO backend axioms, enforced on every button press.
Full check.sh green: 16 standard certificates + the apex audit.
Phase 2 (the point-level equation [s]B − [k]A = decompress R, needing
to_bytes canonicity and decompress) remains deferred and documented.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-04 17:45:55 +00:00
OUT = \$ ( LEAN_TIMEOUT = $TIMEOUT LEAN_MEM_MB = 4096 '$HERE/lean-guard' \" \$ AUD\" 2>& 1)
echo \" \$ OUT\"
2026-07-28 15:31:54 +00:00
rm -f \" \$ AUD\" \" \$ { AUD%.lean} .olean\"
THE SIGNATURE APEX: the EdDSA verification equation, proven and audited
`Proofs/SigApexSpec.lean`:
- `verify_loop_full` — the extracted 32-byte comparison loop returns exactly
the byte-equality of the two arrays (induction; axiom cone = exactly
[propext, Classical.choice, Quot.sound]).
- `verify_accepts_iff` — THE APEX: for a signature that parses, the
extracted RustCrypto verifier accepts IFF the recomputed compressed point
compress( [s]·B − [k]·A )
equals the signature's R byte-for-byte. The recomputation is grounded in
the PROVEN curve model (every curve and scalar call is a certified
definition); k is whatever scalar the SHA-512 oracle produces — the
honest EdDSA acceptance criterion with the hash opaque.
Boundary hygiene forced by the audit itself:
- The public vartime_double_scalar_mul_basepoint dispatch pulled the AVX2
vector-backend axiom into the apex cone. Fixed at the build level:
extract.sh pins RUSTFLAGS --cfg curve25519_dalek_backend="serial", so the
SIMD arm compiles out; BackendKind has only Serial and
get_selected_backend becomes a real definition (ok Serial).
- subtle.Choice.unwrap_u8 upgraded from axiom to the documented model
definition (Choice := U8; unwrap_u8 = self.0) — it sits on the verify
path via compress → is_negative.
- CurveSig modules added to GEN_MODULES (stale-olean incoherence otherwise).
check.sh grows Phase 3b: the apex certificate's axiom cone must equal
EXACTLY
[propext, Classical.choice, Quot.sound,
ed25519.Signature, sha2.Sha512,
sha512_new, sha512_update, sha512_finalize_bytes,
ed25519.Signature.to_bytes, signature.error.Error, Error.new]
— the SHA-512 hash oracle plus the opaque wire-format types. NO curve
axioms, NO scalar axioms, NO backend axioms, enforced on every button press.
Full check.sh green: 16 standard certificates + the apex audit.
Phase 2 (the point-level equation [s]B − [k]A = decompress R, needing
to_bytes canonicity and decompress) remains deferred and documented.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-04 17:45:55 +00:00
FLAT = \$ ( echo \" \$ OUT\" | tr '\\n' ' ' | tr -s ' ' )
PHASE 2 HALF-LIFT PROVEN: verify_accepts_iff_point, button-enforced
THE THEOREM (CurveFieldProofs.verify_accepts_iff_point): for a parsing
signature, a valid on-curve public-key point, a canonical signature
scalar, and a successful recompute, there is a point R' - the certified
[k](-A) + [s]B, ExtValid and on-curve - with
verifier accepts <=> bytesVal R_bytes
= (edY R').val + ((edX R').val % 2) * 2^255
The apex's byte-for-byte comparison IS point-encoding equality: the
signature's R bytes are accepted exactly when they are THE canonical
encoding of the recomputed point. Axiom cone: EXACTLY the apex boundary
(SHA-512 oracle + wire-format opaques; zero curve/scalar/backend axioms),
now enforced for BOTH apex and half-lift by check.sh Phase 3b.
New machinery in Proofs/PointLiftSpec.lean:
- bind_ok_inv: generic ok-inversion of one monadic bind - the clean way
to invert oracle-bearing chains (axioms cannot be walked).
- recompute_inv: names the recompute chain's intermediates (hash, k,
-A, R') with their defining equations, via eight flat bind_ok_inv
steps after the pass-through reductions.
- Bytes64.exists_bytes + List.exists_len32: the 64-byte destructure -
Lean's match refuses list patterns beyond ~32 elements, so the device
is a 32-cons prefix + a list-level 32-destructure on the tail.
- The assembly: recompute_inv + from_bytes_mod_order_wide_spec (k
canonical) + edwards_neg_law (-A) + vartime_dsm_basepoint_spec (R',
valid, on-curve) + ed_compress_spec (er = canonical encoding) +
rangeEq_iff_bytesVal (byte comparison = value equality), threaded
through the ok-injectivity of the inverted equations.
Full button green fresh, incl. the extended Phase 3b.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-05 14:06:23 +00:00
if echo \" \$ FLAT\" | grep -qF \" 'CurveFieldProofs.verify_accepts_iff' depends on axioms: \$ ALLOWED\" \
2026-07-05 16:27:25 +00:00
&& echo \" \$ FLAT\" | grep -qF \" 'CurveFieldProofs.verify_accepts_iff_point' depends on axioms: \$ ALLOWED\" \
PHASE 2 COMPLETE ON DALEK: THE FULL POINT-LEVEL LIFT
(verify_accepts_iff_decompress, button-enforced)
THE THEOREM: under the apex hypotheses, the signature's R bytes
DECOMPRESS to a valid on-curve point Pt, and
verifier accepts <=> Pt = [k]*(-A) + [s]*B (as points)
- accept iff decompress(R) equals the recomputed point. Every link of
the chain (byte comparison <-> canonical-encoding equality <-> point
equality <-> decompressed-point equality) is machine-checked over the
extracted code. Axiom cone EXACTLY the SHA-512 + wire-format boundary;
Phase 3b now enforces FOUR certificate tiers (byte apex, half-lift,
point equation, full lift).
Proofs/DecompressMain.lean:
- edwards_d_denote: the extracted EDWARDS_D constant denotes THE curve
d (edwards_d_spec + edD_char cancelled by 121666 nonzero).
- decompress_of_canonical (standard three axioms): canonical encodings
of valid on-curve points decompress to them - from_bytes recovers the
y-residue exactly (sign bit discarded), Q's own x witnesses the
square so sqrt_ratio_i returns the even root, the sign bit (Q's
x-parity, from byte 31) selects +/-root, and the parity-injectivity
argument pins the selection to edX Q; the assembled {X,Y,1,X*Y} is
ExtValid and on-curve.
- verify_accepts_iff_decompress: the capstone composition.
Full button green fresh. Remaining: replicate x3, coherence pass 4.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-05 22:05:55 +00:00
&& echo \" \$ FLAT\" | grep -qF \" 'CurveFieldProofs.verify_accepts_iff_point_eq' depends on axioms: \$ ALLOWED\" \
&& echo \" \$ FLAT\" | grep -qF \" 'CurveFieldProofs.verify_accepts_iff_decompress' depends on axioms: \$ ALLOWED\" ; then
2026-07-06 02:01:15 +00:00
echo ' apex + full-lift axiom cones = exactly the SHA-512 + wire-format boundary (no curve/scalar/backend axioms)'
THE SIGNATURE APEX: the EdDSA verification equation, proven and audited
`Proofs/SigApexSpec.lean`:
- `verify_loop_full` — the extracted 32-byte comparison loop returns exactly
the byte-equality of the two arrays (induction; axiom cone = exactly
[propext, Classical.choice, Quot.sound]).
- `verify_accepts_iff` — THE APEX: for a signature that parses, the
extracted RustCrypto verifier accepts IFF the recomputed compressed point
compress( [s]·B − [k]·A )
equals the signature's R byte-for-byte. The recomputation is grounded in
the PROVEN curve model (every curve and scalar call is a certified
definition); k is whatever scalar the SHA-512 oracle produces — the
honest EdDSA acceptance criterion with the hash opaque.
Boundary hygiene forced by the audit itself:
- The public vartime_double_scalar_mul_basepoint dispatch pulled the AVX2
vector-backend axiom into the apex cone. Fixed at the build level:
extract.sh pins RUSTFLAGS --cfg curve25519_dalek_backend="serial", so the
SIMD arm compiles out; BackendKind has only Serial and
get_selected_backend becomes a real definition (ok Serial).
- subtle.Choice.unwrap_u8 upgraded from axiom to the documented model
definition (Choice := U8; unwrap_u8 = self.0) — it sits on the verify
path via compress → is_negative.
- CurveSig modules added to GEN_MODULES (stale-olean incoherence otherwise).
check.sh grows Phase 3b: the apex certificate's axiom cone must equal
EXACTLY
[propext, Classical.choice, Quot.sound,
ed25519.Signature, sha2.Sha512,
sha512_new, sha512_update, sha512_finalize_bytes,
ed25519.Signature.to_bytes, signature.error.Error, Error.new]
— the SHA-512 hash oracle plus the opaque wire-format types. NO curve
axioms, NO scalar axioms, NO backend axioms, enforced on every button press.
Full check.sh green: 16 standard certificates + the apex audit.
Phase 2 (the point-level equation [s]B − [k]A = decompress R, needing
to_bytes canonicity and decompress) remains deferred and documented.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-04 17:45:55 +00:00
else
PHASE 2 HALF-LIFT PROVEN: verify_accepts_iff_point, button-enforced
THE THEOREM (CurveFieldProofs.verify_accepts_iff_point): for a parsing
signature, a valid on-curve public-key point, a canonical signature
scalar, and a successful recompute, there is a point R' - the certified
[k](-A) + [s]B, ExtValid and on-curve - with
verifier accepts <=> bytesVal R_bytes
= (edY R').val + ((edX R').val % 2) * 2^255
The apex's byte-for-byte comparison IS point-encoding equality: the
signature's R bytes are accepted exactly when they are THE canonical
encoding of the recomputed point. Axiom cone: EXACTLY the apex boundary
(SHA-512 oracle + wire-format opaques; zero curve/scalar/backend axioms),
now enforced for BOTH apex and half-lift by check.sh Phase 3b.
New machinery in Proofs/PointLiftSpec.lean:
- bind_ok_inv: generic ok-inversion of one monadic bind - the clean way
to invert oracle-bearing chains (axioms cannot be walked).
- recompute_inv: names the recompute chain's intermediates (hash, k,
-A, R') with their defining equations, via eight flat bind_ok_inv
steps after the pass-through reductions.
- Bytes64.exists_bytes + List.exists_len32: the 64-byte destructure -
Lean's match refuses list patterns beyond ~32 elements, so the device
is a 32-cons prefix + a list-level 32-destructure on the tail.
- The assembly: recompute_inv + from_bytes_mod_order_wide_spec (k
canonical) + edwards_neg_law (-A) + vartime_dsm_basepoint_spec (R',
valid, on-curve) + ed_compress_spec (er = canonical encoding) +
rangeEq_iff_bytesVal (byte comparison = value equality), threaded
through the ok-injectivity of the inverted equations.
Full button green fresh, incl. the extended Phase 3b.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-05 14:06:23 +00:00
echo 'APEX AUDIT FAILED: apex/half-lift cone is not the documented boundary' ; exit 1
THE SIGNATURE APEX: the EdDSA verification equation, proven and audited
`Proofs/SigApexSpec.lean`:
- `verify_loop_full` — the extracted 32-byte comparison loop returns exactly
the byte-equality of the two arrays (induction; axiom cone = exactly
[propext, Classical.choice, Quot.sound]).
- `verify_accepts_iff` — THE APEX: for a signature that parses, the
extracted RustCrypto verifier accepts IFF the recomputed compressed point
compress( [s]·B − [k]·A )
equals the signature's R byte-for-byte. The recomputation is grounded in
the PROVEN curve model (every curve and scalar call is a certified
definition); k is whatever scalar the SHA-512 oracle produces — the
honest EdDSA acceptance criterion with the hash opaque.
Boundary hygiene forced by the audit itself:
- The public vartime_double_scalar_mul_basepoint dispatch pulled the AVX2
vector-backend axiom into the apex cone. Fixed at the build level:
extract.sh pins RUSTFLAGS --cfg curve25519_dalek_backend="serial", so the
SIMD arm compiles out; BackendKind has only Serial and
get_selected_backend becomes a real definition (ok Serial).
- subtle.Choice.unwrap_u8 upgraded from axiom to the documented model
definition (Choice := U8; unwrap_u8 = self.0) — it sits on the verify
path via compress → is_negative.
- CurveSig modules added to GEN_MODULES (stale-olean incoherence otherwise).
check.sh grows Phase 3b: the apex certificate's axiom cone must equal
EXACTLY
[propext, Classical.choice, Quot.sound,
ed25519.Signature, sha2.Sha512,
sha512_new, sha512_update, sha512_finalize_bytes,
ed25519.Signature.to_bytes, signature.error.Error, Error.new]
— the SHA-512 hash oracle plus the opaque wire-format types. NO curve
axioms, NO scalar axioms, NO backend axioms, enforced on every button press.
Full check.sh green: 16 standard certificates + the apex audit.
Phase 2 (the point-level equation [s]B − [k]A = decompress R, needing
to_bytes canonicity and decompress) remains deferred and documented.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-04 17:45:55 +00:00
fi
"
verification: bind the statements, the specifications, and the model (P1-a)
Phases 3/3b establish what each certificate RESTS ON. Neither says what it
SAYS, nor what it is ABOUT. A certificate gutted to a tautology of the same
axiom cone passes both; so does one whose reference definition has been
redefined to BE the extracted code, at which point the theorem reads
`loop = loop` and every cone is byte-identical.
Phase 3c closes that. Proofs/Audit.lean emits a canonical block holding the
policy constants, every certificate's fully-elaborated statement (pp.all, so
implicit arguments, instances and universe levels are visible), and the body
of every specification constant transitively reachable from those statements.
Its SHA-256 is pinned in check.sh and the block itself is committed as
AUDIT-MANIFEST.txt, so a mismatch is DIFFED, not merely reported. 31
certificates, 68 specification constants per repository.
Two tiers, not one. These forks have an arithmetic tier that must stay
oracle-free and an apex tier carrying this fork's hash and wire-format axioms,
and the apex boundary genuinely differs per fork (dalek 8 extra names, anza 4,
risc0 and betrusted 5). One shared constant would have widened the arithmetic
tier to accept hash oracles, which is the most valuable property these repos
have. Each auditor is generated from its own repository's policy.
Phase 0b pins the extracted model. This was not a precaution: risc0 and
betrusted were observed emitting BYTE-IDENTICAL audit-manifest digests
(6c821b8e…) while shipping demonstrably different extracted models, their
point-doubling routines differing in operation order. A statement names an
extracted function; it does not contain that function's body. Binding
statements is not binding the subject. Membership derives from the filesystem,
so a new model file fails closed.
selftest-statements.sh attacks both phases with ten cases, each asserting a
specific diagnostic: an edited model body, an unlisted model file, a widened
policy, a hand-edited committed block, a certificate dropped from the auditor
WITH the digest refreshed to match, and a gutted statement whose cone is
unchanged. It lifts the phases out of check.sh at run time, so it attacks the
shipping gate rather than a copy.
Two bugs found and fixed during that testing, both mine: Phase 3c read `$0`
after `cd "$AENEAS_LEAN"`, and $0 is the caller's relative path; and the
axgate self-test compared the tree against a pristine checkout rather than
against how it found it. A third expectation was wrong rather than the code —
widening the apex boundary is caught by the exact-cone requirement before the
digest ever runs, which is a stronger rejection, and the test now says so.
All sixteen runs green at these commits: four main buttons, four axgate
self-tests, four binding self-tests, four scalar buttons.
TRUSTED-BASE.md records what this binds and, at equal length, what it does
not: a digest binds identity, not meaning; an author can rotate the pins in
one commit and is caught by review, not by the script; and pinning the model
says nothing about whether Charon and Aeneas translated the Rust faithfully.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-28 22:38:17 +00:00
echo ""
# ── Phase 3c: statement + specification binding ─────────────────────────────
# WHAT THE EARLIER PHASES DO NOT ESTABLISH. Phase 3 proves each certificate
# rests on exactly the declared axioms; 3b does the same for the apex tier.
# Neither says WHAT THE THEOREM SAYS. A certificate gutted to a tautology of
# the same cone passes both. So does one whose reference definition has been
# redefined to BE the extracted code, at which point the theorem reads
# `loop = loop` and every cone is byte-identical.
#
# Proofs/Audit.lean emits a canonical block holding the policy constants,
# every certificate's fully-elaborated statement, and the body of every
# specification constant transitively reachable from those statements. This
# phase binds the SHA-256 of that block, and the block's INPUT is committed
# too, so a mismatch can be DIFFED rather than merely reported.
#
# To rotate deliberately: run check.sh, take the printed OBSERVED digest, and
# update the constant below AND AUDIT-MANIFEST.txt in the same reviewable
# commit. That the rotation is visible in review is the whole point — an
# author who edits a statement and refreshes the digest in one commit is
# caught by reading the diff, not by this script.
EXPECTED_AUDIT_SHA256 = "c0cfe800f41ce6c12420afb97ad40330b14a2aaad232077e7579e376c48e2ae4"
echo "=== Phase 3c: statement + specification binding ==="
cd " $AENEAS_LEAN "
# The compiler's own exit code is the primary signal; the transcript is only
# corroboration. A timeout or a memory clamp exits non-zero WITHOUT printing
# "error:", so grepping the text alone would let it through.
AUD_RC = 0
AUD_OUT = $( lake env bash -c "
set -uo pipefail
cd '$HERE/gen' && export LEAN_PATH = \" \$ LEAN_PATH:\$ PWD:$HERE \"
cd '$HERE'
LEAN_TIMEOUT = $TIMEOUT LEAN_MEM_MB = 8192 '$HERE/lean-guard' Proofs/Audit.lean 2>& 1
" ) || AUD_RC= $?
if [ " $AUD_RC " -ne 0 ] ; then
echo " AUDIT FAILED — Proofs/Audit.lean exited $AUD_RC : "
tail -20 <<< " $AUD_OUT " | sed 's/^/ /'
exit 1
fi
if grep -q 'error:' <<< " $AUD_OUT " ; then
echo "AUDIT FAILED — Proofs/Audit.lean did not elaborate cleanly:"
grep 'error:' <<< " $AUD_OUT " | head -20 | sed 's/^/ /'
exit 1
fi
BLOCK = $( awk '/AUDIT-MANIFEST-BEGIN/{f=1;next} /AUDIT-MANIFEST-END/{f=0} f' <<< " $AUD_OUT " )
# FAIL CLOSED ON ABSENCE: no block and a matching block must not share a path.
if [ -z " $BLOCK " ] ; then
echo "AUDIT FAILED — no AUDIT-MANIFEST block was emitted (fail-closed)." ; exit 1
fi
GOT_SHA = $( printf '%s\n' " $BLOCK " | sha256sum | cut -d' ' -f1)
if [ " $GOT_SHA " != " $EXPECTED_AUDIT_SHA256 " ] ; then
printf '%s\n' " $BLOCK " > " $HERE /.audit-manifest.observed "
echo "AUDIT FAILED — audit-manifest digest mismatch."
echo " expected: $EXPECTED_AUDIT_SHA256 "
echo " observed: $GOT_SHA "
echo " A statement, a specification body, or a policy constant changed."
echo " First differences against the committed block:"
diff -u " $HERE /AUDIT-MANIFEST.txt " " $HERE /.audit-manifest.observed " 2>/dev/null \
| head -30 | sed 's/^/ /' || echo " (AUDIT-MANIFEST.txt absent — cannot diff)"
rm -f " $HERE /.audit-manifest.observed "
exit 1
fi
# The digest's INPUT must be committed and current, or the diff above would
# compare against a stale reference and quietly mislead the next reader.
if ! printf '%s\n' " $BLOCK " | cmp -s - " $HERE /AUDIT-MANIFEST.txt " ; then
echo "AUDIT FAILED — the committed AUDIT-MANIFEST.txt does not match the emitted block."
echo " (the digest matched, so the committed copy is stale — refresh it)" ; exit 1
fi
# CROSS-CHECK the certificate list against its OTHER two sources in this file:
# the CERTS array (Phase 3) and the apex names Phase 3b actually asks about.
# The apex names are read back out of this script rather than retyped, so a
# fourth copy cannot drift. Without this, a certificate could be dropped from
# the auditor's manifest and nothing would notice.
# Match only the QUOTED commands Phase 3b actually emits. An unquoted match
# also hits this file's own prose ("#print axioms for every certificate...")
# and silently contributes the word "for" as a certificate name.
# NOT "$0": this phase runs after `cd "$AENEAS_LEAN"`, and $0 is the relative
# path the caller used ("./check.sh"), which no longer resolves from there.
# $HERE was resolved absolutely at the top of the script.
APEX_FROM_3B = $( grep -oE "'#print axioms [A-Za-z0-9_.]+'" " $HERE /check.sh " | tr -d "'" | awk '{print $3}' | sort -u)
if [ -z " $APEX_FROM_3B " ] ; then
echo "AUDIT FAILED — could not recover the apex certificate names from Phase 3b." ; exit 1
fi
# Every recovered name must be namespace-qualified; a bare word means the
# pattern drifted onto prose again rather than onto a command.
while read -r n; do
case " $n " in *.*) ; ; *) echo " AUDIT FAILED — recovered apex name ' $n ' is not qualified. " ; exit 1; ; esac
done <<< " $APEX_FROM_3B "
AUD_CERTS = $( grep -o 'AUDITED-CERTIFICATES:.*' <<< " $AUD_OUT " | sed 's/AUDITED-CERTIFICATES: //' | tr ' ' '\n' | sort -u)
BASH_CERTS = $( printf '%s\n' " ${ CERTS [@] } " $APEX_FROM_3B | sort -u)
if [ " $AUD_CERTS " != " $BASH_CERTS " ] ; then
echo "AUDIT FAILED — the auditor's certificate list and this script's have drifted:"
diff <( echo " $BASH_CERTS " ) <( echo " $AUD_CERTS " ) | sed 's/^/ /'
exit 1
fi
grep -o 'statement audit PASSED:.*' <<< " $AUD_OUT " | sed 's/^/ /'
echo " audit-manifest sha256 = $GOT_SHA (matches the committed block byte-for-byte) "
verification: --audit-only mode, and the guard that keeps it from becoming evidence (T1)
Gate work dominates this estate's wall-clock: on 2026-07-29, 3.9 hours of a
session went to Lean re-elaborating proofs nobody had edited while the audit
phases themselves took about fifteen seconds. --audit-only runs every gate
against the artifacts a previous full run left behind: ~60s against ~1280s.
IT IS SAFE ONLY BECAUSE IT REFUSES.
- It requires every shipped .lean to be BYTE-IDENTICAL to a basis recorded by
a previous full run. Not mtimes: `touch` defeats those, and a stale-artifact
check that fails open is worse than no shortcut at all, because a green
button would then describe a corpus that is no longer on disk.
- The basis is gitignored build state, so a fresh clone cannot inherit
permission to skip compiling.
- The closing banner differs and says in words that the run is not evidence.
selftest-auditonly.sh exercises seven cases: no basis, an edited comment
character, a deleted source, a new source, a missing artifact, a truncated
basis, and — asserted as a PASS — every source's mtime touched with bytes
unchanged, which pins the bytes-not-mtimes decision rather than leaving it
implicit. Negative-tested: with the basis comparison disabled a changed source
is wrongly accepted, exit 0 and zero refusals, so the guard is load-bearing.
A PHASE TERMINATOR, because this broke twice. Every self-test lifts a phase
from check.sh by scanning to the next phase marker. The last phase had no
marker after it, so a lift ran to end-of-file and swallowed whatever was
appended later — first Phase 2c into the axgate lift, then T1's tail into the
binding lift, where it referenced $AUDIT_ONLY and died under `set -u`. Both
surfaced as the BASELINE case failing: a self-test blaming a gate for its own
extraction bug. The phases now end at an explicit sentinel and both lifters
stop there, so nothing appended below can silently become part of the last
phase from a lifter's point of view.
TRUSTED-BASE.md records what an audit-only transcript does and does not
establish, and — because it cost a confusing red run today — that lean-guard's
memory clamp presents as `FAIL: Proofs/<module>` while being a resource
condition, not a broken proof.
Verified green: 8 full button runs (four check.sh, four check-scalar.sh) and 20
self-tests across the four repositories, zero red. One earlier run failed on
the memory clamp because the author ran a test suite concurrently; re-run on a
quiet machine, green.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-30 17:16:17 +00:00
# ── Phases end ──────────────────────────────────────────────────────────────
# Sentinel. Self-tests lift a phase by scanning from its header to the NEXT
# marker; without this the final phase's lift ran to end-of-file and picked up
# everything appended afterwards. Do not remove: anything added below this line
# would otherwise silently become part of the last phase from a lifter's point
# of view.
2026-07-02 12:17:44 +00:00
echo ""
verification: --audit-only mode, and the guard that keeps it from becoming evidence (T1)
Gate work dominates this estate's wall-clock: on 2026-07-29, 3.9 hours of a
session went to Lean re-elaborating proofs nobody had edited while the audit
phases themselves took about fifteen seconds. --audit-only runs every gate
against the artifacts a previous full run left behind: ~60s against ~1280s.
IT IS SAFE ONLY BECAUSE IT REFUSES.
- It requires every shipped .lean to be BYTE-IDENTICAL to a basis recorded by
a previous full run. Not mtimes: `touch` defeats those, and a stale-artifact
check that fails open is worse than no shortcut at all, because a green
button would then describe a corpus that is no longer on disk.
- The basis is gitignored build state, so a fresh clone cannot inherit
permission to skip compiling.
- The closing banner differs and says in words that the run is not evidence.
selftest-auditonly.sh exercises seven cases: no basis, an edited comment
character, a deleted source, a new source, a missing artifact, a truncated
basis, and — asserted as a PASS — every source's mtime touched with bytes
unchanged, which pins the bytes-not-mtimes decision rather than leaving it
implicit. Negative-tested: with the basis comparison disabled a changed source
is wrongly accepted, exit 0 and zero refusals, so the guard is load-bearing.
A PHASE TERMINATOR, because this broke twice. Every self-test lifts a phase
from check.sh by scanning to the next phase marker. The last phase had no
marker after it, so a lift ran to end-of-file and swallowed whatever was
appended later — first Phase 2c into the axgate lift, then T1's tail into the
binding lift, where it referenced $AUDIT_ONLY and died under `set -u`. Both
surfaced as the BASELINE case failing: a self-test blaming a gate for its own
extraction bug. The phases now end at an explicit sentinel and both lifters
stop there, so nothing appended below can silently become part of the last
phase from a lifter's point of view.
TRUSTED-BASE.md records what an audit-only transcript does and does not
establish, and — because it cost a confusing red run today — that lean-guard's
memory clamp presents as `FAIL: Proofs/<module>` while being a resource
condition, not a broken proof.
Verified green: 8 full button runs (four check.sh, four check-scalar.sh) and 20
self-tests across the four repositories, zero red. One earlier run failed on
the memory clamp because the author ran a test suite concurrently; re-run on a
quiet machine, green.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-30 17:16:17 +00:00
if [ " $AUDIT_ONLY " = 1 ] ; then
echo "AUDIT-ONLY RUN — GATES PASSED, PROOFS NOT RECOMPILED."
echo "This is NOT evidence: the kernel did not re-elaborate a single proof in"
echo "this run. It says the gates accept the artifacts a previous full run"
echo "left behind. For a recorded result, run ./check.sh with no arguments."
exit 0
fi
# Only a full run earns the right to let a later --audit-only skip compiling.
source_basis > " $BASIS "
2026-07-02 12:17:44 +00:00
echo "ALL PROOFS PASS. ALL CERTIFICATES AXIOM-CLEAN. NO DEAD FILES."
verification: bind the statements, the specifications, and the model (P1-a)
Phases 3/3b establish what each certificate RESTS ON. Neither says what it
SAYS, nor what it is ABOUT. A certificate gutted to a tautology of the same
axiom cone passes both; so does one whose reference definition has been
redefined to BE the extracted code, at which point the theorem reads
`loop = loop` and every cone is byte-identical.
Phase 3c closes that. Proofs/Audit.lean emits a canonical block holding the
policy constants, every certificate's fully-elaborated statement (pp.all, so
implicit arguments, instances and universe levels are visible), and the body
of every specification constant transitively reachable from those statements.
Its SHA-256 is pinned in check.sh and the block itself is committed as
AUDIT-MANIFEST.txt, so a mismatch is DIFFED, not merely reported. 31
certificates, 68 specification constants per repository.
Two tiers, not one. These forks have an arithmetic tier that must stay
oracle-free and an apex tier carrying this fork's hash and wire-format axioms,
and the apex boundary genuinely differs per fork (dalek 8 extra names, anza 4,
risc0 and betrusted 5). One shared constant would have widened the arithmetic
tier to accept hash oracles, which is the most valuable property these repos
have. Each auditor is generated from its own repository's policy.
Phase 0b pins the extracted model. This was not a precaution: risc0 and
betrusted were observed emitting BYTE-IDENTICAL audit-manifest digests
(6c821b8e…) while shipping demonstrably different extracted models, their
point-doubling routines differing in operation order. A statement names an
extracted function; it does not contain that function's body. Binding
statements is not binding the subject. Membership derives from the filesystem,
so a new model file fails closed.
selftest-statements.sh attacks both phases with ten cases, each asserting a
specific diagnostic: an edited model body, an unlisted model file, a widened
policy, a hand-edited committed block, a certificate dropped from the auditor
WITH the digest refreshed to match, and a gutted statement whose cone is
unchanged. It lifts the phases out of check.sh at run time, so it attacks the
shipping gate rather than a copy.
Two bugs found and fixed during that testing, both mine: Phase 3c read `$0`
after `cd "$AENEAS_LEAN"`, and $0 is the caller's relative path; and the
axgate self-test compared the tree against a pristine checkout rather than
against how it found it. A third expectation was wrong rather than the code —
widening the apex boundary is caught by the exact-cone requirement before the
digest ever runs, which is a stronger rejection, and the test now says so.
All sixteen runs green at these commits: four main buttons, four axgate
self-tests, four binding self-tests, four scalar buttons.
TRUSTED-BASE.md records what this binds and, at equal length, what it does
not: a digest binds identity, not meaning; an author can rotate the pins in
one commit and is caught by review, not by the script; and pinning the model
says nothing about whether Charon and Aeneas translated the Rust faithfully.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-28 22:38:17 +00:00
echo "STATEMENTS AND SPECIFICATIONS BOUND TO THE COMMITTED AUDIT MANIFEST."
