Merge commit '154d840a3c7d7836207e05c93d3e4c98cb15d44a' into _goto_for_early_return0

Author: tahina-pro

.github/workflows/ci.yml

@@ -39,13 +39,14 @@ jobs:
         uses: actions/cache/restore@v4
         with:
           path: _opam
-          key: opam-${{ runner.os }}-${{ runner.arch }}-${{ github.run_id }}
+          key: opam-${{ runner.os }}-${{ runner.arch }}-fstar1-${{ github.run_id }}
           restore-keys: |
+            opam-${{ runner.os }}-${{ runner.arch }}-fstar1-
             opam-${{ runner.os }}-${{ runner.arch }}-
 
-      # Build F* master.
+      # Build F*, from the fstar1 branch.
       - run: opam update
-      - run: opam pin -n fstar --dev-repo
+      - run: opam pin -n fstar git+https://github.com/FStarLang/FStar#fstar1
       - run: opam install fstar
 
       # Install karamel deps
@@ -64,9 +65,10 @@ jobs:
           # and so far no Karamel regression test suite for EverParse
           # requires 3d
 
+      # Paranoid delete before saving. Note: run_id is constant across reruns.
       - name: Delete OPAM state if it already existed
         run: |
-          gh cache delete opam-${{ runner.os }}-${{ runner.arch }}-${{ github.run_id }} || true
+          gh cache delete opam-${{ runner.os }}-${{ runner.arch }}-fstar1-${{ github.run_id }} || true
         env:
           GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
           GH_REPO: ${{ github.repository }}
@@ -76,7 +78,7 @@ jobs:
         uses: actions/cache/save@v4
         with:
           path: _opam
-          key: opam-${{ runner.os }}-${{ runner.arch }}-${{ github.run_id }}
+          key: opam-${{ runner.os }}-${{ runner.arch }}-fstar1-${{ github.run_id }}
 
   build-and-test:
     needs: build-deps
@@ -94,7 +96,7 @@ jobs:
       - name: Setup ocaml
         uses: ocaml/setup-ocaml@v3
         with:
-           ocaml-compiler: 4.14.2
+           ocaml-compiler: 5.3.0
 
       - uses: actions/checkout@master
         with:
@@ -103,16 +105,14 @@ jobs:
       - name: Restore OPAM state
         uses: actions/cache/restore@v4
         with:
-          fail-on-cache-miss: true
+          fail-on-cache-miss: true # should never happen, cache was filled by build-deps
           path: _opam
-          key: opam-${{ runner.os }}-${{ runner.arch }}-${{ github.run_id }}
+          key: opam-${{ runner.os }}-${{ runner.arch }}-fstar1-${{ github.run_id }}
 
       - uses: actions/setup-node@v4
         with:
           node-version: 16
 
-      - run: echo "KRML_HOME=$(pwd)/karamel" >> $GITHUB_ENV
-
       - name: Karamel CI
         working-directory: karamel
         run: |
@@ -144,7 +144,7 @@ jobs:
       - name: Setup ocaml
         uses: ocaml/setup-ocaml@v3
         with:
-           ocaml-compiler: 4.14.2
+           ocaml-compiler: 5.3.0
 
       - uses: actions/checkout@master
         with:
@@ -153,9 +153,9 @@ jobs:
       - name: Restore OPAM state
         uses: actions/cache/restore@v4
         with:
-          fail-on-cache-miss: true
+          fail-on-cache-miss: true # should never happen, cache was filled by build-deps
           path: _opam
-          key: opam-${{ runner.os }}-${{ runner.arch }}-${{ github.run_id }}
+          key: opam-${{ runner.os }}-${{ runner.arch }}-fstar1-${{ github.run_id }}
 
       - name: Setup environment
         run: |
@@ -193,6 +193,7 @@ jobs:
         run: |
           git pull && make cbor-extract-krml cose-extract-krml -kj$(nproc)
 
+      # Paranoid delete before saving. Note: run_id is constant across reruns.
       - name: Delete EverParse cache if it already existed
         run: |
           gh cache delete everparse-${{ runner.os }}-${{ runner.arch }}-${{ github.run_id }} || true
