proofs.yml

# This is a basic workflow to help you get started with Actions

name: Code Verification CI

# Controls when the workflow will run
on:
  # Triggers the workflow on push or pull request events but only for the develop branch
  push:

  # Allows you to run this workflow manually from the Actions tab
  #workflow_dispatch:

# A workflow run is made up of one or more jobs that can run sequentially or in parallel
jobs:

  mps-verify-cn:
    runs-on: ubuntu-22.04
    steps:
      - name: Checkout repository and submodules
        uses: actions/checkout@v4
      - name: Prove MPS Components
        uses: addnab/docker-run-action@v3
        with:
          image: ghcr.io/rems-project/cerberus/cn@sha256:7f999b2d3126458f364bfd177edeef3a161f0b4fd306e942e07d81311f24b325
          registry: ghcr.io
          options: -v ${{ github.workspace }}:/data
          # This action seems to override the docker image entrypoint, as a result
          # we need to run "eval `opam env`" first
          # Use `>` so newlines will be replaced with spaces
          run: >
            eval `opam env` &&
            cd components/mission_protection_system/src &&
            make -f cn.mk proofs

  mps-verify-frama-c:
    runs-on: ubuntu-22.04
    steps:
      - name: Checkout repository and submodules
        uses: actions/checkout@v4
      - name: Prove MPS Components
        uses: addnab/docker-run-action@v3
        with:
          image: framac/frama-c:dev
          options: -v ${{ github.workspace }}:/work -w /work
          run: |
            cd components/mission_protection_system/src
            mkdir -p /tmp/wp-session/script
            mkdir -p /tmp/wp-session/cache
            make -f frama_c.mk proofs

  secure-boot-verify-cn:
    runs-on: ubuntu-22.04
    steps:
      - name: Checkout repository and submodules
        uses: actions/checkout@v4
      - name: Prove secure boot
        uses: addnab/docker-run-action@v3
        with:
          image: ghcr.io/rems-project/cerberus/cn@sha256:7f999b2d3126458f364bfd177edeef3a161f0b4fd306e942e07d81311f24b325
          registry: ghcr.io
          options: -v ${{ github.workspace }}:/data
          # This action seems to override the docker image entrypoint, as a result
          # we need to run "eval `opam env`" first
          # Use `>` so newlines will be replaced with spaces
          run: >
            eval `opam env` &&
            cd components/platform_crypto/shave_trusted_boot &&
            make cn_proof