From 486076de72f32ab96f24e576557ffe5889245c94 Mon Sep 17 00:00:00 2001
From: Hanno Becker <beckphan@amazon.co.uk>
Date: Tue, 5 Nov 2024 07:04:52 +0000
Subject: [PATCH] CI: Run CBMC proofs for MLKEM=2,3,4 on separate EC2 instances

By now, the CBMC proofs take more than >40min. This commit
- Spawns separate instances for MLKEM_K=2,3,4 CBMC proofs
- Uses -j8 to enable multicore checking

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
---
 .github/actions/cbmc/action.yml       | 11 +++---
 .github/workflows/ci.yml              | 48 +++++++++++++++++++++++++--
 .github/workflows/ci_ec2_reusable.yml |  4 +++
 3 files changed, 55 insertions(+), 8 deletions(-)

diff --git a/.github/actions/cbmc/action.yml b/.github/actions/cbmc/action.yml
index bc7025ede..b1b768564 100644
--- a/.github/actions/cbmc/action.yml
+++ b/.github/actions/cbmc/action.yml
@@ -16,6 +16,9 @@ inputs:
   custom_shell:
     description: The shell to use. Only relevant if use-nix is 'false'
     default: "bash"
+  mlkem_k:
+    description: "Security level for ML-KEM (2,3,4)"
+    default: "2"
   gh_token:
     description: Github access token to use
     required: true
@@ -40,12 +43,10 @@ runs:
               - Cadical Version $(cadical --version)
               - $(bash --version | grep -m1 "")
             EOF
-      - name: Run CBMC proofs
+      - name: Run CBMC proofs (MLKEM_K=${{ inputs.mlkem_k }})
         shell: ${{ env.SHELL }}
         run: |
           cd cbmc/proofs;
-          echo "::group::cbmc"
-          MLKEM_K=2 ./run-cbmc-proofs.py --summarize;
-          MLKEM_K=3 ./run-cbmc-proofs.py --summarize;
-          MLKEM_K=4 ./run-cbmc-proofs.py --summarize;
+          echo "::group::cbmc_${{ inputs.mlkem_k }}"
+          MLKEM_K=${{ inputs.mlkem_k }} ./run-cbmc-proofs.py --summarize -j8;
           echo "::endgroup::"
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 335f40ccd..715c13dfd 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -233,7 +233,7 @@ jobs:
       lint: false
       verbose: true
     secrets: inherit
-  cbmc:
+  cbmc_k2:
     needs: quickcheck
     permissions:
       contents: 'read'
@@ -241,7 +241,7 @@ jobs:
     uses: ./.github/workflows/ci_ec2_reusable.yml
     if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
     with:
-      name: CBMC
+      name: CBMC (MLKEM-512)
       ec2_instance_type: c7g.4xlarge
       ec2_ami: ubuntu-latest (custom AMI)
       ec2_ami_id: ami-08ddb0acd99dc3d33 # aarch64, ubuntu-latest, 64g
@@ -252,5 +252,47 @@ jobs:
       functest: true
       kattest: false
       nistkattest: false
-      cbmc: true
+      cbmc: 2
+    secrets: inherit
+  cbmc_k3:
+    needs: quickcheck
+    permissions:
+      contents: 'read'
+      id-token: 'write'
+    uses: ./.github/workflows/ci_ec2_reusable.yml
+    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
+    with:
+      name: CBMC (MLKEM-768)
+      ec2_instance_type: c7g.4xlarge
+      ec2_ami: ubuntu-latest (custom AMI)
+      ec2_ami_id: ami-08ddb0acd99dc3d33 # aarch64, ubuntu-latest, 64g
+      compile_mode: native
+      opt: non-opt
+      lint: false
+      verbose: true
+      functest: true
+      kattest: false
+      nistkattest: false
+      cbmc: 3
+    secrets: inherit
+  cbmc_k4:
+    needs: quickcheck
+    permissions:
+      contents: 'read'
+      id-token: 'write'
+    uses: ./.github/workflows/ci_ec2_reusable.yml
+    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
+    with:
+      name: CBMC (MLKEM-1024)
+      ec2_instance_type: c7g.4xlarge
+      ec2_ami: ubuntu-latest (custom AMI)
+      ec2_ami_id: ami-08ddb0acd99dc3d33 # aarch64, ubuntu-latest, 64g
+      compile_mode: native
+      opt: non-opt
+      lint: false
+      verbose: true
+      functest: true
+      kattest: false
+      nistkattest: false
+      cbmc: 4
     secrets: inherit
diff --git a/.github/workflows/ci_ec2_reusable.yml b/.github/workflows/ci_ec2_reusable.yml
index 1d3cd8960..47fe2e1f7 100644
--- a/.github/workflows/ci_ec2_reusable.yml
+++ b/.github/workflows/ci_ec2_reusable.yml
@@ -53,6 +53,9 @@ on:
       cbmc:
         type: boolean
         default: false
+      cbmc_mlkem_k:
+        type string
+        default: '2'
 env:
   AWS_ROLE: arn:aws:iam::559050233797:role/mlkem-c-aarch64-gh-action
   AWS_REGION: us-east-1
@@ -139,6 +142,7 @@ jobs:
         with:
           nix-shell: ${{ steps.preprocess.outputs.nix-shell }}
           nix-verbose: ${{ inputs.verbose }}
+          mlkem_k: ${{ inputs.cbmc_mlkem_k }}
           gh_token: ${{ secrets.AWS_GITHUB_TOKEN }}
   stop-ec2-runner:
     name: Stop ${{ inputs.name }} (${{ inputs.ec2_instance_type }})