Crate miden_ace_codegen 

ACE circuit codegen for Plonky3-based Miden AIRs.

The pipeline is:

1. Capture AIR constraints into the miden-constraint-compiler IR.
2. Lower the constraint graph into a DAG that mirrors verifier constraints evaluation.
3. Emit an ACE circuit plus an InputLayout describing the MASM ACE-READ section order.

The resulting circuit is intended to run inside the recursive verifier. All input layout decisions (point-major OOD ordering, aux/quotient coords, and alpha/beta randomness expansion) are centralized in this crate so tests can validate both layout and evaluation.

Quick start:

use miden_ace_codegen::{AceConfig, LayoutKind, build_ace_circuit_for_air};
use miden_air::ChipletsAir;

let config = AceConfig { num_quotient_chunks: 8, layout: LayoutKind::Masm, num_airs: 1 };
let circuit = build_ace_circuit_for_air(&ChipletsAir, config)?;

Module map (data flow):

• pipeline: public entry points that orchestrate layout + DAG + circuit emission.
• dag: verifier-style DAG IR and lowering helpers.
• circuit: off-VM circuit representation (inputs/constants/ops/root).
• factored: shuffle/common split of a multi-AIR circuit, so per-proof-order variants share one order-invariant section (used by the recursive verifier’s circuit registry).
• factory: cached per-order encoding and registry-leaf construction.
• layout: READ-section layout and index mapping.
• encode: ACE stream encoding + padding rules.
• masm: shared renderer for relation-local MASM constraint evaluators.
• randomness: challenge input planning for layouts + DAG lowering.
• quotient: barycentric quotient recomposition helpers (used by DAG + tests).
• registry: order tags, registry layout, subtree construction, and path authentication.

Structs

AceArtifacts

Output of the ACE codegen pipeline.

AceCircuit

Emitted ACE circuit with layout and operation list.

AceConfig

Configuration for building an ACE DAG and its input layout.

AceDag

A built DAG with a designated root.

DagBuilder

A hash-consed DAG builder.

DagSnapshot

Exported DAG data that preserves the source DAG id across imports.

EncodedCircuit

Encoded ACE circuit ready for chiplet consumption.

FactoredCircuitFactory

Factory caching the order-invariant parts of a factored multi-AIR composition.

FactoredEncodedCircuit

One proof order’s encoded circuit plus its stream-segment commitments.

FactoredMultiAirCircuit

Multi-AIR ACE circuit factored into a per-order shuffle section and an order-invariant common section.

InputCounts

Counts needed to build the ACE input layout.

InputLayout

ACE input layout for circuit evaluation.

MasmConstraintsEvalConfig

Relation-specific inputs to the shared MASM constraint-evaluator renderer.

NodeId

Identifier for a node in the DAG.

PackedLeafScratch

Reusable scratch for FactoredCircuitFactory::leaves_for_orders.

RegistryLayout

Shape of a registry: how many orderings it covers and where its checked-in node row sits.

ShuffleEncodeBuffer

Reusable scratch for FactoredMultiAirCircuit::encode_shuffle_section_for_order.

Enums

AceError

Errors returned by ACE codegen.

InputKey

Logical inputs required by the ACE circuit.

LayoutKind

Layout strategy for arranging ACE inputs.

NodeKind

Node kinds in the DAG.

Constants

EXT_DEGREE

Extension field degree (quadratic extension for Miden VM).

MAX_REGISTRY_AIRS

Largest AIR count whose complete permutation set fits in the u32 registry-tag space.

Functions

build_ace_circuit_for_air

Build a verifier-equivalent ACE circuit for the provided AIR.

build_ace_dag_for_air

Build a verifier-equivalent DAG and layout for the provided AIR.

build_factored_multi_air_ace_circuit

Factored variant of build_multi_air_ace_circuit.

build_multi_air_ace_circuit

Build one ACE circuit for several AIR instances.

ceil_log2

Return the smallest d such that 2^d >= value.

emit_circuit

Emit an ACE circuit from the DAG and input layout.

factorial

Compute n!.

fold_row_to_root

Fold a node row up to the tree root.

order_from_tag

Decode a registry tag into its proof ordering over num_airs AIRs.

order_tag

Registry tag of a proof ordering: its Lehmer rank relative to the canonical (identity) instance order.

padding_leaf

Leaf value for registry slots that no proof ordering maps to.

path_in_verified_tree

Splice the authentication path for tag from its recomputed subtree and the verified pyramid above the row.

render_masm_constraints_eval

Render the MASM wrapper that prepares ACE inputs, authenticates the selected circuit, and executes it.

subtree_leaves

Compute the leaves of one row node’s subtree, in slot order.

verify_row

Hash a checked-in node row upward and authenticate it against the registry root.