Merge branch 'main' into afromher_shifts

.github/workflows/ci.yml

@@ -0,0 +1,34 @@
+on:
+  push:
+    branches-ignore: [ '_**' ]
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  nix:
+    #runs-on: ubuntu-latest
+    runs-on: [self-hosted, linux, nix]
+    steps:
+      #- uses: cachix/install-nix-action@v22
+      - uses: actions/checkout@v4
+      - run: nix build -L .#aeneas
+      - run: nix build -L .#checks.x86_64-linux.aeneas-tests
+      - run: nix build -L .#checks.x86_64-linux.aeneas-verify-fstar
+      - run: nix build -L .#checks.x86_64-linux.aeneas-verify-coq
+      - run: nix build -L .#checks.x86_64-linux.aeneas-verify-hol4
+      # Lean doesn't work with Nix
+      #- run: nix build -L .#checks.x86_64-linux.aeneas-verify-lean
+  lean: # Lean isn't supported by Nix, so we put it in a different job
+    runs-on: [ubuntu-latest]
+    steps:
+      # Install curl
+      - run: sudo apt update && sudo apt install curl
+      # Install Elan (https://leanprover-community.github.io/install/linux.html) and Lean in
+      # non-interactive mode:
+      - run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | bash -s -- -y
+      # Checkout the repo and download it to the runner
+      - name: Checkout
+        uses: actions/checkout@v4
+      # Verify - note that we need to update the environment with `source` so
+      # that the lake binary is in the path.
+      - run: source ~/.profile && cd tests/lean && make

Makefile

@@ -27,14 +27,11 @@ CHARON_TESTS_POLONIUS_DIR ?= $(CHARON_HOME)/tests-polonius
 
 # The path to the Aeneas executable to run the tests - we need the ability to
 # change this path for the Nix package.
-AENEAS_EXE ?= bin/aeneas.exe
+AENEAS_EXE ?= bin/aeneas
 
 # The user can specify additional translation options for Aeneas.
-# By default we do:
-# - unfold all the monadic let bindings to matches (required by F*)
-# - insert calls to the normalizer in the translated code to test the
-#   generated unit functions
-OPTIONS +=
+# By default we activate the (expensive) sanity checks.
+OPTIONS ?= -checks
 
 #
 # The rules use (and update) the following variables
@@ -58,22 +55,25 @@ build-tests-verify: build tests verify
 
 # Build the project
 .PHONY: build
-build: build-driver build-lib build-bin-dir doc
+build: build-bin build-lib build-bin-dir doc
 
-.PHONY: build-driver
-build-driver:
-	cd compiler && dune build $(AENEAS_DRIVER)
+.PHONY: build-bin
+build-bin:
+	cd compiler && dune build
 
 .PHONY: build-lib
 build-lib:
 	cd compiler && dune build aeneas.cmxs
 
 .PHONY: build-bin-dir
-build-bin-dir: build-driver build-lib
+build-bin-dir: build-bin build-lib
 	mkdir -p bin
