Add self-contained kernel verification and relative consistency for environment checking

.github/workflows/ci.yml

@@ -31,7 +31,9 @@ jobs:
         with:
           build-args: "--wfail -v"
           test: false
-      # build-all lint driver compiles every lib/exe target with --wfail, so a
+      # build-all checks production targets and the consistency foundation
+      # with --wfail. The legacy named-specification proofs are not part of
+      # this gate; named-spec-verification.yml builds them on demand. A
       # warning in any target (exes, benchmarks, Apps) — not just the default lib
       # lean-action builds above — fails CI.
       - name: Build all targets
@@ -86,6 +88,30 @@ jobs:
           use-github-cache: false
       - name: Test Ix CLI
         run: lake test --wfail -- cli
+      - name: Check certified source and claim adapters
+        run: lake run check-certified
+
+  theory:
+    needs: build
+    runs-on: warp-ubuntu-latest-x64-16x
+    steps:
+      - uses: actions/checkout@v7
+      - uses: ./.github/actions/setup-rust-toolchain
+      - 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') }}-
+      - uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+          use-github-cache: false
+      - name: Check compiler implementation proofs
+        run: lake build --wfail IxCompileVerify
+      - name: Check direct kernel consistency refinement
+        run: lake build --wfail IxKernelConsistency
+      - name: Check consistency model and exact foundation manifest
+        run: lake run check-theory
 
   rust-test:
     runs-on: warp-ubuntu-latest-x64-8x

.github/workflows/merge-tests.yml

@@ -47,13 +47,13 @@ jobs:
           - name: Valgrind FFI
             kind: valgrind
             runner: warp-ubuntu-latest-x64-8x
-          - name: Ix.Tc verification and parity
+          - name: Ix.Kernel verification and parity
             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
+              tc-pins tc-accel-diff
     runs-on: ${{ matrix.runner }}
     steps:
       - name: Validate merge-test variant
@@ -147,19 +147,19 @@ jobs:
             --suppressions=.github/valgrind.supp \
             .lake/build/bin/IxTests ffi
 
-      - name: Check Ix.Tc exported theorem trust manifest
+      # The legacy named-specification proofs (`IxKernelVerify` with its exact
+      # trust manifests and sorry frontier) are not required here; the
+      # named-spec-verification workflow builds them on demand.
+      - name: Build Ix compiler verification
         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
+        run: lake build --wfail IxCompileVerify
+      - name: Check Ix.Kernel consistency refinement
         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
+        run: lake build --wfail IxKernelConsistency
+      - name: Test Ix.Kernel unit and adversarial fixtures
         if: ${{ matrix.kind == 'tc' }}
         run: lake test --wfail -- tc-unit
-      - name: Run Ix.Tc ignored tests
+      - name: Run Ix.Kernel ignored tests
         if: ${{ matrix.kind == 'tc' }}
         run: lake test --wfail -- ${{ matrix.test_args }}
 

.github/workflows/named-spec-verification.yml

@@ -0,0 +1,49 @@
+name: Named specification verification
+
+# Legacy, non-required track: the Lean4Lean-derived named specification
+# (`Ix.Theory.Named`) and the `Ix.Kernel.Verify` implementation proofs
+# stated against it, with their exact trust manifests and sorry frontier.
+# The kernel proof gate required on every PR is `lake build --wfail
+# IxKernelConsistency` in ci.yml, whose audit rejects any `Ix.Theory.Named`
+# module in its import closure. This track is being retired in favour of the
+# set model, so it runs on demand and on a weekly schedule only; its audit
+# numbers are frozen at the counts recorded in the manifests it builds.
+
+on:
+  workflow_dispatch:
+  schedule:
+    # Weekly, Monday 06:00 UTC.
+    - cron: '0 6 * * 1'
+
+permissions:
+  contents: read
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  named-spec:
+    runs-on: warp-ubuntu-latest-x64-16x
+    steps:
+      - uses: actions/checkout@v7
+      - uses: ./.github/actions/setup-rust-toolchain
+      # Same `.lake` cache as ci.yml (`./.lake`, per-sha key with prefix
+      # fallback): the newest CI build of the toolchain/manifest pair is
+      # restored and Lake rebuilds whatever differs. Restore-only: this
+      # workflow never publishes a cache entry that ci.yml could restore.
+      - 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') }}-
+      - uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+          use-github-cache: false
+      - name: Build named-specification implementation proofs
+        run: lake build IxKernelVerify
+      - name: Check Ix.Kernel exported theorem trust manifest
+        run: lake build Ix.Kernel.Verify.Audit.Completed Ix.Kernel.Verify.Audit.Conditional Ix.Kernel.Verify.Audit.Statements
+      - name: Check Ix.Kernel verification sorry frontier
+        run: lake build Ix.Kernel.Verify.Audit.SorryFrontier

