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 in the SMTVerifier has a state.
 22
 23This is the state machine.
 24
 25The signals are
 26
 27levIns: 1 if we are in the level where the insertion should happen
 28xor: 1 if the bitKey of the old and new keys are different in this level
 29is0: Input that indicates that the oldKey is 0
 30fnc:  0 -> VERIFY INCLUSION
 31      1 -> VERIFY NOT INCLUSION
 32
 33err state is not a state itself. It's a lack of state.
 34
 35The end of the last level will have to be `na`
 36
 37   levIns=0                                                                                any
 38     ┌────┐                                                                              ┌────┐
 39     │    │                                                                              │    │
 40     │    ▼                          levIns=1                                            ▼    │
 41     │    ###########                is0=1      ###########                    ###########    │
 42     │   #           #               fnc=1     #           #       any        #           #   │
 43     └──#    top      # ─────────────────────▶#     i0      #───────────────▶#    na       #──┘
 44         ##         ## ──────────┐             ##         ##         ┌───────▶##         ##
 45           ########─────────────┐│               #########           │┌────────▶#########
 46                                ││ levIns=1                          ││
 47                                ││ is0=0        ###########          ││
 48                                ││ fnc=1       #           #       any│
 49                                │└──────────▶ #    iold     #────────┘│
 50                                │              ##         ##          │
 51                                │                #########            │
 52                                │                                     │
 53                                │  levIns=1     ###########           │
 54                                │  fnc=0       #           #        any
 55                                └────────────▶#    inew     #─────────┘
 56                                               ##         ##
 57                                                 #########
 58
 59 */
 60
 61
 62template SMTVerifierSM() {
 63    signal input is0;
 64    signal input levIns;
 65    signal input fnc;
 66
 67    signal input prev_top;
 68    signal input prev_i0;
 69    signal input prev_iold;
 70    signal input prev_inew;
 71    signal input prev_na;
 72
 73    signal output st_top;
 74    signal output st_i0;
 75    signal output st_iold;
 76    signal output st_inew;
 77    signal output st_na;
 78
 79    signal prev_top_lev_ins;
 80    signal prev_top_lev_ins_fnc;
 81
 82    prev_top_lev_ins <== prev_top * levIns;
 83    prev_top_lev_ins_fnc <== prev_top_lev_ins*fnc;  // prev_top * levIns * fnc
 84
 85    // st_top = prev_top * (1-levIns)
 86    //    = + prev_top
 87    //      - prev_top * levIns
 88    st_top <== prev_top - prev_top_lev_ins;
 89
 90    // st_inew = prev_top * levIns * (1-fnc)
 91    //   = + prev_top * levIns
 92    //     - prev_top * levIns * fnc
 93    st_inew <== prev_top_lev_ins - prev_top_lev_ins_fnc;
 94
 95    // st_iold = prev_top * levIns * (1-is0)*fnc
 96    //   = + prev_top * levIns * fnc
 97    //     - prev_top * levIns * fnc * is0
 98    st_iold <== prev_top_lev_ins_fnc * (1 - is0);
 99
100    // st_i0 = prev_top * levIns * is0
101    //  = + prev_top * levIns * is0
102    st_i0 <== prev_top_lev_ins * is0;
103
104    st_na <== prev_na + prev_inew + prev_iold + prev_i0;
105}