pulsar/.hanzo/workflows/ci.yml

name: CI

# The Go reference implementation, the spec PDF and the high-assurance gate,
# on the native runners (git.hanzo.ai → git-runner).
#
# This replaces .github/workflows/ci.yml. Every one of its five jobs named
# `runs-on: lux-build-amd64`. No runner on this forge carries that label — the
# pools are `lux-build-linux-<arch>` — and a job naming a label nothing carries
# does not fail, it waits. Every push left five jobs queued permanently, and
# these are among the longest jobs the fleet runs.
#
# Nothing else changes: the work here all earns its keep, so it moves across
# intact onto a label the fleet actually carries.

on:
  push:
    branches: [main]
    tags: ['v*']
  pull_request:
    branches: [main]
  workflow_dispatch:

permissions:
  contents: read

# A newer commit makes the older run irrelevant. These jobs are expensive
# enough that queueing them behind each other is how the pool saturates.
concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true

jobs:
  go-test:
    name: Go reference impl + KAT + Class N1 interop
    runs-on: [linux-amd64]
    timeout-minutes: 30
    steps:
      - uses: actions/checkout@v4

      - uses: actions/setup-go@v5
        with:
          go-version-file: go.mod
          cache-dependency-path: go.sum

      - name: Build (Go ref)
        run: go build ./ref/go/...

      - name: Test (Go ref, all)
        run: go test -count=1 -race -timeout=900s ./ref/go/...

      - name: KAT replay
        run: |
          set -o pipefail
          ./scripts/test.sh

  spec-pdf:
    name: spec PDF build
    runs-on: [linux-amd64]
    timeout-minutes: 30
    steps:
      - uses: actions/checkout@v4

      - name: Install TeX Live (latexmk + amsmath + cleveref + fonts)
        run: |
          sudo apt-get update
          sudo apt-get install -y --no-install-recommends \
            texlive-latex-base texlive-latex-recommended \
            texlive-latex-extra texlive-fonts-recommended \
            texlive-fonts-extra texlive-science latexmk \
            cm-super

      - name: Build pulsar.pdf
        working-directory: spec
        run: latexmk -pdf -interaction=nonstopmode -halt-on-error pulsar.tex

      - name: Upload PDF artifact
        uses: actions/upload-artifact@v4
        with:
          name: pulsar-pdf
          path: spec/pulsar.pdf
          if-no-files-found: error

  high-assurance:
    name: Jasmin type-check + EasyCrypt admit budget + EC compile
    runs-on: [linux-amd64]
    timeout-minutes: 120
    steps:
      - uses: actions/checkout@v4

      - name: Cache opam + tools
        uses: actions/cache@v4
        with:
          path: |
            ~/.opam
          key: opam-jasmin-easycrypt-${{ runner.os }}-v2

      - name: Install system deps (OCaml + Why3 SMT)
        run: |
          # Ubuntu 24.04 (noble) dropped `alt-ergo` from apt — it is installed
          # via opam in the EasyCrypt step below. apt only ships SMT solvers and
          # the opam base. libmpfr-dev + libppl-dev are required transitively by
          # the jasmin opam package (apron → mlgmpidl), and opam refuses to
          # invoke apt interactively in CI, so they are preinstalled here.
          sudo apt-get update
          sudo apt-get install -y --no-install-recommends \
            opam ocaml-nox m4 pkg-config libgmp-dev libpcre3-dev \
            libmpfr-dev libppl-dev z3 zlib1g-dev

      - name: opam init (idempotent)
        run: |
          if [ ! -d ~/.opam ]; then
            opam init --bare --disable-sandboxing --yes
          fi
          opam update -y || true

      - name: opam switch jasmin (idempotent)
        run: |
          if ! opam switch list --short | grep -q '^jasmin$' ; then
            opam switch create jasmin 4.14.2 --yes
          fi
          eval $(opam env --switch=jasmin)
          opam install jasmin --yes

      - name: Install EasyCrypt (source build)
        run: |
          eval $(opam env --switch=jasmin)
          opam install alt-ergo --yes || true
          if ! command -v easycrypt >/dev/null 2>&1; then
            git clone --depth 1 https://github.com/EasyCrypt/easycrypt.git /tmp/easycrypt-src
            cd /tmp/easycrypt-src && opam install . --yes
          fi

      - name: Configure why3 / EasyCrypt
        run: |
          eval $(opam env --switch=jasmin)
          easycrypt why3config || true

      - name: Fetch libjade (pinned commit)
        run: bash jasmin/ml-dsa-65/fetch.sh

      - name: Run high-assurance gate
        run: |
          eval $(opam env --switch=jasmin)
          bash scripts/check-high-assurance.sh

  jasmin-ct-threshold:
    # BLOCKING. The threshold .jazz files (round1, round2, combine) carry
    # explicit `#[ct = "..."]` security signatures and targeted `#declassify`
    # pragmas at the protocol-level public-output boundaries (rejection bits,
    # c_tilde, aggregates). They MUST pass `jasmin-ct` in signature-checked
    # mode (no --infer) on every push. A regression here is CI red.
    name: jasmin-ct on threshold layer (blocking)
    needs: high-assurance
    runs-on: [linux-amd64]
    timeout-minutes: 60
    steps:
      - uses: actions/checkout@v4

      - name: Restore opam cache
        uses: actions/cache@v4
        with:
          path: |
            ~/.opam
          key: opam-jasmin-easycrypt-${{ runner.os }}-v2

      - name: Fetch libjade (pinned commit)
        run: bash jasmin/ml-dsa-65/fetch.sh

      - name: jasmin-ct on threshold layer
        run: |
          eval $(opam env --switch=jasmin)
          LIBJADE="$PWD/jasmin/ml-dsa-65/libjade/oldsrc-should-delete"
          for f in jasmin/threshold/round1.jazz \
                   jasmin/threshold/round2.jazz \
                   jasmin/threshold/combine.jazz ; do
            echo "==> $f"
            jasmin-ct -I "Jade=$LIBJADE" "$f"
          done

  jasmin-ct-libjade:
    # Tracked allowed-failure for the libjade ML-DSA-65 sign source. Runs
    # jasmin-ct --infer on libjade's sign.jazz; it currently fails at
    # keygen_inner because libjade upstream lacks the public/secret annotations
    # needed to bridge the secret seed `random_zeta` through the SHAKE-based PRF
    # to the public PK components (rho, t1). Closing it requires libjade-internal
    # CT analysis we should NOT attempt blind — a misplaced `#declassify` in
    # libjade would create a real CT vulnerability.
    #
    # Tracking: https://github.com/luxfi/pulsar/issues/2
    # When libjade upstream (or a carefully audited vendor patch under
    # jasmin/ml-dsa-65/overlays/) lands the annotations, drop
    # `continue-on-error` to flip this job to blocking.
    name: jasmin-ct on libjade ML-DSA-65 sign (tracked allowed-failure, #2)
    needs: high-assurance
    runs-on: [linux-amd64]
    timeout-minutes: 60
    continue-on-error: true
    steps:
      - uses: actions/checkout@v4

      - name: Restore opam cache
        uses: actions/cache@v4
        with:
          path: |
            ~/.opam
          key: opam-jasmin-easycrypt-${{ runner.os }}-v2

      - name: Fetch libjade (pinned commit)
        run: bash jasmin/ml-dsa-65/fetch.sh

      - name: jasmin-ct on libjade sign.jazz
        id: ct
        run: |
          eval $(opam env --switch=jasmin)
          mkdir -p ct/reports
          LIBJADE="$PWD/jasmin/ml-dsa-65/libjade/oldsrc-should-delete"
          rc=0
          f="$LIBJADE/crypto_sign/dilithium/dilithium3/amd64/ref/sign.jazz"
          echo "==> $f"
          if ! jasmin-ct --infer -I "Jade=$LIBJADE" "$f" \
               2>&1 | tee "ct/reports/libjade-sign.log" ; then
            rc=2
          fi
          echo "ct-rc=$rc" >> $GITHUB_OUTPUT
          exit 0

      - name: Upload jasmin-ct report
        uses: actions/upload-artifact@v4
        with:
          name: jasmin-ct-libjade-report
          path: ct/reports/
          if-no-files-found: warn

      - name: Mark libjade CT result
        run: |
          if [[ "${{ steps.ct.outputs.ct-rc }}" = "2" ]]; then
            echo "::warning::jasmin-ct on libjade ML-DSA-65 sign reports findings — see artifact 'jasmin-ct-libjade-report'. Tracked under issue #2."
          else
            echo "::notice::jasmin-ct clean on libjade ML-DSA-65 sign. This job can be flipped to blocking."
          fi