Clearmatics Libsnark  0.1
C++ library for zkSNARK proofs
memory_checker_gadget.tcc
Go to the documentation of this file.
1 /** @file
2  *****************************************************************************
3 
4  Implementation of interfaces for memory_checker_gadget.
5 
6  See memory_checker_gadget.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 MEMORY_CHECKER_GADGET_TCC_
15 #define MEMORY_CHECKER_GADGET_TCC_
16 
17 namespace libsnark
18 {
19 
20 template<typename ramT>
21 memory_checker_gadget<ramT>::memory_checker_gadget(
22  ram_protoboard<ramT> &pb,
23  const size_t timestamp_size,
24  const memory_line_variable_gadget<ramT> &line1,
25  const memory_line_variable_gadget<ramT> &line2,
26  const std::string &annotation_prefix)
27  : ram_gadget_base<ramT>(pb, annotation_prefix), line1(line1), line2(line2)
28 {
29  /* compare the two timestamps */
30  timestamps_leq.allocate(
31  pb, FMT(this->annotation_prefix, " timestamps_leq"));
32  timestamps_less.allocate(
33  pb, FMT(this->annotation_prefix, " timestamps_less"));
34  compare_timestamps.reset(new comparison_gadget<FieldT>(
35  pb,
36  timestamp_size,
37  line1.timestamp->packed,
38  line2.timestamp->packed,
39  timestamps_less,
40  timestamps_leq,
41  FMT(this->annotation_prefix, " compare_ts")));
42 
43  /* compare the two addresses */
44  const size_t address_size = pb.ap.address_size();
45  addresses_eq.allocate(pb, FMT(this->annotation_prefix, " addresses_eq"));
46  addresses_leq.allocate(pb, FMT(this->annotation_prefix, " addresses_leq"));
47  addresses_less.allocate(
48  pb, FMT(this->annotation_prefix, " addresses_less"));
49  compare_addresses.reset(new comparison_gadget<FieldT>(
50  pb,
51  address_size,
52  line1.address->packed,
53  line2.address->packed,
54  addresses_less,
55  addresses_leq,
56  FMT(this->annotation_prefix, " compare_addresses")));
57 
58  /*
59  Add variables that will contain flags representing the following
60  relations:
61  - "line1.contents_after = line2.contents_before" (to check that contents
62  do not change between instructions);
63  - "line2.contents_before = 0" (for the first access at an address); and
64  - "line2.timestamp = 0" (for wrap-around checks to ensure only one 'cycle'
65  in the memory sort).
66 
67  More precisely, each of the above flags is "loose" (i.e., it equals 0 if
68  the relation holds, but can be either 0 or 1 if the relation does not
69  hold).
70  */
71  loose_contents_after1_equals_contents_before2.allocate(
72  pb,
73  FMT(this->annotation_prefix,
74  " loose_contents_after1_equals_contents_before2"));
75  loose_contents_before2_equals_zero.allocate(
76  pb,
77  FMT(this->annotation_prefix, " loose_contents_before2_equals_zero"));
78  loose_timestamp2_is_zero.allocate(
79  pb, FMT(this->annotation_prefix, " loose_timestamp2_is_zero"));
80 }
81 
82 template<typename ramT>
83 void memory_checker_gadget<ramT>::generate_r1cs_constraints()
84 {
85  /* compare the two timestamps */
86  compare_timestamps->generate_r1cs_constraints();
87 
88  /* compare the two addresses */
89  compare_addresses->generate_r1cs_constraints();
90  this->pb.add_r1cs_constraint(
91  r1cs_constraint<FieldT>(
92  addresses_leq, 1 - addresses_less, addresses_eq),
93  FMT(this->annotation_prefix, " addresses_eq"));
94 
95  /*
96  Add constraints for the following three flags:
97  - loose_contents_after1_equals_contents_before2;
98  - loose_contents_before2_equals_zero;
99  - loose_timestamp2_is_zero.
100  */
101  this->pb.add_r1cs_constraint(
102  r1cs_constraint<FieldT>(
103  loose_contents_after1_equals_contents_before2,
104  line1.contents_after->packed - line2.contents_before->packed,
105  0),
106  FMT(this->annotation_prefix,
107  " loose_contents_after1_equals_contents_before2"));
108  generate_boolean_r1cs_constraint<FieldT>(
109  this->pb,
110  loose_contents_after1_equals_contents_before2,
111  FMT(this->annotation_prefix,
112  " loose_contents_after1_equals_contents_before2"));
113 
114  this->pb.add_r1cs_constraint(
115  r1cs_constraint<FieldT>(
116  loose_contents_before2_equals_zero,
117  line2.contents_before->packed,
118  0),
119  FMT(this->annotation_prefix, " loose_contents_before2_equals_zero"));
120  generate_boolean_r1cs_constraint<FieldT>(
121  this->pb,
122  loose_contents_before2_equals_zero,
123  FMT(this->annotation_prefix, " loose_contents_before2_equals_zero"));
124 
125  this->pb.add_r1cs_constraint(
126  r1cs_constraint<FieldT>(
127  loose_timestamp2_is_zero, line2.timestamp->packed, 0),
128  FMT(this->annotation_prefix, " loose_timestamp2_is_zero"));
129  generate_boolean_r1cs_constraint<FieldT>(
130  this->pb,
131  loose_timestamp2_is_zero,
132  FMT(this->annotation_prefix, " loose_timestamp2_is_zero"));
133 
134  /*
135  The three cases that need to be checked are:
136 
137  line1.address = line2.address => line1.contents_after =
138  line2.contents_before (i.e. contents do not change between accesses to the
139  same address)
140 
141  line1.address < line2.address => line2.contents_before = 0
142  (i.e. access to new address has the "before" value set to 0)
143 
144  line1.address > line2.address => line2.timestamp = 0
145  (i.e. there is only one cycle with non-decreasing addresses, except
146  for the case where we go back to a unique pre-set timestamp; we choose
147  timestamp 0 to be the one that touches address 0)
148 
149  As usual, we implement "A => B" as "NOT (A AND (NOT B))".
150  */
151  this->pb.add_r1cs_constraint(
152  r1cs_constraint<FieldT>(
153  addresses_eq, 1 - loose_contents_after1_equals_contents_before2, 0),
154  FMT(this->annotation_prefix,
155  " memory_retains_contents_between_accesses"));
156  this->pb.add_r1cs_constraint(
157  r1cs_constraint<FieldT>(
158  addresses_less, 1 - loose_contents_before2_equals_zero, 0),
159  FMT(this->annotation_prefix, " new_address_starts_at_zero"));
160  this->pb.add_r1cs_constraint(
161  r1cs_constraint<FieldT>(
162  1 - addresses_leq, 1 - loose_timestamp2_is_zero, 0),
163  FMT(this->annotation_prefix, " only_one_cycle"));
164 }
165 
166 template<typename ramT>
167 void memory_checker_gadget<ramT>::generate_r1cs_witness()
168 {
169  /* compare the two addresses */
170  compare_addresses->generate_r1cs_witness();
171  this->pb.val(addresses_eq) = this->pb.val(addresses_leq) *
172  (FieldT::one() - this->pb.val(addresses_less));
173 
174  /* compare the two timestamps */
175  compare_timestamps->generate_r1cs_witness();
176 
177  /*
178  compare the values of:
179  - loose_contents_after1_equals_contents_before2;
180  - loose_contents_before2_equals_zero;
181  - loose_timestamp2_is_zero.
182  */
183  this->pb.val(loose_contents_after1_equals_contents_before2) =
184  (this->pb.val(line1.contents_after->packed) ==
185  this->pb.val(line2.contents_before->packed))
186  ? FieldT::one()
187  : FieldT::zero();
188  this->pb.val(loose_contents_before2_equals_zero) =
189  this->pb.val(line2.contents_before->packed).is_zero() ? FieldT::one()
190  : FieldT::zero();
191  this->pb.val(loose_timestamp2_is_zero) =
192  (this->pb.val(line2.timestamp->packed) == FieldT::zero()
193  ? FieldT::one()
194  : FieldT::zero());
195 }
196 
197 } // namespace libsnark
198 
199 #endif // MEMORY_CHECKER_GADGET_TCC_
Generated on Wed Jan 25 2023 11:05:58 for Clearmatics Libsnark by   doxygen 1.8.17