(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>
kernel-audited)
Proofs/FromBytesSpec.lean: FieldElement51::from_bytes is exact below bit
255 - for any 32 input bytes it succeeds with 51-bit limbs denoting
bytesVal b mod 2^255 (the sign bit is discarded, everything else is the
little-endian value). This is the y-parse of decompression: a canonical
encoding parses to exactly its y-residue.
- load8_at_spec: generic 8-byte little-endian loader (the disjoint-OR
idiom with the product-order-robust or_add_low helper; per-round clear
hygiene cured a fat-context elaboration timeout).
- window_extract / window_shift / digits_tile: the pure window algebra -
five 64-bit windows at byte offsets 0/6/12/19/24, shifted 0/3/6/1/12,
tile bits 0..254 exactly (base-2^51 digit identity).
- from_bytes_spec: the walk composing them; the five window equations
come from ring-verified low/window/high decompositions of the byte sum.
Certificate exact standard three; full button green fresh. Next:
decompress_of_canonical (step 3/5).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
(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>
(kernel-audited)
- fe_cond_assign_spec: the per-limb constant-time selection on field
elements (real extracted code: five index_mut rounds over the u64
select) keeps self iff the choice is 0 - the operation sqrt_ratio_i
uses for both the root flip and the sign normalization. Walked with
backfun-rewrite hygiene; the u64 model lemma restated locally
(Proofs.Basic is a parallel root that clashes with ConstSpecs).
- sqrt_core: THE ALGEBRAIC HEART - for square u/v (witness x, v nonzero)
the candidate r = (u*v^3)*(u*v^7)^((p-5)/8) satisfies v*r^2 = +/-u.
The v-part of the exponent collapses by Fermat (8*(2^253-5) = 2(p-1));
the residual x^((p-1)/2) is +/-1 by factoring its square. Exponent
bookkeeping: (p-5)/8 = 2^252-3, (p-1)/2 = 2^254-10, all closed by
norm_num after pow_mul merges.
Both certificates exact standard three. Full button green fresh.
Remaining: the sqrt_ratio_i walk composing these, from_bytes,
decompress_of_canonical.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Proofs/DecompressSpec.lean, the arithmetic ingredients of sqrt_ratio_i:
- pow_p58_spec: a^((p-5)/8) = a^(2^252 - 3) via the pow22501 chain (the
invert_spec pattern).
- fe_ct_eq_spec: the constant-time field comparison DECIDES denotational
equality - because to_bytes is canonical (to_bytes_spec), byte equality
is residue equality in both directions. Supporting bridge lemmas:
bytesVal_inj (little-endian digits are unique, so value equality forces
list equality), bytesVal_congr, bytes_eq_iff_denote.
- sqrt(-1) needs no new work: ConstSpecs.sqrt_m1_spec (the constants
campaign) already pins SQRT_M1 to Bnd + denote*denote = -1.
Both new certificates exact standard three; full button green fresh.
Remaining in the chain: the sqrt_ratio_i success-case walk, from_bytes,
decompress_of_canonical.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
button-enforced (phase-2 goal reached on dalek)
CurveFieldProofs.verify_accepts_iff_point_eq: under the half-lift's
hypotheses, for ANY valid on-curve point Q whose canonical encoding is
the signature's R bytes,
verifier accepts <=> Q = [k]*(-A) + [s]*B (as denoted points)
- the literal point-level EdDSA verification equation, no decompress
needed: the canonical encoding is INJECTIVE on curve points.
Proofs/PointEqSpec.lean:
- one_add_d_y_sq_ne_zero: 1 + d*y^2 never vanishes - d nonsquare
(edD_not_square, the completeness ingredient doing its second job)
vs -1 a square (p = 1 mod 4).
- x_sq_of_onCurve + enc_inj_coord: the curve equation determines x^2
from y; +/-x have different parities mod an odd prime unless x = 0,
so y-residue + parity bit determine the point.
- enc_point_inj (standard three axioms): equal canonical encodings of
valid on-curve points force equal denoted points.
- verify_accepts_iff_point_eq: half-lift + injectivity. Axiom cone
EXACTLY the apex boundary; Phase 3b now enforces all THREE tiers
(byte apex, half-lift, point equation).
Remaining phase-2 garnish: the constructive decompress specs (sqrt
chain), giving "the accepted bytes decompress to the recomputed point".
Full button green fresh.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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>
bridge (Proofs/PointLiftSpec.lean, kernel-audited)
- vartime_dsm_basepoint_spec: the PUBLIC dsm entry the verifier calls
(EdwardsPoint::vartime_double_scalar_mul_basepoint) satisfies the dsm
certificate - under the serial pin the backend dispatch is the real
constant Serial, so the wrapper reduces definitionally to the certified
serial path. No new axioms; in CERTS.
- rangeEq_iff_bytesVal: the verifier's byte-wise comparison IS value
equality of the encodings - little-endian digits are unique (32-fold
byte peel, one omega over the flat bound set; U8 equality recovered via
UScalar.eq_of_val_eq).
With ed_compress_spec and from_bytes_mod_order_wide_spec already landed,
the half-lift now needs only the recompute bind-chain inversion (the sha
calls are oracles - inverted from the hrec hypothesis the apex carries)
and the assembly theorem. Full button green fresh.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
(from_bytes_mod_order_wide_spec, kernel-audited)
Proofs/ScalarPackSpec.lean:
- scalar52_to_bytes_spec: Scalar52::to_bytes (the PACK step - pure
bit-packing at radix 2^52, no reduction) serializes canonical limbs to
exactly their value: bytesVal s = scVal a. Second application of the
ToBytesSpec walk generator; boundary bytes 6 and 19 only (the two
non-byte-aligned 52j offsets), disjoint ORs to additions as before.
- from_bytes_mod_order_wide_spec: the verifier's k = SHA-512-to-scalar
entry composes from_bytes_wide_spec (the proven mod-l reduction) with
the pack: for 64 input bytes of value T, the returned Scalar's 32
bytes denote V with V < l and V = T (mod l) - precisely the scalar
premises vartime_double_base_mul_spec consumes (V < l < 2^253).
- byte_split_52_4: the offset-4 chunk split for 52-bit limbs; the five
ToBytesMath byte_split_* lemmas shed their unused 2^51 premises (pure
telescopes, valid for all f).
Both certificates exact-standard-three. Full button green fresh.
Half-lift remaining (mapped in memory): dsm dispatch wrapper, recompute
bind-chain inversion, bytesVal injectivity, assembly in PointLiftSpec.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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>
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>
`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>
- `Proofs/DsmNafLoadSpec.lean` (generated) — the byte-to-word LE load of
`non_adjacent_form`: four 8-peel inner walks (t |= bytes[8k+bi] << 8bi)
and the outer 4-peel filling x_u64[0..3]; x_u64[4] stays 0 (the pad word
the cross-word window reads at positions >= 251).
- `Proofs/DsmNafMath.lean` — the pure arithmetic of the w=5 digit loop:
`nafSum`/`nafSum_set`; window-read lemmas `naf_window_single` /
`naf_window_cross` (cross-word disjoint-OR read sees (V >> pos) mod 32);
invariant steps `naf_even_step` / `naf_odd_step` (Nat.mod_mul telescope:
digit + promoted carry reconstruct the consumed bits EXACTLY, in ZZ);
carry-kill `naf_carry_even` / `naf_carry_odd` (V < 2^253 forces the
carry dead before bit 256); `naf_exit` (nafSum naf 256 = V exactly).
The digit-loop walk (stage 3) composes these next; its invariant is
nafSum naf 256 + carry*2^pos = V mod 2^pos
with digits at k >= pos all zero and carry = 1 -> pos <= 254.
CERTS += naf_load_spec, naf_window_cross, naf_exit (axiom-clean).
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.
Phase B - montgomery_reduce (Proofs/ScalarMontSpec.lean + Proofs/ScalarReduceSpec.lean):
- mont_key: LFACTOR*L0 + 1 = 214835089243030*2^52 (the -1 inverse identity, norm_num)
- mont_cancel: (s + ((s*LFACTOR) % 2^52)*L0) % 2^52 = 0 via Nat.ModEq - every
part1 shift is an EXACT division, nothing discarded
- part1_spec / part2_spec: per-round helpers (carry*2^52 = sum + p*L0; exact split)
- mont_head_telescope (E0-E4) and mont_tail_telescope (E5-E8): linear_combination
certificates with weights 2^52k; mont_bound: X' < 2*ell from Z < 2^260*ell
- montgomery_reduce_spec: post `scDenote r * 2^260 = Z` in ZMod ell + 52-bit bounds.
METHOD-4 split at the round-4/5 boundary: the 74-step monolith is
elaboration-pathological; each half compiles in ~25s/3GB.
- The single death-spiral line: an omega for the nonce-sum bound with ~110
hypotheses in context never returns; extracted to nonce_sum_bound (5 hypotheses,
instant). Bisected with fail-probes; documented in control-repo FAILURES.md.
Phase C - mul (Proofs/ScalarFullMulSpec.lean):
- RR_limbs/RR_scVal/RR_lt; RR_denote: RR = 2^520 - K*ell kernel-checked, so
⟦RR⟧ = R^2; R_isUnit: 2^260 unit of ZMod ell (coprime oddness witness)
- mul_spec: mul_internal -> montgomery_reduce -> mul_internal(*, RR) ->
montgomery_reduce composed; column values folded by `ring`; R cancelled via
IsUnit.mul_right_cancel. Hypothesis scVal a * scVal b < 2^260*ell (honest
Montgomery bound; canonical inputs satisfy it).
Aggregate (Proofs/ScalarMain.lean): scalar_add/sub/mul_correct on ScBnd
interfaces + canonical_mul_bound + scalarImplementation bundling all three.
sub_val_spec/add_val_spec posts strengthened with result-limb 52-bit bounds
(the montgomery tail feeds sub's output back into mul_internal).
check-scalar.sh: 9 proof files, 10 kernel audits (was 6), all exactly
[propext, Classical.choice, Quot.sound]. Button pressed fresh: green.
Proofs/ScalarMulSpec.lean (axiom-clean, no sorry):
- m_spec: the widening 52x52->104-bit product helper — total, exact
- mul_internal_spec: all NINE schoolbook column sums proven exact
(z_k = sum_{i+j=k} a_i*b_j) and bounded (each product < 2^104, each
column < 2^107) through the 60-step straight-line extraction
This is the half of Scalar52::mul that the kernel-capacity frontier does
NOT touch. Phase B — montgomery_reduce (74 steps, part1/part2, the
Montgomery invariant result = input * R^{-1} mod l with R = 2^260, and
the double-round composition through RR) — remains the open frontier,
now precisely one function wide.
check-scalar.sh: ScalarMulSpec in manifest + audit (6/6 clean), green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Proofs/ScalarAddSpec.lean, axiom-clean, no sorry:
- add_loop_spec: the 5-limb carry loop unrolled (same skeleton as the
proven conditional-add-L chain, with b's limbs in place of L's
constants); per-limb equations r_i + 2^52*g_(i+1) = a_i + b_i + g_i.
- add_val_spec: denote(add a b) = denote a + denote b in ZMod l for
limb-bounded canonical inputs. Composition: add_telescope lifts the
carry equations to scLimbs sum + 2^260*g5 = scVal a + scVal b;
canonicity (a,b < l < 2^253) forces g5 = 0; the trailing sub(sum, L)
goes through sub_val_spec with subtrahend L — enabled by weakening
sub_val_spec's hypothesis from scVal b < l to scVal b <= l (the
gamma5=1 forcing argument only needs <=), since scVal L = l exactly.
denote L = 0 in ZMod l closes it.
check-scalar.sh: ScalarAddSpec in manifest + audit (5/5 clean), button
green at the re-budgeted 300s/4096MB caps.
With sub (previous commit): the scalar layer's + and - are both fully
verified against dalek's own extraction. Remaining: x3 fork port,
Montgomery mul/reduce (kernel frontier).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
sub_val_spec closes the top-level two-clause value spec:
denote(Scalar52.sub a b) = denote(a) - denote(b) in ZMod l
for limb-bounded inputs with canonical subtrahend (scVal b < l).
Axiom-clean [propext, Classical.choice, Quot.sound]; no sorry.
The assembly documented-as-remaining last session is now done. Key resolutions:
- Applied the WP "spec_bind" rule manually instead of "step", and reduced the
resulting "let (difference,borrow) := (dw,w)" Prod-let with an explicit
"show" — this was the destructuring friction that blocked the earlier
attempt (step's arity heuristics mis-typed the pair result).
- Inlined the subtle "Choice::from" identity (no step-spec, like csel_step).
- PERFORMANCE: kept "scLimbs" as opaque atoms in the gamma5=1 derivation
instead of "unfold ... at *" — the unfold exploded omega with 2^52..2^260
coefficients and blew past 600s; atomic form proves in ~1 min (METHOD 4,
same kernel-cost discipline as the field layer).
- The 2^260 borrow-wrap and the +l conditional-add cancel in ZMod l:
beta5=0 direct; beta5=1 forces top carry gamma5=1 from scVal b < l, closed
by linear_combination over the two telescopes (sub_telescope, add_telescope).
check-scalar.sh: sub_val_spec in the manifest + Phase-3 audit (4/4 clean);
proof-phase caps raised to 600s/8192MB for the assembly; full button green.
exponentiation.threshold raised to 300 for the 2^260 literal.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
New in Proofs/ScalarSubSpec.lean (all axiom-clean [propext, Classical.choice,
Quot.sound], no sorry, no native_decide):
- nat_and_mask52 / nat_shift52 / nat_shift63 : 52/63-bit ops -> %,/
- sub_step_arith : isolated per-limb borrow accounting (tiny ℕ context,
correction-on-the-left so no truncated subtraction) — the METHOD-4
discipline that keeps 2^260-scale coefficients out of any one certificate
- sub_loop_spec : the FULL 5-limb borrow chain of Scalar52::sub, unrolled
via loop_step/range_next_*; wrapping_sub, 52-bit mask store, borrow-out
bit. This is the loop unroll that blocked the earlier attempt.
- csel_step : step-spec for the subtle conditional_select (faithful model)
- cond_add_l_zero_spec / cond_add_l_one_spec : BOTH cases of conditional
add-of-L, full carry chains; the condition-1 case steps the addend as a
clean value so the index_mut write-back matches sub_loop's pattern
- sub_telescope / add_telescope : the 2^52i-weighted value telescopes to
2^260, discharged by omega (no kernel-capacity blowup)
check-scalar.sh: ScalarSubSpec added to the compile manifest; Phase-3 axiom
audit extended to sub_loop_spec + cond_add_l_one_spec (3/3 clean). Full
button green.
Honest boundary: top-level sub_val_spec (⟦sub a b⟧ = ⟦a⟧-⟦b⟧ in ZMod ℓ)
is documented as remaining — every lemma it needs is proven; what's left is
the Aeneas binding-arity for destructuring sub_loop_spec's pair-valued
multi-existential postcondition inside the do-block, a mechanical not a
mathematical gap. No sorry shipped (Invariants H1/H4).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Reusable infrastructure for the scalar Range-loop reductions (sub_loop,
add_loop, conditional_add_l). Re-stated standalone so scalar proofs stay
independent of the field gen tree. Compiles axiom-clean.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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>
