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, 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    // Ensure vars and instructions are word-aligned and non-empty. Note that variables are
68    // quadratic extension field elements while instructions are encoded as base field elements.
69    // Hence we can pack 2 variables and 4 instructions per word.
70    if num_vars % 2 != 0 || num_vars == 0 {
71        return Err(ExecutionError::failed_arithmetic_evaluation(
72            error_ctx,
73            AceError::NumVarIsNotWordAlignedOrIsEmpty(num_vars),
74        ));
75    }
76    if num_eval % 4 != 0 || num_eval == 0 {
77        return Err(ExecutionError::failed_arithmetic_evaluation(
78            error_ctx,
79            AceError::NumEvalIsNotWordAlignedOrIsEmpty(num_eval),
80        ));
81    }
82
83    // Ensure instructions are word-aligned and non-empty
84    let num_read_rows = num_vars as u32 / 2;
85    let num_eval_rows = num_eval as u32;
86
87    let mut evaluation_context =
88        CircuitEvaluation::new(ctx, clk + op_idx, num_read_rows, num_eval_rows);
89
90    let mut ptr = ptr;
91    // perform READ operations
92    for _ in 0..num_read_rows {
93        let word = mem.read_word(ctx, ptr, clk + op_idx)?;
94        evaluation_context.do_read(ptr, *word)?;
95        ptr += PTR_OFFSET_WORD;
96    }
97    // perform EVAL operations
98    for _ in 0..num_eval_rows {
99        let instruction = mem.read_element(ctx, ptr)?;
100        evaluation_context.do_eval(ptr, instruction, error_ctx)?;
101        ptr += PTR_OFFSET_ELEM;
102    }
103
104    // Ensure the circuit evaluated to zero.
105    if !evaluation_context.output_value().is_some_and(|eval| eval == QuadFelt::ZERO) {
106        return Err(ExecutionError::failed_arithmetic_evaluation(
107            error_ctx,
108            AceError::CircuitNotEvaluateZero,
109        ));
110    }
111
112    Ok(evaluation_context)
113}