diff --git a/hosts/ocaml/bin/run_tests.ml b/hosts/ocaml/bin/run_tests.ml index 14ecb408..ea4736c7 100644 --- a/hosts/ocaml/bin/run_tests.ml +++ b/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; diff --git a/hosts/ocaml/lib/sx_ed25519.ml b/hosts/ocaml/lib/sx_ed25519.ml new file mode 100644 index 00000000..0b7a42bc --- /dev/null +++ b/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) diff --git a/hosts/ocaml/lib/sx_primitives.ml b/hosts/ocaml/lib/sx_primitives.ml index a05643d4..bf05f806 100644 --- a/hosts/ocaml/lib/sx_primitives.ml +++ b/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) diff --git a/plans/fed-sx-host-primitives.md b/plans/fed-sx-host-primitives.md index 33a4c76d..04fe6d5e 100644 --- a/plans/fed-sx-host-primitives.md +++ b/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: