Clearmatics Libsnark  0.1
C++ library for zkSNARK proofs
alu_control_flow.tcc
Go to the documentation of this file.
1 /** @file
2  *****************************************************************************
3 
4  Implementation of interfaces for the TinyRAM ALU control-flow gadgets.
5 
6  See alu_control_flow.hpp .
7 
8  *****************************************************************************
9  * @author This file is part of libsnark, developed by SCIPR Lab
10  * and contributors (see AUTHORS).
11  * @copyright MIT license (see LICENSE file)
12  *****************************************************************************/
13 
14 #ifndef ALU_CONTROL_FLOW_TCC_
15 #define ALU_CONTROL_FLOW_TCC_
16 
17 #include <libff/common/profiling.hpp>
18 
19 namespace libsnark
20 {
21 
22 /* jmp */
23 template<typename FieldT>
24 void ALU_jmp_gadget<FieldT>::generate_r1cs_constraints()
25 {
26  this->pb.add_r1cs_constraint(
27  r1cs_constraint<FieldT>({ONE}, {this->argval2.packed}, {this->result}),
28  FMT(this->annotation_prefix, " jmp_result"));
29 }
30 
31 template<typename FieldT> void ALU_jmp_gadget<FieldT>::generate_r1cs_witness()
32 {
33  this->pb.val(this->result) = this->pb.val(this->argval2.packed);
34 }
35 
36 template<typename FieldT> void test_ALU_jmp_gadget()
37 {
38  libff::print_time("starting jmp test");
39 
40  tinyram_architecture_params ap(16, 16);
41  tinyram_program P;
42  P.instructions = generate_tinyram_prelude(ap);
43  tinyram_protoboard<FieldT> pb(ap, P.size(), 0, 10);
44 
45  word_variable_gadget<FieldT> pc(pb, "pc"), argval2(pb, "argval2");
46  pb_variable<FieldT> flag, result;
47 
48  pc.generate_r1cs_constraints(true);
49  argval2.generate_r1cs_constraints(true);
50  flag.allocate(pb, "flag");
51  result.allocate(pb, "result");
52 
53  ALU_jmp_gadget<FieldT> jmp(pb, pc, argval2, flag, result, "jmp");
54  jmp.generate_r1cs_constraints();
55 
56  pb.val(argval2.packed) = FieldT(123);
57  argval2.generate_r1cs_witness_from_packed();
58 
59  jmp.generate_r1cs_witness();
60 
61  assert(pb.val(result) == FieldT(123));
62  assert(pb.is_satisfied());
63  libff::print_time("positive jmp test successful");
64 
65  pb.val(result) = FieldT(1);
66  assert(!pb.is_satisfied());
67  libff::print_time("negative jmp test successful");
68 }
69 
70 /* cjmp */
71 template<typename FieldT>
72 void ALU_cjmp_gadget<FieldT>::generate_r1cs_constraints()
73 {
74  /*
75  flag1 * argval2 + (1-flag1) * (pc1 + 1) = cjmp_result
76  flag1 * (argval2 - pc1 - 1) = cjmp_result - pc1 - 1
77 
78  Note that instruction fetch semantics require program counter to
79  be aligned to the double word by rounding down, and pc_addr in
80  the outer reduction is expressed as a double word address. To
81  achieve this we just discard the first ap.subaddr_len() bits of
82  the byte address of the PC.
83  */
84  this->pb.add_r1cs_constraint(
85  r1cs_constraint<FieldT>(
86  this->flag,
87  pb_packing_sum<FieldT>(pb_variable_array<FieldT>(
88  this->argval2.bits.begin() + this->pb.ap.subaddr_len(),
89  this->argval2.bits.end())) -
90  this->pc.packed - 1,
91  this->result - this->pc.packed - 1),
92  FMT(this->annotation_prefix, " cjmp_result"));
93 }
94 
95 template<typename FieldT> void ALU_cjmp_gadget<FieldT>::generate_r1cs_witness()
96 {
97  this->pb.val(this->result) =
98  ((this->pb.val(this->flag) == FieldT::one())
99  ? FieldT(
100  this->pb.val(this->argval2.packed).as_ulong() >>
101  this->pb.ap.subaddr_len())
102  : this->pb.val(this->pc.packed) + FieldT::one());
103 }
104 
105 template<typename FieldT> void test_ALU_cjmp_gadget()
106 {
107  // TODO: update
108  libff::print_time("starting cjmp test");
109 
110  tinyram_architecture_params ap(16, 16);
111  tinyram_program P;
112  P.instructions = generate_tinyram_prelude(ap);
113  tinyram_protoboard<FieldT> pb(ap, P.size(), 0, 10);
114 
115  word_variable_gadget<FieldT> pc(pb, "pc"), argval2(pb, "argval2");
116  pb_variable<FieldT> flag, result;
117 
118  pc.generate_r1cs_constraints(true);
119  argval2.generate_r1cs_constraints(true);
120  flag.allocate(pb, "flag");
121  result.allocate(pb, "result");
122 
123  ALU_cjmp_gadget<FieldT> cjmp(pb, pc, argval2, flag, result, "cjmp");
124  cjmp.generate_r1cs_constraints();
125 
126  pb.val(argval2.packed) = FieldT(123);
127  argval2.generate_r1cs_witness_from_packed();
128  pb.val(pc.packed) = FieldT(456);
129  pc.generate_r1cs_witness_from_packed();
130 
131  pb.val(flag) = FieldT(1);
132  cjmp.generate_r1cs_witness();
133 
134  assert(pb.val(result) == FieldT(123));
135  assert(pb.is_satisfied());
136  libff::print_time("positive cjmp test successful");
137 
138  pb.val(flag) = FieldT(0);
139  assert(!pb.is_satisfied());
140  libff::print_time("negative cjmp test successful");
141 
142  pb.val(flag) = FieldT(0);
143  cjmp.generate_r1cs_witness();
144 
145  assert(pb.val(result) == FieldT(456 + 2 * ap.w / 8));
146  assert(pb.is_satisfied());
147  libff::print_time("positive cjmp test successful");
148 
149  pb.val(flag) = FieldT(1);
150  assert(!pb.is_satisfied());
151  libff::print_time("negative cjmp test successful");
152 }
153 
154 /* cnjmp */
155 template<typename FieldT>
156 void ALU_cnjmp_gadget<FieldT>::generate_r1cs_constraints()
157 {
158  /*
159  flag1 * (pc1 + inc) + (1-flag1) * argval2 = cnjmp_result
160  flag1 * (pc1 + inc - argval2) = cnjmp_result - argval2
161 
162  Note that instruction fetch semantics require program counter to
163  be aligned to the double word by rounding down, and pc_addr in
164  the outer reduction is expressed as a double word address. To
165  achieve this we just discard the first ap.subaddr_len() bits of
166  the byte address of the PC.
167  */
168  this->pb.add_r1cs_constraint(
169  r1cs_constraint<FieldT>(
170  this->flag,
171  this->pc.packed + 1 -
172  pb_packing_sum<FieldT>(pb_variable_array<FieldT>(
173  this->argval2.bits.begin() + this->pb.ap.subaddr_len(),
174  this->argval2.bits.end())),
175  this->result -
176  pb_packing_sum<FieldT>(pb_variable_array<FieldT>(
177  this->argval2.bits.begin() + this->pb.ap.subaddr_len(),
178  this->argval2.bits.end()))),
179  FMT(this->annotation_prefix, " cnjmp_result"));
180 }
181 
182 template<typename FieldT> void ALU_cnjmp_gadget<FieldT>::generate_r1cs_witness()
183 {
184  this->pb.val(this->result) =
185  ((this->pb.val(this->flag) == FieldT::one())
186  ? this->pb.val(this->pc.packed) + FieldT::one()
187  : FieldT(
188  this->pb.val(this->argval2.packed).as_ulong() >>
189  this->pb.ap.subaddr_len()));
190 }
191 
192 template<typename FieldT> void test_ALU_cnjmp_gadget()
193 {
194  // TODO: update
195  libff::print_time("starting cnjmp test");
196 
197  tinyram_architecture_params ap(16, 16);
198  tinyram_program P;
199  P.instructions = generate_tinyram_prelude(ap);
200  tinyram_protoboard<FieldT> pb(ap, P.size(), 0, 10);
201 
202  word_variable_gadget<FieldT> pc(pb, "pc"), argval2(pb, "argval2");
203  pb_variable<FieldT> flag, result;
204 
205  pc.generate_r1cs_constraints(true);
206  argval2.generate_r1cs_constraints(true);
207  flag.allocate(pb, "flag");
208  result.allocate(pb, "result");
209 
210  ALU_cnjmp_gadget<FieldT> cnjmp(pb, pc, argval2, flag, result, "cjmp");
211  cnjmp.generate_r1cs_constraints();
212 
213  pb.val(argval2.packed) = FieldT(123);
214  argval2.generate_r1cs_witness_from_packed();
215  pb.val(pc.packed) = FieldT(456);
216  pc.generate_r1cs_witness_from_packed();
217 
218  pb.val(flag) = FieldT(0);
219  cnjmp.generate_r1cs_witness();
220 
221  assert(pb.val(result) == FieldT(123));
222  assert(pb.is_satisfied());
223  libff::print_time("positive cnjmp test successful");
224 
225  pb.val(flag) = FieldT(1);
226  assert(!pb.is_satisfied());
227  libff::print_time("negative cnjmp test successful");
228 
229  pb.val(flag) = FieldT(1);
230  cnjmp.generate_r1cs_witness();
231 
232  assert(pb.val(result) == FieldT(456 + (2 * pb.ap.w / 8)));
233  assert(pb.is_satisfied());
234  libff::print_time("positive cnjmp test successful");
235 
236  pb.val(flag) = FieldT(0);
237  assert(!pb.is_satisfied());
238  libff::print_time("negative cnjmp test successful");
239 }
240 
241 } // namespace libsnark
242 
243 #endif // ALU_CONTROL_FLOW_TCC_
Generated on Wed Jan 25 2023 11:05:57 for Clearmatics Libsnark by   doxygen 1.8.17