miden_processor/fast/
circuit_eval.rs

1use miden_air::RowIndex;
2use miden_core::{Felt, FieldElement, QuadFelt};
3
4use super::{FastProcessor, memory::Memory};
5use crate::{
6    ContextId, ExecutionError,
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(
31        &mut self,
32        op_idx: usize,
33        err_ctx: &impl ErrorContext,
34    ) -> Result<(), ExecutionError> {
35        let num_eval_rows = self.stack_get(2);
36        let num_read_rows = self.stack_get(1);
37        let ptr = self.stack_get(0);
38        let ctx = self.ctx;
39        let clk = self.clk;
40        let circuit_evaluation = eval_circuit_fast_(
41            ctx,
42            ptr,
43            clk,
44            num_read_rows,
45            num_eval_rows,
46            &mut self.memory,
47            op_idx,
48            err_ctx,
49        )?;
50        self.ace.add_circuit_evaluation(clk, circuit_evaluation);
51
52        Ok(())
53    }
54}
55
56/// Identical to `[chiplets::ace::eval_circuit]` but adapted for use with `[FastProcessor]`.
57#[allow(clippy::too_many_arguments)]
58pub fn eval_circuit_fast_(
59    ctx: ContextId,
60    ptr: Felt,
61    clk: RowIndex,
62    num_vars: Felt,
63    num_eval: Felt,
64    mem: &mut Memory,
65    op_idx: usize,
66    err_ctx: &impl ErrorContext,
67) -> Result<CircuitEvaluation, ExecutionError> {
68    let num_vars = num_vars.as_int();
69    let num_eval = num_eval.as_int();
70
71    let num_wires = num_vars + num_eval;
72    if num_wires > MAX_NUM_ACE_WIRES as u64 {
73        return Err(ExecutionError::failed_arithmetic_evaluation(
74            err_ctx,
75            AceError::TooManyWires(num_wires),
76        ));
77    }
78
79    // Ensure vars and instructions are word-aligned and non-empty. Note that variables are
80    // quadratic extension field elements while instructions are encoded as base field elements.
81    // Hence we can pack 2 variables and 4 instructions per word.
82    if num_vars % 2 != 0 || num_vars == 0 {
83        return Err(ExecutionError::failed_arithmetic_evaluation(
84            err_ctx,
85            AceError::NumVarIsNotWordAlignedOrIsEmpty(num_vars),
86        ));
87    }
88    if num_eval % 4 != 0 || num_eval == 0 {
89        return Err(ExecutionError::failed_arithmetic_evaluation(
90            err_ctx,
91            AceError::NumEvalIsNotWordAlignedOrIsEmpty(num_eval),
92        ));
93    }
94
95    // Ensure instructions are word-aligned and non-empty
96    let num_read_rows = num_vars as u32 / 2;
97    let num_eval_rows = num_eval as u32;
98
99    let mut evaluation_context =
100        CircuitEvaluation::new(ctx, clk + op_idx, num_read_rows, num_eval_rows);
101
102    let mut ptr = ptr;
103    // perform READ operations
104    for _ in 0..num_read_rows {
105        let word = mem
106            .read_word(ctx, ptr, clk + op_idx, err_ctx)
107            .map_err(ExecutionError::MemoryError)?;
108        evaluation_context.do_read(ptr, word)?;
109        ptr += PTR_OFFSET_WORD;
110    }
111    // perform EVAL operations
112    for _ in 0..num_eval_rows {
113        let instruction =
114            mem.read_element(ctx, ptr, err_ctx).map_err(ExecutionError::MemoryError)?;
115        evaluation_context.do_eval(ptr, instruction, err_ctx)?;
116        ptr += PTR_OFFSET_ELEM;
117    }
118
119    // Ensure the circuit evaluated to zero.
120    if !evaluation_context.output_value().is_some_and(|eval| eval == QuadFelt::ZERO) {
121        return Err(ExecutionError::failed_arithmetic_evaluation(
122            err_ctx,
123            AceError::CircuitNotEvaluateZero,
124        ));
125    }
126
127    Ok(evaluation_context)
128}
miden_processor/fast/circuit_eval.rs

miden_processor/fast/
circuit_eval.rs
