IxVM: reference-faithful def-eq and whnf, environment-machine reduction, and Init+Std/mathlib-scale checking by arthurpaulino · Pull Request #543 · argumentcomputer/ix

arthurpaulino · 2026-08-07T20:24:46Z

This branch takes the IxVM Aiur kernel from diverging on Init+Std- and
mathlib-scale environments to checking them: 33/36 Init+Std shards green
under a 3-minute cap (from 29 at the branch point, with the remaining 3
root-caused and documented), every reported mathlib CategoryTheory/
FiniteInter/generatePiSystem/Rat.instEncodable-class constant
passing, and the heaviest known mathlib proof obligation
(Algebra.kerTensorProductMapIdToAlgHomEquiv._proof_1) checking in
~2m15s at 1.48e12 FFT — 21% below its previous cost.

Kernel changes

Def-eq restructured around the reference's lazy-delta discipline.
Proof irrelevance runs on no-delta whnf forms strictly before any delta
unfolding; delta happens only inside a hint-ranked lazy loop (one
definition at a time, no-delta renormalization per step, same-head spine
probes under the reference's H2 gate, Nat-offset handling at the loop
top); the post-loop fallback mirrors the reference's break path exactly
(4c full-projection escape with restart, 4d spine-wise app congruence,
then the tier-5 tail: lam-eta, string-literal retry, struct-eta,
unit-like, proof irrelevance, terminal structural compare). Spine-wise
same-head comparison (tier 4d) runs before binary structural descent —
attribution showed the per-App-layer descent was the dominant pair
generator on mathlib workloads.

