certified kernel and certified compilation

.config/nextest.toml

@@ -8,5 +8,7 @@ status-level = "skip"
 fail-fast = false
 # Mark tests as slow after 5mins, kill them after 20mins
 slow-timeout = { period = "300s", terminate-after = 4 }
-# Retry failed tests once, marked flaky if test then passes
-retries = 1
+# No retries: a test that fails once fails the run. A retry would let a
+# nondeterministic failure (parallel compilation, sharing, the kernel's
+# caches) pass as "flaky".
+retries = 0

.gitattributes

@@ -0,0 +1,35 @@
+# 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
+
+# AuxGen's frozen reference outputs; the decoder beside them is hand-written
+Tests/Ix/AuxGen/Reference/*.lean linguist-generated=true
+Tests/Ix/AuxGen/Reference/JsonTable.lean -linguist-generated
+
+# The default role table, its evidence and the Ixon prelude (`kernel-pin-gen`)
+IxC/Kernel/Ixon/RoleData.lean linguist-generated=true
+
+# The compiler's non-canonical record (the `twins` suite's re-record mode)
+Tests/Ix/Compile/NonCanonicalDefault.lean linguist-generated=true

.github/workflows/bench-main.yml

@@ -193,7 +193,7 @@ jobs:
           auto-config: false
           use-github-cache: false
           use-mathlib-cache: ${{ matrix.mathlib && 'true' || 'false' }}
-      - run: lake build Compile${{ matrix.env }}
+      - run: lake build Compile${{ matrix.env }} IxC.Kernel.PinGen.Certs
         working-directory: ${{ env.COMPILE_DIR }}
       # The measured compile: serializes the env to `<env>.ixe` at the
       # workspace root and writes one results row keyed by the env name.

.github/workflows/bench-pr.yml

@@ -20,10 +20,9 @@
 #                                  #  predates the flag proves whole
 #   RUST_LOG=info                  # passthrough env (allowlisted)
 #   IX_COMPILE_EAGER=1             # compile-knob passthrough (also IX_COMPILE_DEMOTE /
-#                                  # IX_COMPILE_WORKERS): RAM/speed knobs for the
-#                                  # measured `ix compile`. Every setting emits a
-#                                  # bit-identical `.ixe`, so they move the compile
-#                                  # backend's own numbers and nothing downstream.
+#                                  # IX_COMPILE_WORKERS): Rust compiler knobs for
+#                                  # older base checkouts; the certified default
+#                                  # does not use them.
 #                                  # The `.ixe` and compile-row caches are keyed by
 #                                  # SHA alone, so a knob run on a commit already
 #                                  # benchmarked replays the cached row instead of
@@ -362,7 +361,7 @@ jobs:
       # `lake build` below clones this package's Lake dependencies.
       - uses: $/.github/actions/authenticate-github-fetches
       # Apply the allowlisted KEY=VALUE lines from the !benchmark comment,
-      # so IX_COMPILE_* knobs reach the measured compile. Delivered via an
+      # including Rust compiler knobs for older base checkouts. Delivered via an
       # env var, not inline `${{ }}` — inlining would risk shell injection.
       - name: Apply passthrough env
         env:
@@ -439,7 +438,7 @@ jobs:
         working-directory: Benchmarks/Compile
         env:
           COMPILE_ENV: ${{ matrix.env }}
-        run: lake build "Compile$COMPILE_ENV"
+        run: lake build "Compile$COMPILE_ENV" IxC.Kernel.PinGen.Certs
       - name: Compile ${{ matrix.env }}.ixe
         if: steps.compile-source.outputs.rebuild == 'true'
         env:

.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`, `ix-decompile`, `aiur`, `ooc-check`) or
+#     `ix-compile-certified`, `ix-decompile`, `aiur`, `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
@@ -44,7 +44,7 @@ on:
         # 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, ix-decompile, aiur, aiur-sharded-env-check, ooc-check, all]
+        options: [ix-compile-certified, ix-decompile, aiur, aiur-sharded-env-check, ooc-check, all]
       sha:
         description: "Commit to anchor to (default: HEAD)"
         required: false
@@ -78,7 +78,7 @@ jobs:
           # (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 ix-decompile ooc-check"
+          valid="aiur 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 ix-decompile ooc-check"
+          valid="aiur 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" \

.github/workflows/ci.yml

@@ -71,7 +71,7 @@ jobs:
           diff lean-toolchain Models/SetTheory/lean-toolchain
       - name: Test Ix CLI
         if: github.event_name != 'push'
-        run: lake test --wfail -- cli
+        run: lake test --wfail -- --tier ci:cli
       - name: Test Ixon v4 contracts and consumers
         if: github.event_name != 'push'
         run: |
@@ -122,7 +122,7 @@ jobs:
       - name: Get Rust version
         if: github.event_name != 'push'
         run: |
-          echo "RUST_VERSION=$(awk -F '"' '/^channel/ {print $2}' rust-toolchain.toml)" | tee -a $GITHUB_ENV
+          echo "RUST_VERSION=$(awk -F '"' '/^channel/ {print $2}' rust-toolchain.toml)" | tee -a "$GITHUB_ENV"
       # A Docker action: the job's RUSTC_WRAPPER reaches its container, where
       # sccache is not installed, and cargo fails before deny runs. Deny only
       # reads metadata, and cargo treats an empty wrapper as none.

.github/workflows/merge-tests-stub.yml

@@ -3,6 +3,7 @@ name: Merge tests
 # Ignored suites run against merge-group commits. Pull requests publish the
 # same gate name so they can enter the queue before those suites run. This
 # workflow never runs on merge_group, where merge-tests.yml owns the real gate.
+# The check it publishes runs nothing; see docs/ci.md, "Required checks".
 on:
   pull_request:
 

.github/workflows/merge-tests.yml

@@ -126,31 +126,29 @@ jobs:
         include:
           - name: Lake ignored tests (compile pipeline)
             kind: lake
-            test_args: >-
-              --ignored
-              rust-canon-roundtrip serial-canon-roundtrip parallel-canon-roundtrip
-              graph-cross condense-cross rust-serialize ixon-corpus
-              rust-decompile validate-aux aux-gen-diff decompile-diff
-              aux-gen-closure canon-closure-aux
+            test_args: --tier ci:compile-pipeline
+          - name: Lake ignored tests (compiler closures)
+            kind: lake
+            test_args: --tier ci:compiler-closures
           - name: Lake ignored tests (compile)
             kind: lake
-            test_args: --ignored compile
+            test_args: --tier ci:compile
           - name: Lake ignored tests (decompile)
             kind: lake
-            test_args: --ignored decompile
+            test_args: --tier ci:decompile
           - name: Lake ignored tests (misc)
             kind: lake
-            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
+            test_args: --tier ci:misc
             zk_voting: true
-          - name: Ix.Tc unit and parity tests
-            kind: tc
-            test_args: >-
-              tc-anon-diff tc-init tc-tutorial tc-roundtrip tc-ingress-meta
-              tc-pins tc-accel-diff
+          - name: Lake ignored tests (landing, compilers)
+            kind: lake
+            test_args: --tier ci:landing-compilers
+          - name: Lake ignored tests (landing, Init+Std)
+            kind: lake
+            test_args: --tier ci:landing-initstd
+          - name: Lake ignored tests (landing, Init+Std through ix)
+            kind: lake
+            test_args: --tier ci:landing-initstd-cli
           - name: Certified kernel
             kind: kernel
     # On-demand rather than Spot: a reclaimed partition restarts from scratch
@@ -169,7 +167,7 @@ jobs:
           TEST_KIND: ${{ matrix.kind }}
         run: |
           case "$TEST_KIND" in
-            lake|tc|kernel) ;;
+            lake|kernel) ;;
             *) echo "::error::Unknown merge-test variant: $TEST_KIND"; exit 1 ;;
           esac
 
@@ -215,16 +213,11 @@ jobs:
         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 }}
-
       # The certified kernel gate (docs/kernel.md): the standalone IxC
       # package build, which has no dependencies and so proves the kernel needs
       # only the toolchain, then the host tests, the Rust differentials, the
-      # set-theory model, the fences, the entry cases and the reader fidelity.
+      # set-theory model, the fences, the entry cases, the reader fidelity, the
+      # `.meta` and `.source` names, and quotient Source on Init and Std.
       # The kernel artifacts come from .lake/kernel on the sticky disk. The
       # model lives in its own workspace so Mathlib stays out of the root
       # package; its objects come from Mathlib's cache and persist on the
@@ -236,7 +229,7 @@ jobs:
             Mathlib.SetTheory.Cardinal.Regular \
             Mathlib.SetTheory.ZFC.VonNeumann \
             Mathlib.SetTheory.ZFC.Cardinal
-      - name: Check certified kernel, codec and order differentials, model, entry cases and reader fidelity
+      - name: Check certified kernel, codec and order differentials, model, entry cases, reader fidelity and quotient Source
         if: ${{ matrix.kind == 'kernel' }}
         run: lake run check-kernel --with-model
 

Apps/ZKVoting/Prover.lean

@@ -1,5 +1,6 @@
 import Ix.Claim
 import Ix.Commit
+import Ix.ClaimContext
 import Ix.Address
 import Ix.Meta
 import Ix.CompileM
@@ -52,6 +53,7 @@ def main : IO UInt32 := do
   let arg : Lean.Expr ← runMeta (metaMakeList voteType as) env
   let (lvls, input, output, type, _sort) ←
     runMeta (metaMakeEvalClaim ``runElection [arg]) env
-  let claim ← IO.ofExcept <| Ix.Commit.evalClaim compileEnv lvls input output type
+  let ctx ← IO.ofExcept Ix.ClaimContext.ofDefaultTable
+  let claim ← IO.ofExcept <| Ix.Commit.evalClaim ctx compileEnv lvls input output type
   IO.println s!"{claim}"
   return 0

BENCHMARKS.md

@@ -1,3 +1,14 @@
+> Historical pipeline results (the refresh below is dated 2026-08-07).
+> The measurements and methodology describe that pipeline: its `Ix.Tc`
+> checker, regenerating Lean decompiler, canonical block order and
+> auxiliary regeneration, all since removed. Recorded agreement concerns
+> the measured inputs.
+>
+> Current `ix check-lean` uses IxC and rejects nonzero `--clear-every`,
+> including the recorded `--clear-every 50`. The compiler now compiles
+> Lean verbatim. See the [current benchmark commands](docs/benchmarking.md#local-usage)
+> and [checker contract and commands](docs/kernel.md#environment-check).
+
 # Ix pipeline benchmarks: pure-Lean vs Rust
 
 Head-to-head timings for every stage of the Ix pipeline across three