openvm_ecc_circuit/weierstrass_chip/
add_ne.rs

1use std::{cell::RefCell, rc::Rc};
2
3use openvm_circuit_primitives::var_range::VariableRangeCheckerBus;
4use openvm_mod_circuit_builder::{ExprBuilder, ExprBuilderConfig, FieldExpr};
5
6// Assumes that (x1, y1), (x2, y2) both lie on the curve and are not the identity point.
7// Further assumes that x1, x2 are not equal in the coordinate field.
8pub fn ec_add_ne_expr(
9    config: ExprBuilderConfig, // The coordinate field.
10    range_bus: VariableRangeCheckerBus,
11) -> FieldExpr {
12    config.check_valid();
13    let builder = ExprBuilder::new(config, range_bus.range_max_bits);
14    let builder = Rc::new(RefCell::new(builder));
15
16    let x1 = ExprBuilder::new_input(builder.clone());
17    let y1 = ExprBuilder::new_input(builder.clone());
18    let x2 = ExprBuilder::new_input(builder.clone());
19    let y2 = ExprBuilder::new_input(builder.clone());
20    let mut lambda = (y2 - y1.clone()) / (x2.clone() - x1.clone());
21    let mut x3 = lambda.square() - x1.clone() - x2;
22    x3.save_output();
23    let mut y3 = lambda * (x1 - x3.clone()) - y1;
24    y3.save_output();
25
26    let builder = builder.borrow().clone();
27    FieldExpr::new(builder, range_bus, true)
28}