|
@ -31,14 +31,13 @@ fnc[0] fnc[1] |
|
|
1 1 DELETE |
|
|
1 1 DELETE |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
########### |
|
|
########### |
|
|
# # |
|
|
# # |
|
|
┌────────────────────────────▶# upd #─────────────────────┐ |
|
|
┌────────────────────────────▶# upd #─────────────────────┐ |
|
|
│ ## ## │ |
|
|
│ ## ## │ |
|
|
│ ######### │ |
|
|
│ ######### │ |
|
|
levIns=1 │ │ |
|
|
levIns=1 │ │ |
|
|
fnc[0]=0 │ │ any |
|
|
|
|
|
|
|
|
fnc[0]=0 │ │ any |
|
|
│ │ |
|
|
│ │ |
|
|
│ │ |
|
|
│ │ |
|
|
│ │ |
|
|
│ │ |
|
@ -51,18 +50,18 @@ fnc[0] fnc[1] |
|
|
│ ########### │ │ ########### │ |
|
|
│ ########### │ │ ########### │ |
|
|
│ # # ────────────┘ └────────▶# #│ |
|
|
│ # # ────────────┘ └────────▶# #│ |
|
|
└──# top # # na # |
|
|
└──# top # # na # |
|
|
## ## ────┐ ┌──▶## ## |
|
|
|
|
|
######### │ │ ######### |
|
|
|
|
|
│ │ |
|
|
|
|
|
│ ########### ########### │ any |
|
|
|
|
|
levIns=1 │ # # xor=1 # # │ |
|
|
|
|
|
is0=0 └───▶# old1 #─────────────▶# new1 #──┘ |
|
|
|
|
|
fnc[0]=1 ## ## ## ## |
|
|
|
|
|
#########│ ######### |
|
|
|
|
|
│ ▲ |
|
|
|
|
|
└───┐ ┌─────┘ |
|
|
|
|
|
xor=0 │ ###########│ xor=1 |
|
|
|
|
|
│ # # |
|
|
|
|
|
|
|
|
## ## ───────────────────┐ levIns=1 ┌──▶## ## |
|
|
|
|
|
######### │ is0=0 │ ######### |
|
|
|
|
|
│ │ fnc[0]=1 │ |
|
|
|
|
|
│ │ xor=1 ########### │ any |
|
|
|
|
|
│ └──────────────────▶# # │ |
|
|
|
|
|
│ # new1 #──┘ |
|
|
|
|
|
│ ## ## |
|
|
|
|
|
└────────────────────────────────┐ ######### |
|
|
|
|
|
levIns=1 │ ▲ |
|
|
|
|
|
is0=0 │ ┌─────┘ |
|
|
|
|
|
fnc[0]=1 │ ###########│ xor=1 |
|
|
|
|
|
xor=0 │ # # |
|
|
▼# btn # |
|
|
▼# btn # |
|
|
## ## |
|
|
## ## |
|
|
#########◀───────┐ |
|
|
#########◀───────┐ |
|
@ -81,7 +80,6 @@ template SMTInsertSM() { |
|
|
|
|
|
|
|
|
signal input prev_top; |
|
|
signal input prev_top; |
|
|
signal input prev_old0; |
|
|
signal input prev_old0; |
|
|
signal input prev_old1; |
|
|
|
|
|
signal input prev_bot; |
|
|
signal input prev_bot; |
|
|
signal input prev_new1; |
|
|
signal input prev_new1; |
|
|
signal input prev_na; |
|
|
signal input prev_na; |
|
@ -89,7 +87,6 @@ template SMTInsertSM() { |
|
|
|
|
|
|
|
|
signal output st_top; |
|
|
signal output st_top; |
|
|
signal output st_old0; |
|
|
signal output st_old0; |
|
|
signal output st_old1; |
|
|
|
|
|
signal output st_bot; |
|
|
signal output st_bot; |
|
|
signal output st_new1; |
|
|
signal output st_new1; |
|
|
signal output st_na; |
|
|
signal output st_na; |
|
@ -98,21 +95,51 @@ template SMTInsertSM() { |
|
|
signal aux1; |
|
|
signal aux1; |
|
|
signal aux2; |
|
|
signal aux2; |
|
|
|
|
|
|
|
|
aux1 <== prev_top * levIns; |
|
|
|
|
|
aux2 <== aux1*is0; |
|
|
|
|
|
st_top <== prev_top - aux1 // prev_top * (1-levIns) = |
|
|
|
|
|
// = prev_top - aux1; |
|
|
|
|
|
st_old0 <== aux2 * fnc[0]; // (prev_top * levIns * is0)*fnc[0] = aux2 |
|
|
|
|
|
st_old1 <== (aux1 - aux2)*fnc[0]; // (prev_top * levIns * (1-is0))*fnc[0] = |
|
|
|
|
|
// = (aux1 * (1-is0))*fnc[0] = |
|
|
|
|
|
// = (aux1 - aux2) * fnc[0] |
|
|
|
|
|
st_new1 <== (prev_old1 + prev_bot)*xor // prev_old1*xor + prev_bot*xor = |
|
|
|
|
|
// = (prev_old1 + prev_bot)*xor; |
|
|
|
|
|
st_bot <== -st_new1 + prev_old1 + prev_bot // prev_old1*(1-xor) + prev_bot*(1-xor) = |
|
|
|
|
|
// = - prev_old1*xor -prev_bot*xor + prev_old1 + prev_bot = |
|
|
|
|
|
// = -st_new1 + prev_old1 + prev_bot |
|
|
|
|
|
|
|
|
aux1 <== prev_top * levIns; |
|
|
|
|
|
aux2 <== aux1*fnc[0]; // prev_top * levIns * fnc[0] |
|
|
|
|
|
|
|
|
|
|
|
// st_top = prev_top*(1-levIns) |
|
|
|
|
|
// = + prev_top |
|
|
|
|
|
// - prev_top * levIns = aux1 |
|
|
|
|
|
|
|
|
|
|
|
st_top <== prev_top - aux1; |
|
|
|
|
|
|
|
|
|
|
|
// st_old0 = prev_top * levIns * is0 * fnc[0] |
|
|
|
|
|
// = + prev_top * levIns * is0 * fnc[0] = aux2 * is0 |
|
|
|
|
|
|
|
|
|
|
|
st_old0 <== aux2 * is0; // prev_top * levIns * is0 * fnc[0] |
|
|
|
|
|
|
|
|
|
|
|
// st_new1 = prev_top * levIns * (1-is0)*fnc[0] * xor + prev_bot*xor = |
|
|
|
|
|
// = + prev_top * levIns * fnc[0] * xor = aux2 * xor |
|
|
|
|
|
// - prev_top * levIns * is0 * fnc[0] * xor = st_old0 * xor |
|
|
|
|
|
// + prev_bot * xor = prev_bot * xor |
|
|
|
|
|
|
|
|
|
|
|
st_new1 <== (aux2 - st_old0 + prev_bot)*xor; |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
// st_bot = prev_top * levIns * (1-is0)*fnc[0] * (1-xor) + prev_bot*(1-xor); |
|
|
|
|
|
// = + prev_top * levIns * fnc[0] |
|
|
|
|
|
// - prev_top * levIns * is0 * fnc[0] |
|
|
|
|
|
// - prev_top * levIns * fnc[0] * xor |
|
|
|
|
|
// + prev_top * levIns * is0 * fnc[0] * xor |
|
|
|
|
|
// + prev_bot |
|
|
|
|
|
// - prev_bot * xor |
|
|
|
|
|
|
|
|
|
|
|
st_bot <== (1-xor) * (aux2 - st_old0 + prev_bot) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
// st_upd = prev_top * (1-fnc[0]) *levIns; |
|
|
|
|
|
// = + prev_top * levIns |
|
|
|
|
|
// - prev_top * levIns * fnc[0] |
|
|
|
|
|
|
|
|
|
|
|
st_upd <== aux1 - aux2 |
|
|
|
|
|
|
|
|
|
|
|
// st_na = prev_new1 + prev_old0 + prev_na + prev_upd; |
|
|
|
|
|
// = + prev_new1 |
|
|
|
|
|
// + prev_old0 |
|
|
|
|
|
// + prev_na |
|
|
|
|
|
// + prev_upd |
|
|
|
|
|
|
|
|
st_na <== prev_new1 + prev_old0 + prev_na + prev_upd; |
|
|
st_na <== prev_new1 + prev_old0 + prev_na + prev_upd; |
|
|
st_upd <== aux1*(1-fnc[0]); // prev_top*levIns*(1-fnc[0]) = |
|
|
|
|
|
// = aux1 * (1-fnc[0]) |
|
|
|
|
|
|
|
|
|
|
|
} |
|
|
} |