circomlib/circuits/smt/smtprocessorsm.circom
circuits/smt/smtprocessorsm.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/***************************************************************************************************
21Each level on a SMTProcessor has a state.
22
23The state of the level depends on the state of te botom level and on `xor` and
24`is0` signals.
25
26`isOldLev` 1 when is the level where oldLeaf is.
27
28`xor` signal is 0 if the index bit at the current level is the same in the old
29and the new index, and 1 if it is different.
30
31`is0` signal, is 1 if we are inserting/deleting in an empty leaf and 0 if we
32are inserting/deleting in a leaf that contains an element.
33
34The states are:
35
36top: While the index bits of the old and new insex in the top level is the same, whe are in the top state.
37old0: When the we reach insert level, we go to old0 state
38if `is0`=1.
39btn: Once in insert level and `is0` =0 we go to btn or new1 level if xor=1
40new1: This level is reached when xor=1. Here is where we insert/delete the hash of the
41old and the new trees with just one element.
42na: Not appliable. After processing it, we go to the na level.
43
44
45Fnction
46fnc[0] fnc[1]
470 0 NOP
480 1 UPDATE
491 0 INSERT
501 1 DELETE
51
52
53 ###########
54 # #
55 ┌────────────────────────────▶# upd #─────────────────────┐
56 │ ## ## │
57 │ ######### │
58 levIns=1 │ │
59 fnc[0]=0 │ │ any
60 │ │
61 │ │
62 │ │
63 │ ########### │
64 │ levIns=1 # # │
65 levIns=0 │ is0=1 ┌────────────▶# old0 #────────┐ │ any
66 ┌─────┐ │ fnc[0]=1│ ## ## │ │ ┌──────┐
67 │ │ │ │ ######### │ any │ │ │
68 │ ▼ │ │ │ ▼ ▼ │
69 │ ########### │ │ ########### │
70 │ # # ────────────┘ └────────▶# #│
71 └──# top # # na #
72 ## ## ───────────────────┐ levIns=1 ┌──▶## ##
73 ######### │ is0=0 │ #########
74 │ │ fnc[0]=1 │
75 │ │ xor=1 ########### │ any
76 │ └──────────────────▶# # │
77 │ # new1 #──┘
78 │ ## ##
79 └────────────────────────────────┐ #########
80 levIns=1 │ ▲
81 is0=0 │ ┌─────┘
82 fnc[0]=1 │ ###########│ xor=1
83 xor=0 │ # #
84 ▼# btn #
85 ## ##
86 #########◀───────┐
87 │ │
88 │ │
89 └────────────┘
90 xor=0
91
92***************************************************************************************************/
93
94template SMTProcessorSM() {
95 signal input xor;
96 signal input is0;
97 signal input levIns;
98 signal input fnc[2];
99
100 signal input prev_top;
101 signal input prev_old0;
102 signal input prev_bot;
103 signal input prev_new1;
104 signal input prev_na;
105 signal input prev_upd;
106
107 signal output st_top;
108 signal output st_old0;
109 signal output st_bot;
110 signal output st_new1;
111 signal output st_na;
112 signal output st_upd;
113
114 signal aux1;
115 signal aux2;
116
117 aux1 <== prev_top * levIns;
118 aux2 <== aux1*fnc[0]; // prev_top * levIns * fnc[0]
119
120 // st_top = prev_top*(1-levIns)
121 // = + prev_top
122 // - prev_top * levIns = aux1
123
124 st_top <== prev_top - aux1;
125
126 // st_old0 = prev_top * levIns * is0 * fnc[0]
127 // = + prev_top * levIns * is0 * fnc[0] = aux2 * is0
128
129 st_old0 <== aux2 * is0; // prev_top * levIns * is0 * fnc[0]
130
131 // st_new1 = prev_top * levIns * (1-is0)*fnc[0] * xor + prev_bot*xor =
132 // = + prev_top * levIns * fnc[0] * xor = aux2 * xor
133 // - prev_top * levIns * is0 * fnc[0] * xor = st_old0 * xor
134 // + prev_bot * xor = prev_bot * xor
135
136 st_new1 <== (aux2 - st_old0 + prev_bot)*xor;
137
138
139 // st_bot = prev_top * levIns * (1-is0)*fnc[0] * (1-xor) + prev_bot*(1-xor);
140 // = + prev_top * levIns * fnc[0]
141 // - prev_top * levIns * is0 * fnc[0]
142 // - prev_top * levIns * fnc[0] * xor
143 // + prev_top * levIns * is0 * fnc[0] * xor
144 // + prev_bot
145 // - prev_bot * xor
146
147 st_bot <== (1-xor) * (aux2 - st_old0 + prev_bot)
148
149
150 // st_upd = prev_top * (1-fnc[0]) *levIns;
151 // = + prev_top * levIns
152 // - prev_top * levIns * fnc[0]
153
154 st_upd <== aux1 - aux2
155
156 // st_na = prev_new1 + prev_old0 + prev_na + prev_upd;
157 // = + prev_new1
158 // + prev_old0
159 // + prev_na
160 // + prev_upd
161
162 st_na <== prev_new1 + prev_old0 + prev_na + prev_upd;
163
164}