/- ──────────────────────────────────────────────────────────────────────────────
   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)

end CurveFieldProofs
