ark-r1cs-std/src/select.rs
src/select.rsRaw
1use crate::prelude::*;
2use ark_ff::Field;
3use ark_relations::r1cs::SynthesisError;
4use ark_std::vec::Vec;
5/// Generates constraints for selecting between one of two values.
6pub trait CondSelectGadget<ConstraintF: Field>
7where
8 Self: Sized,
9 Self: Clone,
10{
11 /// If `cond == &Boolean::TRUE`, then this returns `true_value`; else,
12 /// returns `false_value`.
13 ///
14 /// # Note
15 /// `Self::conditionally_select(cond, true_value, false_value)?` can be more
16 /// succinctly written as `cond.select(&true_value, &false_value)?`.
17 fn conditionally_select(
18 cond: &Boolean<ConstraintF>,
19 true_value: &Self,
20 false_value: &Self,
21 ) -> Result<Self, SynthesisError>;
22
23 /// Returns an element of `values` whose index in represented by `position`.
24 /// `position` is an array of boolean that represents an unsigned integer in big endian order.
25 ///
26 /// # Example
27 /// To get the 6th element of `values`, convert unsigned integer 6 (`0b110`) to `position = [True, True, False]`,
28 /// and call `conditionally_select_power_of_two_vector(position, values)`.
29 fn conditionally_select_power_of_two_vector(
30 position: &[Boolean<ConstraintF>],
31 values: &[Self],
32 ) -> Result<Self, SynthesisError> {
33 let m = values.len();
34 let n = position.len();
35
36 // Assert m is a power of 2, and n = log(m)
37 assert!(m.is_power_of_two());
38 assert_eq!(1 << n, m);
39
40 let mut cur_mux_values = values.to_vec();
41
42 // Traverse the evaluation tree from bottom to top in level order traversal.
43 // This is method 5.1 from https://github.com/mir-protocol/r1cs-workshop/blob/master/workshop.pdf
44 // TODO: Add method 5.2/5.3
45 for i in 0..n {
46 // Size of current layer.
47 let cur_size = 1 << (n - i);
48 assert_eq!(cur_mux_values.len(), cur_size);
49
50 let mut next_mux_values = Vec::new();
51 for j in (0..cur_size).step_by(2) {
52 let cur = Self::conditionally_select(
53 &position[n - 1 - i],
54 // true case
55 &cur_mux_values[j + 1],
56 // false case
57 &cur_mux_values[j],
58 )?;
59 next_mux_values.push(cur);
60 }
61 cur_mux_values = next_mux_values;
62 }
63
64 Ok(cur_mux_values[0].clone())
65 }
66}
67
68/// Performs a lookup in a 4-element table using two bits.
69pub trait TwoBitLookupGadget<ConstraintF: Field>
70where
71 Self: Sized,
72{
73 /// The type of values being looked up.
74 type TableConstant;
75
76 /// Interprets the slice `bits` as a two-bit integer `b = bits[0] + (bits[1]
77 /// << 1)`, and then outputs `constants[b]`.
78 ///
79 /// For example, if `bits == [0, 1]`, and `constants == [0, 1, 2, 3]`, this
80 /// method should output a variable corresponding to `2`.
81 ///
82 /// # Panics
83 ///
84 /// This method panics if `bits.len() != 2` or `constants.len() != 4`.
85 fn two_bit_lookup(
86 bits: &[Boolean<ConstraintF>],
87 constants: &[Self::TableConstant],
88 ) -> Result<Self, SynthesisError>;
89}
90
91/// Uses three bits to perform a lookup into a table, where the last bit
92/// conditionally negates the looked-up value.
93pub trait ThreeBitCondNegLookupGadget<ConstraintF: Field>
94where
95 Self: Sized,
96{
97 /// The type of values being looked up.
98 type TableConstant;
99
100 /// Interprets the slice `bits` as a two-bit integer `b = bits[0] + (bits[1]
101 /// << 1)`, and then outputs `constants[b] * c`, where `c = if bits[2] {
102 /// -1 } else { 1 };`.
103 ///
104 /// That is, `bits[2]` conditionally negates the looked-up value.
105 ///
106 /// For example, if `bits == [1, 0, 1]`, and `constants == [0, 1, 2, 3]`,
107 /// this method should output a variable corresponding to `-1`.
108 ///
109 /// # Panics
110 ///
111 /// This method panics if `bits.len() != 3` or `constants.len() != 4`.
112 fn three_bit_cond_neg_lookup(
113 bits: &[Boolean<ConstraintF>],
114 b0b1: &Boolean<ConstraintF>,
115 constants: &[Self::TableConstant],
116 ) -> Result<Self, SynthesisError>;
117}