diff options
| -rw-r--r-- | Makefile | 6 | ||||
| -rw-r--r-- | flake.lock | 373 | ||||
| -rw-r--r-- | flake.nix | 28 |
3 files changed, 388 insertions, 19 deletions
@@ -262,7 +262,7 @@ tleanp-%: # Nix .PHONY: nix -nix: nix-aeneas-tests nix-aeneas-verify-fstar nix-aeneas-verify-coq +nix: nix-aeneas-tests nix-aeneas-verify-fstar nix-aeneas-verify-coq nix-aeneas-verify-lean .PHONY: nix-aeneas-tests nix-aeneas-tests: @@ -275,3 +275,7 @@ nix-aeneas-verify-fstar: .PHONY: nix-aeneas-verify-coq nix-aeneas-verify-coq: nix build .#checks.x86_64-linux.aeneas-verify-coq --show-trace -L + +.PHONY: nix-aeneas-verify-lean +nix-aeneas-verify-lean: + nix build .#checks.x86_64-linux.aeneas-verify-lean --show-trace -L @@ -8,11 +8,11 @@ "rust-overlay": "rust-overlay_2" }, "locked": { - "lastModified": 1678136172, - "narHash": "sha256-4XFs4MKtOmJTrer+uIz1t3XP+DeN72Kr6FZB5tdX3Zg=", + "lastModified": 1679487286, + "narHash": "sha256-CSg7RD174YC2Vf/qPb3aRcabFaT9vYDm1HnJrlWhyAE=", "owner": "aeneasverif", "repo": "charon", - "rev": "f2436fd2002084e6e966918ff462eb436f1c64a4", + "rev": "0f33a841710dfabf2557e7cfb30c820027ca56d1", "type": "github" }, "original": { @@ -93,17 +93,65 @@ "type": "indirect" } }, + "flake-utils_3": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1681202837, + "narHash": "sha256-H+Rh19JDwRtpVPAWp64F+rlEtxUWBAQW28eAi3SRSzg=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "cfacdce06f30d2b68473a46042957675eebb3401", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "flake-utils_4": { + "locked": { + "lastModified": 1656928814, + "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "flake-utils_5": { + "locked": { + "lastModified": 1656928814, + "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, "fstar": { "inputs": { "flake-utils": "flake-utils_2", "nixpkgs": "nixpkgs_2" }, "locked": { - "lastModified": 1678051679, - "narHash": "sha256-AC8dzASxvQQDB1KpBVGRG3Sa/9HZv6Xu+77MA6nbsAw=", + "lastModified": 1683501815, + "narHash": "sha256-+DX6VE4CmO5+n+Vp+BJi0qLWh8BJZk5i3SqKUjhRMBg=", "owner": "fstarlang", "repo": "fstar", - "rev": "72e1dc828d2b79234bd5cf26f011f877280f581f", + "rev": "3f1c7aecb2f24ec907cdcb1c480f2aa67b087063", "type": "github" }, "original": { @@ -132,11 +180,11 @@ ] }, "locked": { - "lastModified": 1678019549, - "narHash": "sha256-TWym/lTC22Y9rXKZZqpN/RR+UzcY2ftcxrc1+uNogkM=", + "lastModified": 1683481401, + "narHash": "sha256-NEFEEjDDew6Q8p4zExOX2FBXcqoZrz1yVZFWIH0kFyA=", "owner": "hacl-star", "repo": "hacl-star", - "rev": "5ea164d21c553bd3703ed31be9163ad66c2ba0d9", + "rev": "f55deda4d9ce1f06c71d23180911163a75c85c85", "type": "github" }, "original": { @@ -162,11 +210,11 @@ ] }, "locked": { - "lastModified": 1678067125, - "narHash": "sha256-4cU6Ic8273l4X38YAX2jDL3pA3iR4gxgoZIpt5lsEc0=", + "lastModified": 1683508931, + "narHash": "sha256-EbwwSDubjm12tyWcxhjwWsmgzuI1M5pVdO+9k+hPXZ0=", "owner": "hacl-star", "repo": "hacl-nix", - "rev": "b30ddd505375c203bbf33445a7755b705b2a900a", + "rev": "4f427b15b3c0766938b0ba387a0716991a18e692", "type": "github" }, "original": { @@ -191,11 +239,11 @@ ] }, "locked": { - "lastModified": 1677084714, - "narHash": "sha256-yjeq6lUpJpqRmL9UIBSoFLbi8TLNY7vsCH2E1SrSfYI=", + "lastModified": 1683133881, + "narHash": "sha256-dSAuF9gVDxsolPOS6h7Z5iL04KK69VJkhq7xNtCL0KQ=", "owner": "fstarlang", "repo": "karamel", - "rev": "bd359d86d59401b001788468fa7366e741836c02", + "rev": "8cf8b4e569f5690c51a5954695dcb7fc622cf77b", "type": "github" }, "original": { @@ -204,6 +252,172 @@ "type": "github" } }, + "lake": { + "inputs": { + "flake-utils": "flake-utils_3", + "lean": "lean", + "nixpkgs": "nixpkgs_5" + }, + "locked": { + "lastModified": 1681865920, + "narHash": "sha256-jaZ2QpZxG4OGeJW8T5WFw+eAt09GDbk0sStc7WCoxsg=", + "owner": "leanprover", + "repo": "lake", + "rev": "257fc59a6464f5732a4f49e7dda0fc37475819fb", + "type": "github" + }, + "original": { + "owner": "leanprover", + "repo": "lake", + "type": "github" + } + }, + "lean": { + "inputs": { + "flake-utils": "flake-utils_4", + "lean4-mode": "lean4-mode", + "nix": "nix", + "nixpkgs": "nixpkgs_4" + }, + "locked": { + "lastModified": 1683577548, + "narHash": "sha256-kujPgXEoXUsUt7MIwIaOjNLSIkHpqx7o8kT01nRIpYM=", + "owner": "leanprover", + "repo": "lean4", + "rev": "ad4b822734adfd7800194eb574b31fe540923302", + "type": "github" + }, + "original": { + "owner": "leanprover", + "repo": "lean4", + "type": "github" + } + }, + "lean4-mode": { + "flake": false, + "locked": { + "lastModified": 1676498134, + "narHash": "sha256-u3WvyKxOViZG53hkb8wd2/Og6muTecbh+NdflIgVeyk=", + "owner": "leanprover", + "repo": "lean4-mode", + "rev": "2c6ef33f476fdf5eb5e4fa4fa023ba8b11372440", + "type": "github" + }, + "original": { + "owner": "leanprover", + "repo": "lean4-mode", + "type": "github" + } + }, + "lean4-mode_2": { + "flake": false, + "locked": { + "lastModified": 1676498134, + "narHash": "sha256-u3WvyKxOViZG53hkb8wd2/Og6muTecbh+NdflIgVeyk=", + "owner": "leanprover", + "repo": "lean4-mode", + "rev": "2c6ef33f476fdf5eb5e4fa4fa023ba8b11372440", + "type": "github" + }, + "original": { + "owner": "leanprover", + "repo": "lean4-mode", + "type": "github" + } + }, + "lean_2": { + "inputs": { + "flake-utils": "flake-utils_5", + "lean4-mode": "lean4-mode_2", + "nix": "nix_2", + "nixpkgs": "nixpkgs_7" + }, + "locked": { + "lastModified": 1683577548, + "narHash": "sha256-kujPgXEoXUsUt7MIwIaOjNLSIkHpqx7o8kT01nRIpYM=", + "owner": "leanprover", + "repo": "lean4", + "rev": "ad4b822734adfd7800194eb574b31fe540923302", + "type": "github" + }, + "original": { + "owner": "leanprover", + "repo": "lean4", + "type": "github" + } + }, + "lowdown-src": { + "flake": false, + "locked": { + "lastModified": 1633514407, + "narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=", + "owner": "kristapsdz", + "repo": "lowdown", + "rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8", + "type": "github" + }, + "original": { + "owner": "kristapsdz", + "repo": "lowdown", + "type": "github" + } + }, + "lowdown-src_2": { + "flake": false, + "locked": { + "lastModified": 1633514407, + "narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=", + "owner": "kristapsdz", + "repo": "lowdown", + "rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8", + "type": "github" + }, + "original": { + "owner": "kristapsdz", + "repo": "lowdown", + "type": "github" + } + }, + "nix": { + "inputs": { + "lowdown-src": "lowdown-src", + "nixpkgs": "nixpkgs_3", + "nixpkgs-regression": "nixpkgs-regression" + }, + "locked": { + "lastModified": 1657097207, + "narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=", + "owner": "NixOS", + "repo": "nix", + "rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f", + "type": "github" + }, + "original": { + "owner": "NixOS", + "repo": "nix", + "type": "github" + } + }, + "nix_2": { + "inputs": { + "lowdown-src": "lowdown-src_2", + "nixpkgs": "nixpkgs_6", + "nixpkgs-regression": "nixpkgs-regression_2" + }, + "locked": { + "lastModified": 1657097207, + "narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=", + "owner": "NixOS", + "repo": "nix", + "rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f", + "type": "github" + }, + "original": { + "owner": "NixOS", + "repo": "nix", + "type": "github" + } + }, "nixpkgs": { "locked": { "lastModified": 1673134516, @@ -219,6 +433,38 @@ "type": "indirect" } }, + "nixpkgs-regression": { + "locked": { + "lastModified": 1643052045, + "narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2", + "type": "github" + }, + "original": { + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2", + "type": "github" + } + }, + "nixpkgs-regression_2": { + "locked": { + "lastModified": 1643052045, + "narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2", + "type": "github" + }, + "original": { + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2", + "type": "github" + } + }, "nixpkgs_2": { "locked": { "lastModified": 1669140675, @@ -234,6 +480,86 @@ "type": "indirect" } }, + "nixpkgs_3": { + "locked": { + "lastModified": 1653988320, + "narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-22.05-small", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs_4": { + "locked": { + "lastModified": 1657208011, + "narHash": "sha256-BlIFwopAykvdy1DYayEkj6ZZdkn+cVgPNX98QVLc0jM=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "2770cc0b1e8faa0e20eb2c6aea64c256a706d4f2", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixpkgs-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs_5": { + "locked": { + "lastModified": 1659914493, + "narHash": "sha256-lkA5X3VNMKirvA+SUzvEhfA7XquWLci+CGi505YFAIs=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "022caabb5f2265ad4006c1fa5b1ebe69fb0c3faf", + "type": "github" + }, + "original": { + "owner": "nixos", + "ref": "nixos-21.05", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs_6": { + "locked": { + "lastModified": 1653988320, + "narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-22.05-small", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs_7": { + "locked": { + "lastModified": 1657208011, + "narHash": "sha256-BlIFwopAykvdy1DYayEkj6ZZdkn+cVgPNX98QVLc0jM=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "2770cc0b1e8faa0e20eb2c6aea64c256a706d4f2", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixpkgs-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, "root": { "inputs": { "charon": "charon", @@ -242,6 +568,8 @@ "flake-utils" ], "hacl-nix": "hacl-nix", + "lake": "lake", + "lean": "lean_2", "nixpkgs": [ "charon", "nixpkgs" @@ -299,6 +627,21 @@ "repo": "rust-overlay", "type": "github" } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } } }, "root": "root", @@ -2,13 +2,19 @@ description = "Aeneas"; inputs = { + # Remark: when adding inputs here, don't forget to also add them in the list + # of outputs below! charon.url = "github:aeneasverif/charon"; flake-utils.follows = "charon/flake-utils"; nixpkgs.follows = "charon/nixpkgs"; hacl-nix.url = "github:hacl-star/hacl-nix"; + lean.url = "github:leanprover/lean4"; + lake.url = "github:leanprover/lake"; }; - outputs = { self, charon, flake-utils, nixpkgs, hacl-nix }: + # Remark: keep the list of outputs in sync with the list of inputs above + # (see above remark) + outputs = { self, charon, flake-utils, nixpkgs, hacl-nix, lean, lake }: flake-utils.lib.eachSystem [ "x86_64-linux" ] (system: let pkgs = import nixpkgs { inherit system; }; @@ -115,12 +121,28 @@ # The tests don't generate anything installPhase = "touch $out"; }; + # Replay the Lean proofs. + aeneas-verify-lean = pkgs.stdenv.mkDerivation { + name = "aeneas_verify_lean"; + src = ./tests/lean; + #LAKE_EXE = lean.packages.${system}; + #buildInputs = [lean.packages.${system}.lake-dev]; + buildInputs = [lean.packages.${system} lake.packages.${system}.cli]; + #buildInputs = [lake.packages.${system}.cli]; + buildPhase= '' + make prepare-projects + #make verify -j $NIX_BUILD_CORES + make verify + ''; + # The tests don't generate anything + installPhase = "touch $out"; + }; in { packages = { inherit aeneas; default = aeneas; }; - checks = { inherit aeneas aeneas-tests aeneas-verify-fstar aeneas-verify-coq; }; - hydraJobs = { inherit aeneas aeneas-tests aeneas-verify-fstar aeneas-verify-coq; }; + checks = { inherit aeneas aeneas-tests aeneas-verify-fstar aeneas-verify-coq aeneas-verify-lean; }; + hydraJobs = { inherit aeneas aeneas-tests aeneas-verify-fstar aeneas-verify-coq aeneas-verify-lean; }; }); } |