98 lines
4.2 KiB
Plaintext
98 lines
4.2 KiB
Plaintext
|
/*
|
||
|
|
Each level in the SMTVerifier has a state.
|
||
|
|
|
||
|
|
This is the state machine.
|
||
|
|
|
||
|
|
The signals are
|
||
|
|
|
||
|
|
levIns: 1 if we are in the level where the insertion should happen
|
||
|
|
xor: 1 if the bitKey of the old and new keys are different in this level
|
||
|
|
is0: Input that indicates that the oldKey is 0
|
||
|
|
fnc: 0 -> VERIFY INCLUSION
|
||
|
|
1 -> VERIFY NOT INCLUSION
|
||
|
|
|
||
|
|
err state is not a state itself. It's a lack of state.
|
||
|
|
|
||
|
|
The end of the last level will have to be `na`
|
||
|
|
|
||
|
|
levIns=0 ###########
|
||
|
|
xor=1 # #
|
||
|
|
fnc=1 ┌──────────▶# err #
|
||
|
|
│ ## ##
|
||
|
|
levIns=0 │ #########
|
||
|
|
xor=0 || fnc=0 │ any
|
||
|
|
┌────┐ │ ┌────┐
|
||
|
|
│ │ │ │ │
|
||
|
|
│ ▼ │ levIns=1 ▼ │
|
||
|
|
│ ########### │ is0=1 ########### ########### │
|
||
|
|
│ # # ───────────┘ fnc=1 # # any # # │
|
||
|
|
└──# top # ─────────────────────▶# i0 #───────────────▶# na #──┘
|
||
|
|
## ## ──────────┐ ## ## ┌───────▶## ##
|
||
|
|
########─────────────┐│ ######### │┌────────▶#########
|
||
|
|
││ levIns=1 ││
|
||
|
|
││ is0=0 ########### ││
|
||
|
|
││ fnc=1 # # any│
|
||
|
|
│└──────────▶ # iold #────────┘│
|
||
|
|
│ ## ## │
|
||
|
|
│ ######### │
|
||
|
|
│ │
|
||
|
|
│ levIns=1 ########### │
|
||
|
|
│ fnc=0 # # any
|
||
|
|
└────────────▶# inew #─────────┘
|
||
|
|
## ##
|
||
|
|
#########
|
||
|
|
|
||
|
|
*/
|
||
|
|
|
||
|
|
|
||
|
|
template SMTVerifierSM() {
|
||
|
|
signal input xor;
|
||
|
|
signal input is0;
|
||
|
|
signal input levIns;
|
||
|
|
signal input fnc;
|
||
|
|
|
||
|
|
signal input prev_top;
|
||
|
|
signal input prev_i0;
|
||
|
|
signal input prev_iold;
|
||
|
|
signal input prev_inew;
|
||
|
|
signal input prev_na;
|
||
|
|
|
||
|
|
signal output st_top;
|
||
|
|
signal output st_i0;
|
||
|
|
signal output st_iold;
|
||
|
|
signal output st_inew;
|
||
|
|
signal output st_na;
|
||
|
|
|
||
|
|
signal prev_top_lev_ins;
|
||
|
|
signal prev_top_lev_ins_fnc;
|
||
|
|
signal xor_fnc;
|
||
|
|
|
||
|
|
prev_top_lev_ins <== prev_top * levIns;
|
||
|
|
prev_top_lev_ins_fnc <== prev_top_lev_ins*fnc; // prev_top * levIns * fnc
|
||
|
|
xor_fnc <== xor*fnc;
|
||
|
|
|
||
|
|
|
||
|
|
// st_top = prev_top * (1-levIns) * (1 - xor*fnc)
|
||
|
|
// = + prev_top
|
||
|
|
// - prev_top * levIns
|
||
|
|
// - prev_top * xor * fnc
|
||
|
|
// + prev_top * levIns * xor * fnc
|
||
|
|
st_top <== (prev_top - prev_top_lev_ins)*(1-xor_fnc);
|
||
|
|
|
||
|
|
// st_inew = prev_top * levIns * (1-fnc)
|
||
|
|
// = + prev_top * levIns
|
||
|
|
// - prev_top * levIns * fnc
|
||
|
|
st_inew <== prev_top_lev_ins - prev_top_lev_ins_fnc;
|
||
|
|
|
||
|
|
// st_iold = prev_top * levIns * (1-is0)*fnc
|
||
|
|
// = + prev_top * levIns * fnc
|
||
|
|
// - prev_top * levIns * fnc * is0
|
||
|
|
st_iold <== prev_top_lev_ins_fnc * (1 - is0);
|
||
|
|
|
||
|
|
// st_i0 = prev_top * levIns * is0
|
||
|
|
// = + prev_top * levIns * is0
|
||
|
|
st_i0 <== prev_top_lev_ins * is0;
|
||
|
|
|
||
|
|
st_na <== prev_na + prev_inew + prev_iold + prev_i0;
|
||
|
|
}
|