A certified consistent Ix.Kernel based on Con-Leche

.gitattributes

@@ -0,0 +1,19 @@
+# Collapse in GitHub's diff the files a reviewer does not read line by line.
+
+# The certified checker's kernel, derived from con-leche (docs/kernel.md),
+# except Ix's own boundary and modules beside it.
+Ix/Kernel/**/*.lean linguist-generated=true
+Ix/Kernel/Admission.lean -linguist-generated
+Ix/Kernel/Admission/** -linguist-generated
+Ix/Kernel/Ixon/** -linguist-generated
+Ix/Kernel/Audit/** -linguist-generated
+Ix/Kernel/Ingress/** -linguist-generated
+Ix/Kernel/Egress/** -linguist-generated
+Ix/Kernel/Ref.lean -linguist-generated
+Ix/Kernel/Search.lean -linguist-generated
+Ix/Kernel/LevelGeran.lean -linguist-generated
+Ix/Kernel/Verify/LevelGeran.lean -linguist-generated
+
+# The pin tables, written by `kernel-pin-gen`.
+Ix/Kernel/Ixon/PinData.lean linguist-generated=true
+Ix/Kernel/Ixon/NatOpPinData.lean linguist-generated=true

.github/workflows/ci.yml

@@ -55,14 +55,15 @@ jobs:
           test-args: "--wfail"
           lint-args: "-- --wfail -v"
           use-github-cache: false
-      - name: Build Ix.Tc formal verification
-        run: lake build IxTcVerify
       - name: Check codegen'd IxVM kernel is up to date
         if: github.event_name != 'push'
         run: lake exe ix codegen --check
-      - name: Check Lean versions match for Ix and compiler bench
+      - name: Check Lean versions match for Ix, compiler bench, certified kernel and its model
         if: github.event_name != 'push'
-        run: diff lean-toolchain Benchmarks/Compile/lean-toolchain
+        run: |
+          diff lean-toolchain Benchmarks/Compile/lean-toolchain
+          diff lean-toolchain IxKernel/lean-toolchain
+          diff lean-toolchain Models/SetTheory/lean-toolchain
       - name: Test Ix CLI
         if: github.event_name != 'push'
         run: lake test --wfail -- cli
@@ -72,6 +73,47 @@ jobs:
           lake exe ixon-v4-primitives
           lake exe ixon-v4-tests --primitives
 
+  # A fresh package build keeps host dependencies out of the certified import
+  # closure. Mathlib is confined to its separate model package; its cache only
+  # supplies pinned dependency objects, not this checkout's kernel or fixtures.
+  # No sticky disk and no Cargo cache: the job builds from an empty tree.
+  certified-kernel:
+    name: Certified Lean kernel
+    runs-on: runs-on=${{ github.run_id }}-certified-kernel-${{ github.run_attempt }}/cpu=16/family=r7i+r8i+r7a+r8a/image=ubuntu26-full-x64/volume=100gb/extras=s3-cache
+    steps:
+      - uses: runs-on/action@dfae4d98c5537a0dc7bbb7e6b9211f30ba240f6d # v2.4.0
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
+      - uses: $/.github/actions/setup-rust-toolchain
+        with:
+          codegen: portable
+          use-github-cache: "false"
+      - uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0
+        with:
+          auto-config: false
+          use-github-cache: false
+      - name: Fetch pinned set-theory dependencies
+        run: |
+          MATHLIB_NO_CACHE_ON_UPDATE=1 lake -d Models/SetTheory update
+          lake -d Models/SetTheory exe cache get \
+            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
+        run: lake run check-kernel --with-model
+      - name: Retain codec, block-order, entry-case and reader-fidelity results
+        if: ${{ always() }}
+        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
+        with:
+          name: certified-kernel-differential
+          path: |
+            .lake/build/kernel-codec.log
+            .lake/build/kernel-order.jsonl
+            .lake/build/kernel-entry-cases.jsonl
+            .lake/build/kernel-reader-fidelity.log
+          if-no-files-found: warn
+
   rust-test:
     runs-on: runs-on=${{ github.run_id }}-rust-test-${{ github.run_attempt }}/cpu=8/family=r7i+r8i+r7a+r8a/image=ubuntu26-full-x64/volume=100gb/sticky=ci-rust-test-x86-64-v4:50gb/extras=s3-cache
     steps:
@@ -190,7 +232,7 @@ jobs:
 
   ci-gate:
     if: ${{ always() }}
-    needs: [lean-test, rust-test, cuda-compile, lints]
+    needs: [lean-test, certified-kernel, rust-test, cuda-compile, lints]
     permissions:
       actions: read
       checks: read

.github/workflows/merge-tests.yml

@@ -131,6 +131,7 @@ jobs:
               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
           - name: Lake ignored tests (compile)
             kind: lake
             test_args: --ignored compile
@@ -149,7 +150,7 @@ jobs:
             kind: tc
             test_args: >-
               tc-anon-diff tc-init tc-tutorial tc-roundtrip tc-ingress-meta
-              tc-pins tc-accel-diff lean4lean
+              tc-pins tc-accel-diff
     # On-demand rather than Spot: a reclaimed partition restarts from scratch
     # only after the whole attempt finishes, and the longest partitions
     # already run close to the merge queue's status-check timeout, so one

.github/workflows/update.yml

@@ -33,8 +33,12 @@ jobs:
           # The root package plus every package under Benchmarks/ — `/**`
           # walks the whole tree (catching Catalog's nested fixture
           # workspaces) and skips dotted directories, so `.lake`
-          # dependency checkouts are never swept up.
-          lake_package_directory: ". Benchmarks/**"
+          # dependency checkouts are never swept up — and the certified
+          # kernel's package and its model, whose Mathlib `rev` is a Lean
+          # version tag and moves with the toolchain. The pin tables and
+          # frozen audit counts are not regenerated here: see "On a
+          # toolchain bump" in docs/kernel.md.
+          lake_package_directory: ". Benchmarks/** IxKernel Models/SetTheory"
           bump_mode: pinned-tags
           pr: true
           update_lean4_nix: true

Benchmarks/Compile/TruthMines/lake-manifest.json

@@ -375,16 +375,6 @@
    "inputRev": "453f4feb6508ec787fc325a70523d38e4378ef8f",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/digama0/lean4lean",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "e0e3f6bcccb840cb0ea6f11c2b274ada93a12e00",
-   "name": "lean4lean",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "e0e3f6bcccb840cb0ea6f11c2b274ada93a12e00",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,

Benchmarks/Compile/lake-manifest.json

@@ -168,16 +168,6 @@
    "inputRev": null,
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/argumentcomputer/lean4ix",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "a5621ecfe6416360d4e310c0ed40f3e79ae0710e",
-   "name": "lean4lean",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "a5621ecfe6416360d4e310c0ed40f3e79ae0710e",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,

Benchmarks/Compile/lakefile.toml

@@ -69,7 +69,7 @@ name = "TauCeti"
 git = "https://github.com/TauCetiProject/TauCeti"
 rev = "afb1aacb3632d3236eee756ea1683290c07270a3"
 
-# Keep the workspace's Lean 4.33 dependency closure authoritative over
+# Keep the workspace's Lean 4.34 dependency closure authoritative over
 # older or moving transitive Mathlib pins.
 [[require]]
 name = "mathlib"