@@ -239,17 +240,96 @@ jobs:
       - uses: actions/checkout@master
       - name: Build the checked-in krmllib
         run: |
-          export KRML_HOME=$(pwd)
           export CC=${{matrix.cc}}
+          export KRML_INCLUDEDIR=$(pwd)/include
+          export KRML_LIBDIR=$(pwd)/krmllib
           make -kj$(nproc) -C krmllib/dist/generic -f Makefile.basic
 
+  build-and-test-pulse:
+    runs-on: ubuntu-latest
+    needs: build-deps
+    steps:
+      - name: Setup ocaml
+        uses: ocaml/setup-ocaml@v3
+        with:
+           ocaml-compiler: 5.3.0
+
+      # Note, we prefer to restore the -master cache, but if it doesn't exist,
+      # we restore the latest normal one.
+      - name: Restore OPAM state
+        uses: actions/cache/restore@v4
+        with:
+          fail-on-cache-miss: true
+          path: _opam
+          key: opam-${{ runner.os }}-${{ runner.arch }}-master-${{ github.run_id }}
+          restore-keys: |
+            opam-${{ runner.os }}-${{ runner.arch }}-master-
+            opam-${{ runner.os }}-${{ runner.arch }}-
+
+      # Build F*, master branch
+      - run: opam update
+      - run: opam pin -n fstar git+https://github.com/FStarLang/FStar#master
+      - run: opam install fstar
+
+      # Save OPAM state, note master- in key.
+      - name: Save OPAM state
+        uses: actions/cache/save@v4
+        with:
+          path: _opam
+          key: opam-${{ runner.os }}-${{ runner.arch }}-master-${{ github.run_id }}
+
+      - name: Install Z3 with script
+        run: |
+          wget https://raw.githubusercontent.com/FStarLang/FStar/refs/heads/master/.scripts/get_fstar_z3.sh -O get_fstar_z3.sh
+          chmod +x get_fstar_z3.sh
+          ./get_fstar_z3.sh /usr/local/bin
+       # If these fail, stop right now.
+      - run: which z3-4.8.5
+      - run: which z3-4.13.3
+
+      - uses: actions/checkout@master
+        with:
+          path: karamel
+
+      - uses: actions/setup-node@v4
+        with:
+          node-version: 16
+
+      - run: echo "KRML_HOME=$(pwd)/karamel" >> $GITHUB_ENV
+
+      - name: Karamel CI (test-pulse)
+        working-directory: karamel
+        run: |
+          eval $(opam env)
+          export OCAMLRUNPARAM=b
+          make -kj$(nproc) test-pulse
+
+  test-eurydice:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Install Nix
+        uses: DeterminateSystems/nix-installer-action@main
+
+      - name: Setup Cachix
+        uses: cachix/cachix-action@v15
+        with:
+          name: hacl
+
+      - name: Build and test Eurydice against this Karamel
+        run: |
+          nix build -L --no-link \
+            "github:AeneasVerif/eurydice#checks.x86_64-linux.default" \
+            --override-input karamel "github:FStarLang/karamel/$GITHUB_SHA"
+
   # A single no-op job to use for branch protection
   ciok:
     runs-on: ubuntu-latest
     if: ${{ cancelled() || contains(needs.*.result, 'cancelled') || contains(needs.*.result, 'failure') }}
     needs:
       - build-and-test
+      - build-and-test-pulse
       - build-krmllib
+      - test-eurydice
     steps:
       # Note: this only runs when a dependency fails. If they all succeed,
       # this jobs is skipped, which counts as a success.

.gitignore

@@ -12,10 +12,11 @@ fstar-mode.el
 lib/Version.ml
 *.runlim
 karamel-nofstar.opam
-lib/AutoConfig.ml
 *.orig
 .exrc
 *.cmd
 *.err
 *.output
 *.time
+out
+krml.tar.gz

.nix/karamel.nix

