formalization: verify Ix.Tc and establish the Ixon v2 compiler refinement path

[johnchandlerburnham]

Summary

This PR lands the current Ix formalization checkpoint on Lean 4.33.1 and the
published argumentcomputer/lean4ix development line. It brings together
three connected pieces of work:

1. an audited Ix.Tc verification layer for production checking, ingress,
   block transactions, and the currently supported inductive, projection, and
   quotient slices;
2. Ixon v2, which records usage and ownership modes on binders in both Lean
   and Rust while conservatively embedding ordinary Lean terms; and
3. a new compiler-verification library that relates source Lean values,
   production compiler execution, Ixon values and metadata arenas, wire
   codecs, and Lean4Ix's independent Theory semantics.

The compiler theorem is intentionally independent of Ix.Tc acceptance. The
checker and compiler now meet at the same Lean4Ix semantic endpoint, but a
compiler theorem cannot prove correctness merely by showing that the output
checker accepts its own encoding.

This is a foundation checkpoint rather than the end of the compiler roadmap.
It proves the ordinary, surgery-free expression path and the first complete
codec domains; whole declarations, mutual blocks, whole environments,
canonical-address invariance, richer mode-producing compilers, and production
Rust refinement remain later milestones.

Why this is one PR

These changes share one representation and trust boundary:

• Ix.Tc interprets potentially hostile Ixon and must show that successful
  checking admits valid Lean4Ix declarations.
• The compiler starts with kernel-admitted Lean objects and must show that its
  Ixon output has the same independently stated value.
• Ixon v2 is the format both sides exchange, so its binder modes, table
  semantics, metadata, and byte grammar must be represented consistently in
  Lean, Rust, ingress, decompilation, tests, and proofs.

Landing only one layer would either leave the new format without its semantic
bridge or leave the proofs pinned to the obsolete representation. This stack
keeps the format transition, production behavior, semantic relations, and
trust audits reviewable at the same commit boundary.

Main changes

1. Lean 4.33.1 and Lean4Ix integration

• Pins argumentcomputer/lean4ix at
  a4188d7c2979378d85c6bb41fdd96c3a48a71371. The Lake package and Lean
  namespace remain lean4lean / Lean4Lean for source compatibility.
• Builds against leanprover/lean4:v4.33.1.
• Ports the Ix.Tc proof layer to the current Lean4Ix theory, inductive
  certificate, nested-block, projection, and checker surfaces.
• Reconciles the formalization with current main's plan-head arity audit,
  eta-adapter metadata, self-contained catalog work, and compiler/kernel
  changes.
• Narrows the exact upstream axiom manifest after the new Lean4Ix revision
  removed the transitive dependency on Lean4Lean.ptrEqExpr_eq from the
  produced-generation transaction roots.

2. Audited Ix.Tc verification checkpoint

The Ix.Tc.Verify tree connects the production checker to
Lean4Lean.Theory through explicit translation, state, cache, collision, and
world-extension invariants. The public checkpoint includes:

• successful standalone constant checking through the production
  TcM.checkConst path, including concrete promotion from pending to trusted
  semantic worlds;
• exact failure and rollback behavior for rejected checks, rather than an
  invariant that constrains only successful executions;
• coordinated block classification, all-or-nothing admission, ownership,
  block-cache publication, and the anonymous-environment driver;
• proof-visible cache, context, inference, WHNF, definitional-equality,
  projection, and bounded-recursion interfaces used by those public roots;
• a concrete supported Boolean environment whose production enumeration and
  checking schedule is related to an independently justified semantic
  topological schedule;
• singleton, indexed, mutual, recursive-Pi, alias, and nested inductive
  fixtures, including constructor positivity and validation traversals;
• generated-recursor construction, selection, metadata, type closure,
  member checking, rule comparison, and atomic family/recursor admission;
• the concrete LeanBox/LeanTree nested transaction, with restored
  recursors and rules, both production block checkers, exact restored iota
  patterns, and no surviving flat auxiliary declaration;
• small-elimination and Eq/K-target fixtures that preserve recursor universe
  layout and the generated K bit;
• an Ix projection relation instantiated by Lean4Ix's registered projection
  semantics, including substitution, universe instantiation, and a concrete
  dependent-record projection; and
