IxVM kernel: canonical level normalization + FFT-cost pinning - #447

Merged
arthurpaulino merged 2 commits into
mainfrom
ap/level-leq-normalize
Jun 17, 2026
Merged

IxVM kernel: canonical level normalization + FFT-cost pinning#447
arthurpaulino merged 2 commits into
mainfrom
ap/level-leq-normalize

Conversation

@arthurpaulino

@arthurpaulinoarthurpaulino commented Jun 17, 2026•
edited
Loading

Copy link
Copy Markdown
Member

Summary

Two commits on level-normalization:

  1. IxVM: canonical level normalization for level_equal /
    level_leq.     Replaces the recursive Level.leq mirror (two-way
    param-substitution split per Max / IMax — exponential in unresolved
    universe params) with a port of Rust's Géran canonical-form machinery
    from src/ix/kernel/level.rs::normalize_level / norm_level_eq /
    norm_level_le. level_equal and level_leq now normalize-and-compare;
    the substitution helpers (level_subst_reduce, level_has_param,
    level_any_param) are deleted.

  2. Tests: pin FFT cost per kernel-check target. Adds
    expectedFftCost : Option Nat to AiurTestCase; runTestCase asserts
    the rounded Aiur.computeStats.totalFftCost matches exactly. Pins all
    41 entries in Tests/Ix/IxVM.lean::kernelCheckEntries.

Motivation

The recursive Level.leq split was exponential in the number of params and
each branch materialized freshly substituted levels. On
_private.…SInt.0.Int16.instRxcHasSize_eq the level family was 93% of the
record at 2^31 ops (level_subst_reduce 60.8M + level_leq 53.2M +
level_max 30.4M entries…), entered through Inductive's ctor-field
universe constraint (level_leq), not def-eq's level_equal.

The same algorithmic gap blocks several stdlib targets in the in-tree
ixvm test suite. Beyond the fix itself, the existing suite has no
per-target FFT-cost floor: a kernel change can silently shift cost on any
pinned constant without review.

What changed

Kernel (Ix/IxVM/Kernel/Levels.lean)

  • Canonical form: path-sorted list of entries (path, const, vars) where
    path is the sorted list of param indices conditioning an imax
    chain, const the max constant contribution, vars the
    idx-sorted (param, offset) contributions.
  • normalize_aux walks the level with imax-path conditioning,
    delegating IMax-shape cases to normalize_imax_dispatch.
  • Phase-2 nl_subsumption_walk drops contributions dominated by another
    entry whose path is a subset. Called once at the end of
    level_normalize (with the same list as both rem and snapshot).
  • nl_le / nl_eq operate on canonical forms; covers-split soundness
    fix matches level.rs.
  • level_normalize is keyed on the level alone, so each distinct level
    normalizes once per run; equality / leq on canonical forms is cheap.

Tests

  • Tests/Aiur/Common.lean: new expectedFftCost : Option Nat field on
    AiurTestCase. runTestCase consumes queryCounts, computes
    Aiur.computeStats, and asserts the rounded totalFftCost matches
    exactly. Adds Ix.Aiur.Statistics to the imports.
  • Tests/Ix/IxVM.lean: kernelCheckNames : List String →
    kernelCheckEntries : List (String × Nat). kernelChecks now sets
    expectedFftCost := some expected per entry.

Results

Unlocked targets

Before the kernel commit these typechecks OOM'd (process killed under
14 GB ulimit). After: complete with the FFT cost reported by
lake exe check <target>.

TargetBeforeAfter (FFT cost)
Trans.mkOOM2.91M
Array.append_assocOOM3.94G
Vector.appendOOM4.02G
Vector.extract_appendOOM63.76G

No regression on previously-passing targets

8-target sample, build clean both sides:

TargetBeforeAfter
Nat.add_comm56.05M56.08M
Nat.add13.34M13.34M
Nat.decEq71.92M71.92M
Nat.decLe209.64M209.64M
Nat.sub_le_of_le_add567.58M567.58M

Differences are sub-0.1%, attributable to the inlined-nl_subsumption
micro-cleanup (one fewer memoized dispatch per level_normalize call).

Pinned suite coverage

41 kernel-check constants now assert exact rounded FFT cost: the 38 prior
kernelCheckNames entries (Stdlib, IxVMPrim, IxVMInd, edge-case
prelude) plus 3 newly-unlocked targets (Trans.mk,
Array.append_assoc, Vector.append). Vector.extract_append is
deliberately omitted (too heavy for CI; verified manually).

How to update a pinned cost

If a future kernel change legitimately shifts FFT cost on a pinned
target, the test failure message contains the new value:

× ∃: FFT cost matches for Kernel check Trans.mk: expected 2911629, got 2911635

Paste the got N value back into kernelCheckEntries. No tooling
beyond lake test -- --ignored ixvm is required.

Test plan

  • lake build check — clean
  • lake build IxTests — clean
  • lake test -- --ignored ixvm — 41 FFT-cost pins pass, no
    regressions in the rest of the suite
  • lake exe check Trans.mk — 2.91 M FFT, passes
  • lake exe check Vector.append — 4.02 G FFT, passes
  • lake exe check Array.append_assoc — 3.94 G FFT, passes
  • lake exe check Vector.extract_append — 63.76 G FFT, passes
  • lake exe check Nat.add_comm — 56.08 M FFT, no regression

