Skip to content

feat(prover): add composable prover interface - #3437

Open
adr1anh wants to merge 28 commits into
nextfrom
adr1anh/prover-api
Open

feat(prover): add composable prover interface#3437
adr1anh wants to merge 28 commits into
nextfrom
adr1anh/prover-api

Conversation

@adr1anh

@adr1anh adr1anh commented Jul 29, 2026

Copy link
Copy Markdown
Contributor

Summary

Closes #3420.

This PR replaces the intermediate partial-proof APIs with a composable execution-proof lifecycle
built around the upstream canonical miden_core::program::ExecutionClaim.

  • Execution produces checked ExecutionWitness { VmWitness, Option<PrecompileWitness> } artifacts.
  • VM-first proving may finish immediately or retain authenticated precompile work in
    ExecutionProof::Deferred.
  • Precompile proving may run later and complete the existing VM proof without reproving it.
  • Verification borrows the canonical claim and proof, validates public structure, verifies every
    supplied STARK, and reports any authenticated outstanding precompile root.
  • Synchronous end-to-end proving retains Parallelize chiplet trace generation and overlap it with execution #3407's overlapped execution/hasher trace-building path.
  • Recursive VM verification uses the upstream claim encoding and commitment from Recursive verifier API #3422.

Public lifecycle

impl Prover {
    /// Proves the VM and returns either an empty Complete proof or a Deferred proof.
    pub fn prove(&self, witness: ExecutionWitness) -> Result<ExecutionProof, ProverError>;

    /// Proves the VM and all retained precompile work in memory.
    pub fn prove_full(&self, witness: ExecutionWitness) -> Result<ExecutionProof, ProverError>;

    /// Proves one singleton or merged precompile witness.
    pub fn prove_precompile(
        &self,
        witness: &PrecompileWitness,
    ) -> Result<PrecompileProof, ProverError>;
}

impl Verifier {
    pub fn verify(
        &self,
        claim: &ExecutionClaim,
        proof: &ExecutionProof,
    ) -> Result<VerificationOutcome, VerificationError>;
}

ExecutionProof has two public states:

pub enum ExecutionProof {
    Deferred { vm: VmProof, precompile: PrecompileWitness },
    Complete { vm: VmProof, precompile: Option<PrecompileProof> },
}

Public construction and serialization preserve representation; they are not cryptographic proof
validation. ExecutionProof::validate_structure is the shared structural-validation seam used by
Verifier::verify. For deferred proofs, verification verifies the VM STARK and returns its
authenticated precompile root as an outstanding obligation. For complete proofs, it verifies the VM
STARK and any supplied precompile STARK and returns the minimum component security level.

VerificationOutcome is #[must_use] because successful verification may still leave an
outstanding precompile obligation.

Examples

Complete local proving

let witness = processor.execute_for_proving_sync(&program, &mut host)?;
let claim = witness.claim();
let proof = Prover::new().prove_full(witness)?;
let outcome = Verifier::new().verify(&claim, &proof)?;
assert!(outcome.is_complete());

VM-first proving and later completion

let witness = processor.execute_for_proving_sync(&program, &mut host)?;
let claim = witness.claim();
let prover = Prover::new();
let proof = prover.prove(witness)?;

let deferred = Verifier::new().verify(&claim, &proof)?;
assert!(!deferred.is_complete());

let precompile = prover.prove_precompile(
    proof.precompile_witness().expect("deferred proof retains its witness"),
)?;
let proof = proof.complete(precompile)?;
assert!(Verifier::new().verify(&claim, &proof)?.is_complete());

