miden_processor/fast/
circuit_eval.rs

1use miden_air::RowIndex;
2use vm_core::{Felt, FieldElement, mast::BasicBlockNode};
3
4use super::{FastProcessor, memory::Memory};
5use crate::{
6    ContextId, ExecutionError, QuadFelt,
7    chiplets::{CircuitEvaluation, MAX_NUM_ACE_WIRES, PTR_OFFSET_ELEM, PTR_OFFSET_WORD},
8    errors::{AceError, ErrorContext},
9};
10
11impl FastProcessor {
12    /// Checks that the evaluation of an arithmetic circuit is equal to zero.
13    ///
14    /// The inputs are composed of:
15    ///
16    /// 1. a pointer to the memory region containing the arithmetic circuit description, which
17    ///    itself is arranged as:
18    ///
19    ///    a. `Read` section:
20    ///       1. Inputs to the circuit which are elements in the quadratic extension field,
21    ///       2. Constants of the circuit which are elements in the quadratic extension field,
22    ///
23    ///    b. `Eval` section, which contains the encodings of the evaluation gates of the circuit.
24    ///    Each gate is encoded as a single base field element.
25    /// 2. the number of rows in the `READ` section,
26    /// 3. the number of rows in the `EVAL` section,
27    ///
28    /// Stack transition:
29    /// [ptr, num_read_rows, num_eval_rows, ...] -> [ptr, num_read_rows, num_eval_rows, ...]
30    pub fn arithmetic_circuit_eval(&mut self, op_idx: usize) -> Result<(), ExecutionError> {
31        let num_eval_rows = self.stack_get(2);
32        let num_read_rows = self.stack_get(1);
33        let ptr = self.stack_get(0);
34        let ctx = self.ctx;
35        let clk = self.clk;
36        let circuit_evaluation = eval_circuit_fast_(
37            ctx,
38            ptr,
39            clk,
40            num_read_rows,
41            num_eval_rows,
42            &mut self.memory,
43            op_idx,
44            &ErrorContext::default(),
45        )?;
46        self.ace.add_circuit_evaluation(clk, circuit_evaluation);
47
48        Ok(())
49    }
50}
51
52/// Identical to `[chiplets::ace::eval_circuit]` but adapted for use with `[FastProcessor]`.
53#[allow(clippy::too_many_arguments)]
54pub fn eval_circuit_fast_(
55    ctx: ContextId,
56    ptr: Felt,
57    clk: RowIndex,
58    num_vars: Felt,
59    num_eval: Felt,
60    mem: &mut Memory,
61    op_idx: usize,
62    error_ctx: &ErrorContext<'_, BasicBlockNode>,
63) -> Result<CircuitEvaluation, ExecutionError> {
64    let num_vars = num_vars.as_int();
65    let num_eval = num_eval.as_int();
66
67    let num_wires = num_vars + num_eval;
68    if num_wires > MAX_NUM_ACE_WIRES as u64 {
69        return Err(ExecutionError::failed_arithmetic_evaluation(
70            error_ctx,
71            AceError::TooManyWires(num_wires),
72        ));
73    }
74
75    // Ensure vars and instructions are word-aligned and non-empty. Note that variables are
76    // quadratic extension field elements while instructions are encoded as base field elements.
77    // Hence we can pack 2 variables and 4 instructions per word.
78    if num_vars % 2 != 0 || num_vars == 0 {
79        return Err(ExecutionError::failed_arithmetic_evaluation(
80            error_ctx,
81            AceError::NumVarIsNotWordAlignedOrIsEmpty(num_vars),
82        ));
83    }
84    if num_eval % 4 != 0 || num_eval == 0 {
85        return Err(ExecutionError::failed_arithmetic_evaluation(
86            error_ctx,
87            AceError::NumEvalIsNotWordAlignedOrIsEmpty(num_eval),
88        ));
89    }
90
91    // Ensure instructions are word-aligned and non-empty
92    let num_read_rows = num_vars as u32 / 2;
93    let num_eval_rows = num_eval as u32;
94
95    let mut evaluation_context =
96        CircuitEvaluation::new(ctx, clk + op_idx, num_read_rows, num_eval_rows);
97
98    let mut ptr = ptr;
99    // perform READ operations
100    for _ in 0..num_read_rows {
101        let word = mem.read_word(ctx, ptr, clk + op_idx)?;
102        evaluation_context.do_read(ptr, *word)?;
103        ptr += PTR_OFFSET_WORD;
104    }
105    // perform EVAL operations
106    for _ in 0..num_eval_rows {
107        let instruction = mem.read_element(ctx, ptr)?;
108        evaluation_context.do_eval(ptr, instruction, error_ctx)?;
109        ptr += PTR_OFFSET_ELEM;
110    }
111
112    // Ensure the circuit evaluated to zero.
113    if !evaluation_context.output_value().is_some_and(|eval| eval == QuadFelt::ZERO) {
114        return Err(ExecutionError::failed_arithmetic_evaluation(
115            error_ctx,
116            AceError::CircuitNotEvaluateZero,
117        ));
118    }
119
120    Ok(evaluation_context)
121}