@arthurpaulino
arthurpaulinoforce-pushed the ap/level-leq-normalize branch from 439dd16 to 7821fcbCompareJune 17, 2026 15:58
@samuelburnham@arthurpaulino
IxVM: canonical level normalization for level_equal / level_leq
34e2cfc
Port the Rust kernel's canonical-form level machinery (level.rs
normalize_level / norm_level_eq / norm_level_le, itself a line-by-line
port of Lean4Lean's Level.Normalize with the covers-split soundness
fix): normalize_aux with imax-path conditioning, phase-2 subsumption,
and structural/dominance comparison on canonical forms. level_equal and
level_leq now normalize-and-compare; the previous recursive Level.leq
mirror with its two-way param-substitution split per Max/IMax — and its
helpers level_subst_reduce / level_has_param / level_any_param — is
deleted. level_normalize is keyed on the level alone, so each distinct
level normalizes once per run.
The split was exponential in the number of params and every branch
materialized freshly substituted levels. On
_private.…SInt.0.Int16.instRxcHasSize_eq the level family was 93% of
the record at 2^31 ops (level_subst_reduce 60.8M + level_leq 53.2M +
level_max 30.4M entries…), entered through Inductive's ctor-field
universe constraint (level_leq), not def-eq's level_equal.
Measured: Int16.instRxcHasSize_eq goes from NON-COMPLETING (killed at
178 GB RSS after 21 min, growth not converging) to 2m23s / 17.9 GB /
295.7B FFT. Int8 completes in 21s. The bench suite is unaffected (its
level comparisons hit the structural fast path). 297 ixvm tests pass.
@arthurpaulino
arthurpaulinoforce-pushed the ap/level-leq-normalize branch from 7821fcb to 95c3695CompareJune 17, 2026 20:17
@arthurpaulinoarthurpaulino changed the title IxVM kernel: port Rust's Géran normalize for level_leq + pin per-target FFT costIxVM kernel: canonical level normalization + FFT-cost pinningJun 17, 2026
@arthurpaulino
Tests: pin FFT cost per kernel-check target
31a35f0
## Summary
Adds `expectedFftCost : Option Nat` to `AiurTestCase`. When set,
`runTestCase` asserts the rounded `Aiur.computeStats.totalFftCost`
matches exactly. Converts `Tests/Ix/IxVM.lean::kernelCheckNames` to
`kernelCheckEntries : List (String × Nat)` and pins all 41 entries.
## Motivation
Without per-circuit cost pinning, kernel changes that silently shift
FFT cost can land without review. Pinning forces every cost change to
be acknowledged in the test source — failures report `expected X, got
Y` so the new value can be pasted back.
## Coverage
Pins the 38 prior `kernelCheckNames` entries (Stdlib, `IxVMPrim`,
`IxVMInd`, edge-case prelude) plus 3 newly-unlocked targets from the
`level_leq` Géran-normalize fix:
- `Trans.mk` — 2,732,504
- `Array.append_assoc` — 3,938,369,542
- `Vector.append` — 4,023,063,255
`Vector.extract_append` deliberately omitted (too heavy for the suite).
@arthurpaulino
arthurpaulinoforce-pushed the ap/level-leq-normalize branch from 95c3695 to 31a35f0CompareJune 17, 2026 20:32
@arthurpaulino
arthurpaulino merged commit 59a4183 into mainJun 17, 2026
14 checks passed
@arthurpaulino
arthurpaulino deleted the ap/level-leq-normalize branch June 17, 2026 21:02
@samuelburnhamsamuelburnham mentioned this pull request Jun 24, 2026
Closed
@arthurpaulinoarthurpaulino mentioned this pull request Jul 21, 2026
Merged
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@johnchandlerburnhamjohnchandlerburnhamjohnchandlerburnham approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@arthurpaulino@johnchandlerburnham@samuelburnham
, 'i'); if (__m === '*' || __re.test(location.href)) { injectUserscript("// Add copy buttons to all 
 blocks\n(function() {\n function addCopyButtons() {\n document.querySelectorAll('pre code').forEach(function(codeBlock) {\n if (codeBlock.parentElement.hasAttribute('data-copy-added')) return;\n codeBlock.parentElement.setAttribute('data-copy-added', 'true');\n \n var btn = document.createElement('button');\n btn.textContent = 'Copy';\n btn.style.cssText = 'position:absolute;top:4px;right:4px;padding:2px 8px;font-size:11px;background:#4ecdc4;border:none;border-radius:4px;color:#1a1a2e;cursor:pointer;opacity:0.7;transition:opacity 0.2s;';\n btn.onmouseover = function() { this.style.opacity = '1'; };\n btn.onmouseout = function() { this.style.opacity = '0.7'; };\n btn.onclick = function() {\n navigator.clipboard.writeText(codeBlock.textContent).then(function() {\n btn.textContent = 'Copied!';\n setTimeout(function() { btn.textContent = 'Copy'; }, 1500);\n });\n };\n codeBlock.parentElement.style.position = 'relative';\n codeBlock.parentElement.appendChild(btn);\n });\n }\n \n addCopyButtons();\n \n // Re-run on dynamic content\n var observer = new MutationObserver(addCopyButtons);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Add Copy Buttons to Code Blocks");
}
} catch(__e) { console.warn('[Userscript:Add Copy Buttons to Code Blocks]', __e); }
})();
(function(){
try {
var __m = "github.com";
var __re = new RegExp('^' + "github\\.com" + '

Skip to content
IxVM kernel: canonical level normalization + FFT-cost pinning - #447
Merged
arthurpaulino merged 2 commits into
mainfrom 
ap/level-leq-normalize
Jun 17, 2026
Merged
IxVM kernel: canonical level normalization + FFT-cost pinning#447
arthurpaulino merged 2 commits into
mainfrom 
ap/level-leq-normalize
Conversation
@arthurpaulino
@arthurpaulinoarthurpaulino
commented
Jun 17, 2026•

edited

Loading

Copy link


Copy Markdown

Member
Summary
Two commits on level-normalization:
  1. IxVM: canonical level normalization for level_equal /
    level_leq.     Replaces the recursive Level.leq mirror (two-way
    
param-substitution split per Max / IMax — exponential in unresolved
    
universe params) with a port of Rust's Géran canonical-form machinery
    
from src/ix/kernel/level.rs::normalize_level / norm_level_eq /
    norm_level_le. level_equal and level_leq now normalize-and-compare;
    
the substitution helpers (level_subst_reduce, level_has_param,
    level_any_param) are deleted.
  2. Tests: pin FFT cost per kernel-check target. Adds
    expectedFftCost : Option Nat to AiurTestCase; runTestCase asserts
    
the rounded Aiur.computeStats.totalFftCost matches exactly. Pins all
    
41 entries in Tests/Ix/IxVM.lean::kernelCheckEntries.
Motivation
The recursive Level.leq split was exponential in the number of params and

each branch materialized freshly substituted levels. On
_private.…SInt.0.Int16.instRxcHasSize_eq the level family was 93% of the

record at 2^31 ops (level_subst_reduce 60.8M + level_leq 53.2M +
level_max 30.4M entries…), entered through Inductive's ctor-field

universe constraint (level_leq), not def-eq's level_equal.
The same algorithmic gap blocks several stdlib targets in the in-tree
ixvm test suite. Beyond the fix itself, the existing suite has no

per-target FFT-cost floor: a kernel change can silently shift cost on any

pinned constant without review.
What changed
Kernel (Ix/IxVM/Kernel/Levels.lean)
  • Canonical form: path-sorted list of entries (path, const, vars) where
    path is the sorted list of param indices conditioning an imax
    
chain, const the max constant contribution, vars the
    
idx-sorted (param, offset) contributions.
  • normalize_aux walks the level with imax-path conditioning,
    
delegating IMax-shape cases to normalize_imax_dispatch.
  • Phase-2 nl_subsumption_walk drops contributions dominated by another
    
entry whose path is a subset. Called once at the end of
    level_normalize (with the same list as both rem and snapshot).
  • nl_le / nl_eq operate on canonical forms; covers-split soundness
    
fix matches level.rs.
  • level_normalize is keyed on the level alone, so each distinct level
    
normalizes once per run; equality / leq on canonical forms is cheap.
Tests
  • Tests/Aiur/Common.lean: new expectedFftCost : Option Nat field on
    AiurTestCase. runTestCase consumes queryCounts, computes
    Aiur.computeStats, and asserts the rounded totalFftCost matches
    
exactly. Adds Ix.Aiur.Statistics to the imports.
  • Tests/Ix/IxVM.lean: kernelCheckNames : List String →
    kernelCheckEntries : List (String × Nat). kernelChecks now sets
    expectedFftCost := some expected per entry.
Results
Unlocked targets
Before the kernel commit these typechecks OOM'd (process killed under

14 GB ulimit). After: complete with the FFT cost reported by
lake exe check <target>.
TargetBeforeAfter (FFT cost)
Trans.mkOOM2.91M
Array.append_assocOOM3.94G
Vector.appendOOM4.02G
Vector.extract_appendOOM63.76G
No regression on previously-passing targets
8-target sample, build clean both sides:
TargetBeforeAfter
Nat.add_comm56.05M56.08M
Nat.add13.34M13.34M
Nat.decEq71.92M71.92M
Nat.decLe209.64M209.64M
Nat.sub_le_of_le_add567.58M567.58M
Differences are sub-0.1%, attributable to the inlined-nl_subsumption

micro-cleanup (one fewer memoized dispatch per level_normalize call).
Pinned suite coverage
41 kernel-check constants now assert exact rounded FFT cost: the 38 prior
kernelCheckNames entries (Stdlib, IxVMPrim, IxVMInd, edge-case

prelude) plus 3 newly-unlocked targets (Trans.mk,
Array.append_assoc, Vector.append). Vector.extract_append is

deliberately omitted (too heavy for CI; verified manually).
How to update a pinned cost
If a future kernel change legitimately shifts FFT cost on a pinned

target, the test failure message contains the new value:
× ∃: FFT cost matches for Kernel check Trans.mk: expected 2911629, got 2911635

Paste the got N value back into kernelCheckEntries. No tooling

beyond lake test -- --ignored ixvm is required.
Test plan
  • lake build check — clean
  • lake build IxTests — clean
  • lake test -- --ignored ixvm — 41 FFT-cost pins pass, no
    
regressions in the rest of the suite
  • lake exe check Trans.mk — 2.91 M FFT, passes
  • lake exe check Vector.append — 4.02 G FFT, passes
  • lake exe check Array.append_assoc — 3.94 G FFT, passes
  • lake exe check Vector.extract_append — 63.76 G FFT, passes
  • lake exe check Nat.add_comm — 56.08 M FFT, no regression
@arthurpaulino
arthurpaulinoforce-pushed
the
ap/level-leq-normalize
branch
from
439dd16 to
7821fcbCompareJune 17, 2026 15:58
@samuelburnham@arthurpaulino
IxVM: canonical level normalization for level_equal / level_leq
34e2cfc
Port the Rust kernel's canonical-form level machinery (level.rs
normalize_level / norm_level_eq / norm_level_le, itself a line-by-line
port of Lean4Lean's Level.Normalize with the covers-split soundness
fix): normalize_aux with imax-path conditioning, phase-2 subsumption,
and structural/dominance comparison on canonical forms. level_equal and
level_leq now normalize-and-compare; the previous recursive Level.leq
mirror with its two-way param-substitution split per Max/IMax — and its
helpers level_subst_reduce / level_has_param / level_any_param — is
deleted. level_normalize is keyed on the level alone, so each distinct
level normalizes once per run.
The split was exponential in the number of params and every branch
materialized freshly substituted levels. On
_private.…SInt.0.Int16.instRxcHasSize_eq the level family was 93% of
the record at 2^31 ops (level_subst_reduce 60.8M + level_leq 53.2M +
level_max 30.4M entries…), entered through Inductive's ctor-field
universe constraint (level_leq), not def-eq's level_equal.
Measured: Int16.instRxcHasSize_eq goes from NON-COMPLETING (killed at
178 GB RSS after 21 min, growth not converging) to 2m23s / 17.9 GB /
295.7B FFT. Int8 completes in 21s. The bench suite is unaffected (its
level comparisons hit the structural fast path). 297 ixvm tests pass.
@arthurpaulino
arthurpaulinoforce-pushed
the
ap/level-leq-normalize
branch
from
7821fcb to
95c3695CompareJune 17, 2026 20:17
@arthurpaulinoarthurpaulino
changed the title
IxVM kernel: port Rust's Géran normalize for level_leq + pin per-target FFT costIxVM kernel: canonical level normalization + FFT-cost pinningJun 17, 2026
@arthurpaulino
Tests: pin FFT cost per kernel-check target
31a35f0
## Summary
Adds `expectedFftCost : Option Nat` to `AiurTestCase`. When set,
`runTestCase` asserts the rounded `Aiur.computeStats.totalFftCost`
matches exactly. Converts `Tests/Ix/IxVM.lean::kernelCheckNames` to
`kernelCheckEntries : List (String × Nat)` and pins all 41 entries.
## Motivation
Without per-circuit cost pinning, kernel changes that silently shift
FFT cost can land without review. Pinning forces every cost change to
be acknowledged in the test source — failures report `expected X, got
Y` so the new value can be pasted back.
## Coverage
Pins the 38 prior `kernelCheckNames` entries (Stdlib, `IxVMPrim`,
`IxVMInd`, edge-case prelude) plus 3 newly-unlocked targets from the
`level_leq` Géran-normalize fix:
- `Trans.mk` — 2,732,504
- `Array.append_assoc` — 3,938,369,542
- `Vector.append` — 4,023,063,255
`Vector.extract_append` deliberately omitted (too heavy for the suite).
@arthurpaulino
arthurpaulinoforce-pushed
the
ap/level-leq-normalize
branch
from
95c3695 to
31a35f0CompareJune 17, 2026 20:32
@arthurpaulino
arthurpaulino
merged commit 59a4183
into
mainJun 17, 2026

14 checks passed

@arthurpaulino
arthurpaulino
deleted the

ap/level-leq-normalize

branch
June 17, 2026 21:02
@samuelburnhamsamuelburnham
mentioned this pull request
Jun 24, 2026
 Closed

@arthurpaulinoarthurpaulino
mentioned this pull request
Jul 21, 2026
 Merged

Sign up for freeto join this conversation on GitHub.
Already have an account?
Sign in to comment

Reviewers

@johnchandlerburnhamjohnchandlerburnhamjohnchandlerburnham approved these changes

Assignees


No one assigned


Labels


None yet


Projects


None yet


Milestone


No milestone


Development

Successfully merging this pull request may close these issues.

3 participants

@arthurpaulino@johnchandlerburnham@samuelburnham

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Force GitHub README to respect dark mode\n(function() {\n var style = document.createElement('style');\n style.textContent = '\n .markdown-body {\n color-scheme: dark light;\n }\n .markdown-body pre { background: #161b22 !important; }\n .markdown-body code { background: rgba(110, 118, 129, 0.4) !important; }\n .markdown-body table th, .markdown-body table td { border-color: #30363d !important; }\n .markdown-body img { background: #0d1117; }\n .markdown-body blockquote { border-left-color: #8b949e; }\n .markdown-body hr { border-color: #30363d; }\n ';\n document.head.appendChild(style);\n})();", "GitHub Dark Mode README Fix");
}
} catch(__e) { console.warn('[Userscript:GitHub Dark Mode README Fix]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
IxVM kernel: canonical level normalization + FFT-cost pinning - #447
Merged
arthurpaulino merged 2 commits into
mainfrom 
ap/level-leq-normalize
Jun 17, 2026
Merged
IxVM kernel: canonical level normalization + FFT-cost pinning#447
arthurpaulino merged 2 commits into
mainfrom 
ap/level-leq-normalize
Conversation
@arthurpaulino
@arthurpaulinoarthurpaulino
commented
Jun 17, 2026•

edited

Loading

Copy link


Copy Markdown

Member
Summary
Two commits on level-normalization:
  1. IxVM: canonical level normalization for level_equal /
    level_leq.     Replaces the recursive Level.leq mirror (two-way
    
param-substitution split per Max / IMax — exponential in unresolved
    
universe params) with a port of Rust's Géran canonical-form machinery
    
from src/ix/kernel/level.rs::normalize_level / norm_level_eq /
    norm_level_le. level_equal and level_leq now normalize-and-compare;
    
the substitution helpers (level_subst_reduce, level_has_param,
    level_any_param) are deleted.
  2. Tests: pin FFT cost per kernel-check target. Adds
    expectedFftCost : Option Nat to AiurTestCase; runTestCase asserts
    
the rounded Aiur.computeStats.totalFftCost matches exactly. Pins all
    
41 entries in Tests/Ix/IxVM.lean::kernelCheckEntries.
Motivation
The recursive Level.leq split was exponential in the number of params and

each branch materialized freshly substituted levels. On
_private.…SInt.0.Int16.instRxcHasSize_eq the level family was 93% of the

record at 2^31 ops (level_subst_reduce 60.8M + level_leq 53.2M +
level_max 30.4M entries…), entered through Inductive's ctor-field

universe constraint (level_leq), not def-eq's level_equal.
The same algorithmic gap blocks several stdlib targets in the in-tree
ixvm test suite. Beyond the fix itself, the existing suite has no

per-target FFT-cost floor: a kernel change can silently shift cost on any

pinned constant without review.
What changed
Kernel (Ix/IxVM/Kernel/Levels.lean)
  • Canonical form: path-sorted list of entries (path, const, vars) where
    path is the sorted list of param indices conditioning an imax
    
chain, const the max constant contribution, vars the
    
idx-sorted (param, offset) contributions.
  • normalize_aux walks the level with imax-path conditioning,
    
delegating IMax-shape cases to normalize_imax_dispatch.
  • Phase-2 nl_subsumption_walk drops contributions dominated by another
    
entry whose path is a subset. Called once at the end of
    level_normalize (with the same list as both rem and snapshot).
  • nl_le / nl_eq operate on canonical forms; covers-split soundness
    
fix matches level.rs.
  • level_normalize is keyed on the level alone, so each distinct level
    
normalizes once per run; equality / leq on canonical forms is cheap.
Tests
  • Tests/Aiur/Common.lean: new expectedFftCost : Option Nat field on
    AiurTestCase. runTestCase consumes queryCounts, computes
    Aiur.computeStats, and asserts the rounded totalFftCost matches
    
exactly. Adds Ix.Aiur.Statistics to the imports.
  • Tests/Ix/IxVM.lean: kernelCheckNames : List String →
    kernelCheckEntries : List (String × Nat). kernelChecks now sets
    expectedFftCost := some expected per entry.
Results
Unlocked targets
Before the kernel commit these typechecks OOM'd (process killed under

14 GB ulimit). After: complete with the FFT cost reported by
lake exe check <target>.
TargetBeforeAfter (FFT cost)
Trans.mkOOM2.91M
Array.append_assocOOM3.94G
Vector.appendOOM4.02G
Vector.extract_appendOOM63.76G
No regression on previously-passing targets
8-target sample, build clean both sides:
TargetBeforeAfter
Nat.add_comm56.05M56.08M
Nat.add13.34M13.34M
Nat.decEq71.92M71.92M
Nat.decLe209.64M209.64M
Nat.sub_le_of_le_add567.58M567.58M
Differences are sub-0.1%, attributable to the inlined-nl_subsumption

micro-cleanup (one fewer memoized dispatch per level_normalize call).
Pinned suite coverage
41 kernel-check constants now assert exact rounded FFT cost: the 38 prior
kernelCheckNames entries (Stdlib, IxVMPrim, IxVMInd, edge-case

prelude) plus 3 newly-unlocked targets (Trans.mk,
Array.append_assoc, Vector.append). Vector.extract_append is

deliberately omitted (too heavy for CI; verified manually).
How to update a pinned cost
If a future kernel change legitimately shifts FFT cost on a pinned

target, the test failure message contains the new value:
× ∃: FFT cost matches for Kernel check Trans.mk: expected 2911629, got 2911635

Paste the got N value back into kernelCheckEntries. No tooling

beyond lake test -- --ignored ixvm is required.
Test plan
  • lake build check — clean
  • lake build IxTests — clean
  • lake test -- --ignored ixvm — 41 FFT-cost pins pass, no
    
regressions in the rest of the suite
  • lake exe check Trans.mk — 2.91 M FFT, passes
  • lake exe check Vector.append — 4.02 G FFT, passes
  • lake exe check Array.append_assoc — 3.94 G FFT, passes
  • lake exe check Vector.extract_append — 63.76 G FFT, passes
  • lake exe check Nat.add_comm — 56.08 M FFT, no regression
@arthurpaulino
arthurpaulinoforce-pushed
the
ap/level-leq-normalize
branch
from
439dd16 to
7821fcbCompareJune 17, 2026 15:58
@samuelburnham@arthurpaulino
IxVM: canonical level normalization for level_equal / level_leq
34e2cfc
Port the Rust kernel's canonical-form level machinery (level.rs
normalize_level / norm_level_eq / norm_level_le, itself a line-by-line
port of Lean4Lean's Level.Normalize with the covers-split soundness
fix): normalize_aux with imax-path conditioning, phase-2 subsumption,
and structural/dominance comparison on canonical forms. level_equal and
level_leq now normalize-and-compare; the previous recursive Level.leq
mirror with its two-way param-substitution split per Max/IMax — and its
helpers level_subst_reduce / level_has_param / level_any_param — is
deleted. level_normalize is keyed on the level alone, so each distinct
level normalizes once per run.
The split was exponential in the number of params and every branch
materialized freshly substituted levels. On
_private.…SInt.0.Int16.instRxcHasSize_eq the level family was 93% of
the record at 2^31 ops (level_subst_reduce 60.8M + level_leq 53.2M +
level_max 30.4M entries…), entered through Inductive's ctor-field
universe constraint (level_leq), not def-eq's level_equal.
Measured: Int16.instRxcHasSize_eq goes from NON-COMPLETING (killed at
178 GB RSS after 21 min, growth not converging) to 2m23s / 17.9 GB /
295.7B FFT. Int8 completes in 21s. The bench suite is unaffected (its
level comparisons hit the structural fast path). 297 ixvm tests pass.
@arthurpaulino
arthurpaulinoforce-pushed
the
ap/level-leq-normalize
branch
from
7821fcb to
95c3695CompareJune 17, 2026 20:17
@arthurpaulinoarthurpaulino
changed the title
IxVM kernel: port Rust's Géran normalize for level_leq + pin per-target FFT costIxVM kernel: canonical level normalization + FFT-cost pinningJun 17, 2026
@arthurpaulino
Tests: pin FFT cost per kernel-check target
31a35f0
## Summary
Adds `expectedFftCost : Option Nat` to `AiurTestCase`. When set,
`runTestCase` asserts the rounded `Aiur.computeStats.totalFftCost`
matches exactly. Converts `Tests/Ix/IxVM.lean::kernelCheckNames` to
`kernelCheckEntries : List (String × Nat)` and pins all 41 entries.
## Motivation
Without per-circuit cost pinning, kernel changes that silently shift
FFT cost can land without review. Pinning forces every cost change to
be acknowledged in the test source — failures report `expected X, got
Y` so the new value can be pasted back.
## Coverage
Pins the 38 prior `kernelCheckNames` entries (Stdlib, `IxVMPrim`,
`IxVMInd`, edge-case prelude) plus 3 newly-unlocked targets from the
`level_leq` Géran-normalize fix:
- `Trans.mk` — 2,732,504
- `Array.append_assoc` — 3,938,369,542
- `Vector.append` — 4,023,063,255
`Vector.extract_append` deliberately omitted (too heavy for the suite).
@arthurpaulino
arthurpaulinoforce-pushed
the
ap/level-leq-normalize
branch
from
95c3695 to
31a35f0CompareJune 17, 2026 20:32
@arthurpaulino
arthurpaulino
merged commit 59a4183
into
mainJun 17, 2026

