diff --git a/compiler/noirc_evaluator/src/acir/acir_context/black_box.rs b/compiler/noirc_evaluator/src/acir/acir_context/black_box.rs index 12406c25e18..7da59e421ca 100644 --- a/compiler/noirc_evaluator/src/acir/acir_context/black_box.rs +++ b/compiler/noirc_evaluator/src/acir/acir_context/black_box.rs @@ -1,6 +1,9 @@ use acvm::{ BlackBoxFunctionSolver, - acir::{AcirField, BlackBoxFunc, circuit::opcodes::FunctionInput}, + acir::{ + AcirField, BlackBoxFunc, + circuit::opcodes::{ConstantOrWitnessEnum, FunctionInput}, + }, }; use iter_extended::vecmap; use num_bigint::BigUint; @@ -218,7 +221,11 @@ impl> AcirContext { | BlackBoxFunc::EmbeddedCurveAdd ); // Convert `AcirVar` to `FunctionInput` - let inputs = self.prepare_inputs_for_black_box_func_call(inputs, allow_constant_inputs)?; + let mut inputs = + self.prepare_inputs_for_black_box_func_call(inputs, allow_constant_inputs)?; + if name == BlackBoxFunc::EmbeddedCurveAdd { + inputs = self.all_or_nothing_for_ec_add(inputs)?; + } Ok(inputs) } @@ -261,4 +268,39 @@ impl> AcirContext { } Ok(witnesses) } + + /// EcAdd has 6 inputs representing the two points to add + /// Each point must be either all constant, or all witnesses + fn all_or_nothing_for_ec_add( + &mut self, + inputs: Vec>>, + ) -> Result>>, RuntimeError> { + let mut has_constant = false; + let mut has_witness = false; + let mut result = inputs.clone(); + for (i, input) in inputs.iter().enumerate() { + if input[0].is_constant() { + has_constant = true; + } else { + has_witness = true; + } + if i % 3 == 2 { + if has_constant && has_witness { + // Convert the constants to witness if mixed constant and witness, + for j in i - 2..i + 1 { + if let ConstantOrWitnessEnum::Constant(constant) = inputs[j][0].input() { + let constant = self.add_constant(constant); + let witness_var = self.get_or_create_witness_var(constant)?; + let witness = self.var_to_witness(witness_var)?; + result[j] = + vec![FunctionInput::witness(witness, inputs[j][0].num_bits())]; + } + } + } + has_constant = false; + has_witness = false; + } + } + Ok(result) + } } diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/embedded_curve_ops/execute__tests__force_brillig_false_inliner_-9223372036854775808.snap b/tooling/nargo_cli/tests/snapshots/execution_success/embedded_curve_ops/execute__tests__force_brillig_false_inliner_-9223372036854775808.snap index f9a02f36065..95e9276a19b 100644 --- a/tooling/nargo_cli/tests/snapshots/execution_success/embedded_curve_ops/execute__tests__force_brillig_false_inliner_-9223372036854775808.snap +++ b/tooling/nargo_cli/tests/snapshots/execution_success/embedded_curve_ops/execute__tests__force_brillig_false_inliner_-9223372036854775808.snap @@ -34,25 +34,26 @@ expression: artifact }, "bytecode": [ "func 0", - "current witness index : _17", + "current witness index : _18", "private parameters indices : [_0]", "public parameters indices : [_1, _2]", "return value indices : []", "BLACKBOX::MULTI_SCALAR_MUL [(1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (_0, 254), (0, 254)] [_3, _4, _5]", "EXPR [ (-1, _1) (1, _3) 0 ]", "EXPR [ (-1, _2) (1, _4) 0 ]", - "BLACKBOX::EMBEDDED_CURVE_ADD [(_1, 254), (_2, 254), (0, 1), (_1, 254), (_2, 254), (0, 1)] [_6, _7, _8]", - "EXPR [ (-1, _6) 3078034153852398078128400807926804309327113743808504829582559963737223069694 ]", - "BLACKBOX::MULTI_SCALAR_MUL [(1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (_0, 254), (0, 254), (_0, 254), (0, 254)] [_9, _10, _11]", - "EXPR [ (-1, _9) 3078034153852398078128400807926804309327113743808504829582559963737223069694 ]", - "BLACKBOX::MULTI_SCALAR_MUL [(1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (_1, 254), (_2, 254), (0, 1), (11179562631109628533987091031692370366552561688588090155835439555627259799605, 254), (3443719903172018228650470536370404288991794296383447657609081676265727805364, 254), (0, 1), (_0, 254), (0, 254), (_0, 254), (0, 254), (1, 254), (0, 254)] [_12, _13, _14]", - "EXPR [ (1, _12) 7349266043899242844836273743257843180744506495159104166319746739537754653274 ]", - "BLACKBOX::MULTI_SCALAR_MUL [(1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (_0, 254), (0, 254)] [_15, _16, _17]", - "EXPR [ (1, _17) 0 ]", - "EXPR [ (1, _15) -1 ]", - "EXPR [ (1, _16) -17631683881184975370165255887551781615748388533673675138860 ]" + "EXPR [ (-1, _6) 0 ]", + "BLACKBOX::EMBEDDED_CURVE_ADD [(_1, 254), (_2, 254), (_6, 1), (_1, 254), (_2, 254), (_6, 1)] [_7, _8, _9]", + "EXPR [ (-1, _7) 3078034153852398078128400807926804309327113743808504829582559963737223069694 ]", + "BLACKBOX::MULTI_SCALAR_MUL [(1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (_0, 254), (0, 254), (_0, 254), (0, 254)] [_10, _11, _12]", + "EXPR [ (-1, _10) 3078034153852398078128400807926804309327113743808504829582559963737223069694 ]", + "BLACKBOX::MULTI_SCALAR_MUL [(1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (_1, 254), (_2, 254), (0, 1), (11179562631109628533987091031692370366552561688588090155835439555627259799605, 254), (3443719903172018228650470536370404288991794296383447657609081676265727805364, 254), (0, 1), (_0, 254), (0, 254), (_0, 254), (0, 254), (1, 254), (0, 254)] [_13, _14, _15]", + "EXPR [ (1, _13) 7349266043899242844836273743257843180744506495159104166319746739537754653274 ]", + "BLACKBOX::MULTI_SCALAR_MUL [(1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (_0, 254), (0, 254)] [_16, _17, _18]", + "EXPR [ (1, _18) 0 ]", + "EXPR [ (1, _16) -1 ]", + "EXPR [ (1, _17) -17631683881184975370165255887551781615748388533673675138860 ]" ], - "debug_symbols": "tVVLjsIwDL1L1lnE+YerjEaolIAqRW0V2pFGiLuPg5oCiyAUhpWbxO/JfnbtM9n73Xzcdv1hOJHN15nsYhdCd9yGoW2mbujx9nyhJB+3U/Qer8jdO6LGJvp+Ipt+DoGSnybMV6fT2PRXOzURXxklvt+jRcJDF3z6utAbmpWhXOgFzIVZ4eplvOB8wQvjSnhexkvl5EIgtbwlALqOQZQYnuXgcg6S6QoNJM8FkEJW4LXMNdCal/DmCZ5Dxiso5W/LeCtYJrBC8hKDKzMAcGYWCvxW8h84TEUlzcpgeE0lLOROsBZKeBBvt/PrFDX97FYCYAAVMoDgK4O0RSHBvC+E+aQQIN3aUcqyGiUsV5nBSVUccPD+hIOPKuGUXfMwj3l846lpu/iwmgjDuUgJoAslHCcLJSL1EyUSDf4lKslLiU5RUGKSVJRYzANdHBp0AeRIjQSwWJ7sJUUZu2YX/LIDD3Pf3q3E6XfML3lpjnFo/X6OPsV4fcOo/wA=", + "debug_symbols": "tVXbbsIwDP2XPOchzj37lWlCpQRUKWqr0E6aEP8+hzUFHoJQGE9u4pwj+9i1T2Tnt/Nh0/X74Ug+Pk9kG7sQusMmDG0zdUOPt6czJfm4maL3eEVu/Igam+j7iXz0cwiUfDdhvjw6jk1/sVMT0cso8f0OLRLuu+DT15le0awM5UIvYC7MCldP4wXnC14YV8LzMl4qJxcCqeU1AdB1DKLE8CgHl3OQTFdoIHkugBSyAq9lroHWvIQ3D/AcMl5BKX9bxlvBMoEVkpcYXJkBgDOzUOC3kv/AYSoqaVYGw2sqYSF3grVQwoN4uZ2fp6jpZ7cSAAOokAEEXxmkLQoJ5nUhzDuFAOnWjlKW1ShhucoMTqrigIPXJxy8VQmn7JqHuc/jC09N28W71UQYzkVKAJ9QwnGyUCJSP1Ei/4xCgz+LTipTYlIwlNikGCUO08EngBxpPQCypIYCvliR7DlFG7tmG/yyC/dz396sxulnzJ68PMc4tH43R59ivfgw+l8=", "file_map": { "16": { "source": "use crate::cmp::Eq;\nuse crate::hash::Hash;\nuse crate::ops::arith::{Add, Neg, Sub};\n\n/// A point on the embedded elliptic curve\n/// By definition, the base field of the embedded curve is the scalar field of the proof system curve, i.e the Noir Field.\n/// x and y denotes the Weierstrass coordinates of the point, if is_infinite is false.\npub struct EmbeddedCurvePoint {\n pub x: Field,\n pub y: Field,\n pub is_infinite: bool,\n}\n\nimpl EmbeddedCurvePoint {\n /// Elliptic curve point doubling operation\n /// returns the doubled point of a point P, i.e P+P\n pub fn double(self) -> EmbeddedCurvePoint {\n embedded_curve_add(self, self)\n }\n\n /// Returns the null element of the curve; 'the point at infinity'\n pub fn point_at_infinity() -> EmbeddedCurvePoint {\n EmbeddedCurvePoint { x: 0, y: 0, is_infinite: true }\n }\n\n /// Returns the curve's generator point.\n pub fn generator() -> EmbeddedCurvePoint {\n // Generator point for the grumpkin curve (y^2 = x^3 - 17)\n EmbeddedCurvePoint {\n x: 1,\n y: 17631683881184975370165255887551781615748388533673675138860, // sqrt(-16)\n is_infinite: false,\n }\n }\n}\n\nimpl Add for EmbeddedCurvePoint {\n /// Adds two points P+Q, using the curve addition formula, and also handles point at infinity\n fn add(self, other: EmbeddedCurvePoint) -> EmbeddedCurvePoint {\n embedded_curve_add(self, other)\n }\n}\n\nimpl Sub for EmbeddedCurvePoint {\n /// Points subtraction operation, using addition and negation\n fn sub(self, other: EmbeddedCurvePoint) -> EmbeddedCurvePoint {\n self + other.neg()\n }\n}\n\nimpl Neg for EmbeddedCurvePoint {\n /// Negates a point P, i.e returns -P, by negating the y coordinate.\n /// If the point is at infinity, then the result is also at infinity.\n fn neg(self) -> EmbeddedCurvePoint {\n EmbeddedCurvePoint { x: self.x, y: -self.y, is_infinite: self.is_infinite }\n }\n}\n\nimpl Eq for EmbeddedCurvePoint {\n /// Checks whether two points are equal\n fn eq(self: Self, b: EmbeddedCurvePoint) -> bool {\n (self.is_infinite & b.is_infinite)\n | ((self.is_infinite == b.is_infinite) & (self.x == b.x) & (self.y == b.y))\n }\n}\n\nimpl Hash for EmbeddedCurvePoint {\n fn hash(self, state: &mut H)\n where\n H: crate::hash::Hasher,\n {\n if self.is_infinite {\n self.is_infinite.hash(state);\n } else {\n self.x.hash(state);\n self.y.hash(state);\n }\n }\n}\n\n/// Scalar for the embedded curve represented as low and high limbs\n/// By definition, the scalar field of the embedded curve is base field of the proving system curve.\n/// It may not fit into a Field element, so it is represented with two Field elements; its low and high limbs.\npub struct EmbeddedCurveScalar {\n pub lo: Field,\n pub hi: Field,\n}\n\nimpl EmbeddedCurveScalar {\n pub fn new(lo: Field, hi: Field) -> Self {\n EmbeddedCurveScalar { lo, hi }\n }\n\n #[field(bn254)]\n pub fn from_field(scalar: Field) -> EmbeddedCurveScalar {\n let (a, b) = crate::field::bn254::decompose(scalar);\n EmbeddedCurveScalar { lo: a, hi: b }\n }\n\n //Bytes to scalar: take the first (after the specified offset) 16 bytes of the input as the lo value, and the next 16 bytes as the hi value\n #[field(bn254)]\n pub(crate) fn from_bytes(bytes: [u8; 64], offset: u32) -> EmbeddedCurveScalar {\n let mut v = 1;\n let mut lo = 0 as Field;\n let mut hi = 0 as Field;\n for i in 0..16 {\n lo = lo + (bytes[offset + 31 - i] as Field) * v;\n hi = hi + (bytes[offset + 15 - i] as Field) * v;\n v = v * 256;\n }\n let sig_s = crate::embedded_curve_ops::EmbeddedCurveScalar { lo, hi };\n sig_s\n }\n}\n\nimpl Eq for EmbeddedCurveScalar {\n fn eq(self, other: Self) -> bool {\n (other.hi == self.hi) & (other.lo == self.lo)\n }\n}\n\nimpl Hash for EmbeddedCurveScalar {\n fn hash(self, state: &mut H)\n where\n H: crate::hash::Hasher,\n {\n self.hi.hash(state);\n self.lo.hash(state);\n }\n}\n\n// Computes a multi scalar multiplication over the embedded curve.\n// For bn254, We have Grumpkin and Baby JubJub.\n// For bls12-381, we have JubJub and Bandersnatch.\n//\n// The embedded curve being used is decided by the\n// underlying proof system.\n// docs:start:multi_scalar_mul\npub fn multi_scalar_mul(\n points: [EmbeddedCurvePoint; N],\n scalars: [EmbeddedCurveScalar; N],\n) -> EmbeddedCurvePoint\n// docs:end:multi_scalar_mul\n{\n multi_scalar_mul_array_return(points, scalars)[0]\n}\n\n#[foreign(multi_scalar_mul)]\npub(crate) fn multi_scalar_mul_array_return(\n points: [EmbeddedCurvePoint; N],\n scalars: [EmbeddedCurveScalar; N],\n) -> [EmbeddedCurvePoint; 1] {}\n\n// docs:start:fixed_base_scalar_mul\npub fn fixed_base_scalar_mul(scalar: EmbeddedCurveScalar) -> EmbeddedCurvePoint\n// docs:end:fixed_base_scalar_mul\n{\n multi_scalar_mul([EmbeddedCurvePoint::generator()], [scalar])\n}\n\n/// This function only assumes that the points are on the curve\n/// It handles corner cases around the infinity point causing some overhead compared to embedded_curve_add_not_nul and embedded_curve_add_unsafe\n// docs:start:embedded_curve_add\npub fn embedded_curve_add(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n // docs:end:embedded_curve_add\n if crate::runtime::is_unconstrained() {\n // `embedded_curve_add_unsafe` requires the inputs not to be the infinity point, so we check it here.\n // This is because `embedded_curve_add_unsafe` uses the `embedded_curve_add` opcode.\n // For efficiency, the backend does not check the inputs for the infinity point, but it assumes that they are not the infinity point\n // so that it can apply the ec addition formula directly.\n if point1.is_infinite {\n point2\n } else if point2.is_infinite {\n point1\n } else {\n embedded_curve_add_unsafe(point1, point2)\n }\n } else {\n // In a constrained context, we also need to check the inputs are not the infinity point because we also use `embedded_curve_add_unsafe`\n // However we also need to identify the case where the two inputs are the same, because then\n // the addition formula does not work and we need to use the doubling formula instead.\n // In unconstrained context, we can check directly if the input values are the same when solving the opcode, so it is not an issue.\n\n // x_coordinates_match is true if both abscissae are the same\n let x_coordinates_match = point1.x == point2.x;\n // y_coordinates_match is true if both ordinates are the same\n let y_coordinates_match = point1.y == point2.y;\n // double_predicate is true if both abscissae and ordinates are the same\n let double_predicate = (x_coordinates_match & y_coordinates_match);\n // If the abscissae are the same, but not the ordinates, then one point is the opposite of the other\n let infinity_predicate = (x_coordinates_match & !y_coordinates_match);\n let point1_1 = EmbeddedCurvePoint {\n x: point1.x + (x_coordinates_match as Field),\n y: point1.y,\n is_infinite: false,\n };\n let point2_1 = EmbeddedCurvePoint { x: point2.x, y: point2.y, is_infinite: false };\n // point1_1 is guaranteed to have a different abscissa than point2:\n // - if x_coordinates_match is 0, that means point1.x != point2.x, and point1_1.x = point1.x + 0\n // - if x_coordinates_match is 1, that means point1.x = point2.x, but point1_1.x = point1.x + 1 in this case\n // Because the abscissa is different, the addition formula is guaranteed to succeed, so we can safely use `embedded_curve_add_unsafe`\n // Note that this computation may be garbage: if x_coordinates_match is 1, or if one of the input is the point at infinity.\n let mut result = embedded_curve_add_unsafe(point1_1, point2_1);\n\n // `embedded_curve_add_unsafe` is doing a doubling if the input is the same variable, because in this case it is guaranteed (at 'compile time') that the input is the same.\n let double = embedded_curve_add_unsafe(point1, point1);\n // `embedded_curve_add_unsafe` would not perform doubling, even if the inputs point1 and point2 are the same, because it cannot know this without adding some logic (and some constraints)\n // However we did this logic when we computed `double_predicate`, so we set the result to 2*point1 if point1 and point2 are the same\n result = if double_predicate { double } else { result };\n\n // Same logic as above for unconstrained context, we set the proper result when one of the inputs is the infinity point\n if point1.is_infinite {\n result = point2;\n }\n if point2.is_infinite {\n result = point1;\n }\n\n // Finally, we set the is_infinity flag of the result:\n // Opposite points should sum into the infinity point, however, if one of them is point at infinity, their coordinates are not meaningful\n // so we should not use the fact that the inputs are opposite in this case:\n let mut result_is_infinity =\n infinity_predicate & (!point1.is_infinite & !point2.is_infinite);\n // However, if both of them are at infinity, then the result is also at infinity\n result.is_infinite = result_is_infinity | (point1.is_infinite & point2.is_infinite);\n result\n }\n}\n\n#[foreign(embedded_curve_add)]\nfn embedded_curve_add_array_return(\n _point1: EmbeddedCurvePoint,\n _point2: EmbeddedCurvePoint,\n) -> [EmbeddedCurvePoint; 1] {}\n\n/// This function assumes that:\n/// The points are on the curve, and\n/// The points don't share an x-coordinate, and\n/// Neither point is the infinity point.\n/// If it is used with correct input, the function ensures the correct non-zero result is returned.\n/// Except for points on the curve, the other assumptions are checked by the function. It will cause assertion failure if they are not respected.\npub fn embedded_curve_add_not_nul(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n assert(point1.x != point2.x);\n assert(!point1.is_infinite);\n assert(!point2.is_infinite);\n // Ensure is_infinite is comptime\n let point1_1 = EmbeddedCurvePoint { x: point1.x, y: point1.y, is_infinite: false };\n let point2_1 = EmbeddedCurvePoint { x: point2.x, y: point2.y, is_infinite: false };\n embedded_curve_add_unsafe(point1_1, point2_1)\n}\n\n/// Unsafe ec addition\n/// If the inputs are the same, it will perform a doubling, but only if point1 and point2 are the same variable.\n/// If they have the same value but are different variables, the result will be incorrect because in this case\n/// it assumes (but does not check) that the points' x-coordinates are not equal.\n/// It also assumes neither point is the infinity point.\npub fn embedded_curve_add_unsafe(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n embedded_curve_add_array_return(point1, point2)[0]\n}\n", diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/embedded_curve_ops/execute__tests__force_brillig_false_inliner_0.snap b/tooling/nargo_cli/tests/snapshots/execution_success/embedded_curve_ops/execute__tests__force_brillig_false_inliner_0.snap index f9a02f36065..95e9276a19b 100644 --- a/tooling/nargo_cli/tests/snapshots/execution_success/embedded_curve_ops/execute__tests__force_brillig_false_inliner_0.snap +++ b/tooling/nargo_cli/tests/snapshots/execution_success/embedded_curve_ops/execute__tests__force_brillig_false_inliner_0.snap @@ -34,25 +34,26 @@ expression: artifact }, "bytecode": [ "func 0", - "current witness index : _17", + "current witness index : _18", "private parameters indices : [_0]", "public parameters indices : [_1, _2]", "return value indices : []", "BLACKBOX::MULTI_SCALAR_MUL [(1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (_0, 254), (0, 254)] [_3, _4, _5]", "EXPR [ (-1, _1) (1, _3) 0 ]", "EXPR [ (-1, _2) (1, _4) 0 ]", - "BLACKBOX::EMBEDDED_CURVE_ADD [(_1, 254), (_2, 254), (0, 1), (_1, 254), (_2, 254), (0, 1)] [_6, _7, _8]", - "EXPR [ (-1, _6) 3078034153852398078128400807926804309327113743808504829582559963737223069694 ]", - "BLACKBOX::MULTI_SCALAR_MUL [(1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (_0, 254), (0, 254), (_0, 254), (0, 254)] [_9, _10, _11]", - "EXPR [ (-1, _9) 3078034153852398078128400807926804309327113743808504829582559963737223069694 ]", - "BLACKBOX::MULTI_SCALAR_MUL [(1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (_1, 254), (_2, 254), (0, 1), (11179562631109628533987091031692370366552561688588090155835439555627259799605, 254), (3443719903172018228650470536370404288991794296383447657609081676265727805364, 254), (0, 1), (_0, 254), (0, 254), (_0, 254), (0, 254), (1, 254), (0, 254)] [_12, _13, _14]", - "EXPR [ (1, _12) 7349266043899242844836273743257843180744506495159104166319746739537754653274 ]", - "BLACKBOX::MULTI_SCALAR_MUL [(1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (_0, 254), (0, 254)] [_15, _16, _17]", - "EXPR [ (1, _17) 0 ]", - "EXPR [ (1, _15) -1 ]", - "EXPR [ (1, _16) -17631683881184975370165255887551781615748388533673675138860 ]" + "EXPR [ (-1, _6) 0 ]", + "BLACKBOX::EMBEDDED_CURVE_ADD [(_1, 254), (_2, 254), (_6, 1), (_1, 254), (_2, 254), (_6, 1)] [_7, _8, _9]", + "EXPR [ (-1, _7) 3078034153852398078128400807926804309327113743808504829582559963737223069694 ]", + "BLACKBOX::MULTI_SCALAR_MUL [(1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (_0, 254), (0, 254), (_0, 254), (0, 254)] [_10, _11, _12]", + "EXPR [ (-1, _10) 3078034153852398078128400807926804309327113743808504829582559963737223069694 ]", + "BLACKBOX::MULTI_SCALAR_MUL [(1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (_1, 254), (_2, 254), (0, 1), (11179562631109628533987091031692370366552561688588090155835439555627259799605, 254), (3443719903172018228650470536370404288991794296383447657609081676265727805364, 254), (0, 1), (_0, 254), (0, 254), (_0, 254), (0, 254), (1, 254), (0, 254)] [_13, _14, _15]", + "EXPR [ (1, _13) 7349266043899242844836273743257843180744506495159104166319746739537754653274 ]", + "BLACKBOX::MULTI_SCALAR_MUL [(1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (_0, 254), (0, 254)] [_16, _17, _18]", + "EXPR [ (1, _18) 0 ]", + "EXPR [ (1, _16) -1 ]", + "EXPR [ (1, _17) -17631683881184975370165255887551781615748388533673675138860 ]" ], - "debug_symbols": "tVVLjsIwDL1L1lnE+YerjEaolIAqRW0V2pFGiLuPg5oCiyAUhpWbxO/JfnbtM9n73Xzcdv1hOJHN15nsYhdCd9yGoW2mbujx9nyhJB+3U/Qer8jdO6LGJvp+Ipt+DoGSnybMV6fT2PRXOzURXxklvt+jRcJDF3z6utAbmpWhXOgFzIVZ4eplvOB8wQvjSnhexkvl5EIgtbwlALqOQZQYnuXgcg6S6QoNJM8FkEJW4LXMNdCal/DmCZ5Dxiso5W/LeCtYJrBC8hKDKzMAcGYWCvxW8h84TEUlzcpgeE0lLOROsBZKeBBvt/PrFDX97FYCYAAVMoDgK4O0RSHBvC+E+aQQIN3aUcqyGiUsV5nBSVUccPD+hIOPKuGUXfMwj3l846lpu/iwmgjDuUgJoAslHCcLJSL1EyUSDf4lKslLiU5RUGKSVJRYzANdHBp0AeRIjQSwWJ7sJUUZu2YX/LIDD3Pf3q3E6XfML3lpjnFo/X6OPsV4fcOo/wA=", + "debug_symbols": "tVXbbsIwDP2XPOchzj37lWlCpQRUKWqr0E6aEP8+hzUFHoJQGE9u4pwj+9i1T2Tnt/Nh0/X74Ug+Pk9kG7sQusMmDG0zdUOPt6czJfm4maL3eEVu/Igam+j7iXz0cwiUfDdhvjw6jk1/sVMT0cso8f0OLRLuu+DT15le0awM5UIvYC7MCldP4wXnC14YV8LzMl4qJxcCqeU1AdB1DKLE8CgHl3OQTFdoIHkugBSyAq9lroHWvIQ3D/AcMl5BKX9bxlvBMoEVkpcYXJkBgDOzUOC3kv/AYSoqaVYGw2sqYSF3grVQwoN4uZ2fp6jpZ7cSAAOokAEEXxmkLQoJ5nUhzDuFAOnWjlKW1ShhucoMTqrigIPXJxy8VQmn7JqHuc/jC09N28W71UQYzkVKAJ9QwnGyUCJSP1Ei/4xCgz+LTipTYlIwlNikGCUO08EngBxpPQCypIYCvliR7DlFG7tmG/yyC/dz396sxulnzJ68PMc4tH43R59ivfgw+l8=", "file_map": { "16": { "source": "use crate::cmp::Eq;\nuse crate::hash::Hash;\nuse crate::ops::arith::{Add, Neg, Sub};\n\n/// A point on the embedded elliptic curve\n/// By definition, the base field of the embedded curve is the scalar field of the proof system curve, i.e the Noir Field.\n/// x and y denotes the Weierstrass coordinates of the point, if is_infinite is false.\npub struct EmbeddedCurvePoint {\n pub x: Field,\n pub y: Field,\n pub is_infinite: bool,\n}\n\nimpl EmbeddedCurvePoint {\n /// Elliptic curve point doubling operation\n /// returns the doubled point of a point P, i.e P+P\n pub fn double(self) -> EmbeddedCurvePoint {\n embedded_curve_add(self, self)\n }\n\n /// Returns the null element of the curve; 'the point at infinity'\n pub fn point_at_infinity() -> EmbeddedCurvePoint {\n EmbeddedCurvePoint { x: 0, y: 0, is_infinite: true }\n }\n\n /// Returns the curve's generator point.\n pub fn generator() -> EmbeddedCurvePoint {\n // Generator point for the grumpkin curve (y^2 = x^3 - 17)\n EmbeddedCurvePoint {\n x: 1,\n y: 17631683881184975370165255887551781615748388533673675138860, // sqrt(-16)\n is_infinite: false,\n }\n }\n}\n\nimpl Add for EmbeddedCurvePoint {\n /// Adds two points P+Q, using the curve addition formula, and also handles point at infinity\n fn add(self, other: EmbeddedCurvePoint) -> EmbeddedCurvePoint {\n embedded_curve_add(self, other)\n }\n}\n\nimpl Sub for EmbeddedCurvePoint {\n /// Points subtraction operation, using addition and negation\n fn sub(self, other: EmbeddedCurvePoint) -> EmbeddedCurvePoint {\n self + other.neg()\n }\n}\n\nimpl Neg for EmbeddedCurvePoint {\n /// Negates a point P, i.e returns -P, by negating the y coordinate.\n /// If the point is at infinity, then the result is also at infinity.\n fn neg(self) -> EmbeddedCurvePoint {\n EmbeddedCurvePoint { x: self.x, y: -self.y, is_infinite: self.is_infinite }\n }\n}\n\nimpl Eq for EmbeddedCurvePoint {\n /// Checks whether two points are equal\n fn eq(self: Self, b: EmbeddedCurvePoint) -> bool {\n (self.is_infinite & b.is_infinite)\n | ((self.is_infinite == b.is_infinite) & (self.x == b.x) & (self.y == b.y))\n }\n}\n\nimpl Hash for EmbeddedCurvePoint {\n fn hash(self, state: &mut H)\n where\n H: crate::hash::Hasher,\n {\n if self.is_infinite {\n self.is_infinite.hash(state);\n } else {\n self.x.hash(state);\n self.y.hash(state);\n }\n }\n}\n\n/// Scalar for the embedded curve represented as low and high limbs\n/// By definition, the scalar field of the embedded curve is base field of the proving system curve.\n/// It may not fit into a Field element, so it is represented with two Field elements; its low and high limbs.\npub struct EmbeddedCurveScalar {\n pub lo: Field,\n pub hi: Field,\n}\n\nimpl EmbeddedCurveScalar {\n pub fn new(lo: Field, hi: Field) -> Self {\n EmbeddedCurveScalar { lo, hi }\n }\n\n #[field(bn254)]\n pub fn from_field(scalar: Field) -> EmbeddedCurveScalar {\n let (a, b) = crate::field::bn254::decompose(scalar);\n EmbeddedCurveScalar { lo: a, hi: b }\n }\n\n //Bytes to scalar: take the first (after the specified offset) 16 bytes of the input as the lo value, and the next 16 bytes as the hi value\n #[field(bn254)]\n pub(crate) fn from_bytes(bytes: [u8; 64], offset: u32) -> EmbeddedCurveScalar {\n let mut v = 1;\n let mut lo = 0 as Field;\n let mut hi = 0 as Field;\n for i in 0..16 {\n lo = lo + (bytes[offset + 31 - i] as Field) * v;\n hi = hi + (bytes[offset + 15 - i] as Field) * v;\n v = v * 256;\n }\n let sig_s = crate::embedded_curve_ops::EmbeddedCurveScalar { lo, hi };\n sig_s\n }\n}\n\nimpl Eq for EmbeddedCurveScalar {\n fn eq(self, other: Self) -> bool {\n (other.hi == self.hi) & (other.lo == self.lo)\n }\n}\n\nimpl Hash for EmbeddedCurveScalar {\n fn hash(self, state: &mut H)\n where\n H: crate::hash::Hasher,\n {\n self.hi.hash(state);\n self.lo.hash(state);\n }\n}\n\n// Computes a multi scalar multiplication over the embedded curve.\n// For bn254, We have Grumpkin and Baby JubJub.\n// For bls12-381, we have JubJub and Bandersnatch.\n//\n// The embedded curve being used is decided by the\n// underlying proof system.\n// docs:start:multi_scalar_mul\npub fn multi_scalar_mul(\n points: [EmbeddedCurvePoint; N],\n scalars: [EmbeddedCurveScalar; N],\n) -> EmbeddedCurvePoint\n// docs:end:multi_scalar_mul\n{\n multi_scalar_mul_array_return(points, scalars)[0]\n}\n\n#[foreign(multi_scalar_mul)]\npub(crate) fn multi_scalar_mul_array_return(\n points: [EmbeddedCurvePoint; N],\n scalars: [EmbeddedCurveScalar; N],\n) -> [EmbeddedCurvePoint; 1] {}\n\n// docs:start:fixed_base_scalar_mul\npub fn fixed_base_scalar_mul(scalar: EmbeddedCurveScalar) -> EmbeddedCurvePoint\n// docs:end:fixed_base_scalar_mul\n{\n multi_scalar_mul([EmbeddedCurvePoint::generator()], [scalar])\n}\n\n/// This function only assumes that the points are on the curve\n/// It handles corner cases around the infinity point causing some overhead compared to embedded_curve_add_not_nul and embedded_curve_add_unsafe\n// docs:start:embedded_curve_add\npub fn embedded_curve_add(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n // docs:end:embedded_curve_add\n if crate::runtime::is_unconstrained() {\n // `embedded_curve_add_unsafe` requires the inputs not to be the infinity point, so we check it here.\n // This is because `embedded_curve_add_unsafe` uses the `embedded_curve_add` opcode.\n // For efficiency, the backend does not check the inputs for the infinity point, but it assumes that they are not the infinity point\n // so that it can apply the ec addition formula directly.\n if point1.is_infinite {\n point2\n } else if point2.is_infinite {\n point1\n } else {\n embedded_curve_add_unsafe(point1, point2)\n }\n } else {\n // In a constrained context, we also need to check the inputs are not the infinity point because we also use `embedded_curve_add_unsafe`\n // However we also need to identify the case where the two inputs are the same, because then\n // the addition formula does not work and we need to use the doubling formula instead.\n // In unconstrained context, we can check directly if the input values are the same when solving the opcode, so it is not an issue.\n\n // x_coordinates_match is true if both abscissae are the same\n let x_coordinates_match = point1.x == point2.x;\n // y_coordinates_match is true if both ordinates are the same\n let y_coordinates_match = point1.y == point2.y;\n // double_predicate is true if both abscissae and ordinates are the same\n let double_predicate = (x_coordinates_match & y_coordinates_match);\n // If the abscissae are the same, but not the ordinates, then one point is the opposite of the other\n let infinity_predicate = (x_coordinates_match & !y_coordinates_match);\n let point1_1 = EmbeddedCurvePoint {\n x: point1.x + (x_coordinates_match as Field),\n y: point1.y,\n is_infinite: false,\n };\n let point2_1 = EmbeddedCurvePoint { x: point2.x, y: point2.y, is_infinite: false };\n // point1_1 is guaranteed to have a different abscissa than point2:\n // - if x_coordinates_match is 0, that means point1.x != point2.x, and point1_1.x = point1.x + 0\n // - if x_coordinates_match is 1, that means point1.x = point2.x, but point1_1.x = point1.x + 1 in this case\n // Because the abscissa is different, the addition formula is guaranteed to succeed, so we can safely use `embedded_curve_add_unsafe`\n // Note that this computation may be garbage: if x_coordinates_match is 1, or if one of the input is the point at infinity.\n let mut result = embedded_curve_add_unsafe(point1_1, point2_1);\n\n // `embedded_curve_add_unsafe` is doing a doubling if the input is the same variable, because in this case it is guaranteed (at 'compile time') that the input is the same.\n let double = embedded_curve_add_unsafe(point1, point1);\n // `embedded_curve_add_unsafe` would not perform doubling, even if the inputs point1 and point2 are the same, because it cannot know this without adding some logic (and some constraints)\n // However we did this logic when we computed `double_predicate`, so we set the result to 2*point1 if point1 and point2 are the same\n result = if double_predicate { double } else { result };\n\n // Same logic as above for unconstrained context, we set the proper result when one of the inputs is the infinity point\n if point1.is_infinite {\n result = point2;\n }\n if point2.is_infinite {\n result = point1;\n }\n\n // Finally, we set the is_infinity flag of the result:\n // Opposite points should sum into the infinity point, however, if one of them is point at infinity, their coordinates are not meaningful\n // so we should not use the fact that the inputs are opposite in this case:\n let mut result_is_infinity =\n infinity_predicate & (!point1.is_infinite & !point2.is_infinite);\n // However, if both of them are at infinity, then the result is also at infinity\n result.is_infinite = result_is_infinity | (point1.is_infinite & point2.is_infinite);\n result\n }\n}\n\n#[foreign(embedded_curve_add)]\nfn embedded_curve_add_array_return(\n _point1: EmbeddedCurvePoint,\n _point2: EmbeddedCurvePoint,\n) -> [EmbeddedCurvePoint; 1] {}\n\n/// This function assumes that:\n/// The points are on the curve, and\n/// The points don't share an x-coordinate, and\n/// Neither point is the infinity point.\n/// If it is used with correct input, the function ensures the correct non-zero result is returned.\n/// Except for points on the curve, the other assumptions are checked by the function. It will cause assertion failure if they are not respected.\npub fn embedded_curve_add_not_nul(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n assert(point1.x != point2.x);\n assert(!point1.is_infinite);\n assert(!point2.is_infinite);\n // Ensure is_infinite is comptime\n let point1_1 = EmbeddedCurvePoint { x: point1.x, y: point1.y, is_infinite: false };\n let point2_1 = EmbeddedCurvePoint { x: point2.x, y: point2.y, is_infinite: false };\n embedded_curve_add_unsafe(point1_1, point2_1)\n}\n\n/// Unsafe ec addition\n/// If the inputs are the same, it will perform a doubling, but only if point1 and point2 are the same variable.\n/// If they have the same value but are different variables, the result will be incorrect because in this case\n/// it assumes (but does not check) that the points' x-coordinates are not equal.\n/// It also assumes neither point is the infinity point.\npub fn embedded_curve_add_unsafe(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n embedded_curve_add_array_return(point1, point2)[0]\n}\n", diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/embedded_curve_ops/execute__tests__force_brillig_false_inliner_9223372036854775807.snap b/tooling/nargo_cli/tests/snapshots/execution_success/embedded_curve_ops/execute__tests__force_brillig_false_inliner_9223372036854775807.snap index f9a02f36065..95e9276a19b 100644 --- a/tooling/nargo_cli/tests/snapshots/execution_success/embedded_curve_ops/execute__tests__force_brillig_false_inliner_9223372036854775807.snap +++ b/tooling/nargo_cli/tests/snapshots/execution_success/embedded_curve_ops/execute__tests__force_brillig_false_inliner_9223372036854775807.snap @@ -34,25 +34,26 @@ expression: artifact }, "bytecode": [ "func 0", - "current witness index : _17", + "current witness index : _18", "private parameters indices : [_0]", "public parameters indices : [_1, _2]", "return value indices : []", "BLACKBOX::MULTI_SCALAR_MUL [(1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (_0, 254), (0, 254)] [_3, _4, _5]", "EXPR [ (-1, _1) (1, _3) 0 ]", "EXPR [ (-1, _2) (1, _4) 0 ]", - "BLACKBOX::EMBEDDED_CURVE_ADD [(_1, 254), (_2, 254), (0, 1), (_1, 254), (_2, 254), (0, 1)] [_6, _7, _8]", - "EXPR [ (-1, _6) 3078034153852398078128400807926804309327113743808504829582559963737223069694 ]", - "BLACKBOX::MULTI_SCALAR_MUL [(1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (_0, 254), (0, 254), (_0, 254), (0, 254)] [_9, _10, _11]", - "EXPR [ (-1, _9) 3078034153852398078128400807926804309327113743808504829582559963737223069694 ]", - "BLACKBOX::MULTI_SCALAR_MUL [(1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (_1, 254), (_2, 254), (0, 1), (11179562631109628533987091031692370366552561688588090155835439555627259799605, 254), (3443719903172018228650470536370404288991794296383447657609081676265727805364, 254), (0, 1), (_0, 254), (0, 254), (_0, 254), (0, 254), (1, 254), (0, 254)] [_12, _13, _14]", - "EXPR [ (1, _12) 7349266043899242844836273743257843180744506495159104166319746739537754653274 ]", - "BLACKBOX::MULTI_SCALAR_MUL [(1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (_0, 254), (0, 254)] [_15, _16, _17]", - "EXPR [ (1, _17) 0 ]", - "EXPR [ (1, _15) -1 ]", - "EXPR [ (1, _16) -17631683881184975370165255887551781615748388533673675138860 ]" + "EXPR [ (-1, _6) 0 ]", + "BLACKBOX::EMBEDDED_CURVE_ADD [(_1, 254), (_2, 254), (_6, 1), (_1, 254), (_2, 254), (_6, 1)] [_7, _8, _9]", + "EXPR [ (-1, _7) 3078034153852398078128400807926804309327113743808504829582559963737223069694 ]", + "BLACKBOX::MULTI_SCALAR_MUL [(1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (_0, 254), (0, 254), (_0, 254), (0, 254)] [_10, _11, _12]", + "EXPR [ (-1, _10) 3078034153852398078128400807926804309327113743808504829582559963737223069694 ]", + "BLACKBOX::MULTI_SCALAR_MUL [(1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (_1, 254), (_2, 254), (0, 1), (11179562631109628533987091031692370366552561688588090155835439555627259799605, 254), (3443719903172018228650470536370404288991794296383447657609081676265727805364, 254), (0, 1), (_0, 254), (0, 254), (_0, 254), (0, 254), (1, 254), (0, 254)] [_13, _14, _15]", + "EXPR [ (1, _13) 7349266043899242844836273743257843180744506495159104166319746739537754653274 ]", + "BLACKBOX::MULTI_SCALAR_MUL [(1, 254), (17631683881184975370165255887551781615748388533673675138860, 254), (0, 1), (_0, 254), (0, 254)] [_16, _17, _18]", + "EXPR [ (1, _18) 0 ]", + "EXPR [ (1, _16) -1 ]", + "EXPR [ (1, _17) -17631683881184975370165255887551781615748388533673675138860 ]" ], - "debug_symbols": "tVVLjsIwDL1L1lnE+YerjEaolIAqRW0V2pFGiLuPg5oCiyAUhpWbxO/JfnbtM9n73Xzcdv1hOJHN15nsYhdCd9yGoW2mbujx9nyhJB+3U/Qer8jdO6LGJvp+Ipt+DoGSnybMV6fT2PRXOzURXxklvt+jRcJDF3z6utAbmpWhXOgFzIVZ4eplvOB8wQvjSnhexkvl5EIgtbwlALqOQZQYnuXgcg6S6QoNJM8FkEJW4LXMNdCal/DmCZ5Dxiso5W/LeCtYJrBC8hKDKzMAcGYWCvxW8h84TEUlzcpgeE0lLOROsBZKeBBvt/PrFDX97FYCYAAVMoDgK4O0RSHBvC+E+aQQIN3aUcqyGiUsV5nBSVUccPD+hIOPKuGUXfMwj3l846lpu/iwmgjDuUgJoAslHCcLJSL1EyUSDf4lKslLiU5RUGKSVJRYzANdHBp0AeRIjQSwWJ7sJUUZu2YX/LIDD3Pf3q3E6XfML3lpjnFo/X6OPsV4fcOo/wA=", + "debug_symbols": "tVXbbsIwDP2XPOchzj37lWlCpQRUKWqr0E6aEP8+hzUFHoJQGE9u4pwj+9i1T2Tnt/Nh0/X74Ug+Pk9kG7sQusMmDG0zdUOPt6czJfm4maL3eEVu/Igam+j7iXz0cwiUfDdhvjw6jk1/sVMT0cso8f0OLRLuu+DT15le0awM5UIvYC7MCldP4wXnC14YV8LzMl4qJxcCqeU1AdB1DKLE8CgHl3OQTFdoIHkugBSyAq9lroHWvIQ3D/AcMl5BKX9bxlvBMoEVkpcYXJkBgDOzUOC3kv/AYSoqaVYGw2sqYSF3grVQwoN4uZ2fp6jpZ7cSAAOokAEEXxmkLQoJ5nUhzDuFAOnWjlKW1ShhucoMTqrigIPXJxy8VQmn7JqHuc/jC09N28W71UQYzkVKAJ9QwnGyUCJSP1Ei/4xCgz+LTipTYlIwlNikGCUO08EngBxpPQCypIYCvliR7DlFG7tmG/yyC/dz396sxulnzJ68PMc4tH43R59ivfgw+l8=", "file_map": { "16": { "source": "use crate::cmp::Eq;\nuse crate::hash::Hash;\nuse crate::ops::arith::{Add, Neg, Sub};\n\n/// A point on the embedded elliptic curve\n/// By definition, the base field of the embedded curve is the scalar field of the proof system curve, i.e the Noir Field.\n/// x and y denotes the Weierstrass coordinates of the point, if is_infinite is false.\npub struct EmbeddedCurvePoint {\n pub x: Field,\n pub y: Field,\n pub is_infinite: bool,\n}\n\nimpl EmbeddedCurvePoint {\n /// Elliptic curve point doubling operation\n /// returns the doubled point of a point P, i.e P+P\n pub fn double(self) -> EmbeddedCurvePoint {\n embedded_curve_add(self, self)\n }\n\n /// Returns the null element of the curve; 'the point at infinity'\n pub fn point_at_infinity() -> EmbeddedCurvePoint {\n EmbeddedCurvePoint { x: 0, y: 0, is_infinite: true }\n }\n\n /// Returns the curve's generator point.\n pub fn generator() -> EmbeddedCurvePoint {\n // Generator point for the grumpkin curve (y^2 = x^3 - 17)\n EmbeddedCurvePoint {\n x: 1,\n y: 17631683881184975370165255887551781615748388533673675138860, // sqrt(-16)\n is_infinite: false,\n }\n }\n}\n\nimpl Add for EmbeddedCurvePoint {\n /// Adds two points P+Q, using the curve addition formula, and also handles point at infinity\n fn add(self, other: EmbeddedCurvePoint) -> EmbeddedCurvePoint {\n embedded_curve_add(self, other)\n }\n}\n\nimpl Sub for EmbeddedCurvePoint {\n /// Points subtraction operation, using addition and negation\n fn sub(self, other: EmbeddedCurvePoint) -> EmbeddedCurvePoint {\n self + other.neg()\n }\n}\n\nimpl Neg for EmbeddedCurvePoint {\n /// Negates a point P, i.e returns -P, by negating the y coordinate.\n /// If the point is at infinity, then the result is also at infinity.\n fn neg(self) -> EmbeddedCurvePoint {\n EmbeddedCurvePoint { x: self.x, y: -self.y, is_infinite: self.is_infinite }\n }\n}\n\nimpl Eq for EmbeddedCurvePoint {\n /// Checks whether two points are equal\n fn eq(self: Self, b: EmbeddedCurvePoint) -> bool {\n (self.is_infinite & b.is_infinite)\n | ((self.is_infinite == b.is_infinite) & (self.x == b.x) & (self.y == b.y))\n }\n}\n\nimpl Hash for EmbeddedCurvePoint {\n fn hash(self, state: &mut H)\n where\n H: crate::hash::Hasher,\n {\n if self.is_infinite {\n self.is_infinite.hash(state);\n } else {\n self.x.hash(state);\n self.y.hash(state);\n }\n }\n}\n\n/// Scalar for the embedded curve represented as low and high limbs\n/// By definition, the scalar field of the embedded curve is base field of the proving system curve.\n/// It may not fit into a Field element, so it is represented with two Field elements; its low and high limbs.\npub struct EmbeddedCurveScalar {\n pub lo: Field,\n pub hi: Field,\n}\n\nimpl EmbeddedCurveScalar {\n pub fn new(lo: Field, hi: Field) -> Self {\n EmbeddedCurveScalar { lo, hi }\n }\n\n #[field(bn254)]\n pub fn from_field(scalar: Field) -> EmbeddedCurveScalar {\n let (a, b) = crate::field::bn254::decompose(scalar);\n EmbeddedCurveScalar { lo: a, hi: b }\n }\n\n //Bytes to scalar: take the first (after the specified offset) 16 bytes of the input as the lo value, and the next 16 bytes as the hi value\n #[field(bn254)]\n pub(crate) fn from_bytes(bytes: [u8; 64], offset: u32) -> EmbeddedCurveScalar {\n let mut v = 1;\n let mut lo = 0 as Field;\n let mut hi = 0 as Field;\n for i in 0..16 {\n lo = lo + (bytes[offset + 31 - i] as Field) * v;\n hi = hi + (bytes[offset + 15 - i] as Field) * v;\n v = v * 256;\n }\n let sig_s = crate::embedded_curve_ops::EmbeddedCurveScalar { lo, hi };\n sig_s\n }\n}\n\nimpl Eq for EmbeddedCurveScalar {\n fn eq(self, other: Self) -> bool {\n (other.hi == self.hi) & (other.lo == self.lo)\n }\n}\n\nimpl Hash for EmbeddedCurveScalar {\n fn hash(self, state: &mut H)\n where\n H: crate::hash::Hasher,\n {\n self.hi.hash(state);\n self.lo.hash(state);\n }\n}\n\n// Computes a multi scalar multiplication over the embedded curve.\n// For bn254, We have Grumpkin and Baby JubJub.\n// For bls12-381, we have JubJub and Bandersnatch.\n//\n// The embedded curve being used is decided by the\n// underlying proof system.\n// docs:start:multi_scalar_mul\npub fn multi_scalar_mul(\n points: [EmbeddedCurvePoint; N],\n scalars: [EmbeddedCurveScalar; N],\n) -> EmbeddedCurvePoint\n// docs:end:multi_scalar_mul\n{\n multi_scalar_mul_array_return(points, scalars)[0]\n}\n\n#[foreign(multi_scalar_mul)]\npub(crate) fn multi_scalar_mul_array_return(\n points: [EmbeddedCurvePoint; N],\n scalars: [EmbeddedCurveScalar; N],\n) -> [EmbeddedCurvePoint; 1] {}\n\n// docs:start:fixed_base_scalar_mul\npub fn fixed_base_scalar_mul(scalar: EmbeddedCurveScalar) -> EmbeddedCurvePoint\n// docs:end:fixed_base_scalar_mul\n{\n multi_scalar_mul([EmbeddedCurvePoint::generator()], [scalar])\n}\n\n/// This function only assumes that the points are on the curve\n/// It handles corner cases around the infinity point causing some overhead compared to embedded_curve_add_not_nul and embedded_curve_add_unsafe\n// docs:start:embedded_curve_add\npub fn embedded_curve_add(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n // docs:end:embedded_curve_add\n if crate::runtime::is_unconstrained() {\n // `embedded_curve_add_unsafe` requires the inputs not to be the infinity point, so we check it here.\n // This is because `embedded_curve_add_unsafe` uses the `embedded_curve_add` opcode.\n // For efficiency, the backend does not check the inputs for the infinity point, but it assumes that they are not the infinity point\n // so that it can apply the ec addition formula directly.\n if point1.is_infinite {\n point2\n } else if point2.is_infinite {\n point1\n } else {\n embedded_curve_add_unsafe(point1, point2)\n }\n } else {\n // In a constrained context, we also need to check the inputs are not the infinity point because we also use `embedded_curve_add_unsafe`\n // However we also need to identify the case where the two inputs are the same, because then\n // the addition formula does not work and we need to use the doubling formula instead.\n // In unconstrained context, we can check directly if the input values are the same when solving the opcode, so it is not an issue.\n\n // x_coordinates_match is true if both abscissae are the same\n let x_coordinates_match = point1.x == point2.x;\n // y_coordinates_match is true if both ordinates are the same\n let y_coordinates_match = point1.y == point2.y;\n // double_predicate is true if both abscissae and ordinates are the same\n let double_predicate = (x_coordinates_match & y_coordinates_match);\n // If the abscissae are the same, but not the ordinates, then one point is the opposite of the other\n let infinity_predicate = (x_coordinates_match & !y_coordinates_match);\n let point1_1 = EmbeddedCurvePoint {\n x: point1.x + (x_coordinates_match as Field),\n y: point1.y,\n is_infinite: false,\n };\n let point2_1 = EmbeddedCurvePoint { x: point2.x, y: point2.y, is_infinite: false };\n // point1_1 is guaranteed to have a different abscissa than point2:\n // - if x_coordinates_match is 0, that means point1.x != point2.x, and point1_1.x = point1.x + 0\n // - if x_coordinates_match is 1, that means point1.x = point2.x, but point1_1.x = point1.x + 1 in this case\n // Because the abscissa is different, the addition formula is guaranteed to succeed, so we can safely use `embedded_curve_add_unsafe`\n // Note that this computation may be garbage: if x_coordinates_match is 1, or if one of the input is the point at infinity.\n let mut result = embedded_curve_add_unsafe(point1_1, point2_1);\n\n // `embedded_curve_add_unsafe` is doing a doubling if the input is the same variable, because in this case it is guaranteed (at 'compile time') that the input is the same.\n let double = embedded_curve_add_unsafe(point1, point1);\n // `embedded_curve_add_unsafe` would not perform doubling, even if the inputs point1 and point2 are the same, because it cannot know this without adding some logic (and some constraints)\n // However we did this logic when we computed `double_predicate`, so we set the result to 2*point1 if point1 and point2 are the same\n result = if double_predicate { double } else { result };\n\n // Same logic as above for unconstrained context, we set the proper result when one of the inputs is the infinity point\n if point1.is_infinite {\n result = point2;\n }\n if point2.is_infinite {\n result = point1;\n }\n\n // Finally, we set the is_infinity flag of the result:\n // Opposite points should sum into the infinity point, however, if one of them is point at infinity, their coordinates are not meaningful\n // so we should not use the fact that the inputs are opposite in this case:\n let mut result_is_infinity =\n infinity_predicate & (!point1.is_infinite & !point2.is_infinite);\n // However, if both of them are at infinity, then the result is also at infinity\n result.is_infinite = result_is_infinity | (point1.is_infinite & point2.is_infinite);\n result\n }\n}\n\n#[foreign(embedded_curve_add)]\nfn embedded_curve_add_array_return(\n _point1: EmbeddedCurvePoint,\n _point2: EmbeddedCurvePoint,\n) -> [EmbeddedCurvePoint; 1] {}\n\n/// This function assumes that:\n/// The points are on the curve, and\n/// The points don't share an x-coordinate, and\n/// Neither point is the infinity point.\n/// If it is used with correct input, the function ensures the correct non-zero result is returned.\n/// Except for points on the curve, the other assumptions are checked by the function. It will cause assertion failure if they are not respected.\npub fn embedded_curve_add_not_nul(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n assert(point1.x != point2.x);\n assert(!point1.is_infinite);\n assert(!point2.is_infinite);\n // Ensure is_infinite is comptime\n let point1_1 = EmbeddedCurvePoint { x: point1.x, y: point1.y, is_infinite: false };\n let point2_1 = EmbeddedCurvePoint { x: point2.x, y: point2.y, is_infinite: false };\n embedded_curve_add_unsafe(point1_1, point2_1)\n}\n\n/// Unsafe ec addition\n/// If the inputs are the same, it will perform a doubling, but only if point1 and point2 are the same variable.\n/// If they have the same value but are different variables, the result will be incorrect because in this case\n/// it assumes (but does not check) that the points' x-coordinates are not equal.\n/// It also assumes neither point is the infinity point.\npub fn embedded_curve_add_unsafe(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n embedded_curve_add_array_return(point1, point2)[0]\n}\n", diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/regression_5045/execute__tests__force_brillig_false_inliner_-9223372036854775808.snap b/tooling/nargo_cli/tests/snapshots/execution_success/regression_5045/execute__tests__force_brillig_false_inliner_-9223372036854775808.snap index 61823158262..3ab64605154 100644 --- a/tooling/nargo_cli/tests/snapshots/execution_success/regression_5045/execute__tests__force_brillig_false_inliner_-9223372036854775808.snap +++ b/tooling/nargo_cli/tests/snapshots/execution_success/regression_5045/execute__tests__force_brillig_false_inliner_-9223372036854775808.snap @@ -20,24 +20,25 @@ expression: artifact }, "bytecode": [ "func 0", - "current witness index : _11", + "current witness index : _12", "private parameters indices : [_0]", "public parameters indices : []", "return value indices : []", "BLACKBOX::RANGE [(_0, 1)] []", "EXPR [ (-1, _0) (-1, _1) 1 ]", "EXPR [ (-17631683881184975370165255887551781615748388533673675138855, _0) (-1, _2) 17631683881184975370165255887551781615748388533673675138860 ]", - "BLACKBOX::EMBEDDED_CURVE_ADD [(_1, 254), (_2, 254), (0, 1), (_1, 254), (_2, 254), (0, 1)] [_3, _4, _5]", - "BLACKBOX::MULTI_SCALAR_MUL [(-8519034168028805793603472410045416908800114122389094750979358290384607299995, 254), (2726875754519434671146873023426441956600113087238248464305840046775215989920, 254), (_1, 1), (0, 254), (5, 254), (_1, 1), (1, 254), (0, 254), (1, 254), (0, 254)] [_6, _7, _8]", - "EXPR [ (-1, _3) (1, _6) (-1, _9) 0 ]", - "BRILLIG CALL func 0: inputs: [Single(Expression { mul_terms: [], linear_combinations: [(1, Witness(9))], q_c: 0 })], outputs: [Simple(Witness(10))]", - "EXPR [ (1, _9, _10) (1, _11) -1 ]", - "EXPR [ (1, _9, _11) 0 ]", - "EXPR [ (1, _0, _11) 0 ]", + "EXPR [ (-1, _3) 0 ]", + "BLACKBOX::EMBEDDED_CURVE_ADD [(_1, 254), (_2, 254), (_3, 1), (_1, 254), (_2, 254), (_3, 1)] [_4, _5, _6]", + "BLACKBOX::MULTI_SCALAR_MUL [(-8519034168028805793603472410045416908800114122389094750979358290384607299995, 254), (2726875754519434671146873023426441956600113087238248464305840046775215989920, 254), (_1, 1), (0, 254), (5, 254), (_1, 1), (1, 254), (0, 254), (1, 254), (0, 254)] [_7, _8, _9]", + "EXPR [ (-1, _4) (1, _7) (-1, _10) 0 ]", + "BRILLIG CALL func 0: inputs: [Single(Expression { mul_terms: [], linear_combinations: [(1, Witness(10))], q_c: 0 })], outputs: [Simple(Witness(11))]", + "EXPR [ (1, _10, _11) (1, _12) -1 ]", + "EXPR [ (1, _10, _12) 0 ]", + "EXPR [ (1, _0, _12) 0 ]", "unconstrained func 0", "[Const { destination: Direct(21), bit_size: Integer(U32), value: 1 }, Const { destination: Direct(20), bit_size: Integer(U32), value: 0 }, CalldataCopy { destination_address: Direct(0), size_address: Direct(21), offset_address: Direct(20) }, Const { destination: Direct(2), bit_size: Field, value: 0 }, BinaryFieldOp { destination: Direct(3), op: Equals, lhs: Direct(0), rhs: Direct(2) }, JumpIf { condition: Direct(3), location: 8 }, Const { destination: Direct(1), bit_size: Field, value: 1 }, BinaryFieldOp { destination: Direct(0), op: Div, lhs: Direct(1), rhs: Direct(0) }, Stop { return_data: HeapVector { pointer: Direct(20), size: Direct(21) } }]" ], - "debug_symbols": "rVTLboQgFP0X1i54q/MrTWNQcUJC0DDapDH+e68odlxg2slsOMDlHO6Dy4xaXU/3yriuf6Dbx4xqb6w198r2jRpN72B3XjIUl9XotYYt9GQH1qC8diO6ucnaDH0pO4VDj0G5gKPyYMUZ0q4FBMHOWL3OluyXjdNULulO5jk96OLMJ2m+pGTnS0EOPpEnPk3zCyyiAwUu85QCSysQQnG+S8Bc8Fe8YDiGUTBOUwriDV78QyOZjYt6Sn7UgyfrefUeSnrUU6b45QVflDw+KMlxKoI/K7BXcpCzGEPBTjF8wko1xp+6EBE4mCEaRhZGDtfBBQIA0iE3yDcoNihXWFYnvFG11Xs/d5Nrntp7/B6iJX4Ag+8b3U5er04EG7j1Aw==", + "debug_symbols": "rVTLboQgFP0X1i54q/MrTWNQcUJC0DDapDH+e68odlxg2slsOMDlHO6Dy4xaXU/3yriuf6Dbx4xqb6w198r2jRpN72B3XjIUl9XotYYt9GQH1qC8diO6ucnaDH0pO4VDj0G5gKPyYMUZ0q4FBMHOWL3OluyXjdNULulO5jk96OLMJ2m+pGTnS0EOPpEnPk3zCyyiAwUu85QCSysQQnG+S8Bc8Fe8YDiGUTBOUwriDV78QyOZjYt6Sn7UgyfrefUeSnrUU6b45QVflDw+KMlxKoI/K7BXcpCzGEPBTjF8wko1xp+6EBE4mCEaRhZGHkYBl8I1EgCSkm9QbFBuQPCKy+qLN6q2em/rbnLNU5eP30O0xH9g8H2j28nr1ZdgA+9+AA==", "file_map": { "16": { "source": "use crate::cmp::Eq;\nuse crate::hash::Hash;\nuse crate::ops::arith::{Add, Neg, Sub};\n\n/// A point on the embedded elliptic curve\n/// By definition, the base field of the embedded curve is the scalar field of the proof system curve, i.e the Noir Field.\n/// x and y denotes the Weierstrass coordinates of the point, if is_infinite is false.\npub struct EmbeddedCurvePoint {\n pub x: Field,\n pub y: Field,\n pub is_infinite: bool,\n}\n\nimpl EmbeddedCurvePoint {\n /// Elliptic curve point doubling operation\n /// returns the doubled point of a point P, i.e P+P\n pub fn double(self) -> EmbeddedCurvePoint {\n embedded_curve_add(self, self)\n }\n\n /// Returns the null element of the curve; 'the point at infinity'\n pub fn point_at_infinity() -> EmbeddedCurvePoint {\n EmbeddedCurvePoint { x: 0, y: 0, is_infinite: true }\n }\n\n /// Returns the curve's generator point.\n pub fn generator() -> EmbeddedCurvePoint {\n // Generator point for the grumpkin curve (y^2 = x^3 - 17)\n EmbeddedCurvePoint {\n x: 1,\n y: 17631683881184975370165255887551781615748388533673675138860, // sqrt(-16)\n is_infinite: false,\n }\n }\n}\n\nimpl Add for EmbeddedCurvePoint {\n /// Adds two points P+Q, using the curve addition formula, and also handles point at infinity\n fn add(self, other: EmbeddedCurvePoint) -> EmbeddedCurvePoint {\n embedded_curve_add(self, other)\n }\n}\n\nimpl Sub for EmbeddedCurvePoint {\n /// Points subtraction operation, using addition and negation\n fn sub(self, other: EmbeddedCurvePoint) -> EmbeddedCurvePoint {\n self + other.neg()\n }\n}\n\nimpl Neg for EmbeddedCurvePoint {\n /// Negates a point P, i.e returns -P, by negating the y coordinate.\n /// If the point is at infinity, then the result is also at infinity.\n fn neg(self) -> EmbeddedCurvePoint {\n EmbeddedCurvePoint { x: self.x, y: -self.y, is_infinite: self.is_infinite }\n }\n}\n\nimpl Eq for EmbeddedCurvePoint {\n /// Checks whether two points are equal\n fn eq(self: Self, b: EmbeddedCurvePoint) -> bool {\n (self.is_infinite & b.is_infinite)\n | ((self.is_infinite == b.is_infinite) & (self.x == b.x) & (self.y == b.y))\n }\n}\n\nimpl Hash for EmbeddedCurvePoint {\n fn hash(self, state: &mut H)\n where\n H: crate::hash::Hasher,\n {\n if self.is_infinite {\n self.is_infinite.hash(state);\n } else {\n self.x.hash(state);\n self.y.hash(state);\n }\n }\n}\n\n/// Scalar for the embedded curve represented as low and high limbs\n/// By definition, the scalar field of the embedded curve is base field of the proving system curve.\n/// It may not fit into a Field element, so it is represented with two Field elements; its low and high limbs.\npub struct EmbeddedCurveScalar {\n pub lo: Field,\n pub hi: Field,\n}\n\nimpl EmbeddedCurveScalar {\n pub fn new(lo: Field, hi: Field) -> Self {\n EmbeddedCurveScalar { lo, hi }\n }\n\n #[field(bn254)]\n pub fn from_field(scalar: Field) -> EmbeddedCurveScalar {\n let (a, b) = crate::field::bn254::decompose(scalar);\n EmbeddedCurveScalar { lo: a, hi: b }\n }\n\n //Bytes to scalar: take the first (after the specified offset) 16 bytes of the input as the lo value, and the next 16 bytes as the hi value\n #[field(bn254)]\n pub(crate) fn from_bytes(bytes: [u8; 64], offset: u32) -> EmbeddedCurveScalar {\n let mut v = 1;\n let mut lo = 0 as Field;\n let mut hi = 0 as Field;\n for i in 0..16 {\n lo = lo + (bytes[offset + 31 - i] as Field) * v;\n hi = hi + (bytes[offset + 15 - i] as Field) * v;\n v = v * 256;\n }\n let sig_s = crate::embedded_curve_ops::EmbeddedCurveScalar { lo, hi };\n sig_s\n }\n}\n\nimpl Eq for EmbeddedCurveScalar {\n fn eq(self, other: Self) -> bool {\n (other.hi == self.hi) & (other.lo == self.lo)\n }\n}\n\nimpl Hash for EmbeddedCurveScalar {\n fn hash(self, state: &mut H)\n where\n H: crate::hash::Hasher,\n {\n self.hi.hash(state);\n self.lo.hash(state);\n }\n}\n\n// Computes a multi scalar multiplication over the embedded curve.\n// For bn254, We have Grumpkin and Baby JubJub.\n// For bls12-381, we have JubJub and Bandersnatch.\n//\n// The embedded curve being used is decided by the\n// underlying proof system.\n// docs:start:multi_scalar_mul\npub fn multi_scalar_mul(\n points: [EmbeddedCurvePoint; N],\n scalars: [EmbeddedCurveScalar; N],\n) -> EmbeddedCurvePoint\n// docs:end:multi_scalar_mul\n{\n multi_scalar_mul_array_return(points, scalars)[0]\n}\n\n#[foreign(multi_scalar_mul)]\npub(crate) fn multi_scalar_mul_array_return(\n points: [EmbeddedCurvePoint; N],\n scalars: [EmbeddedCurveScalar; N],\n) -> [EmbeddedCurvePoint; 1] {}\n\n// docs:start:fixed_base_scalar_mul\npub fn fixed_base_scalar_mul(scalar: EmbeddedCurveScalar) -> EmbeddedCurvePoint\n// docs:end:fixed_base_scalar_mul\n{\n multi_scalar_mul([EmbeddedCurvePoint::generator()], [scalar])\n}\n\n/// This function only assumes that the points are on the curve\n/// It handles corner cases around the infinity point causing some overhead compared to embedded_curve_add_not_nul and embedded_curve_add_unsafe\n// docs:start:embedded_curve_add\npub fn embedded_curve_add(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n // docs:end:embedded_curve_add\n if crate::runtime::is_unconstrained() {\n // `embedded_curve_add_unsafe` requires the inputs not to be the infinity point, so we check it here.\n // This is because `embedded_curve_add_unsafe` uses the `embedded_curve_add` opcode.\n // For efficiency, the backend does not check the inputs for the infinity point, but it assumes that they are not the infinity point\n // so that it can apply the ec addition formula directly.\n if point1.is_infinite {\n point2\n } else if point2.is_infinite {\n point1\n } else {\n embedded_curve_add_unsafe(point1, point2)\n }\n } else {\n // In a constrained context, we also need to check the inputs are not the infinity point because we also use `embedded_curve_add_unsafe`\n // However we also need to identify the case where the two inputs are the same, because then\n // the addition formula does not work and we need to use the doubling formula instead.\n // In unconstrained context, we can check directly if the input values are the same when solving the opcode, so it is not an issue.\n\n // x_coordinates_match is true if both abscissae are the same\n let x_coordinates_match = point1.x == point2.x;\n // y_coordinates_match is true if both ordinates are the same\n let y_coordinates_match = point1.y == point2.y;\n // double_predicate is true if both abscissae and ordinates are the same\n let double_predicate = (x_coordinates_match & y_coordinates_match);\n // If the abscissae are the same, but not the ordinates, then one point is the opposite of the other\n let infinity_predicate = (x_coordinates_match & !y_coordinates_match);\n let point1_1 = EmbeddedCurvePoint {\n x: point1.x + (x_coordinates_match as Field),\n y: point1.y,\n is_infinite: false,\n };\n let point2_1 = EmbeddedCurvePoint { x: point2.x, y: point2.y, is_infinite: false };\n // point1_1 is guaranteed to have a different abscissa than point2:\n // - if x_coordinates_match is 0, that means point1.x != point2.x, and point1_1.x = point1.x + 0\n // - if x_coordinates_match is 1, that means point1.x = point2.x, but point1_1.x = point1.x + 1 in this case\n // Because the abscissa is different, the addition formula is guaranteed to succeed, so we can safely use `embedded_curve_add_unsafe`\n // Note that this computation may be garbage: if x_coordinates_match is 1, or if one of the input is the point at infinity.\n let mut result = embedded_curve_add_unsafe(point1_1, point2_1);\n\n // `embedded_curve_add_unsafe` is doing a doubling if the input is the same variable, because in this case it is guaranteed (at 'compile time') that the input is the same.\n let double = embedded_curve_add_unsafe(point1, point1);\n // `embedded_curve_add_unsafe` would not perform doubling, even if the inputs point1 and point2 are the same, because it cannot know this without adding some logic (and some constraints)\n // However we did this logic when we computed `double_predicate`, so we set the result to 2*point1 if point1 and point2 are the same\n result = if double_predicate { double } else { result };\n\n // Same logic as above for unconstrained context, we set the proper result when one of the inputs is the infinity point\n if point1.is_infinite {\n result = point2;\n }\n if point2.is_infinite {\n result = point1;\n }\n\n // Finally, we set the is_infinity flag of the result:\n // Opposite points should sum into the infinity point, however, if one of them is point at infinity, their coordinates are not meaningful\n // so we should not use the fact that the inputs are opposite in this case:\n let mut result_is_infinity =\n infinity_predicate & (!point1.is_infinite & !point2.is_infinite);\n // However, if both of them are at infinity, then the result is also at infinity\n result.is_infinite = result_is_infinity | (point1.is_infinite & point2.is_infinite);\n result\n }\n}\n\n#[foreign(embedded_curve_add)]\nfn embedded_curve_add_array_return(\n _point1: EmbeddedCurvePoint,\n _point2: EmbeddedCurvePoint,\n) -> [EmbeddedCurvePoint; 1] {}\n\n/// This function assumes that:\n/// The points are on the curve, and\n/// The points don't share an x-coordinate, and\n/// Neither point is the infinity point.\n/// If it is used with correct input, the function ensures the correct non-zero result is returned.\n/// Except for points on the curve, the other assumptions are checked by the function. It will cause assertion failure if they are not respected.\npub fn embedded_curve_add_not_nul(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n assert(point1.x != point2.x);\n assert(!point1.is_infinite);\n assert(!point2.is_infinite);\n // Ensure is_infinite is comptime\n let point1_1 = EmbeddedCurvePoint { x: point1.x, y: point1.y, is_infinite: false };\n let point2_1 = EmbeddedCurvePoint { x: point2.x, y: point2.y, is_infinite: false };\n embedded_curve_add_unsafe(point1_1, point2_1)\n}\n\n/// Unsafe ec addition\n/// If the inputs are the same, it will perform a doubling, but only if point1 and point2 are the same variable.\n/// If they have the same value but are different variables, the result will be incorrect because in this case\n/// it assumes (but does not check) that the points' x-coordinates are not equal.\n/// It also assumes neither point is the infinity point.\npub fn embedded_curve_add_unsafe(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n embedded_curve_add_array_return(point1, point2)[0]\n}\n", diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/regression_5045/execute__tests__force_brillig_false_inliner_0.snap b/tooling/nargo_cli/tests/snapshots/execution_success/regression_5045/execute__tests__force_brillig_false_inliner_0.snap index 61823158262..3ab64605154 100644 --- a/tooling/nargo_cli/tests/snapshots/execution_success/regression_5045/execute__tests__force_brillig_false_inliner_0.snap +++ b/tooling/nargo_cli/tests/snapshots/execution_success/regression_5045/execute__tests__force_brillig_false_inliner_0.snap @@ -20,24 +20,25 @@ expression: artifact }, "bytecode": [ "func 0", - "current witness index : _11", + "current witness index : _12", "private parameters indices : [_0]", "public parameters indices : []", "return value indices : []", "BLACKBOX::RANGE [(_0, 1)] []", "EXPR [ (-1, _0) (-1, _1) 1 ]", "EXPR [ (-17631683881184975370165255887551781615748388533673675138855, _0) (-1, _2) 17631683881184975370165255887551781615748388533673675138860 ]", - "BLACKBOX::EMBEDDED_CURVE_ADD [(_1, 254), (_2, 254), (0, 1), (_1, 254), (_2, 254), (0, 1)] [_3, _4, _5]", - "BLACKBOX::MULTI_SCALAR_MUL [(-8519034168028805793603472410045416908800114122389094750979358290384607299995, 254), (2726875754519434671146873023426441956600113087238248464305840046775215989920, 254), (_1, 1), (0, 254), (5, 254), (_1, 1), (1, 254), (0, 254), (1, 254), (0, 254)] [_6, _7, _8]", - "EXPR [ (-1, _3) (1, _6) (-1, _9) 0 ]", - "BRILLIG CALL func 0: inputs: [Single(Expression { mul_terms: [], linear_combinations: [(1, Witness(9))], q_c: 0 })], outputs: [Simple(Witness(10))]", - "EXPR [ (1, _9, _10) (1, _11) -1 ]", - "EXPR [ (1, _9, _11) 0 ]", - "EXPR [ (1, _0, _11) 0 ]", + "EXPR [ (-1, _3) 0 ]", + "BLACKBOX::EMBEDDED_CURVE_ADD [(_1, 254), (_2, 254), (_3, 1), (_1, 254), (_2, 254), (_3, 1)] [_4, _5, _6]", + "BLACKBOX::MULTI_SCALAR_MUL [(-8519034168028805793603472410045416908800114122389094750979358290384607299995, 254), (2726875754519434671146873023426441956600113087238248464305840046775215989920, 254), (_1, 1), (0, 254), (5, 254), (_1, 1), (1, 254), (0, 254), (1, 254), (0, 254)] [_7, _8, _9]", + "EXPR [ (-1, _4) (1, _7) (-1, _10) 0 ]", + "BRILLIG CALL func 0: inputs: [Single(Expression { mul_terms: [], linear_combinations: [(1, Witness(10))], q_c: 0 })], outputs: [Simple(Witness(11))]", + "EXPR [ (1, _10, _11) (1, _12) -1 ]", + "EXPR [ (1, _10, _12) 0 ]", + "EXPR [ (1, _0, _12) 0 ]", "unconstrained func 0", "[Const { destination: Direct(21), bit_size: Integer(U32), value: 1 }, Const { destination: Direct(20), bit_size: Integer(U32), value: 0 }, CalldataCopy { destination_address: Direct(0), size_address: Direct(21), offset_address: Direct(20) }, Const { destination: Direct(2), bit_size: Field, value: 0 }, BinaryFieldOp { destination: Direct(3), op: Equals, lhs: Direct(0), rhs: Direct(2) }, JumpIf { condition: Direct(3), location: 8 }, Const { destination: Direct(1), bit_size: Field, value: 1 }, BinaryFieldOp { destination: Direct(0), op: Div, lhs: Direct(1), rhs: Direct(0) }, Stop { return_data: HeapVector { pointer: Direct(20), size: Direct(21) } }]" ], - "debug_symbols": "rVTLboQgFP0X1i54q/MrTWNQcUJC0DDapDH+e68odlxg2slsOMDlHO6Dy4xaXU/3yriuf6Dbx4xqb6w198r2jRpN72B3XjIUl9XotYYt9GQH1qC8diO6ucnaDH0pO4VDj0G5gKPyYMUZ0q4FBMHOWL3OluyXjdNULulO5jk96OLMJ2m+pGTnS0EOPpEnPk3zCyyiAwUu85QCSysQQnG+S8Bc8Fe8YDiGUTBOUwriDV78QyOZjYt6Sn7UgyfrefUeSnrUU6b45QVflDw+KMlxKoI/K7BXcpCzGEPBTjF8wko1xp+6EBE4mCEaRhZGDtfBBQIA0iE3yDcoNihXWFYnvFG11Xs/d5Nrntp7/B6iJX4Ag+8b3U5er04EG7j1Aw==", + "debug_symbols": "rVTLboQgFP0X1i54q/MrTWNQcUJC0DDapDH+e68odlxg2slsOMDlHO6Dy4xaXU/3yriuf6Dbx4xqb6w198r2jRpN72B3XjIUl9XotYYt9GQH1qC8diO6ucnaDH0pO4VDj0G5gKPyYMUZ0q4FBMHOWL3OluyXjdNULulO5jk96OLMJ2m+pGTnS0EOPpEnPk3zCyyiAwUu85QCSysQQnG+S8Bc8Fe8YDiGUTBOUwriDV78QyOZjYt6Sn7UgyfrefUeSnrUU6b45QVflDw+KMlxKoI/K7BXcpCzGEPBTjF8wko1xp+6EBE4mCEaRhZGHkYBl8I1EgCSkm9QbFBuQPCKy+qLN6q2em/rbnLNU5eP30O0xH9g8H2j28nr1ZdgA+9+AA==", "file_map": { "16": { "source": "use crate::cmp::Eq;\nuse crate::hash::Hash;\nuse crate::ops::arith::{Add, Neg, Sub};\n\n/// A point on the embedded elliptic curve\n/// By definition, the base field of the embedded curve is the scalar field of the proof system curve, i.e the Noir Field.\n/// x and y denotes the Weierstrass coordinates of the point, if is_infinite is false.\npub struct EmbeddedCurvePoint {\n pub x: Field,\n pub y: Field,\n pub is_infinite: bool,\n}\n\nimpl EmbeddedCurvePoint {\n /// Elliptic curve point doubling operation\n /// returns the doubled point of a point P, i.e P+P\n pub fn double(self) -> EmbeddedCurvePoint {\n embedded_curve_add(self, self)\n }\n\n /// Returns the null element of the curve; 'the point at infinity'\n pub fn point_at_infinity() -> EmbeddedCurvePoint {\n EmbeddedCurvePoint { x: 0, y: 0, is_infinite: true }\n }\n\n /// Returns the curve's generator point.\n pub fn generator() -> EmbeddedCurvePoint {\n // Generator point for the grumpkin curve (y^2 = x^3 - 17)\n EmbeddedCurvePoint {\n x: 1,\n y: 17631683881184975370165255887551781615748388533673675138860, // sqrt(-16)\n is_infinite: false,\n }\n }\n}\n\nimpl Add for EmbeddedCurvePoint {\n /// Adds two points P+Q, using the curve addition formula, and also handles point at infinity\n fn add(self, other: EmbeddedCurvePoint) -> EmbeddedCurvePoint {\n embedded_curve_add(self, other)\n }\n}\n\nimpl Sub for EmbeddedCurvePoint {\n /// Points subtraction operation, using addition and negation\n fn sub(self, other: EmbeddedCurvePoint) -> EmbeddedCurvePoint {\n self + other.neg()\n }\n}\n\nimpl Neg for EmbeddedCurvePoint {\n /// Negates a point P, i.e returns -P, by negating the y coordinate.\n /// If the point is at infinity, then the result is also at infinity.\n fn neg(self) -> EmbeddedCurvePoint {\n EmbeddedCurvePoint { x: self.x, y: -self.y, is_infinite: self.is_infinite }\n }\n}\n\nimpl Eq for EmbeddedCurvePoint {\n /// Checks whether two points are equal\n fn eq(self: Self, b: EmbeddedCurvePoint) -> bool {\n (self.is_infinite & b.is_infinite)\n | ((self.is_infinite == b.is_infinite) & (self.x == b.x) & (self.y == b.y))\n }\n}\n\nimpl Hash for EmbeddedCurvePoint {\n fn hash(self, state: &mut H)\n where\n H: crate::hash::Hasher,\n {\n if self.is_infinite {\n self.is_infinite.hash(state);\n } else {\n self.x.hash(state);\n self.y.hash(state);\n }\n }\n}\n\n/// Scalar for the embedded curve represented as low and high limbs\n/// By definition, the scalar field of the embedded curve is base field of the proving system curve.\n/// It may not fit into a Field element, so it is represented with two Field elements; its low and high limbs.\npub struct EmbeddedCurveScalar {\n pub lo: Field,\n pub hi: Field,\n}\n\nimpl EmbeddedCurveScalar {\n pub fn new(lo: Field, hi: Field) -> Self {\n EmbeddedCurveScalar { lo, hi }\n }\n\n #[field(bn254)]\n pub fn from_field(scalar: Field) -> EmbeddedCurveScalar {\n let (a, b) = crate::field::bn254::decompose(scalar);\n EmbeddedCurveScalar { lo: a, hi: b }\n }\n\n //Bytes to scalar: take the first (after the specified offset) 16 bytes of the input as the lo value, and the next 16 bytes as the hi value\n #[field(bn254)]\n pub(crate) fn from_bytes(bytes: [u8; 64], offset: u32) -> EmbeddedCurveScalar {\n let mut v = 1;\n let mut lo = 0 as Field;\n let mut hi = 0 as Field;\n for i in 0..16 {\n lo = lo + (bytes[offset + 31 - i] as Field) * v;\n hi = hi + (bytes[offset + 15 - i] as Field) * v;\n v = v * 256;\n }\n let sig_s = crate::embedded_curve_ops::EmbeddedCurveScalar { lo, hi };\n sig_s\n }\n}\n\nimpl Eq for EmbeddedCurveScalar {\n fn eq(self, other: Self) -> bool {\n (other.hi == self.hi) & (other.lo == self.lo)\n }\n}\n\nimpl Hash for EmbeddedCurveScalar {\n fn hash(self, state: &mut H)\n where\n H: crate::hash::Hasher,\n {\n self.hi.hash(state);\n self.lo.hash(state);\n }\n}\n\n// Computes a multi scalar multiplication over the embedded curve.\n// For bn254, We have Grumpkin and Baby JubJub.\n// For bls12-381, we have JubJub and Bandersnatch.\n//\n// The embedded curve being used is decided by the\n// underlying proof system.\n// docs:start:multi_scalar_mul\npub fn multi_scalar_mul(\n points: [EmbeddedCurvePoint; N],\n scalars: [EmbeddedCurveScalar; N],\n) -> EmbeddedCurvePoint\n// docs:end:multi_scalar_mul\n{\n multi_scalar_mul_array_return(points, scalars)[0]\n}\n\n#[foreign(multi_scalar_mul)]\npub(crate) fn multi_scalar_mul_array_return(\n points: [EmbeddedCurvePoint; N],\n scalars: [EmbeddedCurveScalar; N],\n) -> [EmbeddedCurvePoint; 1] {}\n\n// docs:start:fixed_base_scalar_mul\npub fn fixed_base_scalar_mul(scalar: EmbeddedCurveScalar) -> EmbeddedCurvePoint\n// docs:end:fixed_base_scalar_mul\n{\n multi_scalar_mul([EmbeddedCurvePoint::generator()], [scalar])\n}\n\n/// This function only assumes that the points are on the curve\n/// It handles corner cases around the infinity point causing some overhead compared to embedded_curve_add_not_nul and embedded_curve_add_unsafe\n// docs:start:embedded_curve_add\npub fn embedded_curve_add(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n // docs:end:embedded_curve_add\n if crate::runtime::is_unconstrained() {\n // `embedded_curve_add_unsafe` requires the inputs not to be the infinity point, so we check it here.\n // This is because `embedded_curve_add_unsafe` uses the `embedded_curve_add` opcode.\n // For efficiency, the backend does not check the inputs for the infinity point, but it assumes that they are not the infinity point\n // so that it can apply the ec addition formula directly.\n if point1.is_infinite {\n point2\n } else if point2.is_infinite {\n point1\n } else {\n embedded_curve_add_unsafe(point1, point2)\n }\n } else {\n // In a constrained context, we also need to check the inputs are not the infinity point because we also use `embedded_curve_add_unsafe`\n // However we also need to identify the case where the two inputs are the same, because then\n // the addition formula does not work and we need to use the doubling formula instead.\n // In unconstrained context, we can check directly if the input values are the same when solving the opcode, so it is not an issue.\n\n // x_coordinates_match is true if both abscissae are the same\n let x_coordinates_match = point1.x == point2.x;\n // y_coordinates_match is true if both ordinates are the same\n let y_coordinates_match = point1.y == point2.y;\n // double_predicate is true if both abscissae and ordinates are the same\n let double_predicate = (x_coordinates_match & y_coordinates_match);\n // If the abscissae are the same, but not the ordinates, then one point is the opposite of the other\n let infinity_predicate = (x_coordinates_match & !y_coordinates_match);\n let point1_1 = EmbeddedCurvePoint {\n x: point1.x + (x_coordinates_match as Field),\n y: point1.y,\n is_infinite: false,\n };\n let point2_1 = EmbeddedCurvePoint { x: point2.x, y: point2.y, is_infinite: false };\n // point1_1 is guaranteed to have a different abscissa than point2:\n // - if x_coordinates_match is 0, that means point1.x != point2.x, and point1_1.x = point1.x + 0\n // - if x_coordinates_match is 1, that means point1.x = point2.x, but point1_1.x = point1.x + 1 in this case\n // Because the abscissa is different, the addition formula is guaranteed to succeed, so we can safely use `embedded_curve_add_unsafe`\n // Note that this computation may be garbage: if x_coordinates_match is 1, or if one of the input is the point at infinity.\n let mut result = embedded_curve_add_unsafe(point1_1, point2_1);\n\n // `embedded_curve_add_unsafe` is doing a doubling if the input is the same variable, because in this case it is guaranteed (at 'compile time') that the input is the same.\n let double = embedded_curve_add_unsafe(point1, point1);\n // `embedded_curve_add_unsafe` would not perform doubling, even if the inputs point1 and point2 are the same, because it cannot know this without adding some logic (and some constraints)\n // However we did this logic when we computed `double_predicate`, so we set the result to 2*point1 if point1 and point2 are the same\n result = if double_predicate { double } else { result };\n\n // Same logic as above for unconstrained context, we set the proper result when one of the inputs is the infinity point\n if point1.is_infinite {\n result = point2;\n }\n if point2.is_infinite {\n result = point1;\n }\n\n // Finally, we set the is_infinity flag of the result:\n // Opposite points should sum into the infinity point, however, if one of them is point at infinity, their coordinates are not meaningful\n // so we should not use the fact that the inputs are opposite in this case:\n let mut result_is_infinity =\n infinity_predicate & (!point1.is_infinite & !point2.is_infinite);\n // However, if both of them are at infinity, then the result is also at infinity\n result.is_infinite = result_is_infinity | (point1.is_infinite & point2.is_infinite);\n result\n }\n}\n\n#[foreign(embedded_curve_add)]\nfn embedded_curve_add_array_return(\n _point1: EmbeddedCurvePoint,\n _point2: EmbeddedCurvePoint,\n) -> [EmbeddedCurvePoint; 1] {}\n\n/// This function assumes that:\n/// The points are on the curve, and\n/// The points don't share an x-coordinate, and\n/// Neither point is the infinity point.\n/// If it is used with correct input, the function ensures the correct non-zero result is returned.\n/// Except for points on the curve, the other assumptions are checked by the function. It will cause assertion failure if they are not respected.\npub fn embedded_curve_add_not_nul(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n assert(point1.x != point2.x);\n assert(!point1.is_infinite);\n assert(!point2.is_infinite);\n // Ensure is_infinite is comptime\n let point1_1 = EmbeddedCurvePoint { x: point1.x, y: point1.y, is_infinite: false };\n let point2_1 = EmbeddedCurvePoint { x: point2.x, y: point2.y, is_infinite: false };\n embedded_curve_add_unsafe(point1_1, point2_1)\n}\n\n/// Unsafe ec addition\n/// If the inputs are the same, it will perform a doubling, but only if point1 and point2 are the same variable.\n/// If they have the same value but are different variables, the result will be incorrect because in this case\n/// it assumes (but does not check) that the points' x-coordinates are not equal.\n/// It also assumes neither point is the infinity point.\npub fn embedded_curve_add_unsafe(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n embedded_curve_add_array_return(point1, point2)[0]\n}\n", diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/regression_5045/execute__tests__force_brillig_false_inliner_9223372036854775807.snap b/tooling/nargo_cli/tests/snapshots/execution_success/regression_5045/execute__tests__force_brillig_false_inliner_9223372036854775807.snap index 61823158262..3ab64605154 100644 --- a/tooling/nargo_cli/tests/snapshots/execution_success/regression_5045/execute__tests__force_brillig_false_inliner_9223372036854775807.snap +++ b/tooling/nargo_cli/tests/snapshots/execution_success/regression_5045/execute__tests__force_brillig_false_inliner_9223372036854775807.snap @@ -20,24 +20,25 @@ expression: artifact }, "bytecode": [ "func 0", - "current witness index : _11", + "current witness index : _12", "private parameters indices : [_0]", "public parameters indices : []", "return value indices : []", "BLACKBOX::RANGE [(_0, 1)] []", "EXPR [ (-1, _0) (-1, _1) 1 ]", "EXPR [ (-17631683881184975370165255887551781615748388533673675138855, _0) (-1, _2) 17631683881184975370165255887551781615748388533673675138860 ]", - "BLACKBOX::EMBEDDED_CURVE_ADD [(_1, 254), (_2, 254), (0, 1), (_1, 254), (_2, 254), (0, 1)] [_3, _4, _5]", - "BLACKBOX::MULTI_SCALAR_MUL [(-8519034168028805793603472410045416908800114122389094750979358290384607299995, 254), (2726875754519434671146873023426441956600113087238248464305840046775215989920, 254), (_1, 1), (0, 254), (5, 254), (_1, 1), (1, 254), (0, 254), (1, 254), (0, 254)] [_6, _7, _8]", - "EXPR [ (-1, _3) (1, _6) (-1, _9) 0 ]", - "BRILLIG CALL func 0: inputs: [Single(Expression { mul_terms: [], linear_combinations: [(1, Witness(9))], q_c: 0 })], outputs: [Simple(Witness(10))]", - "EXPR [ (1, _9, _10) (1, _11) -1 ]", - "EXPR [ (1, _9, _11) 0 ]", - "EXPR [ (1, _0, _11) 0 ]", + "EXPR [ (-1, _3) 0 ]", + "BLACKBOX::EMBEDDED_CURVE_ADD [(_1, 254), (_2, 254), (_3, 1), (_1, 254), (_2, 254), (_3, 1)] [_4, _5, _6]", + "BLACKBOX::MULTI_SCALAR_MUL [(-8519034168028805793603472410045416908800114122389094750979358290384607299995, 254), (2726875754519434671146873023426441956600113087238248464305840046775215989920, 254), (_1, 1), (0, 254), (5, 254), (_1, 1), (1, 254), (0, 254), (1, 254), (0, 254)] [_7, _8, _9]", + "EXPR [ (-1, _4) (1, _7) (-1, _10) 0 ]", + "BRILLIG CALL func 0: inputs: [Single(Expression { mul_terms: [], linear_combinations: [(1, Witness(10))], q_c: 0 })], outputs: [Simple(Witness(11))]", + "EXPR [ (1, _10, _11) (1, _12) -1 ]", + "EXPR [ (1, _10, _12) 0 ]", + "EXPR [ (1, _0, _12) 0 ]", "unconstrained func 0", "[Const { destination: Direct(21), bit_size: Integer(U32), value: 1 }, Const { destination: Direct(20), bit_size: Integer(U32), value: 0 }, CalldataCopy { destination_address: Direct(0), size_address: Direct(21), offset_address: Direct(20) }, Const { destination: Direct(2), bit_size: Field, value: 0 }, BinaryFieldOp { destination: Direct(3), op: Equals, lhs: Direct(0), rhs: Direct(2) }, JumpIf { condition: Direct(3), location: 8 }, Const { destination: Direct(1), bit_size: Field, value: 1 }, BinaryFieldOp { destination: Direct(0), op: Div, lhs: Direct(1), rhs: Direct(0) }, Stop { return_data: HeapVector { pointer: Direct(20), size: Direct(21) } }]" ], - "debug_symbols": "rVTLboQgFP0X1i54q/MrTWNQcUJC0DDapDH+e68odlxg2slsOMDlHO6Dy4xaXU/3yriuf6Dbx4xqb6w198r2jRpN72B3XjIUl9XotYYt9GQH1qC8diO6ucnaDH0pO4VDj0G5gKPyYMUZ0q4FBMHOWL3OluyXjdNULulO5jk96OLMJ2m+pGTnS0EOPpEnPk3zCyyiAwUu85QCSysQQnG+S8Bc8Fe8YDiGUTBOUwriDV78QyOZjYt6Sn7UgyfrefUeSnrUU6b45QVflDw+KMlxKoI/K7BXcpCzGEPBTjF8wko1xp+6EBE4mCEaRhZGDtfBBQIA0iE3yDcoNihXWFYnvFG11Xs/d5Nrntp7/B6iJX4Ag+8b3U5er04EG7j1Aw==", + "debug_symbols": "rVTLboQgFP0X1i54q/MrTWNQcUJC0DDapDH+e68odlxg2slsOMDlHO6Dy4xaXU/3yriuf6Dbx4xqb6w198r2jRpN72B3XjIUl9XotYYt9GQH1qC8diO6ucnaDH0pO4VDj0G5gKPyYMUZ0q4FBMHOWL3OluyXjdNULulO5jk96OLMJ2m+pGTnS0EOPpEnPk3zCyyiAwUu85QCSysQQnG+S8Bc8Fe8YDiGUTBOUwriDV78QyOZjYt6Sn7UgyfrefUeSnrUU6b45QVflDw+KMlxKoI/K7BXcpCzGEPBTjF8wko1xp+6EBE4mCEaRhZGHkYBl8I1EgCSkm9QbFBuQPCKy+qLN6q2em/rbnLNU5eP30O0xH9g8H2j28nr1ZdgA+9+AA==", "file_map": { "16": { "source": "use crate::cmp::Eq;\nuse crate::hash::Hash;\nuse crate::ops::arith::{Add, Neg, Sub};\n\n/// A point on the embedded elliptic curve\n/// By definition, the base field of the embedded curve is the scalar field of the proof system curve, i.e the Noir Field.\n/// x and y denotes the Weierstrass coordinates of the point, if is_infinite is false.\npub struct EmbeddedCurvePoint {\n pub x: Field,\n pub y: Field,\n pub is_infinite: bool,\n}\n\nimpl EmbeddedCurvePoint {\n /// Elliptic curve point doubling operation\n /// returns the doubled point of a point P, i.e P+P\n pub fn double(self) -> EmbeddedCurvePoint {\n embedded_curve_add(self, self)\n }\n\n /// Returns the null element of the curve; 'the point at infinity'\n pub fn point_at_infinity() -> EmbeddedCurvePoint {\n EmbeddedCurvePoint { x: 0, y: 0, is_infinite: true }\n }\n\n /// Returns the curve's generator point.\n pub fn generator() -> EmbeddedCurvePoint {\n // Generator point for the grumpkin curve (y^2 = x^3 - 17)\n EmbeddedCurvePoint {\n x: 1,\n y: 17631683881184975370165255887551781615748388533673675138860, // sqrt(-16)\n is_infinite: false,\n }\n }\n}\n\nimpl Add for EmbeddedCurvePoint {\n /// Adds two points P+Q, using the curve addition formula, and also handles point at infinity\n fn add(self, other: EmbeddedCurvePoint) -> EmbeddedCurvePoint {\n embedded_curve_add(self, other)\n }\n}\n\nimpl Sub for EmbeddedCurvePoint {\n /// Points subtraction operation, using addition and negation\n fn sub(self, other: EmbeddedCurvePoint) -> EmbeddedCurvePoint {\n self + other.neg()\n }\n}\n\nimpl Neg for EmbeddedCurvePoint {\n /// Negates a point P, i.e returns -P, by negating the y coordinate.\n /// If the point is at infinity, then the result is also at infinity.\n fn neg(self) -> EmbeddedCurvePoint {\n EmbeddedCurvePoint { x: self.x, y: -self.y, is_infinite: self.is_infinite }\n }\n}\n\nimpl Eq for EmbeddedCurvePoint {\n /// Checks whether two points are equal\n fn eq(self: Self, b: EmbeddedCurvePoint) -> bool {\n (self.is_infinite & b.is_infinite)\n | ((self.is_infinite == b.is_infinite) & (self.x == b.x) & (self.y == b.y))\n }\n}\n\nimpl Hash for EmbeddedCurvePoint {\n fn hash(self, state: &mut H)\n where\n H: crate::hash::Hasher,\n {\n if self.is_infinite {\n self.is_infinite.hash(state);\n } else {\n self.x.hash(state);\n self.y.hash(state);\n }\n }\n}\n\n/// Scalar for the embedded curve represented as low and high limbs\n/// By definition, the scalar field of the embedded curve is base field of the proving system curve.\n/// It may not fit into a Field element, so it is represented with two Field elements; its low and high limbs.\npub struct EmbeddedCurveScalar {\n pub lo: Field,\n pub hi: Field,\n}\n\nimpl EmbeddedCurveScalar {\n pub fn new(lo: Field, hi: Field) -> Self {\n EmbeddedCurveScalar { lo, hi }\n }\n\n #[field(bn254)]\n pub fn from_field(scalar: Field) -> EmbeddedCurveScalar {\n let (a, b) = crate::field::bn254::decompose(scalar);\n EmbeddedCurveScalar { lo: a, hi: b }\n }\n\n //Bytes to scalar: take the first (after the specified offset) 16 bytes of the input as the lo value, and the next 16 bytes as the hi value\n #[field(bn254)]\n pub(crate) fn from_bytes(bytes: [u8; 64], offset: u32) -> EmbeddedCurveScalar {\n let mut v = 1;\n let mut lo = 0 as Field;\n let mut hi = 0 as Field;\n for i in 0..16 {\n lo = lo + (bytes[offset + 31 - i] as Field) * v;\n hi = hi + (bytes[offset + 15 - i] as Field) * v;\n v = v * 256;\n }\n let sig_s = crate::embedded_curve_ops::EmbeddedCurveScalar { lo, hi };\n sig_s\n }\n}\n\nimpl Eq for EmbeddedCurveScalar {\n fn eq(self, other: Self) -> bool {\n (other.hi == self.hi) & (other.lo == self.lo)\n }\n}\n\nimpl Hash for EmbeddedCurveScalar {\n fn hash(self, state: &mut H)\n where\n H: crate::hash::Hasher,\n {\n self.hi.hash(state);\n self.lo.hash(state);\n }\n}\n\n// Computes a multi scalar multiplication over the embedded curve.\n// For bn254, We have Grumpkin and Baby JubJub.\n// For bls12-381, we have JubJub and Bandersnatch.\n//\n// The embedded curve being used is decided by the\n// underlying proof system.\n// docs:start:multi_scalar_mul\npub fn multi_scalar_mul(\n points: [EmbeddedCurvePoint; N],\n scalars: [EmbeddedCurveScalar; N],\n) -> EmbeddedCurvePoint\n// docs:end:multi_scalar_mul\n{\n multi_scalar_mul_array_return(points, scalars)[0]\n}\n\n#[foreign(multi_scalar_mul)]\npub(crate) fn multi_scalar_mul_array_return(\n points: [EmbeddedCurvePoint; N],\n scalars: [EmbeddedCurveScalar; N],\n) -> [EmbeddedCurvePoint; 1] {}\n\n// docs:start:fixed_base_scalar_mul\npub fn fixed_base_scalar_mul(scalar: EmbeddedCurveScalar) -> EmbeddedCurvePoint\n// docs:end:fixed_base_scalar_mul\n{\n multi_scalar_mul([EmbeddedCurvePoint::generator()], [scalar])\n}\n\n/// This function only assumes that the points are on the curve\n/// It handles corner cases around the infinity point causing some overhead compared to embedded_curve_add_not_nul and embedded_curve_add_unsafe\n// docs:start:embedded_curve_add\npub fn embedded_curve_add(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n // docs:end:embedded_curve_add\n if crate::runtime::is_unconstrained() {\n // `embedded_curve_add_unsafe` requires the inputs not to be the infinity point, so we check it here.\n // This is because `embedded_curve_add_unsafe` uses the `embedded_curve_add` opcode.\n // For efficiency, the backend does not check the inputs for the infinity point, but it assumes that they are not the infinity point\n // so that it can apply the ec addition formula directly.\n if point1.is_infinite {\n point2\n } else if point2.is_infinite {\n point1\n } else {\n embedded_curve_add_unsafe(point1, point2)\n }\n } else {\n // In a constrained context, we also need to check the inputs are not the infinity point because we also use `embedded_curve_add_unsafe`\n // However we also need to identify the case where the two inputs are the same, because then\n // the addition formula does not work and we need to use the doubling formula instead.\n // In unconstrained context, we can check directly if the input values are the same when solving the opcode, so it is not an issue.\n\n // x_coordinates_match is true if both abscissae are the same\n let x_coordinates_match = point1.x == point2.x;\n // y_coordinates_match is true if both ordinates are the same\n let y_coordinates_match = point1.y == point2.y;\n // double_predicate is true if both abscissae and ordinates are the same\n let double_predicate = (x_coordinates_match & y_coordinates_match);\n // If the abscissae are the same, but not the ordinates, then one point is the opposite of the other\n let infinity_predicate = (x_coordinates_match & !y_coordinates_match);\n let point1_1 = EmbeddedCurvePoint {\n x: point1.x + (x_coordinates_match as Field),\n y: point1.y,\n is_infinite: false,\n };\n let point2_1 = EmbeddedCurvePoint { x: point2.x, y: point2.y, is_infinite: false };\n // point1_1 is guaranteed to have a different abscissa than point2:\n // - if x_coordinates_match is 0, that means point1.x != point2.x, and point1_1.x = point1.x + 0\n // - if x_coordinates_match is 1, that means point1.x = point2.x, but point1_1.x = point1.x + 1 in this case\n // Because the abscissa is different, the addition formula is guaranteed to succeed, so we can safely use `embedded_curve_add_unsafe`\n // Note that this computation may be garbage: if x_coordinates_match is 1, or if one of the input is the point at infinity.\n let mut result = embedded_curve_add_unsafe(point1_1, point2_1);\n\n // `embedded_curve_add_unsafe` is doing a doubling if the input is the same variable, because in this case it is guaranteed (at 'compile time') that the input is the same.\n let double = embedded_curve_add_unsafe(point1, point1);\n // `embedded_curve_add_unsafe` would not perform doubling, even if the inputs point1 and point2 are the same, because it cannot know this without adding some logic (and some constraints)\n // However we did this logic when we computed `double_predicate`, so we set the result to 2*point1 if point1 and point2 are the same\n result = if double_predicate { double } else { result };\n\n // Same logic as above for unconstrained context, we set the proper result when one of the inputs is the infinity point\n if point1.is_infinite {\n result = point2;\n }\n if point2.is_infinite {\n result = point1;\n }\n\n // Finally, we set the is_infinity flag of the result:\n // Opposite points should sum into the infinity point, however, if one of them is point at infinity, their coordinates are not meaningful\n // so we should not use the fact that the inputs are opposite in this case:\n let mut result_is_infinity =\n infinity_predicate & (!point1.is_infinite & !point2.is_infinite);\n // However, if both of them are at infinity, then the result is also at infinity\n result.is_infinite = result_is_infinity | (point1.is_infinite & point2.is_infinite);\n result\n }\n}\n\n#[foreign(embedded_curve_add)]\nfn embedded_curve_add_array_return(\n _point1: EmbeddedCurvePoint,\n _point2: EmbeddedCurvePoint,\n) -> [EmbeddedCurvePoint; 1] {}\n\n/// This function assumes that:\n/// The points are on the curve, and\n/// The points don't share an x-coordinate, and\n/// Neither point is the infinity point.\n/// If it is used with correct input, the function ensures the correct non-zero result is returned.\n/// Except for points on the curve, the other assumptions are checked by the function. It will cause assertion failure if they are not respected.\npub fn embedded_curve_add_not_nul(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n assert(point1.x != point2.x);\n assert(!point1.is_infinite);\n assert(!point2.is_infinite);\n // Ensure is_infinite is comptime\n let point1_1 = EmbeddedCurvePoint { x: point1.x, y: point1.y, is_infinite: false };\n let point2_1 = EmbeddedCurvePoint { x: point2.x, y: point2.y, is_infinite: false };\n embedded_curve_add_unsafe(point1_1, point2_1)\n}\n\n/// Unsafe ec addition\n/// If the inputs are the same, it will perform a doubling, but only if point1 and point2 are the same variable.\n/// If they have the same value but are different variables, the result will be incorrect because in this case\n/// it assumes (but does not check) that the points' x-coordinates are not equal.\n/// It also assumes neither point is the infinity point.\npub fn embedded_curve_add_unsafe(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n embedded_curve_add_array_return(point1, point2)[0]\n}\n", diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/regression_7744/execute__tests__force_brillig_false_inliner_-9223372036854775808.snap b/tooling/nargo_cli/tests/snapshots/execution_success/regression_7744/execute__tests__force_brillig_false_inliner_-9223372036854775808.snap index 4dc671c96da..aa5de57031e 100644 --- a/tooling/nargo_cli/tests/snapshots/execution_success/regression_7744/execute__tests__force_brillig_false_inliner_-9223372036854775808.snap +++ b/tooling/nargo_cli/tests/snapshots/execution_success/regression_7744/execute__tests__force_brillig_false_inliner_-9223372036854775808.snap @@ -46,19 +46,20 @@ expression: artifact }, "bytecode": [ "func 0", - "current witness index : _8", + "current witness index : _9", "private parameters indices : [_0]", "public parameters indices : []", "return value indices : [_1, _2, _3]", "BLACKBOX::RANGE [(_0, 1)] []", "EXPR [ (-1, _0) (-1, _4) 1 ]", "EXPR [ (-17631683881184975370165255887551781615748388533673675138855, _0) (-1, _5) 17631683881184975370165255887551781615748388533673675138860 ]", - "BLACKBOX::EMBEDDED_CURVE_ADD [(_4, 254), (_5, 254), (0, 1), (_4, 254), (_5, 254), (0, 1)] [_6, _7, _8]", - "EXPR [ (-1, _0, _6) (1, _1) 0 ]", - "EXPR [ (-1, _0, _7) (1, _2) (-5, _4) 0 ]", - "EXPR [ (-1, _0, _8) (1, _3) 0 ]" + "EXPR [ (-1, _6) 0 ]", + "BLACKBOX::EMBEDDED_CURVE_ADD [(_4, 254), (_5, 254), (_6, 1), (_4, 254), (_5, 254), (_6, 1)] [_7, _8, _9]", + "EXPR [ (-1, _0, _7) (1, _1) 0 ]", + "EXPR [ (-1, _0, _8) (1, _2) (-5, _4) 0 ]", + "EXPR [ (-1, _0, _9) (1, _3) 0 ]" ], - "debug_symbols": "nZFNDoMgEIXvMmsWom2NXqVpDOJoSAgQhCaN8e4diVZduOlm/h7vgwwTdNjGoVGmtyPUzwlar7RWQ6OtFEFZQ9NpZrC1TfCINIKDTi4nPJoAtYlaM3gLHdOh0QmTchCe1IwBmo4yAXulcalmtruza2teVau5KG4/+/3s59d+zvOsXAlU33cGf/zLKE+MF3VCKn/aHHB6OoM8xYLivOC9Eq3GdbN9NPKw6PBxm7J9hfNWYhc9Luik0WVf", + "debug_symbols": "nZHPDoMgDMbfpWcO4p8ZfZVlMajVkBAgCEsW47uvEp168LJLafvx+0rKDD22YWykHswE9XOG1kml5Ngo0wkvjabuvDDYy8Y7RGrBSSfKCofaQ62DUgzeQoV4abJCx9MLR2rCAHVPJxkOUuGaLeygk3s0raoNzrL8hxdXnt/znKdJuTlQXhwe/PGvR3nxeFElOukumwNOT2eQxpjFmFNc1iFOilbhtt8h6O60bv+xu7J/iHWmwz44XAdEjUZ+AQ==", "file_map": { "16": { "source": "use crate::cmp::Eq;\nuse crate::hash::Hash;\nuse crate::ops::arith::{Add, Neg, Sub};\n\n/// A point on the embedded elliptic curve\n/// By definition, the base field of the embedded curve is the scalar field of the proof system curve, i.e the Noir Field.\n/// x and y denotes the Weierstrass coordinates of the point, if is_infinite is false.\npub struct EmbeddedCurvePoint {\n pub x: Field,\n pub y: Field,\n pub is_infinite: bool,\n}\n\nimpl EmbeddedCurvePoint {\n /// Elliptic curve point doubling operation\n /// returns the doubled point of a point P, i.e P+P\n pub fn double(self) -> EmbeddedCurvePoint {\n embedded_curve_add(self, self)\n }\n\n /// Returns the null element of the curve; 'the point at infinity'\n pub fn point_at_infinity() -> EmbeddedCurvePoint {\n EmbeddedCurvePoint { x: 0, y: 0, is_infinite: true }\n }\n\n /// Returns the curve's generator point.\n pub fn generator() -> EmbeddedCurvePoint {\n // Generator point for the grumpkin curve (y^2 = x^3 - 17)\n EmbeddedCurvePoint {\n x: 1,\n y: 17631683881184975370165255887551781615748388533673675138860, // sqrt(-16)\n is_infinite: false,\n }\n }\n}\n\nimpl Add for EmbeddedCurvePoint {\n /// Adds two points P+Q, using the curve addition formula, and also handles point at infinity\n fn add(self, other: EmbeddedCurvePoint) -> EmbeddedCurvePoint {\n embedded_curve_add(self, other)\n }\n}\n\nimpl Sub for EmbeddedCurvePoint {\n /// Points subtraction operation, using addition and negation\n fn sub(self, other: EmbeddedCurvePoint) -> EmbeddedCurvePoint {\n self + other.neg()\n }\n}\n\nimpl Neg for EmbeddedCurvePoint {\n /// Negates a point P, i.e returns -P, by negating the y coordinate.\n /// If the point is at infinity, then the result is also at infinity.\n fn neg(self) -> EmbeddedCurvePoint {\n EmbeddedCurvePoint { x: self.x, y: -self.y, is_infinite: self.is_infinite }\n }\n}\n\nimpl Eq for EmbeddedCurvePoint {\n /// Checks whether two points are equal\n fn eq(self: Self, b: EmbeddedCurvePoint) -> bool {\n (self.is_infinite & b.is_infinite)\n | ((self.is_infinite == b.is_infinite) & (self.x == b.x) & (self.y == b.y))\n }\n}\n\nimpl Hash for EmbeddedCurvePoint {\n fn hash(self, state: &mut H)\n where\n H: crate::hash::Hasher,\n {\n if self.is_infinite {\n self.is_infinite.hash(state);\n } else {\n self.x.hash(state);\n self.y.hash(state);\n }\n }\n}\n\n/// Scalar for the embedded curve represented as low and high limbs\n/// By definition, the scalar field of the embedded curve is base field of the proving system curve.\n/// It may not fit into a Field element, so it is represented with two Field elements; its low and high limbs.\npub struct EmbeddedCurveScalar {\n pub lo: Field,\n pub hi: Field,\n}\n\nimpl EmbeddedCurveScalar {\n pub fn new(lo: Field, hi: Field) -> Self {\n EmbeddedCurveScalar { lo, hi }\n }\n\n #[field(bn254)]\n pub fn from_field(scalar: Field) -> EmbeddedCurveScalar {\n let (a, b) = crate::field::bn254::decompose(scalar);\n EmbeddedCurveScalar { lo: a, hi: b }\n }\n\n //Bytes to scalar: take the first (after the specified offset) 16 bytes of the input as the lo value, and the next 16 bytes as the hi value\n #[field(bn254)]\n pub(crate) fn from_bytes(bytes: [u8; 64], offset: u32) -> EmbeddedCurveScalar {\n let mut v = 1;\n let mut lo = 0 as Field;\n let mut hi = 0 as Field;\n for i in 0..16 {\n lo = lo + (bytes[offset + 31 - i] as Field) * v;\n hi = hi + (bytes[offset + 15 - i] as Field) * v;\n v = v * 256;\n }\n let sig_s = crate::embedded_curve_ops::EmbeddedCurveScalar { lo, hi };\n sig_s\n }\n}\n\nimpl Eq for EmbeddedCurveScalar {\n fn eq(self, other: Self) -> bool {\n (other.hi == self.hi) & (other.lo == self.lo)\n }\n}\n\nimpl Hash for EmbeddedCurveScalar {\n fn hash(self, state: &mut H)\n where\n H: crate::hash::Hasher,\n {\n self.hi.hash(state);\n self.lo.hash(state);\n }\n}\n\n// Computes a multi scalar multiplication over the embedded curve.\n// For bn254, We have Grumpkin and Baby JubJub.\n// For bls12-381, we have JubJub and Bandersnatch.\n//\n// The embedded curve being used is decided by the\n// underlying proof system.\n// docs:start:multi_scalar_mul\npub fn multi_scalar_mul(\n points: [EmbeddedCurvePoint; N],\n scalars: [EmbeddedCurveScalar; N],\n) -> EmbeddedCurvePoint\n// docs:end:multi_scalar_mul\n{\n multi_scalar_mul_array_return(points, scalars)[0]\n}\n\n#[foreign(multi_scalar_mul)]\npub(crate) fn multi_scalar_mul_array_return(\n points: [EmbeddedCurvePoint; N],\n scalars: [EmbeddedCurveScalar; N],\n) -> [EmbeddedCurvePoint; 1] {}\n\n// docs:start:fixed_base_scalar_mul\npub fn fixed_base_scalar_mul(scalar: EmbeddedCurveScalar) -> EmbeddedCurvePoint\n// docs:end:fixed_base_scalar_mul\n{\n multi_scalar_mul([EmbeddedCurvePoint::generator()], [scalar])\n}\n\n/// This function only assumes that the points are on the curve\n/// It handles corner cases around the infinity point causing some overhead compared to embedded_curve_add_not_nul and embedded_curve_add_unsafe\n// docs:start:embedded_curve_add\npub fn embedded_curve_add(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n // docs:end:embedded_curve_add\n if crate::runtime::is_unconstrained() {\n // `embedded_curve_add_unsafe` requires the inputs not to be the infinity point, so we check it here.\n // This is because `embedded_curve_add_unsafe` uses the `embedded_curve_add` opcode.\n // For efficiency, the backend does not check the inputs for the infinity point, but it assumes that they are not the infinity point\n // so that it can apply the ec addition formula directly.\n if point1.is_infinite {\n point2\n } else if point2.is_infinite {\n point1\n } else {\n embedded_curve_add_unsafe(point1, point2)\n }\n } else {\n // In a constrained context, we also need to check the inputs are not the infinity point because we also use `embedded_curve_add_unsafe`\n // However we also need to identify the case where the two inputs are the same, because then\n // the addition formula does not work and we need to use the doubling formula instead.\n // In unconstrained context, we can check directly if the input values are the same when solving the opcode, so it is not an issue.\n\n // x_coordinates_match is true if both abscissae are the same\n let x_coordinates_match = point1.x == point2.x;\n // y_coordinates_match is true if both ordinates are the same\n let y_coordinates_match = point1.y == point2.y;\n // double_predicate is true if both abscissae and ordinates are the same\n let double_predicate = (x_coordinates_match & y_coordinates_match);\n // If the abscissae are the same, but not the ordinates, then one point is the opposite of the other\n let infinity_predicate = (x_coordinates_match & !y_coordinates_match);\n let point1_1 = EmbeddedCurvePoint {\n x: point1.x + (x_coordinates_match as Field),\n y: point1.y,\n is_infinite: false,\n };\n let point2_1 = EmbeddedCurvePoint { x: point2.x, y: point2.y, is_infinite: false };\n // point1_1 is guaranteed to have a different abscissa than point2:\n // - if x_coordinates_match is 0, that means point1.x != point2.x, and point1_1.x = point1.x + 0\n // - if x_coordinates_match is 1, that means point1.x = point2.x, but point1_1.x = point1.x + 1 in this case\n // Because the abscissa is different, the addition formula is guaranteed to succeed, so we can safely use `embedded_curve_add_unsafe`\n // Note that this computation may be garbage: if x_coordinates_match is 1, or if one of the input is the point at infinity.\n let mut result = embedded_curve_add_unsafe(point1_1, point2_1);\n\n // `embedded_curve_add_unsafe` is doing a doubling if the input is the same variable, because in this case it is guaranteed (at 'compile time') that the input is the same.\n let double = embedded_curve_add_unsafe(point1, point1);\n // `embedded_curve_add_unsafe` would not perform doubling, even if the inputs point1 and point2 are the same, because it cannot know this without adding some logic (and some constraints)\n // However we did this logic when we computed `double_predicate`, so we set the result to 2*point1 if point1 and point2 are the same\n result = if double_predicate { double } else { result };\n\n // Same logic as above for unconstrained context, we set the proper result when one of the inputs is the infinity point\n if point1.is_infinite {\n result = point2;\n }\n if point2.is_infinite {\n result = point1;\n }\n\n // Finally, we set the is_infinity flag of the result:\n // Opposite points should sum into the infinity point, however, if one of them is point at infinity, their coordinates are not meaningful\n // so we should not use the fact that the inputs are opposite in this case:\n let mut result_is_infinity =\n infinity_predicate & (!point1.is_infinite & !point2.is_infinite);\n // However, if both of them are at infinity, then the result is also at infinity\n result.is_infinite = result_is_infinity | (point1.is_infinite & point2.is_infinite);\n result\n }\n}\n\n#[foreign(embedded_curve_add)]\nfn embedded_curve_add_array_return(\n _point1: EmbeddedCurvePoint,\n _point2: EmbeddedCurvePoint,\n) -> [EmbeddedCurvePoint; 1] {}\n\n/// This function assumes that:\n/// The points are on the curve, and\n/// The points don't share an x-coordinate, and\n/// Neither point is the infinity point.\n/// If it is used with correct input, the function ensures the correct non-zero result is returned.\n/// Except for points on the curve, the other assumptions are checked by the function. It will cause assertion failure if they are not respected.\npub fn embedded_curve_add_not_nul(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n assert(point1.x != point2.x);\n assert(!point1.is_infinite);\n assert(!point2.is_infinite);\n // Ensure is_infinite is comptime\n let point1_1 = EmbeddedCurvePoint { x: point1.x, y: point1.y, is_infinite: false };\n let point2_1 = EmbeddedCurvePoint { x: point2.x, y: point2.y, is_infinite: false };\n embedded_curve_add_unsafe(point1_1, point2_1)\n}\n\n/// Unsafe ec addition\n/// If the inputs are the same, it will perform a doubling, but only if point1 and point2 are the same variable.\n/// If they have the same value but are different variables, the result will be incorrect because in this case\n/// it assumes (but does not check) that the points' x-coordinates are not equal.\n/// It also assumes neither point is the infinity point.\npub fn embedded_curve_add_unsafe(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n embedded_curve_add_array_return(point1, point2)[0]\n}\n", diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/regression_7744/execute__tests__force_brillig_false_inliner_0.snap b/tooling/nargo_cli/tests/snapshots/execution_success/regression_7744/execute__tests__force_brillig_false_inliner_0.snap index 4dc671c96da..aa5de57031e 100644 --- a/tooling/nargo_cli/tests/snapshots/execution_success/regression_7744/execute__tests__force_brillig_false_inliner_0.snap +++ b/tooling/nargo_cli/tests/snapshots/execution_success/regression_7744/execute__tests__force_brillig_false_inliner_0.snap @@ -46,19 +46,20 @@ expression: artifact }, "bytecode": [ "func 0", - "current witness index : _8", + "current witness index : _9", "private parameters indices : [_0]", "public parameters indices : []", "return value indices : [_1, _2, _3]", "BLACKBOX::RANGE [(_0, 1)] []", "EXPR [ (-1, _0) (-1, _4) 1 ]", "EXPR [ (-17631683881184975370165255887551781615748388533673675138855, _0) (-1, _5) 17631683881184975370165255887551781615748388533673675138860 ]", - "BLACKBOX::EMBEDDED_CURVE_ADD [(_4, 254), (_5, 254), (0, 1), (_4, 254), (_5, 254), (0, 1)] [_6, _7, _8]", - "EXPR [ (-1, _0, _6) (1, _1) 0 ]", - "EXPR [ (-1, _0, _7) (1, _2) (-5, _4) 0 ]", - "EXPR [ (-1, _0, _8) (1, _3) 0 ]" + "EXPR [ (-1, _6) 0 ]", + "BLACKBOX::EMBEDDED_CURVE_ADD [(_4, 254), (_5, 254), (_6, 1), (_4, 254), (_5, 254), (_6, 1)] [_7, _8, _9]", + "EXPR [ (-1, _0, _7) (1, _1) 0 ]", + "EXPR [ (-1, _0, _8) (1, _2) (-5, _4) 0 ]", + "EXPR [ (-1, _0, _9) (1, _3) 0 ]" ], - "debug_symbols": "nZFNDoMgEIXvMmsWom2NXqVpDOJoSAgQhCaN8e4diVZduOlm/h7vgwwTdNjGoVGmtyPUzwlar7RWQ6OtFEFZQ9NpZrC1TfCINIKDTi4nPJoAtYlaM3gLHdOh0QmTchCe1IwBmo4yAXulcalmtruza2teVau5KG4/+/3s59d+zvOsXAlU33cGf/zLKE+MF3VCKn/aHHB6OoM8xYLivOC9Eq3GdbN9NPKw6PBxm7J9hfNWYhc9Luik0WVf", + "debug_symbols": "nZHPDoMgDMbfpWcO4p8ZfZVlMajVkBAgCEsW47uvEp168LJLafvx+0rKDD22YWykHswE9XOG1kml5Ngo0wkvjabuvDDYy8Y7RGrBSSfKCofaQ62DUgzeQoV4abJCx9MLR2rCAHVPJxkOUuGaLeygk3s0raoNzrL8hxdXnt/znKdJuTlQXhwe/PGvR3nxeFElOukumwNOT2eQxpjFmFNc1iFOilbhtt8h6O60bv+xu7J/iHWmwz44XAdEjUZ+AQ==", "file_map": { "16": { "source": "use crate::cmp::Eq;\nuse crate::hash::Hash;\nuse crate::ops::arith::{Add, Neg, Sub};\n\n/// A point on the embedded elliptic curve\n/// By definition, the base field of the embedded curve is the scalar field of the proof system curve, i.e the Noir Field.\n/// x and y denotes the Weierstrass coordinates of the point, if is_infinite is false.\npub struct EmbeddedCurvePoint {\n pub x: Field,\n pub y: Field,\n pub is_infinite: bool,\n}\n\nimpl EmbeddedCurvePoint {\n /// Elliptic curve point doubling operation\n /// returns the doubled point of a point P, i.e P+P\n pub fn double(self) -> EmbeddedCurvePoint {\n embedded_curve_add(self, self)\n }\n\n /// Returns the null element of the curve; 'the point at infinity'\n pub fn point_at_infinity() -> EmbeddedCurvePoint {\n EmbeddedCurvePoint { x: 0, y: 0, is_infinite: true }\n }\n\n /// Returns the curve's generator point.\n pub fn generator() -> EmbeddedCurvePoint {\n // Generator point for the grumpkin curve (y^2 = x^3 - 17)\n EmbeddedCurvePoint {\n x: 1,\n y: 17631683881184975370165255887551781615748388533673675138860, // sqrt(-16)\n is_infinite: false,\n }\n }\n}\n\nimpl Add for EmbeddedCurvePoint {\n /// Adds two points P+Q, using the curve addition formula, and also handles point at infinity\n fn add(self, other: EmbeddedCurvePoint) -> EmbeddedCurvePoint {\n embedded_curve_add(self, other)\n }\n}\n\nimpl Sub for EmbeddedCurvePoint {\n /// Points subtraction operation, using addition and negation\n fn sub(self, other: EmbeddedCurvePoint) -> EmbeddedCurvePoint {\n self + other.neg()\n }\n}\n\nimpl Neg for EmbeddedCurvePoint {\n /// Negates a point P, i.e returns -P, by negating the y coordinate.\n /// If the point is at infinity, then the result is also at infinity.\n fn neg(self) -> EmbeddedCurvePoint {\n EmbeddedCurvePoint { x: self.x, y: -self.y, is_infinite: self.is_infinite }\n }\n}\n\nimpl Eq for EmbeddedCurvePoint {\n /// Checks whether two points are equal\n fn eq(self: Self, b: EmbeddedCurvePoint) -> bool {\n (self.is_infinite & b.is_infinite)\n | ((self.is_infinite == b.is_infinite) & (self.x == b.x) & (self.y == b.y))\n }\n}\n\nimpl Hash for EmbeddedCurvePoint {\n fn hash(self, state: &mut H)\n where\n H: crate::hash::Hasher,\n {\n if self.is_infinite {\n self.is_infinite.hash(state);\n } else {\n self.x.hash(state);\n self.y.hash(state);\n }\n }\n}\n\n/// Scalar for the embedded curve represented as low and high limbs\n/// By definition, the scalar field of the embedded curve is base field of the proving system curve.\n/// It may not fit into a Field element, so it is represented with two Field elements; its low and high limbs.\npub struct EmbeddedCurveScalar {\n pub lo: Field,\n pub hi: Field,\n}\n\nimpl EmbeddedCurveScalar {\n pub fn new(lo: Field, hi: Field) -> Self {\n EmbeddedCurveScalar { lo, hi }\n }\n\n #[field(bn254)]\n pub fn from_field(scalar: Field) -> EmbeddedCurveScalar {\n let (a, b) = crate::field::bn254::decompose(scalar);\n EmbeddedCurveScalar { lo: a, hi: b }\n }\n\n //Bytes to scalar: take the first (after the specified offset) 16 bytes of the input as the lo value, and the next 16 bytes as the hi value\n #[field(bn254)]\n pub(crate) fn from_bytes(bytes: [u8; 64], offset: u32) -> EmbeddedCurveScalar {\n let mut v = 1;\n let mut lo = 0 as Field;\n let mut hi = 0 as Field;\n for i in 0..16 {\n lo = lo + (bytes[offset + 31 - i] as Field) * v;\n hi = hi + (bytes[offset + 15 - i] as Field) * v;\n v = v * 256;\n }\n let sig_s = crate::embedded_curve_ops::EmbeddedCurveScalar { lo, hi };\n sig_s\n }\n}\n\nimpl Eq for EmbeddedCurveScalar {\n fn eq(self, other: Self) -> bool {\n (other.hi == self.hi) & (other.lo == self.lo)\n }\n}\n\nimpl Hash for EmbeddedCurveScalar {\n fn hash(self, state: &mut H)\n where\n H: crate::hash::Hasher,\n {\n self.hi.hash(state);\n self.lo.hash(state);\n }\n}\n\n// Computes a multi scalar multiplication over the embedded curve.\n// For bn254, We have Grumpkin and Baby JubJub.\n// For bls12-381, we have JubJub and Bandersnatch.\n//\n// The embedded curve being used is decided by the\n// underlying proof system.\n// docs:start:multi_scalar_mul\npub fn multi_scalar_mul(\n points: [EmbeddedCurvePoint; N],\n scalars: [EmbeddedCurveScalar; N],\n) -> EmbeddedCurvePoint\n// docs:end:multi_scalar_mul\n{\n multi_scalar_mul_array_return(points, scalars)[0]\n}\n\n#[foreign(multi_scalar_mul)]\npub(crate) fn multi_scalar_mul_array_return(\n points: [EmbeddedCurvePoint; N],\n scalars: [EmbeddedCurveScalar; N],\n) -> [EmbeddedCurvePoint; 1] {}\n\n// docs:start:fixed_base_scalar_mul\npub fn fixed_base_scalar_mul(scalar: EmbeddedCurveScalar) -> EmbeddedCurvePoint\n// docs:end:fixed_base_scalar_mul\n{\n multi_scalar_mul([EmbeddedCurvePoint::generator()], [scalar])\n}\n\n/// This function only assumes that the points are on the curve\n/// It handles corner cases around the infinity point causing some overhead compared to embedded_curve_add_not_nul and embedded_curve_add_unsafe\n// docs:start:embedded_curve_add\npub fn embedded_curve_add(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n // docs:end:embedded_curve_add\n if crate::runtime::is_unconstrained() {\n // `embedded_curve_add_unsafe` requires the inputs not to be the infinity point, so we check it here.\n // This is because `embedded_curve_add_unsafe` uses the `embedded_curve_add` opcode.\n // For efficiency, the backend does not check the inputs for the infinity point, but it assumes that they are not the infinity point\n // so that it can apply the ec addition formula directly.\n if point1.is_infinite {\n point2\n } else if point2.is_infinite {\n point1\n } else {\n embedded_curve_add_unsafe(point1, point2)\n }\n } else {\n // In a constrained context, we also need to check the inputs are not the infinity point because we also use `embedded_curve_add_unsafe`\n // However we also need to identify the case where the two inputs are the same, because then\n // the addition formula does not work and we need to use the doubling formula instead.\n // In unconstrained context, we can check directly if the input values are the same when solving the opcode, so it is not an issue.\n\n // x_coordinates_match is true if both abscissae are the same\n let x_coordinates_match = point1.x == point2.x;\n // y_coordinates_match is true if both ordinates are the same\n let y_coordinates_match = point1.y == point2.y;\n // double_predicate is true if both abscissae and ordinates are the same\n let double_predicate = (x_coordinates_match & y_coordinates_match);\n // If the abscissae are the same, but not the ordinates, then one point is the opposite of the other\n let infinity_predicate = (x_coordinates_match & !y_coordinates_match);\n let point1_1 = EmbeddedCurvePoint {\n x: point1.x + (x_coordinates_match as Field),\n y: point1.y,\n is_infinite: false,\n };\n let point2_1 = EmbeddedCurvePoint { x: point2.x, y: point2.y, is_infinite: false };\n // point1_1 is guaranteed to have a different abscissa than point2:\n // - if x_coordinates_match is 0, that means point1.x != point2.x, and point1_1.x = point1.x + 0\n // - if x_coordinates_match is 1, that means point1.x = point2.x, but point1_1.x = point1.x + 1 in this case\n // Because the abscissa is different, the addition formula is guaranteed to succeed, so we can safely use `embedded_curve_add_unsafe`\n // Note that this computation may be garbage: if x_coordinates_match is 1, or if one of the input is the point at infinity.\n let mut result = embedded_curve_add_unsafe(point1_1, point2_1);\n\n // `embedded_curve_add_unsafe` is doing a doubling if the input is the same variable, because in this case it is guaranteed (at 'compile time') that the input is the same.\n let double = embedded_curve_add_unsafe(point1, point1);\n // `embedded_curve_add_unsafe` would not perform doubling, even if the inputs point1 and point2 are the same, because it cannot know this without adding some logic (and some constraints)\n // However we did this logic when we computed `double_predicate`, so we set the result to 2*point1 if point1 and point2 are the same\n result = if double_predicate { double } else { result };\n\n // Same logic as above for unconstrained context, we set the proper result when one of the inputs is the infinity point\n if point1.is_infinite {\n result = point2;\n }\n if point2.is_infinite {\n result = point1;\n }\n\n // Finally, we set the is_infinity flag of the result:\n // Opposite points should sum into the infinity point, however, if one of them is point at infinity, their coordinates are not meaningful\n // so we should not use the fact that the inputs are opposite in this case:\n let mut result_is_infinity =\n infinity_predicate & (!point1.is_infinite & !point2.is_infinite);\n // However, if both of them are at infinity, then the result is also at infinity\n result.is_infinite = result_is_infinity | (point1.is_infinite & point2.is_infinite);\n result\n }\n}\n\n#[foreign(embedded_curve_add)]\nfn embedded_curve_add_array_return(\n _point1: EmbeddedCurvePoint,\n _point2: EmbeddedCurvePoint,\n) -> [EmbeddedCurvePoint; 1] {}\n\n/// This function assumes that:\n/// The points are on the curve, and\n/// The points don't share an x-coordinate, and\n/// Neither point is the infinity point.\n/// If it is used with correct input, the function ensures the correct non-zero result is returned.\n/// Except for points on the curve, the other assumptions are checked by the function. It will cause assertion failure if they are not respected.\npub fn embedded_curve_add_not_nul(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n assert(point1.x != point2.x);\n assert(!point1.is_infinite);\n assert(!point2.is_infinite);\n // Ensure is_infinite is comptime\n let point1_1 = EmbeddedCurvePoint { x: point1.x, y: point1.y, is_infinite: false };\n let point2_1 = EmbeddedCurvePoint { x: point2.x, y: point2.y, is_infinite: false };\n embedded_curve_add_unsafe(point1_1, point2_1)\n}\n\n/// Unsafe ec addition\n/// If the inputs are the same, it will perform a doubling, but only if point1 and point2 are the same variable.\n/// If they have the same value but are different variables, the result will be incorrect because in this case\n/// it assumes (but does not check) that the points' x-coordinates are not equal.\n/// It also assumes neither point is the infinity point.\npub fn embedded_curve_add_unsafe(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n embedded_curve_add_array_return(point1, point2)[0]\n}\n", diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/regression_7744/execute__tests__force_brillig_false_inliner_9223372036854775807.snap b/tooling/nargo_cli/tests/snapshots/execution_success/regression_7744/execute__tests__force_brillig_false_inliner_9223372036854775807.snap index 4dc671c96da..aa5de57031e 100644 --- a/tooling/nargo_cli/tests/snapshots/execution_success/regression_7744/execute__tests__force_brillig_false_inliner_9223372036854775807.snap +++ b/tooling/nargo_cli/tests/snapshots/execution_success/regression_7744/execute__tests__force_brillig_false_inliner_9223372036854775807.snap @@ -46,19 +46,20 @@ expression: artifact }, "bytecode": [ "func 0", - "current witness index : _8", + "current witness index : _9", "private parameters indices : [_0]", "public parameters indices : []", "return value indices : [_1, _2, _3]", "BLACKBOX::RANGE [(_0, 1)] []", "EXPR [ (-1, _0) (-1, _4) 1 ]", "EXPR [ (-17631683881184975370165255887551781615748388533673675138855, _0) (-1, _5) 17631683881184975370165255887551781615748388533673675138860 ]", - "BLACKBOX::EMBEDDED_CURVE_ADD [(_4, 254), (_5, 254), (0, 1), (_4, 254), (_5, 254), (0, 1)] [_6, _7, _8]", - "EXPR [ (-1, _0, _6) (1, _1) 0 ]", - "EXPR [ (-1, _0, _7) (1, _2) (-5, _4) 0 ]", - "EXPR [ (-1, _0, _8) (1, _3) 0 ]" + "EXPR [ (-1, _6) 0 ]", + "BLACKBOX::EMBEDDED_CURVE_ADD [(_4, 254), (_5, 254), (_6, 1), (_4, 254), (_5, 254), (_6, 1)] [_7, _8, _9]", + "EXPR [ (-1, _0, _7) (1, _1) 0 ]", + "EXPR [ (-1, _0, _8) (1, _2) (-5, _4) 0 ]", + "EXPR [ (-1, _0, _9) (1, _3) 0 ]" ], - "debug_symbols": "nZFNDoMgEIXvMmsWom2NXqVpDOJoSAgQhCaN8e4diVZduOlm/h7vgwwTdNjGoVGmtyPUzwlar7RWQ6OtFEFZQ9NpZrC1TfCINIKDTi4nPJoAtYlaM3gLHdOh0QmTchCe1IwBmo4yAXulcalmtruza2teVau5KG4/+/3s59d+zvOsXAlU33cGf/zLKE+MF3VCKn/aHHB6OoM8xYLivOC9Eq3GdbN9NPKw6PBxm7J9hfNWYhc9Luik0WVf", + "debug_symbols": "nZHPDoMgDMbfpWcO4p8ZfZVlMajVkBAgCEsW47uvEp168LJLafvx+0rKDD22YWykHswE9XOG1kml5Ngo0wkvjabuvDDYy8Y7RGrBSSfKCofaQ62DUgzeQoV4abJCx9MLR2rCAHVPJxkOUuGaLeygk3s0raoNzrL8hxdXnt/znKdJuTlQXhwe/PGvR3nxeFElOukumwNOT2eQxpjFmFNc1iFOilbhtt8h6O60bv+xu7J/iHWmwz44XAdEjUZ+AQ==", "file_map": { "16": { "source": "use crate::cmp::Eq;\nuse crate::hash::Hash;\nuse crate::ops::arith::{Add, Neg, Sub};\n\n/// A point on the embedded elliptic curve\n/// By definition, the base field of the embedded curve is the scalar field of the proof system curve, i.e the Noir Field.\n/// x and y denotes the Weierstrass coordinates of the point, if is_infinite is false.\npub struct EmbeddedCurvePoint {\n pub x: Field,\n pub y: Field,\n pub is_infinite: bool,\n}\n\nimpl EmbeddedCurvePoint {\n /// Elliptic curve point doubling operation\n /// returns the doubled point of a point P, i.e P+P\n pub fn double(self) -> EmbeddedCurvePoint {\n embedded_curve_add(self, self)\n }\n\n /// Returns the null element of the curve; 'the point at infinity'\n pub fn point_at_infinity() -> EmbeddedCurvePoint {\n EmbeddedCurvePoint { x: 0, y: 0, is_infinite: true }\n }\n\n /// Returns the curve's generator point.\n pub fn generator() -> EmbeddedCurvePoint {\n // Generator point for the grumpkin curve (y^2 = x^3 - 17)\n EmbeddedCurvePoint {\n x: 1,\n y: 17631683881184975370165255887551781615748388533673675138860, // sqrt(-16)\n is_infinite: false,\n }\n }\n}\n\nimpl Add for EmbeddedCurvePoint {\n /// Adds two points P+Q, using the curve addition formula, and also handles point at infinity\n fn add(self, other: EmbeddedCurvePoint) -> EmbeddedCurvePoint {\n embedded_curve_add(self, other)\n }\n}\n\nimpl Sub for EmbeddedCurvePoint {\n /// Points subtraction operation, using addition and negation\n fn sub(self, other: EmbeddedCurvePoint) -> EmbeddedCurvePoint {\n self + other.neg()\n }\n}\n\nimpl Neg for EmbeddedCurvePoint {\n /// Negates a point P, i.e returns -P, by negating the y coordinate.\n /// If the point is at infinity, then the result is also at infinity.\n fn neg(self) -> EmbeddedCurvePoint {\n EmbeddedCurvePoint { x: self.x, y: -self.y, is_infinite: self.is_infinite }\n }\n}\n\nimpl Eq for EmbeddedCurvePoint {\n /// Checks whether two points are equal\n fn eq(self: Self, b: EmbeddedCurvePoint) -> bool {\n (self.is_infinite & b.is_infinite)\n | ((self.is_infinite == b.is_infinite) & (self.x == b.x) & (self.y == b.y))\n }\n}\n\nimpl Hash for EmbeddedCurvePoint {\n fn hash(self, state: &mut H)\n where\n H: crate::hash::Hasher,\n {\n if self.is_infinite {\n self.is_infinite.hash(state);\n } else {\n self.x.hash(state);\n self.y.hash(state);\n }\n }\n}\n\n/// Scalar for the embedded curve represented as low and high limbs\n/// By definition, the scalar field of the embedded curve is base field of the proving system curve.\n/// It may not fit into a Field element, so it is represented with two Field elements; its low and high limbs.\npub struct EmbeddedCurveScalar {\n pub lo: Field,\n pub hi: Field,\n}\n\nimpl EmbeddedCurveScalar {\n pub fn new(lo: Field, hi: Field) -> Self {\n EmbeddedCurveScalar { lo, hi }\n }\n\n #[field(bn254)]\n pub fn from_field(scalar: Field) -> EmbeddedCurveScalar {\n let (a, b) = crate::field::bn254::decompose(scalar);\n EmbeddedCurveScalar { lo: a, hi: b }\n }\n\n //Bytes to scalar: take the first (after the specified offset) 16 bytes of the input as the lo value, and the next 16 bytes as the hi value\n #[field(bn254)]\n pub(crate) fn from_bytes(bytes: [u8; 64], offset: u32) -> EmbeddedCurveScalar {\n let mut v = 1;\n let mut lo = 0 as Field;\n let mut hi = 0 as Field;\n for i in 0..16 {\n lo = lo + (bytes[offset + 31 - i] as Field) * v;\n hi = hi + (bytes[offset + 15 - i] as Field) * v;\n v = v * 256;\n }\n let sig_s = crate::embedded_curve_ops::EmbeddedCurveScalar { lo, hi };\n sig_s\n }\n}\n\nimpl Eq for EmbeddedCurveScalar {\n fn eq(self, other: Self) -> bool {\n (other.hi == self.hi) & (other.lo == self.lo)\n }\n}\n\nimpl Hash for EmbeddedCurveScalar {\n fn hash(self, state: &mut H)\n where\n H: crate::hash::Hasher,\n {\n self.hi.hash(state);\n self.lo.hash(state);\n }\n}\n\n// Computes a multi scalar multiplication over the embedded curve.\n// For bn254, We have Grumpkin and Baby JubJub.\n// For bls12-381, we have JubJub and Bandersnatch.\n//\n// The embedded curve being used is decided by the\n// underlying proof system.\n// docs:start:multi_scalar_mul\npub fn multi_scalar_mul(\n points: [EmbeddedCurvePoint; N],\n scalars: [EmbeddedCurveScalar; N],\n) -> EmbeddedCurvePoint\n// docs:end:multi_scalar_mul\n{\n multi_scalar_mul_array_return(points, scalars)[0]\n}\n\n#[foreign(multi_scalar_mul)]\npub(crate) fn multi_scalar_mul_array_return(\n points: [EmbeddedCurvePoint; N],\n scalars: [EmbeddedCurveScalar; N],\n) -> [EmbeddedCurvePoint; 1] {}\n\n// docs:start:fixed_base_scalar_mul\npub fn fixed_base_scalar_mul(scalar: EmbeddedCurveScalar) -> EmbeddedCurvePoint\n// docs:end:fixed_base_scalar_mul\n{\n multi_scalar_mul([EmbeddedCurvePoint::generator()], [scalar])\n}\n\n/// This function only assumes that the points are on the curve\n/// It handles corner cases around the infinity point causing some overhead compared to embedded_curve_add_not_nul and embedded_curve_add_unsafe\n// docs:start:embedded_curve_add\npub fn embedded_curve_add(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n // docs:end:embedded_curve_add\n if crate::runtime::is_unconstrained() {\n // `embedded_curve_add_unsafe` requires the inputs not to be the infinity point, so we check it here.\n // This is because `embedded_curve_add_unsafe` uses the `embedded_curve_add` opcode.\n // For efficiency, the backend does not check the inputs for the infinity point, but it assumes that they are not the infinity point\n // so that it can apply the ec addition formula directly.\n if point1.is_infinite {\n point2\n } else if point2.is_infinite {\n point1\n } else {\n embedded_curve_add_unsafe(point1, point2)\n }\n } else {\n // In a constrained context, we also need to check the inputs are not the infinity point because we also use `embedded_curve_add_unsafe`\n // However we also need to identify the case where the two inputs are the same, because then\n // the addition formula does not work and we need to use the doubling formula instead.\n // In unconstrained context, we can check directly if the input values are the same when solving the opcode, so it is not an issue.\n\n // x_coordinates_match is true if both abscissae are the same\n let x_coordinates_match = point1.x == point2.x;\n // y_coordinates_match is true if both ordinates are the same\n let y_coordinates_match = point1.y == point2.y;\n // double_predicate is true if both abscissae and ordinates are the same\n let double_predicate = (x_coordinates_match & y_coordinates_match);\n // If the abscissae are the same, but not the ordinates, then one point is the opposite of the other\n let infinity_predicate = (x_coordinates_match & !y_coordinates_match);\n let point1_1 = EmbeddedCurvePoint {\n x: point1.x + (x_coordinates_match as Field),\n y: point1.y,\n is_infinite: false,\n };\n let point2_1 = EmbeddedCurvePoint { x: point2.x, y: point2.y, is_infinite: false };\n // point1_1 is guaranteed to have a different abscissa than point2:\n // - if x_coordinates_match is 0, that means point1.x != point2.x, and point1_1.x = point1.x + 0\n // - if x_coordinates_match is 1, that means point1.x = point2.x, but point1_1.x = point1.x + 1 in this case\n // Because the abscissa is different, the addition formula is guaranteed to succeed, so we can safely use `embedded_curve_add_unsafe`\n // Note that this computation may be garbage: if x_coordinates_match is 1, or if one of the input is the point at infinity.\n let mut result = embedded_curve_add_unsafe(point1_1, point2_1);\n\n // `embedded_curve_add_unsafe` is doing a doubling if the input is the same variable, because in this case it is guaranteed (at 'compile time') that the input is the same.\n let double = embedded_curve_add_unsafe(point1, point1);\n // `embedded_curve_add_unsafe` would not perform doubling, even if the inputs point1 and point2 are the same, because it cannot know this without adding some logic (and some constraints)\n // However we did this logic when we computed `double_predicate`, so we set the result to 2*point1 if point1 and point2 are the same\n result = if double_predicate { double } else { result };\n\n // Same logic as above for unconstrained context, we set the proper result when one of the inputs is the infinity point\n if point1.is_infinite {\n result = point2;\n }\n if point2.is_infinite {\n result = point1;\n }\n\n // Finally, we set the is_infinity flag of the result:\n // Opposite points should sum into the infinity point, however, if one of them is point at infinity, their coordinates are not meaningful\n // so we should not use the fact that the inputs are opposite in this case:\n let mut result_is_infinity =\n infinity_predicate & (!point1.is_infinite & !point2.is_infinite);\n // However, if both of them are at infinity, then the result is also at infinity\n result.is_infinite = result_is_infinity | (point1.is_infinite & point2.is_infinite);\n result\n }\n}\n\n#[foreign(embedded_curve_add)]\nfn embedded_curve_add_array_return(\n _point1: EmbeddedCurvePoint,\n _point2: EmbeddedCurvePoint,\n) -> [EmbeddedCurvePoint; 1] {}\n\n/// This function assumes that:\n/// The points are on the curve, and\n/// The points don't share an x-coordinate, and\n/// Neither point is the infinity point.\n/// If it is used with correct input, the function ensures the correct non-zero result is returned.\n/// Except for points on the curve, the other assumptions are checked by the function. It will cause assertion failure if they are not respected.\npub fn embedded_curve_add_not_nul(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n assert(point1.x != point2.x);\n assert(!point1.is_infinite);\n assert(!point2.is_infinite);\n // Ensure is_infinite is comptime\n let point1_1 = EmbeddedCurvePoint { x: point1.x, y: point1.y, is_infinite: false };\n let point2_1 = EmbeddedCurvePoint { x: point2.x, y: point2.y, is_infinite: false };\n embedded_curve_add_unsafe(point1_1, point2_1)\n}\n\n/// Unsafe ec addition\n/// If the inputs are the same, it will perform a doubling, but only if point1 and point2 are the same variable.\n/// If they have the same value but are different variables, the result will be incorrect because in this case\n/// it assumes (but does not check) that the points' x-coordinates are not equal.\n/// It also assumes neither point is the infinity point.\npub fn embedded_curve_add_unsafe(\n point1: EmbeddedCurvePoint,\n point2: EmbeddedCurvePoint,\n) -> EmbeddedCurvePoint {\n embedded_curve_add_array_return(point1, point2)[0]\n}\n",