WIP: Monorepo MegaPR: Integrate certified checking, compilation and Aiur soundness foundations

.github/workflows/ci.yml

@@ -31,7 +31,7 @@ jobs:
         with:
           build-args: "--wfail -v"
           test: false
-      # build-all lint driver compiles every lib/exe target with --wfail, so a
+      # build-all lint driver compiles production lib/exe targets with --wfail, so 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 +86,33 @@ jobs:
           use-github-cache: false
       - name: Test Ix CLI
         run: lake test --wfail -- cli
+      - name: Check Aiur proof boundaries and native verifier binding
+        run: lake run check-aiur
+      - name: Check certified source and claim adapters
+        run: lake run check-certified
+
+  compiler:
+    runs-on: warp-ubuntu-latest-x64-16x
+    steps:
+      - uses: actions/checkout@v7
+      - uses: ./.github/actions/setup-rust-toolchain
+      - uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+          use-github-cache: false
+      - name: Check compiler proofs, trust boundary, and native fixtures
+        run: lake run check-compiler
+
+  theory:
+    runs-on: warp-ubuntu-latest-x64-16x
+    steps:
+      - uses: actions/checkout@v7
+      - uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+          use-github-cache: false
+      - 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

AGENTS.md

@@ -0,0 +1,6 @@
+# Repository guidelines
+
+- Keep local plans and work notes in the gitignored `plans/` directory.
+- Reserve `docs/` for polished, permanent, user-facing documentation.
+- Use Lean or Ix instead of Python, Perl, or shell scripts wherever possible.
+- Use Ixon instead of JSON wherever possible.

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.

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": "a4188d7c2979378d85c6bb41fdd96c3a48a71371",
-   "name": "lean4lean",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "a4188d7c2979378d85c6bb41fdd96c3a48a71371",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,

Benchmarks/Compiler.lean

@@ -0,0 +1,52 @@
+import Benchmarks.Compiler.Reproduce
+import Benchmarks.Compiler.CounterFold
+
+open Ix.Compiler.Tools.Check
+
+def main (args : List String) : IO UInt32 := cli "benchmark failed" do
+  match args with
+  | "counter-fold-build" :: output :: options =>
+    let options ← checked (parseArgs ["--gcc", "--time"] options)
+    Benchmarks.Compiler.CounterFold.buildSuite output (option options "--gcc" "gcc") (option options "--time" "time")
+  | ["counter-fold-verify", build, output] => Benchmarks.Compiler.CounterFold.verifySuite build output
+  | ["counter-fold-smoke", build, output, core] =>
+    Benchmarks.Compiler.CounterFold.smokeSuite build output (← present core.toNat? "core must be a natural number")
+  | ["counter-fold-smoke", build, output] => Benchmarks.Compiler.CounterFold.smokeSuite build output (← Benchmarks.Compiler.firstCore)
+  | ["counter-fold-pilot", build, correctness, output, core] =>
+    Benchmarks.Compiler.CounterFold.pilotSuite build correctness output (← present core.toNat? "core must be a natural number")
+  | ["counter-fold-measure", build, correctness, pilot, output, core] =>
+    Benchmarks.Compiler.CounterFold.measureSuite build correctness pilot output (← present core.toNat? "core must be a natural number")
+  | ["counter-fold-analyze", build, measured, output] => Benchmarks.Compiler.CounterFold.analyzeSuite build measured output
+  | ["counter-fold-reproduce", build, measured, output] => Benchmarks.Compiler.CounterFold.reproduceSuite build measured output
+  | ["datasets", output] =>
+    Benchmarks.Compiler.writeDatasets output
+    IO.println "benchmark datasets: 585 inputs, 19305 arena capacity cases, 38 timing rows"
+  | "build" :: output :: options =>
+    let options ← checked (parseArgs ["--gcc", "--clang", "--compcert", "--cakeml", "--time"] options)
+    Benchmarks.Compiler.buildSuite output {
+      gcc := option options "--gcc" "gcc", clang := option options "--clang" "clang",
+      compcert := option options "--compcert" "ccomp", cakeml := option options "--cakeml" "cake",
+      timerTool := option options "--time" "time" }
+  | ["check-matrix", implementation, path] =>
+    let rows ← Benchmarks.Compiler.readLines path
+    let result ← Benchmarks.Compiler.inspectMatrix implementation rows
+    Benchmarks.Compiler.checkerRegressions implementation rows
+    IO.println result.compress
+  | ["verify", build, output] => Benchmarks.Compiler.verifySuite build output
+  | ["smoke", build, output, core] =>
+    Benchmarks.Compiler.smokeSuite build output (← present core.toNat? "core must be a natural number")
+  | ["smoke", build, output] => Benchmarks.Compiler.smokeSuite build output (← Benchmarks.Compiler.firstCore)
+  | ["gc-smoke", build, output, core] =>
+    Benchmarks.Compiler.gcSmokeSuite build output (← present core.toNat? "core must be a natural number")
+  | ["gc-smoke", build, output] => Benchmarks.Compiler.gcSmokeSuite build output (← Benchmarks.Compiler.firstCore)
+  | ["pilot", build, correctness, output, core] =>
+    Benchmarks.Compiler.pilotSuite build correctness output (← present core.toNat? "core must be a natural number")
+  | ["measure", build, correctness, pilot, output, core] =>
+    Benchmarks.Compiler.measureSuite build correctness pilot output (← present core.toNat? "core must be a natural number")
+  | ["analyze", build, measured, output] => Benchmarks.Compiler.analyzeSuite build measured output
+  | ["analysis-self-check"] => Benchmarks.Compiler.analysisSelfCheck
+  | ["diagnose", build, pilot, output, core] =>
+    Benchmarks.Compiler.diagnoseSuite build pilot output (← present core.toNat? "core must be a natural number")
+  | ["reproduce", build, measured, output] => Benchmarks.Compiler.reproduceSuite build measured output
+  | ["rebuild-check", build, output] => let _ ← Benchmarks.Compiler.rebuildArtifacts build output; pure ()
+  | _ => throw (IO.userError "usage: benchmark datasets OUT | build OUT [--gcc PATH --clang PATH --compcert PATH --cakeml PATH --time PATH] | verify BUILD OUT | smoke BUILD OUT [CORE] | gc-smoke BUILD OUT [CORE] | pilot BUILD VERIFY OUT CORE | measure BUILD VERIFY PILOT OUT CORE | diagnose BUILD PILOT OUT CORE | analyze BUILD MEASURED OUT | reproduce BUILD MEASURED OUT | analysis-self-check")