project-everest · tahina-pro · Jul 3, 2026 · Jul 1, 2026 · Jul 1, 2026 · Jul 1, 2026
diff --git a/Makefile b/Makefile
@@ -65,7 +65,11 @@ lowparse: $(filter src/lowparse/pulse/%,$(ALL_CHECKED_FILES))
 endif
 
 # lowparse needed because of .fst behind .fsti for extraction
-3d-prelude: $(filter src/3d/prelude/%,$(ALL_CHECKED_FILES)) $(filter-out src/lowparse/LowParse.SLow.% src/lowparse/pulse/%,$(filter src/lowparse/%,$(ALL_CHECKED_FILES)))
+3d-prelude-verify: $(filter src/3d/prelude/%,$(ALL_CHECKED_FILES)) $(filter-out src/lowparse/LowParse.SLow.% src/lowparse/pulse/%,$(filter src/lowparse/%,$(ALL_CHECKED_FILES)))
+
+.PHONY: 3d-prelude-verify
+
+3d-prelude: 3d-prelude-verify
 	+$(MAKE) -C src/3d/prelude
 
 .PHONY: 3d-prelude

diff --git a/README.md b/README.md
@@ -387,8 +387,8 @@ variables:
   `EVERPARSE_USE_OPAMROOT=1`.
 
 * If you want to use your own Karamel, first set
-  `EVERPARSE_USE_KRML_HOME=1`, then set `KRML_HOME` to the full path
-  of your clone of the Karamel repository. This will automatically set
+  `EVERPARSE_USE_KRML_EXE=1`, then set `KRML_EXE` to the full path
+  of the Karamel executable. This will automatically set
   `EVERPARSE_USE_FSTAR_HOME=1`, since the Karamel library must be
   compiled with the same F\* as EverParse.
 

diff --git a/deps.Makefile b/deps.Makefile
@@ -18,19 +18,23 @@ EVERPARSE_Z3_VERSION ?= 4.13.3
 ifeq (1,$(EVERPARSE_USE_MY_DEPS))
 export EVERPARSE_USE_OPAMROOT:=1
 export EVERPARSE_USE_FSTAR_EXE:=1
-export EVERPARSE_USE_KRML_HOME:=1
+export EVERPARSE_USE_KRML_EXE:=1
 export EVERPARSE_USE_PULSE_HOME:=1
 endif
 
 NEED_KRML :=
-ifneq (1,$(EVERPARSE_USE_KRML_HOME))
-export KRML_HOME := $(EVERPARSE_OPT_PATH)/karamel
+ifneq (1,$(EVERPARSE_USE_KRML_EXE))
+ifeq ($(OS),Windows_NT)
+export KRML_EXE := $(EVERPARSE_OPT_PATH)/karamel/out/bin/krml.exe
+else
+export KRML_EXE := $(EVERPARSE_OPT_PATH)/karamel/out/bin/krml
+endif
 NEED_KRML := $(EVERPARSE_OPT_PATH)/karamel.done
 else
 export EVERPARSE_USE_FSTAR_EXE:=1
-ifeq (,$(KRML_HOME))
+ifeq (,$(KRML_EXE))
 # TODO: fix Karamel to not require KRML_HOME set
-$(error "Inconsistent setup: EVERPARSE_USE_KRML_HOME set but KRML_HOME not set")
+$(error "Inconsistent setup: EVERPARSE_USE_KRML_EXE set but KRML_EXE not set")
 endif
 endif
 
@@ -145,9 +149,19 @@ $(EVERPARSE_OPT_PATH)/z3: $(EVERPARSE_OPT_PATH)/FStar/Makefile
 	mv $@.tmp $@
 	touch $@
 
+# NOTE: we unset KRML_EXE here so that Karamel's own build (in particular
+# krmllib) uses the freshly-built in-tree `krml` (../krml) instead of the
+# not-yet-installed $(EVERPARSE_OPT_PATH)/karamel/out/bin/krml that we export
+# below for EverParse. Otherwise krmllib's `KRML_EXE ?= ../krml` picks up our
+# exported value and fails with "No rule to make target .../out/bin/krml".
 $(EVERPARSE_OPT_PATH)/karamel.done: $(EVERPARSE_OPT_PATH)/karamel/Makefile $(NEED_FSTAR) $(NEED_OPAM)
 	rm -f $@