Migration

  • Use the canonical miden_core::program::ExecutionClaim; the branch-local competing claim was
    removed. Its encoding, commitment, and recursive-verification semantics are unchanged from Recursive verifier API #3422.
  • TraceWitness is now private TraceReplay.
  • ExecutionTrace is now VmTrace.
  • execute_trace_inputs* is now execute_for_proving* and returns ExecutionWitness.
  • Use Prover::{prove, prove_full, prove_precompile} instead of the removed async, partial, and
    trace-input free proving APIs.
  • ProvingOptions is removed. Configure a Prover with with_hash_fn.
  • The temporary free prove_sync(&Prover, ...) remains for the optimized overlapped synchronous
    route; later Executor work will own this orchestration.
  • Replace the old ExecutionProof/DeferredProof envelope with VmProof, PrecompileProof, and
    ExecutionProof::{Deferred, Complete}.
  • ExecutionProof::complete returns ExecutionProofError; the artifact-recovery completion error is
    removed.
  • Use borrowed Verifier::verify(&claim, &proof) and inspect its #[must_use]
    VerificationOutcome instead of the removed free/partial verification APIs.
  • max_proof_size is now max_stark_proof_size, clarifying that the limit applies independently to
    each inner STARK.
  • Ordinary callers decode with miden_vm::read_execution_proof_from_bytes; custom registries use
    ExecutionProof::read_from_bytes(bytes, registry, max_elements).

Transport and resource policy

  • ExecutionProof::to_bytes and PrecompileWitness::to_bytes are fallible because canonical
    deferred-state materialization may detect an integrity error.
  • Decoding checks syntax, canonical round trips, and context-dependent witness hydration; full
    structural and cryptographic validity remains the verifier's responsibility.
  • StarkProof and VmProof report their actual minimum encoded sizes so budgeted sequence decoding
    does not reject valid compact encodings.
  • The façade decoder uses the bundled precompile registry and the existing default deferred-state
    limit of 1 << 20 approximate field elements.
  • Verifier defaults to 64 MiB for each VM or precompile STARK independently. A configured smaller
    accepted-proof limit does not replace the separate 64 MiB per-allocation decoding ceiling.
  • Aggregate root-count, outer-envelope, merged-witness, and decoder-preallocation policy is tracked
    in Define and enforce aggregate execution-proof resource limits #3458, the successor to planning ticket 022.

Remaining work / non-goals

  • The old planning ticket 021 for delegated VmWitness transport is obsolete for this PR.
    Prover::prove_vm is private, this PR has no delegated VM-worker transport dependency, and any
    separate transport work must adapt to the merged API independently.
  • Define and enforce aggregate execution-proof resource limits #3458 tracks the coherent aggregate resource policy raised during review: root-count and envelope
    bounds, merged-witness budgeting, and decoder preallocation policy.
  • This PR does not add the future Executor, a protocol settlement envelope, a delegated VM-worker
    API, a new registry identity model, or replacement serde fuzzing.

Suggested review order

  1. Proof and witness artifacts: core/src/proof.rs, core/src/deferred/witness.rs.
  2. Execution witness and trace terminology: processor/src/trace/, processor/src/fast/.
  3. Proving implementation: prover/src/prover.rs.
  4. Deferred/complete verification: verifier/src/lib.rs.
  5. Façade and lifecycle migration: miden-vm/src/, miden-vm/tests/integration/prove_verify.rs.
  6. Documentation and migration notes.

Validation

Post-rebase branch validation:

  • RUSTFLAGS=" -D warnings" cargo +stable xclippy
  • cargo +nightly fmt --all --check
  • miden-vm lifecycle: 2 passed; buffered/overlapped regression stress loop: 50/50 passed
  • miden-vm recursive verification: 1 passed
  • miden-verifier: 10 passed
  • miden-prover --features concurrent: 5 passed
  • miden-processor witness/claim tests: 2 passed
  • miden-core-lib deferred-root/request-flow recursive tests: 2 passed
  • GitHub workspace test job: 5,087 passed
  • GitHub lint workflow, including Clippy, rustfmt, docs, and cargo-shear: passed

