summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile6
-rw-r--r--flake.lock373
-rw-r--r--flake.nix28
3 files changed, 388 insertions, 19 deletions
diff --git a/Makefile b/Makefile
index 26daadac..a05ba185 100644
--- a/Makefile
+++ b/Makefile
@@ -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
diff --git a/flake.lock b/flake.lock
index a05dbd50..4112d86f 100644
--- a/flake.lock
+++ b/flake.lock
@@ -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",
diff --git a/flake.nix b/flake.nix
index 8fb20372..8ebbca73 100644
--- a/flake.nix
+++ b/flake.nix
@@ -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; };
});
}