• conditional quotient admission and quotient-reduction bridges that invert
  the real production executions while taking the still-upstream semantic
  transactions as explicit theorem inputs.

The production checker changes associated with this proof work also fail
closed when a coordinated block body disappears and avoid falling through to
a second standalone check after coordinated handling.

The inductive implementation is factored into proof-visible stages and kept
aligned with Rust. The main hardening points include checked metadata sums,
nested-application arity checks, specialization-aware auxiliary deduplication,
block-level recursor construction, complete-type selection for auxiliary
recursors, canonical peer-header checks, and exact type/rule/K-target
comparison before accepting stored recursors.

This is not an unconditional claim about every Ix.Tc feature. The exact
completed manifest contains 2,034 theorem roots. A separate one-root
conditional manifest names the two remaining mutual-recursion witnesses:

• Ix.Tc.Upstream.Pending.mutualTreePhysicalGenerationWF
• Ix.Tc.Upstream.Pending.mutualTreePhysicalRulePatternSound

Quotient bridges similarly receive their semantic transaction/law resources
as parameters; Ix does not manufacture those resources with a new global
axiom. Remaining Lean4Ix metatheory debt is recorded by exact transitive
origin rather than duplicated or hidden locally.

3. Ixon v2 binder modes and wire format

Ixon expressions now carry substructural intent directly:

• lambdas store Uses (erased, linear, affine, or many);
• foralls store both Uses and Owned (unique or shared);
• ordinary Lean lambdas compile as many;
• ordinary Lean foralls compile as many/shared.

The stable format id is ixon-v2; .ixe environment version 2 begins with
the 0xE2 header. The Lean and Rust readers/writers agree on the new mode
bytes and maximal lambda/forall telescope grammar. They reject invalid mode
bits, noncanonical nested telescopes, invalid Boolean let flags, trailing
bytes in full-buffer decoders, and incompatible environment versions.

All affected in-repo consumers are ported, including production compilation,
Lean and Rust decompilation, anonymous and metadata ingress, sharing,
typechecking, FFI conversion, tests, and documentation. Existing v1 .ixe
artifacts must be regenerated; the version error reports that requirement
directly.

The Aiur IxVM is now a first-class v2 consumer as well. Its internal Ixon
schema carries the same Uses and Owned fields, its deserializer validates
the exact v2 mode ranges and Boolean let flag, and its reader rejects
non-maximal App, lambda, and forall telescopes. Its serializer emits the modes
again, so Reveal checks the address of the exact committed v2 expression;
the modes are erased only afterward when converting into the current
mode-agnostic kernel expression representation.

Because binder bytes participate in content addressing, the v2 transition
also rekeys canonical declarations. This checkpoint regenerates the canonical
Rust primitive-address table, the Lean typechecker table, every Aiur IxVM
primitive literal, the generated 5.8 MB Rust Aiur kernel, and the affected FFT
cost pins. The legacy/original primitive table and the synthetic
eagerReduce marker remain unchanged. Address-parity tests scan the elaborated
Aiur AST, including the formerly inline Eq address, so an unlabelled stale
literal cannot bypass the table comparison.

The IxVM coverage includes a positive hash-bound Reveal fixture containing
linear, affine, and erased usage plus unique/shared ownership. Raw committed
fixtures exercise the negative boundary for reserved mode bits, non-Boolean
let flags, and non-maximal App/lambda/forall telescopes.

The semantic bridge proves that erasing v2 modes is constructive in both
directions for the related ordinary Lean fragment. This PR does not yet make
the Lean compiler infer or exploit linear/affine/unique modes; its current
output deliberately inhabits the conservative many/shared subset.

4. Independent compiler semantics

This PR adds IxCompileVerify as a separate, non-default Lean library. Its
statement frontier deliberately does not import checker acceptance as the
compiler specification.

The new source/target model includes:

• IxonExprRel, a table-aware relation from Ixon expressions to Lean4Ix
  VExpr values;
• direct coverage for external references, mutual references, sharing,
  literals, lambdas, foralls, lets, metadata erasure, and projections;
• a SourceExprRel for named Ix source syntax and an explicit
  KernelSourceWitness boundary, without treating the production compiler or
  decompiler as a semantic oracle;
• a finite Catalog with explicit canonical, anonymous-operational,
  metadata-sidecar, and decompile-only views;
