chore: update for new F* build (#3)

Makefile

@@ -1,5 +1,5 @@
 MLS_HOME      ?= .
-FSTAR_HOME    ?= $(dir $(shell which fstar.exe))/..
+FSTAR_EXE     ?= fstar.exe
 COMPARSE_HOME ?= $(MLS_HOME)/../comparse
 DY_HOME       ?= $(MLS_HOME)/../dolev-yao-star
 
@@ -18,7 +18,6 @@ FSTAR_INCLUDE_DIRS = $(addprefix --include , $(INCLUDE_DIRS))
 ADMIT ?=
 MAYBE_ADMIT = $(if $(ADMIT),--admit_smt_queries true)
 
-FSTAR_EXE ?= $(FSTAR_HOME)/bin/fstar.exe
 FSTAR = $(FSTAR_EXE) $(MAYBE_ADMIT)
 
 FSTAR_EXTRACT = --extract '-* +MLS +Comparse -Comparse.Tactic $(if $(USE_DY), +DY)'
@@ -119,10 +118,10 @@ test_vectors/data/%.json: test_vectors/git_commit | test_vectors/data
 .PHONY: build check release
 
 check: copy_lib copy_tests $(ALL_TEST_VECTORS_JSON)
-	OCAMLRUNPARAM=b OCAMLPATH=$(FSTAR_HOME)/lib:$(OCAMLPATH) dune runtest --force --no-buffer --display=quiet --profile=release
+	OCAMLRUNPARAM=b $(FSTAR_EXE) --ocamlenv dune runtest --force --no-buffer --display=quiet --profile=release
 
 js: copy_lib copy_tests
-	OCAMLPATH=$(FSTAR_HOME)/lib:$(OCAMLPATH) dune build --profile=release
+	$(FSTAR_EXE) --ocamlenv dune build --profile=release
 	cd js && ./import.sh
 	cd js && ./package.sh
 

README.md

@@ -52,9 +52,10 @@ cd FStar
 git checkout $(jq -r '.nodes."fstar-flake".locked.rev' path/to/mls-star/flake.lock)
 # install F* dependencies with opam, see F*'s INSTALL.md
 make -j
-export FSTAR_HOME=$(pwd)
+export FSTAR_EXE=$(pwd)/bin/fstar.exe
 # obtain Z3 4.8.5 here https://github.com/FStarLang/binaries/tree/master/z3-tested
 export PATH=$PATH:$(cd directory/where/z3/4.8.5/lives; pwd)
+# alternatively use the get_fstar_z3.sh script in the F* repo
 ```
 
 ### Installing Comparse and DY\*
@@ -65,7 +66,7 @@ Two choices are possible:
   and `fstar.exe` is in the `PATH`
 - or [Comparse](https://github.com/TWal/comparse) is cloned in `COMPARSE_HOME`,
   [DY\*](https://github.com/REPROSEC/dolev-yao-star-extrinsic) is cloned in `DY_HOME`,
-  and F\* in `FSTAR_HOME`,
+  and `FSTAR_EXE` is set to the location of `fstar.exe`,
   in that case using [direnv](https://direnv.net/) is a advisable.
 
 When using relative path, the following commands will setup the dependencies.

default.nix

@@ -1,4 +1,4 @@
-{lib, stdenv, which, fstar, fstar-dune, z3, nodejs_20, ocamlPackages, comparse, dolev-yao-star, hacl-packages-src, fetchFromGitHub}:
+{lib, stdenv, which, fstar, z3, nodejs_20, ocamlPackages, comparse, dolev-yao-star, hacl-packages-src, fetchFromGitHub}:
 
 let
   mls-star = stdenv.mkDerivation {
@@ -48,7 +48,7 @@ let
       ++ (with ocamlPackages; [
         ocaml dune_3 findlib yojson hacl-star
       ])
-      ++ (fstar-dune.buildInputs);
+      ++ (fstar.buildInputs);
     COMPARSE_HOME = comparse;
     DY_HOME = dolev-yao-star;
     # pre-patch uses build output from mls-star, to avoid building things twice
@@ -117,7 +117,7 @@ let
         ocaml dune_3 findlib yojson hacl-star
         js_of_ocaml js_of_ocaml-ppx integers_stubs_js
       ])
-      ++ (fstar-dune.buildInputs);
+      ++ (fstar.buildInputs);
     COMPARSE_HOME = comparse;
     DY_HOME = dolev-yao-star;
     HACL_PACKAGES_HOME = hacl-packages-src;

flake.nix

@@ -28,10 +28,9 @@
     pkgs = import nixpkgs { inherit system; };
     z3 = fstar-flake.packages.${system}.z3;
     fstar = fstar-flake.packages.${system}.fstar;
-    fstar-dune = fstar-flake.packages.${system}.fstar-dune;
     comparse = comparse-flake.packages.${system}.comparse;
     dolev-yao-star = dolev-yao-star-flake.packages.${system}.dolev-yao-star;
-    mls-star = pkgs.callPackage ./default.nix {inherit fstar fstar-dune z3 comparse dolev-yao-star hacl-packages-src; ocamlPackages = pkgs.ocaml-ng.ocamlPackages_4_14;};
+    mls-star = pkgs.callPackage ./default.nix {inherit fstar z3 comparse dolev-yao-star hacl-packages-src; ocamlPackages = pkgs.ocaml-ng.ocamlPackages_4_14;};
   in {
     packages.${system} = {
       default = mls-star;
@@ -44,7 +43,7 @@
         ocaml dune_3 findlib yojson hacl-star
         js_of_ocaml js_of_ocaml-ppx integers_stubs_js
       ])
-      ++ (fstar-dune.buildInputs);
+      ++ (fstar.buildInputs);
       COMPARSE_HOME = comparse;
       DY_HOME = dolev-yao-star;
       HACL_PACKAGES_HOME = hacl-packages-src;

hacl-star-snapshot/haclml/FStar_Range.ml

@@ -0,0 +1,7 @@
+open Prims
+(* Following FStarLang/FStar#3637 FStar_Range is reserved for plugins *)
+(* However it is used by the HACL* snapshot for some reason *)
+(* Emulating the minimal interface here *)
+type ('a, 'b, 'c) labeled = unit
+type range = unit
+let mk_range (s:string) (i1:int) (i2:int) (i3:int) (i4:int): range = ()