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 sm[nLevels];
 50    for (var i=0; i<nLevels; i++) {
 51        sm[i] = SMTVerifierSM();
 52        if (i==0) {
 53            sm[i].prev_top <== 1;
 54            sm[i].prev_i0 <== 0;
 55            sm[i].prev_inew <== 0;
 56            sm[i].prev_iold <== 0;
 57            sm[i].prev_na <== 0;
 58        } else {
 59            sm[i].prev_top <== sm[i-1].st_top;
 60            sm[i].prev_i0 <== sm[i-1].st_i0;
 61            sm[i].prev_inew <== sm[i-1].st_inew;
 62            sm[i].prev_iold <== sm[i-1].st_iold;
 63            sm[i].prev_na <== sm[i-1].st_na;
 64        }
 65        sm[i].is0 <== isOld0;
 66        sm[i].fnc <== fnc;
 67        sm[i].levIns <== smtLevIns.levIns[i];
 68    }
 69    sm[nLevels-1].st_na === 1;
 70
 71    component levels[nLevels];
 72    for (var i=nLevels-1; i != -1; i--) {
 73        levels[i] = SMTVerifierLevel();
 74
 75        levels[i].st_top <== sm[i].st_top;
 76        levels[i].st_i0 <== sm[i].st_i0;
 77        levels[i].st_inew <== sm[i].st_inew;
 78        levels[i].st_iold <== sm[i].st_iold;
 79        levels[i].st_na <== sm[i].st_na;
 80
 81        levels[i].sibling <== siblings[i];
 82        levels[i].old1leaf <== hash1Old.out;
 83        levels[i].new1leaf <== hash1New.out;
 84
 85        levels[i].lrbit <== n2bNew.out[i];
 86        if (i==nLevels-1) {
 87            levels[i].child <== 0;
 88        } else {
 89            levels[i].child <== levels[i+1].root;
 90        }
 91    }
 92
 93
 94    // Check that if checking for non inclussuin and isOld0==0 then key!=old
 95    component areKeyEquals = IsEqual();
 96    areKeyEquals.in[0] <== oldKey;
 97    areKeyEquals.in[1] <== key;
 98
 99    component keysOk = MultiAND(3);
100    keysOk.in[0] <== fnc;
101    keysOk.in[1] <== 1-isOld0;
102    keysOk.in[2] <== areKeyEquals.out;
103
104    keysOk.out === 0;
105
106    // Check the roots
107    levels[0].root === root;
108
109}