- Generated by
1.9.8
|
Barretenberg
The ZK-SNARK library at the core of Aztec
|
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, 25 > | 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 |
Definition at line 35 of file ecc_transcript_relation.hpp.
| using bb::ECCVMTranscriptRelationImpl< FF_ >::FF = FF_ |
Definition at line 37 of file ecc_transcript_relation.hpp.
|
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
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_zero_at_transition is well-formed enough to bear witness to a correct computation.
If the current row is the last mul instruction in a multiscalar multiplication (i.e., if the next row is not a mul instruction), then check that msm_transition_zero_at_transition is constrained as follows: if it is 0, then msm_count + num_muls_in_row != 0 and is in fact the inverse of the (forced-to-be nonzero value of) msm_count_at_transition_inverse.
msm_transition_zero_at_transition to vanish outside of syntactic transitions (meaning when current row is a mul and next row is not a mul). similarly, msm_count_at_transition_inverse is not forced to vanish away from syntactic transitions. However, neither of these is necessary to witness a valid computation: the values away from syntactic transitions may be arbitrary, as the values of these two wires are only used to validate computations at syntactic transitions.Validate msm_transition is well-formed.
If the current row is the last mul instruction in a multiscalar multiplication, and if the putative MSM will have a positive number of terms, then msm_transition = 1. i.e., if q_mul == 1 and q_mul_shift == 0, and msm_count_total:= msm_count + num_muls_in_row > 0, then msm_transition = 1, else 0.
Validate msm_count is 0 when we are not at a mul op. msm_count tracks the number of scalar muls in the current active multiscalar multiplication. (if no msm active, msm_count == 0)
Validate msm_count updates correctly for mul operations. msm_count updates by (!z1_zero + !z2_zero) if current op is a mul instruction with the point not the point-at-infinity and msm is not terminating at next row.
Opcode exclusion tests. We have the following assertions:
eq opcode. Let lhs = transcript_P and rhs = transcript_accumulator If eq = 1, we must validate the following cases: IF lhs and rhs are not at infinity THEN lhs == rhs ELSE lhs and rhs are BOTH points at infinity
Boundary conditions. The first "content" row is the second row of the table.
We demand that the following values are present in this first content row: is_accumulator_empty == 1; and msm_count == 0. We also demand that pc == 0 at the last row.
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 as long as the point-at-infinity flag is off. As q_mul, q_add, and q_eq are pairwise mutually exclusive, the value q_add + q_mul + q_eq is boolean.
Validate relations from ECC Group Operations are well formed
Validate transcript_accumulator_x_shift / transcript_accumulator_y_shift are well formed. Conditions (one of the following):
Validate is_accumulator_empty is updated correctly An add operation can produce a point at infinity Resetting the accumulator produces a point at infinity If we are not adding, performing an msm or resetting the accumulator (or doing a no-op), is_accumulator_empty should not update
Validate transcript_add_x_equal is well-formed If lhs_x == rhs_x, transcript_add_x_equal = 1 If transcript_add_x_equal = 0, a valid inverse must exist for (lhs_x - rhs_x)
Validate transcript_add_y_equal is well-formed If lhs_y == rhs_y, transcript_add_y_equal = 1 If transcript_add_y_equal = 0, a valid inverse must exist for (lhs_y - rhs_y)
Definition at line 40 of file ecc_transcript_relation_impl.hpp.
|
inlinestaticconstexpr |
Definition at line 50 of file ecc_transcript_relation.hpp.
|
staticconstexpr |
Definition at line 39 of file ecc_transcript_relation.hpp.
1.9.8