mirror of
https://github.com/saymrwulf/dalek-ed25519-verified.git
synced 2026-09-04 20:24:12 +00:00
saymrwulf
7dff4157a2
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> |
||
|---|---|---|
| .. | ||
| AddSpec.lean | ||
| Basic.lean | ||
| ConstSpecs.lean | ||
| Denote.lean | ||
| EdAddAffNiels.lean | ||
| EdAddProjNiels.lean | ||
| EdConvert.lean | ||
| EdCurve.lean | ||
| EdDenote.lean | ||
| EdDouble.lean | ||
| EdMain.lean | ||
| FeQ.lean | ||
| Field.lean | ||
| FieldMain.lean | ||
| InvertSpec.lean | ||
| MulSpec.lean | ||
| P25519.lean | ||
| ReduceSpec.lean | ||
| ScalarAddSpec.lean | ||
| ScalarDenote.lean | ||
| ScalarLoop.lean | ||
| ScalarSubSpec.lean | ||
| Square2Spec.lean | ||
| SquareSpec.lean | ||
| SubNegSpec.lean | ||