fed-prims: Phase F — RSA-SHA256 PKCS#1 v1.5 verify, pure OCaml, RSA-2048 vector

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

hosts/ocaml/bin/run_tests.ml

@@ -1467,6 +1467,25 @@ let run_foundation_tests () =
     (Bool false)
     (call "ed25519-verify" [Integer 1; Integer 2; Integer 3]);
 
+  Printf.printf "\nSuite: rsa-sha256\n";
+  (* Fixed RSA-2048 vector: one-off python-cryptography keygen +
+     PKCS1v15/SHA-256 sign of "fed-sx phase F rsa test". *)
+  let rhx = Sx_rsa.unhex in
+  let spki = rhx "30820122300d06092a864886f70d01010105000382010f003082010a0282010100a117b573480bce5a08b54a98384001df26d062e9173caaee2e3a2d0045c6d16f99b2a1e7fb60763f65f95f8c39ff82c18b8590338042914331db3440a06d2dbe65a2f82c82f37d293f67a8b57a1f9014b55150a093cfee90257ef3b4a215d5ab002579bd92b6fcb3536777d51b639347d01e307ddafb209073dd9b8d6a507157c44c624a19b3b9275931472462870ae02132630159132a85c1c889adfb358b6bbd3760ce3fffe6285964833a10ee436d5bc33dfab7f9ed630a74e9a32e5688f5a7797f7cc839ad2494dd1c4c4a8fab844cd26208794bf2602c16b9d12bde434066d8c0dd2d20489f4070f883bae2b4508ead4a1b80b44c576e9e37bdb5df69f10203010001" in
+  let rmsg = rhx "6665642d73782070686173652046207273612074657374" in
+  let rsig = rhx "5e1593d674ed15c0172546d38efdf1aebd252f4b0c0dfbe1f7996fd569d0bfd9f3e8689ea2b14aa45b5fc3f0a05d4f23c6b02b8820d71f6998ea3b5b0d071bb33142236e388b1226ece3ec447d33b38999f189c37564cf052cf038de94c67b2ddf9a97d5a73554bb88818f615824517209a4083258965adace55658f344104eaa0d5f2f44ea00cfac8754674aade87b40d955cccd1ccd9b7649a08b66ce3bc5dba2de96b3e859488ded3ef9fb3744a1e3495fd14841d8319b3cc08054c729d1c02739ee314eba2b20fac46e463f47eb67183d8455583eca73ba37448164612dd9cd77877135d30d12084c2843f986a5b8ad59c6600f9855b91d7cbdf7c6c4b0e" in
+  let rsav s m g = call "rsa-sha256-verify" [String s; String m; String g] in
+  assert_eq "rsa valid" (Bool true) (rsav spki rmsg rsig);
+  assert_eq "rsa tampered msg" (Bool false)
+    (rsav spki (rmsg ^ "x") rsig);
+  assert_eq "rsa tampered sig" (Bool false)
+    (rsav spki rmsg
+       (rhx "5f1593d674ed15c0172546d38efdf1aebd252f4b0c0dfbe1f7996fd569d0bfd9f3e8689ea2b14aa45b5fc3f0a05d4f23c6b02b8820d71f6998ea3b5b0d071bb33142236e388b1226ece3ec447d33b38999f189c37564cf052cf038de94c67b2ddf9a97d5a73554bb88818f615824517209a4083258965adace55658f344104eaa0d5f2f44ea00cfac8754674aade87b40d955cccd1ccd9b7649a08b66ce3bc5dba2de96b3e859488ded3ef9fb3744a1e3495fd14841d8319b3cc08054c729d1c02739ee314eba2b20fac46e463f47eb67183d8455583eca73ba37448164612dd9cd77877135d30d12084c2843f986a5b8ad59c6600f9855b91d7cbdf7c6c4b0e"));
+  assert_eq "rsa garbage spki" (Bool false)
+    (rsav "not der" rmsg rsig);
+  assert_eq "rsa non-string args" (Bool false)
+    (call "rsa-sha256-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_primitives.ml

@@ -4209,4 +4209,10 @@ let () =
     | [String pk; String msg; String sg] ->
       Bool (try Sx_ed25519.verify ~pubkey:pk ~msg ~sig_:sg
             with _ -> false)
+    | _ -> Bool false);
+
+  register "rsa-sha256-verify" (fun args ->
+    match args with
+    | [String spki; String msg; String sg] ->
+      Bool (try Sx_rsa.verify ~spki ~msg ~sig_:sg with _ -> false)
     | _ -> Bool false)

