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 var i;
154
155 enabled <== fnc[0] + fnc[1] - fnc[0]*fnc[1]
156
157 component hash1Old = SMTHash1();
158 hash1Old.key <== oldKey;
159 hash1Old.value <== oldValue;
160
161 component hash1New = SMTHash1();
162 hash1New.key <== newKey;
163 hash1New.value <== newValue;
164
165 component n2bOld = Num2Bits_strict();
166 component n2bNew = Num2Bits_strict();
167
168 n2bOld.in <== oldKey;
169 n2bNew.in <== newKey;
170
171 component smtLevIns = SMTLevIns(nLevels);
172 for (i=0; i<nLevels; i++) smtLevIns.siblings[i] <== siblings[i];
173 smtLevIns.enabled <== enabled;
174
175 component xors[nLevels];
176 for (i=0; i<nLevels; i++) {
177 xors[i] = XOR();
178 xors[i].a <== n2bOld.out[i];
179 xors[i].b <== n2bNew.out[i];
180 }
181
182 component sm[nLevels];
183 for (i=0; i<nLevels; i++) {
184 sm[i] = SMTProcessorSM();
185 if (i==0) {
186 sm[i].prev_top <== enabled;
187 sm[i].prev_old0 <== 0;
188 sm[i].prev_bot <== 0;
189 sm[i].prev_new1 <== 0;
190 sm[i].prev_na <== 1-enabled;
191 sm[i].prev_upd <== 0;
192 } else {
193 sm[i].prev_top <== sm[i-1].st_top;
194 sm[i].prev_old0 <== sm[i-1].st_old0;
195 sm[i].prev_bot <== sm[i-1].st_bot;
196 sm[i].prev_new1 <== sm[i-1].st_new1;
197 sm[i].prev_na <== sm[i-1].st_na;
198 sm[i].prev_upd <== sm[i-1].st_upd;
199 }
200 sm[i].is0 <== isOld0;
201 sm[i].xor <== xors[i].out;
202 sm[i].fnc[0] <== fnc[0];
203 sm[i].fnc[1] <== fnc[1];
204 sm[i].levIns <== smtLevIns.levIns[i];
205 }
206 sm[nLevels-1].st_na + sm[nLevels-1].st_new1 + sm[nLevels-1].st_old0 +sm[nLevels-1].st_upd === 1;
207
208 component levels[nLevels];
209 for (i=nLevels-1; i != -1; i--) {
210 levels[i] = SMTProcessorLevel();
211
212 levels[i].st_top <== sm[i].st_top;
213 levels[i].st_old0 <== sm[i].st_old0;
214 levels[i].st_bot <== sm[i].st_bot;
215 levels[i].st_new1 <== sm[i].st_new1;
216 levels[i].st_na <== sm[i].st_na;
217 levels[i].st_upd <== sm[i].st_upd;
218
219 levels[i].sibling <== siblings[i];
220 levels[i].old1leaf <== hash1Old.out;
221 levels[i].new1leaf <== hash1New.out;
222
223 levels[i].newlrbit <== n2bNew.out[i];
224 if (i==nLevels-1) {
225 levels[i].oldChild <== 0;
226 levels[i].newChild <== 0;
227 } else {
228 levels[i].oldChild <== levels[i+1].oldRoot;
229 levels[i].newChild <== levels[i+1].newRoot;
230 }
231 }
232
233 component topSwitcher = Switcher();
234
235 topSwitcher.sel <== fnc[0]*fnc[1];
236 topSwitcher.L <== levels[0].oldRoot;
237 topSwitcher.R <== levels[0].newRoot;
238
239 component checkOldInput = ForceEqualIfEnabled();
240 checkOldInput.enabled <== enabled;
241 checkOldInput.in[0] <== oldRoot;
242 checkOldInput.in[1] <== topSwitcher.outL;
243
244 newRoot <== enabled * (topSwitcher.outR - oldRoot) + oldRoot;
245
246// topSwitcher.outL === oldRoot*enabled;
247// topSwitcher.outR === newRoot*enabled;
248
249 // Ckeck keys are equal if updating
250 component areKeyEquals = IsEqual();
251 areKeyEquals.in[0] <== oldKey;
252 areKeyEquals.in[1] <== newKey;
253
254 component keysOk = MultiAND(3);
255 keysOk.in[0] <== 1-fnc[0];
256 keysOk.in[1] <== fnc[1];
257 keysOk.in[2] <== 1-areKeyEquals.out;
258
259 keysOk.out === 0;
260}