Certify Formal Aiur & Retire Legacy Aiur/IxVM

.gitattributes

@@ -1,28 +1,5 @@
 # Generated files: GitHub collapses them in diffs and leaves them out of the
-# language statistics. Each is regenerated by the tool named above it; CI checks
-# the codegen and the trace bundle against their generators (`--check`).
-
-# Aiur codegen of the IxVM, ix_aggr and multi-stark programs (`ix codegen`)
-crates/ixvm-codegen/src/aiur_ixvm.rs linguist-generated=true
-crates/ixvm-codegen/src/aiur_ix_aggr.rs linguist-generated=true
-crates/ixvm-codegen/src/aiur_multi_stark.rs linguist-generated=true
-
-# Trace writers, CUDA units and their manifest (`ix codegen --trace-bundle`)
-crates/aiur/src/trace_codegen/programs/ixvm.rs linguist-generated=true
-crates/aiur/src/trace_codegen/programs/ixvm_cuda.rs linguist-generated=true
-crates/aiur/src/trace_codegen/programs/ix_aggr.rs linguist-generated=true
-crates/aiur/src/trace_codegen/programs/ix_aggr_cuda.rs linguist-generated=true
-crates/aiur/src/trace_codegen/programs/multi_stark.rs linguist-generated=true
-crates/aiur/src/trace_codegen/programs/multi_stark_cuda.rs linguist-generated=true
-crates/aiur/cuda/generated/production/** linguist-generated=true
-
-# Trace-codegen test fixtures (`lake exe trace-fixtures`)
-crates/aiur/src/trace_codegen/tests/generated.rs linguist-generated=true
-crates/aiur/src/trace_codegen/tests/generated_cuda.rs linguist-generated=true
-crates/aiur/src/trace_codegen/tests/blake3.rs linguist-generated=true
-crates/aiur/src/trace_codegen/tests/blake3_cuda.rs linguist-generated=true
-crates/aiur/cuda/generated/blake3.cu linguist-generated=true
-crates/aiur/cuda/generated/fixtures.cu linguist-generated=true
+# language statistics. Each is regenerated by the tool named above it.
 
 # AuxGen's frozen reference outputs; the decoder beside them is hand-written
 Tests/Ix/AuxGen/Reference/*.lean linguist-generated=true

.github/workflows/bench-main.yml

@@ -5,7 +5,7 @@ name: Benchmark main
 # parameter combination — the same command you can run locally, and the
 # same one the !benchmark PR workflow uses. Four job roles:
 #
-#   1. build     — compiles and caches `ix` and `bench-typecheck` once.
+#   1. build     — compiles and caches `ix` 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
@@ -14,7 +14,7 @@ name: Benchmark main
 #   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).
+#                  run the entry's backend over it (aiur-sharded-env, 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
@@ -41,8 +41,8 @@ env:
   COMPILE_DIR: Benchmarks/Compile
 
 jobs:
-  # Build the `ix` and `bench-typecheck` binaries once and cache them;
-  # every later job restores them instead of rebuilding. They are built
+  # Build the `ix` binary once and cache it;
+  # every later job restores it instead of rebuilding. It is built
   # with native code generation for r8i, with caches and measured results
   # isolated from other hardware and compiler flags.
   build:
@@ -80,9 +80,6 @@ jobs:
       - 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/
-          chmod +x ~/.local/bin/bench-typecheck
       - uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
         with:
           path: ~/.local/bin
@@ -154,7 +151,7 @@ jobs:
         include:
           - { env: InitStd }
           - { env: Lean }
-          # Init+Std+Lean+Batteries: the aiur-sharded-env (whole-env Aiur
+          # Init+Std+Lean+Batteries: the aiur-sharded-env (whole-env formal Aiur
           # execution) benchmark's fast tier. Batteries builds from the
           # shared Compile package; no mathlib cache needed.
           - { env: ISLB }
@@ -267,17 +264,16 @@ jobs:
   # the compile job's cached `.ixe` — nothing recompiles here.
   #
   # What each backend measures:
-  #   - aiur: the proof pipeline — per constant, every stage plus the
-  #     total: prove the IxVM typecheck (stage 1), then execute and
-  #     prove the in-circuit multi-stark verifier over that fresh proof
-  #     (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.
+  #   - aiur-sharded-env: whole-env formal Aiur execution over a sharded
+  #     manifest — every leaf executed and its proof planned against the
+  #     runner's RAM budget, over-budget leaves split. One row per env.
   #   - 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
   #     checked elsewhere (`ix validate` / roundtrip tests) — this only
   #     measures speed and memory.
+  # The per-constant proof pipeline (`aiur`) is disabled in the registry:
+  # its tool, `bench-typecheck`, was retired with the legacy backend.
   benchmark:
     name: ${{ matrix.params.label }}
     needs: [compile, plan]

.github/workflows/bench-pr.yml

@@ -3,7 +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] [ooc] [compile] [decompile] | all) [execute]
+#   !benchmark ([aiur-sharded-env] [ooc] [compile] [decompile] | all)
 #   BENCH_ENVS=InitStd,Mathlib     # which compiled envs (case-insensitive, any registry env;
 #                                  #  defaults to every env for compile/decompile, InitStd
 #                                  #  for the rest)
@@ -14,7 +14,7 @@
 #                                  #  — so BENCH_ENVS is never required; a single-env
 #                                  #  BENCH_ENVS still forces placement
 #   BENCH_PHASES=1                 # add per-constant phase drill-downs to the comment
-#   BENCH_TRACE_SHARDS=<GiB>       # aiur prove: plan each constant's proof as trace shards
+#   BENCH_TRACE_SHARDS=<GiB>       # aiur prove (disabled): plan each constant's proof as trace shards
 #                                  #  within this per-constant RAM budget (0: detect) and
 #                                  #  report `ixvm-trace-shards`; a base checkout that
 #                                  #  predates the flag proves whole
@@ -32,16 +32,11 @@
 #                                  # (default: 131072)
 #
 # Each backend runs its registry default mode:
-#   - aiur: `prove` — the full proof pipeline per constant (stage 1
-#     proves the IxVM typecheck, stage 2 executes and proves the
-#     in-circuit multi-stark verifier over that fresh proof), reported
-#     as one comparison table per stage — witness execute, prove, peak
-#     RAM, proof size, verify — closing with the pipeline ledger (total
-#     time and the run's RAM ceiling). BENCH_CONSTS overrides the shared
-#     selection. The bare `execute`
-#     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).
+#   - aiur: disabled. Its per-constant proof pipeline ran on the retired
+#     legacy backend's `bench-typecheck`; a bare `!benchmark`, which
+#     requests it, is rejected until a formal Aiur pipeline replaces it.
+#   - aiur-sharded-env: `execute` — whole-env formal Aiur execution and
+#     proof planning over a sharded manifest (`ix check --ram-budget`).
 #   - ooc: `execute`.
 #   - compile: `ix compile <env>.lean` → `<env>.ixe`.
 #   - decompile: `ix decompile` over the compile run's fresh `.ixe`.
@@ -92,7 +87,7 @@ on:
         description: Full head SHA to benchmark
         required: true
       comment-body:
-        description: "The !benchmark command; single-line KEY=VALUE config, e.g. `!benchmark aiur BENCH_ENVS=InitStd,Mathlib`"
+        description: "The !benchmark command; single-line KEY=VALUE config, e.g. `!benchmark ooc BENCH_ENVS=InitStd,Mathlib`"
         required: true
 
 run-name: "${{ github.event_name == 'workflow_dispatch' && format('Benchmark PR #{0} (r8i.8xlarge)', inputs.pr) || 'Relay benchmark comment' }}"
@@ -152,8 +147,8 @@ jobs:
             -f head-sha="$HEAD_SHA" \
             -f comment-body="$COMMENT_BODY"
 
-  # Select or build the PR's `ix` and `bench-typecheck` once, then
-  # publish them as a run-scoped
+  # Select or build the PR's `ix` once, then
+  # publish it as a run-scoped
   # 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.
@@ -249,9 +244,9 @@ jobs:
       - 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/
-          chmod +x ~/.local/bin/ix ~/.local/bin/bench-typecheck
+          lake build ix
+          cp .lake/build/bin/ix ~/.local/bin/
+          chmod +x ~/.local/bin/ix
       - if: steps.parse.outputs.fresh != '1' && steps.bins.outputs.cache-hit != 'true'
         uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
         with:
@@ -260,7 +255,7 @@ jobs:
       - name: Package run binaries
         run: >-
           tar -C "$HOME/.local/bin" -cf benchmark-binaries.tar
-          ix bench-typecheck
+          ix
       - name: Upload run binaries
         uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
         with:
@@ -751,8 +746,8 @@ jobs:
              && cmp -s lean-toolchain base/lean-toolchain; then
             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
-              [ -x base/.lake/build/bin/ix ] && [ -x base/.lake/build/bin/bench-typecheck ] \
+              mv ~/.local/bin/ix base/.lake/build/bin/ 2>/dev/null || true
+              [ -x base/.lake/build/bin/ix ] \
                 && cached=true
             fi
           fi
@@ -777,14 +772,14 @@ jobs:
         uses: $/.github/actions/log-cpu
         with:
           label: Base benchmark binary build CPU
-      - name: Build base (ix, bench-typecheck)
+      - name: Build base (ix)
         if: steps.decide.outputs.run-base == 'true' && steps.base-src.outputs.cached != 'true'
         uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0
         with:
           lake-package-directory: base
           auto-config: false
           build: true
-          build-args: "ix bench-typecheck"
+          build-args: "ix"
           use-github-cache: false
       # For a mathlib-importing env (Mathlib, FLT), the base-side compile
       # resolves imports from the base tree's Benchmarks/Compile

.github/workflows/bencher-thresholds-reset.yml

@@ -22,7 +22,7 @@ name: Bencher thresholds reset
 #     cancel by removing it before merge. Naming convention: one label per token,
 #     `bencher-thresholds-reset:<token>` where <token> is a workload (a backend
 #     testbed stem in Ix/Cli/BenchCmd.lean (backendSpecs):
-#     `ix-compile-certified`, `ix-decompile`, `aiur`, `ooc-check`) or
+#     `ix-compile-certified`, `ix-decompile`, `aiur-sharded-env-check`, `ooc-check`) or
 #     `all` (the merge step expands an `all` label into every workload). Labeling
 #     requires Triage+, so PR authors from forks cannot self-queue a reset. The
 #     label shares the command/workflow name; the ref it moves is
@@ -43,8 +43,8 @@ on:
         type: choice
         # GitHub requires literal choice options, so this list stays static:
         # keep it (and the jobs' valid= lists below) in sync with the
-        # backend testbeds in Ix/Cli/BenchCmd.lean (backendSpecs).
-        options: [ix-compile-certified, ix-decompile, aiur, aiur-sharded-env-check, ooc-check, all]
+        # enabled backend testbeds in Ix/Cli/BenchCmd.lean (backendSpecs).
+        options: [ix-compile-certified, ix-decompile, aiur-sharded-env-check, ooc-check, all]
       sha:
         description: "Commit to anchor to (default: HEAD)"
         required: false
@@ -74,11 +74,11 @@ jobs:
       MERGE_SHA: ${{ github.event.pull_request.merge_commit_sha }}
     steps:
       - run: |
-          # Workload registry: the backend testbeds in Ix/Cli/BenchCmd.lean
-          # (backendSpecs), before its hardware suffix. Static because this
-          # job runs on a cheap runner with no built `ix`; keep in sync when
-          # adding a backend.
-          valid="aiur aiur-sharded-env-check ix-compile-certified ix-decompile ooc-check"
+          # Workload registry: the enabled backend testbeds in
+          # Ix/Cli/BenchCmd.lean (backendSpecs), before their hardware suffix.
+          # Static because this job runs on a cheap runner with no built `ix`;
+          # keep in sync when adding or disabling a backend.
+          valid="aiur-sharded-env-check ix-compile-certified ix-decompile ooc-check"
           if [ "$EVENT" = workflow_dispatch ]; then
             # Reset the chosen workload(s) at the given commit; no PR scan.
             sha="${INPUT_SHA:-$HEAD_SHA}"
@@ -137,7 +137,7 @@ jobs:
           # which the merge job expands into every workload). Same static
           # list as the reset job; keep both in sync with backendSpecs in
           # Ix/Cli/BenchCmd.lean.
-          valid="aiur aiur-sharded-env-check ix-compile-certified ix-decompile ooc-check"
+          valid="aiur-sharded-env-check ix-compile-certified ix-decompile ooc-check"
           accepted="$valid all"
           # Parse the workload token(s) after the command, lowercased.
           workloads=$(printf '%s' "$BODY" \