hosts/ocaml/lib/sx_rsa.ml

@@ -0,0 +1,220 @@
+(** RSASSA-PKCS1-v1_5 verification with SHA-256 — pure OCaml,
+    WASM-safe. Self-contained minimal bignum (modexp only), a tiny
+    DER reader for SubjectPublicKeyInfo, and the fixed SHA-256
+    DigestInfo prefix. Verify only on public data — constant time
+    not required. Reference: RFC 8017 §8.2.2, §9.2. No deps. *)
+
+(* ---- Minimal unsigned bignum: int array, little-endian, base 2^26 ---- *)
+
+let bits = 26
+let base = 1 lsl bits
+let mask = base - 1
+
+type bn = int array
+
+let norm a =
+  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 is_zero a = Array.length a = 1 && a.(0) = 0
+
+let cmp a b =
+  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 b =
+  let la = Array.length a and lb = Array.length b in
+  let n = (max la lb) + 1 in
+  let r = Array.make n 0 and 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
+
+let sub a b =                       (* requires a >= b *)
+  let la = Array.length a and lb = Array.length b in
+  let r = Array.make la 0 and 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 b =
+  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 =
+  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 i =
+  let limb = i / bits and off = i mod bits in
+  if limb >= Array.length a then 0 else (a.(limb) lsr off) land 1
+
+let bn_mod a m =                    (* binary long division, m > 0 *)
+  if cmp a m < 0 then norm a
+  else begin
+    let r = ref bzero in
+    for i = numbits a - 1 downto 0 do
+      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 powmod b0 e m =
+  let result = ref [| 1 |] and b = ref (bn_mod b0 m) in
+  for i = 0 to numbits e - 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_be (s : string) : bn =
+  let acc = ref bzero in
+  for i = 0 to String.length s - 1 do
+    acc := add (mul !acc [| 256 |]) [| Char.code s.[i] |]
+  done;
+  !acc
+
+let div_small a d =
+  let la = Array.length a in
+  let q = Array.make la 0 and 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 to_bytes_be (a : bn) (n : int) : string =
+  let b = Bytes.make n '\000' in
+  let cur = ref (norm a) in
+  for i = n - 1 downto 0 do
+    let q = div_small !cur 256 in
+    let r =
+      let d = sub !cur (mul q [| 256 |]) 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
+
+(* ---- Minimal DER reader (for SubjectPublicKeyInfo) ---- *)
+
+exception Der of string
+
+(* Returns (tag, content_start, content_len, next). *)
+let der_tlv s pos =
+  if pos + 2 > String.length s then raise (Der "short");
+  let tag = Char.code s.[pos] in
+  let l0 = Char.code s.[pos + 1] in
+  let len, hdr =
+    if l0 < 0x80 then l0, 2
+    else begin
+      let nb = l0 land 0x7f in
+      if pos + 2 + nb > String.length s then raise (Der "short len");
+      let v = ref 0 in
+      for i = 0 to nb - 1 do
+        v := (!v lsl 8) lor Char.code s.[pos + 2 + i]
+      done;
+      !v, 2 + nb
+    end
+  in
+  (tag, pos + hdr, len, pos + hdr + len)
+
+(* SPKI DER -> (n, e) as bignums. *)
+let parse_spki (der : string) : bn * bn =
+  let tag, c, _l, _ = der_tlv der 0 in
+  if tag <> 0x30 then raise (Der "spki: outer not SEQUENCE");
+  (* AlgorithmIdentifier SEQUENCE — skip. *)
+  let _, _, _, after_alg = der_tlv der c in
+  (* BIT STRING. *)
+  let bt, bc, bl, _ = der_tlv der after_alg in
+  if bt <> 0x03 then raise (Der "spki: expected BIT STRING");
+  (* First content byte = unused bits (must be 0). *)
+  let rpk_start = bc + 1 in
+  ignore bl;
+  let st, sc, _, _ = der_tlv der rpk_start in
+  if st <> 0x30 then raise (Der "spki: RSAPublicKey not SEQUENCE");
+  let nt, nc, nl, after_n = der_tlv der sc in
+  if nt <> 0x02 then raise (Der "spki: modulus not INTEGER");
+  let et, ec, el, _ = der_tlv der after_n in
+  if et <> 0x02 then raise (Der "spki: exponent not INTEGER");
+  let n = of_bytes_be (String.sub der nc nl) in
+  let e = of_bytes_be (String.sub der ec el) in
+  (n, e)
+
+(* SHA-256 DigestInfo DER prefix (RFC 8017 §9.2 note 1). *)
+let sha256_digestinfo_prefix =
+  "\x30\x31\x30\x0d\x06\x09\x60\x86\x48\x01\x65\x03\x04\x02\x01\x05\x00\x04\x20"
+
+let unhex h =
+  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
+
+(* RSASSA-PKCS1-v1_5 verify with SHA-256. Total: any malformed
+   input yields false (caller wraps, but be defensive here too). *)
+let verify ~spki ~msg ~sig_ : bool =
+  try
+    let n, e = parse_spki spki in
+    let k = (numbits n + 7) / 8 in
+    if String.length sig_ <> k then false
+    else begin
+      let s = of_bytes_be sig_ in
+      if cmp s n >= 0 then false
+      else begin
+        let m = powmod s e n in
+        let em = to_bytes_be m k in
+        (* EM = 0x00 01 FF..FF 00 || DigestInfo || H *)
+        let h = unhex (Sx_sha2.sha256_hex msg) in
+        let t = sha256_digestinfo_prefix ^ h in
+        let tlen = String.length t in
+        if k < tlen + 11 then false
+        else begin
+          let ok = ref (em.[0] = '\x00' && em.[1] = '\x01') in
+          let ps_end = k - tlen - 1 in
+          for i = 2 to ps_end - 1 do
+            if em.[i] <> '\xff' then ok := false
+          done;
+          if em.[ps_end] <> '\x00' then ok := false;
+          if String.sub em (ps_end + 1) tlen <> t then ok := false;
+          !ok
+        end
+      end
+    end
+  with _ -> false

