2 *****************************************************************************
4 Implementation of interfaces for a TBCS-to-USCS reduction.
8 *****************************************************************************
9 * @author This file is part of libsnark, developed by SCIPR Lab
10 * and contributors (see AUTHORS).
11 * @copyright MIT license (see LICENSE file)
12 *****************************************************************************/
14 #ifndef TBCS_TO_USCS_TCC_
15 #define TBCS_TO_USCS_TCC_
17 #include <libff/algebra/fields/field_utils.hpp>
22 template<typename FieldT>
23 uscs_constraint_system<FieldT> tbcs_to_uscs_instance_map(
24 const tbcs_circuit &circuit)
26 assert(circuit.is_valid());
27 uscs_constraint_system<FieldT> result;
30 result.variable_annotations = circuit.variable_annotations;
33 result.primary_input_size = circuit.primary_input_size;
34 result.auxiliary_input_size =
35 circuit.auxiliary_input_size + circuit.gates.size();
37 for (auto &g : circuit.gates) {
38 const variable<FieldT> x(g.left_wire);
39 const variable<FieldT> y(g.right_wire);
40 const variable<FieldT> z(g.output);
43 auto it = circuit.gate_annotations.find(g.output);
44 const std::string annotation =
45 (it != circuit.gate_annotations.end()
47 : FMT("", "compute_wire_%zu", g.output));
49 const std::string annotation = "";
53 case TBCS_GATE_CONSTANT_0:
54 /* Truth table (00, 01, 10, 11): (0, 0, 0, 0)
55 0 * x + 0 * y + 1 * z + 1 \in {-1, 1} */
56 result.add_constraint(0 * x + 0 * y + 1 * z + 1, annotation);
59 /* Truth table (00, 01, 10, 11): (0, 0, 0, 1)
60 -2 * x + -2 * y + 4 * z + 1 \in {-1, 1} */
61 result.add_constraint(-2 * x + -2 * y + 4 * z + 1, annotation);
63 case TBCS_GATE_X_AND_NOT_Y:
64 /* Truth table (00, 01, 10, 11): (0, 0, 1, 0)
65 -2 * x + 2 * y + 4 * z + -1 \in {-1, 1} */
66 result.add_constraint(-2 * x + 2 * y + 4 * z + -1, annotation);
69 /* Truth table (00, 01, 10, 11): (0, 0, 1, 1)
70 -1 * x + 0 * y + 1 * z + 1 \in {-1, 1} */
71 result.add_constraint(-1 * x + 0 * y + 1 * z + 1, annotation);
73 case TBCS_GATE_NOT_X_AND_Y:
74 /* Truth table (00, 01, 10, 11): (0, 1, 0, 0)
75 2 * x + -2 * y + 4 * z + -1 \in {-1, 1} */
76 result.add_constraint(2 * x + -2 * y + 4 * z + -1, annotation);
79 /* Truth table (00, 01, 10, 11): (0, 1, 0, 1)
80 0 * x + 1 * y + 1 * z + -1 \in {-1, 1} */
81 result.add_constraint(0 * x + 1 * y + 1 * z + -1, annotation);
84 /* Truth table (00, 01, 10, 11): (0, 1, 1, 0)
85 1 * x + 1 * y + 1 * z + -1 \in {-1, 1} */
86 result.add_constraint(1 * x + 1 * y + 1 * z + -1, annotation);
89 /* Truth table (00, 01, 10, 11): (0, 1, 1, 1)
90 -2 * x + -2 * y + 4 * z + -1 \in {-1, 1} */
91 result.add_constraint(-2 * x + -2 * y + 4 * z + -1, annotation);
94 /* Truth table (00, 01, 10, 11): (1, 0, 0, 0)
95 2 * x + 2 * y + 4 * z + -3 \in {-1, 1} */
96 result.add_constraint(2 * x + 2 * y + 4 * z + -3, annotation);
98 case TBCS_GATE_EQUIVALENCE:
99 /* Truth table (00, 01, 10, 11): (1, 0, 0, 1)
100 1 * x + 1 * y + 1 * z + -2 \in {-1, 1} */
101 result.add_constraint(1 * x + 1 * y + 1 * z + -2, annotation);
103 case TBCS_GATE_NOT_Y:
104 /* Truth table (00, 01, 10, 11): (1, 0, 1, 0)
105 0 * x + -1 * y + 1 * z + 0 \in {-1, 1} */
106 result.add_constraint(0 * x + -1 * y + 1 * z + 0, annotation);
108 case TBCS_GATE_IF_Y_THEN_X:
109 /* Truth table (00, 01, 10, 11): (1, 0, 1, 1)
110 -2 * x + 2 * y + 4 * z + -3 \in {-1, 1} */
111 result.add_constraint(-2 * x + 2 * y + 4 * z + -3, annotation);
113 case TBCS_GATE_NOT_X:
114 /* Truth table (00, 01, 10, 11): (1, 1, 0, 0)
115 -1 * x + 0 * y + 1 * z + 0 \in {-1, 1} */
116 result.add_constraint(-1 * x + 0 * y + 1 * z + 0, annotation);
118 case TBCS_GATE_IF_X_THEN_Y:
119 /* Truth table (00, 01, 10, 11): (1, 1, 0, 1)
120 2 * x + -2 * y + 4 * z + -3 \in {-1, 1} */
121 result.add_constraint(2 * x + -2 * y + 4 * z + -3, annotation);
124 /* Truth table (00, 01, 10, 11): (1, 1, 1, 0)
125 2 * x + 2 * y + 4 * z + -5 \in {-1, 1} */
126 result.add_constraint(2 * x + 2 * y + 4 * z + -5, annotation);
128 case TBCS_GATE_CONSTANT_1:
129 /* Truth table (00, 01, 10, 11): (1, 1, 1, 1)
130 0 * x + 0 * y + 1 * z + 0 \in {-1, 1} */
131 result.add_constraint(0 * x + 0 * y + 1 * z + 0, annotation);
139 i < circuit.primary_input_size + circuit.auxiliary_input_size +
140 circuit.gates.size();
142 /* require that 2 * wire - 1 \in {-1,1}, that is wire \in {0,1} */
143 result.add_constraint(
144 2 * variable<FieldT>(i) - 1, FMT("", "wire_%zu", i));
147 for (auto &g : circuit.gates) {
148 if (g.is_circuit_output) {
149 /* require that output + 1 \in {-1,1}, this together with output
150 * binary (above) enforces output = 0 */
151 result.add_constraint(
152 variable<FieldT>(g.output) + 1,
153 FMT("", "output_%zu", g.output));
160 template<typename FieldT>
161 uscs_variable_assignment<FieldT> tbcs_to_uscs_witness_map(
162 const tbcs_circuit &circuit,
163 const tbcs_primary_input &primary_input,
164 const tbcs_auxiliary_input &auxiliary_input)
166 const tbcs_variable_assignment all_wires =
167 circuit.get_all_wires(primary_input, auxiliary_input);
168 const uscs_variable_assignment<FieldT> result =
169 libff::convert_bit_vector_to_field_element_vector<FieldT>(all_wires);
173 } // namespace libsnark
175 #endif // TBCS_TO_USCS_TCC_