Add aeneas to CI

flake.nix

@@ -18,6 +18,12 @@
       inputs.rust-overlay.follows = "rust-overlay";
       inputs.crane.follows = "crane";
     };
+    aeneas = {
+      url = "github:aeneasverif/aeneas";
+      inputs.nixpkgs.follows = "nixpkgs";
+      inputs.charon.follows = "charon";
+      inputs.fstar.follows = "fstar";
+    };
     eurydice = {
       url = "github:aeneasverif/eurydice";
       # If we override this, we would need to override karamel's nixpkgs too to
@@ -61,6 +67,7 @@
       packages = {
         hax = inputs.hax.packages.${system}.hax;
         charon = inputs.charon.packages.${system}.default;
+        aeneas = inputs.aeneas.packages.${system}.default;
         eurydice = inputs.eurydice.packages.${system}.default;
         ml-kem = inputs.libcrux.packages.${system}.ml-kem.override {
           cargoLock = ./libcrux-Cargo.lock;
@@ -71,6 +78,7 @@
       checks = rec {
         hax = inputs.hax.checks.${system}.toolchain;
         charon = inputs.charon.checks.${system}.charon-ml-tests;
+        aeneas = inputs.aeneas.checks.${system}.default;
         eurydice = inputs.eurydice.checks.${system}.default;
         ml-kem = packages.ml-kem;
         ml-kem-small = ml-kem.override {

message.sh

@@ -18,7 +18,7 @@ echo "run: https://github.com/inria-prosecco/circus-green/actions/runs/$RUN"
 echo ""
 
 echo "*Statuses:*"
-for project in hax charon eurydice ml-kem bertie; do
+for project in hax charon aeneas eurydice ml-kem bertie; do
     status="$(jq -r 'if .["'"$project"'"].result == "success" then "✅" else "❌" end' results.json)"
     echo "$status $project (main)"
 done
@@ -28,7 +28,7 @@ echo "*Tried to update:*"
 git show origin/main:flake.lock > good.lock
 cat flake.lock good.lock | jq -s -r '
     map( .nodes |
-         [ .fstar, .karamel, .hax, .charon, .eurydice, .libcrux, .bertie ] |
+         [ .fstar, .karamel, .hax, .charon, .aeneas, .eurydice, .libcrux, .bertie ] |
          map( .locked )
     )
     | transpose

update.sh

@@ -4,6 +4,7 @@ FSTAR_BRANCH="${FSTAR_BRANCH:-master}"
 KARAMEL_BRANCH="${KARAMEL_BRANCH:-master}"
 HAX_BRANCH="${HAX_BRANCH:-main}"
 CHARON_BRANCH="${CHARON_BRANCH:-main}"
+AENEAS_BRANCH="${AENEAS_BRANCH:-main}"
 EURYDICE_BRANCH="${EURYDICE_BRANCH:-main}"
 LIBCRUX_BRANCH="${LIBCRUX_BRANCH:-main}"
 BERTIE_BRANCH="${BERTE_BRANCH:-main}"
@@ -12,6 +13,7 @@ BERTIE_BRANCH="${BERTE_BRANCH:-main}"
 nix flake update \
    --override-input hax "github:hacspec/hax?ref=$HAX_BRANCH" \
    --override-input charon "github:aeneasverif/charon?ref=$CHARON_BRANCH" \
+   --override-input aeneas "github:aeneasverif/aeneas?ref=$AENEAS_BRANCH" \
    --override-input eurydice "github:aeneasverif/eurydice?ref=$EURYDICE_BRANCH" \
    --override-input eurydice/karamel "github:FStarLang/karamel?ref=$KARAMEL_BRANCH" \
    --override-input eurydice/karamel/fstar "github:FStarLang/fstar?ref=$FSTAR_BRANCH" \