LocalTransactionProver proves precompile claims locally (prove_sync) instead of deferring them (prove_partial_sync)

[WiktorStarczewski]

LocalTransactionProver::prove calls miden_prover::prove_sync, the final-proof API, so every local prove also generates the precompile-VM STARK for its deferred claims. Precompile proving is meant to happen at batch level; the local prover should call prove_partial_sync and ship the claims as a wire.

Symptom. A locally proven transaction whose auth verifies ECDSA signatures carries DeferredProof::Stark (~277 KB) next to the ~100 KB VM STARK, and that precompile STARK is 55-72% of local prove time.

Repro. Prove any ECDSA-authenticated transaction with LocalTransactionProver::default() and match on proven.proof().deferred_proof(): it is Stark { .. }. Cause: crates/miden-tx/src/prover/mod.rs:17 imports prove_sync and :148 calls it (same on next and 0.16.0-rc.9). prove_partial_sync is the documented API for claims "proved later by a delegated or batching prover" (miden-prover 0.29.4, src/lib.rs:164).

Expected. DeferredProof::Wire; the claims are checked natively by the verifier and proven at batch level. On next the verifier side already exists: TransactionVerifier handles PrecompileStatus::Deferred via validate_deferred_witness (crates/miden-protocol/src/transaction/verifier.rs:76-95), so there the fix is the prover switch plus tests.

Impact. Browser local proving (MT wasm, 6 threads) is 3.5x slower than necessary for guarded accounts and 2.8x for single-sig: with the one-line switch, guarded 7.99 s to 2.27 s and single-sig 4.58 s to 1.66 s; native guarded 1.68 s to 0.63 s. The proven transaction shrinks from 391 KB to 104 KB.

On 0.16.0-rc.9 (VM 0.29.4) the switch alone is not deployable: miden_verifier::verify returns UnsupportedDeferredProof for Wire, and both the node RPC (crates/rpc/src/server/api/submit_proven_tx.rs:108) and the validator (bin/validator/src/tx_validation/mod.rs:52) call TransactionVerifier::verify, so a client cannot opt in. Fixing 0.16 needs TransactionVerifier to accept partial proofs (Verifier::verify_partial exists in 0.29.4; rehydrating the wire re-evaluates every node under the registry, so native settlement is a root check) plus the node picking it up.

Evidence: runtime probes (0.16.0-rc.9 protocol crates, VM 0.29.4, web-sdk 0.16.0-rc.7)

Native, LocalTransactionProver::default().prove(executed), printing proven.proof().deferred_proof():

# 2 ECDSA claims (guarded multisig: 1 approver at threshold 1 + guardian)
tx: total_cycles=29095  auth_procedure=19847
DEFERRED_PROOF  Stark { proof: 276768 bytes, public_root: Word([10652471043400787702, 12148757343284257120, 17083288024192604590, 7234156251587950621]) }
VM_PROOF        101663 bytes

# 1 ECDSA claim (BasicAuth)
tx: total_cycles=17720  auth_procedure=9865
DEFERRED_PROOF  Stark { proof: 283680 bytes, public_root: Word([13415207134405930995, 16485817212495615892, 12092707907113953811, 2871210035726898790]) }
VM_PROOF        99711 bytes

# same two shapes after switching miden-tx to prove_partial_sync
DEFERRED_PROOF  Wire (partial, claims NOT proven)
VM_PROOF        100447 bytes   # 2 claims
VM_PROOF        100895 bytes   # 1 claim

Browser, client.proveTransaction(txResult, TransactionProver.newLocalProver()), proven.serialize().length:

single-sig  provenTxBytes 378589
guarded     provenTxBytes 391045
guarded, prove_partial_sync build   provenTxBytes 104118

Evidence: code pointers

