mirror of
https://github.com/saymrwulf/dalek-ed25519-verified.git
synced 2026-09-04 20:24:12 +00:00
mrwulf
69064a1a3c
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> |
||
|---|---|---|
| .. | ||
| 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 | ||
| ScalarDenote.lean | ||
| Square2Spec.lean | ||
| SquareSpec.lean | ||
| SubNegSpec.lean | ||