diff --git a/.github/actions/authenticate-github-fetches/action.yml b/.github/actions/authenticate-github-fetches/action.yml index 72d60e811..e9e6cbd17 100644 --- a/.github/actions/authenticate-github-fetches/action.yml +++ b/.github/actions/authenticate-github-fetches/action.yml @@ -1,12 +1,12 @@ name: Authenticate git fetches of GitHub repos description: >- Rewrite github.com URLs so git-CLI fetches carry the job's ephemeral token. - GitHub throttles anonymous git HTTPS traffic per source IP, and Warp runners - share egress IPs across tenants, so unauthenticated clones of public repos - can fail with a 401 ("could not read Username"). The rewrite covers every - fetch that goes through the git CLI: Lake dependency clones, Nix's eval-time - `builtins.fetchGit`, script clones, and cargo git dependencies when - CARGO_NET_GIT_FETCH_WITH_CLI is set. + GitHub throttles anonymous git HTTPS traffic per source IP, and managed + runner pools can share egress IPs across tenants, so unauthenticated clones + of public repos can fail with a 401 ("could not read Username"). The rewrite + covers every fetch that goes through the git CLI: Lake dependency clones, + Nix's eval-time `builtins.fetchGit`, script clones, and cargo git dependencies + when CARGO_NET_GIT_FETCH_WITH_CLI is set. runs: using: composite diff --git a/.github/actions/bencher-track/action.yml b/.github/actions/bencher-track/action.yml index 6de6c160d..85c6e9c36 100644 --- a/.github/actions/bencher-track/action.yml +++ b/.github/actions/bencher-track/action.yml @@ -13,7 +13,7 @@ inputs: description: Bencher testbed slug. required: true workload: - description: Workload key for the `refs/bencher/` anchor (the backend testbed minus its runner-arch suffix, e.g. zisk-check-execute). + description: Workload key for the `refs/bencher/` anchor (the backend testbed minus its runner-arch suffix, e.g. ooc-check). required: true file: description: Bencher Metric Format JSON file to upload. diff --git a/.github/actions/install-sp1/action.yml b/.github/actions/install-sp1/action.yml index 5f820cd03..0e386423d 100644 --- a/.github/actions/install-sp1/action.yml +++ b/.github/actions/install-sp1/action.yml @@ -13,11 +13,11 @@ runs: - name: Install system build deps shell: bash run: | - # Some warpbuild images ship an unreachable azure mirror that hangs + # Some runner images ship an unreachable Azure mirror that hangs # `apt-get update`; drop it first (no-op elsewhere). sudo sed -i '/azure\.archive\.ubuntu\.com/d' /etc/apt/apt-mirrors.txt 2>/dev/null || true export DEBIAN_FRONTEND=noninteractive - # The Ubuntu EC2 mirrors sporadically 502 / throttle on these large + # Ubuntu package mirrors sporadically 502 / throttle on these large # fetches (qemu-system alone pulls hundreds of MB), so retry the whole # update+install: `Acquire::Retries` absorbs single-download blips and # `--fix-missing` resumes a partially fetched set. diff --git a/.github/actions/install-zisk/action.yml b/.github/actions/install-zisk/action.yml index 857fcb356..35719d2f0 100644 --- a/.github/actions/install-zisk/action.yml +++ b/.github/actions/install-zisk/action.yml @@ -24,11 +24,11 @@ runs: - name: Install system build deps shell: bash run: | - # Some warpbuild images ship an unreachable azure mirror that hangs + # Some runner images ship an unreachable Azure mirror that hangs # `apt-get update`; drop it first (no-op elsewhere). sudo sed -i '/azure\.archive\.ubuntu\.com/d' /etc/apt/apt-mirrors.txt 2>/dev/null || true export DEBIAN_FRONTEND=noninteractive - # The Ubuntu EC2 mirrors sporadically 502 / throttle on these large + # Ubuntu package mirrors sporadically 502 / throttle on these large # fetches (qemu-system alone pulls hundreds of MB), so retry the whole # update+install: `Acquire::Retries` absorbs single-download blips and # `--fix-missing` resumes a partially fetched set. @@ -90,7 +90,7 @@ runs: "$HOME/.zisk/bin/cargo-zisk" toolchain install --toolchain-version zisk-0.5.1 echo "$HOME/.zisk/bin" >> "$GITHUB_PATH" # Pre-build the proofman C++ sys crate ALONE so its build script runs - # exactly once before any parallel zisk-host build. zisk-host pulls + # exactly once before zisk-host's parallel Cargo build. zisk-host pulls # zisk-sdk as both a dependency and a build-dependency, so cargo compiles # proofman-starks-lib-c as two units whose build scripts can run # CONCURRENTLY — and both run `make` inside the SHARED @@ -117,9 +117,9 @@ runs: # reuse a stale key. `aws s3 cp` (multipart, no creds — public bucket) # holds throughput steady where a single-stream `curl` swings by an # order of magnitude; `curl` is the fallback for hosts without the AWS - # CLI. Deliberately NOT actions/cache'd: the runner fleet is AWS-hosted, - # so multipart S3 outruns the Actions cache service — and the tarball - # would crowd the repo's cache quota besides. + # CLI. Deliberately omitted from the shared runner cache: the multi-GB + # tarball would crowd build artifacts, while its public S3 source supports + # multipart downloads directly. - name: Fetch proving key from S3, extract, regenerate const-trees if: inputs.proving-key == 'true' shell: bash diff --git a/.github/actions/log-cpu/action.yml b/.github/actions/log-cpu/action.yml index b47cea486..ada8c9f16 100644 --- a/.github/actions/log-cpu/action.yml +++ b/.github/actions/log-cpu/action.yml @@ -1,140 +1,52 @@ name: Log CPU information -description: >- - Log a benchmark host's CPU and effective cgroup allocation, optionally - recording the report, printing native-binary build provenance, and warning - when the build and measurement CPUs differ. +description: Log the current host's CPU and effective cgroup allocation inputs: label: - description: Heading and context stored in a newly recorded CPU report + description: Heading and context for the CPU report required: false default: CPU information - output-file: - description: Optional path at which to record the current host report - required: false - provenance-file: - description: Optional native-binary build-host report to print - required: false - provenance-label: - description: Subject named in provenance mismatch warnings - required: false - default: Native benchmark binaries - warning-file: - description: Optional Markdown file to which provenance warnings are appended - required: false - log-current: - description: Whether to log the current host - required: false - default: "true" + +outputs: + summary: + description: CPU model, effective vCPU count, and total RAM + value: ${{ steps.report.outputs.summary }} runs: using: composite steps: - # PR benchmarks execute trusted workflow YAML from the default branch but - # load this action from the PR checkout. Ensure a freshly checked-out base - # has its pinned Rust toolchain before Lake invokes Cargo. - - name: Bootstrap base Rust toolchain - if: inputs.label == 'Base benchmark binary build CPU' + - id: report shell: bash - run: | - set -euo pipefail - - toolchain_file=base/rust-toolchain.toml - [ -f "$toolchain_file" ] || { echo "::error::$toolchain_file is missing"; exit 1; } - channel=$(awk -F '"' '/^[[:space:]]*channel[[:space:]]*=/ { print $2; exit }' "$toolchain_file") - profile=$(awk -F '"' '/^[[:space:]]*profile[[:space:]]*=/ { print $2; exit }' "$toolchain_file") - if [[ ! "$channel" =~ ^[A-Za-z0-9._+-]+$ ]]; then - echo "::error::$toolchain_file has an invalid Rust channel" - exit 1 - fi - case "${profile:-default}" in - minimal|default|complete) ;; - *) echo "::error::$toolchain_file has an invalid Rust profile"; exit 1 ;; - esac - - rustup run "$channel" rustc --version >/dev/null 2>&1 && exit 0 - echo "Installing Rust $channel (${profile:-default} profile) for the fresh base build" - rustup toolchain install "$channel" --profile "${profile:-default}" --no-self-update - - - shell: bash env: CPU_LABEL: ${{ inputs.label }} - CPU_OUTPUT_FILE: ${{ inputs.output-file }} - CPU_PROVENANCE_FILE: ${{ inputs.provenance-file }} - CPU_PROVENANCE_LABEL: ${{ inputs.provenance-label }} - CPU_WARNING_FILE: ${{ inputs.warning-file }} - LOG_CURRENT_CPU: ${{ inputs.log-current }} run: | set -euo pipefail export LC_ALL=C - resolve_path() { - if [[ "$1" == \~/* ]]; then - printf '%s/%s\n' "$HOME" "${1:2}" - else - printf '%s\n' "$1" - fi - } - - model_name() { - awk -F ': *' '/^Model name:/ { print $2; exit }' "$@" - } - - current_cpu_model=$(lscpu | model_name) - - cpu_report() { - echo "Context: $CPU_LABEL" - echo "Runner: ${RUNNER_NAME:-unknown} (${RUNNER_OS:-unknown}/${RUNNER_ARCH:-unknown})" - echo "Kernel: $(uname -srvm)" - echo "nproc: $(nproc)" - if [ -r /sys/fs/cgroup/cpu.max ]; then - echo "cgroup cpu.max: $(< /sys/fs/cgroup/cpu.max)" - fi - if [ -r /sys/fs/cgroup/cpuset.cpus.effective ]; then - echo "cgroup cpuset.cpus.effective: $(< /sys/fs/cgroup/cpuset.cpus.effective)" - fi - grep -m1 '^Cpus_allowed_list:' /proc/self/status || true - lscpu - flags=$({ grep -m1 -oE 'avx2|avx512[a-z0-9_]*' /proc/cpuinfo || true; } \ - | sort -u | tr '\n' ' ') - echo "AVX flags: ${flags:-absent}" - } - - if [ "$LOG_CURRENT_CPU" = true ]; then - echo "::group::$CPU_LABEL" - if [ -n "$CPU_OUTPUT_FILE" ]; then - output_file=$(resolve_path "$CPU_OUTPUT_FILE") - mkdir -p "$(dirname "$output_file")" - cpu_report | tee "$output_file" - else - cpu_report - fi - echo "::endgroup::" + cpu_info=$(lscpu) + cpu_model=$(printf '%s\n' "$cpu_info" | awk -F ': *' '/^Model name:/ { print $2; exit }') + vcpus=$(nproc) + ram_kib=$(awk '/^MemTotal:/ { print $2; exit }' /proc/meminfo) + ram=$(awk -v kib="$ram_kib" 'BEGIN { printf "%.1f GiB", kib / 1048576 }') + + echo "::group::$CPU_LABEL" + echo "Context: $CPU_LABEL" + echo "Runner: ${RUNNER_NAME:-unknown} (${RUNNER_OS:-unknown}/${RUNNER_ARCH:-unknown})" + echo "Kernel: $(uname -srvm)" + echo "nproc: $vcpus" + echo "RAM: $ram" + if [ -r /sys/fs/cgroup/cpu.max ]; then + echo "cgroup cpu.max: $(< /sys/fs/cgroup/cpu.max)" fi - - if [ -n "$CPU_PROVENANCE_FILE" ]; then - provenance_file=$(resolve_path "$CPU_PROVENANCE_FILE") - echo "::group::Native benchmark binary build CPU" - if [ -s "$provenance_file" ]; then - cat "$provenance_file" - else - echo "::warning::Binary build CPU provenance is unavailable (the cache may predate CPU reports)" - fi - echo "::endgroup::" - - provenance_model=$(model_name "$provenance_file" 2>/dev/null || true) - warning="" - if [ -z "$provenance_model" ] || [ -z "$current_cpu_model" ]; then - warning=$(printf '**CPU provenance unavailable for %s:** one report has no CPU model, so native-code compatibility cannot be checked.' "$CPU_PROVENANCE_LABEL") - elif [ "$provenance_model" != "$current_cpu_model" ]; then - warning=$(printf "**CPU model mismatch for %s:** built on \`%s\`; measured on \`%s\`. Native Rust code uses \`-Ctarget-cpu=native\`." "$CPU_PROVENANCE_LABEL" "$provenance_model" "$current_cpu_model") - fi - if [ -n "$warning" ]; then - echo "::warning::$warning" - if [ -n "$CPU_WARNING_FILE" ]; then - warning_file=$(resolve_path "$CPU_WARNING_FILE") - mkdir -p "$(dirname "$warning_file")" - printf '%s\n' "- $warning" >> "$warning_file" - fi - fi + if [ -r /sys/fs/cgroup/cpuset.cpus.effective ]; then + echo "cgroup cpuset.cpus.effective: $(< /sys/fs/cgroup/cpuset.cpus.effective)" fi + grep -m1 '^Cpus_allowed_list:' /proc/self/status || true + printf '%s\n' "$cpu_info" + flags=$({ grep -m1 -oE 'avx2|avx512[a-z0-9_]*' /proc/cpuinfo || true; } \ + | sort -u | tr '\n' ' ') + echo "AVX flags: ${flags:-absent}" + echo "::endgroup::" + + printf 'summary=CPU: `%s` · vCPUs: `%s` · RAM: `%s`\n' \ + "${cpu_model:-unknown}" "$vcpus" "$ram" >> "$GITHUB_OUTPUT" diff --git a/.github/actions/setup-lake-cache/action.yml b/.github/actions/setup-lake-cache/action.yml new file mode 100644 index 000000000..715259ff5 --- /dev/null +++ b/.github/actions/setup-lake-cache/action.yml @@ -0,0 +1,34 @@ +name: Set up Namespace build cache +description: >- + Mount .lake, Namespace's built-in cache presets, and optional build + directories on the shared cache volume. + +inputs: + cache-modes: + description: Built-in Namespace cache presets to mount (for example, rust or nix) + required: false + default: rust + additional-paths: + description: Paths to mount in addition to the repository's .lake directory + required: false + +outputs: + cache-hit: + description: Whether Namespace restored a prior cache volume + value: ${{ steps.cache.outputs.cache-hit }} + +runs: + using: composite + steps: + - name: Create Lake build directory + shell: bash + run: mkdir -p "${{ github.workspace }}/.lake" + + - name: Mount Namespace build cache + id: cache + uses: namespacelabs/nscloud-cache-action@v1 + with: + cache: ${{ inputs.cache-modes }} + path: | + ${{ github.workspace }}/.lake + ${{ inputs.additional-paths }} diff --git a/.github/actions/setup-rust-toolchain/action.yml b/.github/actions/setup-rust-toolchain/action.yml index 6692caa65..5cdf6981f 100644 --- a/.github/actions/setup-rust-toolchain/action.yml +++ b/.github/actions/setup-rust-toolchain/action.yml @@ -1,29 +1,45 @@ name: Set up Rust toolchain description: >- - Install Rust on Warp Linux x64, configure compiler flags, and cache Cargo - artifacts. + Install Rust on supported Linux x64 runners, configure compiler flags, and + optionally cache Cargo artifacts. inputs: cache-workspaces: description: Cargo workspaces to cache required: false + use-github-cache: + description: Enable Cargo artifact caching through the selected provider + required: false + default: "true" + cache-provider: + description: Cache provider used by the Rust setup action + required: false + default: github avx512-codegen: - description: Enable AVX-512 code generation for the Warp x64 fleet's common ISA + description: Enable portable AVX-512 code generation for supported x64 runners required: false default: "true" runs: using: composite steps: - - name: Require Warp Linux x64 runner + # The AVX-512 baseline below is a property of the Warp and Namespace + # fleets; a portable build may run on any Linux x64 host. + - name: Require supported Linux x64 runner shell: bash env: IX_RUNNER_NAME: ${{ runner.name }} IX_RUNNER_OS: ${{ runner.os }} IX_RUNNER_ARCH: ${{ runner.arch }} + IX_AVX512_CODEGEN: ${{ inputs.avx512-codegen }} run: | - if [[ "$IX_RUNNER_NAME" != warp-* || "$IX_RUNNER_OS" != Linux || "$IX_RUNNER_ARCH" != X64 ]]; then - echo "::error::setup-rust-toolchain requires a Warp Linux x64 runner; got name=$IX_RUNNER_NAME os=$IX_RUNNER_OS arch=$IX_RUNNER_ARCH" + if [[ "$IX_RUNNER_OS" != Linux || "$IX_RUNNER_ARCH" != X64 ]]; then + echo "::error::setup-rust-toolchain requires a Linux x64 runner; got os=$IX_RUNNER_OS arch=$IX_RUNNER_ARCH" + exit 1 + fi + if [[ "$IX_AVX512_CODEGEN" == true && \ + "$IX_RUNNER_NAME" != warp-* && "$IX_RUNNER_NAME" != nsc-runner-* ]]; then + echo "::error::AVX-512 builds require a Warp or Namespace runner; got name=$IX_RUNNER_NAME" exit 1 fi @@ -40,16 +56,16 @@ runs: echo "CARGO_NET_GIT_FETCH_WITH_CLI=true" >> "$GITHUB_ENV" fi - # The fleet mixes Intel Granite Rapids and AMD Zen 5, and a binary may be - # built on one and measured on another. Neither vendor's feature set - # contains the other's, so `-Ctarget-cpu=native` is not portable across - # the fleet: Zen 5 enables SSE4A, which LLVM emits (as INSERTQ, in - # witness generation) and Intel traps on with #UD. Pin the measured - # intersection instead. x86-64-v4 covers every AVX-512 subset Plonky3 - # uses; +avx512vbmi2 keeps its VPSHRDQ interleave and +gfni keeps LLVM's - # byte-shift lowering. blake3 selects its kernels via CPUID at runtime - # and is unaffected. Pinning also makes codegen host-independent, so the - # cache key below is sound and main-vs-PR timings stay comparable. + # The supported fleets mix Intel and AMD hosts, and cached artifacts may + # be built on one CPU model and consumed on another. Neither vendor's + # feature set contains the other's, so `-Ctarget-cpu=native` is not + # portable across the fleet: Zen 5 enables SSE4A, which LLVM emits (as + # INSERTQ, in witness generation) and Intel traps on with #UD. Pin the + # measured intersection instead. x86-64-v4 covers every AVX-512 subset + # Plonky3 uses; +avx512vbmi2 keeps its VPSHRDQ interleave and +gfni keeps + # LLVM's byte-shift lowering. blake3 selects its kernels via CPUID at + # runtime and is unaffected. Pinning also makes codegen host-independent, + # so the cache key below is sound and main-vs-PR timings stay comparable. - name: Require the fleet's baseline CPU features if: inputs.avx512-codegen == 'true' shell: bash @@ -59,14 +75,33 @@ runs: grep -qw "$f" /proc/cpuinfo || missing+=("$f") done if [ ${#missing[@]} -gt 0 ]; then - echo "::error::Runner CPU lacks required feature(s): ${missing[*]}. Benchmark binaries are built for x86-64-v4 +avx512vbmi2,+gfni." + echo "::error::Runner CPU lacks required feature(s): ${missing[*]}. Binaries are built for x86-64-v4 +avx512vbmi2,+gfni." exit 1 fi + # bindgen collects include paths from the `clang` binary on PATH and + # passes them as `-isystem`, while clang-sys loads whichever libclang it + # finds. On an image with several LLVM versions those differ: clang's + # `stdatomic.h` then `include_next`s the other version's copy, whose + # identical include guard skips its body, and every C11 atomic in + # `lean.h` comes out undeclared. Point both at one install. + - name: Pin bindgen to a single LLVM install + shell: bash + run: | + for llvm in $(printf '%s\n' /usr/lib/llvm-* | sort -V -r); do + if [ -x "$llvm/bin/clang" ] && ls "$llvm"/lib/libclang*.so* >/dev/null 2>&1; then + echo "LIBCLANG_PATH=$llvm/lib" >> "$GITHUB_ENV" + echo "CLANG_PATH=$llvm/bin/clang" >> "$GITHUB_ENV" + echo "bindgen pinned to $llvm" + exit 0 + fi + done + echo "no versioned LLVM install with both clang and libclang; leaving bindgen defaults" + - uses: actions-rust-lang/setup-rust-toolchain@v1 with: rustflags: ${{ inputs.avx512-codegen == 'true' && '-Ctarget-cpu=x86-64-v4 -Ctarget-feature=+avx512vbmi2,+gfni -Dwarnings' || '-Dwarnings' }} - # Codegen is pinned above, so `target/` artifacts are interchangeable - # across every Warp x64 host. - cache-key: warp-x64 + cache: ${{ inputs.use-github-cache }} + cache-provider: ${{ inputs.cache-provider }} + cache-key: ${{ inputs.avx512-codegen == 'true' && 'x64-avx512' || 'x64-portable' }} cache-workspaces: ${{ inputs.cache-workspaces }} diff --git a/.github/workflows/bench-main.yml b/.github/workflows/bench-main.yml index d97e9a2e6..25f42ea2b 100644 --- a/.github/workflows/bench-main.yml +++ b/.github/workflows/bench-main.yml @@ -3,18 +3,18 @@ name: Benchmark main # Benchmarks every push to main and uploads the results to bencher.dev. # Each measurement is one `ix bench run` with a (backend, env, mode) # parameter combination — the same command you can run locally, and the -# same one the !benchmark PR workflow uses. Three stages: +# same one the !benchmark PR workflow uses. Four job roles: # -# 1. plan — `ix bench ci matrix` prints the list of parameter +# 1. build — compiles and caches `ix` and `bench-typecheck` once. +# 2. plan — `ix bench ci matrix` prints the list of parameter # combinations to run. The list comes from the registry # (Ix/Cli/BenchCmd.lean) and each entry already carries # its bencher testbed, workload, and threshold flags, so # this file hardcodes none of that. -# 2. compile — compiles each Lean env to a `.ixe` file (this IS the -# compile benchmark) and caches the file for stage 3. -# 3. benchmark — one job per remaining entry: restore the `.ixe` and -# run the entry's backend over it (aiur, zisk, ooc, -# decompile). +# 3. compile — compiles each Lean env to a `.ixe` file (this IS the +# compile benchmark) and caches the file for `benchmark`. +# 4. benchmark — one job per remaining entry: restore the `.ixe` and +# run the entry's backend over it (aiur, ooc, decompile). # # Each entry uploads to its own bencher testbed/workload, so a threshold # reset for one workload never touches another. When the kernel REJECTS a @@ -29,7 +29,6 @@ on: permissions: contents: read - checks: write # No concurrency group on purpose: every merged commit gets benchmarked, # and a later merge must never cancel or queue behind an in-flight run. @@ -40,36 +39,40 @@ env: jobs: # Build the `ix` and `bench-typecheck` binaries once and cache them; # every later job restores them instead of rebuilding. They are built - # with -Ctarget-cpu=native, so every job that runs them must use the - # same warp runner class. + # for the fleet's fixed AVX-512 baseline. Measured jobs stay on Warp so + # the benchmark testbed remains consistent. build: runs-on: warp-ubuntu-latest-x64-32x steps: - uses: actions/checkout@v7 - # Native codegen fixes the available instructions at build time. Carry - # this report with the binaries so every later measurement records both - # the build host and its own run host. + - name: Mount Lake build cache + uses: WarpBuilds/cache@v2 + with: + path: .lake + key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} + restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}- - name: Log build CPU uses: ./.github/actions/log-cpu with: label: Benchmark binary build CPU - output-file: ${{ runner.temp }}/benchmark-build-cpu.txt # Rust toolchain + cargo cache, so the cargo step inside `lake build` # does not recompile the Plonky3/multi-stark dependencies every run. - uses: ./.github/actions/setup-rust-toolchain + with: + cache-provider: warpbuild - uses: leanprover/lean-action@v1 with: auto-config: false build: true build-args: "ix --wfail -v" + use-github-cache: false - run: | mkdir -p ~/.local/bin echo | lake run install # copies ix -> ~/.local/bin/ix lake build bench-typecheck cp .lake/build/bin/bench-typecheck ~/.local/bin/ - cp "${{ runner.temp }}/benchmark-build-cpu.txt" ~/.local/bin/ chmod +x ~/.local/bin/bench-typecheck - - uses: actions/cache/save@v6 + - uses: WarpBuilds/cache/save@v2 with: path: ~/.local/bin key: bench-bins-${{ github.sha }} @@ -81,14 +84,14 @@ jobs: # job; only the benchmark job waits on it. plan: needs: build - # Native target features may occur anywhere in `ix`, including this - # registry-only subcommand, so keep it on the Warp x64 runner fleet. + # The restored `ix` targets the fleet's fixed AVX-512 baseline, so keep + # even this registry-only invocation on compatible Warp x64 hardware. runs-on: warp-ubuntu-latest-x64-8x outputs: matrix: ${{ steps.matrix.outputs.matrix }} steps: - uses: actions/checkout@v7 - - uses: actions/cache/restore@v6 + - uses: WarpBuilds/cache/restore@v2 with: path: ~/.local/bin key: bench-bins-${{ github.sha }} @@ -119,6 +122,9 @@ jobs: name: compile-${{ matrix.env }} needs: build runs-on: warp-ubuntu-latest-x64-32x + permissions: + contents: read + checks: write timeout-minutes: 60 strategy: fail-fast: false @@ -142,15 +148,15 @@ jobs: - uses: actions/checkout@v7 # `lake build` below clones this package's Lake dependencies. - uses: ./.github/actions/authenticate-github-fetches - - uses: actions/cache/restore@v6 + - uses: WarpBuilds/cache/restore@v2 with: path: ~/.local/bin key: bench-bins-${{ github.sha }} - name: Log compile CPU + id: cpu uses: ./.github/actions/log-cpu with: label: Compile measurement CPU - provenance-file: ~/.local/bin/benchmark-build-cpu.txt - run: echo "$HOME/.local/bin" >> $GITHUB_PATH # Install the Lean toolchain. The mathlib olean cache is fetched only # for envs that import Mathlib (Mathlib, FLT) — the shared @@ -164,7 +170,7 @@ jobs: use-mathlib-cache: ${{ matrix.mathlib && 'true' || 'false' }} # FLT takes a few minutes to rebuild, so cache its build artifacts. - if: matrix.cache_pkg - uses: actions/cache@v6 + uses: WarpBuilds/cache@v2 with: path: ${{ env.COMPILE_DIR }}/.lake/packages/${{ matrix.cache_pkg }}/.lake/build key: ${{ matrix.cache_pkg }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', env.COMPILE_DIR)) }}-${{ hashFiles(format('{0}/lake-manifest.json', env.COMPILE_DIR)) }} @@ -180,12 +186,10 @@ jobs: ix bench run --backend compile --env ${{ matrix.env }} --out bench.json ix bench bmf --in bench.json --out benchmark.json cat benchmark.json - # Ask the registry three things about this env (instead of keeping + # Ask the registry for this env's metadata (instead of keeping # hand-written env lists here): # consumed — does any benchmark entry restore this env's `.ixe`? # If yes, cache it below. - # zkvm — does a zkVM entry execute this env? If yes, pre-cut - # its closure shards below. # testbed / workload / thresholds — the upload metadata for this # env's own compile benchmark. - id: gates @@ -194,39 +198,38 @@ jobs: ix bench ci matrix > matrix.json gate() { jq --arg env "${{ matrix.env }}" "[.[] | select($1).env] | index(\$env) >= 0" matrix.json; } echo "consumed=$(gate '.backend == "compile" | not')" >> "$GITHUB_OUTPUT" - echo "zkvm=$(gate '.backend == "zisk" or .backend == "sp1"')" >> "$GITHUB_OUTPUT" meta() { jq -r --arg env "${{ matrix.env }}" "first(.[] | select(.backend == \"compile\" and .env == \$env)).$1" matrix.json; } echo "testbed=$(meta testbed)" >> "$GITHUB_OUTPUT" echo "workload=$(meta workload)" >> "$GITHUB_OUTPUT" + echo "mode=$(meta mode)" >> "$GITHUB_OUTPUT" { echo "thresholds<> "$GITHUB_OUTPUT" - # Pre-cut the closure-shard artifacts for this env's zisk constants - # (extract → profile → shard; the planner's RAM budget decides each - # constant's shard count). The zisk runs can cut these lazily - # themselves, but doing it here — right next to the fresh `.ixe`, - # with the toolchain already installed — means they just restore a - # directory. - - if: steps.gates.outputs.zkvm == 'true' - name: Cut closure shards for zisk constants - run: ix bench shard --env ${{ matrix.env }} --ixe ${{ matrix.env }}.ixe # Cache the `.ixe` for the benchmark job. IMPORTANT: every restore of - # this key must list the same paths — actions/cache versions the + # this key must list the same paths — cache versions include the # entry by its path list, so a mismatched list is unreachable # whatever the key. Keeping this entry to one path lets bench-pr's # base-side restore fall back to that workflow's compile-job key (a # stacked PR's base is a PR head, which never passes through here). - if: steps.gates.outputs.consumed == 'true' - uses: actions/cache/save@v6 + uses: WarpBuilds/cache/save@v2 with: path: ${{ matrix.env }}.ixe key: bench-ixe-${{ github.sha }}-${{ matrix.env }} - # Shards get their own entry rather than riding the `.ixe`: only the - # zkVM envs have any, so bundling them would put a directory that - # usually doesn't exist into every `.ixe` restore's path list. - - if: steps.gates.outputs.zkvm == 'true' - uses: actions/cache/save@v6 + # Record the host that measured this row. Bencher stores metric rows + # only, so bench-pr restores this note by (SHA, parameters) to label a + # bencher-sourced base side with its own hardware. Best-effort: a + # missing entry renders as "not recorded". + - name: Record measurement hardware + if: ${{ !cancelled() }} + env: + HARDWARE: ${{ steps.cpu.outputs.summary }} + run: printf '%s\n' "$HARDWARE" > bench-hardware.txt + - name: Cache measurement hardware + if: ${{ !cancelled() }} + continue-on-error: true + uses: WarpBuilds/cache/save@v2 with: - path: zkshards-${{ matrix.env }} - key: bench-shards-${{ github.sha }}-${{ matrix.env }} + path: bench-hardware.txt + key: bench-hardware-${{ github.sha }}-compile-${{ matrix.env }}-${{ steps.gates.outputs.mode }} # Upload the compile metrics. Testbed, workload, and threshold flags # all come from the registry (the reasoning behind each bound lives # next to `thresholds` in Ix/Cli/BenchCmd.lean). @@ -236,14 +239,13 @@ jobs: workload: ${{ steps.gates.outputs.workload }} file: benchmark.json key: ${{ secrets.BENCHER_API_KEY }} - github-token: ${{ secrets.GITHUB_TOKEN }} + github-token: ${{ github.token }} thresholds: ${{ steps.gates.outputs.thresholds }} # One job per remaining matrix entry, all sharing this one step list # (same shape as bench-pr.yml's benchmark job). Each entry brings its - # own label, testbed, workload, and threshold flags, so the only - # backend-specific steps are the zkVM toolchain installs. Every entry - # restores the compile job's cached `.ixe` — nothing recompiles here. + # own label, testbed, workload, and threshold flags. Every entry restores + # the compile job's cached `.ixe` — nothing recompiles here. # # What each backend measures: # - aiur: the proof pipeline — per constant, every stage plus the @@ -252,11 +254,6 @@ jobs: # (stage 2); the KZG stages will fold in as they land. One # subprocess per constant under the RAM watchdog; a too-large # prove is killed and recorded as a `status: oom` row. - # - zisk: executes the same constants in the zkVM (deterministic - # cycle counts; proving would need a GPU, so execute-only). Each - # constant runs as the shard partition the planner's RAM budget - # sized for it (one shard when it fits), reusing the pre-cut - # zkshards-/ dirs; builds its Rust host in-job. # - ooc: the same kernel run out-of-circuit and in parallel (much # faster). One whole-env row plus one row per constant. # - decompile: the inverse of compile. Roundtrip correctness is @@ -266,6 +263,9 @@ jobs: name: ${{ matrix.params.label }} needs: [compile, plan] runs-on: warp-ubuntu-latest-x64-32x + permissions: + contents: read + checks: write # `ix bench run` persists completed rows incrementally, so even a # job-level timeout keeps them on disk, but the bencher upload needs # the job alive. @@ -276,27 +276,15 @@ jobs: params: ${{ fromJson(needs.plan.outputs.matrix) }} steps: - uses: actions/checkout@v7 - - uses: actions/cache/restore@v6 + - uses: WarpBuilds/cache/restore@v2 with: path: ~/.local/bin key: bench-bins-${{ github.sha }} - name: Log run CPU + id: cpu uses: ./.github/actions/log-cpu with: label: Benchmark measurement CPU - provenance-file: ~/.local/bin/benchmark-build-cpu.txt - # The zkVM runs build their Rust host in-run; the rest run staged - # binaries only. (Restore an install-sp1 step here when sp1 is - # re-enabled in the registry.) - - if: matrix.params.backend == 'zisk' || matrix.params.backend == 'sp1' - uses: ./.github/actions/setup-rust-toolchain - with: - cache-workspaces: ${{ matrix.params.backend }} - - name: Install Zisk - if: matrix.params.backend == 'zisk' - uses: ./.github/actions/install-zisk - with: - proving-key: false - run: echo "$HOME/.local/bin" >> $GITHUB_PATH # Provision the toolchain so the staged binaries find libleanshared # (no package build). use-github-cache off: nothing to cache here, and @@ -308,33 +296,19 @@ jobs: use-github-cache: false # Pull the `.ixe` the compile job built — do NOT recompile here. # (The path list must match the compile job's save exactly.) - - uses: actions/cache/restore@v6 + - uses: WarpBuilds/cache/restore@v2 with: path: ${{ matrix.params.env }}.ixe key: bench-ixe-${{ github.sha }}-${{ matrix.params.env }} fail-on-cache-miss: true - # The pre-cut closure shards, for the backends that have any. Not - # fail-on-cache-miss: cutting them in the compile job is an - # optimisation, and `ix bench run` still cuts lazily without them. - - if: matrix.params.backend == 'zisk' || matrix.params.backend == 'sp1' - uses: actions/cache/restore@v6 - with: - path: zkshards-${{ matrix.params.env }} - key: bench-shards-${{ github.sha }}-${{ matrix.params.env }} # If the kernel rejects a constant, `ix bench run` exits 3 and this # step fails — that is a correctness regression, not a benchmark # blip. The completed rows are already on disk for the upload below. - name: Run ${{ matrix.params.label }} benchmark - run: | - # ZisK's ASM microservices mmap with MAP_LOCKED: raise the memlock - # hard limit in this shell so the tools `ix bench run` spawns - # inherit it. - if [ "${{ matrix.params.backend }}" = zisk ]; then - sudo prlimit --pid $$ --memlock=unlimited:unlimited - fi - ix bench run --backend ${{ matrix.params.backend }} \ - --env ${{ matrix.params.env }} --mode ${{ matrix.params.mode }} \ - --ixe ${{ matrix.params.env }}.ixe --out bench.json + run: >- + ix bench run --backend ${{ matrix.params.backend }} + --env ${{ matrix.params.env }} --mode ${{ matrix.params.mode }} + --ixe ${{ matrix.params.env }}.ixe --out bench.json # The ooc run writes a per-constant attribution CSV next to its # results file. Bencher stores metric rows only, so cache the CSV by # (SHA, cell) — bench-pr restores it to render the per-constant @@ -344,10 +318,24 @@ jobs: - name: Cache per-constant attribution CSV if: ${{ !cancelled() && matrix.params.backend == 'ooc' }} continue-on-error: true - uses: actions/cache/save@v6 + uses: WarpBuilds/cache/save@v2 with: path: bench.json.perconst.csv key: bench-perconst-${{ github.sha }}-${{ matrix.params.backend }}-${{ matrix.params.env }}-${{ matrix.params.mode }} + # The measurement host, by (SHA, parameters), for bench-pr to label a + # bencher-sourced base side — same best-effort contract as the CSV. + - name: Record measurement hardware + if: ${{ !cancelled() }} + env: + HARDWARE: ${{ steps.cpu.outputs.summary }} + run: printf '%s\n' "$HARDWARE" > bench-hardware.txt + - name: Cache measurement hardware + if: ${{ !cancelled() }} + continue-on-error: true + uses: WarpBuilds/cache/save@v2 + with: + path: bench-hardware.txt + key: bench-hardware-${{ github.sha }}-${{ matrix.params.backend }}-${{ matrix.params.env }}-${{ matrix.params.mode }} # Convert rows for upload even when the run step failed: bmf drops # every non-ok row (rejected or OOM), so only clean measurements # reach bencher. bmf exits nonzero when NO ok rows survive — the @@ -376,5 +364,5 @@ jobs: workload: ${{ matrix.params.workload }} file: bench-bmf.json key: ${{ secrets.BENCHER_API_KEY }} - github-token: ${{ secrets.GITHUB_TOKEN }} + github-token: ${{ github.token }} thresholds: ${{ matrix.params.thresholds }} diff --git a/.github/workflows/bench-pr.yml b/.github/workflows/bench-pr.yml index bd5cb24b1..4264f6b5f 100644 --- a/.github/workflows/bench-pr.yml +++ b/.github/workflows/bench-pr.yml @@ -3,9 +3,7 @@ # The base is the PR's own base branch — main for an unstacked PR, the # parent PR's head for a stacked one — and the report is labelled with it. # -# !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [decompile] | all) [execute] -# (sp1 is disabled in the registry (Ix/Cli/BenchCmd.lean) — the parser skips it -# with a note in the config summary) +# !benchmark ([aiur] [ooc] [compile] [decompile] | all) [execute] # BENCH_ENVS=InitStd,Mathlib # which compiled envs (case-insensitive, any registry env; # # defaults to every env for compile/decompile, InitStd # # for the rest) @@ -41,7 +39,7 @@ # token switches it to the fast Phase-1-only mode (witness # generation; no bencher baseline exists for that, so the base side # comes from a base-SHA run). -# - zisk / sp1 / ooc: `execute`. +# - ooc: `execute`. # - compile: `ix compile .lean` → `.ixe`. # - decompile: `ix decompile` over the compile run's fresh `.ixe`. # The bare `fresh` token skips the bencher fetch and prevents persistent @@ -64,10 +62,10 @@ # access (anti-poisoning; no token permission can override it), so cache # saves would all fail. The issue_comment run therefore only checks the # commenter is an org MEMBER/OWNER and re-dispatches this same file as -# workflow_dispatch, which is allowed to save caches. The relay rejects fork -# PRs before dispatch so only repository writers can supply code to that cache -# scope. Manual dispatch already requires repo write access and may -# intentionally compare loose commits. +# workflow_dispatch, which is allowed to save caches. The MEMBER/OWNER command +# explicitly authorizes that PR head to run in the cache-writing context. +# Manual dispatch already requires repo write access and may intentionally +# compare loose commits. name: Benchmark pull requests on: @@ -98,8 +96,6 @@ run-name: "${{ github.event_name == 'workflow_dispatch' && format('Benchmark PR permissions: contents: read - issues: read - pull-requests: read jobs: dispatch: @@ -126,11 +122,6 @@ jobs: COMMENT_BODY: ${{ github.event.comment.body }} PR_NUMBER: ${{ github.event.issue.number }} run: | - head_repo=$(gh api "repos/$GITHUB_REPOSITORY/pulls/$PR_NUMBER" --jq '.head.repo.full_name') - if [ "$head_repo" != "$GITHUB_REPOSITORY" ]; then - echo "::error::Comment-triggered benchmarks require a same-repository PR head" - exit 1 - fi gh workflow run bench-pr.yml \ --repo "$GITHUB_REPOSITORY" \ --ref "${{ github.event.repository.default_branch }}" \ @@ -145,12 +136,11 @@ jobs: # artifact for every later job. Normal runs may select a persistent # head-SHA cache. A cached `ix` may bootstrap command parsing, but `fresh` # replaces the full bundle before it is published to benchmark jobs. - # Built on a warp runner like bench-main's binaries, so both sides share - # the same instruction set (AVX-512) — and every job that runs these - # binaries must be a warp host too, or a plain GitHub host crashes with - # an illegal instruction. The job ends by parsing the !benchmark command - # with the selected `ix bench ci parse`: the registry lives in Lean, so - # the matrix can only be computed after a binary is available. + # Built on a Warp runner like bench-main's binaries, so both sides use the + # same fixed AVX-512 baseline and benchmark testbed. The job ends by parsing + # the !benchmark command with the selected `ix bench ci parse`: the registry + # lives in Lean, so the matrix can only be computed after a binary is + # available. build: if: github.event_name == 'workflow_dispatch' runs-on: warp-ubuntu-latest-x64-32x @@ -165,7 +155,7 @@ jobs: # rejected; the failure comment quotes it. parse-error: ${{ steps.parse.outputs.parse-error }} steps: - # The relay admits only same-repository heads; manual dispatch requires + # Comment dispatch requires an org MEMBER/OWNER; manual dispatch requires # repo write access. Emit the validated full SHA once for every checkout. - name: Validate SHAs id: target @@ -182,7 +172,7 @@ jobs: # The job builds and runs PR code; never leave the token in .git. persist-credentials: false - id: bins - uses: actions/cache/restore@v6 + uses: WarpBuilds/cache/restore@v2 with: path: ~/.local/bin key: bench-bins-${{ steps.target.outputs.revision }} @@ -190,6 +180,8 @@ jobs: # remaining binaries are built after parsing, when `fresh` is known. - if: steps.bins.outputs.cache-hit != 'true' uses: ./.github/actions/setup-rust-toolchain + with: + cache-provider: warpbuild # A persistent hit still needs the matching toolchain for libleanshared. - uses: leanprover/lean-action@v1 with: @@ -214,40 +206,27 @@ jobs: # run replaces it before the bundle can reach any measured job. - if: steps.parse.outputs.fresh == '1' && steps.bins.outputs.cache-hit == 'true' uses: ./.github/actions/setup-rust-toolchain - # `.cargo/config.toml` sets `-Ctarget-cpu=native`; log the build CPU so a - # benchmark shift can be traced to the host that selected the native - # instruction set. The report travels with the binaries below. + with: + cache-provider: warpbuild - name: Log build CPU - if: steps.parse.outputs.fresh == '1' || steps.bins.outputs.cache-hit != 'true' uses: ./.github/actions/log-cpu with: label: Benchmark binary build CPU - output-file: ${{ runner.temp }}/benchmark-build-cpu.txt - name: Build benchmark binaries if: steps.parse.outputs.fresh == '1' || steps.bins.outputs.cache-hit != 'true' run: | lake build ix bench-typecheck cp .lake/build/bin/ix .lake/build/bin/bench-typecheck ~/.local/bin/ - cp "${{ runner.temp }}/benchmark-build-cpu.txt" ~/.local/bin/ chmod +x ~/.local/bin/ix ~/.local/bin/bench-typecheck - # Cache entries are immutable and may lack optional provenance. Keep the - # run artifact's shape stable and state explicitly when its build host is - # unknown. - - name: Ensure build CPU provenance - run: | - if [ ! -s "$HOME/.local/bin/benchmark-build-cpu.txt" ]; then - echo "Benchmark binary build CPU unavailable: cache predates CPU provenance." \ - > "$HOME/.local/bin/benchmark-build-cpu.txt" - fi - if: steps.parse.outputs.fresh != '1' && steps.bins.outputs.cache-hit != 'true' - uses: actions/cache/save@v6 + uses: WarpBuilds/cache/save@v2 with: path: ~/.local/bin key: bench-bins-${{ steps.target.outputs.revision }} - name: Package run binaries run: >- tar -C "$HOME/.local/bin" -cf benchmark-binaries.tar - ix bench-typecheck benchmark-build-cpu.txt + ix bench-typecheck - name: Upload run binaries uses: actions/upload-artifact@v7 with: @@ -261,13 +240,16 @@ jobs: # error message if the parse/build failed, otherwise a "running…" # placeholder so the commenter gets immediate feedback. The `comment` # job at the end edits this same comment in place with the results - # (this job's output is the comment id). Holds the App token, so — like - # `comment` — it never checks out or runs PR code; it only reads + # (this job's output is the comment id). This job has write permissions, + # so — like `comment` — it never checks out or runs PR code; it only reads # build's string outputs. announce: needs: build if: always() && github.event_name == 'workflow_dispatch' runs-on: ubuntu-latest + permissions: + issues: write + pull-requests: write outputs: comment-id: ${{ steps.post.outputs.comment-id }} steps: @@ -299,24 +281,18 @@ jobs: echo if [ -n "$SUMMARY" ]; then echo "> $SUMMARY" - echo fi + echo echo "Benchmarking \`${HEAD_SHA:0:7}\` — this comment will be replaced with the results when the run finishes." echo echo "[Watch progress]($RUN_URL)" } > comment-body.md fi - - name: Generate token to write PR comment - id: app-token - uses: actions/create-github-app-token@v3 - with: - client-id: ${{ secrets.TOKEN_APP_ID }} - private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }} - name: Post initial comment id: post uses: peter-evans/create-or-update-comment@v5 with: - token: ${{ steps.app-token.outputs.token }} + token: ${{ github.token }} issue-number: ${{ inputs.pr }} body-path: comment-body.md @@ -356,9 +332,9 @@ jobs: - name: Restore published .ixe if: needs.build.outputs.fresh != '1' id: pr-ixe - uses: actions/cache/restore@v6 + uses: WarpBuilds/cache/restore@v2 with: - # actions/cache derives an entry's version from its path list, so + # The cache derives an entry's version from its path list, so # the list is effectively part of the key: this one path matches # bench-main's compile-job save, which lets a stacked PR's base # run reach either producer's entry from one restore. @@ -367,11 +343,11 @@ jobs: - name: Restore published compile row if: needs.build.outputs.fresh != '1' id: pr-row - uses: actions/cache/restore@v6 + uses: WarpBuilds/cache/restore@v2 with: path: | compile.json - compile-cpu-warnings.md + compile-hardware.txt key: bench-pr-row-${{ needs.build.outputs.revision }}-${{ matrix.env }} - name: Select compile source id: compile-source @@ -390,18 +366,15 @@ jobs: - name: Unpack run binaries if: steps.compile-source.outputs.rebuild == 'true' run: | - rm -f compile-cpu-warnings.md mkdir -p "$HOME/.local/bin" tar -C "$HOME/.local/bin" -xf benchmark-binaries.tar echo "$HOME/.local/bin" >> "$GITHUB_PATH" - name: Log compile CPU if: steps.compile-source.outputs.rebuild == 'true' + id: cpu uses: ./.github/actions/log-cpu with: label: Compile measurement CPU - provenance-file: ~/.local/bin/benchmark-build-cpu.txt - provenance-label: PR benchmark binaries during compile - warning-file: compile-cpu-warnings.md # Pointed at the Benchmarks/Compile subpackage (same toolchain as # the root): mathlib is a dependency only there, so the mathlib # cache fetch has to run from that directory. @@ -424,9 +397,17 @@ jobs: - name: Compile ${{ matrix.env }}.ixe if: steps.compile-source.outputs.rebuild == 'true' run: ix bench run --backend compile --env ${{ matrix.env }} --out compile.json + # The compile row is measured here, not in the benchmark job that + # renders it, so its host travels with the row: same cache entry and + # run artifact below. + - name: Record compile hardware + if: steps.compile-source.outputs.rebuild == 'true' + env: + HARDWARE: ${{ steps.cpu.outputs.summary }} + run: printf '%s\n' "$HARDWARE" > compile-hardware.txt - name: Publish .ixe if: needs.build.outputs.fresh != '1' && steps.pr-ixe.outputs.cache-hit != 'true' - uses: actions/cache/save@v6 + uses: WarpBuilds/cache/save@v2 with: # Path lists are version-significant — keep this identical to the # restore above and to bench-main's save. @@ -436,11 +417,11 @@ jobs: # reuses it as its PR side (same runner class, binaries, command). - name: Publish compile row if: needs.build.outputs.fresh != '1' && steps.pr-row.outputs.cache-hit != 'true' - uses: actions/cache/save@v6 + uses: WarpBuilds/cache/save@v2 with: path: | compile.json - compile-cpu-warnings.md + compile-hardware.txt key: bench-pr-row-${{ needs.build.outputs.revision }}-${{ matrix.env }} - name: Upload run environment uses: actions/upload-artifact@v7 @@ -449,7 +430,7 @@ jobs: path: | ${{ matrix.env }}.ixe compile.json - compile-cpu-warnings.md + compile-hardware.txt if-no-files-found: error retention-days: 1 overwrite: true @@ -514,12 +495,10 @@ jobs: tar -C .lake/build/bin -xf benchmark-binaries.tar echo "$PWD/.lake/build/bin" >> "$GITHUB_PATH" - name: Log run CPU + id: cpu uses: ./.github/actions/log-cpu with: label: Benchmark job CPU - provenance-file: .lake/build/bin/benchmark-build-cpu.txt - provenance-label: PR benchmark binaries in this job - warning-file: cpu-warnings.md # Toolchain only (no package build, no mathlib cache): the restored # binaries need the toolchain's libleanshared to run. This job never # compiles an env — the `.ixe` and compile row come from the compile @@ -535,24 +514,6 @@ jobs: uses: actions/download-artifact@v8 with: name: benchmark-env-${{ matrix.params.env }} - # zkVM runs additionally need the Rust toolchain + the backend's toolchain - # and system deps (the shared composite install actions). - - name: Set up zkVM Rust toolchain - if: matrix.params.backend == 'zisk' || matrix.params.backend == 'sp1' - uses: ./.github/actions/setup-rust-toolchain - with: - cache-workspaces: ${{ matrix.params.backend }} - # sp1 is disabled in the registry (execute too slow for CI); - # re-enable it there and uncomment this install step to restore it. - # - name: Install SP1 - # if: matrix.params.backend == 'sp1' - # uses: ./.github/actions/install-sp1 - - name: Install Zisk - if: matrix.params.backend == 'zisk' - uses: ./.github/actions/install-zisk - with: - proving-key: false - # ---------- PR side ---------- # The PR side runs first: `ix bench run` selects its constants from # the shared set (Ix/BenchConstants.lean), and pr.json's row names @@ -566,11 +527,6 @@ jobs: # the job, after the table upload. continue-on-error: true run: | - if [ "$BACKEND" = zisk ]; then - # ZisK's ASM microservices mmap with MAP_LOCKED: raise the memlock - # hard limit in this shell so the spawned tools inherit it. - sudo prlimit --pid $$ --memlock=unlimited:unlimited - fi if [ "$BACKEND" = compile ]; then # The compile job already measured this env's compile (same # runner class, binaries, and command) — reuse its row instead @@ -638,10 +594,20 @@ jobs: id: perconst if: matrix.params.backend == 'ooc' && env.FRESH != '1' continue-on-error: true - uses: actions/cache/restore@v6 + uses: WarpBuilds/cache/restore@v2 with: path: bench.json.perconst.csv key: bench-perconst-${{ env.BASE_SHA }}-${{ matrix.params.backend }}-${{ matrix.params.env }}-${{ matrix.params.mode }} + # The host that measured the base SHA's rows on main, recorded by + # bench-main next to its bencher upload. Only a bencher-sourced base side + # uses it; a base run in this job is labelled with this runner instead. + - name: Restore base-side measurement hardware + if: env.FRESH != '1' + continue-on-error: true + uses: WarpBuilds/cache/restore@v2 + with: + path: bench-hardware.txt + key: bench-hardware-${{ env.BASE_SHA }}-${{ matrix.params.backend }}-${{ matrix.params.env }}-${{ matrix.params.mode }} # The final base-run decision — every base-side step gates on THIS # step. A base run, whatever triggered it (bencher miss or partial, # `fresh`, or an ooc attribution-CSV cache miss), is always a FULL @@ -675,41 +641,31 @@ jobs: - name: Restore base binaries (bench-bins cache) if: steps.decide.outputs.run-base == 'true' && env.FRESH != '1' id: base-bins - uses: actions/cache/restore@v6 + uses: WarpBuilds/cache/restore@v2 with: path: ~/.local/bin key: bench-bins-${{ env.BASE_SHA }} # Two producers compile the env at a given SHA: bench-main for main # commits, this workflow's compile job for PR heads. A stacked PR's # base is the latter, so both keys are tried from one step. This works - # because both producers save the same single path; actions/cache - # versions an entry by its paths. restore-keys matches by prefix, so + # because both producers save the same single path; the cache versions + # an entry by its paths. restore-keys matches by prefix, so # no registry env name may be a prefix of another. - name: Restore base .ixe (bench-main or bench-pr compile cache) if: steps.decide.outputs.run-base == 'true' && env.FRESH != '1' id: base-ixe - uses: actions/cache/restore@v6 + uses: WarpBuilds/cache/restore@v2 with: path: ${{ matrix.params.env }}.ixe key: bench-ixe-${{ env.BASE_SHA }}-${{ matrix.params.env }} restore-keys: | bench-pr-ixe-${{ env.BASE_SHA }}-${{ matrix.params.env }} - # Shards live in their own entry and only exist for the zkVM - # backends; without them `ix bench run` cuts them itself. - - name: Restore base closure shards - if: >- - steps.decide.outputs.run-base == 'true' && env.FRESH != '1' && - (matrix.params.backend == 'zisk' || matrix.params.backend == 'sp1') - uses: actions/cache/restore@v6 - with: - path: zkshards-${{ matrix.params.env }} - key: bench-shards-${{ env.BASE_SHA }}-${{ matrix.params.env }} # Cached base binaries are only usable when both `lean-toolchain` # files match, and — for Mathlib — only when the `.ixe` also # restored (otherwise the base side would need mathlib oleans that # only a full build fetches). Usable binaries go into # base/.lake/build/bin, where `ix bench run --repo base` finds them; - # a from-scratch base build puts them there natively. + # a from-scratch base build puts them there directly. - name: Resolve base binaries if: steps.decide.outputs.run-base == 'true' id: base-src @@ -727,7 +683,6 @@ jobs: if [ "$BENV" != Mathlib ] || [ "$ixe" = true ]; then mkdir -p base/.lake/build/bin mv ~/.local/bin/ix ~/.local/bin/bench-typecheck base/.lake/build/bin/ 2>/dev/null || true - mv ~/.local/bin/benchmark-build-cpu.txt base/.lake/build/bin/ 2>/dev/null || true [ -x base/.lake/build/bin/ix ] && [ -x base/.lake/build/bin/bench-typecheck ] \ && cached=true fi @@ -735,20 +690,26 @@ jobs: echo "cached=$cached" >> "$GITHUB_OUTPUT" echo "base .ixe: $([ "$ixe" = true ] && echo restored from cache || echo compiling in the base run)" echo "base binaries: $([ "$cached" = true ] && echo restored from cache || echo building from source)" - - name: Log cached base binary build CPU - if: steps.decide.outputs.run-base == 'true' && steps.base-src.outputs.cached == 'true' - uses: ./.github/actions/log-cpu + # A from-scratch base build must match the PR and main binaries: the + # same pinned x86-64-v4 codegen (RUSTFLAGS overrides the tree's + # `.cargo/config.toml`, which selects `native`) and an installed + # toolchain. The action installs the PR checkout's toolchain; the base + # tree may pin a different channel, so ensure its own is present too. + - name: Set up Rust for the base build + if: steps.decide.outputs.run-base == 'true' && steps.base-src.outputs.cached != 'true' + uses: ./.github/actions/setup-rust-toolchain with: - log-current: "false" - provenance-file: base/.lake/build/bin/benchmark-build-cpu.txt - provenance-label: Cached base benchmark binaries - warning-file: cpu-warnings.md + cache-provider: warpbuild + cache-workspaces: base + - name: Install the base tree's Rust toolchain + if: steps.decide.outputs.run-base == 'true' && steps.base-src.outputs.cached != 'true' + working-directory: base + run: rustup show active-toolchain || rustup toolchain install - name: Log base build CPU if: steps.decide.outputs.run-base == 'true' && steps.base-src.outputs.cached != 'true' uses: ./.github/actions/log-cpu with: label: Base benchmark binary build CPU - output-file: base/.lake/build/bin/benchmark-build-cpu.txt - name: Build base (ix, bench-typecheck) if: steps.decide.outputs.run-base == 'true' && steps.base-src.outputs.cached != 'true' uses: leanprover/lean-action@v1 @@ -789,12 +750,6 @@ jobs: run: | if [ "${{ steps.base-src.outputs.ixe }}" = true ]; then mv "${{ matrix.params.env }}.ixe" "base/${{ matrix.params.env }}.ixe" - # Shards, when restored above: in place, `ix bench run` skips - # re-cutting them for the base tree. - mv "zkshards-${{ matrix.params.env }}" "base/zkshards-${{ matrix.params.env }}" 2>/dev/null || true - fi - if [ "$BACKEND" = zisk ]; then - sudo prlimit --pid $$ --memlock=unlimited:unlimited fi flags="" if [ -n "$CONSTS" ]; then @@ -846,18 +801,35 @@ jobs: mv bench.json.perconst.csv "$GITHUB_WORKSPACE/main.json.perconst.csv" fi - name: Build comparison table + env: + RUN_HARDWARE: ${{ steps.cpu.outputs.summary }} run: | mkdir -p out - if [ "$BACKEND" = compile ] && [ -s compile-cpu-warnings.md ]; then - cat compile-cpu-warnings.md >> cpu-warnings.md - fi ix bench compare \ --backend "$BACKEND" --env "$BENV" --mode "$MODE" \ --base "$GITHUB_WORKSPACE/main.json" --pr "$GITHUB_WORKSPACE/pr.json" \ --base-source "${{ steps.decide.outputs.source }}" \ --base-label "${BASE_REF:-${BASE_SHA::7}}" \ - --warning-file "$GITHUB_WORKSPACE/cpu-warnings.md" \ --out "out/table-$LABEL.md" + # Label each side with the host that measured it. The fleet mixes + # CPU models, and the two sides need not share one: the PR compile + # row comes from the compile job, and a bencher-sourced base side + # from bench-main's run at the base SHA. Every other side ran here. + if [ "$BACKEND" = compile ]; then + pr_hw=$(cat compile-hardware.txt 2>/dev/null || true) + else + pr_hw="$RUN_HARDWARE" + fi + if [ "${{ steps.decide.outputs.run-base }}" = true ]; then + base_hw="$RUN_HARDWARE" + else + base_hw=$(cat bench-hardware.txt 2>/dev/null || true) + fi + { + echo + echo "- Base hardware (${{ steps.decide.outputs.source }}): ${base_hw:-not recorded}" + echo "- PR hardware: ${pr_hw:-not recorded}" + } >> "out/table-$LABEL.md" cat "out/table-$LABEL.md" - name: Upload table @@ -878,15 +850,15 @@ jobs: # Assemble the comment body from the per-run tables. Deliberately # UNPRIVILEGED: this job runs PR-built code (`ix bench report`), so it - # must never hold the App token. The posting job below only downloads + # must never receive write permissions. The posting job below only downloads # the finished body and never touches PR code. assemble: needs: [build, benchmark] # Assemble even when benchmark runs failed — the tables carry the ❌ # rows. Only the build job must have succeeded (it made the binaries). if: always() && needs.build.result == 'success' - # The report command uses the build job's native `ix`, so keep it on the - # Warp x64 runner fleet; report assembly does not need benchmark-scale RAM. + # The report command uses the build job's fixed-AVX-512 `ix`, so keep it on + # compatible Warp x64 hardware; report assembly needs little RAM. runs-on: warp-ubuntu-latest-x64-8x permissions: contents: read @@ -938,12 +910,15 @@ jobs: # Replace the announce comment with the assembled results — or with an # error note when a stage failed: a rejected command or broken run must # never end in silence on the PR. This job and `announce` are the only - # two with the App token, and neither checks out or runs repo code — - # just an artifact download and two actions. + # two with write permissions, and neither checks out or runs repo code — + # just an artifact download and the comment action. comment: needs: [build, compile, benchmark, assemble, announce] if: always() && github.event_name == 'workflow_dispatch' runs-on: ubuntu-latest + permissions: + issues: write + pull-requests: write steps: - name: Download comment body if: needs.assemble.result == 'success' @@ -981,21 +956,13 @@ jobs: echo "[Workflow logs](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }})" } > comment-body.md fi - - name: Generate token to write PR comment - id: app-token - uses: actions/create-github-app-token@v3 - with: - # `client-id` accepts the numeric App ID too (the JWT issuer claim - # takes either), so the existing secret works unchanged. - client-id: ${{ secrets.TOKEN_APP_ID }} - private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }} # `comment-id` targets the announce comment; if announce never # posted one (empty id), `issue-number` makes this create a fresh # comment instead. `replace` overwrites the "running…" placeholder. - name: Post / update comment uses: peter-evans/create-or-update-comment@v5 with: - token: ${{ steps.app-token.outputs.token }} + token: ${{ github.token }} issue-number: ${{ inputs.pr }} comment-id: ${{ needs.announce.outputs.comment-id }} edit-mode: replace diff --git a/.github/workflows/bencher-plots.yml b/.github/workflows/bencher-plots.yml index 2db968c67..25cf09b54 100644 --- a/.github/workflows/bencher-plots.yml +++ b/.github/workflows/bencher-plots.yml @@ -24,8 +24,8 @@ permissions: jobs: sync-plots: - # The restored `ix` uses native target features selected on the benchmark - # build runner, even though this subcommand itself is pure Lean. + # The restored `ix` targets the benchmark fleet's fixed AVX-512 baseline, + # so even this pure-Lean subcommand needs compatible Warp x64 hardware. runs-on: warp-ubuntu-latest-x64-8x steps: - uses: actions/checkout@v7 @@ -33,7 +33,7 @@ jobs: # exact cache when bench-main has finished its build, else the newest # available (prefix match) — whose compiled-in registry may then lag # the checkout. - - uses: actions/cache/restore@v6 + - uses: WarpBuilds/cache/restore@v2 with: path: ~/.local/bin key: bench-bins-${{ github.sha }} @@ -46,7 +46,7 @@ jobs: auto-config: false build: false use-github-cache: false - - uses: bencherdev/bencher@v0.6.11 + - uses: bencherdev/bencher@v0.6.12 # Plot create/delete needs those permissions on the ix project: a # user-scoped `bencher_user_*` key (the report-upload token the bench # workflows use may be run-scoped and unable to manage plots). diff --git a/.github/workflows/bencher-thresholds-reset.yml b/.github/workflows/bencher-thresholds-reset.yml index 90111bcde..f9958af04 100644 --- a/.github/workflows/bencher-thresholds-reset.yml +++ b/.github/workflows/bencher-thresholds-reset.yml @@ -53,17 +53,18 @@ on: issue_comment: types: [created] -permissions: - contents: write - pull-requests: write - issues: write # ack creates/applies the bencher-thresholds-reset: label +permissions: {} jobs: reset: if: github.event_name == 'workflow_dispatch' || github.event.pull_request.merged == true runs-on: ubuntu-latest + permissions: + contents: write + issues: write + pull-requests: write env: - GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} + GH_TOKEN: ${{ github.token }} REPO: ${{ github.repository }} EVENT: ${{ github.event_name }} INPUT_WORKLOAD: ${{ inputs.workload }} @@ -122,8 +123,11 @@ jobs: ack: if: github.event_name == 'issue_comment' && github.event.issue.pull_request && github.event.issue.state == 'open' && github.event.comment.user.type != 'Bot' && contains(github.event.comment.body, '!bencher-thresholds-reset') && (github.event.comment.author_association == 'OWNER' || github.event.comment.author_association == 'MEMBER' || github.event.comment.author_association == 'COLLABORATOR') runs-on: ubuntu-latest + permissions: + issues: write + pull-requests: write env: - GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} + GH_TOKEN: ${{ github.token }} REPO: ${{ github.repository }} PR: ${{ github.event.issue.number }} BODY: ${{ github.event.comment.body }} diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 267f0b62e..88a9d5cc6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -13,29 +13,33 @@ concurrency: cancel-in-progress: true jobs: - # Build Ix once and cache `.lake` under lean-action's per-sha key. That cache - # holds the base Ix build — lean-action saves it right after building the - # default lib, before the all-targets lint below — and the parallel lean-test - # job and merge-tests.yml's Lake jobs restore it instead of recompiling the - # base. `test: false` keeps this job build-only; those jobs run the tests. It - # also compiles and publishes the small `nataddcomm.ixe` fixture the zkVM - # execution gates (sp1-build/zisk-build) run their guests over: they need this - # exact `ix` build, so they consume it as an artifact and gate on this job - # succeeding. + # Build every regular Lake target before the test fan-out. The Namespace + # volume is committed only after this job succeeds, so every saved build + # cache contains the complete build rather than one parallel job's subset. + # The small `nataddcomm.ixe` fixture is passed separately to the zkVM jobs. build: - runs-on: warp-ubuntu-latest-x64-16x + runs-on: + - nscloud-ubuntu-26.04-amd64-16x32-with-cache + - nscloud-cache-size-50gb + - nscloud-cache-tag-argumentcomputer-ix steps: - uses: actions/checkout@v7 - uses: ./.github/actions/setup-rust-toolchain + with: + use-github-cache: "false" + - uses: ./.github/actions/setup-lake-cache - uses: leanprover/lean-action@v1 with: build-args: "--wfail -v" test: false + use-github-cache: false # build-all lint driver compiles every lib/exe target with --wfail, so a # warning in any target (exes, benchmarks, Apps) — not just the default lib # lean-action builds above — fails CI. - name: Build all targets run: lake lint -- --wfail -v + - name: Build Ix.Tc formal verification + run: lake build IxTcVerify - name: Check codegen'd IxVM kernel is up to date run: lake exe ix codegen --check - name: Check Lean versions match for Ix and compiler bench @@ -54,31 +58,21 @@ jobs: if-no-files-found: error retention-days: 1 - # The primary test tier, plus the two extras, over the base build the - # `build` job cached. Restores `.lake` read-only (exact per-sha key the - # `build` job wrote, prefix fallback otherwise); lean-action runs the whole - # primary tier as a bare `lake test` against that restored build (no - # build/cache of its own). No `--wfail` there: `test-args` is declared but - # unwired in the released `v1`, so it would be silently ignored, and the - # `build` job already compiles every lib and exe -- `Tests` and `IxTests` - # included -- under `lake lint -- --wfail -v`. The CLI step covers the one - # primary runner that is special-cased ahead of suite dispatch in - # `Tests/Main.lean`; ignored suites run only in `merge-tests.yml`. + # The primary Lean test tier consumes the completed build cache read-only. + # Within this workflow, build and rust-test are the only ordered writers. lean-test: needs: build - runs-on: warp-ubuntu-latest-x64-16x + runs-on: + - nscloud-ubuntu-26.04-amd64-16x32-with-cache + - nscloud-cache-size-50gb + - nscloud-cache-tag-argumentcomputer-ix + - nscloud-cache-exp-do-not-commit steps: - uses: actions/checkout@v7 - uses: ./.github/actions/setup-rust-toolchain - # `./.lake`, not `.lake`: the cache path is hashed into the entry's - # version, and lean-action saves under `./.lake`, so a bare `.lake` here - # computes a different version and the restore misses despite the key - # matching. - - uses: actions/cache/restore@v6 - with: - path: ./.lake - key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} - restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}- + with: + use-github-cache: "false" + - uses: ./.github/actions/setup-lake-cache - uses: leanprover/lean-action@v1 with: auto-config: false @@ -87,11 +81,24 @@ jobs: - name: Test Ix CLI run: lake test --wfail -- cli + # Lake and root Cargo builds both use the repository's target directory, so + # build and rust-test share a volume in dependency order. Namespace volumes + # are last-write-wins; parallel zkVM writers use dedicated tags, while CUDA + # consumes the primary cache without committing its feature-specific output. + # Namespace's remote sccache could share compatible compilation units across + # the zkVM volumes without serializing the jobs. rust-test: - runs-on: warp-ubuntu-latest-x64-8x + needs: build + runs-on: + - nscloud-ubuntu-26.04-amd64-8x16-with-cache + - nscloud-cache-size-50gb + - nscloud-cache-tag-argumentcomputer-ix steps: - uses: actions/checkout@v7 - uses: ./.github/actions/setup-rust-toolchain + with: + use-github-cache: "false" + - uses: ./.github/actions/setup-lake-cache - uses: taiki-e/install-action@nextest # Install Lean for rust-bindgen step - uses: leanprover/lean-action@v1 @@ -117,8 +124,19 @@ jobs: # Compile and link the opt-in backend without requiring a GPU. Runtime and # proof-byte equivalence are covered by multi-stark's NVIDIA smoke suite. cuda-compile: - runs-on: warp-ubuntu-latest-x64-8x - container: nvidia/cuda:12.8.1-devel-ubuntu24.04 + needs: build + runs-on: + - nscloud-ubuntu-26.04-amd64-8x16-with-cache + - nscloud-cache-size-50gb + - nscloud-cache-tag-argumentcomputer-ix + - nscloud-cache-exp-do-not-commit + container: + image: nvidia/cuda:13.3.1-devel-ubuntu26.04 + env: + NSC_CACHE_PATH: ${{ env.NSC_CACHE_PATH }} + volumes: + - /cache:/cache + options: --cap-add=SYS_ADMIN env: # This job validates feature plumbing and the Rust-staticlib-to-Lean # link without paying for a GPU runner. Multi-stark CI compiles the @@ -131,8 +149,11 @@ jobs: run: | apt-get update apt-get install --yes --no-install-recommends \ - build-essential ca-certificates curl git libclang-dev + build-essential ca-certificates curl git libclang-dev sudo - uses: ./.github/actions/setup-rust-toolchain + with: + use-github-cache: "false" + - uses: ./.github/actions/setup-lake-cache - uses: leanprover/lean-action@v1 with: auto-config: false @@ -144,13 +165,11 @@ jobs: # zkVM host build + execute gate: do the Zisk/SP1 hosts (and their guest # ELFs, via each workspace's build.rs) still compile AND run? rust-test - # doesn't build these workspaces (special toolchains), and bench-main.yml's - # zkVM runs — which also run real executions — tolerate per-constant - # failures by design (dropped rows, OOM sentinels), so they never turn red - # on a breakage. These jobs are the red-X signal: each builds its host, then - # runs the guest in the VM over `nataddcomm.ixe` (a ~40-constant closure the - # `build` job publishes as an artifact). They run in parallel with the test - # jobs and with each other after `build` succeeds. Both hosts exit + # doesn't build these workspaces because they need special toolchains. These + # jobs are the red-X signal: each builds its host, then runs the guest in the + # VM over `nataddcomm.ixe` (a ~40-constant closure the `build` job publishes + # as an artifact). They run in parallel with the test jobs and with each + # other after `build` succeeds. Both hosts exit # non-zero when the kernel rejects a constant (sp1: EXIT_REJECTED; zisk: # `reject_failures`), so a guest that compiles but panics / faults / rejects # fails the job. Both execute paths are keyless: Zisk uses its SDK's @@ -160,12 +179,20 @@ jobs: sp1-build: name: SP1 host build needs: build - runs-on: warp-ubuntu-latest-x64-16x + runs-on: + - nscloud-ubuntu-26.04-amd64-8x16-with-cache + - nscloud-cache-size-50gb + - nscloud-cache-tag-argumentcomputer-ix-sp1 steps: - uses: actions/checkout@v7 - uses: ./.github/actions/setup-rust-toolchain with: - cache-workspaces: sp1 + use-github-cache: "false" + - uses: ./.github/actions/setup-lake-cache + with: + additional-paths: | + ${{ github.workspace }}/sp1/target + ${{ github.workspace }}/sp1/guest/target - uses: ./.github/actions/install-sp1 # The precompile-aware SP1 runner-binary is auto-built from the fork git # dep by `sp1-core-executor-runner`'s build script — no manual override. @@ -199,12 +226,21 @@ jobs: zisk-build: name: Zisk host build needs: build - runs-on: warp-ubuntu-latest-x64-16x + runs-on: + - nscloud-ubuntu-26.04-amd64-8x16-with-cache + - nscloud-cache-size-50gb + - nscloud-cache-tag-argumentcomputer-ix-zisk steps: - uses: actions/checkout@v7 - uses: ./.github/actions/setup-rust-toolchain with: - cache-workspaces: zisk + use-github-cache: "false" + - uses: ./.github/actions/setup-lake-cache + with: + additional-paths: | + ${{ github.workspace }}/zisk/target + ${{ github.workspace }}/zisk/guest/target + ${{ github.workspace }}/zisk/agg-guest/target - uses: ./.github/actions/install-zisk with: proving-key: false diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index ab4d1c4c2..4963e986e 100644 --- a/.github/workflows/codeql.yml +++ b/.github/workflows/codeql.yml @@ -8,9 +8,8 @@ # The gates are job-level `if`s rather than workflow-level `on.paths` # (or a dynamically-built matrix) deliberately: a required check that # never triggers sticks at "Expected", while a skipped job satisfies it. -# When the rust analysis does run, it runs on a warp host (CodeQL scales -# with cores; default setup pins it to a stock 4-core runner) with the -# dependency extraction cached between runs. +# Rust analysis runs only when Rust inputs change, with dependency extraction +# cached between runs. name: CodeQL on: diff --git a/.github/workflows/merge-tests-stub.yml b/.github/workflows/merge-tests-stub.yml new file mode 100644 index 000000000..1c829bc14 --- /dev/null +++ b/.github/workflows/merge-tests-stub.yml @@ -0,0 +1,21 @@ +name: Merge tests (pull request) + +# The "Merge tests" required check is enforced by merge-tests.yml, which runs +# the ignored suites only against the merge queue's synthetic commit. A pull +# request cannot enter the queue until every required check has passed on its +# own head, so this workflow reports the same check name there and does +# nothing else. It triggers only on pull_request so that a merge-group commit +# carries exactly one "Merge tests" check run — the real one — and no skipped +# stub alongside it. +on: + pull_request: + +permissions: {} + +jobs: + merge-tests: + name: Merge tests + runs-on: ubuntu-latest + steps: + - name: Defer tests to merge queue + run: echo "Merge tests run against the merge group's synthetic commit." diff --git a/.github/workflows/merge-tests.yml b/.github/workflows/merge-tests.yml index dccdf83cd..0d6dad72c 100644 --- a/.github/workflows/merge-tests.yml +++ b/.github/workflows/merge-tests.yml @@ -1,9 +1,15 @@ name: Merge tests on: - pull_request: - branches: [main] merge_group: + issue_comment: + types: [created] + # Only the valgrind job runs on pull requests, as a trial of the + # GitHub-hosted runner's build and cache times before it takes that role + # in the queue permanently. + pull_request: + +run-name: "${{ github.event_name == 'issue_comment' && format('Merge tests for PR #{0}', github.event.issue.number) || 'Merge tests' }}" permissions: contents: read @@ -12,16 +18,81 @@ permissions: # cannot satisfy the required check, so runs are never superseded here. jobs: + prepare: + name: Prepare merge tests + if: >- + github.event_name == 'merge_group' || + (github.event_name == 'issue_comment' && + github.event.issue.pull_request && + github.event.issue.state == 'open' && + github.event.comment.user.type != 'Bot' && + contains(github.event.comment.body, '!merge-tests') && + (github.event.comment.author_association == 'MEMBER' || + github.event.comment.author_association == 'OWNER')) + runs-on: ubuntu-latest + permissions: + issues: write + pull-requests: write + outputs: + comment-id: ${{ steps.post.outputs.comment-id }} + pr: ${{ steps.target.outputs.pr }} + revision: ${{ steps.target.outputs.revision }} + steps: + - name: Resolve test revision + id: target + env: + EVENT_NAME: ${{ github.event_name }} + EVENT_SHA: ${{ github.sha }} + GH_TOKEN: ${{ github.token }} + PR_NUMBER: ${{ github.event.issue.number }} + run: | + if [ "$EVENT_NAME" = issue_comment ]; then + [[ "$PR_NUMBER" =~ ^[1-9][0-9]*$ ]] \ + || { echo "::error::PR number must be a positive integer"; exit 1; } + revision=$(gh api "repos/$GITHUB_REPOSITORY/pulls/$PR_NUMBER" \ + --jq '.merge_commit_sha // empty') + echo "pr=$PR_NUMBER" >> "$GITHUB_OUTPUT" + else + revision=$EVENT_SHA + fi + + [[ "$revision" =~ ^[0-9a-f]{40}$ ]] \ + || { echo "::error::PR does not currently have a test merge commit"; exit 1; } + echo "revision=$revision" >> "$GITHUB_OUTPUT" + + - name: Compose initial comment + if: github.event_name == 'issue_comment' + env: + MERGE_SHA: ${{ steps.target.outputs.revision }} + PR_NUMBER: ${{ steps.target.outputs.pr }} + run: | + { + echo "## ⏳ Merge tests running…" + echo + echo "Running the ignored test suite for PR #$PR_NUMBER at \`${MERGE_SHA:0:7}\`." + echo + echo "[In-progress logs](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }})" + } > comment-body.md + + - name: Post initial comment + if: github.event_name == 'issue_comment' + id: post + uses: peter-evans/create-or-update-comment@v5 + with: + token: ${{ github.token }} + issue-number: ${{ steps.target.outputs.pr }} + body-path: comment-body.md + merge-tests: name: ${{ matrix.name }} - if: ${{ github.event_name == 'merge_group' }} + needs: prepare + if: ${{ github.event_name == 'merge_group' || github.event_name == 'issue_comment' }} strategy: fail-fast: true matrix: include: - name: Lake ignored tests (compile pipeline) kind: lake - runner: warp-ubuntu-latest-x64-32x test_args: >- --ignored rust-canon-roundtrip serial-canon-roundtrip parallel-canon-roundtrip @@ -29,114 +100,132 @@ jobs: rust-decompile validate-aux aux-gen-diff decompile-diff - name: Lake ignored tests (compile) kind: lake - runner: warp-ubuntu-latest-x64-32x test_args: --ignored compile - name: Lake ignored tests (decompile) kind: lake - runner: warp-ubuntu-latest-x64-32x test_args: --ignored decompile - name: Lake ignored tests (misc) kind: lake - runner: warp-ubuntu-latest-x64-32x test_args: >- --ignored shard-map catalog-dedup commit-io fidelity-initstd kernel-ixon-roundtrip kernel-tutorial kernel-check-env kernel-check-const rust-kernel-build-primitives rust-kernel-build-prim-origs ixvm zk_voting: true - - name: Valgrind FFI - kind: valgrind - runner: warp-ubuntu-latest-x64-8x - - name: Ix.Tc verification and parity + - name: Ix.Tc unit and parity tests kind: tc - runner: warp-ubuntu-latest-x64-16x test_args: >- - --ignored tc-anon-diff tc-init tc-tutorial tc-roundtrip tc-ingress-meta tc-pins tc-accel-diff lean4lean - runs-on: ${{ matrix.runner }} + runs-on: + - nscloud-ubuntu-26.04-amd64-32x64-with-cache + - nscloud-cache-size-50gb + - nscloud-cache-tag-argumentcomputer-ix + - nscloud-cache-exp-do-not-commit steps: - name: Validate merge-test variant env: TEST_KIND: ${{ matrix.kind }} run: | case "$TEST_KIND" in - lake|valgrind|tc) ;; + lake|tc) ;; *) echo "::error::Unknown merge-test variant: $TEST_KIND"; exit 1 ;; esac - uses: actions/checkout@v7 - - uses: ./.github/actions/setup-rust-toolchain with: - # Valgrind cannot decode the AVX-512 the fleet baseline emits. - avx512-codegen: ${{ matrix.kind != 'valgrind' }} + ref: ${{ github.event_name == 'issue_comment' && format('refs/pull/{0}/merge', needs.prepare.outputs.pr) || needs.prepare.outputs.revision }} + persist-credentials: false - # A merge group has its own SHA, so restore the nearest compatible build - # produced by ordinary CI and let Lake rebuild anything that changed. - - if: ${{ matrix.kind == 'lake' }} - uses: actions/cache/restore@v6 - with: - path: ./.lake - key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} - restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}- - - # Valgrind cannot decode AVX-512, so its portable artifacts must not - # share `.lake` with native builds. - - if: ${{ matrix.kind == 'valgrind' }} - uses: actions/cache@v6 - with: - path: ./.lake - key: lake-valgrind-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} - restore-keys: lake-valgrind-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}- - - # A generic cache on the merge-queue ref can shadow a complete `lake-tc` - # cache from main, so this deliberately has no base-cache fallback. - - if: ${{ matrix.kind == 'tc' }} - uses: actions/cache@v6 - with: - path: ./.lake - key: lake-tc-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} - restore-keys: lake-tc-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}- + - name: Verify test revision + env: + TEST_REVISION: ${{ needs.prepare.outputs.revision }} + run: | + checked_out=$(git rev-parse HEAD) + if [ "$checked_out" != "$TEST_REVISION" ]; then + echo "::error::PR merge ref changed before the run started; comment !merge-tests again" + exit 1 + fi - # The Rust FFI bindgen build also needs the Lean toolchain and headers. - - if: ${{ matrix.kind != 'valgrind' }} - uses: leanprover/lean-action@v1 + - uses: ./.github/actions/setup-rust-toolchain with: - auto-config: false - use-github-cache: false - - if: ${{ matrix.kind == 'valgrind' }} - uses: leanprover/lean-action@v1 + use-github-cache: "false" + - uses: ./.github/actions/setup-lake-cache + - uses: leanprover/lean-action@v1 with: auto-config: false - build: true - build-args: "IxTests" use-github-cache: false - # The misc partition drives `.lake/build/bin/ix` in subprocesses. The - # prefix cache can contain an executable from an older SHA because the - # ordinary CI cache is saved before its all-targets lint builds `ix`. - # Rebuild it explicitly so the CLI and the checked-out tests agree. - - name: Build current ix CLI for subprocess tests - if: ${{ matrix.kind == 'lake' && matrix.zk_voting }} - run: lake build ix - - name: Run ignored Lake test partition if: ${{ matrix.kind == 'lake' }} run: lake test --wfail -- ${{ matrix.test_args }} + - name: Run ZK voting prover if: ${{ matrix.kind == 'lake' && matrix.zk_voting }} run: lake exe Apps.ZKVoting.Prover + - name: Run Ix.Tc unit, parity, and regression tests + if: ${{ matrix.kind == 'tc' }} + run: | + lake test --wfail -- tc-unit + lake test --wfail -- --ignored ${{ matrix.test_args }} + + valgrind: + name: Valgrind FFI + needs: prepare + # `prepare` is skipped on pull_request, so `!cancelled()` keeps this job + # eligible there; the other events still require `prepare` to succeed. + if: >- + !cancelled() && + (github.event_name == 'pull_request' || + (needs.prepare.result == 'success' && + (github.event_name == 'merge_group' || github.event_name == 'issue_comment'))) + # Valgrind cannot decode the shared baseline's AVX-512, so this job builds + # portable artifacts under its own cache key. Valgrind itself is + # single-threaded, so a GitHub-hosted runner suffices once that build is + # cached. + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v7 + with: + ref: ${{ github.event_name == 'pull_request' && github.sha || (github.event_name == 'issue_comment' && format('refs/pull/{0}/merge', needs.prepare.outputs.pr) || needs.prepare.outputs.revision) }} + persist-credentials: false + + - name: Verify test revision + if: github.event_name != 'pull_request' + env: + TEST_REVISION: ${{ needs.prepare.outputs.revision }} + run: | + checked_out=$(git rev-parse HEAD) + if [ "$checked_out" != "$TEST_REVISION" ]; then + echo "::error::PR merge ref changed before the run started; comment !merge-tests again" + exit 1 + fi + + - uses: ./.github/actions/setup-rust-toolchain + with: + avx512-codegen: "false" + # `./.lake`, not `.lake`: the path string is hashed into the cache + # entry's version, so the spelling must stay fixed for restores to hit. + - uses: actions/cache@v6 + with: + path: ./.lake + key: lake-valgrind-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} + restore-keys: lake-valgrind-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}- + - uses: leanprover/lean-action@v1 + with: + auto-config: false + use-github-cache: false + + - name: Run FFI tests normally + run: lake test --wfail -- ffi + - name: Install valgrind - if: ${{ matrix.kind == 'valgrind' }} run: | - # Some warpbuild images ship a mirrorlist with an unreachable - # azure.archive.ubuntu.com entry, causing apt-get update to stall indefinitely. - sudo sed -i '/azure\.archive\.ubuntu\.com/d' /etc/apt/apt-mirrors.txt 2>/dev/null || true sudo apt-get update sudo apt-get install -y valgrind + - name: Run tests under valgrind - if: ${{ matrix.kind == 'valgrind' }} run: | valgrind \ --leak-check=full \ @@ -147,30 +236,57 @@ jobs: --suppressions=.github/valgrind.supp \ .lake/build/bin/IxTests ffi - - name: Check Ix.Tc exported theorem trust manifest - if: ${{ matrix.kind == 'tc' }} - run: lake build Ix.Tc.Verify.Audit.Completed Ix.Tc.Verify.Audit.Conditional Ix.Tc.Verify.Audit.Statements - - name: Build Ix.Tc formal verification - if: ${{ matrix.kind == 'tc' }} - run: lake build IxTcVerify - - name: Check Ix.Tc verification sorry frontier - if: ${{ matrix.kind == 'tc' }} - run: lake build Ix.Tc.Verify.Audit.SorryFrontier - - name: Test Ix.Tc unit and adversarial fixtures - if: ${{ matrix.kind == 'tc' }} - run: lake test --wfail -- tc-unit - - name: Run Ix.Tc ignored tests - if: ${{ matrix.kind == 'tc' }} - run: lake test --wfail -- ${{ matrix.test_args }} - merge-tests-result: name: Merge tests - if: ${{ always() }} - needs: merge-tests + if: >- + always() && + github.event_name != 'pull_request' && + (github.event_name != 'issue_comment' || needs.prepare.result != 'skipped') + needs: [prepare, merge-tests, valgrind] runs-on: ubuntu-latest + permissions: + issues: write + pull-requests: write steps: + - name: Compose final comment + if: github.event_name == 'issue_comment' && needs.prepare.result == 'success' + env: + MERGE_SHA: ${{ needs.prepare.outputs.revision }} + PR_NUMBER: ${{ needs.prepare.outputs.pr }} + TEST_RESULT: ${{ needs.merge-tests.result }} + VALGRIND_RESULT: ${{ needs.valgrind.result }} + run: | + if [ "$TEST_RESULT" = success ] && [ "$VALGRIND_RESULT" = success ]; then + heading="## ✅ Merge tests passed" + summary="All ignored test partitions passed" + elif [ "$TEST_RESULT" = cancelled ] || [ "$VALGRIND_RESULT" = cancelled ]; then + heading="## ⚪ Merge tests cancelled" + summary="The ignored test run was cancelled" + else + heading="## ❌ Merge tests failed" + summary="At least one ignored test partition failed" + fi + { + echo "$heading" + echo + echo "$summary for PR #$PR_NUMBER at \`${MERGE_SHA:0:7}\`." + echo + echo "[Workflow logs](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }})" + } > comment-body.md + + - name: Update result comment + if: github.event_name == 'issue_comment' && needs.prepare.result == 'success' + uses: peter-evans/create-or-update-comment@v5 + with: + token: ${{ github.token }} + issue-number: ${{ needs.prepare.outputs.pr }} + comment-id: ${{ needs.prepare.outputs.comment-id }} + edit-mode: replace + body-path: comment-body.md + - name: Propagate merge-test failure if: >- - github.event_name == 'merge_group' && - needs.merge-tests.result != 'success' + needs.prepare.result != 'success' || + needs.merge-tests.result != 'success' || + needs.valgrind.result != 'success' run: exit 1 diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml index 51b38c363..ca842e32a 100644 --- a/.github/workflows/nix.yml +++ b/.github/workflows/nix.yml @@ -13,16 +13,23 @@ concurrency: cancel-in-progress: true jobs: - # Runs Lean tests via Nix nix-test: name: Nix Tests - runs-on: warp-ubuntu-latest-x64-16x + runs-on: + - nscloud-ubuntu-26.04-amd64-16x32-with-cache + - nscloud-cache-size-100gb + - nscloud-cache-tag-argumentcomputer-ix-nix steps: - uses: actions/checkout@v7 + - uses: ./.github/actions/setup-lake-cache + with: + cache-modes: | + nix + rust - uses: cachix/install-nix-action@v31 with: nix_path: nixpkgs=channel:nixos-unstable - github_access_token: ${{ secrets.GITHUB_TOKEN }} + github_access_token: ${{ github.token }} - uses: cachix/cachix-action@v17 with: name: argumentcomputer @@ -37,23 +44,7 @@ jobs: - run: nix run .#ix -- --help # A single invocation lets Nix schedule independent checks concurrently. - run: nix flake check --print-build-logs --accept-flake-config - - # Tests Nix devShell support on Ubuntu - nix-devshell: - name: Nix devShell Tests - runs-on: warp-ubuntu-latest-x64-8x - steps: - - uses: actions/checkout@v7 - - uses: cachix/install-nix-action@v31 - with: - nix_path: nixpkgs=channel:nixos-unstable - github_access_token: ${{ secrets.GITHUB_TOKEN }} - - uses: cachix/cachix-action@v17 - with: - name: argumentcomputer - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - - uses: ./.github/actions/authenticate-github-fetches - # Builds and runs tests using Lake as a Nix package + # Run the real build and test commands inside the development environment. - run: nix develop --accept-flake-config --command bash -c "lake build && lake test" # Realize the zkVM shells so they're verified and pushed to the cache, # and smoke-test each shell's toolchain entrypoint. diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml index f2d50dc64..78e572470 100644 --- a/.github/workflows/update.yml +++ b/.github/workflows/update.yml @@ -14,15 +14,7 @@ jobs: update: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v6 - - # Mint a token from the GitHub App so the opened PR triggers CI; pushes - # made with GITHUB_TOKEN do not. Same App as the org repo-sync workflows. - - uses: actions/create-github-app-token@v3 - id: app-token - with: - client-id: ${{ secrets.TOKEN_APP_ID }} - private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }} + - uses: actions/checkout@v7 # `dev` carries the fork's bump_mode/release_channel support; `main` only # mirrors upstream, which silently ignores these inputs. A PR is opened @@ -39,4 +31,4 @@ jobs: lake_package_directory: ". Benchmarks/**" bump_mode: pinned-tags pr: true - token: ${{ steps.app-token.outputs.token }} + token: ${{ github.token }} diff --git a/Ix/Cli/BenchCmd.lean b/Ix/Cli/BenchCmd.lean index 139154378..ac40b52b2 100644 --- a/Ix/Cli/BenchCmd.lean +++ b/Ix/Cli/BenchCmd.lean @@ -312,6 +312,7 @@ def backendSpecs : List BackendSpec := [ ("check-time", "0.10", "_"), ("throughput", "_", "0.10"), ("peak-rss", "0.10", "_")] }, { name := "zisk", defaultMode := "execute", inputs := .perConstant, + disabled := some "CI benchmarks disabled; covered by build/execute integration jobs", testbeds := [("execute", "zisk-check-execute-x64-32x")], metrics := [("execute", ["execute-time", "throughput", "peak-rss", "cycles", "constants", "shards"])], @@ -323,7 +324,7 @@ def backendSpecs : List BackendSpec := [ ("execute-time", "0.10", "_"), ("peak-rss", "0.10", "_"), ("throughput", "_", "0.10")] }, { name := "sp1", defaultMode := "execute", inputs := .perConstant, - disabled := some "execute run too slow for per-push CI; re-enable here once trimmed", + disabled := some "CI benchmarks disabled; covered by build/execute integration jobs", testbeds := [("execute", "sp1-check-execute-x64-32x")], metrics := [("execute", ["execute-time", "throughput", "peak-rss", "cycles"])], diff --git a/Ix/Cli/BenchReport.lean b/Ix/Cli/BenchReport.lean index f9a2aa3dd..e6c9ec7ed 100644 --- a/Ix/Cli/BenchReport.lean +++ b/Ix/Cli/BenchReport.lean @@ -652,12 +652,6 @@ def runCompareCmd (p : Cli.Parsed) : IO UInt32 := do && (← System.FilePath.pathExists ⟨prAttrib⟩) then table := table ++ "\n\n" ++ (← renderPerConstMovers mainAttrib prAttrib baseLabel) - if let some path := (p.flag? "warning-file").map (·.as! String) then - if ← System.FilePath.pathExists ⟨path⟩ then - let warning := (← IO.FS.readFile path).trimAscii.toString - if !warning.isEmpty then - let lines := (warning.splitOn "\n").map fun line => "> " ++ line - table := "> [!WARNING]\n" ++ "\n".intercalate lines ++ "\n\n" ++ table match p.flag? "out" with | some f => IO.FS.writeFile (f.as! String) (table ++ "\n") | none => IO.println table @@ -952,7 +946,7 @@ def parseError (msg : String) : IO UInt32 := do Grammar (an unknown command-line token, or an unknown env in BENCH_ENVS, rejects the command — exit 2 and a `parse-error` output): - !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] | all) + !benchmark ([aiur] [ooc] [compile] [decompile] | all) [execute] [fresh] [KEY=VALUE …] BENCH_ENVS=InitStd,Mathlib (case-insensitive, any registry env; defaults to every env for the @@ -1026,7 +1020,7 @@ def runParseCmd (p : Cli.Parsed) : IO UInt32 := do freshFlag := true continue let requested := if t == "all" - then Ix.Cli.BenchCmd.backendSpecs + then Ix.Cli.BenchCmd.backendSpecs.filter (·.disabled.isNone) else (Ix.Cli.BenchCmd.findBackend t).toList -- Everything after `!benchmark` on the command line must parse: a -- typo'd backend silently running the default would report numbers @@ -1034,7 +1028,8 @@ def runParseCmd (p : Cli.Parsed) : IO UInt32 := do if requested.isEmpty then return ← parseError s!"unknown token `{t}` in the benchmark command \ (expected a backend — \ - {", ".intercalate (Ix.Cli.BenchCmd.backendSpecs.map (·.name))} — \ + {", ".intercalate ((Ix.Cli.BenchCmd.backendSpecs.filter + (·.disabled.isNone)).map (·.name))} — \ or `all` / `execute` / `fresh`)" for b in requested do if b.disabled.isSome then @@ -1042,6 +1037,10 @@ def runParseCmd (p : Cli.Parsed) : IO UInt32 := do else if backends.all (·.name != b.name) then backends := backends.push b if backends.isEmpty then + if !skipped.isEmpty then + let reasons := ", ".intercalate <| skipped.toList.map fun b => + s!"{b.name} ({b.disabled.getD "disabled in CI"})" + return ← parseError s!"no requested benchmark backend is enabled in CI: {reasons}" backends := (Ix.Cli.BenchCmd.findBackend "aiur").toList.toArray -- KEY=VALUE config: the inline command-line tokens (strict — an @@ -1253,7 +1252,6 @@ def benchCompareCmd : Cli.Cmd := `[Cli| title : String; "Table title (default: derived from the run)" "base-source" : String; "Where the base side came from, for the title" "base-label" : String; "Name the base side in headers (default: main)" - "warning-file" : String; "Markdown warning file to prepend when present" out : String; "Write the table here instead of stdout" ] diff --git a/Ix/Tc/Verify/Audit/Basic.lean b/Ix/Tc/Verify/Audit/Basic.lean index 54f1c2f61..177558f74 100644 --- a/Ix/Tc/Verify/Audit/Basic.lean +++ b/Ix/Tc/Verify/Audit/Basic.lean @@ -78,33 +78,48 @@ private def directConstants : ConstantInfo → Array Name namespace DependencyAudit +structure Cache where + dependencies : NameMap (Array Name) := {} + structure State where + cache : Cache := {} visited : NameSet := {} - names : Array Name := #[] origins : Array Name := #[] + pendingDependency? : Option Name := none abbrev M := ReaderT Environment (StateM State) +/-- Cache direct references across manifest roots, which commonly share large +proof subgraphs. -/ +private def dependencies (declName : Name) : M (Array Name) := do + let state ← get + if let some dependencies := state.cache.dependencies.find? declName then + return dependencies + let env ← read + let dependencies := match env.checked.get.find? declName with + | none => #[] + | some info => directConstants info + modify fun s => + { s with cache := { dependencies := s.cache.dependencies.insert declName dependencies } } + return dependencies + /-- Traverse the checked kernel environment and record each reachable declaration whose type or value directly mentions `sorryAx`. -/ partial def visit (declName : Name) : M Unit := do let state ← get unless state.visited.contains declName do - modify fun s => - { s with - visited := s.visited.insert declName - names := s.names.push declName } - let env ← read - match env.checked.get.find? declName with - | none => pure () - | some info => - let dependencies := directConstants info - if declName != ``sorryAx && dependencies.contains ``sorryAx then - modify fun s => { s with origins := s.origins.push declName } - dependencies.forM visit - -def collect (env : Environment) (root : Name) : State := - let (_, state) := ((visit root).run env).run {} + modify fun s => { s with visited := s.visited.insert declName } + if state.pendingDependency?.isNone && + declName.toString.startsWith "Ix.Tc.Upstream.Pending." then + modify fun s => { s with pendingDependency? := some declName } + let dependencies ← dependencies declName + if declName != ``sorryAx && dependencies.contains ``sorryAx then + modify fun s => { s with origins := s.origins.push declName } + dependencies.forM visit + +def collect (env : Environment) (root : Name) (cache : Cache) : State := + let initial : State := { cache := cache } + let (_, state) := ((visit root).run env).run initial state end DependencyAudit @@ -144,7 +159,8 @@ private def expectedAxioms (allowance : RootAllowance) : Array Lean.Name := sortNames <| if allowance.sorryOrigins.isEmpty then expected else expected.push ``sorryAx -private def checkOne (allowance : RootAllowance) : CommandElabM Unit := do +private def checkOne (dependencyCache : DependencyAudit.Cache) + (allowance : RootAllowance) : CommandElabM DependencyAudit.Cache := do validateCategories allowance let env ← getEnv unless env.contains allowance.root do @@ -164,7 +180,7 @@ private def checkOne (allowance : RootAllowance) : CommandElabM Unit := do -- Origin and architectural-quarantine checks consume the same transitive -- dependency graph. Keep one exact traversal per root: large generated -- recursor proofs make two independent walks unnecessarily expensive. - let dependencyAudit := DependencyAudit.collect env allowance.root + let dependencyAudit := DependencyAudit.collect env allowance.root dependencyCache let actualOrigins := sortNames dependencyAudit.origins let expectedOrigins := sortNames allowance.sorryOrigins unless actualOrigins == expectedOrigins do @@ -177,23 +193,24 @@ private def checkOne (allowance : RootAllowance) : CommandElabM Unit := do -- helper definitions from the quarantine module: otherwise replacing a -- pending witness could silently change the completed proof surface. if allowance.pendingAxioms.isEmpty then - for dependency in dependencyAudit.names do - if dependency.toString.startsWith "Ix.Tc.Upstream.Pending." then - throwError m!"{allowance.root}: unconditional root reaches quarantined dependency {dependency}" + if let some dependency := dependencyAudit.pendingDependency? then + throwError m!"{allowance.root}: unconditional root reaches quarantined dependency {dependency}" for forbidden in allowance.forbiddenDependencies do - if dependencyAudit.names.contains forbidden then + if dependencyAudit.visited.contains forbidden then throwError m!"{allowance.root}: forbidden transitive dependency {forbidden}" + return dependencyAudit.cache /-- Check a complete executable trust manifest. Duplicate roots are rejected instead of being silently audited twice. -/ def check (allowances : Array RootAllowance) : CommandElabM Unit := do let mut roots : NameSet := {} + let mut dependencyCache : DependencyAudit.Cache := {} for allowance in allowances do if roots.contains allowance.root then throwError m!"duplicate axiom-audit root: {allowance.root}" roots := roots.insert allowance.root - checkOne allowance + dependencyCache ← checkOne dependencyCache allowance logInfo m!"Ix.Tc verification trust audit passed for {allowances.size} theorem roots" end Ix.Tc.Verify.Audit diff --git a/Tests/Ix/Tc/Roundtrip.lean b/Tests/Ix/Tc/Roundtrip.lean index 44a990b5b..f46d9d92c 100644 --- a/Tests/Ix/Tc/Roundtrip.lean +++ b/Tests/Ix/Tc/Roundtrip.lean @@ -205,22 +205,6 @@ def unitTests : List TestSeq := [fixtureTests, negativeTests] /-! ### Rust-compiled closures (`tc-roundtrip`, ignored) -/ -/-- Compile a seed closure through the Rust compiler and roundtrip every - constant of the resulting env. -/ -def roundtripOnSeeds (leanEnv : Lean.Environment) (label : String) - (seeds : List Lean.Name) : IO (Nat × Option String) := do - let consts := Tests.Tc.AnonDiff.closureOf leanEnv seeds - if consts.isEmpty then - return (0, some s!"empty closure for {seeds}") - let dir ← IO.FS.createTempDir - let path := dir / s!"tc-roundtrip-{label}.ixe" - let _ ← Ix.CompileM.rsCompileEnvBytesFFI consts path.toString true - let bytes ← IO.FS.readBinFile path - IO.FS.removeDirAll dir - match Ixon.deEnvAnon bytes with - | .error e => return (0, some s!"deEnvAnon failed: {e}") - | .ok ixonEnv => return roundtripAll ixonEnv - def seedSets : List (String × List Lean.Name) := Tests.Tc.AnonDiff.seedSets ++ [ ("inductives-recursors", @@ -250,35 +234,6 @@ def seedSets : List (String × List Lean.Name) := `Tests.Ix.Compile.LevelSpellings.wfTwo, `Tests.Ix.Compile.LevelSpellings.wfTwoEqDef]) ] -def closureSuite : TestSeq := Id.run do - let mut ts : TestSeq := .done - for (label, seeds) in seedSets do - ts := ts ++ .individualIO s!"roundtrip closure: {label}" none (do - let env ← Tests.Tc.Roundtrip.fixtureEnv - let (rows, err?) ← roundtripOnSeeds env label seeds - return (err?.isNone, rows, 0, err?)) .done - return ts - -/-- Whole-environment roundtrip: compile the ENTIRE current Lean env through - the Rust compiler and roundtrip every constant of the result — the - direct analog of the Rust `kernel-ixon-roundtrip`'s input scope. For - external `.ixe` files (e.g. `compilemathlib.ixe`), use - `ix roundtrip-tc ` instead. -/ -def wholeEnvSuite : TestSeq := - .individualIO "roundtrip whole get_env environment" none (do - let leanEnv ← Tests.Tc.Roundtrip.fixtureEnv - let consts := leanEnv.constants.toList - let dir ← IO.FS.createTempDir - let path := dir / "tc-roundtrip-whole-env.ixe" - let _ ← Ix.CompileM.rsCompileEnvBytesFFI consts path.toString true - let bytes ← IO.FS.readBinFile path - IO.FS.removeDirAll dir - match Ixon.deEnvAnon bytes with - | .error e => return (false, 0, 0, some s!"deEnvAnon failed: {e}") - | .ok ixonEnv => - let (rows, err?) := roundtripAll ixonEnv - return (err?.isNone, rows, 0, err?)) .done - /-! ### Meta roundtrip (kernel → Lean, `compare_envs` semantics) The full-fidelity half: pure-parse the Rust-compiled env, meta-ingress the @@ -292,55 +247,77 @@ names are informational `notFound`; aux-rewritten entries (`original.isSome`) are skipped with a count (their anon-structural fidelity is covered by the anon roundtrip above). -/ -/-- Compile `consts` through the Rust compiler and run the shared meta - roundtrip driver (`Ix.Tc.metaRoundtripEnv`) against `leanEnv`. -/ -def metaRoundtripOn (leanEnv : Lean.Environment) (label : String) +/-- Run both roundtrip modes over one Rust compilation. Anon and meta parsing + consume the same immutable bytes, so compiling each fixture twice cannot + add coverage. -/ +def roundtripOn (leanEnv : Lean.Environment) (label : String) (consts : List (Lean.Name × Lean.ConstantInfo)) : - IO (Ix.Tc.MetaRoundtripReport × Option String) := do + IO (Nat × Ix.Tc.MetaRoundtripReport × Option String) := do + if consts.isEmpty then + return (0, {}, some "empty constant closure") let dir ← IO.FS.createTempDir - let path := dir / s!"tc-meta-roundtrip-{label}.ixe" + let path := dir / s!"tc-roundtrip-{label}.ixe" let _ ← Ix.CompileM.rsCompileEnvBytesFFI consts path.toString true let bytes ← IO.FS.readBinFile path IO.FS.removeDirAll dir - let ixonEnv ← match Ixon.deEnv bytes with - | .ok env => pure env - | .error e => return ({}, some s!"pure deEnv failed: {e}") - match metaRoundtripEnv leanEnv ixonEnv with - | .error e => return ({}, some e) - | .ok report => - if report.errorCount == 0 then - return (report, none) - else - let shown := report.errors.toSubarray 0 (min 5 report.errors.size) - |>.toArray - let msgs := shown.map fun (n, m) => s!"{n}: {m}" - return (report, - some s!"{report.errorCount} comparison error(s); first: \ - {String.intercalate " | " msgs.toList}") - -def metaClosureSuite : TestSeq := Id.run do - let mut ts : TestSeq := .done - for (label, seeds) in seedSets do - ts := ts ++ .individualIO s!"meta roundtrip closure: {label}" none (do - let env ← Tests.Tc.Roundtrip.fixtureEnv - let consts := Tests.Tc.AnonDiff.closureOf env seeds - let (report, err?) ← metaRoundtripOn env label consts - return (err?.isNone, report.checked, 0, err?)) .done - return ts - -/-- The centerpiece: meta roundtrip of the WHOLE current Lean env. -/ -def metaWholeEnvSuite : TestSeq := - .individualIO "meta roundtrip whole get_env environment" none (do + let (anonRows, anonErr?) := + match Ixon.deEnvAnon bytes with + | .error e => (0, some s!"deEnvAnon failed: {e}") + | .ok ixonEnv => roundtripAll ixonEnv + let (metaReport, metaErr?) := + match Ixon.deEnv bytes with + | .error e => (({} : Ix.Tc.MetaRoundtripReport), some s!"pure deEnv failed: {e}") + | .ok ixonEnv => + match metaRoundtripEnv leanEnv ixonEnv with + | .error e => (({} : Ix.Tc.MetaRoundtripReport), some e) + | .ok report => + if report.errorCount == 0 then + (report, none) + else + let shown : Array (Ix.Name × String) := + report.errors.toSubarray 0 (min 5 report.errors.size) |>.toArray + let msgs := shown.map fun (error : Ix.Name × String) => + s!"{error.1}: {error.2}" + (report, some s!"{report.errorCount} comparison error(s); first: \ + {String.intercalate " | " msgs.toList}") + let err? := match anonErr?, metaErr? with + | none, none => none + | some e, none => some s!"anon: {e}" + | none, some e => some s!"meta: {e}" + | some anon, some metaErr => some s!"anon: {anon}; meta: {metaErr}" + return (anonRows, metaReport, err?) + +/-- Load the fixture environment once, then check every focused closure and + the whole environment. Loading the same olean graph separately for each + closure is pure setup duplication. External `.ixe` files use + `ix roundtrip-tc `. -/ +def integrationSuite : TestSeq := + .individualIO "anon/meta roundtrip closures and whole environment" none (do let leanEnv ← Tests.Tc.Roundtrip.fixtureEnv - let (report, err?) ← - metaRoundtripOn leanEnv "whole-env" leanEnv.constants.toList - IO.println s!"[tc-meta-roundtrip] checked {report.checked}, \ - notFound {report.notFound}, skippedAux {report.skippedAux}, \ - skippedSurgery {report.skippedSurgery}" - return (err?.isNone, report.checked, 0, err?)) .done + let mut checked := 0 + let mut errors : Array String := #[] + for (label, seeds) in seedSets do + let consts := Tests.Tc.AnonDiff.closureOf leanEnv seeds + let (anonRows, metaReport, err?) ← roundtripOn leanEnv label consts + checked := checked + anonRows + metaReport.checked + match err? with + | some e => errors := errors.push s!"{label}: {e}" + | none => + IO.println s!"[tc-roundtrip] {label}: anon {anonRows}, meta {metaReport.checked}" + let (anonRows, metaReport, err?) ← + roundtripOn leanEnv "whole-env" leanEnv.constants.toList + checked := checked + anonRows + metaReport.checked + if let some e := err? then + errors := errors.push s!"whole-env: {e}" + IO.println s!"[tc-meta-roundtrip] checked {metaReport.checked}, \ + notFound {metaReport.notFound}, skippedAux {metaReport.skippedAux}, \ + skippedSurgery {metaReport.skippedSurgery}" + let msg := if errors.isEmpty then none + else some (String.intercalate "\n" errors.toList) + return (errors.isEmpty, checked, 0, msg)) .done public def suite : List TestSeq := - [closureSuite, wholeEnvSuite, metaClosureSuite, metaWholeEnvSuite] + [integrationSuite] end diff --git a/docs/benchmarking.md b/docs/benchmarking.md index e5a566412..ca12a8f51 100644 --- a/docs/benchmarking.md +++ b/docs/benchmarking.md @@ -1,8 +1,8 @@ # Benchmarking One orchestrator — `ix bench` — runs every benchmark cell, locally and in CI. -A **cell** is `(backend, env, mode)`, e.g. `zisk-InitStd-execute`. CI is a -thin wrapper: the same `ix bench run` you type in a terminal is what both +A **cell** is `(backend, env, mode)`, e.g. `ooc-InitStd-execute`. For backends +scheduled in CI, the same `ix bench run` you type in a terminal is what both workflows execute, so every CI number is reproducible on your machine. - **`!benchmark` PR comment** (`.github/workflows/bench-pr.yml`) — on demand, @@ -101,8 +101,8 @@ a PR tree and compare them — exactly what the PR workflow does. | backend | what it measures | tool | |---|---|---| | `aiur` | the Aiur proof pipeline, per constant: the `ixvm` stage proves the IxVM typecheck, the `fri-verifier` stage executes and proves the in-circuit multi-stark verifier over that fresh proof (the KZG stages fold in as they land, each with its own measure prefix), closed by the pipeline ledger (total-time, pipeline-throughput, pipeline-peak-rss). Each stage's measures carry its prefix (`ixvm-prove-time`, `fri-verifier-fft-cost`, …). The whole system runs under the recursion-tuned FRI parameters. A second mode, execute, is the fast Phase-1-only signal (fft-cost, execute-time, throughput, peak-rss) — unscheduled, local/on-demand only (`!benchmark aiur execute`). The direct `--recursive --join` diagnostic takes exactly two constants as singleton `CheckEnv` shards and appends one pair row carrying `join-{execute-time,fft-cost,prove-time,peak-rss,proof-size,verify-time}`; it remains unscheduled until a runner can carry W0. | `bench-typecheck --recursive` | -| `zisk` | ZisK VM execute: cycles, execute-time, throughput, peak-rss, constants (pre-shard closure count, same universe as aiur's), shards (the runtime-planned partition size; 1 when the closure fits) | `zisk-host` | -| `sp1` | SP1 VM execute (currently disabled in the registry) | `sp1-host` | +| `zisk` | ZisK VM execute: cycles, execute-time, throughput, peak-rss, constants (pre-shard closure count, same universe as aiur's), shards (the runtime-planned partition size; 1 when the closure fits). Available locally; benchmark CI is disabled. | `zisk-host` | +| `sp1` | SP1 VM execute. Available locally; benchmark CI is disabled. | `sp1-host` | | `ooc` | out-of-circuit Rust kernel: whole-env row + one full-closure row per constant (`check-time` wraps only the check — the env loads once, outside every row's timed window) | `ix check-rs --json` | | `lean4lean` | the reference Lean4-in-Lean4 kernel ([digama0/lean4lean](https://github.com/digama0/lean4lean), required by the lakefile at a pinned rev) — the external yardstick for the Ix kernels on the same libraries. Olean-driven (no `.ixe`): the whole-library row replays every module in the env's import closure through lean4lean, module-parallel (check-time, constants, throughput, peak-rss; tune parallelism with `LEAN_NUM_THREADS`), plus one full-closure row per constant (the name's transitive closure into a fresh kernel env), mirroring ooc's row shape. Registry-disabled for CI (no bencher testbed yet); `ix bench run --backend lean4lean` works locally regardless | `bench-lean4lean` | | `compile` | `ix compile .lean → .ixe`: compile-time, file-size, constants, throughput | `ix compile --json` | @@ -174,14 +174,14 @@ approach the ceiling, and a kill there means missing rows and a red cell. There are **no per-constant timeouts**; the job-level `timeout-minutes` is the only clock. -Every zisk constant runs as a closure-shard partition sized at bench +Every local zisk benchmark constant runs as a closure-shard partition sized at runtime: `ix shard extract` → `ix profile` → `ix shard` cut a manifest whose shard count comes from the planner's RAM budget (a closure that fits gets a one-shard plan), and one `--shard-plan` host run executes the shards sequentially, emitting the constant's row with per-shard -breakdowns. bench-main's compile job pre-cuts these artifacts -(`ix bench shard`) and ships them via cache; a zisk run cuts lazily when -they're absent, and falls back to the whole closure if the cut fails. +breakdowns. `ix bench shard` can pre-cut these artifacts; a zisk run cuts +lazily when they're absent and falls back to the whole closure if the cut +fails. ## Registry and constant set @@ -208,7 +208,7 @@ they're absent, and falls back to the whole closure if the cut fails. ## `!benchmark` grammar ``` -!benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [decompile] | all) +!benchmark ([aiur] [ooc] [compile] [decompile] | all) [execute] [fresh] [KEY=VALUE …] BENCH_ENVS=InitStd,Mathlib # default InitStd (case-insensitive); a # compile-only request may name any registry @@ -258,9 +258,8 @@ untouched. **bench-main.yml**: `build` (compile `ix` + `bench-typecheck` once, cache by SHA) → `plan` (`ix bench ci matrix` → job matrices) + `compile` (per env: -`ix bench run --backend compile`, cache the `.ixe` and pre-cut zisk shards -separately) → -one `benchmark` job per remaining cell — aiur / zisk / ooc / decompile — +`ix bench run --backend compile`, cache the `.ixe`) → +one `benchmark` job per remaining cell — aiur / ooc / decompile — (each: restore caches, one `ix bench run … --ixe`, `ix bench bmf`, upload via `.github/actions/bencher-track`). A kernel rejection exits 3 and reddens the @@ -279,29 +278,33 @@ matching plots are kept, stale ones replaced, hand-pinned ones untouched. The sync also asserts every measure's canonical units (bencher auto-creates measures with placeholder units on first upload). -**bench-pr.yml**: `setup` (authorize the comment, resolve base/head SHAs) → -`build` (select or build the PR binaries, publish a run-scoped artifact, -then `ix bench ci parse`) → `compile` (one measured `ix compile` per env, -publishing a run-scoped `.ixe` + row artifact) → `benchmark` matrix (per cell: -download only those run artifacts; run the PR side; fetch main's numbers, -with a base-checkout run covering what bencher lacked (including every -non-`main` base, whose `.ixe` can be restored from its earlier PR run); -`ix bench compare` → table artifact) → `assemble` (`ix bench report` builds -the comment body, unprivileged) → `comment` (posts it — the only job with a -write token, running no PR code). Normal runs may seed the run artifacts from -persistent head/base-SHA caches. `fresh` bypasses those caches and rebuilds -the measured products while retaining dependency caches. +**bench-pr.yml**: `dispatch` (authorize the comment, resolve base/head SHAs, +then start the cache-writing run) → `build` (select or build the PR binaries, +publish a run-scoped artifact, then `ix bench ci parse`). `announce` posts the +initial running/error comment while `compile` runs one measured `ix compile` +per env and publishes a run-scoped `.ixe` + row artifact. The `benchmark` +matrix downloads only those run artifacts, runs the PR side, and fetches +main's numbers, with a base-checkout run covering what bencher lacked +(including every non-`main` +base, whose `.ixe` can be restored from its earlier PR run); `ix bench compare` +then publishes a table artifact. `assemble` runs `ix bench report` without +write privileges, and `comment` replaces the initial comment. Only `announce` +and `comment` hold write tokens, and neither checks out or runs PR code. Normal +runs may seed the run artifacts from persistent head/base-SHA caches. `fresh` +bypasses those caches and rebuilds the measured products while retaining +dependency caches. Benchmark runners use the fixed AVX-512 baseline and +WarpCache for both workflow products and Cargo build artifacts. Every job that creates a timing row logs its CPU model, instruction set, -effective CPU count, affinity, and cgroup allocation. Because the benchmark -binaries use native codegen, their build jobs also record the build CPU and -carry that report inside the binary cache or run artifact; measurement jobs -print it next to their own host report. A cache entry created before this -provenance was introduced remains usable and is reported as having an unknown -build CPU. The exact `lscpu` model name is compared; a difference (or missing -build provenance) is rendered as a warning in that cell's PR comment table. -This is diagnostic only: the CPU model does not participate in cache keys, and -only an explicit `fresh` request bypasses the measured-product caches. +effective CPU count, affinity, and cgroup allocation directly in the Actions +logs. Each table in the `!benchmark` comment ends with one hardware line per +side (CPU model, effective vCPUs, total RAM), because the two sides need not +share a host: the PR compile row is measured in the compile job, and a +bencher-sourced base side was measured by bench-main at the base SHA, which +caches that host next to its upload for the PR run to restore. A base run +performed in the benchmark job is labelled with that job's runner. This is +diagnostic only: CPU information does not participate in cache keys or +benchmark results, and a missing note renders as "not recorded". ## Palomar compatibility corpus @@ -350,10 +353,10 @@ the same artifacts. ## Not yet covered -- **zkVM prove** — the hosts prove, but CI has no GPU runner; cells are - execute-only. -- **sp1** — disabled in the registry (execute too slow per push); - re-enable it there and it returns to the matrices and the parser. +- **Zisk and SP1 benchmark cells** — intentionally disabled in benchmark CI; + regular CI retains their build and keyless-execution integration jobs. +- **zkVM prove** — the hosts prove, but local proving requires suitable GPU + infrastructure. - **aiur prove numbers for the biggest closures** — every constant in the shared set runs the full pipeline, but the largest ones exceed the CI host's RAM ceiling and land as honest `oom` rows, which never upload