Clearmatics Libsnark  0.1
C++ library for zkSNARK proofs
tbcs_to_uscs.tcc
Go to the documentation of this file.
1 /** @file
2 *****************************************************************************
3 
4 Implementation of interfaces for a TBCS-to-USCS reduction.
5 
6 See tbcs_to_uscs.hpp .
7 
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 *****************************************************************************/
13 
14 #ifndef TBCS_TO_USCS_TCC_
15 #define TBCS_TO_USCS_TCC_
16 
17 #include <libff/algebra/fields/field_utils.hpp>
18 
19 namespace libsnark
20 {
21 
22 template<typename FieldT>
23 uscs_constraint_system<FieldT> tbcs_to_uscs_instance_map(
24  const tbcs_circuit &circuit)
25 {
26  assert(circuit.is_valid());
27  uscs_constraint_system<FieldT> result;
28 
29 #ifdef DEBUG
30  result.variable_annotations = circuit.variable_annotations;
31 #endif
32 
33  result.primary_input_size = circuit.primary_input_size;
34  result.auxiliary_input_size =
35  circuit.auxiliary_input_size + circuit.gates.size();
36 
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);
41 
42 #ifdef DEBUG
43  auto it = circuit.gate_annotations.find(g.output);
44  const std::string annotation =
45  (it != circuit.gate_annotations.end()
46  ? it->second
47  : FMT("", "compute_wire_%zu", g.output));
48 #else
49  const std::string annotation = "";
50 #endif
51 
52  switch (g.type) {
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);
57  break;
58  case TBCS_GATE_AND:
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);
62  break;
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);
67  break;
68  case TBCS_GATE_X:
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);
72  break;
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);
77  break;
78  case TBCS_GATE_Y:
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);
82  break;
83  case TBCS_GATE_XOR:
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);
87  break;
88  case TBCS_GATE_OR:
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);
92  break;
93  case TBCS_GATE_NOR:
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);
97  break;
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);
102  break;
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);
107  break;
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);
112  break;
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);
117  break;
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);
122  break;
123  case TBCS_GATE_NAND:
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);
127  break;
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);
132  break;
133  default:
134  assert(0);
135  }
136  }
137 
138  for (size_t i = 0;
139  i < circuit.primary_input_size + circuit.auxiliary_input_size +
140  circuit.gates.size();
141  ++i) {
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));
145  }
146 
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));
154  }
155  }
156 
157  return result;
158 }
159 
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)
165 {
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);
170  return result;
171 }
172 
173 } // namespace libsnark
174 
175 #endif // TBCS_TO_USCS_TCC_