Barretenberg
The ZK-SNARK library at the core of Aztec
Loading...
Searching...
No Matches
ultra_circuit.test.cpp
Go to the documentation of this file.
1#include <fstream>
2#include <iostream>
3#include <string>
4
5#include "barretenberg/common/mem.hpp"
6#include "barretenberg/stdlib_circuit_builders/ultra_circuit_builder.hpp"
7
8#include "barretenberg/crypto/pedersen_commitment/pedersen.hpp"
9#include "barretenberg/stdlib/primitives/bigfield/bigfield.hpp"
10#include "barretenberg/stdlib/primitives/field/field.hpp"
11#include "barretenberg/stdlib/primitives/group/cycle_group.hpp"
12#include "barretenberg/stdlib/primitives/logic/logic.hpp"
13#include "barretenberg/stdlib/primitives/memory/ram_table.hpp"
14#include "barretenberg/stdlib/primitives/memory/rom_table.hpp"
15
16#include "barretenberg/smt_verification/circuit/ultra_circuit.hpp"
17#include "barretenberg/smt_verification/util/smt_util.hpp"
18
19#include <gtest/gtest.h>
20
21using namespace bb;
22using namespace smt_circuit;
23
24namespace {
25auto& engine = numeric::get_randomness();
26}
27
28using Builder = UltraCircuitBuilder;
29
30using witness_t = stdlib::witness_t<UltraCircuitBuilder>;
31using pub_witness_t = stdlib::public_witness_t<UltraCircuitBuilder>;
32
33using field_t = stdlib::field_t<UltraCircuitBuilder>;
34using bigfield_t = bb::stdlib::bigfield<Builder, bb::Bn254FqParams>;
35using rom_table_t = bb::stdlib::rom_table<Builder>;
36using ram_table_t = bb::stdlib::ram_table<Builder>;
37using cycle_group_t = bb::stdlib::cycle_group<Builder>;
38
39TEST(UltraCircuitSMT, AssertEqual)
40{
41 auto builder = UltraCircuitBuilder();
42
43 field_t a(witness_t(&builder, fr::random_element()));
44 field_t b(witness_t(&builder, fr::random_element()));
45 builder.set_variable_name(a.get_witness_index(), "a");
46 builder.set_variable_name(b.get_witness_index(), "b");
47 field_t c = (a + a) / (b + b + b);
48 builder.set_variable_name(c.get_witness_index(), "c");
49
50 field_t d(witness_t(&builder, a.get_value()));
51 field_t e(witness_t(&builder, b.get_value()));
52 field_t f(witness_t(&builder, c.get_value()));
53 builder.assert_equal(d.get_witness_index(), a.get_witness_index());
54 builder.assert_equal(e.get_witness_index(), b.get_witness_index());
55
56 field_t g = d + d;
57 field_t h = e + e + e;
58 field_t i = g / h;
59 builder.assert_equal(i.get_witness_index(), c.get_witness_index());
60 field_t j(witness_t(&builder, i.get_value()));
61 field_t k(witness_t(&builder, j.get_value()));
62 builder.assert_equal(i.get_witness_index(), j.get_witness_index());
63 builder.assert_equal(i.get_witness_index(), k.get_witness_index());
64
65 auto buf = builder.export_circuit();
66 CircuitSchema circuit_info = unpack_from_buffer(buf);
67 Solver s(circuit_info.modulus, ultra_solver_config);
68 UltraCircuit circuit(circuit_info, &s, TermType::FFTerm);
69
70 ASSERT_EQ(circuit[k.get_witness_index()].term, circuit["c"].term);
71 ASSERT_EQ(circuit[d.get_witness_index()].term, circuit["a"].term);
72 ASSERT_EQ(circuit[e.get_witness_index()].term, circuit["b"].term);
73
74 ASSERT_EQ(circuit[i.get_witness_index()].term, circuit[k.get_witness_index()].term);
75 ASSERT_EQ(circuit[i.get_witness_index()].term, circuit[j.get_witness_index()].term);
76}
77
78TEST(UltraCircuitSMT, ArithmeticRelation)
79{
80 UltraCircuitBuilder builder;
81
82 field_t a(witness_t(&builder, fr::random_element()));
83 field_t b(witness_t(&builder, fr::random_element()));
84 field_t c = a * a * b / (a + b * 3) - b / a;
85
86 builder.set_variable_name(a.get_witness_index(), "a");
87 builder.set_variable_name(b.get_witness_index(), "b");
88 builder.set_variable_name(c.get_witness_index(), "c");
89
90 auto circuit_info = unpack_from_buffer(builder.export_circuit());
91 Solver s(circuit_info.modulus, ultra_solver_config);
92 UltraCircuit cir(circuit_info, &s);
93 ASSERT_EQ(cir.get_num_gates(), builder.get_num_finalized_gates_inefficient(/*ensure_nonzero=*/false));
94
95 cir["a"] == a.get_value();
96 cir["b"] == b.get_value();
97
98 bool res = s.check();
99 ASSERT_TRUE(res);
100
101 bb::fr c_solver_val = string_to_fr(s[cir["c"]], /*base=*/10);
102 ASSERT_EQ(c_solver_val, c.get_value());
103}
104
105TEST(UltraCircuitSMT, EllipticRelationADD)
106{
107 UltraCircuitBuilder builder;
108
109 auto p1 =
110 cycle_group_t::from_witness(&builder, bb::stdlib::cycle_group<Builder>::Curve::AffineElement::random_element());
111 auto p2 =
112 cycle_group_t::from_witness(&builder, bb::stdlib::cycle_group<Builder>::Curve::AffineElement::random_element());
113 auto p3 = p1.unconditional_add(p2);
114
115 builder.set_variable_name(p1.x().get_witness_index(), "x1");
116 builder.set_variable_name(p2.x().get_witness_index(), "x2");
117 builder.set_variable_name(p3.x().get_witness_index(), "x3");
118 builder.set_variable_name(p1.y().get_witness_index(), "y1");
119 builder.set_variable_name(p2.y().get_witness_index(), "y2");
120 builder.set_variable_name(p3.y().get_witness_index(), "y3");
121
122 auto circuit_info = unpack_from_buffer(builder.export_circuit());
123 Solver s(circuit_info.modulus, ultra_solver_config);
124 UltraCircuit cir(circuit_info, &s);
125 ASSERT_EQ(cir.get_num_gates(), builder.get_num_finalized_gates_inefficient(/*ensure_nonzero=*/false));
126
127 cir["x1"] == p1.x().get_value();
128 cir["x2"] == p2.x().get_value();
129 cir["y1"] == p1.y().get_value();
130 cir["y2"] == p2.y().get_value();
131
132 bool res = s.check();
133 ASSERT_TRUE(res);
134
135 bb::fr x3_solver_val = string_to_fr(s[cir["x3"]], /*base=*/10);
136 bb::fr y3_solver_val = string_to_fr(s[cir["y3"]], /*base=*/10);
137
138 bb::fr x3_builder_val = p3.x().get_value();
139 bb::fr y3_builder_val = p3.y().get_value();
140
141 ASSERT_EQ(x3_solver_val, x3_builder_val);
142 ASSERT_EQ(y3_solver_val, y3_builder_val);
143
144 ((Bool(cir["x3"]) != Bool(STerm(x3_builder_val, &s, TermType::FFTerm))) |
145 (Bool(cir["y3"]) != Bool(STerm(y3_builder_val, &s, TermType::FFTerm))))
146 .assert_term();
147 res = s.check();
148 ASSERT_FALSE(res);
149}
150
151TEST(UltraCircuitSMT, EllipticRelationDBL)
152{
153 UltraCircuitBuilder builder;
154
155 auto p1 =
156 cycle_group_t::from_witness(&builder, bb::stdlib::cycle_group<Builder>::Curve::AffineElement::random_element());
157 auto p2 = p1.dbl();
158
159 builder.set_variable_name(p1.x().get_witness_index(), "x1");
160 builder.set_variable_name(p2.x().get_witness_index(), "x2");
161 builder.set_variable_name(p1.y().get_witness_index(), "y1");
162 builder.set_variable_name(p2.y().get_witness_index(), "y2");
163 builder.set_variable_name(p1.is_point_at_infinity().get_witness_index(), "is_inf");
164
165 auto circuit_info = unpack_from_buffer(builder.export_circuit());
166 Solver s(circuit_info.modulus, ultra_solver_config);
167 UltraCircuit cir(circuit_info, &s);
168 ASSERT_EQ(cir.get_num_gates(), builder.get_num_finalized_gates_inefficient(/*ensure_nonzero=*/false));
169
170 cir["x1"] == p1.x().get_value();
171 cir["y1"] == p1.y().get_value();
172 cir["is_inf"] == static_cast<size_t>(p1.is_point_at_infinity().get_value());
173
174 bool res = s.check();
175 ASSERT_TRUE(res);
176
177 bb::fr x2_solver_val = string_to_fr(s[cir["x2"]], /*base=*/10);
178 bb::fr y2_solver_val = string_to_fr(s[cir["y2"]], /*base=*/10);
179
180 bb::fr x2_builder_val = p2.x().get_value();
181 bb::fr y2_builder_val = p2.y().get_value();
182
183 ASSERT_EQ(x2_solver_val, x2_builder_val);
184 ASSERT_EQ(y2_solver_val, y2_builder_val);
185
186 ((Bool(cir["x2"]) != Bool(STerm(x2_builder_val, &s, TermType::FFTerm))) |
187 (Bool(cir["y2"]) != Bool(STerm(y2_builder_val, &s, TermType::FFTerm))))
188 .assert_term();
189 res = s.check();
190 ASSERT_FALSE(res);
191}
192
193TEST(UltraCircuitSMT, OptimizedDeltaRangeRelation)
194{
195 UltraCircuitBuilder builder;
196
197 field_t a(witness_t(&builder, engine.get_random_uint32()));
198 a.create_range_constraint(32);
199 builder.set_variable_name(a.get_witness_index(), "a");
200 builder.finalize_circuit(/*ensure_nonzero=*/false); // No need to add nonzero gates if we're not proving
201
202 auto circuit_info = unpack_from_buffer(builder.export_circuit());
203 Solver s(circuit_info.modulus, ultra_solver_config);
204 UltraCircuit cir(circuit_info, &s, TermType::BVTerm);
205 ASSERT_EQ(cir.get_num_gates(), builder.get_num_finalized_gates_inefficient(/*ensure_nonzero=*/false));
206
207 cir["a"] == a.get_value();
208 s.print_assertions();
209
210 bool res = s.check();
211 ASSERT_TRUE(res);
212}
213
214TEST(UltraCircuitSMT, LookupRelation1)
215{
216 UltraCircuitBuilder builder;
217
218 field_t a(witness_t(&builder, engine.get_random_uint8()));
219 field_t b(witness_t(&builder, engine.get_random_uint8()));
220 field_t c = bb::stdlib::logic<UltraCircuitBuilder>::create_logic_constraint(a, b, 8, true);
221 builder.set_variable_name(a.get_witness_index(), "a");
222 builder.set_variable_name(b.get_witness_index(), "b");
223 builder.set_variable_name(c.get_witness_index(), "c");
224
225 auto circuit_info = unpack_from_buffer(builder.export_circuit());
226 Solver slv(circuit_info.modulus, /*config=*/ultra_solver_config, /*base=*/16, /*bvsize=*/256);
227 UltraCircuit cir(circuit_info, &slv, TermType::BVTerm);
228
229 cir["a"] == a.get_value();
230 cir["b"] == b.get_value();
231 slv.print_assertions();
232
233 ASSERT_TRUE(slv.check());
234 bb::fr c_solver_val = string_to_fr(slv[cir["c"]], /*base=*/2);
235 bb::fr c_builder_val = c.get_value();
236 ASSERT_EQ(c_solver_val, c_builder_val);
237}
238
239TEST(UltraCircuitSMT, LookupRelation2)
240{
241 UltraCircuitBuilder builder;
242
243 field_t a(witness_t(&builder, engine.get_random_uint32()));
244 field_t b(witness_t(&builder, engine.get_random_uint32()));
245 field_t c = bb::stdlib::logic<Builder>::create_logic_constraint(a, b, /*num_bits=*/32, /*is_xor_gate=*/true);
246 builder.set_variable_name(a.get_witness_index(), "a");
247 builder.set_variable_name(b.get_witness_index(), "b");
248 builder.set_variable_name(c.get_witness_index(), "c");
249 builder.finalize_circuit(/*ensure_nonzero=*/false); // No need to add nonzero gates if we're not proving
250
251 auto circuit_info = unpack_from_buffer(builder.export_circuit());
252 Solver s(circuit_info.modulus, ultra_solver_config, /*base=*/16, /*bvsize=*/256);
253 UltraCircuit cir(circuit_info, &s, TermType::BVTerm);
254 ASSERT_EQ(cir.get_num_gates(), builder.get_num_finalized_gates_inefficient(/*ensure_nonzero=*/false));
255
256 cir["a"] == a.get_value();
257 cir["b"] == b.get_value();
258 s.print_assertions();
259
260 bool res = s.check();
261 ASSERT_TRUE(res);
262
263 bb::fr c_solver_val = string_to_fr(s[cir["c"]], /*base=*/2, /*is_signed=*/false);
264 bb::fr c_builder_val = c.get_value();
265 ASSERT_EQ(c_solver_val, c_builder_val);
266}
267
269// TODO(alex): Wait until the bug with large sets is resolved by cvc5
270// TEST(UltraCircuitSMT, NNFRelation)
271//{
272// UltraCircuitBuilder builder;
273//
274// bigfield_t a = bigfield_t::from_witness(&builder, bb::fq::random_element());
275// bigfield_t b = bigfield_t::from_witness(&builder, bb::fq::random_element());
276// [[maybe_unused]] auto c = a * b;
277//
278// auto circuit_info = unpack_from_buffer(builder.export_circuit());
279// Solver slv(circuit_info.modulus, /*config=*/debug_solver_config, /*base=*/16);
280// UltraCircuit cir(circuit_info, &slv, TermType::FFTerm);
281//
282// for(uint32_t i = 0; i < builder.get_variables().size(); i++){
283// if (!cir.optimized[i]){
284// cir[i] == builder.get_variables()[i];
285// }
286// }
287//
288// slv.print_assertions();
289// bool res = smt_timer(&slv);
290// ASSERT_TRUE(res);
291//}
292
293TEST(UltraCircuitSMT, ROMTables)
294{
295 Builder builder;
296
297 field_t entry_1 = pub_witness_t(&builder, bb::fr::random_element());
298 field_t entry_2 = pub_witness_t(&builder, bb::fr::random_element());
299 field_t entry_3 = pub_witness_t(&builder, bb::fr::random_element());
300 std::vector<field_t> table_values = { entry_1, entry_2, entry_3 };
301 rom_table_t table(table_values);
302
303 field_t i = witness_t(&builder, 2);
304 builder.set_variable_name(i.get_witness_index(), "i");
305 field_t entry_i = table[i];
306 builder.set_variable_name(entry_i.get_witness_index(), "entry_i");
307
308 field_t j = witness_t(&builder, 1);
309 builder.set_variable_name(j.get_witness_index(), "j");
310 field_t entry_j = table[j];
311 builder.set_variable_name(entry_j.get_witness_index(), "entry_j");
312
313 auto circuit_info = unpack_from_buffer(builder.export_circuit());
314 Solver slv(circuit_info.modulus, /*config=*/ultra_solver_config, /*base=*/16);
315 UltraCircuit cir(circuit_info, &slv, TermType::FFTerm);
316
317 STerm i_s = cir["i"];
318 STerm j_s = cir["j"];
319 i_s != j_s;
320
321 slv.print_assertions();
322
323 ASSERT_TRUE(slv.check());
324
325 bb::fr entry_i_cir = string_to_fr(slv[cir["entry_i"]], /*base=*/10);
326 bb::fr entry_j_cir = string_to_fr(slv[cir["entry_j"]], /*base=*/10);
327 bb::fr i_cir = string_to_fr(slv[cir["i"]], /*base=*/10);
328 bb::fr j_cir = string_to_fr(slv[cir["j"]], /*base=*/10);
329
330 ASSERT_EQ(table_values[static_cast<size_t>(i_cir)].get_value(), entry_i_cir);
331 ASSERT_EQ(table_values[static_cast<size_t>(j_cir)].get_value(), entry_j_cir);
332}
333
334TEST(UltraCircuitSMT, ROMTablesRelaxed)
335{
336 Builder builder;
337
338 field_t entry_1 = pub_witness_t(&builder, bb::fr::random_element());
339 field_t entry_2 = pub_witness_t(&builder, bb::fr::random_element());
340 field_t entry_3 = pub_witness_t(&builder, bb::fr::random_element());
341 std::vector<field_t> table_values = { entry_1, entry_2, entry_3 };
342 rom_table_t table(table_values);
343
344 field_t i = witness_t(&builder, 2);
345 builder.set_variable_name(i.get_witness_index(), "i");
346 field_t entry_i = table[i];
347 builder.set_variable_name(entry_i.get_witness_index(), "entry_i");
348
349 field_t j = witness_t(&builder, 1);
350 builder.set_variable_name(j.get_witness_index(), "j");
351 field_t entry_j = table[j];
352 builder.set_variable_name(entry_j.get_witness_index(), "entry_j");
353
354 auto circuit_info = unpack_from_buffer(builder.export_circuit());
355 Solver slv(circuit_info.modulus, /*config=*/ultra_solver_config, /*base=*/16);
356 UltraCircuit cir(
357 circuit_info, &slv, TermType::FFTerm, /*tag=*/"", /*enable_optimizations=*/true, /*rom_ram_relaxed=*/true);
358
359 STerm i_s = cir["i"];
360 STerm j_s = cir["j"];
361 i_s != j_s;
362
363 slv.print_assertions();
364
365 ASSERT_TRUE(slv.check());
366
367 bb::fr entry_i_cir = string_to_fr(slv[cir["entry_i"]], /*base=*/10);
368 bb::fr entry_j_cir = string_to_fr(slv[cir["entry_j"]], /*base=*/10);
369 bb::fr i_cir = string_to_fr(slv[cir["i"]], /*base=*/10);
370 bb::fr j_cir = string_to_fr(slv[cir["j"]], /*base=*/10);
371
372 ASSERT_EQ(table_values[static_cast<size_t>(i_cir)].get_value(), entry_i_cir);
373 ASSERT_EQ(table_values[static_cast<size_t>(j_cir)].get_value(), entry_j_cir);
374}
375
376TEST(UltraCircuitSMT, RAMTables)
377{
378 Builder builder;
379
380 size_t table_size = 3;
381 std::vector<field_t> zeros(table_size, field_t(0));
382 ram_table_t table(&builder, zeros);
383 for (size_t i = 0; i < table_size; ++i) {
384 table.write(i, 0);
385 }
386
387 field_t i = witness_t(&builder, 2);
388 builder.set_variable_name(i.get_witness_index(), "i");
389
390 bb::fr el0 = bb::fr::random_element();
391 table.write(i, el0);
392 field_t entry_i = table.read(i);
393 builder.set_variable_name(entry_i.get_witness_index(), "entry_i");
394
395 bb::fr el1 = bb::fr::random_element();
396 table.write(i, el1);
397 field_t entry_i_1 = table.read(i);
398 builder.set_variable_name(entry_i_1.get_witness_index(), "entry_i_1");
399
400 auto circuit_info = unpack_from_buffer(builder.export_circuit());
401 Solver slv(circuit_info.modulus, /*config=*/ultra_solver_config, /*base=*/16);
402 UltraCircuit cir(circuit_info, &slv, TermType::FFTerm);
403
404 STerm i_s = cir["i"];
405 STerm entry_i_s = cir["entry_i"];
406 STerm entry_i_1_s = cir["entry_i_1"];
407 entry_i_s != 0;
408
409 slv.print_assertions();
410 ASSERT_TRUE(slv.check());
411
412 bb::fr entry_i_cir = string_to_fr(slv[entry_i_s], /*base=*/10);
413 bb::fr entry_i_1_cir = string_to_fr(slv[entry_i_1_s], /*base=*/10);
414
415 ASSERT_TRUE(entry_i_cir == el0);
416 ASSERT_TRUE(entry_i_1_cir == el1);
417}
418
419TEST(UltraCircuitSMT, RAMTablesRelaxed)
420{
421 Builder builder;
422
423 size_t table_size = 3;
424 std::vector<field_t> zeros(table_size, field_t(0));
425 ram_table_t table(&builder, zeros);
426 for (size_t i = 0; i < table_size; ++i) {
427 table.write(i, 0);
428 }
429
430 field_t i = witness_t(&builder, 2);
431 builder.set_variable_name(i.get_witness_index(), "i");
432
433 bb::fr el0 = bb::fr::random_element();
434 table.write(i, el0);
435 field_t entry_i = table.read(i);
436 builder.set_variable_name(entry_i.get_witness_index(), "entry_i");
437
438 bb::fr el1 = bb::fr::random_element();
439 table.write(i, el1);
440 field_t entry_i_1 = table.read(i);
441 builder.set_variable_name(entry_i_1.get_witness_index(), "entry_i_1");
442
443 auto circuit_info = unpack_from_buffer(builder.export_circuit());
444 Solver slv(circuit_info.modulus, /*config=*/ultra_solver_config, /*base=*/16);
445 UltraCircuit cir(
446 circuit_info, &slv, TermType::FFTerm, /*tag=*/"", /*enable_optimizations=*/true, /*rom_ram_relaxed=*/true);
447
448 STerm i_s = cir["i"];
449 STerm entry_i_s = cir["entry_i"];
450 STerm entry_i_1_s = cir["entry_i_1"];
451 entry_i_s != 0;
452
453 slv.print_assertions();
454 ASSERT_TRUE(slv.check());
455
456 bb::fr entry_i_cir = string_to_fr(slv[entry_i_s], /*base=*/10);
457 bb::fr entry_i_1_cir = string_to_fr(slv[entry_i_1_s], /*base=*/10);
458
459 ASSERT_TRUE(entry_i_cir == el0);
460 ASSERT_TRUE(entry_i_1_cir == el1);
461}
462
463TEST(UltraCircuitSMT, XorOptimization)
464{
465 UltraCircuitBuilder builder;
466 field_t a(witness_t(&builder, engine.get_random_uint32()));
467 builder.set_variable_name(a.get_witness_index(), "a");
468 field_t b(witness_t(&builder, engine.get_random_uint32()));
469 builder.set_variable_name(b.get_witness_index(), "b");
470 field_t c = bb::stdlib::logic<Builder>::create_logic_constraint(a, b, /*num_bits=*/32, /*is_xor_gate=*/true);
471 builder.set_variable_name(c.get_witness_index(), "c");
472
473 CircuitSchema circuit_info = unpack_from_buffer(builder.export_circuit());
474 uint32_t modulus_base = 16;
475 uint32_t bvsize = 256;
476 Solver s(circuit_info.modulus, ultra_solver_config, modulus_base, bvsize);
477
478 UltraCircuit circuit(circuit_info, &s, TermType::BVTerm);
479
480 circuit["a"] == a.get_value();
481 circuit["b"] == b.get_value();
482
483 s.print_assertions();
484
485 bool res = smt_timer(&s);
486 ASSERT_TRUE(res);
487
488 bb::fr c_sym = string_to_fr(s[circuit["c"]], /*base=*/2);
489 bb::fr c_builder = c.get_value();
490 ASSERT_EQ(c_sym, c_builder);
491}
492
493TEST(UltraCircuitSMT, AndOptimization)
494{
495 UltraCircuitBuilder builder;
496 field_t a(witness_t(&builder, engine.get_random_uint32()));
497 builder.set_variable_name(a.get_witness_index(), "a");
498 field_t b(witness_t(&builder, engine.get_random_uint32()));
499 builder.set_variable_name(b.get_witness_index(), "b");
500 field_t c = bb::stdlib::logic<Builder>::create_logic_constraint(a, b, /*num_bits=*/32, /*is_xor_gate=*/false);
501 builder.set_variable_name(c.get_witness_index(), "c");
502
503 CircuitSchema circuit_info = unpack_from_buffer(builder.export_circuit());
504 uint32_t modulus_base = 16;
505 uint32_t bvsize = 256;
506 Solver s(circuit_info.modulus, ultra_solver_config, modulus_base, bvsize);
507
508 UltraCircuit circuit(circuit_info, &s, TermType::BVTerm);
509
510 circuit["a"] == a.get_value();
511 circuit["b"] == b.get_value();
512
513 s.print_assertions();
514
515 bool res = smt_timer(&s);
516 ASSERT_TRUE(res);
517
518 bb::fr c_sym = string_to_fr(s[circuit["c"]], /*base=*/2);
519 bb::fr c_builder = c.get_value();
520 ASSERT_EQ(c_sym, c_builder);
521}
bb::Relation
A wrapper for Relations to expose methods used by the Sumcheck prover or verifier to add the contribu...
Definition relation_types.hpp:96
bb::UltraCircuitBuilder_
Definition ultra_circuit_builder.hpp:41
bb::numeric::RNG::get_random_uint8
virtual uint8_t get_random_uint8()=0
bb::numeric::RNG::get_random_uint32
virtual uint32_t get_random_uint32()=0
bb::stdlib::cycle_group
cycle_group represents a group Element of the proving system's embedded curve, i.e....
Definition cycle_group.hpp:37
bb::stdlib::cycle_group::from_witness
static cycle_group from_witness(Builder *_context, const AffineElement &_in)
Converts an AffineElement into a circuit witness.
Definition cycle_group.cpp:170
bb::stdlib::field_t< Builder >
bb::stdlib::field_t::assert_equal
void assert_equal(const field_t &rhs, std::string const &msg="field_t::assert_equal") const
Copy constraint: constrain that *this field is equal to rhs element.
Definition field.cpp:930
bb::stdlib::field_t::get_value
bb::fr get_value() const
Given a := *this, compute its value given by a.v * a.mul + a.add.
Definition field.cpp:828
bb::stdlib::field_t::get_witness_index
uint32_t get_witness_index() const
Get the witness index of the current field element.
Definition field.hpp:506
bb::stdlib::logic::create_logic_constraint
static field_pt create_logic_constraint(field_pt &a, field_pt &b, size_t num_bits, bool is_xor_gate, const std::function< std::pair< uint256_t, uint256_t >(uint256_t, uint256_t, size_t)> &get_chunk=[](uint256_t left, uint256_t right, size_t chunk_size) { uint256_t left_chunk=left &((uint256_t(1)<< chunk_size) - 1);uint256_t right_chunk=right &((uint256_t(1)<< chunk_size) - 1);return std::make_pair(left_chunk, right_chunk);})
A logical AND or XOR over a variable number of bits.
Definition logic.cpp:32
bb::stdlib::public_witness_t
Definition witness.hpp:59
bb::stdlib::ram_table
Definition ram_table.hpp:16
bb::stdlib::ram_table::read
field_pt read(const field_pt &index) const
Read a field element from the RAM table at an index value.
Definition ram_table.cpp:131
bb::stdlib::ram_table::write
void write(const field_pt &index, const field_pt &value)
Write a field element from the RAM table at an index value.
Definition ram_table.cpp:180
bb::stdlib::rom_table
Definition rom_table.hpp:16
bb::stdlib::witness_t
Definition witness.hpp:16
smt_circuit::UltraCircuit
Symbolic Circuit class for Standard Circuit Builder.
Definition ultra_circuit.hpp:53
smt_circuit::UltraCircuit::get_num_gates
size_t get_num_gates() const
Get the num gates object.
Definition ultra_circuit.hpp:101
smt_solver::Solver
Class for the solver.
Definition solver.hpp:80
smt_solver::Solver::print_assertions
void print_assertions()
Definition solver.cpp:421
smt_solver::Solver::check
bool check()
Definition solver.cpp:11
smt_terms::Bool
Bool element class.
Definition bool.hpp:14
smt_terms::STerm
Symbolic term element class.
Definition term.hpp:114
builder
AluTraceBuilder builder
Definition alu.test.cpp:124
a
FF a
Definition field_gt.test.cpp:52
b
FF b
Definition field_gt.test.cpp:53
cycle_group.hpp
buf
uint8_t const * buf
Definition data_store.hpp:9
engine
numeric::RNG & engine
Definition eccvm_transcript.test.cpp:295
bb::numeric::get_randomness
RNG & get_randomness()
Definition engine.cpp:203
bb
Entry point for Barretenberg command-line interface.
Definition api.hpp:5
bb::UltraCircuitBuilder
UltraCircuitBuilder_< UltraExecutionTraceBlocks > UltraCircuitBuilder
Definition circuit_builders_fwd.hpp:24
bb::TEST
TEST(BoomerangMegaCircuitBuilder, BasicCircuit)
Definition graph_description_megacircuitbuilder.test.cpp:22
smt_circuit_schema::unpack_from_buffer
CircuitSchema unpack_from_buffer(const msgpack::sbuffer &buf)
Get the CircuitSchema object.
Definition circuit_schema.cpp:41
smt_circuit
Definition circuit_base.cpp:3
smt_solver::ultra_solver_config
const SolverConfiguration ultra_solver_config
Definition solver.hpp:47
std::get
constexpr decltype(auto) get(::tuplet::tuple< T... > &&t) noexcept
Definition tuple.hpp:13
pedersen.hpp
ram_table.hpp
rom_table.hpp
smt_timer
bool smt_timer(smt_solver::Solver *s)
Get the solver result and amount of time that it took to solve.
Definition smt_util.cpp:297
string_to_fr
bb::fr string_to_fr(const std::string &number, int base, bool is_signed, size_t step)
Converts a string of an arbitrary base to fr. Note: there should be no prefix.
Definition smt_util.cpp:13
smt_util.hpp
bb::field< Bn254FrParams >::random_element
static field random_element(numeric::RNG *engine=nullptr) noexcept
Definition field_impl.hpp:675
smt_circuit_schema::CircuitSchema
Serialized state of a circuit.
Definition circuit_schema.hpp:24
smt_circuit_schema::CircuitSchema::modulus
std::string modulus
Definition circuit_schema.hpp:25
ultra_circuit.hpp
witness_t
stdlib::witness_t< UltraCircuitBuilder > witness_t
Definition ultra_circuit.test.cpp:30
field_t
stdlib::field_t< UltraCircuitBuilder > field_t
Definition ultra_circuit.test.cpp:33
pub_witness_t
stdlib::public_witness_t< UltraCircuitBuilder > pub_witness_t
Definition ultra_circuit.test.cpp:31
ultra_circuit_builder.hpp