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               ###########
19                          xor=1                 #           #
20                          fnc=1    ┌──────────▶#   err       #
21                                   │            ##         ##
22  levIns=0                         │              #########
23  xor=0 || fnc=0                   │                                                        any
24      ┌────┐                       │                                                      ┌────┐
25      │    │                       │                                                      │    │
26      │    ▼                       │  levIns=1                                            ▼    │
27      │    ###########             │  is0=1      ###########                    ###########    │
28      │   #           # ───────────┘  fnc=1     #           #       any        #           #   │
29      └──#    top      # ─────────────────────▶#     i0      #───────────────▶#    na       #──┘
30          ##         ## ──────────┐             ##         ##         ┌───────▶##         ##
31            ########─────────────┐│               #########           │┌────────▶#########
32                                 ││ levIns=1                          ││
33                                 ││ is0=0        ###########          ││
34                                 ││ fnc=1       #           #       any│
35                                 │└──────────▶ #    iold     #────────┘│
36                                 │              ##         ##          │
37                                 │                #########            │
38                                 │                                     │
39                                 │  levIns=1     ###########           │
40                                 │  fnc=0       #           #        any
41                                 └────────────▶#    inew     #─────────┘
42                                                ##         ##
43                                                  #########
44
45 */
46
47
48template SMTVerifierSM() {
49    signal input xor;
50    signal input is0;
51    signal input levIns;
52    signal input fnc;
53
54    signal input prev_top;
55    signal input prev_i0;
56    signal input prev_iold;
57    signal input prev_inew;
58    signal input prev_na;
59
60    signal output st_top;
61    signal output st_i0;
62    signal output st_iold;
63    signal output st_inew;
64    signal output st_na;
65
66    signal prev_top_lev_ins;
67    signal prev_top_lev_ins_fnc;
68    signal xor_fnc;
69
70    prev_top_lev_ins <== prev_top * levIns;
71    prev_top_lev_ins_fnc <== prev_top_lev_ins*fnc;  // prev_top * levIns * fnc
72    xor_fnc <== xor*fnc;
73
74
75    // st_top = prev_top * (1-levIns) * (1 - xor*fnc)
76    //    = + prev_top
77    //      - prev_top * levIns
78    //      - prev_top *          xor * fnc
79    //      + prev_top * levIns * xor * fnc
80    st_top <== (prev_top - prev_top_lev_ins)*(1-xor_fnc);
81
82    // st_inew = prev_top * levIns * (1-fnc)
83    //   = + prev_top * levIns
84    //     - prev_top * levIns * fnc
85    st_inew <== prev_top_lev_ins - prev_top_lev_ins_fnc;
86
87    // st_iold = prev_top * levIns * (1-is0)*fnc
88    //   = + prev_top * levIns * fnc
89    //     - prev_top * levIns * fnc * is0
90    st_iold <== prev_top_lev_ins_fnc * (1 - is0);
91
92    // st_i0 = prev_top * levIns * is0
93    //  = + prev_top * levIns * is0
94    st_i0 <== prev_top_lev_ins * is0;
95
96    st_na <== prev_na + prev_inew + prev_iold + prev_i0;
97}