ci.yml

name: CI

on:
  push:
    branches: [main, master]
  pull_request:
    branches: [main, master]
  workflow_dispatch:
  schedule:
    # Weekly deep formal run. The regular PR path runs the no-TLC harness.
    - cron: "37 5 * * 0"

env:
  CARGO_TERM_COLOR: always
  # Avoid the unconditional `target-cpu=native` from .cargo/config.toml so CI
  # builds remain portable. AES + SSE2 are required by PathMap's gxhash.
  RUSTFLAGS: "-C target-feature=+aes,+sse2"

jobs:
  # -----------------------------------------------------------------
  # Feature-matrix build. Catches feature-flag bugs that hide behind
  # the default `cargo build --all-features` smoke-test.
  # -----------------------------------------------------------------
  build-matrix:
    name: Build (${{ matrix.features-name }})
    runs-on: ${{ matrix.os }}
    strategy:
      fail-fast: false
      matrix:
        os: [ubuntu-latest]
        include:
          - features-name: default
            features: ""
            os: ubuntu-latest
          - features-name: no-default
            features: --no-default-features
            os: ubuntu-latest
          - features-name: persistent-artrie
            features: --no-default-features --features persistent-artrie
            os: ubuntu-latest
          - features-name: pathmap-backend
            features: --no-default-features --features pathmap-backend
            os: ubuntu-latest
          - features-name: io-uring-backend
            features: --no-default-features --features io-uring-backend
            os: ubuntu-latest
          - features-name: parallel-merge
            features: --no-default-features --features parallel-merge
            os: ubuntu-latest
          - features-name: serialization
            features: --no-default-features --features serialization
            os: ubuntu-latest
          - features-name: protobuf
            features: --no-default-features --features protobuf
            os: ubuntu-latest
          - features-name: all-features
            features: --all-features
            os: ubuntu-latest
          # Cross-OS sanity on the default feature set.
          - features-name: macos-default
            features: ""
            os: macos-latest
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@stable
      - name: cargo build
        run: cargo build ${{ matrix.features }} --verbose
      - name: cargo test
        run: cargo test ${{ matrix.features }} --verbose --no-fail-fast

  # -----------------------------------------------------------------
  # `cargo clippy` with `-D warnings`. Catches all the lint regressions
  # that the default `cargo build` would let pass.
  # -----------------------------------------------------------------
  clippy:
    name: Clippy
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@stable
        with:
          components: clippy
      - name: cargo clippy --all-features -- -D warnings
        run: cargo clippy --all-features --all-targets -- -D warnings

  # -----------------------------------------------------------------
  # `cargo doc` with `-D warnings` so broken intra-doc links fail CI.
  # -----------------------------------------------------------------
  doc:
    name: Doc
    runs-on: ubuntu-latest
    env:
      RUSTDOCFLAGS: "-D warnings"
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@stable
      - name: cargo doc --all-features --no-deps
        run: cargo doc --all-features --no-deps

  # -----------------------------------------------------------------
  # rustfmt --check. Prevents formatting drift.
  # -----------------------------------------------------------------
  fmt:
    name: Rustfmt
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@stable
        with:
          components: rustfmt
      - name: cargo fmt --check
        run: cargo fmt --all -- --check

  # -----------------------------------------------------------------
  # MSRV check. `Cargo.toml` declares `rust-version = "1.70"` —
  # enforce it.
  # -----------------------------------------------------------------
  msrv:
    name: MSRV (1.70)
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@master
        with:
          toolchain: "1.70"
      - name: cargo build --all-features
        run: cargo build --all-features

  # -----------------------------------------------------------------
  # Coverage on nightly (branch coverage requires nightly llvm-cov).
  # The previous coverage.yml ran on stable, which silently degraded
  # branch coverage.
  # -----------------------------------------------------------------
  coverage:
    name: Coverage
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@nightly
        with:
          components: llvm-tools-preview
      - uses: taiki-e/install-action@cargo-llvm-cov
      - name: Run coverage
        run: |
          cargo llvm-cov --all-features --branch \
            --lcov --output-path lcov.info \
            --cobertura --output-path cobertura.xml
      - name: Upload coverage to Codecov
        uses: codecov/codecov-action@v4
        with:
          files: lcov.info,cobertura.xml
          fail_ci_if_error: false
        env:
          CODECOV_TOKEN: ${{ secrets.CODECOV_TOKEN }}

  # -----------------------------------------------------------------
  # Sanitizer suite. Pinned at nightly for `-Z sanitizer=`. Each
  # sanitizer is its own job so failures are localised.
  # -----------------------------------------------------------------
  sanitizers:
    name: Sanitizer (${{ matrix.sanitizer }})
    runs-on: ubuntu-latest
    strategy:
      fail-fast: false
      matrix:
        sanitizer: [address, thread]
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@nightly
        with:
          components: rust-src
      - name: Run ${{ matrix.sanitizer }}sanitizer
        env:
          RUSTFLAGS: "-Z sanitizer=${{ matrix.sanitizer }}"
        run: |
          cargo +nightly test \
            --target x86_64-unknown-linux-gnu \
            --all-features \
            --no-fail-fast

  # -----------------------------------------------------------------
  # Rocq proofs. Requires `coqc` >= 9.1 on the runner.
  # -----------------------------------------------------------------
  rocq:
    name: Rocq proofs
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - name: Install Rocq (Coq)
        run: |
          sudo apt-get update
          sudo apt-get install -y coq
      - name: Build proofs
        working-directory: formal-verification/rocq
        run: make

  # -----------------------------------------------------------------
  # Formal correspondence harness. This ties Rust tests, Rocq, unsafe
  # inventory drift, and TLA+ SANY checks into one PR gate.
  # -----------------------------------------------------------------
  formal-correspondence:
    name: Formal correspondence
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@stable
      - uses: actions/setup-java@v4
        with:
          distribution: temurin
          java-version: "21"
      - name: Install Rocq and TLA+ tools
        run: |
          sudo apt-get update
          sudo apt-get install -y coq curl
          curl -L \
            https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar \
            -o tla2tools.jar
          sudo mkdir -p /opt/tla
          sudo mv tla2tools.jar /opt/tla/tla2tools.jar
          sudo tee /usr/local/bin/tla2sany >/dev/null <<'EOF'
          #!/usr/bin/env bash
          exec java -Xmx"${TLA_JAVA_HEAP:-3g}" -cp /opt/tla/tla2tools.jar tla2sany.SANY "$@"
          EOF
          sudo tee /usr/local/bin/tlc >/dev/null <<'EOF'
          #!/usr/bin/env bash
          exec java -Xmx"${TLA_JAVA_HEAP:-3g}" -cp /opt/tla/tla2tools.jar tlc2.TLC "$@"
          EOF
          sudo chmod +x /usr/local/bin/tla2sany /usr/local/bin/tlc
      - name: Run no-TLC correspondence harness
        env:
          CARGO_BUILD_JOBS: "2"
          FORMAL_MEM_LIMIT_BYTES: "8589934592"
          TLA_JAVA_HEAP: "3g"
        run: prlimit --as="$FORMAL_MEM_LIMIT_BYTES" --rss="$FORMAL_MEM_LIMIT_BYTES" -- bash scripts/verify-formal-correspondence.sh

  # -----------------------------------------------------------------
  # Miri unsafe-boundary checks. Runs on nightly because `cargo miri`
  # is a nightly component.
  # -----------------------------------------------------------------
  formal-miri:
    name: Formal unsafe boundary (Miri)
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@nightly
        with:
          components: miri,rust-src
      - uses: actions/setup-java@v4
        with:
          distribution: temurin
          java-version: "21"
      - name: Install Rocq and TLA+ tools
        run: |
          sudo apt-get update
          sudo apt-get install -y coq curl
          curl -L \
            https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar \
            -o tla2tools.jar
          sudo mkdir -p /opt/tla
          sudo mv tla2tools.jar /opt/tla/tla2tools.jar
          sudo tee /usr/local/bin/tla2sany >/dev/null <<'EOF'
          #!/usr/bin/env bash
          exec java -Xmx"${TLA_JAVA_HEAP:-3g}" -cp /opt/tla/tla2tools.jar tla2sany.SANY "$@"
          EOF
          sudo tee /usr/local/bin/tlc >/dev/null <<'EOF'
          #!/usr/bin/env bash
          exec java -Xmx"${TLA_JAVA_HEAP:-3g}" -cp /opt/tla/tla2tools.jar tlc2.TLC "$@"
          EOF
          sudo chmod +x /usr/local/bin/tla2sany /usr/local/bin/tlc
      - name: Prepare Miri
        env:
          CARGO_BUILD_JOBS: "2"
          FORMAL_MEM_LIMIT_BYTES: "8589934592"
        run: prlimit --as="$FORMAL_MEM_LIMIT_BYTES" --rss="$FORMAL_MEM_LIMIT_BYTES" -- cargo miri setup
      - name: Run Miri-gated correspondence harness
        env:
          CARGO_BUILD_JOBS: "2"
          FORMAL_MEM_LIMIT_BYTES: "8589934592"
          RUN_MIRI: "1"
          TLA_JAVA_HEAP: "3g"
        run: prlimit --as="$FORMAL_MEM_LIMIT_BYTES" --rss="$FORMAL_MEM_LIMIT_BYTES" -- bash scripts/verify-formal-correspondence.sh

  # -----------------------------------------------------------------
  # Linux io_uring backend correspondence. Tests skip internally if
  # the runner kernel/filesystem rejects io_uring + O_DIRECT setup.
  # -----------------------------------------------------------------
  formal-io-uring:
    name: Formal storage backend (io_uring)
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@stable
      - uses: actions/setup-java@v4
        with:
          distribution: temurin
          java-version: "21"
      - name: Install Rocq and TLA+ tools
        run: |
          sudo apt-get update
          sudo apt-get install -y coq curl
          curl -L \
            https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar \
            -o tla2tools.jar
          sudo mkdir -p /opt/tla
          sudo mv tla2tools.jar /opt/tla/tla2tools.jar
          sudo tee /usr/local/bin/tla2sany >/dev/null <<'EOF'
          #!/usr/bin/env bash
          exec java -Xmx"${TLA_JAVA_HEAP:-3g}" -cp /opt/tla/tla2tools.jar tla2sany.SANY "$@"
          EOF
          sudo tee /usr/local/bin/tlc >/dev/null <<'EOF'
          #!/usr/bin/env bash
          exec java -Xmx"${TLA_JAVA_HEAP:-3g}" -cp /opt/tla/tla2tools.jar tlc2.TLC "$@"
          EOF
          sudo chmod +x /usr/local/bin/tla2sany /usr/local/bin/tlc
      - name: Run io_uring-gated correspondence harness
        env:
          CARGO_BUILD_JOBS: "2"
          FORMAL_MEM_LIMIT_BYTES: "8589934592"
          RUN_IO_URING: "1"
          TLA_JAVA_HEAP: "3g"
        run: prlimit --as="$FORMAL_MEM_LIMIT_BYTES" --rss="$FORMAL_MEM_LIMIT_BYTES" -- bash scripts/verify-formal-correspondence.sh

  # -----------------------------------------------------------------
  # Diagram freshness gate. Re-renders every diagrams-as-code source
  # (docs/diagrams/src/* and docs/benchmarks/artifacts/*.gp) with the
  # pinned renderer versions, then fails if any committed SVG is stale
  # — i.e. a source was edited without re-running render-diagrams.sh.
  # Uses the deterministic renderers only (PlantUML/D2/Graphviz/
  # bytefield-svg/gnuplot); Mermaid/Chromium is intentionally excluded
  # because its output is not byte-reproducible across machines.
  # -----------------------------------------------------------------
  diagrams:
    name: Diagrams (freshness)
    runs-on: ubuntu-latest
    env:
      PLANTUML_VERSION: "1.2026.5"
      D2_VERSION: "0.7.1"
      BYTEFIELD_SVG_VERSION: "1.11.0"
      SVGBOB_VERSION: "0.7.6"
    steps:
      - uses: actions/checkout@v4
      - name: Install system renderers (graphviz, gnuplot, java)
        run: |
          sudo apt-get update
          sudo apt-get install -y graphviz gnuplot default-jre-headless
      - name: Install PlantUML (pinned jar)
        run: |
          curl -fsSL \
            "https://github.com/plantuml/plantuml/releases/download/v${PLANTUML_VERSION}/plantuml-${PLANTUML_VERSION}.jar" \
            -o /opt/plantuml.jar
          sudo tee /usr/local/bin/plantuml >/dev/null <<'EOF'
          #!/usr/bin/env bash
          exec java -jar /opt/plantuml.jar "$@"
          EOF
          sudo chmod +x /usr/local/bin/plantuml
      - name: Install D2 (pinned release)
        run: |
          curl -fsSL \
            "https://github.com/terrastruct/d2/releases/download/v${D2_VERSION}/d2-v${D2_VERSION}-linux-amd64.tar.gz" \
            -o /tmp/d2.tar.gz
          tar -xzf /tmp/d2.tar.gz -C /tmp
          sudo install "/tmp/d2-v${D2_VERSION}/bin/d2" /usr/local/bin/d2
      - name: Install Svgbob (pinned)
        run: cargo install svgbob_cli --version "${SVGBOB_VERSION}" --locked
      - uses: actions/setup-node@v4
        with:
          node-version: "20"
      - name: Install Node renderers (bytefield-svg, pinned)
        run: npm install -g "bytefield-svg@${BYTEFIELD_SVG_VERSION}"
      - name: Render all diagrams
        run: bash scripts/render-diagrams.sh
      - name: Fail if any committed SVG is stale
        run: |
          if ! git diff --exit-code -- docs/diagrams docs/benchmarks/artifacts; then
            echo "::error::Committed diagram SVGs are stale. Run 'scripts/render-diagrams.sh' and commit the result."
            exit 1
          fi
      - name: SVG hygiene gate (root viewBox + no baked deprecation banner)
        run: bash scripts/render-diagrams.sh --check

      # GitHub strips backslash-escapes inside `$…$` / `$$…$$` before MathJax parses
      # them, so `\_` `\{` `\;` are corrupted — loudly (parse error) or silently
      # (wrong output). Only $`…`$ and ```math fences survive. See docs/README.md.
      - name: Doc math hygiene gate (GitHub-safe delimiters)
        run: |
          python3 scripts/check-doc-math.py --selftest
          python3 scripts/check-doc-math.py

  # -----------------------------------------------------------------
  # Scheduled/manual deep bounded model check. This is intentionally
  # not a PR job because several focused TLC models are large.
  # -----------------------------------------------------------------
  formal-tlc:
    name: Formal bounded models (TLC)
    runs-on: ubuntu-latest
    if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@stable
      - uses: actions/setup-java@v4
        with:
          distribution: temurin
          java-version: "21"
      - name: Install Rocq and TLA+ tools
        run: |
          sudo apt-get update
          sudo apt-get install -y coq curl
          curl -L \
            https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar \
            -o tla2tools.jar
          sudo mkdir -p /opt/tla
          sudo mv tla2tools.jar /opt/tla/tla2tools.jar
          sudo tee /usr/local/bin/tla2sany >/dev/null <<'EOF'
          #!/usr/bin/env bash
          exec java -Xmx"${TLA_JAVA_HEAP:-5g}" -cp /opt/tla/tla2tools.jar tla2sany.SANY "$@"
          EOF
          sudo tee /usr/local/bin/tlc >/dev/null <<'EOF'
          #!/usr/bin/env bash
          exec java -Xmx"${TLA_JAVA_HEAP:-5g}" -cp /opt/tla/tla2tools.jar tlc2.TLC "$@"
          EOF
          sudo chmod +x /usr/local/bin/tla2sany /usr/local/bin/tlc
      - name: Run TLC-gated correspondence harness
        env:
          CARGO_BUILD_JOBS: "2"
          FORMAL_MEM_LIMIT_BYTES: "10737418240"
          RUN_TLC: "1"
          TLA_JAVA_HEAP: "5g"
        run: prlimit --as="$FORMAL_MEM_LIMIT_BYTES" --rss="$FORMAL_MEM_LIMIT_BYTES" -- bash scripts/verify-formal-correspondence.sh