-	cp -f compiler/_build/default/driver.exe bin/aeneas.exe
-	cp -f compiler/_build/default/driver.exe bin/aeneas.cmxs
-	cp -rf backends bin
+	cp -f compiler/_build/default/main.exe bin/aeneas
+	cp -f compiler/_build/default/main.exe bin/aeneas.cmxs
+	mkdir -p bin/backends/fstar
+	mkdir -p bin/backends/coq
+	cp -rf backends/fstar/*.fst* bin/backends/fstar/
+	cp -rf backends/coq/*.v bin/backends/coq/
 
 .PHONY: doc
 doc:
@@ -85,13 +85,13 @@ clean:
 
 # Test the project by translating test files to F*
 .PHONY: tests
-tests: trans-no_nested_borrows trans-paper \
-	trans-hashmap trans-hashmap_main \
-	trans-external trans-constants \
-	transp-polonius_list transp-betree_main \
-	test-transp-betree_main \
-	trans-loops \
-	trans-array # TODO: generalize to all backends
+tests: test-no_nested_borrows test-paper \
+	test-hashmap test-hashmap_main \
+	test-external test-constants \
+	testp-polonius_list testp-betree_main \
+	ctest-testp-betree_main \
+	test-loops \
+	test-array test-traits # TODO: generalize to all backends
 
 # Verify the F* files generated by the translation
 .PHONY: verify
@@ -114,69 +114,83 @@ AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(BA
 
 
 # Add specific options to some tests
-trans-no_nested_borrows trans-paper: \
-	OPTIONS += -test-units -test-trans-units -no-split-files -no-state
-trans-no_nested_borrows trans-paper: SUBDIR := misc
+test-no_nested_borrows test-paper: \
+	OPTIONS += -test-trans-units
+test-no_nested_borrows test-paper: SUBDIR := misc
 tfstar-no_nested_borrows tfstar-paper:
 tlean-no_nested_borrows: SUBDIR :=
 tlean-paper: SUBDIR :=
 thol4-no_nested_borrows: SUBDIR := misc-no_nested_borrows
 thol4-paper: SUBDIR := misc-paper
 
-trans-array: OPTIONS += -no-state
-trans-array: SUBDIR := array
-tfstar-array: OPTIONS += -decreases-clauses -template-clauses
+test-array: OPTIONS +=
+test-array: SUBDIR := array
+tfstar-array: OPTIONS += -decreases-clauses -template-clauses -split-files
 tcoq-array: OPTIONS += -use-fuel
 tlean-array: SUBDIR :=
 tlean-array: OPTIONS +=
 thol4-array: OPTIONS +=
 
+test-traits: OPTIONS +=
+test-traits: SUBDIR := traits
+tfstar-traits: OPTIONS += -decreases-clauses -template-clauses
+tcoq-traits: OPTIONS +=
+tlean-traits: SUBDIR :=
+tlean-traits: OPTIONS +=
+thol4-traits: OPTIONS +=
+
 # TODO: activate the arrays for all the backends
 thol4-array:
 	echo "Ignoring the array test for HOL4"
 
-trans-loops: OPTIONS += -no-state
-trans-loops: SUBDIR := misc
-tfstar-loops: OPTIONS += -decreases-clauses -template-clauses
-tcoq-loops: OPTIONS += -use-fuel -no-split-files
+# TODO: activate the traits for all the backends
+thol4-traits:
+	echo "Ignoring the traits test for HOL4"
+
+test-loops: OPTIONS +=
+test-loops: SUBDIR := misc
+tfstar-loops: OPTIONS += -decreases-clauses -template-clauses -split-files
+tcoq-loops: OPTIONS += -use-fuel
 tlean-loops: SUBDIR :=
 thol4-loops: SUBDIR := misc-loops
 
-trans-hashmap: OPTIONS += -no-state -test-trans-units
-trans-hashmap: SUBDIR := hashmap
+# TODO: reactivate -test-trans-units
+test-hashmap: OPTIONS += -split-files
+test-hashmap: SUBDIR := hashmap
 tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses
 tcoq-hashmap: OPTIONS += -use-fuel
 tlean-hashmap: SUBDIR :=
 tlean-hashmap: OPTIONS += -no-gen-lib-entry # We add a custom import in the Hashmap.lean file: we do not want to overwrite it
 thol4-hashmap: OPTIONS +=
 
-trans-hashmap_main: OPTIONS += -test-trans-units
-trans-hashmap_main: SUBDIR := hashmap_on_disk
+# TODO: reactivate -test-trans-units
+test-hashmap_main: OPTIONS += -state -split-files
+test-hashmap_main: SUBDIR := hashmap_on_disk
 tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses
 tcoq-hashmap_main: OPTIONS += -use-fuel
 tlean-hashmap_main: SUBDIR :=
 thol4-hashmap_main: OPTIONS +=
 
-transp-polonius_list: OPTIONS += -test-units -test-trans-units -no-split-files -no-state
-transp-polonius_list: SUBDIR := misc
+testp-polonius_list: OPTIONS += -test-trans-units
+testp-polonius_list: SUBDIR := misc
 tfstarp-polonius_list: OPTIONS +=
 tcoqp-polonius_list: OPTIONS +=
 tleanp-polonius_list: SUBDIR :=
 tleanp-polonius_list: OPTIONS +=
 thol4p-polonius_list: SUBDIR := misc-polonius_list
 thol4p-polonius_list: OPTIONS +=
 
-trans-constants: OPTIONS += -test-units -test-trans-units -no-split-files -no-state
-trans-constants: SUBDIR := misc
+test-constants: OPTIONS += -test-trans-units
+test-constants: SUBDIR := misc
 tfstar-constants: OPTIONS +=
 tcoq-constants: OPTIONS +=
 tlean-constants: SUBDIR :=
 tlean-constants: OPTIONS +=
 thol4-constants: SUBDIR := misc-constants
 thol4-constants: OPTIONS +=
 
-trans-external: OPTIONS += -test-trans-units
-trans-external: SUBDIR := misc
+test-external: OPTIONS += -test-trans-units -state -split-files
+test-external: SUBDIR := misc
 tfstar-external: OPTIONS +=
 tcoq-external: OPTIONS +=
 tlean-external: SUBDIR :=
@@ -185,25 +199,25 @@ thol4-external: SUBDIR := misc-external
 thol4-external: OPTIONS +=
 
 BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses
-transp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units
-transp-betree_main: SUBDIR:=betree
+testp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -state -split-files
+testp-betree_main: SUBDIR:=betree
 tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
 tcoqp-betree_main: OPTIONS += -use-fuel
 tleanp-betree_main: SUBDIR :=
 tleanp-betree_main: OPTIONS +=
 thol4-betree_main: OPTIONS +=
 
-# Additional test on the betree: translate it without `-backward-no-state-update`.
+# Additional, *c*ustom test on the betree: translate it without `-backward-no-state-update`.
 # This generates very ugly code, but is good to test the translation.
-.PHONY: test-transp-betree_main
-test-transp-betree_main: transp-betree_main
-test-transp-betree_main: OPTIONS += -backend fstar -test-trans-units
-test-transp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
-test-transp-betree_main: BACKEND_SUBDIR := "fstar"
-test-transp-betree_main: SUBDIR:=betree_back_stateful
-test-transp-betree_main: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
-test-transp-betree_main: FILE = betree_main
-test-transp-betree_main:
+.PHONY: ctest-testp-betree_main
+ctest-testp-betree_main: testp-betree_main
+ctest-testp-betree_main: OPTIONS += -backend fstar -test-trans-units -state -split-files
+ctest-testp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
+ctest-testp-betree_main: BACKEND_SUBDIR := "fstar"
+ctest-testp-betree_main: SUBDIR:=betree_back_stateful
+ctest-testp-betree_main: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
+ctest-testp-betree_main: FILE = betree_main
+ctest-testp-betree_main:
 	$(AENEAS_CMD)
 
 # Generic rules to extract the LLBC from a rust file
@@ -220,20 +234,20 @@ gen-llbcp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
 gen-llbcp-%:
 	$(CHARON_CMD)
 
-# Generic rules to test the translation of an LLBC file.
+# Generic rules to test the testlation of an LLBC file.
 # Note that the files requiring the Polonius borrow-checker are generated
 # in the tests-polonius subdirectory.
-.PHONY: trans-%
-trans-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR)
-trans-%: FILE = $*
-trans-%: gen-llbc-% tfstar-% tcoq-% tlean-% thol4-%
+.PHONY: test-%
+test-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR)
+test-%: FILE = $*
+test-%: gen-llbc-% tfstar-% tcoq-% tlean-% thol4-%
 	echo "# Test $* done"
 
 # "p" stands for "Polonius"
-.PHONY: transp-%
-transp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
-transp-%: FILE = $*
-transp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-%
+.PHONY: testp-%
+testp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
+testp-%: FILE = $*
+testp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-%
 	echo "# Test $* done"
 
 .PHONY: tfstar-%
@@ -276,17 +290,25 @@ tleanp-%: BACKEND_SUBDIR := lean
 tleanp-%:
 	$(AENEAS_CMD)
 
+# TODO: reactivate HOL4 once traits are parameterized by their associated types
 .PHONY: thol4-%
 thol4-%: OPTIONS += -backend hol4
 thol4-%: BACKEND_SUBDIR := hol4
 thol4-%:
-	$(AENEAS_CMD)
+	echo Ignoring the $* test for HOL4
 
+#thol4-%:
+#	$(AENEAS_CMD)
+
+# TODO: reactivate HOL4 once traits are parameterized by their associated types
 .PHONY: thol4p-%
 thol4p-%: OPTIONS += -backend hol4
 thol4p-%: BACKEND_SUBDIR := hol4
 thol4p-%:
-	$(AENEAS_CMD)
+	echo Ignoring the $* test for HOL4
+
+#thol4p-%:
+#	$(AENEAS_CMD)
 
 # Nix - TODO: add the lean tests
 .PHONY: nix

README.md

@@ -17,6 +17,8 @@ internal language to a pure lamdba calculus.  It is intended to be used in combi
 representation called LLBC. It currently has backends for [F\*](https://www.fstar-lang.org),
 [Coq](https://coq.inria.fr/), [HOL4](https://hol-theorem-prover.org/) and [LEAN](https://leanprover.github.io/).
 
+If you want to contribute or ask questions, we strongly encourage you to join the [Zulip](https://aeneas-verif.zulipchat.com/).
+
 ## Project Structure
 
 - `src`: the OCaml sources. Note that we rely on [Dune](https://github.com/ocaml/dune)