- 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>
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>
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.
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>
