diff --git a/verification/Proofs/CompressSpec.lean b/verification/Proofs/CompressSpec.lean
new file mode 100644
index 0000000..e51e8cd
--- /dev/null
+++ b/verification/Proofs/CompressSpec.lean
@@ -0,0 +1,201 @@
+/- ──────────────────────────────────────────────────────────────────────────────
+   Proofs/CompressSpec.lean — phase 2, brick 1: `EdwardsPoint::compress` emits
+   the canonical wire encoding of the denoted affine point.
+
+   THE THEOREM (`ed_compress_spec`): for a valid extended point Pt,
+       compress Pt = ok s   with
+       bytesVal s = (edY Pt).val + ((edX Pt).val % 2) · 2²⁵⁵
+   — the 32 bytes are the canonical little-endian encoding of the affine
+   y-coordinate with the parity ("sign") bit of the affine x-coordinate in
+   bit 255. Combined with `verify_accepts_iff` (SigApexSpec), this pins the
+   byte comparison of the apex to an equation on DENOTED POINTS — the
+   half-lift toward the point-level verification equation.
+
+   CHAIN (all real extracted code, all previously certified):
+     to_affine  = invert Z, mul X, mul Y        (invert_spec, mul_spec')
+     compress   = to_bytes y                     (to_bytes_spec — canonicity)
+                  is_negative x                  (to_bytes again, bit 0)
+                  s[31] ^= sign << 7             (XOR on a clear bit = +2²⁵⁵)
+
+   The parity of the CANONICAL encoding is the standard "sign" convention:
+   is_negative reads bit 0 of to_bytes, i.e. (feVal x mod p) mod 2 =
+   (edX Pt).val mod 2.
+   ────────────────────────────────────────────────────────────────────────────── -/
+import Proofs.ToBytesSpec
+import Proofs.InvertSpec
+import Proofs.EdMain
+open Aeneas Aeneas.Std Result
+open curve25519_dalek
+
+set_option maxHeartbeats 4000000
+set_option linter.unusedSimpArgs false
+set_option maxRecDepth 8000
+
+namespace CurveFieldProofs
+
+open Aeneas.Std.WP
+
+/-- Premise-free restatement of `to_bytes_spec` (destructures internally). -/
+theorem to_bytes_spec' (a : Fe) :
+    fe_to_bytes a ⦃ s => bytesVal s = feVal a % P ⦄ := by
+  obtain ⟨l0, l1, l2, l3, l4, hl⟩ := Fe.exists_limbs a
+  exact to_bytes_spec a l0 l1 l2 l3 l4 hl
+
+/-- Destructuring device for 32-byte arrays (the `Fe.exists_limbs` idiom). -/
+theorem Bytes32.exists_bytes (s : Std.Array Std.U8 32#usize) :
+    ∃ b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15
+      b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 : Std.U8,
+      (↑s : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11,
+        b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25,
+        b26, b27, b28, b29, b30, b31] := by
+  have h : (↑s : List Std.U8).length = 32 := by
+    have := s.property
+    simp_all
+  match hl : (↑s : List Std.U8) with
+  | [c0, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15,
+     c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31] =>
+    exact ⟨c0, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15,
+      c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, rfl⟩
+  | [] | [_] | [_,_] | [_,_,_] | [_,_,_,_] | [_,_,_,_,_] | [_,_,_,_,_,_] | [_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] => simp [hl] at h
+  | _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_ => simp [hl] at h
+
+/-- **`is_negative` is the parity of the canonical residue** — bit 0 of the
+    canonical encoding (`Choice` is the transparent-u8 model). -/
+theorem is_negative_spec (a : Fe) :
+    field.FieldElement51.is_negative a ⦃ c => c.val = (feVal a % P) % 2 ⦄ := by
+  unfold field.FieldElement51.is_negative
+  step with (to_bytes_spec' a) as ⟨s, hs⟩
+  obtain ⟨b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15,
+    b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31,
+    hsl⟩ := Bytes32.exists_bytes s
+  step as ⟨i, hi⟩
+  simp [hsl] at hi
+  step as ⟨i1, hi1⟩
+  -- into Choice = the identity From instance
+  simp only [core.convert.IntoFrom.into, subtle.Choice.Insts.CoreConvertFromU8,
+    subtle.Choice.Insts.CoreConvertFromU8.from]
+  try simp only [spec_ok]
+  -- value: b0 &&& 1 = b0 % 2 = bytesVal s % 2 = (feVal a % P) % 2
+  have hi1v : i1.val = b0.val % 2 := by
+    rw [hi1, hi, UScalar.val_and]
+    have := Nat.and_two_pow_sub_one_eq_mod b0.val 1
+    norm_num at this
+    simpa using this
+  have hb0 : b0.val % 2 = bytesVal s % 2 := by
+    simp only [bytesVal, hsl]
+    omega
+  rw [hi1v, hb0, hs]
+
+/-- **`compress` on a valid extended point emits the canonical encoding**:
+    the affine y-residue with the x-parity bit at position 255. -/
+theorem ed_compress_spec (Pt : EdPoint) (hv : ExtValid Pt) :
+    edwards.EdwardsPoint.compress Pt ⦃ s =>
+      bytesVal s = (edY Pt).val + ((edX Pt).val % 2) * 2^255 ⦄ := by
+  obtain ⟨hbX, hbY, hbZ, hZne, hcoh⟩ := hv
+  unfold edwards.EdwardsPoint.compress
+  -- recip ← invert Z
+  step with (invert_spec Pt.Z (Bnd.mono hbZ (by norm_num))) as ⟨recip, hbr, hrv⟩
+  -- x ← X · recip, y ← Y · recip
+  step with (mul_spec' Pt.X recip (Bnd.mono hbX (by norm_num)) (Bnd.mono hbr (by norm_num)))
+    as ⟨x, hbx, hxv⟩
+  step with (mul_spec' Pt.Y recip (Bnd.mono hbY (by norm_num)) (Bnd.mono hbr (by norm_num)))
+    as ⟨y, hby, hyv⟩
+  -- (v4: the affine conversion is inlined in compress)
+  step with (to_bytes_spec' y) as ⟨s, hs⟩
+  obtain ⟨b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15,
+    b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31,
+    hsl⟩ := Bytes32.exists_bytes s
+  step with (is_negative_spec x) as ⟨c, hc⟩
+  -- unwrap_u8 is the transparent-u8 identity: reduce it away
+  simp only [subtle.Choice.unwrap_u8, bind_tc_ok]
+  have hsignv : c.val = (feVal x % P) % 2 := hc
+  -- sign << 7
+  step as ⟨hi7, hhi7⟩
+  have hsle : c.val ≤ 1 := by rw [hsignv]; omega
+  have hhi7v : hi7.val = c.val * 2^7 := by
+    rw [hhi7]
+    simp only [Nat.shiftLeft_eq]
+    rw [Nat.mod_eq_of_lt (show c.val * 2^7 < U8.size by scalar_tac)]
+  -- s[31]
+  step as ⟨t31, ht31⟩
+  simp [hsl] at ht31
+  -- xor
+  step as ⟨t31x, ht31x⟩
+  -- update
+  step as ⟨s1, hs1⟩
+  have hsl1 : (↑s1 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9,
+      b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23,
+      b24, b25, b26, b27, b28, b29, b30, t31x] := by
+    simp only [hs1, Array.set_val_eq, hsl]
+    rfl
+  try simp only [spec_ok]
+  -- ── value assembly ───────────────────────────────────────────────────────
+  -- the canonical y-residue is < p < 2²⁵⁵, so its top byte is < 2⁷
+  have hsval : bytesVal s = feVal y % P := hs
+  have hslt : bytesVal s < 2^255 := by
+    rw [hsval]
+    have : feVal y % P < P := Nat.mod_lt _ (by unfold P; norm_num)
+    unfold P at this ⊢
+    omega
+  have hb31top : b31.val < 2^7 := by
+    have hexp : bytesVal s = b0.val + b1.val * 2^8 + b2.val * 2^16 + b3.val * 2^24
+        + b4.val * 2^32 + b5.val * 2^40 + b6.val * 2^48 + b7.val * 2^56
+        + b8.val * 2^64 + b9.val * 2^72 + b10.val * 2^80 + b11.val * 2^88
+        + b12.val * 2^96 + b13.val * 2^104 + b14.val * 2^112 + b15.val * 2^120
+        + b16.val * 2^128 + b17.val * 2^136 + b18.val * 2^144 + b19.val * 2^152
+        + b20.val * 2^160 + b21.val * 2^168 + b22.val * 2^176 + b23.val * 2^184
+        + b24.val * 2^192 + b25.val * 2^200 + b26.val * 2^208 + b27.val * 2^216
+        + b28.val * 2^224 + b29.val * 2^232 + b30.val * 2^240 + b31.val * 2^248 := by
+      simp only [bytesVal, hsl]
+    omega
+  -- the xor adds sign·2⁷ to a clear bit
+  have ht31xv : t31x.val = b31.val + c.val * 2^7 := by
+    have hsb : c.val = 0 ∨ c.val = 1 := by
+      rw [hsignv]; omega
+    rw [ht31x, UScalar.val_xor, ht31, hhi7v]
+    rcases hsb with h | h
+    · simp [h]
+    · rw [h]
+      norm_num
+      exact xor_top_bit b31.val hb31top
+  -- reassemble: only byte 31 changed, and it grew by sign·2⁷ at weight 2²⁴⁸
+  have hexp : bytesVal s = b0.val + b1.val * 2^8 + b2.val * 2^16 + b3.val * 2^24
+      + b4.val * 2^32 + b5.val * 2^40 + b6.val * 2^48 + b7.val * 2^56
+      + b8.val * 2^64 + b9.val * 2^72 + b10.val * 2^80 + b11.val * 2^88
+      + b12.val * 2^96 + b13.val * 2^104 + b14.val * 2^112 + b15.val * 2^120
+      + b16.val * 2^128 + b17.val * 2^136 + b18.val * 2^144 + b19.val * 2^152
+      + b20.val * 2^160 + b21.val * 2^168 + b22.val * 2^176 + b23.val * 2^184
+      + b24.val * 2^192 + b25.val * 2^200 + b26.val * 2^208 + b27.val * 2^216
+      + b28.val * 2^224 + b29.val * 2^232 + b30.val * 2^240 + b31.val * 2^248 := by
+    simp only [bytesVal, hsl]
+  have hexp1 : bytesVal s1 = b0.val + b1.val * 2^8 + b2.val * 2^16 + b3.val * 2^24
+      + b4.val * 2^32 + b5.val * 2^40 + b6.val * 2^48 + b7.val * 2^56
+      + b8.val * 2^64 + b9.val * 2^72 + b10.val * 2^80 + b11.val * 2^88
+      + b12.val * 2^96 + b13.val * 2^104 + b14.val * 2^112 + b15.val * 2^120
+      + b16.val * 2^128 + b17.val * 2^136 + b18.val * 2^144 + b19.val * 2^152
+      + b20.val * 2^160 + b21.val * 2^168 + b22.val * 2^176 + b23.val * 2^184
+      + b24.val * 2^192 + b25.val * 2^200 + b26.val * 2^208 + b27.val * 2^216
+      + b28.val * 2^224 + b29.val * 2^232 + b30.val * 2^240 + t31x.val * 2^248 := by
+    simp only [bytesVal, hsl1]
+  have hstep : bytesVal s1 = bytesVal s + c.val * 2^255 := by
+    rw [hexp, hexp1, ht31xv]
+    ring
+  -- denotation bridges: the residues are the .val of the denoted coordinates
+  haveI : NeZero P := ⟨by unfold P; norm_num⟩
+  have hyval : feVal y % P = (edY Pt).val := by
+    have h1 : ⟪y⟫ = edY Pt := by
+      rw [hyv, hrv]
+      unfold edY
+      rw [div_eq_mul_inv]
+    rw [← h1]
+    simp [denote, ZMod.val_natCast]
+  have hxval : (feVal x % P) % 2 = (edX Pt).val % 2 := by
+    have h1 : ⟪x⟫ = edX Pt := by
+      rw [hxv, hrv]
+      unfold edX
+      rw [div_eq_mul_inv]
+    rw [← h1]
+    simp [denote, ZMod.val_natCast]
+  rw [hstep, hs, hsignv, hyval, hxval]
+
+end CurveFieldProofs
diff --git a/verification/Proofs/PointLiftSpec.lean b/verification/Proofs/PointLiftSpec.lean
new file mode 100644
index 0000000..760c5cb
--- /dev/null
+++ b/verification/Proofs/PointLiftSpec.lean
@@ -0,0 +1,321 @@
+/- ──────────────────────────────────────────────────────────────────────────────
+   Proofs/PointLiftSpec.lean — phase 2, the half-lift toward the point-level
+   verification equation.
+
+   This file assembles the connective tissue between the byte-level apex
+   (SigApexSpec: accept ⇔ byte equality) and the denoted-point world:
+
+   1. `vartime_dsm_basepoint_spec` — the public dsm entry is its serial
+      implementation (the backend dispatch is REAL code under the serial
+      pin: get_selected_backend = ok .Serial), so the dsm certificate
+      transfers to the function the verifier actually calls.
+   2. `bytesVal_inj` / `rangeEq_iff_bytesVal` — the byte-wise comparison the
+      verifier performs is exactly value equality of the two encodings
+      (little-endian digits are unique: peel one byte at a time).
+
+   The recompute-chain inversion and the half-lift theorem itself build on
+   these in the sequel (the sha calls are oracles — axioms cannot be walked,
+   so the chain is INVERTED from the `hrec` hypothesis the apex already
+   carries, exactly as the apex itself is hypothesis-parametric).
+   ────────────────────────────────────────────────────────────────────────────── -/
+import Proofs.CompressSpec
+import Proofs.ScalarPackSpec
+import Proofs.DsmMulSpec
+import Proofs.SigApexSpec
+open Aeneas Aeneas.Std Result
+open curve25519_dalek
+
+set_option maxHeartbeats 4000000
+set_option linter.unusedSimpArgs false
+set_option maxRecDepth 8000
+
+namespace CurveFieldProofs
+
+open Aeneas.Std.WP
+
+/-- **The public dsm entry satisfies the dsm certificate**: the backend
+    dispatch is the real constant Serial (no axiom), so
+    `vartime_double_scalar_mul_basepoint` IS the certified serial path. -/
+theorem vartime_dsm_basepoint_spec
+    (a b : scalar.Scalar) (A : EdPoint)
+    (a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 a17 a18 a19 a20 a21 a22 a23 a24 a25 a26 a27 a28 a29 a30 a31 : Std.U8)
+    (b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 : Std.U8)
+    (hab : (↑a.bytes : List Std.U8) = [a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31])
+    (hbb : (↑b.bytes : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31])
+    (Va Vb : ℕ)
+    (hVa : Va = a0.val + a1.val * 2^8 + a2.val * 2^16 + a3.val * 2^24 + a4.val * 2^32 + a5.val * 2^40 + a6.val * 2^48 + a7.val * 2^56 + a8.val * 2^64 + a9.val * 2^72 + a10.val * 2^80 + a11.val * 2^88 + a12.val * 2^96 + a13.val * 2^104 + a14.val * 2^112 + a15.val * 2^120 + a16.val * 2^128 + a17.val * 2^136 + a18.val * 2^144 + a19.val * 2^152 + a20.val * 2^160 + a21.val * 2^168 + a22.val * 2^176 + a23.val * 2^184 + a24.val * 2^192 + a25.val * 2^200 + a26.val * 2^208 + a27.val * 2^216 + a28.val * 2^224 + a29.val * 2^232 + a30.val * 2^240 + a31.val * 2^248)
+    (hVb : Vb = b0.val + b1.val * 2^8 + b2.val * 2^16 + b3.val * 2^24 + b4.val * 2^32 + b5.val * 2^40 + b6.val * 2^48 + b7.val * 2^56 + b8.val * 2^64 + b9.val * 2^72 + b10.val * 2^80 + b11.val * 2^88 + b12.val * 2^96 + b13.val * 2^104 + b14.val * 2^112 + b15.val * 2^120 + b16.val * 2^128 + b17.val * 2^136 + b18.val * 2^144 + b19.val * 2^152 + b20.val * 2^160 + b21.val * 2^168 + b22.val * 2^176 + b23.val * 2^184 + b24.val * 2^192 + b25.val * 2^200 + b26.val * 2^208 + b27.val * 2^216 + b28.val * 2^224 + b29.val * 2^232 + b30.val * 2^240 + b31.val * 2^248)
+    (hValt : Va < 2^253) (hVblt : Vb < 2^253)
+    (hAv : ExtValid A) (hAc : OnCurveExt A) :
+    edwards.EdwardsPoint.vartime_double_scalar_mul_basepoint a A b ⦃ R =>
+      ExtValid R ∧ OnCurveExt R ∧
+      ∃ (na nb : Std.Array Std.I8 256#usize),
+        NafDigits na ∧ NafDigits nb ∧
+        nafSum na 256 = (Va : ℤ) ∧ nafSum nb 256 = (Vb : ℤ) ∧
+        edPt R = dsmFold (nafDigit na) (nafDigit nb) (edPt A) edBasePt edId 256 ⦄ := by
+  unfold edwards.EdwardsPoint.vartime_double_scalar_mul_basepoint
+    backend.vartime_double_base_mul backend.get_selected_backend
+  simp only [bind_tc_ok]
+  exact vartime_double_base_mul_spec a b A
+    a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 a17 a18 a19 a20 a21 a22 a23 a24 a25 a26 a27 a28 a29 a30 a31
+    b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31
+    hab hbb Va Vb hVa hVb hValt hVblt hAv hAc
+
+/-- One digit-peeling step: equal little-endian values with byte-sized heads
+    force equal heads and equal tails. -/
+theorem byte_peel {b c X Y : ℕ} (hb : b < 2^8) (hc : c < 2^8)
+    (h : b + 2^8 * X = c + 2^8 * Y) : b = c ∧ X = Y := by
+  omega
+
+/-- **Little-endian digits are unique**: equal `bytesVal` forces equal byte
+    arrays, hence the verifier's byte-wise comparison IS value equality. -/
+theorem rangeEq_iff_bytesVal (e r : Std.Array Std.U8 32#usize) :
+    rangeEq e r 0 ↔ bytesVal e = bytesVal r := by
+  obtain ⟨e0, e1, e2, e3, e4, e5, e6, e7, e8, e9, e10, e11, e12, e13, e14, e15,
+    e16, e17, e18, e19, e20, e21, e22, e23, e24, e25, e26, e27, e28, e29, e30, e31,
+    hel⟩ := Bytes32.exists_bytes e
+  obtain ⟨r0, r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15,
+    r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31,
+    hrl⟩ := Bytes32.exists_bytes r
+  constructor
+  · -- pointwise equality ⇒ equal sums
+    intro h
+    have hpt : ∀ j, j < 32 → e.val[j]! = r.val[j]! := fun j hj => h j (Nat.zero_le _) hj
+    have h0 : e0 = r0 := by simpa [hel, hrl] using hpt 0 (by norm_num)
+    have h1 : e1 = r1 := by simpa [hel, hrl] using hpt 1 (by norm_num)
+    have h2 : e2 = r2 := by simpa [hel, hrl] using hpt 2 (by norm_num)
+    have h3 : e3 = r3 := by simpa [hel, hrl] using hpt 3 (by norm_num)
+    have h4 : e4 = r4 := by simpa [hel, hrl] using hpt 4 (by norm_num)
+    have h5 : e5 = r5 := by simpa [hel, hrl] using hpt 5 (by norm_num)
+    have h6 : e6 = r6 := by simpa [hel, hrl] using hpt 6 (by norm_num)
+    have h7 : e7 = r7 := by simpa [hel, hrl] using hpt 7 (by norm_num)
+    have h8 : e8 = r8 := by simpa [hel, hrl] using hpt 8 (by norm_num)
+    have h9 : e9 = r9 := by simpa [hel, hrl] using hpt 9 (by norm_num)
+    have h10 : e10 = r10 := by simpa [hel, hrl] using hpt 10 (by norm_num)
+    have h11 : e11 = r11 := by simpa [hel, hrl] using hpt 11 (by norm_num)
+    have h12 : e12 = r12 := by simpa [hel, hrl] using hpt 12 (by norm_num)
+    have h13 : e13 = r13 := by simpa [hel, hrl] using hpt 13 (by norm_num)
+    have h14 : e14 = r14 := by simpa [hel, hrl] using hpt 14 (by norm_num)
+    have h15 : e15 = r15 := by simpa [hel, hrl] using hpt 15 (by norm_num)
+    have h16 : e16 = r16 := by simpa [hel, hrl] using hpt 16 (by norm_num)
+    have h17 : e17 = r17 := by simpa [hel, hrl] using hpt 17 (by norm_num)
+    have h18 : e18 = r18 := by simpa [hel, hrl] using hpt 18 (by norm_num)
+    have h19 : e19 = r19 := by simpa [hel, hrl] using hpt 19 (by norm_num)
+    have h20 : e20 = r20 := by simpa [hel, hrl] using hpt 20 (by norm_num)
+    have h21 : e21 = r21 := by simpa [hel, hrl] using hpt 21 (by norm_num)
+    have h22 : e22 = r22 := by simpa [hel, hrl] using hpt 22 (by norm_num)
+    have h23 : e23 = r23 := by simpa [hel, hrl] using hpt 23 (by norm_num)
+    have h24 : e24 = r24 := by simpa [hel, hrl] using hpt 24 (by norm_num)
+    have h25 : e25 = r25 := by simpa [hel, hrl] using hpt 25 (by norm_num)
+    have h26 : e26 = r26 := by simpa [hel, hrl] using hpt 26 (by norm_num)
+    have h27 : e27 = r27 := by simpa [hel, hrl] using hpt 27 (by norm_num)
+    have h28 : e28 = r28 := by simpa [hel, hrl] using hpt 28 (by norm_num)
+    have h29 : e29 = r29 := by simpa [hel, hrl] using hpt 29 (by norm_num)
+    have h30 : e30 = r30 := by simpa [hel, hrl] using hpt 30 (by norm_num)
+    have h31 : e31 = r31 := by simpa [hel, hrl] using hpt 31 (by norm_num)
+    simp only [bytesVal, hel, hrl, h0, h1, h2, h3, h4, h5, h6, h7, h8, h9, h10, h11, h12, h13, h14, h15, h16, h17, h18, h19, h20, h21, h22, h23, h24, h25, h26, h27, h28, h29, h30, h31]
+  · -- equal sums ⇒ pointwise equality: peel 32 bytes
+    intro h
+    simp only [bytesVal, hel, hrl] at h
+    intro j hj0 hj32
+    simp only [hel, hrl]
+    -- normalize both sums into head + 2^8·tail form, peel, recurse
+    have hb : ∀ x : Std.U8, x.val < 2^8 := fun x => by scalar_tac
+    have hpeel : e0.val = r0.val ∧ e1.val = r1.val ∧ e2.val = r2.val ∧
+        e3.val = r3.val ∧ e4.val = r4.val ∧ e5.val = r5.val ∧
+        e6.val = r6.val ∧ e7.val = r7.val ∧ e8.val = r8.val ∧
+        e9.val = r9.val ∧ e10.val = r10.val ∧ e11.val = r11.val ∧
+        e12.val = r12.val ∧ e13.val = r13.val ∧ e14.val = r14.val ∧
+        e15.val = r15.val ∧ e16.val = r16.val ∧ e17.val = r17.val ∧
+        e18.val = r18.val ∧ e19.val = r19.val ∧ e20.val = r20.val ∧
+        e21.val = r21.val ∧ e22.val = r22.val ∧ e23.val = r23.val ∧
+        e24.val = r24.val ∧ e25.val = r25.val ∧ e26.val = r26.val ∧
+        e27.val = r27.val ∧ e28.val = r28.val ∧ e29.val = r29.val ∧
+        e30.val = r30.val ∧ e31.val = r31.val := by
+      have hbe0 := hb e0; have hbr0 := hb r0
+      have hbe1 := hb e1; have hbr1 := hb r1
+      have hbe2 := hb e2; have hbr2 := hb r2
+      have hbe3 := hb e3; have hbr3 := hb r3
+      have hbe4 := hb e4; have hbr4 := hb r4
+      have hbe5 := hb e5; have hbr5 := hb r5
+      have hbe6 := hb e6; have hbr6 := hb r6
+      have hbe7 := hb e7; have hbr7 := hb r7
+      have hbe8 := hb e8; have hbr8 := hb r8
+      have hbe9 := hb e9; have hbr9 := hb r9
+      have hbe10 := hb e10; have hbr10 := hb r10
+      have hbe11 := hb e11; have hbr11 := hb r11
+      have hbe12 := hb e12; have hbr12 := hb r12
+      have hbe13 := hb e13; have hbr13 := hb r13
+      have hbe14 := hb e14; have hbr14 := hb r14
+      have hbe15 := hb e15; have hbr15 := hb r15
+      have hbe16 := hb e16; have hbr16 := hb r16
+      have hbe17 := hb e17; have hbr17 := hb r17
+      have hbe18 := hb e18; have hbr18 := hb r18
+      have hbe19 := hb e19; have hbr19 := hb r19
+      have hbe20 := hb e20; have hbr20 := hb r20
+      have hbe21 := hb e21; have hbr21 := hb r21
+      have hbe22 := hb e22; have hbr22 := hb r22
+      have hbe23 := hb e23; have hbr23 := hb r23
+      have hbe24 := hb e24; have hbr24 := hb r24
+      have hbe25 := hb e25; have hbr25 := hb r25
+      have hbe26 := hb e26; have hbr26 := hb r26
+      have hbe27 := hb e27; have hbr27 := hb r27
+      have hbe28 := hb e28; have hbr28 := hb r28
+      have hbe29 := hb e29; have hbr29 := hb r29
+      have hbe30 := hb e30; have hbr30 := hb r30
+      have hbe31 := hb e31; have hbr31 := hb r31
+      omega
+    obtain ⟨q0, q1, q2, q3, q4, q5, q6, q7, q8, q9, q10, q11, q12, q13, q14,
+      q15, q16, q17, q18, q19, q20, q21, q22, q23, q24, q25, q26, q27, q28,
+      q29, q30, q31⟩ := hpeel
+    -- j is one of 0..31: close each case with the matching byte equality
+    interval_cases j <;> simp_all <;> exact UScalar.eq_of_val_eq (by assumption)
+
+/-- List-level 32-destructure (helper for the 64-byte device). -/
+theorem List.exists_len32 (l : List Std.U8) (h : l.length = 32) :
+    ∃ (d0 d1 d2 d3 d4 d5 d6 d7 d8 d9 d10 d11 d12 d13 d14 d15 d16 d17 d18 d19 d20 d21 d22 d23 d24 d25 d26 d27 d28 d29 d30 d31 : Std.U8), l = [d0, d1, d2, d3, d4, d5, d6, d7, d8, d9, d10, d11, d12, d13, d14, d15, d16, d17, d18, d19, d20, d21, d22, d23, d24, d25, d26, d27, d28, d29, d30, d31] := by
+  match hl : l with
+  | [d0, d1, d2, d3, d4, d5, d6, d7, d8, d9, d10, d11, d12, d13, d14, d15, d16, d17, d18, d19, d20, d21, d22, d23, d24, d25, d26, d27, d28, d29, d30, d31] => exact ⟨d0, d1, d2, d3, d4, d5, d6, d7, d8, d9, d10, d11, d12, d13, d14, d15, d16, d17, d18, d19, d20, d21, d22, d23, d24, d25, d26, d27, d28, d29, d30, d31, rfl⟩
+  | [] | [_] | [_,_] | [_,_,_] | [_,_,_,_] | [_,_,_,_,_] | [_,_,_,_,_,_] | [_,_,_,_,_,_,_] => simp [hl] at h
+  | [_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] => simp [hl] at h
+  | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] => simp [hl] at h
+  | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] => simp [hl] at h
+  | _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_ => simp [hl] at h
+
+/-- Destructuring device for 64-byte arrays (hash outputs): 32-cons prefix,
+    then the list-level device on the tail. -/
+theorem Bytes64.exists_bytes (s : Std.Array Std.U8 64#usize) :
+    ∃ (c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12 c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 c25 c26 c27 c28 c29 c30 c31 c32 c33 c34 c35 c36 c37 c38 c39 c40 c41 c42 c43 c44 c45 c46 c47 c48 c49 c50 c51 c52 c53 c54 c55 c56 c57 c58 c59 c60 c61 c62 c63 : Std.U8),
+      (↑s : List Std.U8) = [c0, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63] := by
+  have h : (↑s : List Std.U8).length = 64 := by
+    have := s.property
+    simp_all
+  match hl : (↑s : List Std.U8) with
+  | c0 :: c1 :: c2 :: c3 :: c4 :: c5 :: c6 :: c7 :: c8 :: c9 :: c10 :: c11 :: c12 :: c13 :: c14 :: c15 :: c16 :: c17 :: c18 :: c19 :: c20 :: c21 :: c22 :: c23 :: c24 :: c25 :: c26 :: c27 :: c28 :: c29 :: c30 :: c31 :: rest =>
+    have h2 : rest.length = 32 := by
+      rw [hl] at h
+      simp at h
+      omega
+    obtain ⟨c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, hr⟩ := List.exists_len32 rest h2
+    exact ⟨c0, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, by rw [hr]⟩
+  | [] | [_] | [_,_] | [_,_,_] | [_,_,_,_] | [_,_,_,_,_] | [_,_,_,_,_,_] | [_,_,_,_,_,_,_] => simp [hl] at h
+  | [_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] => simp [hl] at h
+  | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] => simp [hl] at h
+  | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] => simp [hl] at h
+
+/-- Generic ok-inversion of one monadic bind: a successful chain names the
+    intermediate and its defining equation. -/
+theorem bind_ok_inv {α β : Type} {e : Result α} {f : α → Result β} {b : β}
+    (h : (do let x ← e; f x) = ok b) : ∃ a, e = ok a ∧ f a = ok b := by
+  cases he : e with
+  | ok v =>
+    refine ⟨v, rfl, ?_⟩
+    rw [he] at h
+    simpa using h
+  | fail err =>
+    rw [he] at h
+    simp [Bind.bind, Aeneas.Std.bind] at h
+  | div =>
+    rw [he] at h
+    simp [Bind.bind, Aeneas.Std.bind] at h
+
+open ed25519_dalek in
+/-- **Inversion of the recompute chain**: a successful recompute names its
+    intermediates — the hash output, the reduced scalar k, the negated key
+    point, and the dsm result — each with its defining equation. (The SHA
+    calls are oracles: axioms cannot be walked, so the chain is inverted
+    from the hypothesis, mirroring the apex's hypothesis-parametric form.) -/
+theorem recompute_inv (key : verifying.VerifyingKey)
+    (sig : signature.InternalSignature) (msg : Slice Std.U8)
+    (er : curve25519_dalek.edwards.CompressedEdwardsY)
+    (hrec : verifying.recompute_r_sha512 key sig msg = ok er) :
+    ∃ (hash : Std.Array Std.U8 64#usize) (k : scalar.Scalar)
+      (mA ep : EdPoint),
+      scalar.Scalar.from_bytes_mod_order_wide hash = ok k ∧
+      edwards.EdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg key.point = ok mA ∧
+      edwards.EdwardsPoint.vartime_double_scalar_mul_basepoint k mA sig.s = ok ep ∧
+      edwards.EdwardsPoint.compress ep = ok er := by
+  unfold verifying.recompute_r_sha512 at hrec
+  simp only [curve25519_dalek.edwards.CompressedEdwardsY.as_bytes, lift,
+    bind_tc_ok] at hrec
+  obtain ⟨hash, _, hrec⟩ := bind_ok_inv hrec
+  obtain ⟨k, hk, hrec⟩ := bind_ok_inv hrec
+  obtain ⟨mA, hmA, hrec⟩ := bind_ok_inv hrec
+  obtain ⟨ep, hep, hrec⟩ := bind_ok_inv hrec
+  exact ⟨hash, k, mA, ep, hk, hmA, hep, hrec⟩
+
+open ed25519_dalek in
+/-- **THE HALF-LIFT: the verifier accepts iff the signature's R bytes are
+    the canonical encoding of the recomputed point.** For a parsing
+    signature (`hparse`), a valid on-curve public-key point, a canonical
+    signature scalar, and a successful recompute (`hrec` — the SHA calls
+    are oracles, hence hypothesis-parametric like the apex itself), there
+    is a point R' — [k](−A) + [s]B over the certified model — with
+        accept  ⇔  bytesVal R_bytes = (edY R').val + ((edX R').val % 2)·2²⁵⁵.
+    The byte-for-byte comparison of the apex IS point-encoding equality. -/
+theorem verify_accepts_iff_point
+    (key : verifying.VerifyingKey) (msg : Slice Std.U8) (sig : ed25519.Signature)
+    (val : signature.InternalSignature)
+    (er : curve25519_dalek.edwards.CompressedEdwardsY)
+    (e r1 : Std.Array Std.U8 32#usize)
+    (hparse : signature.InternalSignature.Insts.CoreConvertTryFromShared0SignatureError.try_from sig
+        = ok (core.result.Result.Ok val))
+    (hrec : verifying.recompute_r_sha512 key val msg = ok er)
+    (he : curve25519_dalek.edwards.CompressedEdwardsY.as_bytes er = ok e)
+    (hr1 : curve25519_dalek.edwards.CompressedEdwardsY.as_bytes val.R = ok r1)
+    (hkv : ExtValid key.point) (hkc : OnCurveExt key.point)
+    (t0 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 t16 t17 t18 t19 t20 t21 t22 t23 t24 t25 t26 t27 t28 t29 t30 t31 : Std.U8)
+    (hsb : (↑val.s.bytes : List Std.U8) = [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31])
+    (Vs : ℕ) (hVs : Vs = t0.val + t1.val * 2^8 + t2.val * 2^16 + t3.val * 2^24 + t4.val * 2^32 + t5.val * 2^40 + t6.val * 2^48 + t7.val * 2^56 + t8.val * 2^64 + t9.val * 2^72 + t10.val * 2^80 + t11.val * 2^88 + t12.val * 2^96 + t13.val * 2^104 + t14.val * 2^112 + t15.val * 2^120 + t16.val * 2^128 + t17.val * 2^136 + t18.val * 2^144 + t19.val * 2^152 + t20.val * 2^160 + t21.val * 2^168 + t22.val * 2^176 + t23.val * 2^184 + t24.val * 2^192 + t25.val * 2^200 + t26.val * 2^208 + t27.val * 2^216 + t28.val * 2^224 + t29.val * 2^232 + t30.val * 2^240 + t31.val * 2^248)
+    (hVslt : Vs < 2^253) :
+    ∃ (R' : EdPoint), ExtValid R' ∧ OnCurveExt R' ∧
+      (verifying.verify_sha512 key msg sig = ok (core.result.Result.Ok ())
+        ↔ bytesVal r1 = (edY R').val + ((edX R').val % 2) * 2^255) := by
+  obtain ⟨hash, k, mA, ep, hk, hmA, hep, hcomp⟩ := recompute_inv key val msg er hrec
+  -- k is canonical (< ℓ < 2²⁵³)
+  obtain ⟨c0, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, hhl⟩ := Bytes64.exists_bytes hash
+  obtain ⟨k', hk', hkpost⟩ := spec_imp_exists
+    (ScalarProofs.from_bytes_mod_order_wide_spec hash c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12 c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 c25 c26 c27 c28 c29 c30 c31 c32 c33 c34 c35 c36 c37 c38 c39 c40 c41 c42 c43 c44 c45 c46 c47 c48 c49 c50 c51 c52 c53 c54 c55 c56 c57 c58 c59 c60 c61 c62 c63 hhl _ rfl)
+  rw [hk] at hk'
+  have hkk : k = k' := by simpa using hk'
+  subst hkk
+  obtain ⟨hklt, -⟩ := hkpost
+  obtain ⟨a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, hkbl⟩ := Bytes32.exists_bytes k.bytes
+  have hkval : bytesVal k.bytes = a0.val + a1.val * 2^8 + a2.val * 2^16 + a3.val * 2^24 + a4.val * 2^32 + a5.val * 2^40 + a6.val * 2^48 + a7.val * 2^56 + a8.val * 2^64 + a9.val * 2^72 + a10.val * 2^80 + a11.val * 2^88 + a12.val * 2^96 + a13.val * 2^104 + a14.val * 2^112 + a15.val * 2^120 + a16.val * 2^128 + a17.val * 2^136 + a18.val * 2^144 + a19.val * 2^152 + a20.val * 2^160 + a21.val * 2^168 + a22.val * 2^176 + a23.val * 2^184 + a24.val * 2^192 + a25.val * 2^200 + a26.val * 2^208 + a27.val * 2^216 + a28.val * 2^224 + a29.val * 2^232 + a30.val * 2^240 + a31.val * 2^248 := by
+    simp only [bytesVal, hkbl]
+  have hValt : (a0.val + a1.val * 2^8 + a2.val * 2^16 + a3.val * 2^24 + a4.val * 2^32 + a5.val * 2^40 + a6.val * 2^48 + a7.val * 2^56 + a8.val * 2^64 + a9.val * 2^72 + a10.val * 2^80 + a11.val * 2^88 + a12.val * 2^96 + a13.val * 2^104 + a14.val * 2^112 + a15.val * 2^120 + a16.val * 2^128 + a17.val * 2^136 + a18.val * 2^144 + a19.val * 2^152 + a20.val * 2^160 + a21.val * 2^168 + a22.val * 2^176 + a23.val * 2^184 + a24.val * 2^192 + a25.val * 2^200 + a26.val * 2^208 + a27.val * 2^216 + a28.val * 2^224 + a29.val * 2^232 + a30.val * 2^240 + a31.val * 2^248) < 2^253 := by
+    have hEll : ScalarProofs.Ell < 2^253 := by unfold ScalarProofs.Ell; norm_num
+    omega
+  -- mA = −A, valid and on-curve
+  unfold edwards.EdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg at hmA
+  obtain ⟨mA', hmA', hmApost⟩ := spec_imp_exists (edwards_neg_law key.point hkv hkc)
+  rw [hmA'] at hmA
+  have hmm : mA = mA' := by simpa using hmA.symm
+  subst hmm
+  obtain ⟨hmAv, hmAc, -⟩ := hmApost
+  -- ep = [k](−A) + [s]B, valid and on-curve
+  obtain ⟨ep', hep', heppost⟩ := spec_imp_exists
+    (vartime_dsm_basepoint_spec k val.s mA
+      a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 a17 a18 a19 a20 a21 a22 a23 a24 a25 a26 a27 a28 a29 a30 a31 t0 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 t16 t17 t18 t19 t20 t21 t22 t23 t24 t25 t26 t27 t28 t29 t30 t31
+      hkbl hsb _ Vs rfl hVs hValt hVslt hmAv hmAc)
+  rw [hep'] at hep
+  have hee' : ep = ep' := by simpa using hep.symm
+  subst hee'
+  obtain ⟨hepv, hepc, -⟩ := heppost
+  -- er is the canonical encoding of ep
+  obtain ⟨er2, hcomp', hcpost⟩ := spec_imp_exists (ed_compress_spec ep hepv)
+  rw [hcomp'] at hcomp
+  have her : er = er2 := by simpa using hcomp.symm
+  subst her
+  -- e IS er (as_bytes is the identity)
+  have hee : er = e := by
+    have : curve25519_dalek.edwards.CompressedEdwardsY.as_bytes er = ok er := by
+      simp [curve25519_dalek.edwards.CompressedEdwardsY.as_bytes]
+    rw [this] at he
+    simpa using he
+  refine ⟨ep, hepv, hepc, ?_⟩
+  rw [verify_accepts_iff key msg sig val er e r1 hparse hrec he hr1,
+      rangeEq_iff_bytesVal, ← hee, hcpost]
+  exact eq_comm
+
+end CurveFieldProofs
diff --git a/verification/Proofs/ScalarPackSpec.lean b/verification/Proofs/ScalarPackSpec.lean
new file mode 100644
index 0000000..ee1e175
--- /dev/null
+++ b/verification/Proofs/ScalarPackSpec.lean
@@ -0,0 +1,599 @@
+/- ──────────────────────────────────────────────────────────────────────────────
+   Proofs/ScalarPackSpec.lean — phase 2, half-lift prerequisite: the scalar
+   PACK step (`Scalar52::to_bytes` / `Scalar52::pack`) and the composed
+   `Scalar::from_bytes_mod_order_wide` — the hash-to-scalar entry the
+   verifier's recompute path calls.
+
+   `Scalar52::to_bytes` is pure bit-packing (radix 2⁵² → little-endian bytes,
+   NO reduction — its callers guarantee canonical limbs): 30 shift-extracts
+   plus 2 limb-boundary bytes (6, 19 — the only offsets where 52j is not
+   byte-aligned). `scalar_pack` (the ℕ identity) mirrors ToBytesMath's
+   bytes_pack at the 52-bit offsets; the boundary ORs become additions via
+   the same disjointness idiom.
+
+   THE COMPOSED SPEC (`from_bytes_mod_order_wide_spec`): for a 64-byte input
+   with value T, the returned Scalar's 32 bytes have value V with
+       V < ℓ   and   (V : ZMod ℓ) = T
+   — i.e. the verifier's k = SHA-512 output reduced mod ℓ, in EXACTLY the
+   byte-value form the dsm certificate (`vartime_double_base_mul_spec`)
+   takes as its scalar premises (V < ℓ < 2²⁵³).
+   ────────────────────────────────────────────────────────────────────────────── -/
+import Proofs.ToBytesSpec
+import Proofs.ScalarFromBytesSpec
+open Aeneas Aeneas.Std Result
+open curve25519_dalek
+
+set_option maxHeartbeats 8000000
+set_option linter.unusedSimpArgs false
+set_option maxRecDepth 8000
+
+namespace ScalarProofs
+
+open Aeneas.Std.WP
+open CurveFieldProofs (bytesVal nat_shr byte_split_0 xor_top_bit)
+
+/-- Offset-4 byte split for 52-bit limbs (the pack's odd-offset limbs 1, 3):
+    low 4 bits close the boundary byte, six whole bytes follow. -/
+theorem byte_split_52_4 (f : ℕ) :
+    f % 2^4 + (f / 2^4 % 2^8) * 2^4 + (f / 2^12 % 2^8) * 2^12
+      + (f / 2^20 % 2^8) * 2^20 + (f / 2^28 % 2^8) * 2^28
+      + (f / 2^36 % 2^8) * 2^36 + (f / 2^44) * 2^44 = f := by
+  have e1 : f / 2^4 / 2^8 = f / 2^12 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e2 : f / 2^12 / 2^8 = f / 2^20 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e3 : f / 2^20 / 2^8 = f / 2^28 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e4 : f / 2^28 / 2^8 = f / 2^36 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e5 : f / 2^36 / 2^8 = f / 2^44 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have d0 := Nat.div_add_mod f (2^4)
+  have d1 := Nat.div_add_mod (f / 2^4) (2^8)
+  have d2 := Nat.div_add_mod (f / 2^12) (2^8)
+  have d3 := Nat.div_add_mod (f / 2^20) (2^8)
+  have d4 := Nat.div_add_mod (f / 2^28) (2^8)
+  have d5 := Nat.div_add_mod (f / 2^36) (2^8)
+  omega
+
+/-- THE 52-BIT PACKING IDENTITY: the 32 bytes `Scalar52::to_bytes` emits
+    assemble to the limb value (boundary bytes 6 and 19 in additive form). -/
+theorem scalar_pack (l0 l1 l2 l3 l4 : ℕ)
+    (h0 : l0 < 2^52) (h1 : l1 < 2^52) (h2 : l2 < 2^52)
+    (h3 : l3 < 2^52) (h4 : l4 < 2^48) :
+    (l0 % 2^8)
+      + (l0 / 2^8 % 2^8) * 2^8
+      + (l0 / 2^16 % 2^8) * 2^16
+      + (l0 / 2^24 % 2^8) * 2^24
+      + (l0 / 2^32 % 2^8) * 2^32
+      + (l0 / 2^40 % 2^8) * 2^40
+      + (l0 / 2^48 + (l1 % 2^4) * 2^4) * 2^48
+      + (l1 / 2^4 % 2^8) * 2^56
+      + (l1 / 2^12 % 2^8) * 2^64
+      + (l1 / 2^20 % 2^8) * 2^72
+      + (l1 / 2^28 % 2^8) * 2^80
+      + (l1 / 2^36 % 2^8) * 2^88
+      + (l1 / 2^44 % 2^8) * 2^96
+      + (l2 % 2^8) * 2^104
+      + (l2 / 2^8 % 2^8) * 2^112
+      + (l2 / 2^16 % 2^8) * 2^120
+      + (l2 / 2^24 % 2^8) * 2^128
+      + (l2 / 2^32 % 2^8) * 2^136
+      + (l2 / 2^40 % 2^8) * 2^144
+      + (l2 / 2^48 + (l3 % 2^4) * 2^4) * 2^152
+      + (l3 / 2^4 % 2^8) * 2^160
+      + (l3 / 2^12 % 2^8) * 2^168
+      + (l3 / 2^20 % 2^8) * 2^176
+      + (l3 / 2^28 % 2^8) * 2^184
+      + (l3 / 2^36 % 2^8) * 2^192
+      + (l3 / 2^44 % 2^8) * 2^200
+      + (l4 % 2^8) * 2^208
+      + (l4 / 2^8 % 2^8) * 2^216
+      + (l4 / 2^16 % 2^8) * 2^224
+      + (l4 / 2^24 % 2^8) * 2^232
+      + (l4 / 2^32 % 2^8) * 2^240
+      + (l4 / 2^40) * 2^248
+      = l0 + l1 * 2^52 + l2 * 2^104 + l3 * 2^156 + l4 * 2^208 := by
+  have s0 := byte_split_0 l0
+  have s1 := byte_split_52_4 l1
+  have s2 := byte_split_0 l2
+  have s3 := byte_split_52_4 l3
+  -- limb 4 has only 6 bytes: split_0's seventh chunk vanishes (l4 < 2^48)
+  have s4 := byte_split_0 l4
+  have h4z : l4 / 2^48 = 0 := Nat.div_eq_of_lt h4
+  -- l1/2^44, l3/2^44, l4/2^40 all fit a byte: the mods are the identity
+  have h1m : l1 / 2^44 % 2^8 = l1 / 2^44 :=
+    Nat.mod_eq_of_lt (Nat.div_lt_of_lt_mul (show l1 < 2^44 * 2^8 by omega))
+  have h3m : l3 / 2^44 % 2^8 = l3 / 2^44 :=
+    Nat.mod_eq_of_lt (Nat.div_lt_of_lt_mul (show l3 < 2^44 * 2^8 by omega))
+  have h4m : l4 / 2^40 % 2^8 = l4 / 2^40 :=
+    Nat.mod_eq_of_lt (Nat.div_lt_of_lt_mul (show l4 < 2^40 * 2^8 by omega))
+  rw [h1m, h3m]
+  rw [h4m, h4z] at s4
+  zify at s0 s1 s2 s3 s4 ⊢
+  linear_combination s0 + 2^52 * s1 + 2^104 * s2 + 2^156 * s3 + 2^208 * s4
+
+/-- **`Scalar52::to_bytes` is the canonical serializer of canonical limbs**:
+    for limbs below 2⁵² with value below 2²⁵³ (every reduced scalar), the 32
+    output bytes denote exactly the limb value. -/
+theorem scalar52_to_bytes_spec (a : Sc) (l0 l1 l2 l3 l4 : U64)
+    (hl : (↑a : List U64) = [l0, l1, l2, l3, l4])
+    (hb0 : l0.val < 2^52) (hb1 : l1.val < 2^52) (hb2 : l2.val < 2^52)
+    (hb3 : l3.val < 2^52) (hb4 : l4.val < 2^48) :
+    backend.serial.u64.scalar.Scalar52.as_bytes a
+      ⦃ s => bytesVal s = scVal a ⦄ := by
+  unfold backend.serial.u64.scalar.Scalar52.as_bytes
+  -- limb 0 read
+  step as ⟨v0, hv0⟩
+  simp [hl] at hv0
+  -- byte 0 (limb 0 >> 0)
+  step as ⟨x0, hx0⟩
+  rw [hv0] at hx0
+  step as ⟨b0, hb0⟩
+  have hb0v : b0.val = l0.val % 2^8 := by
+    rw [hb0, UScalar.cast_val_eq, hx0, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s1, hs1⟩
+  have hsl0 : (↑s1 : List Std.U8) = [b0, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs1, Array.set_val_eq, Array.repeat_val]
+    rfl
+  clear hx0 hb0 hs1
+  -- byte 1 (limb 0 >> 8)
+  step as ⟨x1, hx1⟩
+  rw [hv0] at hx1
+  step as ⟨b1, hb1⟩
+  have hb1v : b1.val = l0.val / 2^8 % 2^8 := by
+    rw [hb1, UScalar.cast_val_eq, hx1, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s2, hs2⟩
+  have hsl1 : (↑s2 : List Std.U8) = [b0, b1, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs2, Array.set_val_eq, hsl0]
+    rfl
+  clear hx1 hb1 hs2 hsl0
+  -- byte 2 (limb 0 >> 16)
+  step as ⟨x2, hx2⟩
+  rw [hv0] at hx2
+  step as ⟨b2, hb2⟩
+  have hb2v : b2.val = l0.val / 2^16 % 2^8 := by
+    rw [hb2, UScalar.cast_val_eq, hx2, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s3, hs3⟩
+  have hsl2 : (↑s3 : List Std.U8) = [b0, b1, b2, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs3, Array.set_val_eq, hsl1]
+    rfl
+  clear hx2 hb2 hs3 hsl1
+  -- byte 3 (limb 0 >> 24)
+  step as ⟨x3, hx3⟩
+  rw [hv0] at hx3
+  step as ⟨b3, hb3⟩
+  have hb3v : b3.val = l0.val / 2^24 % 2^8 := by
+    rw [hb3, UScalar.cast_val_eq, hx3, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s4, hs4⟩
+  have hsl3 : (↑s4 : List Std.U8) = [b0, b1, b2, b3, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs4, Array.set_val_eq, hsl2]
+    rfl
+  clear hx3 hb3 hs4 hsl2
+  -- byte 4 (limb 0 >> 32)
+  step as ⟨x4, hx4⟩
+  rw [hv0] at hx4
+  step as ⟨b4, hb4⟩
+  have hb4v : b4.val = l0.val / 2^32 % 2^8 := by
+    rw [hb4, UScalar.cast_val_eq, hx4, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s5, hs5⟩
+  have hsl4 : (↑s5 : List Std.U8) = [b0, b1, b2, b3, b4, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs5, Array.set_val_eq, hsl3]
+    rfl
+  clear hx4 hb4 hs5 hsl3
+  -- byte 5 (limb 0 >> 40)
+  step as ⟨x5, hx5⟩
+  rw [hv0] at hx5
+  step as ⟨b5, hb5⟩
+  have hb5v : b5.val = l0.val / 2^40 % 2^8 := by
+    rw [hb5, UScalar.cast_val_eq, hx5, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s6, hs6⟩
+  have hsl5 : (↑s6 : List Std.U8) = [b0, b1, b2, b3, b4, b5, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs6, Array.set_val_eq, hsl4]
+    rfl
+  clear hx5 hb5 hs6 hsl4
+  -- byte 6 (boundary: limb 0 >> 48 | limb 1 << 4)
+  step as ⟨x6, hx6⟩
+  rw [hv0] at hx6
+  step as ⟨v1, hv1⟩
+  simp [hl] at hv1
+  step as ⟨y6, hy6⟩
+  rw [hv1] at hy6
+  have hy6v : y6.val = l1.val * 2^4 := by
+    rw [hy6]
+    simp only [Nat.shiftLeft_eq]
+    rw [Nat.mod_eq_of_lt (show l1.val * 2^4 < U64.size by scalar_tac)]
+  step as ⟨z6, hz6⟩
+  step as ⟨b6, hb6⟩
+  have hb6v : b6.val = l0.val / 2^48 + (l1.val % 2^4) * 2^4 := by
+    rw [hb6, UScalar.cast_val_eq]
+    norm_num [UScalarTy.numBits]
+    rw [hz6, UScalar.val_or, hx6, nat_shr, hy6v]
+    have hxlt : l0.val / 2^48 < 2^4 := by omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := l0.val / 2^48) (i := 4) hxlt (l1.val)
+    have hadd : l0.val / 2^48 ||| l1.val * 2^4 = l0.val / 2^48 + l1.val * 2^4 := by
+      calc l0.val / 2^48 ||| l1.val * 2^4
+          = l0.val / 2^48 ||| 2^4 * l1.val := by rw [Nat.mul_comm]
+        _ = 2^4 * l1.val ||| l0.val / 2^48 := Nat.lor_comm _ _
+        _ = 2^4 * l1.val + l0.val / 2^48 := hor.symm
+        _ = l0.val / 2^48 + l1.val * 2^4 := by ring
+    rw [hadd]
+    omega
+  step as ⟨s7, hs7⟩
+  have hsl6 : (↑s7 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs7, Array.set_val_eq, hsl5]
+    rfl
+  clear hx6 hy6 hy6v hz6 hb6 hs7 hsl5
+  -- byte 7 (limb 1 >> 4)
+  step as ⟨x7, hx7⟩
+  rw [hv1] at hx7
+  step as ⟨b7, hb7⟩
+  have hb7v : b7.val = l1.val / 2^4 % 2^8 := by
+    rw [hb7, UScalar.cast_val_eq, hx7, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s8, hs8⟩
+  have hsl7 : (↑s8 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs8, Array.set_val_eq, hsl6]
+    rfl
+  clear hx7 hb7 hs8 hsl6
+  -- byte 8 (limb 1 >> 12)
+  step as ⟨x8, hx8⟩
+  rw [hv1] at hx8
+  step as ⟨b8, hb8⟩
+  have hb8v : b8.val = l1.val / 2^12 % 2^8 := by
+    rw [hb8, UScalar.cast_val_eq, hx8, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s9, hs9⟩
+  have hsl8 : (↑s9 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs9, Array.set_val_eq, hsl7]
+    rfl
+  clear hx8 hb8 hs9 hsl7
+  -- byte 9 (limb 1 >> 20)
+  step as ⟨x9, hx9⟩
+  rw [hv1] at hx9
+  step as ⟨b9, hb9⟩
+  have hb9v : b9.val = l1.val / 2^20 % 2^8 := by
+    rw [hb9, UScalar.cast_val_eq, hx9, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s10, hs10⟩
+  have hsl9 : (↑s10 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs10, Array.set_val_eq, hsl8]
+    rfl
+  clear hx9 hb9 hs10 hsl8
+  -- byte 10 (limb 1 >> 28)
+  step as ⟨x10, hx10⟩
+  rw [hv1] at hx10
+  step as ⟨b10, hb10⟩
+  have hb10v : b10.val = l1.val / 2^28 % 2^8 := by
+    rw [hb10, UScalar.cast_val_eq, hx10, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s11, hs11⟩
+  have hsl10 : (↑s11 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs11, Array.set_val_eq, hsl9]
+    rfl
+  clear hx10 hb10 hs11 hsl9
+  -- byte 11 (limb 1 >> 36)
+  step as ⟨x11, hx11⟩
+  rw [hv1] at hx11
+  step as ⟨b11, hb11⟩
+  have hb11v : b11.val = l1.val / 2^36 % 2^8 := by
+    rw [hb11, UScalar.cast_val_eq, hx11, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s12, hs12⟩
+  have hsl11 : (↑s12 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs12, Array.set_val_eq, hsl10]
+    rfl
+  clear hx11 hb11 hs12 hsl10
+  -- byte 12 (limb 1 >> 44)
+  step as ⟨x12, hx12⟩
+  rw [hv1] at hx12
+  step as ⟨b12, hb12⟩
+  have hb12v : b12.val = l1.val / 2^44 % 2^8 := by
+    rw [hb12, UScalar.cast_val_eq, hx12, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s13, hs13⟩
+  have hsl12 : (↑s13 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs13, Array.set_val_eq, hsl11]
+    rfl
+  clear hx12 hb12 hs13 hsl11
+  -- limb 2 read
+  step as ⟨v2, hv2⟩
+  simp [hl] at hv2
+  -- byte 13 (limb 2 >> 0)
+  step as ⟨x13, hx13⟩
+  rw [hv2] at hx13
+  step as ⟨b13, hb13⟩
+  have hb13v : b13.val = l2.val % 2^8 := by
+    rw [hb13, UScalar.cast_val_eq, hx13, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s14, hs14⟩
+  have hsl13 : (↑s14 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs14, Array.set_val_eq, hsl12]
+    rfl
+  clear hx13 hb13 hs14 hsl12
+  -- byte 14 (limb 2 >> 8)
+  step as ⟨x14, hx14⟩
+  rw [hv2] at hx14
+  step as ⟨b14, hb14⟩
+  have hb14v : b14.val = l2.val / 2^8 % 2^8 := by
+    rw [hb14, UScalar.cast_val_eq, hx14, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s15, hs15⟩
+  have hsl14 : (↑s15 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs15, Array.set_val_eq, hsl13]
+    rfl
+  clear hx14 hb14 hs15 hsl13
+  -- byte 15 (limb 2 >> 16)
+  step as ⟨x15, hx15⟩
+  rw [hv2] at hx15
+  step as ⟨b15, hb15⟩
+  have hb15v : b15.val = l2.val / 2^16 % 2^8 := by
+    rw [hb15, UScalar.cast_val_eq, hx15, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s16, hs16⟩
+  have hsl15 : (↑s16 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs16, Array.set_val_eq, hsl14]
+    rfl
+  clear hx15 hb15 hs16 hsl14
+  -- byte 16 (limb 2 >> 24)
+  step as ⟨x16, hx16⟩
+  rw [hv2] at hx16
+  step as ⟨b16, hb16⟩
+  have hb16v : b16.val = l2.val / 2^24 % 2^8 := by
+    rw [hb16, UScalar.cast_val_eq, hx16, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s17, hs17⟩
+  have hsl16 : (↑s17 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs17, Array.set_val_eq, hsl15]
+    rfl
+  clear hx16 hb16 hs17 hsl15
+  -- byte 17 (limb 2 >> 32)
+  step as ⟨x17, hx17⟩
+  rw [hv2] at hx17
+  step as ⟨b17, hb17⟩
+  have hb17v : b17.val = l2.val / 2^32 % 2^8 := by
+    rw [hb17, UScalar.cast_val_eq, hx17, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s18, hs18⟩
+  have hsl17 : (↑s18 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs18, Array.set_val_eq, hsl16]
+    rfl
+  clear hx17 hb17 hs18 hsl16
+  -- byte 18 (limb 2 >> 40)
+  step as ⟨x18, hx18⟩
+  rw [hv2] at hx18
+  step as ⟨b18, hb18⟩
+  have hb18v : b18.val = l2.val / 2^40 % 2^8 := by
+    rw [hb18, UScalar.cast_val_eq, hx18, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s19, hs19⟩
+  have hsl18 : (↑s19 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs19, Array.set_val_eq, hsl17]
+    rfl
+  clear hx18 hb18 hs19 hsl17
+  -- byte 19 (boundary: limb 2 >> 48 | limb 3 << 4)
+  step as ⟨x19, hx19⟩
+  rw [hv2] at hx19
+  step as ⟨v3, hv3⟩
+  simp [hl] at hv3
+  step as ⟨y19, hy19⟩
+  rw [hv3] at hy19
+  have hy19v : y19.val = l3.val * 2^4 := by
+    rw [hy19]
+    simp only [Nat.shiftLeft_eq]
+    rw [Nat.mod_eq_of_lt (show l3.val * 2^4 < U64.size by scalar_tac)]
+  step as ⟨z19, hz19⟩
+  step as ⟨b19, hb19⟩
+  have hb19v : b19.val = l2.val / 2^48 + (l3.val % 2^4) * 2^4 := by
+    rw [hb19, UScalar.cast_val_eq]
+    norm_num [UScalarTy.numBits]
+    rw [hz19, UScalar.val_or, hx19, nat_shr, hy19v]
+    have hxlt : l2.val / 2^48 < 2^4 := by omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := l2.val / 2^48) (i := 4) hxlt (l3.val)
+    have hadd : l2.val / 2^48 ||| l3.val * 2^4 = l2.val / 2^48 + l3.val * 2^4 := by
+      calc l2.val / 2^48 ||| l3.val * 2^4
+          = l2.val / 2^48 ||| 2^4 * l3.val := by rw [Nat.mul_comm]
+        _ = 2^4 * l3.val ||| l2.val / 2^48 := Nat.lor_comm _ _
+        _ = 2^4 * l3.val + l2.val / 2^48 := hor.symm
+        _ = l2.val / 2^48 + l3.val * 2^4 := by ring
+    rw [hadd]
+    omega
+  step as ⟨s20, hs20⟩
+  have hsl19 : (↑s20 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs20, Array.set_val_eq, hsl18]
+    rfl
+  clear hx19 hy19 hy19v hz19 hb19 hs20 hsl18
+  -- byte 20 (limb 3 >> 4)
+  step as ⟨x20, hx20⟩
+  rw [hv3] at hx20
+  step as ⟨b20, hb20⟩
+  have hb20v : b20.val = l3.val / 2^4 % 2^8 := by
+    rw [hb20, UScalar.cast_val_eq, hx20, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s21, hs21⟩
+  have hsl20 : (↑s21 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs21, Array.set_val_eq, hsl19]
+    rfl
+  clear hx20 hb20 hs21 hsl19
+  -- byte 21 (limb 3 >> 12)
+  step as ⟨x21, hx21⟩
+  rw [hv3] at hx21
+  step as ⟨b21, hb21⟩
+  have hb21v : b21.val = l3.val / 2^12 % 2^8 := by
+    rw [hb21, UScalar.cast_val_eq, hx21, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s22, hs22⟩
+  have hsl21 : (↑s22 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs22, Array.set_val_eq, hsl20]
+    rfl
+  clear hx21 hb21 hs22 hsl20
+  -- byte 22 (limb 3 >> 20)
+  step as ⟨x22, hx22⟩
+  rw [hv3] at hx22
+  step as ⟨b22, hb22⟩
+  have hb22v : b22.val = l3.val / 2^20 % 2^8 := by
+    rw [hb22, UScalar.cast_val_eq, hx22, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s23, hs23⟩
+  have hsl22 : (↑s23 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs23, Array.set_val_eq, hsl21]
+    rfl
+  clear hx22 hb22 hs23 hsl21
+  -- byte 23 (limb 3 >> 28)
+  step as ⟨x23, hx23⟩
+  rw [hv3] at hx23
+  step as ⟨b23, hb23⟩
+  have hb23v : b23.val = l3.val / 2^28 % 2^8 := by
+    rw [hb23, UScalar.cast_val_eq, hx23, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s24, hs24⟩
+  have hsl23 : (↑s24 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs24, Array.set_val_eq, hsl22]
+    rfl
+  clear hx23 hb23 hs24 hsl22
+  -- byte 24 (limb 3 >> 36)
+  step as ⟨x24, hx24⟩
+  rw [hv3] at hx24
+  step as ⟨b24, hb24⟩
+  have hb24v : b24.val = l3.val / 2^36 % 2^8 := by
+    rw [hb24, UScalar.cast_val_eq, hx24, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s25, hs25⟩
+  have hsl24 : (↑s25 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs25, Array.set_val_eq, hsl23]
+    rfl
+  clear hx24 hb24 hs25 hsl23
+  -- byte 25 (limb 3 >> 44)
+  step as ⟨x25, hx25⟩
+  rw [hv3] at hx25
+  step as ⟨b25, hb25⟩
+  have hb25v : b25.val = l3.val / 2^44 % 2^8 := by
+    rw [hb25, UScalar.cast_val_eq, hx25, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s26, hs26⟩
+  have hsl25 : (↑s26 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs26, Array.set_val_eq, hsl24]
+    rfl
+  clear hx25 hb25 hs26 hsl24
+  -- limb 4 read
+  step as ⟨v4, hv4⟩
+  simp [hl] at hv4
+  -- byte 26 (limb 4 >> 0)
+  step as ⟨x26, hx26⟩
+  rw [hv4] at hx26
+  step as ⟨b26, hb26⟩
+  have hb26v : b26.val = l4.val % 2^8 := by
+    rw [hb26, UScalar.cast_val_eq, hx26, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s27, hs27⟩
+  have hsl26 : (↑s27 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs27, Array.set_val_eq, hsl25]
+    rfl
+  clear hx26 hb26 hs27 hsl25
+  -- byte 27 (limb 4 >> 8)
+  step as ⟨x27, hx27⟩
+  rw [hv4] at hx27
+  step as ⟨b27, hb27⟩
+  have hb27v : b27.val = l4.val / 2^8 % 2^8 := by
+    rw [hb27, UScalar.cast_val_eq, hx27, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s28, hs28⟩
+  have hsl27 : (↑s28 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs28, Array.set_val_eq, hsl26]
+    rfl
+  clear hx27 hb27 hs28 hsl26
+  -- byte 28 (limb 4 >> 16)
+  step as ⟨x28, hx28⟩
+  rw [hv4] at hx28
+  step as ⟨b28, hb28⟩
+  have hb28v : b28.val = l4.val / 2^16 % 2^8 := by
+    rw [hb28, UScalar.cast_val_eq, hx28, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s29, hs29⟩
+  have hsl28 : (↑s29 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs29, Array.set_val_eq, hsl27]
+    rfl
+  clear hx28 hb28 hs29 hsl27
+  -- byte 29 (limb 4 >> 24)
+  step as ⟨x29, hx29⟩
+  rw [hv4] at hx29
+  step as ⟨b29, hb29⟩
+  have hb29v : b29.val = l4.val / 2^24 % 2^8 := by
+    rw [hb29, UScalar.cast_val_eq, hx29, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s30, hs30⟩
+  have hsl29 : (↑s30 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, 0#u8, 0#u8] := by
+    simp only [hs30, Array.set_val_eq, hsl28]
+    rfl
+  clear hx29 hb29 hs30 hsl28
+  -- byte 30 (limb 4 >> 32)
+  step as ⟨x30, hx30⟩
+  rw [hv4] at hx30
+  step as ⟨b30, hb30⟩
+  have hb30v : b30.val = l4.val / 2^32 % 2^8 := by
+    rw [hb30, UScalar.cast_val_eq, hx30, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s31, hs31⟩
+  have hsl30 : (↑s31 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, 0#u8] := by
+    simp only [hs31, Array.set_val_eq, hsl29]
+    rfl
+  clear hx30 hb30 hs31 hsl29
+  -- byte 31 (limb 4 >> 40)
+  step as ⟨x31, hx31⟩
+  rw [hv4] at hx31
+  step as ⟨b31, hb31⟩
+  have hb31v : b31.val = l4.val / 2^40 := by
+    rw [hb31, UScalar.cast_val_eq, hx31, nat_shr]
+    norm_num [UScalarTy.numBits]
+    omega
+  step as ⟨s32, hs32⟩
+  have hsl31 : (↑s32 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31] := by
+    simp only [hs32, Array.set_val_eq, hsl30]
+    rfl
+  clear hx31 hb31 hs32 hsl30
+  try simp only [spec_ok]
+  -- assembly via the 52-bit packing identity
+  have hsum : bytesVal s32 = l0.val + l1.val * 2^52 + l2.val * 2^104
+      + l3.val * 2^156 + l4.val * 2^208 := by
+    simp only [bytesVal, hsl31]
+    rw [hb0v, hb1v, hb2v, hb3v, hb4v, hb5v, hb6v, hb7v, hb8v, hb9v, hb10v,
+        hb11v, hb12v, hb13v, hb14v, hb15v, hb16v, hb17v, hb18v, hb19v, hb20v,
+        hb21v, hb22v, hb23v, hb24v, hb25v, hb26v, hb27v, hb28v, hb29v, hb30v,
+        hb31v]
+    exact scalar_pack l0.val l1.val l2.val l3.val l4.val hb0 hb1 hb2 hb3 hb4
+  rw [hsum, scVal_eq a l0 l1 l2 l3 l4 hl]
+  unfold scLimbs
+  ring
+
+/-- **The hash-to-scalar entry is total and canonical**: for a 64-byte input
+    of value T, `from_bytes_mod_order_wide` returns a Scalar whose 32 bytes
+    denote V with V < ℓ and V ≡ T (mod ℓ) — exactly the scalar premises the
+    dsm certificate consumes. -/
+theorem from_bytes_mod_order_wide_spec (input : Std.Array Std.U8 64#usize)
+    (b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 b32 b33 b34 b35 b36 b37 b38 b39 b40 b41 b42 b43 b44 b45 b46 b47 b48 b49 b50 b51 b52 b53 b54 b55 b56 b57 b58 b59 b60 b61 b62 b63 : Std.U8)
+    (hb : (↑input : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31, b32, b33, b34, b35, b36, b37, b38, b39, b40, b41, b42, b43, b44, b45, b46, b47, b48, b49, b50, b51, b52, b53, b54, b55, b56, b57, b58, b59, b60, b61, b62, b63])
+    (T : ℕ) (hT : T = b0.val + b1.val * 2^8 + b2.val * 2^16 + b3.val * 2^24 + b4.val * 2^32 + b5.val * 2^40 + b6.val * 2^48 + b7.val * 2^56 + b8.val * 2^64 + b9.val * 2^72 + b10.val * 2^80 + b11.val * 2^88 + b12.val * 2^96 + b13.val * 2^104 + b14.val * 2^112 + b15.val * 2^120 + b16.val * 2^128 + b17.val * 2^136 + b18.val * 2^144 + b19.val * 2^152 + b20.val * 2^160 + b21.val * 2^168 + b22.val * 2^176 + b23.val * 2^184 + b24.val * 2^192 + b25.val * 2^200 + b26.val * 2^208 + b27.val * 2^216 + b28.val * 2^224 + b29.val * 2^232 + b30.val * 2^240 + b31.val * 2^248 + b32.val * 2^256 + b33.val * 2^264 + b34.val * 2^272 + b35.val * 2^280 + b36.val * 2^288 + b37.val * 2^296 + b38.val * 2^304 + b39.val * 2^312 + b40.val * 2^320 + b41.val * 2^328 + b42.val * 2^336 + b43.val * 2^344 + b44.val * 2^352 + b45.val * 2^360 + b46.val * 2^368 + b47.val * 2^376 + b48.val * 2^384 + b49.val * 2^392 + b50.val * 2^400 + b51.val * 2^408 + b52.val * 2^416 + b53.val * 2^424 + b54.val * 2^432 + b55.val * 2^440 + b56.val * 2^448 + b57.val * 2^456 + b58.val * 2^464 + b59.val * 2^472 + b60.val * 2^480 + b61.val * 2^488 + b62.val * 2^496 + b63.val * 2^504) :
+    scalar.Scalar.from_bytes_mod_order_wide input
+      ⦃ k => bytesVal k.bytes < Ell ∧ (bytesVal k.bytes : ZMod Ell) = (T : ZMod Ell) ⦄ := by
+  unfold scalar.Scalar.from_bytes_mod_order_wide scalar.Scalar52.pack
+  step with (from_bytes_wide_spec input b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 b32 b33 b34 b35 b36 b37 b38 b39 b40 b41 b42 b43 b44 b45 b46 b47 b48 b49 b50 b51 b52 b53 b54 b55 b56 b57 b58 b59 b60 b61 b62 b63 hb T hT)
+    as ⟨r, hex, hlt, hden⟩
+  obtain ⟨s0, s1, s2, s3, s4, hrl, hs0, hs1, hs2, hs3, hs4⟩ := hex
+  -- top-limb tightening: scVal r < ℓ < 2²⁵³ forces s4 < 2⁴⁵ < 2⁴⁸
+  have hs4' : s4.val < 2^48 := by
+    have hv := scVal_eq r s0 s1 s2 s3 s4 hrl
+    have : scVal r < 2^253 := by
+      have : Ell < 2^253 := by unfold Ell; norm_num
+      omega
+    unfold scLimbs at hv
+    omega
+  step with (scalar52_to_bytes_spec r s0 s1 s2 s3 s4 hrl hs0 hs1 hs2 hs3 hs4')
+    as ⟨bytes, hbv⟩
+  try simp only [spec_ok]
+  constructor
+  · simpa [hbv] using hlt
+  · rw [hbv]
+    exact hden
+
+end ScalarProofs
diff --git a/verification/Proofs/ToBytesMath.lean b/verification/Proofs/ToBytesMath.lean
new file mode 100644
index 0000000..205b250
--- /dev/null
+++ b/verification/Proofs/ToBytesMath.lean
@@ -0,0 +1,281 @@
+/- ──────────────────────────────────────────────────────────────────────────────
+   Proofs/ToBytesMath.lean — the pure ℕ mathematics of `FieldElement51::to_bytes`
+   (phase 2 of the signature apex: compress semantics, brick "to_bytes canonicity").
+
+   `to_bytes` canonicalizes a weakly-reduced field element (limbs < 2⁵¹+19·2¹³,
+   hence value h < 2p) to r = h mod p and serializes r little-endian:
+
+   1. THE q-TRICK: q := carry of h + 19 out of bit 255 = (h+19)/2²⁵⁵, computed
+      limb-wise as a 5-rung carry telescope; q ∈ {0,1}, and q = 1 ↔ h ≥ p
+      (h ≥ p ↔ h + 19 ≥ 2²⁵⁵).                          (q_telescope, q_facts)
+   2. r = (h + 19q) mod 2²⁵⁵ = h mod p — adding 19q and discarding bit 255
+      subtracts exactly pq.                                        (q_mod_p)
+   3. The carry chain computing (h + 19q) mod 2²⁵⁵ limb-wise.    (carry_pack)
+   4. The 32-byte little-endian packing: each limb splits into byte chunks
+      (byte_split_*); their weighted sum reassembles the value. (bytes_pack)
+
+   Everything here is context-free ℕ arithmetic (METHOD 4: heavy identities in
+   isolation, applied once). The symbolic execution of the transpiled code
+   lives in Proofs/ToBytesSpec.lean, which consumes exactly these lemmas.
+   ────────────────────────────────────────────────────────────────────────────── -/
+import Proofs.Denote
+import Mathlib.Tactic.LinearCombination
+open Aeneas Aeneas.Std Result
+
+set_option maxHeartbeats 4000000
+
+namespace CurveFieldProofs
+
+/-- `>>>` on ℕ is division (generic-exponent companion of ReduceSpec's
+    `nat_shift_div`, which is specialized to 51). -/
+theorem nat_shr (n k : ℕ) : n >>> k = n / 2^k :=
+  Nat.shiftRight_eq_div_pow n k
+
+/-- One rung of a carry telescope: absorbing a floor-quotient into the next
+    limb and re-dividing is one division at the combined weight. -/
+theorem div_rung (a b j k : ℕ) : (a + b / 2^j) / 2^k = (a * 2^j + b) / 2^(j+k) := by
+  have h1 : (a * 2^j + b) / 2^j = a + b / 2^j := by
+    rw [Nat.add_comm (a * 2^j) b, Nat.add_mul_div_right _ _ (Nat.two_pow_pos j)]
+    omega
+  rw [← h1, Nat.div_div_eq_div_mul, ← pow_add]
+
+/-- THE q-TELESCOPE: the limb-wise 5-rung carry computation equals one
+    division of the assembled value by 2²⁵⁵. `x` is the (already offset)
+    limb-0 summand — in `to_bytes`, x = m0 + 19 for the q pass and
+    x = m0 + 19q for the final carry pass. -/
+theorem q_telescope (x m1 m2 m3 m4 : ℕ) :
+    (m4 + (m3 + (m2 + (m1 + x / 2^51) / 2^51) / 2^51) / 2^51) / 2^51
+      = (x + m1 * 2^51 + m2 * 2^102 + m3 * 2^153 + m4 * 2^204) / 2^255 := by
+  have h1 : (m1 + x / 2^51) / 2^51 = (m1 * 2^51 + x) / 2^102 := by
+    have h := div_rung m1 x 51 51; norm_num at h; exact h
+  have h2 : (m2 + (m1 * 2^51 + x) / 2^102) / 2^51
+      = (m2 * 2^102 + (m1 * 2^51 + x)) / 2^153 := by
+    have h := div_rung m2 (m1 * 2^51 + x) 102 51; norm_num at h; exact h
+  have h3 : (m3 + (m2 * 2^102 + (m1 * 2^51 + x)) / 2^153) / 2^51
+      = (m3 * 2^153 + (m2 * 2^102 + (m1 * 2^51 + x))) / 2^204 := by
+    have h := div_rung m3 (m2 * 2^102 + (m1 * 2^51 + x)) 153 51; norm_num at h; exact h
+  have h4 : (m4 + (m3 * 2^153 + (m2 * 2^102 + (m1 * 2^51 + x))) / 2^204) / 2^51
+      = (m4 * 2^204 + (m3 * 2^153 + (m2 * 2^102 + (m1 * 2^51 + x)))) / 2^255 := by
+    have h := div_rung m4 (m3 * 2^153 + (m2 * 2^102 + (m1 * 2^51 + x))) 204 51
+    norm_num at h; exact h
+  rw [h1, h2, h3, h4]
+  congr 1
+  ring
+
+/-- The q facts: for h < 2p (p = 2²⁵⁵ − 19), the carry q = (h+19)/2²⁵⁵ is a
+    bit, and it fires exactly when h is not yet canonical. -/
+theorem q_facts (h : ℕ) (hh : h < 2 * P) :
+    (h + 19) / 2^255 ≤ 1 ∧ ((h + 19) / 2^255 = 1 ↔ P ≤ h) := by
+  unfold P at *
+  constructor
+  · omega
+  · omega
+
+/-- Adding 19q and discarding bit 255 computes h mod p exactly. -/
+theorem q_mod_p (h : ℕ) (hh : h < 2 * P) :
+    (h + 19 * ((h + 19) / 2^255)) % 2^255 = h % P := by
+  have h1 : (h + 19) / 2^255 ≤ 1 := (q_facts h hh).1
+  rcases Nat.le_one_iff_eq_zero_or_eq_one.mp h1 with hq | hq <;>
+    · rw [hq]
+      unfold P at *
+      omega
+
+/-- THE CARRY-PACK ACCOUNTING: the masked limbs of the final carry pass
+    assemble to the value mod 2²⁵⁵. Stated over the *quotient/remainder
+    forms* the symbolic execution produces:
+      t₀ = x,  t_{i+1} = m_{i+1} + t_i / 2⁵¹,  f_i = t_i mod 2⁵¹. -/
+theorem carry_pack (x m1 m2 m3 m4 : ℕ) :
+    (x % 2^51)
+      + ((m1 + x / 2^51) % 2^51) * 2^51
+      + ((m2 + (m1 + x / 2^51) / 2^51) % 2^51) * 2^102
+      + ((m3 + (m2 + (m1 + x / 2^51) / 2^51) / 2^51) % 2^51) * 2^153
+      + ((m4 + (m3 + (m2 + (m1 + x / 2^51) / 2^51) / 2^51) / 2^51) % 2^51) * 2^204
+      = (x + m1 * 2^51 + m2 * 2^102 + m3 * 2^153 + m4 * 2^204) % 2^255 := by
+  -- name the telescope stages
+  set t0 := x with ht0
+  set t1 := m1 + t0 / 2^51 with ht1
+  set t2 := m2 + t1 / 2^51 with ht2
+  set t3 := m3 + t2 / 2^51 with ht3
+  set t4 := m4 + t3 / 2^51 with ht4
+  -- the top carry-out equals the global quotient (the same telescope as q)
+  have htop : t4 / 2^51
+      = (x + m1 * 2^51 + m2 * 2^102 + m3 * 2^153 + m4 * 2^204) / 2^255 := by
+    simpa [ht1, ht2, ht3, ht4] using q_telescope x m1 m2 m3 m4
+  -- flat div/mod facts for each stage
+  have d0 := Nat.div_add_mod t0 (2^51)
+  have d1 := Nat.div_add_mod t1 (2^51)
+  have d2 := Nat.div_add_mod t2 (2^51)
+  have d3 := Nat.div_add_mod t3 (2^51)
+  have d4 := Nat.div_add_mod t4 (2^51)
+  have dT := Nat.div_add_mod
+    (x + m1 * 2^51 + m2 * 2^102 + m3 * 2^153 + m4 * 2^204) (2^255)
+  -- linear assembly: Σ fᵢ·2⁵¹ⁱ + 2²⁵⁵·(t4/2⁵¹) = T, then subtract via dT
+  omega
+
+/-! ### Byte-chunk splits: one per limb, offsets follow 51·j mod 8. -/
+
+/-- Limb 0 (bit offset 0): bytes 0–5 whole, low 3 bits of byte 6. -/
+theorem byte_split_0 (f : ℕ) :
+    f % 2^8 + (f / 2^8 % 2^8) * 2^8 + (f / 2^16 % 2^8) * 2^16
+      + (f / 2^24 % 2^8) * 2^24 + (f / 2^32 % 2^8) * 2^32
+      + (f / 2^40 % 2^8) * 2^40 + (f / 2^48) * 2^48 = f := by
+  have e1 : f / 2^8 / 2^8 = f / 2^16 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e2 : f / 2^16 / 2^8 = f / 2^24 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e3 : f / 2^24 / 2^8 = f / 2^32 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e4 : f / 2^32 / 2^8 = f / 2^40 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e5 : f / 2^40 / 2^8 = f / 2^48 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have d0 := Nat.div_add_mod f (2^8)
+  have d1 := Nat.div_add_mod (f / 2^8) (2^8)
+  have d2 := Nat.div_add_mod (f / 2^16) (2^8)
+  have d3 := Nat.div_add_mod (f / 2^24) (2^8)
+  have d4 := Nat.div_add_mod (f / 2^32) (2^8)
+  have d5 := Nat.div_add_mod (f / 2^40) (2^8)
+  omega
+
+/-- Limb 1 (bit offset 3): low 5 bits close byte 6, bytes 7–11 whole,
+    low 6 bits of byte 12 take the top (f < 2⁵¹ ⇒ f/2⁴⁵ < 2⁶). -/
+theorem byte_split_1 (f : ℕ) :
+    f % 2^5 + (f / 2^5 % 2^8) * 2^5 + (f / 2^13 % 2^8) * 2^13
+      + (f / 2^21 % 2^8) * 2^21 + (f / 2^29 % 2^8) * 2^29
+      + (f / 2^37 % 2^8) * 2^37 + (f / 2^45) * 2^45 = f := by
+  have e1 : f / 2^5 / 2^8 = f / 2^13 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e2 : f / 2^13 / 2^8 = f / 2^21 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e3 : f / 2^21 / 2^8 = f / 2^29 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e4 : f / 2^29 / 2^8 = f / 2^37 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e5 : f / 2^37 / 2^8 = f / 2^45 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have d0 := Nat.div_add_mod f (2^5)
+  have d1 := Nat.div_add_mod (f / 2^5) (2^8)
+  have d2 := Nat.div_add_mod (f / 2^13) (2^8)
+  have d3 := Nat.div_add_mod (f / 2^21) (2^8)
+  have d4 := Nat.div_add_mod (f / 2^29) (2^8)
+  have d5 := Nat.div_add_mod (f / 2^37) (2^8)
+  omega
+
+/-- Limb 2 (bit offset 6): low 2 bits close byte 12, bytes 13–18 whole,
+    the single top bit lands in byte 19 (f/2⁵⁰ < 2). -/
+theorem byte_split_2 (f : ℕ) :
+    f % 2^2 + (f / 2^2 % 2^8) * 2^2 + (f / 2^10 % 2^8) * 2^10
+      + (f / 2^18 % 2^8) * 2^18 + (f / 2^26 % 2^8) * 2^26
+      + (f / 2^34 % 2^8) * 2^34 + (f / 2^42 % 2^8) * 2^42
+      + (f / 2^50) * 2^50 = f := by
+  have e1 : f / 2^2 / 2^8 = f / 2^10 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e2 : f / 2^10 / 2^8 = f / 2^18 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e3 : f / 2^18 / 2^8 = f / 2^26 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e4 : f / 2^26 / 2^8 = f / 2^34 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e5 : f / 2^34 / 2^8 = f / 2^42 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e6 : f / 2^42 / 2^8 = f / 2^50 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have d0 := Nat.div_add_mod f (2^2)
+  have d1 := Nat.div_add_mod (f / 2^2) (2^8)
+  have d2 := Nat.div_add_mod (f / 2^10) (2^8)
+  have d3 := Nat.div_add_mod (f / 2^18) (2^8)
+  have d4 := Nat.div_add_mod (f / 2^26) (2^8)
+  have d5 := Nat.div_add_mod (f / 2^34) (2^8)
+  have d6 := Nat.div_add_mod (f / 2^42) (2^8)
+  omega
+
+/-- Limb 3 (bit offset 1): low 7 bits close byte 19, bytes 20–24 whole,
+    low 4 bits of byte 25 take the top (f/2⁴⁷ < 2⁴). -/
+theorem byte_split_3 (f : ℕ) :
+    f % 2^7 + (f / 2^7 % 2^8) * 2^7 + (f / 2^15 % 2^8) * 2^15
+      + (f / 2^23 % 2^8) * 2^23 + (f / 2^31 % 2^8) * 2^31
+      + (f / 2^39 % 2^8) * 2^39 + (f / 2^47) * 2^47 = f := by
+  have e1 : f / 2^7 / 2^8 = f / 2^15 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e2 : f / 2^15 / 2^8 = f / 2^23 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e3 : f / 2^23 / 2^8 = f / 2^31 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e4 : f / 2^31 / 2^8 = f / 2^39 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e5 : f / 2^39 / 2^8 = f / 2^47 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have d0 := Nat.div_add_mod f (2^7)
+  have d1 := Nat.div_add_mod (f / 2^7) (2^8)
+  have d2 := Nat.div_add_mod (f / 2^15) (2^8)
+  have d3 := Nat.div_add_mod (f / 2^23) (2^8)
+  have d4 := Nat.div_add_mod (f / 2^31) (2^8)
+  have d5 := Nat.div_add_mod (f / 2^39) (2^8)
+  omega
+
+/-- Limb 4 (bit offset 4): high 4 bits of byte 25 take the low 4 bits,
+    bytes 26–31 whole (f/2⁴⁴ < 2⁷ — the canonical top byte < 2⁷). -/
+theorem byte_split_4 (f : ℕ) :
+    f % 2^4 + (f / 2^4 % 2^8) * 2^4 + (f / 2^12 % 2^8) * 2^12
+      + (f / 2^20 % 2^8) * 2^20 + (f / 2^28 % 2^8) * 2^28
+      + (f / 2^36 % 2^8) * 2^36 + (f / 2^44) * 2^44 = f := by
+  have e1 : f / 2^4 / 2^8 = f / 2^12 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e2 : f / 2^12 / 2^8 = f / 2^20 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e3 : f / 2^20 / 2^8 = f / 2^28 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e4 : f / 2^28 / 2^8 = f / 2^36 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have e5 : f / 2^36 / 2^8 = f / 2^44 := by rw [Nat.div_div_eq_div_mul]; norm_num
+  have d0 := Nat.div_add_mod f (2^4)
+  have d1 := Nat.div_add_mod (f / 2^4) (2^8)
+  have d2 := Nat.div_add_mod (f / 2^12) (2^8)
+  have d3 := Nat.div_add_mod (f / 2^20) (2^8)
+  have d4 := Nat.div_add_mod (f / 2^28) (2^8)
+  have d5 := Nat.div_add_mod (f / 2^36) (2^8)
+  omega
+
+/-- THE PACKING IDENTITY: the 32 little-endian bytes that `to_bytes` emits —
+    27 plain shift-extracts plus 4 boundary bytes (each an OR of the high
+    bits of one limb with the low bits of the next, already normalized to
+    its additive form by the walk) — assemble to the limb value. -/
+theorem bytes_pack (f0 f1 f2 f3 f4 : ℕ)
+    (h0 : f0 < 2^51) (h1 : f1 < 2^51) (h2 : f2 < 2^51)
+    (h3 : f3 < 2^51) (h4 : f4 < 2^51) :
+    (f0 % 2^8)
+      + (f0 / 2^8 % 2^8) * 2^8
+      + (f0 / 2^16 % 2^8) * 2^16
+      + (f0 / 2^24 % 2^8) * 2^24
+      + (f0 / 2^32 % 2^8) * 2^32
+      + (f0 / 2^40 % 2^8) * 2^40
+      + (f0 / 2^48 + (f1 % 2^5) * 2^3) * 2^48
+      + (f1 / 2^5 % 2^8) * 2^56
+      + (f1 / 2^13 % 2^8) * 2^64
+      + (f1 / 2^21 % 2^8) * 2^72
+      + (f1 / 2^29 % 2^8) * 2^80
+      + (f1 / 2^37 % 2^8) * 2^88
+      + (f1 / 2^45 + (f2 % 2^2) * 2^6) * 2^96
+      + (f2 / 2^2 % 2^8) * 2^104
+      + (f2 / 2^10 % 2^8) * 2^112
+      + (f2 / 2^18 % 2^8) * 2^120
+      + (f2 / 2^26 % 2^8) * 2^128
+      + (f2 / 2^34 % 2^8) * 2^136
+      + (f2 / 2^42 % 2^8) * 2^144
+      + (f2 / 2^50 + (f3 % 2^7) * 2^1) * 2^152
+      + (f3 / 2^7 % 2^8) * 2^160
+      + (f3 / 2^15 % 2^8) * 2^168
+      + (f3 / 2^23 % 2^8) * 2^176
+      + (f3 / 2^31 % 2^8) * 2^184
+      + (f3 / 2^39 % 2^8) * 2^192
+      + (f3 / 2^47 + (f4 % 2^4) * 2^4) * 2^200
+      + (f4 / 2^4 % 2^8) * 2^208
+      + (f4 / 2^12 % 2^8) * 2^216
+      + (f4 / 2^20 % 2^8) * 2^224
+      + (f4 / 2^28 % 2^8) * 2^232
+      + (f4 / 2^36 % 2^8) * 2^240
+      + (f4 / 2^44) * 2^248
+      = f0 + f1 * 2^51 + f2 * 2^102 + f3 * 2^153 + f4 * 2^204 := by
+  have s0 := byte_split_0 f0
+  have s1 := byte_split_1 f1
+  have s2 := byte_split_2 f2
+  have s3 := byte_split_3 f3
+  have s4 := byte_split_4 f4
+  -- Each limb's split, scaled by its radix weight, accounts for exactly the
+  -- terms above that mention it (boundary bytes contribute to two limbs).
+  -- Cast to ℤ and take the weighted linear combination of the five splits.
+  zify at s0 s1 s2 s3 s4 ⊢
+  linear_combination s0 + 2^51 * s1 + 2^102 * s2 + 2^153 * s3 + 2^204 * s4
+
+/-- Setting a clear top bit by XOR is addition (compress's sign-bit write). -/
+theorem xor_top_bit (a : ℕ) (h : a < 2^7) : a ^^^ 2^7 = a + 2^7 := by
+  have hdiv : (a ^^^ 2^7) / 2^7 = 1 := by
+    rw [Nat.xor_div_two_pow]
+    rw [Nat.div_eq_of_lt h]
+    norm_num
+  have hand := Nat.and_two_pow_sub_one_eq_mod (a ^^^ 2^7) 7
+  have hdistrib := Nat.and_xor_distrib_right (a := a) (b := 2^7) (c := 2^7 - 1)
+  have ha : a &&& (2^7 - 1) = a := by
+    rw [Nat.and_two_pow_sub_one_eq_mod, Nat.mod_eq_of_lt h]
+  have h2 : 2^7 &&& (2^7 - 1) = 0 := by decide
+  have hmod : (a ^^^ 2^7) % 2^7 = a := by
+    rw [← hand, hdistrib, ha, h2, Nat.xor_zero]
+  have hdm := Nat.div_add_mod (a ^^^ 2^7) (2^7)
+  omega
+
+end CurveFieldProofs
diff --git a/verification/Proofs/ToBytesSpec.lean b/verification/Proofs/ToBytesSpec.lean
new file mode 100644
index 0000000..4712ef2
--- /dev/null
+++ b/verification/Proofs/ToBytesSpec.lean
@@ -0,0 +1,767 @@
+/- ──────────────────────────────────────────────────────────────────────────────
+   Proofs/ToBytesSpec.lean — total-correctness spec of `FieldElement51::to_bytes`
+   (phase 2 of the signature apex: the "to_bytes canonicity" brick).
+
+   THE THEOREM (`to_bytes_spec`): for any field element a,
+       to_bytes a = ok s   with   bytesVal s = feVal a mod p
+   — the emitted 32 bytes are the CANONICAL little-endian encoding of the
+   represented residue. Canonicity (bytesVal s < p, top bit clear) and
+   injectivity ("equal residues ⇒ equal bytes, equal bytes ⇒ equal residues")
+   are corollaries (`to_bytes_lt`, at the end), because bytesVal s is pinned
+   to the residue itself.
+
+   STRUCTURE: one straight-line symbolic execution (~150 machine ops — the
+   longest walk in the repo, but loop-free), consuming the pure ℕ lemmas of
+   Proofs/ToBytesMath.lean at exactly four joints:
+     q_telescope   — the 5-rung carry chain that computes q = (h+19)/2²⁵⁵;
+     q_facts       — q ∈ {0,1} (also feeds the no-overflow side conditions);
+     carry_pack + q_mod_p — the final carry pass assembles (h+19q) mod 2²⁵⁵
+                     = h mod p;
+     bytes_pack    — the 32 shift/mask extractions reassemble the value.
+   The four boundary bytes (6, 12, 19, 25) OR the high bits of one limb with
+   the low bits of the next; disjointness turns each OR into +
+   (Nat.two_pow_add_eq_or_of_lt, the ScalarBytesSpec idiom).
+
+   Rust: `FieldElement51::to_bytes`, curve25519-dalek/src/backend/serial/u64/
+   field.rs:368-450 (incl. its trailing debug-assert that the top bit is
+   clear — discharged, not assumed). Gen: gen/CurveField/Funs.lean
+   `backend.serial.u64.field.FieldElement51.as_bytes`.
+   ────────────────────────────────────────────────────────────────────────────── -/
+import Proofs.ReduceSpec
+import Proofs.ToBytesMath
+open Aeneas Aeneas.Std Result
+open curve25519_dalek
+
+set_option maxHeartbeats 8000000
+set_option linter.unusedSimpArgs false
+set_option maxRecDepth 8000
+
+namespace CurveFieldProofs
+
+open Aeneas.Std.WP
+
+abbrev fe_to_bytes := backend.serial.u64.field.FieldElement51.as_bytes
+
+/-- Little-endian value of a 32-byte array (match-style, like `feVal`). -/
+def bytesVal (s : Std.Array Std.U8 32#usize) : ℕ :=
+  match (↑s : List Std.U8) with
+  | [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15,
+     b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31] =>
+    b0.val + b1.val * 2^8 + b2.val * 2^16 + b3.val * 2^24 + b4.val * 2^32
+      + b5.val * 2^40 + b6.val * 2^48 + b7.val * 2^56 + b8.val * 2^64
+      + b9.val * 2^72 + b10.val * 2^80 + b11.val * 2^88 + b12.val * 2^96
+      + b13.val * 2^104 + b14.val * 2^112 + b15.val * 2^120 + b16.val * 2^128
+      + b17.val * 2^136 + b18.val * 2^144 + b19.val * 2^152 + b20.val * 2^160
+      + b21.val * 2^168 + b22.val * 2^176 + b23.val * 2^184 + b24.val * 2^192
+      + b25.val * 2^200 + b26.val * 2^208 + b27.val * 2^216 + b28.val * 2^224
+      + b29.val * 2^232 + b30.val * 2^240 + b31.val * 2^248
+  | _ => 0
+
+/-- **`to_bytes` is the canonical encoder**: it always succeeds and its
+    output bytes denote exactly the represented residue mod p. -/
+theorem to_bytes_spec (a : Fe) (l0 l1 l2 l3 l4 : U64)
+    (hl : (↑a : List U64) = [l0, l1, l2, l3, l4]) :
+    fe_to_bytes a ⦃ s => bytesVal s = feVal a % P ⦄ := by
+  unfold fe_to_bytes backend.serial.u64.field.FieldElement51.as_bytes
+  -- weak reduction: limbs < 2⁵¹ + 19·2¹³, value preserved mod p (exactly)
+  step with (reduce_spec a l0 l1 l2 l3 l4 hl) as ⟨fe, hbnd, hval⟩
+  obtain ⟨m0, m1, m2, m3, m4, hm⟩ := Fe.exists_limbs fe
+  rw [Bnd_eq fe m0 m1 m2 m3 m4 _ hm] at hbnd
+  obtain ⟨hbm0, hbm1, hbm2, hbm3, hbm4⟩ := hbnd
+  rw [feVal_eq fe m0 m1 m2 m3 m4 hm] at hval
+  -- h := the weakly-reduced value; h < 2p
+  have hh2p : limbsVal m0 m1 m2 m3 m4 < 2 * P := by
+    unfold limbsVal P
+    omega
+  -- ── the q pass: q = (h+19)/2²⁵⁵ ─────────────────────────────────────────
+  step as ⟨i, hi⟩
+  simp [hm] at hi
+  step as ⟨i1, hi1⟩
+  rw [hi] at hi1
+  step as ⟨q, hq⟩
+  step as ⟨i2, hi2⟩
+  simp [hm] at hi2
+  step as ⟨i3, hi3⟩
+  rw [hi2] at hi3
+  step as ⟨q1, hq1⟩
+  step as ⟨i4, hi4⟩
+  simp [hm] at hi4
+  step as ⟨i5, hi5⟩
+  rw [hi4] at hi5
+  step as ⟨q2, hq2⟩
+  step as ⟨i6, hi6⟩
+  simp [hm] at hi6
+  step as ⟨i7, hi7⟩
+  rw [hi6] at hi7
+  step as ⟨q3, hq3⟩
+  step as ⟨i8, hi8⟩
+  simp [hm] at hi8
+  step as ⟨i9, hi9⟩
+  rw [hi8] at hi9
+  step as ⟨q4, hq4⟩
+  -- q4 = (h + 19) / 2²⁵⁵, and q4 ≤ 1
+  have hq4v : q4.val = (limbsVal m0 m1 m2 m3 m4 + 19) / 2^255 := by
+    rw [hq4, nat_shr, hi9, hq3, nat_shr, hi7, hq2, nat_shr, hi5, hq1, nat_shr,
+        hi3, hq, nat_shr, hi1]
+    have := q_telescope (m0.val + 19) m1.val m2.val m3.val m4.val
+    unfold limbsVal
+    omega
+  have hq4le : q4.val ≤ 1 := by
+    rw [hq4v]; exact (q_facts _ hh2p).1
+  -- fold 19q into limb 0
+  step as ⟨i10, hi10⟩
+  step as ⟨i11, hi11⟩
+  rw [hi] at hi11
+  step as ⟨limbs, hlimbs⟩
+  have hll : (↑limbs : List U64) = [i11, m1, m2, m3, m4] := by
+    simp only [hlimbs, Array.set_val_eq, hm]
+    rfl
+  have hi11v : i11.val = m0.val + 19 * q4.val := by
+    rw [hi11, hi10]
+  -- the local mask constant 2⁵¹ − 1
+  step as ⟨i12, hi12⟩
+  step as ⟨mask, hmask⟩
+  have hmaskv : mask.val = 2251799813685247 := by
+    rw [hmask, hi12]
+    simp [Nat.shiftLeft_eq]
+    scalar_tac
+  have hmask_mod : ∀ n : ℕ, n &&& mask.val = n % 2^51 := by
+    intro n
+    rw [hmaskv, nat_and_mask]
+    norm_num
+  -- ── the carry pass: normalize to radix 2⁵¹, dropping the 2²⁵⁵ carry ────
+  -- round 0→1
+  step as ⟨i13, hi13⟩
+  simp [hll] at hi13
+  step as ⟨i14, hi14⟩
+  rw [hi13] at hi14
+  step as ⟨i15, hi15⟩
+  simp [hll] at hi15
+  step as ⟨i16, hi16⟩
+  rw [hi15] at hi16
+  step as ⟨limbs1, hlimbs1⟩
+  have hll1 : (↑limbs1 : List U64) = [i11, i16, m2, m3, m4] := by
+    simp only [hlimbs1, Array.set_val_eq, hll]; rfl
+  step as ⟨i17, hi17⟩
+  simp [hll1] at hi17
+  step as ⟨i18, hi18⟩
+  rw [hi17] at hi18
+  step as ⟨limbs2, hlimbs2⟩
+  have hll2 : (↑limbs2 : List U64) = [i18, i16, m2, m3, m4] := by
+    simp only [hlimbs2, Array.set_val_eq, hll1]; rfl
+  -- round 1→2
+  step as ⟨i19, hi19⟩
+  simp [hll2] at hi19
+  step as ⟨i20, hi20⟩
+  rw [hi19] at hi20
+  step as ⟨i21, hi21⟩
+  simp [hll2] at hi21
+  step as ⟨i22, hi22⟩
+  rw [hi21] at hi22
+  step as ⟨limbs3, hlimbs3⟩
+  have hll3 : (↑limbs3 : List U64) = [i18, i16, i22, m3, m4] := by
+    simp only [hlimbs3, Array.set_val_eq, hll2]; rfl
+  step as ⟨i23, hi23⟩
+  simp [hll3] at hi23
+  step as ⟨i24, hi24⟩
+  rw [hi23] at hi24
+  step as ⟨limbs4, hlimbs4⟩
+  have hll4 : (↑limbs4 : List U64) = [i18, i24, i22, m3, m4] := by
+    simp only [hlimbs4, Array.set_val_eq, hll3]; rfl
+  -- round 2→3
+  step as ⟨i25, hi25⟩
+  simp [hll4] at hi25
+  step as ⟨i26, hi26⟩
+  rw [hi25] at hi26
+  step as ⟨i27, hi27⟩
+  simp [hll4] at hi27
+  step as ⟨i28, hi28⟩
+  rw [hi27] at hi28
+  step as ⟨limbs5, hlimbs5⟩
+  have hll5 : (↑limbs5 : List U64) = [i18, i24, i22, i28, m4] := by
+    simp only [hlimbs5, Array.set_val_eq, hll4]; rfl
+  step as ⟨i29, hi29⟩
+  simp [hll5] at hi29
+  step as ⟨i30, hi30⟩
+  rw [hi29] at hi30
+  step as ⟨limbs6, hlimbs6⟩
+  have hll6 : (↑limbs6 : List U64) = [i18, i24, i30, i28, m4] := by
+    simp only [hlimbs6, Array.set_val_eq, hll5]; rfl
+  -- round 3→4
+  step as ⟨i31, hi31⟩
+  simp [hll6] at hi31
+  step as ⟨i32, hi32⟩
+  rw [hi31] at hi32
+  step as ⟨i33, hi33⟩
+  simp [hll6] at hi33
+  step as ⟨i34, hi34⟩
+  rw [hi33] at hi34
+  step as ⟨limbs7, hlimbs7⟩
+  have hll7 : (↑limbs7 : List U64) = [i18, i24, i30, i28, i34] := by
+    simp only [hlimbs7, Array.set_val_eq, hll6]; rfl
+  step as ⟨i35, hi35⟩
+  simp [hll7] at hi35
+  step as ⟨i36, hi36⟩
+  rw [hi35] at hi36
+  step as ⟨limbs8, hlimbs8⟩
+  have hll8 : (↑limbs8 : List U64) = [i18, i24, i30, i36, i34] := by
+    simp only [hlimbs8, Array.set_val_eq, hll7]; rfl
+  -- top slot: final mask
+  step as ⟨i37, hi37⟩
+  simp [hll8] at hi37
+  step as ⟨i38, hi38⟩
+  rw [hi37] at hi38
+  step as ⟨limbs9, hlimbs9⟩
+  have hll9 : (↑limbs9 : List U64) = [i18, i24, i30, i36, i38] := by
+    simp only [hlimbs9, Array.set_val_eq, hll8]; rfl
+  -- ── final-limb values in the exact nested q/r forms carry_pack expects ──
+  have hf0v : i18.val = i11.val % 2^51 := by
+    rw [hi18, UScalar.val_and, hmask_mod]
+  have hi14v : i14.val = i11.val / 2^51 := by
+    rw [hi14, nat_shr]
+  have hi16v : i16.val = m1.val + i11.val / 2^51 := by
+    rw [hi16, hi14v]
+  have hf1v : i24.val = (m1.val + i11.val / 2^51) % 2^51 := by
+    rw [hi24, UScalar.val_and, hmask_mod, hi16v]
+  have hi20v : i20.val = (m1.val + i11.val / 2^51) / 2^51 := by
+    rw [hi20, nat_shr, hi16v]
+  have hi22v : i22.val = m2.val + (m1.val + i11.val / 2^51) / 2^51 := by
+    rw [hi22, hi20v]
+  have hf2v : i30.val = (m2.val + (m1.val + i11.val / 2^51) / 2^51) % 2^51 := by
+    rw [hi30, UScalar.val_and, hmask_mod, hi22v]
+  have hi26v : i26.val = (m2.val + (m1.val + i11.val / 2^51) / 2^51) / 2^51 := by
+    rw [hi26, nat_shr, hi22v]
+  have hi28v : i28.val = m3.val + (m2.val + (m1.val + i11.val / 2^51) / 2^51) / 2^51 := by
+    rw [hi28, hi26v]
+  have hf3v : i36.val = (m3.val + (m2.val + (m1.val + i11.val / 2^51) / 2^51) / 2^51) % 2^51 := by
+    rw [hi36, UScalar.val_and, hmask_mod, hi28v]
+  have hi32v : i32.val = (m3.val + (m2.val + (m1.val + i11.val / 2^51) / 2^51) / 2^51) / 2^51 := by
+    rw [hi32, nat_shr, hi28v]
+  have hi34v : i34.val = m4.val + (m3.val + (m2.val + (m1.val + i11.val / 2^51) / 2^51) / 2^51) / 2^51 := by
+    rw [hi34, hi32v]
+  have hf4v : i38.val = (m4.val + (m3.val + (m2.val + (m1.val + i11.val / 2^51) / 2^51) / 2^51) / 2^51) % 2^51 := by
+    rw [hi38, UScalar.val_and, hmask_mod, hi34v]
+  have hf0lt : i18.val < 2^51 := by rw [hf0v]; exact Nat.mod_lt _ (by norm_num)
+  have hf1lt : i24.val < 2^51 := by rw [hf1v]; exact Nat.mod_lt _ (by norm_num)
+  have hf2lt : i30.val < 2^51 := by rw [hf2v]; exact Nat.mod_lt _ (by norm_num)
+  have hf3lt : i36.val < 2^51 := by rw [hf3v]; exact Nat.mod_lt _ (by norm_num)
+  have hf4lt : i38.val < 2^51 := by rw [hf4v]; exact Nat.mod_lt _ (by norm_num)
+  clear hi14 hi16 hi20 hi22 hi26 hi28 hi32 hi34 hi18 hi24 hi30 hi36 hi38
+  clear hi14v hi16v hi20v hi22v hi26v hi28v hi32v hi34v
+  clear hlimbs hlimbs1 hlimbs2 hlimbs3 hlimbs4 hlimbs5 hlimbs6 hlimbs7 hlimbs8 hlimbs9
+  clear hll hll1 hll2 hll3 hll4 hll5 hll6 hll7 hll8
+  -- ── the 32 byte extractions ──────────────────────────────────────────────
+  -- byte 0 (limb 0 read + low byte)
+  step as ⟨v0, hv0⟩
+  simp [hll9] at hv0
+  step as ⟨b0, hb0⟩
+  rw [hv0] at hb0
+  have hb0v : b0.val = i18.val % 2^8 := by
+    rw [hb0, UScalar.cast_val_eq]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s1, hs1⟩
+  have hsl0 : (↑s1 : List Std.U8) = [b0, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs1, Array.set_val_eq, Array.repeat_val]
+    rfl
+  clear hb0 hs1
+  -- byte 1 (limb 0 >> 8)
+  step as ⟨x1, hx1⟩
+  rw [hv0] at hx1
+  step as ⟨b1, hb1⟩
+  have hb1v : b1.val = i18.val / 2^8 % 2^8 := by
+    rw [hb1, UScalar.cast_val_eq, hx1, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s2, hs2⟩
+  have hsl1 : (↑s2 : List Std.U8) = [b0, b1, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs2, Array.set_val_eq, hsl0]
+    rfl
+  clear hx1 hb1 hs2 hsl0
+  -- byte 2 (limb 0 >> 16)
+  step as ⟨x2, hx2⟩
+  rw [hv0] at hx2
+  step as ⟨b2, hb2⟩
+  have hb2v : b2.val = i18.val / 2^16 % 2^8 := by
+    rw [hb2, UScalar.cast_val_eq, hx2, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s3, hs3⟩
+  have hsl2 : (↑s3 : List Std.U8) = [b0, b1, b2, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs3, Array.set_val_eq, hsl1]
+    rfl
+  clear hx2 hb2 hs3 hsl1
+  -- byte 3 (limb 0 >> 24)
+  step as ⟨x3, hx3⟩
+  rw [hv0] at hx3
+  step as ⟨b3, hb3⟩
+  have hb3v : b3.val = i18.val / 2^24 % 2^8 := by
+    rw [hb3, UScalar.cast_val_eq, hx3, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s4, hs4⟩
+  have hsl3 : (↑s4 : List Std.U8) = [b0, b1, b2, b3, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs4, Array.set_val_eq, hsl2]
+    rfl
+  clear hx3 hb3 hs4 hsl2
+  -- byte 4 (limb 0 >> 32)
+  step as ⟨x4, hx4⟩
+  rw [hv0] at hx4
+  step as ⟨b4, hb4⟩
+  have hb4v : b4.val = i18.val / 2^32 % 2^8 := by
+    rw [hb4, UScalar.cast_val_eq, hx4, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s5, hs5⟩
+  have hsl4 : (↑s5 : List Std.U8) = [b0, b1, b2, b3, b4, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs5, Array.set_val_eq, hsl3]
+    rfl
+  clear hx4 hb4 hs5 hsl3
+  -- byte 5 (limb 0 >> 40)
+  step as ⟨x5, hx5⟩
+  rw [hv0] at hx5
+  step as ⟨b5, hb5⟩
+  have hb5v : b5.val = i18.val / 2^40 % 2^8 := by
+    rw [hb5, UScalar.cast_val_eq, hx5, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s6, hs6⟩
+  have hsl5 : (↑s6 : List Std.U8) = [b0, b1, b2, b3, b4, b5, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs6, Array.set_val_eq, hsl4]
+    rfl
+  clear hx5 hb5 hs6 hsl4
+  -- byte 6 (boundary: limb 0 >> 48  |  limb 1 << 3)
+  step as ⟨x6, hx6⟩
+  rw [hv0] at hx6
+  step as ⟨v1, hv1⟩
+  simp [hll9] at hv1
+  step as ⟨y6, hy6⟩
+  rw [hv1] at hy6
+  have hy6v : y6.val = i24.val * 2^3 := by
+    rw [hy6]
+    simp only [Nat.shiftLeft_eq]
+    rw [Nat.mod_eq_of_lt (show i24.val * 2^3 < U64.size by scalar_tac)]
+  step as ⟨z6, hz6⟩
+  step as ⟨b6, hb6⟩
+  have hb6v : b6.val = i18.val / 2^48 + (i24.val % 2^5) * 2^3 := by
+    rw [hb6, UScalar.cast_val_eq]
+    norm_num [UScalarTy.numBits]
+    rw [hz6, UScalar.val_or, hx6, nat_shr, hy6v]
+    have hxlt : i18.val / 2^48 < 2^3 := by omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := i18.val / 2^48) (i := 3) hxlt (i24.val)
+    have hadd : i18.val / 2^48 ||| i24.val * 2^3 = i18.val / 2^48 + i24.val * 2^3 := by
+      calc i18.val / 2^48 ||| i24.val * 2^3
+          = i18.val / 2^48 ||| 2^3 * i24.val := by rw [Nat.mul_comm]
+        _ = 2^3 * i24.val ||| i18.val / 2^48 := Nat.lor_comm _ _
+        _ = 2^3 * i24.val + i18.val / 2^48 := hor.symm
+        _ = i18.val / 2^48 + i24.val * 2^3 := by ring
+    rw [hadd]
+    omega
+  step as ⟨s7, hs7⟩
+  have hsl6 : (↑s7 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs7, Array.set_val_eq, hsl5]
+    rfl
+  clear hx6 hy6 hy6v hz6 hb6 hs7 hsl5
+  -- byte 7 (limb 1 >> 5)
+  step as ⟨x7, hx7⟩
+  rw [hv1] at hx7
+  step as ⟨b7, hb7⟩
+  have hb7v : b7.val = i24.val / 2^5 % 2^8 := by
+    rw [hb7, UScalar.cast_val_eq, hx7, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s8, hs8⟩
+  have hsl7 : (↑s8 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs8, Array.set_val_eq, hsl6]
+    rfl
+  clear hx7 hb7 hs8 hsl6
+  -- byte 8 (limb 1 >> 13)
+  step as ⟨x8, hx8⟩
+  rw [hv1] at hx8
+  step as ⟨b8, hb8⟩
+  have hb8v : b8.val = i24.val / 2^13 % 2^8 := by
+    rw [hb8, UScalar.cast_val_eq, hx8, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s9, hs9⟩
+  have hsl8 : (↑s9 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs9, Array.set_val_eq, hsl7]
+    rfl
+  clear hx8 hb8 hs9 hsl7
+  -- byte 9 (limb 1 >> 21)
+  step as ⟨x9, hx9⟩
+  rw [hv1] at hx9
+  step as ⟨b9, hb9⟩
+  have hb9v : b9.val = i24.val / 2^21 % 2^8 := by
+    rw [hb9, UScalar.cast_val_eq, hx9, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s10, hs10⟩
+  have hsl9 : (↑s10 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs10, Array.set_val_eq, hsl8]
+    rfl
+  clear hx9 hb9 hs10 hsl8
+  -- byte 10 (limb 1 >> 29)
+  step as ⟨x10, hx10⟩
+  rw [hv1] at hx10
+  step as ⟨b10, hb10⟩
+  have hb10v : b10.val = i24.val / 2^29 % 2^8 := by
+    rw [hb10, UScalar.cast_val_eq, hx10, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s11, hs11⟩
+  have hsl10 : (↑s11 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs11, Array.set_val_eq, hsl9]
+    rfl
+  clear hx10 hb10 hs11 hsl9
+  -- byte 11 (limb 1 >> 37)
+  step as ⟨x11, hx11⟩
+  rw [hv1] at hx11
+  step as ⟨b11, hb11⟩
+  have hb11v : b11.val = i24.val / 2^37 % 2^8 := by
+    rw [hb11, UScalar.cast_val_eq, hx11, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s12, hs12⟩
+  have hsl11 : (↑s12 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs12, Array.set_val_eq, hsl10]
+    rfl
+  clear hx11 hb11 hs12 hsl10
+  -- byte 12 (boundary: limb 1 >> 45  |  limb 2 << 6)
+  step as ⟨x12, hx12⟩
+  rw [hv1] at hx12
+  step as ⟨v2, hv2⟩
+  simp [hll9] at hv2
+  step as ⟨y12, hy12⟩
+  rw [hv2] at hy12
+  have hy12v : y12.val = i30.val * 2^6 := by
+    rw [hy12]
+    simp only [Nat.shiftLeft_eq]
+    rw [Nat.mod_eq_of_lt (show i30.val * 2^6 < U64.size by scalar_tac)]
+  step as ⟨z12, hz12⟩
+  step as ⟨b12, hb12⟩
+  have hb12v : b12.val = i24.val / 2^45 + (i30.val % 2^2) * 2^6 := by
+    rw [hb12, UScalar.cast_val_eq]
+    norm_num [UScalarTy.numBits]
+    rw [hz12, UScalar.val_or, hx12, nat_shr, hy12v]
+    have hxlt : i24.val / 2^45 < 2^6 := by omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := i24.val / 2^45) (i := 6) hxlt (i30.val)
+    have hadd : i24.val / 2^45 ||| i30.val * 2^6 = i24.val / 2^45 + i30.val * 2^6 := by
+      calc i24.val / 2^45 ||| i30.val * 2^6
+          = i24.val / 2^45 ||| 2^6 * i30.val := by rw [Nat.mul_comm]
+        _ = 2^6 * i30.val ||| i24.val / 2^45 := Nat.lor_comm _ _
+        _ = 2^6 * i30.val + i24.val / 2^45 := hor.symm
+        _ = i24.val / 2^45 + i30.val * 2^6 := by ring
+    rw [hadd]
+    omega
+  step as ⟨s13, hs13⟩
+  have hsl12 : (↑s13 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs13, Array.set_val_eq, hsl11]
+    rfl
+  clear hx12 hy12 hy12v hz12 hb12 hs13 hsl11
+  -- byte 13 (limb 2 >> 2)
+  step as ⟨x13, hx13⟩
+  rw [hv2] at hx13
+  step as ⟨b13, hb13⟩
+  have hb13v : b13.val = i30.val / 2^2 % 2^8 := by
+    rw [hb13, UScalar.cast_val_eq, hx13, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s14, hs14⟩
+  have hsl13 : (↑s14 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs14, Array.set_val_eq, hsl12]
+    rfl
+  clear hx13 hb13 hs14 hsl12
+  -- byte 14 (limb 2 >> 10)
+  step as ⟨x14, hx14⟩
+  rw [hv2] at hx14
+  step as ⟨b14, hb14⟩
+  have hb14v : b14.val = i30.val / 2^10 % 2^8 := by
+    rw [hb14, UScalar.cast_val_eq, hx14, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s15, hs15⟩
+  have hsl14 : (↑s15 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs15, Array.set_val_eq, hsl13]
+    rfl
+  clear hx14 hb14 hs15 hsl13
+  -- byte 15 (limb 2 >> 18)
+  step as ⟨x15, hx15⟩
+  rw [hv2] at hx15
+  step as ⟨b15, hb15⟩
+  have hb15v : b15.val = i30.val / 2^18 % 2^8 := by
+    rw [hb15, UScalar.cast_val_eq, hx15, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s16, hs16⟩
+  have hsl15 : (↑s16 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs16, Array.set_val_eq, hsl14]
+    rfl
+  clear hx15 hb15 hs16 hsl14
+  -- byte 16 (limb 2 >> 26)
+  step as ⟨x16, hx16⟩
+  rw [hv2] at hx16
+  step as ⟨b16, hb16⟩
+  have hb16v : b16.val = i30.val / 2^26 % 2^8 := by
+    rw [hb16, UScalar.cast_val_eq, hx16, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s17, hs17⟩
+  have hsl16 : (↑s17 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs17, Array.set_val_eq, hsl15]
+    rfl
+  clear hx16 hb16 hs17 hsl15
+  -- byte 17 (limb 2 >> 34)
+  step as ⟨x17, hx17⟩
+  rw [hv2] at hx17
+  step as ⟨b17, hb17⟩
+  have hb17v : b17.val = i30.val / 2^34 % 2^8 := by
+    rw [hb17, UScalar.cast_val_eq, hx17, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s18, hs18⟩
+  have hsl17 : (↑s18 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs18, Array.set_val_eq, hsl16]
+    rfl
+  clear hx17 hb17 hs18 hsl16
+  -- byte 18 (limb 2 >> 42)
+  step as ⟨x18, hx18⟩
+  rw [hv2] at hx18
+  step as ⟨b18, hb18⟩
+  have hb18v : b18.val = i30.val / 2^42 % 2^8 := by
+    rw [hb18, UScalar.cast_val_eq, hx18, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s19, hs19⟩
+  have hsl18 : (↑s19 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs19, Array.set_val_eq, hsl17]
+    rfl
+  clear hx18 hb18 hs19 hsl17
+  -- byte 19 (boundary: limb 2 >> 50  |  limb 3 << 1)
+  step as ⟨x19, hx19⟩
+  rw [hv2] at hx19
+  step as ⟨v3, hv3⟩
+  simp [hll9] at hv3
+  step as ⟨y19, hy19⟩
+  rw [hv3] at hy19
+  have hy19v : y19.val = i36.val * 2^1 := by
+    rw [hy19]
+    simp only [Nat.shiftLeft_eq]
+    rw [Nat.mod_eq_of_lt (show i36.val * 2^1 < U64.size by scalar_tac)]
+  step as ⟨z19, hz19⟩
+  step as ⟨b19, hb19⟩
+  have hb19v : b19.val = i30.val / 2^50 + (i36.val % 2^7) * 2^1 := by
+    rw [hb19, UScalar.cast_val_eq]
+    norm_num [UScalarTy.numBits]
+    rw [hz19, UScalar.val_or, hx19, nat_shr, hy19v]
+    have hxlt : i30.val / 2^50 < 2^1 := by omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := i30.val / 2^50) (i := 1) hxlt (i36.val)
+    have hadd : i30.val / 2^50 ||| i36.val * 2^1 = i30.val / 2^50 + i36.val * 2^1 := by
+      calc i30.val / 2^50 ||| i36.val * 2^1
+          = i30.val / 2^50 ||| 2^1 * i36.val := by rw [Nat.mul_comm]
+        _ = 2^1 * i36.val ||| i30.val / 2^50 := Nat.lor_comm _ _
+        _ = 2^1 * i36.val + i30.val / 2^50 := hor.symm
+        _ = i30.val / 2^50 + i36.val * 2^1 := by ring
+    rw [hadd]
+    omega
+  step as ⟨s20, hs20⟩
+  have hsl19 : (↑s20 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs20, Array.set_val_eq, hsl18]
+    rfl
+  clear hx19 hy19 hy19v hz19 hb19 hs20 hsl18
+  -- byte 20 (limb 3 >> 7)
+  step as ⟨x20, hx20⟩
+  rw [hv3] at hx20
+  step as ⟨b20, hb20⟩
+  have hb20v : b20.val = i36.val / 2^7 % 2^8 := by
+    rw [hb20, UScalar.cast_val_eq, hx20, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s21, hs21⟩
+  have hsl20 : (↑s21 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs21, Array.set_val_eq, hsl19]
+    rfl
+  clear hx20 hb20 hs21 hsl19
+  -- byte 21 (limb 3 >> 15)
+  step as ⟨x21, hx21⟩
+  rw [hv3] at hx21
+  step as ⟨b21, hb21⟩
+  have hb21v : b21.val = i36.val / 2^15 % 2^8 := by
+    rw [hb21, UScalar.cast_val_eq, hx21, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s22, hs22⟩
+  have hsl21 : (↑s22 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs22, Array.set_val_eq, hsl20]
+    rfl
+  clear hx21 hb21 hs22 hsl20
+  -- byte 22 (limb 3 >> 23)
+  step as ⟨x22, hx22⟩
+  rw [hv3] at hx22
+  step as ⟨b22, hb22⟩
+  have hb22v : b22.val = i36.val / 2^23 % 2^8 := by
+    rw [hb22, UScalar.cast_val_eq, hx22, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s23, hs23⟩
+  have hsl22 : (↑s23 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs23, Array.set_val_eq, hsl21]
+    rfl
+  clear hx22 hb22 hs23 hsl21
+  -- byte 23 (limb 3 >> 31)
+  step as ⟨x23, hx23⟩
+  rw [hv3] at hx23
+  step as ⟨b23, hb23⟩
+  have hb23v : b23.val = i36.val / 2^31 % 2^8 := by
+    rw [hb23, UScalar.cast_val_eq, hx23, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s24, hs24⟩
+  have hsl23 : (↑s24 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs24, Array.set_val_eq, hsl22]
+    rfl
+  clear hx23 hb23 hs24 hsl22
+  -- byte 24 (limb 3 >> 39)
+  step as ⟨x24, hx24⟩
+  rw [hv3] at hx24
+  step as ⟨b24, hb24⟩
+  have hb24v : b24.val = i36.val / 2^39 % 2^8 := by
+    rw [hb24, UScalar.cast_val_eq, hx24, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s25, hs25⟩
+  have hsl24 : (↑s25 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs25, Array.set_val_eq, hsl23]
+    rfl
+  clear hx24 hb24 hs25 hsl23
+  -- byte 25 (boundary: limb 3 >> 47  |  limb 4 << 4)
+  step as ⟨x25, hx25⟩
+  rw [hv3] at hx25
+  step as ⟨v4, hv4⟩
+  simp [hll9] at hv4
+  step as ⟨y25, hy25⟩
+  rw [hv4] at hy25
+  have hy25v : y25.val = i38.val * 2^4 := by
+    rw [hy25]
+    simp only [Nat.shiftLeft_eq]
+    rw [Nat.mod_eq_of_lt (show i38.val * 2^4 < U64.size by scalar_tac)]
+  step as ⟨z25, hz25⟩
+  step as ⟨b25, hb25⟩
+  have hb25v : b25.val = i36.val / 2^47 + (i38.val % 2^4) * 2^4 := by
+    rw [hb25, UScalar.cast_val_eq]
+    norm_num [UScalarTy.numBits]
+    rw [hz25, UScalar.val_or, hx25, nat_shr, hy25v]
+    have hxlt : i36.val / 2^47 < 2^4 := by omega
+    have hor := Nat.two_pow_add_eq_or_of_lt (b := i36.val / 2^47) (i := 4) hxlt (i38.val)
+    have hadd : i36.val / 2^47 ||| i38.val * 2^4 = i36.val / 2^47 + i38.val * 2^4 := by
+      calc i36.val / 2^47 ||| i38.val * 2^4
+          = i36.val / 2^47 ||| 2^4 * i38.val := by rw [Nat.mul_comm]
+        _ = 2^4 * i38.val ||| i36.val / 2^47 := Nat.lor_comm _ _
+        _ = 2^4 * i38.val + i36.val / 2^47 := hor.symm
+        _ = i36.val / 2^47 + i38.val * 2^4 := by ring
+    rw [hadd]
+    omega
+  step as ⟨s26, hs26⟩
+  have hsl25 : (↑s26 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs26, Array.set_val_eq, hsl24]
+    rfl
+  clear hx25 hy25 hy25v hz25 hb25 hs26 hsl24
+  -- byte 26 (limb 4 >> 4)
+  step as ⟨x26, hx26⟩
+  rw [hv4] at hx26
+  step as ⟨b26, hb26⟩
+  have hb26v : b26.val = i38.val / 2^4 % 2^8 := by
+    rw [hb26, UScalar.cast_val_eq, hx26, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s27, hs27⟩
+  have hsl26 : (↑s27 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs27, Array.set_val_eq, hsl25]
+    rfl
+  clear hx26 hb26 hs27 hsl25
+  -- byte 27 (limb 4 >> 12)
+  step as ⟨x27, hx27⟩
+  rw [hv4] at hx27
+  step as ⟨b27, hb27⟩
+  have hb27v : b27.val = i38.val / 2^12 % 2^8 := by
+    rw [hb27, UScalar.cast_val_eq, hx27, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s28, hs28⟩
+  have hsl27 : (↑s28 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, 0#u8, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs28, Array.set_val_eq, hsl26]
+    rfl
+  clear hx27 hb27 hs28 hsl26
+  -- byte 28 (limb 4 >> 20)
+  step as ⟨x28, hx28⟩
+  rw [hv4] at hx28
+  step as ⟨b28, hb28⟩
+  have hb28v : b28.val = i38.val / 2^20 % 2^8 := by
+    rw [hb28, UScalar.cast_val_eq, hx28, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s29, hs29⟩
+  have hsl28 : (↑s29 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, 0#u8, 0#u8, 0#u8] := by
+    simp only [hs29, Array.set_val_eq, hsl27]
+    rfl
+  clear hx28 hb28 hs29 hsl27
+  -- byte 29 (limb 4 >> 28)
+  step as ⟨x29, hx29⟩
+  rw [hv4] at hx29
+  step as ⟨b29, hb29⟩
+  have hb29v : b29.val = i38.val / 2^28 % 2^8 := by
+    rw [hb29, UScalar.cast_val_eq, hx29, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s30, hs30⟩
+  have hsl29 : (↑s30 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, 0#u8, 0#u8] := by
+    simp only [hs30, Array.set_val_eq, hsl28]
+    rfl
+  clear hx29 hb29 hs30 hsl28
+  -- byte 30 (limb 4 >> 36)
+  step as ⟨x30, hx30⟩
+  rw [hv4] at hx30
+  step as ⟨b30, hb30⟩
+  have hb30v : b30.val = i38.val / 2^36 % 2^8 := by
+    rw [hb30, UScalar.cast_val_eq, hx30, nat_shr]
+    norm_num [UScalarTy.numBits]
+  step as ⟨s31, hs31⟩
+  have hsl30 : (↑s31 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, 0#u8] := by
+    simp only [hs31, Array.set_val_eq, hsl29]
+    rfl
+  clear hx30 hb30 hs31 hsl29
+  -- byte 31 (limb 4 >> 44)
+  step as ⟨x31, hx31⟩
+  rw [hv4] at hx31
+  step as ⟨b31, hb31⟩
+  have hb31v : b31.val = i38.val / 2^44 := by
+    rw [hb31, UScalar.cast_val_eq, hx31, nat_shr]
+    norm_num [UScalarTy.numBits]
+    omega
+  step as ⟨s32, hs32⟩
+  have hsl31 : (↑s32 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31] := by
+    simp only [hs32, Array.set_val_eq, hsl30]
+    rfl
+  clear hx31 hb31 hs32 hsl30
+  -- ── the trailing debug-assert: the top bit of byte 31 is clear ───────────
+  step as ⟨t115, ht115⟩
+  simp [hsl31] at ht115
+  step as ⟨t116, ht116⟩
+  rw [ht115] at ht116
+  have hb31lt : b31.val < 2^7 := by
+    rw [hb31v]; omega
+  have ht116z : t116 = 0#u8 := by
+    have hval : t116.val = 0 := by
+      rw [ht116, UScalar.val_and]
+      have h128 : (128#u8).val = 2^7 := by norm_num
+      rw [h128, Nat.and_two_pow]
+      have htb : b31.val.testBit 7 = false := Nat.testBit_lt_two_pow hb31lt
+      rw [htb]
+      simp
+    scalar_tac
+  rw [ht116z]
+  step
+  try simp only [spec_ok]
+  -- ── assembly: bytes → limbs → mod-2²⁵⁵ → mod-p ──────────────────────────
+  have hsum : bytesVal s32 =
+      i18.val + i24.val * 2^51 + i30.val * 2^102 + i36.val * 2^153 + i38.val * 2^204 := by
+    simp only [bytesVal, hsl31]
+    rw [hb0v, hb1v, hb2v, hb3v, hb4v, hb5v, hb6v, hb7v, hb8v, hb9v, hb10v,
+        hb11v, hb12v, hb13v, hb14v, hb15v, hb16v, hb17v, hb18v, hb19v, hb20v,
+        hb21v, hb22v, hb23v, hb24v, hb25v, hb26v, hb27v, hb28v, hb29v, hb30v,
+        hb31v]
+    exact bytes_pack i18.val i24.val i30.val i36.val i38.val
+      hf0lt hf1lt hf2lt hf3lt hf4lt
+  have hmod255 : i18.val + i24.val * 2^51 + i30.val * 2^102 + i36.val * 2^153 + i38.val * 2^204
+      = (i11.val + m1.val * 2^51 + m2.val * 2^102 + m3.val * 2^153 + m4.val * 2^204) % 2^255 := by
+    rw [hf0v, hf1v, hf2v, hf3v, hf4v]
+    exact carry_pack i11.val m1.val m2.val m3.val m4.val
+  have hmodp : (i11.val + m1.val * 2^51 + m2.val * 2^102 + m3.val * 2^153 + m4.val * 2^204) % 2^255
+      = limbsVal m0 m1 m2 m3 m4 % P := by
+    have hre : i11.val + m1.val * 2^51 + m2.val * 2^102 + m3.val * 2^153 + m4.val * 2^204
+        = limbsVal m0 m1 m2 m3 m4 + 19 * ((limbsVal m0 m1 m2 m3 m4 + 19) / 2^255) := by
+      rw [hi11v, hq4v]
+      unfold limbsVal
+      ring
+    rw [hre]
+    exact q_mod_p _ hh2p
+  have hfe_a : feVal a % P = limbsVal m0 m1 m2 m3 m4 % P := by
+    rw [← hval]
+    rw [Nat.add_mul_mod_self_left]
+  rw [hsum, hmod255, hmodp, hfe_a]
+
+end CurveFieldProofs
diff --git a/verification/check.sh b/verification/check.sh
index bd3b853..80d9e71 100755
--- a/verification/check.sh
+++ b/verification/check.sh
@@ -63,7 +63,12 @@ PROOFS=(
   DsmNafLoopSpec
   DsmNafSpec
   DsmMulSpec
+  ToBytesMath
+  ToBytesSpec
+  ScalarPackSpec
+  CompressSpec
   SigApexSpec
+  PointLiftSpec
 )
 # Fully-qualified certificate names; each must be axiom-clean.
 CERTS=(
@@ -83,6 +88,10 @@ CERTS=(
   CurveFieldProofs.run_basepoint
   CurveFieldProofs.vartime_double_base_mul_spec
   CurveFieldProofs.verify_loop_full
+  CurveFieldProofs.to_bytes_spec
+  CurveFieldProofs.ed_compress_spec
+  ScalarProofs.from_bytes_mod_order_wide_spec
+  CurveFieldProofs.vartime_dsm_basepoint_spec
 )
 # Imports needed so every certificate in CERTS is in scope for the audit.
 AUDIT_IMPORTS=(
@@ -94,6 +103,10 @@ AUDIT_IMPORTS=(
   Proofs.DsmNafSpec
   Proofs.DsmMulSpec
   Proofs.SigApexSpec
+  Proofs.ToBytesSpec
+  Proofs.CompressSpec
+  Proofs.ScalarPackSpec
+  Proofs.PointLiftSpec
 )
 
 # ── Phase 0: resource + integrity guards ────────────────────────────────────
@@ -185,12 +198,13 @@ lake env bash -c "
   cd '$HERE'
   ALLOWED='[propext, Classical.choice, Quot.sound, ed25519.Signature, verifying.sha512_hash3, ed25519.Signature.to_bytes, signature.error.Error, signature.error.Error.new]'
   AUD=\$(mktemp '$HERE/.apex-XXXX.lean')
-  { echo 'import Proofs.SigApexSpec'; echo '#print axioms CurveFieldProofs.verify_accepts_iff'; } > \"\$AUD\"
+  { echo 'import Proofs.SigApexSpec'; echo 'import Proofs.PointLiftSpec'; echo '#print axioms CurveFieldProofs.verify_accepts_iff'; echo '#print axioms CurveFieldProofs.verify_accepts_iff_point'; } > \"\$AUD\"
   OUT=\$(LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1)
   echo \"\$OUT\"
   rm -f \"\$AUD\"
   FLAT=\$(echo \"\$OUT\" | tr '\\n' ' ' | tr -s ' ')
-  if echo \"\$FLAT\" | grep -qF \"depends on axioms: \$ALLOWED\"; then
+  if echo \"\$FLAT\" | grep -qF \"'CurveFieldProofs.verify_accepts_iff' depends on axioms: \$ALLOWED\" \
+     && echo \"\$FLAT\" | grep -qF \"'CurveFieldProofs.verify_accepts_iff_point' depends on axioms: \$ALLOWED\"; then
     echo '  apex axiom cone = exactly the SHA-512 + wire-format boundary (no curve/scalar/backend axioms)'
   else
     echo 'APEX AUDIT FAILED: verify_accepts_iff cone is not the documented boundary'; exit 1