scalar layer: Scalar52::sub FULLY proven mod l (sub_val_spec)

sub_val_spec closes the top-level two-clause value spec:
  denote(Scalar52.sub a b) = denote(a) - denote(b)   in ZMod l
for limb-bounded inputs with canonical subtrahend (scVal b < l).
Axiom-clean [propext, Classical.choice, Quot.sound]; no sorry.

The assembly documented-as-remaining last session is now done. Key resolutions:
- Applied the WP "spec_bind" rule manually instead of "step", and reduced the
  resulting "let (difference,borrow) := (dw,w)" Prod-let with an explicit
  "show" — this was the destructuring friction that blocked the earlier
  attempt (step's arity heuristics mis-typed the pair result).
- Inlined the subtle "Choice::from" identity (no step-spec, like csel_step).
- PERFORMANCE: kept "scLimbs" as opaque atoms in the gamma5=1 derivation
  instead of "unfold ... at *" — the unfold exploded omega with 2^52..2^260
  coefficients and blew past 600s; atomic form proves in ~1 min (METHOD 4,
  same kernel-cost discipline as the field layer).
- The 2^260 borrow-wrap and the +l conditional-add cancel in ZMod l:
  beta5=0 direct; beta5=1 forces top carry gamma5=1 from scVal b < l, closed
  by linear_combination over the two telescopes (sub_telescope, add_telescope).

check-scalar.sh: sub_val_spec in the manifest + Phase-3 audit (4/4 clean);
proof-phase caps raised to 600s/8192MB for the assembly; full button green.
exponentiation.threshold raised to 300 for the 2^260 literal.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

README.md

@@ -27,7 +27,7 @@ in this repository.
 |-------|-------------|--------|-----------------------|
 | Field 𝔽_p          | `fieldImplementation`    | ✅ proven | `[propext, Classical.choice, Quot.sound]` |
 | Group law (Edwards) | `edwardsImplementation`  | ✅ proven | `[propext, Classical.choice, Quot.sound]` |
-| Scalar mod ℓ        | `scalarImplementation` (planned; `L_val`, `sub_loop_spec`, `cond_add_l_*_spec` proven)   | 🔨 foundation+sub | denotation + L=ℓ + sub borrow/carry chains proven; sub value-assembly & mul in progress |
+| Scalar mod ℓ        | `scalarImplementation` (planned; `sub_val_spec` ✅, `L_val`, loop specs proven)   | 🔨 sub done · add/mul next | denotation + L=ℓ + FULL sub (⟦sub a b⟧=⟦a⟧−⟦b⟧ in ZMod ℓ) proven; add & Montgomery mul next |
 | Signature (EdDSA)   | `verifyEquation` (planned)          | ⏳ planned | — |
 
 Status legend: ✅ proven & axiom-audited · ⏳ in progress · ❌ not started.

verification/Proofs/ScalarSubSpec.lean

@@ -51,6 +51,7 @@ open curve25519_dalek
 
 set_option maxHeartbeats 4000000
 set_option linter.unusedSimpArgs false
+set_option exponentiation.threshold 300
 
 namespace ScalarProofs
 
@@ -705,32 +706,111 @@ theorem add_telescope
         + (c0 + 2^52*c1 + 2^104*c2 + 2^156*c3 + 2^208*c4) := by
   omega
 
-/-! ### Top-level `sub_val_spec` — remaining assembly (no `sorry` shipped)
+/-! ### Top-level subtraction value spec -/
 
-Every mechanically hard piece is proven above and kernel-checked:
-  • `sub_loop_spec`   — the full 5-limb borrow chain (wrapping_sub, mask,
-                        borrow-out bit): the loop unroll that blocked the
-                        earlier attempt;
-  • `cond_add_l_zero_spec`, `cond_add_l_one_spec` — both conditional-add-ℓ
-                        cases, full carry chains (the condition-1 case drives
-                        the write-back through a stepped `csel_step` so the
-                        `index_mut` matches `sub_loop`'s working pattern);
-  • `sub_telescope`, `add_telescope` — the 2⁵²ⁱ-weighted value telescopes
-                        up to 2²⁶⁰, discharged by `omega` (no kernel-capacity
-                        blowup — coefficients stay ≤ 2²⁶⁰);
-  • `sub_step_arith`, `csel_step`, the bit↔arith lemmas.
-
-`sub_val_spec` assembles them: unfold `sub`, run `sub_loop`, read
-`borrow >>> 63` into a `Choice`, run `conditional_add_l`, split on the
-underflow bit β5. The value identity in `ZMod ℓ`,
-  ⟦sub a b⟧ = ⟦a⟧ − ⟦b⟧      (canonical inputs, scVal b < ℓ),
-is complete on paper: β5 = 0 gives ⟦d⟧ + ⟦b⟧ = ⟦a⟧ directly; β5 = 1 gives
-the borrow-wrap 2²⁶⁰ and the +ℓ, which cancel in `ZMod ℓ` once the top
-carry γ5 = 1 (forced by scVal b < ℓ). The remaining step is purely the
-Aeneas binding-arity for destructuring `sub_loop_spec`'s pair-valued,
-multi-existential postcondition inside the outer `do`-block — a mechanical,
-not a mathematical or trust gap. Tracked in the control-repo MANIFEST
-scalar `open_frontier`; this file ships only kernel-checked content
-(Invariants H1/H4). -/
+/-- **Scalar subtraction is correct mod ℓ.** For limb-bounded inputs with
+    canonical subtrahend (scVal b < ℓ), the transpiled `Scalar52::sub`
+    denotes ⟦a⟧ − ⟦b⟧ in `ZMod ℓ`. Assembly of `sub_loop_spec` (borrow
+    chain) and `cond_add_l_{zero,one}_spec` (conditional +ℓ) through the
+    two telescopes; the bind is applied manually via `spec_bind` to keep
+    full control of the postcondition destructuring. -/
+theorem sub_val_spec (a b : Sc)
+    (a0 a1 a2 a3 a4 b0 b1 b2 b3 b4 : U64)
+    (ha : (↑a : List U64) = [a0, a1, a2, a3, a4])
+    (hb : (↑b : List U64) = [b0, b1, b2, b3, b4])
+    (hab : a0.val < 2^52 ∧ a1.val < 2^52 ∧ a2.val < 2^52 ∧ a3.val < 2^52 ∧ a4.val < 2^52)
+    (hbb : b0.val < 2^52 ∧ b1.val < 2^52 ∧ b2.val < 2^52 ∧ b3.val < 2^52 ∧ b4.val < 2^52)
+    (hcb : scVal b < Ell) :
+    backend.serial.u64.scalar.Scalar52.sub a b
+      ⦃ r => scDenote r = scDenote a - scDenote b ⦄ := by
+  obtain ⟨hA0, hA1, hA2, hA3, hA4⟩ := hab
+  obtain ⟨hB0, hB1, hB2, hB3, hB4⟩ := hbb
+  unfold backend.serial.u64.scalar.Scalar52.sub
+  step as ⟨sh, hsh⟩
+  step as ⟨mask, hmask⟩
+  have hmaskv : mask.val = 2^52 - 1 := by
+    simp [hmask, hsh, U64.size_def, U64.numBits]
+  -- bind the borrow loop manually
+  apply spec_bind (sub_loop_spec a b mask a0 a1 a2 a3 a4 b0 b1 b2 b3 b4 ha hb hmaskv
+      ⟨hA0, hA1, hA2, hA3, hA4, hB0, hB1, hB2, hB3, hB4⟩)
+  rintro ⟨dw, w⟩ ⟨d0, d1, d2, d3, d4, β1, β2, β3, β4, β5, hdl,
+    hβ1, hβ2, hβ3, hβ4, hβ5, hd0, hd1, hd2, hd3, hd4,
+    he0, he1, he2, he3, he4, hbor⟩
+  simp only at hdl hbor
+  show (do
+    let i1 ← w >>> 63#i32
+    let i2 ← lift (UScalar.cast UScalarTy.U8 i1)
+    let c ← subtle.Choice.Insts.CoreConvertFromU8.from i2
+    let (_, difference1) ← dw.conditional_add_l c
+    ok difference1) ⦃ r => scDenote r = scDenote a - scDenote b ⦄
+  -- borrow >>> 63, cast, Choice
+  step as ⟨i1, hi1⟩
+  have hi1v : i1.val = β5 := by rw [hi1]; exact hbor
+  step as ⟨i2, hi2⟩
+  -- Choice.from is the identity model; inline c := i2
+  simp only [subtle.Choice.Insts.CoreConvertFromU8.from, bind_tc_ok]
+  set cc := i2 with hccdef
+  have hccv : cc.val = β5 := by
+    have hb5 : β5 < 2^8 := by omega
+    rw [hi2, UScalar.cast_val_eq, hi1v]
+    simp only [UScalarTy.U8, UScalarTy.numBits]
+    omega
+  have hdb : d0.val < 2^52 ∧ d1.val < 2^52 ∧ d2.val < 2^52 ∧ d3.val < 2^52 ∧ d4.val < 2^52 :=
+    ⟨hd0, hd1, hd2, hd3, hd4⟩
+  have hTsub : scLimbs d0 d1 d2 d3 d4 + scLimbs b0 b1 b2 b3 b4
+      = scLimbs a0 a1 a2 a3 a4 + 2^260 * β5 := by
+    unfold scLimbs
+    exact sub_telescope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ he0 he1 he2 he3 he4
+  have hsva : scVal a = scLimbs a0 a1 a2 a3 a4 := scVal_eq a a0 a1 a2 a3 a4 ha
+  have hsvb : scVal b = scLimbs b0 b1 b2 b3 b4 := scVal_eq b b0 b1 b2 b3 b4 hb
+  rcases (Nat.le_one_iff_eq_zero_or_eq_one.mp hβ5) with hβz | hβo
+  · -- β5 = 0: no underflow, cond-add is identity on values
+    have hc0 : cc.val = 0 := by rw [hccv, hβz]
+    apply spec_bind (cond_add_l_zero_spec dw cc d0 d1 d2 d3 d4 hdl hc0 hdb)
+    rintro ⟨cw1, cw2⟩ ⟨r0, r1, r2, r3, r4, hrl, hr0, hr1, hr2, hr3, hr4⟩
+    simp only at hrl
+    show scDenote cw2 = scDenote a - scDenote b
+    have hcwval : scVal cw2 = scLimbs d0 d1 d2 d3 d4 := by
+      rw [scVal_eq cw2 r0 r1 r2 r3 r4 hrl]; unfold scLimbs; rw [hr0, hr1, hr2, hr3, hr4]
+    have key : scVal cw2 + scVal b = scVal a := by
+      rw [hcwval, hsva, hsvb]; rw [hβz] at hTsub; simpa using hTsub
+    have hc := congrArg (Nat.cast (R := ZMod Ell)) key
+    push_cast at hc
+    simp only [scDenote]; rw [eq_sub_iff_add_eq]; exact hc
+  · -- β5 = 1: underflow; +ℓ, and the 2^260 wrap cancels in ZMod ℓ
+    have hc1 : cc.val = 1 := by rw [hccv, hβo]
+    apply spec_bind (cond_add_l_one_spec dw cc d0 d1 d2 d3 d4 hdl hc1 hdb)
+    rintro ⟨cw1, cw2⟩ ⟨r0, r1, r2, r3, r4, γ1, γ2, γ3, γ4, γ5, hrl,
+      hgb1, hgb2, hgb3, hgb4, hgb5, hrb0, hrb1, hrb2, hrb3, hrb4,
+      hf0, hf1, hf2, hf3, hf4⟩
+    simp only at hrl
+    show scDenote cw2 = scDenote a - scDenote b
+    have hLsum : (671914833335277 + 2^52*3916664325105025 + 2^104*1367801
+        + 2^156*0 + 2^208*17592186044416 : ℕ) = Ell := by unfold Ell; norm_num
+    have hTadd : scLimbs r0 r1 r2 r3 r4 + 2^260 * γ5 = scLimbs d0 d1 d2 d3 d4 + Ell := by
+      have h := add_telescope r0.val r1.val r2.val r3.val r4.val
+        d0.val d1.val d2.val d3.val d4.val
+        671914833335277 3916664325105025 1367801 0 17592186044416
+        γ1 γ2 γ3 γ4 γ5 hf0 hf1 hf2 hf3 hf4
+      unfold scLimbs; rw [← hLsum]; linear_combination h
+    have hblt : scLimbs b0 b1 b2 b3 b4 < Ell := by rw [← hsvb]; exact hcb
+    -- γ5 = 1, derived with scLimbs kept as opaque atoms (no 2^52i unfold →
+    -- omega stays cheap: 4 atoms + one 2^260 literal + Ell as an atom)
+    have hrlt : scLimbs r0 r1 r2 r3 r4 < 2^260 := by unfold scLimbs; omega
+    have hd_eq : scLimbs d0 d1 d2 d3 d4 + scLimbs b0 b1 b2 b3 b4
+        = scLimbs a0 a1 a2 a3 a4 + 2^260 := by rw [hβo] at hTsub; simpa using hTsub
+    have hγ5 : γ5 = 1 := by
+      -- atoms: R,D,B,A := scLimbs …, Ell; facts below force γ5 = 1
+      have hRnn : 0 ≤ scLimbs a0 a1 a2 a3 a4 := Nat.zero_le _
+      omega
+    have hc := congrArg (Nat.cast (R := ZMod Ell)) hTadd
+    have hc2 := congrArg (Nat.cast (R := ZMod Ell)) hTsub
+    have hEz : (Ell : ZMod Ell) = 0 := ZMod.natCast_self Ell
+    simp only [scDenote, scVal_eq cw2 r0 r1 r2 r3 r4 hrl, hsva, hsvb, hβo, hγ5]
+    rw [hγ5] at hc
+    rw [hβo] at hc2
+    push_cast at hc hc2 ⊢
+    rw [hEz] at hc
+    linear_combination hc + hc2
 
 end ScalarProofs

verification/check-scalar.sh

@@ -19,7 +19,7 @@ lake env bash -c "
   cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
   for m in ${GEN[*]}; do echo \"  · gen \$m\"; LEAN_TIMEOUT=300 LEAN_MEM_MB=6144 '$HERE/lean-guard' \"\$m.lean\" || exit 1; done
   cd '$HERE'
-  for m in ${PROOFS[*]}; do echo \"  · proof \$m\"; LEAN_TIMEOUT=300 LEAN_MEM_MB=6144 '$HERE/lean-guard' \"Proofs/\$m.lean\" || exit 1; done
+  for m in ${PROOFS[*]}; do echo \"  · proof \$m\"; LEAN_TIMEOUT=600 LEAN_MEM_MB=8192 '$HERE/lean-guard' \"Proofs/\$m.lean\" || exit 1; done
 " || { echo FAIL; exit 1; }
 echo "=== Phase 3: axiom audit (kernel-level) ==="
 cd "$AENEAS_LEAN"
@@ -30,12 +30,12 @@ lake env bash -c "
   AUD=\$(mktemp '$HERE/.audit-scalar-XXXX.lean')
   { echo 'import Proofs.ScalarDenote'; echo 'import Proofs.ScalarSubSpec'; echo '#print axioms ScalarProofs.L_val'
     echo '#print axioms ScalarProofs.sub_loop_spec'
-    echo '#print axioms ScalarProofs.cond_add_l_one_spec'; } > \"\$AUD\"
+    echo '#print axioms ScalarProofs.cond_add_l_one_spec'; echo '#print axioms ScalarProofs.sub_val_spec'; } > \"\$AUD\"
   OUT=\$(LEAN_TIMEOUT=120 LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1)
   echo \"\$OUT\"
   rm -f \"\$AUD\" \"\${AUD%.lean}.olean\"
   N=\$(echo \"\$OUT\" | grep -cF \"depends on axioms: [propext, Classical.choice, Quot.sound]\" || true)
-  [ \"\$N\" -eq 3 ] || { echo \"AXIOM AUDIT FAILED: \$N/3 clean\"; exit 1; }
+  [ \"\$N\" -eq 4 ] || { echo \"AXIOM AUDIT FAILED: \$N/4 clean\"; exit 1; }
 " || { echo FAIL; exit 1; }
 echo "  L_val axiom-clean"