1/*
  2
  3SMTVerifier is a component to verify inclusion/exclusion of an element in the tree
  4
  5
  6fnc:  0 -> VERIFY INCLUSION
  7      1 -> VERIFY NOT INCLUSION
  8
  9 */
 10
 11
 12include "../gates.circom";
 13include "../bitify.circom";
 14include "../comparators.circom";
 15include "../switcher.circom";
 16include "smtlevins.circom";
 17include "smtverifierlevel.circom";
 18include "smtverifiersm.circom";
 19include "smthash.circom";
 20
 21template SMTVerifier(nLevels) {
 22    signal input root;
 23    signal input siblings[nLevels];
 24    signal input oldKey;
 25    signal input oldValue;
 26    signal input isOld0;
 27    signal input key;
 28    signal input value;
 29    signal input fnc;
 30
 31    component hash1Old = SMTHash1();
 32    hash1Old.key <== oldKey;
 33    hash1Old.value <== oldValue;
 34
 35    component hash1New = SMTHash1();
 36    hash1New.key <== key;
 37    hash1New.value <== value;
 38
 39    component n2bOld = Num2Bits_strict();
 40    component n2bNew = Num2Bits_strict();
 41
 42    n2bOld.in <== oldKey;
 43    n2bNew.in <== key;
 44
 45    component smtLevIns = SMTLevIns(nLevels);
 46    for (var i=0; i<nLevels; i++) smtLevIns.siblings[i] <== siblings[i];
 47    smtLevIns.enabled <== 1;
 48
 49    component xors[nLevels];
 50    for (var i=0; i<nLevels; i++) {
 51        xors[i] = XOR();
 52        xors[i].a <== n2bOld.out[i];
 53        xors[i].b <== n2bNew.out[i];
 54    }
 55
 56    component sm[nLevels];
 57    for (var i=0; i<nLevels; i++) {
 58        sm[i] = SMTVerifierSM();
 59        if (i==0) {
 60            sm[i].prev_top <== 1;
 61            sm[i].prev_i0 <== 0;
 62            sm[i].prev_inew <== 0;
 63            sm[i].prev_iold <== 0;
 64            sm[i].prev_na <== 0;
 65        } else {
 66            sm[i].prev_top <== sm[i-1].st_top;
 67            sm[i].prev_i0 <== sm[i-1].st_i0;
 68            sm[i].prev_inew <== sm[i-1].st_inew;
 69            sm[i].prev_iold <== sm[i-1].st_iold;
 70            sm[i].prev_na <== sm[i-1].st_na;
 71        }
 72        sm[i].is0 <== isOld0;
 73        sm[i].xor <== xors[i].out;
 74        sm[i].fnc <== fnc;
 75        sm[i].levIns <== smtLevIns.levIns[i];
 76    }
 77//    sm[nLevels-1].st_na === 1;
 78
 79    component levels[nLevels];
 80    for (var i=nLevels-1; i != -1; i--) {
 81        levels[i] = SMTVerifierLevel();
 82
 83        levels[i].st_top <== sm[i].st_top;
 84        levels[i].st_i0 <== sm[i].st_i0;
 85        levels[i].st_inew <== sm[i].st_inew;
 86        levels[i].st_iold <== sm[i].st_iold;
 87        levels[i].st_na <== sm[i].st_na;
 88
 89        levels[i].sibling <== siblings[i];
 90        levels[i].old1leaf <== hash1Old.out;
 91        levels[i].new1leaf <== hash1New.out;
 92
 93        levels[i].lrbit <== n2bNew.out[i];
 94        if (i==nLevels-1) {
 95            levels[i].child <== 0;
 96        } else {
 97            levels[i].child <== levels[i+1].root;
 98        }
 99    }
100
101
102    // Check that if checking for non inclussuin and isOld0==0 then key!=old
103    component areKeyEquals = IsEqual();
104    areKeyEquals.in[0] <== oldKey;
105    areKeyEquals.in[1] <== key;
106
107    component keysOk = MultiAND(3);
108    keysOk.in[0] <== fnc;
109    keysOk.in[1] <== 1-isOld0;
110    keysOk.in[2] <== areKeyEquals.out;
111
112    keysOk.out === 0;
113
114    // Check the roots
115    levels[0].root === root;
116
117}