14 checks passed

@arthurpaulino
arthurpaulino
deleted the

ap/level-leq-normalize

branch
June 17, 2026 21:02
@samuelburnhamsamuelburnham
mentioned this pull request
Jun 24, 2026
 Closed

@arthurpaulinoarthurpaulino
mentioned this pull request
Jul 21, 2026
 Merged

Sign up for freeto join this conversation on GitHub.
Already have an account?
Sign in to comment

Reviewers

@johnchandlerburnhamjohnchandlerburnhamjohnchandlerburnham approved these changes

Assignees


No one assigned


Labels


None yet


Projects


None yet


Milestone


No milestone


Development

Successfully merging this pull request may close these issues.

3 participants

@arthurpaulino@johnchandlerburnham@samuelburnham

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Highlight search terms from Google/DuckDuckGo/Bing referrer\n(function() {\n var ref = document.referrer;\n var terms = [];\n \n if (ref.includes('google.com') || ref.includes('duckduckgo.com') || ref.includes('bing.com')) {\n var url = new URL(ref);\n var q = url.searchParams.get('q') || url.searchParams.get('p');\n if (q) {\n terms = q.split(/\\s+/).filter(function(t) { return t.length > 2; });\n }\n }\n \n if (terms.length === 0) return;\n \n var style = document.createElement('style');\n style.textContent = '.userscript-highlight { background: #fbbf24; color: #1a1a2e; padding: 1px 3px; border-radius: 2px; }';\n document.head.appendChild(style);\n \n function highlight(node) {\n if (node.nodeType === 3) { // text node\n var text = node.textContent;\n var found = false;\n terms.forEach(function(term) {\n var regex = new RegExp('(' + term.replace(/[.*+?^${}()|[\\]\\\\]/g, '\\\\') + ')', 'gi');\n if (regex.test(text)) {\n found = true;\n var frag = document.createDocumentFragment();\n var parts = text.split(regex);\n parts.forEach(function(part, i) {\n if (i % 2 === 0) {\n frag.appendChild(document.createTextNode(part));\n } else {\n var span = document.createElement('span');\n span.className = 'userscript-highlight';\n span.textContent = part;\n frag.appendChild(span);\n }\n });\n node.parentNode.replaceChild(frag, node);\n }\n });\n } else if (node.nodeType === 1 && node.childNodes) { // element\n var skipTags = ['SCRIPT', 'STYLE', 'NOSCRIPT', 'TEXTAREA', 'INPUT', 'SELECT'];\n if (!skipTags.includes(node.tagName)) {\n Array.from(node.childNodes).forEach(highlight);\n }\n }\n }\n \n highlight(document.body);\n \n // Re-highlight on dynamic content\n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1 || node.nodeType === 3) highlight(node);\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Highlight Search Terms");
}
} catch(__e) { console.warn('[Userscript:Highlight Search Terms]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
IxVM kernel: canonical level normalization + FFT-cost pinning - #447
Merged
arthurpaulino merged 2 commits into
mainfrom 
ap/level-leq-normalize
Jun 17, 2026
Merged
IxVM kernel: canonical level normalization + FFT-cost pinning#447
arthurpaulino merged 2 commits into
mainfrom 
ap/level-leq-normalize
Conversation
@arthurpaulino
@arthurpaulinoarthurpaulino
commented
Jun 17, 2026•

edited

Loading

Copy link


Copy Markdown

Member
Summary
Two commits on level-normalization:
  1. IxVM: canonical level normalization for level_equal /
    level_leq.     Replaces the recursive Level.leq mirror (two-way
    
param-substitution split per Max / IMax — exponential in unresolved
    
universe params) with a port of Rust's Géran canonical-form machinery
    
from src/ix/kernel/level.rs::normalize_level / norm_level_eq /
    norm_level_le. level_equal and level_leq now normalize-and-compare;
    
the substitution helpers (level_subst_reduce, level_has_param,
    level_any_param) are deleted.
  2. Tests: pin FFT cost per kernel-check target. Adds
    expectedFftCost : Option Nat to AiurTestCase; runTestCase asserts
    
the rounded Aiur.computeStats.totalFftCost matches exactly. Pins all
    
41 entries in Tests/Ix/IxVM.lean::kernelCheckEntries.
Motivation
The recursive Level.leq split was exponential in the number of params and

each branch materialized freshly substituted levels. On
_private.…SInt.0.Int16.instRxcHasSize_eq the level family was 93% of the

record at 2^31 ops (level_subst_reduce 60.8M + level_leq 53.2M +
level_max 30.4M entries…), entered through Inductive's ctor-field

universe constraint (level_leq), not def-eq's level_equal.
The same algorithmic gap blocks several stdlib targets in the in-tree
ixvm test suite. Beyond the fix itself, the existing suite has no

per-target FFT-cost floor: a kernel change can silently shift cost on any

pinned constant without review.
What changed
Kernel (Ix/IxVM/Kernel/Levels.lean)
  • Canonical form: path-sorted list of entries (path, const, vars) where
    path is the sorted list of param indices conditioning an imax
    
chain, const the max constant contribution, vars the
    
idx-sorted (param, offset) contributions.
  • normalize_aux walks the level with imax-path conditioning,
    
delegating IMax-shape cases to normalize_imax_dispatch.
  • Phase-2 nl_subsumption_walk drops contributions dominated by another
    
entry whose path is a subset. Called once at the end of
    level_normalize (with the same list as both rem and snapshot).
  • nl_le / nl_eq operate on canonical forms; covers-split soundness
    
fix matches level.rs.
  • level_normalize is keyed on the level alone, so each distinct level
    
normalizes once per run; equality / leq on canonical forms is cheap.
Tests
  • Tests/Aiur/Common.lean: new expectedFftCost : Option Nat field on
    AiurTestCase. runTestCase consumes queryCounts, computes
    Aiur.computeStats, and asserts the rounded totalFftCost matches
    
exactly. Adds Ix.Aiur.Statistics to the imports.
  • Tests/Ix/IxVM.lean: kernelCheckNames : List String →
    kernelCheckEntries : List (String × Nat). kernelChecks now sets
    expectedFftCost := some expected per entry.
Results
Unlocked targets
Before the kernel commit these typechecks OOM'd (process killed under

14 GB ulimit). After: complete with the FFT cost reported by
lake exe check <target>.
TargetBeforeAfter (FFT cost)
Trans.mkOOM2.91M
Array.append_assocOOM3.94G
Vector.appendOOM4.02G
Vector.extract_appendOOM63.76G
No regression on previously-passing targets
8-target sample, build clean both sides:
TargetBeforeAfter
Nat.add_comm56.05M56.08M
Nat.add13.34M13.34M
Nat.decEq71.92M71.92M
Nat.decLe209.64M209.64M
Nat.sub_le_of_le_add567.58M567.58M
Differences are sub-0.1%, attributable to the inlined-nl_subsumption

micro-cleanup (one fewer memoized dispatch per level_normalize call).
Pinned suite coverage
41 kernel-check constants now assert exact rounded FFT cost: the 38 prior
kernelCheckNames entries (Stdlib, IxVMPrim, IxVMInd, edge-case

prelude) plus 3 newly-unlocked targets (Trans.mk,
Array.append_assoc, Vector.append). Vector.extract_append is

deliberately omitted (too heavy for CI; verified manually).
How to update a pinned cost
If a future kernel change legitimately shifts FFT cost on a pinned

target, the test failure message contains the new value:
× ∃: FFT cost matches for Kernel check Trans.mk: expected 2911629, got 2911635

Paste the got N value back into kernelCheckEntries. No tooling

beyond lake test -- --ignored ixvm is required.
Test plan
  • lake build check — clean
  • lake build IxTests — clean
  • lake test -- --ignored ixvm — 41 FFT-cost pins pass, no
    
regressions in the rest of the suite
  • lake exe check Trans.mk — 2.91 M FFT, passes
  • lake exe check Vector.append — 4.02 G FFT, passes
  • lake exe check Array.append_assoc — 3.94 G FFT, passes
  • lake exe check Vector.extract_append — 63.76 G FFT, passes
  • lake exe check Nat.add_comm — 56.08 M FFT, no regression
@arthurpaulino
arthurpaulinoforce-pushed
the
ap/level-leq-normalize
branch
from
439dd16 to
7821fcbCompareJune 17, 2026 15:58
@samuelburnham@arthurpaulino
IxVM: canonical level normalization for level_equal / level_leq
34e2cfc
Port the Rust kernel's canonical-form level machinery (level.rs
normalize_level / norm_level_eq / norm_level_le, itself a line-by-line
port of Lean4Lean's Level.Normalize with the covers-split soundness
fix): normalize_aux with imax-path conditioning, phase-2 subsumption,
and structural/dominance comparison on canonical forms. level_equal and
level_leq now normalize-and-compare; the previous recursive Level.leq
mirror with its two-way param-substitution split per Max/IMax — and its
helpers level_subst_reduce / level_has_param / level_any_param — is
deleted. level_normalize is keyed on the level alone, so each distinct
level normalizes once per run.
The split was exponential in the number of params and every branch
materialized freshly substituted levels. On
_private.…SInt.0.Int16.instRxcHasSize_eq the level family was 93% of
the record at 2^31 ops (level_subst_reduce 60.8M + level_leq 53.2M +
level_max 30.4M entries…), entered through Inductive's ctor-field
universe constraint (level_leq), not def-eq's level_equal.
Measured: Int16.instRxcHasSize_eq goes from NON-COMPLETING (killed at
178 GB RSS after 21 min, growth not converging) to 2m23s / 17.9 GB /
295.7B FFT. Int8 completes in 21s. The bench suite is unaffected (its
level comparisons hit the structural fast path). 297 ixvm tests pass.
@arthurpaulino
arthurpaulinoforce-pushed
the
ap/level-leq-normalize
branch
from
7821fcb to
95c3695CompareJune 17, 2026 20:17
@arthurpaulinoarthurpaulino
changed the title
IxVM kernel: port Rust's Géran normalize for level_leq + pin per-target FFT costIxVM kernel: canonical level normalization + FFT-cost pinningJun 17, 2026
@arthurpaulino
Tests: pin FFT cost per kernel-check target
31a35f0
## Summary
Adds `expectedFftCost : Option Nat` to `AiurTestCase`. When set,
`runTestCase` asserts the rounded `Aiur.computeStats.totalFftCost`
matches exactly. Converts `Tests/Ix/IxVM.lean::kernelCheckNames` to
`kernelCheckEntries : List (String × Nat)` and pins all 41 entries.
## Motivation
Without per-circuit cost pinning, kernel changes that silently shift
FFT cost can land without review. Pinning forces every cost change to
be acknowledged in the test source — failures report `expected X, got
Y` so the new value can be pasted back.
## Coverage
Pins the 38 prior `kernelCheckNames` entries (Stdlib, `IxVMPrim`,
`IxVMInd`, edge-case prelude) plus 3 newly-unlocked targets from the
`level_leq` Géran-normalize fix:
- `Trans.mk` — 2,732,504
- `Array.append_assoc` — 3,938,369,542
- `Vector.append` — 4,023,063,255
`Vector.extract_append` deliberately omitted (too heavy for the suite).
@arthurpaulino
arthurpaulinoforce-pushed
the
ap/level-leq-normalize
branch
from
95c3695 to
31a35f0CompareJune 17, 2026 20:32
@arthurpaulino
arthurpaulino
merged commit 59a4183
into
mainJun 17, 2026

14 checks passed

@arthurpaulino
arthurpaulino
deleted the

ap/level-leq-normalize

branch
June 17, 2026 21:02
@samuelburnhamsamuelburnham
mentioned this pull request
Jun 24, 2026
 Closed

@arthurpaulinoarthurpaulino
mentioned this pull request
Jul 21, 2026
 Merged

Sign up for freeto join this conversation on GitHub.
Already have an account?
Sign in to comment

Reviewers

@johnchandlerburnhamjohnchandlerburnhamjohnchandlerburnham approved these changes

Assignees


No one assigned


Labels


None yet


Projects


None yet


Milestone


No milestone


Development

Successfully merging this pull request may close these issues.

3 participants

@arthurpaulino@johnchandlerburnham@samuelburnham

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Strip utm_, fbclid, gclid, etc. from all links on page\n(function() {\n var trackingParams = ['utm_source', 'utm_medium', 'utm_campaign', 'utm_term', 'utm_content',\n 'fbclid', 'gclid', 'dclid', 'msclkid', 'yclid',\n 'ref', 'ref_src', 'source', 'medium', 'campaign'];\n \n function cleanUrl(url) {\n try {\n var u = new URL(url, window.location.origin);\n var changed = false;\n trackingParams.forEach(function(p) {\n if (u.searchParams.has(p)) {\n u.searchParams.delete(p);\n changed = true;\n }\n });\n return changed ? u.toString() : url;\n } catch (e) {\n return url;\n }\n }\n \n function cleanLinks() {\n document.querySelectorAll('a[href]').forEach(function(a) {\n var clean = cleanUrl(a.href);\n if (clean !== a.href) a.href = clean;\n });\n }\n \n cleanLinks();\n \n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1) {\n if (node.tagName === 'A') cleanLinks();\n node.querySelectorAll('a[href]').forEach(function(a) {\n var clean = cleanUrl(a.href);\n if (clean !== a.href) a.href = clean;\n });\n }\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Remove Tracking Parameters from Links");
}
} catch(__e) { console.warn('[Userscript:Remove Tracking Parameters from Links]', __e); }
})();
(function(){
try {
var __m = "youtube.com";
var __re = new RegExp('^' + "youtube\\.com" + '

Skip to content
IxVM kernel: canonical level normalization + FFT-cost pinning - #447
Merged
arthurpaulino merged 2 commits into
mainfrom 
ap/level-leq-normalize
Jun 17, 2026
Merged
IxVM kernel: canonical level normalization + FFT-cost pinning#447
arthurpaulino merged 2 commits into
mainfrom 
ap/level-leq-normalize
Conversation
@arthurpaulino
@arthurpaulinoarthurpaulino
commented
Jun 17, 2026•

edited

Loading

Copy link


Copy Markdown

Member
Summary
Two commits on level-normalization:
  1. IxVM: canonical level normalization for level_equal /
    level_leq.     Replaces the recursive Level.leq mirror (two-way
    
param-substitution split per Max / IMax — exponential in unresolved
    
universe params) with a port of Rust's Géran canonical-form machinery
    
from src/ix/kernel/level.rs::normalize_level / norm_level_eq /
    norm_level_le. level_equal and level_leq now normalize-and-compare;
    
the substitution helpers (level_subst_reduce, level_has_param,
    level_any_param) are deleted.
  2. Tests: pin FFT cost per kernel-check target. Adds
    expectedFftCost : Option Nat to AiurTestCase; runTestCase asserts
    
the rounded Aiur.computeStats.totalFftCost matches exactly. Pins all
    
41 entries in Tests/Ix/IxVM.lean::kernelCheckEntries.
Motivation
The recursive Level.leq split was exponential in the number of params and

each branch materialized freshly substituted levels. On
_private.…SInt.0.Int16.instRxcHasSize_eq the level family was 93% of the

record at 2^31 ops (level_subst_reduce 60.8M + level_leq 53.2M +
level_max 30.4M entries…), entered through Inductive's ctor-field

universe constraint (level_leq), not def-eq's level_equal.
The same algorithmic gap blocks several stdlib targets in the in-tree
ixvm test suite. Beyond the fix itself, the existing suite has no

per-target FFT-cost floor: a kernel change can silently shift cost on any

pinned constant without review.
What changed
Kernel (Ix/IxVM/Kernel/Levels.lean)
  • Canonical form: path-sorted list of entries (path, const, vars) where
    path is the sorted list of param indices conditioning an imax
    
chain, const the max constant contribution, vars the
    
idx-sorted (param, offset) contributions.
  • normalize_aux walks the level with imax-path conditioning,
    
delegating IMax-shape cases to normalize_imax_dispatch.
  • Phase-2 nl_subsumption_walk drops contributions dominated by another
    
entry whose path is a subset. Called once at the end of
    level_normalize (with the same list as both rem and snapshot).
  • nl_le / nl_eq operate on canonical forms; covers-split soundness
    
fix matches level.rs.
  • level_normalize is keyed on the level alone, so each distinct level
    
normalizes once per run; equality / leq on canonical forms is cheap.
Tests
  • Tests/Aiur/Common.lean: new expectedFftCost : Option Nat field on
    AiurTestCase. runTestCase consumes queryCounts, computes
    Aiur.computeStats, and asserts the rounded totalFftCost matches
    
exactly. Adds Ix.Aiur.Statistics to the imports.
  • Tests/Ix/IxVM.lean: kernelCheckNames : List String →
    kernelCheckEntries : List (String × Nat). kernelChecks now sets
    expectedFftCost := some expected per entry.
Results
Unlocked targets
Before the kernel commit these typechecks OOM'd (process killed under

14 GB ulimit). After: complete with the FFT cost reported by
lake exe check <target>.
TargetBeforeAfter (FFT cost)
Trans.mkOOM2.91M
Array.append_assocOOM3.94G
Vector.appendOOM4.02G
Vector.extract_appendOOM63.76G
No regression on previously-passing targets
8-target sample, build clean both sides:
TargetBeforeAfter
Nat.add_comm56.05M56.08M
Nat.add13.34M13.34M
Nat.decEq71.92M71.92M
Nat.decLe209.64M209.64M
Nat.sub_le_of_le_add567.58M567.58M
Differences are sub-0.1%, attributable to the inlined-nl_subsumption

micro-cleanup (one fewer memoized dispatch per level_normalize call).
Pinned suite coverage
41 kernel-check constants now assert exact rounded FFT cost: the 38 prior
kernelCheckNames entries (Stdlib, IxVMPrim, IxVMInd, edge-case

prelude) plus 3 newly-unlocked targets (Trans.mk,
Array.append_assoc, Vector.append). Vector.extract_append is

deliberately omitted (too heavy for CI; verified manually).
How to update a pinned cost
If a future kernel change legitimately shifts FFT cost on a pinned

target, the test failure message contains the new value:
× ∃: FFT cost matches for Kernel check Trans.mk: expected 2911629, got 2911635

Paste the got N value back into kernelCheckEntries. No tooling

beyond lake test -- --ignored ixvm is required.
Test plan
  • lake build check — clean
  • lake build IxTests — clean
  • lake test -- --ignored ixvm — 41 FFT-cost pins pass, no
    
regressions in the rest of the suite
  • lake exe check Trans.mk — 2.91 M FFT, passes
  • lake exe check Vector.append — 4.02 G FFT, passes
  • lake exe check Array.append_assoc — 3.94 G FFT, passes
  • lake exe check Vector.extract_append — 63.76 G FFT, passes
  • lake exe check Nat.add_comm — 56.08 M FFT, no regression
@arthurpaulino
arthurpaulinoforce-pushed
the
ap/level-leq-normalize
branch
from
439dd16 to
7821fcbCompareJune 17, 2026 15:58
@samuelburnham@arthurpaulino
IxVM: canonical level normalization for level_equal / level_leq
34e2cfc
Port the Rust kernel's canonical-form level machinery (level.rs
normalize_level / norm_level_eq / norm_level_le, itself a line-by-line
port of Lean4Lean's Level.Normalize with the covers-split soundness
fix): normalize_aux with imax-path conditioning, phase-2 subsumption,
and structural/dominance comparison on canonical forms. level_equal and
level_leq now normalize-and-compare; the previous recursive Level.leq
mirror with its two-way param-substitution split per Max/IMax — and its
helpers level_subst_reduce / level_has_param / level_any_param — is
deleted. level_normalize is keyed on the level alone, so each distinct
level normalizes once per run.
The split was exponential in the number of params and every branch
materialized freshly substituted levels. On
_private.…SInt.0.Int16.instRxcHasSize_eq the level family was 93% of
the record at 2^31 ops (level_subst_reduce 60.8M + level_leq 53.2M +
level_max 30.4M entries…), entered through Inductive's ctor-field
universe constraint (level_leq), not def-eq's level_equal.
Measured: Int16.instRxcHasSize_eq goes from NON-COMPLETING (killed at
178 GB RSS after 21 min, growth not converging) to 2m23s / 17.9 GB /
295.7B FFT. Int8 completes in 21s. The bench suite is unaffected (its
level comparisons hit the structural fast path). 297 ixvm tests pass.
@arthurpaulino
arthurpaulinoforce-pushed
the
ap/level-leq-normalize
branch
from
7821fcb to
95c3695CompareJune 17, 2026 20:17
@arthurpaulinoarthurpaulino
changed the title
IxVM kernel: port Rust's Géran normalize for level_leq + pin per-target FFT costIxVM kernel: canonical level normalization + FFT-cost pinningJun 17, 2026
@arthurpaulino
Tests: pin FFT cost per kernel-check target
31a35f0
## Summary
Adds `expectedFftCost : Option Nat` to `AiurTestCase`. When set,
`runTestCase` asserts the rounded `Aiur.computeStats.totalFftCost`
matches exactly. Converts `Tests/Ix/IxVM.lean::kernelCheckNames` to
`kernelCheckEntries : List (String × Nat)` and pins all 41 entries.
## Motivation
Without per-circuit cost pinning, kernel changes that silently shift
FFT cost can land without review. Pinning forces every cost change to
be acknowledged in the test source — failures report `expected X, got
Y` so the new value can be pasted back.
## Coverage
Pins the 38 prior `kernelCheckNames` entries (Stdlib, `IxVMPrim`,
`IxVMInd`, edge-case prelude) plus 3 newly-unlocked targets from the
`level_leq` Géran-normalize fix:
- `Trans.mk` — 2,732,504
- `Array.append_assoc` — 3,938,369,542
- `Vector.append` — 4,023,063,255
`Vector.extract_append` deliberately omitted (too heavy for the suite).
@arthurpaulino
arthurpaulinoforce-pushed
the
ap/level-leq-normalize
branch
from
95c3695 to
31a35f0CompareJune 17, 2026 20:32
@arthurpaulino
arthurpaulino
merged commit 59a4183
into
mainJun 17, 2026

14 checks passed

@arthurpaulino
arthurpaulino
deleted the

ap/level-leq-normalize

branch
June 17, 2026 21:02
@samuelburnhamsamuelburnham
mentioned this pull request
Jun 24, 2026
 Closed

@arthurpaulinoarthurpaulino
mentioned this pull request
Jul 21, 2026
 Merged

Sign up for freeto join this conversation on GitHub.
Already have an account?
Sign in to comment

Reviewers

@johnchandlerburnhamjohnchandlerburnhamjohnchandlerburnham approved these changes

Assignees


No one assigned


Labels


None yet


Projects


None yet


Milestone


No milestone


Development

Successfully merging this pull request may close these issues.

3 participants

@arthurpaulino@johnchandlerburnham@samuelburnham

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Auto-enable theater mode on YouTube\n(function() {\n function tryTheater() {\n var btn = document.querySelector('button[aria-label=\"Theater mode\"], ytd-player #player button[title=\"Theater mode\"]');\n if (btn && !btn.classList.contains('activated')) {\n btn.click();\n }\n }\n \n // Try immediately\n tryTheater();\n \n // Try after navigation (SPA)\n var lastUrl = location.href;\n setInterval(function() {\n if (location.href !== lastUrl) {\n lastUrl = location.href;\n setTimeout(tryTheater, 500);\n }\n }, 1000);\n \n // Also try on player load\n var observer = new MutationObserver(tryTheater);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "YouTube Theater Mode Default");
}
} catch(__e) { console.warn('[Userscript:YouTube Theater Mode Default]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
IxVM kernel: canonical level normalization + FFT-cost pinning - #447
Merged
arthurpaulino merged 2 commits into
mainfrom 
ap/level-leq-normalize
Jun 17, 2026
Merged
IxVM kernel: canonical level normalization + FFT-cost pinning#447
arthurpaulino merged 2 commits into
mainfrom 
ap/level-leq-normalize
Conversation
@arthurpaulino
@arthurpaulinoarthurpaulino
commented
Jun 17, 2026•

edited

Loading

Copy link


Copy Markdown

Member
Summary
Two commits on level-normalization:
  1. IxVM: canonical level normalization for level_equal /
    level_leq.     Replaces the recursive Level.leq mirror (two-way
    
param-substitution split per Max / IMax — exponential in unresolved
    
universe params) with a port of Rust's Géran canonical-form machinery
    
from src/ix/kernel/level.rs::normalize_level / norm_level_eq /
    norm_level_le. level_equal and level_leq now normalize-and-compare;
    
the substitution helpers (level_subst_reduce, level_has_param,
    level_any_param) are deleted.
  2. Tests: pin FFT cost per kernel-check target. Adds
    expectedFftCost : Option Nat to AiurTestCase; runTestCase asserts
    
the rounded Aiur.computeStats.totalFftCost matches exactly. Pins all
    
41 entries in Tests/Ix/IxVM.lean::kernelCheckEntries.
Motivation
The recursive Level.leq split was exponential in the number of params and

each branch materialized freshly substituted levels. On
_private.…SInt.0.Int16.instRxcHasSize_eq the level family was 93% of the

record at 2^31 ops (level_subst_reduce 60.8M + level_leq 53.2M +
level_max 30.4M entries…), entered through Inductive's ctor-field

universe constraint (level_leq), not def-eq's level_equal.
The same algorithmic gap blocks several stdlib targets in the in-tree
ixvm test suite. Beyond the fix itself, the existing suite has no

per-target FFT-cost floor: a kernel change can silently shift cost on any

pinned constant without review.
What changed
Kernel (Ix/IxVM/Kernel/Levels.lean)
  • Canonical form: path-sorted list of entries (path, const, vars) where
    path is the sorted list of param indices conditioning an imax
    
chain, const the max constant contribution, vars the
    
idx-sorted (param, offset) contributions.
  • normalize_aux walks the level with imax-path conditioning,
    
delegating IMax-shape cases to normalize_imax_dispatch.
  • Phase-2 nl_subsumption_walk drops contributions dominated by another
    
entry whose path is a subset. Called once at the end of
    level_normalize (with the same list as both rem and snapshot).
  • nl_le / nl_eq operate on canonical forms; covers-split soundness
    
fix matches level.rs.
  • level_normalize is keyed on the level alone, so each distinct level
    
normalizes once per run; equality / leq on canonical forms is cheap.
Tests
  • Tests/Aiur/Common.lean: new expectedFftCost : Option Nat field on
    AiurTestCase. runTestCase consumes queryCounts, computes
    Aiur.computeStats, and asserts the rounded totalFftCost matches
    
exactly. Adds Ix.Aiur.Statistics to the imports.
  • Tests/Ix/IxVM.lean: kernelCheckNames : List String →
    kernelCheckEntries : List (String × Nat). kernelChecks now sets
    expectedFftCost := some expected per entry.
Results
Unlocked targets
Before the kernel commit these typechecks OOM'd (process killed under

14 GB ulimit). After: complete with the FFT cost reported by
lake exe check <target>.
TargetBeforeAfter (FFT cost)
Trans.mkOOM2.91M
Array.append_assocOOM3.94G
Vector.appendOOM4.02G
Vector.extract_appendOOM63.76G
No regression on previously-passing targets
8-target sample, build clean both sides:
TargetBeforeAfter
Nat.add_comm56.05M56.08M
Nat.add13.34M13.34M
Nat.decEq71.92M71.92M
Nat.decLe209.64M209.64M
Nat.sub_le_of_le_add567.58M567.58M
Differences are sub-0.1%, attributable to the inlined-nl_subsumption

micro-cleanup (one fewer memoized dispatch per level_normalize call).
Pinned suite coverage
41 kernel-check constants now assert exact rounded FFT cost: the 38 prior
kernelCheckNames entries (Stdlib, IxVMPrim, IxVMInd, edge-case

prelude) plus 3 newly-unlocked targets (Trans.mk,
Array.append_assoc, Vector.append). Vector.extract_append is

deliberately omitted (too heavy for CI; verified manually).
How to update a pinned cost
If a future kernel change legitimately shifts FFT cost on a pinned

target, the test failure message contains the new value:
× ∃: FFT cost matches for Kernel check Trans.mk: expected 2911629, got 2911635

Paste the got N value back into kernelCheckEntries. No tooling

beyond lake test -- --ignored ixvm is required.
Test plan
  • lake build check — clean
  • lake build IxTests — clean
  • lake test -- --ignored ixvm — 41 FFT-cost pins pass, no
    
regressions in the rest of the suite
  • lake exe check Trans.mk — 2.91 M FFT, passes
  • lake exe check Vector.append — 4.02 G FFT, passes
  • lake exe check Array.append_assoc — 3.94 G FFT, passes
  • lake exe check Vector.extract_append — 63.76 G FFT, passes
  • lake exe check Nat.add_comm — 56.08 M FFT, no regression
@arthurpaulino
arthurpaulinoforce-pushed
the
ap/level-leq-normalize
branch
from
439dd16 to
7821fcbCompareJune 17, 2026 15:58
@samuelburnham@arthurpaulino
IxVM: canonical level normalization for level_equal / level_leq
34e2cfc
Port the Rust kernel's canonical-form level machinery (level.rs
normalize_level / norm_level_eq / norm_level_le, itself a line-by-line
port of Lean4Lean's Level.Normalize with the covers-split soundness
fix): normalize_aux with imax-path conditioning, phase-2 subsumption,
and structural/dominance comparison on canonical forms. level_equal and
level_leq now normalize-and-compare; the previous recursive Level.leq
mirror with its two-way param-substitution split per Max/IMax — and its
helpers level_subst_reduce / level_has_param / level_any_param — is
deleted. level_normalize is keyed on the level alone, so each distinct
level normalizes once per run.
The split was exponential in the number of params and every branch
materialized freshly substituted levels. On
_private.…SInt.0.Int16.instRxcHasSize_eq the level family was 93% of
the record at 2^31 ops (level_subst_reduce 60.8M + level_leq 53.2M +
level_max 30.4M entries…), entered through Inductive's ctor-field
universe constraint (level_leq), not def-eq's level_equal.
Measured: Int16.instRxcHasSize_eq goes from NON-COMPLETING (killed at
178 GB RSS after 21 min, growth not converging) to 2m23s / 17.9 GB /
295.7B FFT. Int8 completes in 21s. The bench suite is unaffected (its
level comparisons hit the structural fast path). 297 ixvm tests pass.
@arthurpaulino
arthurpaulinoforce-pushed
the
ap/level-leq-normalize
branch
from
7821fcb to
95c3695CompareJune 17, 2026 20:17
@arthurpaulinoarthurpaulino
changed the title
IxVM kernel: port Rust's Géran normalize for level_leq + pin per-target FFT costIxVM kernel: canonical level normalization + FFT-cost pinningJun 17, 2026
@arthurpaulino
Tests: pin FFT cost per kernel-check target
31a35f0
## Summary
Adds `expectedFftCost : Option Nat` to `AiurTestCase`. When set,
`runTestCase` asserts the rounded `Aiur.computeStats.totalFftCost`
matches exactly. Converts `Tests/Ix/IxVM.lean::kernelCheckNames` to
`kernelCheckEntries : List (String × Nat)` and pins all 41 entries.
## Motivation
Without per-circuit cost pinning, kernel changes that silently shift
FFT cost can land without review. Pinning forces every cost change to
be acknowledged in the test source — failures report `expected X, got
Y` so the new value can be pasted back.
## Coverage
Pins the 38 prior `kernelCheckNames` entries (Stdlib, `IxVMPrim`,
`IxVMInd`, edge-case prelude) plus 3 newly-unlocked targets from the
`level_leq` Géran-normalize fix:
- `Trans.mk` — 2,732,504
- `Array.append_assoc` — 3,938,369,542
- `Vector.append` — 4,023,063,255
`Vector.extract_append` deliberately omitted (too heavy for the suite).
@arthurpaulino
arthurpaulinoforce-pushed
the
ap/level-leq-normalize
branch
from
95c3695 to
31a35f0CompareJune 17, 2026 20:32
@arthurpaulino
arthurpaulino
merged commit 59a4183
into
mainJun 17, 2026

14 checks passed

@arthurpaulino
arthurpaulino
deleted the

ap/level-leq-normalize

branch
June 17, 2026 21:02
@samuelburnhamsamuelburnham
mentioned this pull request
Jun 24, 2026
 Closed

@arthurpaulinoarthurpaulino
mentioned this pull request
Jul 21, 2026
 Merged

Sign up for freeto join this conversation on GitHub.
Already have an account?
Sign in to comment

Reviewers

@johnchandlerburnhamjohnchandlerburnhamjohnchandlerburnham approved these changes

Assignees


No one assigned


Labels


None yet


Projects


None yet


Milestone


No milestone


Development

Successfully merging this pull request may close these issues.

3 participants

@arthurpaulino@johnchandlerburnham@samuelburnham

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Remove or un-stick sticky/fixed headers that block content\n(function() {\n function unstick() {\n document.querySelectorAll('header, nav, [role=\"banner\"], .header, .navbar, .sticky, .fixed-top, [style*=\"position: fixed\"], [style*=\"position:sticky\"]').forEach(function(el) {\n if (el.style.position === 'fixed' || el.style.position === 'sticky' || \n getComputedStyle(el).position === 'fixed' || getComputedStyle(el).position === 'sticky') {\n el.style.position = 'static';\n el.style.top = 'auto';\n el.style.zIndex = 'auto';\n }\n });\n }\n \n unstick();\n \n var observer = new MutationObserver(unstick);\n observer.observe(document.body, { childList: true, subtree: true, attributes: true, attributeFilter: ['style', 'class'] });\n})();", "Kill Sticky Headers");
}
} catch(__e) { console.warn('[Userscript:Kill Sticky Headers]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
IxVM kernel: canonical level normalization + FFT-cost pinning - #447
Merged
arthurpaulino merged 2 commits into
mainfrom 
ap/level-leq-normalize
Jun 17, 2026
Merged
IxVM kernel: canonical level normalization + FFT-cost pinning#447
arthurpaulino merged 2 commits into
mainfrom 
ap/level-leq-normalize
Conversation
@arthurpaulino
@arthurpaulinoarthurpaulino
commented
Jun 17, 2026•

edited

Loading

Copy link


Copy Markdown

Member
Summary
Two commits on level-normalization:
  1. IxVM: canonical level normalization for level_equal /
    level_leq.     Replaces the recursive Level.leq mirror (two-way
    
param-substitution split per Max / IMax — exponential in unresolved
    
universe params) with a port of Rust's Géran canonical-form machinery
    
from src/ix/kernel/level.rs::normalize_level / norm_level_eq /
    norm_level_le. level_equal and level_leq now normalize-and-compare;
    
the substitution helpers (level_subst_reduce, level_has_param,
    level_any_param) are deleted.
  2. Tests: pin FFT cost per kernel-check target. Adds
    expectedFftCost : Option Nat to AiurTestCase; runTestCase asserts
    
the rounded Aiur.computeStats.totalFftCost matches exactly. Pins all
    
41 entries in Tests/Ix/IxVM.lean::kernelCheckEntries.
Motivation
The recursive Level.leq split was exponential in the number of params and

each branch materialized freshly substituted levels. On
_private.…SInt.0.Int16.instRxcHasSize_eq the level family was 93% of the

record at 2^31 ops (level_subst_reduce 60.8M + level_leq 53.2M +
level_max 30.4M entries…), entered through Inductive's ctor-field

universe constraint (level_leq), not def-eq's level_equal.
The same algorithmic gap blocks several stdlib targets in the in-tree
ixvm test suite. Beyond the fix itself, the existing suite has no

per-target FFT-cost floor: a kernel change can silently shift cost on any

pinned constant without review.
What changed
Kernel (Ix/IxVM/Kernel/Levels.lean)
  • Canonical form: path-sorted list of entries (path, const, vars) where
    path is the sorted list of param indices conditioning an imax
    
chain, const the max constant contribution, vars the
    
idx-sorted (param, offset) contributions.
  • normalize_aux walks the level with imax-path conditioning,
    
delegating IMax-shape cases to normalize_imax_dispatch.
  • Phase-2 nl_subsumption_walk drops contributions dominated by another
    
entry whose path is a subset. Called once at the end of
    level_normalize (with the same list as both rem and snapshot).
  • nl_le / nl_eq operate on canonical forms; covers-split soundness
    
fix matches level.rs.
  • level_normalize is keyed on the level alone, so each distinct level
    
normalizes once per run; equality / leq on canonical forms is cheap.
Tests
  • Tests/Aiur/Common.lean: new expectedFftCost : Option Nat field on
    AiurTestCase. runTestCase consumes queryCounts, computes
    Aiur.computeStats, and asserts the rounded totalFftCost matches
    
exactly. Adds Ix.Aiur.Statistics to the imports.
  • Tests/Ix/IxVM.lean: kernelCheckNames : List String →
    kernelCheckEntries : List (String × Nat). kernelChecks now sets
    expectedFftCost := some expected per entry.
Results
Unlocked targets
Before the kernel commit these typechecks OOM'd (process killed under

14 GB ulimit). After: complete with the FFT cost reported by
lake exe check <target>.
TargetBeforeAfter (FFT cost)
Trans.mkOOM2.91M
Array.append_assocOOM3.94G
Vector.appendOOM4.02G
Vector.extract_appendOOM63.76G
No regression on previously-passing targets
8-target sample, build clean both sides:
TargetBeforeAfter
Nat.add_comm56.05M56.08M
Nat.add13.34M13.34M
Nat.decEq71.92M71.92M
Nat.decLe209.64M209.64M
Nat.sub_le_of_le_add567.58M567.58M
Differences are sub-0.1%, attributable to the inlined-nl_subsumption

micro-cleanup (one fewer memoized dispatch per level_normalize call).
Pinned suite coverage
41 kernel-check constants now assert exact rounded FFT cost: the 38 prior
kernelCheckNames entries (Stdlib, IxVMPrim, IxVMInd, edge-case

prelude) plus 3 newly-unlocked targets (Trans.mk,
Array.append_assoc, Vector.append). Vector.extract_append is

deliberately omitted (too heavy for CI; verified manually).
How to update a pinned cost
If a future kernel change legitimately shifts FFT cost on a pinned

target, the test failure message contains the new value:
× ∃: FFT cost matches for Kernel check Trans.mk: expected 2911629, got 2911635

Paste the got N value back into kernelCheckEntries. No tooling

beyond lake test -- --ignored ixvm is required.
Test plan
  • lake build check — clean
  • lake build IxTests — clean
  • lake test -- --ignored ixvm — 41 FFT-cost pins pass, no
    
regressions in the rest of the suite
  • lake exe check Trans.mk — 2.91 M FFT, passes
  • lake exe check Vector.append — 4.02 G FFT, passes
  • lake exe check Array.append_assoc — 3.94 G FFT, passes
  • lake exe check Vector.extract_append — 63.76 G FFT, passes
  • lake exe check Nat.add_comm — 56.08 M FFT, no regression
@arthurpaulino
arthurpaulinoforce-pushed
the
ap/level-leq-normalize
branch
from
439dd16 to
7821fcbCompareJune 17, 2026 15:58
@samuelburnham@arthurpaulino
IxVM: canonical level normalization for level_equal / level_leq
34e2cfc
Port the Rust kernel's canonical-form level machinery (level.rs
normalize_level / norm_level_eq / norm_level_le, itself a line-by-line
port of Lean4Lean's Level.Normalize with the covers-split soundness
fix): normalize_aux with imax-path conditioning, phase-2 subsumption,
and structural/dominance comparison on canonical forms. level_equal and
level_leq now normalize-and-compare; the previous recursive Level.leq
mirror with its two-way param-substitution split per Max/IMax — and its
helpers level_subst_reduce / level_has_param / level_any_param — is
deleted. level_normalize is keyed on the level alone, so each distinct
level normalizes once per run.
The split was exponential in the number of params and every branch
materialized freshly substituted levels. On
_private.…SInt.0.Int16.instRxcHasSize_eq the level family was 93% of
the record at 2^31 ops (level_subst_reduce 60.8M + level_leq 53.2M +
level_max 30.4M entries…), entered through Inductive's ctor-field
universe constraint (level_leq), not def-eq's level_equal.
Measured: Int16.instRxcHasSize_eq goes from NON-COMPLETING (killed at
178 GB RSS after 21 min, growth not converging) to 2m23s / 17.9 GB /
295.7B FFT. Int8 completes in 21s. The bench suite is unaffected (its
level comparisons hit the structural fast path). 297 ixvm tests pass.
@arthurpaulino
arthurpaulinoforce-pushed
the
ap/level-leq-normalize
branch
from
7821fcb to
95c3695CompareJune 17, 2026 20:17
@arthurpaulinoarthurpaulino
changed the title
IxVM kernel: port Rust's Géran normalize for level_leq + pin per-target FFT costIxVM kernel: canonical level normalization + FFT-cost pinningJun 17, 2026
@arthurpaulino
Tests: pin FFT cost per kernel-check target
31a35f0
## Summary
Adds `expectedFftCost : Option Nat` to `AiurTestCase`. When set,
`runTestCase` asserts the rounded `Aiur.computeStats.totalFftCost`
matches exactly. Converts `Tests/Ix/IxVM.lean::kernelCheckNames` to
`kernelCheckEntries : List (String × Nat)` and pins all 41 entries.
## Motivation
Without per-circuit cost pinning, kernel changes that silently shift
FFT cost can land without review. Pinning forces every cost change to
be acknowledged in the test source — failures report `expected X, got
Y` so the new value can be pasted back.
## Coverage
Pins the 38 prior `kernelCheckNames` entries (Stdlib, `IxVMPrim`,
`IxVMInd`, edge-case prelude) plus 3 newly-unlocked targets from the
`level_leq` Géran-normalize fix:
- `Trans.mk` — 2,732,504
- `Array.append_assoc` — 3,938,369,542
- `Vector.append` — 4,023,063,255
`Vector.extract_append` deliberately omitted (too heavy for the suite).
@arthurpaulino
arthurpaulinoforce-pushed
the
ap/level-leq-normalize
branch
from
95c3695 to
31a35f0CompareJune 17, 2026 20:32
@arthurpaulino
arthurpaulino
merged commit 59a4183
into
mainJun 17, 2026

