circomlib/circuits/smt/smtprocessor.circom
circuits/smt/smtprocessor.circomRaw
1/***************************************************************************************************
2
3SMTProcessor: Sparse Merkle Tree processor is a component to verify an insert/update/delete elements
4into the Sparse Merkle tree.
5
6
7Insert to an empty leaf
8=======================
9
10 STATE OLD STATE NEW STATE
11 ===== ========= =========
12
13 oldRoot newRoot
14 ▲ ▲
15 │ │
16 ┌───────┐ ┏━━━┻━━━┓ ┌───────┐ ┏━━━┻━━━┓
17 top │Sibling├────▶┃ Hash ┃◀─┐ │Sibling├────▶┃ Hash ┃◀─┐
18 └───────┘ ┗━━━━━━━┛ │ └───────┘ ┗━━━━━━━┛ │
19 │ │
20 │ │
21 ┏━━━┻━━━┓ ┌───────┐ ┏━━━┻━━━┓ ┌───────┐
22 top ┌─────▶┃ Hash ┃◀──┤Sibling│ ┌─────▶┃ Hash ┃◀──┤Sibling│
23 │ ┗━━━━━━━┛ └───────┘ │ ┗━━━━━━━┛ └───────┘
24 │ │
25 │ │
26 ┌───────┐ ┏━━━┻━━━┓ ┌───────┐ ┏━━━┻━━━┓
27 top │Sibling├──▶┃ Hash ┃◀─────┐ │Sibling├──▶┃ Hash ┃◀─────┐
28 └───────┘ ┗━━━━━━━┛ │ └───────┘ ┗━━━━━━━┛ │
29 │ │
30 │ │
31 ┌────┴────┐ ┌────┴────┐
32 old0 │ 0 │ │New1Leaf │
33 └─────────┘ └─────────┘
34
35
36 ┏━━━━━━━┓ ┏━━━━━━━┓
37 na ┃ Hash ┃ ┃ Hash ┃
38 ┗━━━━━━━┛ ┗━━━━━━━┛
39
40
41 ┏━━━━━━━┓ ┏━━━━━━━┓
42 na ┃ Hash ┃ ┃ Hash ┃
43 ┗━━━━━━━┛ ┗━━━━━━━┛
44
45
46
47Insert to a used leaf.
48=====================
49
50 STATE OLD STATE NEW STATE
51 ===== ========= =========
52
53
54 oldRoot newRoot
55 ▲ ▲
56 │ │
57 ┌───────┐ ┏━━━┻━━━┓ ┌───────┐ ┏━━━┻━━━┓
58 top │Sibling├────▶┃ Hash ┃◀─┐ │Sibling├────▶┃ Hash ┃◀─┐
59 └───────┘ ┗━━━━━━━┛ │ └───────┘ ┗━━━━━━━┛ │
60 │ │
61 │ │
62 ┏━━━┻━━━┓ ┌───────┐ ┏━━━┻━━━┓ ┌───────┐
63 top ┌─────▶┃ Hash ┃◀──┤Sibling│ ┌─────▶┃ Hash ┃◀──┤Sibling│
64 │ ┗━━━━━━━┛ └───────┘ │ ┗━━━━━━━┛ └───────┘
65 │ │
66 │ │
67 ┌───────┐ ┏━━━┻━━━┓ ┌───────┐ ┏━━━┻━━━┓
68 top │Sibling├──▶┃ Hash ┃◀─────┐ │Sibling├──▶┃ Hash ┃◀─────┐
69 └───────┘ ┗━━━━━━━┛ │ └───────┘ ┗━━━━━━━┛ │
70 │ │
71 │ │
72 ┌────┴────┐ ┏━━━┻━━━┓ ┌───────┐
73 bot │Old1Leaf │ ┌─────▶┃ Hash ┃◀──┼─ 0 │
74 └─────────┘ │ ┗━━━━━━━┛ └───────┘
75 │
76 │
77 ┏━━━━━━━┓ ┌───────┐ ┏━━━┻━━━┓
78 bot ┃ Hash ┃ │ 0 ─┼──▶┃ Hash ┃◀─────┐
79 ┗━━━━━━━┛ └───────┘ ┗━━━━━━━┛ │
80 │
81 │
82 ┏━━━━━━━┓ ┏━━━┻━━━┓ ┌───────┐
83 bot ┃ Hash ┃ ┌─────▶┃ Hash ┃◀──│ 0 │
84 ┗━━━━━━━┛ │ ┗━━━━━━━┛ └───────┘
85 │
86 │
87 ┏━━━━━━━┓ ┌─────────┐ ┏━━━┻━━━┓ ┌─────────┐
88 new1 ┃ Hash ┃ │Old1Leaf ├──▶┃ Hash ┃◀──│New1Leaf │
89 ┗━━━━━━━┛ └─────────┘ ┗━━━━━━━┛ └─────────┘
90
91
92 ┏━━━━━━━┓ ┏━━━━━━━┓
93 na ┃ Hash ┃ ┃ Hash ┃
94 ┗━━━━━━━┛ ┗━━━━━━━┛
95
96
97 ┏━━━━━━━┓ ┏━━━━━━━┓
98 na ┃ Hash ┃ ┃ Hash ┃
99 ┗━━━━━━━┛ ┗━━━━━━━┛
100
101
102Fnction
103fnc[0] fnc[1]
1040 0 NOP
1050 1 UPDATE
1061 0 INSERT
1071 1 DELETE
108
109
110***************************************************************************************************/
111
112include "../gates.circom";
113include "../bitify.circom";
114include "../comparators.circom";
115include "../switcher.circom";
116include "smtlevins.circom";
117include "smtprocessorlevel.circom";
118include "smtprocessorsm.circom";
119include "smthash.circom";
120
121template SMTProcessor(nLevels) {
122 signal input oldRoot;
123 signal input newRoot;
124 signal input siblings[nLevels];
125 signal input oldKey;
126 signal input oldValue;
127 signal input isOld0;
128 signal input newKey;
129 signal input newValue;
130 signal input fnc[2];
131
132 signal enabled;
133
134 enabled <== fnc[0] + fnc[1] - fnc[0]*fnc[1]
135
136 component hash1Old = SMTHash1();
137 hash1Old.key <== oldKey;
138 hash1Old.value <== oldValue;
139
140 component hash1New = SMTHash1();
141 hash1New.key <== newKey;
142 hash1New.value <== newValue;
143
144 component n2bOld = Num2Bits_strict();
145 component n2bNew = Num2Bits_strict();
146
147 n2bOld.in <== oldKey;
148 n2bNew.in <== newKey;
149
150 component smtLevIns = SMTLevIns(nLevels);
151 for (var i=0; i<nLevels; i++) smtLevIns.siblings[i] <== siblings[i];
152 smtLevIns.enabled <== enabled;
153
154 component xors[nLevels];
155 for (var i=0; i<nLevels; i++) {
156 xors[i] = XOR();
157 xors[i].a <== n2bOld.out[i];
158 xors[i].b <== n2bNew.out[i];
159 }
160
161 component sm[nLevels];
162 for (var i=0; i<nLevels; i++) {
163 sm[i] = SMTProcessorSM();
164 if (i==0) {
165 sm[i].prev_top <== enabled;
166 sm[i].prev_old0 <== 0;
167 sm[i].prev_bot <== 0;
168 sm[i].prev_new1 <== 0;
169 sm[i].prev_na <== 1-enabled;
170 sm[i].prev_upd <== 0;
171 } else {
172 sm[i].prev_top <== sm[i-1].st_top;
173 sm[i].prev_old0 <== sm[i-1].st_old0;
174 sm[i].prev_bot <== sm[i-1].st_bot;
175 sm[i].prev_new1 <== sm[i-1].st_new1;
176 sm[i].prev_na <== sm[i-1].st_na;
177 sm[i].prev_upd <== sm[i-1].st_upd;
178 }
179 sm[i].is0 <== isOld0;
180 sm[i].xor <== xors[i].out;
181 sm[i].fnc[0] <== fnc[0];
182 sm[i].fnc[1] <== fnc[1];
183 sm[i].levIns <== smtLevIns.levIns[i];
184 }
185 sm[nLevels-1].st_na === 1;
186
187 component levels[nLevels];
188 for (var i=nLevels-1; i != -1; i--) {
189 levels[i] = SMTProcessorLevel();
190
191 levels[i].st_top <== sm[i].st_top;
192 levels[i].st_old0 <== sm[i].st_old0;
193 levels[i].st_bot <== sm[i].st_bot;
194 levels[i].st_new1 <== sm[i].st_new1;
195 levels[i].st_na <== sm[i].st_na;
196 levels[i].st_upd <== sm[i].st_upd;
197
198 levels[i].sibling <== siblings[i];
199 levels[i].old1leaf <== hash1Old.out;
200 levels[i].new1leaf <== hash1New.out;
201
202 levels[i].newlrbit <== n2bNew.out[i];
203 if (i==nLevels-1) {
204 levels[i].oldChild <== 0;
205 levels[i].newChild <== 0;
206 } else {
207 levels[i].oldChild <== levels[i+1].oldRoot;
208 levels[i].newChild <== levels[i+1].newRoot;
209 }
210 }
211
212 component topSwitcher = Switcher();
213
214 topSwitcher.sel <== fnc[0]*fnc[1];
215 topSwitcher.L <== levels[0].oldRoot;
216 topSwitcher.R <== levels[0].newRoot;
217
218 topSwitcher.outL === oldRoot*enabled;
219 topSwitcher.outR === newRoot*enabled;
220
221 // Ckeck keys are equal if updating
222 component areKeyEquals = IsEqual();
223 areKeyEquals.in[0] <== oldKey;
224 areKeyEquals.in[1] <== newKey;
225
226 component keysOk = MultiAND(3);
227 keysOk.in[0] <== 1-fnc[0];
228 keysOk.in[1] <== fnc[1];
229 keysOk.in[2] <== 1-areKeyEquals.out;
230
231 keysOk.out === 0;
232}