Ixon v4, with canonical sharing and TagN integers

[johnchandlerburnham]

Ixon v4: canonical sharing (two-phase exact construction canonicalSharingTiered) and TagN integers

Summary

This PR makes a constant's sharing table part of its canonical bytes. The table is built by a
construction whose phase-1 minimality is machine-checked, whose reported length is proved to be
its serialized length, and whose output is proved to be in the codec's wire domain. The PR also
replaces Ixon's three variable-length integer codes with one bijective code, TagN, and
compresses the metadata arenas with an implicit post-order child encoding. Together these bump
the binary format to version 4: every address, .ixe, claim and primitive pin changes.

• Size. The import Mathlib environment is 2,318,833,546 bytes in v4, against
  3,343,271,273 bytes in v3 (−30.6%) and 2,620,063,965 bytes for v4's integers and arenas with
  the old heuristic sharing (−11.5%); Init is 143,680,738 bytes against 195,387,870 (−26.5%) and
  155,259,078 (−7.5%) [Perf; Arena §7]. Constant bytes fall by 21.2% on Mathlib and 14.8%
  on Init against the heuristic tables [Perf §Format v4].
• Compile time. Mathlib ix compile takes 1.24–1.30× the heuristic route's wall time
  (within the owner's 1.5× bound), with byte-identical output before and after the
  optimizations [Perf].
• Proofs. 250 audited theorem roots; the compiler's fast code is tied to the proved
  specifications by audited @[csimp] equalities.

Why: the heuristic was neither minimal nor safe from blow-up

The previous sharing heuristic (Ix/Sharing.lean, crates/ixon/src/sharing.rs, both removed
here) picked subterms by a local profitability test.

• It missed obvious savings. On the plan's T2 → T2 fixture (T2 = Prop → Prop → Prop):

  • unshared: 20 bytes;
  • heuristic: 19 bytes;
  • minimum: 17 bytes (d200009117b0b001921700170000000100).

  The canonical construction produces those 17 bytes [Ixon §Sharing System, Example;
  Tests/Ix/SharingExact.lean group "fixture T2 → T2 (19 → 17)"; exact-sharing-ffi "compiler
  route: T2 → T2 in the 17-byte minimum"].

• It could be larger than not sharing at all.

  • On T16 → T16: heuristic 81 bytes against 78 unshared; the construction gives 46
    [Init §Witnesses from the plan; Tests/Ix/SharingTiered.lean].
  • In the corpora, the heuristic's stored bytes exceed the unshared encoding for 600 Init
    constants [Init §Headline] and 20,237 Mathlib constants [ML §Headline].
  • The canonical construction is never larger than unshared on either corpus [Perf §Bytes, X1 X2].

• Its output was never specified. It was deterministic, but defined only as an algorithm with
  local choices. Nothing stated or checked what an encoder must produce, or how close to optimal
  it is.

The canonical rule

The canonical sharing of a constant is defined as a function of its expanded anonymous
expressions, its roots in ConstantInfo order [Ixon §Sharing System]. Two compilers, or two
runs, that agree on the expressions must produce the same bytes, regardless of in-memory pointer
sharing, construction order or existing tables. Metadata never influences the table.

Construction (Ix.Sharing.Exact.canonicalSharingTiered .tagN, Rust
canonical_sharing_tiered(ShareLayout::TagN, ..); the only sharing route of both compilers):

0. Structural IDs. Subterms are numbered by height, then by (tag, scalars, child IDs).
   Identity is the structural key, never a hash or pointer [Plan §3.2; Ix/Sharing/Exact/Dag.lean].
1. Phase 1: uniform-model optimum at each width w ∈ {1, 2, 3}.
   • Every Share costs w bytes and everything else is priced exactly.
   • The class is tables of terms with compact in-degree ≥ 2. The search classifies candidates
     (certain-stored, certain-excluded, uncertain) and runs an exhaustive branch and bound per
     independent component.
   • Ties go to the setPrec-least minimum [Plan §12.3, §12.6].
2. Phase 2: slot allocation.
   • An exact maximum-reference first tier of at most 8 one-byte slots, closed under body
     references.
   • The rest in Kahn priority order (most references first, ties by ID).
   • A guard keeps the phase-1 order if it is cheaper [Plan §12.14].
3. Phase 3: re-materialization. Each entry and each root is rewritten at minimum length
   against its dictionary, with every Share priced at its real TagN width.
4. Width selection. Keep the candidate with the fewest real bytes, ties to the lower w
   [Plan §12.11]. An error at any width fails the call, with the lowest failing width's error.

Width 3 stays: dropping it would cost 35,783 bytes on Mathlib (1,395 constants) and 6,891 bytes
on Init (184 constants), and is held in reserve [Plan §12.18].

What is proved, and what is not

Lean, roots of the compiler audit manifest: each root's axioms are fixed exactly, and the sorry
frontier covers Ix.Compile.Verify and Ix.Sharing (250 roots at d47b39f9 [Audit]). The
construction theorems are stated for a successful run on the canonical DAG of the input
[Ixon §What is proved, and what is not; Plan §12.13].

• Phase 1 (Ix/Compile/Verify/UniformOptimality.lean), optimizeUniform_minimum and
  optimizeUniform_least. Given a successful run with the default search
  (uniformSubsetSearch = false; the compiler cannot change it):

  • the stored set minimizes the uniform-width model over all tables of in-degree-≥ 2 terms;
  • its model bytes equal that minimum;
  • it is the setPrec-least minimum.

  The certain-excluded rule needs telescope spines shorter than the fifth TagN rung end; the
  optimizer checks that before it runs, so the theorems carry no extra hypothesis.

• Phase 2 (TieredTier.lean: allocate_spec, firstTier_spec; TieredGuard.lean:
  allocate_optimal): the first tier is a maximum-weight closed set, first in the tie order;
  the final order is a dependency-respecting permutation whose reference cost is at most the
  phase-1 order's, and the minimum over all dependency-respecting orders for tables of at most
  1,032 entries.

• Phase 3 (TieredPhase3.lean: materializeTable_min, rematerialize_spec,
  materializeTableOnePass_eq; TieredGuard.lean: phase3_le_phase1): every entry and root has
  the minimum layout length for its dictionary; the output re-expands, against the canonical
  DAG, to the stored terms and the input's root IDs; references are backward; the length is at
  most the phase-1 candidate's; the one-pass implementation equals the per-prefix specification
  on every input.

• Selection (TieredSelect.lean, canonicalTieredCore_select): the fewest final layout
  bytes of the three candidates, and the lowest width on ties.

• Serialized length (TieredWire.lean, canonicalSharingTiered_serialized): the length the
  construction reports is the table count's length plus the serialized length of every entry
  and root, and equals the layout price it minimized. So the minimized bytes are wire bytes.

• Wire validity (TieredWire.lean, canonicalSharingTiered_format): every output entry and
  root is wireWF, the table count is below 2^64, and Shares are backward. The compiler
  endpoint theorems (buildConstantWithSharing_wireWF and every *_codecWF endpoint) are
  stated over it and conclude SharingRunOK: a compiler run returns an exactly decodable block,
  or fails with an error of the sharing builder (whose payload the theorem quantifies
  existentially).

• Structural IDs (SharingExactCanon.lean, canonicalize_det): canonicalizing interned
  terms depends only on the terms the roots denote.

• TagN (Ix/Compile/Verify/TagN.lean): putTagN_inj, runGetExact_getTagN_eq/_iff/_inj,
  getTagN_rejects_code, getTagN_rejects_overflow; every codec theorem is stated over the
  TagN facts.

The compiled code is the proved code. The compiler runs fast twins of the specifications
(Ix/Sharing/Exact/{Phase3,Reexpand,UniformSearchLocal,TierFast,PinnedDeps,PinnedFast,KnapsackFast,TieredFast}.lean,
and a few inside the specification modules). Each is attached by a @[csimp] theorem
@f = @fFast, an unconditional equality of the whole result (values, metered counts, errors),
so compiled code calls the twin while every theorem talks about the specification. The new audit
module Ix/Compile/Verify/Audit/CompiledCode.lean fails the build unless every @[csimp]
theorem on the compiler's import path is an audit root (19 at d47b39f9), and unless
Ix.Sharing.* contains no unsafe, partial, @[implemented_by] or @[extern] declaration
besides the interner's pointer-cache key exprPtr. The module map in Ix/Sharing/Exact.lean
lists every specification, twin and csimp theorem.

Run-time checks that remain, each failing closed with an internal error: in Lean's phase 3,
layout length = evaluated length, at most phase 1's layout length, re-expansion to the stored
terms and the input's root IDs, and the wire domain (every candidate); in Rust, the checks listed
in the module documentation of crates/ixon/src/sharing_exact/tiered.rs (below).

What is not proved or claimed:

• No global minimum. The result is not a global byte minimum over all tables, orders and
  occurrence choices. The original target, the global minimum under the key of plan §3.3, was
  found infeasible at production scale and superseded [Plan status note, §12.1].
• Phase 2 on tables of more than 1,032 entries, whose indices span the 2- and 3-byte rungs.
• Expansion. The step from the input expressions to the canonical DAG (expand: share
  expansion and interning, with a pointer cache keyed by exprPtr, an unsafe address read) is
  outside the proofs: no theorem states that the DAG denotes the input. The round trip is proved
  relative to the DAG and re-checked at run time through the same interner; independence from
  in-memory pointer sharing is tested (120 generated inputs in four pointer layouts), not
  proved. Idempotence is proved only under the hypothesis that the output expands to the
  input's DAG (canonicalSharingTieredTable_idem), and tested.
• Rust is not proved. It is held to Lean by byte-for-byte differential tests (below). Its
  phase-1 search evaluates a component's area under a truncated cost model where the Lean
  specification evaluates the whole closure; outputs are equal on every input tested.
• 128-bit lengths in Rust. Rust's phase 1 fails closed (format bound: LengthOverflow) where
  Lean's Nat succeeds, for example on the chain e(i+1) = App(e(i), e(i)) at depth 127 or more.
  No Init or Mathlib constant is near this; the divergence is documented, not removed.
• No fixed distance from optimal. On Init, no measured encoding (heuristic, MSS, uniform
  outputs) was shorter than the width-1 model optimum, for the 55,263 constants certified at all
  three widths [Init §Checks]. The gap to the true minimum is not measured; the width-state
  oracle only runs on small inputs [Perf §What is not covered].

Format: TagN and version 4

TagN replaces Tag0, Tag2 and Tag4 everywhere, with flag widths 0, 2 and 4 [Ixon §Integer
Encoding (TagN); Plan §12.12, §12.16].

• Layout. A header byte holds the flag and a payload, followed by 0, 1, 2, 3, 4 or 8 bytes.
  The six rungs are 1, 2, 3, 4, 5 and 9 bytes wide. For f = 4 the rung ends are 8, 1,032,
  66,568, 16,843,784 and 4,311,811,080. The normative layout is the TagN docstring in
  Ix/Ixon.lean.
• Bijective. Each rung starts where the previous one ends, so every value has exactly one
  encoding. The three "noncanonical Tag0/Tag2/Tag4 integer" reader checks are gone. Readers
  reject only invalid codes, values reaching 2^64 and truncation.
• Compatibility. Values below 128, 32 or 8 (for f = 0, 2, 4) encode to the same single byte
  as before. Larger ones change: Share(8) was B8 08 and is now B8 00, and N0(1000) was
  81 E8 03 and is now 83 68 [Ixon §Examples].
• No integer gets longer below 4,311,811,080, the fifth rung end. Repricing every integer of
  Init's stored encoding saves 2,050,766 bytes (−2.56%), of which −2,046,174 is Share indices
  256–1,031, which go from 3 bytes to 2 [Init §Integer repricing (TagN) follow-up].

Version and identifiers [Ixon §Environment Serialization, §Proofs and Claims]:

item	v3	v4
.ixe header byte TagN(0xE, version) (Ixon.Env.VERSION, Env::VERSION)	0xE3	0xE4 (the same byte as the Check claim tag; readers interpret it by context, as 0xE3/Eval before)
wire format ID (wireFormatId, WIRE_FORMAT_ID)	ixon-v3	ixon-v4
claim/proof/catalog object-format byte (Env.OBJECT_FORMAT)	3	4
resource validator ID (and profile prefix)	ixon-v3/resource-v1	ixon-v4/resource-v1 (wireFormatId ++ "/resource-v1")
Catalog / Resource claim tags	E8 08 / E8 09	E8 00 / E8 01 (TagN rung 2)
catalog manifest version	2	2 (object-format byte inside: 4)
text grammar version	3	3 (no change)

A reader given another version fails with "expected .ixe format version 4, got N — recompile
the artifact"; a claim with another object format with "claim: unsupported object format N,
expected 4 — regenerate the claim". There is no back-compat reading.

Address impact and regenerated artifacts.

• Every .ixe changes, through its header byte. Every constant with a sharing table can change,
  through the new construction; every constant with a Share index ≥ 8, a count ≥ 128 or a
  universe value ≥ 32 changes, through TagN.
• Regenerated through their producers, never edited by hand [Map §6]:
  • Tests/Fixtures/ixon-v4/ (renamed from ixon-v3/): the handoff set
    (lake exe ixon-v4-tests --export-handoff; manifest schema ixon-v4-handoff-1), claims.tsv,
    addressed.tsv and resource.tsv (--export-fixtures; the checks compare whole files),
    primitives.tsv (lake exe ixon-v4-primitives, which fails if the file differs from the
    live addresses), and expressions.txt with hand-derived multi-byte TagN rows;
  • the canonical primitive addresses in crates/common/src/prim_addrs.rs,
    Ix/Tc/Primitive.lean and the IxVM kernel (the original, LEON addresses are unchanged);
  • the catalog claim digest pin (Tests/Ix/Claim.lean, proof.rs) and the env-bytes hash
    (crates/compile/src/graph.rs);
  • the IxVM FFT-cost pins (below).
• Renamed: executables ixon-v4-tests, ixon-v4-primitives (scratch files under
  $IX_IXON_V4_DIR, default /tmp); test modules Tests/IxonV4{Main,Handoff,Primitives}.lean,
  Tests/Ix/IxonV4{,FFI,VM,Paths}.lean, Tests/Ix/ClaimsV4.lean, Tests/Ix/IxonText.lean; CI,
  flake.nix and .gitignore follow.
• Caches keyed by the version: the TruthMines piece-cache key includes ixe=<VERSION>, and
  tc-parity.ixe is recompiled when its header carries another version.

Results

Machine: AMD Ryzen AI 9 HX 370, 12 cores / 24 threads, 93.6 GiB RAM, shared with other jobs (figures indicative). Corpora: Init (56,622
constants) and the whole import Mathlib environment (679,499 constants) [Perf §Corpora].

Files [Perf]:

corpus	v3	v4 integers and arenas, heuristic sharing	v4 (this PR)
Init .ixe	195,387,870 B	155,259,078 B	143,680,738 B (−26.5% vs v3, −7.5% vs heuristic sharing)
Mathlib .ixe	3,343,271,273 B	2,620,063,965 B	2,318,833,546 B (−30.6% vs v3, −11.5% vs heuristic sharing)

Constant bytes, canonical against the heuristic tables (Rust sharing_corpus re-sharing the
heuristic-route corpora of 36fe2777, certified constants): Init 78,231,552 → 66,644,219 bytes
(−14.81%) [Perf §Format v4, R10]; Mathlib 1,422,929,264 → 1,121,697,655 bytes (−21.17%) with the
final Rust construction [Perf, R11].

Totals over rooted constants, by encoding (earlier rules: the phase-2 order before Kahn, and
v3 integers except Shares) [Perf §Bytes, X1 X2]:

encoding	Init bytes	vs heuristic	Mathlib bytes	vs heuristic
heuristic (stored on main)	80,161,846		1,468,281,356
MSS (store every in-degree-≥ 2 term), Tag4	68,547,873	−14.49%	1,148,195,956	−21.80%
MSS at TagN widths	67,556,587	−15.72%	1,130,381,317	−23.01%
canonical, TagN	66,602,235	−16.92%	1,121,167,486	−23.64%

Against MSS at the same widths, canonical is −1.41% (Init) and −0.82% (Mathlib) [Perf §Bytes].

Per constant, canonical TagN − heuristic (rooted constants) [Perf §Canonical (best of three):
per-constant distributions]:

corpus	smaller / equal / larger	p1	p50	p99	max
Init	50,406 / 4,933 / 47	−3,566	−51	0	+7
Mathlib	627,129 / 35,622 / 503	−7,015	−125	0	+36

The largest single-constant saving on Mathlib is −270,911 bytes. The largest MSS saving was on
CategoryTheory.Functor.IsDenseSubsite.isIso_ranCounit_app_of_isDenseSubsite, whose heuristic
table has 81,565 entries: 608,188 → 349,429 bytes [ML §MSS vs heuristic vs unshared].

Lean/Rust parity [Perf §Lean/Rust parity]:

run	constants	same bytes	disagreements	source
TagN corpus (36fe2777), Init, tiered-TagN	56,622	56,622	0	D10
TagN corpus (36fe2777), Mathlib sample (every 50th + every constant with > 2,000 candidates)	20,265	20,264 (1 same error on both sides)	0	D11
merge-queue partition lake test -- --ignored compile at 1179d7ba (Lean and Rust compile every constant of the test environment)	237,295	all; the serialized environments are identical (428.4 MB)	0	[Perf]
best of three, v3 corpus, Init, tiered-TagN and tiered-Tag4	56,622 each	all	0	D7

• The one same-error constant at 36fe2777 exhausted a resource limit on both sides, in the
  count-bracket knapsack, which now has its own limit (knapsack_cells) [Perf, D11 X9].

• The Rust checked mode (sharing_corpus --full-check) over all of Init (56,622) and all of
  Mathlib (679,499) reports no failure and the same output as the default mode [Perf].

Compile time

Rust (ix compile, the production compiler). The owner's bound: Mathlib within 1.5× of the
heuristic route, ideally closer; only speedups specific to the canonical route are in this PR
[Plan §12.18; Perf].

	heuristic route	canonical, before the optimizations	canonical, this PR
Mathlib, back to back (load ~8)	1:55.4 wall, 1,653 CPU-s, 19.2 GB		2:29.8, 2,294 CPU-s, 18.7 GB (1.30×)
Mathlib, quieter machine	1:50.9 / 1:46.6	8:56.6, 10,529 CPU-s	2:17.8 / 2:14.5 (1.24–1.26×)
Init	9.2 s	32.4 s	11.3–11.9 s

• The optimizations are byte-identical (same .ixe sha256 before and after). The construction
  alone, summed per constant: Mathlib 9,685 s → 940 s, Init 379 s → 50 s, slowest constant
  211 s → 1.6 s.

• What changed (Rust): phase 3 evaluates the whole table once when the order is closed under
  stored descendants (every order of Init and Mathlib; otherwise per prefix), width-independent
  tables are shared by the three widths, the table-count knapsack works on ranks, and phase 1 is
  a dry run that builds no expressions. The default mode checks every limit and every length of
  all three candidates and the built expressions of the returned one; the checked mode builds
  and checks all three [Ixon §Canonical construction].

Lean (the proved reference, and the compiler of ix compile-lean). The route switch made
the Lean compile step of the merge-queue partition 21× slower (176.6 s → 3,683.7 s). The fast
twins above bring it to 237.7 s, and the whole partition to 11:51 against 15:30 before the
route switch (the Rust side is faster) [Perf]. Single-threaded, like for like against Rust's
default mode on Init samples, the Lean construction is 8.3× (bulk, 373 constants), 10.5× (p99, 66
constants) and 15.4× (slowest 15) slower; it was 29×, 151× and 453× before the Lean
optimization work. With the
width tasks on, Lean's wall time on those samples is 885, 5,656 and 9,209 ms. The target of
2–4× is not met: the specification's cost model evaluates a component's whole closure where
Rust evaluates its area, and closing that gap needs a change of the specification and its
proofs (follow-up).

Review-driven fixes worth a reviewer's attention

• Candidate count. Rust enforced its candidates limit (2^16, meant for the width-state
  oracle) on the compiler path, so a constant with more candidates failed in Rust and compiled
  in Lean. Now neither language limits the count on the canonical path (regression test: 70,000
  distinct references used twice).
• Checked mode. ExactSharingLimits::full_check (unit tests, FFI parity hooks,
  sharing_corpus --full-check) builds and verifies all three candidates, so the default mode's
  "built expressions of the returned candidate only" cannot hide a wrong length of a losing
  candidate; it agrees with the default mode on all of Init and Mathlib.
• Per-prefix fallback fixture. The one-pass phase 3 falls back to per-prefix evaluation when
  the order is not closed under stored descendants. That path is reached by an App spine of
  1,288 nodes ending in a stored term (7,105 bytes, candidate lengths (1, 7106), (2, 7106),
  (3, 7123) in both languages), now a fixture in Lean and Rust.
• Linear metadata check. validateMetaSharing/validate_meta_sharing visit each shared
  node once; the tree walk was exponential on in-memory tables with deep sharing.
• Limits parser parity. --sharing-limits/IX_SHARING_LIMITS has one grammar in both
  languages (ASCII digits, 2^k, max, unbounded; only space, tab, LF and CR trimmed), pinned
  by one shared list of 35 specifications; the variable is read once per run, so an invalid
  value fails the run before any block is shared.
• Error messages of kernel egress and the decompiler's recompile name the constant
  (egress '<name>': …, recompile of '<name>' (sharing): …), and a recompile keeps the compile
  error's category.

Limits and failure semantics

• Explicit limits (Lean Ix.Sharing.Exact.Limits, Rust ExactSharingLimits) are a safety
  net: they decide whether a run succeeds, never which bytes a success produces. Each default is
  at least 2^6 (Lean) or 2^8 (Rust) times the earlier default under which the corpora were
  measured (for example states 2^40, materialize_work 2^56). knapsack_cells is 2^28, about
  27 times the largest knapsack on Init and Mathlib [Ixon §Canonical construction].
• Override. ix compile --sharing-limits SPEC (also ix compile-lean) sets
  IX_SHARING_LIMITS, which both compilers read once per run; keys of the other language are
  accepted and ignored. A malformed override is rejected before compiling (lake test -- cli).
• Errors, no fallback. Exceeding a limit is CompileError.resourceLimit, and the message
  names the limit and the override, e.g. canonical sharing: resource exhausted: states (limit 1099511627776); raise it with --sharing-limits states=N (IX_SHARING_LIMITS). Any other
  construction failure is CompileError.sharingConstruction. An error at any width fails the
  whole construction; no partial table is ever emitted.
• Lean and Rust count work differently (Rust's work charges the evaluations it does), so
  equal limits can succeed in one and fail in the other; every observed case was a Lean-only
  exhaustion that matched Rust once raised [Map §7 risk 2].

Metadata expressions: the reader rule only

ConstantMeta.metaSharing (collapsed call-site arguments) may contain Share(i). With p
entries in the primary table, a Share(i) inside metaSharing[j] denotes primary entry i when
i < p and metaSharing[i − p] when p ≤ i < p + j; anything else is a decode error
(invalidMetaShareIndex). A Share in a primary expression always denotes a primary entry, and
the primary table never depends on metadata [Ixon §Sharing in metadata expressions; Plan §13.1].

• Readers. Both decompilers implement the rule (Lean Ix.DecompileM.ShareScope, Rust
  decompile::ShareScope) and check the whole table, in linear time, when metadata is loaded.
  Kernel ingress, the IxVM circuit and the resource validators do not read metaSharing.
• No construction. No compiler emits such a Share. In the whole Mathlib environment,
  metadata expressions are 524 entries in 7 tables, 42,929 bytes (0.0013% of the file)
  [Init §metaSharing].
• Behaviour change. A malformed primary Share found by the semantic-contract scan is now
  reported as InvalidShareIndex instead of BadConstantFormat("semantic scan: …").

Metadata arenas

ExprMeta arenas are 43% of the Mathlib file [Arena §1]. This PR changes their encoding only:
child references that a post-order cursor predicts are implicit (one mask bit), and the others
are backward deltas [Ixon §ExprMeta Arena].

• Arenas shrink by 13.2% of the Mathlib file and 12.9% of the Init file, against the v4 baseline
  with absolute TagN indices; Lean and Rust are byte-identical [Arena §4].
• The change is serializer-only: the decoded arena is the one the compiler built.
• Not in this PR: hash-consing duplicate arena subtrees (a further 10.6% on Mathlib, 10.3% on
  Init), designed for a stacked PR [Arena §5].

IxVM

The IxVM circuit has its own Ixon codec, generated into crates/ixvm-codegen/src/aiur_ixvm.rs by
lake exe ix codegen (CI: codegen --check) [Map §3.1]. This PR updates it in the same change:

• TagN codec. Readers get_tagn0/2/4 (Ix/IxVM/IxonDeserialize.lean) and writers
  put_tagn0/2/4 (Ix/IxVM/IxonSerialize.lean): the one-byte case on one narrow row, the longer
  encodings through one shared helper per direction (get_tagn_tail/get_tagn_wide,
  put_tagn_tail/put_tagn_wide), parameterised by the flag width. The circuit rejects what
  Lean and Rust reject (invalid codes, values reaching 2^64, truncation); the primary runner
  ixvm-tagn (about 16 s) holds it to Ixon.putTagN/getTagN on every rung boundary, the
  rejection vectors (every invalid code followed by as many zero bytes as a valid rung reads, so
  length alone does not reject them), every one-byte string and a sample of two-byte strings.

• Claims. Object format 4 in run_claim and in the aggregator's CheckEnv parser; Resource
  (E8 01) decodes and is rejected explicitly, Catalog (E8 00) has no arm and is rejected; the
  assumption-tree header check is exact (0xE2). The VM tests reject object formats 3 and 5
  and include positive controls.

• Primitive addresses. The kernel's address literals (Ix/IxVM/Kernel/*.lean) are the v4
  canonical addresses (prim-addrs).

• Cost. Committed column widths per row of the codec functions (ungrouped):

  function	f = 0	f = 2	f = 4
  reader, old → new	48 → 29	48 → 36	45 → 36
  writer, old → new	32 → 25	33 → 26	33 → 26

  A two-byte integer read costs 64 committed cells instead of 251 (f = 4) and 57 instead of 254
  (f = 0).

• FFT-cost pins re-pinned (Tests/Ix/IxVM.lean, shard pin in Tests/Main.lean), against
  current main: all 83 kernel-check pins fall, in sum from 84,117,274,306 to 78,407,654,680
  (−6.79%), and the shard pipeline from 7,189,745,580 to 6,236,673,618 (−13.3%). This is the
  combined effect of canonical sharing, TagN and the new addresses.

• Not changed here: the IxVM function grouping (the writers stay in their 70/128-column
  groups and the four new helper circuits are ungrouped) and the reviewer's put_tagn_tail
  lookup micro-optimization; both are left to the optimization pass of the circuits during
  review.

Reviewer's guide

Sizes are from wc -l at this head, or git diff --stat b4fea976.. (the merge base with
main) for the proofs. The PR is squashed into the logical commits of plans/squash-plan.md.

area	files	notes
TagN codec and version	Ix/Ixon.lean (TagN section, putTagN/getTagN, Env.VERSION, Env.OBJECT_FORMAT), crates/ixon/src/tag.rs, crates/ixon/src/serialize.rs, crates/ffi/src/lean_ixon/serialize.rs; tests Tests/Ix/Ixon.lean (tagNUnits), Tests/FFI/Ixon.lean	start here: every other part builds on it
exact core, Lean (12,942 lines)	specifications Ix/Sharing/Exact.lean, Ix/Sharing/Exact/{Basic,Dag,Dictionary,Search,UniformSearch,Uniform,Tiered}.lean; fast twins Ix/Sharing/Exact/{Phase3,Reexpand,UniformSearchLocal,TierFast,PinnedDeps,PinnedFast,KnapsackFast,TieredFast}.lean; helpers SortedSets.lean, test oracle Oracle.lean	read the module map in Exact.lean first; Tiered.lean has each phase's claim; review a twin through its csimp theorem, not line by line
exact core, Rust (12,786 lines, of which 3,846 are tests)	crates/ixon/src/sharing_exact.rs, crates/ixon/src/sharing_exact/{dag,cost,dict,search,uniform,tiered,par,roots,oracle,mss,prof,tests}.rs	a port of the Lean core; tiered.rs module docs, "Checks", list every check per mode; par.rs is deterministic parallelism; mss.rs is a test-only reference; prof.rs the sharing-profile timers
Lean/Rust parity	crates/ffi/src/lean_ixon/sharing.rs, Tests/Ix/SharingExactFFI.lean (suite exact-sharing-ffi; corpus mode via IX_SHARING_CORPUS)	re-normalization of table-carrying inputs and malformed tables included
proofs (+27,188 / −2,379 lines in 54 files, 30 of them new)	Ix/Compile/Verify/{TagN,SharingExact,SharingExactPasses,SharingExactCanon}.lean, Uniform*.lean (phase 1; headline in UniformOptimality.lean), Tiered{Select,Tier,Guard,Model,Phase3,Idem,Wire}.lean, the endpoint wiring in CompileSharingCodec.lean and Compile*Codec.lean; roots in Audit/Statements.lean; Audit/CompiledCode.lean (csimp and unsafe audit); Audit/SorryFrontier.lean	read the headline statements, then each module docstring
compiler routing	Ix/CompileM.lean (buildConstantWithSharing, compilerSharingLimitsFromEnv), Ix/CompileDriver.lean, Ix/DecompileDriver.lean, Ix/AuxGen/CompileAux.lean, Ix/Cli/CompileCmd.lean (--sharing-limits), crates/compile/src/{compile.rs,compile/mutual.rs,kernel_egress.rs,decompile.rs}	one route; decompile's recompile uses the compiler's route (the recompiled address must equal Named.original); Ix/Sharing.lean, crates/ixon/src/sharing.rs, Ix/Compile/Verify/Sharing.lean and Tests/Ix/Sharing.lean are deleted
metadata readers	Ix/DecompileM.lean, Ix/SemanticContract.lean, crates/compile/src/{decompile.rs,semantic_contract.rs}, crates/ixon/src/error.rs; tests Tests/Ix/Decompile.lean	the extended index space of Share in metaSharing
arenas	Ix/Ixon.lean and crates/ixon/src/metadata.rs (ExprMeta serialization)	serializer-only
tests (Lean, 2,619 lines)	Tests/Ix/Sharing{Exact,Uniform,Tiered}.lean (suite exact-sharing), Tests/Ix/SharingExactFFI.lean	fixtures with exact bytes, oracles, tiered at scale and under each limit, pointer-layout independence, limit grammar
IxVM	Ix/IxVM/{IxonDeserialize,IxonSerialize}.lean, Ix/IxVM/Kernel/*, Ix/Aggr/Circuit.lean, crates/ixvm-codegen/src/{aiur_ixvm,aiur_ix_aggr}.rs (generated); tests Tests/Ix/IxVM/TagN.lean, Tests/Ix/IxonV4VM.lean, Tests/Ix/IxVM.lean	see the IxVM section
fixtures	Tests/Fixtures/ixon-v4/, crates/common/src/prim_addrs.rs, Ix/Tc/Primitive.lean, pins in Tests/Ix/Claim.lean, crates/ixon/src/proof.rs, crates/compile/src/graph.rs	regenerated by their producers, never edited by hand
docs	docs/Ixon.md (TagN, Sharing System, version), docs/Ixon-v4.md, docs/ix_canonicity.md §6.7, docs/sharing-minimum.md §12–§13 (decision record), docs/sharing-minimum-integration.md (map of the code), docs/sharing-minimum-measurements*.md, docs/sharing-minimum-performance.md, docs/sharing-minimum-arena.md	the measurement docs are the evidence behind every number here
benchmarks	Benchmarks/SharingStudy.lean (sharing-study), Benchmarks/LeanSharingProf.lean (lean-sharing-prof), Benchmarks/UniformHard.lean (uniform-hard), crates/ixon/examples/sharing_corpus.rs (--full-check, --sharing-limits)	measurement tools; the cargo feature ixon/sharing-profile adds phase timers

How to check locally:

• lake build IxCompileVerify IxTcVerify;
• lake test -- exact-sharing exact-sharing-ffi ixon ixvm-tagn;
• lake exe ixon-v4-primitives && lake exe ixon-v4-tests --primitives;
• cargo test -p ixon;
• with IX_SHARING_CORPUS=<init.ixe> (compiled at the same commit), lake test -- exact-sharing-ffi runs the corpus differential;
• cargo run --release -p ixon --example sharing_corpus -- <init.ixe> --full-check runs the Rust
  checked mode over a corpus.

Open items for the owner (follow-ups, not in this PR)

• (a) Reader hardening against malformed input (pre-existing on main): allocation bombs from
  decoded counts passed to Vec::with_capacity; cyclic sharing tables, metadata or call-site
  references that make the decompilers and kernel ingress loop; a universe decompression bomb.
  Details in plans/followup-hardening.md; recommended as a dedicated PR.
• (b) Lean compile driver. Speculative scheduling of blocks ahead of their wave (branch
  ix-sharing-w5) cut the Lean step of the merge-queue partition from 623.8 s to 386.5 s at an
  older construction commit. It is a general driver change with an empirical output-identity
  argument and is kept out of this PR.
• (c) Lean construction within 2–4× of Rust. Needs a cost model in the specification that
  evaluates a component's area, and the corresponding re-proofs.
• (d) 128-bit phase-1 lengths in Rust. Arbitrary-precision lengths, or a bound agreed in both
  languages, would remove the documented divergence.
• (e) Artifacts that need other machines. Benchmarks/Kernel/AnthropicFLT/cases.json pins
  the 30 GB v3 artifact flt-after-source-hints-1.ixe by sha256 and must be re-derived from it
  recompiled at v4 (until then the harness rejects the old artifact by hash, and a v4 binary
  rejects its header). Under the fixture policy a new dated aggregate fixture
  Tests/Fixtures/Aggregate/mathlib-YYYY-MM-DD/ needs the large machine (64 vCPU, about 495 GiB);
  the historical mathlib-2026-09-03 stays and its test now requires rejection with "claim:
  unsupported object format". Both can wait.
• (f) ExprMeta arena hash-consing, the stacked PR designed in docs/sharing-minimum-arena.md.
• IxVM. Function regrouping and the put_tagn_tail lookup micro-optimization are left to the
  optimization pass of the circuits during review.

[arthurpaulino]

!benchmark fresh

[github-actions]

!benchmark — main vs 22afee6

backends: aiur=prove · envs: InitStd · machine: r8i.8xlarge · baseline: fresh (benchmark products rebuilt, base-SHA run, bencher bypassed)

aiur · InitStd · prove — main from: base run @ b4fea97 (fresh — bencher bypassed)

8 workloads · 5 with regressions · 7 with improvements (|Δ| > 3.0% on any metric).

IxVM on FRI (7 constants)

constant	execute-time (main)	execute-time (PR)	Δ%	prove-time (main)	prove-time (PR)	Δ%	throughput (const/s) (main)	throughput (const/s) (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	proof-size (main)	proof-size (PR)	Δ%	verify-time (main)	verify-time (PR)	Δ%	fft-cost (main)	fft-cost (PR)	Δ%	trace-shards (main)	trace-shards (PR)	Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append	8.876 s	8.021 s	-9.6% (1.11× faster) 🟢	56.246 s	53.874 s	-4.2% 🟢	49.340	51.510	+4.4% 🟢	73.35 GiB	70.77 GiB	-3.5% 🟢	5.01 MiB	4.98 MiB	-0.7%	33.2 ms	30.8 ms	-7.2% (1.08× faster) 🟢	135.66B	122.12B	-10.0% (1.11× fewer) 🟢	1	1	+0.0%
Array.extract_append	6.522 s	5.863 s	-10.1% (1.11× faster) 🟢	41.181 s	38.959 s	-5.4% (1.06× faster) 🟢	39	41.220	+5.7% (1.06× faster) 🟢	53.97 GiB	51.17 GiB	-5.2% (1.05× smaller) 🟢	4.89 MiB	4.83 MiB	-1.3%	29.6 ms	30.8 ms	+4.1% ⚠️	97.92B	89.40B	-8.7% (1.10× fewer) 🟢	1	1	+0.0%
Char.ofOrdinal_le_of_le	6.420 s	5.749 s	-10.5% (1.12× faster) 🟢	45.273 s	36.638 s	-19.1% (1.24× faster) 🟢	61.030	75.410	+23.6% (1.24× faster) 🟢	62.27 GiB	51.19 GiB	-17.8% (1.22× smaller) 🟢	5.01 MiB	4.94 MiB	-1.3%	29.8 ms	30.9 ms	+3.9% ⚠️	97.27B	87.86B	-9.7% (1.11× fewer) 🟢	1	1	+0.0%
Std.HashMap	4.026 s	3.720 s	-7.6% (1.08× faster) 🟢	25.803 s	24.808 s	-3.9% 🟢	79.140	82.310	+4.0% 🟢	36.91 GiB	35.09 GiB	-4.9% (1.05× smaller) 🟢	4.94 MiB	4.88 MiB	-1.1%	30.2 ms	33.8 ms	+11.9% (1.12× slower) ⚠️	62.29B	56.20B	-9.8% (1.11× fewer) 🟢	1	1	+0.0%
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq	3.709 s	3.470 s	-6.4% (1.07× faster) 🟢	24.456 s	23.824 s	-2.6%	76.340	78.370	+2.7%	35.41 GiB	33.92 GiB	-4.2% 🟢	4.91 MiB	4.84 MiB	-1.6%	34.6 ms	31.6 ms	-8.6% (1.09× faster) 🟢	56.81B	51.60B	-9.2% (1.10× fewer) 🟢	1	1	+0.0%
String.append	740.8 ms	721.8 ms	-2.6%	2.496 s	2.441 s	-2.2%	131.020	133.970	+2.3%	5.08 GiB	4.81 GiB	-5.4% (1.06× smaller) 🟢	4.65 MiB	4.58 MiB	-1.4%	26.8 ms	27.9 ms	+4.1% ⚠️	3.49B	3.27B	-6.3% (1.07× fewer) 🟢	1	1	+0.0%
Nat.add_comm	532.0 ms	502.6 ms	-5.5% (1.06× faster) 🟢	1.071 s	1.085 s	+1.3%	42.960	42.410	-1.3%	4.56 GiB	4.55 GiB	-0.2%	4.47 MiB	4.39 MiB	-1.8%	24.7 ms	24.7 ms	+0.1%	306.71M	295.31M	-3.7% 🟢	1	1	+0.0%

FRI verifier on FRI (7 constants)

constant	execute-time (main)	execute-time (PR)	Δ%	prove-time (main)	prove-time (PR)	Δ%	throughput (const/s) (main)	throughput (const/s) (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	proof-size (main)	proof-size (PR)	Δ%	verify-time (main)	verify-time (PR)	Δ%	fft-cost (main)	fft-cost (PR)	Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append	3.072 s	3.002 s	-2.3%	34.687 s	33.704 s	-2.8%	80	82.340	+2.9%	53.77 GiB	52.27 GiB	-2.8%	2.67 MiB	2.67 MiB	-0.1%	17.1 ms	15.6 ms	-8.3% (1.09× faster) 🟢	94.15B	93.61B	-0.6%
Array.extract_append	3.089 s	2.945 s	-4.7% 🟢	33.636 s	33.286 s	-1.0%	47.750	48.250	+1.0%	51.33 GiB	50.39 GiB	-1.8%	2.67 MiB	2.67 MiB	+0.1%	15.3 ms	15.8 ms	+3.2% ⚠️	92.62B	90.10B	-2.7%
Char.ofOrdinal_le_of_le	3.027 s	3.040 s	+0.5%	33.764 s	33.634 s	-0.4%	81.830	82.150	+0.4%	52.00 GiB	51.69 GiB	-0.6%	2.67 MiB	2.67 MiB	+0.0%	15.5 ms	16.4 ms	+5.7% (1.06× slower) ⚠️	93.40B	92.21B	-1.3%
Std.HashMap	3.135 s	3.091 s	-1.4%	33.772 s	33.518 s	-0.8%	60.460	60.920	+0.8%	51.54 GiB	50.57 GiB	-1.9%	2.67 MiB	2.67 MiB	-0.1%	15.5 ms	17.7 ms	+14.1% (1.14× slower) ⚠️	92.66B	90.72B	-2.1%
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq	3.045 s	2.990 s	-1.8%	33.627 s	32.718 s	-2.7%	55.520	57.060	+2.8%	50.96 GiB	49.56 GiB	-2.8%	2.67 MiB	2.67 MiB	+0.1%	15.6 ms	16.4 ms	+5.3% (1.05× slower) ⚠️	92.06B	90.03B	-2.2%
String.append	2.814 s	2.755 s	-2.1%	31.856 s	31.814 s	-0.1%	10.260	10.280	+0.2%	46.94 GiB	47.25 GiB	+0.6%	2.67 MiB	2.67 MiB	-0.1%	15.4 ms	16.0 ms	+3.6% ⚠️	83.91B	83.58B	-0.4%
Nat.add_comm	2.779 s	2.579 s	-7.2% (1.08× faster) 🟢	31.531 s	30.458 s	-3.4% 🟢	1.460	1.510	+3.4% 🟢	46.08 GiB	44.80 GiB	-2.8%	2.67 MiB	2.67 MiB	-0.2%	16.5 ms	16.1 ms	-2.3%	78.77B	75.14B	-4.6% 🟢

Aggregate flat join (1 pair)

pair	execute-time (main)	execute-time (PR)	Δ%	prove-time (main)	prove-time (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	proof-size (main)	proof-size (PR)	Δ%	verify-time (main)	verify-time (PR)	Δ%	fft-cost (main)	fft-cost (PR)	Δ%
Nat.add_comm + String.append	3.714 s	3.604 s	-3.0%	37.151 s	36.963 s	-0.5%	54.98 GiB	55.12 GiB	+0.3%	2.83 MiB	2.83 MiB	-0.1%	17.1 ms	16.7 ms	-2.5%	108.96B	108.61B	-0.3%

Pipeline total (7 constants)

constant	total-time (main)	total-time (PR)	Δ%	pipeline-throughput (const/s) (main)	pipeline-throughput (const/s) (PR)	Δ%	pipeline-peak-ram (main)	pipeline-peak-ram (PR)	Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append	1m 30.9s	1m 27.6s	-3.7% 🟢	30.520	31.690	+3.8% 🟢	73.35 GiB	70.77 GiB	-3.5% 🟢
Array.extract_append	1m 14.8s	1m 12.2s	-3.4% 🟢	21.470	22.230	+3.5% 🟢	53.97 GiB	51.17 GiB	-5.2% (1.05× smaller) 🟢
Char.ofOrdinal_le_of_le	1m 19.0s	1m 10.3s	-11.1% (1.12× faster) 🟢	34.960	39.320	+12.5% (1.12× faster) 🟢	62.27 GiB	51.69 GiB	-17.0% (1.20× smaller) 🟢
Std.HashMap	59.575 s	58.326 s	-2.1%	34.280	35.010	+2.1%	51.54 GiB	50.57 GiB	-1.9%
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq	58.083 s	56.542 s	-2.7%	32.140	33.020	+2.7%	50.96 GiB	49.56 GiB	-2.8%
String.append	34.352 s	34.255 s	-0.3%	9.520	9.550	+0.3%	46.94 GiB	47.25 GiB	+0.6%
Nat.add_comm	32.602 s	31.542 s	-3.3% 🟢	1.410	1.460	+3.5% 🟢	46.08 GiB	44.80 GiB	-2.8%

• Base hardware (base run @ b4fea97 (fresh — bencher bypassed)): CPU: Intel(R) Xeon(R) 6975P-C · vCPUs: 32 · RAM: 247.7 GiB
• PR hardware: CPU: Intel(R) Xeon(R) 6975P-C · vCPUs: 32 · RAM: 247.7 GiB

Workflow logs