Add kernel type-checker by johnchandlerburnham · Pull Request #375 · argumentcomputer/ix

.github/valgrind.supp

-Original file line number
+Diff line change
@@ -0,0 +1,31 @@
+{
+ mimalloc-prim-mem-init-uninit-cond
+ Memcheck:Cond
+ fun:_mi_strnlen
+ fun:_mi_strnstr
+ fun:_mi_prim_mem_init
+ fun:mi_process_init
+ ...
+}
+{
+ mimalloc-prim-mem-init-uninit-value8
+ Memcheck:Value8
+ fun:_mi_strnlen
+ fun:_mi_strnstr
+ fun:_mi_prim_mem_init
+ fun:mi_process_init
+ ...
+}
+{
+ glibc-pthread-create-tls-dtv
+ Memcheck:Leak
+ match-leak-kinds: possible
+ fun:calloc
+ fun:allocate_dtv
+ fun:_dl_allocate_tls
+ ...
+ fun:pthread_create*
+ ...
+}

.github/workflows/ignored.yml

-Original file line number
+Diff line change
@@ Expand Up / @@ -53,7 +53,12 @@ jobs: @@
  build-args: "IxTests"
  use-github-cache: false
  - name: Install valgrind
- run: sudo apt-get update && sudo apt-get install -y valgrind
+ run: |
+ # Some warpbuild images ship a mirrorlist with an unreachable
+ # azure.archive.ubuntu.com entry, causing apt-get update to stall indefinitely.
+ sudo sed -i '/azure\.archive\.ubuntu\.com/d' /etc/apt/apt-mirrors.txt 2>/dev/null || true
+ sudo apt-get update
+ sudo apt-get install -y valgrind
  - name: Run tests under valgrind
  run: |
  valgrind \
@@ Expand All / @@ -62,4 +67,5 @@ jobs: @@
  --errors-for-leak-kinds=definite \
  --track-origins=yes \
  --error-exitcode=1 \
