mirror of
https://github.com/saymrwulf/dalek-ed25519-verified.git
synced 2026-09-03 20:13:48 +00:00
saymrwulf
0120fe971a
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>
|
||
|---|---|---|
| .. | ||
| gen | ||
| Proofs | ||
| check-scalar.sh | ||
| check.sh | ||
| CurveField.llbc | ||
| CurveScalar.llbc | ||
| extract-scalar.sh | ||
| extract.sh | ||
| lean-guard | ||