AAdrian Hamelinkfix: restore proof and witness transport format v2
| 文件 | 最后提交记录 | 最后更新时间 |
|---|---|---|
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 个月前 | |
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 个月前 | |
Fix Merkle tree depth bound issue (#3671) | 1 个月前 | |
fix(processor): return error on empty OverflowTable instead of panicking (#3370) Signed-off-by: Sertug17 <104278804+Sertug17@users.noreply.github.com> Co-authored-by: François Garillot <4142+huitseeker@users.noreply.github.com> | 1 个月前 | |
fix(verifier): evaluate portable precompile witnesses | 12 天前 | |
3/3 test: Add trace proving input fuzz and proptest coverage (#3315) * test: cover trace input trusted round trips * chore: Changelog * chore: move trace proving input test coverage changelog entry to v0.30.0 section * Address review feedback on PR #3315 Update the changelog phrasing away from the outdated trace proving input wording, and teach the serialization tests to reach the queue-reading helpers from their new home in the trace_state serde submodule. * Adapt fuzz coverage to the witness prover API Keep the external-library and deferred-wire round-trip coverage after the trace-specific proving input API removal. Deserialize ExecutionWitness and prove it through the regular Prover interface. * Test ExecutionWitness serialization directly Generate property cases through real executions and fuzz the bounded witness decoder with valid ordinary and deferred seeds. Remove feature wiring that only supported blanket serializer Arbitrary implementations. * Use a replay-sized witness fuzz budget Give the witness fuzzer the same bounded allocation budget as the round-trip tests. Verify each generated corpus seed decodes under that exact budget. * chore: resolve changelog overlap after squash merge The child series was replayed after #3314's squash merge. New upstream changelog entries made two historical hunks apply at a second location, which duplicated the #3314 entry and retained a superseded #3315 entry. Keep the merged #3314 entries and the final #3315 coverage description. | 1 个月前 | |
docs: trim decorative comments Address Al-Kindi review themes #3 (historical leftovers) and #4 (over-justification of Rust mechanics) on PR #2962, plus a small going-beyond sweep for doc comments that just restate the signature. - Historical narration: drop "removed in Milestone B", "legacy AuxCols<T>", "the legacy v_wiring", "previously two walkers ran back-to-back", "the way the legacy verify_b_chip_step_by_step did", and similar back-references in module headers and test docs; forward-point where the prose still earned its keep. - Rust-mechanics narration: drop split-borrow / GAT-lifetime / snapshot-up-front / scope-the-borrow comments in lookup builder, prover adapter, fraction collector, and main-air eval — the code reads cleanly without them. - Signature restatements: drop "Returns true if the block stack is empty" / "Removes a block from the top of the stack" / etc. on block_stack.rs methods whose names already say it. No logic changes. \`make lint\` and \`make doc\` clean. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> | 4 个月前 | |
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 个月前 | |
fix: restore proof and witness transport format v2 | 12 天前 | |
3/3 test: Add trace proving input fuzz and proptest coverage (#3315) * test: cover trace input trusted round trips * chore: Changelog * chore: move trace proving input test coverage changelog entry to v0.30.0 section * Address review feedback on PR #3315 Update the changelog phrasing away from the outdated trace proving input wording, and teach the serialization tests to reach the queue-reading helpers from their new home in the trace_state serde submodule. * Adapt fuzz coverage to the witness prover API Keep the external-library and deferred-wire round-trip coverage after the trace-specific proving input API removal. Deserialize ExecutionWitness and prove it through the regular Prover interface. * Test ExecutionWitness serialization directly Generate property cases through real executions and fuzz the bounded witness decoder with valid ordinary and deferred seeds. Remove feature wiring that only supported blanket serializer Arbitrary implementations. * Use a replay-sized witness fuzz budget Give the witness fuzzer the same bounded allocation budget as the round-trip tests. Verify each generated corpus seed decodes under that exact budget. * chore: resolve changelog overlap after squash merge The child series was replayed after #3314's squash merge. New upstream changelog entries made two historical hunks apply at a second location, which duplicated the #3314 entry and retained a superseded #3315 entry. Keep the merged #3314 entries and the final #3315 coverage description. | 1 个月前 | |
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 个月前 |