Zero Knowledge Proof —Deep into libsnark
I recommend libsnark source code to folks interested to dive deep in Zero-Knowledge Proof. Bellman library is based on the Groth 16 algorithm. And libsnark offers an overlook of related SNARK algorithmes, such as the various Relation, Language and Proof System. libsnark extracts Protoboard and Gadget in order to find a smarter way to generate R1CS circuit, in convenience for developers to build the circuit faster.
The last commit for libsnark source code mentioned in this article is shown below:
commit 477c9dfd07b280e42369f82f89c08416319e24ae
Author: Madars Virza <madars@mit.edu>
Date: Tue Jun 18 18:43:12 2019 -0400Document that we also implement the Groth16 proof system.
1. Source code directory
Source code is under libsnark directory:
common — defines and implements common data structures, i.e. Merkle tree, sparse vector, etc.
relations — describe the “constraint” relationship. There are many other languages that desctibe such constraint besides the R1CS that we often mention.
reductions — translate between different description languages.
knowledge_commit — indroduces the concept of “pair”, two nodes with one coefficient, based on multiexp. We call the result of calculation a pair.
zk_proof_systems — various proofing systems in zero-knowledge proof (including Groth16, GM17, etc).
gadgetlib1/gadgetlib2 — libsnark extracts a layer of gadget to construct R1CS more conviniently. We can utilize and integrate the existing gadget to build new circuits.
2. Relation
All problems that require zero-knowledge proof are NP problems. There is one type of NP problems called NP-complete. Essentially, any NP problem can be transformed into any of the NP-complete problems. If there exists one NP-complete problem that can be solved in polynomial time, then all NP pronlems can be solved in polynomial time. There are multiple ways to describe an NP-complete problem. We refer to these ways to describe NP-complete problems as “language”. And Relation means the relationship between an NP-complete problem and its solution.
libsnark library summarizes several description languages:
constraint satisfaction problem type
- R1CS — Rank-1 Constraint System
- USCS — Unitary-Square Constraint System
circuit satisfaction problem type
- BACS — Bilinear Arithmetic Circuit Satisfiability
- TBCS — Two-input Boolean Circuit Satisfiability
ram computation type
RAM is acronym for Random Access Machine. libsnark summarizes two types of RAM frameworks:
- tinyRAM
- fooRAM
- arithmetic program type
- QAP — Quadratic Arithmetic Program（GGPR13）
- SQP — Square Arithmetic Program（GM17）
- SSP — Square Span Program (DFGK14)
I will first introduce the “viariable” needed for implementation in multiple languages (variable.hpp/variable.tcc), then go over the the details on R1CS and QAP language.
2.1 variable
template<typename FieldT>
class variable {
public:
var_index_t index;
...
};Definition of variable is simple. To describe a variable, all you need is an index that correspondes to the variable. For example, the variable with “index” as its index, stands for x_{index} variable.
2.2 linear_term
linear_term makes up one part of linear combination. An instance of linear term consists of a variable and its coefficient:
template<typename FieldT>
class linear_term {
public:
var_index_t index;
FieldT coeff;
...
};2.3 linear_combination
linear_combination defines a full linear combination. One linear combination is composed of multiple linear terms:
template<typename FieldT>
class linear_combination {
public:
std::vector<linear_term<FieldT> > terms;
...
};2.4 R1CS
R1CS is defined in constraint_satisfaction_problems/r1cs/r1cs.hpp. R1CS constraint is satisfied by following the expression:
< A , X > * < B , X > = < C , X >
x is the vector for all variable combinations. A/B/C is has the same length as x. <,> stands for dot product. One R1CS system is made up of multiple R1CS constraints.
R1CS constraint is defined as follows:
template<typename FieldT>
class r1cs_constraint {
public:
linear_combination<FieldT> a, b, c;
...
};One R1CS constraint can be written in three linear_combinations of a/b/c.
In an R1CS system, the variable assignment can be divided into two parts: primary input and auxiliary input. Primary means “statement”, while auxiliary means “witness”.
template<typename FieldT>
using r1cs_primary_input = std::vector<FieldT>;
template<typename FieldT>
using r1cs_auxiliary_input = std::vector<FieldT>;An R1CS system consists of multiple R1CS constraints. Needless to say, each vector constraint comes with fixed length (primary input size + auxiliary input size + 1).
template<typename FieldT>
class r1cs_constraint_system {
public:
size_t primary_input_size;
size_t auxiliary_input_size;
std::vector<r1cs_constraint<FieldT> > constraints;
...
}2.5 QAP
QAP is degined in arithmetic_programs/qap/qap.hpp. libsnark uses QAP formulaA*B-C=H*Z。
template<typename FieldT>
class qap_instance {
private:
size_t num_variables_;
size_t degree_;
size_t num_inputs_;
public:
std::shared_ptr<libfqfft::evaluation_domain<FieldT> > domain;
std::vector<std::map<size_t, FieldT> > A_in_Lagrange_basis;
std::vector<std::map<size_t, FieldT> > B_in_Lagrange_basis;
std::vector<std::map<size_t, FieldT> > C_in_Lagrange_basis;
}num_variables_ stands for count of QAP circuit variables. num_inputs_ stands for count of variables related to “statement” of a QAP circuit. degree_ stands for count of orders of each polynomial in A/B/C (which is related to count of circuit gates).
domain is the engine for calculating Fourier transform and inverse Fourier transform, which is implemented by using libfqfft library.
What is Lagrange basis？
Given a series of functions of x and y, we can come up with a polynomial by Lagrange polynomial interpolation:
p(x) = y_0l_0(x) + y_1l_1(x) + … + y_nl_n(x)
where l_0(x), l_1(x), … l_n(x) is called Lagrange basis.
A_in_Lagrange_basis/B_in_Lagrange_basis/C_in_Lagrange_basis integrates values for different gates in each variable exsiting in one circuit. For example, below is the R1CS constraint for a x³+x+5 circuit:
The corresponding A_in_Lagrange_basis/B_in_Lagrange_basis/C_in_Lagrange_basis is:
qap_instance describes a QAP circuit. corresponding A/B/C polynomial written in Lagrange basis. Apply A/B/C polynomial on one point, and use qap_instance_evaluation to reflect the result:
template<typename FieldT>
class qap_instance_evaluation {
private:
size_t num_variables_;
size_t degree_;
size_t num_inputs_;
public:
std::shared_ptr<libfqfft::evaluation_domain<FieldT> > domain;
FieldT t;
std::vector<FieldT> At, Bt, Ct, Ht;
FieldT Zt;
...
}qap_instance_evaluation: notes A/B/C/H and corresponding Z values on t point.
Given a QAP circuit, the corresponding primary/auxiliary is called witness, defined as:
template<typename FieldT>
class qap_witness {
private:
size_t num_variables_;
size_t degree_;
size_t num_inputs_;
public:
FieldT d1, d2, d3;
std::vector<FieldT> coefficients_for_ABCs;
std::vector<FieldT> coefficients_for_H;
...
}coefficients_for_ABCs is witness. For the ease of calculation, it also gives the corresponding coefficients for H polynomial. Given a qap_instance_evaluation and a qap_witness, we can evaluate the rationality of witness by is_satisfied function.
template<typename FieldT>
bool qap_instance_evaluation<FieldT>::is_satisfied(const qap_witness<FieldT> &witness) const
{
...
ans_A = ans_A + libff::inner_product<FieldT>(this->At.begin()+1,
this->At.begin()+1+this->num_variables(),witness.coefficients_for_ABCs.begin(),witness.coefficients_for_ABCs.begin()+this->num_variables());
ans_B = ans_B + libff::inner_product<FieldT>(this->Bt.begin()+1,
this->Bt.begin()+1+this->num_variables(),witness.coefficients_for_ABCs.begin(),witness.coefficients_for_ABCs.begin()+this->num_variables());
ans_C = ans_C + libff::inner_product<FieldT>(this->Ct.begin()+1,
this->Ct.begin()+1+this->num_variables(),witness.coefficients_for_ABCs.begin(),witness.coefficients_for_ABCs.begin()+this->num_variables());
ans_H = ans_H + libff::inner_product<FieldT>(this->Ht.begin(),
this->Ht.begin()+this->degree()+1,
witness.coefficients_for_H.begin(),
witness.coefficients_for_H.begin()+this->degree()+1);
if (ans_A * ans_B - ans_C != ans_H * this->Zt)
{
return false;
}
...
}To validate a witness, is to check if wA*wB-w*C = HZ is current.
3. Reduction
Reduction implements the translation between different description languages. libsnark gives the following series of translation:
- bacs -> r1cs
- r1cs -> qap
- r1cs -> sap
- ram -> r1cs
- tbcs -> uscs
- uscs -> ssp
Take r1cs->qap as an exmaple. Let us walk through the logic of Reduction. To transform from R1CS to QAP, we find three functions defined in reductions/r1cs_to_qap/ directory:
3.1 r1cs_to_qap_instance_map
r1cs_to_qap_instance_map realizes an instance transform from R1CS to QAP. The transfrom process is rather easy — it is a process of reassining the coefficients (check QAP instructions in section 2.5).
3.2 r1cs_to_qap_instance_map_with_evaluation
Function r1cs_to_qap_instance_map_with_evaluation implements implements an instance transform from R1CS to qap_instance_evaluation. Given value of t, we want to calculate A/B/C and H/Z.
3.3 r1cs_to_qap_witness_map
Function r1cs_to_qap_witness_map implements an instance transform from R1CS to qap_witness.
template<typename FieldT>
qap_witness<FieldT> r1cs_to_qap_witness_map(const r1cs_constraint_system<FieldT> &cs,
const r1cs_primary_input<FieldT> &primary_input,
const r1cs_auxiliary_input<FieldT> &auxiliary_input,
const FieldT &d1,
const FieldT &d2,
const FieldT &d3)Given primary/auxiliary input, we want to get witness (coefficient for A/B/C and H). d1/d2/d3 gives us expandability during H coefficient calculation. When we use Groth16 during calculation, d1/d2/d3 takes value of 0.
Given primary/auxiliary input, it is easy to get coefficients of A/B/C, by a simple concatenation of primary/auxiliary input.
r1cs_variable_assignment<FieldT> full_variable_assignment = primary_input;
full_variable_assignment.insert(full_variable_assignment.end(), auxiliary_input.begin(), auxiliary_input.end());When it comes to coefficient for the H polynomial, things get relatively comlex , involving Fourier transform and inverse Fourier transform. The formula for H polynomial is as following:
H(z) := (A(z)*B(z)-C(z))/Z(z)
Note that A(z) := A_0(z) + w_1 A_1(z) + … + w_m A_m(z) + d1 * Z(z)，B(z) := B_0(z) + w_1 B_1(z) + … + w_m B_m(z) + d2 * Z(z)，C(z) := C_0(z) + w_1 C_1(z) + … + w_m C_m(z) + d3 * Z(z), Z(z) = (z-sigma_1)(z-sigma_2)…(z-sigma_n)（m is count of variables in QAP circuit, n is count of gates in QAP circuit ). Pay special attention to A(z)/B(z)/C(z) , it is the sum for multiple polynomials, not corresponsing polynomial for each variable.
1/ Establish A and B polynomial (by inverse Fourier transform)
for (size_t i = 0; i < cs.num_constraints(); ++i)
{
aA[i] += cs.constraints[i].a.evaluate(full_variable_assignment);
aB[i] += cs.constraints[i].b.evaluate(full_variable_assignment);
}
domain->iFFT(aA);
domain->iFFT(aB);2/ Calculate A and B corresponds FieldT::multiplicative_generator
domain->cosetFFT(aA, FieldT::multiplicative_generator);
domain->cosetFFT(aB, FieldT::multiplicative_generator);3/ Establish C polynomial (by inverse Fourier Transform)
for (size_t i = 0; i < cs.num_constraints(); ++i)
{
aC[i] += cs.constraints[i].c.evaluate(full_variable_assignment);
}
domain->iFFT(aC);4/ Calculate C corresponds FieldT::multiplicative_generator
domain->cosetFFT(aC, FieldT::multiplicative_generator);5/ Calculate H corresponds FieldT::multiplicative_generator
for (size_t i = 0; i < domain->m; ++i)
{
H_tmp[i] = aA[i]*aB[i];
}
for (size_t i = 0; i < domain->m; ++i)
{
H_tmp[i] = (H_tmp[i]-aC[i]);
}
domain->divide_by_Z_on_coset(H_tmp);6/ Calculate coefficient for H polynomial (by inverse Fourier Transform)
domain->icosetFFT(H_tmp, FieldT::multiplicative_generator);4. ZK Proof System
libsnark provides four proving systems:
- pcd (Proof-Carrying Data)
- ppzkadsnark (PreProcessing Zero-Knowledge Succinct Non-interactive ARgument of Knowledge Over Authenticated Data)
- ppzksnark (PreProcessing Zero-Knowledge Succinct Non-interactive ARgument of Knowledge)
- zksnark (Zero-Knowledge Succinct Non-interactive ARgument of Knowledge)
The famouns Groth16 algorithms belongs to ppzksnark. SInce pre-process and generate CRS is required before Groth16 proving. ppzksnark can be divided in several types:
Among them:
r1cs_gg_ppzksnark, gg stands for General Group, aka Groth16 algorithm.
r1cs_se_ppzksnark, se stands for Simulation Extractable, aka GM17 algorithm.
r1cs_ppzksnark, also referred as PGHR13.
Take Groth16 algorithm (r1cs_gg_ppzksnark) as an example, let us go over the logic. Groth16 algorithm and related logic is documented under zk_proof_systems/ppzksnark/r1cs_gg_ppzksnark directory.
4.1 r1cs_gg_ppzksnark_proving_key
r1cs_gg_ppzksnark_proving_key records information required for proving in CRS.
template<typename ppT>
class r1cs_gg_ppzksnark_proving_key {
public:
libff::G1<ppT> alpha_g1;
libff::G1<ppT> beta_g1;
libff::G2<ppT> beta_g2;
libff::G1<ppT> delta_g1;
libff::G2<ppT> delta_g2;
libff::G1_vector<ppT> A_query;
knowledge_commitment_vector<libff::G2<ppT>, libff::G1<ppT> > B_query;
libff::G1_vector<ppT> H_query;
libff::G1_vector<ppT> L_query;
r1cs_gg_ppzksnark_constraint_system<ppT> constraint_system;
...
}A_query is result for A(t) multiexp based on G1 as generator.
B_query is result for B(t) multiexp based on G1/G2 as generator.
H_query is result for following expression multiexp based on G1 as generator.:
H(t)*Z(t)/delta
L_query is result for following expression multiexp based on G1 as generator.:(beta*A(t)+alpha*B(t)+C(t))/delta
That is to say, r1cs_gg_ppzksnark_proving_key gives the CRS information of Groth16 algorithm (highlighted in blue):
r1cs_gg_ppzksnark_constraint_system<ppT> is defined in zk_proof_systems/ppzksnark/r1cs_gg_ppzksnark/r1cs_gg_ppzksnark_params.hpp.
template<typename ppT>
using r1cs_gg_ppzksnark_constraint_system = r1cs_constraint_system<libff::Fr<ppT> >;This means r1cs_gg_ppzksnark_constraint_system is r1cs_constraint_system。
4.2 r1cs_gg_ppzksnark_verification_key
r1cs_gg_ppzksnark_verification_keyrecords information required for verify in CRS.
template<typename ppT>
class r1cs_gg_ppzksnark_verification_key {
public:
libff::GT<ppT> alpha_g1_beta_g2;
libff::G2<ppT> gamma_g2;
libff::G2<ppT> delta_g2;
accumulation_vector<libff::G1<ppT> > gamma_ABC_g1;
...
}In another word, r1cs_gg_ppzksnark_verification_key gives following inormation about CRS in Groth16 (highlighted in blue)
4.3 r1cs_gg_ppzksnark_processed_verification_key
r1cs_gg_ppzksnark_processed_verification_key is similar to r1cs_gg_ppzksnark_verification_key. “processed” means verification key will take next step, and the verification process can move faster.
template<typename ppT>
class r1cs_gg_ppzksnark_processed_verification_key {
public:
libff::GT<ppT> vk_alpha_g1_beta_g2;
libff::G2_precomp<ppT> vk_gamma_g2_precomp;
libff::G2_precomp<ppT> vk_delta_g2_precomp;
accumulation_vector<libff::G1<ppT> > gamma_ABC_g1;
...
}4.4 r1cs_gg_ppzksnark_keypair
r1cs_gg_ppzksnark_keypair includes two parts: r1cs_gg_ppzksnark_proving_key and r1cs_gg_ppzksnark_verification_key.
template<typename ppT>
class r1cs_gg_ppzksnark_keypair {
public:
r1cs_gg_ppzksnark_proving_key<ppT> pk;
r1cs_gg_ppzksnark_verification_key<ppT> vk;
...
}4.5 r1cs_gg_ppzksnark_proof
As we all know, Groth16 algorithm’s proof includes three results A/B/C.
template<typename ppT>
class r1cs_gg_ppzksnark_proof {
public:
libff::G1<ppT> g_A;
libff::G2<ppT> g_B;
libff::G1<ppT> g_C;
...
}4.6 r1cs_gg_ppzksnark_generator
Given an r1cs_constraint_system, r1cs_gg_ppzksnark_generator can generate r1cs_gg_ppzksnark_keypair. Also known as generating CRS information.
template<typename ppT>
r1cs_gg_ppzksnark_keypair<ppT> r1cs_gg_ppzksnark_generator(const r1cs_gg_ppzksnark_constraint_system<ppT> &cs);4.7 r1cs_gg_ppzksnark_prover
Given proving key and primary/auxiliary input, calculate the A/B/C result of proof.
template<typename ppT>
r1cs_gg_ppzksnark_proof<ppT> r1cs_gg_ppzksnark_prover(const r1cs_gg_ppzksnark_proving_key<ppT> &pk,
const r1cs_gg_ppzksnark_primary_input<ppT> &primary_input,
const r1cs_gg_ppzksnark_auxiliary_input<ppT> &auxiliary_input);With known proving key, it is staright forward to get valules for A/B/C:
/* A = alpha + sum_i(a_i*A_i(t)) + r*delta */
libff::G1<ppT> g1_A = pk.alpha_g1 + evaluation_At + r * pk.delta_g1;
/* B = beta + sum_i(a_i*B_i(t)) + s*delta */
libff::G1<ppT> g1_B = pk.beta_g1 + evaluation_Bt.h + s * pk.delta_g1;
libff::G2<ppT> g2_B = pk.beta_g2 + evaluation_Bt.g + s * pk.delta_g2;
/* C = sum_i(a_i*((beta*A_i(t) + alpha*B_i(t) + C_i(t)) + H(t)*Z(t))/delta) + A*s + r*b - r*s*delta */
libff::G1<ppT> g1_C = evaluation_Ht + evaluation_Lt + s * g1_A + r * g1_B - (r * s) * pk.delta_g1;4.8 r1cs_gg_ppzksnark_verifier
r1cs_gg_ppzksnark_verifier provides four verification functions, and there are two types of them: processed/non-processed and weak/strong IC. processed/non-processed means whether the verification key is processed or not. weak/strong IC means whether the input is consist. If the size of primary input is equal to size of QAP statement, we call it strong IC. Otherwise, if the size of Primary input is smaller than the size of QAP statement, we call it weak IC.
Take r1cs_gg_ppzksnark_verifier_strong_IC as an example. Given verification key/primary input, we can verify if the proof is correct.
template<typename ppT>
bool r1cs_gg_ppzksnark_verifier_strong_IC(const r1cs_gg_ppzksnark_verification_key<ppT> &vk,const r1cs_gg_ppzksnark_primary_input<ppT> &primary_input,const r1cs_gg_ppzksnark_proof<ppT> &proof);
In general, the following diagram shows the generation and verification of a Groth16 proof:
We can see that a r1cs_constraint_system needs to be built to use ZKSNARK(Groth16) proof. To construct such system, libsnark designed the Gadget framework.
5. Gadget
libsnark provides two Gadget libraries: gadgetlib1 and gadgetlib2. Many of the examples in libsnark are based on gadgetlib1. gadgetlib1 also provides more variaties of gadget to choose from. Thie article primarity focus on gadgetlib1 logic. gadgetlib1 source code is located at libsnark/gadgetlib1 directory.
5.1 protoboard
protoboard is encapsulation of r1cs_constraint_system. Through each Gadget, it adds constraits to r1cs_constraint_system. In order to standardize variable and Lc among diffrent Gadget, protoboard monitors Variables and Lc created by all the Gadgets through ”next_free_var” and “next_free_lc”.
template<typename FieldT>
class protoboard {
...
FieldT constant_term;
r1cs_variable_assignment<FieldT> values;
var_index_t next_free_var;
lc_index_t next_free_lc;
std::vector<FieldT> lc_values;
r1cs_constraint_system<FieldT> constraint_system;
...
}5.2 pb_variable
libsnark has four types: pb_variable，pb_variable_array，pb_linear_combination and pb_linear_combination_array as encapsulations for variable and linear_combination to support management of protoboard.
5.3 gadget
gadget’s definition is pretty straight forward:
template<typename FieldT>
class gadget {
protected:
protoboard<FieldT> &pb;
const std::string annotation_prefix;
public:
gadget(protoboard<FieldT> &pb, const std::string &annotation_prefix="");
};Following steps needs to be done to every specific Gadget logic:
1/ allocate space to Variable or Lc （allocate）
2/ add constraints related to Gadget logic（generate_r1cs_constraints）
3/ generate corresponding Witness（generate_r1cs_witness）
5.4 example
There are many Gadget implementations under gadgetlib1/gadgets directory: Elliptic Curve Computation, hash algorithms, Merkle tree algorithms, Pairing function, and so on. This article takes comparison gadget from basic gadget as an example to illustrate the Gadget logic.
comparison_gadget is defined in gadgetlib1/gadgets/basic_gadgets.hpp:
comparison_gadget(protoboard<FieldT>& pb,
const size_t n,
const pb_linear_combination<FieldT> &A,
const pb_linear_combination<FieldT> &B,
const pb_variable<FieldT> &less,
const pb_variable<FieldT> &less_or_eq,
const std::string &annotation_prefix="") :
gadget<FieldT>(pb, annotation_prefix), n(n), A(A), B(B), less(less), less_or_eq(less_or_eq)
{
alpha.allocate(pb, n, FMT(this->annotation_prefix, " alpha"));
alpha.emplace_back(less_or_eq); // alpha[n] is less_or_eq
alpha_packed.allocate(pb, FMT(this->annotation_prefix, " alpha_packed"));
not_all_zeros.allocate(pb, FMT(this->annotation_prefix, " not_all_zeros"));
pack_alpha.reset(new packing_gadget<FieldT>(pb, alpha, alpha_packed, FMT(this->annotation_prefix, " pack_alpha")));
all_zeros_test.reset(new disjunction_gadget<FieldT>(pb, pb_variable_array<FieldT>(alpha.begin(), alpha.begin() + n),not_all_zeros, FMT(this->annotation_prefix, " all_zeros_test")));
};The logic of comparison_gadget constructor is prrety clear: given two n-digit number A and B, output two variables: less and less_or_eq (a < b?). The constructor creates Gadget and other variables.
alpha is an array of length n+1. alpha[n] is less_or_eq. alpha denotes digits of 2^n+B-A. alpha_packed is a variable, the value associated with alpha. That is to say, alpha_packed = 2^n+B-A.
not_all_zeros is a variable, meaning whether results for B-A are all zero. pack_alpha is packing_gadget. Pack the (n+1) digits of alpha, and store the result in alpha_packed. packing_gadget shows the data with value, indead of with digits. all_zeros_test is disjunction_gadget，whether the n variables of alpha are all zero. comparison_gadget and generate_r1cs_constraints function add constraints.
template<typename FieldT>
void comparison_gadget<FieldT>::generate_r1cs_constraints()
{
generate_boolean_r1cs_constraint<FieldT>(this->pb, not_all_zeros, FMT(this->annotation_prefix, " not_all_zeros"));
pack_alpha->generate_r1cs_constraints(true);
this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(1, (FieldT(2)^n) + B - A, alpha_packed), FMT(this->annotation_prefix, " main_constraint"));
all_zeros_test->generate_r1cs_constraints();
this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(less_or_eq, not_all_zeros, less), FMT(this->annotation_prefix, " less"));
}a. Add boolean constraint to not_all_zeros (this variable can only be 0 or 1). b. pack_alpha->generate_r1cs_constraints(true) constraints the alpha pointer to value alpha_packed. c. 1*(2^n+B-A) = alpah_packed d. not_all_zeros variable value is equal to count of variables that equal to 0 from the n variables in alpha. e. less_or_eq * not_all_zeros = less
The complete circuit logic for comparison_gadget is shown below: figure 12
comparison_gadget design principle is:
If B — A > 0, then 2^n + B — A > 2^n, less_or_eq = 1, not_all_zeros = 1
If B — A = 0, then 2^n + B — A = 2^n, less_or_eq = 1, not_all_zeros = 0
If B — A < 0, then 2^n + B — A in range {0, 1, …, 2^n-1}, less_or_eq = 0，not_all_zeros = 1
That is to say, less_or_eq * not_all_zeros = less。
To put it in a simple way, to compare the value of two numbers, we compute product of certain “symbol” location of 2^n + B — A.
Function generate_r1cs_witness from comparison_gadget generates the witness of circuit. Function test_comparison_gadget from comparison_gadget is the test function for comparison gadget, and it is easy to comprehend. Folks can feel free to go through the source code.
Conclusion:
libsnark libraries has very clear layers. Most importantly, libsnark gives an overlook of SNARK related algorithms, such as the Relation, Language, Proof System. To better generate R1CS circuit, libsnark extracts protoboard and gadget, for the convenience of developers to rapidly construct circuits.