plans/fed-sx-host-primitives.md

@@ -115,7 +115,7 @@ check** → tests → commit → tick box → Progress-log line → push.
 - **Acceptance:** all RFC 8032 vectors pass; WASM links. Satisfies fed-sx Step 2
   (Ed25519 sig-suite).
 
-### Phase F — RSA-SHA256 verify (PKCS#1 v1.5), pure OCaml
+### Phase F — RSA-SHA256 verify (PKCS#1 v1.5), pure OCaml ✅ DONE
 - Minimal pure-OCaml bignum (only need modexp + DER parse). Parse SPKI DER →
   (n, e). RSASSA-PKCS1-v1_5 verify with SHA-256 (Phase A).
 - Primitive `rsa-sha256-verify (der-spki msg sig) -> bool`.
@@ -205,6 +205,14 @@ printf '(epoch 1)\n(crypto-sha256 "abc")\n' | \
 
 _Newest first._
 
+- 2026-05-18 — Phase F: pure-OCaml `lib/sx_rsa.ml` (self-contained
+  bignum modexp, minimal DER SPKI reader, RFC 8017 §8.2.2 PKCS#1
+  v1.5 verify with SHA-256 DigestInfo prefix). Primitive
+  `rsa-sha256-verify` total. 5 tests on a fixed RSA-2048 vector
+  (one-off python-cryptography keygen, hardcoded): valid, tampered
+  msg/sig, garbage SPKI, non-string. WASM boot green with new lib
+  module; Erlang 530/530; run_tests +5. Satisfies fed-sx Step 2
+  (rsa-sha256-2018 sig-suite).
 - 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