From 19932a42a9bba3798c692b3a9c83b550f8641fd7 Mon Sep 17 00:00:00 2001 From: giles Date: Mon, 18 May 2026 15:17:35 +0000 Subject: [PATCH] =?UTF-8?q?fed-prims:=20Phase=20A=20=E2=80=94=20SHA-256=20?= =?UTF-8?q?+=20SHA-512,=20pure=20OCaml,=207=20NIST=20vectors?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 4.7 (1M context) --- hosts/ocaml/bin/run_tests.ml | 27 ++++ hosts/ocaml/lib/sx_primitives.ml | 13 +- hosts/ocaml/lib/sx_sha2.ml | 212 +++++++++++++++++++++++++++++++ plans/fed-sx-host-primitives.md | 7 +- 4 files changed, 256 insertions(+), 3 deletions(-) create mode 100644 hosts/ocaml/lib/sx_sha2.ml diff --git a/hosts/ocaml/bin/run_tests.ml b/hosts/ocaml/bin/run_tests.ml index 9689fa35..034caa90 100644 --- a/hosts/ocaml/bin/run_tests.ml +++ b/hosts/ocaml/bin/run_tests.ml @@ -1292,6 +1292,33 @@ let run_foundation_tests () = ignore (Sx_types.set_lambda_name (Lambda l) "my-fn"); assert_eq "lambda name mutated" (String "my-fn") (lambda_name (Lambda l)); + Printf.printf "\nSuite: crypto-sha2\n"; + (* NIST FIPS 180-4 published vectors. *) + assert_eq "sha256 empty" + (String "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855") + (call "crypto-sha256" [String ""]); + assert_eq "sha256 abc" + (String "ba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad") + (call "crypto-sha256" [String "abc"]); + assert_eq "sha256 896-bit" + (String "248d6a61d20638b8e5c026930c3e6039a33ce45964ff2167f6ecedd419db06c1") + (call "crypto-sha256" + [String "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq"]); + assert_eq "sha256 1M 'a'" + (String "cdc76e5c9914fb9281a1c7e284d73e67f1809a48a497200e046d39ccc7112cd0") + (call "crypto-sha256" [String (String.make 1000000 'a')]); + assert_eq "sha512 empty" + (String "cf83e1357eefb8bdf1542850d66d8007d620e4050b5715dc83f4a921d36ce9ce47d0d13c5d85f2b0ff8318d2877eec2f63b931bd47417a81a538327af927da3e") + (call "crypto-sha512" [String ""]); + assert_eq "sha512 abc" + (String "ddaf35a193617abacc417349ae20413112e6fa4e89a97ea20a9eeee64b55d39a2192992a274fc1a836ba3c23a3feebbd454d4423643ce80e2a9ac94fa54ca49f") + (call "crypto-sha512" [String "abc"]); + assert_eq "sha512 896-bit" + (String "8e959b75dae313da8cf4f72814fc143f8f7779c6eb9f7fa17299aeadb6889018501d289e4900f7e4331b99dec4b5433ac7d329eeb6dd26545e96e55b874be909") + (call "crypto-sha512" + [String ("abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmn" + ^ "hijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu")]); + 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_primitives.ml b/hosts/ocaml/lib/sx_primitives.ml index bd25563c..683a3d99 100644 --- a/hosts/ocaml/lib/sx_primitives.ml +++ b/hosts/ocaml/lib/sx_primitives.ml @@ -4158,4 +4158,15 @@ let () = Sx_types.jit_skipped_count := 0; Sx_types.jit_threshold_skipped_count := 0; Sx_types.jit_evicted_count := 0; - Nil) + Nil); + + (* fed-sx host primitives — pure-OCaml crypto (WASM-safe). *) + register "crypto-sha256" (fun args -> + match args with + | [String s] -> String (Sx_sha2.sha256_hex s) + | _ -> raise (Eval_error "crypto-sha256: (bytes)")); + + register "crypto-sha512" (fun args -> + match args with + | [String s] -> String (Sx_sha2.sha512_hex s) + | _ -> raise (Eval_error "crypto-sha512: (bytes)")) diff --git a/hosts/ocaml/lib/sx_sha2.ml b/hosts/ocaml/lib/sx_sha2.ml new file mode 100644 index 00000000..1ea6b8f8 --- /dev/null +++ b/hosts/ocaml/lib/sx_sha2.ml @@ -0,0 +1,212 @@ +(** SHA-2 (SHA-256, SHA-512) — pure OCaml, WASM-safe. + + No C stubs, no external deps. Used by the fed-sx host primitives + [crypto-sha256] / [crypto-sha512]. Reference: FIPS 180-4. *) + +(* ---- SHA-256 (FIPS 180-4 §6.2). 32-bit words held in native int, + masked to 32 bits after every arithmetic op. ---- *) + +let mask32 = 0xFFFFFFFF + +let k256 = [| + 0x428a2f98; 0x71374491; 0xb5c0fbcf; 0xe9b5dba5; + 0x3956c25b; 0x59f111f1; 0x923f82a4; 0xab1c5ed5; + 0xd807aa98; 0x12835b01; 0x243185be; 0x550c7dc3; + 0x72be5d74; 0x80deb1fe; 0x9bdc06a7; 0xc19bf174; + 0xe49b69c1; 0xefbe4786; 0x0fc19dc6; 0x240ca1cc; + 0x2de92c6f; 0x4a7484aa; 0x5cb0a9dc; 0x76f988da; + 0x983e5152; 0xa831c66d; 0xb00327c8; 0xbf597fc7; + 0xc6e00bf3; 0xd5a79147; 0x06ca6351; 0x14292967; + 0x27b70a85; 0x2e1b2138; 0x4d2c6dfc; 0x53380d13; + 0x650a7354; 0x766a0abb; 0x81c2c92e; 0x92722c85; + 0xa2bfe8a1; 0xa81a664b; 0xc24b8b70; 0xc76c51a3; + 0xd192e819; 0xd6990624; 0xf40e3585; 0x106aa070; + 0x19a4c116; 0x1e376c08; 0x2748774c; 0x34b0bcb5; + 0x391c0cb3; 0x4ed8aa4a; 0x5b9cca4f; 0x682e6ff3; + 0x748f82ee; 0x78a5636f; 0x84c87814; 0x8cc70208; + 0x90befffa; 0xa4506ceb; 0xbef9a3f7; 0xc67178f2 |] + +let rotr32 x n = ((x lsr n) lor (x lsl (32 - n))) land mask32 + +let sha256_hex (msg : string) : string = + let h = [| 0x6a09e667; 0xbb67ae85; 0x3c6ef372; 0xa54ff53a; + 0x510e527f; 0x9b05688c; 0x1f83d9ab; 0x5be0cd19 |] in + let len = String.length msg in + (* Padded length: multiple of 64 bytes. *) + let bitlen = len * 8 in + let padlen = + let r = (len + 1) mod 64 in + if r <= 56 then 56 - r else 120 - r + in + let total = len + 1 + padlen + 8 in + let buf = Bytes.make total '\000' in + Bytes.blit_string msg 0 buf 0 len; + Bytes.set buf len '\x80'; + (* 64-bit big-endian bit length (we cap at OCaml int range). *) + for i = 0 to 7 do + Bytes.set buf (total - 1 - i) + (Char.chr ((bitlen lsr (8 * i)) land 0xFF)) + done; + let w = Array.make 64 0 in + let nblocks = total / 64 in + for b = 0 to nblocks - 1 do + let base = b * 64 in + for t = 0 to 15 do + let o = base + t * 4 in + w.(t) <- + (Char.code (Bytes.get buf o) lsl 24) + lor (Char.code (Bytes.get buf (o + 1)) lsl 16) + lor (Char.code (Bytes.get buf (o + 2)) lsl 8) + lor (Char.code (Bytes.get buf (o + 3))) + done; + for t = 16 to 63 do + let s0 = + (rotr32 w.(t - 15) 7) lxor (rotr32 w.(t - 15) 18) + lxor (w.(t - 15) lsr 3) in + let s1 = + (rotr32 w.(t - 2) 17) lxor (rotr32 w.(t - 2) 19) + lxor (w.(t - 2) lsr 10) in + w.(t) <- (w.(t - 16) + s0 + w.(t - 7) + s1) land mask32 + done; + let a = ref h.(0) and bb = ref h.(1) and c = ref h.(2) + and d = ref h.(3) and e = ref h.(4) and f = ref h.(5) + and g = ref h.(6) and hh = ref h.(7) in + for t = 0 to 63 do + let s1 = + (rotr32 !e 6) lxor (rotr32 !e 11) lxor (rotr32 !e 25) in + let ch = (!e land !f) lxor ((lnot !e land mask32) land !g) in + let t1 = (!hh + s1 + ch + k256.(t) + w.(t)) land mask32 in + let s0 = + (rotr32 !a 2) lxor (rotr32 !a 13) lxor (rotr32 !a 22) in + let maj = (!a land !bb) lxor (!a land !c) lxor (!bb land !c) in + let t2 = (s0 + maj) land mask32 in + hh := !g; g := !f; f := !e; + e := (!d + t1) land mask32; + d := !c; c := !bb; bb := !a; + a := (t1 + t2) land mask32 + done; + h.(0) <- (h.(0) + !a) land mask32; + h.(1) <- (h.(1) + !bb) land mask32; + h.(2) <- (h.(2) + !c) land mask32; + h.(3) <- (h.(3) + !d) land mask32; + h.(4) <- (h.(4) + !e) land mask32; + h.(5) <- (h.(5) + !f) land mask32; + h.(6) <- (h.(6) + !g) land mask32; + h.(7) <- (h.(7) + !hh) land mask32 + done; + let out = Buffer.create 64 in + Array.iter (fun x -> Buffer.add_string out (Printf.sprintf "%08x" x)) h; + Buffer.contents out + +(* ---- SHA-512 (FIPS 180-4 §6.4). 64-bit words via Int64. + 128-bit length append; we only support messages whose bit length + fits in 64 bits (high word is always zero). ---- *) + +let k512 = [| + 0x428a2f98d728ae22L; 0x7137449123ef65cdL; 0xb5c0fbcfec4d3b2fL; + 0xe9b5dba58189dbbcL; 0x3956c25bf348b538L; 0x59f111f1b605d019L; + 0x923f82a4af194f9bL; 0xab1c5ed5da6d8118L; 0xd807aa98a3030242L; + 0x12835b0145706fbeL; 0x243185be4ee4b28cL; 0x550c7dc3d5ffb4e2L; + 0x72be5d74f27b896fL; 0x80deb1fe3b1696b1L; 0x9bdc06a725c71235L; + 0xc19bf174cf692694L; 0xe49b69c19ef14ad2L; 0xefbe4786384f25e3L; + 0x0fc19dc68b8cd5b5L; 0x240ca1cc77ac9c65L; 0x2de92c6f592b0275L; + 0x4a7484aa6ea6e483L; 0x5cb0a9dcbd41fbd4L; 0x76f988da831153b5L; + 0x983e5152ee66dfabL; 0xa831c66d2db43210L; 0xb00327c898fb213fL; + 0xbf597fc7beef0ee4L; 0xc6e00bf33da88fc2L; 0xd5a79147930aa725L; + 0x06ca6351e003826fL; 0x142929670a0e6e70L; 0x27b70a8546d22ffcL; + 0x2e1b21385c26c926L; 0x4d2c6dfc5ac42aedL; 0x53380d139d95b3dfL; + 0x650a73548baf63deL; 0x766a0abb3c77b2a8L; 0x81c2c92e47edaee6L; + 0x92722c851482353bL; 0xa2bfe8a14cf10364L; 0xa81a664bbc423001L; + 0xc24b8b70d0f89791L; 0xc76c51a30654be30L; 0xd192e819d6ef5218L; + 0xd69906245565a910L; 0xf40e35855771202aL; 0x106aa07032bbd1b8L; + 0x19a4c116b8d2d0c8L; 0x1e376c085141ab53L; 0x2748774cdf8eeb99L; + 0x34b0bcb5e19b48a8L; 0x391c0cb3c5c95a63L; 0x4ed8aa4ae3418acbL; + 0x5b9cca4f7763e373L; 0x682e6ff3d6b2b8a3L; 0x748f82ee5defb2fcL; + 0x78a5636f43172f60L; 0x84c87814a1f0ab72L; 0x8cc702081a6439ecL; + 0x90befffa23631e28L; 0xa4506cebde82bde9L; 0xbef9a3f7b2c67915L; + 0xc67178f2e372532bL; 0xca273eceea26619cL; 0xd186b8c721c0c207L; + 0xeada7dd6cde0eb1eL; 0xf57d4f7fee6ed178L; 0x06f067aa72176fbaL; + 0x0a637dc5a2c898a6L; 0x113f9804bef90daeL; 0x1b710b35131c471bL; + 0x28db77f523047d84L; 0x32caab7b40c72493L; 0x3c9ebe0a15c9bebcL; + 0x431d67c49c100d4cL; 0x4cc5d4becb3e42b6L; 0x597f299cfc657e2aL; + 0x5fcb6fab3ad6faecL; 0x6c44198c4a475817L |] + +let ( &: ) = Int64.logand +let ( |: ) = Int64.logor +let ( ^: ) = Int64.logxor +let ( +: ) = Int64.add +let lnot64 = Int64.lognot + +let rotr64 x n = + (Int64.shift_right_logical x n) |: (Int64.shift_left x (64 - n)) + +let sha512_hex (msg : string) : string = + let h = [| 0x6a09e667f3bcc908L; 0xbb67ae8584caa73bL; + 0x3c6ef372fe94f82bL; 0xa54ff53a5f1d36f1L; + 0x510e527fade682d1L; 0x9b05688c2b3e6c1fL; + 0x1f83d9abfb41bd6bL; 0x5be0cd19137e2179L |] in + let len = String.length msg in + let bitlen = len * 8 in + (* Pad to a multiple of 128 bytes; 16-byte big-endian length. *) + let padlen = + let r = (len + 1) mod 128 in + if r <= 112 then 112 - r else 240 - r + in + let total = len + 1 + padlen + 16 in + let buf = Bytes.make total '\000' in + Bytes.blit_string msg 0 buf 0 len; + Bytes.set buf len '\x80'; + for i = 0 to 7 do + Bytes.set buf (total - 1 - i) + (Char.chr ((bitlen lsr (8 * i)) land 0xFF)) + done; + let w = Array.make 80 0L in + let nblocks = total / 128 in + for b = 0 to nblocks - 1 do + let base = b * 128 in + for t = 0 to 15 do + let o = base + t * 8 in + let v = ref 0L in + for j = 0 to 7 do + v := Int64.logor (Int64.shift_left !v 8) + (Int64.of_int (Char.code (Bytes.get buf (o + j)))) + done; + w.(t) <- !v + done; + for t = 16 to 79 do + let s0 = + (rotr64 w.(t - 15) 1) ^: (rotr64 w.(t - 15) 8) + ^: (Int64.shift_right_logical w.(t - 15) 7) in + let s1 = + (rotr64 w.(t - 2) 19) ^: (rotr64 w.(t - 2) 61) + ^: (Int64.shift_right_logical w.(t - 2) 6) in + w.(t) <- w.(t - 16) +: s0 +: w.(t - 7) +: s1 + done; + let a = ref h.(0) and bb = ref h.(1) and c = ref h.(2) + and d = ref h.(3) and e = ref h.(4) and f = ref h.(5) + and g = ref h.(6) and hh = ref h.(7) in + for t = 0 to 79 do + let s1 = (rotr64 !e 14) ^: (rotr64 !e 18) ^: (rotr64 !e 41) in + let ch = (!e &: !f) ^: ((lnot64 !e) &: !g) in + let t1 = !hh +: s1 +: ch +: k512.(t) +: w.(t) in + let s0 = (rotr64 !a 28) ^: (rotr64 !a 34) ^: (rotr64 !a 39) in + let maj = (!a &: !bb) ^: (!a &: !c) ^: (!bb &: !c) in + let t2 = s0 +: maj in + hh := !g; g := !f; f := !e; + e := !d +: t1; + d := !c; c := !bb; bb := !a; + a := t1 +: t2 + done; + h.(0) <- h.(0) +: !a; + h.(1) <- h.(1) +: !bb; + h.(2) <- h.(2) +: !c; + h.(3) <- h.(3) +: !d; + h.(4) <- h.(4) +: !e; + h.(5) <- h.(5) +: !f; + h.(6) <- h.(6) +: !g; + h.(7) <- h.(7) +: !hh + done; + let out = Buffer.create 128 in + Array.iter + (fun x -> Buffer.add_string out (Printf.sprintf "%016Lx" x)) h; + Buffer.contents out diff --git a/plans/fed-sx-host-primitives.md b/plans/fed-sx-host-primitives.md index f3261aaa..66affdfd 100644 --- a/plans/fed-sx-host-primitives.md +++ b/plans/fed-sx-host-primitives.md @@ -68,7 +68,7 @@ Errors: `raise (Eval_error "name: shape")`. Byte strings are OCaml `string` Dependency order. Each phase: implement → `dune build` (ocaml) → **WASM build check** → tests → commit → tick box → Progress-log line → push. -### Phase A — SHA-2 (sha256 + sha512), pure OCaml +### Phase A — SHA-2 (sha256 + sha512), pure OCaml ✅ DONE - New `lib/sx_sha2.ml` (or inline in primitives if small): SHA-256 + SHA-512. - Primitives `crypto-sha256`, `crypto-sha512` → lowercase hex string. - Tests (`bin/run_tests.ml` or a dedicated `bin/test_crypto.ml`): NIST vectors — @@ -205,7 +205,10 @@ printf '(epoch 1)\n(crypto-sha256 "abc")\n' | \ _Newest first._ -- (none yet — Phase A is first) +- 2026-05-18 — Phase A: pure-OCaml `lib/sx_sha2.ml` (SHA-256 + SHA-512), + primitives `crypto-sha256`/`crypto-sha512`. 7 NIST FIPS 180-4 vectors pass + (empty/abc/896-bit/1M-'a' for sha256; empty/abc/896-bit for sha512). WASM + boot green with new lib module; Erlang conformance 530/530 unchanged. ## Blockers