WIP: improve certified kernel and certify compilation

.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/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: |

.github/workflows/merge-tests.yml

@@ -126,31 +126,26 @@ 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: Certified kernel
             kind: kernel
     # On-demand rather than Spot: a reclaimed partition restarts from scratch
@@ -169,7 +164,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,12 +210,6 @@ 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

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

Benchmarks/Canon/IxeDiff.lean

@@ -0,0 +1,213 @@
+/-
+  ixe-diff: which Lean names changed address between two compiled
+  environments, grouped by the block they belong to, with a one-word
+  cause where it can be inferred.
+
+  ```
+  ixe-diff <old.ixe> <new.ixe> [--names] [--tsv <rows.tsv>]
+  ```
+
+  The join and the per-field classification are
+  `Ixon.rsDiffEnvFiles` (both files memory-mapped, anonymous structure
+  only; the ripple verdict marks a row whose change is explained by
+  re-addressed dependencies). Each changed name is then placed in a group
+  and given a cause:
+
+  * the group is the Muts block its old address projects into, else the
+    block its new address projects into, else the name alone;
+  * `cascade`: the constant itself is unchanged; only addresses it refers
+    to moved (Rust's ripple verdict, which includes a block whose sibling
+    moved);
+  * `packaging`: the name moved between a projection and a standalone
+    constant, or between blocks of different sizes;
+  * `nested-order`: a projection into a block of the same size at another
+    index (a permutation of the block);
+  * `content`: anything else (the constant's own terms changed).
+
+  Printed: totals per cause, one line per group (first member, size,
+  counts per cause), added and removed names, and with `--names` every
+  changed name. `--tsv` writes `name, group, cause, old kind, new kind`.
+
+  Untrusted measurement tooling; it never writes an environment.
+-/
+import Ix.Ixon
+
+namespace Benchmarks.Canon.IxeDiff
+
+open Ixon
+
+/-- The shape of a constant: standalone (with its kind) or a projection
+    into a block of `size` members at `idx`. -/
+inductive Shape where
+  | standalone (kind : String)
+  | proj (kind : String) (block : Address) (idx : UInt64) (size : Nat)
+  | missing
+  deriving Inhabited, BEq
+
+def Shape.kind : Shape → String
+  | .standalone k => k
+  | .proj k .. => k
+  | .missing => "missing"
+
+def Shape.block? : Shape → Option Address
+  | .proj _ b .. => some b
+  | _ => none
+
+/-- Constant windows of one file. -/
+structure Slices where
+  buf : ByteArray
+  idx : Std.HashMap Address (Nat × Nat)
+
+def Slices.load (path : String) : IO Slices := do
+  let buf ← IO.FS.readBinFile path
+  let raw ← IO.ofExcept (Ixon.rsDeEnvLazyFFI buf)
+  let idx := raw.consts.foldl (init := {}) fun m s =>
+    m.insert s.addr (s.offset.toNat, s.len.toNat)
+  return { buf, idx }
+
+def Slices.get? (s : Slices) (a : Address) : Option Constant :=
+  match s.idx.get? a with
+  | some (off, len) => (LazyConstant.ofSlice s.buf off len).get?
+  | none => none
+
+/-- The shape of the constant at `a`; block sizes are cached. -/
+def shapeOf (s : Slices) (cache : IO.Ref (Std.HashMap Address Nat)) (a : Address) :
+    IO Shape := do
+  let some c := s.get? a | return .missing
+  let blockSize (b : Address) : IO Nat := do
+    if let some n := (← cache.get).get? b then return n
+    let n := match s.get? b with
+      | some { info := .muts ms, .. } => ms.size
+      | _ => 0
+    cache.modify (·.insert b n)
+    return n
+  match c.info with
+  | .defn _ => return .standalone "defn"
+  | .recr _ => return .standalone "recr"
+  | .axio _ => return .standalone "axio"
+  | .quot _ => return .standalone "quot"
+  | .muts _ => return .standalone "muts"
+  | .dPrj p => return .proj "dprj" p.block p.idx (← blockSize p.block)
+  | .rPrj p => return .proj "rprj" p.block p.idx (← blockSize p.block)
+  | .iPrj p => return .proj "iprj" p.block p.idx (← blockSize p.block)
+  | .cPrj p => return .proj "cprj" p.block p.idx (← blockSize p.block)
+
+/-- Packaging: a projection on one side and a standalone constant on the
+    other, or projections into blocks of different sizes. -/
+def isPackaging : Shape → Shape → Bool
+  | .proj .., .standalone _ => true
+  | .standalone _, .proj .. => true
+  | .proj _ _ _ n, .proj _ _ _ m => n != m
+  | _, _ => false
+
+def isReorder : Shape → Shape → Bool
+  | .proj _ _ i n, .proj _ _ j m => n == m && i != j
+  | _, _ => false
+
+structure Row where
+  name : String
+  group : String
+  cause : String
+  oldKind : String
+  newKind : String
+  deriving Inhabited
+
+def groupKey (name : String) (a b : Shape) : String :=
+  match a.block?, b.block? with
+  | some x, _ => s!"old:{x}"
+  | none, some y => s!"new:{y}"
+  | none, none => s!"name:{name}"
+
+def causes : List String := ["packaging", "nested-order", "cascade", "content"]
+
+/-- Print the grouped report of `rows`. -/
+def report (rows : Array Row) (names : Bool) : IO Unit := do
+  let mut perCause : Std.HashMap String Nat := {}
+  let mut groups : Std.HashMap String (Array Row) := {}
+  for r in rows do
+    perCause := perCause.insert r.cause (perCause.getD r.cause 0 + 1)
+    groups := groups.insert r.group ((groups.getD r.group #[]).push r)
+  IO.println <| s!"changed names: {rows.size}; " ++ ", ".intercalate
+    (causes.map fun c => s!"{c} {perCause.getD c 0}")
+  -- groups, labelled by their least member name, sorted by label
+  let labelled := groups.toArray.map fun (_, rs) =>
+    let sorted := rs.qsort (·.name < ·.name)
+    (sorted[0]!.name, sorted)
+  let labelled := labelled.qsort (·.1 < ·.1)
+  let mut groupsPerCause : Std.HashMap String Nat := {}
+  for (_, rs) in labelled do
+    let main := causes.find? (fun c => rs.any (·.cause == c)) |>.getD "content"
+    groupsPerCause := groupsPerCause.insert main (groupsPerCause.getD main 0 + 1)
+  IO.println <| s!"groups: {labelled.size}; by leading cause: " ++ ", ".intercalate
+    (causes.map fun c => s!"{c} {groupsPerCause.getD c 0}")
+  for (label, rs) in labelled do
+    let counts := causes.filterMap fun c =>
+      let n := rs.foldl (fun k r => if r.cause == c then k + 1 else k) 0
+      if n == 0 then none else some s!"{c} {n}"
+    IO.println s!"  {label} ({rs.size}): {", ".intercalate counts}"
+    if names then
+      for r in rs do
+        let kind := if r.oldKind == r.newKind then r.oldKind else s!"{r.oldKind}→{r.newKind}"
+        IO.println s!"      {r.name}  {kind}  {r.cause}"
+
+def writeTsv (path : String) (rows : Array Row) : IO Unit := do
+  let lines := rows.map fun r => s!"{r.name}\t{r.group}\t{r.cause}\t{r.oldKind}\t{r.newKind}"
+  IO.FS.writeFile path ("name\tgroup\tcause\told_kind\tnew_kind\n" ++ "\n".intercalate lines.toList ++ "\n")
+
+def diffMode (oldPath newPath : String) (names : Bool) (tsv? : Option String) : IO UInt32 := do
+  let t0 ← IO.monoMsNow
+  if ← Ixon.rsIxeFilesEqual oldPath newPath then
+    IO.println "identical"
+    return 0
+  let d ← Ixon.rsDiffEnvFiles oldPath newPath false
+  IO.eprintln s!"[ixe-diff] diff: {d.namedChanged.size} changed, {d.namedAdded.size} added, \
+    {d.namedRemoved.size} removed ({(← IO.monoMsNow) - t0} ms)"
+  let sa ← Slices.load oldPath
+  let sb ← Slices.load newPath
+  let ca ← IO.mkRef ({} : Std.HashMap Address Nat)
+  let cb ← IO.mkRef ({} : Std.HashMap Address Nat)
+  let mut rows : Array Row := #[]
+  for c in d.namedChanged do
+    -- synthetic Muts names (`Ix.<block hash>.…`) never join as changed rows
+    let a ← shapeOf sa ca c.oldAddr
+    let b ← shapeOf sb cb c.newAddr
+    let cause :=
+      if c.rippled then "cascade"
+      else if isPackaging a b then "packaging"
+      else if isReorder a b then "nested-order"
+      else "content"
+    rows := rows.push { name := c.name, group := groupKey c.name a b, cause,
+                        oldKind := a.kind, newKind := b.kind }
+  IO.println s!"# ixe-diff {oldPath} → {newPath}"
+  report rows names
+  let isSyn (s : String) : Bool := s.startsWith "Ix." && ((s.drop 3).takeWhile (· != '.')).positions.length == 64
+  let added := d.namedAdded.filter (!isSyn ·.1)
+  let removed := d.namedRemoved.filter (!isSyn ·.1)
+  IO.println s!"added names: {added.size}; removed names: {removed.size} \
+    (synthetic block names: {d.namedAdded.size - added.size} added, \
+    {d.namedRemoved.size - removed.size} removed)"
+  if names then
+    for (n, _) in added do IO.println s!"  + {n}"
+    for (n, _) in removed do IO.println s!"  - {n}"
+  if let some p := tsv? then writeTsv p rows
+  IO.eprintln s!"[ixe-diff] done ({(← IO.monoMsNow) - t0} ms)"
+  return if rows.isEmpty && added.isEmpty && removed.isEmpty then 0 else 1
+
+def usage : String :=
+  "usage: ixe-diff <old.ixe> <new.ixe> [--names] [--tsv <rows.tsv>]"
+
+def main (args : List String) : IO UInt32 := do
+  let rec flags (acc : Bool × Option String) : List String → Option (Bool × Option String)
+    | [] => some acc
+    | "--names" :: rest => flags (true, acc.2) rest
+    | "--tsv" :: p :: rest => flags (acc.1, some p) rest
+    | _ => none
+  match args with
+  | a :: b :: rest =>
+    let some (names, tsv?) := flags (false, none) rest | IO.eprintln usage; return 2
+    diffMode a b names tsv?
+  | _ => IO.eprintln usage; return 2
+
+end Benchmarks.Canon.IxeDiff
+
+def main (args : List String) : IO UInt32 := Benchmarks.Canon.IxeDiff.main args