14 checks passed

@arthurpaulino
arthurpaulino
deleted the

ap/level-leq-normalize

branch
June 17, 2026 21:02
@samuelburnhamsamuelburnham
mentioned this pull request
Jun 24, 2026
 Closed

@arthurpaulinoarthurpaulino
mentioned this pull request
Jul 21, 2026
 Merged

Sign up for freeto join this conversation on GitHub.
Already have an account?
Sign in to comment

Reviewers

@johnchandlerburnhamjohnchandlerburnhamjohnchandlerburnham approved these changes

Assignees


No one assigned


Labels


None yet


Projects


None yet


Milestone


No milestone


Development

Successfully merging this pull request may close these issues.

3 participants

@arthurpaulino@johnchandlerburnham@samuelburnham

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Universal Dark Mode - works on any site\n(function() {\n var enabled = true;\n \n function applyDarkMode() {\n if (!enabled) return;\n \n // Create style element if it doesn't exist\n var style = document.getElementById('universal-dark-mode-style');\n if (!style) {\n style = document.createElement('style');\n style.id = 'universal-dark-mode-style';\n document.head.appendChild(style);\n }\n \n // Dark mode CSS - inverts colors but preserves images/video\n style.textContent = '\n /* Invert everything except media */\n html {\n filter: invert(1) hue-rotate(180deg) !important;\n background: #1a1a2e !important;\n }\n \n /* Restore images, videos, iframes, canvas */\n img, video, iframe, canvas, svg, picture, [style*=\"background-image\"] {\n filter: invert(1) hue-rotate(180deg) !important;\n }\n \n /* Preserve specific elements that should not be inverted */\n .no-dark-mode, .no-dark-mode *,\n [data-theme=\"light\"], [data-theme=\"light\"],\n .ace_editor, .ace_editor *,\n .CodeMirror, .CodeMirror *,\n .monaco-editor, .monaco-editor *,\n .markdown-body pre, .markdown-body pre *,\n .highlight, .highlight *,\n pre code, pre code * {\n filter: none !important;\n }\n \n /* Fix common UI elements */\n .modal, .popup, .dropdown-menu, .tooltip, .popover {\n filter: invert(1) hue-rotate(180deg) !important;\n background: #2d2d44 !important;\n border-color: #444 !important;\n }\n \n /* Scrollbars */\n ::-webkit-scrollbar { background: #1a1a2e !important; }\n ::-webkit-scrollbar-thumb { background: #444 !important; }\n ::-webkit-scrollbar-thumb:hover { background: #555 !important; }\n \n /* Selection */\n ::selection { background: #4ecdc4 !important; color: #1a1a2e !important; }\n ::-moz-selection { background: #4ecdc4 !important; color: #1a1a2e !important; }\n ';\n }\n \n function removeDarkMode() {\n var style = document.getElementById('universal-dark-mode-style');\n if (style) style.remove();\n }\n \n // Toggle with Alt+Shift+D\n document.addEventListener('keydown', function(e) {\n if (e.altKey && e.shiftKey && e.key === 'D') {\n e.preventDefault();\n enabled = !enabled;\n if (enabled) {\n applyDarkMode();\n console.log('[Universal Dark Mode] Enabled');\n } else {\n removeDarkMode();\n console.log('[Universal Dark Mode] Disabled');\n }\n }\n });\n \n // Apply on load\n applyDarkMode();\n \n // Re-apply on dynamic content\n var observer = new MutationObserver(function(mutations) {\n if (enabled && !document.getElementById('universal-dark-mode-style')) {\n applyDarkMode();\n }\n });\n observer.observe(document.head, { childList: true });\n \n console.log('[Universal Dark Mode] Loaded - Press Alt+Shift+D to toggle');\n})();", "Universal Dark Mode");
}
} catch(__e) { console.warn('[Userscript:Universal Dark Mode]', __e); }
})();
})();

