WIP: Jcb/ixvm consistency

.github/workflows/ci.yml

@@ -31,7 +31,8 @@ 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. Named implementation proofs have a separate trust gate. 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 +87,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 implementation proofs and exact trust manifests
+        run: lake build IxKernelVerify 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,22 @@ jobs:
             --suppressions=.github/valgrind.supp \
             .lake/build/bin/IxTests ffi
 
-      - name: Check Ix.Tc exported theorem trust manifest
+      - name: Check Ix.Kernel 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
+        run: lake build Ix.Kernel.Verify.Audit.Completed Ix.Kernel.Verify.Audit.Conditional Ix.Kernel.Verify.Audit.Statements
+      - name: Build Ix.Kernel formal verification
         if: ${{ matrix.kind == 'tc' }}
-        run: lake build IxTcVerify
-      - name: Check Ix.Tc verification sorry frontier
+        run: lake build IxKernelVerify IxCompileVerify
+      - name: Check Ix.Kernel consistency refinement
         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: Check Ix.Kernel verification sorry frontier
+        if: ${{ matrix.kind == 'tc' }}
+        run: lake build Ix.Kernel.Verify.Audit.SorryFrontier
+      - 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/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.