main.yml

# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
# SPDX-License-Identifier: Apache-2.0


# This workflow checks out the repository and runs an action that starts up the dockerfile for proofs

name: CI

# Controls when the action will run. Triggers the workflow on push or pull request
# events but only for the master branch
on: [push, pull_request]

# A workflow run is made up of one or more jobs that can run sequentially or in parallel
jobs:
  
  saw-x86_64:
    # The type of runner that the job will run on
    runs-on: aws-lc-verification_ubuntu-latest_16-core

    # Steps represent a sequence of tasks that will be executed as part of the job
    steps:
    # Check out main repo and submodules.
    - uses: actions/checkout@v2
      name: check out top-level repository and all submodules
      with:
        submodules: true

    # Runs the formal verification action
    - name: SAW X86_64 Proofs
      uses: ./.github/actions/SAW_X86_64
  saw-x86_64-aes-gcm:
    # The type of runner that the job will run on
    runs-on: aws-lc-verification_ubuntu-latest_16-core

    # Steps represent a sequence of tasks that will be executed as part of the job
    steps:
    # Check out main repo and submodules.
    - uses: actions/checkout@v2
      name: check out top-level repository and all submodules
      with:
        submodules: true

    # Runs the formal verification action
    - name: SAW X86_64 AES-GCM Proof
      uses: ./.github/actions/SAW_X86_64_AES_GCM
  saw-aarch64:
    # The type of runner that the job will run on
    runs-on: aws-lc-verification_ubuntu-latest_16-core

    # Steps represent a sequence of tasks that will be executed as part of the job
    steps:
    # Check out main repo and submodules.
    - uses: actions/checkout@v2
      name: check out top-level repository and all submodules
      with:
        submodules: true

    # Runs the formal verification action
    - name: SAW AARCH64 Proofs
      uses: ./.github/actions/SAW_AARCH64
  coq:
    # The type of runner that the job will run on
    runs-on: aws-lc-verification_ubuntu-latest_16-core

    # Steps represent a sequence of tasks that will be executed as part of the job
    steps:
    # Checkout main repo and submodules
    - uses: actions/checkout@v2
      name: check out top-level repository
      with:
        submodules: true

    # Check out fiat-crypto submodule recursively 
    - name: recursively check out fiat-crypto submodule
      run: |
        git submodule update --init --recursive Coq/fiat-crypto

    # Runs the formal verification action
    - name: Coq Proofs
      uses: ./.github/actions/Coq
  nsym:
    # The type of runner that the job will run on
    runs-on: aws-lc-verification_ubuntu-latest_16-core

    # Steps represent a sequence of tasks that will be executed as part of the job
    steps:
    # Check out main repo and submodules.
    - uses: actions/checkout@v2
      name: check out top-level repository and all submodules
      with:
        submodules: true

    # Runs the formal verification action
    - name: NSym Proofs
      uses: ./.github/actions/NSym