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/chonk_verifier/chonk_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.set_variable(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_128_Unsigned_128";
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_128_Unsigned_128";
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_128_Unsigned_128";
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_128_Unsigned_128";
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_128_Unsigned_128";
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_128_Unsigned_128";
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_128_Unsigned_128";
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_128_Unsigned_128";
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_shl8)
270{
271 std::string TESTNAME = "Binary::Shl_Unsigned_8_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_shl8(&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_128_Unsigned_128";
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_128_Unsigned_128";
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_128";
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_128(&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_64_Signed_64";
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_truncate_field_to_u64)
497{
498 std::string TESTNAME = "Truncate_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_truncate_u64_to_u8)
510{
511 std::string TESTNAME = "Truncate_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_truncate_i64_to_u8)
523{
524 std::string TESTNAME = "Truncate_Signed_64";
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}
530
535TEST(AcirFormalProofs, SignedAdd)
536{
537 std::string TESTNAME = "Binary::Add_Signed_64_Signed_64";
538 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
539 smt_solver::Solver solver = loader.get_smt_solver();
540 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
541 bool res = verify_add_signed(&solver, circuit, 64);
542 EXPECT_FALSE(res);
543 if (res) {
544 save_buggy_witness(TESTNAME, circuit);
545 }
546}
547
552TEST(AcirFormalProofs, SignedAnd)
553{
554 std::string TESTNAME = "Binary::And_Signed_64_Signed_64";
555 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
556 smt_solver::Solver solver = loader.get_smt_solver();
557 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
558 bool res = verify_and(&solver, circuit);
559 EXPECT_FALSE(res);
560 if (res) {
561 save_buggy_witness(TESTNAME, circuit);
562 }
563}
564
569TEST(AcirFormalProofs, SignedEq)
570{
571 std::string TESTNAME = "Binary::Eq_Signed_64_Signed_64";
572 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
573 smt_solver::Solver solver = loader.get_smt_solver();
574 smt_circuit::UltraCircuit circuit = loader.get_integer_smt_circuit(&solver);
575 bool res = verify_eq_on_equlaity(&solver, circuit);
576 EXPECT_FALSE(res);
577 if (res) {
578 save_buggy_witness(TESTNAME, circuit);
579 }
580 bool res2 = verify_eq_on_inequlaity(&solver, circuit);
581 EXPECT_FALSE(res2);
582 if (res2) {
583 save_buggy_witness(TESTNAME, circuit);
584 }
585}
586
591TEST(AcirFormalProofs, SignedMod)
592{
593 std::string TESTNAME = "Binary::Mod_Signed_64_Signed_64";
594 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
595 smt_solver::Solver solver = loader.get_smt_solver();
596 smt_circuit::UltraCircuit circuit = loader.get_integer_smt_circuit(&solver);
597 bool res = verify_mod(&solver, circuit);
598 EXPECT_FALSE(res);
599 if (res) {
600 save_buggy_witness(TESTNAME, circuit);
601 }
602}
603
608TEST(AcirFormalProofs, SignedMul)
609{
610 std::string TESTNAME = "Binary::Mul_Signed_64_Signed_64";
611 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
612 smt_solver::Solver solver = loader.get_smt_solver();
613 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
614 bool res = verify_mul_signed(&solver, circuit, 64);
615 EXPECT_FALSE(res);
616 if (res) {
617 save_buggy_witness(TESTNAME, circuit);
618 }
619}
620
625TEST(AcirFormalProofs, SignedOr)
626{
627 std::string TESTNAME = "Binary::Or_Signed_64_Signed_64";
628 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
629 smt_solver::Solver solver = loader.get_smt_solver();
630 smt_circuit::UltraCircuit circuit = loader.get_integer_smt_circuit(&solver);
631 bool res = verify_or(&solver, circuit);
632 EXPECT_FALSE(res);
633 if (res) {
634 save_buggy_witness(TESTNAME, circuit);
635 }
636}
637
642TEST(AcirFormalProofs, SignedShl)
643{
644 std::string TESTNAME = "Binary::Shl_Signed_8_Signed_8";
645 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
646 smt_solver::Solver solver = loader.get_smt_solver();
647 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
648 bool res = verify_shl8(&solver, circuit);
649 EXPECT_FALSE(res);
650 if (res) {
651 save_buggy_witness(TESTNAME, circuit);
652 }
653}
654
659TEST(AcirFormalProofs, SignedShr)
660{
661 std::string TESTNAME = "Binary::Shr_Signed_8_Signed_8";
662 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
663 smt_solver::Solver solver = loader.get_smt_solver();
664 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
665 bool res = verify_shr(&solver, circuit);
666 EXPECT_FALSE(res);
667 if (res) {
668 save_buggy_witness(TESTNAME, circuit);
669 }
670}
671
676TEST(AcirFormalProofs, SignedSub)
677{
678 std::string TESTNAME = "Binary::Sub_Signed_64_Signed_64";
679 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
680 smt_solver::Solver solver = loader.get_smt_solver();
681 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
682 bool res = verify_sub_signed(&solver, circuit, 64);
683 EXPECT_FALSE(res);
684 if (res) {
685 save_buggy_witness(TESTNAME, circuit);
686 }
687}
688
693TEST(AcirFormalProofs, SignedXor)
694{
695 std::string TESTNAME = "Binary::Xor_Signed_64_Signed_64";
696 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
697 smt_solver::Solver solver = loader.get_smt_solver();
698 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
699 bool res = verify_xor(&solver, circuit);
700 EXPECT_FALSE(res);
701}
702
707TEST(AcirFormalProofs, SignedNot)
708{
709 std::string TESTNAME = "Not_Signed_64";
710 AcirToSmtLoader loader = AcirToSmtLoader(ARTIFACTS_PATH + TESTNAME + ".acir");
711 smt_solver::Solver solver = loader.get_smt_solver();
712 smt_circuit::UltraCircuit circuit = loader.get_bitvec_smt_circuit(&solver);
713 bool res = verify_not_64(&solver, circuit);
714 EXPECT_FALSE(res);
715 if (res) {
716 save_buggy_witness(TESTNAME, circuit);
717 }
718}
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 128-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
chonk_recursive_verifier.hpp
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:36
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::CircuitBuilderBase::set_variable
void set_variable(const uint32_t index, const FF &value)
Set the value of the variable pointed to by a witness index.
Definition circuit_builder_base.hpp:168
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:41
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
info
void info(Args... args)
Definition log.hpp:75
builder
AluTraceBuilder builder
Definition alu.test.cpp:124
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:232
verify_xor
bool verify_xor(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify bitwise XOR operation: c = a ^ b.
Definition formal_proofs.cpp:184
verify_sub_signed
bool verify_sub_signed(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit, uint32_t bit_size)
Verify subtraction operation: c = a - b + truncate to bit_size bits.
Definition formal_proofs.cpp:62
verify_mod
bool verify_mod(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify modulo operation: c = a mod b.
Definition formal_proofs.cpp:139
verify_not_128
bool verify_not_128(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify NOT operation on 128 bits: b = ~a.
Definition formal_proofs.cpp:216
verify_not_64
bool verify_not_64(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify NOT operation on 64 bits: b = ~a.
Definition formal_proofs.cpp:199
verify_add_signed
bool verify_add_signed(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit, uint32_t bit_size)
Verify addition operation: c = a + b + truncate to bit_size bits.
Definition formal_proofs.cpp:32
verify_lt
bool verify_lt(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify less than comparison: a < b.
Definition formal_proofs.cpp:322
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:122
verify_div
bool verify_div(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify integer division operation: c = a / b.
Definition formal_proofs.cpp:107
verify_mul
bool verify_mul(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify multiplication operation: c = a * b.
Definition formal_proofs.cpp:77
verify_add
bool verify_add(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify addition operation: c = a + b.
Definition formal_proofs.cpp:17
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:307
verify_sub
bool verify_sub(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify subtraction operation: c = a - b.
Definition formal_proofs.cpp:47
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:367
verify_shl8
bool verify_shl8(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify 8-bit left shift operation: c = a << b.
Definition formal_proofs.cpp:262
verify_and
bool verify_and(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify bitwise AND operation: c = a & b.
Definition formal_proofs.cpp:169
verify_shr
bool verify_shr(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify right shift operation: c = a >> b.
Definition formal_proofs.cpp:277
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:292
verify_or
bool verify_or(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify bitwise OR operation: c = a | b.
Definition formal_proofs.cpp:154
verify_mul_signed
bool verify_mul_signed(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit, uint32_t bit_size)
Verify multiplication operation: c = a * b with signed operands and truncate to bit_size bits.
Definition formal_proofs.cpp:92
verify_gt
bool verify_gt(smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
Verify greater than comparison: a > b.
Definition formal_proofs.cpp:337
formal_proofs.hpp
smt_terms::TermType::BVTerm
@ BVTerm
smt_terms::TermType::FFTerm
@ FFTerm
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