CI: Run CBMC proofs for MLKEM=2,3,4 on separate EC2 instances #11
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # SPDX-License-Identifier: Apache-2.0 | ||
| name: ci-ec2-reusable | ||
| permissions: | ||
| contents: read | ||
| on: | ||
| workflow_call: | ||
| inputs: | ||
| name: | ||
| type: string | ||
| description: Alternative name of instance | ||
| default: Graviton2 | ||
| ec2_instance_type: | ||
| type: string | ||
| description: Type if EC2 instance to benchmark on | ||
| default: t4g.small | ||
| ec2_ami: | ||
| type: string | ||
| description: Textual description of AMI | ||
| default: ubuntu-latest (aarch64) | ||
| ec2_ami_id: | ||
| type: string | ||
| description: AMI ID | ||
| default: ami-096ea6a12ea24a797 | ||
| cflags: | ||
| type: string | ||
| description: Custom CFLAGS for compilation | ||
| default: "" | ||
| verbose: | ||
| description: Determine for the log verbosity | ||
| type: boolean | ||
| default: false | ||
| compile_mode: | ||
| type: string | ||
| description: either all, native, cross or none | ||
| default: all | ||
| opt: | ||
| type: string | ||
| description: either all, opt or non-opt | ||
| default: all | ||
| functest: | ||
| type: boolean | ||
| default: true | ||
| kattest: | ||
| type: boolean | ||
| default: true | ||
| nistkattest: | ||
| type: boolean | ||
| default: true | ||
| lint: | ||
| type: boolean | ||
| default: true | ||
| 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 | ||
| AMI_UBUNTU_LATEST_X86_64: ami-0e86e20dae9224db8 | ||
| AMI_UBUNTU_LATEST_AARCH64: ami-096ea6a12ea24a797 | ||
| jobs: | ||
| start-ec2-runner: | ||
| name: Start ${{ inputs.name }} (${{ inputs.ec2_instance_type }}) | ||
| permissions: | ||
| contents: 'read' | ||
| id-token: 'write' | ||
| runs-on: ubuntu-latest | ||
| outputs: | ||
| label: ${{ steps.start-ec2-runner.outputs.label }} | ||
| ec2-instance-id: ${{ steps.start-ec2-runner.outputs.ec2-instance-id }} | ||
| steps: | ||
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | ||
| - name: Determine AMI ID | ||
| id: det_ami_id | ||
| run: | | ||
| if [[ "${{ inputs.ec2_ami }}" == "ubuntu-latest (x86_64)" ]]; then | ||
| AMI_ID=${{ env.AMI_UBUNTU_LATEST_X86_64 }} | ||
| elif [[ "${{ inputs.ec2_ami }}" == "ubuntu-latest (aarch64)" ]]; then | ||
| AMI_ID=${{ env.AMI_UBUNTU_LATEST_AARCH64 }} | ||
| elif [[ "${{ inputs.ec2_ami }}" == "ubuntu-latest (custom AMI)" ]]; then | ||
| AMI_ID=${{ inputs.ec2_ami_id }} | ||
| fi | ||
| echo "Using AMI ID: $AMI_ID" | ||
| echo "AMI_ID=$AMI_ID" >> $GITHUB_OUTPUT | ||
| - name: Clear nix-installer action cache | ||
| uses: ./.github/actions/clear-cache | ||
| with: | ||
| key_prefix: determinatesystem-nix-installer- | ||
| repository: ${{ github.repository }} | ||
| gh_token: ${{ secrets.AWS_GITHUB_TOKEN }} | ||
| - name: Configure AWS credentials | ||
| uses: aws-actions/configure-aws-credentials@e3dd6a429d7300a6a4c196c26e071d42e0343502 # v4.0.2 | ||
| with: | ||
| role-to-assume: ${{ env.AWS_ROLE }} | ||
| aws-region: ${{ env.AWS_REGION }} | ||
| - name: Start EC2 runner | ||
| id: start-ec2-runner | ||
| uses: machulav/ec2-github-runner@1827d6ca7544d7044ddbd2e9360564651b463da2 # v2.3.7 | ||
| with: | ||
| mode: start | ||
| github-token: ${{ secrets.AWS_GITHUB_TOKEN }} | ||
| ec2-image-id: ${{ steps.det_ami_id.outputs.AMI_ID }} | ||
| ec2-instance-type: ${{ inputs.ec2_instance_type }} | ||
| subnet-id: subnet-07b2729e5e065962f | ||
| security-group-id: sg-0ab2e297196c8c381 | ||
| tests: | ||
| needs: start-ec2-runner | ||
| runs-on: ${{ needs.start-ec2-runner.outputs.label }} | ||
| steps: | ||
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | ||
| - name: Linting | ||
| if: ${{ inputs.lint }} | ||
| uses: ./.github/actions/lint | ||
| with: | ||
| nix-shell: ci-linter | ||
| gh_token: ${{ secrets.AWS_GITHUB_TOKEN }} | ||
| nix-verbose: ${{ inputs.verbose }} | ||
| - name: Preprocess | ||
| id: preprocess | ||
| shell: bash | ||
| run: | | ||
| echo "nix-shell=${{ inputs.cbmc && 'ci-cbmc' || 'ci' }}${{ (inputs.compile_mode == 'cross' || inputs.compile_mode == 'all') && '-cross' || '' }}" >> $GITHUB_OUTPUT | ||
| - name: Functional Tests | ||
| uses: ./.github/actions/multi-functest | ||
| with: | ||
| nix-shell: ${{ steps.preprocess.outputs.nix-shell }} | ||
| nix-cache: ${{ inputs.cbmc || inputs.compile_mode == 'cross' || inputs.compile_mode == 'all' }} | ||
| nix-verbose: ${{ inputs.verbose }} | ||
| gh_token: ${{ secrets.AWS_GITHUB_TOKEN }} | ||
| cflags: ${{ inputs.cflags }} | ||
| compile_mode: ${{ inputs.compile_mode }} | ||
| opt: ${{ inputs.opt }} | ||
| func: ${{ inputs.functest }} | ||
| kat: ${{ inputs.kattest }} | ||
| nistkat: ${{ inputs.nistkattest }} | ||
| - name: CBMC | ||
| if: ${{ inputs.cbmc && (success() || failure()) }} | ||
| uses: ./.github/actions/cbmc | ||
| 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 }}) | ||
| permissions: | ||
| contents: 'read' | ||
| id-token: 'write' | ||
| needs: | ||
| - start-ec2-runner | ||
| - tests | ||
| runs-on: ubuntu-latest | ||
| if: ${{ always() }} # required to stop the runner even if the error happened in the previous jobs | ||
| steps: | ||
| - name: Configure AWS credentials | ||
| uses: aws-actions/configure-aws-credentials@e3dd6a429d7300a6a4c196c26e071d42e0343502 # v4.0.2 | ||
| with: | ||
| role-to-assume: ${{ env.AWS_ROLE }} | ||
| aws-region: ${{ env.AWS_REGION }} | ||
| - name: Stop EC2 runner | ||
| uses: machulav/ec2-github-runner@1827d6ca7544d7044ddbd2e9360564651b463da2 # v2.3.7 | ||
| with: | ||
| mode: stop | ||
| github-token: ${{ secrets.AWS_GITHUB_TOKEN }} | ||
| label: ${{ needs.start-ec2-runner.outputs.label }} | ||
| ec2-instance-id: ${{ needs.start-ec2-runner.outputs.ec2-instance-id }} | ||
