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***************************************************************************************************/
 93pragma circom 2.0.0;
 94
 95template SMTProcessorSM() {
 96  signal input xor;
 97  signal input is0;
 98  signal input levIns;
 99  signal input fnc[2];
100
101  signal input prev_top;
102  signal input prev_old0;
103  signal input prev_bot;
104  signal input prev_new1;
105  signal input prev_na;
106  signal input prev_upd;
107
108  signal output st_top;
109  signal output st_old0;
110  signal output st_bot;
111  signal output st_new1;
112  signal output st_na;
113  signal output st_upd;
114
115  signal aux1;
116  signal aux2;
117
118  aux1 <==                  prev_top * levIns;
119  aux2 <== aux1*fnc[0];  // prev_top * levIns * fnc[0]
120
121  // st_top = prev_top*(1-levIns)
122  //    = + prev_top
123  //      - prev_top * levIns            = aux1
124
125  st_top <== prev_top - aux1;
126
127  // st_old0 = prev_top * levIns * is0 * fnc[0]
128  //      = + prev_top * levIns * is0 * fnc[0]            = aux2 * is0
129
130  st_old0 <== aux2 * is0;  // prev_top * levIns * is0 * fnc[0]
131
132  // st_new1 = prev_top * levIns * (1-is0)*fnc[0] * xor   +  prev_bot*xor =
133  //    = + prev_top * levIns *       fnc[0] * xor     = aux2     * xor
134  //      - prev_top * levIns * is0 * fnc[0] * xor     = st_old0  * xor
135  //      + prev_bot *                         xor     = prev_bot * xor
136
137  st_new1 <== (aux2 - st_old0 + prev_bot)*xor;
138
139
140  // st_bot = prev_top * levIns * (1-is0)*fnc[0] * (1-xor) + prev_bot*(1-xor);
141  //    = + prev_top * levIns *       fnc[0]
142  //      - prev_top * levIns * is0 * fnc[0]
143  //      - prev_top * levIns *       fnc[0] * xor
144  //      + prev_top * levIns * is0 * fnc[0] * xor
145  //      + prev_bot
146  //      - prev_bot *                         xor
147
148  st_bot <== (1-xor) * (aux2 - st_old0 + prev_bot);
149
150
151  // st_upd = prev_top * (1-fnc[0]) *levIns;
152  //    = + prev_top * levIns
153  //      - prev_top * levIns * fnc[0]
154
155  st_upd <== aux1 - aux2;
156
157  // st_na = prev_new1 + prev_old0 + prev_na + prev_upd;
158  //    = + prev_new1
159  //      + prev_old0
160  //      + prev_na
161  //      + prev_upd
162
163  st_na <== prev_new1 + prev_old0 + prev_na + prev_upd;
164
165}