Repository navigation
Certify Formal Aiur & Retire Legacy Aiur/IxVM - #678
Open
johnchandlerburnham wants to merge 1519 commits into
Open
johnchandlerburnham wants to merge 1519 commits into
johnchandlerburnham wants to merge 1519 commits into
Conversation
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.
Give the flat compilation fold a distinct literal-coverage theorem name, preserving the existing source-collection theorem. Remove two singleton-list simp arguments that the direct member context no longer needs. Preserve the full failed run and its unchanged axiom guards.
Document the current canonicalization, literal, source-admission and reader arguments directly. Remove donor-stage references without changing declarations. Extend the source terminology lint to root source and documentation files; all 1948 files and CLI rejection/acceptance controls pass.
Case on the actual member list so the returned rows and metadata stay specialized together. Supply the explicit member binder in the source-order membership corollary. Preserve the unchanged axiom guards that detected the failed proof.
Open Ix in the ordered Lean/Rust primitive-table test after moving the address-only data. Extend the terminology scanner with a regression control for opens of the retired namespace, while allowing the existing negative namespace-audit fixtures.
Render exact role types, universe counts, typed equation sides and theorem statements directly from the Lean specifications and shared telescope helpers. Admit definitions only after checking their actual kind, safety, type, equations, proof bodies and complete carried proof support under earlier admitted roles. Preserve the original specialized validators and Nat certificate locality restrictions. Derive extra primitive identities only from admitted roles; leave unsupported extra reduction groups disabled. Regenerate the wire-shape fixture from 59 to 103 roles, attributing all 44 added rows to the extra definitions and support anchors and recording each allowed evidence kind. Check every generated group and dependency while preserving the original validator coverage. Cover definition, proof, universe, kind, safety and unchecked-helper mutants, verified external helpers, and refusal of axioms through new anchors. Canonical generation checks, formatting and strict lint pass; all 927 kernel release tests and doctests pass with 8 unchanged ignores. Actual all-role artifact validation and native shortcut activation remain separate follow-up work.
Keep the logical wave driver and replace only its task construction through an exact equality theorem. Project snapshots before Task.spawn so workers capture source lookups, primary addresses, ambient blobs and sharing limits without the driver output registries. Prove the complete compiler read frame, including every failed outcome and retained local state, and lift it through block compilation and unchanged ordered task chunks. Preserve the schedule audit source safety and no-implemented-by checks while requiring the exact reviewed csimp source, target and theorem. Add the block read-frame and task equality roots (13 to 15); replace the original constructor in the no-substitution group with its projected target and projection (5 to 6), and check the original constructor separately. Guard the whole frame module and both boundary theorems at the standard axioms. CompileCorrect and the runtime closure audit remain unchanged. Add native controls against direct full-snapshot outcomes for empty and uneven chunks, fallback source lookup, mixed first refusals, ambient blob conflicts, required address resolution and nondefault sharing limits. Strict ix/IxTests builds and the worker-snapshot, local-blob, header-count, source-contract and record-decoding suites pass. This change is not yet a measured performance result.
The flat row-name induction no longer uses flatten-cons, flatMap-append or map-flatMap. Remove those three unused arguments so the already checked final compiler theorem passes the strict warning gate.
Use the mathematical purpose in the remaining component-proof headings and retain the runtime audit count explanation without its milestone label.
Open _root_.Ix explicitly inside Tests.Ix.Kernel.PrimitiveTable so the shared address table is found without an ambiguous-open warning. The preceding full gate passed every strict compiler proof and audit; this test namespace ambiguity was its only build failure. Further cloud validation is held for coordinated performance measurements.
Authenticate a retained Lean-generated artifact, require admission of every role, and check every carried unit with the production checker stack. Accept the artifact path through IX_ROLE_ARTIFACT so the generator gate can test its exact output without maintaining another binary fixture. The explicit integration test is excluded from ordinary runs that have no generator output. The release harness and strict lint pass. The generated all-role artifact admits all 103 roles and checks all 5441 units; its independently measured hash matches the generator record. Extra native shortcuts remain disabled.
Adapt the exact worker read frame to the single expression compiler and flat mutual-member fold. Remove the obsolete class-tail frame helpers and preserve the loader universe-budget postcheck by rewriting the equal compiled result beneath it. Resolve the schedule audit with all extracted parallel-map roots, both worker equality roots, the exact checked replacement and the renamed InitStd parity suite. Retain singleton metadata groups while using journalled Rust block registration, preserving atomic failure rollback. Require both decoder and worker-snapshot controls in the primary test registry.
Generate and check the Rust validator terms and shared evidence-shape fixture alongside the IxVM role specifications. Both consumers read the canonical Lean specifications instead of separate handwritten schemas.
Derive optional String and BitVec reduction permissions from semantic admission, and check each referenced head independently. Restrict bound BitVec reductions to ofNat operands whose widths match the supplied width by definitional equality; do not apply the arbitrary-value fallback beyond the generated specification. Add an artifact-backed constructed-result gate covering String literal operations, typed Decidable results, constructor collapse, BitVec literals, definitional width equality, unsupported inputs, and candidate heads excluded from admission. Keep decision-procedure proof shortcuts and Nat offset/linear-recursion shortcuts disabled. Cloud validation is pending the coordinated performance window.
Build an alternate Int.negSucc anchor through a helper whose erased argument is ill typed, alongside a correctly typed control with the same reduction. The anchor appears only on the generated equation right-hand side and is absent from the operation closure. Require both the anchor and its dependent equation role to refuse the invalid helper. The regression is preserved before the support-validation fix. Its red run is pending the coordinated cloud hold.
Strip an optional _root_. prefix before checking an opened namespace. Add rejection controls for retired root-qualified opens and acceptance controls for current root namespaces. The scanner controls, explicit CLI cases and all 1948 source files pass locally without a grandfather baseline.
Generate the 103-role table with 41 proof records and a checked closure of 4,250 records. The added equation roles retain ordinary checked theorem support; the original 18 Source evidence records remain unchanged in scope. Keep the fifteen Nat evidence-kind controls separately, and extend reader controls to the twenty-nine definition-equation rows and mixed evidence.
Check the complete carried support of new anchors and every constant or projection referenced by generated types, equation statements and definitional sides. Require each external generated reference to belong to a completely admitted group; same-group candidates remain available without native permission. Preserve specialized validators and existing Nat certificate behavior. Validate generated anchor/equation dependencies against their declared groups in the shared Lean renderer. Add runtime partial-group controls and independent generator omission/projection mutants. A static audit of the existing generated specifications finds no missing dependency groups; generation is expected to remain byte-identical. Cloud execution of the regression and fix remains pending the coordinated hold.
…join it on every path finalize started a certificate compile before it knew its roles, and dropped it unjoined when supportInput threw, when the roles needed other certificates, or when anything after it threw. A compile left running when main returns waits for subtasks the runtime's shutdown no longer runs, and the process hangs at exit. finalize now starts at most one compile of its own, after supportInput, and joins it in a finally; a prefetched compile is still used when its theorems match and stays its caller's to join. checkFinalized waits for every one of its check tasks before it reports the first failure, in the same order and with the same messages: a check left running could start its parMap after the workers have exited.
drain left the final batch of published candidates, fewer than a release batch, in the controller's state, to be freed with it on the calling thread. It now releases them as the other batches are.
A compile of the default scope (or of an empty --module list, the full environment) publishes every role, so, as compile-lean without --local, it starts every role's certificate compile beside the source compile. --local, --consts, --module and --exclude compiles do not.
loadEnv pinned its setup for the life of the process on every call, and kernel-check-ixe then marked it a second time. loadEnv (and load) now take persistent (default false); kernel-check-ixe sets it when its loop runs on its own thread, as it marks the eager path's setup, and then marks only the report names.
runMode noted a user axiom when its record was read, before the record's verdict, so a selected run listed axioms whose records were then blocked, declined or rejected. The report now keeps the user axioms whose records the run accepted (admittedUserAxioms), as kernel-check-ixe lists them. A whole run's conditional verdict still uses the kernel's list (receipt.axioms). The user-axiom checks gain a rejected user axiom, selected beside one that is accepted: only the accepted one is listed.
A results row said ok whenever no subject failed, also for a partial run (exit 4) and a conditional one (exit 5). The status now names the exit (runStatus): ok, rejected, partial or conditional. bench bmf already drops every row that is not ok, so neither becomes a bencher data point; the gate still fails only on rejected or missing rows. The row contract (Ix.Benchmark.Results, docs/benchmarking.md) and the check-lean docs list the new statuses, and the CLI and user-axiom tests check them.
With chunk 0 every read returned no bytes, so the loop ended at once with the empty input's digest.
…tement could be issued
Brings in #675 (426a242) with the formal Aiur bridge from jcb/certified-compression (d9ac196): crates/proof-compression and the compression FFI and CLI run on aiur::trace::stark and MultiStark::ix_aggr shape 1, and multi-stark is pinned to main (3515632), which the compression Plonkish backend needs. The Lean certification of compression (Ix/Cert/Compression, its module audit guards and docs/certified-compression.md) stays on jcb/certified-compression. d9ac196 is not an ancestor, so merging this branch there keeps it.
#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.
check-formal.sh's generators read the pinned Ix revisions with `git show`, which a depth-1 CI checkout lacks; fetch just those commits when missing. Apply rustfmt to the merged compression and trace code.
Formal Aiur's mathlib requirement adds mathlib, ProofWidgets, LeanSearchClient, importGraph, aesop and Qq to the workspace. lean4-nix builds every manifest package as a library, which compiles all of Mathlib plus its shared library and fails on ProofWidgets by guessing a `Proofwidgets` target. Nothing the flake builds imports them, so give them a no-op build: Lake needs only their sources to resolve the workspace. The ix-tests check marks the unbuilt mathlib present. Otherwise `ix validate-lean`'s source build sees mathlib in the manifest and runs `lake exe cache get` (`Ix.fetchMathlibCache`), which the sandbox cannot.
…tests needs no ix binary
…degen Unify RoleSpecGen's Formal Aiur renderer with its RVal DAG CSE so renderFormalAiur emits IxVM/IxVM/Modules/KernelRoleSpec.aiur byte-for-byte from Ix.Kernel.Role.spec without LegacyIxVM or adapt.py, and remove the dead legacy RoleSpec.lean renderer. Wire KernelRoleSpec.aiur into ix codegen (--check) and guard check-formal.sh against GC'd pre-migration branch commits.
….Audit library coverage
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.
Overview
This PR is the third step in the certification sequence following #665 (
jcb/ix-certified-v3) and #677 (jcb/ix-certified-v3-followup). It merges the formalized Aiur compiler and runtime frommigration/formal-aiur(34619c5c1) onto #677 (05cc396fc), and accomplishes two goals:LegacyAiur,LegacyIxVM, andLegacyMultiStarkcompletely, migrating allIxVM,MultiStark, and CLI proving/aggregation workflows to the verified Formal Aiur pipeline and porting all role-binding and aggregation protocol changes from certified kernel and certified compilation #665 / Jcb/ix-certified-v3 followup: Formalize nominal-to-quotient Source bridge, optimize compiler/kernel, and retire uncertified Rust/Lean pipelines #677 into.aiurmodules.Aiur/) from grouped/activated STARK traces back to source.aiurevaluation,U64andBlake3Goldilocks libraries, heap monotonicity, andIxVMheap representation predicates—with zerosorrys, zero custom axioms, and zerobv_decide(Lean.ofReduceBool/Lean.trustCompiler) dependencies.1. Formal
.aiurPort & Complete Retirement of Legacy StackLegacy Removals
LegacyAiur/,LegacyIxVM/,LegacyMultiStark/,crates/aiur-legacy/,crates/ixvm-legacy/, andcrates/ixvm-legacy-native/(while preserving Jcb/ix-certified-v3 followup: Formalize nominal-to-quotient Source bridge, optimize compiler/kernel, and retire uncertified Rust/Lean pipelines #677's removal ofcrates/compile,crates/kernel,Ix/Tc, andIx/AuxGen).Ix/Aiur/Protocol.lean,Ix/IxVM/ClaimHarness.lean,Ix/Aggr/Statement.lean) so CLI and test harnesses build witnesses and public statements without any dependency on legacy circuits.Ix/Cli/FormalAiur.lean,Ix/Cli/FormalAggregate.lean,Ix/Cli/ProveBindingCmd.lean,Ix/Cli/CatalogAggregate.lean,Ix/Cli/ProverCmd.lean,Ix/Cli/AggregateCmd.lean) to Formal Aiur.Role-Binding & Aggregation Protocol in
.aiurKernelRoleSpec.aiur&KernelRoles.aiur:Ix/IxVM/RoleSpecGen.lean(renderFormalAiur) andtools/ixvm/adapt.pyto generate and portIxVM/IxVM/Modules/KernelRoleSpec.aiurandIxVM/IxVM/Modules/KernelRoles.aiur.Addr-keyedRBTreeMap<Field>(canon_addr_cmpforRoleCtx.by_addr) vsField-keyedRoleMap<V>(u32_less_thanforRoleCtx.by_roleandRoleCtx.evidence) under Formal Aiur's typed pointer discipline (Addr = &[U8; 32]).ptr_val) fast-paths fromKernelRoles.aiurandKernelClaim.aiurin favor of semantick_is_def_eq,addr_eq, androle_ctx_limit.KernelSubst::ctx_close_cutto handle open recursor rule comparisons (Acc.rec) when the outer context isLists::Node::Nil.check_ownedKeys:crates/ixvm/src/lib.rsstream preparation filter to[1, 2, 4, 6].contains(&s.channel)so role-binding channel6streams are loaded intoio_buffer.MultiStark/MultiStark/Modules/Aggregate.aiur(ix_aggrshapes13..=16),tools/ixvm/recursion.py, andcrates/ix-prover/src/distributed.rsfor 65-elementcheck_ownedpublic keys ([claim_tag, ctx_8, target_8, value_8]= 25 field elements + 40 VK words) and role-binding claim routing.Aiur/Aiur/Generic/Elaborate.lean):variables.length-iteration substitution loop inElaborate.normalizewith early-stoppingnormalizeAux, and avoided redundantfreshvariable allocations in.store/.tuple/.constructwhenexpectedis already known.lake -d IxVM exe ixvm check/check-claimacross all 823 functions (including the 2,000-lineKernelRoleSpecmodule) from >40 minutes to 8.2 seconds.2. Formal Aiur Certification (
Aiur/)Aiur/Aiur/Optimized/EndToEnd.lean):checkerMemo_acyclic_heap_sound(Aiur/CheckerCorrectness.lean),Modules.Prepared.compile_sound_heap(Aiur/Optimized/Correctness.lean),Physical.Prepared.derives_to_logical(Aiur/Optimized/Physical.lean),Grouping.Plan.derives_sound_plan(Aiur/Optimized/Grouping/Plan.lean), andActivation.activeRule_iff(Aiur/Optimized/Grouping/Snapshot.lean) into:Modules.Prepared.physical_heap_soundModules.Prepared.grouped_heap_soundModules.Prepared.grouped_activated_heap_soundU64&Blake3Correctness:Aiur/Aiur/Library/U64/Goldilocks.lean&Aiur/Aiur/Library/U64/Correctness.lean: provesU64.Compatible Goldilocks.Fand end-to-end specifications foradd_check_iff,sub_sound,mul_check_iff,divmod_check_iff,less_than_iff,xor_check_iff,and_check_iff,or_check_iff,shr_check_iff, androtl_check_iff.Aiur/Aiur/Library/Blake3/Correctness.lean: provesg_round_spec,compress_spec,merkle_node_hash_spec, andverify_bytes_against_iff(linking Goldilocks field equality of 8U32words to exact 32-byte Blake3 digest equality).Aiur/Aiur/Library/U8Facts.lean: replacedbv_decideproofs inxor_and_sumandxor_or_sumwith inductive proofs overNat.bitwise, eliminatingLean.ofReduceBoolandLean.trustCompilerfrom the entireAiurproof tree.IxVMHeap Representations:Aiur/Aiur/HeapMono.lean&Aiur/Aiur/StepLemmas.lean: provesHeap.Extendsreflexivity/transitivity,DerefTypedpreservation, and weakest-precondition (WP/WPEval) combinators for.store,.load,.letBind,.matchEnum,.hint, and.call.Aiur/Aiur/Library/List/Correctness.lean,Aiur/Aiur/Library/Bytes/Correctness.lean,Aiur/Aiur/Library/RBTreeMap/Correctness.lean, andAiur/Aiur/Library/IxVMRep.lean: proves heap representation predicates (RepLinkedList,RepByteStream,RepRBTreePtr,RepIxVMUniv,RepIxVMIExpr,RepIxVMKUniv,RepIxVMKExpr,RepRoleCtx),ingress_verify_stream_sound, andTagNheader decoding uniqueness.Aiur/Aiur/Audit.lean):Aiurusing#guard_msgsto enforce that every theorem depends only on[propext, Classical.choice, Quot.sound].Verification
lake -d Aiur build --wfail&lake -d Aiur build --wfail Aiur.Audit(3,489 jobs, 0 warnings,[propext, Classical.choice, Quot.sound]only)lake -d IxVM build ixvm(3,971 jobs)lake -d IxC build --wfail&kernel-layering/kernel-trust-surface(594 jobs, 0 boundary violations)lake build(443 default jobs)lake run check-modules(4,875 jobs under--wfail, includingIx.Cert.IxVM.CircuitCorrespondenceandIx.Cert.ModuleAudit)lake run check-source-docs(2,217 files checked)lake run check-ixtests-registrycargo test --workspacelake exe IxTests binding-proof-cli(10/10 subtests)bash tools/ixvm/check-formal.sh