Repository navigation
WIP: improve certified kernel and certify compilation - #665
Open
johnchandlerburnham wants to merge 1072 commits into
Open
johnchandlerburnham wants to merge 1072 commits into
johnchandlerburnham wants to merge 1072 commits into
Conversation
The production sharing rule sharing-k16-greedy-v1 lived in the namespace
Ix.Sharing.FamilyPrototype, with the parameter Config.experimentK; both names
date from its measurement phase. Rename, with no change to behavior or bytes:
- the modules Ix.Sharing.FamilyPrototype{,Fast,Cached} become
Ix.Sharing.Family{,Fast,Cached}, and the namespace becomes
Ix.Sharing.Family, including the IxSharingVerify proofs and their audit
roots;
- Config.experimentK becomes Config.exactLimit: the largest component whose
family is every subset;
- the test suite sharing-family-prototype becomes sharing-family, and the
trace tool of the same name becomes sharing-family-trace;
- the Rust unit-test control uniform::experimental becomes
uniform::family_trace.
Internal error, test and doc messages that said "experimental" or
"prototype" now name the component family. The statement audit's root list
changes only in these names; its size and the fixed axioms are unchanged.
Also correct two stale docs. The IxSharingVerify root doc now describes the
production family route and its proofs apart from the reference exact
route. The lakefile no longer implies that no Ix module depends on
IxSharingVerify: Ix.CompileCert.SharingRoots and Ix.CompileCert.WireTables
import it.
FamilyCost is part of the family's main proof chain (its minimum-cost theorem is a statement audit root), so the root doc should not group it with the output-size groundwork modules.
The checked theory is Lean with its three standard axioms; evaluation by the compiler is outside it. The certified checker declines `Lean.trustCompiler` as a non-standard axiom and blocks `Lean.reduceBool`, `Lean.reduceNat`, `Lean.ofReduceBool` and `Lean.ofReduceNat`, which are built on it. The Rust kernel instead evaluated `reduceBool c` and `reduceNat c` by reducing the body of `c`, and accepted all five declarations. - Remove native evaluation: `try_reduce_native`, its primitive family and its re-entrancy flag. `reduceBool c` is now a stuck application of an opaque, as in the certified checker. - Decline each of the five declarations by canonical content address, and every checked declaration that refers to one of them, with the new `TcError::NativeEvaluation`. Inference without validation, which also drives auxiliary-definition generation, is unaffected. - Keep the three addresses that were not pinned yet in a kernel table (`primitive::native_evaluation_addrs`), not in `PrimAddrs`, whose parity table also scopes IxVM witnesses. The `primitive-address-parity` suite compares all five with a live compile through the new `rs_native_evaluation_addrs` symbol. On Init+Std the five are the only verdicts that change: `check-rs` now fails exactly them, which the certified checker declines or blocks. Tests: the re-entrancy test of the removed evaluator becomes a test that `reduceBool` of a constant unfolding to `true` stays stuck and does not convert to `true`; the reset test drops its assertions on the removed flag. New tests decline each of the five declarations and a declaration referring to one, and accept an ordinary axiom and definition of the same shape. `kernel-check-env`, which required every constant of the test environment to pass, now requires the five to be declined with the native-evaluation error and every other constant to pass.
The certified checker specifies Lean's kernel rules plus its primitive roles: the Nat basis with literals and fifteen operations on literals, Eq, Quot and the string-literal support. The Rust kernel also took shortcuts that have no specification there. Each is sound, but a Rust verdict that rests on one is not one the certified checker would give, so they are now off, and the terms they shortcut reduce by ordinary delta and iota: - Decidable: Nat.decEq/decLe/decLt on literals, which built Decidable.isTrue/isFalse from four pinned Nat lemmas, and the literal normalisation of Int.decEq/decLe/decLt arguments; - BitVec.toNat (BitVec.ofNat w n) and BitVec.ult on literals; - String operations on literals: the String.ofList collapse, append, decEq, back, Legacy.back, utf8ByteSize and toByteArray ""; - the Nat offset forms, as one unit: x + k, x / k and x % k kept stuck, the recursor-major cleanup to Nat.succ (x + k) and the definitional strip of a shared + k. The stuck forms without the cleanup leave recursors stuck on offset majors, so they cannot go off separately. Without them the strip reads only Nat.succ layers and rebuilds them as such; - the collapse of succ-step Nat.rec applications on a literal major. The groups are listed in the new extra_reductions module, and each reducer checks its group on entry. Every checker starts with none, and only unit tests of the reducers enable them (a test-only method), so the code stays for the groups the certified checker specifies later. Tests: the 21 unit tests of these reducers (their results, and their guards against misfiring) enable the groups explicitly. New tests check that a default checker takes no group, and that each group's shortcut does not fire by default.
Replace the nominal statement over the weak value-model commutation with the final statement, `Ix.Cert.CompileCorrect` (new module `Ix/Cert/CompileCorrect.lean`). From quotient Source acceptance at the compiled artifact, the compile's report with no failure in the closure, the pinned role configuration (`PublishedRolesBound`, `RoleClosure.RoleEvidenceChecks`), one validation hypothesis per kind of change (`KindAccepted`) and the Source forms of rewritten records inferring in their compiled closures (`SourceFormInfers`), it concludes that the closure is published and its compiled closure is accepted at the reference level, that every constant of the closure, a dropped alias included, reads as a compiled constant (`ReadingCovers`), and that every strong target model gives one value model of quotient Source for the whole closure (`CommutesStrong`). The reading takes a role key's address from the role table (`readingAt`). The older `reading` finds it by the role's Lean name among the published names, so it misses a representative that the table rule makes a role key when that name is unpublished; the two agree wherever `reading` is defined (`readingAt_of_reading`), so the conclusion gives `IxonCommutesStrongRef` (`IxonCommutesCovering.toStrongRef`). New module `Ix/Cert/ChangedCone.lean`: the record kinds that are not a renaming of their Source form (`ChangeKind`: changed components, regenerated auxiliaries, images, image computation-rule rows, rewritten call sites, transported cliques, clique rows, the cascade), the per call site rewrites (`CallRewrite`: the baseline development and O11a, O2, O3, O4, O6), the records of a kind read off the changed set (`KindRoot`), the validation hypotheses, and the changed-cone validator's interface (`ConeInput`, `ConeValidator.Sound`, `compileValidated`). The nominal-to-quotient link is now per instance (`NominalQuotientAgreeAt`, discharged by the executed quotient check). The universal form was false: on the deliberately aliased AuxDedup and AuxOwnership fixtures (218 names) nominal Source and the Ixon side accept while quotient Source declines, so a corollary assuming it held vacuously. `CompileCorrect.nominal` states the nominal corollary at the instances where the link holds. The `Commutes` docstring no longer claims that everything the source entails transports: a value model fixes types, `False`, `Eq` and definition values only. Audit re-freeze (`Ix/Cert/Audit.lean`), each change for the reason above: - removed the `#print` of the old `CompileCorrect` and the `#check`s of its `published`/`of_published`/`compileCorrect_iff_published` bridges; the bridges are restated for the new statement (against `CompileCorrectPublished`) and their `#print axioms` guards, unchanged in text, now cover the restated theorems; - `NominalQuotientAgree`'s `#print` replaced by `NominalQuotientAgreeAt`'s, with a `#check` and an axioms guard of `nominalQuotientAgreeAt_of_check`; - new section "The final statement": `#print` of the 27 new definitions the statement reads, `#check` of the 10 new theorems, and one `checkRoots` guard over 26 roots (definitions and theorems) at the three standard axioms.
`ChangedSet.Avoids` was described as the hypothesis the final statement takes. The statement takes no such hypothesis: the changed records are validated instead (`Ix.Cert.KindAccepted`), and a closure that avoids the set is the case of the proof in which the compiled closure is a renaming of its source. Docstrings only, in `Ix/Compile/ChangedSet.lean` and `Ix/Cert/Unchanged.lean`.
Output of ix codegen for the IxVM kernel and ix_aggr circuits as they stand after the binding claim: validator 4, the binding claim's validation, the validator-keyed check_owned and the binding discharge shapes. No hand edits. The trace bundle's generated writers are regenerated separately, with the CUDA units.
Bring in typing claims that assume the role binding (validator 4), the binding claim and its discharge in ix_aggr, ix prove-binding and the reusable --binding-proof, with the generated circuit code for those circuits. The generated files take this side's regeneration, which matches the merged circuits; the proofs merged since are disjoint.
Add compileReport_owned_stored: compileReport_owned_fresh's conclusion, plus that the block compile behind the claim has its block record (blockAddr, blockBytes) stored in the artifact. A name's block can then be read from the artifact at its claim. - mergeCompiledBlock_stored: a checked merge writes the block record first, and every later write at that address carries the same bytes (the merge's content check), so the record stays. - applyCompiled_stored and applyCompiled_failed: applying a compiled block stores its record when its check passes, and leaves the resolution and aux maps when it fails. - CompiledFresh now also records that the state the application made is on the run and, for a compiled outcome, stores the block's record. The provenance step takes a claim from a failed check as the earlier entry it is. - compileEnvFold_provenanceFresh adds that every record a state of the run stores is the artifact's (StepKeeps.stepKeeps, onRun_persists). compileReport_owned_fresh keeps its statement; it is now derived from the new theorem. The module now imports Ix.Cert.StepKeeps, and guards the axioms of both theorems: propext, Classical.choice and Quot.sound.
Bring in the proof that a claiming block's own record is stored in the artifact, alongside the fresh-snapshot provenance. Proofs only; disjoint from the binding validated once per aggregate.
Add Ix/Cert/BlockWire.lean, which proves BlockLayout.BlocksWire: every block runBlock returns is in the constant wire format. A block compiles as a lone constant's compileConstantInfo or a mutual block's compileMutualBlock, from the empty block state (BlockRecords.runBlockWithAux_records), whose tables are on the wire (BlockStart.wire_empty). EmissionDispatch.constant_codec and EmissionDispatch.mutualBlock_codec already show that both compiles return a block that decodes exactly, and so is wire-valid. The preseed puts the tables on the wire and the payload emitters keep them there (EmissionWire). The builder makes a wire-valid constant from wire tables and a payload whose header counts the emitters check (buildConstantWithSharing_wireWF_headers). The module guards the theorem's axioms: propext, Classical.choice and Quot.sound.
Split checkBlockClaims_walk out of checkBlockClaims_primary_agrees: a passed claim check's table holds every primary write, and every entry agrees with the resolution before the block. The earlier theorem keeps its statement and now follows from it. The table is what shows that a merged block resolves each of its claims at the claimed address.
Add compileReport_owned_block and Ix/Cert/BlockPublication.lean: the artifact facts that BlockRefs.exactNames_of takes for a definition block, from the fold's application of the block. compileReport_owned_block extends compileReport_owned_stored with two facts: - a closure name that a state of the run resolves is published at that address (the resolution persists by StepKeeps, and NoFailure rules out a failure); - every claim of the claiming block for a closure name is published at its address, with its record stored there. For the second, the application's merge resolves each primary claim at its claimed address (the claim walk agrees duplicate writes, foldl_insert_consistent) and stores each projection's record (mergeCompiledBlock_projection, by the content check). The fresh witness now records that a compiled block's check passed, which gives both. compileReport_owned_stored and compileReport_owned_fresh keep their statements and are derived from the new theorem. BlockPublication: - stored: the block's record decodes to the block (BlocksWire). - owned: member j of a block of several definitions is published at its projection memberProjection B j, whose owner is the block. - apart: members are published at distinct addresses, since one address holds one record and the projections differ in their index. - published: a closure name the snapshot resolves outside the aux map is published there. - sameKey: two closure names with one ingress key are published alike, from Source totality, where the key is not the sorryAx role's. - exactNames_of_published: exactNames_of with stored, owned and apart discharged. The modules guard their theorems' axioms: propext, Classical.choice and Quot.sound.
Add compileReport_owned_blobs: compileReport_owned_block's conclusion, plus that every blob the claiming block reads (its own blob table, then the snapshot's store, BlobWrites.readBlob) is stored in the artifact. A block's reference table can then tell a stored blob apart from a stored record. - StepKeeps: the relation a step keeps (KR) now also keeps every blob. Only a merge and the original-form promotion write blobs, and both fold the block's blobs into the store (mergeCompiledBlock_blobs). So every driver step keeps the blobs (stepBlobs). - FreshSnapshot: blobs persist along the run to its final state (onRun_grows), and the assembled environment stores the final state's blobs (assembleEnv_blobs). A checked compiled application holds the block's own blobs (applyCompiled_blobs). compileEnvFold_provenanceFresh adds that a state of the run's blobs are the artifact's. compileReport_owned_block, _stored and _fresh keep their statements and are derived from the new theorem. The module guards its axioms: propext, Classical.choice and Quot.sound.
Layout.extra asks that the edges the fold follows without a reference lead to records of names of quotient Source's groups. For recursor edges this follows from three facts: - the artifact's recursor index files recursors only under block records, so both records of a name whose block has indexed recursors resolve to that block; - the recursors it files there are published recursors of that name's family (RecursorsOwned, the meaning of a compile-report check); - the closure takes every recursor of the family of each of its inductives, constructors and recursors (DependsOn), and every closure name is a name of a group. Also prove that every group name of an accepted closure is a name the closure stores a constant under.
Every claim reads its role table, and building the table's maps by insertion was about a third of that read: each binding and each evidence entry went through a red-black insert with rebalancing. The bindings and the evidence entries arrive in strictly increasing role order, as the canonical codec requires, so the two maps keyed by role are now read straight into balanced trees: the first half of a run is the left subtree, the next entry the root and the rest the right subtree. Lookups ignore colours, and nothing inserts into a table once it is read. The index by address is keyed by interned pointers, in no particular order, and is still built by insertion. The reader's checks are unchanged: role indices known and strictly increasing, and no address bound to two roles. A claim's execution costs about 8.2 to 8.9 million less: 692 million less over the 83 pinned kernel checks (1.07%), and 10.4 million less for the shard pipeline's claim. Tests: tables whose bindings or evidence entries are out of order at the first entries, at the end of the first half and just after it, a table that binds one address to two roles, and one that binds a role past the specification's; each is refused with its reason.
Output of ix codegen for the IxVM kernel after the role table's maps by role are read without rebalancing. No hand edits.
Output of ix codegen --trace-bundle for the IxVM and ix_aggr circuits as they now stand: the host trace writers, their CUDA registries, the CUDA units and the manifest's digests. The multi-stark program is unchanged. No hand edits.
The ixvm suite pins the FFT cost of 83 kernel checks, of the shard pipeline, and now of four claims that validate their role binding and of the binding claim, exactly, so that any cost change is reviewed. The circuit changes since the last re-pin moved every pin; the suite's other checks (execution, outputs, codegen parity, exploits, dependencies) pass on the committed tree. The 83 kernel checks, 78,508,759,033 to 64,279,046,101 in total (-14,229,712,932, -18.1%), each step measured on the branch: - Accept mutual blocks in any member order in IxVM: 83 moved, -14,161,946 (-1,893,614 to -29 each). - Relate typing claims to a specification, binding and axioms: 83 moved, +62,348,399. The longer claim header adds up to 13.9 million a claim; three test fixtures that compiler changes recompiled in the meantime fall by up to 10.3 million. - Read IxVM's primitives through the claim's role binding, admit only Lean's standard axioms, and check role constants once under their groups' contexts: 83 moved, +42,359,014,406 (+51,448,771 to +4,888,516,138 each). Each claim then validated, in its own proof, the role groups it used. - Validate the role binding once per aggregate: these pins now measure claims that assume their binding (validator 4). 83 moved, -55,944,603,195 (-8,130,804,958 to +38,536 each). - The smaller well-founded certificates (a new default table): 65 moved by at most 6,172 either way (-49,524 in total), from the table's bytes; claims that assume their binding validate no certificate. - Read the role table's maps by role without rebalancing: 83 moved, -692,261,072 (-8,904,012 to -8,208,713 each). Against the last re-pin, a claim moves by -3,249,718,279 to +58,997,549; the small claims rise, by the table load on the fixed per-proof floor. New pins: - four claims that validate their binding (validator 3), one per cost class: nat_succ_lit 175,418,320, nat_mul_lit 251,906,554, nat_div_lit 1,774,702,424, nat_land_lit 5,509,726,719; - the binding claim for the default table: 7,616,726,220. The shard pipeline (a claim that validates its binding), 6,229,188,031 to 9,283,737,916 (+3,054,549,885): any member order -2,999,248; the claim header +1,096,326; role dispatch +3,664,884,512; the validator in the owned-check key +2,168,098; the smaller certificates -600,244,440; the maps without rebalancing -10,355,363. The verifying keys change with the circuits; none is pinned in the repository. On this tree the IxVM key is 832,555 bytes with BLAKE3 e4bf74d547809e4163b55d386828349f18f5419e5f22104f235fe31df865cecc, and ix_aggr's 230,771 bytes with BLAKE3 05635577cf42db54a317f6120a361ba43863f4d477ab4a7bca0e1648e3612f3b. The values are measured with this series' circuits and written in place of each moved pin; the suite passes on the committed tree.
Key every published name in the closure's reading context as its quotient key renamed, from the compile's authenticity and the stored records' canonical decoding (ClosureKeying). Build a block's compile-side reading context from the closure's: the closure's records where the block reads references, stored records of the order and their blocks, an axiom record elsewhere, so that every address the compile binds is keyed and the closure reads the block's references alike (BlockContext). With it, discharge the context premises of the singleton readings: a compiled definition, axiom or quotient constant reads in the closure's context as quotient Source's unit renamed (SingletonReads). The fold's facts stay premises: every address the compile binds holds a stored record that resolves in the artifact (BoundResolve), the blobs the compile reads are stored with their bytes, and a name the compile binds for the block is published at its binding.
Layout.extra's ground disjunct: from a record of a group's name, the record of a role a Nat operation's install guard reads is a record of a name of a group. Under the default table the operation's record is a standalone definition (RoleRecordKinds, the meaning of a compile-report check), so it owns no projection and is no block record: the edge starts at a group name's own published record. That name has the operation's key, quotient Source declares the key by a definition (OpsDeclared, a premise here), and the definition's install guard found every ground role installed. The fold installs only names its stream declares besides the prelude's roles, the stream declares a role key only for a closure name with that key, and that name is published at the role's address. Supporting facts: a block with a projection row is a block record, a name published at a role's address has the role's key, a scheduled group's lowering declares only keys over its names' keys (generated names included), and every read a trace keeps comes from a lowering.
A definition, axiom or quotient constant lowers to one declaration, which quotient Source's collapse keeps or drops. A kept read's segment is the constant's compiled record, read from every related state as the lowering renamed; a dropped read is inert with an empty segment. Prove the collapse of one declaration, the segment reading for both cases, and the three singleton kinds' segments from the closure readings. Where the segment lies (the record alone for a kept read, nothing for a dropped one) stays a premise of the segment theorems.
Bring in the closure's reading context for compiled singletons: how the closure context keys a published name, the block's reading context built through the store, and the segment readings of compiled definitions, axioms and quotients. Proofs only, four new modules; disjoint from the recursor-edge proof and the IxVM re-pin merged since.
Steps now records that no key a read keeps is declared by an earlier read (the collapse state owns every earlier read's keys, and a kept key is fresh there). The closure order's cut also exports that the lowered items are schedule items, and unitsRead_of_layout passes the order and the empty segments of dropped reads to the segment readings. With these, a kept singleton's segment is its record alone: an earlier name at the record's address has the singleton's quotient key, which no earlier read declares, and an earlier name whose record projects from the record would not resolve. The latter is the named premise PublishedResolve: a published closure name's record resolves in the artifact's store.
A closure name published at a standalone definition record of kind defn is an input definition: the record is the claim's block itself (a definition record owns no projection), a lone constant's compile makes such a block only of a definition, and a mutual block makes one only of a single class whose member the block's members' loop made of an input definition. This is the compile half of the stream's role declarations being definitions. Also show that a published name whose record is no axiom record does not have sorryAx's key, from the role's record kind; a member of a block of several definitions is published at its definition projection.
definition_block_reads now takes any names with external, as the singleton readings do: names holds at each member's own name and key, and implies quotient Source's names on each member's mentions. The emission reading runs at those names, and the member lowering converts its relations to quotient Source's through related_mono. lower_defs also states that a definition group's read is plain.
Bring in the ground edges of the closure layout under the role record kinds premise, the compile half of the operations-declared-by-definitions fact, and the lemma that a non-axiom record carries no sorryAx key. Proofs only; disjoint from the singleton readings merged since.
OpsDeclared from the role's record kind and the closure names' claims. Every closure name with a Nat operation's key sits at the role's address, whose record is a standalone definition of kind defn, so it is an input definition. Quotient Source's stream then declares the key by a definition: a prelude declaration names only prelude roles; a group's names are stored constants of the group's kind, so an inductive, axiom or quotient group has no definition with the key; and a definitions group converts and lowers each member at its own kind. With it the ground edges of the closure layout follow from the compile's claims of the closure's names (ClaimedIn) and the role records' kinds.
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.
tbd