fed-prims: Phase E — Ed25519 verify (RFC 8032), pure-OCaml bignum + edwards25519

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

hosts/ocaml/bin/run_tests.ml

@@ -1422,6 +1422,51 @@ let run_foundation_tests () =
            | String s -> String.length s > 1 && s.[0] = 'b'
            | _ -> false));
 
+  Printf.printf "\nSuite: ed25519\n";
+  let hx = Sx_ed25519.unhex in
+  let edv pk msg sg = call "ed25519-verify"
+      [String (hx pk); String (hx msg); String (hx sg)] in
+  (* RFC 8032 §7.1 TEST 1-3 (deterministic; re-derived independently). *)
+  assert_eq "ed25519 RFC T1"
+    (Bool true)
+    (edv "d75a980182b10ab7d54bfed3c964073a0ee172f3daa62325af021a68f707511a"
+         ""
+         "e5564300c360ac729086e2cc806e828a84877f1eb8e5d974d873e065224901555fb8821590a33bacc61e39701cf9b46bd25bf5f0595bbe24655141438e7a100b");
+  assert_eq "ed25519 RFC T2"
+    (Bool true)
+    (edv "3d4017c3e843895a92b70aa74d1b7ebc9c982ccf2ec4968cc0cd55f12af4660c"
+         "72"
+         "92a009a9f0d4cab8720e820b5f642540a2b27b5416503f8fb3762223ebdb69da085ac1e43e15996e458f3613d0f11d8c387b2eaeb4302aeeb00d291612bb0c00");
+  assert_eq "ed25519 RFC T3"
+    (Bool true)
+    (edv "fc51cd8e6218a1a38da47ed00230f0580816ed13ba3303ac5deb911548908025"
+         "af82"
+         "6291d657deec24024827e69c3abe01a30ce548a284743a445e3680d7db5ac3ac18ff9b538d16f290ae67f760984dc6594a7c15e9716ed28dc027beceea1ec40a");
+  (* Tampered message -> false. *)
+  assert_eq "ed25519 tampered msg"
+    (Bool false)
+    (edv "fc51cd8e6218a1a38da47ed00230f0580816ed13ba3303ac5deb911548908025"
+         "af83"
+         "6291d657deec24024827e69c3abe01a30ce548a284743a445e3680d7db5ac3ac18ff9b538d16f290ae67f760984dc6594a7c15e9716ed28dc027beceea1ec40a");
+  (* Tampered signature -> false. *)
+  assert_eq "ed25519 tampered sig"
+    (Bool false)
+    (edv "d75a980182b10ab7d54bfed3c964073a0ee172f3daa62325af021a68f707511a"
+         ""
+         "f5564300c360ac729086e2cc806e828a84877f1eb8e5d974d873e065224901555fb8821590a33bacc61e39701cf9b46bd25bf5f0595bbe24655141438e7a100b");
+  (* Total: wrong-length pubkey / sig -> false, no exception. *)
+  assert_eq "ed25519 short pubkey"
+    (Bool false)
+    (call "ed25519-verify" [String "abc"; String ""; String (String.make 64 '\000')]);
+  assert_eq "ed25519 short sig"
+    (Bool false)
+    (call "ed25519-verify"
+       [String (hx "d75a980182b10ab7d54bfed3c964073a0ee172f3daa62325af021a68f707511a");
+        String ""; String "short"]);
+  assert_eq "ed25519 non-string args"
+    (Bool false)
+    (call "ed25519-verify" [Integer 1; Integer 2; Integer 3]);
+
   Printf.printf "\nSuite: vm-extension-dispatch\n";
   let make_bc op = ({
     vc_arity = 0; vc_rest_arity = -1; vc_locals = 0;

hosts/ocaml/lib/sx_ed25519.ml

@@ -0,0 +1,289 @@
+(** 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)

hosts/ocaml/lib/sx_primitives.ml

@@ -4201,4 +4201,12 @@ let () =
     | [v] ->
       (try String (Sx_cid.cid_from_sx v)
        with Sx_cbor.Cbor_error m -> raise (Eval_error m))
-    | _ -> raise (Eval_error "cid-from-sx: (value)"))
+    | _ -> raise (Eval_error "cid-from-sx: (value)"));
+
+  (* Verify is total: any malformed input -> false, never raises. *)
+  register "ed25519-verify" (fun args ->
+    match args with
+    | [String pk; String msg; String sg] ->
+      Bool (try Sx_ed25519.verify ~pubkey:pk ~msg ~sig_:sg
+            with _ -> false)
+    | _ -> Bool false)

plans/fed-sx-host-primitives.md

@@ -105,7 +105,7 @@ check** → tests → commit → tick box → Progress-log line → push.
 - **Acceptance:** matches reference CIDs; determinism holds; WASM links. Satisfies
   fed-sx Milestone 1 Step 1.
 
-### Phase E — Ed25519 verify, pure OCaml
+### Phase E — Ed25519 verify, pure OCaml ✅ DONE
 - Curve25519/edwards25519 field arith (mod 2^255-19), point decompress,
   SHA-512-based verify per RFC 8032 §5.1.7. (Reuse Phase A sha512.)
 - Primitive `ed25519-verify (pubkey msg sig) -> bool`. Bad-length args → false,
@@ -205,6 +205,14 @@ printf '(epoch 1)\n(crypto-sha256 "abc")\n' | \
 
 _Newest first._
 
+- 2026-05-18 — Phase E: pure-OCaml `lib/sx_ed25519.ml` (minimal
+  base-2^26 bignum, edwards25519 extended-coord points, RFC 8032
+  §5.1.7 cofactorless verify reusing Phase-A sha512). Primitive
+  `ed25519-verify` is total (bad/short/non-string args → false).
+  8 tests: RFC 8032 §7.1 TEST 1-3 (re-derived independently via
+  python-cryptography), tampered msg/sig, wrong-length, non-string.
+  WASM boot green with new lib module; Erlang 530/530; run_tests +8.
+  Satisfies fed-sx Milestone 1 Step 2 (Ed25519 sig-suite).
 - 2026-05-18 — Phase D: pure-OCaml `lib/sx_cid.ml` (unsigned-varint,
   multihash, CIDv1, multibase base32-lower), primitives `cid-from-bytes`
   / `cid-from-sx` (cbor→sha2-256→mh→cidv1, dag-cbor codec 0x71). 5 tests: