Repository navigation
Jcb/ix-certified-v3 followup: Formalize nominal-to-quotient Source bridge, optimize compiler/kernel, and retire uncertified Rust/Lean pipelines - #677
Merged
Conversation
Preserve the fallback-only input recursor guard and specification version 3 role validation. Measure the combined runtime closures before refreezing: - Public admission: 6032 to 6036; tiered admission: 6142 to 6146. - Admission operations: 6029 to 6033; projection: 6054 to 6058. - Authenticated operations: 6070 to 6074; tiered: 6152 to 6156. - Artifact check and checkAt: 6068 to 6072 each. - Artifact checkTiered and checkTieredAt: 6202 to 6206 each. - Host admission: 6461 to 6465. The role-shape changes add iffFamily, nonemptyFamily, sorryAxSpecTy and its two closed terms and remove Role.spec._closed_1. The earlier 32-function inputIndexed change remains. Extern, implemented_by, unsafe, csimp and all ruling counts remain unchanged. Inherit regenerated role files without manual edits.
Combine the bounded decoder, strict host admission, certified compiler path, and benchmark registry. Preserve both the execution-substitution audit and the measured standard-axiom task-equivalence guards. Register all decoder rejection-parity and node-budget boundary cases in the required primary tier.
Run the committed Lean code generator, trace bundle generator, and claim fixture exporter after integrating the corrected role specification. Preserve the catalog shape pin and unchanged IxVM generated outputs; the schema digest and aggregate claims follow the corrected role table. Regeneration and focused aggregate, ingress, and wire-format checks pass.
Preserve the binding-proof refusal controls and the trace-shard aggregate path together. Register the cross-toolchain aggregate runner beside the decoder rejection-parity suite. The generated role and aggregate artifacts come from the committed generators after the role-table correction.
Describe the committed toolchain fixtures, catalog verification and refusals, prerequisites, and separate aggregate and shard memory budgets. Include the aggregate budget setting in the existing manual runner description.
Make compileExpr the well-founded implementation and compileExprStep its constructor step. Keep the reading and wire theorem statements while removing the identity alias and duplicate proof wrappers. ReadingAudit drops only those redundant roots: two expression theorems, one wire wrapper and one runtime alias; all remaining roots and axiom checks stay enforced. Retain the index and blob refusal controls, replacing duplicate alias calls with retry and cache-hit checks. Run each semantic-contract fixture through the single implementation.
The bounded parallel map now lives in Ix.Compile.Parallel. Freeze its complete body alongside the thin Cert.parMap wrapper, and audit the four slice lemmas at their actual declaration names. Add map_eq as the thirteenth schedule proof root and Parallel.map as the fifth checked safe definition; these count increases cover the shared implementation without dropping any of the existing scheduling proofs or runtime checks.
Update the compiler overviews to describe the certified CLI default, shared wave driver, checked parallel report helper, and reused ground split and condensation. Distinguish the optional streamed front end and remove the unsupported Rust memory comparison. This changes comments only.
Merge the pending native-definition specifications with the bounded decoder, certified execution path, strict host admission, and catalog aggregation. The new ordinary-checker equation validation and PinGen call are an unvalidated work in progress. Preserve measured hardened audit expectations until explicit measurement of the larger specification; generated roles, fixtures and pins still require regeneration. Do not publish this checkpoint.
Compile every mutual member in source order with its own consecutive index. Remove singleton-vector allocation, representative selection and maximum constructor reservations; preserve singleton grouping at the serialized metadata boundary. Exercise distinct definition indices and constructor slots across multiple members.
Exercise a late mutual name conflict against a real compiled owner and a scheduler failure after literal storage. Require the remaining serialized artifact to equal the successful subset, including its anonymous records and metadata.
Keep the serial recordStore definition and replace its runtime evaluation through an exact equality theorem. Sort records and blobs and run preflight, uniqueness, and authentication before parallel canonical decoding; replay results in original order so the complete first refusal is unchanged. Kernel admission keeps its original path. Guard the decoder equality and store replacement at the standard three axioms. Add native controls against the literal serial implementation for chunk boundaries, late record limits, authentication precedence, conflicting caches, and malformed or noncanonical authenticated orphan records. No benchmark result is claimed.
Combine the expression compiler cleanup with proved graph, ground-check, and canonical-record decoding replacements. Preserve checked-store indices, certificate overlap refusals and both primary decoder suites. The existing combined gate continues on its frozen parent source. This integration will be checked separately before publication.
Replace singleton member classes with ordered members in the Lean compiler, context and projections. Keep singleton grouping at serialized metadata boundaries. Remove representative/equivalent folds and the vacuous class-shape hypotheses; preserve the source-order and constructor-index contracts and final certification statements. ReadingAudit removes two obsolete wire lemmas, four redundant count/shape lemmas, four class projection lemmas, three class maximum/fold lemmas and two runtime class wrappers. Their flat-member counterparts retain the applicable obligations. The internal ClassesAgree print guard disappears with its definition; mutual_correct now has no class-specific premises. These are structural simplifications, not reduced coverage.
Move the shared primitive-address data and membership helpers into Ix and update the resource validator, claim harness and parity fixtures. The address bytes and table order are unchanged.
Stage anonymous records, blobs, names, metadata, hints and class ordering until the whole block succeeds. Recheck the complete batch under a shared publication lock before inserting any entry, and report a late conflict as the scheduler block failure. Dropping staged output never deletes identical content owned by concurrent successful blocks. Cover both failure orders, concurrent conflicting commits, late constant/blob/name conflicts, successful publication byte equality, and production named/anonymous partial-file output. Require Rust and Lean partial artifacts to agree and preserve fail-closed destination behavior. The compiler release suite passes 259 tests; strict lint, formatting, the Lean test build and the claim/publication FFI suite pass.
Describe exact cache keys, checked report properties and current metadata behavior without private work-queue or plan-file references. Give the index-safety fixture a descriptive name. Add a baseline-free source terminology lint and scanner controls, and run it from the existing lint driver. The standalone scanner passes over 1941 source and documentation files.
Give the bind proof its expected postcondition before introducing run arguments in the flat payload shape and definition-kind inductions. The first strict core run found the shape elaboration mismatch; context and source-order proofs and Rust compiler tests passed.
Remove obsolete compiler-stage references and singleton-class terminology from the affected compiler proof comments. Retain the semantic reading, table and source-position conditions.
Relate the member projection loop to its explicit indexed step by cases on each member, and use the rewritten lookup equation after selecting a payload. Preserve the failed full proof run and strengthen no assumptions.
Describe the current Source admission, projection layout and dependency scheduler directly, without retired compiler hooks or proof-stage labels.
Member
Author
|
!merge-tests |
Member
Author
|
!benchmark aiur fresh |
johnchandlerburnham
enabled stacked auto-merge
November 5, 2026 22:17
Contributor
|
| constant | execute-time (main) | execute-time (PR) | Δ% | prove-time (main) | prove-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | proof-size (main) | proof-size (PR) | Δ% | verify-time (main) | verify-time (PR) | Δ% | fft-cost (main) | fft-cost (PR) | Δ% | trace-shards (main) | trace-shards (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
ByteArray.utf8DecodeChar?_utf8EncodeChar_append |
9.240 s | 6.793 s | -26.5% (1.36× faster) 🟢 | 54.083 s | 49.875 s | -7.8% (1.08× faster) 🟢 | 49.870 | 54.070 | +8.4% (1.08× faster) 🟢 | 67.11 GiB | 67.09 GiB | -0.0% | 5.43 MiB | 5.44 MiB | +0.2% | 33.6 ms | 32.5 ms | -3.4% 🟢 | 116.27B | 116.27B | +0.0% | 1 | 1 | +0.0% |
Array.extract_append |
7.404 s | 5.217 s | -29.5% (1.42× faster) 🟢 | 42.060 s | 38.295 s | -9.0% (1.10× faster) 🟢 | 35.880 | 39.400 | +9.8% (1.10× faster) 🟢 | 50.42 GiB | 50.52 GiB | +0.2% | 5.36 MiB | 5.36 MiB | -0.1% | 35.7 ms | 32.3 ms | -9.4% (1.10× faster) 🟢 | 85.54B | 85.54B | +0.0% | 1 | 1 | +0.0% |
Char.ofOrdinal_le_of_le |
6.453 s | 5.065 s | -21.5% (1.27× faster) 🟢 | 38.608 s | 35.130 s | -9.0% (1.10× faster) 🟢 | 69.310 | 76.170 | +9.9% (1.10× faster) 🟢 | 49.81 GiB | 49.77 GiB | -0.1% | 5.42 MiB | 5.41 MiB | -0.1% | 32.9 ms | 32.9 ms | +0.2% | 83.05B | 83.05B | +0.0% | 1 | 1 | +0.0% |
Std.HashMap |
4.274 s | 3.521 s | -17.6% (1.21× faster) 🟢 | 25.735 s | 23.562 s | -8.4% (1.09× faster) 🟢 | 79.230 | 86.540 | +9.2% (1.09× faster) 🟢 | 34.19 GiB | 34.15 GiB | -0.1% | 5.36 MiB | 5.35 MiB | -0.2% | 34.2 ms | 31.3 ms | -8.6% (1.09× faster) 🟢 | 55.46B | 55.46B | +0.0% | 1 | 1 | +0.0% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
3.641 s | 3.041 s | -16.5% (1.20× faster) 🟢 | 24.086 s | 22.074 s | -8.4% (1.09× faster) 🟢 | 73.400 | 80.100 | +9.1% (1.09× faster) 🟢 | 32.24 GiB | 32.12 GiB | -0.4% | 5.31 MiB | 5.32 MiB | +0.1% | 40.1 ms | 32.0 ms | -20.1% (1.25× faster) 🟢 | 48.32B | 48.32B | +0.0% | 1 | 1 | +0.0% |
String.append |
804.0 ms | 699.6 ms | -13.0% (1.15× faster) 🟢 | 2.451 s | 2.369 s | -3.3% 🟢 | 107.320 | 111.010 | +3.4% 🟢 | 5.55 GiB | 5.61 GiB | +1.0% | 5.09 MiB | 5.08 MiB | -0.2% | 29.5 ms | 32.5 ms | +10.2% (1.10× slower) |
2.91B | 2.91B | +0.0% | 1 | 1 | +0.0% |
Nat.add_comm |
507.3 ms | 480.6 ms | -5.3% (1.06× faster) 🟢 | 1.102 s | 1.039 s | -5.7% (1.06× faster) 🟢 | 30.860 | 32.730 | +6.1% (1.06× faster) 🟢 | 4.08 GiB | 3.91 GiB | -4.4% 🟢 | 4.88 MiB | 4.87 MiB | -0.2% | 28.7 ms | 27.2 ms | -5.2% (1.05× faster) 🟢 | 362.82M | 362.82M | +0.0% | 1 | 1 | +0.0% |
FRI verifier on FRI (7 constants)
| constant | execute-time (main) | execute-time (PR) | Δ% | prove-time (main) | prove-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | proof-size (main) | proof-size (PR) | Δ% | verify-time (main) | verify-time (PR) | Δ% | fft-cost (main) | fft-cost (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
ByteArray.utf8DecodeChar?_utf8EncodeChar_append |
3.477 s | 3.108 s | -10.6% (1.12× faster) 🟢 | 37.300 s | 35.252 s | -5.5% (1.06× faster) 🟢 | 72.310 | 76.510 | +5.8% (1.06× faster) 🟢 | 54.11 GiB | 54.57 GiB | +0.9% | 2.69 MiB | 2.69 MiB | +0.3% | 15.7 ms | 15.9 ms | +1.1% | 102.42B | 102.89B | +0.5% |
Array.extract_append |
3.415 s | 3.008 s | -11.9% (1.14× faster) 🟢 | 37.293 s | 35.190 s | -5.6% (1.06× faster) 🟢 | 40.460 | 42.880 | +6.0% (1.06× faster) 🟢 | 53.54 GiB | 53.26 GiB | -0.5% | 2.69 MiB | 2.70 MiB | +0.3% | 15.6 ms | 15.8 ms | +0.9% | 101.02B | 100.81B | -0.2% |
Char.ofOrdinal_le_of_le |
3.505 s | 3.152 s | -10.1% (1.11× faster) 🟢 | 37.945 s | 35.328 s | -6.9% (1.07× faster) 🟢 | 70.520 | 75.750 | +7.4% (1.07× faster) 🟢 | 54.21 GiB | 54.42 GiB | +0.4% | 2.69 MiB | 2.70 MiB | +0.2% | 16.0 ms | 15.8 ms | -1.4% | 102.52B | 101.82B | -0.7% |
Std.HashMap |
3.410 s | 3.065 s | -10.1% (1.11× faster) 🟢 | 37.046 s | 34.786 s | -6.1% (1.06× faster) 🟢 | 55.040 | 58.610 | +6.5% (1.06× faster) 🟢 | 52.79 GiB | 52.50 GiB | -0.6% | 2.70 MiB | 2.70 MiB | -0.2% | 16.0 ms | 17.0 ms | +6.1% (1.06× slower) |
100.87B | 99.82B | -1.0% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
3.328 s | 3.134 s | -5.8% (1.06× faster) 🟢 | 36.229 s | 34.793 s | -4.0% 🟢 | 48.800 | 50.810 | +4.1% 🟢 | 52.58 GiB | 52.63 GiB | +0.1% | 2.70 MiB | 2.70 MiB | +0.1% | 15.9 ms | 15.8 ms | -0.8% | 98.88B | 99.17B | +0.3% |
String.append |
3.116 s | 2.831 s | -9.1% (1.10× faster) 🟢 | 35.924 s | 32.757 s | -8.8% (1.10× faster) 🟢 | 7.320 | 8.030 | +9.7% (1.10× faster) 🟢 | 50.40 GiB | 48.60 GiB | -3.6% 🟢 | 2.70 MiB | 2.70 MiB | -0.0% | 16.4 ms | 16.1 ms | -2.0% | 93.30B | 91.62B | -1.8% |
Nat.add_comm |
2.912 s | 2.719 s | -6.6% (1.07× faster) 🟢 | 34.059 s | 31.723 s | -6.9% (1.07× faster) 🟢 | 1 | 1.070 | +7.0% (1.07× faster) 🟢 | 47.40 GiB | 46.53 GiB | -1.8% | 2.70 MiB | 2.70 MiB | -0.2% | 16.6 ms | 16.4 ms | -1.2% | 88.44B | 86.15B | -2.6% |
Aggregate flat join (1 pair)
| pair | execute-time (main) | execute-time (PR) | Δ% | prove-time (main) | prove-time (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | proof-size (main) | proof-size (PR) | Δ% | verify-time (main) | verify-time (PR) | Δ% | fft-cost (main) | fft-cost (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Nat.add_comm + String.append |
4.111 s | 3.836 s | -6.7% (1.07× faster) 🟢 | 38.978 s | 37.648 s | -3.4% 🟢 | 56.32 GiB | 56.21 GiB | -0.2% | 2.88 MiB | 2.91 MiB | +0.8% | 20.6 ms | 17.1 ms | -16.9% (1.20× faster) 🟢 | 118.74B | 119.33B | +0.5% |
Pipeline total (7 constants)
| constant | total-time (main) | total-time (PR) | Δ% | pipeline-throughput (const/s) (main) | pipeline-throughput (const/s) (PR) | Δ% | pipeline-peak-ram (main) | pipeline-peak-ram (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|
ByteArray.utf8DecodeChar?_utf8EncodeChar_append |
1m 31.4s | 1m 25.1s | -6.8% (1.07× faster) 🟢 | 29.510 | 31.680 | +7.4% (1.07× faster) 🟢 | 67.11 GiB | 67.09 GiB | -0.0% |
Array.extract_append |
1m 19.4s | 1m 13.5s | -7.4% (1.08× faster) 🟢 | 19.020 | 20.530 | +7.9% (1.08× faster) 🟢 | 53.54 GiB | 53.26 GiB | -0.5% |
Char.ofOrdinal_le_of_le |
1m 16.6s | 1m 10.5s | -8.0% (1.09× faster) 🟢 | 34.960 | 37.980 | +8.6% (1.09× faster) 🟢 | 54.21 GiB | 54.42 GiB | +0.4% |
Std.HashMap |
1m 2.8s | 58.349 s | -7.1% (1.08× faster) 🟢 | 32.480 | 34.940 | +7.6% (1.08× faster) 🟢 | 52.79 GiB | 52.50 GiB | -0.6% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
1m 0.3s | 56.867 s | -5.7% (1.06× faster) 🟢 | 29.310 | 31.090 | +6.1% (1.06× faster) 🟢 | 52.58 GiB | 52.63 GiB | +0.1% |
String.append |
38.374 s | 35.126 s | -8.5% (1.09× faster) 🟢 | 6.850 | 7.490 | +9.3% (1.09× faster) 🟢 | 50.40 GiB | 48.60 GiB | -3.6% 🟢 |
Nat.add_comm |
35.161 s | 32.762 s | -6.8% (1.07× faster) 🟢 | 0.970 | 1.040 | +7.2% (1.07× faster) 🟢 | 47.40 GiB | 46.53 GiB | -1.8% |
- Base hardware (base run @ 3c8999c (fresh — bencher bypassed)): CPU:
Intel(R) Xeon(R) 6975P-C· vCPUs:32· RAM:247.7 GiB - PR hardware: CPU:
Intel(R) Xeon(R) 6975P-C· vCPUs:32· RAM:247.7 GiB
johnchandlerburnham
added a commit
that referenced
this pull request
Nov 6, 2026
johnchandlerburnham
added a commit
that referenced
this pull request
Nov 6, 2026
#677's history after 05cc396 is squashed into fb8e986 (tree of 38f0340; #675's 426a242 kept as a parent so the compression bridge merges against #675's original files). - Legacy Aiur, IxVM, MultiStark and codegen files #677 changed stay deleted. Their semantics reach the formal programs by regeneration: tools/ixvm/adapt.py and recursion.py now read Ix at 38f0340 (self-assumption and duplicate-discharge checks, user axioms in claims, RoleSpecGen CSE). run_check_env's pointer-identity guard against an empty owned tree becomes a reviewed refutable Cons pattern. - The security fix's regressions move to the formal harnesses: Tests/FormalAiur.lean (Check/CheckEnv self-assumption, empty owned tree) and Tests/FormalAggregate.lean (duplicate and self-discharging joins, overlapping subjects). - ClaimContext.ofEnv keeps #678's bindingAssumed and gains #677's user axiom tree; ClaimHarness takes #677's assumeBinding/user-axiom scope. - #677's deletions win where #678 had only kept code alive: ix-bench (its two helpers move into the stark-verifier compare example), shardManifestFromPartition, dead ffi dependencies, retired suites and CI jobs. Tests/Main.lean starts from #677's registry minus the legacy suites #678 retired. - ProveCmd: --compress is refused with --assume-binding, as #677 refuses aggregation. - CI: drop ixon/sharing-profile, which no ixon version defines.
johnchandlerburnham
added a commit
that referenced
this pull request
Nov 6, 2026
Member
|
!benchmark aiur-sharded-env BENCH_ENVS=ISLB |
Contributor
|
| constant | check-time (main) | check-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | constants (main) | constants (PR) | Δ% | shards (main) | shards (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
ISLB |
1m 16.9s | 1m 19.1s | +2.8% | 2.40K | 2.33K | -2.7% | 183.93 GiB | 183.41 GiB | -0.3% | 184,335 | 184,335 | +0.0% | 114 | 114 | +0.0% |
- Base hardware (bencher @ 3c8999c): CPU:
Intel(R) Xeon(R) 6975P-C· vCPUs:32· RAM:247.7 GiB - PR hardware: CPU:
Intel(R) Xeon(R) 6975P-C· vCPUs:32· RAM:247.7 GiB
arthurpaulino
previously approved these changes
Nov 6, 2026
…tests needs no ix binary
johnchandlerburnham
removed this pull request from the merge queue due to a manual request
Nov 6, 2026
Member
Author
|
!merge-tests |
arthurpaulino
approved these changes
Nov 6, 2026
johnchandlerburnham
added a commit
that referenced
this pull request
Nov 6, 2026
johnchandlerburnham
added a commit
that referenced
this pull request
Nov 6, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Formalize nominal-to-quotient Source bridge, optimize compiler/kernel, and retire uncertified Rust/Lean pipelines
Summary
Following the merge of #665 (
3c8999c18), this PR delivers:Lean.EnvironmentIngress, Collapsed-Trace Characterization & Conditional Nominal-to-Quotient Pullback (Ix.Cert.Canon,Ix.LeanIngress.Theorems,Ix.LeanIngress.Rename,Ix.LeanIngress.NominalQuotient,Ix.Cert.Quotient,Ix.Cert.CompileCorrect,Ix.Cert.ModuleAudit,Ix.Cert.Audit)GraphM,CondenseM, Compiler, Finalizer, Serializer, andIxCKernel Performance OptimizationsIx.Aggr.Circuit,Ix.Aggr.Host,Ix.IxVM.Kernel.Claim,Tests.Aggr)ShardMap, and Redundant/Formally-Subsumed Test Suites (merge-queue matrix streamlined from 9 partitions to 4)IxC.Kernel.Cached.Policy,IxC.Kernel.Admission.UserAxioms,Ix.RoleBinding.UserAxioms,ix check-lean --allow-user-axioms, CONDITIONAL verdict with exit5)compile-exportregression fixed, every merge-queue tier green, a lighter CI workload, Blake3 digests throughout, more dead code removed, and design docs rewritten against the Lean code1. Raw
Lean.EnvironmentIngress & Nominal-to-Quotient Source BridgeRaw
Lean.EnvironmenttoIx.EnvironmentIngress Theorems (Ix/Cert/Canon.lean):leanConstantVal,leanAxiomVal,leanQuotVal,leanDefinitionVal,leanTheoremVal,leanOpaqueVal,leanInductiveVal,leanConstructorVal,leanRecursorRule).Ix.LeanIngress.convertAxiom,Ix.LeanIngress.convertQuotient, and single-memberIx.LeanIngress.convertDefinitionson canonicalizedIx.ConstantInfoagree with the direct raw-Lean readings (ingressConstantVal_constValS,convertAxiom_axiomValS,convertQuotient_quotValS,convertDefinitions_defnValS,convertDefinitions_thmValS,convertDefinitions_opaqueValS,ingressInductiveVal_inductValS,ingressConstructorVal_ctorValS,ingressRecursorRule_recRuleS).Pure Canonicalization, Quotient Commutation & Shared
substKeysLemmas (Ix/LeanIngress/Theorems.lean,Ix/LeanIngress/Rename.lean):Ix.CanonMexpression and declaration canonicalization via pure functions (canonExprM,canonValM,DefMember.canon,canonInfo,BlockRead.canon,Converted.canon,canonDecl), proves conditional idempotence (*_idem, given level-canonicalizer idempotencehf), and proves thatConverted.quotient σequalssubstKeys σafter pure canonicalization (Converted.quotient_eq_substKeys_canon,BlockRead.canon_substKeys,DefMember.canon_substKeys,canonDecl_substKeys).ConstantVal.substKeys_*,ConstantInfo.substKeys_*,RecRule.substKeys_*, andBlockRead.substKeys_names@[simp]lemmas intoIx/LeanIngress/Rename.lean.Collapsed-Trace Characterization & Conditional Nominal Pullback (
Ix/LeanIngress/NominalQuotient.lean,Ix/Cert/Quotient.lean,Ix/Cert/CompileCorrect.lean,Ix/Cert/ModuleAudit.lean,Ix/Cert/Audit.lean):prepareSourceCollapsedAt_trace): proves that every step in a successful quotient Source preparation (prepareSourceCollapsedAt) either keeps a fresh declaration/block or drops an alias declaration/block that is structurally identical (Declaration.beqF/BlockRead.beqF, hence=) to an already-kept representative after applyingKey.subst (fiberAliasAt ixe (roleAtMap t)). Together withCompileCorrect(which unconditionally transports bothValueModelandLawModelbetween quotient SourceenvQand compiled IxonenvA), this completes the primary security guarantee.GroupIntraInjective,HintsAgreeAt, andFiberAliasSafe(checkGroupFiberSafe,checkGroupFiberSafe_sound), and proves conditional pullback corollaries (EnvSubstRel.toModelPullback,IxonCommutesCovering.nominalBridgeAt,IxonCommutesCovering.nominalPullback,NominalSemanticBridgeAt.of_covering,CompileCorrect.nominalBridgeAt,CompileCorrect.nominalPullback) showing howValueModel(fromEnvSubstRel) andLawModel(givenLawModel.RelinEnvSubstPullback) pull back fromenvQto a nominalenvSaccepted bySourceAccepts. (DerivingLawModel.RelfromEnvSubstReland dischargingEnvSubstRelfromFiberAliasSafeon closures whose alias fibers do not mix reducibility hints is left for future work.)Ix/Cert/Audit.lean(#guard_msgs in #check) and pins their axioms inIx/Cert/ModuleAudit.lean(#guard_module_axiomsand#guard_kernel_axiomswith[propext, Classical.choice, Quot.sound]).2.
GraphM,CondenseM, Compiler, Finalizer, Serializer, andIxCPerformanceSingle-Accumulator
GraphM& Direct-ComponentCondenseM(Ix/GraphM.lean,Ix/Cert/GraphWalk.lean,Ix/Cert/RecursorIndexFacts.lean,Ix/CondenseM.lean,Ix/Cert/Condense.lean,Ix/Cert/GroupRefs.lean,Ix/Cert/TraceFold.lean):HashSetallocations andHashSet.unionmerges inIx.GraphMwith a single-accumulator walk (graphExprAcc) that records visited expressions in aStd.HashSet ExprKey(keyed by cached 64-bit hash with full structuralLawfulBEqequality) and skips already-traversed DAG subtrees while preserving the pure specificationGraph.envandGraphWalkproofs (1.77×faster than the pre-retirement Rust implementation ongraph-cross).Ix.CondenseMnow that mutual blocks preserve discovery/source order: removes the unusedrootNameandbyDiscoveryhash maps and redundant self-loop filters, constructingscc.blocksdirectly when popping an SCC root (1.26×faster than the pre-retirement Rust implementation oncondense-cross).O(1)Loose-BVar Cutoffs inIxC.Kernel.ExprOps(IxC/Kernel/ExprOps.lean,IxC/Kernel/Expr.lean):e.bvarB ≤ dearly cutoffs ininstantiate1Go/instantiate1Fast,instantiateListGo/instantiateListFast, andliftLooseBVarsGo/liftLooseBVarsFast, plus root cutoffs inabstract1Fast,lowerBVarsFast,instantiate1LiftFast, andinstLPFast, with full correctness and@[csimp]proofs.Parallel Pre-Read, Unified Role-Binding Admission &
O(1)Pool Installation (Ix/KernelCheck/Binding.lean,Ix/KernelCheck/Stream.lean,Ix/KernelCheck/Step.lean,Ix/KernelCheck/Pool.lean,Ix/KernelCheck/Run.lean,Ix/Ixon/CheckOrder.lean,Benchmarks/Kernel/CheckIxe.lean):Ix.KernelCheck.Stream.loadvia chunk-paralleldecodeChunkandpreReadChunk(preReadRecord) tasks so state-independentExpr .anonDAGs are constructed in parallel before Phase A, cutting sequential Phase A time onInit+Stdfrom50.83s→31.21s(-19.62s/-38.6%) and total 32-workerkernel-check-ixetime from66.10s→46.27s(-19.84s/-30.0%).Env.constsclones inIx.KernelCheck.PoolwithO(1)visibleBelowtracking, pre-computestierAddressesduring load, optimizesfastKeysOf,buildIndex, andCheckOrder, makesCheckIxeMeta.displayTablelazy, and buffers Pass 2 JSONL output writes (flushing on completion and watchdog exit).Incremental
finalizeFiltering,recordBlockFast&putNamedEntriesFusion (Ix/Compile/ExactKey.lean,Ix/Compile/ReadyQueue.lean,Ix/Compile/ReadyCompile.lean,Ix/Cert/Compile.lean,Ix/RoleBinding/Compile.lean,Ix/RoleBinding/Generate.lean,Ix/Ixon.lean):ExactKey.preseedKeyBEqviacontextHashand overlapsvalidationTaskwithReadyQueue.run.addedConstsinIx.RoleBinding.Compile.finalizeby!artifact.consts.contains ato eliminate false-positivehasNewRecandhasNewDPrjfull-env scans onInit+Std, proves and wiresrecordBlockFast(recordBlockFast_eq) inunownedRecursorWith, skips redundantCanonical.deConstantinGenerated.emit, deduplicatessliceSupportClosure, and fusesputNamedEntriesmask and byte sizing inIx.Ixon.3. Retirement of Uncertified Rust/Lean Pipelines & Test Suite Streamlining
With the certified Lean compiler (
Ix.CompileCertified) and certifiedIxCkernel checker (Ix.KernelCheck) established as the sole compilation and verification engines (and the pre-retirement Rust implementation archived onjcb/archive-rust-compiler-kernel), this PR removes the following (the PR's whole diff is-128,043net lines across514files):crates/ixon(crates/ixon/src/shard.rs,crates/ffi/src/lean_ixon.rs):ixonstatic DAG sharding (ShardManifest,AggNode,LeafRefinement,shard_static,shard_static_ordered,shard_static_graph,shard_manifest_explicit,shard_manifest_refine,build_sub_env*) and the sharedinput_contractstest fixtures fromcrates/kernelintocrates/ixon, and moves the 5 static sharding FFI entrypoints (rs_env_extract,rs_shard_env_static,rs_shard_manifest_from_partition,rs_shard_manifest_refine,rs_shard_static_graph) intocrates/ffi/src/lean_ixon.rs.ShardMapDeleted:crates/compile(32,571lines) andcrates/kernel(62,672lines) from the Cargo workspace.crates/ixonmodules (sharing_exact*,resource*,canon_univ.rs,contract/source.rs) andcrates/commonmodules (env.rs,name_table.rs).crates/ffi/src/{compile,kernel,graph,lean_env,lean_build,builder,ix*,lean_ixon/sharing,lean_ixon/compare}.rs(11,222lines) and removes 40 C-ABI@[extern]symbols.Ix/ShardMap.leanlibrary,Tests/ShardMap.lean, andBenchmarks/ShardMap.lean.DecompileDriver.lean,ImportIxe.lean,Check.lean,IxEval.lean,Commit.lean,ClaimHarness.lean,Apps/ZKVoting/Prover.lean, and CLI commands (decompile,validate-lean,compile-export,bench,addr-of) to the certified Lean compiler andIxCchecker (ix check-lean, including--json,--json-name, and--per-constbenchmark reporting).Ix/CompileResource.lean,Ix/Cli/DriverOptions.lean,Ix/Cli/CheckRsCmd.lean(ix check-rs),Ix/Cli/ProfileCmd.lean(ix profile), andIx/Cli/IngressCmd.lean(ix ingress).CompileCorrect,Ix.CompileCert,IxSharingVerify,Ix.Cert.FreshSnapshot, andIx.Compile.ReadyCompile.reportIO(retainingkernel-record-checkandcompile-ind-flagsin.primary), and streamlines.github/workflows/merge-tests.ymlfrom 9 matrix partitions down to 4 (ci:compiler-closures,ci:misc,ci:landing-initstd-cli, andCertified kernel) plusValgrind FFI.docs/ci.md("Retired suites") records each retired suite and what covers it now. Certification proves soundness; completeness and behaviour at scale are exercised by the real-corpus runs (initstd-reference,fidelity-initstd).4. Custom User Axioms (Strict by Default)
ix check-leanandkernel-check-ixedecline every axiom outside the standard roles unless--allow-user-axiomsis given. With the flag, an accept that depends on user axioms is reported as CONDITIONAL and lists those axioms. It is never reported as certified.IxCFold (IxC/Kernel/Cached/Policy.lean,IxC/Kernel/Admission.lean,IxC/Kernel/Admission/UserAxioms.lean):Cached.AxiomPolicy(.strict/.allowUser) parameterises a single axiom arm (checkAxiomDeclC).Admission.checkBytesUnder,checkConstantsUnderand the tieredcheckBytesTieredUsingUnder/checkConstantsTieredUnderreturn the checked environment together with the user axioms the accept depends on..allowUser, the fold declines an axiom whose type restates the pinned specification ofpropext,Classical.choice,sorryAxorQuot.sound(axiomRoleSpecHit?). Admission refuses the policy unless the role table bindssorryAx,propextandClassical.choice(admitAxiomPolicy,Error.axiomRoleUnbound). Together these close a path where an unboundsorryAx, read as an ordinary axiom, was admitted.IxC/Kernel/Audit/Roots.lean):checkDeclsUnder_eq_checkDecls: without user axioms, the fold under any policy is the certified fold, with the same verdict, environment and failure.checkDecls_iff_userAxioms: the certified fold accepts exactly when the user-axiom fold accepts with no user axioms.checkBytesUnder_strict_of_nilandcheckBytesTieredUsingUnder_strict_of_nil: an.allowUserrun that reports no user axioms yields the strict entry's certifiedReceipt/TierReceipt.checkBytesUnder_has_model_of_nil(IxC/Kernel/Admission/UserAxioms/Model.lean): an accept under any policy that lists no user axiom has a model in every set theory.Ix/RoleBinding/UserAxioms.lean,Ix/RoleBinding/Artifact.lean,Ix/Cli/CheckLeanCmd.lean,Benchmarks/Kernel/CheckIxe.lean):--allow-user-axiomsfirst runs the kernel'sadmitAxiomPolicy .allowUseron the artifact's role binding. A refusal exits3incheck-leanand2inkernel-check-ixe. Every path to the record-by-record checker (Ix.KernelCheck.Step/Pool/Run) runs after this check.CONDITIONAL on K user axioms, with each axiom's address (and its name in meta mode). The run exits5and refuses--host-out/--host-store.check-leanpasses 99,514 of 99,519 subjects and exits3.Lean.trustCompilerdeclines as a non-standard axiom, andLean.reduceNat,Lean.ofReduceNat,Lean.reduceBoolandLean.ofReduceBoolare blocked by it.initstd-referencepins exactly this refused set.--allow-user-axioms, the run is CONDITIONAL onLean.trustCompiler,Lean.ofReduceNatandLean.ofReduceBool, and exits5(2:27 wall).5. Follow-Up Review Fixes
Kernel-Check and Compile Performance (
Ix/KernelCheck/Pool.lean,Ix/KernelCheck/Stream.lean,Ix/RoleBinding/Artifact.lean,Ix/RoleBinding/Compile.lean,Ix/Compile/ReadyQueue.lean):prepareRecordsdecodes in parallel.decodeRecordsPar_eqandprepareRecordsPar_eqprove it computes the same value.finalizecompiles the role certificates during the source compile on whole-environment compiles (prefetchCertificates).compileReport: published candidates are freed off the publication thread..ixehas Blake3a24fd146…eca9a3. Thekernel-check-ixerows, with their timing fields removed, are byte-identical to the base binary's (98,030 rows).c9575dca1)kernel-check-ixe --jobs 32load16.7s7.0s-58%kernel-check-ixephase A33.5s7.0s-79%kernel-check-ixetotal57.3s20.5s-64%(2.8×)kernel-check-ixeuser CPU444s152s-66%compile-leancompileReport31.9s27.9s-13%compile-leanfinalize5.03s1.78s-65%compile-leantotal42.3s35.2s-17%ix compile-exportRegression Fixed (Ix/CompileCertified.lean,Ix/Cli/CompileExportCmd.lean):compile-exportnow skips that pre-check (defaultRoles := false). The artifact's own binding is still checked infinalize, and role generation still checks each role against its certificates.main's, and regression tests cover it.Merge-Queue Tiers Green. All of these failures were already present at
c9575dca1.compiler-selected-closure-e2e,checker-support-regression: the report parser acceptstypedrows, which must give a tier safety as their reason.canon-closure-aux: IxC declines an inductive block read without its recursor. A newselectedleg type-checks each seed in its self-contained selected closure.kernel-tutorial: 376 passed, 0 failed. The changes:native_decidefixtures must not pass under strict.nestedSpecLocalFis a corner case whose expected outcome is "either", following lean-kernel-arena'scorner-cases/nested-nonuniform-paramandbugs/nested-unused-param. IxC's decline is pinned with its reason.tut06_bad01must be rejected in Source mode.CI Workload (
.github/workflows/{ci,nix,merge-tests}.yml,Tests/Main.lean,lakefile.lean):ixonandexact-sharingsuites run their checks concurrently, taking primary from507.6sto355.9son the box.ci:cli:binding-proof-cli(75.6 GBpeak) moves toci:compiler-closures, andcompile-determinismcompiles with--local.ci:cligoes from503.8sto165.4s, and lean-test's memory peak from75.6 GBto47.8 GB.nix.ymldrops the dev-shelllake testand the flake's clippy and nextest checks, whichci.ymlalready runs.Ix.Cert.AuditleavesIxTests' import closure and is built bycheck-kernel.merge-tests.ymlbuilds once per merge group, in abuildjob whose output the partitions restore.ffi-testsexecutable: 5:50 under Valgrind, whereIxTests ffihadn't finished after 23.5 min.admission-hash-diff-initstd(landing) compares native and pure Blake3 admission hashes on every record, blob and the binding of the Init+Std artifact.Tests:
kernel-user-axioms(primary).record-decodingcases moved intokernel-record-check.Blake3 Digests Throughout:
Ix.FileDigest.blake3Filereplaces SHA-256 ininitstd-reference,compile-determinism,CheckIxePaired,PinGenand theIxC/Kernel/Ixon/RoleData.leanprovenance.artifact.blake3before its next run.Dead Code and Stale Docs:
Ix.CanonM.canonEnv;ix-benchcrate;shardManifestFromPartitionchain;IxSharingVerify.UniformCappedSizeand its 13 audit roots;rustOnlyLimitKeys;CompileError/DecompileError;KernelCheckplumbing;check-lean's--clear-every/--no-verify.compileAndFinalize.docs/retired-rust.mdsummarises the retired Rust.docs/certified-compiler-progress.mdwithdraws the unmeasured4.65s/44.6sfigures.Known limitation, deferred.
Ix.Cert.RecursorsOwnedmatches recursors to families by name. So a closure holdingHAdd.recbut notHPow.recis refused, because those alpha-equivalent families merge into one block. A name-free restatement is planned as follow-up work.Benchmark Results on
perfspec(Init+Std, 117,694 inputs / 100,402 records, 32 workers)These
perfspectables were measured before §§4–5 and were not re-run. For the §5 changes, see its before/after table.This PR)ReadyBenchmarkcanon2,210 ms2,175 ms2,071 ms-6.3%ReadyBenchmarkcompileReport33,221 ms29,828 ms27,478 ms-17.3%(-5.74s,1.21×)ReadyBenchmarkfinalize5,075 ms5,307 ms4,557 ms-10.2%(-0.52s,1.11×)ReadyBenchmarkserialize1,264 ms1,238 ms1,251 ms-1.0%ReadyBenchmarktotal-ms45,017 ms41,663 ms38,613 ms-14.2%(-6.40s,1.17×)ReadyBenchmarkProcess Wall46.84s43.62s40.69s-13.1%(-6.15s)ReadyBenchmarkPeak RSS7,881 MB7,698 MB7,525 MB-39.0%vs PR #665 (12,331 MB)ReadyBenchmarkOutput Blake3a24fd146...eca9a3a24fd146...eca9a3a24fd146...eca9a3kernel-check-ixestreaming load6,348 ms6,348 ms8,725 ms(incl. parallelpreReadRecord)kernel-check-ixephase A50,829 ms45,519 ms31,211 ms-38.6%(-19.62s,1.63×)kernel-check-ixemarkPersistent1,675 ms1,004 ms972 ms-42.0%kernel-check-ixephase B(32w)3,893 ms3,522 ms3,199 ms-17.8%(1.22×)kernel-check-ixePass 2+ tier3,355 ms3,254 ms1,970 ms-41.3%(1.70×)kernel-check-ixe --jobs 32Total66,100 ms56,120 ms46,265 ms-30.0%(-19.84s,1.43×)kernel-check-ixePeak RSS2,879 MB2,336 MB2,746 MB-5.5%vs PR #665 (2,905 MB)graph-cross(182,249 constants, vs archived Rust)3,954 ms(Rust)2,232 ms(Lean)2,232 ms(Lean)1.77×faster than Rustcondense-cross(182,305 constants, vs archived Rust)4,864 ms(Rust)3,859 ms(Lean)3,859 ms(Lean)1.26×faster than RustBenchmark Results on
perfspec(Mathlib, 783,115 inputs, 32 workers, lookahead 8192)jcb/ix-certified-v3)jcb/ix-certified-v3-followup)load6,348 ms6,506 ms6,470 ms-0.6%+1.9%select136 ms134 ms130 ms-3.0%-4.4%source-contracts977 ms985 ms964 ms-2.1%-1.3%canon24,187 ms23,864 ms24,476 ms+2.6%+1.2%compileReport369,900 ms341,690 ms295,635 ms(4m 55.6s)-46,055 ms(-13.5%,1.16×)-74,265 ms(-20.1%,1.25×)finalize66,435 ms7,310 ms6,201 ms(6.20s)-1,109 ms(-15.2%,1.18×)-60,234 ms(-90.7%,10.71×)serialize42,742 ms13,225 ms12,296 ms(12.30s)-929 ms(-7.0%,1.08×)-30,446 ms(-71.2%,3.48×)write681 ms696 ms711 ms+2.2%+4.4%total-ms511,430 ms(8m 31.4s)394,439 ms(6m 34.4s)346,908 ms(5m 46.9s)-47,531 ms(-12.1%,1.14×)-164,522 ms(-32.2%,1.47×)10:30.02(630.02swave)6:53.34(413.34s)6:05.91(365.91s)-47.43s(-11.5%,1.13×)-264.11s(-41.9%,1.72×)~110 GiB~110 GiB65.68 GiB(67,257,828 kB)-40.3%(~44 GiBsaved)-40.3%458b7798...9374a458b7798...9374a458b7798...9374aVerification Gates
The commands of the
ci.yml,nix.ymlandmerge-tests.ymljobs (all butcuda-compile) were run on the head,cc78388af, on a 64-core / 495 GB test box, in three parallel lanes:lake build --wfail,lake build ix,IxTests,Apps.ZKVoting.Prover,ffi-tests,kernel-check-ixe,lake -d IxC build --wfail,Ix.Cert.Auditand the kernel fence targets1459s10.8 GBlake exe ix codegen --check&--trace-bundle --check; toolchain versions agree268s1.3 GBlake test(primary)1359s47.9 GBlake lint(including the sharing-proof trust audit)330s3.1 GBlake test -- --tier ci:cli178s2.9 GBixon-v4-primitives&ixon-v4-tests --primitives86s3.0 GBlake test -- --tier ci:compiler-closures667s75.6 GBlake test -- --tier ci:misc&Apps.ZKVoting.Proverkernel-tutorial376/0)1077s25.8 GBlake test -- --tier ci:landing-initstd-cliinitstd-reference: 103 roles admitted, 99,514/99,519, Blake3a24fd146...eca9a3)322s13.8 GBlake run check-kernel --with-model27s(built by the first step)3.0 GBffi-testsunder Valgrind (generic codegen, as CI builds it)830s13.1 GBcargo fmt --check,cargo clippy -D warnings,cargo check,cargo nextest(CI's features)1095s9.7 GBnix flake check(ix-tests)2012smain2s