Barretenberg
The ZK-SNARK library at the core of Aztec
Loading...
Searching...
No Matches
bvterm.test.cpp
Go to the documentation of this file.
1#include <cstdint>
2#include <unordered_map>
3
4#include "barretenberg/smt_verification/util/smt_util.hpp"
5#include "barretenberg/stdlib/primitives/logic/logic.hpp"
6#include "term.hpp"
7
8#include <gtest/gtest.h>
9
10namespace {
11auto& engine = bb::numeric::get_randomness();
12}
13
14using namespace bb;
15using Builder = UltraCircuitBuilder;
16using witness_ct = stdlib::witness_t<Builder>;
17
18using namespace smt_terms;
19
20TEST(BVTerm, addition)
21{
22 uint32_t a = engine.get_random_uint32();
23 uint32_t b = engine.get_random_uint32();
24 uint32_t c = a + b;
25
26 uint32_t modulus_base = 16;
27 uint32_t bitvector_size = 32;
28 Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001",
29 default_solver_config,
30 modulus_base,
31 bitvector_size);
32
33 STerm x = BVVar("x", &s);
34 STerm y = BVVar("y", &s);
35 STerm z = x + y;
36
37 z == c;
38 x == a;
39 ASSERT_TRUE(s.check());
40
41 bb::fr yvals = string_to_fr(s[y], /*base=*/2, /*is_signed=*/false);
42 ASSERT_EQ(bb::fr(b), yvals);
43}
44
45TEST(BVTerm, subtraction)
46{
47 uint32_t a = engine.get_random_uint32();
48 uint32_t b = engine.get_random_uint32();
49 uint32_t c = a - b;
50
51 uint32_t modulus_base = 16;
52 uint32_t bitvector_size = 32;
53 Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001",
54 default_solver_config,
55 modulus_base,
56 bitvector_size);
57
58 STerm x = BVVar("x", &s);
59 STerm y = BVVar("y", &s);
60 STerm z = x - y;
61
62 z == c;
63 x == a;
64 ASSERT_TRUE(s.check());
65
66 bb::fr yvals = string_to_fr(s[y], /*base=*/2, /*is_signed=*/false);
67 ASSERT_EQ(bb::fr(b), yvals);
68}
69
70TEST(BVTerm, xor)
71{
72 uint32_t a = engine.get_random_uint32();
73 uint32_t b = engine.get_random_uint32();
74 uint32_t c = a ^ b;
75
76 uint32_t modulus_base = 16;
77 uint32_t bitvector_size = 32;
78 Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001",
79 default_solver_config,
80 modulus_base,
81 bitvector_size);
82
83 STerm x = BVVar("x", &s);
84 STerm y = BVVar("y", &s);
85 STerm z = x ^ y;
86
87 z == c;
88 x == a;
89 ASSERT_TRUE(s.check());
90
91 bb::fr yvals = string_to_fr(s[y], /*base=*/2, /*is_signed=*/false);
92 ASSERT_EQ(bb::fr(b), yvals);
93}
94
95TEST(BVTerm, rotr)
96{
97 uint32_t a = engine.get_random_uint32();
98 uint32_t b = (a >> 10) | (a << 22);
99
100 uint32_t modulus_base = 16;
101 uint32_t bitvector_size = 32;
102 Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001",
103 default_solver_config,
104 modulus_base,
105 bitvector_size);
106
107 STerm x = BVVar("x", &s);
108 STerm y = x.rotr(10);
109
110 y == b;
111 ASSERT_TRUE(s.check());
112
113 bb::fr xvals = string_to_fr(s[x], /*base=*/2, /*is_signed=*/false);
114 ASSERT_EQ(bb::fr(a), xvals);
115}
116
117TEST(BVTerm, rotl)
118{
119 uint32_t a = engine.get_random_uint32();
120 uint32_t b = (a << 10) | (a >> 22);
121
122 uint32_t modulus_base = 16;
123 uint32_t bitvector_size = 32;
124 Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001",
125 default_solver_config,
126 modulus_base,
127 bitvector_size);
128
129 STerm x = BVVar("x", &s);
130 STerm y = x.rotl(10);
131
132 y == b;
133 ASSERT_TRUE(s.check());
134
135 bb::fr xvals = string_to_fr(s[x], /*base=*/2, /*is_signed=*/false);
136 ASSERT_EQ(bb::fr(a), xvals);
137}
138
139// non bijective operators
140TEST(BVTerm, mul)
141{
142 Builder builder;
143 uint32_t a = engine.get_random_uint32();
144 uint32_t b = engine.get_random_uint32();
145 uint32_t c = a * b;
146
147 uint32_t modulus_base = 16;
148 uint32_t bitvector_size = 32;
149 Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001",
150 default_solver_config,
151 modulus_base,
152 bitvector_size);
153
154 STerm x = BVVar("x", &s);
155 STerm y = BVVar("y", &s);
156 STerm z = x * y;
157
158 x == a;
159 y == b;
160
161 ASSERT_TRUE(s.check());
162
163 bb::fr xvals = string_to_fr(s[z], /*base=*/2, /*is_signed=*/false);
164 ASSERT_EQ(bb::fr(c), xvals);
165}
166
167TEST(BVTerm, and)
168{
169 uint32_t a = engine.get_random_uint32();
170 uint32_t b = engine.get_random_uint32();
171 uint32_t c = a & b;
172
173 uint32_t modulus_base = 16;
174 uint32_t bitvector_size = 32;
175 Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001",
176 default_solver_config,
177 modulus_base,
178 bitvector_size);
179
180 STerm x = BVVar("x", &s);
181 STerm y = BVVar("y", &s);
182 STerm z = x & y;
183
184 x == a;
185 y == b;
186
187 ASSERT_TRUE(s.check());
188
189 bb::fr xvals = string_to_fr(s[z], /*base=*/2, /*is_signed=*/false);
190 ASSERT_EQ(bb::fr(c), xvals);
191}
192
193TEST(BVTerm, or)
194{
195 uint32_t a = engine.get_random_uint32();
196 uint32_t b = engine.get_random_uint32();
197 uint32_t c = a | b;
198
199 uint32_t modulus_base = 16;
200 uint32_t bitvector_size = 32;
201 Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001",
202 default_solver_config,
203 modulus_base,
204 bitvector_size);
205
206 STerm x = BVVar("x", &s);
207 STerm y = BVVar("y", &s);
208 STerm z = x | y;
209
210 x == a;
211 y == b;
212
213 ASSERT_TRUE(s.check());
214
215 bb::fr xvals = string_to_fr(s[z], /*base=*/2, /*is_signed=*/false);
216 ASSERT_EQ(bb::fr(c), xvals);
217}
218
219TEST(BVTerm, div)
220{
221 uint32_t a = engine.get_random_uint32();
222 uint32_t b = engine.get_random_uint32();
223 uint32_t c = a / b;
224
225 uint32_t modulus_base = 16;
226 uint32_t bitvector_size = 32;
227 Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001",
228 default_solver_config,
229 modulus_base,
230 bitvector_size);
231
232 STerm x = BVVar("x", &s);
233 STerm y = BVVar("y", &s);
234 STerm z = x / y;
235
236 x == a;
237 y == b;
238
239 ASSERT_TRUE(s.check());
240
241 bb::fr xvals = string_to_fr(s[z], /*base=*/2, /*is_signed=*/false);
242 ASSERT_EQ(bb::fr(c), xvals);
243}
244
245TEST(BVTerm, shr)
246{
247 uint32_t a = engine.get_random_uint32();
248 uint32_t b = a >> 5;
249
250 uint32_t modulus_base = 16;
251 uint32_t bitvector_size = 32;
252 Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001",
253 default_solver_config,
254 modulus_base,
255 bitvector_size);
256
257 STerm x = BVVar("x", &s);
258 STerm y = x >> 5;
259
260 x == a;
261
262 ASSERT_TRUE(s.check());
263
264 bb::fr xvals = string_to_fr(s[y], /*base=*/2, /*is_signed=*/false);
265 ASSERT_EQ(bb::fr(b), xvals);
266}
267
268TEST(BVTerm, shl)
269{
270 uint32_t a = engine.get_random_uint32();
271 uint32_t b = a << 5;
272
273 uint32_t modulus_base = 16;
274 uint32_t bitvector_size = 32;
275 Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001",
276 default_solver_config,
277 modulus_base,
278 bitvector_size);
279
280 STerm x = BVVar("x", &s);
281 STerm y = x << 5;
282
283 x == a;
284
285 ASSERT_TRUE(s.check());
286
287 bb::fr xvals = string_to_fr(s[y], /*base=*/2, /*is_signed=*/false);
288 ASSERT_EQ(bb::fr(b), xvals);
289}
290
291TEST(BVTerm, truncate)
292{
293 uint32_t a = engine.get_random_uint32();
294 unsigned int mask = (1 << 10) - 1;
295 uint32_t b = a & mask;
296
297 uint32_t modulus_base = 16;
298 uint32_t bitvector_size = 32;
299 Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001",
300 default_solver_config,
301 modulus_base,
302 bitvector_size);
303
304 STerm x = BVVar("x", &s);
305 STerm y = x.truncate(9);
306
307 x == a;
308
309 ASSERT_TRUE(s.check());
310
311 bb::fr xvals = string_to_fr(s[y], /*base=*/2, /*is_signed=*/false);
312 ASSERT_EQ(bb::fr(b), xvals);
313}
314
315TEST(BVTerm, extract_bit)
316{
317 uint32_t a = engine.get_random_uint32();
318 unsigned int mask = (1 << 10);
319 uint32_t b = a & mask;
320 b >>= 10;
321
322 uint32_t modulus_base = 16;
323 uint32_t bitvector_size = 32;
324 Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001",
325 default_solver_config,
326 modulus_base,
327 bitvector_size);
328
329 STerm x = BVVar("x", &s);
330 STerm y = x.extract_bit(10);
331
332 x == a;
333
334 ASSERT_TRUE(s.check());
335
336 bb::fr xvals = string_to_fr(s[y], /*base=*/2, /*is_signed=*/false);
337 ASSERT_EQ(bb::fr(b), xvals);
338}
bb::stdlib::witness_t
Definition witness.hpp:16
smt_solver::Solver
Class for the solver.
Definition solver.hpp:80
smt_solver::Solver::check
bool check()
Definition solver.cpp:11
smt_terms::STerm
Symbolic term element class.
Definition term.hpp:114
smt_terms::STerm::rotl
STerm rotl(const uint32_t &n) const
Definition term.cpp:450
smt_terms::STerm::rotr
STerm rotr(const uint32_t &n) const
Definition term.cpp:439
smt_terms::STerm::extract_bit
STerm extract_bit(const uint32_t &bit_index)
Returns ith bit of variable.
Definition term.cpp:476
smt_terms::STerm::truncate
STerm truncate(const uint32_t &to_size)
Returns last to_size bits of variable.
Definition term.cpp:461
builder
AluTraceBuilder builder
Definition alu.test.cpp:123
a
FF a
Definition field_gt.test.cpp:52
b
FF b
Definition field_gt.test.cpp:53
engine
auto & engine
Definition graph_description_protogalaxy.test.cpp:15
shr
smt_circuit::STerm shr(smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver::Solver *solver)
Right shift operation.
Definition helpers.cpp:40
shl
smt_circuit::STerm shl(smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver::Solver *solver)
Left shift operation without truncation.
Definition helpers.cpp:34
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::UltraCircuitBuilder
UltraCircuitBuilder_< UltraExecutionTraceBlocks > UltraCircuitBuilder
Definition circuit_builders_fwd.hpp:24
bb::TEST
TEST(BoomerangMegaCircuitBuilder, BasicCircuit)
Definition graph_description_megacircuitbuilder.test.cpp:22
smt_solver::default_solver_config
const SolverConfiguration default_solver_config
Definition solver.hpp:37
smt_terms
Definition bool.cpp:3
smt_terms::BVVar
STerm BVVar(const std::string &name, Solver *slv)
Definition term.cpp:615
smt_terms::TermType::BVTerm
@ BVTerm
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