Latest review-fix validation:

  • miden-core proof minimum-size regression: 1 passed
  • miden-verifier: 10 passed
  • miden-vm deferred/merged lifecycle: 1 passed

Checklist

  • Uses the upstream canonical execution claim and recursive commitment semantics.
  • Reconciles façade, CLI, benchmarks, precompile prover, recursive verifier, and tests.
  • Removes superseded APIs instead of restoring them.
  • Keeps changed documentation within the 100-character convention.
  • All existing branch commits are signed.
  • Changelog preserves upstream history and adds one feat(prover): add composable prover interface #3437 lifecycle entry.
  • Rebase the final review fixes onto current next before marking ready.

@github-actions

Copy link
Copy Markdown

This PR contains unsigned commits. All commits must be cryptographically signed (GPG or SSH).

Unsigned commits:

  • a86312ee feat: represent deferred execution proofs
  • 7a953501 refactor(prover): simplify proving interface
  • 40324bb0 feat(verifier): verify deferred execution proofs
  • 4813e3d5 refactor(prover): complete deferred proof migration

For instructions on setting up commit signing and re-signing existing commits, see:
https://docs.github.com/en/authentication/managing-commit-signature-verification/signing-commits

2 similar comments
@github-actions

Copy link
Copy Markdown

This PR contains unsigned commits. All commits must be cryptographically signed (GPG or SSH).

Unsigned commits:

  • a86312ee feat: represent deferred execution proofs
  • 7a953501 refactor(prover): simplify proving interface
  • 40324bb0 feat(verifier): verify deferred execution proofs
  • 4813e3d5 refactor(prover): complete deferred proof migration

For instructions on setting up commit signing and re-signing existing commits, see:
https://docs.github.com/en/authentication/managing-commit-signature-verification/signing-commits

@github-actions

Copy link
Copy Markdown

This PR contains unsigned commits. All commits must be cryptographically signed (GPG or SSH).

Unsigned commits:

  • a86312ee feat: represent deferred execution proofs
  • 7a953501 refactor(prover): simplify proving interface
  • 40324bb0 feat(verifier): verify deferred execution proofs
  • 4813e3d5 refactor(prover): complete deferred proof migration

For instructions on setting up commit signing and re-signing existing commits, see:
https://docs.github.com/en/authentication/managing-commit-signature-verification/signing-commits

@adr1anh
adr1anh force-pushed the adr1anh/prover-api branch from 2503624 to 49bbc76 Compare July 31, 2026 09:03
@github-actions

Copy link
Copy Markdown

This PR contains unsigned commits. All commits must be cryptographically signed (GPG or SSH).

Unsigned commits:

  • de6d8181 feat(core): add mergeable precompile witnesses
  • 296a7268 feat(core): represent deferred execution proofs
  • 28d7bf94 refactor(prover): support deferred and full proving
  • f70d7349 feat(verifier): verify deferred execution proofs
  • e4c53133 refactor(vm): migrate deferred proof workflows
  • d182df95 refactor(deferred): make wire encoding infallible
  • 49bbc761 docs: simplify prover API documentation

For instructions on setting up commit signing and re-signing existing commits, see:
https://docs.github.com/en/authentication/managing-commit-signature-verification/signing-commits

