(** Ed25519 signature verification — pure OCaml, WASM-safe.

    RFC 8032 §5.1.7 cofactorless verify over edwards25519. Includes a
    minimal arbitrary-precision unsigned bignum (no Zarith / no deps)
    and twisted-Edwards extended-coordinate point arithmetic. Verify
    is total: malformed inputs return [false], never raise. SHA-512
    is reused from {!Sx_sha2}. Reference: RFC 8032, RFC 7748. *)

(* ---- Minimal bignum: int array, little-endian, base 2^26. ---- *)

let bits = 26
let base = 1 lsl bits
let mask = base - 1

type bn = int array  (* normalized: no high zero limbs, length >= 1 *)

let norm (a : bn) : bn =
  let n = ref (Array.length a) in
  while !n > 1 && a.(!n - 1) = 0 do decr n done;
  if !n = Array.length a then a else Array.sub a 0 !n

let bzero : bn = [| 0 |]
let of_int n : bn =
  if n = 0 then bzero
  else begin
    let r = ref [] and n = ref n in
    while !n > 0 do r := (!n land mask) :: !r; n := !n lsr bits done;
    norm (Array.of_list (List.rev !r))
  end

let is_zero (a : bn) = Array.length a = 1 && a.(0) = 0

let cmp (a : bn) (b : bn) : int =
  let a = norm a and b = norm b in
  let la = Array.length a and lb = Array.length b in
  if la <> lb then compare la lb
  else begin
    let r = ref 0 and i = ref (la - 1) in
    while !r = 0 && !i >= 0 do
      if a.(!i) <> b.(!i) then r := compare a.(!i) b.(!i);
      decr i
    done; !r
  end

let add (a : bn) (b : bn) : bn =
  let la = Array.length a and lb = Array.length b in
  let n = (max la lb) + 1 in
  let r = Array.make n 0 in
  let carry = ref 0 in
  for i = 0 to n - 1 do
    let s = !carry
            + (if i < la then a.(i) else 0)
            + (if i < lb then b.(i) else 0) in
    r.(i) <- s land mask; carry := s lsr bits
  done;
  norm r

(* a - b, requires a >= b *)
let sub (a : bn) (b : bn) : bn =
  let la = Array.length a and lb = Array.length b in
  let r = Array.make la 0 in
  let borrow = ref 0 in
  for i = 0 to la - 1 do
    let s = a.(i) - !borrow - (if i < lb then b.(i) else 0) in
    if s < 0 then (r.(i) <- s + base; borrow := 1)
    else (r.(i) <- s; borrow := 0)
  done;
  norm r

let mul (a : bn) (b : bn) : bn =
  let la = Array.length a and lb = Array.length b in
  let r = Array.make (la + lb) 0 in
  for i = 0 to la - 1 do
    let carry = ref 0 in
    for j = 0 to lb - 1 do
      let s = r.(i + j) + a.(i) * b.(j) + !carry in
      r.(i + j) <- s land mask; carry := s lsr bits
    done;
    r.(i + lb) <- r.(i + lb) + !carry
  done;
  norm r

let numbits (a : bn) : int =
  let a = norm a in
  let hi = Array.length a - 1 in
  if hi = 0 && a.(0) = 0 then 0
  else begin
    let b = ref 0 and v = ref a.(hi) in
    while !v > 0 do incr b; v := !v lsr 1 done;
    hi * bits + !b
  end

let bit (a : bn) (i : int) : int =
  let limb = i / bits and off = i mod bits in
  if limb >= Array.length a then 0 else (a.(limb) lsr off) land 1

(* r = a mod m  (m > 0), binary long division. *)
let bn_mod (a : bn) (m : bn) : bn =
  if cmp a m < 0 then norm a
  else begin
    let r = ref bzero in
    for i = numbits a - 1 downto 0 do
      (* r = r*2 + bit *)
      r := add !r !r;
      if bit a i = 1 then r := add !r [| 1 |];
      if cmp !r m >= 0 then r := sub !r m
    done;
    !r
  end

let div_small (a : bn) (d : int) : bn =
  let la = Array.length a in
  let q = Array.make la 0 in
  let rem = ref 0 in
  for i = la - 1 downto 0 do
    let cur = (!rem lsl bits) lor a.(i) in
    q.(i) <- cur / d; rem := cur mod d
  done;
  norm q

let powmod (b0 : bn) (e : bn) (m : bn) : bn =
  let result = ref [| 1 |] and b = ref (bn_mod b0 m) in
  let nb = numbits e in
  for i = 0 to nb - 1 do
    if bit e i = 1 then result := bn_mod (mul !result !b) m;
    b := bn_mod (mul !b !b) m
  done;
  !result

let of_bytes_le (s : string) : bn =
  let acc = ref bzero in
  for i = String.length s - 1 downto 0 do
    acc := add (mul !acc (of_int 256)) (of_int (Char.code s.[i]))
  done;
  !acc

let to_bytes_le (a : bn) (n : int) : string =
  let b = Bytes.make n '\000' in
  let cur = ref (norm a) in
  for i = 0 to n - 1 do
    let q = div_small !cur 256 in
    let r =
      let qm = mul q (of_int 256) in
      let d = sub !cur qm in
      if is_zero d then 0 else d.(0)
    in
    Bytes.set b i (Char.chr r);
    cur := q
  done;
  Bytes.unsafe_to_string b

(* ---- Field GF(p), p = 2^255 - 19 ---- *)

let p =
  let twop255 = Array.make 11 0 in   (* 11*26 = 286 > 255 *)
  let limb = 255 / bits and off = 255 mod bits in
  twop255.(limb) <- 1 lsl off;
  sub (norm twop255) (of_int 19)