-	+$(with_opam) env OTHERFLAGS='--admit_smt_queries true' $(MAKE) -C $(EVERPARSE_OPT_PATH)/karamel
+	+$(with_opam) env -u KRML_EXE OTHERFLAGS='--admit_smt_queries true' $(MAKE) -C $(EVERPARSE_OPT_PATH)/karamel minimal
+	+$(with_opam) env -u KRML_EXE OTHERFLAGS='--admit_smt_queries true' KRML_LIBDIR="$(EVERPARSE_OPT_PATH)/karamel/krmllib" KRML_INCLUDEDIR="$(EVERPARSE_OPT_PATH)/karamel/include" KRML_MISCDIR="$(EVERPARSE_OPT_PATH)/karamel/misc" $(MAKE) -C "$(EVERPARSE_OPT_PATH)/karamel/krmllib"
+	+$(with_opam) env -u KRML_EXE $(MAKE) -C "$(EVERPARSE_OPT_PATH)/karamel" _install PREFIX="$(EVERPARSE_OPT_PATH)/karamel/out"
+ifeq ($(OS),Windows_NT)
+	mv "$(EVERPARSE_OPT_PATH)/karamel/out/bin/krml" "$(EVERPARSE_OPT_PATH)/karamel/out/bin/krml.exe"
+endif
 	touch $@
 
 $(EVERPARSE_OPT_PATH)/pulse.done: $(EVERPARSE_OPT_PATH)/pulse/Makefile $(NEED_FSTAR) $(NEED_OPAM)
