Add the factored precompile VM ACE registry - #3465
Conversation
9cc7966 to
8b8c952
Compare
8b8c952 to
eabf90f
Compare
|
This PR contains unsigned commits. All commits must be cryptographically signed (GPG or SSH). Unsigned commits:
For instructions on setting up commit signing and re-signing existing commits, see: |
- 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
eabf90f to
eb05168
Compare
| /// Add a subtraction node with constant folding, add/sub cancellation, and negation | ||
| /// normalization. | ||
| pub fn sub(&mut self, a: NodeId, b: NodeId) -> NodeId { |
There was a problem hiding this comment.
One issue with the new DagBuilder::sub handling is that now the unreachable path in reemit_air_root is no longer unreachable I believe (DagBuilder::sub can return a non-Sub node via the new cancel_sub / negated)
There was a problem hiding this comment.
It's still unreachable, though the argument deserved to be written down and it now lives at the call site. The root's right operand is the freshly interned Mul(q, v) over the quotient inputs, which no node built from the AIR constraints can reference or equal. Every non-Sub return in DagBuilder::sub — the cancel_sub branches and the negation rewrites — requires exactly such a relation to the right operand, and sub has no left-operand rewrites, so none of the new simplifications can fire on this root.
There's also a unit test now pinning the no-left-rewrite half, which is the part a future rewrite could silently erode.
| let registry_tree = config::ace_circuit_registry_tree(); | ||
| store.extend(registry_tree.inner_nodes()); | ||
| extend_ace_registry_store(&mut store, proof_order)?; | ||
|
|
||
| let circuit = build_recursive_verifier_ace_circuit(proof_order).map_err(|_| { |
There was a problem hiding this comment.
Aren't we computing the ACE twice? i.e. once in ace_registry_path (within extend_ace_registry_store) then in build_recursive_verifier_ace_circuit?
There was a problem hiding this comment.
I think it's even worse with no-std builds as we don't do caching
There was a problem hiding this comment.
Indeed, the entry was minted twice and things are fixed now so that call sites now collapse into a single recursive_registry_entry(order) that serves circuit, leaf, and path from one factory.
On std vs no-std: under std the factory and the registry tree sit behind OnceLocks, so everything is computed once per process. Under no-std the entry is still built per call, though now it's one factory serving both outputs instead of two independent computations. We could cache there too via miden-utils-sync's racy statics, but that adds a dependency edge and pins the factory and tree in memory for the process lifetime, which only pays off for a consumer that verifies repeatedly in one process. If such a no-std consumer shows up, wiring the same cache through utils-sync is a small follow-up.
| pub fn pvm_ace_registry_path(tag: u32) -> Option<(Word, MerklePath)> { | ||
| if (tag as usize) >= PVM_REGISTRY_LAYOUT.leaf_count() { | ||
| return None; | ||
| } | ||
| let subtree_index = tag as usize / PVM_REGISTRY_LAYOUT.subtree_leaves(); | ||
| let leaves = leaves_for_subtree(subtree_index); | ||
| let subtree = MerkleTree::new(&leaves).expect("subtree has power-of-two leaves"); | ||
| Some( | ||
| path_in_verified_tree( | ||
| &PVM_REGISTRY_LAYOUT, | ||
| verified_pyramid(), | ||
| &subtree, | ||
| tag, | ||
| MISMATCH_HINT, | ||
| ) | ||
| .expect("bounded tag and verified pyramid must produce a registry path"), | ||
| ) | ||
| } |
There was a problem hiding this comment.
We're recomputing the subtree on every lookup, couldn't we amortize that?
There was a problem hiding this comment.
Good catch. Leaves are now cached in per-subtree OnceLocks.
Caching leaves is better because this is where most of the cost lives and it allows us to get away with less memory pressure.
- build MVM circuits and authentication paths from one shared factory - cache PVM active-subtree leaves and share the padding allocation - enforce registry-entry coherence and harden DAG and packed-hash invariants
2 participants
The recursive verifier must use the ACE circuit matching the proof's height-sorted AIR order. With ten AIRs there are
10! = 3,628,800valid orders, so checking in every circuit commitment or rebuilding the complete registry for each proof is impractical.This PR makes the registry compact to store and cheap to serve while retaining exhaustive checks over every proof order.
How it works
Each ACE circuit is split into a short order-dependent prefix and a larger common section:
The factory builds the common circuit once, caches its commitment and the sponge state after the constants, and then emits only the shuffle section for each order. When a protocol change requires minting a new registry from scratch, this reduces the offline leaf-and-root construction phase from 169 seconds with per-order assembly to 58 seconds with the factored encoder (2.9x). Packed hashing and the final two-tier layout reduce that phase further to 37.6 seconds on M4 NEON. None of this full-registry work is performed at process startup or while serving a proof.
The complete tree has
2^22slots. Instead of checking in its 3.6 million active leaves, the repository stores 4,096 authenticated subtree roots. The complete registry is rebuilt only by the maintenance tool; normal proof serving never performs that work. A serving process authenticates the checked-in row and builds the circuit factory once, then reconstructs only the selected 1,024-leaf subtree for each proof.The regeneration tool has two roles:
--checkrecomputes the complete registry, checks the fast shuffle encoding against full circuit assembly for every order, and compares the result with the checked-in artifacts.--writeis the rarer minting path. Before replacing protocol constants, it compares every packed leaf with the scalar commitment obtained from fully assembling that order's circuit.The Miden VM registry moves to the same factored commitment format. Registry roots and relation digests change, so recursive-proof artifacts created with the previous format are incompatible.
Factoring adds an order-dependent shuffle section. This PR also applies a conservative DAG normalization pass that retains only circuit-shrinking rewrites while preserving evaluation. The net size change at this branch tip is:
Unlike full-registry minting, this extra work is paid when a recursive verifier loads and evaluates the circuit. If end-to-end profiling shows that cost is material, a follow-up can retain the two-tier registry while investigating unfactored per-order circuits and a different strategy for constructing or serving their authenticated subtrees.
Performance
All figures below use release mode on M4 NEON. The full-registry figures are offline maintenance costs, not per-proof costs:
concurrent. The default single-threadedstdpath takes 106.0 ms warm.Circuit generation and validation dominate these measurements. Building the Merkle subtrees is less than 1% of the full construction cost.