1/*
 2Each level in the SMTVerifier has a state.
 3
 4This is the state machine.
 5
 6The signals are
 7
 8levIns: 1 if we are in the level where the insertion should happen
 9xor: 1 if the bitKey of the old and new keys are different in this level
10is0: Input that indicates that the oldKey is 0
11fnc:  0 -> VERIFY INCLUSION
12      1 -> VERIFY NOT INCLUSION
13
14err state is not a state itself. It's a lack of state.
15
16The end of the last level will have to be `na`
17
18   levIns=0                                                                                any
19     ┌────┐                                                                              ┌────┐
20     │    │                                                                              │    │
21     │    ▼                          levIns=1                                            ▼    │
22     │    ###########                is0=1      ###########                    ###########    │
23     │   #           #               fnc=1     #           #       any        #           #   │
24     └──#    top      # ─────────────────────▶#     i0      #───────────────▶#    na       #──┘
25         ##         ## ──────────┐             ##         ##         ┌───────▶##         ##
26           ########─────────────┐│               #########           │┌────────▶#########
27                                ││ levIns=1                          ││
28                                ││ is0=0        ###########          ││
29                                ││ fnc=1       #           #       any│
30                                │└──────────▶ #    iold     #────────┘│
31                                │              ##         ##          │
32                                │                #########            │
33                                │                                     │
34                                │  levIns=1     ###########           │
35                                │  fnc=0       #           #        any
36                                └────────────▶#    inew     #─────────┘
37                                               ##         ##
38                                                 #########
39
40 */
41
42
43template SMTVerifierSM() {
44    signal input is0;
45    signal input levIns;
46    signal input fnc;
47
48    signal input prev_top;
49    signal input prev_i0;
50    signal input prev_iold;
51    signal input prev_inew;
52    signal input prev_na;
53
54    signal output st_top;
55    signal output st_i0;
56    signal output st_iold;
57    signal output st_inew;
58    signal output st_na;
59
60    signal prev_top_lev_ins;
61    signal prev_top_lev_ins_fnc;
62
63    prev_top_lev_ins <== prev_top * levIns;
64    prev_top_lev_ins_fnc <== prev_top_lev_ins*fnc;  // prev_top * levIns * fnc
65
66    // st_top = prev_top * (1-levIns)
67    //    = + prev_top
68    //      - prev_top * levIns
69    st_top <== prev_top - prev_top_lev_ins;
70
71    // st_inew = prev_top * levIns * (1-fnc)
72    //   = + prev_top * levIns
73    //     - prev_top * levIns * fnc
74    st_inew <== prev_top_lev_ins - prev_top_lev_ins_fnc;
75
76    // st_iold = prev_top * levIns * (1-is0)*fnc
77    //   = + prev_top * levIns * fnc
78    //     - prev_top * levIns * fnc * is0
79    st_iold <== prev_top_lev_ins_fnc * (1 - is0);
80
81    // st_i0 = prev_top * levIns * is0
82    //  = + prev_top * levIns * is0
83    st_i0 <== prev_top_lev_ins * is0;
84
85    st_na <== prev_na + prev_inew + prev_iold + prev_i0;
86}