Barretenberg
The ZK-SNARK library at the core of Aztec
Loading...
Searching...
No Matches
subcircuits.test.cpp
Go to the documentation of this file.
1// #include <iostream>
2// #include <string>
3
4// #include "barretenberg/stdlib/primitives/field/field.hpp"
5// #include "barretenberg/stdlib_circuit_builders/standard_circuit_builder.hpp"
6
7// #include "barretenberg/smt_verification/circuit/subcircuits.hpp"
8
9// #include <gtest/gtest.h>
10
11// using namespace bb;
12
13// // Check that all the relative offsets are calculated correctly.
14// // I.e. I can find an operand at the index, given by get_standard_range_constraint_circuit
15// TEST(Subcircuits, range_circuit)
16// {
17// for (size_t i = 1; i < 255; i++) {
18// smt_subcircuits::CircuitProps range_props = smt_subcircuits::get_standard_range_constraint_circuit(i);
19// smt_circuit_schema::CircuitSchema circuit = range_props.circuit;
20
21// size_t a_gate = range_props.gate_idxs[0];
22// uint32_t a_gate_idx = range_props.idxs[0];
23// size_t start_gate = range_props.start_gate;
24
25// ASSERT_EQ(
26// "a",
27// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
28// a_gate][a_gate_idx]]]);
29
30// size_t num_accs = range_props.gate_idxs.size() - 1;
31// for (size_t j = 1; j < num_accs + 1; j++) {
32// size_t acc_gate = range_props.gate_idxs[j];
33// uint32_t acc_gate_idx = range_props.idxs[j];
34// ASSERT_EQ("acc_" + std::to_string(num_accs - j),
35// circuit.vars_of_interest
36// [circuit.real_variable_index[circuit.wires[0][start_gate + acc_gate][acc_gate_idx]]]);
37// }
38// }
39// }
40// // Check that all the relative offsets are calculated correctly.
41// // I.e. I can find all three operands at the indices, given by get_standard_logic_circuit
42// TEST(Subcircuits, logic_circuit)
43// {
44// for (size_t i = 2; i < 256; i += 2) {
45// smt_subcircuits::CircuitProps logic_props = smt_subcircuits::get_standard_logic_circuit(i, true);
46// smt_circuit_schema::CircuitSchema circuit = logic_props.circuit;
47
48// size_t a_gate = logic_props.gate_idxs[0];
49// uint32_t a_gate_idx = logic_props.idxs[0];
50// size_t start_gate = logic_props.start_gate;
51// ASSERT_EQ(
52// "a",
53// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
54// a_gate][a_gate_idx]]]);
55
56// size_t b_gate = logic_props.gate_idxs[1];
57// uint32_t b_gate_idx = logic_props.idxs[1];
58// ASSERT_EQ(
59// "b",
60// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
61// b_gate][b_gate_idx]]]);
62
63// size_t c_gate = logic_props.gate_idxs[2];
64// uint32_t c_gate_idx = logic_props.idxs[2];
65// ASSERT_EQ(
66// "c",
67// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
68// c_gate][c_gate_idx]]]);
69// }
70// }
71
72// // Check that all the relative offsets are calculated correctly.
73// // I.e. I can find all three operands at the indices, given by get_standard_logic_circuit
74// TEST(Subcircuits, ror_circuit)
75// {
76// for (uint32_t r = 1; r < 8; r += 1) {
77// unsigned char n = 8;
78// smt_subcircuits::CircuitProps ror_props = smt_subcircuits::get_standard_ror_circuit(n, r);
79// smt_circuit_schema::CircuitSchema circuit = ror_props.circuit;
80
81// size_t a_gate = ror_props.gate_idxs[0];
82// uint32_t a_gate_idx = ror_props.idxs[0];
83// size_t start_gate = ror_props.start_gate;
84// ASSERT_EQ(
85// "a",
86// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
87// a_gate][a_gate_idx]]]);
88
89// size_t b_gate = ror_props.gate_idxs[1];
90// uint32_t b_gate_idx = ror_props.idxs[1];
91// ASSERT_EQ(
92// "b",
93// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
94// b_gate][b_gate_idx]]]);
95// }
96// for (uint32_t r = 1; r < 16; r += 1) {
97// uint16_t n = 16;
98// smt_subcircuits::CircuitProps ror_props = smt_subcircuits::get_standard_ror_circuit(n, r);
99// smt_circuit_schema::CircuitSchema circuit = ror_props.circuit;
100
101// size_t a_gate = ror_props.gate_idxs[0];
102// uint32_t a_gate_idx = ror_props.idxs[0];
103// size_t start_gate = ror_props.start_gate;
104// ASSERT_EQ(
105// "a",
106// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
107// a_gate][a_gate_idx]]]);
108
109// size_t b_gate = ror_props.gate_idxs[1];
110// uint32_t b_gate_idx = ror_props.idxs[1];
111// ASSERT_EQ(
112// "b",
113// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
114// b_gate][b_gate_idx]]]);
115// }
116// for (uint32_t r = 1; r < 32; r += 1) {
117// uint32_t n = 16;
118// smt_subcircuits::CircuitProps ror_props = smt_subcircuits::get_standard_ror_circuit(n, r);
119// smt_circuit_schema::CircuitSchema circuit = ror_props.circuit;
120
121// size_t a_gate = ror_props.gate_idxs[0];
122// uint32_t a_gate_idx = ror_props.idxs[0];
123// size_t start_gate = ror_props.start_gate;
124// ASSERT_EQ(
125// "a",
126// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
127// a_gate][a_gate_idx]]]);
128
129// size_t b_gate = ror_props.gate_idxs[1];
130// uint32_t b_gate_idx = ror_props.idxs[1];
131// ASSERT_EQ(
132// "b",
133// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
134// b_gate][b_gate_idx]]]);
135// }
136// for (uint32_t r = 1; r < 64; r += 1) {
137// uint64_t n = 16;
138// smt_subcircuits::CircuitProps ror_props = smt_subcircuits::get_standard_ror_circuit(n, r);
139// smt_circuit_schema::CircuitSchema circuit = ror_props.circuit;
140
141// size_t a_gate = ror_props.gate_idxs[0];
142// uint32_t a_gate_idx = ror_props.idxs[0];
143// size_t start_gate = ror_props.start_gate;
144// ASSERT_EQ(
145// "a",
146// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
147// a_gate][a_gate_idx]]]);
148
149// size_t b_gate = ror_props.gate_idxs[1];
150// uint32_t b_gate_idx = ror_props.idxs[1];
151// ASSERT_EQ(
152// "b",
153// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
154// b_gate][b_gate_idx]]]);
155// }
156// }
157
158// // Check that all the relative offsets are calculated correctly.
159// // I.e. I can find all three operands at the indices, given by get_standard_logic_circuit
160// TEST(Subcircuits, shl_circuit)
161// {
162// for (uint32_t r = 1; r < 8; r += 1) {
163// unsigned char n = 8;
164// smt_subcircuits::CircuitProps shift_left_props = smt_subcircuits::get_standard_shift_left_circuit(n, r);
165// smt_circuit_schema::CircuitSchema circuit = shift_left_props.circuit;
166
167// size_t a_gate = shift_left_props.gate_idxs[0];
168// uint32_t a_gate_idx = shift_left_props.idxs[0];
169// size_t start_gate = shift_left_props.start_gate;
170// ASSERT_EQ(
171// "a",
172// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
173// a_gate][a_gate_idx]]]);
174
175// size_t b_gate = shift_left_props.gate_idxs[1];
176// uint32_t b_gate_idx = shift_left_props.idxs[1];
177// ASSERT_EQ(
178// "b",
179// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
180// b_gate][b_gate_idx]]]);
181// }
182// for (uint32_t r = 1; r < 16; r += 1) {
183// uint16_t n = 16;
184// smt_subcircuits::CircuitProps shift_left_props = smt_subcircuits::get_standard_shift_left_circuit(n, r);
185// smt_circuit_schema::CircuitSchema circuit = shift_left_props.circuit;
186
187// size_t a_gate = shift_left_props.gate_idxs[0];
188// uint32_t a_gate_idx = shift_left_props.idxs[0];
189// size_t start_gate = shift_left_props.start_gate;
190// ASSERT_EQ(
191// "a",
192// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
193// a_gate][a_gate_idx]]]);
194
195// size_t b_gate = shift_left_props.gate_idxs[1];
196// uint32_t b_gate_idx = shift_left_props.idxs[1];
197// ASSERT_EQ(
198// "b",
199// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
200// b_gate][b_gate_idx]]]);
201// }
202// for (uint32_t r = 1; r < 32; r += 1) {
203// uint32_t n = 16;
204// smt_subcircuits::CircuitProps shift_left_props = smt_subcircuits::get_standard_shift_left_circuit(n, r);
205// smt_circuit_schema::CircuitSchema circuit = shift_left_props.circuit;
206
207// size_t a_gate = shift_left_props.gate_idxs[0];
208// uint32_t a_gate_idx = shift_left_props.idxs[0];
209// size_t start_gate = shift_left_props.start_gate;
210// ASSERT_EQ(
211// "a",
212// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
213// a_gate][a_gate_idx]]]);
214
215// size_t b_gate = shift_left_props.gate_idxs[1];
216// uint32_t b_gate_idx = shift_left_props.idxs[1];
217// ASSERT_EQ(
218// "b",
219// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
220// b_gate][b_gate_idx]]]);
221// }
222// for (uint32_t r = 1; r < 64; r += 1) {
223// uint64_t n = 16;
224// smt_subcircuits::CircuitProps shift_left_props = smt_subcircuits::get_standard_shift_left_circuit(n, r);
225// smt_circuit_schema::CircuitSchema circuit = shift_left_props.circuit;
226
227// size_t a_gate = shift_left_props.gate_idxs[0];
228// uint32_t a_gate_idx = shift_left_props.idxs[0];
229// size_t start_gate = shift_left_props.start_gate;
230// ASSERT_EQ(
231// "a",
232// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
233// a_gate][a_gate_idx]]]);
234
235// size_t b_gate = shift_left_props.gate_idxs[1];
236// uint32_t b_gate_idx = shift_left_props.idxs[1];
237// ASSERT_EQ(
238// "b",
239// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
240// b_gate][b_gate_idx]]]);
241// }
242// }
243
244// // Check that all the relative offsets are calculated correctly.
245// // I.e. I can find all three operands at the indices, given by get_standard_logic_circuit
246// // I can't check the position of the lhs here, since shr doesn't use the witness directly but
247// // it's accumulators.
248// // However, according to standard_circuit test they seem fine.
249// TEST(Subcircuits, shr_circuit)
250// {
251// for (uint32_t r = 1; r < 8; r += 2) {
252// unsigned char n = 8;
253// smt_subcircuits::CircuitProps shift_right_props = smt_subcircuits::get_standard_shift_right_circuit(n, r);
254// smt_circuit_schema::CircuitSchema circuit = shift_right_props.circuit;
255
256// size_t start_gate = shift_right_props.start_gate;
257// size_t b_gate = shift_right_props.gate_idxs[1];
258// uint32_t b_gate_idx = shift_right_props.idxs[1];
259// ASSERT_EQ(
260// "b",
261// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
262// b_gate][b_gate_idx]]]);
263// }
264// for (uint32_t r = 1; r < 16; r += 2) {
265// uint16_t n = 16;
266// smt_subcircuits::CircuitProps shift_right_props = smt_subcircuits::get_standard_shift_right_circuit(n, r);
267// smt_circuit_schema::CircuitSchema circuit = shift_right_props.circuit;
268
269// size_t start_gate = shift_right_props.start_gate;
270// size_t b_gate = shift_right_props.gate_idxs[1];
271// uint32_t b_gate_idx = shift_right_props.idxs[1];
272// ASSERT_EQ(
273// "b",
274// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
275// b_gate][b_gate_idx]]]);
276// }
277// for (uint32_t r = 1; r < 32; r += 2) {
278// uint32_t n = 16;
279// smt_subcircuits::CircuitProps shift_right_props = smt_subcircuits::get_standard_shift_right_circuit(n, r);
280// smt_circuit_schema::CircuitSchema circuit = shift_right_props.circuit;
281
282// size_t start_gate = shift_right_props.start_gate;
283// size_t b_gate = shift_right_props.gate_idxs[1];
284// uint32_t b_gate_idx = shift_right_props.idxs[1];
285// ASSERT_EQ(
286// "b",
287// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
288// b_gate][b_gate_idx]]]);
289// }
290// for (uint32_t r = 1; r < 64; r += 2) {
291// uint64_t n = 16;
292// smt_subcircuits::CircuitProps shift_right_props = smt_subcircuits::get_standard_shift_right_circuit(n, r);
293// smt_circuit_schema::CircuitSchema circuit = shift_right_props.circuit;
294
295// size_t start_gate = shift_right_props.start_gate;
296// size_t b_gate = shift_right_props.gate_idxs[1];
297// uint32_t b_gate_idx = shift_right_props.idxs[1];
298// ASSERT_EQ(
299// "b",
300// circuit.vars_of_interest[circuit.real_variable_index[circuit.wires[0][start_gate +
301// b_gate][b_gate_idx]]]);
302// }
303// }