Add aeneas to CI

.github/workflows/nightly.yml

@@ -23,6 +23,10 @@ on:
         description: "Eurydice"
         type: "string"
         default: "main"
+      aeneas:
+        description: "Aeneas"
+        type: "string"
+        default: "main"
       libcrux:
         description: "Libcrux"
         type: "string"
@@ -51,6 +55,7 @@ jobs:
         env:
           HAX_BRANCH: ${{ inputs.hax }}
           CHARON_BRANCH: ${{ inputs.charon }}
+          AENEAS_BRANCH: ${{ inputs.aeneas }}
           EURYDICE_BRANCH: ${{ inputs.eurydice }}
           LIBCRUX_BRANCH: ${{ inputs.libcrux }}
           BERTIE_BRANCH: ${{ inputs.bertie }}
@@ -87,6 +92,16 @@ jobs:
           ref: nightly
       - run: ./check.sh charon
 
+  aeneas:
+    needs: update-flake
+    runs-on: [self-hosted, linux, nix]
+    steps:
+      - name: checkout
+        uses: actions/checkout@v4
+        with:
+          ref: nightly
+      - run: ./check.sh aeneas
+
   eurydice:
     needs: update-flake
     runs-on: [self-hosted, linux, nix]
@@ -118,7 +133,7 @@ jobs:
       - run: ./check.sh bertie
 
   process_results:
-    needs: [hax, charon, eurydice, ml-kem, bertie]
+    needs: [hax, charon, aeneas, eurydice, ml-kem, bertie]
     runs-on: [self-hosted, linux, nix]
     if: ${{ success() || failure() }} # Will always run unless canceled
     steps:

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" \