amd64-linux.yml

name: amd64-linux

on:
  workflow_dispatch:
  push:
    branches:
      - main
  pull_request:

jobs:

  # src
  check-safety:
    runs-on: [self-hosted, linux, X64, amd64-main]
    steps:
      - name: checkout
        uses: actions/checkout@v4
      - name: preprocess
        run: make -j$JOBS -C src/ CI=1 preprocess-inplace

      - name: check safety
        run: make -j$JOBS -C src/ CI=1 check-safety
      - name: print report
        run: make -C src/ CI=1 reporter-check-safety
      - name: return error
        run: make -C src/ CI=1 err

  check-sct:
    runs-on: [self-hosted, linux, X64, amd64-main]
    steps:
      - name: checkout
        uses: actions/checkout@v4
      - name: preprocess
        run: make -j$JOBS -C src/ CI=1 preprocess-inplace

      - name: check speculative constant-time (v1)
        run: make -j$JOBS -C src/ CI=1 check-sct
      - name: print report
        run: make -C src/ CI=1 reporter-check-sct
      - name: return error
        run: make -C src/ CI=1 err

  extract-to-easycrypt:
    runs-on: [self-hosted, linux, X64, amd64-main]
    steps:
      - name: checkout
        uses: actions/checkout@v4
      - name: preprocess
        run: make -j$JOBS -C src/ CI=1 preprocess-inplace

      - name: check extraction from Jasmin to EasyCrypt
        run: make -j$JOBS -C src/ CI=1 extract-to-easycrypt
      - name: print report
        run: make -C src/ CI=1 reporter-extract-to-easycrypt
      - name: return error
        run: make -C src/ CI=1 err

  compile-src:
    runs-on: [self-hosted, linux, X64, amd64-main]
    steps:
      - name: checkout
        uses: actions/checkout@v4
      - name: preprocess
        run: make -j$JOBS -C src/ CI=1 preprocess-inplace

      - name: check compilation of libformosa25519.a
        run: make -j$JOBS -C src/ CI=1 libformosa25519.a
      - name: print report
        run: make -C src/ CI=1 reporter-compile
      - name: return error
        run: make -C src/ CI=1 err

  # test
  test:
    runs-on: [self-hosted, linux, X64, amd64-main]
    steps:
      - name: checkout
        uses: actions/checkout@v4
      - name: preprocess
        run: make -j$JOBS -C src/ CI=1 preprocess-inplace

      - name: run tests
        run: make -j$JOBS -C test/

  # bench
  bench:
    runs-on: [self-hosted, linux, X64, amd64-main]
    steps:
      - name: checkout
        uses: actions/checkout@v4
        with:
          submodules: recursive
      - name: preprocess
        run: make -j$JOBS -C src/ CI=1 preprocess-inplace

      - name: run benchmarks
        run: make -j$JOBS -C bench/

  # proof
  proof:
    runs-on: [self-hosted, linux, X64, amd64-main]
    steps:
      - name: checkout
        uses: actions/checkout@v4
      - name: preprocess
        run: make -j$JOBS -C src/ CI=1 preprocess-inplace

      - name: run proof
        run: make -j$JOBS -C proof/ all-no-report
      - name: print report
        run: make -C proof/ CI=1 reporter
      - name: return error
        run: make -C proof/ CI=1 err

  # proof (using runtest)
  proof-runtest:
    runs-on: [self-hosted, linux, X64, amd64-main]
    steps:
      - name: checkout
        uses: actions/checkout@v4
      - name: preprocess
        run: make -j$JOBS -C src/ CI=1 preprocess-inplace

      - name: run proof
        run: make -j$JOBS -C proof/ all-runtest
      - name: print report
        run: make -C proof/ CI=1 reporter
      - name: return error
        run: make -C proof/ CI=1 err