circomlib/circuits/smt/smtprocessor.circom
circuits/smt/smtprocessor.circomRaw
1/*
2 Copyright 2018 0KIMS association.
3
4 This file is part of circom (Zero Knowledge Circuit Compiler).
5
6 circom is a free software: you can redistribute it and/or modify it
7 under the terms of the GNU General Public License as published by
8 the Free Software Foundation, either version 3 of the License, or
9 (at your option) any later version.
10
11 circom is distributed in the hope that it will be useful, but WITHOUT
12 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13 or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14 License for more details.
15
16 You should have received a copy of the GNU General Public License
17 along with circom. If not, see <https://www.gnu.org/licenses/>.
18*/
19
20/***************************************************************************************************
21
22SMTProcessor: Sparse Merkle Tree processor is a component to verify an insert/update/delete elements
23into the Sparse Merkle tree.
24
25
26Insert to an empty leaf
27=======================
28
29 STATE OLD STATE NEW STATE
30 ===== ========= =========
31
32 oldRoot newRoot
33 ▲ ▲
34 │ │
35 ┌───────┐ ┏━━━┻━━━┓ ┌───────┐ ┏━━━┻━━━┓
36 top │Sibling├────▶┃ Hash ┃◀─┐ │Sibling├────▶┃ Hash ┃◀─┐
37 └───────┘ ┗━━━━━━━┛ │ └───────┘ ┗━━━━━━━┛ │
38 │ │
39 │ │
40 ┏━━━┻━━━┓ ┌───────┐ ┏━━━┻━━━┓ ┌───────┐
41 top ┌─────▶┃ Hash ┃◀──┤Sibling│ ┌─────▶┃ Hash ┃◀──┤Sibling│
42 │ ┗━━━━━━━┛ └───────┘ │ ┗━━━━━━━┛ └───────┘
43 │ │
44 │ │
45 ┌───────┐ ┏━━━┻━━━┓ ┌───────┐ ┏━━━┻━━━┓
46 top │Sibling├──▶┃ Hash ┃◀─────┐ │Sibling├──▶┃ Hash ┃◀─────┐
47 └───────┘ ┗━━━━━━━┛ │ └───────┘ ┗━━━━━━━┛ │
48 │ │
49 │ │
50 ┌────┴────┐ ┌────┴────┐
51 old0 │ 0 │ │New1Leaf │
52 └─────────┘ └─────────┘
53
54
55 ┏━━━━━━━┓ ┏━━━━━━━┓
56 na ┃ Hash ┃ ┃ Hash ┃
57 ┗━━━━━━━┛ ┗━━━━━━━┛
58
59
60 ┏━━━━━━━┓ ┏━━━━━━━┓
61 na ┃ Hash ┃ ┃ Hash ┃
62 ┗━━━━━━━┛ ┗━━━━━━━┛
63
64
65
66Insert to a used leaf.
67=====================
68
69 STATE OLD STATE NEW STATE
70 ===== ========= =========
71
72
73 oldRoot newRoot
74 ▲ ▲
75 │ │
76 ┌───────┐ ┏━━━┻━━━┓ ┌───────┐ ┏━━━┻━━━┓
77 top │Sibling├────▶┃ Hash ┃◀─┐ │Sibling├────▶┃ Hash ┃◀─┐
78 └───────┘ ┗━━━━━━━┛ │ └───────┘ ┗━━━━━━━┛ │
79 │ │
80 │ │
81 ┏━━━┻━━━┓ ┌───────┐ ┏━━━┻━━━┓ ┌───────┐
82 top ┌─────▶┃ Hash ┃◀──┤Sibling│ ┌─────▶┃ Hash ┃◀──┤Sibling│
83 │ ┗━━━━━━━┛ └───────┘ │ ┗━━━━━━━┛ └───────┘
84 │ │
85 │ │
86 ┌───────┐ ┏━━━┻━━━┓ ┌───────┐ ┏━━━┻━━━┓
87 top │Sibling├──▶┃ Hash ┃◀─────┐ │Sibling├──▶┃ Hash ┃◀─────┐
88 └───────┘ ┗━━━━━━━┛ │ └───────┘ ┗━━━━━━━┛ │
89 │ │
90 │ │
91 ┌────┴────┐ ┏━━━┻━━━┓ ┌───────┐
92 bot │Old1Leaf │ ┌─────▶┃ Hash ┃◀──┼─ 0 │
93 └─────────┘ │ ┗━━━━━━━┛ └───────┘
94 │
95 │
96 ┏━━━━━━━┓ ┌───────┐ ┏━━━┻━━━┓
97 bot ┃ Hash ┃ │ 0 ─┼──▶┃ Hash ┃◀─────┐
98 ┗━━━━━━━┛ └───────┘ ┗━━━━━━━┛ │
99 │
100 │
101 ┏━━━━━━━┓ ┏━━━┻━━━┓ ┌───────┐
102 bot ┃ Hash ┃ ┌─────▶┃ Hash ┃◀──│ 0 │
103 ┗━━━━━━━┛ │ ┗━━━━━━━┛ └───────┘
104 │
105 │
106 ┏━━━━━━━┓ ┌─────────┐ ┏━━━┻━━━┓ ┌─────────┐
107 new1 ┃ Hash ┃ │Old1Leaf ├──▶┃ Hash ┃◀──│New1Leaf │
108 ┗━━━━━━━┛ └─────────┘ ┗━━━━━━━┛ └─────────┘
109
110
111 ┏━━━━━━━┓ ┏━━━━━━━┓
112 na ┃ Hash ┃ ┃ Hash ┃
113 ┗━━━━━━━┛ ┗━━━━━━━┛
114
115
116 ┏━━━━━━━┓ ┏━━━━━━━┓
117 na ┃ Hash ┃ ┃ Hash ┃
118 ┗━━━━━━━┛ ┗━━━━━━━┛
119
120
121Fnction
122fnc[0] fnc[1]
1230 0 NOP
1240 1 UPDATE
1251 0 INSERT
1261 1 DELETE
127
128
129***************************************************************************************************/
130
131include "../gates.circom";
132include "../bitify.circom";
133include "../comparators.circom";
134include "../switcher.circom";
135include "smtlevins.circom";
136include "smtprocessorlevel.circom";
137include "smtprocessorsm.circom";
138include "smthash_poseidon.circom";
139
140template SMTProcessor(nLevels) {
141 signal input oldRoot;
142 signal output newRoot;
143 signal input siblings[nLevels];
144 signal input oldKey;
145 signal input oldValue;
146 signal input isOld0;
147 signal input newKey;
148 signal input newValue;
149 signal input fnc[2];
150
151 signal enabled;
152
153 enabled <== fnc[0] + fnc[1] - fnc[0]*fnc[1]
154
155 component hash1Old = SMTHash1();
156 hash1Old.key <== oldKey;
157 hash1Old.value <== oldValue;
158
159 component hash1New = SMTHash1();
160 hash1New.key <== newKey;
161 hash1New.value <== newValue;
162
163 component n2bOld = Num2Bits_strict();
164 component n2bNew = Num2Bits_strict();
165
166 n2bOld.in <== oldKey;
167 n2bNew.in <== newKey;
168
169 component smtLevIns = SMTLevIns(nLevels);
170 for (var i=0; i<nLevels; i++) smtLevIns.siblings[i] <== siblings[i];
171 smtLevIns.enabled <== enabled;
172
173 component xors[nLevels];
174 for (var i=0; i<nLevels; i++) {
175 xors[i] = XOR();
176 xors[i].a <== n2bOld.out[i];
177 xors[i].b <== n2bNew.out[i];
178 }
179
180 component sm[nLevels];
181 for (var i=0; i<nLevels; i++) {
182 sm[i] = SMTProcessorSM();
183 if (i==0) {
184 sm[i].prev_top <== enabled;
185 sm[i].prev_old0 <== 0;
186 sm[i].prev_bot <== 0;
187 sm[i].prev_new1 <== 0;
188 sm[i].prev_na <== 1-enabled;
189 sm[i].prev_upd <== 0;
190 } else {
191 sm[i].prev_top <== sm[i-1].st_top;
192 sm[i].prev_old0 <== sm[i-1].st_old0;
193 sm[i].prev_bot <== sm[i-1].st_bot;
194 sm[i].prev_new1 <== sm[i-1].st_new1;
195 sm[i].prev_na <== sm[i-1].st_na;
196 sm[i].prev_upd <== sm[i-1].st_upd;
197 }
198 sm[i].is0 <== isOld0;
199 sm[i].xor <== xors[i].out;
200 sm[i].fnc[0] <== fnc[0];
201 sm[i].fnc[1] <== fnc[1];
202 sm[i].levIns <== smtLevIns.levIns[i];
203 }
204 sm[nLevels-1].st_na + sm[nLevels-1].st_new1 + sm[nLevels-1].st_old0 +sm[nLevels-1].st_upd === 1;
205
206 component levels[nLevels];
207 for (var i=nLevels-1; i != -1; i--) {
208 levels[i] = SMTProcessorLevel();
209
210 levels[i].st_top <== sm[i].st_top;
211 levels[i].st_old0 <== sm[i].st_old0;
212 levels[i].st_bot <== sm[i].st_bot;
213 levels[i].st_new1 <== sm[i].st_new1;
214 levels[i].st_na <== sm[i].st_na;
215 levels[i].st_upd <== sm[i].st_upd;
216
217 levels[i].sibling <== siblings[i];
218 levels[i].old1leaf <== hash1Old.out;
219 levels[i].new1leaf <== hash1New.out;
220
221 levels[i].newlrbit <== n2bNew.out[i];
222 if (i==nLevels-1) {
223 levels[i].oldChild <== 0;
224 levels[i].newChild <== 0;
225 } else {
226 levels[i].oldChild <== levels[i+1].oldRoot;
227 levels[i].newChild <== levels[i+1].newRoot;
228 }
229 }
230
231 component topSwitcher = Switcher();
232
233 topSwitcher.sel <== fnc[0]*fnc[1];
234 topSwitcher.L <== levels[0].oldRoot;
235 topSwitcher.R <== levels[0].newRoot;
236
237 component checkOldInput = ForceEqualIfEnabled();
238 checkOldInput.enabled <== enabled;
239 checkOldInput.in[0] <== oldRoot;
240 checkOldInput.in[1] <== topSwitcher.outL;
241
242 newRoot <== enabled * (topSwitcher.outR - oldRoot) + oldRoot;
243
244// topSwitcher.outL === oldRoot*enabled;
245// topSwitcher.outR === newRoot*enabled;
246
247 // Ckeck keys are equal if updating
248 component areKeyEquals = IsEqual();
249 areKeyEquals.in[0] <== oldKey;
250 areKeyEquals.in[1] <== newKey;
251
252 component keysOk = MultiAND(3);
253 keysOk.in[0] <== 1-fnc[0];
254 keysOk.in[1] <== fnc[1];
255 keysOk.in[2] <== 1-areKeyEquals.out;
256
257 keysOk.out === 0;
258}