@adr1anh
adr1anh force-pushed the adr1anh/prover-api branch from 49bbc76 to 2ec75c4 Compare July 31, 2026 09:42
Comment thread core/src/proof.rs
/// Returns the deferred proof material associated with the Miden VM proof.
pub const fn deferred_proof(&self) -> &DeferredProof {
&self.deferred
impl Deserializable for VmProof {

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Vec<VmProof> uses Deserializable::min_serialized_size() before allocation, and the default is the 64-byte in-memory size even though the shortest encoding is 34 bytes.

I think we need to override the minima for StarkProof and VmProof (plus optionally an all-settled batch round-trip test) to keep canonical encodings readable.

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this concern is still live

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fixed. StarkProof now reports the minimum size of its encoded byte vector plus hash-function tag, and VmProof composes that with the deferred-root encoding. This gives VmProof its actual 34-byte minimum rather than its 64-byte in-memory size, so budgeted Vec decoding continues to accept compact canonical encodings.

I also added a regression test that checks the reported StarkProof and VmProof minima against their shortest canonical encodings.

Comment thread verifier/src/lib.rs
Comment thread prover/src/prover.rs Outdated
@github-actions

github-actions Bot commented Aug 1, 2026

Copy link
Copy Markdown

This PR contains unsigned commits. All commits must be cryptographically signed (GPG or SSH).

Unsigned commits:

  • 4577ef23 refactor(proof): clarify deferred verification semantics
  • 7c2a43c5 refactor(processor): privatize trace replay
  • eddb74ca refactor(processor): aggregate execution witnesses
  • 172cde1b refactor(processor): rename materialized VM trace
  • 279c1ee4 refactor(processor): rename execution-for-proving API
  • c073ce98 refactor(prover): converge witness and trace proving
  • 8f8b821c chore(processor): format replay refactor
  • 448ca214 refactor(vm): migrate composable proof lifecycle
  • a069fae7 chore(core): remove redundant proof clone

For instructions on setting up commit signing and re-signing existing commits, see:
https://docs.github.com/en/authentication/managing-commit-signature-verification/signing-commits

1 similar comment
@github-actions

github-actions Bot commented Aug 1, 2026

Copy link
Copy Markdown

This PR contains unsigned commits. All commits must be cryptographically signed (GPG or SSH).

Unsigned commits:

  • 4577ef23 refactor(proof): clarify deferred verification semantics
  • 7c2a43c5 refactor(processor): privatize trace replay
  • eddb74ca refactor(processor): aggregate execution witnesses
  • 172cde1b refactor(processor): rename materialized VM trace
  • 279c1ee4 refactor(processor): rename execution-for-proving API
  • c073ce98 refactor(prover): converge witness and trace proving
  • 8f8b821c chore(processor): format replay refactor
  • 448ca214 refactor(vm): migrate composable proof lifecycle
  • a069fae7 chore(core): remove redundant proof clone

For instructions on setting up commit signing and re-signing existing commits, see:
https://docs.github.com/en/authentication/managing-commit-signature-verification/signing-commits

@bobbinth bobbinth mentioned this pull request Aug 2, 2026
@adr1anh
adr1anh force-pushed the adr1anh/prover-api branch from 487ae98 to 293e599 Compare August 3, 2026 14:55
@adr1anh
adr1anh force-pushed the adr1anh/prover-api branch from 293e599 to 9bbc353 Compare August 3, 2026 14:57
@adr1anh
adr1anh force-pushed the adr1anh/prover-api branch from 673b3db to a09439b Compare August 3, 2026 17:07

@huitseeker huitseeker left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the aggregate limit issue is still unsolved as well.

Comment thread verifier/src/lib.rs
Comment thread verifier/src/lib.rs Outdated
Comment thread core/src/proof.rs
/// Returns the deferred proof material associated with the Miden VM proof.
pub const fn deferred_proof(&self) -> &DeferredProof {
&self.deferred
impl Deserializable for VmProof {

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this concern is still live

Comment thread verifier/src/lib.rs
@bobbinth

bobbinth commented Aug 3, 2026

Copy link
Copy Markdown
Contributor
impl Prover {
    pub fn prove(&self, witness: ExecutionWitness) -> Result<ExecutionProof, ProverError>;
    pub fn prove_full(&self, witness: ExecutionWitness) -> Result<ExecutionProof, ProverError>;
    pub fn prove_vm(&self, witness: VmWitness) -> Result<VmProof, ProverError>;
    pub fn prove_precompile(
        &self,
        witness: &PrecompileWitness,
    ) -> Result<PrecompileProof, ProverError>;
}

In the above, what's the difference between prove(), prove_full(), and prove_vm()?

@adr1anh

adr1anh commented Aug 4, 2026

Copy link
Copy Markdown
Contributor Author
impl Prover {

    pub fn prove(&self, witness: ExecutionWitness) -> Result<ExecutionProof, ProverError>;

    pub fn prove_full(&self, witness: ExecutionWitness) -> Result<ExecutionProof, ProverError>;

    pub fn prove_vm(&self, witness: VmWitness) -> Result<VmProof, ProverError>;

    pub fn prove_precompile(

        &self,

        witness: &PrecompileWitness,

    ) -> Result<PrecompileProof, ProverError>;

}

In the above, what's the difference between prove(), prove_full(), and prove_vm()?

Here, prove would be better named prove_partial, which returns an ExecutionProof with a unproven precompile state. If there are no precompiles, then it returns a complete proof, with an empty precompile proof.

The prove_full will also run the precompile prover to produce a full proof.

In contrast, prove_vm is a convenience function which proves a VM witness, without access to the precompile witness. I understood that we might have a VM-only delegated prover, which this prover would invoke.

@adr1anh
adr1anh marked this pull request as ready for review August 4, 2026 15:28
@adr1anh

adr1anh commented Aug 4, 2026

Copy link
Copy Markdown
Contributor Author

@huitseeker Agreed that the full aggregate policy was still unresolved. I have split the work into:

  1. Direct safety fixes in this PR:
    • hard constituent-root ceiling enforced before root-vector allocation and aggregate-root folding;
    • explicit aggregate element bound for witness merging;
    • rejection of an already-oversized merge accumulator.
  2. A stacked follow-up in Define and enforce aggregate execution-proof resource limits #3458:
    • complete execution-proof envelope limits;
    • early inner-STARK byte limits;
    • configurable acceptance limits below the hard ceilings;
    • consistent prover/verifier/facade and ingestion policy.

This removes the unbounded operations introduced by this PR without defining the broader resource-policy interface in the middle of the prover lifecycle review.

Comment thread core/src/proof.rs
}

impl Deserializable for ExecutionProof {
impl Deserializable for PrecompileProof {

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

PrecompileProof still inherits the 56-byte in-memory default for min_serialized_size(), although its smallest valid encoding is 35 bytes.

This makes the recommended budgeted decoder reject valid collections: two singleton proofs encode in 71 bytes, but Vec<PrecompileProof>::read_from_bytes_with_budget(..., 71) fails with requested 2 elements but reader can provide at most 1.

We should override the minimum for the required one-root shape (and optionally add a budgeted two-proof round-trip test).

Comment thread prover/README.md

The deferred-wire canonical decode-and-reencode policy remains unchanged. The outer execution-proof
decoder now rejects trailing bytes and encodings that do not round-trip exactly. Hydration takes an
explicit deferred-element bound, and decoding retains its per-allocation ceiling. Merging resets the

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This paragraph now describes the opposite of 74a5bed7: PrecompileWitness::merge requires max_elements, enforces it across the whole merged state, and caps the list at MAX_PRECOMPILE_ROOTS.

The same stale policy appears in docs/src/design/deferred/semantics.md, and docs/src/design/stack/precompiles.md still shows the old one-argument call.

Can you update all three together?

Comment thread core/src/proof.rs
roots: Vec<DeferredRoot>,
}

let Fields { proof, roots } = Fields::deserialize(deserializer)?;

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit: The 4,096-root check in from_parts runs only after this Vec has been fully deserialized, so a serde/Postcard caller can reserve and parse more roots than the cap before rejection.

There's no in-repo serde consumer of PrecompileProof, and the standard ExecutionProof transport uses the early-checked binary decoder, so this is not currently reachable here.

Still, could we either use a bounded visitor or document this serde path as trusted-only?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Introduce a configurable Prover API

3 participants