circomlib/circuits/smt/smtinsertsm.circom
circuits/smt/smtinsertsm.circomRaw
1/***************************************************************************************************
2Each level on a SMTInsert 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 in an empty leaf and 0 if we are inserting
13in 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 and old1: When the we reach insert level, we go to old0 and old1 states
19according to `is0` signal.
20btn: Once in old1 we go to btn until xor=1
21new1: This level is reached when xor=1. Here is where we insert the hash of the
22old and the new trees with just one element.
23na: Not appliable. After inserting 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 # #
37 ┌────────────────────────────▶# upd #─────────────────────┐
38 │ ## ## │
39 │ ######### │
40 levIns=1 │ │
41 fnc[0]=0 │ │ any
42 │ │
43 │ │
44 │ │
45 │ ########### │
46 │ levIns=1 # # │
47 levIns=0 │ is0=1 ┌────────────▶# old0 #────────┐ │ any
48 ┌─────┐ │ fnc[0]=1│ ## ## │ │ ┌──────┐
49 │ │ │ │ ######### │ any │ │ │
50 │ ▼ │ │ │ ▼ ▼ │
51 │ ########### │ │ ########### │
52 │ # # ────────────┘ └────────▶# #│
53 └──# top # # na #
54 ## ## ────┐ ┌──▶## ##
55 ######### │ │ #########
56 │ │
57 │ ########### ########### │ any
58 levIns=1 │ # # xor=1 # # │
59 is0=0 └───▶# old1 #─────────────▶# new1 #──┘
60 fnc[0]=1 ## ## ## ##
61 #########│ #########
62 │ ▲
63 └───┐ ┌─────┘
64 xor=0 │ ###########│ xor=1
65 │ # #
66 ▼# btn #
67 ## ##
68 #########◀───────┐
69 │ │
70 │ │
71 └────────────┘
72 xor=0
73
74***************************************************************************************************/
75
76template SMTInsertSM() {
77 signal input xor;
78 signal input is0;
79 signal input levIns;
80 signal input fnc[2];
81
82 signal input prev_top;
83 signal input prev_old0;
84 signal input prev_old1;
85 signal input prev_bot;
86 signal input prev_new1;
87 signal input prev_na;
88 signal input prev_upd;
89
90 signal output st_top;
91 signal output st_old0;
92 signal output st_old1;
93 signal output st_bot;
94 signal output st_new1;
95 signal output st_na;
96 signal output st_upd;
97
98 signal aux1;
99 signal aux2;
100
101 aux1 <== prev_top * levIns;
102 aux2 <== aux1*is0;
103 st_top <== prev_top - aux1 // prev_top * (1-levIns) =
104 // = prev_top - aux1;
105 st_old0 <== aux2 * fnc[0]; // (prev_top * levIns * is0)*fnc[0] = aux2
106 st_old1 <== (aux1 - aux2)*fnc[0]; // (prev_top * levIns * (1-is0))*fnc[0] =
107 // = (aux1 * (1-is0))*fnc[0] =
108 // = (aux1 - aux2) * fnc[0]
109 st_new1 <== (prev_old1 + prev_bot)*xor // prev_old1*xor + prev_bot*xor =
110 // = (prev_old1 + prev_bot)*xor;
111 st_bot <== -st_new1 + prev_old1 + prev_bot // prev_old1*(1-xor) + prev_bot*(1-xor) =
112 // = - prev_old1*xor -prev_bot*xor + prev_old1 + prev_bot =
113 // = -st_new1 + prev_old1 + prev_bot
114 st_na <== prev_new1 + prev_old0 + prev_na + prev_upd;
115 st_upd <== aux1*(1-fnc[0]); // prev_top*levIns*(1-fnc[0]) =
116 // = aux1 * (1-fnc[0])
117
118}