ci.yml

name: Cargo Build & Test

on:
  push:
    branches:
      - main
      - dev
    tags:
      - v[0-9]+.*
  pull_request:
    branches:
      - main
      - dev
      - gc-v2

env:
  CARGO_TERM_COLOR: always

concurrency:
  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
  cancel-in-progress: true

jobs:
  # Runs first and gates everything else (fmt/clippy/test all `needs: tla-plus`
  # below) - it's the fastest job (seconds, no Rust toolchain to build) and a
  # failure here means either a real regression the other, much slower jobs
  # can't catch, or a stale/broken spec - either way not worth burning 30+
  # minutes of Cargo Test/Clippy compute on before finding out.
  #
  # All 8 findings from audit/TLAPlus-20260630.md were fixed in commit
  # 991faaa, so this job is expected to be GREEN. Its steps still run every
  # bug config that reproduced the original counterexamples, but a bug
  # config correctly still failing is no longer treated as a job failure -
  # see the second step's own comment for why (its constants are frozen
  # historical snapshots, not a live read of the Rust source, so they can't
  # detect a regression by staying red; only an unexpected PASS is a real
  # drift signal now).
  tla-plus:
    name: TLA+ Formal Verification
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v5
      - uses: actions/setup-java@v4
        with:
          distribution: temurin
          java-version: "21"
      - name: Download TLA+ tools
        run: |
          mkdir -p ~/.local/share/tlaplus
          curl -sL -o ~/.local/share/tlaplus/tla2tools.jar \
            https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar
      # This audit pass proves bugs exist in CURRENT code and proves correct
      # fix designs for them - the fixes are NOT yet applied to the Rust code
      # (see node/README.md's "Known gap" sections). These configs model the
      # verified fix designs (or a baseline that was never buggy) and must
      # always pass. See root README.md's "Formal verification (TLA+)"
      # section for what each spec covers.
      - name: Run baseline + proposed-fix specs (must pass)
        working-directory: node/tla
        run: |
          set -e
          JAR=~/.local/share/tlaplus/tla2tools.jar
          java -jar "$JAR" -config GraphLifecycleCoreOnly.cfg GraphLifecycle.tla
          java -jar "$JAR" -config GraphLifecycleFixed.cfg GraphLifecycle.tla
          java -jar "$JAR" -config GraphLifecycleFineGrainedFixed.cfg GraphLifecycleFineGrainedFixed.tla
          java -jar "$JAR" -config InstancePresignedFixed.cfg InstancePresigned.tla
          java -jar "$JAR" -config Take2DisproveRace.cfg Take2DisproveRace.tla
          java -jar "$JAR" -config MultiActorRace.cfg MultiActorRace.tla
          java -jar "$JAR" -config InstanceBridgeOutRaceFixed.cfg InstanceBridgeOutRace.tla
          java -jar "$JAR" -config MessageStateRaceFixed.cfg MessageStateRace.tla
          java -jar "$JAR" -config Take1ChallengeRaceFixed.cfg Take1ChallengeRace.tla
      # This job's earlier design (while all 8 findings from this round were
      # still genuinely unfixed) made this step - and everything gated
      # behind it - fail for as long as any bug config still reproduced its
      # counterexample. As of commit 991faaa, every one of those findings
      # has actually been fixed in the shipped Rust code (see
      # audit/TLAPlus-20260630.md) - keeping the job permanently red past
      # that point stopped being useful: these bug configs' constants are
      # frozen historical snapshots (e.g. Take1ChallengeRace.tla's
      # ConnectorA), not live readings of the current Rust source, so they
      # can never detect a real code regression by themselves - they will
      # keep reproducing the same counterexample forever regardless of
      # what the Rust code does. Their only genuine ongoing signal is the
      # OPPOSITE direction: if one of them ever unexpectedly STOPS
      # reproducing its counterexample, that means the spec itself was
      # edited into no longer demonstrating the bug it's supposed to -
      # that's the one case this step still treats as a hard failure.
      # Otherwise, a bug config correctly still failing is expected and
      # does not fail the job - it's just printed as an informational
      # reproduction pointer.
      - name: Confirm known-bug specs still reproduce their counterexample
        working-directory: node/tla
        run: |
          JAR=~/.local/share/tlaplus/tla2tools.jar
          {
            echo "## TLA+ audit: historical bug-reproduction specs"
            echo
            echo "These model the PRE-FIX code as a permanent historical record (all"
            echo "findings below were fixed in commit 991faaa - see"
            echo "\`audit/TLAPlus-20260630.md\`). Still correctly reproducing their"
            echo "original counterexample below is expected and does not fail this job."
            echo
          } >> "$GITHUB_STEP_SUMMARY"
          while IFS='|' read -r cfg tla finding; do
            [ -z "$cfg" ] && continue
            if java -jar "$JAR" -config "$cfg" "$tla" | grep -q "Model checking completed. No error has been found."; then
              echo "::error::$tla / $cfg was expected to keep reproducing its historical counterexample but passed instead - the spec itself was likely edited into no longer demonstrating the bug it's supposed to. If the underlying Rust fix was somehow reverted, this is also how you'd find out - either way, investigate before trusting this spec again."
              exit 1
            fi
            repro="cd node/tla && java -jar ~/.local/share/tlaplus/tla2tools.jar -config $cfg $tla"
            echo "- **$finding** - reproduce: \`$repro\`" >> "$GITHUB_STEP_SUMMARY"
          done <<'BUGS'
          GraphLifecycle.cfg|GraphLifecycle.tla|Finding 1: Graph.status race
          GraphLifecycleFineGrained.cfg|GraphLifecycleFineGrained.tla|Finding 1b: naive guard still unsafe
          InstancePresignedBug.cfg|InstancePresigned.tla|Finding 2: Instance.status regression past Presigned
          InstanceBridgeOutRace.cfg|InstanceBridgeOutRace.tla|Finding 6: InstanceBridgeOutStatus resurrection
          MessageStateRace.cfg|MessageStateRace.tla|Finding 7: MessageState resurrection
          Take1ChallengeRace.cfg|Take1ChallengeRace.tla|Finding 9: connector_a has no margin check
          BUGS
  fmt:
    name: Rustfmt
    needs: tla-plus
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v5
      - uses: actions-rs/toolchain@v1
        timeout-minutes: 30
        with:
          profile: minimal
          toolchain: stable
          override: true
      - run: rustup component add rustfmt
      - uses: actions-rs/cargo@v1
        with:
          command: fmt
          args: --all -- --check
  clippy:
    name: Clippy
    needs: tla-plus
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v5
      - uses: actions-rs/toolchain@v1
        timeout-minutes: 30
        with:
          profile: minimal
          toolchain: nightly-2025-12-11
          override: true
          components: clippy
      - run: curl --proto '=https' --tlsv1.2 -sSf https://raw.githubusercontent.com/ProjectZKM/toolchain/refs/heads/main/setup.sh | sh
      - name: Install Dependencies
        run: sudo apt update && sudo apt install protobuf-compiler
      - run: |
          source ~/.zkm-toolchain/env
          cargo clippy --all-targets -- -D warnings
  test:
    name: Cargo Test
    needs: tla-plus
    runs-on: ubuntu-latest
    strategy:
      matrix:
        toolchain:
          - nightly-2025-12-11
    steps:
      - uses: actions/checkout@v5
      - name: Install Ziren toolchain
        run: curl --proto '=https' --tlsv1.2 -sSf https://raw.githubusercontent.com/ProjectZKM/toolchain/refs/heads/main/setup.sh | sh
      - name: Install Dependencies
        run: sudo apt update && sudo apt install protobuf-compiler
      - name: Launch the Regtest
        run: cd scripts && docker compose up -d
      - name: Run all unit tests
        run: |
          set -e
          source ~/.zkm-toolchain/env
          cargo test -r --all --all-targets