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