2 commits

Author	SHA1	Message	Date
mrwulf	3d3cb9d0d5	Scalar layer complete: Montgomery reduction + full mul ported, scalarImplementation aggregate ... Port of the dalek Montgomery stack against THIS fork's own extraction (gen sections byte-identical, proofs recompiled from scratch here): - Proofs/ScalarMulSpec.lean - mul_internal: 9 exact schoolbook columns - Proofs/ScalarMontSpec.lean - part1/part2 exact-division rounds (LFACTOR*L0 = -1 mod 2^52), head/tail telescopes, mont_bound, tail walk - Proofs/ScalarReduceSpec.lean - montgomery_reduce main walk: scDenote r * 2^260 = Z in ZMod ell + 52-bit output bounds - Proofs/ScalarFullMulSpec.lean - mul = double Montgomery round through RR = R^2 mod ell; R cancelled as a unit; post: [mul a b] = [a]*[b] - Proofs/ScalarMain.lean - scalarImplementation aggregate (ScBnd interfaces; canonical inputs discharge the Montgomery bound) sub_val_spec/add_val_spec posts strengthened with result-limb bounds. check-scalar.sh: 9 proof files, 10 kernel audits, all exactly [propext, Classical.choice, Quot.sound]. Button pressed fresh: green.	2026-07-03 21:36:35 +02:00
saymrwulf	962fa89e06	scalar layer: add+sub fully proven mod l (port from dalek, own extraction) ... 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>	2026-07-03 18:17:30 +02:00