Struct-eta only when lazy delta cannot step. The pre-loop unit-like/
struct-eta tiers now fire only when neither side has a Defn/Thm head or
a projection-unfoldable head — i.e. only when the loop would break
immediately, where they are exactly the tier-5 fallback minus a no-op
loop pass. Firing eta on a pair delta could still process descends into
field pairs that pit a projection against a value and force one-sided
grinding to constructor form; on UInt8.ofBitVec_not (whose ofBitVec
head is the UInt8 constructor, so eta's gate passes immediately) that
descent unfolded BitVec.not on a symbolic argument into
ofFin ⟨Nat.xor …, proof⟩ and from there into unbounded
Nat.le.rec/Nat.le.below.rec towers behind the bound proofs.

Theorems delta-unfold in the full reducer. The reference unfolds
Definition | Theorem alike; a kernel whose full whnf keeps Thm heads
stuck cannot fire iota on theorem-headed majors and false-rejects the
Rat.instEncodable._proof_1 shape (And.rec over an
abstractNestedProofs-generated auto-theorem). The no-delta stepping
layers keep theorems stuck, as the reference's do.

Environment-machine whnf. Beta/zeta cascades evaluate through a
Krivine-style closure machine (O(1) environment pushes instead of eager
substitution per redex), with mode-selected exits preserving the
no-delta semantics def-eq depends on, machine-native delta for full-mode
definition and theorem chains, and closure-iota with mode-correct major
reduction. K-like recursor synthesis gates on the raw major before any
major whnf (mirroring the reference's synth_ctor_when_k placement) —
critical once theorems unfold, since whnf of a decide-style Eq.rec
major would otherwise evaluate the whole decision procedure.

Recursor reconstruction whnf-discipline. The canonical recursor
rebuild whnfs while peeling motive telescopes and collecting index
domains, so inductives whose declared types hide binders behind
definitional wrappers (abbrev) reconstruct correctly — the
CategoryTheory.MorphismProperty.limitsOfShape.rec failure shape.
Constructor gates, arity guards, and field-universe checks got the same
whnf discipline in an audited pass (six-agent audit: no soundness
findings; the audit's structural suggestions are applied where they
measured neutral-or-better).

Sharding

ix shard <env.ixe> --shards N now partitions directly from the
environment — byte-weight vertices and static-reference nets, no
ix profile pass required. Measured against profiled sharding: 1.69x
vs 1.67x ingress imbalance on mathlib at 512 shards. An ingress-bytes
balance metric supports the Aiur backend's cost model.

Tests and pins

Every fixed failure shape is pinned by a minimal fixture whose comment
explains the shape and the tier that guards it: HiddenIdx
(wrapper-hidden index binder), FnField (abbrev-wrapped recursive
field), thmMajorUse (theorem-headed iota major), BvBox/bvBoxNot
(structure ctor vs Complement-projection chain over a symbolic BitVec —
within 0.05% of the real UInt8.ofBitVec_not workload, which is also
pinned directly). The FFT pin table is an exact-equality regression
gate: any cost shift fails the suite and forces an explicit re-pin.

Validation

Full ixvm suite green at the tip: all fixtures, 73 FFT pins,
codegen↔bytecode parity, shard-pipeline pin.
Default lake test primary suites green; cargo test --release -p ix-kernel shard tests 22/22.
34/34 mathlib target constants pass against a freshly compiled
mathlib.ixe (37s total for the batch).
Init+Std 36-shard sweep: 33/36 under a 3-minute per-shard cap.

Notes for reviewers

FFT pins are only valid at the tip. The branch was rebased past
the FFT cost-model grounding that merged to main with conflicting pin
resolutions; per-commit pin conflicts were resolved as the branch side
and the final commit regenerates the kernel and re-harvests every pin
from a green suite run. Gate CI on the tip or squash-merge; a
per-commit bisect will trip on pins mid-branch.
Known limitation (not a regression): Std shards 20/24/32 exceed
the check cap on the Std.Tactic.BVDecide.BVExpr.bitblast equation-
lemma class. These never passed on this branch's ancestry. Root cause
is profiled and documented: the def-eq memo fragments on binder
contexts that embed terms at many unfolding stages (the reference's
fvar-based binder opening keys those obligations context-free), and
the fix is a follow-up campaign.

…tion Checking CategoryTheory.MorphismProperty.limitsOfShape.rec (mathlib) aborted with `no match case for value 3`: a flat-block member's index binders hide behind a definitional wrapper, so after peeling the params the type is structurally an App (KExprNode tag 3), and collect_index_doms only matched Forall. The reference kernel (crates/kernel/src/inductive.rs) whnfs before every peel step of these telescopes and breaks tolerantly on a non-Forall; the DSL mirrors peeled structurally and either aborted or silently stopped short. Bring all six divergent sites in the canonical reconstruction in line with the reference (structural-first, whnf fallback, tolerant stop): - peel_motive_params_subst, collect_index_doms (motive types; the observed abort) - peel_ctor_params_subst (whnf fallback existed, but its non-Forall arm aborted instead of breaking) - walk_fields_classify (field walk stopped at the first wrapped binder, losing fields and induction hypotheses) - build_rule_rhs's counting pass (new peel_n_foralls_whnf_tol + count_foralls_whnf; the old structural peel_n_foralls aborted on a wrapped ctor param) - peel_leading_foralls_acc (IH xs-walk, mirrors build_direct_ih) The tolerant stops only move failures from abort to reject: a short telescope yields a reconstruction that differs from the declared type, so the existing def-eq / compare_rules asserts fire with an accurate message. Intolerant peels over the recursor's DECLARED type are unchanged — those reject adversarial arity, and kernel-generated recursor types are literal foralls. Tests: minimal fixture IxVMInd.HiddenIdx — an inductive whose result type is an abbrev wrapper (`PredOver α := α → Prop`), the smallest shape whose index binder only appears after whnf. Fails pre-fix with the original signature, pinned passing post-fix. The elaborator only accepts the wrapper as a reducible def and stores it un-unfolded, which is why core-only envs never hit this. FFT pins re-harvested (+0.001-0.1%, concentrated in the rec circuits); shard-pipeline pin bumped to match. Codegen kernel regenerated.

Checking mathlib's Algebra.kerTensorProductMapIdToAlgHomEquiv._proof_1 (140 KB proof term, rank 1229/631006 by reference cost) ran the IxVM into an unbounded memo flood: >11 min native and 97.8 GiB of QueryMap growth without terminating, with 85% of CPU inside the memo table. Root cause: k_is_def_eq_slow2 fully delta-whnf'd both sides BEFORE proof irrelevance, normalizing entire proof/instance towers that the reference discharges with two infers — its slow path runs proof irrelevance strictly before any delta and unfolds only through the hint-guided lazy loop, one definition at a time. Restructure, each piece mirroring crates/kernel/src/def_eq.rs+whnf.rs: - proof irrelevance runs on the whnf_nd forms, before any delta ("Tier 3: proof irrelevance (before delta)"). - lazy_delta_loop is the ONLY delta engine inside def-eq: hint-ranked single-step unfolds, whnf_nd renormalization between steps (never full whnf), fuel 10_000 (MAX_WHNF_FUEL), Nat-offset check at loop top, returns its final forms so the trailing tiers compare the partially-unfolded pair the way the reference's loop break does. - same-head spine probes only under H2: equal ranks + same addr + Regular hint; a miss feeds forward into unfold-both. The pre-whnf and pre-loop app-congruence probes are gone (the reference's quick tier handles only Sort/Lam/Forall); each probe miss cost a full recursive arg tree at every unfold height. - Tier 1b eager Bool: `decide P = Bool.true` obligations full-whnf the closed side — the single sanctioned full whnf on a def-eq term. - Tier 4c escape: whnf_ndfp, a no-delta core pass with the FULL projection policy (scrutinees get full whnf, heads stay stuck); on any progress the whole def-eq restarts on the reduced forms. - The no-delta layer's Rec arm now runs the same iota fallbacks as the full reducer — K-synth (Eq/HEq transports over proof-typed majors) and struct-eta iota — since the reference's DEF_EQ_CORE flags keep cheap_rec FALSE. Without this a cast never strips off a no-delta form and `x = Eq.rec ... x ...` false-rejects. try_k_synth_iota now returns a verdict + raw reduct so each layer picks its own renormalization. Validated: the constant typechecks natively in 4m43s (FFT 1.98e12, 61.7% cache-saved); ixvm suite fully green with re-harvested pins (mean +0.47%, median +0.17%, worst +2.31% on Vector.append; shard pipeline pin +7.0%) — the small Init-scale tax for removing the unbounded mathlib blowup class. Parity, arena, and exploit gates all pass, so the tier restructure holds against the negative corpus. Known remaining gap, deliberate: per-constant cost is still ~500x the reference — circuit heights show a uniform ~10^2-10^3x query multiplier rooted in eager per-binder substitution (expr_inst1: 60.7M queries vs the reference's 370k subst nodes), where the reference's beta enters an environment machine and materializes nothing until exit. That port is next. Also: route the IX_PERF_COUNTERS summary dump to stderr — the FFI hosts install no `log` backend, so the previous log::info! went nowhere.

On the Aiur STARK backend, measured shard prove time tracks the shard's byte load, not its op counts: a 72-shard Init prove sweep fit wall time at R^2 0.75 against owned serialized bytes and 0.02 against heartbeats, with peak RSS a near-perfect linear function of prove time (R^2 0.996). The partitioner balanced heartbeats, producing a 3.3x spread in actual prove times. Add BalanceMetric to the partitioner: `steps` (existing Zisk step-cost model, default) or `ingress` (serialized bytes). The cut objective is unchanged — cross-shard ingress bytes — so `ingress` balances what a shard always pays (own bytes: loaded and blake3-verified) while the min-cut keeps the frontier term small. The report gains an ingress_load line (0.75·own + 0.15·frontier bytes, weights from the same regression) so the achieved balance is visible in the metric that predicts prove time. Wired through rs_shard_esp and `ix shard --balance-metric`; the budget path keeps the step model (its RAM cap is inherently step-based). On the 512-shard mathlib partition this brings ingress-load imbalance to 1.67x (heartbeat imbalance 10.95x, deliberately unconstrained).

Call-site attribution on the mathlib monster (per-call-site wrapper circuits over k_is_def_eq) showed 2.06M of 2.72M def-eq calls coming from k_is_def_eq_struct_go's binary App/Lam/Forall decomposition: a pair that breaks out of the lazy-delta loop with same-head STUCK spines (Rec/ctor/non-Regular heads, which H2's gate rightly excludes from in-loop probing) decomposed one full-cascade pair per App LAYER. Mirror the reference's tier 4d (def_eq.rs, lean4lean isDefEqApp): after the Tier-4c no-progress check, try the SPINE-WISE same-head comparison (try_def_eq_app) before eta-swap and the binary structural tiers — one pair per argument instead of one per layer. On the monster this cuts def-eq calls 2.72M -> 2.43M and total FFT 1.976e12 -> 1.896e12 (-4.1%, 4m39s); the suite pin table moves net DOWN (28 down, 18 up), shard pipeline pin -0.2%. Documented deviation kept: unit-like + struct-eta stay PRE-loop in slow2, where the reference runs them only in the tier-5 fallback. Removing them (to mirror exactly) stalled the suite's first kernel check for minutes: this kernel's instance-heavy fixtures rely on those tiers deciding pairs that otherwise take the loop's unfold-both path. Their pre-loop cost on the monster is ~neutral (+0.3%). Pins re-harvested; all parity/arena/exploit gates green.

wrapper inlining, invariant docs Six-agent audit of the last four kernel commits found no soundness bugs; this lands its high- and medium-priority fixes. Parity/completeness: - The three structural ctor gates now whnf per step with the binder context, mirroring the reference (inductive.rs): the return-type gate whnf-peels the full params+fields telescope (intolerant, the reference's "not enough binders"; the return type itself stays un-whnf'd per the reference's "do NOT whnf here"), param agreement whnfs both sides, field universes whnfs with tolerant breaks. These gates run before the canonical reconstruction, so the ctor-side whnf fallbacks landed earlier were unreachable behind them. (A ctor whose whole declared type hides behind an abbrev is rejected by Lean's own kernel, so the intolerant arms only ever fire on adversarial wire input — the correct verdict.) - Level-arity gate on both Rec dispatch arms covering all three iota paths (plain, K-synth, struct-eta): the reference checks rec_us.len() != recr.lvls before instantiating rule RHSes; a mismatched application now stays stuck instead of reaching expr_inst_levels. - is_bool_true_const requires an EMPTY level list (the reference's us.is_empty() gate), keeping Tier 1b independent of infer's arity assert. Cost (trivial pass-through fns waste a circuit plus a lookup per row — inlined): dead peel_n_lams_tol removed; k_is_def_eq_ordered and the k_is_def_eq_struct alias collapsed; k_is_def_eq_slow merged into slow_nd (same argument tuple, zero memo differentiation); whnf_core/whnf_nd_core inlined into their entries. Net on the mathlib monster: 1.896e12 -> 1.876e12 FFT (-1.0%) with the gates' whnf steps included. Measured deviation kept and documented: whnf_ndfp's stuck-projection rebuild keeps the WHNF'D scrutinee. The reference returns the term unchanged there; the raw-rebuild mirror was tried and measured +9.6% FFT on the monster (whnf_ndfp_proj_head 3x, whnf_nd family +30%) — under Aiur memoization, materialize-once-and-restart shares the reduced scrutinee across every downstream pair, where the raw form makes each comparison context re-reduce it. Docs: the six tolerant-stop comments now state the real soundness invariant — the stops are unreachable on accepting runs because the telescopes are pinned by the shape gates (check_ctor_return_type, get_result_sort_level) plus compare_rules' field-count assert; the previous "a short reconstruction fails the def-eq" argument was wrong against an adversary who declares the short form. The DefEq module-doc tier ladder, the slow-path comment, and the delta-engine comments now describe the post-restructure architecture (including try_lazy_delta_app's fuel-exhaustion-only residual reachability). Tests: IxVMInd.FnField — a recursive field whose function type hides behind an abbrev; exercises the previously-untested whnf fallback in the IH xs-walk (peel_leading_foralls_acc). Pins re-harvested (70), shard pipeline pin -0.04%; all parity/arena/exploit gates green.

… batch 2 Profile-free sharding: `ix shard <env.ixe> --shards N` now partitions an env directly — profile_from_env_static builds a synthetic BlockProfile from the env's static structure (vertex weight = serialized byte length, nets = the static reference graph, blob refs excluded; heartbeats stay zero) and shard_env_static runs the same partitioner/manifest path over it. No `ix profile` kernel run. For the Aiur backend the static graph is arguably the MORE faithful ingress model: the lazy kernel also loads type-lookup refs that never appear in the dynamic delta-unfold graph. Only the ingress metric is meaningful on the synthetic profile; the CLI defaults to it for .ixe inputs and rejects an explicit `steps`. Validated on mathlib: 647,127 blocks / 18.1M static-ref edges -> 512 non-empty shards at ingress-load imbalance 1.69x, vs 1.67x for the profiled partition — parity, minus a 2.5-minute profiling step. shard_esp's core is extracted (shard_profile_core) and shared by both inputs. Def-eq: post-loop string-literal retry tier (mirror def_eq.rs tier 5) — a side can become a Lit(Str) only through the loop's Thm/Defn unfolding, after the entry tier ran on the raw forms. FFT-neutral on the mathlib monster (1.876e12 unchanged); pins re-harvested. Audit batch 2 (from the six-agent review): - `--shards 0` no longer panics across the FFI: clamped in the CLI and guarded at the ABI (ShardManifest::build indexed an empty members vec and unwound through extern "C"). - The "balance floored by largest atomic block" note is computed in the BALANCED metric's unit (bytes under ingress), so it no longer fires or stays silent against the wrong quantity. - Stale heartbeat-era docs in shard.rs (module hypergraph doc, cap comments) updated for metric-generic weights.

Rat.instEncodable false-rejected ("inferred type is not def-eq to the expected type"): its value eliminates an And proof whose major is the auto-abstracted THEOREM Rat.instEncodable._proof_1, and the kernel's full whnf kept Thm heads stuck — so `And.rec p q motive minor _proof_1` could never fire its iota (And is a Prop, so the struct-eta fallback rightly refuses), and def-eq died on `x ≟ And.rec …` pairs no tier can decide. The module doc claimed Thm-stuck as a mirror; the reference's delta phase (delta_unfold_one, whnf.rs) actually matches `DefKind::Definition | DefKind::Theorem` alike. Fix: the FULL reducer's Const dispatch unfolds Thm exactly like Defn. The no-delta layer (whnf_nd — everything def-eq steps with) keeps Defn AND Thm stuck as before, so the lazy-delta discipline and proof irrelevance's first shot at Thm-headed pairs are unchanged. Reproducer, pinned as IxVMInd.thmMajorUse: the And proof is written INLINE (the elaborator's Meta def-eq treats theorems as opaque, so no source-level rfl can state the equality — Meta sees And.intro and accepts), and abstractNestedProofs then pulls it out as the ._proof_1 auto-theorem, exactly how Rat.instEncodable._proof_1 was born; the kernel alone faces `1 ≟ And.rec … ._proof_1`. Verified failing pre-fix with the exact mathlib signature, passing post-fix. Validation: all 12 reported mathlib constants now pass (the 11 wrapper-index recursors already did — that class was closed by the whnf-peel work; Rat.instEncodable was the holdout). The mathlib def-eq monster IMPROVED: 4m32s/1.876e12 -> 2m50s/1.869e12, since proof towers now discharge through iota instead of grinding the def-eq ladder. Pin table: only nat_pow_big shifted (+1 entry), everything else byte-identical; suite fully green.

Std.Time shard checks stalled without bound (7 of 36 Init+Std shards past 3 minutes; Std.Time.Nanosecond.Offset.ofDays._proof_1 alone ran >10 min at 63 GiB). Two independent causes, both fixed here: 1. K-synth ordering (the trigger). ofDays is `UnitVal.cast` — an Eq.rec over a `decide +kernel` proof. The reference runs synth_ctor_when_k PRE-whnf of the major (whnf.rs:1350); our try_iota whnf'd the major first, with K-synth only as the stuck fallback. Thm-stuck used to make that whnf a no-op, so the fallback fired; once theorems delta-unfold (the Rat.instEncodable fix), the major-whnf forces of_decide_eq_true's body — i.e. EVALUATES the entire Rat decision procedure over 14-digit literals — before the K gate ever runs. Now k_flag=1 recursors try the synth gate on the RAW major first (one type inference + an index def-eq; no decide evaluation), falling to the major-whnf path only on a gate miss. Applied to both plain Rec arms and the machine's closure-iota keeps its K-miss-to-plain-path routing. 2. Environment-machine whnf (the port, from ap/ixvm-machine/de42a61, re-composed onto the current kernel). Eager per-beta substitution made the surviving reduction quadratic — perf showed 85% of CPU in the memo table under an expr_inst_many tower. The machine makes beta/zeta O(1) environment pushes with substitution only at exit readbacks: Clo/clo_subst (Subst), mwhnf_spine with mode-selected exits (0=full, 1=whnf_nd, 2=whnf_ndfp — each layer's no-delta semantics preserved at the exits), lazy closure-iota (try_iota_c, with the ctor-parent identity assert and the level-arity gate), machine-native delta for mode-0 Defn heads (prim/proj-def gated) and — new versus the parked branch — for mode-0 THM heads, so the theorem unfolds ride the closure spine instead of forcing a full readback per delta step. Measured: ofDays 1m48s / 5.49e10 (was unbounded); Rat.instEncodable and IxVMInd.thmMajorUse stay green; the mathlib def-eq monster is wall-flat (2m53s vs 2m50s) at +10% FFT (2.06e12 vs 1.87e12) — the machine's closure overhead on def-eq-heavy work, accepted for the liveness class it buys. Suite fully green; pins re-harvested (64 up, 6 down; shard pipeline +1.2%).

…irrors the reference tier order Checking UInt8.ofBitVec_not (and its Std shard class) never terminated: try_eta_struct fired on pairs the lazy-delta loop could still process — pre-loop, and post-loop BEFORE the 4c projection escape. On `UInt8.ofBitVec (~~~b) ≟ ~~~(UInt8.ofBitVec b)` (ofBitVec IS the UInt8 ctor, so eta's gate passes immediately) the field descent pits `Prj(UInt8, 0, ~~~x)` against a value, grinding BitVec.not on a symbolic argument into `ofFin ⟨Nat.xor …, proof⟩` and from there into unbounded Nat.le.rec/Nat.le.below.rec towers behind the bound proofs. The reference never fires struct-eta here: its ladder unfolds both sides in lock-step and closes via H2/app-congruence + proj-iota (6 def-eq pairs, 49 whnf_core calls total). Two changes: - slow2 pre-loop unit-like/struct-eta gated on lazy_can_step: they run only when NEITHER side has a Defn/Thm head or a proj-unfoldable head — i.e. when the loop would break immediately and the pre-loop tiers are exactly the tier-5 fallback minus a no-op loop pass. Keeps the measured instance-fixture win; steppable pairs take the loop like the reference. - k_def_eq_post_loop reordered to the reference break path (def_eq.rs:539-590 + is_def_eq_whnf): 4c ndfp escape + restart, 4d spine compare, then lam-eta, string-lit, struct-eta, unit-like, proof irrelevance, structural. UInt8.ofBitVec_not: unbounded → 9.1e9 FFT (seconds). Mathlib monster (Algebra.kerTensorProductMapIdToAlgHomEquiv._proof_1): 1.88e12 → 1.48e12 (-21%). Std shards 17/33 unblocked (20/24/32 remain on the separate bitblast.goCache class). Every kernel FFT pin shifted slightly down; re-pinned. New pins: bvBoxNot (minimal reproducer fixture: structure ctor vs Complement-projection chain over a symbolic BitVec) and UInt8.ofBitVec_not itself.

The branch was rebased onto main past the merged FFT cost-model grounding (the branch-local copy of that commit was dropped; main's merge resolution supersedes it). Pin conflicts during the replay were deliberately taken as the branch side per commit — intermediate commits therefore carry stale pin values — and this commit is the single point of truth: aiur_ixvm.rs regenerated from the rebased sources, and every kernelCheckEntries pin plus the shard-pipeline pin re-harvested from a green suite run on the rebased tree.

arthurpaulino added 10 commits August 7, 2026 19:50

Navigation Menu

Uh oh!

IxVM: reference-faithful def-eq and whnf, environment-machine reduction, and Init+Std/mathlib-scale checking - #543

IxVM: reference-faithful def-eq and whnf, environment-machine reduction, and Init+Std/mathlib-scale checking#543
arthurpaulino wants to merge 10 commits into
mainfrom
ap/ixvm

arthurpaulino commented Aug 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

arthurpaulino commented Aug 7, 2026

Kernel changes

Sharding

Tests and pins

Validation

Notes for reviewers

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant