diff options
| -rw-r--r-- | Makefile | 9 | ||||
| -rw-r--r-- | flake.lock | 120 | ||||
| -rw-r--r-- | flake.nix | 32 | ||||
| -rw-r--r-- | tests/fstar/betree/Makefile | 3 | ||||
| -rw-r--r-- | tests/fstar/betree_back_stateful/Makefile | 3 | ||||
| -rw-r--r-- | tests/fstar/hashmap/Makefile | 3 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/Makefile | 3 | ||||
| -rw-r--r-- | tests/fstar/misc/Makefile | 3 |
8 files changed, 159 insertions, 17 deletions
@@ -218,5 +218,12 @@ tcoqp-%: # Nix .PHONY: nix -nix: +nix: nix-aeneas-tests nix-aeneas-verify-fstar + +.PHONY: nix-aeneas-tests +nix-aeneas-tests: nix build .#checks.x86_64-linux.aeneas-tests --show-trace -L + +.PHONY: nix-aeneas-verify-fstar +nix-aeneas-verify-fstar: + nix build .#checks.x86_64-linux.aeneas-verify-fstar --show-trace -L @@ -79,6 +79,110 @@ "type": "github" } }, + "flake-utils_2": { + "locked": { + "lastModified": 1667395993, + "narHash": "sha256-nuEHfE/LcWyuSWnS8t12N1wc105Qtau+/OdUAjtQ0rA=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "5aed5285a952e0b949eb3ba02c12fa4fcfef535f", + "type": "github" + }, + "original": { + "id": "flake-utils", + "type": "indirect" + } + }, + "fstar-src": { + "flake": false, + "locked": { + "lastModified": 1668549455, + "narHash": "sha256-WHgHYmeWwy3RfIE2pkOyLTpkhi8FXL83zO8Tv2N9Iic=", + "owner": "fstarlang", + "repo": "fstar", + "rev": "2040a595ed2faff0a1dce782fefbb518102eb1dd", + "type": "github" + }, + "original": { + "owner": "fstarlang", + "repo": "fstar", + "type": "github" + } + }, + "hacl": { + "inputs": { + "flake-utils": [ + "hacl-nix", + "flake-utils" + ], + "fstar-src": [ + "hacl-nix", + "fstar-src" + ], + "hacl-nix": [ + "hacl-nix" + ], + "karamel-src": [ + "hacl-nix", + "karamel-src" + ], + "nixpkgs": [ + "hacl-nix", + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1668456660, + "narHash": "sha256-m4/L+AgF5LaG6v82L3TpB66vv/PIORtd0XTvoOlP1Ok=", + "owner": "hacl-star", + "repo": "hacl-star", + "rev": "7241848c958eb6ae7dec0cd683852ae10a3bd799", + "type": "github" + }, + "original": { + "owner": "hacl-star", + "repo": "hacl-star", + "type": "github" + } + }, + "hacl-nix": { + "inputs": { + "flake-utils": "flake-utils_2", + "fstar-src": "fstar-src", + "hacl": "hacl", + "karamel-src": "karamel-src", + "nixpkgs": "nixpkgs_2" + }, + "locked": { + "lastModified": 1668558838, + "narHash": "sha256-etn/6ASEQFHIbTddAaHuz55/mWNz/UJcu3363YUHUOE=", + "owner": "hacl-star", + "repo": "hacl-nix", + "rev": "8f22117a9e9b2733acfa0f50fc5cf849bca18860", + "type": "github" + }, + "original": { + "owner": "hacl-star", + "repo": "hacl-nix", + "type": "github" + } + }, + "karamel-src": { + "flake": false, + "locked": { + "lastModified": 1668034772, + "narHash": "sha256-1Z3is1g0qhrn4eKFepXxD1fPhcPVIB02rAihMUU5zyc=", + "owner": "fstarlang", + "repo": "karamel", + "rev": "55b36e2c06b99f735283062e74f826d3088c2697", + "type": "github" + }, + "original": { + "owner": "fstarlang", + "repo": "karamel", + "type": "github" + } + }, "nixpkgs": { "locked": { "lastModified": 1666703756, @@ -94,6 +198,21 @@ "type": "indirect" } }, + "nixpkgs_2": { + "locked": { + "lastModified": 1667811565, + "narHash": "sha256-HYml7RdQPQ7X13VNe2CoDMqmifsXbt4ACTKxHRKQE3Q=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "667e5581d16745bcda791300ae7e2d73f49fff25", + "type": "github" + }, + "original": { + "id": "nixpkgs", + "ref": "nixos-unstable", + "type": "indirect" + } + }, "root": { "inputs": { "charon": "charon", @@ -101,6 +220,7 @@ "charon", "flake-utils" ], + "hacl-nix": "hacl-nix", "nixpkgs": [ "charon", "nixpkgs" @@ -5,9 +5,10 @@ charon.url = "github:aeneasverif/charon"; flake-utils.follows = "charon/flake-utils"; nixpkgs.follows = "charon/nixpkgs"; + hacl-nix.url = "github:hacl-star/hacl-nix"; }; - outputs = { self, charon, flake-utils, nixpkgs }: + outputs = { self, charon, flake-utils, nixpkgs, hacl-nix }: flake-utils.lib.eachSystem [ "x86_64-linux" ] (system: let pkgs = import nixpkgs { inherit system; }; @@ -40,6 +41,7 @@ echo charon.packages.${system}.tests ''; }; + # Run the translation on various files. # Make sure we don't need to recompile the package whenever we make # unnecessary changes - we list the exact files and folders the package # depends upon. @@ -54,28 +56,36 @@ || pkgs.lib.hasPrefix (toString ./tests) path; }; buildPhase = '' - # We need to provide the paths to the Charon tests derivations - export CHARON_TESTS_REGULAR_DIR=${charon.checks.${system}.tests} - export CHARON_TESTS_POLONIUS_DIR=${charon.checks.${system}.tests-polonius} + # We need to provide the paths to the Charon tests derivations + export CHARON_TESTS_REGULAR_DIR=${charon.checks.${system}.tests} + export CHARON_TESTS_POLONIUS_DIR=${charon.checks.${system}.tests-polonius} - # Copy the Aeneas executable, and update the path to it - cp ${aeneas}/bin/aeneas_driver aeneas.exe - export AENEAS_EXE=./aeneas.exe + # Copy the Aeneas executable, and update the path to it + cp ${aeneas}/bin/aeneas_driver aeneas.exe + export AENEAS_EXE=./aeneas.exe - # Run the tests - make tests + # Run the tests + make tests ''; # Tests don't generate anything new as the generated files are # versionned, but the installation phase still needs to prodocue # something, otherwise Nix will consider the build has failed. installPhase = "touch $out"; }; + # Replay the F* proofs. + aeneas-verify-fstar = pkgs.stdenv.mkDerivation { + name = "aeneas_tests"; + src = ./tests/fstar; + FSTAR_EXE = "${hacl-nix.packages.${system}.fstar}/bin/fstar.exe"; + # Tests don't generate anything + installPhase = "touch $out"; + }; in { packages = { inherit aeneas; default = aeneas; }; - checks = { inherit aeneas aeneas-tests; }; - hydraJobs = { inherit aeneas aeneas-tests; }; + checks = { inherit aeneas aeneas-tests aeneas-verify-fstar; }; + hydraJobs = { inherit aeneas aeneas-tests aeneas-verify-fstar; }; }); } diff --git a/tests/fstar/betree/Makefile b/tests/fstar/betree/Makefile index a16b0edb..14790d6d 100644 --- a/tests/fstar/betree/Makefile +++ b/tests/fstar/betree/Makefile @@ -8,7 +8,8 @@ FSTAR_OPTIONS = $(FSTAR_HINTS) \ --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ --warn_error '+241@247+285-274' \ -FSTAR_NO_FLAGS = fstar.exe --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj +FSTAR_EXE ?= fstar.exe +FSTAR_NO_FLAGS = $(FSTAR_EXE) --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS) diff --git a/tests/fstar/betree_back_stateful/Makefile b/tests/fstar/betree_back_stateful/Makefile index a16b0edb..14790d6d 100644 --- a/tests/fstar/betree_back_stateful/Makefile +++ b/tests/fstar/betree_back_stateful/Makefile @@ -8,7 +8,8 @@ FSTAR_OPTIONS = $(FSTAR_HINTS) \ --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ --warn_error '+241@247+285-274' \ -FSTAR_NO_FLAGS = fstar.exe --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj +FSTAR_EXE ?= fstar.exe +FSTAR_NO_FLAGS = $(FSTAR_EXE) --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS) diff --git a/tests/fstar/hashmap/Makefile b/tests/fstar/hashmap/Makefile index a16b0edb..14790d6d 100644 --- a/tests/fstar/hashmap/Makefile +++ b/tests/fstar/hashmap/Makefile @@ -8,7 +8,8 @@ FSTAR_OPTIONS = $(FSTAR_HINTS) \ --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ --warn_error '+241@247+285-274' \ -FSTAR_NO_FLAGS = fstar.exe --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj +FSTAR_EXE ?= fstar.exe +FSTAR_NO_FLAGS = $(FSTAR_EXE) --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS) diff --git a/tests/fstar/hashmap_on_disk/Makefile b/tests/fstar/hashmap_on_disk/Makefile index a16b0edb..14790d6d 100644 --- a/tests/fstar/hashmap_on_disk/Makefile +++ b/tests/fstar/hashmap_on_disk/Makefile @@ -8,7 +8,8 @@ FSTAR_OPTIONS = $(FSTAR_HINTS) \ --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ --warn_error '+241@247+285-274' \ -FSTAR_NO_FLAGS = fstar.exe --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj +FSTAR_EXE ?= fstar.exe +FSTAR_NO_FLAGS = $(FSTAR_EXE) --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS) diff --git a/tests/fstar/misc/Makefile b/tests/fstar/misc/Makefile index a16b0edb..14790d6d 100644 --- a/tests/fstar/misc/Makefile +++ b/tests/fstar/misc/Makefile @@ -8,7 +8,8 @@ FSTAR_OPTIONS = $(FSTAR_HINTS) \ --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ --warn_error '+241@247+285-274' \ -FSTAR_NO_FLAGS = fstar.exe --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj +FSTAR_EXE ?= fstar.exe +FSTAR_NO_FLAGS = $(FSTAR_EXE) --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS) |