miden/air/src · mi/miden-vm

文件	最后提交记录	最后更新时间
ace	PVM MASM verifier (#3467) * feat(core-lib): add recursive PVM proof verification - add sys::pvm::verify_proof and its Poseidon2 host-input adapter - extract relation-independent STARK verifier logic for MVM and PVM wrappers - generate and authenticate the factored PVM ACE evaluator with four quotient chunks - define relation-local memory layouts and guard them against overlap - pin transcript, PCS, circuit, and proof-order contracts with cross-language tests - verify MVM and PVM proofs can execute safely in the same program * feat(core-lib): support awaited PVM proof settlement - share proof-request addressing and security outputs across recursive verifiers - let async hosts install PVM proof packages for authenticated deferred roots - test MVM-to-PVM ECDSA settlement and harden verifier input handling * refactor(deferred): represent PVM proofs with explicit claims * test(core-lib): verify recursive AIR selectors * perf(core-lib): optimize generic proof-order tag derivation - split the height scan to remove redundant comparisons - reduce PVM verification by 2,431 cycles without scratch memory - cover AIR counts 2–12, u32 boundaries, stable ties, and cycle regressions * Precompute factorials for generic proof-order tags * perf(core-lib): batch PVM public-input transcript absorption * perf(core-lib): optimize PVM auxiliary-boundary folding * Benchmark mixed MVM and PVM recursive verification compare 4 MVM + 1 PVM and 5 MVM + 1 PVM against 7 and 8 MVM proofs using the canonical 100-Keccak/4-ECDSA PVM proof * fix(ace): address registry review feedback * chore: address FG review * fix(pvm): address review feedback on proof shape and regen config * chore: address FG comment	1 个月前
constraints	fix: remove the bus debugger (#3775) * Remove the bus debugger * Address review findings * chore: Changelog	25 天前
lookup	Misc. perf improvements (#3851)	12 天前
snapshots	Constrain stack overflow pointer transitions (#3684) * fix(air): constrain overflow pointer transitions * test(air): cover overflow pointer restoration * chore: Changelog * fix(air): address overflow review feedback	1 个月前
trace	2/3 Serialize trace proving inputs (#3314) * Serialize trace proving inputs Adds the trusted binary wire format for trace proving inputs on top of the post-#3437 witness API: - serialize VmWitness (program info, stack i/o, trace replay, precompile root) - serialize ExecutionWitness with an option-tagged singleton precompile witness (ordered roots plus canonical deferred wire) via local helper functions, since PrecompileWitness and the serde traits are both foreign to the processor crate - TraceProvingInputs wraps ExecutionWitness plus a HashFunction and keeps the budgeted trusted read path; prove_from_trace_sync and prove_partial_from_trace_sync map to Prover::prove_full and Prover::prove - range-check replay covers the U32DIV remainder diffs recorded since #3604 The wire is trusted replay data: sparse MAST node and digest maps are not checked against a source MastForest commitment (#3303 tracks the untrusted reader). * chore: Changelog * fix: Make trace input serialization features standalone * fix: Address trace input serialization review comments * docs: clarify trace input trust boundary * refactor: reduce trace input serialization diff * fix: adapt trace serialization tests to streamed hasher replay * fix: validate precompile witness and VM witness roots agree on wire reads ExecutionWitness::read_from accepted wires whose halves describe different executions: each half was validated individually, but nothing compared them. Enforce the construction invariant in both directions: - when a precompile witness is present, its root must equal the VM witness precompile root (both derive from the same deferred state), and - when it is absent, the VM witness precompile root must be TRUE_DIGEST, since a non-TRUE root means execution authenticated deferred work and cannot round-trip without its precompile half. Cover both tampered cases with in-crate regression tests. * chore: use miden-crypto's arbitrary feature for replay Arbitrary impls miden-crypto, now maintained in this repository, exposes a public arbitrary feature providing Arbitrary for MerklePath (plus Felt and Word via miden-field/arbitrary), resolving the two TODOs this PR carried: - miden-core's arbitrary feature now enables miden-crypto/arbitrary directly instead of reaching through miden-crypto/testing, which is a strict superset of it - the trace replay proptest strategies use any::<MerklePath>() instead of a local hand-rolled strategy, exercising Merkle paths up to SMT_MAX_DEPTH instead of the previous 8-element cap * Address review feedback on PR #3314 - Add a wire format version tag to ExecutionWitness serialization: the first byte of every serialized witness is a version constant, and deserialization only accepts the current value, so future format changes have an explicit evolution point - Drop source_node_ids from the serialized ContinuationStack: those indices reference a package's PackageDebugInfo, which is not on the wire, so they would be dangling on the deserialized side; a restored stack simply does not track source nodes, as a non-debug-aware execution would - Document that Continuation serialization deliberately omits package_debug_info, so round-tripping any struct containing a Continuation is not exact, and note why the VecDeque serialization uses a newtype view and why ACE replay serialization uses free functions (the orphan rule forbids impls on the foreign types) - Move the trace fragment state serialization impls into a trace_state/serde submodule to keep trace_state.rs focused - Update the changelog phrasing away from the outdated trace proving input wording and add a README for the test-serde-macros helper crate * Remove trace-specific proving inputs API * Keep property tests in the follow-up PR Remove generated property-test support from the serializer implementation branch. Apply the latest review feedback to the changelog, module layout, replay helper docs, and prover manifest. * Reuse workspace serialization implementations	1 个月前
ace.rs	PVM MASM verifier (#3467) * feat(core-lib): add recursive PVM proof verification - add sys::pvm::verify_proof and its Poseidon2 host-input adapter - extract relation-independent STARK verifier logic for MVM and PVM wrappers - generate and authenticate the factored PVM ACE evaluator with four quotient chunks - define relation-local memory layouts and guard them against overlap - pin transcript, PCS, circuit, and proof-order contracts with cross-language tests - verify MVM and PVM proofs can execute safely in the same program * feat(core-lib): support awaited PVM proof settlement - share proof-request addressing and security outputs across recursive verifiers - let async hosts install PVM proof packages for authenticated deferred roots - test MVM-to-PVM ECDSA settlement and harden verifier input handling * refactor(deferred): represent PVM proofs with explicit claims * test(core-lib): verify recursive AIR selectors * perf(core-lib): optimize generic proof-order tag derivation - split the height scan to remove redundant comparisons - reduce PVM verification by 2,431 cycles without scratch memory - cover AIR counts 2–12, u32 boundaries, stable ties, and cycle regressions * Precompute factorials for generic proof-order tags * perf(core-lib): batch PVM public-input transcript absorption * perf(core-lib): optimize PVM auxiliary-boundary folding * Benchmark mixed MVM and PVM recursive verification compare 4 MVM + 1 PVM and 5 MVM + 1 PVM against 7 and 8 MVM proofs using the canonical 100-Keccak/4-ECDSA PVM proof * fix(ace): address registry review feedback * chore: address FG review * fix(pvm): address review feedback on proof shape and regen config * chore: address FG comment	1 个月前
config.rs	feat: add recursive PVM security estimator (#3752)	27 天前
lib.rs	chore: bump Plonky3 deps to v0.7.0 (#3778) * chore: bump Plonky3 deps to v0.7.0 * chore: CHANGELOG * review: address comments - Derive OOD_COEFFICIENT's combo term from AIR_SHAPE.max_combo instead of repeating its current value as a literal, in both the main and precompiles security estimators, so it can't go stale if NUM_OOD_POINTS changes. - Move the periodic-column arrays into their Cow::Owned instead of cloning them via to_vec(), in the chunk/Keccak-node/Keccak-sponge, Keccak round, Keccak sponge, and Poseidon2 AIR adapters.	25 天前
memory.rs	feat: bound prover memory with a byte budget instead of a trace-row cap (#3706) * feat: bound prover memory with a byte budget instead of a trace-row cap The trace-row cap stopped tracking memory once the VM moved to three independently-padded AIRs: it checked max per-AIR height, ignoring width differences and real workload divergence (2^18 core vs 2^20 chiplets on bench-tx b2agg). At ~10 KiB peak prover memory per row, the 2^29 default admitted ~5 TB. Add `miden_air::memory`, which models peak prover memory from per-AIR padded heights, deriving widths, aux widths, and quotient degrees from the AIR trait impls, and blowup from `PcsParams`. Trace building enforces it in two tiers: a permissive row cap from the cheapest AIR retains the existing incremental chiplet guards, and an exact check on padded heights runs before the padded matrices are allocated, returning `ExecutionError::ProverMemoryExceeded`. The budget is configured via `ExecutionOptions::max_prover_memory_bytes` (default 64 GiB, CLI flag `--max-prover-memory`) and rides to `build_trace` on the witness, covering both buffered and overlapped proving paths. `build_trace_with_max_len` is replaced by `build_trace_with_budget`, and `TraceLenSummary` now records per-AIR padded heights for telemetry. The model covers main and aux traces at 1x plus their LDEs, the quotient accumulator, and the three LMCS digest trees; smaller/transient allocations are covered by a safety multiplier rather than modelled. It does not cover the precompile prover. Addresses #2845. * review: address comments * refactor: apply adr1anh's suggestion * fix	1 个月前
proof_order.rs	Add the factored precompile VM ACE registry (#3465) * feat(ace): Add the factored precompile VM ACE registry - factor multi-AIR ACE circuits into per-order and shared sections - add reusable order tagging, packed leaf hashing, and path authentication - mint the 10-chiplet PVM registry over all 10! proof orders - bind the registry root into the PVM relation digest - serve one authenticated subtree path per proof	1 个月前
security.rs	chore: bump Plonky3 deps to v0.7.0 (#3778) * chore: bump Plonky3 deps to v0.7.0 * chore: CHANGELOG * review: address comments - Derive OOD_COEFFICIENT's combo term from AIR_SHAPE.max_combo instead of repeating its current value as a literal, in both the main and precompiles security estimators, so it can't go stale if NUM_OOD_POINTS changes. - Move the periodic-column arrays into their Cow::Owned instead of cloning them via to_vec(), in the chunk/Keccak-node/Keccak-sponge, Keccak round, Keccak sponge, and Poseidon2 AIR adapters.	25 天前