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