Skip to content
IxVM kernel: canonical level normalization + FFT-cost pinning - #447
Merged
arthurpaulino merged 2 commits into
mainfrom 
ap/level-leq-normalize
Jun 17, 2026
Merged
IxVM kernel: canonical level normalization + FFT-cost pinning#447
arthurpaulino merged 2 commits into
mainfrom 
ap/level-leq-normalize
Conversation
@arthurpaulino
@arthurpaulinoarthurpaulino
commented
Jun 17, 2026•

edited

Loading

Copy link


Copy Markdown

Member
Summary
Two commits on level-normalization:
  1. IxVM: canonical level normalization for level_equal /
    level_leq.     Replaces the recursive Level.leq mirror (two-way
    
param-substitution split per Max / IMax — exponential in unresolved
    
universe params) with a port of Rust's Géran canonical-form machinery
    
from src/ix/kernel/level.rs::normalize_level / norm_level_eq /
    norm_level_le. level_equal and level_leq now normalize-and-compare;
    
the substitution helpers (level_subst_reduce, level_has_param,
    level_any_param) are deleted.
  2. Tests: pin FFT cost per kernel-check target. Adds
    expectedFftCost : Option Nat to AiurTestCase; runTestCase asserts
    
the rounded Aiur.computeStats.totalFftCost matches exactly. Pins all
    
