saymrwulf 73cc6ecff9 scalar layer: add+sub fully proven mod l against THIS fork's v4 extraction ... This v4.1.x fork implements Scalar52::sub with TWO loops (loop0 = borrow chain; loop1 adds L &&& underflow_mask — the arithmetic-mask constant-time conditional), a genuinely different code path from upstream v5's subtle-based conditional_add_l. Verified per R2 against this fork's own gen: - sub_loop_spec (= loop0): borrow chain, verbatim technique from dalek - sub_loop1_zero_spec / sub_loop1_one_spec: the masked-L add, both mask values (0 / 2^64-1), full carry chains - sub_val_spec: denote(sub a b) = denote a - denote b in ZMod l; the underflow mask um = ((borrow>>>63) XOR 1) - 1 resolved per case - add_loop_spec + add_val_spec: denote(add a b) = denote a + denote b (v4 add_loop extracts token-identical to v5; composition through this fork's own sub_val_spec) check-scalar.sh: full manifest, 5/5 kernel axiom audit [propext, Classical.choice, Quot.sound], green at 300-400s/4096MB. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>		2026-07-03 18:45:17 +02:00
..
gen	Add scalar-layer foundation (Scalar52 arithmetic mod ℓ)	2026-07-02 21:27:33 +02:00
Proofs	scalar layer: add+sub fully proven mod l against THIS fork's v4 extraction	2026-07-03 18:45:17 +02:00
check-scalar.sh	scalar layer: add+sub fully proven mod l against THIS fork's v4 extraction	2026-07-03 18:45:17 +02:00
check.sh	coherence pass 2: restore the one-button property, institutionalize audits	2026-07-03 12:54:30 +02:00
CurveField.llbc	lean-guard: disable core dumps (no more apport popups on capped aborts)	2026-07-02 16:23:31 +02:00
CurveScalar.llbc	Add scalar-layer foundation (Scalar52 arithmetic mod ℓ)	2026-07-02 21:27:33 +02:00
extract-scalar.sh	Add scalar-layer foundation (Scalar52 arithmetic mod ℓ)	2026-07-02 21:27:33 +02:00
extract.sh	lean-guard: disable core dumps (no more apport popups on capped aborts)	2026-07-02 16:23:31 +02:00
lean-guard	lean-guard 3b: global-headroom clamp (sync with control master)	2026-07-03 17:51:18 +02:00