rsnark_core/api.rs
1use crate::{
2 Metadata, Variable,
3 types::{OpCode, VariableType},
4};
5
6/// The main API trait for building arithmetic circuits in zero-knowledge proof systems.
7///
8/// This trait provides a comprehensive set of operations for constructing arithmetic circuits,
9/// including basic arithmetic operations, logical operations, assertions, and utility functions.
10/// All operations work with variables that implement the `Variable` trait, enabling flexible
11/// circuit construction with different variable types.
12pub trait API {
13 fn metadata(&self) -> &impl Metadata;
14
15 fn append_operation(
16 &mut self,
17 op: OpCode,
18 inputs: Vec<VariableType>,
19 outputs: Vec<VariableType>,
20 );
21
22 fn allocate_local_variable(&mut self) -> VariableType;
23
24 fn allocate_local_variable_n(&mut self, n: u64) -> Vec<VariableType> {
25 let mut res = Vec::with_capacity(n as usize);
26 for _ in 0..n {
27 res.push(self.allocate_local_variable());
28 }
29 res
30 }
31
32 /// Performs addition of two variables: res = x1 + x2
33 ///
34 /// This is a convenience method that calls `add_multi` with no additional variables.
35 ///
36 /// # Arguments
37 /// * `x1` - First operand
38 /// * `x2` - Second operand
39 ///
40 /// # Returns
41 /// A new local variable containing the sum
42 fn add(&mut self, x1: &impl Variable, x2: &impl Variable) -> VariableType {
43 self.add_multi(x1, x2, &[])
44 }
45
46 /// Performs addition of multiple variables: res = x1 + x2 + ... + xn
47 ///
48 /// # Arguments
49 /// * `x1` - First operand
50 /// * `x2` - Second operand
51 /// * `xn` - Additional operands to sum
52 ///
53 /// # Returns
54 /// A new local variable containing the sum of all operands
55 fn add_multi(
56 &mut self,
57 x1: &impl Variable,
58 x2: &impl Variable,
59 xn: &[&dyn Variable],
60 ) -> VariableType {
61 let res = self.allocate_local_variable();
62
63 self.append_operation(
64 OpCode::Add,
65 get_variable_type_2n(x1, x2, xn),
66 vec![res.clone()],
67 );
68
69 res
70 }
71
72 /// Performs multiply-accumulate operation: res = a + (b * c)
73 ///
74 /// This is an optimized operation that combines multiplication and addition
75 /// in a single constraint, which can be more efficient than separate operations.
76 ///
77 /// # Arguments
78 /// * `a` - The accumulator value
79 /// * `b` - First multiplicand
80 /// * `c` - Second multiplicand
81 ///
82 /// # Returns
83 /// A new local variable containing the result a + (b * c)
84 fn mul_acc(&mut self, a: &impl Variable, b: &impl Variable, c: &impl Variable) -> VariableType {
85 let res = self.allocate_local_variable();
86
87 self.append_operation(
88 OpCode::MulAcc,
89 vec![a.ty(), b.ty(), c.ty()],
90 vec![res.clone()],
91 );
92
93 res
94 }
95
96 /// Performs negation: res = -x
97 ///
98 /// # Arguments
99 /// * `x` - The variable to negate
100 ///
101 /// # Returns
102 /// A new local variable containing the negated value
103 fn neg(&mut self, x: &impl Variable) -> VariableType {
104 let res = self.allocate_local_variable();
105
106 self.append_operation(OpCode::Neg, vec![x.ty()], vec![res.clone()]);
107
108 res
109 }
110
111 /// Performs subtraction of two variables: res = x1 - x2
112 ///
113 /// This is a convenience method that calls `sub_multi` with no additional variables.
114 ///
115 /// # Arguments
116 /// * `x1` - Minuend (value to subtract from)
117 /// * `x2` - Subtrahend (value to subtract)
118 ///
119 /// # Returns
120 /// A new local variable containing the difference
121 fn sub(&mut self, x1: &impl Variable, x2: &impl Variable) -> VariableType {
122 self.sub_multi(x1, x2, &[])
123 }
124
125 /// Performs subtraction of multiple variables: res = x1 - x2 - ... - xn
126 ///
127 /// # Arguments
128 /// * `x1` - Minuend (value to subtract from)
129 /// * `x2` - First subtrahend
130 /// * `xn` - Additional values to subtract
131 ///
132 /// # Returns
133 /// A new local variable containing the result of all subtractions
134 fn sub_multi(
135 &mut self,
136 x1: &impl Variable,
137 x2: &impl Variable,
138 xn: &[&dyn Variable],
139 ) -> VariableType {
140 let res = self.allocate_local_variable();
141
142 self.append_operation(
143 OpCode::Sub,
144 get_variable_type_2n(x1, x2, xn),
145 vec![res.clone()],
146 );
147
148 res
149 }
150
151 /// Performs multiplication of two variables: res = x1 * x2
152 ///
153 /// This is a convenience method that calls `mul_multi` with no additional variables.
154 ///
155 /// # Arguments
156 /// * `x1` - First multiplicand
157 /// * `x2` - Second multiplicand
158 ///
159 /// # Returns
160 /// A new local variable containing the product
161 fn mul(&mut self, x1: &impl Variable, x2: &impl Variable) -> VariableType {
162 self.mul_multi(x1, x2, &[])
163 }
164
165 /// Performs multiplication of multiple variables: res = x1 * x2 * ... * xn
166 ///
167 /// # Arguments
168 /// * `x1` - First multiplicand
169 /// * `x2` - Second multiplicand
170 /// * `xn` - Additional multiplicands
171 ///
172 /// # Returns
173 /// A new local variable containing the product of all operands
174 fn mul_multi(
175 &mut self,
176 x1: &impl Variable,
177 x2: &impl Variable,
178 xn: &[&dyn Variable],
179 ) -> VariableType {
180 let res = self.allocate_local_variable();
181
182 self.append_operation(
183 OpCode::Mul,
184 get_variable_type_2n(x1, x2, xn),
185 vec![res.clone()],
186 );
187
188 res
189 }
190
191 /// Performs unchecked division: res = x1 / x2
192 ///
193 /// This division operation does not enforce that the divisor is non-zero.
194 /// If both x1 and x2 are zero, the result is defined as 0.
195 ///
196 /// # Arguments
197 /// * `x1` - Dividend
198 /// * `x2` - Divisor
199 ///
200 /// # Returns
201 /// A new local variable containing the quotient
202 ///
203 /// # Safety
204 /// This operation does not verify that x2 ≠ 0. Use `div` for checked division.
205 fn div_unchecked(&mut self, x1: &impl Variable, x2: &impl Variable) -> VariableType {
206 let res = self.allocate_local_variable();
207
208 self.append_operation(
209 OpCode::DivUnchecked,
210 vec![x1.ty(), x2.ty()],
211 vec![res.clone()],
212 );
213
214 res
215 }
216
217 /// Performs checked division: res = x1 / x2
218 ///
219 /// This division operation enforces that the divisor is non-zero.
220 /// The circuit constraint will fail if x2 equals zero.
221 ///
222 /// # Arguments
223 /// * `x1` - Dividend
224 /// * `x2` - Divisor (must be non-zero)
225 ///
226 /// # Returns
227 /// A new local variable containing the quotient
228 ///
229 /// # Panics
230 /// The circuit will be unsatisfiable if x2 == 0
231 fn div(&mut self, x1: &impl Variable, x2: &impl Variable) -> VariableType {
232 let res = self.allocate_local_variable();
233
234 self.append_operation(OpCode::Div, vec![x1.ty(), x2.ty()], vec![res.clone()]);
235
236 res
237 }
238
239 /// Computes the multiplicative inverse: res = 1 / x
240 ///
241 /// This operation enforces that x is non-zero. The circuit constraint
242 /// will fail if x equals zero.
243 ///
244 /// # Arguments
245 /// * `x` - The variable to invert (must be non-zero)
246 ///
247 /// # Returns
248 /// A new local variable containing the multiplicative inverse
249 ///
250 /// # Panics
251 /// The circuit will be unsatisfiable if x == 0
252 fn inverse(&mut self, x: &impl Variable) -> VariableType {
253 let res = self.allocate_local_variable();
254
255 self.append_operation(OpCode::Inverse, vec![x.ty()], vec![res.clone()]);
256
257 res
258 }
259
260 /// Converts a variable to its binary representation
261 ///
262 /// Decomposes the input variable into its constituent bits, returning
263 /// them as a vector of boolean variables.
264 ///
265 /// # Arguments
266 /// * `x` - The variable to decompose
267 /// * `n` - Number of bits to extract (starting from least significant bit)
268 ///
269 /// # Returns
270 /// A vector of local variables representing the binary decomposition,
271 /// where index 0 is the least significant bit
272 fn variable_to_binary(&mut self, x: &impl Variable, n: u64) -> Vec<VariableType> {
273 let res = self.allocate_local_variable_n(n);
274
275 self.append_operation(OpCode::ToBinary, vec![x.ty(), n.ty()], res.clone());
276
277 res
278 }
279
280 /// Reconstructs a variable from its binary representation
281 ///
282 /// Combines a vector of bit variables into a single field element,
283 /// with the first element being the least significant bit.
284 ///
285 /// # Arguments
286 /// * `b` - Array of bit variables (each should be 0 or 1)
287 ///
288 /// # Returns
289 /// A local variable representing the packed binary value
290 fn variable_from_binary(&mut self, b: &[&dyn Variable]) -> VariableType {
291 let res = self.allocate_local_variable();
292
293 self.append_operation(
294 OpCode::FromBinary,
295 b.iter().map(|x| x.ty()).collect(),
296 vec![res.clone()],
297 );
298
299 res
300 }
301
302 /// Performs bitwise XOR operation: res = x1 ^ x2
303 ///
304 /// # Arguments
305 /// * `x1` - First operand
306 /// * `x2` - Second operand
307 ///
308 /// # Returns
309 /// A new local variable containing the XOR result
310 fn xor(&mut self, x1: &impl Variable, x2: &impl Variable) -> VariableType {
311 let res = self.allocate_local_variable();
312
313 self.append_operation(OpCode::Xor, vec![x1.ty(), x2.ty()], vec![res.clone()]);
314
315 res
316 }
317
318 /// Performs bitwise OR operation: res = x1 | x2
319 ///
320 /// # Arguments
321 /// * `x1` - First operand
322 /// * `x2` - Second operand
323 ///
324 /// # Returns
325 /// A new local variable containing the OR result
326 fn or(&mut self, x1: &impl Variable, x2: &impl Variable) -> VariableType {
327 let res = self.allocate_local_variable();
328
329 self.append_operation(OpCode::Or, vec![x1.ty(), x2.ty()], vec![res.clone()]);
330
331 res
332 }
333
334 /// Performs bitwise AND operation: res = x1 & x2
335 ///
336 /// # Arguments
337 /// * `x1` - First operand
338 /// * `x2` - Second operand
339 ///
340 /// # Returns
341 /// A new local variable containing the AND result
342 fn and(&mut self, x1: &impl Variable, x2: &impl Variable) -> VariableType {
343 let res = self.allocate_local_variable();
344
345 self.append_operation(OpCode::And, vec![x1.ty(), x2.ty()], vec![res.clone()]);
346
347 res
348 }
349
350 /// Performs conditional selection: res = x1 ? x2 : x3
351 ///
352 /// If x1 is non-zero (true), returns x2; otherwise returns x3.
353 /// This is equivalent to a ternary operator in programming languages.
354 ///
355 /// # Arguments
356 /// * `x1` - Condition variable (typically 0 or 1)
357 /// * `x2` - Value to return if condition is true
358 /// * `x3` - Value to return if condition is false
359 ///
360 /// # Returns
361 /// A new local variable containing the selected value
362 fn select(
363 &mut self,
364 x1: &impl Variable,
365 x2: &impl Variable,
366 x3: &impl Variable,
367 ) -> VariableType {
368 let res = self.allocate_local_variable();
369
370 self.append_operation(
371 OpCode::Select,
372 vec![x1.ty(), x2.ty(), x3.ty()],
373 vec![res.clone()],
374 );
375
376 res
377 }
378
379 /// Performs a 2-bit lookup table operation
380 ///
381 /// Selects one of four values (y1, y2, y3, y4) based on a 2-bit index
382 /// formed by concatenating bits b1 and b0 (b1 is MSB, b0 is LSB).
383 ///
384 /// # Arguments
385 /// * `b0` - Least significant bit of the index
386 /// * `b1` - Most significant bit of the index
387 /// * `y1` - Value for index 00 (b1=0, b0=0)
388 /// * `y2` - Value for index 01 (b1=0, b0=1)
389 /// * `y3` - Value for index 10 (b1=1, b0=0)
390 /// * `y4` - Value for index 11 (b1=1, b0=1)
391 ///
392 /// # Returns
393 /// The selected value based on the 2-bit index
394 fn lookup2(
395 &mut self,
396 b0: &impl Variable,
397 b1: &impl Variable,
398 y1: &impl Variable,
399 y2: &impl Variable,
400 y3: &impl Variable,
401 y4: &impl Variable,
402 ) -> VariableType {
403 let res = self.allocate_local_variable();
404
405 self.append_operation(
406 OpCode::Lookup2,
407 vec![b0.ty(), b1.ty(), y1.ty(), y2.ty(), y3.ty(), y4.ty()],
408 vec![res.clone()],
409 );
410
411 res
412 }
413
414 /// Tests if a variable is zero
415 ///
416 /// Returns 1 if the input variable equals zero, 0 otherwise.
417 /// This is useful for implementing conditional logic based on zero checks.
418 ///
419 /// # Arguments
420 /// * `x` - The variable to test
421 ///
422 /// # Returns
423 /// A boolean variable (1 if x == 0, 0 if x != 0)
424 fn is_zero(&mut self, x: &impl Variable) -> VariableType {
425 let res = self.allocate_local_variable();
426
427 self.append_operation(OpCode::IsZero, vec![x.ty()], vec![res.clone()]);
428
429 res
430 }
431
432 /// Compares two variables and returns the comparison result
433 ///
434 /// Returns a three-way comparison result:
435 /// * 1 if x1 > x2
436 /// * 0 if x1 = x2
437 /// * -1 if x1 < x2
438 ///
439 /// # Arguments
440 /// * `x1` - First value to compare
441 /// * `x2` - Second value to compare
442 ///
443 /// # Returns
444 /// A local variable containing the comparison result (-1, 0, or 1)
445 fn cmp(&mut self, x1: &impl Variable, x2: &impl Variable) -> VariableType {
446 let res = self.allocate_local_variable();
447
448 self.append_operation(OpCode::Cmp, vec![x1.ty(), x2.ty()], vec![res.clone()]);
449
450 res
451 }
452
453 /// Asserts that two variables are equal
454 ///
455 /// Adds a constraint requiring x1 == x2. The circuit will be
456 /// unsatisfiable if this condition is not met.
457 ///
458 /// # Arguments
459 /// * `x1` - First variable
460 /// * `x2` - Second variable
461 ///
462 /// # Panics
463 /// The circuit will be unsatisfiable if x1 != x2
464 fn assert_is_equal(&mut self, x1: &impl Variable, x2: &impl Variable) {
465 self.append_operation(OpCode::AssertIsEqual, vec![x1.ty(), x2.ty()], vec![]);
466 }
467
468 /// Asserts that two variables are different
469 ///
470 /// Adds a constraint requiring x1 != x2. The circuit will be
471 /// unsatisfiable if this condition is not met.
472 ///
473 /// # Arguments
474 /// * `x1` - First variable
475 /// * `x2` - Second variable
476 ///
477 /// # Panics
478 /// The circuit will be unsatisfiable if x1 == x2
479 fn assert_is_different(&mut self, x1: &impl Variable, x2: &impl Variable) {
480 self.append_operation(OpCode::AssertIsDifferent, vec![x1.ty(), x2.ty()], vec![]);
481 }
482
483 /// Asserts that a variable is a boolean value
484 ///
485 /// Adds a constraint requiring x to be either 0 or 1.
486 /// The circuit will be unsatisfiable if x has any other value.
487 ///
488 /// # Arguments
489 /// * `x` - The variable to constrain as boolean
490 ///
491 /// # Panics
492 /// The circuit will be unsatisfiable if x is not 0 or 1
493 fn assert_is_boolean(&mut self, x: &impl Variable) {
494 self.append_operation(OpCode::AssertIsBoolean, vec![x.ty()], vec![]);
495 }
496
497 /// Asserts that a variable is a crumb (2-bit value)
498 ///
499 /// Adds a constraint requiring x to be one of {0, 1, 2, 3}.
500 /// The circuit will be unsatisfiable if x has any other value.
501 ///
502 /// # Arguments
503 /// * `x` - The variable to constrain as a crumb
504 ///
505 /// # Panics
506 /// The circuit will be unsatisfiable if x is not in {0, 1, 2, 3}
507 fn assert_is_crumb(&mut self, x: &impl Variable) {
508 self.append_operation(OpCode::AssertIsCrumb, vec![x.ty()], vec![]);
509 }
510
511 /// Asserts that a variable is less than or equal to a bound
512 ///
513 /// Adds a constraint requiring v <= bound. The circuit will be
514 /// unsatisfiable if this condition is not met.
515 ///
516 /// # Arguments
517 /// * `v` - The variable to check
518 /// * `bound` - The upper bound
519 ///
520 /// # Panics
521 /// The circuit will be unsatisfiable if v > bound
522 fn assert_is_less_or_equal(&mut self, v: &impl Variable, bound: &impl Variable) {
523 self.append_operation(
524 OpCode::AssertIsLessOrEqual,
525 vec![v.ty(), bound.ty()],
526 vec![],
527 );
528 }
529
530 /// Prints a debug message during circuit execution
531 ///
532 /// This is primarily useful for debugging circuits. The actual
533 /// implementation depends on the backend prover system.
534 ///
535 /// # Arguments
536 /// * `message` - The variable value to print
537 fn println(&mut self, message: &impl Variable) {
538 self.append_operation(OpCode::Println, vec![message.ty()], vec![]);
539 }
540}
541
542fn get_variable_type_2n(
543 x1: &impl Variable,
544 x2: &impl Variable,
545 xn: &[&dyn Variable],
546) -> Vec<VariableType> {
547 let mut types = Vec::with_capacity(2 + xn.len());
548 types.push(x1.ty());
549 types.push(x2.ty());
550 for x in xn {
551 types.push(x.ty());
552 }
553 types
554}