1
 2
 3/******
 4
 5SMTInsertLevel
 6
 7This circuit has 2 has
 8
 9Outputs according to the state.
10
11State        oldRoot                    newRoot
12=====        =======                    =======
13top          H'(oldChild, sibling)       H'(newChild, sibling)
14old1         old1leaf                    H'(newChild, 0)
15old0         0                           new1leaf
16bot          0                           H'(newChild, 0)
17new1         0                           H'(new1leaf, old1leaf)
18na           0                           0
19
20upd          old1leaf                    new1leaf
21
22H' is the Hash function with the inputs shifted acordingly.
23
24*****/
25
26
27template SMTInsertLevel() {
28    signal input st_top;
29    signal input st_old1;
30    signal input st_old0;
31    signal input st_bot;
32    signal input st_new1;
33    signal input st_na;
34    signal input st_upd;
35
36    signal output oldRoot;
37    signal output newRoot;
38    signal input sibling;
39    signal input old1leaf;
40    signal input new1leaf;
41    signal input newlrbit;
42    signal input oldChild;
43    signal input newChild;
44
45    signal aux[4];
46
47    component oldProofHash = SMTHash2();
48    component newProofHash = SMTHash2();
49
50    component oldSwitcher = Switcher();
51    component newSwitcher = Switcher();
52
53    // Old side
54
55    oldSwitcher.L <== oldChild;
56    oldSwitcher.R <== sibling;
57
58    oldSwitcher.sel <== newlrbit;
59    oldProofHash.L <== oldSwitcher.outL;
60    oldProofHash.R <== oldSwitcher.outR;
61
62    aux[0] <== old1leaf * (st_old1 + st_upd);
63    oldRoot <== aux[0] +  oldProofHash.out * st_top;
64
65    // New side
66
67    aux[1] <== newChild * ( st_top + st_old1 + st_bot);
68    newSwitcher.L <== aux[1] + new1leaf*st_new1;
69
70    aux[2] <== sibling*st_top;
71    newSwitcher.R <== aux[2] + old1leaf*st_new1;
72
73    newSwitcher.sel <== newlrbit;
74    newProofHash.L <== newSwitcher.outL;
75    newProofHash.R <== newSwitcher.outR;
76
77    aux[3] <== newProofHash.out * (st_top + st_old1 + st_bot + st_new1);
78    newRoot <==  aux[3] + new1leaf * (st_old0 + st_upd);
79}