openvm_algebra_circuit/modular_chip/
addsub.rs

1use std::{cell::RefCell, rc::Rc};
2
3use openvm_algebra_transpiler::Rv32ModularArithmeticOpcode;
4use openvm_circuit::{
5    arch::ExecutionBridge,
6    system::memory::{offline_checker::MemoryBridge, SharedMemoryHelper},
7};
8use openvm_circuit_primitives::{
9    bitwise_op_lookup::{BitwiseOperationLookupBus, SharedBitwiseOperationLookupChip},
10    var_range::{SharedVariableRangeCheckerChip, VariableRangeCheckerBus},
11};
12use openvm_instructions::riscv::RV32_CELL_BITS;
13use openvm_mod_circuit_builder::{
14    ExprBuilder, ExprBuilderConfig, FieldExpr, FieldExpressionCoreAir, FieldExpressionExecutor,
15    FieldExpressionFiller, FieldVariable,
16};
17use openvm_rv32_adapters::{
18    Rv32VecHeapAdapterAir, Rv32VecHeapAdapterExecutor, Rv32VecHeapAdapterFiller,
19};
20
21use super::{ModularAir, ModularChip, ModularExecutor};
22use crate::FieldExprVecHeapExecutor;
23
24pub fn addsub_expr(
25    config: ExprBuilderConfig,
26    range_bus: VariableRangeCheckerBus,
27) -> (FieldExpr, usize, usize) {
28    config.check_valid();
29    let builder = ExprBuilder::new(config, range_bus.range_max_bits);
30    let builder = Rc::new(RefCell::new(builder));
31
32    let x1 = ExprBuilder::new_input(builder.clone());
33    let x2 = ExprBuilder::new_input(builder.clone());
34    let x3 = x1.clone() + x2.clone();
35    let x4 = x1.clone() - x2.clone();
36    let is_add_flag = (*builder).borrow_mut().new_flag();
37    let is_sub_flag = (*builder).borrow_mut().new_flag();
38    let x5 = FieldVariable::select(is_sub_flag, &x4, &x1);
39    let mut x6 = FieldVariable::select(is_add_flag, &x3, &x5);
40    x6.save_output();
41    let builder = (*builder).borrow().clone();
42
43    (
44        FieldExpr::new(builder, range_bus, true),
45        is_add_flag,
46        is_sub_flag,
47    )
48}
49
50fn gen_base_expr(
51    config: ExprBuilderConfig,
52    range_checker_bus: VariableRangeCheckerBus,
53) -> (FieldExpr, Vec<usize>, Vec<usize>) {
54    let (expr, is_add_flag, is_sub_flag) = addsub_expr(config, range_checker_bus);
55
56    let local_opcode_idx = vec![
57        Rv32ModularArithmeticOpcode::ADD as usize,
58        Rv32ModularArithmeticOpcode::SUB as usize,
59        Rv32ModularArithmeticOpcode::SETUP_ADDSUB as usize,
60    ];
61    let opcode_flag_idx = vec![is_add_flag, is_sub_flag];
62
63    (expr, local_opcode_idx, opcode_flag_idx)
64}
65
66pub fn get_modular_addsub_air<const BLOCKS: usize, const BLOCK_SIZE: usize>(
67    exec_bridge: ExecutionBridge,
68    mem_bridge: MemoryBridge,
69    config: ExprBuilderConfig,
70    range_checker_bus: VariableRangeCheckerBus,
71    bitwise_lookup_bus: BitwiseOperationLookupBus,
72    pointer_max_bits: usize,
73    offset: usize,
74) -> ModularAir<BLOCKS, BLOCK_SIZE> {
75    let (expr, local_opcode_idx, opcode_flag_idx) = gen_base_expr(config, range_checker_bus);
76    ModularAir::new(
77        Rv32VecHeapAdapterAir::new(
78            exec_bridge,
79            mem_bridge,
80            bitwise_lookup_bus,
81            pointer_max_bits,
82        ),
83        FieldExpressionCoreAir::new(expr, offset, local_opcode_idx, opcode_flag_idx),
84    )
85}
86
87pub fn get_modular_addsub_step<const BLOCKS: usize, const BLOCK_SIZE: usize>(
88    config: ExprBuilderConfig,
89    range_checker_bus: VariableRangeCheckerBus,
90    pointer_max_bits: usize,
91    offset: usize,
92) -> ModularExecutor<BLOCKS, BLOCK_SIZE> {
93    let (expr, local_opcode_idx, opcode_flag_idx) = gen_base_expr(config, range_checker_bus);
94
95    FieldExprVecHeapExecutor(FieldExpressionExecutor::new(
96        Rv32VecHeapAdapterExecutor::new(pointer_max_bits),
97        expr,
98        offset,
99        local_opcode_idx,
100        opcode_flag_idx,
101        "ModularAddSub",
102    ))
103}
104
105pub fn get_modular_addsub_chip<F, const BLOCKS: usize, const BLOCK_SIZE: usize>(
106    config: ExprBuilderConfig,
107    mem_helper: SharedMemoryHelper<F>,
108    range_checker: SharedVariableRangeCheckerChip,
109    bitwise_lookup_chip: SharedBitwiseOperationLookupChip<RV32_CELL_BITS>,
110    pointer_max_bits: usize,
111) -> ModularChip<F, BLOCKS, BLOCK_SIZE> {
112    let (expr, local_opcode_idx, opcode_flag_idx) = gen_base_expr(config, range_checker.bus());
113    ModularChip::new(
114        FieldExpressionFiller::new(
115            Rv32VecHeapAdapterFiller::new(pointer_max_bits, bitwise_lookup_chip),
116            expr,
117            local_opcode_idx,
118            opcode_flag_idx,
119            range_checker,
120            false,
121        ),
122        mem_helper,
123    )
124}