41 entries in Tests/Ix/IxVM.lean::kernelCheckEntries.
Motivation
The recursive Level.leq split was exponential in the number of params and

each branch materialized freshly substituted levels. On
_private.…SInt.0.Int16.instRxcHasSize_eq the level family was 93% of the

record at 2^31 ops (level_subst_reduce 60.8M + level_leq 53.2M +
level_max 30.4M entries…), entered through Inductive's ctor-field

universe constraint (level_leq), not def-eq's level_equal.
The same algorithmic gap blocks several stdlib targets in the in-tree
ixvm test suite. Beyond the fix itself, the existing suite has no

per-target FFT-cost floor: a kernel change can silently shift cost on any

pinned constant without review.
What changed
Kernel (Ix/IxVM/Kernel/Levels.lean)
  • Canonical form: path-sorted list of entries (path, const, vars) where
    path is the sorted list of param indices conditioning an imax
    
chain, const the max constant contribution, vars the
    
idx-sorted (param, offset) contributions.
  • normalize_aux walks the level with imax-path conditioning,
    
delegating IMax-shape cases to normalize_imax_dispatch.
  • Phase-2 nl_subsumption_walk drops contributions dominated by another
    
entry whose path is a subset. Called once at the end of
    level_normalize (with the same list as both rem and snapshot).
  • nl_le / nl_eq operate on canonical forms; covers-split soundness
    
