Repository navigation
certified kernel and certified compilation - #665
Merged
Merged
Conversation
A name a fold state binds is exactly a key the input stores a constant under: the binding is a claim of a compiled block (Resolution's provenance), either a projection's name, which is a member's or a constructor's own name (inputsNamed), or the block's key, an element of a block of the input's condensation. The condensation's blocks hold the graph's own keys, read exactly here (blocksOfDisc_exact, block_exact, blockKey_exact; Condense.blocksOfDisc_mem reads them only up to the stored hash), and the ground graph's keys are the input's (envSerial_key, groundSplit_key). So a name a closure constant's term mentions and the snapshot binds is a closure constant (sub_of_ref), the snapshot's resolution publishes it, and the artifact's entry that hashes like it is under that exact name (nameHashes_distinct): TraceSegments.MentionsPublished, with each group kind's mentions shown to be a closure constant's (definitions_mentioned, definition_mentioned, axiom_mentioned, quot_mentioned, types_mentioned, recursors_mentioned). The fold block lemmas of TraceFold now live in GroupRuns.FoldBlock's namespace, so they apply with dot notation.
FamilyGroups stated the family check's meaning locally until the compile report had it. ReportChecks now defines FamilyBlocks, InFamily and InRecursors in the same form (FamilyBlocks reads compileBlocks env, definitionally CompiledRefs.envBlocks env), with familyBlocks giving it from compileReport. Drop the local copies and use those.
The definitions of a block of two or more have distinct names (definitions_distinct), and a name one of them applies with a member's ingress key is that member (definitions_exactNames): the block's compile references no record of its own block, its members are published apart, and a mentioned name the block binds is a closure constant published at its binding, so one ingress key gives one address (GroupRuns.addr_of_key, without Source totality). This uses a local copy of BlockRefs.exactNames_of whose published and sameKey premises are asked only at bound mentioned names and at members (exactNames_bound); a binding of a name no closure constant mentions need not be published. A singleton group's constant (a definition, an axiom or a quotient) compiles alone at its fold block, to runBlock's final state, and its one claim is the block record, published under the constant's name (singleton_compiled, lone_compiled, with definition_single, axiom_single and quot_single for the group's side). definitions_occ_input: a name a definition of such a block applies is a key the input stores a constant under.
Quotient Source's collapse keeps or drops each declaration of a lowered group by the names it declares. New Ix.Cert.CollapseWhole: - collapseRead_whole: a read whose names are fresh in the collapse state and pairwise distinct is kept whole (an invariant over the collapse's loop). - owned_iff: along a trace, the collapse owns exactly the names its reads declare. - trace_baseClosed: along quotient Source's trace, every kept name has its base kept: ordinary names are their own base, and a derived name is in an inductive read's generated prefix, whose block names that read keeps. - lowered_inductive_whole, trace_inductive_whole: an inductive group is lowered only when its block's names are fresh; its derived names are then fresh too (their bases are block names), and lowerInductive's declared names are distinct, so the read is kept whole. - TraceAt (each read with the trace before it, at that trace's collapse state), InductiveWhole, inductiveWhole_of_traceAt. ClosureLayout.trace_lowered gains a TraceAt conjunct, proved in the same induction; closureOrder_segments and unitsRead_of_layout's callback carry it. TraceSegments: InductiveNeeds loses its kept field; inductive_at takes it, derived from InductiveWhole in segmentsRead_of_needs; the per-cut obligation of unitsRead_of_needs now receives InductiveWhole.
Quotient Source lowers a group of several definitions to one declaration per member, at the member's quotient key, and its collapse keeps or drops each declaration by whether an earlier read declares its key. The reader's block segments need the read kept whole or dropped whole (BlockNeeds.collapse). New module Ix/Cert/BlockCollapse.lean: - collapseRead_whole_or_none: a read of declarations with distinct keys, none generated, is kept whole when no key is declared earlier and dropped whole when every key is, from the collapse's retained subsequence and which keys earlier reads declare; - block_raw_keys: the lowering declares each member once, in the block's dependency order, at distinct keys when members are published apart; - dPrj_claimant, earlier_block: a name published at a definition projection is a definition that a block of several compiled, so an earlier group with a name where one member is published is a group of several definitions at the same block, with a name where every member is published; - block_collapse: BlockNeeds.collapse for a lowered item of the trace, from Premises, the trace's Steps and the schedule's conversions. SourceDeclares: defOrder_perm states what defOrder_complete's proof already showed (the order lists each member once); defOrder_complete now uses it.
The compile report's inductive-input checks now have their meanings and theorems in ReportChecks. Three modules still stated their own copies: - TraceSource.FamilyLevelParams: family_levels now takes FamilyLevelParams, whose third conjunct (a recursor's level count is its family's or one more) it does not use; - BindingsResolve.ConstructorIndices: its lemmas and TraceFold's FoldBlock.bound now take ConstructorIndices; - RecursorIndex.Checks: RecursorIndexFacts and RecursorIndex now use RecursorSlotsUnique, RecursorShapes, FamilyNamesStored and FamilyLevelParams, and the analysis helpers they are stated with. No statement changes beyond the premises' names; each premise is discharged from compileReport by constructorIndices, familyLevelParams, recursorSlotsUnique, recursorShapes and familyNamesStored.
…atives Every group of quotient Source's graph that converts has its quotient terms in the scope of representatives (`TraceGood.converted_good`, the `good` field of `TraceSegments.TraceNeeds`). A name a closure constant's terms reference is published. The compile read the constant's sources as `Related` terms at any names that its bindings and its block's members satisfy, so every referenced name is a member of the block the fold compiled it in, or a binding of the fold's snapshot (`lone_names`, `block_names`, `fold_member_names`). Both are keys the input stores a constant under, so the closure holds the name and publishes it. A recursor's rules name their constructors outside its terms; the report's family-name check makes those input keys. The ingress keys each referenced name by its ingress key (`ingress_good`), so a converted group is in the scope of input keys. Quotient Source's hint override, renaming onto representatives and canonical levels keep every key in scope (`convGood_quotient`).
The reader's segment theorems ask that every state the trace's reads are read from have its projection owners, constant types and inductive blocks in the scope of representatives (TraceNeeds.states). New module Ix/Cert/TraceStates.lean: - prelude_good: the prelude's state names no input (the decided prelude check), so it lies in every scope of ids; - commit_good, collapse_good: a commit of a good read keeps a state good, and a read the collapse keeps from a good lowering is good; - lower_good: a lowering of a group whose terms lie in the scope lies in it. A definition's, axiom's or quotient constant's noted type is its converted one. An inductive group's owners and block are its block's, and its declarations, the generated ones included, are fixed by a renaming that fixes the scope's ids and moves every other id (lowerInductive_mapKeys at a state that is its own renaming); a term such a renaming fixes names only the scope's ids; - states_good: TraceNeeds.states, by induction over the trace's reads, from the prelude check, the trace's Steps and the groups' good terms; - trace_states_good: the same for a trace over the schedule from the prelude's state, with the groups' goodness from TraceGood.converted_good.
Discharge every field of `TraceSegments.TraceNeeds` and give `Obligation.ReaderStreams` (`ReaderStreamsTrace.readerStreams`), then `CompileCorrect` through `compileCorrect_unchanged` with the other proved obligations (`compileCorrect_of`). - `good`: `TraceGood.converted_good`; `states`: `TraceStates.trace_states_good`; `levels`, the headers' level parameters and `noSelf`, and an inductive group's level parameters, constructor names and shape come from quotient Source's acceptance (`TraceSource`). - Every scheduled item of a trace converts (`trace_scheduled`): a refused conversion ends the trace. - Axioms and quotient constants compile alone (`TraceFold.lone_compiled`); blocks of definitions are distinct, name their members exactly and are collapsed whole (`TraceFold`, `BlockCollapse`). - An inductive group's types and recursors run at their fold blocks (`GroupRuns.types_compiled`, `recursors_family`), and the closure's recursor index files them (`RecursorIndex.closure_recursor_index`). Its members have distinct names (`inductive_distinct`): the reader's lowering declines a block whose declarations repeat a key, and the block's `indDecl` declares every member's key, a function of its name. Three statements about the compile remain premises: the closure's record layout (`LayoutsHold`) and the definitions' hints (`SingletonsHinted`, `BlocksHinted`).
The reader takes a definition's hint at its member reference: at the member's projection record, or at the member's block address when no stored projection record projects it. A stored definition projection names as its block an address whose stored record is a block record (projections_owned), so none projects a lone record's member (no_projection_of_lone), and a singleton definition's hint is read at its own record. The fold keeps it (reach_owned): a merged block is checked against the store and against itself, so the merge only adds records; the block record is stored before its projections; and a block with a projection other than itself was built from Muts payloads, which the canonical sharing keeps (built_muts, runBlock_rows).
The reader takes a definition's reducibility hint from the artifact's anonHints at its address (hintsOf), and quotient Source takes the same entry (fiberHintsMap), so the two agree whenever it exists (CtxAgree.hints_agree); a definition without one would be read at no hint. The compile records every definition's hint, so a real artifact always has one, but showing that from the compile would take a walk of the whole block compile for one field. checkReport now refuses an artifact in which a published input definition, theorem or opaque has no anonHints entry at its address (unhintedDefinition, twenty-three checks), naming it. DefinitionsHinted is its meaning and definitionsHinted gives it from compileReport; CheckReportOk gains hints. Byte-neutral: no artifact changes. Audit: checkReport's and CheckReportOk's prints re-frozen for the new check and field, and a section auditing the new theorems. The test compiles the closure of Nat.add, which passes, and erases the hint at Nat.add's address, which the check refuses, naming the definition.
A singleton definition's record is lone, so no stored projection projects its member (ProjectionOwners.no_projection_of_lone) and the reader reads its hint at the record's own address; quotient Source reads the same anonHints entry (CtxAgree.hints_agree), and the compile report's hint check makes it present (definitionsHinted). Two alpha-equivalent definitions published at one address share that entry, which the assembly merges, so both sides still read one hint. singleton_hint, definition_compiled, and definition_needs: the whole DefinitionNeeds of a singleton definition group, at quotient Source's hints.
Prove BlockCompiled for a quotient Source group of two or more definitions, at quotient Source's hints. The fold's run of the block gives the run, the members' freshness, the claim, the bindings, the blobs and the mentioned names. Each member is published at its projection record (BlockPublication.member_published); the reader reads the member's hint there, since a successful report stores one projection per member, and quotient Source reads the same anonHints entry. The report's hint check makes the entry present. New: TraceFold.projection_hint, defs_definitions, block_compiled, with an axiom guard on block_compiled (the standard three).
The compiler compiles every block in Lean's order (sourceClasses), so the
structural comparator, the partition refinement it fed and the proofs
about them have no caller left.
- Delete Ix/Compile/Canon/{Order,Classes,Expr} and the comparator proofs
in Ix/CompileCert/Canon (Level, Expr, Const, Rel, Cache, Sort, Group,
Refine, Round, Coarsest, EqSound). The Canon umbrella keeps the
condensation.
- Keep what the reader path uses, under the same module names:
Canon.Basic (the preorder combinators, now importing Ix.SOrder, with
the two lawfulness lemmas that lived in Level), Canon.Ref (the name and
address orders) and Canon.Ctx (the class context's lemmas); drop the
comparator halves of Ref and Ctx.
- CompileM: delete sortConsts, throwCmpError, constAddrLookup and
orderRecursorFamily; the driver calls none of them.
- Delete the lemmas whose statements are about the class sort:
ProjectionLayout's sort section, MutualProjections' class agreement,
MutualArtifact's mutual_sorted_correct and mutual_ordered_correct with
the family-order permutation, MutualInductiveReading's driver_singleton
and inductive_reads_driver(_source), NoCtor's
inductive_reads_driver_sourceAccepts, and Claims' class-sort section.
No other module uses them. MutualProjections imports Canon.Ctx in place
of the comparator chain.
- Audits: ReadingAudit's name-order and class-context roots keep only the
remaining lemmas; the class sort's roots and runtime lists, and the cert
audit's class-sort section and driver-inductive root, are removed.
Re-frozen: the driver-inductive guard, 12 to 7 roots (the five deleted
lemmas) and 2 to 1 safe definitions (orderRecursorFamily).
- Tests: drop the comparator check from ContractTransport and the tests
of the universe-substitution helper Canon.substLevels, deleted with
Canon/Expr, from SourceContract.
Init+Std compiles byte-identically.
Both check canonical block order, which the compiler no longer produces. - Delete the twins suite: Twins, its fixtures library, NonCanonical and its record, the LetNonDep and NestedLevels fixtures, and the clique and oracle fixtures that only twins imported; drop its registry entry and the TwinsFixtures library. - Delete BlockOrderHost, the differential of canonical classes against the Rust kernel, with its kernel-order executable and check-kernel step. - compile-schedule-identity runs over the fixture corpus alone and requires no block failure under any schedule (the expected refusals were the twins' presentations).
Every block is stored in its source's order, so only a recursor block's order, its motives', is constrained. - Ixon.BlockOrder keeps the motive-order check (checkMotives, checkRecord). The structural comparator, the refinement (canonicalClasses), the structural check of other blocks, the order limits and the entry that ran the check before the checker (BlockOrder.checkBytes) are removed with their theorems. - Ixon.Authenticated: remove checkBytesBlockOrder and its theorems. - KernelFidelity's egress report calls checkRecord directly. - Tests: BlockOrder keeps the motive-order cases and checks that other blocks are accepted in any member order; CertifiedEntry and Authentication drop the removed entry's cases. - Audits re-frozen: BlockOrder.Audit's runtime closure is checkRecord's alone, and it adds no extern or unsafe primitive to the projection entry's; Authenticated.Audit's closure loses the removed entry's 141 compiled functions and String.compare, the one extern only it reached. The removed entry's prints and axiom guards are gone.
…heck - ix-compile: delete compare_level through compare_const, the merge sort and sort_consts, and BlockCache's comparison cache; keep recursor_family_position and source_classes. Delete compare_const_tests; keep the flag tests that do not compare (flag validation, the safety flag through compilation, the kernel's safety check). Drop the comparator check from semantic_contract's test and the sort_consts unit test. - ix-kernel: delete canonical_check.rs, the canonical-order-test feature with convert_anon_order_fixture, and the comparator contract test. - ix-ffi: delete lean_ixon/order.rs (rs_kernel_canonical_classes, whose Lean caller went with the kernel-order suite) and the feature from test-ffi.
Add `Ix.Cert.LayoutsHold` with `layouts_hold`, the closure's record layout (`ClosureLayout.Layout`) for every accepted compiled closure whose schedule lets every group through. Its statement is the body of `ReaderStreamsTrace.LayoutsHold`; the module does not import `ReaderStreamsTrace`, so that module can import it. `layout_of` gives the layout at any hints. - `block`: `BlockLayout.layoutBlock_of_claimed` with `LayoutExtra.claimedIn_of`. - `extra`: `LayoutExtra.layout_extra_of`. - `refs`: `CompiledRefs.compiledRefs_of`, read against quotient Source's graph by `LayoutRefs.layoutRefs_of_compiled`. Its premises are `TraceFold.cacheRefs`, `blobsApart`, the report's acyclicity check, `inBlocks` (every closure name is a member of the block that claims it) and `refsAt_of`, from each group name's fold block. The new fact is that every member of a fold block is published at a record the block owns (`FoldBlock.owned`). The member is a closure name, so some fold block claims it (`GroupRuns.foldBlock_of`). That block holds the member (`claim_in_block`: a block's key, a member's name, or a constructor that the family check puts in its inductive's block), so it is the same block (`block_unique`). Two runs of one block, in states that read the same constants, claim the same names (`runBlock_names`, `claim_transfer`): both take the lone path, or both run the members' loop and the mutual compile, whose rows carry their sources' names (`mutual_names`). The block owns the record of each of its claims (`claim_owned`). This covers inductive blocks, recursor families and lone records alike.
Add Ix/Cert/CompileCorrectProof.lean. It discharges the three statements ReaderStreamsTrace.compileCorrect_of still took: the closure's record layout (layoutsHold, from LayoutsHold.layouts_hold), a singleton definition's hint at its lone record (singletonsHinted, from TraceFold.definition_needs), and a block member's hint at its projection record (blocksHinted, from TraceFold.block_compiled). Then ReaderStreamsTrace.compileCorrect : CompileCorrect is proved outright. Axiom guards on all four show only propext, Classical.choice and Quot.sound. Audit: import the module and freeze the final theorem's statement next to compileCorrect_unchanged's. The composition skeleton's roots go from 25 to 27: the two added are ReaderStreamsTrace.compileCorrect and ReaderStreamsTrace.readerStreams, so the audit's axiom guard covers the complete proof. The section's prose says CompileCorrect is proved. Docstrings: Statement.lean's header no longer says CompileCorrect is stated but not proved, and drops the validation premises the statement lost with the changed path. Composition.lean and ReaderStreamsTrace.lean point to the proof.
The comparator that used SOrd was removed with the canonical block order, so the module has no users. The crate doc also listed a mutual-block module that now lives in ix-compile; list the modules the crate actually has.
TcError::NonCanonicalBlock was raised only by the kernel's canonical-order check, and TcError::UnexpectedFVarInComparator only by the canonical-order comparator. Both were removed with the canonical block order, so neither variant is constructed any more. Drop them and their Display arms.
The kernel's comments still said the compiler sorts each block with sort_consts and regenerates nested auxiliaries in that order. The compiler now stores each block in Lean's member order and keeps Lean's auxiliary recursors, so the stored recursor block is in Lean's order. Say so in the RecursorAuxOrder docs, the ingress notes and the recursor-alignment comments, and describe max_smart by its remaining user, the inductive-flags check. Comments only.
Ixon.BlockOrder now checks only a recursor block's motive order; it no longer reads projection records or ends in checkConstantsAt. Name the projection variant alone as the user of checkConstantsAt, ByteError.outcome and the projection-record reading. Comments only; no docstring here is frozen by an audit.
Ix/Runtime/Thread.lean still declared setLeanThreadStackSize in Ix.Tc, after the Ix.Tc checker was removed. Put it in Ix.Runtime, matching its module, and update the two CLI callers and the Rust shim's doc comment. The extern symbol is unchanged.
Auxiliary generation and its Source service were removed, but the typing tier's module docs still named them as the reason the tier types unsafe inductive blocks and builds its answer view. The remaining user is resource typing's uncertified part, so say that. Also drop references to a deleted agreement test and to the compiler's former canonical motive order in the in-model nested reader, and a stale caller in the Source evidence docstring. Comments only; no audited docstring changes.
docs/kernel.md still said CompileCorrect was an unproved Prop over nominal Source and an older value-model quantifier, with permutations, images and changed-cone checks outstanding. State the theorem as it is: per closure over quotient Source, proved by ReaderStreamsTrace.compileCorrect, with reference acceptance and one quotient Source value model for every strong target model, and say that ix compile-lean runs the report checks. Drop the removed block-order entry: the projection variant is the only entry variant, and the recursor motive-order check is described as the standalone check the fidelity suite runs. Refresh the frozen closure table to the audits' current values, and drop the retired kernel-order gate step.
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 25.5s | ❌ failed typecheck | +24.0% (1.24× slower) |
2.16K | ❌ failed typecheck | -19.4% (1.24× slower) |
199.64 GiB | ❌ failed typecheck | +9.7% (1.10× larger) |
184,450 | ❌ failed typecheck | -0.1% | 114 | ❌ failed typecheck | +75.4% (1.75× more) |
- Base hardware (bencher @ 426a242): 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
…s, and support user axioms in claims - Fold u8_range_check into read_checked_byte_stream (2 bytes/row via io_read) and remove the second assert_byte_stream pass - Inline all 108 0-arg constant functions (@role_*, @spec_digest, @spec_version, etc.) to eliminate singleton circuits - Add per-arm DAG CSE and sparsification in RoleSpecGen, and return (fam, op) from role_prim_family for flat primitive dispatch - Group remaining cold role-admission, decidable, and aggr functions (IxVM: 382 -> 221 circuits, -41% committed width; Aggr: 102 -> 73 circuits, -23% committed width) - Pull custom user axiom admission into IxC.Kernel and wire custom user axioms into ClaimContext.axioms and IxVM claim verification - Validate Claim::Binding once per shard batch in rs_aiur_toplevel_shard_check_batch while running shards with assume_binding = true - Regenerate RoleSpec.lean, Rust/CUDA codegen, trace-bundle, and trace-fixtures
- Release obsolete publication snapshots and deduplicate ready-plan parents with an ordered hash-set pass - Expand source units once and cache certified family checks with exact-name proof-carrying entries - Reuse authenticated compact mutual-owner layouts, scan nested application spines once, and prove an indexed inductive shape guard (indShapeOkFast) equivalent to indShapeOk - Select sequential sharing evaluation when task capture would force disproportionate whole-DAG scratch copies - Format Rust crates and pass strict clippy, source hygiene, and Lean --wfail / audit checks
Member
Author
|
!benchmark aiur fresh |
Member
Author
|
!benchmark aiur-sharded-env BENCH_ENVS=ISLB |
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 |
11.434 s | 10.548 s | -7.8% (1.08× faster) 🟢 | 1m 1.4s | 59.038 s | -3.9% 🟢 | 45.290 | 61.620 | +36.1% (1.36× faster) 🟢 | 70.63 GiB | 71.70 GiB | +1.5% | 4.98 MiB | 6.27 MiB | +25.9% (1.26× larger) |
31.1 ms | 38.3 ms | +23.3% (1.23× slower) |
122.53B | 126.79B | +3.5% |
1 | 1 | +0.0% |
Char.ofOrdinal_le_of_le |
7.105 s | 7.461 s | +5.0% (1.05× slower) |
39.602 s | 45.132 s | +14.0% (1.14× slower) |
69.770 | 79.680 | +14.2% (1.14× faster) 🟢 | 51.23 GiB | 57.86 GiB | +12.9% (1.13× larger) |
4.94 MiB | 6.25 MiB | +26.3% (1.26× larger) |
31.0 ms | 41.3 ms | +33.0% (1.33× slower) |
88.19B | 91.74B | +4.0% |
1 | 1 | +0.0% |
Array.extract_append |
8.287 s | 8.240 s | -0.6% | 44.203 s | 44.240 s | +0.1% | 36.380 | 54.700 | +50.4% (1.50× faster) 🟢 | 51.18 GiB | 52.63 GiB | +2.8% | 4.83 MiB | 6.18 MiB | +28.1% (1.28× larger) |
30.7 ms | 38.1 ms | +24.3% (1.24× slower) |
89.42B | 92.97B | +4.0% |
1 | 1 | +0.0% |
Std.HashMap |
4.757 s | 5.504 s | +15.7% (1.16× slower) |
27.145 s | 29.316 s | +8.0% (1.08× slower) |
78.210 | 101.240 | +29.4% (1.29× faster) 🟢 | 35.85 GiB | 37.92 GiB | +5.8% (1.06× larger) |
4.89 MiB | 6.19 MiB | +26.5% (1.27× larger) |
30.2 ms | 37.7 ms | +24.8% (1.25× slower) |
58.88B | 63.34B | +7.6% (1.08× more) |
1 | 1 | +0.0% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
4.288 s | 4.841 s | +12.9% (1.13× slower) |
25.859 s | 27.065 s | +4.7% |
72.310 | 99.320 | +37.4% (1.37× faster) 🟢 | 34.02 GiB | 35.16 GiB | +3.3% |
4.84 MiB | 6.17 MiB | +27.4% (1.27× larger) |
32.1 ms | 38.3 ms | +19.3% (1.19× slower) |
51.63B | 55.47B | +7.5% (1.07× more) |
1 | 1 | +0.0% |
String.append |
744.2 ms | 946.5 ms | +27.2% (1.27× slower) |
2.554 s | 3.690 s | +44.5% (1.45× slower) |
128.060 | 211.640 | +65.3% (1.65× faster) 🟢 | 5.92 GiB | 6.29 GiB | +6.2% (1.06× larger) |
4.58 MiB | 6.15 MiB | +34.5% (1.34× larger) |
29.3 ms | 40.6 ms | +38.7% (1.39× slower) |
3.27B | 4.58B | +40.0% (1.40× more) |
1 | 1 | +0.0% |
Nat.add_comm |
524.4 ms | 619.3 ms | +18.1% (1.18× slower) |
1.080 s | 1.256 s | +16.3% (1.16× slower) |
42.580 | 41.390 | -2.8% | 4.58 GiB | 4.64 GiB | +1.3% | 4.39 MiB | 5.41 MiB | +23.1% (1.23× larger) |
25.2 ms | 30.1 ms | +19.2% (1.19× slower) |
295.32M | 390.06M | +32.1% (1.32× more) |
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.312 s | 4.062 s | +22.6% (1.23× slower) |
36.558 s | 39.912 s | +9.2% (1.09× slower) |
76.070 | 91.150 | +19.8% (1.20× faster) 🟢 | 52.02 GiB | 58.42 GiB | +12.3% (1.12× larger) |
2.68 MiB | 2.68 MiB | +0.2% | 16.0 ms | 18.4 ms | +15.5% (1.16× slower) |
93.98B | 118.73B | +26.3% (1.26× more) |
Char.ofOrdinal_le_of_le |
3.120 s | 3.893 s | +24.8% (1.25× slower) |
35.261 s | 39.691 s | +12.6% (1.13× slower) |
78.360 | 90.600 | +15.6% (1.16× faster) 🟢 | 51.65 GiB | 58.06 GiB | +12.4% (1.12× larger) |
2.67 MiB | 2.68 MiB | +0.6% | 15.7 ms | 16.0 ms | +1.4% | 92.20B | 118.09B | +28.1% (1.28× more) |
Array.extract_append |
3.385 s | 3.933 s | +16.2% (1.16× slower) |
36.510 s | 39.678 s | +8.7% (1.09× slower) |
44.040 | 60.990 | +38.5% (1.38× faster) 🟢 | 50.37 GiB | 57.65 GiB | +14.4% (1.14× larger) |
2.67 MiB | 2.69 MiB | +0.9% | 16.2 ms | 16.8 ms | +3.8% |
89.48B | 115.50B | +29.1% (1.29× more) |
Std.HashMap |
3.268 s | 3.956 s | +21.1% (1.21× slower) |
35.681 s | 39.610 s | +11.0% (1.11× slower) |
59.500 | 74.930 | +25.9% (1.26× faster) 🟢 | 50.90 GiB | 57.43 GiB | +12.8% (1.13× larger) |
2.67 MiB | 2.68 MiB | +0.3% | 15.7 ms | 15.4 ms | -1.6% | 91.56B | 116.71B | +27.5% (1.27× more) |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
3.213 s | 4.002 s | +24.6% (1.25× slower) |
35.624 s | 39.615 s | +11.2% (1.11× slower) |
52.490 | 67.850 | +29.3% (1.29× faster) 🟢 | 50.99 GiB | 57.27 GiB | +12.3% (1.12× larger) |
2.67 MiB | 2.68 MiB | +0.2% | 15.9 ms | 16.6 ms | +4.9% |
91.20B | 117.39B | +28.7% (1.29× more) |
String.append |
2.820 s | 3.960 s | +40.4% (1.40× slower) |
33.745 s | 38.502 s | +14.1% (1.14× slower) |
9.690 | 20.280 | +109.3% (2.09× faster) 🟢 | 46.68 GiB | 53.63 GiB | +14.9% (1.15× larger) |
2.67 MiB | 2.68 MiB | +0.6% | 17.0 ms | 15.5 ms | -8.9% (1.10× faster) 🟢 | 82.79B | 109.19B | +31.9% (1.32× more) |
Nat.add_comm |
2.670 s | 3.401 s | +27.4% (1.27× slower) |
33.055 s | 35.751 s | +8.2% (1.08× slower) |
1.390 | 1.450 | +4.3% 🟢 | 45.93 GiB | 49.04 GiB | +6.8% (1.07× larger) |
2.67 MiB | 2.68 MiB | +0.4% | 15.5 ms | 16.1 ms | +3.9% |
77.17B | 94.55B | +22.5% (1.23× more) |
Aggregate flat join (1 pair)
| pair | execute-time (main) | execute-time (PR) | Δ% | prove-time (main) | prove-time (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | proof-size (main) | proof-size (PR) | Δ% | verify-time (main) | verify-time (PR) | Δ% | fft-cost (main) | fft-cost (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Nat.add_comm + String.append |
3.682 s | 4.269 s | +15.9% (1.16× slower) |
38.261 s | 40.604 s | +6.1% (1.06× slower) |
54.62 GiB | 58.89 GiB | +7.8% (1.08× larger) |
2.83 MiB | 2.89 MiB | +2.2% | 17.6 ms | 17.1 ms | -3.0% | 104.32B | 125.01B | +19.8% (1.20× more) |
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 38.0s | 1m 38.9s | +1.0% | 28.390 | 36.770 | +29.5% (1.30× faster) 🟢 | 70.63 GiB | 71.70 GiB | +1.5% |
Char.ofOrdinal_le_of_le |
1m 14.9s | 1m 24.8s | +13.3% (1.13× slower) |
36.910 | 42.390 | +14.8% (1.15× faster) 🟢 | 51.65 GiB | 58.06 GiB | +12.4% (1.12× larger) |
Array.extract_append |
1m 20.7s | 1m 23.9s | +4.0% |
19.920 | 28.840 | +44.8% (1.45× faster) 🟢 | 51.18 GiB | 57.65 GiB | +12.6% (1.13× larger) |
Std.HashMap |
1m 2.8s | 1m 8.9s | +9.7% (1.10× slower) |
33.790 | 43.060 | +27.4% (1.27× faster) 🟢 | 50.90 GiB | 57.43 GiB | +12.8% (1.13× larger) |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
1m 1.5s | 1m 6.7s | +8.5% (1.08× slower) |
30.410 | 40.310 | +32.6% (1.33× faster) 🟢 | 50.99 GiB | 57.27 GiB | +12.3% (1.12× larger) |
String.append |
36.298 s | 42.193 s | +16.2% (1.16× slower) |
9.010 | 18.510 | +105.4% (2.05× faster) 🟢 | 46.68 GiB | 53.63 GiB | +14.9% (1.15× larger) |
Nat.add_comm |
34.135 s | 37.007 s | +8.4% (1.08× slower) |
1.350 | 1.410 | +4.4% 🟢 | 45.93 GiB | 49.04 GiB | +6.8% (1.07× larger) |
- Base hardware (base run @ 426a242 (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
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 25.5s | 1m 29.0s | +4.1% |
2.16K | 2.07K | -4.0% |
199.64 GiB | 195.94 GiB | -1.9% | 184,450 | 184,335 | -0.1% | 114 | 116 | +1.8% |
- Base hardware (bencher @ 426a242): 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
…CharOfNat admission
Regroup cold IxVM and aggregation helpers to reduce active openings while preserving the function library and constrained entrypoints. Extract cold substitution branches, fuse PCS opening-width checks with the existing fold, and process four BLAKE3 input bytes per hot circuit row without skipping any byte or block-boundary check. Regenerate native Rust and production CUDA/trace artifacts through their standard producers. Add substitution, PCS and hash boundary regressions, reproducible function/circuit profiling, and stale-profile digest validation. Matched the benchmark's 103-role InitStd artifact and retained every checked constant, 50 FRI queries, log blowup 2, and zero proof-of-work bits. IxVM FFT cost falls across all seven benchmark workloads; verified Nat/String inner proofs shrink about 5%, and recursive FFT cost falls about 6%/8%, with a small increase in outer proof size. Use HashMap.alter for host IOBuffer arena appends so ownership permits in-place growth instead of repeated whole-arena copies. Preserve per-channel indices, duplicate-key semantics, and persistent snapshots. Validation:150 exact kernel/Eval cost fixtures, native output/IO/query parity, 2304 substitution boundary cases, hash and PCS rejection controls,19 generated trace tests, all standard producer check modes, and warning-free Main source typecheck. Record baseline provenance and measured proof-size tradeoffs in docs/benchmarking.md. Native codegen O0 builds were used for correctness; no production CI wall-time speedup is claimed.
Member
Author
|
!benchmark aiur fresh |
Member
Author
|
!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 25.5s | 1m 17.6s | -9.3% (1.10× faster) 🟢 | 2.16K | 2.38K | +10.1% (1.10× faster) 🟢 | 199.64 GiB | 186.36 GiB | -6.7% (1.07× smaller) 🟢 | 184,450 | 184,335 | -0.1% | 114 | 114 | +0.0% |
- Base hardware (bencher @ 426a242): 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
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 |
8.691 s | 6.970 s | -19.8% (1.25× faster) 🟢 | 56.915 s | 49.907 s | -12.3% (1.14× faster) 🟢 | 48.860 | 54.040 | +10.6% (1.11× faster) 🟢 | 70.67 GiB | 67.08 GiB | -5.1% (1.05× smaller) 🟢 | 4.98 MiB | 5.43 MiB | +8.9% (1.09× larger) |
30.9 ms | 32.6 ms | +5.3% (1.05× slower) |
122.53B | 116.27B | -5.1% (1.05× fewer) 🟢 | 1 | 1 | +0.0% |
Array.extract_append |
5.797 s | 5.209 s | -10.1% (1.11× faster) 🟢 | 40.480 s | 38.336 s | -5.3% (1.06× faster) 🟢 | 39.720 | 39.360 | -0.9% | 51.36 GiB | 50.37 GiB | -1.9% | 4.83 MiB | 5.36 MiB | +11.1% (1.11× larger) |
29.6 ms | 32.0 ms | +7.9% (1.08× slower) |
89.42B | 85.54B | -4.3% 🟢 | 1 | 1 | +0.0% |
Char.ofOrdinal_le_of_le |
5.931 s | 5.083 s | -14.3% (1.17× faster) 🟢 | 37.988 s | 35.299 s | -7.1% (1.08× faster) 🟢 | 72.730 | 75.810 | +4.2% 🟢 | 51.13 GiB | 49.71 GiB | -2.8% | 4.94 MiB | 5.42 MiB | +9.6% (1.10× larger) |
31.1 ms | 32.9 ms | +5.5% (1.05× slower) |
88.19B | 83.05B | -5.8% (1.06× fewer) 🟢 | 1 | 1 | +0.0% |
Std.HashMap |
4.112 s | 3.432 s | -16.5% (1.20× faster) 🟢 | 26.504 s | 23.433 s | -11.6% (1.13× faster) 🟢 | 80.100 | 87.010 | +8.6% (1.09× faster) 🟢 | 35.74 GiB | 34.10 GiB | -4.6% 🟢 | 4.89 MiB | 5.36 MiB | +9.5% (1.10× larger) |
30.9 ms | 32.7 ms | +5.8% (1.06× slower) |
58.88B | 55.46B | -5.8% (1.06× fewer) 🟢 | 1 | 1 | +0.0% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
3.350 s | 3.104 s | -7.3% (1.08× faster) 🟢 | 24.234 s | 21.936 s | -9.5% (1.10× faster) 🟢 | 77.170 | 80.600 | +4.4% 🟢 | 34.05 GiB | 32.19 GiB | -5.5% (1.06× smaller) 🟢 | 4.84 MiB | 5.31 MiB | +9.8% (1.10× larger) |
30.6 ms | 34.6 ms | +13.2% (1.13× slower) |
51.63B | 48.32B | -6.4% (1.07× fewer) 🟢 | 1 | 1 | +0.0% |
String.append |
721.2 ms | 704.5 ms | -2.3% | 2.495 s | 2.369 s | -5.1% (1.05× faster) 🟢 | 131.060 | 111.020 | -15.3% (1.18× slower) |
5.76 GiB | 5.52 GiB | -4.2% 🟢 | 4.58 MiB | 5.09 MiB | +11.3% (1.11× larger) |
28.0 ms | 29.5 ms | +5.3% (1.05× slower) |
3.27B | 2.91B | -10.9% (1.12× fewer) 🟢 | 1 | 1 | +0.0% |
Nat.add_comm |
534.4 ms | 478.6 ms | -10.4% (1.12× faster) 🟢 | 1.127 s | 1.048 s | -7.0% (1.08× faster) 🟢 | 40.810 | 32.440 | -20.5% (1.26× slower) |
4.36 GiB | 4.11 GiB | -5.7% (1.06× smaller) 🟢 | 4.39 MiB | 4.88 MiB | +10.9% (1.11× larger) |
25.3 ms | 28.3 ms | +11.9% (1.12× slower) |
295.32M | 362.82M | +22.9% (1.23× more) |
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.187 s | 3.228 s | +1.3% | 35.333 s | 35.430 s | +0.3% | 78.710 | 76.120 | -3.3% |
52.34 GiB | 54.39 GiB | +3.9% |
2.68 MiB | 2.69 MiB | +0.3% | 15.7 ms | 15.7 ms | +0.0% | 93.98B | 102.42B | +9.0% (1.09× more) |
Array.extract_append |
2.968 s | 2.969 s | +0.0% | 34.630 s | 35.069 s | +1.3% | 46.430 | 43.030 | -7.3% (1.08× slower) |
50.42 GiB | 53.30 GiB | +5.7% (1.06× larger) |
2.67 MiB | 2.69 MiB | +0.8% | 15.8 ms | 15.7 ms | -1.0% | 89.48B | 101.02B | +12.9% (1.13× more) |
Char.ofOrdinal_le_of_le |
3.128 s | 3.146 s | +0.6% | 34.932 s | 35.327 s | +1.1% | 79.100 | 75.750 | -4.2% |
51.82 GiB | 54.32 GiB | +4.8% |
2.67 MiB | 2.69 MiB | +1.0% | 15.7 ms | 15.5 ms | -1.1% | 92.20B | 102.52B | +11.2% (1.11× more) |
Std.HashMap |
3.163 s | 3.062 s | -3.2% 🟢 | 35.924 s | 34.645 s | -3.6% 🟢 | 59.100 | 58.850 | -0.4% | 50.82 GiB | 52.96 GiB | +4.2% |
2.67 MiB | 2.70 MiB | +1.3% | 15.6 ms | 15.5 ms | -0.9% | 91.56B | 100.87B | +10.2% (1.10× more) |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
3.048 s | 3.105 s | +1.9% | 34.844 s | 34.638 s | -0.6% | 53.670 | 51.040 | -4.9% (1.05× slower) |
50.95 GiB | 52.41 GiB | +2.9% | 2.67 MiB | 2.70 MiB | +0.8% | 16.0 ms | 15.6 ms | -2.2% | 91.20B | 98.88B | +8.4% (1.08× more) |
String.append |
2.879 s | 2.995 s | +4.0% |
33.429 s | 34.406 s | +2.9% | 9.780 | 7.640 | -21.9% (1.28× slower) |
47.14 GiB | 50.35 GiB | +6.8% (1.07× larger) |
2.67 MiB | 2.70 MiB | +1.3% | 16.8 ms | 16.2 ms | -3.4% 🟢 | 82.79B | 93.30B | +12.7% (1.13× more) |
Nat.add_comm |
2.785 s | 2.710 s | -2.7% | 32.824 s | 32.110 s | -2.2% | 1.400 | 1.060 | -24.3% (1.32× slower) |
45.78 GiB | 47.72 GiB | +4.2% |
2.67 MiB | 2.70 MiB | +1.4% | 15.4 ms | 15.4 ms | -0.3% | 77.17B | 88.44B | +14.6% (1.15× more) |
Aggregate flat join (1 pair)
| pair | execute-time (main) | execute-time (PR) | Δ% | prove-time (main) | prove-time (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | proof-size (main) | proof-size (PR) | Δ% | verify-time (main) | verify-time (PR) | Δ% | fft-cost (main) | fft-cost (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Nat.add_comm + String.append |
3.714 s | 3.719 s | +0.1% | 38.549 s | 37.549 s | -2.6% | 54.84 GiB | 56.00 GiB | +2.1% | 2.83 MiB | 2.88 MiB | +2.1% | 17.7 ms | 18.0 ms | +1.3% | 104.32B | 118.74B | +13.8% (1.14× more) |
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 32.2s | 1m 25.3s | -7.5% (1.08× faster) 🟢 | 30.150 | 31.600 | +4.8% 🟢 | 70.67 GiB | 67.08 GiB | -5.1% (1.05× smaller) 🟢 |
Array.extract_append |
1m 15.1s | 1m 13.4s | -2.3% | 21.410 | 20.560 | -4.0% |
51.36 GiB | 53.30 GiB | +3.8% |
Char.ofOrdinal_le_of_le |
1m 12.9s | 1m 10.6s | -3.1% 🟢 | 37.890 | 37.890 | +0.0% | 51.82 GiB | 54.32 GiB | +4.8% |
Std.HashMap |
1m 2.4s | 58.078 s | -7.0% (1.07× faster) 🟢 | 34.010 | 35.110 | +3.2% 🟢 | 50.82 GiB | 52.96 GiB | +4.2% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
59.077 s | 56.574 s | -4.2% 🟢 | 31.650 | 31.250 | -1.3% | 50.95 GiB | 52.41 GiB | +2.9% |
String.append |
35.924 s | 36.775 s | +2.4% | 9.100 | 7.150 | -21.4% (1.27× slower) |
47.14 GiB | 50.35 GiB | +6.8% (1.07× larger) |
Nat.add_comm |
33.951 s | 33.158 s | -2.3% | 1.350 | 1.030 | -23.7% (1.31× slower) |
45.78 GiB | 47.72 GiB | +4.2% |
- Base hardware (base run @ 426a242 (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
enabled stacked auto-merge
November 3, 2026 22:49
arthurpaulino
previously approved these changes
Nov 4, 2026
| ListNode.Nil => | ||
| -- A missing bucket does not run ro_fold. Keep the original width | ||
| -- check on this defensive path as well. | ||
| assert_eq!(eq_zero(list_length(p_x) - list_length(p_z)), 1); |
Member
There was a problem hiding this comment.
assert_eq!(list_length(p_x), list_length(p_z));
johnchandlerburnham
removed this pull request from the merge queue due to a manual request
Nov 4, 2026
johnchandlerburnham
enabled stacked auto-merge
November 4, 2026 02:54
samuelburnham
approved these changes
Nov 4, 2026
github-merge-queue
Bot
removed this pull request from the merge queue due to no response for status checks
Nov 4, 2026
johnchandlerburnham
removed this pull request from the merge queue due to a manual request
Nov 4, 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.
Certified Compilation v3 (
Ix.CompileCertified)Overview
This pull request delivers Certified Compilation v3 (
Ix.CompileCertified), an end-to-end verified compilation and verification stack from Lean 4 environments (Lean.Environment) to content-addressed Ixon artifacts (Ixon.Env) and the standalone verified kernel (IxC).Key deliverables:
Machine-Checked Soundness Theorem (
Ix.Cert.ReaderStreamsTrace.compileCorrect):Ix.Cert.CompileCorrect(Ix/Cert/CompileCorrect.lean) over quotient Source (SourceAcceptsQ): for any dependency-closed set of roots accepted by the quotient Source front end at the compiled artifact where no constant in the closure is reported as failed (NoFailure), and where the artifact's role bindings (PublishedRolesBound), address map (PublishedAgree), and role-evidence bundle (EvidenceCheck.EvidenceAgrees,RoleClosure.RoleEvidenceChecks) check out:Published ixe sub).IxonAcceptsRef) accepts the compiled closure at the reference level in topological dependency order (ClosureOrder).RenamesSource: preserving types, definition bodies, theorem statements and proofs, inductives, constructors, and recursors).sorryAxconstant in the closure — including collapsed α-equal alias fibers — resolves to a total compiled reading (ReadingCovers).readingAt) to a law-abiding value model of quotient Source (CommutesStrong,IxonCommutesCovering).Ix.Cert.compileCovers : CompileCovers), pure BLAKE3 content authenticity (Ix.Cert.compileAuthentic : CompileAuthentic), and worklist closure exactness (Ix.Cert.closureCorrect : ClosureCorrect).[propext, Classical.choice, Quot.sound]), with zerosorryornative_decideaxioms.Four-Layer Trust-Boundary Audit Suite:
Ix/Cert/Audit.lean,IxC/Kernel/Audit/Roots.lean,IxSharingVerify/Audit/Statements.lean): Freezes the exact definitions (#print) and theorem signatures (#check) of every certification and sharing obligation so no specification can drift silently.IxC/Kernel/Audit/Axioms.lean): Traverses checked types, bodies, and inductive constructors directly inenv.checked(#guard_kernel_axioms) rather than relying on imported axiom summaries.Ix/Cert/ModuleAudit.lean,IxSharingVerify/Audit/CompiledCode.lean): Enforces#guard_module_axiomsacross 18 compiler/scheduler/role-binding modules and#guard_module_axioms_under Ix.Cert Ix.CompileCert, and scans the compiler's import closure to ensure every@[csimp]theorem is an audited root and no unapprovedunsafe,partial,@[implemented_by], or@[extern]declaration exists inIx.Sharing.*.IxC/Kernel/Audit/Runtime.lean,Ix/Cert/RuntimeAudit.lean): Walks the emitted compiler IR (Lean.IR.findEnvDecl) from public entrypoints (Ix.Cert.compile,Ix.Compile.ReadyCompile.reportIO,Ix.CompileM.compileCertified,Ix.RoleBinding.Compile.finalize,Ixon.serEnv), stripping compiler-generated suffixes (_redArg,_boxed,_impl,_spec_<n>), tracking both forward, module-overwritten, and inlined target-side@[implemented_by]and@[csimp]substitutions, verifying@[csimp]theorem axioms viaIx.Kernel.Audit.collect, and freezing the exact runtime boundary.Three-Way Aligned Role Admission (103-Role Catalog across
IxC, Rustix_kernel, andIxVM):Nat,Bool,Char,UInt32,String,ByteArray, andBitVecoperations) validated by structural pins, well-founded recurrences, and equation certificates acrossIxC, the Rust kernel (crates/kernel/src/role_admission/), and theIxVMcircuit backend.Polynomial-Budget Canonical Sharing & Tiered Fast Verification (
Ix/Sharing/,IxSharingVerify/):sorrycorrectness, format, meaning, idempotence, and polynomial budget-sufficiency proofs (IxSharingVerify) paired with proved@[csimp]fast evaluators: closure-local and area-truncated component search (Ix/Sharing/FamilyFast.lean,Ix/Sharing/Exact/AreaSearch.lean), light lazy component contexts (Ix/Sharing/FamilyContext.lean), parallel exact-$K_{16}$ subset folds (Ix/Sharing/FamilyParallel.lean), and cached single-width materialization (Ix/Sharing/Exact/TieredFast.lean).Verified Dependency-Driven Parallel Ready-Queue Runtime (
Ix/Compile/Ready*):Ix/Compile/ReadyQueue.lean,Ix/Compile/ReadyCompile.lean) backed by proof-carrying ordered publication (Ix/Compile/ReadyPublication.lean,Ix/Compile/WorkerReplay.lean), returning an explicit subtype witness{ result // result = Ix.Cert.compileReport env }.Architecture & End-to-End Pipeline
flowchart LR A["Lean.Environment<br/>Source Ingress & Contracts<br/>(Ix/Compile/FrontEnd.lean)"] --> B["Parallel Canonicalization<br/>canonInput<br/>(Ix/CompileCertified.lean)"] B --> C["Dependency-Ready Parallel Compile<br/>ReadyCompile.reportIO = compileReport<br/>(Ix/Compile/ReadyCompile.lean)"] C --> D["Canonical Sharing & Tiered Fast<br/>LightContext / TieredFast<br/>(Ix/Sharing/FamilyContext.lean)"] D --> E["21-Check Report Verification<br/>checkReport / checkReportPar<br/>(Ix/Cert/Compile.lean)"] E --> F["Role Binding & Support Finalizer<br/>Ix.RoleBinding.Compile.finalize<br/>(Ix/RoleBinding/Compile.lean)"] F --> G["Parallel Ixon Serialization<br/>Ixon.serEnv<br/>(Ix/Ixon.lean)"]1. Source Ingress & Contract Checks (
Ix/Compile/FrontEnd.lean,Ix/Environment.lean,Ix/CompileCertified.lean)prepareCertified): Scans input constants in parallel (Ix.Compile.checkOrdinaryConstants) for contract registrations, measure hints, duplicate names, or key mismatches; when contracts are present, resolves and validates all binder and semantic resource contracts (Ix.CompileM.checkPreparedSource,Ix.Resource.validate).canonInput): Partitions constants into consecutive slices canonicalized across worker tasks (Ix.CanonM.canonChunk, proved equivalent to per-constant canonicalization inIx.Cert.Canon.canonChunkCorrect) and joined in deterministic order while verifying zero structural hash collisions (inputs == prepared.length).Ix/Compile/FrontEnd.lean): Computes per-constant reference sets (FrontEnd.graph,@[csimp] theorem graph_eq : @GraphM.envSerial = @graph) and immediate grounding refusals (FrontEnd.ground,@[csimp] theorem ground_eq : @groundConsts = @ground) across task chunks while preserving exact map insertion and worklist propagation order.2. Rust Kernel Typechecking & Role Admission (
crates/kernel/src/role_admission/,IxC/Kernel.lean,Ix/Kernel.lean)crates/kernel/src/role_admission/):RoleTable) against structural inductive/constructor/recursor shapes, primitive anchor specifications (groups.rs), well-founded recurrence certificates (validate_wf_op), and equational theorem evidence (equations.rs,validate_structural_op).check_support),DefinitionSafety::Safeguards on all theorem evidence, and locality of evidence closures (check_evidence_locality).crates/kernel/src/tc.rs,check.rs,whnf.rs,extra_reductions.rs):TypeChecker::unfoldswithIxC(matches!(safety, DefinitionSafety::Safe)soPartialandUnsafedeclarations never unfold during WHNF or definitional equality).ExprData::Prj) inwalk_for_unsafeand gates native reductions (ExtraReductions::from_admitted, includingRole::StringOfList) strictly on admitted role equations.3. Dependency-Driven Ready-Queue Parallel Compilation (
Ix/Compile/ReadyQueue.lean,Ix/Compile/ReadyCompile.lean,Ix/Compile/ReadyPublication.lean,Ix/Compile/WorkerReplay.lean)Ix/Compile/WorkerContext.lean,Ix/Compile/WorkerSuccess.lean,Ix/Compile/WorkerReplay.lean):compileBlockdepends only on the fixed source environment, sharing limits, resolved dependency addresses (SameInputs), and compatible blob tables (Compatible), establishingrunBlock_successfor speculative worker execution.Ix/Compile/ReadyQueue.lean):makePlan) and schedules ready SCC blocks onto worker tasks as soon as their parent blocks finish, without waiting for coarse wave stragglers.Ix/Compile/ReadyPublication.lean,Ix/Compile/ReadyCompile.lean):Candidateagainst the liveCompileEnvsnapshot (selectOutcome,checkedOutcome_eq), falls back to the reference worker on any frame mismatch, and returns an IO subtype{ result : ReportResult // result = Ix.Cert.compileReport env }proved equal to the pure specification (ReadyCompile.reportIO).4. Canonical Sharing & Tiered Fast Checker (
Ix/Sharing/FamilyFast.lean,Ix/Sharing/Exact/AreaSearch.lean,Ix/Sharing/Exact/TieredFast.lean,Ix/Sharing/FamilyContext.lean)Ix/Sharing/Exact/AreaSearch.lean,Ix/Sharing/FamilyFast.lean):phiA,areaFoldDirect) rather than the full ancestor closure, proved equal to the reference evaluator (AreaProof.searchComponentsArea_eq,localPhi_eq) with automatic fallback if the opacity guard (tGuard) ever fails.Ix/Sharing/FamilyContext.lean,Ix/Sharing/FamilyParallel.lean):eraseUnused) unless an opacity fallback forces the lazy thunk (fullContext), and parallelizes exactParallel.table_eq_function).Ix/Sharing/Exact/TieredFast.lean,Ix/Sharing/FamilyContext.lean):emptyEvalacross widthsInit+StdandMathlib), avoiding redundant DAG materialization and re-expansion while preserving exact@[csimp]definitional equivalence (LightContext.expanded_eq,canonicalTieredExpanded_eq_C).5. Certified Replay Checker & Soundness Theorem (
Ix/Cert/Statement.lean,Ix/Cert/Compile.lean,Ix/Cert/CompileCorrect.lean)Ix/Cert/Compile.lean):Ix.Cert.compileReportexecutescompileUncheckedfollowed bycheckReport(@[csimp] theorem checkReport_eq_par), verifying 21 structural and cryptographic invariants (CheckReportOk): coverage (uncovered), BLAKE3 content authenticity (unauthentic), reference acyclicity (referenceCycle), exact name-hash injectivity (nameHashCollision), mutual block consistency (mutsMismatch), address resolution (resolutionMismatch,unresolvedPublished), constructor/inductive/recursor shapes (recursorShapeError,unownedRecursor), role record kinds (roleRecordKind), literal support roles (literalRoleUnnamed), and reducibility hints (unhintedDefinition).Ix/Cert/CompileCorrect.lean,Ix/Cert/EvidenceCheck.lean):artifactCheckdecidesPublishedRolesBound,PublishedAgree, andEvidenceCheck.EvidenceAgreeson the compiled artifact, discharging the artifact premises ofCompileCorrect(CompileCorrect.artifactChecked,CompileCorrect.checked).6. Finalization & Ixon Serialization (
Ix/CompileCertified.lean,Ix/RoleBinding/Compile.lean,Ix/Ixon.lean)Ix/RoleBinding/Compile.lean,Ix/RoleBinding/Generate.lean):sliceSupport?,sliceSupportRoles?, including projection owners and sibling projections), merges any missing role support and certificate closures (mergeSupport), synthesizes the artifact'sRoleTableand theorem evidence records (Generate.generate,Generated.emit), and validates the finalized artifact (checkFinalized,Ix.Cert.EvidenceCheck.evidenceCheck).Ix/Ixon.lean):qsortByAddrPar), parallelizes canonical Merkle tree construction (Ix/Merkle.lean), and encodes sections concurrently into pre-sized buffers (Ixon.serEnv).Trust Boundary & Audit Suite
Ix/Cert/Audit.leanIxC/Kernel/Audit/Roots.leanIxSharingVerify/Audit/Statements.lean#print) and theorem types (#check) ofCompileCorrect,CompileCovers,CompileAuthentic,ClosureCorrect,SourceConsistent,IxonConsistent,IxonAuthentic,SourceValueSound,IxonValueSound, and all 175+ sharing/kernel theorem roots.IxC/Kernel/Audit/Axioms.leanIx/Cert/Audit.leanIxSharingVerify/Audit/Statements.leanenv.checked(Ix.Kernel.Audit.collect,#guard_kernel_axioms). Every theorem and executable root is bounded by[propext, Classical.choice, Quot.sound];sorryAxandLean.ofReduceBool(native_decide) are rejected.Ix/Cert/ModuleAudit.leanIxSharingVerify/Audit/CompiledCode.lean#guard_module_axiomsacross 18 compiler/scheduler/role-binding modules (Closure,HostAdmission.Theorems,Artifact*Theorems,RecordDecoding,Generate,FrontEnd,CompileDriver,WorkerContext,TaskWindow,WorkerSuccess,WorkerReplay,ReadyPublication,ReadyQueue,ReadyCompile,CompileCertified) and#guard_module_axioms_under Ix.Cert Ix.CompileCert. ScansLean.Compiler.CSimp.extacross the compiler's import closure to require every@[csimp]theorem to be an audited root, and bansunsafe,partial,@[implemented_by], and@[extern]inIx.Sharing.*(outside the single pointer-cache hintexprPtr).IxC/Kernel/Audit/Runtime.leanIx/Cert/RuntimeAudit.leanLean.IR.findEnvDecl) reachable fromIx.Cert.compile,Ix.Compile.ReadyCompile.reportIO,Ix.LeanIngress.checkSourceCollapsedBundledAt,Ix.Cert.compileChecked,Ix.Cert.artifactCheck,Ix.CanonM.canonEnv,Ix.CompileM.compileCertified,Ix.CompileM.validateFinalized,Ix.RoleBinding.Compile.finalize, andIxon.serEnv. Resolves stacked compiler suffixes (_redArg,_boxed,_impl,_spec_<n>), detects@[implemented_by]and@[csimp]at source, module-overwritten, and inlined target sites, verifies@[csimp]theorem axioms viaIx.Kernel.Audit.collect, validatesAssumedSubstitutionextern sets (Address.admissionHashAddress.blake3), and freezes the exact project-level runtime inventory.Soundness, Security & Code Quality Hardening
PublishedRolesBound,PublishedAgree,Ix.Cert.EvidenceCheck.evidenceCheck, and full post-finalization artifact verification (checkFinalizedcoveringliteralRoleUnnamed,unreadablePublished,unhintedDefinition,unownedRecursor,recursorShapeError, androleRecordKindagainst the finalized role table) intocompileCertifiedandRoleBinding.Compile.finalize.ExactName/ExprKey):Ix.NameandIx.Exprlookups with structural collision checks andExactKeymaps acrosscanonInput,mergeSupport,IndFlags(walkCache,occCache,replaceFVarsMap,hasInvalidSpecRef),familyRecursors/familyBlockOk,CompileDriver.reclaimedNames, and Rustind_flags(replace_all_nested,has_ind_occ,checked_expr::any).check_support) across all anchor, structural-op, well-founded-op, and theorem-evidence validators incrates/kernel/src/role_admission/groups.rs.DefinitionSafety::Safeon theorem evidence, restrictedTypeChecker::unfoldsto safe definitions only, addedExprData::Prjstructure checks towalk_for_unsafe, addedRole::StringOfListtoExtraReductions::from_admitted, and fixedlean_egressinductive flag assignment (v.is_reflexive).Vec::with_capacityallocations from untrustedTagNheaders incrates/compile/src/decompile.rs, replaced.expect()calls on demoted §5 metadata windows incrates/ixon/src/env.rs(LazyMetaWindow) and universe conversions with checkedResultreturns, and implemented iterativeDropforUnivandKUnivto prevent stack overflow on deep universe terms.arith::saturated()intiered_at_width) and fixed left-associative binary operator precedence (+,-,*) in the Aiur surface macro DSL (Ix/Aiur/Meta.lean).keepAlive/dropAsync):keepAlivewith a live value dependency so Lean'sElimDeadParams(___redArg) pass cannot erase the captured payload ofdropAsync, keeping large AST/environment reference-count teardowns off the critical path.Performance Benchmarks
End-to-end certified compilation ($\to$ $\to$ $\to$ $\to$ $\to$ $\to$ $\to$
loadselectsource-contractscanoncompileReportfinalizeserializewrite) achieves sub-10s compilation onInit+Std(4.65 son the 32-core / 64-threadperfspechost) and sub-60s compilation onMathlib(44.6 sonperfspec), while producing bit-for-bit identical canonical.ixonoutputs.Headline Summary (
perfspec32-Core / 64-Thread Benchmark Host & 32-Core Cloud Box)d3e3a6f41, 32 vCPU)perfspecHost (d3e3a6f41, 32C / 64T)98.05 s43.26 s(2.27×vs. wave)4.65 s(target< 10 s)e48adef624e70bcdd3f22e1d96251682ac046a088700ccf5cf512f1b49afcda110:30.02(630.02 s)6:53.34(413.34 s,1.52×vs. wave)44.6 s(target< 60 s)458b779888c8f9627bba58d41a3a2cdf48c38eec32d0a4f36606856782c9374aPhase-by-Phase Breakdown (32-Core Cloud Box,
john@18.216.46.61, 32 Workers)1.
Init + Std(117,694 Constants)ms)load2,864 ms.oleanenvironment loadingselect10 mssource-contracts104 mscheckOrdinaryConstantsscancanon2,071 mscanonInput)compileReport29,594 mscheckReportParfinalize5,121 mscheckFinalizedserialize1,359 msIxon.serEnv)write69 ms253 MB,writeAtomic)3 msdropAsyncteardown (keepAliveretained)41,195 ms43.26 s(4.65 sonperfspec)2.
Mathlib(783,115 Constants)ms)ms)load5,910 ms5,862 ms-48 ms.oleanenvironment loadselect128 ms124 ms-4 mssource-contracts955 ms941 ms-14 mscanon24,710 ms24,614 ms-96 mscompileReport369,900 ms341,690 ms-28,210 ms(1.08×)finalize66,435 ms7,310 ms9.09× faster(-59,125 ms)sliceSupportRoles?O(roles) lookup + delta-onlypreflight/checkFinalizedserialize42,742 ms13,225 ms3.23× faster(-29,517 ms)qsortByAddrPar+ parallel Merkle hashing + pre-sizedByteArraywrite650 ms647 ms-3 ms2.35 GB,writeAtomic)24,996 ms26 ms961× faster(-24,970 ms)keepAlivedead-parameter erasure (dropAsync)511,430 ms394,439 ms(6m 34.4s)-116,991 ms(1.30×)6:53.34(413.34 son Cloud Box;44.6 sonperfspec)Verification & Codegen Synchronization
lake test --wfail&lake test --wfail -- --tier ci:cli: All 78 primary Lean test suites and 5 CLI integration suites (plusixon-v4-primitivesandixon-v4-tests --primitives) pass with 0 warnings/errors.lake run check-source-docs,lake lint -- --wfail,lake run check-modules&lake run check-kernel --with-model: Zero source hygiene violations across 1,975 files, zero lint violations, and zero kernel/model trust-boundary findings (sorry = 0,axiom = 0,unsafe = 0,partial = 0,implemented_by = 0,extern = 0), includingallCSimpEntriesscanning for inlined@[csimp]replacement targets (List.append_eq_appendTR) andkernel-source-ingressacross all 118,830Init+Stdconstants.cargo fmt --all -- --check,cargo clippy --workspace --all-targets -- -D warnings,cargo nextest run --workspace): Clean formatting, zero clippy warnings, and all Rust unit/integration tests passing.ix codegenandix codegen --trace-bundleartifacts (--checkverified), merged latestmain(#676), and updated allkernelCheckEntries, shard pipeline, andevalFftCostspins inTests/Ix/IxVM.lean,Tests/Main.lean, andTests/Ix/IxVM/Eval.leanwhile preserving bytecode/generated-kernel parity checks.