@@ -158,10 +172,10 @@ $(EVERPARSE_OPT_PATH)/pulse.done: $(EVERPARSE_OPT_PATH)/pulse/Makefile $(NEED_FS
 env:
 	@echo export EVERPARSE_USE_OPAMROOT=$(EVERPARSE_USE_OPAMROOT)
 	@echo export EVERPARSE_USE_FSTAR_EXE=$(EVERPARSE_USE_FSTAR_EXE)
-	@echo export EVERPARSE_USE_KRML_HOME=$(EVERPARSE_USE_KRML_HOME)
+	@echo export EVERPARSE_USE_KRML_EXE=$(EVERPARSE_USE_KRML_EXE)
 	@echo export EVERPARSE_USE_PULSE_HOME=$(EVERPARSE_USE_PULSE_HOME)
 	@echo export FSTAR_EXE=$(FSTAR_EXE)
-	@echo export KRML_HOME=$(KRML_HOME)
+	@echo export KRML_EXE=$(KRML_EXE)
 ifeq (,$(NO_PULSE))
 	@echo export PULSE_HOME=$(PULSE_HOME)
 endif

diff --git a/doc/3d-snapshot/BoundedSumConst.c b/doc/3d-snapshot/BoundedSumConst.c
@@ -79,8 +79,7 @@ BoundedSumConstValidateBoundedSum(
     uint32_t right_refinement = Load32Le(Input + (uint32_t)positionAfterleft);
     /* start: checking constraint */
     BOOLEAN
-    right_refinementConstraintIsOk =
-      left <= (uint32_t)42U && right_refinement <= ((uint32_t)42U - left);
+    right_refinementConstraintIsOk = left <= 42U && right_refinement <= ((uint32_t)42U - left);
     /* end: checking constraint */
     positionAfterBoundedSum0 =
       EverParseCheckConstraintOk(right_refinementConstraintIsOk,

diff --git a/doc/3d-snapshot/BoundedSumWhere.c b/doc/3d-snapshot/BoundedSumWhere.c
@@ -29,7 +29,7 @@ BoundedSumWhereValidateBoundedSum(
   }
   else
   {
-    BOOLEAN preconditionConstraintIsOk = Bound <= (uint32_t)1729U;
+    BOOLEAN preconditionConstraintIsOk = Bound <= 1729U;
     uint64_t
     positionAfterPrecondition1 =
       EverParseCheckConstraintOk(preconditionConstraintIsOk,

diff --git a/doc/3d-snapshot/EnumConstraint.c b/doc/3d-snapshot/EnumConstraint.c
@@ -75,8 +75,7 @@ EnumConstraintValidateEnumConstraint(
         /* reading field_value */
         uint32_t x_refinement = Load32Le(Input + (uint32_t)positionAftercol1);
         /* start: checking constraint */
-        BOOLEAN
-        x_refinementConstraintIsOk = x_refinement == (uint32_t)0U || col == ENUMCONSTRAINT_GREEN;
+        BOOLEAN x_refinementConstraintIsOk = x_refinement == 0U || col == ENUMCONSTRAINT_GREEN;
         /* end: checking constraint */
         positionAfterEnumConstraint0 =
           EverParseCheckConstraintOk(x_refinementConstraintIsOk,

diff --git a/doc/3d-snapshot/Smoker.c b/doc/3d-snapshot/Smoker.c
@@ -41,7 +41,7 @@ SmokerValidateSmoker(
   else
   {
     uint32_t age = Load32Le(Input + (uint32_t)StartPosition);
-    BOOLEAN ageConstraintIsOk = age >= (uint32_t)21U;
+    BOOLEAN ageConstraintIsOk = age >= 21U;
     uint64_t positionAfterage1 = EverParseCheckConstraintOk(ageConstraintIsOk, positionAfterage);
     if (EverParseIsError(positionAfterage1))
     {

diff --git a/doc/3d-snapshot/SpecializeDep1.c b/doc/3d-snapshot/SpecializeDep1.c
@@ -549,7 +549,7 @@ ValidateWrapper(
         uint64_t readOffset = 0ULL;
         uint64_t writeOffset = 0ULL;
         BOOLEAN failed = FALSE;
-        BOOLEAN ok = ProbeInit("_WRAPPER.tlv", (uint64_t)Len, Output);
+        BOOLEAN ok = ProbeInit("_WRAPPER.tlv", (uint64_t)(uint32_t)Len, Output);
         if (ok)
         {
           ProbeTlv((uint32_t)Len - (uint32_t)(uint16_t)5U,
@@ -562,7 +562,7 @@ ValidateWrapper(
             &writeOffset,
             &failed,
             src64,
-            (uint64_t)Len,
+            (uint64_t)(uint32_t)Len,
             Output);
         }
         else
@@ -711,7 +711,7 @@ ValidateSpecializedWrapper32(
         uint64_t readOffset = 0ULL;
         uint64_t writeOffset = 0ULL;
         BOOLEAN failed = FALSE;
-        BOOLEAN ok = ProbeInit("___specialized_WRAPPER_32.tlv", (uint64_t)Len, Output);
+        BOOLEAN ok = ProbeInit("___specialized_WRAPPER_32.tlv", (uint64_t)(uint32_t)Len, Output);
         if (ok)
         {
           Specialized32ProbeTlv((uint32_t)Len - (uint32_t)(uint16_t)5U,

diff --git a/doc/Makefile b/doc/Makefile
@@ -7,8 +7,6 @@ export EVERPARSE_HOME?=$(realpath ..)
 
 FSTAR_EXE ?= fstar.exe
 
-export KRML_HOME?=$(realpath $(EVERPARSE_HOME)/../karamel)
-
 3D=$(EVERPARSE_HOME)/bin/3d.exe --fstar $(FSTAR_EXE)
 3D_EXCLUDE=ConstColor.3d
 3D_CONFIG=Arch.3d.config

diff --git a/fstar.sh b/fstar.sh
@@ -3,4 +3,10 @@ set -e
 unset CDPATH
 EVERPARSE_HOME="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
 source "$EVERPARSE_HOME"/env.sh
-exec "$FSTAR_EXE" --z3version $EVERPARSE_Z3_VERSION --include "$KRML_HOME/krmllib" --include "$KRML_HOME/krmllib/obj" --include "$PULSE_HOME/lib/pulse" "$@"
+if [[ -z "$KRML_LIB" ]] ; then
+    KRML_LIB="$("$KRML_EXE" -locate-krmllib)"
+fi
+if [[ "$OS" = Windows_NT ]] ; then
+    KRML_LIB="$(cygpath -m "$(echo "$KRML_LIB" | sed 's!\r!!g')")"
+fi
+exec "$FSTAR_EXE" --z3version $EVERPARSE_Z3_VERSION --include "$KRML_LIB" --include "$KRML_LIB"/obj --include "$PULSE_HOME/lib/pulse" "$@"
diff --git a/opt/advance.Makefile b/opt/advance.Makefile
@@ -1,3 +1,3 @@
 FStar_hash := origin/fstar1
-karamel_hash := origin/everparse-fstar1
+karamel_hash := origin/master
 pulse_hash := origin/fstar1
diff --git a/opt/hashes.Makefile b/opt/hashes.Makefile
@@ -1,3 +1,3 @@
-FStar_hash := a22c99321085c847012759d062e718db55aed01d
-karamel_hash := 5b4384116d96ca9af7732d2f7d1fe3b5284d421f
-pulse_hash := 74bb5a472cf0f0ef5e2eb2262a3411349efa21cc
+FStar_hash := de9d045cbfa5d0dc456fbeae04389c3d98a59347
+karamel_hash := 11bb8e1ac2f720fb7144b9b768c7251526caa149
+pulse_hash := 8b5f45df8ccbccba122742c5ae6e6d2925dde09f
diff --git a/share/everparse/tests/lowparse/Makefile b/share/everparse/tests/lowparse/Makefile
@@ -22,7 +22,7 @@ ifeq ($(OS),Darwin)
 KRML_OPTS += -ccopt -Wno-tautological-constant-out-of-range-compare
 endif
 
-KRML=$(KRML_HOME)/krml -fstar $(FSTAR_EXE) $(KRML_OPTS)
+KRML=$(KRML_EXE) -fstar $(FSTAR_EXE) $(KRML_OPTS)
 
 EXAMPLES=Example3 ExampleConstInt32le Example2 Example5 Example7 Example8 Example9 Example10 Example11 Example12 ExampleDepLen
 

diff --git a/share/everparse/tests/qd/unit/extracted.Makefile b/share/everparse/tests/qd/unit/extracted.Makefile
@@ -2,13 +2,12 @@ EVERPARSE_HOME ?= $(realpath ../../../../../..)
 EVERPARSE_SRC_PATH ?= $(EVERPARSE_HOME)/src
 
 LOWPARSE_HOME ?= $(EVERPARSE_SRC_PATH)/lowparse
-KRML_HOME ?= $(EVERPARSE_HOME)/opt/karamel
 
+include $(EVERPARSE_SRC_PATH)/karamel.Makefile
 include $(EVERPARSE_SRC_PATH)/fstar.Makefile
 
 export FSTAR_EXE
 export LOWPARSE_HOME
-export KRML_HOME
 
 ifdef NO_QD_VERIFY
 LAX_EXT=.lax
@@ -24,7 +23,7 @@ CHECKED_EXT=.checked$(LAX_EXT)
 
 FSTAR_OPTIONS += --odir krml --cache_dir $(CACHE_DIR) $(LAX_OPT) --cache_checked_modules \
 		--already_cached +Prims,+FStar,+LowStar,+C,+Spec.Loops,+LowParse \
-		--include $(LOWPARSE_HOME) --include $(LOWPARSE_HOME)/pulse --include $(PULSE_HOME)/lib/pulse --include $(KRML_HOME)/krmllib --include $(KRML_HOME)/krmllib/obj --include .. --cmi --ext context_pruning \
+		--include $(LOWPARSE_HOME) --include $(LOWPARSE_HOME)/pulse --include $(PULSE_HOME)/lib/pulse --include .. --cmi --ext context_pruning \
 		--ext 'optimize_let_vc=false' \
 		--warn_error '@272'
 
@@ -37,7 +36,7 @@ KRML_OPTS += -ccopt -Wno-tautological-constant-out-of-range-compare
 endif
 
 # -Wno-tautological-overlap-compare because of T32
-KRML = $(KRML_HOME)/krml \
+KRML = $(KRML_EXE) \
 	 -fstar $(FSTAR_EXE) \
 	 -ccopt "-O3" -ccopt "-ffast-math" \
 	 -ccopt "-Wno-tautological-overlap-compare" \

diff --git a/src/3d/Batch.fsti b/src/3d/Batch.fsti
@@ -2,6 +2,9 @@ module Batch
 open HashingOptions
 open FStar.All
 
+val krmllib: string -> ML string
+val krmlinclude: string -> ML string
+
 val cl_wrapper: unit -> ML string
 
 (* The --print_in_place step has to be performed at source generation

diff --git a/src/3d/Main.fst b/src/3d/Main.fst
@@ -556,7 +556,7 @@ let build_test_exe
   end else
   if not (Options.get_skip_c_makefiles ())
   then begin
-    OS.run_cmd "make" ["-C"; out_dir; "-f"; "Makefile.basic"; "USER_TARGET=test.exe"; "USER_CFLAGS=-Wno-type-limits"]
+    OS.run_cmd "make" ["-C"; out_dir; "-f"; "Makefile.basic"; "USER_TARGET=test.exe"; "USER_CFLAGS=-Wno-type-limits"; "KRML_LIBDIR=" ^ Batch.krmllib out_dir; "KRML_INCLUDEDIR=" ^ Batch.krmlinclude out_dir]
   end
 
 let build_and_run_test_exe