Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -1486,7 +1486,7 @@ bigfield<Builder, T> bigfield<Builder, T>::msub_div(const std::vector<bigfield>&
{
// Check the basics
BB_ASSERT_EQ(mul_left.size(), mul_right.size());
BB_ASSERT(divisor.get_value() != 0);
BB_ASSERT((divisor.get_value() % modulus_u512) != 0, "bigfield: Division by zero in msub_div");

OriginTag new_tag = divisor.get_origin_tag();
for (auto [left_element, right_element] : zip_view(mul_left, mul_right)) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -490,7 +490,7 @@ element<C, Fq, Fr, G> element<C, Fq, Fr, G>::multiple_montgomery_ladder(
// Let A = (x, y) and P = (x₁, y₁)
// For the first point P, we want to compute: (2A + P) = (A + P) + A
// We first need to check if x ≠ x₁.
x().assert_is_not_equal(add[0].x3_prev);
x().assert_is_not_equal(add[0].x3_prev, "biggroup::multiple_montgomery_ladder: x-coordinates must be distinct.");

// Compute λ₁ for computing the first addition: (A + P)
Fq lambda1;
Expand Down Expand Up @@ -522,7 +522,7 @@ element<C, Fq, Fr, G> element<C, Fq, Fr, G>::multiple_montgomery_ladder(
// = (y - (λ₁ * (x - x₃) - y)) / (x - x₃) (substituting y₃)
// = (2y) / (x - x₃) - λ₁
//
x().assert_is_not_equal(x_3);
x().assert_is_not_equal(x_3, "biggroup::multiple_montgomery_ladder: x-coordinates must be distinct.");
Fq lambda2 = Fq::div_without_denominator_check({ y() + y() }, (x() - x_3)) - lambda1;

// Using λ₂, compute x₄ for the final result:
Expand Down Expand Up @@ -552,7 +552,8 @@ element<C, Fq, Fr, G> element<C, Fq, Fr, G>::multiple_montgomery_ladder(
// Let x = previous_x, y = previous_y
// Let P = (xᵢ, yᵢ) be the next point to add (represented by add[i])
// Ensure x-coordinates are distinct: x ≠ xᵢ
previous_x.assert_is_not_equal(add[i].x3_prev);
previous_x.assert_is_not_equal(add[i].x3_prev,
"biggroup::multiple_montgomery_ladder: x-coordinates must be distinct.");

// Determine sign adjustment based on previous y's sign
// If the previous y was positive, we need to negate the y-component from add[i]
Expand Down Expand Up @@ -602,7 +603,7 @@ element<C, Fq, Fr, G> element<C, Fq, Fr, G>::multiple_montgomery_ladder(
// = (2y) / (x - x₃) - λ₁
// = -2(y / (x₃ - x)) - λ₁
//
previous_x.assert_is_not_equal(x_3);
previous_x.assert_is_not_equal(x_3, "biggroup::multiple_montgomery_ladder: x-coordinates must be distinct.");
Fq l2_denominator = previous_y.is_negative ? previous_x - x_3 : x_3 - previous_x;
Fq partial_lambda2 = Fq::msub_div(previous_y.mul_left,
previous_y.mul_right,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -374,46 +374,60 @@ template <typename Curve> class stdlibBiggroupSecp256k1 : public testing::Test {
EXPECT_CIRCUIT_CORRECTNESS(builder);
}

static void test_secp256k1_ecdsa_mul_point_at_infinity()
static void test_secp256k1_ecdsa_mul_point_at_infinity_fails()
{
// This test checks if secp256k1_ecdsa_mul properly handles the case when
// the result u1*G + u2*P is the point at infinity, ensuring that the
// incomplete addition formulas don't cause issues.
// ============================================================================
// REGRESSION TEST: Intermediate collision in Montgomery ladder
// ============================================================================
//
// We'll use simple scalars where u1 and u2 are chosen such that:
// u1*G + u2*P = O (point at infinity)
// Edge case: u1·G + u2·P = O (point at infinity).
//
// This means u1*G = -u2*P, or equivalently u1 = -u2*s where P = s*G

Builder builder = Builder();
// The secp256k1_ecdsa_mul function uses multiple_montgomery_ladder which computes:
// multiple_montgomery_ladder([A, B, C]) = 2·(2·(2·Q + A) + B) + C
//
// At each step, it computes R_{i+1} = 2·R_i + P_i using the Montgomery ladder:
// 1. Compute (R_i + P_i) with coordinates (x_3, y_3)
// 2. Compute (R_i + P_i) + R_i with slope λ₂ = (y_Ri - y_3) / (x_Ri - x_3)
//
// When x_Ri == x_3 (R_i and R_i+P_i have the same x-coordinate), we run into division by zero!
//
// When computing u1·G + u2·P = O with random scalars, the probability of hitting
// an intermediate collision is negligible (~1/2^256).
//
// But when we CONSTRAIN u1 = -(u2·s), the wNAF digits of u1 and u2 become correlated.
// Some (u2, s) pairs produce wNAF decompositions where an intermediate partial sum leads to
// a point at infinity. We are testing one such (u2, s) pair here.
//
// Disable asserts to test circuit error handling
BB_DISABLE_ASSERTS();

// Choose a random scalar for the public key
fr scalar_s = fr::random_element();
const uint256_t scalar_s_val("0xa829a047d570ff736a868434729a1d364547f538ead58ddf5acf9b9811da7017");
const uint256_t scalar_u1_val("0x5ab31ec9ed17cb51e6c706b3ebcd7aaef9f33b4e0fa80f68d2923b7aa432ac3c");
const uint256_t scalar_u2_val("0x089dc0bec4aba71bc35daf714bf21f221890b47a12944e8a156a32fd27d8e963");

// Choose a random u2
fr scalar_u2 = fr::random_element();
fr scalar_s(scalar_s_val);
fr scalar_u1(scalar_u1_val);
fr scalar_u2(scalar_u2_val);

// Compute u1 such that u1*G = -u2*P
// u1 = -u2*s
fr scalar_u1 = -(scalar_u2 * scalar_s);
// Verify the relationship: u1 = -u2 * s (mod r)
EXPECT_EQ(scalar_u1, -(scalar_u2 * scalar_s));

// Verify our construction
// Verify u1*G + u2*P = O (the final result is point at infinity)
element expected_result = g1::one * scalar_u1 + (g1::one * scalar_s) * scalar_u2;
EXPECT_TRUE(expected_result.is_point_at_infinity());

// Create circuit elements
Builder builder = Builder();
element_ct P_a = element_ct::from_witness(&builder, g1::one * scalar_s);
scalar_ct u1 = scalar_ct::from_witness(&builder, scalar_u1);
scalar_ct u2 = scalar_ct::from_witness(&builder, scalar_u2);

// Call secp256k1_ecdsa_mul
auto output = element_ct::secp256k1_ecdsa_mul(P_a, u1, u2);
element_ct::secp256k1_ecdsa_mul(P_a, u1, u2);

// Check that the output is correctly identified as point at infinity
EXPECT_TRUE(output.is_point_at_infinity().get_value());

// Verify circuit correctness
EXPECT_CIRCUIT_CORRECTNESS(builder);
// Verify that circuit fails
EXPECT_CIRCUIT_CORRECTNESS(builder, false);
EXPECT_EQ(builder.err(), "biggroup::multiple_montgomery_ladder: x-coordinates must be distinct.");
}
};

Expand Down Expand Up @@ -461,7 +475,7 @@ TYPED_TEST(stdlibBiggroupSecp256k1, EcdsaMulSecp256k1StaggerRegression)
{
TestFixture::test_secp256k1_ecdsa_mul_stagger_regression();
}
TYPED_TEST(stdlibBiggroupSecp256k1, EcdsaMulSecp256k1PointAtInfinity)
TYPED_TEST(stdlibBiggroupSecp256k1, EcdsaMulSecp256k1PointAtInfinityFails)
{
TestFixture::test_secp256k1_ecdsa_mul_point_at_infinity();
TestFixture::test_secp256k1_ecdsa_mul_point_at_infinity_fails();
}
Loading