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.witness_index, "a");
46 builder.set_variable_name(b.witness_index, "b");
47 field_t c = (a + a) / (b + b + b);
48 builder.set_variable_name(c.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_estimated_num_finalized_gates());
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_estimated_num_finalized_gates());
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().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_estimated_num_finalized_gates());
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_estimated_num_finalized_gates());
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_estimated_num_finalized_gates());
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 ram_table_t table(&builder, table_size);
382 for (size_t i = 0; i < table_size; ++i) {
383 table.write(i, 0);
384 }
385
386 field_t i = witness_t(&builder, 2);
387 builder.set_variable_name(i.get_witness_index(), "i");
388
389 bb::fr el0 = bb::fr::random_element();
390 table.write(i, el0);
391 field_t entry_i = table.read(i);
392 builder.set_variable_name(entry_i.get_witness_index(), "entry_i");
393
394 bb::fr el1 = bb::fr::random_element();
395 table.write(i, el1);
396 field_t entry_i_1 = table.read(i);
397 builder.set_variable_name(entry_i_1.get_witness_index(), "entry_i_1");
398
399 auto circuit_info = unpack_from_buffer(builder.export_circuit());
400 Solver slv(circuit_info.modulus, /*config=*/ultra_solver_config, /*base=*/16);
401 UltraCircuit cir(circuit_info, &slv, TermType::FFTerm);
402
403 STerm i_s = cir["i"];
404 STerm entry_i_s = cir["entry_i"];
405 STerm entry_i_1_s = cir["entry_i_1"];
406 entry_i_s != 0;
407
408 slv.print_assertions();
409 ASSERT_TRUE(slv.check());
410
411 bb::fr entry_i_cir = string_to_fr(slv[entry_i_s], /*base=*/10);
412 bb::fr entry_i_1_cir = string_to_fr(slv[entry_i_1_s], /*base=*/10);
413
414 ASSERT_TRUE(entry_i_cir == el0);
415 ASSERT_TRUE(entry_i_1_cir == el1);
416}
417
418TEST(UltraCircuitSMT, RAMTablesRelaxed)
419{
420 Builder builder;
421
422 size_t table_size = 3;
423 ram_table_t table(&builder, table_size);
424 for (size_t i = 0; i < table_size; ++i) {
425 table.write(i, 0);
426 }
427
428 field_t i = witness_t(&builder, 2);
429 builder.set_variable_name(i.get_witness_index(), "i");
430
431 bb::fr el0 = bb::fr::random_element();
432 table.write(i, el0);
433 field_t entry_i = table.read(i);
434 builder.set_variable_name(entry_i.get_witness_index(), "entry_i");
435
436 bb::fr el1 = bb::fr::random_element();
437 table.write(i, el1);
438 field_t entry_i_1 = table.read(i);
439 builder.set_variable_name(entry_i_1.get_witness_index(), "entry_i_1");
440
441 auto circuit_info = unpack_from_buffer(builder.export_circuit());
442 Solver slv(circuit_info.modulus, /*config=*/ultra_solver_config, /*base=*/16);
443 UltraCircuit cir(
444 circuit_info, &slv, TermType::FFTerm, /*tag=*/"", /*enable_optimizations=*/true, /*rom_ram_relaxed=*/true);
445
446 STerm i_s = cir["i"];
447 STerm entry_i_s = cir["entry_i"];
448 STerm entry_i_1_s = cir["entry_i_1"];
449 entry_i_s != 0;
450
451 slv.print_assertions();
452 ASSERT_TRUE(slv.check());
453
454 bb::fr entry_i_cir = string_to_fr(slv[entry_i_s], /*base=*/10);
455 bb::fr entry_i_1_cir = string_to_fr(slv[entry_i_1_s], /*base=*/10);
456
457 ASSERT_TRUE(entry_i_cir == el0);
458 ASSERT_TRUE(entry_i_1_cir == el1);
459}
460
461TEST(UltraCircuitSMT, XorOptimization)
462{
463 UltraCircuitBuilder builder;
464 field_t a(witness_t(&builder, engine.get_random_uint32()));
465 builder.set_variable_name(a.get_witness_index(), "a");
466 field_t b(witness_t(&builder, engine.get_random_uint32()));
467 builder.set_variable_name(b.get_witness_index(), "b");
468 field_t c = bb::stdlib::logic<Builder>::create_logic_constraint(a, b, /*num_bits=*/32, /*is_xor_gate=*/true);
469 builder.set_variable_name(c.get_witness_index(), "c");
470
471 CircuitSchema circuit_info = unpack_from_buffer(builder.export_circuit());
472 uint32_t modulus_base = 16;
473 uint32_t bvsize = 256;
474 Solver s(circuit_info.modulus, ultra_solver_config, modulus_base, bvsize);
475
476 UltraCircuit circuit(circuit_info, &s, TermType::BVTerm);
477
478 circuit["a"] == a.get_value();
479 circuit["b"] == b.get_value();
480
481 s.print_assertions();
482
483 bool res = smt_timer(&s);
484 ASSERT_TRUE(res);
485
486 bb::fr c_sym = string_to_fr(s[circuit["c"]], /*base=*/2);
487 bb::fr c_builder = c.get_value();
488 ASSERT_EQ(c_sym, c_builder);
489}
490
491TEST(UltraCircuitSMT, AndOptimization)
492{
493 UltraCircuitBuilder builder;
494 field_t a(witness_t(&builder, engine.get_random_uint32()));
495 builder.set_variable_name(a.get_witness_index(), "a");
496 field_t b(witness_t(&builder, engine.get_random_uint32()));
497 builder.set_variable_name(b.get_witness_index(), "b");
498 field_t c = bb::stdlib::logic<Builder>::create_logic_constraint(a, b, /*num_bits=*/32, /*is_xor_gate=*/false);
499 builder.set_variable_name(c.get_witness_index(), "c");
500
501 CircuitSchema circuit_info = unpack_from_buffer(builder.export_circuit());
502 uint32_t modulus_base = 16;
503 uint32_t bvsize = 256;
504 Solver s(circuit_info.modulus, ultra_solver_config, modulus_base, bvsize);
505
506 UltraCircuit circuit(circuit_info, &s, TermType::BVTerm);
507
508 circuit["a"] == a.get_value();
509 circuit["b"] == b.get_value();
510
511 s.print_assertions();
512
513 bool res = smt_timer(&s);
514 ASSERT_TRUE(res);
515
516 bb::fr c_sym = string_to_fr(s[circuit["c"]], /*base=*/2);
517 bb::fr c_builder = c.get_value();
518 ASSERT_EQ(c_sym, c_builder);
519}
bb::UltraCircuitBuilder_
Definition ultra_circuit_builder.hpp:42
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:36
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:146
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:929
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:827
bb::stdlib::field_t::witness_index
uint32_t witness_index
Definition field.hpp:132
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:461
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:200
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:244
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:123
a
FF a
Definition field_gt.test.cpp:51
b
FF b
Definition field_gt.test.cpp:52
pedersen.hpp
cycle_group.hpp
buf
uint8_t const * buf
Definition data_store.hpp:9
engine
numeric::RNG & engine
Definition eccvm_transcript.test.cpp:282
bb::numeric::get_randomness
RNG & get_randomness()
Definition engine.cpp:203
bb
Entry point for Barretenberg command-line interface.
Definition acir_format_getters.cpp:6
bb::TEST
TEST(MegaCircuitBuilder, CopyConstructor)
Definition mega_circuit_builder.test.cpp:14
bb::UltraCircuitBuilder
UltraCircuitBuilder_< UltraExecutionTraceBlocks > UltraCircuitBuilder
Definition circuit_builders_fwd.hpp:24
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
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:665
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
pub_witness_t
stdlib::public_witness_t< UltraCircuitBuilder > pub_witness_t
Definition ultra_circuit.test.cpp:31
ultra_circuit_builder.hpp