.github/workflows/set-theory-model.yml

@@ -0,0 +1,47 @@
+name: Set-theory model
+
+on:
+  pull_request:
+    paths:
+      - 'Models/SetTheory/**'
+      - 'Ix/Theory/Model/SetTheory/Core.lean'
+      - 'lakefile.lean'
+      - 'lake-manifest.json'
+      - 'lean-toolchain'
+      - '.github/workflows/set-theory-model.yml'
+  merge_group:
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
+  cancel-in-progress: true
+
+jobs:
+  model:
+    runs-on: warp-ubuntu-latest-x64-16x
+    timeout-minutes: 60
+    defaults:
+      run:
+        working-directory: Models/SetTheory
+    env:
+      MATHLIB_NO_CACHE_ON_UPDATE: '1'
+      MATHLIB_CACHE_DIR: .lake/mathlib-cache
+    steps:
+      - uses: actions/checkout@v7
+      - uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+          use-github-cache: false
+      - name: Check Lean toolchains match
+        run: cmp ../../lean-toolchain lean-toolchain
+      - uses: actions/cache@v6
+        with:
+          path: Models/SetTheory/.lake
+          key: set-theory-model-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('Models/SetTheory/lean-toolchain', 'Models/SetTheory/lakefile.toml', 'Models/SetTheory/lake-manifest.json') }}
+      - name: Fetch the imported Mathlib modules and dependencies
+        run: lake exe cache get Mathlib.SetTheory.Cardinal.Regular Mathlib.SetTheory.ZFC.VonNeumann Mathlib.SetTheory.ZFC.Cardinal
+      - name: Build model and check axiom guard
+        run: lake build --wfail

BENCHMARKS.md

@@ -2,7 +2,7 @@
 
 Head-to-head timings for every stage of the Ix pipeline across three
 environments, comparing the pure-Lean implementation (`Ix.CompileM` /
-`Ix.DecompileM` / `Ix.Tc`) against the Rust implementation
+`Ix.DecompileM` / `Ix.Kernel`) against the Rust implementation
 (`crates/compile` / `crates/kernel`).
 
 ## Methodology
@@ -119,7 +119,7 @@ Rust: `ix decompile` (the decompile pass over a `.ixe`). Lean:
 flags → Pass 2 aux regeneration/recovery) *plus* the hash comparison
 against the canonicalized source (comparison overhead ~5 s at 205k
 constants). Lean decompilation is dominated by Pass 2's kernel bridge
-(regeneration re-infers through `Ix.Tc`); Pass 2 runs on the
+(regeneration re-infers through `Ix.Kernel`); Pass 2 runs on the
 wave-parallel driver (`decompileEnvPass2Parallel`, 16 workers — the
 count is memory-bound, not core-bound; `IX_DECOMPILE_WORKERS`
 overrides). The sequential figures from before the parallel driver are
@@ -147,7 +147,7 @@ full verdict parity.
 worker config keeps warm caches; both a 32-worker meta run and a
 32-worker anon run without cache clearing were OOM-killed while
 swap-thrashing). The anon row uses the scale configuration from the
-`Ix.Tc` Mathlib-tier validation: 16 workers, `--clear-every 50`
+`Ix.Kernel` Mathlib-tier validation: 16 workers, `--clear-every 50`
 (whole-worker-state renewal every 50 items; RSS plateaus ~42 GB) —
 **640,658/640,658 passed, zero failures, full verdict parity**. Anon
 mode dedups alpha-identical constants, hence the smaller count.