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>
Phase 3 and 3b mktemp an audit file, compile it, then removed only the .lean —
leaving the .olean behind on every run. check-scalar.sh:38 has always done this
correctly (`rm -f "$AUD" "${AUD%.lean}.olean"`); the main script was the odd one
out. Estate-wide that had accumulated 101 orphan compiled modules with no
sibling source (dalek 44, anza/risc0/betrusted 19 each), invisible to git
because *.olean is gitignored. All swept.
The litter was inert — the names are not valid Lean identifiers, so nothing
could import them. It matters as a pattern: an audit whose verdict can depend on
untracked build state is the class of defect that took eight review rounds to
close in the sibling SLH-DSA repository (there: an orphan .olean with its source
deleted satisfied an import and the button went green). A build-hygiene phase
that purges compiled artifacts and bans stray files is the proper fix and is
queued as part of the protocol port; this commit stops the bleeding.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
- README: pyramid-diagram apex row upgraded to the proven full lift
(accepted <=> decompress(R) = [k](-A)+[s]B), status table names all
four button-enforced tiers, apex section gains the phase-2 tier table
(half-lift / point equation / full lift) + the decompress-chain
summary; source pin updated to the pushed patch commit.
- TRUSTED-BASE item 5: rewritten from the single byte-apex certificate
to the FOUR enforced tiers (decompress_of_canonical noted as
standard-three-only).
- gen/CurveField/FunsExternal.lean: stale root-namespace
edwards.decompress.step_1/step_2 axioms removed (dead weight left
behind by un-opaquing; outside every cone, but they forced
fully-qualified unfolds - see control FAILURES.md).
- check.sh Phase 3b success echo aligned to "apex + full-lift" (echo
only; the enforcing greps covered all four tiers already).
Validated by the pass-4 sweep: 9/9 buttons green (this repo's check.sh
+ check-scalar.sh among them), logs retained in the pass workspace.
Full record: formal-verification-control/COHERENCE-PASS-4.md.
Co-Authored-By: Claude Fable 5 <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>
- README: the pyramid diagram claimed the cofactored ZIP-215 equation,
which is NOT the proven statement - corrected to the actual theorem
(accepted IFF compress([s]B-[k]A) = R, byte-for-byte) and the signature
row now names verify_accepts_iff; new "The signature apex (phase 1)"
section states the theorem, this repo's glue architecture, the exact
button-enforced axiom cone, and the phase-2 deferral.
- TRUSTED-BASE: item 5 rewritten from an aspirational hash paragraph to
the structural boundary - certificate name, exact allowed cone, and the
Phase 3b enforcement that fails the build on any deviation.
- Dead pre-merge artifacts removed: gen/CurveScalar, CurveScalar.llbc,
extract-scalar.sh (the merged gen/CurveField universe is the single
model; check-scalar.sh remains the scalar button, header updated).
- lean-guard: Guard 3a retry ladder (LEAN_MEM_WAIT_SEC) - a clamped run
that dies on memory retries as headroom improves, converting ambient
memory pressure from a deterministic abort into a delayed pass.
Fresh green buttons after these changes: check.sh (incl. Phase 3b apex
audit) + check-scalar.sh, both at shipped defaults, coherence pass 3
sweep 2026-07-05.
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>
extract.sh now opens crate::backend::serial::scalar_mul::vartime_double_base
(the other scalar_mul strategies stay opaque): non_adjacent_form (with its
loops), NafLookupTable5 (from/select), the curve-model helpers and
vartime_double_base::mul itself land in gen/CurveField - the same
namespace as the proven edwards operations, so the coming double-and-add
induction can consume EdDouble/EdAddProjNiels/EdConvert directly.
Zero sorries, zero external axioms (the pinned sources carry documented
compat refactors: single-assignment loop helpers, param-rooted while,
always-256-iterations, index-based LE load).
Full check.sh pressed fresh over the regenerated model: every existing
field and group-law certificate still green and axiom-clean - the scope
extension is purely additive.
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>
- check.sh: proofs memory default 6144 -> 8192 (ReduceSpec's norm_num
step peaks above 6144; guard aborted gracefully — R3 was broken, S1
held). Matches pasta's calibration.
- check.sh: dead-file gate now exempts Scalar* (delegated to
check-scalar.sh); the gate had been un-passable since the scalar layer
landed, masked by the memory failure.
- check.sh: axiom-audit phase routed through lean-guard (cgroup + flock;
was raw lean -M), audit temp file moved into the workspace (lake env
rejects /tmp inputs — the /tmp phase had never run green).
- check-scalar.sh: NEW Phase 3 kernel axiom audit — ScalarProofs.L_val
must report exactly [propext, Classical.choice, Quot.sound].
- README: signature layer '⏳ planned' (was 'in progress' with nothing
started); planned certificate names marked as such.
Validated: full check.sh + check-scalar.sh green end-to-end in the pass-2
sweep (see formal-verification-control/COHERENCE-PASS-2.md).
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>
