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                         levIns=1              #           #
 37  levIns=0                is0=1 ┌────────────▶#    old0     #────────┐                 any
 38  ┌─────┐                       │              ##         ##         │               ┌──────┐
 39  │     │                       │                #########           │ any           │      │
 40  │     ▼                       │                                    │               ▼      │
 41  │    ###########              │                                    │          ########### │
 42  │   #           # ────────────┘                                    └────────▶#           #│
 43  └──#    top      #                                                          #    na       #
 44      ##         ## ────┐                                                  ┌──▶##         ##
 45        #########       │                                                  │     #########
 46                        │                                                  │
 47                        │      ###########                  ###########    │ any
 48           levIns=1     │     #           #      xor=1     #           #   │
 49            is0=0       └───▶#   old1      #─────────────▶#    new1     #──┘
 50                              ##         ##                ##         ##
 51                                #########│                   #########
 52                                         │                       ▲
 53                                         └───┐             ┌─────┘
 54                                     xor=0   │  ###########│  xor=1
 55                                             │ #           #
 56                                             ▼#    btn      #
 57                                               ##         ##
 58                                                 #########◀───────┐
 59                                                     │            │
 60                                                     │            │
 61                                                     └────────────┘
 62                                                         xor=0
 63
 64***************************************************************************************************/
 65
 66template SMTInsertSM() {
 67  signal input xor;
 68  signal input is0;
 69  signal input levIns;
 70  signal input fnc[0];
 71  signal input fnc[1];
 72
 73  signal input prev_top;
 74  signal input prev_old0;
 75  signal input prev_old1;
 76  signal input prev_bot;
 77  signal input prev_new1;
 78  signal input prev_na;
 79  signal input prev_upd;
 80
 81  signal output st_top;
 82  signal output st_old0;
 83  signal output st_old1;
 84  signal output st_bot;
 85  signal output st_new1;
 86  signal output st_na;
 87  signal output st_upd;
 88
 89  signal aux1;
 90  signal aux2;
 91
 92  aux1 <== prev_top * levIns;
 93  aux2 <== aux1*is0;
 94  st_top <==  prev_top - aux1            // prev_top * (1-levIns) =
 95                                         //  = prev_top - aux1;
 96  st_old0 <== aux2 * fnc[0];                       // (prev_top * levIns * is0)*fnc[0] = aux2
 97  st_old1 <== (aux1 - aux2)*fnc[0];                // (prev_top * levIns * (1-is0))*fnc[0] =
 98                                                   //   = (aux1 * (1-is0))*fnc[0] =
 99                                                   //   = (aux1 - aux2) * fnc[0]
100  st_new1 <== (prev_old1 + prev_bot)*xor     // prev_old1*xor + prev_bot*xor =
101                                             //   = (prev_old1 + prev_bot)*xor;
102  st_bot <== -st_new1 + prev_old1 + prev_bot // prev_old1*(1-xor) + prev_bot*(1-xor) =
103                                             //  = - prev_old1*xor -prev_bot*xor + prev_old1 + prev_bot =
104                                             //  = -st_new1 + prev_old1 + prev_bot
105  st_na <== prev_new1 + prev_old0 + prev_na + st_upd;
106  st_upd <== aux1*(1-fnc[0]);                // prev_top*levIns*(1-fnc[0]) =
107                                             //   = aux1 * (1-fnc[0])
108
109}