- 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>
`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>
Gen merge: extract.sh now co-extracts the Scalar52 backend and the public
scalar::from_bytes_mod_order[_wide] conversions into the SAME CurveField
model, so the whole library — field, curve_models, edwards, scalar — shares
one type universe (Scalar is a single structure, not two). The scalar proof
chain repoints by one import line (ScalarDenote: CurveScalar.Funs ->
CurveField.Funs); check-scalar.sh's gen list follows. Both buttons — the
scalar certificates and the field/group/dsm certificates — pass fresh over
the merged gen, so the merge is proven-safe, not merely hoped-safe.
Verify glue (gen/CurveSig): the extracted ed25519-dalek verify_sha512 path,
integrated against the proven model:
- TypesExternal.lean imports CurveField.Types, so CompressedEdwardsY /
EdwardsPoint / Scalar in the glue ARE the proven model's types. Only the
genuinely foreign types stay opaque: sha2.Sha512, ed25519.Signature,
signature.error.Error.
- FunsExternal.lean imports CurveField.Funs, so every curve/scalar call
(compress, vartime_double_scalar_mul_basepoint, as_bytes, neg,
from_bytes_mod_order[_wide]) resolves to a proven definition — no axioms.
The `?`-operator plumbing (Try::branch, FromResidual::from_residual) and
compressed_from_bytes get real definitions. Only the SHA-512 hasher
(sha512_new/update/finalize_bytes) and two opaque wire accessors
(Signature.to_bytes, Error.new) remain axiomatized — the deliberate,
documented hash-oracle boundary.
Audited: `verify_sha512`'s entire axiom cone is
[propext, Classical.choice, Quot.sound,
sha2.Sha512, sha512_new, sha512_update, sha512_finalize_bytes,
ed25519.Signature.to_bytes, signature.error.Error.new]
— zero curve axioms, zero scalar axioms. The verify path is definitionally
grounded in the certified model; the only trust boundary is SHA-512.
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>
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.
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.
extract-scalar.sh: function-level roots (add/sub/mul/square/montgomery_*)
yield a 28-def Scalar52 limb-arithmetic gen with ZERO iterator/byte/wrapper
entanglement — the byte-serialization and high-level Scalar wrapper (which
pull untranslatable chunks/zip iterators) are excluded by scoping, not faked.
Proofs/ScalarDenote.lean (compiles, axiom-clean): Ell = ℓ = 2^252+..., the
Scalar52 denotation ⟦·⟧ : Scalar52 → ZMod ℓ, the ScBnd 52-bit limb invariant,
and L_val — the transpiled constants::L denotes EXACTLY the group order ℓ
(kernel-checked, no native_decide).
add/sub (Range-loop conditional reductions, tractable — field-layer pattern)
and the Montgomery mul path (shares pasta's big-coefficient kernel limit) are
in progress. check-scalar.sh is green for the foundation.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Ported from the locally verified Hermes working copy; FeQ and Square2Spec
(dead files in the published replica) now compile and are in the check
manifest. check.sh gates: source integrity, stub audit, zero axiom
declarations under Proofs/, per-certificate axiom audit.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
