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