1/*
 2
 3This component finds the level where the oldInsert is done.
 4The rules are:
 5
 6levIns[i] == 1 if its level and all the child levels have a sibling of 0 and
 7the parent level has a sibling != 0.  Considere that the root level always has
 8a parent with a sibling != 0.
 9
10
11                                  ┌──────────────┐
12                                  │              │
13                                  │              │───▶ levIns[0] <== (1-done[i])
14                                  │              │
15                                  └──────────────┘
16                                          ▲
17                                          │
18                                          │
19                                       done[0]
20
21
22
23                                      done[i-1] <== levIns[i] + done[i]
24                                          ▲
25                                          │
26                                          │
27                   ┌───────────┐  ┌──────────────┐
28                   │           │  │              │
29   sibling[i-1]───▶│IsZero[i-1]│─▶│              │───▶ levIns[i] <== (1-done[i])*(1-isZero[i-1].out)
30                   │           │  │              │
31                   └───────────┘  └──────────────┘
32                                          ▲
33                                          │
34                                          │
35                                       done[i]
36
37
38
39                                     done[n-2] <== levIns[n-1]
40                                         ▲
41                                         │
42                                         │
43                  ┌───────────┐  ┌──────────────┐
44                  │           │  │              │
45  sibling[n-2]───▶│IsZero[n-2]│─▶│              │────▶ levIns[n-1] <== (1-isZero[n-2].out)
46                  │           │  │              │
47                  └───────────┘  └──────────────┘
48
49                  ┌───────────┐
50                  │           │
51  sibling[n-1]───▶│IsZero[n-1]│────▶ === 0
52                  │           │
53                  └───────────┘
54
55 */
56
57template SMTLevIns(nLevels) {
58    signal input siblins[nLevels];
59    signal output levIns[nLevels];
60    signal done[nLevels-1];        // Indicates if the insLevel has aready been detecetd.
61
62    component isZero[nLevels];
63
64    for (var i=0; i<nLevels; i++) {
65        isZero[i] = IsZero();
66        isZero[i].in <== siblings[i];
67    }
68
69    // The last level must always have a sibling of 0. If not, then it cannot be inserted.
70    isZero[nLevels-2].out === 1;
71
72    levIns[nLevels-1] <== (1-isZero[nLevels-2].out);
73    done[nLevels-2] <== levIns[nLevels-1];
74    for (var i=nLevels-2; i>0; i--) {
75        levIns[i] <== (1-done[i])*(1-isZero[i-1].out)
76        done[i-1] <== levIns[i] + done[i];
77    }
78
79    levIns[0] <== (1-done[0]);
80}