Repository navigation
Certify Formal Aiur & Retire Legacy Aiur/IxVM - #678
Open
johnchandlerburnham wants to merge 1597 commits into
Open
johnchandlerburnham wants to merge 1597 commits into
johnchandlerburnham wants to merge 1597 commits into
Conversation
Integrate the reviewed fixture narration and Rust-help corrections. Keep the frozen native baseline as an ancestor; no executable behavior or test assertions change. Native link caches remain at the measured baseline.
Validate Char.ofNat as a dependency when String.back synthesizes its result, including claims that assume their binding. Retain ordinary and assumed consumer controls and the earlier well-founded evidence checks. Strict source/link and fresh interpreter controls pass. Generated backends and exact native parity must be refreshed and gated before publication.
Name the raw streamed and Rust entry points used by the closure, schedule, and publication fixtures, and separate their checks from CLI finalization. Replace obsolete collapse/rewriting history and private queue references with the current source-order, reconstruction, and closure assertions. Preserve every declaration, identifier, log label, and executable assertion. Validation: inspect the actual harness, schedule, FFI, and closure callers; the strict standalone source terminology check passed all 1,965 files, and the reverse patch check passed. The extra scanned file is the already integrated BindingFrontier module. All changes are comments; no dependency build or remote work was run during performance calibration.
Describe --rust-check as a raw Rust handoff followed by shared finalization and Lean serialization on both final envelopes. State that a later mismatch leaves the Lean output already written. Explain that fail-closed compilation failures leave an absent or existing destination untouched and that --allow-partial permits the successfully compiled subset. Validation: traced both compile commands through their failure checks, finalization, serialization, and atomic writes; inspected the retained existing/absent destination controls. The strict standalone source terminology check passed all 1,965 files and the reverse patch check passed. Only comments and CLI help strings changed; no executable assertions, identifiers, diagnostics, behavior, dependency builds, or remote execution changed.
Copy the ordinary Rust executor and IxVM trace/CUDA outputs from the checked producer. Its grouped program matches the reviewed character-validation source, and both producer freshness checks pass. Sixteen producer outputs were copied and SHA256-verified; exactly five IxVM outputs change.
Add a two-byte header check (`recursorRecordHeader`) before decoding `LazyConstant` entries in `storedRecursorRecords`, and prove that `recursorRecordFast` agrees with `recursorRecord` in `Ix.Cert.ProjectionRead`. Migrate `ExprCache` and `occCache` in `Ix.IndFlags` from hash-only `Ix.Expr` keys to `ExactKey.ExprKey`, reject colliding `Ix.Name` hashes when merging support publications in `Ix.RoleBinding.Compile`, and parallelize the artifact checks in `checkFinalized`.
Extend `checkFinalized` with the remaining artifact-level checks from `checkReport` (`unreadablePublished`, `unresolvedPublished`, `unhintedDefinition`, `unownedRecursor`, `literalRoleUnnamed`) and `roleBindingError` (`PublishedAgree`, canonical role-binding admission, `PublishedRolesBound`, and bound role record kinds). Check input cardinality after `canonInput` and verify `sourceAddresses` and `unboundPublishedRole` in `compileCertifiedPrepared`. In `finalize`, when `artifact` already publishes every constant in `selected.constants`, slice the role-support sub-environment directly from `artifact` (`sliceSupport?`) instead of re-compiling `selected` from source.
…zation Add `Ix.Sharing.ParallelTable`, `Ix.Sharing.ParallelChoices`, and `Ix.Sharing.FamilyParallel` with proved associative table merging, bounded task-frontier subset search (`depth <= 3`), and sort-free leaf enumeration (`foldChoicesRev` / `foldChoicesFast`) when component members are pairwise sorted. Register `@[csimp] theorem table_eq_function` and `@[csimp] theorem trace_eq_parallel` in `Ix.Sharing.FamilyContext` and audit the new theorem roots in `IxSharingVerify.Audit.Statements`. Pre-size section and envelope `ByteArray` buffers (`runPutWithCapacity`) and overlap section sorting and serialization tasks in `Ixon.putSections` and `Ixon.serEnv`.
Make `+`, `-`, and `*` left-associative in `Ix.Aiur.Meta` (`syntax:50 aiur_trm:50 " + " aiur_trm:51`, `syntax:50 aiur_trm:50 " - " aiur_trm:51`, `syntax:60 aiur_trm:60 " * " aiur_trm:61`) and add elaboration-time parse checks. Extend `reducedAritySource?` in `IxC.Kernel.Audit.Runtime` to recursively strip stacked compiler suffixes (`_redArg`, `_boxed`, `_impl`, `_spec_<n>`) back to source declarations, and audit `Ix.CompileM.compileCertified` and `Ix.RoleBinding.Compile.finalize` in `Ix.Cert.RuntimeAudit`.
Validate interior section-5 metadata windows at load time in `ixon` (`validate_window` / `LazyMetaWindow::new_validated`) and replace panicking unwrap calls in `LazyMetaWindow` with checked fallible helpers (`split_checked`, `decode_meta_checked`, `decode_original_checked`). Reuse caller-owned stamp/epoch and stack buffers in `component_area` (`component_area_with` / `component_area_pos`) across exact sharing components in `ixon::sharing_exact::uniform`. Include `Role::StringOfList` in `ExtraReductions::from_admitted`, check both operation and evidence references in `validate_wf_op`, and add unit tests across `ixon` and `ix-kernel`.
Add `unauthenticPar` (`parMap` over stored records and blobs) and prove `unauthenticPar_eq : unauthenticPar ixe = unauthentic ixe` for `@[csimp] theorem checkReport_eq_par`. Spawn `storedRecursorRecords` once in `checkReportPar` and share it between `unownedRecursorWith` and `recursorShapeErrorWith`. Overlap `GraphM.envSerial` and `FrontEnd.immediate` in `groundSplitLazy`.
Add `authenticateParallel` (`Parallel.map`) and `authenticateParallel_eq` in `Ix.RoleBinding.RecordDecoding` and wire it into `recordStoreParallel` (`@[csimp] theorem recordStore_eq_parallel`). Add `ensureModuleSearchPath` in `Ix.Meta` and cache `nativeCertSource` (`loadExts := false`) in `Ix.RoleBinding.Compile` so certificate loading avoids spawning `lake env printenv LEAN_PATH` when `.olean` artifacts are already on the search path or in `.lake/`. In `finalize`, overlap certificate compilation (`IO.asTask`) with `checkedStore` and `sliceSupport?`, share `storedRecursorRecords` and use `unauthenticPar` in `FinalizedCheckTasks.spawn`, and offload `CheckedStore` reference-count teardown after `Generated.emit`.
Port the proved dependency-ready block execution modules (TaskWindow, WorkerSuccess, WorkerReplay, ReadyPublication, ReadyQueue, ReadyCompile) and benchmark harnesses (ReadyExecutor, ReadyBenchmark). Ensure linear ownership across ReadyQueue state maps and inner waiter arrays before mutation, add pointer-equality fast paths to WaveBlocks decidable equality in ReadyPublication, and route compileCertifiedPrepared through ReadyCompile.reportIO with an 8192-block lookahead window while preserving its exact equality certificate to Ix.Cert.compileReport.
Ensure sliceSupport? traverses Ixon.CheckOrder.owner for projection records and retains sibling projections of visited mutual and inductive blocks so role publication and reducibility-hint lookup resolve without falling back to support recompilation.
Export Ix.CompileCertified from the Ix library root, migrate the remaining Name hash sets in Ix.IndFlags to ExactKey.NameKey, include parent workspace build paths in ensureModuleSearchPath, and extend RuntimeAudit and ModuleAudit to cover CanonM.canonEnv, Ixon.serEnv, and the Ix.Compile.ReadyCompile scheduler modules.
Spawn parallel tasks for the independent output-map folds in assembleEnvPar (proved equal to assembleEnv via @[csimp]) and parallelize the remaining list-backed findSome? and filterMap checks in checkReportPar via parFindSome? and projectionCollisionPar.
Slice support directly from lazy record references without decoding the entire artifact into a CheckedStore when support is already covered, fast-path standalone constant headers in unresolvedPublished and unownedRecursorWith, and parallelize named role and source-address scans.
The specification digest moves to 84d3999ef8f830d2d0678f21d81730d2aee6f9a2cfd04c84d593b38f52eb7fae (19427 bytes; was 6d02153e..., 17727). The schedule it commits to is unchanged: 72 groups, the well-founded block from group 33, the equation groups from 41. - `IxVM/IxVM/Modules/KernelRoleSpec.lean`: `ix codegen`. Only the `spec_digest` literal changes; every rendered table is as before. `spec-shape.tsv` is unchanged. - `Tests/Fixtures/ixon-v4/claims.tsv`: `ixon-v4-tests --export-fixtures`. The seven rows whose context names the digest change, with their addresses. - `crates/ixon/src/proof.rs` (`SPEC_DIGEST_HEX`) and `Ix.SpecDigest.Audit`: re-pinned from the computed value. - `Ix.HostAdmission.Audit`: the host closure, which computes the digest, grows 7173 -> 7725 compiled functions. Externs, implemented_by, unsafe, csimp and every ruling are unchanged. The IxVM fixture `nat-add-comm.ixf` holds the default role table, not the digest, so it does not move.
`specBytes` checks the schedule at run time, so `checkOrder` is in the host-admission closure. Spelling a role by `Role.leanName`, which is `@[inline]`, copied its 103-arm table and closed terms into the order loop: 189 compiled functions, beside the copy `roleName` needs to encode the names. The errors now give the role's index.
Measured on the box (spec-5) after the schedule's errors stopped spelling role names. Against the base, by module: `Ix.SpecDigest` grows 47 -> 289 (the role names with `Role.leanName`'s table inlined, 187; `nativeOp`, 42; the new rows, 13) and `Ix.SpecDigest.Schedule` adds 127 (`groupOrder`'s closed terms, 73; the checks, 54). The extern, implemented_by, unsafe and csimp counts and every ruling are unchanged.
The module layout's compatibility notes now cover the library: the converted modules and test clients equal their string-parsed programs, and the library example exports are byte-identical.
A get on an IO.Ref shared between threads writes back the value it read over a concurrent set, so the polling task could miss the sibling's signal and hang formal-aggregate-tests before its first case.
The rendered circuit specification and the digest that IxVM holds beside it were produced from the same Lean data, but nothing checked that the file is a function of the bytes the digest hashes. The renderer now reads only those bytes. - `Ix.SpecDigest` encodes a `Committed` record (versions, one `Row` per role, schedule); `specBytes` is `encode Committed.current`, byte for byte the encoding before. - `Ix/SpecDigest/Decode.lean` reads the bytes back. It refuses bad tags, contract bits, role indices and counts, and `Committed.ofBytes` accepts bytes only when what it reads re-encodes to them. - `IxVM.RoleSpecGen` renders from that `Source` (`renderFromBytes`). Roles are indices into its rows; the circuit's named roles and the `Nat` and `Eq` of the closing terms are looked up by the names the bytes give. `renderFormalAiur` checks IxC's specification set and schedule, then renders `specBytes`. `checkRendering` compares a file with the rendering and names the first differing line. The gate is `ix codegen --check`, which `tools/ixvm/check-formal.sh` runs on every PR; it now compares the file with the rendering of the bytes, and prints the first difference. The primary test `spec-digest-rendering` accepts the checked-in file and refuses five mutations: Nat.add's native rule renumbered, the first two groups swapped, the last byte (the first equation group) decremented, a byte appended, and the file's first_equation_group edited. Docs: `docs/kernel.md`, `docs/host-admission.md` (whose frozen-value sentence was stale) and `docs/formal-aiur-modules.md`.
A byte mutation is refused through the digest literal alone, which a renderer that ignored everything but the hash would also produce. The suite now also renders the mutated bytes and requires a difference outside the `spec_digest` line, and prints the first one.
Measured on the box (spec-8) by diffing the closures by name against the wave-2 base (7173): `Ix.SpecDigest` grows 47 -> 291 (the role names with `Role.leanName`'s table inlined into `Row.ofRole`, 186; `nativeOp`, 42; the record's rows, schedule and encoder, 26; less 10 of the old `specBytes`'s own) and `Ix.SpecDigest.Schedule` adds 127. The decoder is not reached. Externs, implemented_by, unsafe, csimp and every ruling are unchanged.
The fixed root layout that `ix compress layout` writes, that
`--fixed-root` and `ix compress normalize` read and that the release
bundles was pretty-printed JSON, parsed with serde. It is now an Ixon
file (`.ixl`), written with `aiur::ixon`'s primitives like the Aiur
artifacts:
layout = "IXROOTL\0" nat(1) list(nat(log_height))
list(nat(memory_width) nat(circuit)) nat(claim_len)
Decoding refuses another magic or version, out-of-range values and
trailing bytes, so an accepted file re-encodes to itself and its BLAKE3
digest is its identity. The fixed verifier's identity hashes that digest
(`ix/fixed-root/v2`) instead of the JSON text. The FFI and the
`ix compress` commands pass layouts as bytes, and a normalized root
directory carries `fixed-root.ixl`.
The release becomes version 0.2. Its layout,
`verifying-keys/0.2/root-layout.ixl`, is the formal aggregation
backend's (Nat.add_comm's roots under every root shape, with one
doubling of headroom), pinned by `LAYOUT_BLAKE3`. The keys moved beside
it are still 0.1's, derived for the legacy aggregator; the following
commits regenerate them, and until then the release refuses the formal
aggregation key.
The backend theorems assume plan.WellFormedActivation, but the exporter checked only that each chip is well-formed after activation. It now decides the theorems' own predicate on every exported plan.
The empty input, one byte, one block, both sides of the chunk boundary, and trees of two, three, four and nine chunks (BLAKE3 1.5.4 test_vectors.json).
Six audited statements assume (Classical.choice ⋯).Acyclic, and the elided proof is what names the memo graph that must be acyclic, so the frozen text did not pin it. They are now printed with pp.proofs true and name Circuit.System.checkMemo_sound of the statement's own check.
# Conflicts: # docs/benchmarking.md
A release is fixed by its trusted inputs alone: the IxVM and aggregation keys, the root layout and the Ignition SRS. `derive_release` builds the first stage's FRI verifier and the recursive frontend as `prepare` does, publishes both stages' fixed preprocessing to the cache, and returns the recursive key with `FIRST_PLAN_ID`, `RECURSIVE_FRONTEND_ID` and `RECURSIVE_VK_ID`. `final_schema` gives the verifier description both final circuits prove (`FINAL_SCHEMA_SHA256`), and `statement::backend_prefix` the ten words every statement of an aggregation backend begins with, as `Aiur.buildClaim` and `Aggr.pubInput` lay them out over `Aggr.allowedBlob`. `examples/release_keys.rs` runs them from the `ixvm-proof key` and `stark-verifier key` directories and a `.ixl` layout, writes the release files and prints every pin of `verifying_keys.rs`. With `--finals` it starts from an existing recursive key and derives only the PLONK key and the Groth16 development key, which need the `plonk` and `groth16` features (and Go). Its cache root is the one `ix compress` reads, with the setup and caches `CompressConfig::from_env` gives, so a later compression reuses what it published.
Without `--fixed-root`, `ix compress` compresses under the bundled keys, which verify only statements that begin with the release's prefix. A statement of another IxVM or aggregation backend was refused only after the root had been normalized and every stage proved, when the recursive stage compared its statement with the release. `pipeline::check_release_statement` (FFI `rs_compression_check_release_statement`, Lean `Compression.checkReleaseStatement`) binds the statement to its claim and compares its first ten words with `STATEMENT_PREFIX`. `ix compress` calls it beside `releaseRootLayout`, before any proving.
The release pinned the retired legacy aggregator: `ROOT_VK_BLAKE3` named its key, and `STATEMENT_PREFIX` began with its call channel 0 and function index 293, so `ix compress` without `--fixed-root` refused the formal aggregation key and compressed `ix verify` accepted only legacy statements (review item B2). The pins now follow from the formal backends under the restored STARK parameters (log_blowup 2, 100 queries, 20 query PoW bits): - `ROOT_VK_BLAKE3`: the BLAKE3 of the aggregation key (`stark-verifier key` of `stark-export export-trace --aggregate`). - `STATEMENT_PREFIX`: `backend_prefix` of that key and the IxVM key (4c4b908c...), with call channel 1 and `ix_aggr` at index 0. - `recursive-vk.bin` with `RECURSIVE_VK_BLAKE3`, `RECURSIVE_VK_ID`, `FIRST_PLAN_ID` and `RECURSIVE_FRONTEND_ID`: `derive_release` of that key and the bundled layout under Ignition (`release_keys`, box job params-b2-3, 1256 s and 99 GB peak RSS). The unit test now also requires the prefix to name call channel 1.
The final keys prove the recursive verifier description, which commits to the recursive key and the statement prefix, so both changed with the previous commit. `release_keys --finals` derived them from the bundled recursive key under Ignition (box job params-b2-4, 492 s and 15 GB peak RSS): the PLONK key with `PLONK_VK_SHA256`, a fresh Groth16 development key with `GROTH16_VK_SHA256` and `GROTH16_CIRCUIT_SHA256`, and `FINAL_SCHEMA_SHA256`. The same job compressed Nat.add_comm's root in PLONK and in Groth16 under them, and `ix verify` accepted both. `contracts/plonk` follows the PLONK key: `src/PlonkVerifier.sol` is gnark's export of it (only the key's commitments change), and the test pins its SHA-256. The test proof `testdata/init.json` was already under another key than the one the test pinned; it is replaced by `testdata/nat-add-comm.json`, the PLONK proof of that same run.
`Tests/CompressionCli.lean` only checked rejections, so nothing noticed that the release pinned the legacy aggregator. `compression-cli` now also requires, against the checkout's IxVM and aggregation artifacts: - a release layout (`.ixl`) for the formal aggregation key, and the release's statement prefix on a formal statement: what `ix compress` without `--fixed-root` checks before proving. Another IxVM backend's statement is refused. - `ix verify` to accept a recursive KZG proof of `Nat.add_comm`'s aggregate root under the bundled keys, and to refuse the same proof under another claim. The proof, `Tests/Fixtures/Compression/nat-add-comm.ixon-proof`, is what `ix compress` made of the wrapped-leaf root when the 0.2 keys were derived (box job params-b2-4, 2,326 s and 389 GB peak RSS); its `PROVENANCE.md` records the inputs.
The proof-compression README cited the 0.1 keys and their JSON layout. It now describes release 0.2: the formal backends it belongs to, its layout (139 circuit heights, 11 of them memory circuits, 18 claim words, one doubling of headroom over Nat.add_comm's four root shapes), the `.ixl` grammar, and the complete derivation: exporting the artifacts and keys, proving the four roots, `ix compress layout`, the Ignition SRS, `release_keys` for the recursive key and the final keys, with their measured cost, and what to replace when a release changes. `docs/stark-parameters.md` points there from its parameter-change checklist.
They prove hand-written Lean models of the library functions against Lean specifications; no theorem evaluates the library's Aiur source. Also say that the memo-check theorems cover the compiled typed circuits, not the grouped, activated ones, and name the elaborators that replaced the .aiur parser.
The PR's lean-test filled its 50 GB sticky disk (48.9/48.9 GB on run 42366575382, failing "Check formal Aiur proofs"); the next run found it critically full and reset every cache. A full build now keeps about 33 GB there, Mathlib's checkout and oleans alone 7.5 GB, and stale build products accumulate on top. Match nix.yml's 100 GB. RunsOn snapshots are keyed by lineage name, not size, and its docs do not say whether a larger disk restored from a 50 GB snapshot grows its filesystem, so the name changes with the size and the job starts a new lineage. The PR's own lineage was just reset, so it loses nothing; main repopulates the new lineage on its first push run.
lean-action v1.6.0 runs `lake exe cache get` whenever use-mathlib-cache is "auto" (the default) and the root lake-manifest.json names mathlib4, independently of auto-config. #678 put Mathlib in the root manifest through Aiur, so rust-test and cuda-compile now clone every Lake dependency and download Mathlib's oleans (about 7.5 GB with the checkout) that they never use: rust-test only needs the toolchain for bindgen, and cuda-compile builds `ix`, whose imports (Main, Ix, Aiur.Ixon) do not reach Mathlib. In rust-test that lands on its sticky disk; in cuda-compile it rides through the actions/cache save. Set use-mathlib-cache: false there, and true in lean-test, whose Aiur proofs import Mathlib, so the dependency no longer rests on detection.
90fe85d opted aiur into the workspace lints and fixed what the default features reported, but the `cuda` feature compiles more: the device plan encoding in trace/plan.rs, stark/gpu.rs and its tests. cuda-compile checks those with warnings denied (CARGO_BUILD_WARNINGS=deny from setup-rust-toolchain) and failed on 18 lib and 2 test warnings: - unreachable_pub: the items of the private `plan::device` module become pub(crate); - unused_qualifications: `size_of`/`size_of_val` are in the prelude, and the GPU tests already glob-import `gpu` from their parent.
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.
Formal Aiur: a verified Aiur compiler, with IxVM and MultiStark on it
Summary
This PR replaces the Aiur backend with formal Aiur: an Aiur compiler and execution model written and proved in Lean (
Aiur/). The IxVM kernel checker and the MultiStark recursion and aggregation programs are rewritten on it. It is based on main after #677 (3d725c8c0) and #685 (bdd4304fa).docs/formal-aiur-migration.mdcovers the package layout and the migration.[propext, Classical.choice, Quot.sound].IxC. That refinement is follow-up work.aiur⟦ … ⟧). The Aiur library usesaiur_library% ⟦ … ⟧.0.2.What is proved (
Aiur/)Aiur/Aiur/Optimized/EndToEnd.lean):Physical.Prepared.native_heap_soundlifts to grouped and activated circuits throughGrouping.Plan.derives_sound,Grouping.Plan.activatedDerives_soundandActivation.activeRule_iff.Modules.Prepared.grouped_activated_heap_sound(also stated asOptimized.ModulesArtifact.grouped_activated_heap_sound).plan.ActivatedDerives;rom.Valid;Circuit.Erasure.Signed;plan.WellFormedActivation, which the exporter decides for every exported trace plan (Trace.exportPreparedPlan).checkerMemo_acyclic_heap_sound/checkMemo_acyclic_soundfamily starts from what a verifier can check: the memo derivation thatcheckMemo_soundextracts from balanced lookups.pp.proofs true), so they name the exact graph that must be acyclic.Correctnessmodules prove hand-written Lean models of the library functions, and their byte and limb arithmetic, against Lean specifications. For example:add_sound,sub_with_borrow_sound,mul_sound,and_sound,or_sound,xor_sound,eq_sound.g_spec,round_spec,compress_spec,compress_layer_step_spec,digest_bytes_spec,verify_bytes_against_iff, againstBlake3.digest.IxVMRep, lists, byte streams, red-black trees.Aiur/AiurTests/Blake3Vectors.lean).Aiur/Aiur/Audit.leanfreezes the statement and axioms of 325 theorems.--wfail, so asorryfails it.axiom_sweepchecks every declaration in theAiurmodules for custom axioms andofReduceBool.Trust boundary
Assumed, not proved:
loop(0) = 42row balancesfn loop(x) { loop(x) }.aiur⟦ … ⟧andaiur_library%elaborators, and the Ixon artifact exporter.Reprrendering, so it is stable within a Lean toolchain but may change when the toolchain changes. The artifact cache is keyed on the exporter binary as well as the digest.IxVM and MultiStark as Lean modules
IxVM/IxVM/Modules/*.leanandMultiStark/MultiStark/Modules/*.leanhold the programs asaiur⟦ … ⟧blocks. The library (Aiur/Aiur/Library/**) usesaiur_library%.Aiur,IxVMandMultiStarkare nested Lake packages that the rootlakefile.leanrequires.Ix.SpecDigest.specBytesnow commits to everythingRoleSpecGenrenders into the circuit: the group schedule and boundaries, role names, inert, quotKind and nativeOp.encodingVersion2 is new;specVersionstays 3. The digest is84d3999ef8f830d2d0678f21d81730d2aee6f9a2cfd04c84d593b38f52eb7fae(main:6d02153e…).KernelRoleSpec.leanis rendered from the decoded bytes alone.ix codegen --checkand the primary-tier testspec-digest-renderingrebuild it, and the test includes five mutation cases.lake exe ixvm/ixvm digest,stark-export digest [--aggregate]):d688a528decc6d14c03c1a7da6ce9af48aba4e40dbb3b4c74bb959e353b490f4;16f71882223eb33daef9582d38c441f05645c1b65488fdafc14ff67069175654;55f83f502d82c64ac5ebaf13574fd583c0cf805c264aa8d567d78926005f9478.Artifacts in Ixon
IXAIURPprogram package (.ixa);IXAIURXexecution package;IXAIURGgrouping;IXAIURIinvocation (.ixi);IXAIURTtest cases (.ixt);IXROOTL, the compression root layout (.ixl).--aiur-artifact-digest,IX_AIUR_ARTIFACT_DIGEST,IX_AGGR_ARTIFACT_DIGEST).ix-prover serverefuses an artifact whose digest differs from its configuration.ix preparecompiles and exports the artifacts ahead of time. Otherwise the first use builds them once per source revision.STARK parameters and compression
Parameters:log_blowup · queries + query_pow ≥ 220. The explicit*_below_floorwaivers are for tests and forstark-verifier statistics, which trusts no key.lake exe fri-securityreplacestools/compression/fri_security_estimate.py.docs/stark-parameters.md).0.2(crates/proof-compression/verifying-keys/0.2/), regenerated for the formal aggregation verifying key. The0.1keys are removed.ROOT_VK_BLAKE3d286b37b8b9167fff7de272b70a577d1a8e5fb7ba66dd68488d3b79467820c02;STATEMENT_PREFIX[1, 0, 860334012, 1220120966, 1187167253, 3205439471, 3112596009, 4264259287, 80555980, 4021139237], which now starts with call channel 1 instead of main's 0;LAYOUT_BLAKE3708e3b5d7494d3657e78c104d15a276df89299cc589b4444fa1b4ade80cdd928;RECURSIVE_VK_BLAKE381ca053b35d43bf4d17447e8c21749ad74d24573abc367da5682b4bb6506c7fd.contracts/plonk/src/PlonkVerifier.sol.root-layout.ixl) and replaceslayout.json.release_keysexample derives the keys and prints every pin.crates/proof-compression/README.md, "Deriving the verifying keys".ix compresschecks a claim's statement against the release before proving.Tests/Fixtures/Compression/nat-add-comm.ixon-proofis a compressedNat.add_commproof under the new keys.PROVENANCE.md).90f78383….Tests and CI
Tests/FormalAggregate.lean).ci:ixvmtier: runs them on every PR. On main the IxVM suites ran only in the merge queue'sci:misc.spec-digest-rendering;Tests/CompressionCli.lean;formal-aggregate-tests, including a scheduler self-test.ci.yml,bench-main.yml,bench-pr.yml,bencher-thresholds-reset.ymlandupdate.yml.Breaking changes
See
docs/formal-aiur-migration.md.Aiurrequires Mathlib (with aesop, Qq, proofwidgets, importGraph and LeanSearchClient). The root package requires the nestedaiur,ixvmandmultiStarkpackages.ix's proving commands run separate Rust hosts:ixvm-proof,stark-verifierandix-prover.ixneedsIX_ROOT, or prebuilt artifacts plusIX_AIUR_HOST,IX_PROVER_HOSTandIX_STARK_HOST.ix-ffitoix-prover.ix prove --gpusbecomes--lanes.ix codegen --trace-bundle/--trace-cuda/--trace-rust/--targetare removed, along with the legacy multi-GPU scheduler and the generated CUDA trace writers (docs/aiur-gpu-proving.mdis now marked historical).Ix.Aiur.*andIx.IxVM.*modules are removed, exceptIx.Aiur.{FriSecurity,Goldilocks,Parameters,Protocol}andIx.IxVM.{ClaimHarness,RoleSpecGen}. So are the rootMultiStarklibrary andIx.Aggr.{Backend,Circuit,FFI,FunctionGroups}.bench-aiur,bench-blake3,bench-sha256,bench-ixvm,bench-recursion-debug,bench-aggregate-policyandbench-typecheck;proving-profile,function-groupingandtrace-fixtures.aiurbench backend stays registered but is disabled until a formal replacement exists.crates/ixvm-codegenis removed. New crates:ixvm,stark-verifier,stark-key,record-poolandix-prover.0.1to0.2, and0.1compressed proofs no longer verify.Kept from #677
The formal programs keep the checks #677 added to the legacy backend:
990ec1da5);e8ee6f7b4).Since the review
.aiursource files became embeddedaiur⟦ … ⟧Lean modules. Every converted program, and its exported artifacts, is byte-identical to its string-parsed predecessor (docs/formal-aiur-modules.md)..pytools this branch had added (tools/ixvm/adapt.py,modules.py,recursion.py,audit.pyand others) are ported to Lean. The JSON artifacts are ported to Ixon.WellFormedActivation. The audit freezes the acyclicity hypotheses with proofs printed.formal-aggregate-tests, a cross-threadIO.Refsignal, now goes through a promise.Follow-ups
IxC, and relate the library's Aiur source to its Lean models.IO.Refsignal inix check-lean's progress reporter, already on main.Ix.HostAdmission.Auditinto CI, also already on main.of_decide_eq_true/_false,Decidable.isTrue/isFalse) wherever a decision role is bound.NatorIntdecision evaluates to false, IxVM usesof_decide_eq_false, but no decision role lists it inRole.deps.Array.extract_append._proof_1_1.Verification
Final head
030205946, checked on a 64-core box.At
e339ca8db, everyci.ymlPR step exceptcuda-compilepassed:lake build --wfail, the spec, host-admission and certificate audits, the role-dependency script and the axiom sweep;Aiur.Audit, and the Aiur test binaries;ix codegen --check, the IxVM fixture export and validation, andcheck-formal.sh;lake test(default,ci:ixvm,ci:cli),ixon-v4,ffi-testsandcompression-cli;cargo fmt, clippy,cargo test(713 passed),cargo check --all-targetsand cargo-deny;Also at
e339ca8db, thenix.ymlsteps passed:nix build,nix run .#ix,nix flake check, andlake buildin the dev shell.The two commits after
e339ca8dbchange only comments. At030205946:issue_commentfindings).The compress → verify roundtrip under the 0.2 keys ran at
c8029ad44, and nothing after it touches compression.Not run before pushing:
cuda-compile(no CUDA toolkit on the box) and the merge-queue suite (merge-tests.yml).