Merge pull request #1 from Inria-Prosecco/protz_js

Restore some of the JS build

Makefile

@@ -24,7 +24,7 @@ FSTAR_EXTRACT = --extract '-* +MLS +Comparse $(DY_EXTRACT) -Comparse.Tactic'
 # - (Warning 242) Definitions of inner let-rec ... and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types
 # - (Warning 331) This name is being ignored
 # - (Warning 335) Interface ... is admitted without an implementation 
-FSTAR_FLAGS = $(FSTAR_INCLUDE_DIRS) --cache_checked_modules --already_cached '+Prims +FStar' --warn_error '@0..1000' --warn_error '+242+331-335' --cache_dir cache --odir obj --cmi
+FSTAR_FLAGS = $(FSTAR_INCLUDE_DIRS) --cache_checked_modules --already_cached '+Prims +FStar' --warn_error '@0..1000' --warn_error '+242+331-335' --cache_dir cache --odir obj --cmi $(OTHERFLAGS)
 
 .PHONY: all clean
 
@@ -114,8 +114,7 @@ test_vectors/data/%.json: test_vectors/git_commit | test_vectors/data
 
 .PHONY: build check release
 
-build: copy_lib
-	$(MAKE) -C fstar extract
+build: copy_lib copy_tests
 	OCAMLPATH=$(FSTAR_HOME)/lib:$(OCAMLPATH) dune build --profile=release
 
 check: copy_lib copy_tests $(ALL_TEST_VECTORS_JSON)

default.nix

@@ -25,6 +25,7 @@ let
       cp -r ml fstar cache hints $out
     '';
     passthru.tests = mls-star-tests;
+    passthru.js = mls-star-js;
   };
 
   mls-star-tests = stdenv.mkDerivation {
@@ -60,7 +61,8 @@ let
     '';
     doCheck = true;
     installPhase = ''
-      touch $out
+      mkdir -p $out
+      cp -r ml fstar cache hints $out
     '';
     passthru.test-vectors = test-files;
   };
@@ -74,5 +76,42 @@ let
       sha256 = "sha256-qYtSzY9epzvgahbJ3/omzGRwH5PVDLQmFfHzmQLDRc8=";
     }
   ;