• Catalog.WF, table resolution, ordered sharing resolution, projection
  address integrity, and explicit digest/key-faithfulness assumptions; and
• a total ordinary-fragment reference compiler whose universe and expression
  outputs preserve the independent Lean4Ix value.

Hash-map and content-address assumptions are scoped to finite run support.
They are theorem premises, not implicit claims that cryptographic collision
freedom follows from Lean's BEq implementation.

5. Production compiler refinement

The production compiler now exposes kernel-visible total paths for the part
covered by this checkpoint:

• CompileM.compileUniv is structurally total and refines the reference
  universe compiler through CompileM.run.
• Universe interning preserves finite-table well-formedness, sound warm
  memos, and the independent Lean4Ix universe value.
• CompileEnv.surgeryFree selects a total compileExprNoSurgery path when no
  ordinary, brecOn, or below call-site plans are present.
• Plan-bearing environments retain the existing eta/plan-aware surgical
  compiler; the merge preserves main's plan-head arity checks and eta adapter
  behavior.
• The total expression path preserves the existing production flattened-App
  spine, arena allocation order, cache lookup/insertion behavior, local mutual
  references, external references, arbitrary universe vectors, literals,
  projections, binders, lets, and metadata. Lean/Rust equality remains checked
  by the differential gates below.

The refinement proof is layered rather than monolithic:

• structural expressions first refine the reference compiler with a sound
  warm expression cache;
• frozen preseed relations then cover table-backed external and mutual
  constants, universes, literals, and projections across the complete
  recursive ordinary-expression tree;
• ArenaRel connects the returned metadata root to the source expression;
• arena growth is append-only and bounded by a cache-free source allocation
  cost, with UInt64 no-wrap stated explicitly; and
• all of the above composes into a production-run theorem preserving the
  independent Lean4Ix expression value.

Call-site surgery itself is not claimed by these theorems. The public
dispatcher is proved only under CompileEnv.surgeryFree; plan-bearing
behavior remains protected by the existing differential tests while its
formal refinement is future work.

6. Metadata and presentation-store refinement

Expression metadata is no longer restricted to empty maps in the verified
ordinary path.

• Production serializeIxSyntax is structurally total and has an exact
  reference/run theorem.
• Metadata compilation covers strings, booleans, names, naturals, integers,
  source spans, pre-resolved identifiers, nested syntax arrays, and final
  serialized syntax blobs.
• compileDataValue and compileKVMap refine their total reference encoders
  while changing only presentation-side name/blob stores.
• A separate strict theorem scopes name-hash and blob-address faithfulness to
  the finite metadata traversal, preserves old lookups, and proves recovery
  of every collected name, ancestor name component, and blob payload.

This separation is intentional: anonymous semantic preservation does not
inherit stronger metadata-key assumptions merely because a source expression
contains presentation data.

7. Total Ixon codec foundations

The production Lean universe and expression writers/readers are now
kernel-visible total definitions.

For universes, this PR proves:

• exact full-buffer decoding;
• inverse laws for trimmed little-endian integers and both Tag2 forms; and
• exact round trips for the full representable universe domain, including the
  Sort 1 universe required by the first declaration fixture.

For expressions, this PR proves:

• exact Tag0 and Tag4 inverse laws;
• full-buffer rejection of trailing bytes; and
• exact round trips for all twelve expression constructors on the canonical
  singleton-spine, empty-universe-vector domain.

That expression domain contains the A : Sort 1 type and both the type and
value shapes of idA : A -> A. Nonempty universe-index vectors and maximal
App/lambda/forall telescope round trips remain the next X1 codec slice; this
PR does not claim the full expression wire theorem yet.

8. Exact trust manifests

Trust is checked per exported theorem root rather than summarized informally.

• Ix.Tc.Verify.Audit.Completed: 2,034 completed roots.
• Ix.Tc.Verify.Audit.Conditional: one root with exactly named pending
  dependencies.
• Ix.Tc.Verify.Audit.Statements: seven statement/frontier roots.
• Ix.Compile.Verify.Audit.Statements: 47 compiler roots.
• Both Ix.Tc and compiler source-frontier audits reject any local declaration
  that directly uses sorryAx.

Each root records its exact standard axioms, native axioms, upstream
sorryAx origins, pending assumptions, and forbidden dependencies. The audit
fails both when an unlisted dependency appears and when a stale expected
dependency disappears. The compiler statement frontier independently relates
source and Ixon values and does not use checker acceptance as its semantic
specification.

