miden_ace_codegen/
encode.rs

1//! ACE circuit encoding for the chiplet format.
2//!
3//! Encoding rules:
4//! - The READ section stores extension-field (EF) elements; each EF occupies two base-field
5//!   elements.
6//! - Each ACE READ row consumes two EF elements (four base-field elements or a `Word`).
7//! - The EVAL section stores one operation per row, encoded as a single base-field element.
8//!
9//! The encoded stream concatenates constants (EF) followed by operations
10//! (base-field), then pads to an `adv_pipe` block boundary.
11
12use miden_core::{Felt, Word, crypto::hash::Poseidon2};
13use miden_crypto::field::ExtensionField;
14
15use crate::{
16    AceError,
17    circuit::{AceCircuit, AceNode, AceOp, AceOpNode},
18};
19
20// NOTE: `num_vars`/`num_const_nodes` count extension-field (EF) nodes, while the
21// instruction stream (`instructions.len()`) is measured in base field elements.
22
23/// Number of base field elements per extension field element.
24const BASE_FELTS_PER_EF: usize = crate::EXT_DEGREE;
25/// Number of EF nodes read per ACE READ row (two EF per row).
26const ACE_READ_ROW_EF_NODES: usize = 2;
27/// Constants are padded to an even number of EF nodes (full READ rows).
28const CONST_EF_ALIGN: usize = 2;
29/// Instruction stream padding unit in base felts (adv_pipe block size), so that
30/// the constants+ops stream can be read in aligned chunks.
31const ADV_PIPE_BLOCK_FELTS: usize = 8;
32
33/// Encoded ACE circuit ready for chiplet consumption.
34///
35/// This packs the circuit into the chiplet instruction stream and exposes
36/// helpers for stream sizing. `num_vars` counts extension-field nodes
37/// (inputs + constants + padding). `num_ops` and `num_eval_rows` count
38/// base-field operation rows (including padding ops).
39#[derive(Debug, Clone)]
40pub struct EncodedCircuit {
41    num_vars: usize,
42    num_ops: usize,
43    instructions: Vec<Felt>,
44}
45
46impl EncodedCircuit {
47    /// Number of ACE READ rows (two EF nodes per row).
48    pub fn num_read_rows(&self) -> usize {
49        self.num_vars() / ACE_READ_ROW_EF_NODES
50    }
51
52    /// Number of rows needed to evaluate operations (one op per base-field row).
53    pub fn num_eval_rows(&self) -> usize {
54        self.num_ops
55    }
56
57    /// Total number of variable slots (inputs + constants + padding), counted in EF nodes.
58    pub fn num_vars(&self) -> usize {
59        self.num_vars
60    }
61
62    /// Number of input slots in the READ section.
63    pub fn num_inputs(&self) -> usize {
64        self.num_vars - self.num_constants()
65    }
66
67    /// Number of constants encoded into the circuit stream, counted in EF nodes.
68    pub fn num_constants(&self) -> usize {
69        (self.instructions.len() - self.num_ops) / BASE_FELTS_PER_EF
70    }
71
72    /// Total number of nodes (inputs + constants + ops).
73    pub fn num_nodes(&self) -> usize {
74        self.num_vars + self.num_ops
75    }
76
77    /// Raw instruction stream (constants + ops).
78    pub fn instructions(&self) -> &[Felt] {
79        &self.instructions
80    }
81
82    /// Instruction stream length in base field elements.
83    pub fn size_in_felt(&self) -> usize {
84        self.instructions.len()
85    }
86
87    /// Poseidon2 digest of the instruction stream.
88    pub fn circuit_hash(&self) -> Word {
89        Poseidon2::hash_elements(self.instructions())
90    }
91}
92
93impl<EF> AceCircuit<EF>
94where
95    EF: ExtensionField<Felt>,
96{
97    /// Encode the circuit into the ACE chiplet format.
98    pub fn to_ace(&self) -> Result<EncodedCircuit, AceError> {
99        const MAX_NODE_ID: u64 = (1 << 30) - 1;
100
101        if !self.layout.total_inputs.is_multiple_of(ACE_READ_ROW_EF_NODES) {
102            return Err(AceError::InvalidInputLayout {
103                message: "ACE READ layout must be aligned to two EF nodes (use LayoutKind::Masm or pad inputs)"
104                    .to_string(),
105            });
106        }
107
108        let num_input_nodes = self.layout.total_inputs;
109        let num_const_nodes = self.constants.len().next_multiple_of(CONST_EF_ALIGN);
110        let num_op_nodes = self.operations.len();
111        if num_op_nodes == 0 {
112            return Err(AceError::InvalidInputLayout {
113                message: "ACE circuit has no operations to encode".to_string(),
114            });
115        }
116        if self.root != AceNode::Operation(num_op_nodes - 1) {
117            return Err(AceError::InvalidInputLayout {
118                message: "ACE circuit root must be the last operation before padding".to_string(),
119            });
120        }
121
122        // Constants are serialized as EF elements (2 base felts per EF).
123        let num_const_felts = num_const_nodes * BASE_FELTS_PER_EF;
124        let num_op_felts = num_op_nodes;
125        // The instruction stream is measured in base felts:
126        // - constants are EF-encoded (2 base felts each)
127        // - ops are 1 base felt each
128        let len_circuit = num_const_felts + num_op_felts;
129        let len_circuit_padded = len_circuit.next_multiple_of(ADV_PIPE_BLOCK_FELTS);
130
131        let num_padding_felts = len_circuit_padded - len_circuit;
132        let num_padding_nodes = num_padding_felts;
133        let num_nodes = num_input_nodes + num_const_nodes + num_op_nodes + num_padding_nodes;
134
135        if num_nodes as u64 > MAX_NODE_ID {
136            return Err(AceError::InvalidInputLayout {
137                message: format!("ACE circuit has {num_nodes} nodes, exceeds 2^30-1 limit"),
138            });
139        }
140
141        let mut instructions = Vec::with_capacity(len_circuit_padded);
142        for constant in &self.constants {
143            let coeffs = constant.as_basis_coefficients_slice();
144            instructions.push(coeffs[0]);
145            instructions.push(coeffs[1]);
146        }
147        instructions.resize(num_const_felts, Felt::ZERO);
148
149        let node_id = |node: AceNode| -> Result<u64, AceError> {
150            let input_start = num_nodes - 1;
151            let constants_start = input_start - num_input_nodes;
152            let ops_start = constants_start - num_const_nodes;
153
154            let id = match node {
155                AceNode::Input(idx) => input_start.checked_sub(idx),
156                AceNode::Constant(idx) => constants_start.checked_sub(idx),
157                AceNode::Operation(idx) => ops_start.checked_sub(idx),
158            }
159            .ok_or_else(|| AceError::InvalidInputLayout {
160                message: format!("ACE circuit node index out of range: {node:?}"),
161            })?;
162            Ok(id as u64)
163        };
164
165        let op_tag = |op: AceOp| -> u64 {
166            match op {
167                AceOp::Sub => 0,
168                AceOp::Mul => 1,
169                AceOp::Add => 2,
170            }
171        };
172
173        let encode_operation = |op: &AceOpNode| -> Result<Felt, AceError> {
174            // Pack as: lhs_id + rhs_id * 2^30 + op_tag * 2^60.
175            const RHS_NODE_OFFSET: u64 = 1 << 30;
176            const OP_TAG_OFFSET: u64 = 1 << 60;
177            let lhs_id = node_id(op.lhs)?;
178            let rhs_id = node_id(op.rhs)?;
179            let tag = op_tag(op.op);
180            Ok(Felt::new_unchecked(lhs_id + rhs_id * RHS_NODE_OFFSET + tag * OP_TAG_OFFSET))
181        };
182
183        for op in &self.operations {
184            instructions.push(encode_operation(op)?);
185        }
186
187        // The ACE chiplet checks the last EVAL row. Padding preserves zero-ness by repeatedly
188        // squaring the current root, so the unpadded root must be the last emitted operation.
189        let mut last_node_index = num_op_nodes - 1;
190        while instructions.len() < len_circuit_padded {
191            let last_node = AceNode::Operation(last_node_index);
192            let dummy_op = AceOpNode {
193                op: AceOp::Mul,
194                lhs: last_node,
195                rhs: last_node,
196            };
197            instructions.push(encode_operation(&dummy_op)?);
198            last_node_index += 1;
199        }
200
201        let num_vars = num_input_nodes + num_const_nodes;
202        let num_ops = num_op_nodes + num_padding_nodes;
203        Ok(EncodedCircuit { num_vars, num_ops, instructions })
204    }
205
206    /// Return true if inputs/constants/ops satisfy chiplet padding rules:
207    /// - inputs/constants are aligned to full READ rows (EF nodes)
208    /// - constants+ops stream is aligned to adv_pipe blocks (base felts)
209    pub fn is_padded(&self) -> bool {
210        if !self.layout.total_inputs.is_multiple_of(ACE_READ_ROW_EF_NODES) {
211            return false;
212        }
213        if !self.constants.len().is_multiple_of(CONST_EF_ALIGN) {
214            return false;
215        }
216        let const_felts = self.constants.len() * BASE_FELTS_PER_EF;
217        let op_felts = self.operations.len();
218        (const_felts + op_felts).is_multiple_of(ADV_PIPE_BLOCK_FELTS)
219    }
220}
miden_ace_codegen/encode.rs

miden_ace_codegen/
encode.rs