+ --suppressions=.github/valgrind.supp \
  .lake/build/bin/IxTests -- ffi

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 contentNavigation Menu Sign inAppearance settings AI CODE CREATIONGitHub CopilotWrite better code with AI GitHub Copilot appDirect agents from issue to merge MCP RegistryIntegrate external tools DEVELOPER WORKFLOWSActionsAutomate any workflow CodespacesInstant dev environments IssuesPlan and track work Code ReviewManage code changes Code QualityEnforce quality at merge APPLICATION SECURITYGitHub Advanced SecurityFind and fix vulnerabilities Code securitySecure your code as you build Secret protectionStop leaks before they start EXPLOREWhy GitHub Documentation Blog Changelog Marketplace View all features BY COMPANY SIZEEnterprises Small and medium teams Startups Nonprofits BY USE CASEApp Modernization DevSecOps DevOps CI/CD View all use cases BY INDUSTRYHealthcare Financial services Manufacturing Government View all industries View all solutions EXPLORE BY TOPICAI Software Development DevOps Security View all topics EXPLORE BY TYPECustomer stories Events & webinars Ebooks & reports Business insights GitHub Skills SUPPORT & SERVICESDocumentation Customer support Community forum Trust center Partners View all resources COMMUNITYGitHub SponsorsFund open source developers PROGRAMSSecurity Lab Maintainer Community GitHub Stars Archive Program REPOSITORIESTopics Trending Collections ENTERPRISE SOLUTIONSEnterprise platformAI-powered developer platform AVAILABLE ADD-ONSGitHub Advanced SecurityEnterprise-grade security features Copilot for BusinessEnterprise-grade AI features Premium SupportEnterprise-grade 24/7 support Pricing Sign in Sign upAppearance settings You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert Uh oh! There was an error while loading. Please reload this page. argumentcomputer /ixPublic Notifications You must be signed in to change notification settings Fork 3 Star 91 Code Issues10 Pull requests14 Actions Projects Security and quality0 Insights Additional navigation options Code Issues Pull requests Actions Projects Security and quality Insights Add kernel type-checker#375 New issue Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community. Sign up for GitHub By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails. Already on GitHub? Sign in to your account Merged johnchandlerburnham merged 35 commits into main from jcb/kernelMay 7, 2026 Conversation 7 Commits 35 Checks 14 Files changed Uh oh! There was an error while loading. Please reload this page. Merged Add kernel type-checker #375 Show file tree Hide file tree Changes from all commits Commits Show all changes 35 commits Select commit Hold shift + click to select a range 8024807 Add kernel type-checker and restructure ConstantMeta for aux_gen johnchandlerburnham Apr 12, 20265fb6a7a Extract compile_env scheduler and resolve all cargo xclippy warnings johnchandlerburnham Apr 12, 2026142cc5e Add canonical aux_gen pipeline for alpha-collapsed inductive blocks johnchandlerburnham Apr 13, 2026718a0e6 fmt johnchandlerburnham Apr 13, 20264fa8cfa refactor validate-aux test johnchandlerburnham Apr 13, 2026114be51 fix Ixon Lean serialization johnchandlerburnham Apr 13, 20265d54533 Lift kernel caches into Arc<KEnv> and switch to content-addressed cac… johnchandlerburnham Apr 15, 2026f0bceac Call-site surgery, aux_gen cleanup, and Env Arc refactor johnchandlerburnham Apr 17, 2026e4579e0 solve mathlib compilation and ingress roundtrip issues johnchandlerburnham Apr 17, 202605bdf10 Close the Mathlib aux_gen congruence loop: CompileMathlib.lean passes johnchandlerburnham Apr 19, 2026a034db2 Kernel soundness hardening, two-env split, Int native reduction, tole… johnchandlerburnham Apr 21, 2026ec05c94 Anonymous canonicity: aux permutation sidecar, perm-aware congruence,… johnchandlerburnham Apr 24, 2026a37d592 Kernel-side canonicity validation and full-env check pipeline johnchandlerburnham Apr 26, 202626c3be7 xclippy warnings johnchandlerburnham Apr 26, 202656e3e79 Stream ixon_ingress into KEnv; own-and-drop IxonEnv before kernel check johnchandlerburnham Apr 27, 2026c749b58 Add IX_PERF_COUNTERS instrumentation for kernel cache hit rates johnchandlerburnham Apr 27, 20261847240 kernel: add cheap projection def-eq WHNF safely johnchandlerburnham Apr 27, 2026508ca82 Speed up kernel validation and refine infer cache keys johnchandlerburnham Apr 27, 20261dfafd5 Add `ix ingress` CLI; expand kernel caches; parallel-shard env drops johnchandlerburnham Apr 28, 20264b2409d Speed up ixon_ingress: hash-first interning + 2048-shard intern table johnchandlerburnham Apr 28, 2026ec95312 Align nested-aux canonical order between compile and kernel johnchandlerburnham Apr 28, 20261d930c8 kernel: fix over-discovery in build_flat_block johnchandlerburnham Apr 28, 20264951b0d kernel: per-worker KEnv with lazy Ixon ingress; add `ix check-ixon` CLI johnchandlerburnham Apr 29, 20268f15dc0 kernel: add FVar binder opening, alpha-invariant hashing, Nat reduc… johnchandlerburnham Apr 30, 2026aea118d fmt & clippy johnchandlerburnham May 1, 20266e802ce Merge branch 'main' of github.com:argumentcomputer/ix into jcb/kernel johnchandlerburnham May 1, 20265b14e5c aux_gen: alpha-collapse-aware roundtrip + alias-only patching johnchandlerburnham May 1, 2026d9e0fbb aux_gen: source-shape-preserving WHNF + Phase 1 cache prewarming johnchandlerburnham May 1, 2026ef4b061 `decide` is enough to prove `Aiur.G.one_ne_zero` arthurpaulino May 4, 2026a289432 Update docs/ix_canonicity.md johnchandlerburnham May 5, 20262d5cabd xclippy warnings johnchandlerburnham May 5, 2026e5d5a34 fix aux_gen test johnchandlerburnham May 5, 20269d132ef comment out ixvm tests arthurpaulino May 6, 20266e4d1ad chore: Fix lean-ffi (#395) samuelburnham May 6, 2026bef77b1 ci: Fix valgrind samuelburnham May 6, 2026 File filter Filter by extension Filter by extension .lean (33) .lock (1) .md (1) .rs (65) .supp (1) .toml (2) .yml (1) All 7 file types selected Only manifest files Viewed files Clear filters Conversations Failed to load comments. Loading Uh oh! There was an error while loading. Please reload this page. Jump to Jump to file Failed to load files. Loading Uh oh! There was an error while loading. Please reload this page. Diff view Unified Split Hide whitespace Diff view Unified Split Hide whitespace .github/valgrind.supp valgrind.supp .github/workflows/ignored.yml ignored.yml Cargo.lock Cargo.lock Cargo.toml Cargo.toml Ix.lean Ix.lean Ix/Aiur/Goldilocks.lean Goldilocks.lean Ix/Cli/CheckCmd.lean CheckCmd.lean Ix/Cli/CheckIxonCmd.lean CheckIxonCmd.lean Ix/Cli/CompileCmd.lean CompileCmd.lean Ix/Cli/IngressCmd.lean IngressCmd.lean Ix/Cli/ValidateCmd.lean ValidateCmd.lean Ix/Commit.lean Commit.lean Ix/CompileM.lean CompileM.lean Ix/DecompileM.lean DecompileM.lean Ix/Ixon.lean Ixon.lean Ix/KernelCheck.lean KernelCheck.lean Ix/Meta.lean Meta.lean Main.lean Main.lean Tests/FFI.lean FFI.lean Tests/FFI/Ixon.lean Ixon.lean Tests/FFI/Lifecycle.lean Lifecycle.lean Tests/Gen/Ixon.lean Ixon.lean Tests/Ix/Compile.lean Compile.lean Tests/Ix/Compile/Canonicity.lean Canonicity.lean Tests/Ix/Compile/Mutual.lean Mutual.lean Tests/Ix/Compile/ValidateAux.lean ValidateAux.lean Tests/Ix/Kernel/BuildPrimOrigs.lean BuildPrimOrigs.lean Tests/Ix/Kernel/BuildPrimitives.lean BuildPrimitives.lean Tests/Ix/Kernel/CheckEnv.lean CheckEnv.lean Tests/Ix/Kernel/NatReduction.lean NatReduction.lean Tests/Ix/Kernel/Roundtrip.lean Roundtrip.lean Tests/Ix/Kernel/RoundtripNoCompile.lean RoundtripNoCompile.lean Tests/Ix/Kernel/Tutorial.lean Tutorial.lean Tests/Ix/Kernel/TutorialDefs.lean TutorialDefs.lean Tests/Ix/Kernel/TutorialMeta.lean TutorialMeta.lean Tests/Main.lean Main.lean deny.toml deny.toml docs/ix_canonicity.md ix_canonicity.md lakefile.lean lakefile.lean src/ffi.rs ffi.rs src/ffi/compile.rs compile.rs src/ffi/ix/env.rs env.rs src/ffi/ixon/meta.rs meta.rs src/ffi/ixon/serialize.rs serialize.rs src/ffi/ixon/sharing.rs sharing.rs src/ffi/kernel.rs kernel.rs src/ffi/lean_env.rs lean_env.rs src/ix.rs ix.rs src/ix/address.rs address.rs src/ix/compile.rs compile.rs src/ix/compile/aux_gen.rs aux_gen.rs src/ix/compile/aux_gen/below.rs below.rs src/ix/compile/aux_gen/brecon.rs brecon.rs src/ix/compile/aux_gen/cases_on.rs cases_on.rs src/ix/compile/aux_gen/expr_utils.rs expr_utils.rs src/ix/compile/aux_gen/nested.rs nested.rs src/ix/compile/aux_gen/rec_on.rs rec_on.rs src/ix/compile/aux_gen/recursor.rs recursor.rs src/ix/compile/env.rs env.rs src/ix/compile/mutual.rs mutual.rs src/ix/compile/nat_conv.rs nat_conv.rs src/ix/compile/surgery.rs surgery.rs src/ix/congruence.rs congruence.rs src/ix/congruence/perm.rs perm.rs src/ix/decompile.rs decompile.rs src/ix/env.rs env.rs src/ix/graph.rs graph.rs src/ix/ground.rs ground.rs src/ix/ixon/env.rs env.rs src/ix/ixon/error.rs error.rs src/ix/ixon/metadata.rs metadata.rs src/ix/ixon/serialize.rs serialize.rs src/ix/ixon/sharing.rs sharing.rs src/ix/kernel.rs kernel.rs src/ix/kernel/canonical_check.rs canonical_check.rs src/ix/kernel/check.rs check.rs src/ix/kernel/congruence.rs congruence.rs src/ix/kernel/constant.rs constant.rs src/ix/kernel/def_eq.rs def_eq.rs src/ix/kernel/egress.rs egress.rs src/ix/kernel/env.rs env.rs src/ix/kernel/equiv.rs equiv.rs src/ix/kernel/error.rs error.rs src/ix/kernel/expr.rs expr.rs src/ix/kernel/id.rs id.rs src/ix/kernel/inductive.rs inductive.rs src/ix/kernel/infer.rs infer.rs src/ix/kernel/ingress.rs ingress.rs src/ix/kernel/lctx.rs lctx.rs src/ix/kernel/level.rs level.rs src/ix/kernel/mode.rs mode.rs src/ix/kernel/perf.rs perf.rs src/ix/kernel/primitive.rs primitive.rs src/ix/kernel/subst.rs subst.rs src/ix/kernel/tc.rs tc.rs src/ix/kernel/testing.rs testing.rs src/ix/kernel/tutorial/basic.rs basic.rs src/ix/kernel/tutorial/defeq.rs defeq.rs src/ix/kernel/tutorial/inductive.rs inductive.rs src/ix/kernel/tutorial/mod.rs mod.rs src/ix/kernel/tutorial/reduction.rs reduction.rs src/ix/kernel/whnf.rs whnf.rs src/lean.rs lean.rs src/lib.rs lib.rs There are no files selected for viewing 31 changes: 31 additions & 0 deletions 31 .github/valgrind.supp Show comments View file Open in desktop Original file line number Diff line number Diff line change @@ -0,0 +1,31 @@ { mimalloc-prim-mem-init-uninit-cond Memcheck:Cond fun:_mi_strnlen fun:_mi_strnstr fun:_mi_prim_mem_init fun:mi_process_init ... } { mimalloc-prim-mem-init-uninit-value8 Memcheck:Value8 fun:_mi_strnlen fun:_mi_strnstr fun:_mi_prim_mem_init fun:mi_process_init ... } { glibc-pthread-create-tls-dtv Memcheck:Leak match-leak-kinds: possible fun:calloc fun:allocate_dtv fun:_dl_allocate_tls ... fun:pthread_create* ... } 8 changes: 7 additions & 1 deletion 8 .github/workflows/ignored.yml Show comments View file Open in desktop Original file line number Diff line number Diff line change Expand Up @@ -53,7 +53,12 @@ jobs: build-args: "IxTests" use-github-cache: false - name: Install valgrind run: sudo apt-get update && sudo apt-get install -y valgrind run: | # Some warpbuild images ship a mirrorlist with an unreachable # azure.archive.ubuntu.com entry, causing apt-get update to stall indefinitely. sudo sed -i '/azure\.archive\.ubuntu\.com/d' /etc/apt/apt-mirrors.txt 2>/dev/null || true sudo apt-get update sudo apt-get install -y valgrind - name: Run tests under valgrind run: | valgrind \ Expand All @@ -62,4 +67,5 @@ jobs: --errors-for-leak-kinds=definite \ --track-origins=yes \ --error-exitcode=1 \ --suppressions=.github/valgrind.supp \ .lake/build/bin/IxTests -- ffi Loading Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later. Footer © 2026 GitHub, Inc. Footer navigation Terms Privacy Security Status Community Docs Contact You can’t perform that action at this time. , '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 contentNavigation Menu Sign inAppearance settings AI CODE CREATIONGitHub CopilotWrite better code with AI GitHub Copilot appDirect agents from issue to merge MCP RegistryIntegrate external tools DEVELOPER WORKFLOWSActionsAutomate any workflow CodespacesInstant dev environments IssuesPlan and track work Code ReviewManage code changes Code QualityEnforce quality at merge APPLICATION SECURITYGitHub Advanced SecurityFind and fix vulnerabilities Code securitySecure your code as you build Secret protectionStop leaks before they start EXPLOREWhy GitHub Documentation Blog Changelog Marketplace View all features BY COMPANY SIZEEnterprises Small and medium teams Startups Nonprofits BY USE CASEApp Modernization DevSecOps DevOps CI/CD View all use cases BY INDUSTRYHealthcare Financial services Manufacturing Government View all industries View all solutions EXPLORE BY TOPICAI Software Development DevOps Security View all topics EXPLORE BY TYPECustomer stories Events & webinars Ebooks & reports Business insights GitHub Skills SUPPORT & SERVICESDocumentation Customer support Community forum Trust center Partners View all resources COMMUNITYGitHub SponsorsFund open source developers PROGRAMSSecurity Lab Maintainer Community GitHub Stars Archive Program REPOSITORIESTopics Trending Collections ENTERPRISE SOLUTIONSEnterprise platformAI-powered developer platform AVAILABLE ADD-ONSGitHub Advanced SecurityEnterprise-grade security features Copilot for BusinessEnterprise-grade AI features Premium SupportEnterprise-grade 24/7 support Pricing Sign in Sign upAppearance settings You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert Uh oh! There was an error while loading. Please reload this page. argumentcomputer /ixPublic Notifications You must be signed in to change notification settings Fork 3 Star 91 Code Issues10 Pull requests14 Actions Projects Security and quality0 Insights Additional navigation options Code Issues Pull requests Actions Projects Security and quality Insights Add kernel type-checker#375 New issue Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community. Sign up for GitHub By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails. Already on GitHub? Sign in to your account Merged johnchandlerburnham merged 35 commits into main from jcb/kernelMay 7, 2026 Conversation 7 Commits 35 Checks 14 Files changed Uh oh! There was an error while loading. Please reload this page. Merged Add kernel type-checker #375 Show file tree Hide file tree Changes from all commits Commits Show all changes 35 commits Select commit Hold shift + click to select a range 8024807 Add kernel type-checker and restructure ConstantMeta for aux_gen johnchandlerburnham Apr 12, 20265fb6a7a Extract compile_env scheduler and resolve all cargo xclippy warnings johnchandlerburnham Apr 12, 2026142cc5e Add canonical aux_gen pipeline for alpha-collapsed inductive blocks johnchandlerburnham Apr 13, 2026718a0e6 fmt johnchandlerburnham Apr 13, 20264fa8cfa refactor validate-aux test johnchandlerburnham Apr 13, 2026114be51 fix Ixon Lean serialization johnchandlerburnham Apr 13, 20265d54533 Lift kernel caches into Arc<KEnv> and switch to content-addressed cac… johnchandlerburnham Apr 15, 2026f0bceac Call-site surgery, aux_gen cleanup, and Env Arc refactor johnchandlerburnham Apr 17, 2026e4579e0 solve mathlib compilation and ingress roundtrip issues johnchandlerburnham Apr 17, 202605bdf10 Close the Mathlib aux_gen congruence loop: CompileMathlib.lean passes johnchandlerburnham Apr 19, 2026a034db2 Kernel soundness hardening, two-env split, Int native reduction, tole… johnchandlerburnham Apr 21, 2026ec05c94 Anonymous canonicity: aux permutation sidecar, perm-aware congruence,… johnchandlerburnham Apr 24, 2026a37d592 Kernel-side canonicity validation and full-env check pipeline johnchandlerburnham Apr 26, 202626c3be7 xclippy warnings johnchandlerburnham Apr 26, 202656e3e79 Stream ixon_ingress into KEnv; own-and-drop IxonEnv before kernel check johnchandlerburnham Apr 27, 2026c749b58 Add IX_PERF_COUNTERS instrumentation for kernel cache hit rates johnchandlerburnham Apr 27, 20261847240 kernel: add cheap projection def-eq WHNF safely johnchandlerburnham Apr 27, 2026508ca82 Speed up kernel validation and refine infer cache keys johnchandlerburnham Apr 27, 20261dfafd5 Add `ix ingress` CLI; expand kernel caches; parallel-shard env drops johnchandlerburnham Apr 28, 20264b2409d Speed up ixon_ingress: hash-first interning + 2048-shard intern table johnchandlerburnham Apr 28, 2026ec95312 Align nested-aux canonical order between compile and kernel johnchandlerburnham Apr 28, 20261d930c8 kernel: fix over-discovery in build_flat_block johnchandlerburnham Apr 28, 20264951b0d kernel: per-worker KEnv with lazy Ixon ingress; add `ix check-ixon` CLI johnchandlerburnham Apr 29, 20268f15dc0 kernel: add FVar binder opening, alpha-invariant hashing, Nat reduc… johnchandlerburnham Apr 30, 2026aea118d fmt & clippy johnchandlerburnham May 1, 20266e802ce Merge branch 'main' of github.com:argumentcomputer/ix into jcb/kernel johnchandlerburnham May 1, 20265b14e5c aux_gen: alpha-collapse-aware roundtrip + alias-only patching johnchandlerburnham May 1, 2026d9e0fbb aux_gen: source-shape-preserving WHNF + Phase 1 cache prewarming johnchandlerburnham May 1, 2026ef4b061 `decide` is enough to prove `Aiur.G.one_ne_zero` arthurpaulino May 4, 2026a289432 Update docs/ix_canonicity.md johnchandlerburnham May 5, 20262d5cabd xclippy warnings johnchandlerburnham May 5, 2026e5d5a34 fix aux_gen test johnchandlerburnham May 5, 20269d132ef comment out ixvm tests arthurpaulino May 6, 20266e4d1ad chore: Fix lean-ffi (#395) samuelburnham May 6, 2026bef77b1 ci: Fix valgrind samuelburnham May 6, 2026 File filter Filter by extension Filter by extension .lean (33) .lock (1) .md (1) .rs (65) .supp (1) .toml (2) .yml (1) All 7 file types selected Only manifest files Viewed files Clear filters Conversations Failed to load comments. Loading Uh oh! There was an error while loading. Please reload this page. Jump to Jump to file Failed to load files. Loading Uh oh! There was an error while loading. Please reload this page. Diff view Unified Split Hide whitespace Diff view Unified Split Hide whitespace .github/valgrind.supp valgrind.supp .github/workflows/ignored.yml ignored.yml Cargo.lock Cargo.lock Cargo.toml Cargo.toml Ix.lean Ix.lean Ix/Aiur/Goldilocks.lean Goldilocks.lean Ix/Cli/CheckCmd.lean CheckCmd.lean Ix/Cli/CheckIxonCmd.lean CheckIxonCmd.lean Ix/Cli/CompileCmd.lean CompileCmd.lean Ix/Cli/IngressCmd.lean IngressCmd.lean Ix/Cli/ValidateCmd.lean ValidateCmd.lean Ix/Commit.lean Commit.lean Ix/CompileM.lean CompileM.lean Ix/DecompileM.lean DecompileM.lean Ix/Ixon.lean Ixon.lean Ix/KernelCheck.lean KernelCheck.lean Ix/Meta.lean Meta.lean Main.lean Main.lean Tests/FFI.lean FFI.lean Tests/FFI/Ixon.lean Ixon.lean Tests/FFI/Lifecycle.lean Lifecycle.lean Tests/Gen/Ixon.lean Ixon.lean Tests/Ix/Compile.lean Compile.lean Tests/Ix/Compile/Canonicity.lean Canonicity.lean Tests/Ix/Compile/Mutual.lean Mutual.lean Tests/Ix/Compile/ValidateAux.lean ValidateAux.lean Tests/Ix/Kernel/BuildPrimOrigs.lean BuildPrimOrigs.lean Tests/Ix/Kernel/BuildPrimitives.lean BuildPrimitives.lean Tests/Ix/Kernel/CheckEnv.lean CheckEnv.lean Tests/Ix/Kernel/NatReduction.lean NatReduction.lean Tests/Ix/Kernel/Roundtrip.lean Roundtrip.lean Tests/Ix/Kernel/RoundtripNoCompile.lean RoundtripNoCompile.lean Tests/Ix/Kernel/Tutorial.lean Tutorial.lean Tests/Ix/Kernel/TutorialDefs.lean TutorialDefs.lean Tests/Ix/Kernel/TutorialMeta.lean TutorialMeta.lean Tests/Main.lean Main.lean deny.toml deny.toml docs/ix_canonicity.md ix_canonicity.md lakefile.lean lakefile.lean src/ffi.rs ffi.rs src/ffi/compile.rs compile.rs src/ffi/ix/env.rs env.rs src/ffi/ixon/meta.rs meta.rs src/ffi/ixon/serialize.rs serialize.rs src/ffi/ixon/sharing.rs sharing.rs src/ffi/kernel.rs kernel.rs src/ffi/lean_env.rs lean_env.rs src/ix.rs ix.rs src/ix/address.rs address.rs src/ix/compile.rs compile.rs src/ix/compile/aux_gen.rs aux_gen.rs src/ix/compile/aux_gen/below.rs below.rs src/ix/compile/aux_gen/brecon.rs brecon.rs src/ix/compile/aux_gen/cases_on.rs cases_on.rs src/ix/compile/aux_gen/expr_utils.rs expr_utils.rs src/ix/compile/aux_gen/nested.rs nested.rs src/ix/compile/aux_gen/rec_on.rs rec_on.rs src/ix/compile/aux_gen/recursor.rs recursor.rs src/ix/compile/env.rs env.rs src/ix/compile/mutual.rs mutual.rs src/ix/compile/nat_conv.rs nat_conv.rs src/ix/compile/surgery.rs surgery.rs src/ix/congruence.rs congruence.rs src/ix/congruence/perm.rs perm.rs src/ix/decompile.rs decompile.rs src/ix/env.rs env.rs src/ix/graph.rs graph.rs src/ix/ground.rs ground.rs src/ix/ixon/env.rs env.rs src/ix/ixon/error.rs error.rs src/ix/ixon/metadata.rs metadata.rs src/ix/ixon/serialize.rs serialize.rs src/ix/ixon/sharing.rs sharing.rs src/ix/kernel.rs kernel.rs src/ix/kernel/canonical_check.rs canonical_check.rs src/ix/kernel/check.rs check.rs src/ix/kernel/congruence.rs congruence.rs src/ix/kernel/constant.rs constant.rs src/ix/kernel/def_eq.rs def_eq.rs src/ix/kernel/egress.rs egress.rs src/ix/kernel/env.rs env.rs src/ix/kernel/equiv.rs equiv.rs src/ix/kernel/error.rs error.rs src/ix/kernel/expr.rs expr.rs src/ix/kernel/id.rs id.rs src/ix/kernel/inductive.rs inductive.rs src/ix/kernel/infer.rs infer.rs src/ix/kernel/ingress.rs ingress.rs src/ix/kernel/lctx.rs lctx.rs src/ix/kernel/level.rs level.rs src/ix/kernel/mode.rs mode.rs src/ix/kernel/perf.rs perf.rs src/ix/kernel/primitive.rs primitive.rs src/ix/kernel/subst.rs subst.rs src/ix/kernel/tc.rs tc.rs src/ix/kernel/testing.rs testing.rs src/ix/kernel/tutorial/basic.rs basic.rs src/ix/kernel/tutorial/defeq.rs defeq.rs src/ix/kernel/tutorial/inductive.rs inductive.rs src/ix/kernel/tutorial/mod.rs mod.rs src/ix/kernel/tutorial/reduction.rs reduction.rs src/ix/kernel/whnf.rs whnf.rs src/lean.rs lean.rs src/lib.rs lib.rs There are no files selected for viewing 31 changes: 31 additions & 0 deletions 31 .github/valgrind.supp Show comments View file Open in desktop Original file line number Diff line number Diff line change @@ -0,0 +1,31 @@ { mimalloc-prim-mem-init-uninit-cond Memcheck:Cond fun:_mi_strnlen fun:_mi_strnstr fun:_mi_prim_mem_init fun:mi_process_init ... } { mimalloc-prim-mem-init-uninit-value8 Memcheck:Value8 fun:_mi_strnlen fun:_mi_strnstr fun:_mi_prim_mem_init fun:mi_process_init ... } { glibc-pthread-create-tls-dtv Memcheck:Leak match-leak-kinds: possible fun:calloc fun:allocate_dtv fun:_dl_allocate_tls ... fun:pthread_create* ... } 8 changes: 7 additions & 1 deletion 8 .github/workflows/ignored.yml Show comments View file Open in desktop Original file line number Diff line number Diff line change Expand Up @@ -53,7 +53,12 @@ jobs: build-args: "IxTests" use-github-cache: false - name: Install valgrind run: sudo apt-get update && sudo apt-get install -y valgrind run: | # Some warpbuild images ship a mirrorlist with an unreachable # azure.archive.ubuntu.com entry, causing apt-get update to stall indefinitely. sudo sed -i '/azure\.archive\.ubuntu\.com/d' /etc/apt/apt-mirrors.txt 2>/dev/null || true sudo apt-get update sudo apt-get install -y valgrind - name: Run tests under valgrind run: | valgrind \ Expand All @@ -62,4 +67,5 @@ jobs: --errors-for-leak-kinds=definite \ --track-origins=yes \ --error-exitcode=1 \ --suppressions=.github/valgrind.supp \ .lake/build/bin/IxTests -- ffi Loading Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later. Footer © 2026 GitHub, Inc. Footer navigation Terms Privacy Security Status Community Docs Contact You can’t perform that action at this time. , '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 contentNavigation Menu Sign inAppearance settings AI CODE CREATIONGitHub CopilotWrite better code with AI GitHub Copilot appDirect agents from issue to merge MCP RegistryIntegrate external tools DEVELOPER WORKFLOWSActionsAutomate any workflow CodespacesInstant dev environments IssuesPlan and track work Code ReviewManage code changes Code QualityEnforce quality at merge APPLICATION SECURITYGitHub Advanced SecurityFind and fix vulnerabilities Code securitySecure your code as you build Secret protectionStop leaks before they start EXPLOREWhy GitHub Documentation Blog Changelog Marketplace View all features BY COMPANY SIZEEnterprises Small and medium teams Startups Nonprofits BY USE CASEApp Modernization DevSecOps DevOps CI/CD View all use cases BY INDUSTRYHealthcare Financial services Manufacturing Government View all industries View all solutions EXPLORE BY TOPICAI Software Development DevOps Security View all topics EXPLORE BY TYPECustomer stories Events & webinars Ebooks & reports Business insights GitHub Skills SUPPORT & SERVICESDocumentation Customer support Community forum Trust center Partners View all resources COMMUNITYGitHub SponsorsFund open source developers PROGRAMSSecurity Lab Maintainer Community GitHub Stars Archive Program REPOSITORIESTopics Trending Collections ENTERPRISE SOLUTIONSEnterprise platformAI-powered developer platform AVAILABLE ADD-ONSGitHub Advanced SecurityEnterprise-grade security features Copilot for BusinessEnterprise-grade AI features Premium SupportEnterprise-grade 24/7 support Pricing Sign in Sign upAppearance settings You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert Uh oh! There was an error while loading. Please reload this page. argumentcomputer /ixPublic Notifications You must be signed in to change notification settings Fork 3 Star 91 Code Issues10 Pull requests14 Actions Projects Security and quality0 Insights Additional navigation options Code Issues Pull requests Actions Projects Security and quality Insights Add kernel type-checker#375 New issue Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community. Sign up for GitHub By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails. Already on GitHub? Sign in to your account Merged johnchandlerburnham merged 35 commits into main from jcb/kernelMay 7, 2026 Conversation 7 Commits 35 Checks 14 Files changed Uh oh! There was an error while loading. Please reload this page. Merged Add kernel type-checker #375 Show file tree Hide file tree Changes from all commits Commits Show all changes 35 commits Select commit Hold shift + click to select a range 8024807 Add kernel type-checker and restructure ConstantMeta for aux_gen johnchandlerburnham Apr 12, 20265fb6a7a Extract compile_env scheduler and resolve all cargo xclippy warnings johnchandlerburnham Apr 12, 2026142cc5e Add canonical aux_gen pipeline for alpha-collapsed inductive blocks johnchandlerburnham Apr 13, 2026718a0e6 fmt johnchandlerburnham Apr 13, 20264fa8cfa refactor validate-aux test johnchandlerburnham Apr 13, 2026114be51 fix Ixon Lean serialization johnchandlerburnham Apr 13, 20265d54533 Lift kernel caches into Arc<KEnv> and switch to content-addressed cac… johnchandlerburnham Apr 15, 2026f0bceac Call-site surgery, aux_gen cleanup, and Env Arc refactor johnchandlerburnham Apr 17, 2026e4579e0 solve mathlib compilation and ingress roundtrip issues johnchandlerburnham Apr 17, 202605bdf10 Close the Mathlib aux_gen congruence loop: CompileMathlib.lean passes johnchandlerburnham Apr 19, 2026a034db2 Kernel soundness hardening, two-env split, Int native reduction, tole… johnchandlerburnham Apr 21, 2026ec05c94 Anonymous canonicity: aux permutation sidecar, perm-aware congruence,… johnchandlerburnham Apr 24, 2026a37d592 Kernel-side canonicity validation and full-env check pipeline johnchandlerburnham Apr 26, 202626c3be7 xclippy warnings johnchandlerburnham Apr 26, 202656e3e79 Stream ixon_ingress into KEnv; own-and-drop IxonEnv before kernel check johnchandlerburnham Apr 27, 2026c749b58 Add IX_PERF_COUNTERS instrumentation for kernel cache hit rates johnchandlerburnham Apr 27, 20261847240 kernel: add cheap projection def-eq WHNF safely johnchandlerburnham Apr 27, 2026508ca82 Speed up kernel validation and refine infer cache keys johnchandlerburnham Apr 27, 20261dfafd5 Add `ix ingress` CLI; expand kernel caches; parallel-shard env drops johnchandlerburnham Apr 28, 20264b2409d Speed up ixon_ingress: hash-first interning + 2048-shard intern table johnchandlerburnham Apr 28, 2026ec95312 Align nested-aux canonical order between compile and kernel johnchandlerburnham Apr 28, 20261d930c8 kernel: fix over-discovery in build_flat_block johnchandlerburnham Apr 28, 20264951b0d kernel: per-worker KEnv with lazy Ixon ingress; add `ix check-ixon` CLI johnchandlerburnham Apr 29, 20268f15dc0 kernel: add FVar binder opening, alpha-invariant hashing, Nat reduc… johnchandlerburnham Apr 30, 2026aea118d fmt & clippy johnchandlerburnham May 1, 20266e802ce Merge branch 'main' of github.com:argumentcomputer/ix into jcb/kernel johnchandlerburnham May 1, 20265b14e5c aux_gen: alpha-collapse-aware roundtrip + alias-only patching johnchandlerburnham May 1, 2026d9e0fbb aux_gen: source-shape-preserving WHNF + Phase 1 cache prewarming johnchandlerburnham May 1, 2026ef4b061 `decide` is enough to prove `Aiur.G.one_ne_zero` arthurpaulino May 4, 2026a289432 Update docs/ix_canonicity.md johnchandlerburnham May 5, 20262d5cabd xclippy warnings johnchandlerburnham May 5, 2026e5d5a34 fix aux_gen test johnchandlerburnham May 5, 20269d132ef comment out ixvm tests arthurpaulino May 6, 20266e4d1ad chore: Fix lean-ffi (#395) samuelburnham May 6, 2026bef77b1 ci: Fix valgrind samuelburnham May 6, 2026 File filter Filter by extension Filter by extension .lean (33) .lock (1) .md (1) .rs (65) .supp (1) .toml (2) .yml (1) All 7 file types selected Only manifest files Viewed files Clear filters Conversations Failed to load comments. Loading Uh oh! There was an error while loading. Please reload this page. Jump to Jump to file Failed to load files. Loading Uh oh! There was an error while loading. Please reload this page. Diff view Unified Split Hide whitespace Diff view Unified Split Hide whitespace .github/valgrind.supp valgrind.supp .github/workflows/ignored.yml ignored.yml Cargo.lock Cargo.lock Cargo.toml Cargo.toml Ix.lean Ix.lean Ix/Aiur/Goldilocks.lean Goldilocks.lean Ix/Cli/CheckCmd.lean CheckCmd.lean Ix/Cli/CheckIxonCmd.lean CheckIxonCmd.lean Ix/Cli/CompileCmd.lean CompileCmd.lean Ix/Cli/IngressCmd.lean IngressCmd.lean Ix/Cli/ValidateCmd.lean ValidateCmd.lean Ix/Commit.lean Commit.lean Ix/CompileM.lean CompileM.lean Ix/DecompileM.lean DecompileM.lean Ix/Ixon.lean Ixon.lean Ix/KernelCheck.lean KernelCheck.lean Ix/Meta.lean Meta.lean Main.lean Main.lean Tests/FFI.lean FFI.lean Tests/FFI/Ixon.lean Ixon.lean Tests/FFI/Lifecycle.lean Lifecycle.lean Tests/Gen/Ixon.lean Ixon.lean Tests/Ix/Compile.lean Compile.lean Tests/Ix/Compile/Canonicity.lean Canonicity.lean Tests/Ix/Compile/Mutual.lean Mutual.lean Tests/Ix/Compile/ValidateAux.lean ValidateAux.lean Tests/Ix/Kernel/BuildPrimOrigs.lean BuildPrimOrigs.lean Tests/Ix/Kernel/BuildPrimitives.lean BuildPrimitives.lean Tests/Ix/Kernel/CheckEnv.lean CheckEnv.lean Tests/Ix/Kernel/NatReduction.lean NatReduction.lean Tests/Ix/Kernel/Roundtrip.lean Roundtrip.lean Tests/Ix/Kernel/RoundtripNoCompile.lean RoundtripNoCompile.lean Tests/Ix/Kernel/Tutorial.lean Tutorial.lean Tests/Ix/Kernel/TutorialDefs.lean TutorialDefs.lean Tests/Ix/Kernel/TutorialMeta.lean TutorialMeta.lean Tests/Main.lean Main.lean deny.toml deny.toml docs/ix_canonicity.md ix_canonicity.md lakefile.lean lakefile.lean src/ffi.rs ffi.rs src/ffi/compile.rs compile.rs src/ffi/ix/env.rs env.rs src/ffi/ixon/meta.rs meta.rs src/ffi/ixon/serialize.rs serialize.rs src/ffi/ixon/sharing.rs sharing.rs src/ffi/kernel.rs kernel.rs src/ffi/lean_env.rs lean_env.rs src/ix.rs ix.rs src/ix/address.rs address.rs src/ix/compile.rs compile.rs src/ix/compile/aux_gen.rs aux_gen.rs src/ix/compile/aux_gen/below.rs below.rs src/ix/compile/aux_gen/brecon.rs brecon.rs src/ix/compile/aux_gen/cases_on.rs cases_on.rs src/ix/compile/aux_gen/expr_utils.rs expr_utils.rs src/ix/compile/aux_gen/nested.rs nested.rs src/ix/compile/aux_gen/rec_on.rs rec_on.rs src/ix/compile/aux_gen/recursor.rs recursor.rs src/ix/compile/env.rs env.rs src/ix/compile/mutual.rs mutual.rs src/ix/compile/nat_conv.rs nat_conv.rs src/ix/compile/surgery.rs surgery.rs src/ix/congruence.rs congruence.rs src/ix/congruence/perm.rs perm.rs src/ix/decompile.rs decompile.rs src/ix/env.rs env.rs src/ix/graph.rs graph.rs src/ix/ground.rs ground.rs src/ix/ixon/env.rs env.rs src/ix/ixon/error.rs error.rs src/ix/ixon/metadata.rs metadata.rs src/ix/ixon/serialize.rs serialize.rs src/ix/ixon/sharing.rs sharing.rs src/ix/kernel.rs kernel.rs src/ix/kernel/canonical_check.rs canonical_check.rs src/ix/kernel/check.rs check.rs src/ix/kernel/congruence.rs congruence.rs src/ix/kernel/constant.rs constant.rs src/ix/kernel/def_eq.rs def_eq.rs src/ix/kernel/egress.rs egress.rs src/ix/kernel/env.rs env.rs src/ix/kernel/equiv.rs equiv.rs src/ix/kernel/error.rs error.rs src/ix/kernel/expr.rs expr.rs src/ix/kernel/id.rs id.rs src/ix/kernel/inductive.rs inductive.rs src/ix/kernel/infer.rs infer.rs src/ix/kernel/ingress.rs ingress.rs src/ix/kernel/lctx.rs lctx.rs src/ix/kernel/level.rs level.rs src/ix/kernel/mode.rs mode.rs src/ix/kernel/perf.rs perf.rs src/ix/kernel/primitive.rs primitive.rs src/ix/kernel/subst.rs subst.rs src/ix/kernel/tc.rs tc.rs src/ix/kernel/testing.rs testing.rs src/ix/kernel/tutorial/basic.rs basic.rs src/ix/kernel/tutorial/defeq.rs defeq.rs src/ix/kernel/tutorial/inductive.rs inductive.rs src/ix/kernel/tutorial/mod.rs mod.rs src/ix/kernel/tutorial/reduction.rs reduction.rs src/ix/kernel/whnf.rs whnf.rs src/lean.rs lean.rs src/lib.rs lib.rs There are no files selected for viewing 31 changes: 31 additions & 0 deletions 31 .github/valgrind.supp Show comments View file Open in desktop Original file line number Diff line number Diff line change @@ -0,0 +1,31 @@ { mimalloc-prim-mem-init-uninit-cond Memcheck:Cond fun:_mi_strnlen fun:_mi_strnstr fun:_mi_prim_mem_init fun:mi_process_init ... } { mimalloc-prim-mem-init-uninit-value8 Memcheck:Value8 fun:_mi_strnlen fun:_mi_strnstr fun:_mi_prim_mem_init fun:mi_process_init ... } { glibc-pthread-create-tls-dtv Memcheck:Leak match-leak-kinds: possible fun:calloc fun:allocate_dtv fun:_dl_allocate_tls ... fun:pthread_create* ... } 8 changes: 7 additions & 1 deletion 8 .github/workflows/ignored.yml Show comments View file Open in desktop Original file line number Diff line number Diff line change Expand Up @@ -53,7 +53,12 @@ jobs: build-args: "IxTests" use-github-cache: false - name: Install valgrind run: sudo apt-get update && sudo apt-get install -y valgrind run: | # Some warpbuild images ship a mirrorlist with an unreachable # azure.archive.ubuntu.com entry, causing apt-get update to stall indefinitely. sudo sed -i '/azure\.archive\.ubuntu\.com/d' /etc/apt/apt-mirrors.txt 2>/dev/null || true sudo apt-get update sudo apt-get install -y valgrind - name: Run tests under valgrind run: | valgrind \ Expand All @@ -62,4 +67,5 @@ jobs: --errors-for-leak-kinds=definite \ --track-origins=yes \ --error-exitcode=1 \ --suppressions=.github/valgrind.supp \ .lake/build/bin/IxTests -- ffi Loading Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later. Footer © 2026 GitHub, Inc. Footer navigation Terms Privacy Security Status Community Docs Contact You can’t perform that action at this time. , '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 contentNavigation Menu Sign inAppearance settings AI CODE CREATIONGitHub CopilotWrite better code with AI GitHub Copilot appDirect agents from issue to merge MCP RegistryIntegrate external tools DEVELOPER WORKFLOWSActionsAutomate any workflow CodespacesInstant dev environments IssuesPlan and track work Code ReviewManage code changes Code QualityEnforce quality at merge APPLICATION SECURITYGitHub Advanced SecurityFind and fix vulnerabilities Code securitySecure your code as you build Secret protectionStop leaks before they start EXPLOREWhy GitHub Documentation Blog Changelog Marketplace View all features BY COMPANY SIZEEnterprises Small and medium teams Startups Nonprofits BY USE CASEApp Modernization DevSecOps DevOps CI/CD View all use cases BY INDUSTRYHealthcare Financial services Manufacturing Government View all industries View all solutions EXPLORE BY TOPICAI Software Development DevOps Security View all topics EXPLORE BY TYPECustomer stories Events & webinars Ebooks & reports Business insights GitHub Skills SUPPORT & SERVICESDocumentation Customer support Community forum Trust center Partners View all resources COMMUNITYGitHub SponsorsFund open source developers PROGRAMSSecurity Lab Maintainer Community GitHub Stars Archive Program REPOSITORIESTopics Trending Collections ENTERPRISE SOLUTIONSEnterprise platformAI-powered developer platform AVAILABLE ADD-ONSGitHub Advanced SecurityEnterprise-grade security features Copilot for BusinessEnterprise-grade AI features Premium SupportEnterprise-grade 24/7 support Pricing Sign in Sign upAppearance settings You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert Uh oh! There was an error while loading. Please reload this page. argumentcomputer /ixPublic Notifications You must be signed in to change notification settings Fork 3 Star 91 Code Issues10 Pull requests14 Actions Projects Security and quality0 Insights Additional navigation options Code Issues Pull requests Actions Projects Security and quality Insights Add kernel type-checker#375 New issue Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community. Sign up for GitHub By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails. Already on GitHub? Sign in to your account Merged johnchandlerburnham merged 35 commits into main from jcb/kernelMay 7, 2026 Conversation 7 Commits 35 Checks 14 Files changed Uh oh! There was an error while loading. Please reload this page. Merged Add kernel type-checker #375 Show file tree Hide file tree Changes from all commits Commits Show all changes 35 commits Select commit Hold shift + click to select a range 8024807 Add kernel type-checker and restructure ConstantMeta for aux_gen johnchandlerburnham Apr 12, 20265fb6a7a Extract compile_env scheduler and resolve all cargo xclippy warnings johnchandlerburnham Apr 12, 2026142cc5e Add canonical aux_gen pipeline for alpha-collapsed inductive blocks johnchandlerburnham Apr 13, 2026718a0e6 fmt johnchandlerburnham Apr 13, 20264fa8cfa refactor validate-aux test johnchandlerburnham Apr 13, 2026114be51 fix Ixon Lean serialization johnchandlerburnham Apr 13, 20265d54533 Lift kernel caches into Arc<KEnv> and switch to content-addressed cac… johnchandlerburnham Apr 15, 2026f0bceac Call-site surgery, aux_gen cleanup, and Env Arc refactor johnchandlerburnham Apr 17, 2026e4579e0 solve mathlib compilation and ingress roundtrip issues johnchandlerburnham Apr 17, 202605bdf10 Close the Mathlib aux_gen congruence loop: CompileMathlib.lean passes johnchandlerburnham Apr 19, 2026a034db2 Kernel soundness hardening, two-env split, Int native reduction, tole… johnchandlerburnham Apr 21, 2026ec05c94 Anonymous canonicity: aux permutation sidecar, perm-aware congruence,… johnchandlerburnham Apr 24, 2026a37d592 Kernel-side canonicity validation and full-env check pipeline johnchandlerburnham Apr 26, 202626c3be7 xclippy warnings johnchandlerburnham Apr 26, 202656e3e79 Stream ixon_ingress into KEnv; own-and-drop IxonEnv before kernel check johnchandlerburnham Apr 27, 2026c749b58 Add IX_PERF_COUNTERS instrumentation for kernel cache hit rates johnchandlerburnham Apr 27, 20261847240 kernel: add cheap projection def-eq WHNF safely johnchandlerburnham Apr 27, 2026508ca82 Speed up kernel validation and refine infer cache keys johnchandlerburnham Apr 27, 20261dfafd5 Add `ix ingress` CLI; expand kernel caches; parallel-shard env drops johnchandlerburnham Apr 28, 20264b2409d Speed up ixon_ingress: hash-first interning + 2048-shard intern table johnchandlerburnham Apr 28, 2026ec95312 Align nested-aux canonical order between compile and kernel johnchandlerburnham Apr 28, 20261d930c8 kernel: fix over-discovery in build_flat_block johnchandlerburnham Apr 28, 20264951b0d kernel: per-worker KEnv with lazy Ixon ingress; add `ix check-ixon` CLI johnchandlerburnham Apr 29, 20268f15dc0 kernel: add FVar binder opening, alpha-invariant hashing, Nat reduc… johnchandlerburnham Apr 30, 2026aea118d fmt & clippy johnchandlerburnham May 1, 20266e802ce Merge branch 'main' of github.com:argumentcomputer/ix into jcb/kernel johnchandlerburnham May 1, 20265b14e5c aux_gen: alpha-collapse-aware roundtrip + alias-only patching johnchandlerburnham May 1, 2026d9e0fbb aux_gen: source-shape-preserving WHNF + Phase 1 cache prewarming johnchandlerburnham May 1, 2026ef4b061 `decide` is enough to prove `Aiur.G.one_ne_zero` arthurpaulino May 4, 2026a289432 Update docs/ix_canonicity.md johnchandlerburnham May 5, 20262d5cabd xclippy warnings johnchandlerburnham May 5, 2026e5d5a34 fix aux_gen test johnchandlerburnham May 5, 20269d132ef comment out ixvm tests arthurpaulino May 6, 20266e4d1ad chore: Fix lean-ffi (#395) samuelburnham May 6, 2026bef77b1 ci: Fix valgrind samuelburnham May 6, 2026 File filter Filter by extension Filter by extension .lean (33) .lock (1) .md (1) .rs (65) .supp (1) .toml (2) .yml (1) All 7 file types selected Only manifest files Viewed files Clear filters Conversations Failed to load comments. Loading Uh oh! There was an error while loading. Please reload this page. Jump to Jump to file Failed to load files. Loading Uh oh! There was an error while loading. Please reload this page. Diff view Unified Split Hide whitespace Diff view Unified Split Hide whitespace .github/valgrind.supp valgrind.supp .github/workflows/ignored.yml ignored.yml Cargo.lock Cargo.lock Cargo.toml Cargo.toml Ix.lean Ix.lean Ix/Aiur/Goldilocks.lean Goldilocks.lean Ix/Cli/CheckCmd.lean CheckCmd.lean Ix/Cli/CheckIxonCmd.lean CheckIxonCmd.lean Ix/Cli/CompileCmd.lean CompileCmd.lean Ix/Cli/IngressCmd.lean IngressCmd.lean Ix/Cli/ValidateCmd.lean ValidateCmd.lean Ix/Commit.lean Commit.lean Ix/CompileM.lean CompileM.lean Ix/DecompileM.lean DecompileM.lean Ix/Ixon.lean Ixon.lean Ix/KernelCheck.lean KernelCheck.lean Ix/Meta.lean Meta.lean Main.lean Main.lean Tests/FFI.lean FFI.lean Tests/FFI/Ixon.lean Ixon.lean Tests/FFI/Lifecycle.lean Lifecycle.lean Tests/Gen/Ixon.lean Ixon.lean Tests/Ix/Compile.lean Compile.lean Tests/Ix/Compile/Canonicity.lean Canonicity.lean Tests/Ix/Compile/Mutual.lean Mutual.lean Tests/Ix/Compile/ValidateAux.lean ValidateAux.lean Tests/Ix/Kernel/BuildPrimOrigs.lean BuildPrimOrigs.lean Tests/Ix/Kernel/BuildPrimitives.lean BuildPrimitives.lean Tests/Ix/Kernel/CheckEnv.lean CheckEnv.lean Tests/Ix/Kernel/NatReduction.lean NatReduction.lean Tests/Ix/Kernel/Roundtrip.lean Roundtrip.lean Tests/Ix/Kernel/RoundtripNoCompile.lean RoundtripNoCompile.lean Tests/Ix/Kernel/Tutorial.lean Tutorial.lean Tests/Ix/Kernel/TutorialDefs.lean TutorialDefs.lean Tests/Ix/Kernel/TutorialMeta.lean TutorialMeta.lean Tests/Main.lean Main.lean deny.toml deny.toml docs/ix_canonicity.md ix_canonicity.md lakefile.lean lakefile.lean src/ffi.rs ffi.rs src/ffi/compile.rs compile.rs src/ffi/ix/env.rs env.rs src/ffi/ixon/meta.rs meta.rs src/ffi/ixon/serialize.rs serialize.rs src/ffi/ixon/sharing.rs sharing.rs src/ffi/kernel.rs kernel.rs src/ffi/lean_env.rs lean_env.rs src/ix.rs ix.rs src/ix/address.rs address.rs src/ix/compile.rs compile.rs src/ix/compile/aux_gen.rs aux_gen.rs src/ix/compile/aux_gen/below.rs below.rs src/ix/compile/aux_gen/brecon.rs brecon.rs src/ix/compile/aux_gen/cases_on.rs cases_on.rs src/ix/compile/aux_gen/expr_utils.rs expr_utils.rs src/ix/compile/aux_gen/nested.rs nested.rs src/ix/compile/aux_gen/rec_on.rs rec_on.rs src/ix/compile/aux_gen/recursor.rs recursor.rs src/ix/compile/env.rs env.rs src/ix/compile/mutual.rs mutual.rs src/ix/compile/nat_conv.rs nat_conv.rs src/ix/compile/surgery.rs surgery.rs src/ix/congruence.rs congruence.rs src/ix/congruence/perm.rs perm.rs src/ix/decompile.rs decompile.rs src/ix/env.rs env.rs src/ix/graph.rs graph.rs src/ix/ground.rs ground.rs src/ix/ixon/env.rs env.rs src/ix/ixon/error.rs error.rs src/ix/ixon/metadata.rs metadata.rs src/ix/ixon/serialize.rs serialize.rs src/ix/ixon/sharing.rs sharing.rs src/ix/kernel.rs kernel.rs src/ix/kernel/canonical_check.rs canonical_check.rs src/ix/kernel/check.rs check.rs src/ix/kernel/congruence.rs congruence.rs src/ix/kernel/constant.rs constant.rs src/ix/kernel/def_eq.rs def_eq.rs src/ix/kernel/egress.rs egress.rs src/ix/kernel/env.rs env.rs src/ix/kernel/equiv.rs equiv.rs src/ix/kernel/error.rs error.rs src/ix/kernel/expr.rs expr.rs src/ix/kernel/id.rs id.rs src/ix/kernel/inductive.rs inductive.rs src/ix/kernel/infer.rs infer.rs src/ix/kernel/ingress.rs ingress.rs src/ix/kernel/lctx.rs lctx.rs src/ix/kernel/level.rs level.rs src/ix/kernel/mode.rs mode.rs src/ix/kernel/perf.rs perf.rs src/ix/kernel/primitive.rs primitive.rs src/ix/kernel/subst.rs subst.rs src/ix/kernel/tc.rs tc.rs src/ix/kernel/testing.rs testing.rs src/ix/kernel/tutorial/basic.rs basic.rs src/ix/kernel/tutorial/defeq.rs defeq.rs src/ix/kernel/tutorial/inductive.rs inductive.rs src/ix/kernel/tutorial/mod.rs mod.rs src/ix/kernel/tutorial/reduction.rs reduction.rs src/ix/kernel/whnf.rs whnf.rs src/lean.rs lean.rs src/lib.rs lib.rs There are no files selected for viewing 31 changes: 31 additions & 0 deletions 31 .github/valgrind.supp Show comments View file Open in desktop Original file line number Diff line number Diff line change @@ -0,0 +1,31 @@ { mimalloc-prim-mem-init-uninit-cond Memcheck:Cond fun:_mi_strnlen fun:_mi_strnstr fun:_mi_prim_mem_init fun:mi_process_init ... } { mimalloc-prim-mem-init-uninit-value8 Memcheck:Value8 fun:_mi_strnlen fun:_mi_strnstr fun:_mi_prim_mem_init fun:mi_process_init ... } { glibc-pthread-create-tls-dtv Memcheck:Leak match-leak-kinds: possible fun:calloc fun:allocate_dtv fun:_dl_allocate_tls ... fun:pthread_create* ... } 8 changes: 7 additions & 1 deletion 8 .github/workflows/ignored.yml Show comments View file Open in desktop Original file line number Diff line number Diff line change Expand Up @@ -53,7 +53,12 @@ jobs: build-args: "IxTests" use-github-cache: false - name: Install valgrind run: sudo apt-get update && sudo apt-get install -y valgrind run: | # Some warpbuild images ship a mirrorlist with an unreachable # azure.archive.ubuntu.com entry, causing apt-get update to stall indefinitely. sudo sed -i '/azure\.archive\.ubuntu\.com/d' /etc/apt/apt-mirrors.txt 2>/dev/null || true sudo apt-get update sudo apt-get install -y valgrind - name: Run tests under valgrind run: | valgrind \ Expand All @@ -62,4 +67,5 @@ jobs: --errors-for-leak-kinds=definite \ --track-origins=yes \ --error-exitcode=1 \ --suppressions=.github/valgrind.supp \ .lake/build/bin/IxTests -- ffi Loading Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later. Footer © 2026 GitHub, Inc. Footer navigation Terms Privacy Security Status Community Docs Contact You can’t perform that action at this time. , '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 contentNavigation Menu Sign inAppearance settings AI CODE CREATIONGitHub CopilotWrite better code with AI GitHub Copilot appDirect agents from issue to merge MCP RegistryIntegrate external tools DEVELOPER WORKFLOWSActionsAutomate any workflow CodespacesInstant dev environments IssuesPlan and track work Code ReviewManage code changes Code QualityEnforce quality at merge APPLICATION SECURITYGitHub Advanced SecurityFind and fix vulnerabilities Code securitySecure your code as you build Secret protectionStop leaks before they start EXPLOREWhy GitHub Documentation Blog Changelog Marketplace View all features BY COMPANY SIZEEnterprises Small and medium teams Startups Nonprofits BY USE CASEApp Modernization DevSecOps DevOps CI/CD View all use cases BY INDUSTRYHealthcare Financial services Manufacturing Government View all industries View all solutions EXPLORE BY TOPICAI Software Development DevOps Security View all topics EXPLORE BY TYPECustomer stories Events & webinars Ebooks & reports Business insights GitHub Skills SUPPORT & SERVICESDocumentation Customer support Community forum Trust center Partners View all resources COMMUNITYGitHub SponsorsFund open source developers PROGRAMSSecurity Lab Maintainer Community GitHub Stars Archive Program REPOSITORIESTopics Trending Collections ENTERPRISE SOLUTIONSEnterprise platformAI-powered developer platform AVAILABLE ADD-ONSGitHub Advanced SecurityEnterprise-grade security features Copilot for BusinessEnterprise-grade AI features Premium SupportEnterprise-grade 24/7 support Pricing Sign in Sign upAppearance settings You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert Uh oh! There was an error while loading. Please reload this page. argumentcomputer /ixPublic Notifications You must be signed in to change notification settings Fork 3 Star 91 Code Issues10 Pull requests14 Actions Projects Security and quality0 Insights Additional navigation options Code Issues Pull requests Actions Projects Security and quality Insights Add kernel type-checker#375 New issue Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community. Sign up for GitHub By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails. Already on GitHub? Sign in to your account Merged johnchandlerburnham merged 35 commits into main from jcb/kernelMay 7, 2026 Conversation 7 Commits 35 Checks 14 Files changed Uh oh! There was an error while loading. Please reload this page. Merged Add kernel type-checker #375 Show file tree Hide file tree Changes from all commits Commits Show all changes 35 commits Select commit Hold shift + click to select a range 8024807 Add kernel type-checker and restructure ConstantMeta for aux_gen johnchandlerburnham Apr 12, 20265fb6a7a Extract compile_env scheduler and resolve all cargo xclippy warnings johnchandlerburnham Apr 12, 2026142cc5e Add canonical aux_gen pipeline for alpha-collapsed inductive blocks johnchandlerburnham Apr 13, 2026718a0e6 fmt johnchandlerburnham Apr 13, 20264fa8cfa refactor validate-aux test johnchandlerburnham Apr 13, 2026114be51 fix Ixon Lean serialization johnchandlerburnham Apr 13, 20265d54533 Lift kernel caches into Arc<KEnv> and switch to content-addressed cac… johnchandlerburnham Apr 15, 2026f0bceac Call-site surgery, aux_gen cleanup, and Env Arc refactor johnchandlerburnham Apr 17, 2026e4579e0 solve mathlib compilation and ingress roundtrip issues johnchandlerburnham Apr 17, 202605bdf10 Close the Mathlib aux_gen congruence loop: CompileMathlib.lean passes johnchandlerburnham Apr 19, 2026a034db2 Kernel soundness hardening, two-env split, Int native reduction, tole… johnchandlerburnham Apr 21, 2026ec05c94 Anonymous canonicity: aux permutation sidecar, perm-aware congruence,… johnchandlerburnham Apr 24, 2026a37d592 Kernel-side canonicity validation and full-env check pipeline johnchandlerburnham Apr 26, 202626c3be7 xclippy warnings johnchandlerburnham Apr 26, 202656e3e79 Stream ixon_ingress into KEnv; own-and-drop IxonEnv before kernel check johnchandlerburnham Apr 27, 2026c749b58 Add IX_PERF_COUNTERS instrumentation for kernel cache hit rates johnchandlerburnham Apr 27, 20261847240 kernel: add cheap projection def-eq WHNF safely johnchandlerburnham Apr 27, 2026508ca82 Speed up kernel validation and refine infer cache keys johnchandlerburnham Apr 27, 20261dfafd5 Add `ix ingress` CLI; expand kernel caches; parallel-shard env drops johnchandlerburnham Apr 28, 20264b2409d Speed up ixon_ingress: hash-first interning + 2048-shard intern table johnchandlerburnham Apr 28, 2026ec95312 Align nested-aux canonical order between compile and kernel johnchandlerburnham Apr 28, 20261d930c8 kernel: fix over-discovery in build_flat_block johnchandlerburnham Apr 28, 20264951b0d kernel: per-worker KEnv with lazy Ixon ingress; add `ix check-ixon` CLI johnchandlerburnham Apr 29, 20268f15dc0 kernel: add FVar binder opening, alpha-invariant hashing, Nat reduc… johnchandlerburnham Apr 30, 2026aea118d fmt & clippy johnchandlerburnham May 1, 20266e802ce Merge branch 'main' of github.com:argumentcomputer/ix into jcb/kernel johnchandlerburnham May 1, 20265b14e5c aux_gen: alpha-collapse-aware roundtrip + alias-only patching johnchandlerburnham May 1, 2026d9e0fbb aux_gen: source-shape-preserving WHNF + Phase 1 cache prewarming johnchandlerburnham May 1, 2026ef4b061 `decide` is enough to prove `Aiur.G.one_ne_zero` arthurpaulino May 4, 2026a289432 Update docs/ix_canonicity.md johnchandlerburnham May 5, 20262d5cabd xclippy warnings johnchandlerburnham May 5, 2026e5d5a34 fix aux_gen test johnchandlerburnham May 5, 20269d132ef comment out ixvm tests arthurpaulino May 6, 20266e4d1ad chore: Fix lean-ffi (#395) samuelburnham May 6, 2026bef77b1 ci: Fix valgrind samuelburnham May 6, 2026 File filter Filter by extension Filter by extension .lean (33) .lock (1) .md (1) .rs (65) .supp (1) .toml (2) .yml (1) All 7 file types selected Only manifest files Viewed files Clear filters Conversations Failed to load comments. Loading Uh oh! There was an error while loading. Please reload this page. Jump to Jump to file Failed to load files. Loading Uh oh! There was an error while loading. Please reload this page. Diff view Unified Split Hide whitespace Diff view Unified Split Hide whitespace .github/valgrind.supp valgrind.supp .github/workflows/ignored.yml ignored.yml Cargo.lock Cargo.lock Cargo.toml Cargo.toml Ix.lean Ix.lean Ix/Aiur/Goldilocks.lean Goldilocks.lean Ix/Cli/CheckCmd.lean CheckCmd.lean Ix/Cli/CheckIxonCmd.lean CheckIxonCmd.lean Ix/Cli/CompileCmd.lean CompileCmd.lean Ix/Cli/IngressCmd.lean IngressCmd.lean Ix/Cli/ValidateCmd.lean ValidateCmd.lean Ix/Commit.lean Commit.lean Ix/CompileM.lean CompileM.lean Ix/DecompileM.lean DecompileM.lean Ix/Ixon.lean Ixon.lean Ix/KernelCheck.lean KernelCheck.lean Ix/Meta.lean Meta.lean Main.lean Main.lean Tests/FFI.lean FFI.lean Tests/FFI/Ixon.lean Ixon.lean Tests/FFI/Lifecycle.lean Lifecycle.lean Tests/Gen/Ixon.lean Ixon.lean Tests/Ix/Compile.lean Compile.lean Tests/Ix/Compile/Canonicity.lean Canonicity.lean Tests/Ix/Compile/Mutual.lean Mutual.lean Tests/Ix/Compile/ValidateAux.lean ValidateAux.lean Tests/Ix/Kernel/BuildPrimOrigs.lean BuildPrimOrigs.lean Tests/Ix/Kernel/BuildPrimitives.lean BuildPrimitives.lean Tests/Ix/Kernel/CheckEnv.lean CheckEnv.lean Tests/Ix/Kernel/NatReduction.lean NatReduction.lean Tests/Ix/Kernel/Roundtrip.lean Roundtrip.lean Tests/Ix/Kernel/RoundtripNoCompile.lean RoundtripNoCompile.lean Tests/Ix/Kernel/Tutorial.lean Tutorial.lean Tests/Ix/Kernel/TutorialDefs.lean TutorialDefs.lean Tests/Ix/Kernel/TutorialMeta.lean TutorialMeta.lean Tests/Main.lean Main.lean deny.toml deny.toml docs/ix_canonicity.md ix_canonicity.md lakefile.lean lakefile.lean src/ffi.rs ffi.rs src/ffi/compile.rs compile.rs src/ffi/ix/env.rs env.rs src/ffi/ixon/meta.rs meta.rs src/ffi/ixon/serialize.rs serialize.rs src/ffi/ixon/sharing.rs sharing.rs src/ffi/kernel.rs kernel.rs src/ffi/lean_env.rs lean_env.rs src/ix.rs ix.rs src/ix/address.rs address.rs src/ix/compile.rs compile.rs src/ix/compile/aux_gen.rs aux_gen.rs src/ix/compile/aux_gen/below.rs below.rs src/ix/compile/aux_gen/brecon.rs brecon.rs src/ix/compile/aux_gen/cases_on.rs cases_on.rs src/ix/compile/aux_gen/expr_utils.rs expr_utils.rs src/ix/compile/aux_gen/nested.rs nested.rs src/ix/compile/aux_gen/rec_on.rs rec_on.rs src/ix/compile/aux_gen/recursor.rs recursor.rs src/ix/compile/env.rs env.rs src/ix/compile/mutual.rs mutual.rs src/ix/compile/nat_conv.rs nat_conv.rs src/ix/compile/surgery.rs surgery.rs src/ix/congruence.rs congruence.rs src/ix/congruence/perm.rs perm.rs src/ix/decompile.rs decompile.rs src/ix/env.rs env.rs src/ix/graph.rs graph.rs src/ix/ground.rs ground.rs src/ix/ixon/env.rs env.rs src/ix/ixon/error.rs error.rs src/ix/ixon/metadata.rs metadata.rs src/ix/ixon/serialize.rs serialize.rs src/ix/ixon/sharing.rs sharing.rs src/ix/kernel.rs kernel.rs src/ix/kernel/canonical_check.rs canonical_check.rs src/ix/kernel/check.rs check.rs src/ix/kernel/congruence.rs congruence.rs src/ix/kernel/constant.rs constant.rs src/ix/kernel/def_eq.rs def_eq.rs src/ix/kernel/egress.rs egress.rs src/ix/kernel/env.rs env.rs src/ix/kernel/equiv.rs equiv.rs src/ix/kernel/error.rs error.rs src/ix/kernel/expr.rs expr.rs src/ix/kernel/id.rs id.rs src/ix/kernel/inductive.rs inductive.rs src/ix/kernel/infer.rs infer.rs src/ix/kernel/ingress.rs ingress.rs src/ix/kernel/lctx.rs lctx.rs src/ix/kernel/level.rs level.rs src/ix/kernel/mode.rs mode.rs src/ix/kernel/perf.rs perf.rs src/ix/kernel/primitive.rs primitive.rs src/ix/kernel/subst.rs subst.rs src/ix/kernel/tc.rs tc.rs src/ix/kernel/testing.rs testing.rs src/ix/kernel/tutorial/basic.rs basic.rs src/ix/kernel/tutorial/defeq.rs defeq.rs src/ix/kernel/tutorial/inductive.rs inductive.rs src/ix/kernel/tutorial/mod.rs mod.rs src/ix/kernel/tutorial/reduction.rs reduction.rs src/ix/kernel/whnf.rs whnf.rs src/lean.rs lean.rs src/lib.rs lib.rs There are no files selected for viewing 31 changes: 31 additions & 0 deletions 31 .github/valgrind.supp Show comments View file Open in desktop Original file line number Diff line number Diff line change @@ -0,0 +1,31 @@ { mimalloc-prim-mem-init-uninit-cond Memcheck:Cond fun:_mi_strnlen fun:_mi_strnstr fun:_mi_prim_mem_init fun:mi_process_init ... } { mimalloc-prim-mem-init-uninit-value8 Memcheck:Value8 fun:_mi_strnlen fun:_mi_strnstr fun:_mi_prim_mem_init fun:mi_process_init ... } { glibc-pthread-create-tls-dtv Memcheck:Leak match-leak-kinds: possible fun:calloc fun:allocate_dtv fun:_dl_allocate_tls ... fun:pthread_create* ... } 8 changes: 7 additions & 1 deletion 8 .github/workflows/ignored.yml Show comments View file Open in desktop Original file line number Diff line number Diff line change Expand Up @@ -53,7 +53,12 @@ jobs: build-args: "IxTests" use-github-cache: false - name: Install valgrind run: sudo apt-get update && sudo apt-get install -y valgrind run: | # Some warpbuild images ship a mirrorlist with an unreachable # azure.archive.ubuntu.com entry, causing apt-get update to stall indefinitely. sudo sed -i '/azure\.archive\.ubuntu\.com/d' /etc/apt/apt-mirrors.txt 2>/dev/null || true sudo apt-get update sudo apt-get install -y valgrind - name: Run tests under valgrind run: | valgrind \ Expand All @@ -62,4 +67,5 @@ jobs: --errors-for-leak-kinds=definite \ --track-origins=yes \ --error-exitcode=1 \ --suppressions=.github/valgrind.supp \ .lake/build/bin/IxTests -- ffi Loading Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later. Footer © 2026 GitHub, Inc. Footer navigation Terms Privacy Security Status Community Docs Contact You can’t perform that action at this time. , '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 contentNavigation Menu Sign inAppearance settings AI CODE CREATIONGitHub CopilotWrite better code with AI GitHub Copilot appDirect agents from issue to merge MCP RegistryIntegrate external tools DEVELOPER WORKFLOWSActionsAutomate any workflow CodespacesInstant dev environments IssuesPlan and track work Code ReviewManage code changes Code QualityEnforce quality at merge APPLICATION SECURITYGitHub Advanced SecurityFind and fix vulnerabilities Code securitySecure your code as you build Secret protectionStop leaks before they start EXPLOREWhy GitHub Documentation Blog Changelog Marketplace View all features BY COMPANY SIZEEnterprises Small and medium teams Startups Nonprofits BY USE CASEApp Modernization DevSecOps DevOps CI/CD View all use cases BY INDUSTRYHealthcare Financial services Manufacturing Government View all industries View all solutions EXPLORE BY TOPICAI Software Development DevOps Security View all topics EXPLORE BY TYPECustomer stories Events & webinars Ebooks & reports Business insights GitHub Skills SUPPORT & SERVICESDocumentation Customer support Community forum Trust center Partners View all resources COMMUNITYGitHub SponsorsFund open source developers PROGRAMSSecurity Lab Maintainer Community GitHub Stars Archive Program REPOSITORIESTopics Trending Collections ENTERPRISE SOLUTIONSEnterprise platformAI-powered developer platform AVAILABLE ADD-ONSGitHub Advanced SecurityEnterprise-grade security features Copilot for BusinessEnterprise-grade AI features Premium SupportEnterprise-grade 24/7 support Pricing Sign in Sign upAppearance settings You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert Uh oh! There was an error while loading. Please reload this page. argumentcomputer /ixPublic Notifications You must be signed in to change notification settings Fork 3 Star 91 Code Issues10 Pull requests14 Actions Projects Security and quality0 Insights Additional navigation options Code Issues Pull requests Actions Projects Security and quality Insights Add kernel type-checker#375 New issue Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community. Sign up for GitHub By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails. Already on GitHub? Sign in to your account Merged johnchandlerburnham merged 35 commits into main from jcb/kernelMay 7, 2026 Conversation 7 Commits 35 Checks 14 Files changed Uh oh! There was an error while loading. Please reload this page. Merged Add kernel type-checker #375 Show file tree Hide file tree Changes from all commits Commits Show all changes 35 commits Select commit Hold shift + click to select a range 8024807 Add kernel type-checker and restructure ConstantMeta for aux_gen johnchandlerburnham Apr 12, 20265fb6a7a Extract compile_env scheduler and resolve all cargo xclippy warnings johnchandlerburnham Apr 12, 2026142cc5e Add canonical aux_gen pipeline for alpha-collapsed inductive blocks johnchandlerburnham Apr 13, 2026718a0e6 fmt johnchandlerburnham Apr 13, 20264fa8cfa refactor validate-aux test johnchandlerburnham Apr 13, 2026114be51 fix Ixon Lean serialization johnchandlerburnham Apr 13, 20265d54533 Lift kernel caches into Arc<KEnv> and switch to content-addressed cac… johnchandlerburnham Apr 15, 2026f0bceac Call-site surgery, aux_gen cleanup, and Env Arc refactor johnchandlerburnham Apr 17, 2026e4579e0 solve mathlib compilation and ingress roundtrip issues johnchandlerburnham Apr 17, 202605bdf10 Close the Mathlib aux_gen congruence loop: CompileMathlib.lean passes johnchandlerburnham Apr 19, 2026a034db2 Kernel soundness hardening, two-env split, Int native reduction, tole… johnchandlerburnham Apr 21, 2026ec05c94 Anonymous canonicity: aux permutation sidecar, perm-aware congruence,… johnchandlerburnham Apr 24, 2026a37d592 Kernel-side canonicity validation and full-env check pipeline johnchandlerburnham Apr 26, 202626c3be7 xclippy warnings johnchandlerburnham Apr 26, 202656e3e79 Stream ixon_ingress into KEnv; own-and-drop IxonEnv before kernel check johnchandlerburnham Apr 27, 2026c749b58 Add IX_PERF_COUNTERS instrumentation for kernel cache hit rates johnchandlerburnham Apr 27, 20261847240 kernel: add cheap projection def-eq WHNF safely johnchandlerburnham Apr 27, 2026508ca82 Speed up kernel validation and refine infer cache keys johnchandlerburnham Apr 27, 20261dfafd5 Add `ix ingress` CLI; expand kernel caches; parallel-shard env drops johnchandlerburnham Apr 28, 20264b2409d Speed up ixon_ingress: hash-first interning + 2048-shard intern table johnchandlerburnham Apr 28, 2026ec95312 Align nested-aux canonical order between compile and kernel johnchandlerburnham Apr 28, 20261d930c8 kernel: fix over-discovery in build_flat_block johnchandlerburnham Apr 28, 20264951b0d kernel: per-worker KEnv with lazy Ixon ingress; add `ix check-ixon` CLI johnchandlerburnham Apr 29, 20268f15dc0 kernel: add FVar binder opening, alpha-invariant hashing, Nat reduc… johnchandlerburnham Apr 30, 2026aea118d fmt & clippy johnchandlerburnham May 1, 20266e802ce Merge branch 'main' of github.com:argumentcomputer/ix into jcb/kernel johnchandlerburnham May 1, 20265b14e5c aux_gen: alpha-collapse-aware roundtrip + alias-only patching johnchandlerburnham May 1, 2026d9e0fbb aux_gen: source-shape-preserving WHNF + Phase 1 cache prewarming johnchandlerburnham May 1, 2026ef4b061 `decide` is enough to prove `Aiur.G.one_ne_zero` arthurpaulino May 4, 2026a289432 Update docs/ix_canonicity.md johnchandlerburnham May 5, 20262d5cabd xclippy warnings johnchandlerburnham May 5, 2026e5d5a34 fix aux_gen test johnchandlerburnham May 5, 20269d132ef comment out ixvm tests arthurpaulino May 6, 20266e4d1ad chore: Fix lean-ffi (#395) samuelburnham May 6, 2026bef77b1 ci: Fix valgrind samuelburnham May 6, 2026 File filter Filter by extension Filter by extension .lean (33) .lock (1) .md (1) .rs (65) .supp (1) .toml (2) .yml (1) All 7 file types selected Only manifest files Viewed files Clear filters Conversations Failed to load comments. Loading Uh oh! There was an error while loading. Please reload this page. Jump to Jump to file Failed to load files. Loading Uh oh! There was an error while loading. Please reload this page. Diff view Unified Split Hide whitespace Diff view Unified Split Hide whitespace .github/valgrind.supp valgrind.supp .github/workflows/ignored.yml ignored.yml Cargo.lock Cargo.lock Cargo.toml Cargo.toml Ix.lean Ix.lean Ix/Aiur/Goldilocks.lean Goldilocks.lean Ix/Cli/CheckCmd.lean CheckCmd.lean Ix/Cli/CheckIxonCmd.lean CheckIxonCmd.lean Ix/Cli/CompileCmd.lean CompileCmd.lean Ix/Cli/IngressCmd.lean IngressCmd.lean Ix/Cli/ValidateCmd.lean ValidateCmd.lean Ix/Commit.lean Commit.lean Ix/CompileM.lean CompileM.lean Ix/DecompileM.lean DecompileM.lean Ix/Ixon.lean Ixon.lean Ix/KernelCheck.lean KernelCheck.lean Ix/Meta.lean Meta.lean Main.lean Main.lean Tests/FFI.lean FFI.lean Tests/FFI/Ixon.lean Ixon.lean Tests/FFI/Lifecycle.lean Lifecycle.lean Tests/Gen/Ixon.lean Ixon.lean Tests/Ix/Compile.lean Compile.lean Tests/Ix/Compile/Canonicity.lean Canonicity.lean Tests/Ix/Compile/Mutual.lean Mutual.lean Tests/Ix/Compile/ValidateAux.lean ValidateAux.lean Tests/Ix/Kernel/BuildPrimOrigs.lean BuildPrimOrigs.lean Tests/Ix/Kernel/BuildPrimitives.lean BuildPrimitives.lean Tests/Ix/Kernel/CheckEnv.lean CheckEnv.lean Tests/Ix/Kernel/NatReduction.lean NatReduction.lean Tests/Ix/Kernel/Roundtrip.lean Roundtrip.lean Tests/Ix/Kernel/RoundtripNoCompile.lean RoundtripNoCompile.lean Tests/Ix/Kernel/Tutorial.lean Tutorial.lean Tests/Ix/Kernel/TutorialDefs.lean TutorialDefs.lean Tests/Ix/Kernel/TutorialMeta.lean TutorialMeta.lean Tests/Main.lean Main.lean deny.toml deny.toml docs/ix_canonicity.md ix_canonicity.md lakefile.lean lakefile.lean src/ffi.rs ffi.rs src/ffi/compile.rs compile.rs src/ffi/ix/env.rs env.rs src/ffi/ixon/meta.rs meta.rs src/ffi/ixon/serialize.rs serialize.rs src/ffi/ixon/sharing.rs sharing.rs src/ffi/kernel.rs kernel.rs src/ffi/lean_env.rs lean_env.rs src/ix.rs ix.rs src/ix/address.rs address.rs src/ix/compile.rs compile.rs src/ix/compile/aux_gen.rs aux_gen.rs src/ix/compile/aux_gen/below.rs below.rs src/ix/compile/aux_gen/brecon.rs brecon.rs src/ix/compile/aux_gen/cases_on.rs cases_on.rs src/ix/compile/aux_gen/expr_utils.rs expr_utils.rs src/ix/compile/aux_gen/nested.rs nested.rs src/ix/compile/aux_gen/rec_on.rs rec_on.rs src/ix/compile/aux_gen/recursor.rs recursor.rs src/ix/compile/env.rs env.rs src/ix/compile/mutual.rs mutual.rs src/ix/compile/nat_conv.rs nat_conv.rs src/ix/compile/surgery.rs surgery.rs src/ix/congruence.rs congruence.rs src/ix/congruence/perm.rs perm.rs src/ix/decompile.rs decompile.rs src/ix/env.rs env.rs src/ix/graph.rs graph.rs src/ix/ground.rs ground.rs src/ix/ixon/env.rs env.rs src/ix/ixon/error.rs error.rs src/ix/ixon/metadata.rs metadata.rs src/ix/ixon/serialize.rs serialize.rs src/ix/ixon/sharing.rs sharing.rs src/ix/kernel.rs kernel.rs src/ix/kernel/canonical_check.rs canonical_check.rs src/ix/kernel/check.rs check.rs src/ix/kernel/congruence.rs congruence.rs src/ix/kernel/constant.rs constant.rs src/ix/kernel/def_eq.rs def_eq.rs src/ix/kernel/egress.rs egress.rs src/ix/kernel/env.rs env.rs src/ix/kernel/equiv.rs equiv.rs src/ix/kernel/error.rs error.rs src/ix/kernel/expr.rs expr.rs src/ix/kernel/id.rs id.rs src/ix/kernel/inductive.rs inductive.rs src/ix/kernel/infer.rs infer.rs src/ix/kernel/ingress.rs ingress.rs src/ix/kernel/lctx.rs lctx.rs src/ix/kernel/level.rs level.rs src/ix/kernel/mode.rs mode.rs src/ix/kernel/perf.rs perf.rs src/ix/kernel/primitive.rs primitive.rs src/ix/kernel/subst.rs subst.rs src/ix/kernel/tc.rs tc.rs src/ix/kernel/testing.rs testing.rs src/ix/kernel/tutorial/basic.rs basic.rs src/ix/kernel/tutorial/defeq.rs defeq.rs src/ix/kernel/tutorial/inductive.rs inductive.rs src/ix/kernel/tutorial/mod.rs mod.rs src/ix/kernel/tutorial/reduction.rs reduction.rs src/ix/kernel/whnf.rs whnf.rs src/lean.rs lean.rs src/lib.rs lib.rs There are no files selected for viewing 31 changes: 31 additions & 0 deletions 31 .github/valgrind.supp Show comments View file Open in desktop Original file line number Diff line number Diff line change @@ -0,0 +1,31 @@ { mimalloc-prim-mem-init-uninit-cond Memcheck:Cond fun:_mi_strnlen fun:_mi_strnstr fun:_mi_prim_mem_init fun:mi_process_init ... } { mimalloc-prim-mem-init-uninit-value8 Memcheck:Value8 fun:_mi_strnlen fun:_mi_strnstr fun:_mi_prim_mem_init fun:mi_process_init ... } { glibc-pthread-create-tls-dtv Memcheck:Leak match-leak-kinds: possible fun:calloc fun:allocate_dtv fun:_dl_allocate_tls ... fun:pthread_create* ... } 8 changes: 7 additions & 1 deletion 8 .github/workflows/ignored.yml Show comments View file Open in desktop Original file line number Diff line number Diff line change Expand Up @@ -53,7 +53,12 @@ jobs: build-args: "IxTests" use-github-cache: false - name: Install valgrind run: sudo apt-get update && sudo apt-get install -y valgrind run: | # Some warpbuild images ship a mirrorlist with an unreachable # azure.archive.ubuntu.com entry, causing apt-get update to stall indefinitely. sudo sed -i '/azure\.archive\.ubuntu\.com/d' /etc/apt/apt-mirrors.txt 2>/dev/null || true sudo apt-get update sudo apt-get install -y valgrind - name: Run tests under valgrind run: | valgrind \ Expand All @@ -62,4 +67,5 @@ jobs: --errors-for-leak-kinds=definite \ --track-origins=yes \ --error-exitcode=1 \ --suppressions=.github/valgrind.supp \ .lake/build/bin/IxTests -- ffi Loading Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later. Footer © 2026 GitHub, Inc. Footer navigation Terms Privacy Security Status Community Docs Contact You can’t perform that action at this time. , '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 contentNavigation Menu Sign inAppearance settings AI CODE CREATIONGitHub CopilotWrite better code with AI GitHub Copilot appDirect agents from issue to merge MCP RegistryIntegrate external tools DEVELOPER WORKFLOWSActionsAutomate any workflow CodespacesInstant dev environments IssuesPlan and track work Code ReviewManage code changes Code QualityEnforce quality at merge APPLICATION SECURITYGitHub Advanced SecurityFind and fix vulnerabilities Code securitySecure your code as you build Secret protectionStop leaks before they start EXPLOREWhy GitHub Documentation Blog Changelog Marketplace View all features BY COMPANY SIZEEnterprises Small and medium teams Startups Nonprofits BY USE CASEApp Modernization DevSecOps DevOps CI/CD View all use cases BY INDUSTRYHealthcare Financial services Manufacturing Government View all industries View all solutions EXPLORE BY TOPICAI Software Development DevOps Security View all topics EXPLORE BY TYPECustomer stories Events & webinars Ebooks & reports Business insights GitHub Skills SUPPORT & SERVICESDocumentation Customer support Community forum Trust center Partners View all resources COMMUNITYGitHub SponsorsFund open source developers PROGRAMSSecurity Lab Maintainer Community GitHub Stars Archive Program REPOSITORIESTopics Trending Collections ENTERPRISE SOLUTIONSEnterprise platformAI-powered developer platform AVAILABLE ADD-ONSGitHub Advanced SecurityEnterprise-grade security features Copilot for BusinessEnterprise-grade AI features Premium SupportEnterprise-grade 24/7 support Pricing Sign in Sign upAppearance settings You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert Uh oh! There was an error while loading. Please reload this page. argumentcomputer /ixPublic Notifications You must be signed in to change notification settings Fork 3 Star 91 Code Issues10 Pull requests14 Actions Projects Security and quality0 Insights Additional navigation options Code Issues Pull requests Actions Projects Security and quality Insights Add kernel type-checker#375 New issue Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community. Sign up for GitHub By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails. Already on GitHub? Sign in to your account Merged johnchandlerburnham merged 35 commits into main from jcb/kernelMay 7, 2026 Conversation 7 Commits 35 Checks 14 Files changed Uh oh! There was an error while loading. Please reload this page. Merged Add kernel type-checker #375 Show file tree Hide file tree Changes from all commits Commits Show all changes 35 commits Select commit Hold shift + click to select a range 8024807 Add kernel type-checker and restructure ConstantMeta for aux_gen johnchandlerburnham Apr 12, 20265fb6a7a Extract compile_env scheduler and resolve all cargo xclippy warnings johnchandlerburnham Apr 12, 2026142cc5e Add canonical aux_gen pipeline for alpha-collapsed inductive blocks johnchandlerburnham Apr 13, 2026718a0e6 fmt johnchandlerburnham Apr 13, 20264fa8cfa refactor validate-aux test johnchandlerburnham Apr 13, 2026114be51 fix Ixon Lean serialization johnchandlerburnham Apr 13, 20265d54533 Lift kernel caches into Arc<KEnv> and switch to content-addressed cac… johnchandlerburnham Apr 15, 2026f0bceac Call-site surgery, aux_gen cleanup, and Env Arc refactor johnchandlerburnham Apr 17, 2026e4579e0 solve mathlib compilation and ingress roundtrip issues johnchandlerburnham Apr 17, 202605bdf10 Close the Mathlib aux_gen congruence loop: CompileMathlib.lean passes johnchandlerburnham Apr 19, 2026a034db2 Kernel soundness hardening, two-env split, Int native reduction, tole… johnchandlerburnham Apr 21, 2026ec05c94 Anonymous canonicity: aux permutation sidecar, perm-aware congruence,… johnchandlerburnham Apr 24, 2026a37d592 Kernel-side canonicity validation and full-env check pipeline johnchandlerburnham Apr 26, 202626c3be7 xclippy warnings johnchandlerburnham Apr 26, 202656e3e79 Stream ixon_ingress into KEnv; own-and-drop IxonEnv before kernel check johnchandlerburnham Apr 27, 2026c749b58 Add IX_PERF_COUNTERS instrumentation for kernel cache hit rates johnchandlerburnham Apr 27, 20261847240 kernel: add cheap projection def-eq WHNF safely johnchandlerburnham Apr 27, 2026508ca82 Speed up kernel validation and refine infer cache keys johnchandlerburnham Apr 27, 20261dfafd5 Add `ix ingress` CLI; expand kernel caches; parallel-shard env drops johnchandlerburnham Apr 28, 20264b2409d Speed up ixon_ingress: hash-first interning + 2048-shard intern table johnchandlerburnham Apr 28, 2026ec95312 Align nested-aux canonical order between compile and kernel johnchandlerburnham Apr 28, 20261d930c8 kernel: fix over-discovery in build_flat_block johnchandlerburnham Apr 28, 20264951b0d kernel: per-worker KEnv with lazy Ixon ingress; add `ix check-ixon` CLI johnchandlerburnham Apr 29, 20268f15dc0 kernel: add FVar binder opening, alpha-invariant hashing, Nat reduc… johnchandlerburnham Apr 30, 2026aea118d fmt & clippy johnchandlerburnham May 1, 20266e802ce Merge branch 'main' of github.com:argumentcomputer/ix into jcb/kernel johnchandlerburnham May 1, 20265b14e5c aux_gen: alpha-collapse-aware roundtrip + alias-only patching johnchandlerburnham May 1, 2026d9e0fbb aux_gen: source-shape-preserving WHNF + Phase 1 cache prewarming johnchandlerburnham May 1, 2026ef4b061 `decide` is enough to prove `Aiur.G.one_ne_zero` arthurpaulino May 4, 2026a289432 Update docs/ix_canonicity.md johnchandlerburnham May 5, 20262d5cabd xclippy warnings johnchandlerburnham May 5, 2026e5d5a34 fix aux_gen test johnchandlerburnham May 5, 20269d132ef comment out ixvm tests arthurpaulino May 6, 20266e4d1ad chore: Fix lean-ffi (#395) samuelburnham May 6, 2026bef77b1 ci: Fix valgrind samuelburnham May 6, 2026 File filter Filter by extension Filter by extension .lean (33) .lock (1) .md (1) .rs (65) .supp (1) .toml (2) .yml (1) All 7 file types selected Only manifest files Viewed files Clear filters Conversations Failed to load comments. Loading Uh oh! There was an error while loading. Please reload this page. Jump to Jump to file Failed to load files. Loading Uh oh! There was an error while loading. Please reload this page. Diff view Unified Split Hide whitespace Diff view Unified Split Hide whitespace .github/valgrind.supp valgrind.supp .github/workflows/ignored.yml ignored.yml Cargo.lock Cargo.lock Cargo.toml Cargo.toml Ix.lean Ix.lean Ix/Aiur/Goldilocks.lean Goldilocks.lean Ix/Cli/CheckCmd.lean CheckCmd.lean Ix/Cli/CheckIxonCmd.lean CheckIxonCmd.lean Ix/Cli/CompileCmd.lean CompileCmd.lean Ix/Cli/IngressCmd.lean IngressCmd.lean Ix/Cli/ValidateCmd.lean ValidateCmd.lean Ix/Commit.lean Commit.lean Ix/CompileM.lean CompileM.lean Ix/DecompileM.lean DecompileM.lean Ix/Ixon.lean Ixon.lean Ix/KernelCheck.lean KernelCheck.lean Ix/Meta.lean Meta.lean Main.lean Main.lean Tests/FFI.lean FFI.lean Tests/FFI/Ixon.lean Ixon.lean Tests/FFI/Lifecycle.lean Lifecycle.lean Tests/Gen/Ixon.lean Ixon.lean Tests/Ix/Compile.lean Compile.lean Tests/Ix/Compile/Canonicity.lean Canonicity.lean Tests/Ix/Compile/Mutual.lean Mutual.lean Tests/Ix/Compile/ValidateAux.lean ValidateAux.lean Tests/Ix/Kernel/BuildPrimOrigs.lean BuildPrimOrigs.lean Tests/Ix/Kernel/BuildPrimitives.lean BuildPrimitives.lean Tests/Ix/Kernel/CheckEnv.lean CheckEnv.lean Tests/Ix/Kernel/NatReduction.lean NatReduction.lean Tests/Ix/Kernel/Roundtrip.lean Roundtrip.lean Tests/Ix/Kernel/RoundtripNoCompile.lean RoundtripNoCompile.lean Tests/Ix/Kernel/Tutorial.lean Tutorial.lean Tests/Ix/Kernel/TutorialDefs.lean TutorialDefs.lean Tests/Ix/Kernel/TutorialMeta.lean TutorialMeta.lean Tests/Main.lean Main.lean deny.toml deny.toml docs/ix_canonicity.md ix_canonicity.md lakefile.lean lakefile.lean src/ffi.rs ffi.rs src/ffi/compile.rs compile.rs src/ffi/ix/env.rs env.rs src/ffi/ixon/meta.rs meta.rs src/ffi/ixon/serialize.rs serialize.rs src/ffi/ixon/sharing.rs sharing.rs src/ffi/kernel.rs kernel.rs src/ffi/lean_env.rs lean_env.rs src/ix.rs ix.rs src/ix/address.rs address.rs src/ix/compile.rs compile.rs src/ix/compile/aux_gen.rs aux_gen.rs src/ix/compile/aux_gen/below.rs below.rs src/ix/compile/aux_gen/brecon.rs brecon.rs src/ix/compile/aux_gen/cases_on.rs cases_on.rs src/ix/compile/aux_gen/expr_utils.rs expr_utils.rs src/ix/compile/aux_gen/nested.rs nested.rs src/ix/compile/aux_gen/rec_on.rs rec_on.rs src/ix/compile/aux_gen/recursor.rs recursor.rs src/ix/compile/env.rs env.rs src/ix/compile/mutual.rs mutual.rs src/ix/compile/nat_conv.rs nat_conv.rs src/ix/compile/surgery.rs surgery.rs src/ix/congruence.rs congruence.rs src/ix/congruence/perm.rs perm.rs src/ix/decompile.rs decompile.rs src/ix/env.rs env.rs src/ix/graph.rs graph.rs src/ix/ground.rs ground.rs src/ix/ixon/env.rs env.rs src/ix/ixon/error.rs error.rs src/ix/ixon/metadata.rs metadata.rs src/ix/ixon/serialize.rs serialize.rs src/ix/ixon/sharing.rs sharing.rs src/ix/kernel.rs kernel.rs src/ix/kernel/canonical_check.rs canonical_check.rs src/ix/kernel/check.rs check.rs src/ix/kernel/congruence.rs congruence.rs src/ix/kernel/constant.rs constant.rs src/ix/kernel/def_eq.rs def_eq.rs src/ix/kernel/egress.rs egress.rs src/ix/kernel/env.rs env.rs src/ix/kernel/equiv.rs equiv.rs src/ix/kernel/error.rs error.rs src/ix/kernel/expr.rs expr.rs src/ix/kernel/id.rs id.rs src/ix/kernel/inductive.rs inductive.rs src/ix/kernel/infer.rs infer.rs src/ix/kernel/ingress.rs ingress.rs src/ix/kernel/lctx.rs lctx.rs src/ix/kernel/level.rs level.rs src/ix/kernel/mode.rs mode.rs src/ix/kernel/perf.rs perf.rs src/ix/kernel/primitive.rs primitive.rs src/ix/kernel/subst.rs subst.rs src/ix/kernel/tc.rs tc.rs src/ix/kernel/testing.rs testing.rs src/ix/kernel/tutorial/basic.rs basic.rs src/ix/kernel/tutorial/defeq.rs defeq.rs src/ix/kernel/tutorial/inductive.rs inductive.rs src/ix/kernel/tutorial/mod.rs mod.rs src/ix/kernel/tutorial/reduction.rs reduction.rs src/ix/kernel/whnf.rs whnf.rs src/lean.rs lean.rs src/lib.rs lib.rs There are no files selected for viewing 31 changes: 31 additions & 0 deletions 31 .github/valgrind.supp Show comments View file Open in desktop Original file line number Diff line number Diff line change @@ -0,0 +1,31 @@ { mimalloc-prim-mem-init-uninit-cond Memcheck:Cond fun:_mi_strnlen fun:_mi_strnstr fun:_mi_prim_mem_init fun:mi_process_init ... } { mimalloc-prim-mem-init-uninit-value8 Memcheck:Value8 fun:_mi_strnlen fun:_mi_strnstr fun:_mi_prim_mem_init fun:mi_process_init ... } { glibc-pthread-create-tls-dtv Memcheck:Leak match-leak-kinds: possible fun:calloc fun:allocate_dtv fun:_dl_allocate_tls ... fun:pthread_create* ... } 8 changes: 7 additions & 1 deletion 8 .github/workflows/ignored.yml Show comments View file Open in desktop Original file line number Diff line number Diff line change Expand Up @@ -53,7 +53,12 @@ jobs: build-args: "IxTests" use-github-cache: false - name: Install valgrind run: sudo apt-get update && sudo apt-get install -y valgrind run: | # Some warpbuild images ship a mirrorlist with an unreachable # azure.archive.ubuntu.com entry, causing apt-get update to stall indefinitely. sudo sed -i '/azure\.archive\.ubuntu\.com/d' /etc/apt/apt-mirrors.txt 2>/dev/null || true sudo apt-get update sudo apt-get install -y valgrind - name: Run tests under valgrind run: | valgrind \ Expand All @@ -62,4 +67,5 @@ jobs: --errors-for-leak-kinds=definite \ --track-origins=yes \ --error-exitcode=1 \ --suppressions=.github/valgrind.supp \ .lake/build/bin/IxTests -- ffi Loading Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later. Footer © 2026 GitHub, Inc. Footer navigation Terms Privacy Security Status Community Docs Contact You can’t perform that action at this time.