chore: ec addition for non-zero points (#5858)

# Description

## Problem\*

This PR performs 'safe' ec addition in Noir, assuming the EC ADD opcode
is unsafe, i.e it does not handle point at infinity.

an ec addition for the embedded curve dedicated to non-zero inputs.



## Summary\*
embedded_curve_add in stdlib now handles corner cases for ec addition
Add 2 methods:
embedded_curve_add_not_nul which assumes the inputs are not null
embedded_curve_add_unsafe which assumes inputs are not null and distinct
(or identical)

Enable the constant inputs for ec_add.


## Additional Context
This PR should cause an overhead, because corner cases are not checked
in Noir and in BB. However, we want to change BB so that EC ADD is not
safe anymore which will improve the performance, so we need to add the
safe version in Noir first.

I am not sure whether we want to document this or not?


## Documentation\*

Check one:
- [X] No documentation needed.
- [ ] Documentation included in this PR.
- [ ] **[For Experimental Features]** Documentation to be submitted in a
separate PR.

# PR Checklist\*

- [X] I have tested the changes locally.
- [X] I have formatted the changes with [Prettier](https://prettier.io/)
and/or `cargo fmt` on default settings.

acvm-repo/acir/src/circuit/black_box_functions.rs

@@ -164,7 +164,15 @@ pub enum BlackBoxFunc {
     /// ultimately fail.
     RecursiveAggregation,
 
-    /// Addition over the embedded curve on which the witness is defined.
+    /// Addition over the embedded curve on which the witness is defined
+    /// The opcode makes the following assumptions but does not enforce them because
+    /// it is more efficient to do it only when required. For instance, adding two
+    /// points that are on the curve it guarantee to give a point on the curve.
+    ///
+    /// It assumes that the points are on the curve.
+    /// If the inputs are the same witnesses index, it will perform a doubling,
+    /// If not, it assumes that the points' x-coordinates are not equal.
+    /// It also assumes neither point is the infinity point.
     EmbeddedCurveAdd,
 
     /// BigInt addition

compiler/noirc_evaluator/src/ssa/acir_gen/acir_ir/acir_variable.rs

@@ -1471,6 +1471,7 @@ impl<F: AcirField> AcirContext<F> {
                 | BlackBoxFunc::AND
                 | BlackBoxFunc::XOR
                 | BlackBoxFunc::AES128Encrypt
+                | BlackBoxFunc::EmbeddedCurveAdd
         );
         // Convert `AcirVar` to `FunctionInput`
         let inputs = self.prepare_inputs_for_black_box_func_call(inputs, allow_constant_inputs)?;

noir_stdlib/src/embedded_curve_ops.nr

@@ -125,20 +125,63 @@ pub fn fixed_base_scalar_mul(scalar: EmbeddedCurveScalar) -> EmbeddedCurvePoint
     multi_scalar_mul([g1], [scalar])
 }
 
-// This is a hack as returning an `EmbeddedCurvePoint` from a foreign function in brillig returns a [BrilligVariable::SingleAddr; 2] rather than BrilligVariable::BrilligArray
+/// This function only assumes that the points are on the curve
+/// It handles corner cases around the infinity point causing some overhead compared to embedded_curve_add_not_nul and embedded_curve_add_unsafe
+// This is a hack because returning an `EmbeddedCurvePoint` from a foreign function in brillig returns a [BrilligVariable::SingleAddr; 2] rather than BrilligVariable::BrilligArray
 // as is defined in the brillig bytecode format. This is a workaround which allows us to fix this without modifying the serialization format.
 // docs:start:embedded_curve_add
-fn embedded_curve_add(
-    point1: EmbeddedCurvePoint,
-    point2: EmbeddedCurvePoint
-) -> EmbeddedCurvePoint
-// docs:end:embedded_curve_add
-{
-    let point_array = embedded_curve_add_array_return(point1, point2);
-    let x = point_array[0];
-    let y = point_array[1];
-    EmbeddedCurvePoint { x, y, is_infinite: point_array[2] == 1 }
+pub fn embedded_curve_add(point1: EmbeddedCurvePoint, point2: EmbeddedCurvePoint) -> EmbeddedCurvePoint {
+    // docs:end:embedded_curve_add
+    let x_coordinates_match = point1.x == point2.x;
+    let y_coordinates_match = point1.y == point2.y;
+    let double_predicate = (x_coordinates_match & y_coordinates_match);
+    let infinity_predicate = (x_coordinates_match & !y_coordinates_match);
+    let point1_1 = EmbeddedCurvePoint { x: point1.x + (x_coordinates_match as Field), y: point1.y, is_infinite: x_coordinates_match };
+    // point1_1 is guaranteed to have a different abscissa than point2
+    let mut result = embedded_curve_add_unsafe(point1_1, point2);
+    result.is_infinite = x_coordinates_match;
+
+    // dbl if x_match, y_match
+    let double = embedded_curve_add_unsafe(point1, point1);
+    result = if double_predicate { double } else { result };
+
+    // infinity if x_match, !y_match
+    if point1.is_infinite {
+        result= point2;
+    }
+    if point2.is_infinite {
+        result = point1;
+    }
+    let mut result_is_infinity = infinity_predicate & (!point1.is_infinite & !point2.is_infinite);
+    result.is_infinite = result_is_infinity | (point1.is_infinite & point2.is_infinite);
+    result
 }
 
 #[foreign(embedded_curve_add)]
 fn embedded_curve_add_array_return(_point1: EmbeddedCurvePoint, _point2: EmbeddedCurvePoint) -> [Field; 3] {}
+
+/// This function assumes that:
+/// The points are on the curve, and
+/// The points don't share an x-coordinate, and
+/// Neither point is the infinity point.
+/// If it is used with correct input, the function ensures the correct non-zero result is returned.
+/// Except for points on the curve, the other assumptions are checked by the function. It will cause assertion failure if they are not respected.
+pub fn embedded_curve_add_not_nul(point1: EmbeddedCurvePoint, point2: EmbeddedCurvePoint) -> EmbeddedCurvePoint {
+    assert(point1.x != point2.x);
+    assert(!point1.is_infinite);
+    assert(!point2.is_infinite);
+    embedded_curve_add_unsafe(point1, point2)
+}
+
+/// Unsafe ec addition
+/// If the inputs are the same, it will perform a doubling, but only if point1 and point2 are the same variable.
+/// If they have the same value but are different variables, the result will be incorrect because in this case
+/// it assumes (but does not check) that the points' x-coordinates are not equal.
+/// It also assumes neither point is the infinity point.
+pub fn embedded_curve_add_unsafe(point1: EmbeddedCurvePoint, point2: EmbeddedCurvePoint) -> EmbeddedCurvePoint {
+    let point_array = embedded_curve_add_array_return(point1, point2);
+    let x = point_array[0];
+    let y = point_array[1];
+
+    EmbeddedCurvePoint { x, y, is_infinite: false }
+}