Skip to content

Commit 8745960

Browse files
notnotrajunotnotraju
notnotraju
and
notnotraju
authored
chore: audit PointTable relation in the ECCVM. (#16592)
Adds/fixes some documentation to the PointTable relation in the ECCVM. Co-authored-by: notnotraju <[email protected]>
1 parent 137436b commit 8745960

File tree

2 files changed

+43
-43
lines changed

2 files changed

+43
-43
lines changed

‎barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_point_table_relation_impl.hpp‎

Lines changed: 38 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -57,24 +57,24 @@ void ECCVMPointTableRelationImpl<FF>::accumulate(ContainerOverSubrelations& accu
5757
* In the table, the point associated with `pc = 1` is labelled P.
5858
* the point associated with `pc = 0` is labelled Q.
5959
*
60-
* | precompute_pc | precompute_point_transition | precompute_round | Tx | Ty | Dx | Dy |
61-
* | -------- | ----------------------- | ----------- | ----- | ----- | ---- | ---- |
62-
* | 1 | 0 | 0 |15P.x | 15P.y | 2P.x | 2P.y |
63-
* | 1 | 0 | 1 |13P.x | 13P.y | 2P.x | 2P.y |
64-
* | 1 | 0 | 2 |11P.x | 11P.y | 2P.x | 2P.y |
65-
* | 1 | 0 | 3 | 9P.x | 9P.y | 2P.x | 2P.y |
66-
* | 1 | 0 | 4 | 7P.x | 7P.y | 2P.x | 2P.y |
67-
* | 1 | 0 | 5 | 5P.x | 5P.y | 2P.x | 2P.y |
68-
* | 1 | 0 | 6 | 3P.x | 3P.y | 2P.x | 2P.y |
69-
* | 1 | 1 | 7 | P.x | P.y | 2P.x | 2P.y |
70-
* | 0 | 0 | 0 |15Q.x | 15Q.y | 2Q.x | 2Q.y |
71-
* | 0 | 0 | 1 |13Q.x | 13Q.y | 2Q.x | 2Q.y |
72-
* | 0 | 0 | 2 |11Q.x | 11Q.y | 2Q.x | 2Q.y |
73-
* | 0 | 0 | 3 | 9Q.x | 9Q.y | 2Q.x | 2Q.y |
74-
* | 0 | 0 | 4 | 7Q.x | 7Q.y | 2Q.x | 2Q.y |
75-
* | 0 | 0 | 5 | 5Q.x | 5Q.y | 2Q.x | 2Q.y |
76-
* | 0 | 0 | 6 | 3Q.x | 3Q.y | 2Q.x | 2Q.y |
77-
* | 0 | 1 | 7 | Q.x | Q.y | 2Q.x | 2Q.y |
60+
* | precompute_pc | precompute_point_transition | precompute_round | Tx | Ty | Dx | Dy |
61+
* | ------------- | ---------------------------- | ------------------- | ----- | ----- | ---- | ---- |
62+
* | 1 | 0 | 0 | 15P.x | 15P.y | 2P.x | 2P.y |
63+
* | 1 | 0 | 1 | 13P.x | 13P.y | 2P.x | 2P.y |
64+
* | 1 | 0 | 2 | 11P.x | 11P.y | 2P.x | 2P.y |
65+
* | 1 | 0 | 3 | 9P.x | 9P.y | 2P.x | 2P.y |
66+
* | 1 | 0 | 4 | 7P.x | 7P.y | 2P.x | 2P.y |
67+
* | 1 | 0 | 5 | 5P.x | 5P.y | 2P.x | 2P.y |
68+
* | 1 | 0 | 6 | 3P.x | 3P.y | 2P.x | 2P.y |
69+
* | 1 | 1 | 7 | P.x | P.y | 2P.x | 2P.y |
70+
* | 0 | 0 | 0 | 15Q.x | 15Q.y | 2Q.x | 2Q.y |
71+
* | 0 | 0 | 1 | 13Q.x | 13Q.y | 2Q.x | 2Q.y |
72+
* | 0 | 0 | 2 | 11Q.x | 11Q.y | 2Q.x | 2Q.y |
73+
* | 0 | 0 | 3 | 9Q.x | 9Q.y | 2Q.x | 2Q.y |
74+
* | 0 | 0 | 4 | 7Q.x | 7Q.y | 2Q.x | 2Q.y |
75+
* | 0 | 0 | 5 | 5Q.x | 5Q.y | 2Q.x | 2Q.y |
76+
* | 0 | 0 | 6 | 3Q.x | 3Q.y | 2Q.x | 2Q.y |
77+
* | 0 | 1 | 7 | Q.x | Q.y | 2Q.x | 2Q.y |
7878
*
7979
* We apply the following relations to constrain the above table:
8080
*
@@ -84,9 +84,12 @@ void ECCVMPointTableRelationImpl<FF>::accumulate(ContainerOverSubrelations& accu
8484
*
8585
* The relations that constrain `precompute_point_transition` and `precompute_pc` are in `ecc_wnaf_relation.hpp`
8686
*
87-
* When precompute_point_transition = 1, we use a strict lookup protocol in `ecc_set_relation.hpp` to validate (pc,
88-
* Tx, Ty) belong to the set of points present in our transcript columns.
89-
* ("strict" lookup protocol = every item in the table must be read from once, and only once)
87+
* When precompute_point_transition = 1, the next row corresponds to the beginning of the processing of a new point.
88+
* We use a multiset-equality check, `ecc_set_relation.hpp` to validate (pc, Tx, Ty, scalar-multiplier) is the same
89+
* as something derived from the transcript columns. In other words, the multiset equality check allows the tables
90+
* to communicate, and in particular validates that we are populating our PointTable with precomputed values that
91+
* indeed arise from the Transcript columns. (Formerly, we referred to this as a "strict" lookup protocol = every
92+
* item in the table must be read from once, and only once)
9093
*
9194
* For every row, we use a lookup protocol in `ecc_lookup_relation.hpp` to write the following tuples into a lookup
9295
* table:
@@ -102,15 +105,15 @@ void ECCVMPointTableRelationImpl<FF>::accumulate(ContainerOverSubrelations& accu
102105
* negative values produces the WNAF slice values that correspond to the multipliers for (Tx, Ty) and (Tx, -Ty):
103106
*
104107
* | Tx | Ty | x = 15 - precompute_round | 2x - 15 | y = precompute_round | 2y - 15 |
105-
* | ----- | ----- | -------------------- | ------- | --------------- | ------- |
106-
* | 15P.x | 15P.y | 15 | 15 | 0 | -15 |
107-
* | 13P.x | 13P.y | 14 | 13 | 1 | -13 |
108-
* | 11P.x | 11P.y | 13 | 11 | 2 | -11 |
109-
* | 9P.x | 9P.y | 12 | 9 | 3 | -9 |
110-
* | 7P.x | 7P.y | 11 | 7 | 4 | -7 |
111-
* | 5P.x | 5P.y | 10 | 5 | 5 | -5 |
112-
* | 3P.x | 3P.y | 9 | 3 | 6 | -3 |
113-
* | P.x | P.y | 8 | 1 | 7 | -1 |
108+
* | ----- | ----- | -------------------- | ------- | --------------- | ------- |
109+
* | 15P.x | 15P.y | 15 | 15 | 0 | -15 |
110+
* | 13P.x | 13P.y | 14 | 13 | 1 | -13 |
111+
* | 11P.x | 11P.y | 13 | 11 | 2 | -11 |
112+
* | 9P.x | 9P.y | 12 | 9 | 3 | -9 |
113+
* | 7P.x | 7P.y | 11 | 7 | 4 | -7 |
114+
* | 5P.x | 5P.y | 10 | 5 | 5 | -5 |
115+
* | 3P.x | 3P.y | 9 | 3 | 6 | -3 |
116+
* | P.x | P.y | 8 | 1 | 7 | -1 |
114117
*/
115118

116119
/**
@@ -161,9 +164,11 @@ void ECCVMPointTableRelationImpl<FF>::accumulate(ContainerOverSubrelations& accu
161164
* (x_3 + x_2 + x_1) * (x_2 - x_1)^2 - (y_2 - y_1)^2 = 0
162165
* (y_3 + y_1) * (x_2 - x_1) + (x_3 - x_1) * (y_2 - y_1) = 0
163166
*
164-
* We don't need to check for incomplete point addition edge case (x_1 == x_2)
165-
* TODO explain why (computing simple point multiples cannot trigger the edge cases, but need to serve a proof of
166-
* this...)
167+
* We don't need to check for incomplete point addition edge case (x_1 == x_2); the only cases this would correspond
168+
* to are y2 == y1 or y2 == -y1. Both of these cases may be ruled out as follows.
169+
* 1. y2 == y1. Then 2P == kP, where k∈{1, ..., 13}, which of course cannot happen because the order r of E(Fₚ)
170+
* is a large prime and P is already assumed to not be the neutral element.
171+
* 2. y2 == -y1. Again, then -2P == kP, k∈{1, ..., 13}, and we get the same contradiction.
167172
*/
168173
const auto& x1 = Tx_shift;
169174
const auto& y1 = Ty_shift;

‎barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_set_relation_impl.hpp‎

Lines changed: 5 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -145,7 +145,8 @@ Accumulator ECCVMSetRelationImpl<FF>::compute_grand_product_numerator(const AllE
145145
return negative_inverse_seven;
146146
}
147147
};
148-
auto adjusted_skew = precompute_skew * negative_inverse_seven();
148+
auto adjusted_skew =
149+
precompute_skew * negative_inverse_seven(); // `precompute_skew` ∈ {0, 7}, `adjusted_skew`∈ {0, -1}
149150

150151
const auto& wnaf_scalar_sum = View(in.precompute_scalar_sum);
151152
const auto w0 = convert_to_wnaf<Accumulator>(View(in.precompute_s1hi), View(in.precompute_s1lo));
@@ -168,7 +169,7 @@ Accumulator ECCVMSetRelationImpl<FF>::compute_grand_product_numerator(const AllE
168169
row_slice += row_slice;
169170
row_slice += row_slice;
170171
row_slice += row_slice;
171-
row_slice += w3;
172+
row_slice += w3; // row_slice = 2^12 w_0 + 2^8 w_1 + 2^4 w_2 + 2^0 w_3
172173

173174
auto scalar_sum_full = wnaf_scalar_sum + wnaf_scalar_sum;
174175
scalar_sum_full += scalar_sum_full;
@@ -186,7 +187,8 @@ Accumulator ECCVMSetRelationImpl<FF>::compute_grand_product_numerator(const AllE
186187
scalar_sum_full += scalar_sum_full;
187188
scalar_sum_full += scalar_sum_full;
188189
scalar_sum_full += scalar_sum_full;
189-
scalar_sum_full += row_slice + adjusted_skew;
190+
scalar_sum_full +=
191+
row_slice + adjusted_skew; // scalar_sum_full = 2^16 * wnaf_scalar_sum + row_slice + adjusted_skew
190192

191193
auto precompute_point_transition = View(in.precompute_point_transition);
192194

@@ -314,7 +316,6 @@ Accumulator ECCVMSetRelationImpl<FF>::compute_grand_product_denominator(const Al
314316

315317
auto lookup_first = (-z1_zero + 1);
316318
auto lookup_second = (-z2_zero + 1);
317-
// FF endomorphism_base_field_shift = FF::cube_root_of_unity();
318319
FF endomorphism_base_field_shift = FF(bb::fq::cube_root_of_unity());
319320

320321
auto transcript_input1 =
@@ -342,12 +343,6 @@ Accumulator ECCVMSetRelationImpl<FF>::compute_grand_product_denominator(const Al
342343
// point_table_init_write = degree 7
343344
auto point_table_init_write = transcript_mul * transcript_product + (-transcript_mul + 1);
344345
denominator *= point_table_init_write; // degree 17
345-
346-
// auto point_table_init_write_1 = transcript_mul * transcript_input1 + (-transcript_mul + 1);
347-
// denominator *= point_table_init_write_1; // degree-11
348-
349-
// auto point_table_init_write_2 = transcript_mul * transcript_input2 + (-transcript_mul + 1);
350-
// denominator *= point_table_init_write_2; // degree-14
351346
}
352347
/**
353348
* @brief Third term: tuple of (point-counter, P.x, P.y, msm-size) from ECCVMTranscriptRelation.

0 commit comments

Comments
 (0)