openvm_algebra_circuit/modular_chip/
addsub.rs1use 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}