• crates/miden-tx/src/prover/mod.rs:17 use miden_prover::{ExecutionProof, Word, prove_sync}; and :148 prove_sync( (next at b5cbb34; identical in 0.16.0-rc.9).
• miden-prover 0.29.4 src/lib.rs:123 prove_sync (final), :164 prove_partial_sync, :235-241 prove_deferred_state inside the precompile_vm span, :248-258 the wire variant.
• miden-core 0.29.4 src/proof.rs:261-275 DeferredProof::{Empty, Wire, Stark}.
• miden-verifier 0.29.4 src/lib.rs:177-188 resolve_final_deferred_root: Wire yields UnsupportedDeferredProof; src/lib.rs:123-135 verify_partial returns Unsettled(DeferredState).
• miden-protocol 0.16.0-rc.9 src/transaction/verifier.rs:33 calls miden_verifier::verify (full).
• node next: crates/rpc/src/server/api/submit_proven_tx.rs:108 and bin/validator/src/tx_validation/mod.rs:52 call TransactionVerifier::new(MIN_PROOF_SECURITY_LEVEL).verify.
• web-sdk crates/web-client/src/new_transactions.rs:713 LocalTransactionProver::default() for newLocalProver().

Measurements (M5, 4P+6E; native concurrent; browser MT wasm at 6 threads, 9 timed proves per run after a discarded warm-up, medians)

shape	prover	native prove	browser prove	proven tx
single-sig ECDSA	prove_sync (today)	1376 ms	4584 ms	379 KB
single-sig ECDSA	prove_partial_sync	602 ms	1663 ms	~104 KB
guarded (2 ECDSA claims)	prove_sync (today)	1678 ms	7987 ms	391 KB
guarded (2 ECDSA claims)	prove_partial_sync	630 ms	2272 ms	104 KB

The native precompile_vm span accounts for the whole difference (744 ms and 998 ms respectively; 0 ms with the partial API). The guarded premium over single-sig drops from 302 ms to 28 ms, since only the main trace remains and both shapes pad to 2^15 rows.

The one-line switch used for the "partial" rows, applied to 0.16.0-rc.9 and reverted afterwards:

-use miden_prover::{ExecutionProof, Word, prove_sync};
+use miden_prover::{ExecutionProof, Word, prove_partial_sync};
...
-        let (stack_outputs, proof) = prove_sync(
+        let (stack_outputs, proof) = prove_partial_sync(

[bobbinth]

I believe this is an issue for v0.17 branch as well. I'm actually not 100% sure how this passes our tests because we explicitly prohibit execution proofs that contain precompile proofs (cc @huitseeker in case you know off the top of your head).

The main question is whether we want to fix it just for v0.17 or for v0.16 as well. My thinking is that given that v0.16 is going to be relatively short-lived, we can make the fix only for v0.17 (and it should be easier to make it there too).

[huitseeker]

I checked that this is a mismatch between the prover and verifier. LocalTransactionProver calls prove_sync, so a real ECDSA transaction carries PrecompileStatus::Proven. TransactionVerifier rejects the same proof by design. We are not accepting proofs with precompiles. The local prover is making one that cannot pass transaction verification.

As to the test gap, the main prove and verify helper expects a complete proof, and every test that reaches it uses Falcon. The rejection test injects a dummy precompile proof. No test runs a real ECDSA transaction through LocalTransactionProver and TransactionVerifier together.

[PhilippGackstatter]

prove_partial_sync was removed in the latest version, but it looks like its replacement is FastProcessor::execute_for_proving_sync + Prover::prove. To close the issue, I would fix only the bug (see below for a larger refactor) by using these two APIs in LocalTransactionProver.

The bigger issue this creates is that ProposedBatch requires that tx proofs are complete, and this requirement makes sense. To execute the batch kernel, it will require a complete tx proof so it can verify it, so the proof must be complete by the time the batch is executed, and that is essentially what ProposedBatch::new represents on the Rust side.

We can prove precompiles during construction (in ProposedBatch::new following Deferred precompile workflow), but this creates two small issues in practice:

• If a tx is added to a batch multiple times (because a batch ultimately fails or reverts), the node would prove precompiles every time.
• The batch receives an Arc<ProvenTransaction> (eases integration in the node) and so it cannot complete the proof using ExecutionProof::complete, that is, it would need to clone the tx (bad).

One reasonable alternative is proving precompiles before the proposed batch is constructed, i.e. the node/batch builder would effectively have to do that when it receives a transaction. This means it does this exactly once (good). This might create a DoS risk, depending on how expensive precompile proving is if we do it too early (maybe bad). I could be missing additional pros/cons. cc @Mirko-von-Leipzig in case you have opinions.

Avoiding re-execution during proving

Afaict, the long-term goal is still to avoid re-execution during proving, right? We can create the ExecutionWitness during tx execution to avoid the re-execution in the prover step. The main issue here is that the ProgramExecutor abstraction only offers execute which returns ExecutionOutput, but not ExecutionWitness. From what I can tell, the options are:

• Introduce two versions of ExecutedTransaction where one contains an ExecutionWitness and the other doesn't (I would definitely avoid using Option<ExecutedWitness> to represent this) and add a separate API in the TransactionExecutor that returns an "ExecutedTransactionWithExecutionWitness",
• or always return an ExecutionWitness from ProgramExecutor::execute.

I don't like the first option as it makes the API more confusing ("there should be one, simple execute api"). Specifically, I find the current FastProcessor API confusing due to its many variants and I would like to avoid a similar situation on TransactionExecutor.
I'm not sure if the second option is practical though, given that this is also used for debugging, etc.

[Mirko-von-Leipzig]

I don't like the first option as it makes the API more confusing ("there should be one, simple execute api"). Specifically, I find the current FastProcessor API confusing due to its many variants and I would like to avoid a similar situation on TransactionExecutor.
I'm not sure if the second option is practical though, given that this is also used for debugging, etc.

iirc, debugging is opt-in?

One could use generics to do something like this:

struct TransactionExecutor<S = DebugDisabled> {
    ...
}

struct DebugDisabled;
struct DebugEnabled;

impl TransactionExecutor<DebugDisabled> {
    fn execute(...) -> Result<ExecutedTransaction> {...}

    fn with_debug_enabled(self) -> TransactionExecutor<DebugEnabled> {
        self
    } 
}

impl TransactionExecutor<DebugEnabled> {
    fn execute(...) -> Result<(ExecutedTransaction, ExecutionWitnesss) {...}
}

impl TransactionExecutor<S> {
    fn execute_inner(...) ...
}

though perhaps this is what you're hoping to avoid...

[PhilippGackstatter]

iirc, debugging is opt-in?

I think there is no processor-global debug flag anymore. It depends on whether the source and the debug info is available whether it is used.

What I meant was that I'm not sure if we can change the API to require returning an ExecutionWitness in all cases, specifically thinking about the compiler implementing a custom ProgramExecutor for debug purposes. Maybe this is an orthogonal concern, not sure.

[bobbinth]

The bigger issue this creates is that ProposedBatch requires that tx proofs are complete, and this requirement makes sense. To execute the batch kernel, it will require a complete tx proof so it can verify it, so the proof must be complete by the time the batch is executed, and that is essentially what ProposedBatch::new represents on the Rust side.

I don't think this is correct. Batch proving should work as follows:

• We pick $n$ proven transactions. For now, $n <= 4$ so that proving a batch takes roughly 1 second.
• For each transaction that has deferred precompile, we collect precompile witnesses and merge them into a single precompile witness.
• Then we generate a single precompile proof that covers all precompile witnesses.
• Lastly we run the batch kernel which, among other things, does the following:
  • Checks main VM proofs for each transaction. This outputs deferred precompile roots (when there are deferred precompiles).
  • Merges deferred precompile roots to get a single root.
  • Verifies the single precompile proof and makes sure it is consistent with the merged precompile roots.

So, the current check in the ProposedBatch that the proofs must be complete is incorrect. Maybe we should consider removing the ExecutionProof::is_complete() method because it is causing quite a bit of confusion and has been a source of several bugs so far. cc @Al-Kindi-0 and @adr1anh

We can prove precompiles during construction (in ProposedBatch::new following Deferred precompile workflow), but this creates two small issues in practice:

As mentioned above, we shouldn't be doing this in the ProposedBatch. Proposed batch constructor should make sure that the precompiles are consistent with the main VM proof (I believe we are doing this in the TransactionVerifier::verify() method) but the proving should happen when we construct a proven batch (i.e., in the batch prover). And as I mentioned above, we would be proving only a single precompile proof per batch - and this proof should cover deferred precompiles for all transactions.

Avoiding re-execution during proving

Not commenting on this for now - I think we have a separate issue for this, right? May be worth moving this part of the comment there.

[PhilippGackstatter]

Thanks, I wasn't aware that was possible with precompiles.

#3851 fixes the current bug.

For the follow-up of handling the precompiles in the batch, there are two options:

• Produce the single precompile proof in the BatchExecutor, verify it (maybe this step is superfluous given the same code produces the proof), and drop it. The batch kernel doesn't read it currently (recursive verification isn't implemented).
• Produce the single precompile proof in the BatchExecutor, propagate it through ExecutedBatch and ProvenBatch to be able to verify it using BatchVerifier.

The problem with the 2nd option is that we'd have to include the precompile proof in the gRPC format of ProvenBatch only to drop it once the batch kernel starts attesting to the validity of those precompile proofs. For that reason, I think it's not a good option.

The first option means, afaict, that the node in verify_batch_proof would need to execute the ProposedBatch to run precompile proof verification of user-submitted transactions, as verifying the ProvenBatch proof would not cover the precompiles. This is a subtle setup, but I think it's the better intermediate choice since it goes away once we have precompile-attesting batch proofs. Let me know if you think differently.

[bobbinth]

• Produce the single precompile proof in the BatchExecutor, verify it (maybe this step is superfluous given the same code produces the proof), and drop it. The batch kernel doesn't read it currently (recursive verification isn't implemented).
• Produce the single precompile proof in the BatchExecutor, propagate it through ExecutedBatch and ProvenBatch to be able to verify it using BatchVerifier.

Could we do the following?:

• In the BatchExecutor::execute():
  • Iterate over all transaction proofs of the proposed batch, extract all deferred precompile witnesses from them, and merge them into a single precompile witness. This would give us the witness needed to prove the single precompile proof for the entire batch.
  • Execute BatchKernel::main() (as we do now) and ensure that the resulting witness have no precompiles (either deferred or proven) - i.e., executing the batch kernel should never require precompiles.
  • Put the precompile witness into the ExecutedBatch.
• In the LocalBatchProver::prove():
  • Use the pre-compile witness to generate the precompile proof.
  • Use the batch kernel witness to generate the main VM proof.

The ExecutedBatch struct would then look something like:

pub struct ExecutedBatch {
    proposed_batch: ProposedBatch,
    vm_witness: VmWitness,
    precomile_witness: Option<PrecompileWitness>,
    batch_outputs: BatchOutputs,
}

This is not the final state though, because once the batch kernel has recursive proof verification of the precompile proof implemented, the flow would be something like this:

• In the BatchExecutor::execute()
  • Build the single precompile witness for all transactions in the batch.
  • Execute the batch kernel up until it needs to verify the precompile proof. If there are any precompiles, the batch kernel will error out at this point, but that's OK - we'll know that everything else worked. This would also mean that we won't have the main VM witness at this stage yet.
• In the LocalBatchProver::prove():
  • Use the pre-compile witness to generate the precompile proof.
  • Execute the batch kernel providing precompile proof as input into it - this generates the final main VM witness.
  • Use this witness to prove the batch kernel execution.

With this approach the ExecutedBatch would look like:

pub struct ExecutedBatch {
    proposed_batch: ProposedBatch,
    precomile_witness: Option<PrecompileWitness>,
    batch_outputs: BatchOutputs,
}

[Mirko-von-Leipzig]

Why is the precompile witness optional?

[bobbinth]

If none of the transactions use precompiles (e.g., all of them use Falcon signature) then there is no precompile witness.

[PhilippGackstatter]

Could we do the following?:
In the LocalBatchProver::prove():
* Execute the batch kernel providing precompile proof as input into it - this generates the final main VM witness.

Yes, I think that works, but it means we execute the batch kernel twice, and while that may not be the most expensive part, it still seems worth skipping that. Or at least I don't see why producing the precompile proofs before executing the MASM batch kernel is a problem, and this way we only need to execute the batch kernel once. With this we should be able to end up with the same approach of separating execution and proving (without re-execution) for tx, batch and block kernel (i.e. what #3852 proposes for tx kernel).

If the point is to delay precompile proving until the point where the proof is actually needed, we could also request it via an event from the "batch kernel host", but this is more or less the same as what I just described.

The main advantage of delaying the precompile proof generation to the LocalBatchProver I can think of is to do all the computationally expensive proving in one conceptual step (the proving phase). Whether that's necessary depends on whether the batch kernel executor is a different entity/machine from the batch kernel prover. I thought this all happens on the same (powerful) machine, but maybe that's a wrong assumption?

[bobbinth]

Or at least I don't see why producing the precompile proofs before executing the MASM batch kernel is a problem, and this way we only need to execute the batch kernel once.

It is not a problem and is actually what we have to do: precompile proof needs to be built before we can successfully execute the batch kernel. The main question is where that happens, and here, I think the most appropriate location is LocalBatchProver.

The setup that I have in mind is that there is a pool of LocalBatchProvers running on remote machines and the batch builder (in the sequencer) sends proof requests to them. So, the separation of tasks looks as follows:

• The sequencer, builds an ExecutedBatch. It does not have the necessary power to generate the proofs though.
• The sequencer then dispatches proof requests to the batch provers. There are two options here:
  • The sequencer dispatches individual proof requests - e.g., to generate precompile proof, and then to generate the batch proof.
  • The sequencer sends the ExecutedBatch to the provers and the provers handle both proofs internally.
• Once the proving are done, the sequencer outputs the ProvenBatch.

I think the main point here is that generating proofs in BatchExecutor::execute() is probably not something we'd want to do because this method is meant to be pretty light-weight and so, shouldn't require maintaining connections to remote provers etc. But, of course, we can re-think this if needed as well.