fix matches level.rs.
  • level_normalize is keyed on the level alone, so each distinct level
    
normalizes once per run; equality / leq on canonical forms is cheap.
Tests
  • Tests/Aiur/Common.lean: new expectedFftCost : Option Nat field on
    AiurTestCase. runTestCase consumes queryCounts, computes
    Aiur.computeStats, and asserts the rounded totalFftCost matches
    
exactly. Adds Ix.Aiur.Statistics to the imports.
  • Tests/Ix/IxVM.lean: kernelCheckNames : List String →
    kernelCheckEntries : List (String × Nat). kernelChecks now sets
    expectedFftCost := some expected per entry.
Results
Unlocked targets
Before the kernel commit these typechecks OOM'd (process killed under

14 GB ulimit). After: complete with the FFT cost reported by
lake exe check <target>.
TargetBeforeAfter (FFT cost)
Trans.mkOOM2.91M
Array.append_assocOOM3.94G
Vector.appendOOM4.02G
Vector.extract_appendOOM63.76G
No regression on previously-passing targets
8-target sample, build clean both sides:
TargetBeforeAfter
Nat.add_comm56.05M56.08M
Nat.add13.34M13.34M
Nat.decEq71.92M71.92M
Nat.decLe209.64M209.64M
Nat.sub_le_of_le_add567.58M567.58M
Differences are sub-0.1%, attributable to the inlined-nl_subsumption