The conditional Ix.Tc audit is added to the merge workflow. IxCompileVerify
remains deliberately separate and non-default, so its focused build/audit
command is included below.

Compatibility and operational impact

• Wire compatibility: .ixe v1 artifacts are not accepted as v2 and must
  be recompiled.
• Content addresses: any expression or declaration whose canonical bytes
  contain binders receives a new v2 address. Canonical primitive tables and
  fixtures in this repository have been regenerated; external catalogs,
  claims, caches, and address-pinned artifacts must be rebuilt.
• Compiler output: ordinary Lean compilation remains conservative
  (many/shared) and passed Lean/Rust byte-differential checks.
• Call-site plans: plan-bearing compilation continues through the existing
  surgical implementation; main's eta adapters and plan-head validation are
  preserved.
• Kernel behavior: malformed nested applications, inconsistent generated
  recursor peers, missing generated recursors, and mismatched recursor
  metadata/rules now fail closed.
• IxVM behavior: Aiur parses and reserializes the exact v2 expression at
  the content-address boundary, rejects noncanonical encodings, and erases
  binder modes only when entering the current kernel AST.
• Cryptography and proof artifacts: BLAKE3, SHA-256, Merkle, claim, and
  multi-STARK algorithms and codecs are unchanged. Their inputs are not:
  regenerated Ixon addresses and the changed guest/kernel programs invalidate
  cached Aiur proofs and any SP1/Zisk proof or verification-key material tied
  to the prior program bytes. Those artifacts must be regenerated rather than
  translated.
• Build topology: the large proof libraries remain outside the default
  runtime build. They are built explicitly for formalization and trust
  auditing.
• Trust posture: no claim silently upgrades an explicit collision,
  native-reduction, upstream theorem, or semantic-transaction premise into a
  proved fact.

Validation

The merged branch was validated at 158108e6 with the following commands.

Default build

nix develop --command lake build

Result: passed, 301 jobs.

Ix.Tc proof and trust frontier

nix develop --command lake build \
  Ix.Tc.Verify.Audit.Completed \
  Ix.Tc.Verify.Audit.Conditional \
  Ix.Tc.Verify.Audit.Statements \
  Ix.Tc.Verify.Audit.SorryFrontier

Result: passed, 620 jobs; 2,034 completed roots, one conditional root, seven
statement roots, and no Ix.Tc verification source declaration using
sorryAx.

Compiler proof and trust frontier

nix develop --command lake build \
  Ix.Compile.Verify.Audit.Statements \
  Ix.Compile.Verify.Audit.SorryFrontier

Result: passed, 99 jobs; 47 exact theorem roots and no compiler-verification
source declaration using sorryAx.

Lean/Rust auxiliary compiler differential

nix develop --command lake test -- --ignored aux-gen-diff

Result: passed all plain-drift, expansion, patch, plan, driver, and parallel
gates. Lean and Rust produced identical 6,893,510-byte environments.

Ingress corpus

nix develop --command lake test -- --ignored tc-ingress-meta

Result: passed all seven corpus groups: nat-add, list-map, nat-arith,
eq-basics, bool-decide, char-ordinal, and inductives-recursors.

Decompiler differential

nix develop --command lake test -- --ignored decompile-diff

Result: passed for 6,615 constants with zero errors or mismatches: 3,969 plain
constants and 2,646 auxiliary constants. Call-site replay and plan parity
gates also passed.

Ixon codec and parity suite

nix develop --command lake test -- ixon

Result: passed the full Ixon syntax/codec suite, including v2 mode vectors,
malformed-input rejection, and Lean/Rust byte parity.

IxVM generated kernel and security boundary

nix develop --command lake exe ix codegen --check
nix develop --command lake test -- prim-addrs primitive-address-parity
nix develop --command lake test -- --ignored ixvm

Result: generated Aiur sources were current; canonical and original primitive
address parity passed across Rust, Lean, and 89 named Aiur literals; and the
full ignored IxVM suite passed. The latter includes all kernel execution and
interpreter/native parity cases, every regenerated FFT cost pin, the shard
pipeline pin (6,859,583,032), the positive v2 binder-mode Reveal, and all
six malformed-v2 rejection fixtures.