let fmod a = bn_mod a p
let fadd a b = fmod (add a b)
let fsub a b = fmod (add a (sub p (fmod b)))
let fmul a b = fmod (mul a b)
let fpow a e = powmod a e p
let finv a = fpow a (sub p (of_int 2))   (* Fermat: a^(p-2) *)

(* group order L = 2^252 + 27742317777372353535851937790883648493 *)
let ell =
  of_bytes_le
    "\xed\xd3\xf5\x5c\x1a\x63\x12\x58\xd6\x9c\xf7\xa2\xde\xf9\xde\x14\
     \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10"

(* d = -121665 / 121666 mod p *)
let dconst =
  let inv666 = finv (of_int 121666) in
  fmod (mul (fsub (of_int 0) (of_int 121665)) inv666)

(* sqrt(-1) = 2^((p-1)/4) mod p *)
let sqrtm1 = fpow (of_int 2) (div_small (sub p (of_int 1)) 4)

(* ---- edwards25519 points in extended coords (X,Y,Z,T) ---- *)

type pt = { x : bn; y : bn; z : bn; t : bn }

let identity = { x = bzero; y = of_int 1; z = of_int 1; t = bzero }

(* add-2008-hwcd-3, complete for a = -1 on ed25519 *)
let padd (p1 : pt) (p2 : pt) : pt =
  let a = fmul (fsub p1.y p1.x) (fsub p2.y p2.x) in
  let b = fmul (fadd p1.y p1.x) (fadd p2.y p2.x) in
  let c = fmul (fmul p1.t (fmul (of_int 2) dconst)) p2.t in
  let dd = fmul (fmul p1.z (of_int 2)) p2.z in
  let e = fsub b a in
  let f = fsub dd c in
  let g = fadd dd c in
  let h = fadd b a in
  { x = fmul e f; y = fmul g h; t = fmul e h; z = fmul f g }

let scalar_mul (n : bn) (q : pt) : pt =
  let r = ref identity in
  for i = numbits n - 1 downto 0 do
    r := padd !r !r;
    if bit n i = 1 then r := padd !r q
  done;
  !r

let pnegate (q : pt) : pt =
  { q with x = fsub (of_int 0) q.x; t = fsub (of_int 0) q.t }

(* Decompress a 32-byte little-endian point encoding. *)
let decompress (s : string) : pt option =
  if String.length s <> 32 then None
  else begin
    let sign = (Char.code s.[31] lsr 7) land 1 in
    let s' = Bytes.of_string s in
    Bytes.set s' 31 (Char.chr (Char.code s.[31] land 0x7f));
    let y = of_bytes_le (Bytes.unsafe_to_string s') in
    if cmp y p >= 0 then None
    else begin
      let y2 = fmul y y in
      let u = fsub y2 (of_int 1) in
      let v = fadd (fmul dconst y2) (of_int 1) in
      (* x = u v^3 (u v^7)^((p-5)/8) *)
      let v3 = fmul (fmul v v) v in
      let v7 = fmul (fmul v3 v3) v in
      let exp = div_small (sub p (of_int 5)) 8 in
      let x0 = fmul (fmul u v3) (fpow (fmul u v7) exp) in
      let vx2 = fmul v (fmul x0 x0) in
      let x =
        if cmp vx2 u = 0 then Some x0
        else if cmp vx2 (fsub (of_int 0) u) = 0 then Some (fmul x0 sqrtm1)
        else None
      in
      match x with
      | None -> None
      | Some x ->
        if is_zero x && sign = 1 then None
        else begin
          let x = if (bit x 0) <> sign then fsub (of_int 0) x else x in
          Some { x; y; z = of_int 1; t = fmul x y }
        end
    end
  end

(* Encode a point to 32-byte little-endian (y with x-parity bit). *)
let encode (q : pt) : string =
  let zi = finv q.z in
  let x = fmul q.x zi and y = fmul q.y zi in
  let b = Bytes.of_string (to_bytes_le y 32) in
  let last = Char.code (Bytes.get b 31) lor ((bit x 0) lsl 7) in
  Bytes.set b 31 (Char.chr last);
  Bytes.unsafe_to_string b

(* base point: y = 4/5 mod p, x even (sign 0). *)
let base_point =
  let by = fmul (of_int 4) (finv (of_int 5)) in
  match decompress (to_bytes_le by 32) with
  | Some pt -> pt
  | None -> failwith "ed25519: base point decompress failed"

let unhex (h : string) : string =
  let n = String.length h / 2 in
  let b = Bytes.create n in
  for i = 0 to n - 1 do
    Bytes.set b i
      (Char.chr (int_of_string ("0x" ^ String.sub h (2 * i) 2)))
  done;
  Bytes.unsafe_to_string b

let sha512_bytes s = unhex (Sx_sha2.sha512_hex s)

(* RFC 8032 §5.1.7 cofactorless: encode([S]B - [k]A) == R. *)
let verify ~pubkey ~msg ~sig_ : bool =
  if String.length pubkey <> 32 || String.length sig_ <> 64 then false
  else
    let rb = String.sub sig_ 0 32 in
    let sb = String.sub sig_ 32 32 in
    let s = of_bytes_le sb in
    if cmp s ell >= 0 then false
    else
      match decompress pubkey with
      | None -> false
      | Some a ->
        let h = sha512_bytes (rb ^ pubkey ^ msg) in
        let k = bn_mod (of_bytes_le h) ell in
        let sb_pt = scalar_mul s base_point in
        let ka = scalar_mul k a in
        let chk = padd sb_pt (pnegate ka) in
        (try encode chk = rb with _ -> false)