|
barretenberg
|
ECCVMTranscriptRelationImpl evaluates the correctness of the ECCVM transcript columns. More...
#include <ecc_transcript_relation.hpp>
Public Types | |
| using | FF = FF_ |
Static Public Member Functions | |
| template<typename ContainerOverSubrelations , typename AllEntities , typename Parameters > | |
| static void | accumulate (ContainerOverSubrelations &accumulator, const AllEntities &in, const Parameters &, const FF &scaling_factor) |
| ECCVMTranscriptRelationImpl evaluates the correctness of the ECCVM transcript columns. | |
| static constexpr FF | get_curve_b () |
Static Public Attributes | |
| static constexpr std::array< size_t, 35 > | SUBRELATION_PARTIAL_LENGTHS |
ECCVMTranscriptRelationImpl evaluates the correctness of the ECCVM transcript columns.
The transcript relations directly evaluate the correctness of add, eq, reset operations. mul operations are lazily evaluated. The output of multiscalar multiplications is present in transcript_msm_x, transcript_msm_y columns. A set equality check is used to validate these have been correctly read from a table produced by the relations in ecc_msm_relation.hpp.
Sequential mul opcodes are interpreted as a multiscalar multiplication. The column transcript_msm_count tracks the number of muls in a given multiscalar multiplication.
The column transcript_pc tracks a "point counter" value, that describes the number of multiplications that must be evaluated.
One mul opcode can generate up to TWO multiplications. Each 128-bit scalar z1, z2 is treated as an independent mul. The purpose of this is to reduce the length of the MSM algorithm evalauted in ecc_msm_relation.hpp to 128 bits (from 256 bits). Many scalar muls required to recursively verify a proof are only 128-bits in length; this prevents us doing redundant computation.
| FF |
|
static |
ECCVMTranscriptRelationImpl evaluates the correctness of the ECCVM transcript columns.
The transcript relations directly evaluate the correctness of add, eq, reset operations. mul operations are lazily evaluated. The output of multiscalar multiplications is present in transcript_msm_x, transcript_msm_y columns. A set equality check is used to validate these have been correctly read from a table produced by the relations in ecc_msm_relation.hpp.
Sequential mul opcodes are interpreted as a multiscalar multiplication. The column transcript_msm_count tracks the number of muls in a given multiscalar multiplication.
The column transcript_pc tracks a "point counter" value, that describes the number of multiplications that must be evaluated.
One mul opcode can generate up to TWO multiplications. Each 128-bit scalar z1, z2 is treated as an independent mul. The purpose of this is to reduce the length of the MSM algorithm evalauted in ecc_msm_relation.hpp to 128 bits (from 256 bits). Many scalar muls required to recursively verify a proof are only 128-bits in length; this prevents us doing redundant computation.
| FF | |
| AccumulatorTypes | |
| PolynomialTypes |
Validate correctness of z1_zero, z2_zero. If z1_zero = 0 and operation is a MUL, we will write a scalar mul instruction into our multiplication table. If z1_zero = 1 and operation is a MUL, we will NOT write a scalar mul instruction. (same with z2_zero). z1_zero / z2_zero is user-defined. We constraint z1_zero such that if z1_zero == 1, we require z1 == 0. (same for z2_zero). We do NOT constrain z1 != 0 if z1_zero = 0. If the user sets z1_zero = 0 and z1 = 0, this will add a scalar mul instruction into the multiplication table, where the scalar multiplier is 0. This is inefficient but will still produce the correct output.
Validate op opcode is well formed. op is defined to be q_reset_accumulator + 2 * q_eq + 4 * q_mul + 8 * q_add, where q_reset_accumulator, q_eq, q_mul, q_add are all boolean (TODO: bool constrain these efficiently #2223)
Validate pc is updated correctly. pc stands for Point Counter. It decrements by 1 for every 128-bit multiplication operation. If q_mul = 1, pc decrements by !z1_zero + !z2_zero, else pc decrements by 0
Validate msm_transition is well-formed.
If the current row is the last mul instruction in a multiscalar multiplication, msm_transition = 1. i.e. if q_mul == 1 and q_mul_shift == 0, msm_transition = 1, else is 0
Validate msm_count resets when we end a multiscalar multiplication. msm_count tracks the number of scalar muls in the current active multiscalar multiplication. (if no msm active, msm_count == 0) If current row ends an MSM, msm_count_shift = 0 (msm_count value at next row)
Validate msm_count updates correctly for mul operations. msm_count updates by (!z1_zero + !z2_zero) if current op is a mul instruction (and msm is not terminating at next row).
Add multiscalar multiplication result into transcript accumulator. If msm_transition == 1, we expect msm output to be present on (transcript_msm_x, transcript_msm_y). (this is enforced via a lookup protocol). If is_accumulator_empty == 0, we ADD msm output into transcript_accumulator. If is_accumulator_empty = =1, we ASSIGN msm output to transcript_accumulator.
If is_accumulator_empty == 1, assign transcript_accumulator output into accumulator
i is the accumulator point at row i + 1!Constrain add opcode.
add will add the input point in (transcript_Px, transcript_Py) into the accumulator. Correctly handles case where accumulator is point at infinity. TODO: need to add constraints to rule out point doubling case (x2 != x1) TODO: need to assert input point is on the curve!
Opcode exclusion tests. We have the following assertions:
eq opcode. If eq = 1, assert transcript_Px/y = transcript_accumulator_x/y. If eq = 1, assert is_accumulator_empty = 0 (input point cannot be point at infinity)Initial condition check on 1st row. We require the following values are 0 on 1st row: is_accumulator_empty = 1 msm_count = 0 note...actually second row? bleurgh NOTE: we want pc = 0 at lagrange_last :o
On-curve validation checks. If q_mul = 1 OR q_add = 1 OR q_eq = 1, require (transcript_Px, transcript_Py) is valid ecc point q_mul/q_add/q_eq mutually exclusive, can represent as sum of 3
If performing an add, validate x-coordintes of inputs do not collide. If adding msm output into accumulator, validate x-coordinates of inputs do not collide
|
staticconstexpr |
1.9.6