@@ -65,7 +65,7 @@ in
           # the library is named `krml` rather than `karamel`
           mv karamel.opam krml.opam
           sed -i '/name krml/a (public_name krml)' lib/dune
-          make lib/Version.ml lib/AutoConfig.ml
+          make lib/Version.ml
         '';
         src = ../.;
       };

CI.md

@@ -0,0 +1,35 @@
+# Extended CI for krml
+
+In addition to the regular krml test files (`test/*.fst`), we now run three
+additional "extended" CIs, two of which track the C output to catch any code
+quality regressions.
+- Pulse-based tests (in `test/pulse`), along with the expected C
+- EverParse
+- Eurydice, which contains the expected C in its own repository
+
+# Coarse instructions for dealing with PRs that have impact on Eurydice
+
+If a PR changes the generated C code, chances are it will generate a diff in
+Eurydice, which will make the corresponding CI job fail.
+
+Because krml does *not* have a flake.lock, it always builds against Eurydice
+`main`. This means that Eurydice must be upgraded first. So, once a krml PR is
+ready to be merged:
+
+```bash
+$ cd eurydice
+$ (cd karamel && git fetch && git checkout my-pr-branch && git merge)
+$ (cd out/ && git clean -fdx)
+$ make test -j
+$ nix flake update karamel --override-input karamel "github:fstarlang/karamel/$(cd karamel && git rev-parse head)"
+$ git commit -am "Update krml to latest revision on branch my-pr-branch"
+```
+
+If the PR is being submitted from a *fork* of krml, then you must replicate the
+branch on the `fstarlang/karamel` repository (or face a two-step process on the
+Eurydice side).
+
+Then, merge the Eurydice PR and restart the krml-side PR for it to pick up the
+changes. Do NOT squash or rebase while merging otherwise the commit that
+Eurydice points to will disappear and you'll need a second PR on Eurydice to fix
+that up.

Makefile

@@ -1,49 +1,40 @@
-# Including a Makefile from the visitors package, but making sure
-# to give decent errors.
-
 # make src/Ast.processed.ml