micro-cleanup (one fewer memoized dispatch per level_normalize call).
Pinned suite coverage
41 kernel-check constants now assert exact rounded FFT cost: the 38 prior
kernelCheckNames entries (Stdlib, IxVMPrim, IxVMInd, edge-case

prelude) plus 3 newly-unlocked targets (Trans.mk,
Array.append_assoc, Vector.append). Vector.extract_append is

deliberately omitted (too heavy for CI; verified manually).
How to update a pinned cost
If a future kernel change legitimately shifts FFT cost on a pinned

target, the test failure message contains the new value:
× ∃: FFT cost matches for Kernel check Trans.mk: expected 2911629, got 2911635

Paste the got N value back into kernelCheckEntries. No tooling

beyond lake test -- --ignored ixvm is required.
Test plan
  • lake build check — clean
  • lake build IxTests — clean
  • lake test -- --ignored ixvm — 41 FFT-cost pins pass, no
    
regressions in the rest of the suite
  • lake exe check Trans.mk — 2.91 M FFT, passes
  • lake exe check Vector.append — 4.02 G FFT, passes
  • lake exe check Array.append_assoc — 3.94 G FFT, passes
  • lake exe check Vector.extract_append — 63.76 G FFT, passes
  • lake exe check Nat.add_comm — 56.08 M FFT, no regression
@arthurpaulino
arthurpaulinoforce-pushed
the
ap/level-leq-normalize
branch
from
439dd16 to
7821fcbCompareJune 17, 2026 15:58
@samuelburnham@arthurpaulino
IxVM: canonical level normalization for level_equal / level_leq
34e2cfc
Port the Rust kernel's canonical-form level machinery (level.rs
normalize_level / norm_level_eq / norm_level_le, itself a line-by-line
port of Lean4Lean's Level.Normalize with the covers-split soundness
fix): normalize_aux with imax-path conditioning, phase-2 subsumption,
and structural/dominance comparison on canonical forms. level_equal and
level_leq now normalize-and-compare; the previous recursive Level.leq
mirror with its two-way param-substitution split per Max/IMax — and its
helpers level_subst_reduce / level_has_param / level_any_param — is
deleted. level_normalize is keyed on the level alone, so each distinct
level normalizes once per run.
The split was exponential in the number of params and every branch
materialized freshly substituted levels. On
_private.…SInt.0.Int16.instRxcHasSize_eq the level family was 93% of
the record at 2^31 ops (level_subst_reduce 60.8M + level_leq 53.2M +
level_max 30.4M entries…), entered through Inductive's ctor-field
universe constraint (level_leq), not def-eq's level_equal.
Measured: Int16.instRxcHasSize_eq goes from NON-COMPLETING (killed at
178 GB RSS after 21 min, growth not converging) to 2m23s / 17.9 GB /
295.7B FFT. Int8 completes in 21s. The bench suite is unaffected (its
level comparisons hit the structural fast path). 297 ixvm tests pass.
@arthurpaulino
arthurpaulinoforce-pushed
the
ap/level-leq-normalize
branch
from
7821fcb to
95c3695CompareJune 17, 2026 20:17
@arthurpaulinoarthurpaulino
changed the title
IxVM kernel: port Rust's Géran normalize for level_leq + pin per-target FFT costIxVM kernel: canonical level normalization + FFT-cost pinningJun 17, 2026
@arthurpaulino
Tests: pin FFT cost per kernel-check target
31a35f0
## Summary
Adds `expectedFftCost : Option Nat` to `AiurTestCase`. When set,
`runTestCase` asserts the rounded `Aiur.computeStats.totalFftCost`
matches exactly. Converts `Tests/Ix/IxVM.lean::kernelCheckNames` to
`kernelCheckEntries : List (String × Nat)` and pins all 41 entries.
## Motivation
Without per-circuit cost pinning, kernel changes that silently shift
FFT cost can land without review. Pinning forces every cost change to
be acknowledged in the test source — failures report `expected X, got
Y` so the new value can be pasted back.
## Coverage
Pins the 38 prior `kernelCheckNames` entries (Stdlib, `IxVMPrim`,
`IxVMInd`, edge-case prelude) plus 3 newly-unlocked targets from the
`level_leq` Géran-normalize fix:
- `Trans.mk` — 2,732,504
- `Array.append_assoc` — 3,938,369,542
- `Vector.append` — 4,023,063,255
`Vector.extract_append` deliberately omitted (too heavy for the suite).
@arthurpaulino
arthurpaulinoforce-pushed
the
ap/level-leq-normalize
branch
from
95c3695 to
31a35f0CompareJune 17, 2026 20:32
@arthurpaulino
arthurpaulino
merged commit 59a4183
into
mainJun 17, 2026

14 checks passed

@arthurpaulino
arthurpaulino
deleted the

ap/level-leq-normalize

branch
June 17, 2026 21:02
@samuelburnhamsamuelburnham
mentioned this pull request
Jun 24, 2026
 Closed

@arthurpaulinoarthurpaulino
mentioned this pull request
Jul 21, 2026
 Merged

Sign up for freeto join this conversation on GitHub.
Already have an account?
Sign in to comment

Reviewers

@johnchandlerburnhamjohnchandlerburnhamjohnchandlerburnham approved these changes

Assignees


No one assigned


Labels


None yet


Projects


None yet


Milestone


No milestone


Development

Successfully merging this pull request may close these issues.

3 participants

@arthurpaulino@johnchandlerburnham@samuelburnham