Barretenberg
The ZK-SNARK library at the core of Aztec
Loading...
Searching...
No Matches
acir_loader.test.cpp
Go to the documentation of this file.
1
9#include "acir_loader.hpp"
10#include "barretenberg/circuit_checker/circuit_checker.hpp"
11#include "barretenberg/common/test.hpp"
12#include "barretenberg/dsl/acir_format/acir_format.hpp"
13#include "barretenberg/smt_verification/circuit/ultra_circuit.hpp"
14#include "barretenberg/smt_verification/solver/solver.hpp"
15#include "barretenberg/smt_verification/util/smt_util.hpp"
16#include "barretenberg/stdlib/client_ivc_verifier/client_ivc_recursive_verifier.hpp"
17#include "barretenberg/stdlib_circuit_builders/ultra_circuit_builder.hpp"
18#include "formal_proofs.hpp"
19#include "helpers.hpp"
20#include <vector>
21
22// Path to test artifacts containing ACIR programs and witness files
23const std::string ARTIFACTS_PATH = "/tmp/";
24
32void save_buggy_witness(std::string instruction_name, smt_circuit::UltraCircuit circuit)
33{
34 std::vector<std::string> special_names;
35 info("Saving bug for op ", instruction_name);
36 default_model_single(special_names, circuit, ARTIFACTS_PATH + instruction_name + ".witness");
37}
38
46bool verify_buggy_witness(std::string instruction_name)
47{
48 std::vector<bb::fr> witness = import_witness_single(ARTIFACTS_PATH + instruction_name + ".witness.pack");
49 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + instruction_name + ".acir");
50 bb::UltraCircuitBuilder builder = loader.get_circuit_builder();
51 for (uint i = 0; i < witness.size(); i++) {
52 builder.variables[i] = witness[i];
53 if (i < 100) {
54 info(witness[i]);
55 }
56 }
57 return bb::CircuitChecker::check(builder);
58}
59
65TEST(acir_formal_proofs, uint_terms_add)
66{
67 std::string TESTNAME = "Binary::Add_Unsigned_127_Unsigned_127";
68 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
69 smt_solver::Solver solver = loader.get_smt_solver();
70 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
71 bool res = verify_add(&solver, circuit);
72 EXPECT_FALSE(res);
73
74 if (res) {
75 save_buggy_witness(TESTNAME, circuit);
76 }
77}
78
83TEST(acir_formal_proofs, uint_terms_and)
84{
85 std::string TESTNAME = "Binary::And_Unsigned_127_Unsigned_127";
86 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
87 smt_solver::Solver solver = loader.get_smt_solver();
88 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
89 bool res = verify_and(&solver, circuit);
90 EXPECT_FALSE(res);
91 if (res) {
92 save_buggy_witness(TESTNAME, circuit);
93 }
94}
95
101TEST(acir_formal_proofs, uint_terms_and32)
102{
103 std::string TESTNAME = "Binary::And_Unsigned_32_Unsigned_32";
104 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
105 smt_solver::Solver solver = loader.get_smt_solver();
106 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
107 bool res = verify_and(&solver, circuit);
108 EXPECT_FALSE(res);
109 if (res) {
110 save_buggy_witness(TESTNAME, circuit);
111 }
112}
113
118TEST(acir_formal_proofs, uint_terms_div)
119{
120 std::string TESTNAME = "Binary::Div_Unsigned_126_Unsigned_126";
121 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
122 smt_solver::Solver solver = loader.get_smt_solver();
123 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
124 bool res = verify_div(&solver, circuit);
125 EXPECT_FALSE(res);
126 if (res) {
127 save_buggy_witness(TESTNAME, circuit);
128 }
129}
130
138TEST(acir_formal_proofs, uint_terms_eq)
139{
140 std::string TESTNAME = "Binary::Eq_Unsigned_127_Unsigned_127";
141 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
142 smt_solver::Solver solver1 = loader.get_smt_solver();
143 smt_circuit::UltraCircuit circuit1 = loader.get_bitvec_smt_circuit(&solver1);
144
145 bool res1 = verify_eq_on_equlaity(&solver1, circuit1);
146 EXPECT_FALSE(res1);
147 if (res1) {
148 save_buggy_witness(TESTNAME, circuit1);
149 }
150
151 smt_solver::Solver solver2 = loader.get_smt_solver();
152 smt_circuit::UltraCircuit circuit2 = loader.get_bitvec_smt_circuit(&solver2);
153
154 bool res2 = verify_eq_on_inequlaity(&solver2, circuit2);
155 EXPECT_FALSE(res2);
156 if (res2) {
157 save_buggy_witness(TESTNAME, circuit2);
158 }
159}
160
168TEST(acir_formal_proofs, uint_terms_lt)
169{
170 std::string TESTNAME = "Binary::Lt_Unsigned_127_Unsigned_127";
171 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
172 smt_solver::Solver solver1 = loader.get_smt_solver();
173 smt_circuit::UltraCircuit circuit1 = loader.get_bitvec_smt_circuit(&solver1);
174
175 bool res1 = verify_lt(&solver1, circuit1);
176 EXPECT_FALSE(res1);
177 if (res1) {
178 save_buggy_witness(TESTNAME, circuit1);
179 }
180
181 smt_solver::Solver solver2 = loader.get_smt_solver();
182 smt_circuit::UltraCircuit circuit2 = loader.get_bitvec_smt_circuit(&solver2);
183
184 bool res2 = verify_gt(&solver2, circuit2);
185 EXPECT_FALSE(res2);
186 if (res2) {
187 save_buggy_witness(TESTNAME, circuit2);
188 }
189}
190
196TEST(acir_formal_proofs, uint_terms_mod)
197{
198 std::string TESTNAME = "Binary::Mod_Unsigned_126_Unsigned_126";
199 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
200 smt_solver::Solver solver = loader.get_smt_solver();
201 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
202 bool res = verify_mod(&solver, circuit);
203 solver.print_assertions();
204 EXPECT_FALSE(res);
205 if (res) {
206 save_buggy_witness(TESTNAME, circuit);
207 }
208}
209
215TEST(acir_formal_proofs, uint_terms_mul)
216{
217 std::string TESTNAME = "Binary::Mul_Unsigned_127_Unsigned_127";
218 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
219 smt_solver::Solver solver = loader.get_smt_solver();
220 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
221 bool res = verify_mul(&solver, circuit);
222 EXPECT_FALSE(res);
223 if (res) {
224 save_buggy_witness(TESTNAME, circuit);
225 }
226}
227
232TEST(acir_formal_proofs, uint_terms_or)
233{
234 std::string TESTNAME = "Binary::Or_Unsigned_127_Unsigned_127";
235 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
236 smt_solver::Solver solver = loader.get_smt_solver();
237 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
238 bool res = verify_or(&solver, circuit);
239 EXPECT_FALSE(res);
240 if (res) {
241 save_buggy_witness(TESTNAME, circuit);
242 }
243}
244
250TEST(acir_formal_proofs, uint_terms_or32)
251{
252 std::string TESTNAME = "Binary::Or_Unsigned_32_Unsigned_32";
253 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
254 smt_solver::Solver solver = loader.get_smt_solver();
255 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
256 bool res = verify_or(&solver, circuit);
257 EXPECT_FALSE(res);
258 if (res) {
259 save_buggy_witness(TESTNAME, circuit);
260 }
261}
262
269TEST(acir_formal_proofs, uint_terms_shl64)
270{
271 std::string TESTNAME = "Binary::Shl_Unsigned_64_Unsigned_8";
272 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
273 smt_solver::Solver solver = loader.get_smt_solver();
274 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
275 bool res = verify_shl64(&solver, circuit);
276 if (res) {
277 save_buggy_witness(TESTNAME, circuit);
278 }
279 EXPECT_FALSE(res);
280}
281
288TEST(acir_formal_proofs, uint_terms_shl32)
289{
290 std::string TESTNAME = "Binary::Shl_Unsigned_32_Unsigned_8";
291 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
292 smt_solver::Solver solver = loader.get_smt_solver();
293 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
294 bool res = verify_shl32(&solver, circuit);
295 if (res) {
296 save_buggy_witness(TESTNAME, circuit);
297 }
298 EXPECT_FALSE(res);
299}
300
307TEST(acir_formal_proofs, uint_terms_shr)
308{
309 std::string TESTNAME = "Binary::Shr_Unsigned_64_Unsigned_8";
310 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
311 smt_solver::Solver solver = loader.get_smt_solver();
312 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
313 bool res = verify_shr(&solver, circuit);
314 if (res) {
315 save_buggy_witness(TESTNAME, circuit);
316 }
317 EXPECT_FALSE(res);
318}
319
325TEST(acir_formal_proofs, uint_terms_sub)
326{
327 std::string TESTNAME = "Binary::Sub_Unsigned_127_Unsigned_127";
328 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
329 smt_solver::Solver solver = loader.get_smt_solver();
330 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
331 bool res = verify_sub(&solver, circuit);
332 EXPECT_FALSE(res);
333 if (res) {
334 save_buggy_witness(TESTNAME, circuit);
335 }
336}
337
342TEST(acir_formal_proofs, uint_terms_xor)
343{
344 std::string TESTNAME = "Binary::Xor_Unsigned_127_Unsigned_127";
345 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
346 smt_solver::Solver solver = loader.get_smt_solver();
347 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
348 bool res = verify_xor(&solver, circuit);
349 EXPECT_FALSE(res);
350 if (res) {
351 save_buggy_witness(TESTNAME, circuit);
352 }
353}
354
359TEST(acir_formal_proofs, uint_terms_xor32)
360{
361 std::string TESTNAME = "Binary::Xor_Unsigned_32_Unsigned_32";
362 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
363 smt_solver::Solver solver = loader.get_smt_solver();
364 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
365 bool res = verify_xor(&solver, circuit);
366 EXPECT_FALSE(res);
367 if (res) {
368 save_buggy_witness(TESTNAME, circuit);
369 }
370}
371
377TEST(acir_formal_proofs, uint_terms_not)
378{
379 std::string TESTNAME = "Not_Unsigned_127";
380 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
381 smt_solver::Solver solver = loader.get_smt_solver();
382 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
383 bool res = verify_not_127(&solver, circuit);
384 EXPECT_FALSE(res);
385 if (res) {
386 save_buggy_witness(TESTNAME, circuit);
387 }
388}
389
395TEST(acir_formal_proofs, field_terms_add)
396{
397 std::string TESTNAME = "Binary::Add_Field_0_Field_0";
398 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
399 smt_solver::Solver solver = loader.get_smt_solver();
400 smt_circuit::UltraCircuit circuit = loader.get_field_smt_circuit(&solver);
401 bool res = verify_add(&solver, circuit);
402 EXPECT_FALSE(res);
403 if (res) {
404 save_buggy_witness(TESTNAME, circuit);
405 }
406}
407
413TEST(acir_formal_proofs, field_terms_div)
414{
415 std::string TESTNAME = "Binary::Div_Field_0_Field_0";
416 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
417 smt_solver::Solver solver = loader.get_smt_solver();
418 smt_circuit::UltraCircuit circuit = loader.get_field_smt_circuit(&solver);
419 bool res = verify_div_field(&solver, circuit);
420 EXPECT_FALSE(res);
421 if (res) {
422 save_buggy_witness(TESTNAME, circuit);
423 }
424}
425
433TEST(acir_formal_proofs, field_terms_eq)
434{
435 std::string TESTNAME = "Binary::Eq_Field_0_Field_0";
436 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
437 smt_solver::Solver solver1 = loader.get_smt_solver();
438 smt_circuit::UltraCircuit circuit1 = loader.get_field_smt_circuit(&solver1);
439
440 bool res1 = verify_eq_on_equlaity(&solver1, circuit1);
441 EXPECT_FALSE(res1);
442 if (res1) {
443 save_buggy_witness(TESTNAME, circuit1);
444 }
445
446 smt_solver::Solver solver2 = loader.get_smt_solver();
447 smt_circuit::UltraCircuit circuit2 = loader.get_field_smt_circuit(&solver2);
448
449 bool res2 = verify_eq_on_inequlaity(&solver2, circuit2);
450 EXPECT_FALSE(res2);
451 if (res2) {
452 save_buggy_witness(TESTNAME, circuit2);
453 }
454}
455
461TEST(acir_formal_proofs, field_terms_mul)
462{
463 std::string TESTNAME = "Binary::Mul_Field_0_Field_0";
464 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
465 smt_solver::Solver solver = loader.get_smt_solver();
466 smt_circuit::UltraCircuit circuit = loader.get_field_smt_circuit(&solver);
467 bool res = verify_mul(&solver, circuit);
468 EXPECT_FALSE(res);
469 if (res) {
470 save_buggy_witness(TESTNAME, circuit);
471 }
472}
473
479TEST(acir_formal_proofs, integer_terms_div)
480{
481 std::string TESTNAME = "Binary::Div_Signed_126_Signed_126";
482 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
483 smt_solver::Solver solver = loader.get_smt_solver();
484 smt_circuit::UltraCircuit circuit = loader.get_integer_smt_circuit(&solver);
485 bool res = verify_div(&solver, circuit);
486 EXPECT_FALSE(res);
487 if (res) {
488 save_buggy_witness(TESTNAME, circuit);
489 }
490}
491
496TEST(acir_formal_proofs, non_uniqueness_for_casts_field_to_u64)
497{
498 std::string TESTNAME = "Cast_Field_0";
499 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
500 smt_solver::Solver solver = loader.get_smt_solver();
501 bool res = verify_non_uniqueness_for_casts(&solver, &loader, smt_terms::TermType::FFTerm);
502 EXPECT_FALSE(res);
503}
504
509TEST(acir_formal_proofs, non_uniqueness_for_casts_u64_to_u8)
510{
511 std::string TESTNAME = "Cast_Unsigned_64";
512 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
513 smt_solver::Solver solver = loader.get_smt_solver();
514 bool res = verify_non_uniqueness_for_casts(&solver, &loader, smt_terms::TermType::BVTerm);
515 EXPECT_FALSE(res);
516}
517
522TEST(acir_formal_proofs, non_uniqueness_for_casts_u8_to_u64)
523{
524 std::string TESTNAME = "Cast_Unsigned_8";
525 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
526 smt_solver::Solver solver = loader.get_smt_solver();
527 bool res = verify_non_uniqueness_for_casts(&solver, &loader, smt_terms::TermType::BVTerm);
528 EXPECT_FALSE(res);
529}
acir_format.hpp
acir_loader.hpp
verify_buggy_witness
bool verify_buggy_witness(std::string instruction_name)
Verifies a previously saved witness file for correctness.
Definition acir_loader.test.cpp:46
TEST
TEST(acir_formal_proofs, uint_terms_add)
Tests 127-bit unsigned addition Verifies that the ACIR implementation of addition is correct Executio...
Definition acir_loader.test.cpp:65
ARTIFACTS_PATH
const std::string ARTIFACTS_PATH
Definition acir_loader.test.cpp:23
save_buggy_witness
void save_buggy_witness(std::string instruction_name, smt_circuit::UltraCircuit circuit)
Saves witness data when a bug is found during verification.
Definition acir_loader.test.cpp:32
circuit_checker.hpp
AcirToSmtLoader
Class for loading ACIR (Arithmetic Circuit Intermediate Representation) programs and converting them ...
Definition acir_loader.hpp:21
AcirToSmtLoader::get_smt_solver
smt_solver::Solver get_smt_solver()
Gets an SMT solver instance.
Definition acir_loader.cpp:46
AcirToSmtLoader::get_field_smt_circuit
smt_circuit::UltraCircuit get_field_smt_circuit(smt_solver::Solver *solver)
Creates an SMT circuit for field operations.
Definition acir_loader.cpp:65
AcirToSmtLoader::get_circuit_builder
bb::UltraCircuitBuilder get_circuit_builder()
Creates a circuit builder for the loaded program.
Definition acir_loader.cpp:37
AcirToSmtLoader::get_bitvec_smt_circuit
smt_circuit::UltraCircuit get_bitvec_smt_circuit(smt_solver::Solver *solver)
Creates an SMT circuit for bitvector operations.
Definition acir_loader.cpp:59
AcirToSmtLoader::get_integer_smt_circuit
smt_circuit::UltraCircuit get_integer_smt_circuit(smt_solver::Solver *solver)
Creates an SMT circuit for integer operations.
Definition acir_loader.cpp:71
bb::TranslatorCircuitChecker::check
static bool check(const Builder &circuit)
Check the witness satisifies the circuit.
Definition translator_circuit_checker.cpp:20
bb::UltraCircuitBuilder_
Definition ultra_circuit_builder.hpp:42
smt_circuit::UltraCircuit
Symbolic Circuit class for Standard Circuit Builder.
Definition ultra_circuit.hpp:53
smt_solver::Solver
Class for the solver.
Definition solver.hpp:80
smt_solver::Solver::print_assertions
void print_assertions()
Definition solver.cpp:421
client_ivc_recursive_verifier.hpp
info
void info(Args... args)
Definition log.hpp:70
builder
AluTraceBuilder builder
Definition alu.test.cpp:123
verify_shl32
bool verify_shl32(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify 32-bit left shift operation: c = a << b.
Definition formal_proofs.cpp:170
verify_xor
bool verify_xor(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify bitwise XOR operation: c = a ^ b.
Definition formal_proofs.cpp:138
verify_mod
bool verify_mod(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify modulo operation: c = a mod b.
Definition formal_proofs.cpp:93
verify_not_127
bool verify_not_127(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify NOT operation on 127 bits: b = ~a.
Definition formal_proofs.cpp:154
verify_lt
bool verify_lt(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify less than comparison: a < b.
Definition formal_proofs.cpp:245
verify_div_field
bool verify_div_field(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify field division operation: c = a / b (in field)
Definition formal_proofs.cpp:76
verify_div
bool verify_div(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify integer division operation: c = a / b.
Definition formal_proofs.cpp:61
verify_mul
bool verify_mul(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify multiplication operation: c = a * b.
Definition formal_proofs.cpp:46
verify_add
bool verify_add(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify addition operation: c = a + b.
Definition formal_proofs.cpp:16
verify_eq_on_inequlaity
bool verify_eq_on_inequlaity(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify equality comparison when values are not equal.
Definition formal_proofs.cpp:230
verify_sub
bool verify_sub(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify subtraction operation: c = a - b.
Definition formal_proofs.cpp:31
verify_shl64
bool verify_shl64(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify 64-bit left shift operation: c = a << b.
Definition formal_proofs.cpp:185
verify_non_uniqueness_for_casts
bool verify_non_uniqueness_for_casts(smt_solver::Solver *solver, AcirToSmtLoader *loader, smt_circuit::TermType type)
Verify non-uniqueness for casts.
Definition formal_proofs.cpp:290
verify_and
bool verify_and(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify bitwise AND operation: c = a & b.
Definition formal_proofs.cpp:123
verify_shr
bool verify_shr(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify right shift operation: c = a >> b.
Definition formal_proofs.cpp:200
verify_eq_on_equlaity
bool verify_eq_on_equlaity(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify equality comparison when values are equal.
Definition formal_proofs.cpp:215
verify_or
bool verify_or(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify bitwise OR operation: c = a | b.
Definition formal_proofs.cpp:108
verify_gt
bool verify_gt(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify greater than comparison: a > b.
Definition formal_proofs.cpp:260
formal_proofs.hpp
smt_terms::TermType::BVTerm
@ BVTerm
smt_terms::TermType::FFTerm
@ FFTerm
std::get
constexpr decltype(auto) get(::tuplet::tuple< T... > &&t) noexcept
Definition tuple.hpp:13
default_model_single
std::vector< bb::fr > default_model_single(const std::vector< std::string > &special, smt_circuit::CircuitBase &c, const std::string &fname, bool pack)
Get pretty formatted result of the solver work.
Definition smt_util.cpp:162
import_witness_single
std::vector< bb::fr > import_witness_single(const std::string &fname)
Import witness, obtained by solver, from file.
Definition smt_util.cpp:269
smt_util.hpp
ultra_circuit.hpp
ultra_circuit_builder.hpp