-_:=$(shell ocamlfind query)
-ifneq ($(.SHELLSTATUS),0)
-_: $(error "'ocamlfind query' failed, please install OCaml and put it in your PATH)
-endif
-visitors_root:=$(shell ocamlfind query visitors)
-ifneq ($(.SHELLSTATUS),0)
-_: $(error "'ocamlfind query visitors' failed, please 'opam install visitors')
-endif
-include $(visitors_root)/Makefile.preprocess
+include visitors.mk
 
 .PHONY: all minimal clean test pre krmllib install
 
 FSTAR_EXE ?= fstar.exe
 
-all: minimal krmllib
+all: local-install
 
 # If we are just trying to do a minimal build, we don't need F*.
 # Note: lazy assignment so this does not warn if fstar.exe is not there
 # (e.g. on a minimal build or cleaning)
 FSTAR_OCAMLENV = $(shell $(FSTAR_EXE) --ocamlenv)
 
-minimal: lib/AutoConfig.ml lib/Version.ml
+# Creates a top-level ./krml symlink to the built Karamel executable. But, does
+# not build krmllib nor is set up in a way that allows karamel to find its
+# runtime/misc/include directories, so it is somewhat barebones.
+minimal: lib/Version.ml
 	dune build
 	ln -sf _build/default/src/Karamel.exe krml
 
 krmllib: minimal
-	$(MAKE) -C krmllib
-
-lib/AutoConfig.ml:
-	@if [ x"$(PREFIX)" != x ]; then \
-	  echo "let krmllib_dir = \"$(PREFIX)/lib/krml\";;" > $@; \
-	  echo "let runtime_dir = \"$(PREFIX)/lib/krml/runtime\";;" >> $@; \
-	  echo "let include_dir = \"$(PREFIX)/include/\";;" >> $@; \
-	  echo "let misc_dir = \"$(PREFIX)/share/krml/misc/\";;" >> $@; \
-	else \
-	  echo "let krmllib_dir = \"\";;" > $@; \
-	  echo "let runtime_dir = \"\";;" >> $@; \
-	  echo "let include_dir = \"\";;" >> $@; \
-	  echo "let misc_dir = \"\";;" >> $@; \
-	fi
-
-.PHONY: src/Version.ml
+	@# Make sure krml can find its relevant directories, since
+	@# it is not yet installed with them.
+	env \
+	  KRML_LIBDIR=$(CURDIR)/krmllib \
+	  KRML_INCLUDEDIR=$(CURDIR)/include \
+	  KRML_MISCDIR=$(CURDIR)/misc \
+	  $(MAKE) -C krmllib
+
+# A full local install. out/ will contain essentially the same directory
+# as an OPAM install or binary package.
+local-install: krmllib
+	$(MAKE) PREFIX=$(CURDIR)/out _install
+	ln -sf out/bin/krml krml
+
+.PHONY: lib/Version.ml
 lib/Version.ml:
 	@echo "let version = \"$(shell git rev-parse HEAD || echo ${GIT_REV})\"" > $@
 
@@ -56,24 +47,38 @@ clean:
 test: all
 	$(MAKE) -C test
 
+# This depends on minimal since fstar2 (with Pulse) is not expected
+# to be able to build krmllib.
+test-pulse: minimal
+	$(MAKE) -C test/pulse
+
 # Auto-detection
 pre:
 	@eval "$(FSTAR_OCAMLENV)" && \
 	ocamlfind query fstar.lib >/dev/null 2>&1 || \
 	  { echo "Didn't find fstar.lib via ocamlfind; is F* properly installed? (FSTAR_EXE = $(FSTAR_EXE))"; exit 1; }
 
-
 install: all
+	$(MAKE) _install
+
+_install:
 	@if [ x"$(PREFIX)" = x ]; then echo "please define PREFIX"; exit 1; fi
 	mkdir -p $(PREFIX)/bin
-	cp _build/default/src/Karamel.exe $(PREFIX)/bin/krml
-	mkdir -p $(PREFIX)/include
-	cp -r include/* $(PREFIX)/include
+	install _build/default/src/Karamel.exe $(PREFIX)/bin/krml
+	mkdir -p $(PREFIX)/include/krml
+	cp -r include/* $(PREFIX)/include/krml
 	mkdir -p $(PREFIX)/lib/krml
 	cp -r krmllib/* $(PREFIX)/lib/krml
-	mkdir -p $(PREFIX)/lib/krml/runtime
-	cp -r runtime/* $(PREFIX)/lib/krml/runtime
+	echo 'obj' >> $(PREFIX)/lib/krml/fstar.include
+	@# ^ So users can just --include lib/krml and also see the checked files.
 	mkdir -p $(PREFIX)/share/krml/examples
 	cp -r test/*.fst $(PREFIX)/share/krml/examples
 	mkdir -p $(PREFIX)/share/krml/misc
 	cp -r misc/* $(PREFIX)/share/krml/misc
+
+package: krml.tar.gz
+
+krml.tar.gz:
+	$(MAKE) _install PREFIX=$(CURDIR)/pkgtmp/krml
+	tar czf krml.tar.gz -C pkgtmp .
+	rm -rf pkgtmp

book/tutorial/Makefile

@@ -139,7 +139,7 @@ obj/Specs_Driver.ml: specs/ml/Specs_Driver.ml
 # F* --> C
 # --------
 
-KRML=$(KRML_HOME)/krml
+KRML_EXE ?= krml
 
 # Note: the implementation of the intrinsic uses external linkage, but you could
 # easily turn this file into a .h, use -add-include '"Impl_Bignum_Intrinsics.h"'
@@ -240,7 +240,7 @@ obj/specs-test.exe: $(ALL_CMX_FILES) obj/Specs_Driver.cmx
 # Compiling the hand-written test
 # -------------------------------
 
-CFLAGS += -I dist -I $(KRML_HOME)/include
+CFLAGS += -I dist -I $(shell $(KRML_EXE) -locate-include)
 
 tests/c-tests.exe: tests/c-tests.o dist/libbignum.a
 	$(CC) $^ -o $@