Cryptography and recursive-verifier regression suite

nix develop --command lake test -- \
  aiur-hashes claim merkle assumption-tree multi-stark

Result: passed BLAKE3 and SHA-256 execution/proving vectors, claim and
assumption-tree codecs, Merkle properties, and the multi-STARK PCS, challenger,
FRI, reduced-opening, and field-arithmetic reference comparisons.

Rust workspace check

nix develop --command cargo check --all-targets --all-features --workspace

Result: passed, including ixon, ix-kernel, aiur, multi-stark,
ixvm-codegen, ix-compile, and the FFI crates.

The SP1 and Zisk guests depend on the shared ixon, ix-kernel, and
ix-common crates, so their CI jobs must rebuild their guest ELFs and derive
fresh program verification keys. Those specialized guest toolchains were not
run locally; the ordinary Rust workspace check does not compile the excluded
zkVM targets.

The final merge also passed git diff --check and contained no unresolved Jj
conflict markers.

Suggested review order

The branch is intentionally split into reviewable commits:

Commit	Review focus
8a17a720	Lean 4.33 Ix.Tc verification checkpoint, production checking/inductive changes, and trust manifests
49f2dd43	Ixon v2 binder modes and Lean/Rust representation port
f5660b1b	Conservative v2 value relation to Lean4Ix
d1eae96b	Reference compiler semantics and production state relation
6fece592	Production expression compiler refinement
5a077b94	Table-backed leaves and universe/reference interning
5cc3d4af	Complete ordinary-expression refinement and value theorem
cac72b91	Metadata arena relation and growth bounds
2f205d5f	Scalar expression metadata integration
fa449102	Total syntax metadata serialization
fd1a7417	Strict metadata side-store recovery
fee3b893	Initial total universe codec laws
df7d67cb	Full representable universe codec theorem
aa286acc	Singleton-domain expression codec theorem
6f18ea90	Merge of current main and compiler/ingress reconciliation
158108e6	Aiur IxVM Ixon v2 consumer, regenerated addresses/kernel, strict Reveal tests, and FFT pins

A practical review sequence is:

1. review Ixon v2 and production consumer changes;
2. review the public Ix.Tc and compiler statement frontiers;
3. inspect the exact trust manifests and forbidden-dependency lists;
4. review proof modules by theorem slice; and
5. use the differential and corpus gates to assess production equivalence.

Non-goals and follow-up work

This PR does not claim:

• complete Ix.Tc soundness for every kernel feature and every hostile Ixon
  environment;
• constructive discharge of the separately named mutual-recursion or
  quotient semantic resources still assigned to Lean4Ix;
• removal of all upstream Lean4Ix metatheory debt;
• a production compiler for non-conservative linear, affine, erased, or unique
  binder modes;
• formal refinement of plan-bearing call-site surgery;
• the full expression codec theorem for nonempty universe vectors and maximal
  telescopes;
• declaration, mutual-block, whole-environment, or canonical-address compiler
  theorems (X3-X5);
• full metadata/decompile/recompile recovery (X6);
• refinement of the parallel Lean compiler or Rust compiler to the verified
  reference pipeline (X7); or
• Rust-kernel, Aiur, or proof-system soundness.

The next bounded compiler slice is to extend the expression codec theorem to
nonempty universe-index vectors and maximal App/lambda/forall telescopes, then
lift the A/idA fixture through declaration bytes and content addresses.
The typechecker track can continue independently by replacing the remaining
conditional Lean4Ix resources with constructive definitions and proofs as
they become available.

[arthurpaulino]

!benchmark aiur-sharded-env

[argument-ci-bot]

!benchmark — main vs 1d9242e

backends: aiur-sharded-env · envs: ISLB

aiur-sharded-env · ISLB — main from: bencher @ 0f34977

1 constant · 0 with regressions · 0 with improvements (|Δ| > 3.0% on any metric).

constant	check-time (main)	check-time (PR)	Δ%	throughput (const/s) (main)	throughput (const/s) (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	constants (main)	constants (PR)	Δ%	shards (main)	shards (PR)	Δ%
ISLB	1m 21.7s	1m 23.0s	+1.6%	2.24K	2.21K	-1.5%	94.18 GiB	94.72 GiB	+0.6%	183,062	183,062	+0.0%	151	152	+0.7%

Workflow logs