+
+  mls-star-js = stdenv.mkDerivation {
+    name = "mls-star-js";
+    src =
+      lib.sources.sourceByRegex ./. [
+        "hacl-star-snapshot(/.*)?"
+        "fstar(/.*)?"
+        "Makefile"
+        "dune-project"
+        "ml(/lib(/dune)?)?"
+        "ml(/tests(/dune)?)?"
+        "js(/.*)?"
+        "mls.opam"
+      ]
+    ;
+    enableParallelBuilding = true;
+    buildFlags = "build";
+    buildInputs =
+      [ which fstar z3 ]
+      ++ (with ocamlPackages; [
+        ocaml dune_3 findlib yojson hacl-star
+        js_of_ocaml js_of_ocaml-ppx integers_stubs_js
+      ])
+      ++ (fstar-dune.buildInputs);
+    COMPARSE_HOME = comparse;
+    DY_HOME = dolev-yao-star;
+    # pre-patch uses build output from mls-star, to avoid building things twice
+    prePatch = ''
+      cp -pr --no-preserve=mode ${mls-star-tests}/cache ${mls-star-tests}/ml .
+      mkdir obj
+      cp -p ml/lib/src/* obj/
+    '';
+    installPhase = ''
+      touch $out
+    '';
+  };
+
 in
   mls-star

flake.nix

@@ -39,8 +39,9 @@
       ++ (fstar.buildInputs);
     };
     checks.${system} = {
-      mls-build = mls-star;
-      mls-tests = mls-star.tests;
+      mls-star-build = mls-star;
+      mls-star-tests = mls-star.tests;
+      mls-star-js = mls-star.js;
     };
   };
 }

fstar/api/MLS.fst

@@ -703,6 +703,8 @@ let process_group_message state msg =
     | _ ->
         internal_failure "unknown message type"
   ) in
+  // Needed to prove the completeness of the pattern-match below
+  let _ = allow_inversion content_type_nt in
   // Note: can't do a dependent pair pattern matching, have to nest matches +
   // annotations because of the dependency
   match message.content.content.content_type with
@@ -742,5 +744,3 @@ let process_group_message state msg =
   | CT_application ->
       let data: bytes = message.content.content.content in
       return (state, MsgData data)
-  | _ ->
-      internal_failure "unknown message content type"

hacl-star-snapshot/js-helpers/JsHelpers.ml

@@ -0,0 +1,36 @@
+open Js_of_ocaml
+
+(* In spec-land, `FStar.Seq.seq FStar.UInt8.t` becomes this: *)
+type bytes = int FStar_Seq_Base.seq
+
+let list_of_bytes = FStar_Seq_Properties.seq_to_list
+
+let bytes_of_list l =
+  FStar_Seq_Base.MkSeq (List.map (fun x ->
+    assert (x <= 255);
+    x
+  ) l)
+
+let bytes_of_js_string (s: Js.js_string Js.t) =
+  let s = Js.to_string s in
+  bytes_of_list (List.map (fun x -> Char.code x) (List.of_seq (String.to_seq s)))
+
+let js_string_of_bytes (b: bytes): Js.js_string Js.t =
+  let FStar_Seq_Base.MkSeq b = b in
+  Js.string (String.of_seq (Seq.map Char.chr (List.to_seq b)))
+
+let byte_length (a: Typed_array.uint8Array Js.t) =
+  let a = Obj.magic a in
+  a##.byteLength
+
+let bytes_of_uint8array (a: Typed_array.uint8Array Js.t) =
+  let l = byte_length a in
+  (* Printf.printf "byte length %d\n" l; *)
+  FStar_Seq_Base.MkSeq (List.init l (fun i -> Typed_array.unsafe_get a i))
+
+let uint8array_of_bytes (b: bytes) =
+  let FStar_Seq_Base.MkSeq b = b in
+  let l = List.length b in
+  let a = new%js Typed_array.uint8Array l in
+  List.iteri (Typed_array.set a) b;
+  a

hacl-star-snapshot/js-helpers/dune

@@ -0,0 +1,8 @@
+(library
+ (name js_helpers)
+ (public_name mls.js_helpers)
+ (preprocess
+  (pps js_of_ocaml-ppx))
+ (wrapped false)
+ (modes byte native)
+ (libraries js_of_ocaml fstar.lib))

hacl-star-snapshot/primitives-js/Primitives.ml

@@ -0,0 +1,92 @@
+open Js_of_ocaml
+
+module H = JsHelpers
+
+type bytes = int FStar_Seq_Base.seq
+
+type js_u8array = Typed_array.uint8Array Js.t
+
+external whacl_sha2_256_hash: js_u8array -> js_u8array = "whacl_sha2_256_hash"
+
+let sha2_256_hash b =
+  H.bytes_of_uint8array (whacl_sha2_256_hash (H.uint8array_of_bytes b))
+
+external whacl_hkdf_sha2_256_extract: js_u8array -> js_u8array -> js_u8array = "whacl_hkdf_sha2_256_extract"
+
+let hkdf_sha2_256_extract ~salt ~ikm =
+  let salt = H.uint8array_of_bytes salt in
+  let ikm = H.uint8array_of_bytes ikm in
+  H.bytes_of_uint8array (whacl_hkdf_sha2_256_extract salt ikm)
+
+external whacl_hkdf_sha2_256_expand: js_u8array -> js_u8array -> int -> js_u8array = "whacl_hkdf_sha2_256_expand"
+
+let hkdf_sha2_256_expand ~prk ~info ~size =
+  let prk = H.uint8array_of_bytes prk in
+  let info = H.uint8array_of_bytes info in
+  let size = Z.to_int size in
+  H.bytes_of_uint8array (whacl_hkdf_sha2_256_expand prk info size)
+
+external whacl_sha2_512_hash: js_u8array -> js_u8array = "whacl_sha2_512_hash"
+
+let sha2_512_hash b =
+  let b = H.uint8array_of_bytes b in
+  H.bytes_of_uint8array (whacl_sha2_512_hash b)
+
+external whacl_ed25519_secret_to_public: js_u8array -> js_u8array = "whacl_ed25519_secret_to_public"
+
+let ed25519_secret_to_public ~sk =
+  let sk = H.uint8array_of_bytes sk in
+  H.bytes_of_uint8array (whacl_ed25519_secret_to_public sk)
+
+external whacl_ed25519_sign: js_u8array -> js_u8array -> js_u8array = "whacl_ed25519_sign"
+
+let ed25519_sign ~sk ~msg =
+  let sk = H.uint8array_of_bytes sk in
+  let msg = H.uint8array_of_bytes msg in
+  H.bytes_of_uint8array (whacl_ed25519_sign sk msg)
+
+external whacl_ed25519_verify: js_u8array -> js_u8array -> js_u8array -> bool Js.t = "whacl_ed25519_verify"
+
+let ed25519_verify ~pk ~msg ~signature =
+  let pk = H.uint8array_of_bytes pk in
+  let msg = H.uint8array_of_bytes msg in
+  let signature = H.uint8array_of_bytes signature in
+  Js.to_bool (whacl_ed25519_verify pk msg signature)
+
+external whacl_chacha20_poly1305_encrypt:
+  js_u8array -> js_u8array -> js_u8array -> js_u8array -> js_u8array Js.js_array Js.t
+= "whacl_chacha20_poly1305_encrypt"
+
+let chacha20_poly1305_encrypt ~key ~iv ~ad ~pt =
+  let key = H.uint8array_of_bytes key in
+  let iv = H.uint8array_of_bytes iv in
+  let ad = H.uint8array_of_bytes ad in
+  let pt = H.uint8array_of_bytes pt in
+  let ret = whacl_chacha20_poly1305_encrypt key iv ad pt in
+  let ret = Js.to_array ret in
+  let ct = H.bytes_of_uint8array ret.(0) in
+  let tag = H.bytes_of_uint8array ret.(1) in
+  FStar_Seq_Base.append ct tag
+
+external whacl_chacha20_poly1305_decrypt:
+  js_u8array -> js_u8array -> js_u8array -> js_u8array -> js_u8array -> js_u8array Js.Opt.t
+= "whacl_chacha20_poly1305_decrypt"
+
+let chacha20_poly1305_decrypt ~key ~iv ~ad ~ct ~tag =
+  let key = H.uint8array_of_bytes key in
+  let iv = H.uint8array_of_bytes iv in
+  let ad = H.uint8array_of_bytes ad in
+  let ct = H.uint8array_of_bytes ct in
+  let tag = H.uint8array_of_bytes tag in
+  match Js.Opt.to_option (whacl_chacha20_poly1305_decrypt key iv ad ct tag) with
+  | Some pt -> Some (H.bytes_of_uint8array pt)
+  | None -> None
+
+
+let aes128gcm_encrypt ~key ~iv ~ad ~pt =
+  ignore (key, iv, ad, pt);
+  failwith "Not implemented in JS: aes128gcm_encrypt"
+
+let aes128gcm_decrypt ~key ~iv ~ad ~ct ~tag =
+  ignore (key, iv, ad, ct, tag);
+  failwith "Not implemented in JS: aes128gcm_decrypt"

hacl-star-snapshot/primitives-js/dummy.c

@@ -0,0 +1,39 @@
+#include <caml/fail.h>
+
+const char *error_msg = "This is a stub that was never intended to be called";
+
+CAMLprim value whacl_sha2_256_hash() {
+  caml_failwith(error_msg);
+}
+
+CAMLprim value whacl_hkdf_sha2_256_extract() {
+  caml_failwith(error_msg);
+}
+
+CAMLprim value whacl_hkdf_sha2_256_expand() {
+  caml_failwith(error_msg);
+}
+
+CAMLprim value whacl_sha2_512_hash() {
+  caml_failwith(error_msg);
+}
+
+CAMLprim value whacl_ed25519_secret_to_public() {
+  caml_failwith(error_msg);
+}
+
+CAMLprim value whacl_ed25519_sign() {
+  caml_failwith(error_msg);
+}
+
+CAMLprim value whacl_ed25519_verify() {
+  caml_failwith(error_msg);
+}
+
+CAMLprim value whacl_chacha20_poly1305_encrypt() {
+  caml_failwith(error_msg);
+}
+
+CAMLprim value whacl_chacha20_poly1305_decrypt() {
+  caml_failwith(error_msg);
+}

hacl-star-snapshot/primitives-js/dune

@@ -0,0 +1,11 @@
+(library
+ (public_name mls.primitives_js)
+ (name primitives_js)
+ (libraries js_helpers)
+ (foreign_stubs
+  (language c)
+  ;(flags -I/blah/include)
+  (names dummy))
+ (implements haclml)
+ ; (modes byte)
+)

hacl-star-snapshot/primitives-native/dune

@@ -2,4 +2,6 @@
  (public_name mls.primitive_native)
  (name primitives_native)
  (libraries hacl-star)
- (implements haclml))
+ (implements haclml)
+ ; (modes native)
+)