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>
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>
verify_accepts_iff_point_eq, button-enforced
Port of dalek's PointEqSpec (the encoding-injectivity mathematics is
fork-independent; compiled first try): for any valid on-curve point Q
whose canonical encoding is the signature's R bytes, the verifier
accepts IFF Q equals the recomputed point as denoted affine points -
the literal point-level EdDSA verification equation, no decompress
needed. enc_point_inj carries the standard three axioms; the equation
itself carries exactly this fork's enforced apex boundary, and Phase 3b
now audits all three tiers (byte apex, half-lift, point equation).
Full button green fresh.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
THE HALF-LIFT IS NOW PROVEN ON ALL FOUR PYRAMIDS. anza's shape: the hash
oracle is one sha512_hash3 bind, -A is the STORED minus_A field (no
negation call), and the scalar arrives already parsed - so the recompute
inversion is five flat bind_ok_inv steps (two anonymous slice reads, the
oracle, the reduction, the dsm) and the assembly takes ExtValid/OnCurveExt
of self.minus_A directly. Files 1-4 are dalek's verbatim modulo the
curve25519 namespace; every proof compiled FIRST TRY.
verify_accepts_iff_point: accept IFF the signature's R bytes are the
canonical encoding of the recomputed [k]*minus_A + [s]*B (valid,
on-curve, certified model). Five new standard certificates; Phase 3b
enforces anza's tight boundary (SHA-512 oracle + foreign Signature type
+ its two accessors) on BOTH apex and half-lift. Full button green fresh.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
FOURTH AND FINAL PYRAMID CAPPED - the signature layer is complete on all
four ed25519 forks. anza's verify code lives in the same crate as the
curve (solana-ed25519), so the whole verify path joins the merged
CurveField extraction directly: one universe, no glue layer, no FQ-name
welding, and the Error enum plus the parse/filter helpers are all real
extracted code.
- extract.sh: verify_sha512 start-from joins the merged stanza;
sha512_hash3 and the foreign ed25519 crate opaque; RUSTFLAGS
--cfg curve25519_serial_only pins the serial backend so
get_selected_backend extracts as the real constant Serial (the stale
dispatch axiom is deleted from FunsExternal).
- gen/CurveField externals: real defs for the ?-operator plumbing
(Try::branch, FromResidual) and faithful identity models for
Choice::unwrap_u8 (transparent-u8 body: self.0) and the RangeFull
get_unchecked[_mut] raw-pointer pair (Rust body returns the pointer
unchanged) - the three would-be cone intruders, eliminated.
- Proofs/SigApexSpec.lean: verify_loop_full (standard three-axiom cone)
and verify_accepts_iff - the verifier accepts IFF the recomputed
compress([k](-A) + [s]B) equals the signature's R byte-for-byte, with
the ZIP-215 legacy filters and the s < l parse conditioned by
hypotheses, mirroring the siblings' hparse.
- check.sh Phase 3b enforces the apex cone to be EXACTLY
[propext, Classical.choice, Quot.sound, ed25519.Signature,
ed_sigs.sha512_hash3, ed25519.Signature.r_bytes,
ed25519.Signature.s_bytes]
- the tightest boundary of the four pyramids: the SHA-512 oracle plus
the foreign wire-format type and its two byte accessors, nothing else.
check.sh (incl. Phase 3b) + check-scalar.sh both green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Same architecture as the dalek/risc0/betrusted forks: the Scalar52
arithmetic start-froms (11 fns) plus scalar::from_bytes_mod_order[_wide]
join the CurveField extraction, so the field, curve, and scalar layers
share a single type universe - the prerequisite for the signature apex,
whose verify glue must see curve AND scalar calls resolve to proven
definitions by fully-qualified name.
Proofs/ScalarDenote.lean flips its import CurveScalar.Funs ->
CurveField.Funs (one line; the whole scalar proof chain recompiles
unchanged on the merged gen). check-scalar.sh repoints its GEN list.
gen/CurveScalar retained until the deprecation pass, as on the siblings.
check.sh + check-scalar.sh both green, all certificates axiom-clean.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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>
Three new proof files over the CurveField extraction, composing the proven
group-law layer (no new axioms, no associativity assumed — computational
layering over the abstract `edAdd`):
- `Proofs/DsmTableSpec.lean` — `NafLookupTable5::from(&A)`: the 8 entries
are valid `ProjectiveNielsPoint` caches of valid on-curve points denoting
the odd multiples A, 3A, ..., 15A as the `edOdd` double-and-add recursion.
7 explicit loop peels over edwards_as_projective_niels_spec /
add_projniels_law / compl_as_extended_law, seeded by edwards_double_law.
`select`: both masserts (x odd, x < 16) DISCHARGED — panic-freedom is
proven, not assumed; post enumerates all 8 digit cases.
- `Proofs/DsmStepSpec.lean` — `proj_double_law` (the projective doubling
denotes `edAdd P P`; same Z^2-scaled linear_combination discipline as the
extended-coordinate law), `compl_as_projective_law` ((X:Z),(Y:T) to
(XT:YZ:ZT) preserves the point), `naf_select_entry` (digit-indexed lookup
returns THE entry: NafEntryOf r A ((x-1)/2)), and `dsm_step_p_law` /
`dsm_step_b_law`: the three-way NAF digit step denotes `edDigit` — add
the d-th odd multiple, add its negation, or pass through.
- `Proofs/DsmLoopSpec.lean` — the 256-iteration Straus loop by GENUINE
induction on the counter (one symbolic body walk, no unrolling):
`dsm_loop_spec` — from the identity, the loop returns a valid on-curve
point denoting `dsmFold ... edId 256`, the abstract double-and-add fold
of both digit arrays over the table points. Digit and table hypotheses
are exactly what the NAF spec and naf_table_spec provide (layering).
check.sh wired: PROOFS + AUDIT_IMPORTS + 7 new CERTS (naf_table_spec,
naf_select_spec, proj_double_law, compl_as_projective_law, dsm_step_p_law,
dsm_step_b_law, dsm_loop_spec), each `#print axioms`-audited to exactly
[propext, Classical.choice, Quot.sound]. Full check.sh green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The apex brick of the scalar layer: for any 64 bytes (the opaque SHA-512
digest), [from_bytes_wide bytes] = (LE 512-bit value) mod l, with
canonical 52-bit-bounded output. Composition: bytes_unpack_spec (8x8
loops) -> split_words_lo/hi_spec (exact div/mod per limb, disjoint ORs
as additions) -> wide_split_telescope (isolated omega) -> montgomery_mul
by R and RR (R cancels as a unit, RR restores it) -> the canonical add.
The two kernel-capacity walls found and crossed en route (control repo
FAILURES.md updated):
- a montgomery_mul inside any walk motive replays its 400-line body at
every kernel step (fix: named prefix functions in the pinned source);
- straight-line IndexMut closure chains make kernel defeq exponential in
depth (fix: struct-literal construction - the split halves now build
Scalar52([...]) directly). Full certificate: 77 s kernel-inclusive.
Regenerated gen (sources factor from_bytes_wide -> from_bytes_wide_parts
-> split_words_lo/hi; documented pure refactors, cargo-checked).
check-scalar.sh: 13 proof files, 13 kernel audits, all exactly
[propext, Classical.choice, Quot.sound]. Button pressed fresh: green.
Toward Scalar::from_hash: bytes_unpack_spec proves the from_bytes_wide
word-unpack loops pack 64 little-endian bytes into 8 words exactly.
- Proofs/ScalarBytesSpec.lean (3308 lines): bytes_word_loop_spec_0..7,
each split head/tail at j=4 (the 8-fold monolith grows exponentially
in elaboration - METHOD 4). Disjoint-bit ORs become additions via
core's Nat.two_pow_add_eq_or_of_lt with explicit calc bridges (the
default simp set literalizes 2^8 -> 256 and breaks pow-form rewrites;
simp only everywhere).
- Proofs/ScalarUnpackSpec.lean: bytes_unpack_spec composes the eight
inner lemmas through the outer loop (iterator start needs a term-level
equality rewrite per peel).
The from_bytes_wide main walk itself is proven at elaboration level
(fail-probe verified end to end) but its single-decl kernel certificate
replays >30min; it ships next as a phase-split (plan in the control
repo's method notes). check-scalar.sh: 12 proof files, 12 kernel audits,
all exactly [propext, Classical.choice, Quot.sound]. Button green.
Canonicity pass (the layer is now closed under its own preconditions):
- sub_val_spec post carries the exact value equation
(exists beta <= 1, scVal r + scVal b = scVal a + ell*beta, with the
underflow guard beta = 1 -> scVal a < scVal b)
- add/montgomery_reduce/mul/aggregate posts all carry scVal r < ell:
canonical inputs give canonical outputs everywhere. Needed because
from_bytes_wide (hash-to-scalar) feeds Montgomery outputs into add.
Hash-to-scalar foundation (toward Scalar::from_hash / EdDSA verify):
- extraction scope + from_bytes_wide (brings constants::R); regenerated gen
- source repos carry a documented Aeneas-compat patch: the bare
`hi[4] = words[7] >> 20` extracts ill-typed at pin bf13c42e; masked
(semantic no-op, words[7] >> 20 < 2^44)
- Proofs/ScalarWideSpec.lean: R constant lemmas (R = 2^260 mod ell,
witness 2^260 = R + 255*ell) and montgomery_mul_spec, the single
Montgomery round: [r]*2^260 = [a]*[b], canonical bounded output
check-scalar.sh: 10 proof files, 11 kernel audits, all exactly
[propext, Classical.choice, Quot.sound]. Button pressed fresh: green.
The solana fork's Scalar52 sub/add/conditional_add_l extract token-identical
to upstream dalek (only the crate namespace differs: curve25519 vs
curve25519_dalek), so ScalarSubSpec/ScalarAddSpec port with the namespace
adjustment and verify against THIS fork's own gen (R2). ScalarLoop
infrastructure included. check-scalar.sh at dalek parity: full manifest +
5/5 kernel axiom audit, green at 300s/4096MB.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Transpile the Scalar52 limb backend (backend::serial::u64::scalar
add/sub/mul/square/montgomery_*) from Rust to Lean via Charon/Aeneas,
scoped at the function level to the iterator-free arithmetic core.
- verification/extract-scalar.sh: function-level Charon/Aeneas extraction
- verification/gen/CurveScalar/{Types,Funs}.lean: transpiled model (28 defs)
- verification/gen/CurveScalar/{TypesExternal,FunsExternal}.lean: hand-written
external models (subtle.Choice + 2 subtle fns; namespace = curve25519)
- verification/Proofs/ScalarDenote.lean: semantic foundation — Scalar52
denotation into ℤ/ℓℤ, limb-bound invariant, and L_val (the transpiled
constants::L denotes exactly the group order ℓ, kernel-checked)
- verification/check-scalar.sh: guarded compile of the four gen modules
plus the denotation foundation
check-scalar.sh passes: gen compiles; denotation + L = ℓ proven.
add/sub/mul remain in progress.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Extraction widened to backend::serial::curve_models + edwards (matching the
reference recipe; extra opaque: backend::scalar_fits_in_128_bits — a
post-reference NAF-path helper whose generated code trips an Aeneas
namespace-shadowing wart). Reference Ed* suite compiles UNCHANGED (same
crate namespace). All proofs pass; both certificates axiom-clean.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
