mirror of
https://github.com/arnaucube/circomlib.git
synced 2026-02-07 03:06:44 +01:00
Merge other basic circuits here
This commit is contained in:
Jordi Baylina
186
circuits/smt/smtinsert.circom
Normal file
186
circuits/smt/smtinsert.circom
Normal file
@@ -0,0 +1,186 @@
|
||||
/***************************************************************************************************
|
||||
|
||||
Insert to an empty leaf
|
||||
=======================
|
||||
|
||||
STATE OLD STATE NEW STATE
|
||||
===== ========= =========
|
||||
|
||||
oldRoot newRoot
|
||||
▲ ▲
|
||||
│ │
|
||||
┌───────┐ ┏━━━┻━━━┓ ┌───────┐ ┏━━━┻━━━┓
|
||||
top │Sibling├────▶┃ Hash ┃◀─┐ │Sibling├────▶┃ Hash ┃◀─┐
|
||||
└───────┘ ┗━━━━━━━┛ │ └───────┘ ┗━━━━━━━┛ │
|
||||
│ │
|
||||
│ │
|
||||
┏━━━┻━━━┓ ┌───────┐ ┏━━━┻━━━┓ ┌───────┐
|
||||
top ┌─────▶┃ Hash ┃◀──┤Sibling│ ┌─────▶┃ Hash ┃◀──┤Sibling│
|
||||
│ ┗━━━━━━━┛ └───────┘ │ ┗━━━━━━━┛ └───────┘
|
||||
│ │
|
||||
│ │
|
||||
┌───────┐ ┏━━━┻━━━┓ ┌───────┐ ┏━━━┻━━━┓
|
||||
top │Sibling├──▶┃ Hash ┃◀─────┐ │Sibling├──▶┃ Hash ┃◀─────┐
|
||||
└───────┘ ┗━━━━━━━┛ │ └───────┘ ┗━━━━━━━┛ │
|
||||
│ │
|
||||
│ │
|
||||
┌────┴────┐ ┌────┴────┐
|
||||
old0 │ 0 │ │New1Leaf │
|
||||
└─────────┘ └─────────┘
|
||||
|
||||
|
||||
┏━━━━━━━┓ ┏━━━━━━━┓
|
||||
na ┃ Hash ┃ ┃ Hash ┃
|
||||
┗━━━━━━━┛ ┗━━━━━━━┛
|
||||
|
||||
|
||||
┏━━━━━━━┓ ┏━━━━━━━┓
|
||||
na ┃ Hash ┃ ┃ Hash ┃
|
||||
┗━━━━━━━┛ ┗━━━━━━━┛
|
||||
|
||||
|
||||
|
||||
Insert to a used leaf.
|
||||
=====================
|
||||
|
||||
STATE OLD STATE NEW STATE
|
||||
===== ========= =========
|
||||
|
||||
|
||||
oldRoot newRoot
|
||||
▲ ▲
|
||||
│ │
|
||||
┌───────┐ ┏━━━┻━━━┓ ┌───────┐ ┏━━━┻━━━┓
|
||||
top │Sibling├────▶┃ Hash ┃◀─┐ │Sibling├────▶┃ Hash ┃◀─┐
|
||||
└───────┘ ┗━━━━━━━┛ │ └───────┘ ┗━━━━━━━┛ │
|
||||
│ │
|
||||
│ │
|
||||
┏━━━┻━━━┓ ┌───────┐ ┏━━━┻━━━┓ ┌───────┐
|
||||
top ┌─────▶┃ Hash ┃◀──┤Sibling│ ┌─────▶┃ Hash ┃◀──┤Sibling│
|
||||
│ ┗━━━━━━━┛ └───────┘ │ ┗━━━━━━━┛ └───────┘
|
||||
│ │
|
||||
│ │
|
||||
┌───────┐ ┏━━━┻━━━┓ ┌───────┐ ┏━━━┻━━━┓
|
||||
top │Sibling├──▶┃ Hash ┃◀─────┐ │Sibling├──▶┃ Hash ┃◀─────┐
|
||||
└───────┘ ┗━━━━━━━┛ │ └───────┘ ┗━━━━━━━┛ │
|
||||
│ │
|
||||
│ │
|
||||
┌────┴────┐ ┏━━━┻━━━┓ ┌───────┐
|
||||
old1 │Old1Leaf │ ┌─────▶┃ Hash ┃◀──┼─ 0 │
|
||||
└─────────┘ │ ┗━━━━━━━┛ └───────┘
|
||||
│
|
||||
│
|
||||
┏━━━━━━━┓ ┌───────┐ ┏━━━┻━━━┓
|
||||
bot ┃ Hash ┃ │ 0 ─┼──▶┃ Hash ┃◀─────┐
|
||||
┗━━━━━━━┛ └───────┘ ┗━━━━━━━┛ │
|
||||
│
|
||||
│
|
||||
┏━━━━━━━┓ ┏━━━┻━━━┓ ┌───────┐
|
||||
bot ┃ Hash ┃ ┌─────▶┃ Hash ┃◀──│ 0 │
|
||||
┗━━━━━━━┛ │ ┗━━━━━━━┛ └───────┘
|
||||
│
|
||||
│
|
||||
┏━━━━━━━┓ ┌─────────┐ ┏━━━┻━━━┓ ┌─────────┐
|
||||
new1 ┃ Hash ┃ │Old1Leaf ├──▶┃ Hash ┃◀──│New1Leaf │
|
||||
┗━━━━━━━┛ └─────────┘ ┗━━━━━━━┛ └─────────┘
|
||||
|
||||
|
||||
┏━━━━━━━┓ ┏━━━━━━━┓
|
||||
na ┃ Hash ┃ ┃ Hash ┃
|
||||
┗━━━━━━━┛ ┗━━━━━━━┛
|
||||
|
||||
|
||||
┏━━━━━━━┓ ┏━━━━━━━┓
|
||||
na ┃ Hash ┃ ┃ Hash ┃
|
||||
┗━━━━━━━┛ ┗━━━━━━━┛
|
||||
|
||||
***************************************************************************************************/
|
||||
|
||||
include "../node_modules/circom/circuits/gates.circom";
|
||||
include "../node_modules/circom/circuits/bitify.circom";
|
||||
|
||||
template SMTInsert(nLevels) {
|
||||
signal input oldRoot;
|
||||
signal input newRoot;
|
||||
signal input siblings[nLevels];
|
||||
signal input oldHKey;
|
||||
signal input oldHValue;
|
||||
signal input newHKey;
|
||||
signal input newHValue;
|
||||
|
||||
component hash1Old = SMTHash1();
|
||||
hash1Old.l <== oldHKey;
|
||||
hash1Old.r <== oldHValue;
|
||||
|
||||
component hash1New = SMTHash1();
|
||||
hash1New.l <== newHKey;
|
||||
hash1New.r <== newHValue;
|
||||
|
||||
component n2bOld = Num2BinStrinct();
|
||||
component n2bNew = Num2BinStrinct();
|
||||
|
||||
component dmtLevIns = SMTLevIns(nLevels);
|
||||
for (var i=0; i<nLevels; i++) dmtLevIns.siblings[i] <== siblings[i];
|
||||
|
||||
component xors[nLevels];
|
||||
for (var i=0; i<nLevels; i++) {
|
||||
xors[i] = XOR();
|
||||
xors[i].a <== n2bOld.out[i];
|
||||
xors[i].a <== n2bNew.out[i];
|
||||
}
|
||||
|
||||
component isOld0 = IsZero();
|
||||
isOld0.in <== oldHValue;
|
||||
|
||||
component sm[nLevels];
|
||||
for (var i=0; i<sm; i++) {
|
||||
sm[i] = SMTInsertSM();
|
||||
if (i==0) {
|
||||
sm[i].prevst_top <== 1;
|
||||
sm[i].prevst_old1 <== 0;
|
||||
sm[i].prevst_old0 <== 0;
|
||||
sm[i].prevst_bot <== 0;
|
||||
sm[i].prevst_new1 <== 0;
|
||||
sm[i].prevst_na <== 0;
|
||||
} else {
|
||||
sm[i].prevst_top <== sm[i-1].st_top;
|
||||
sm[i].prevst_old1 <== sm[i-1].st_old1;
|
||||
sm[i].prevst_old0 <== sm[i-1].st_old0;
|
||||
sm[i].prevst_bot <== sm[i-1].st_bot;
|
||||
sm[i].prevst_new1 <== sm[i-1].st_new1;
|
||||
sm[i].prevst_na <== sm[i-1].st_na;
|
||||
}
|
||||
sm[i].is0 <== isOld0.out;
|
||||
sm[i].xor <== xors[i].out;
|
||||
sm[i].levIns <== dmtLevIns.out[i];
|
||||
}
|
||||
sm[nLevels-1].prevst_na === 1;
|
||||
|
||||
component levels[nLevels];
|
||||
for (var i=nLevels-1; i != -1; i--) {
|
||||
levels[i] = SMTInsertLevel();
|
||||
|
||||
levels[i].st_top <== sm[i].st_top;
|
||||
levels[i].st_old1 <== sm[i].st_old1;
|
||||
levels[i].st_old0 <== sm[i].st_old0;
|
||||
levels[i].st_bot <== sm[i].st_bot;
|
||||
levels[i].st_new1 <== sm[i].st_new1;
|
||||
levels[i].st_na <==sm[i].st_na;
|
||||
|
||||
levels[i].sibling <== siblings[i];
|
||||
levels[i].old1leaf <== hash1Old.out;
|
||||
levels[i].new1leaf <== hash1New.out;
|
||||
|
||||
levels[i].new1lrbit <== n2bNew.out[i];
|
||||
if (i==nLevels-1) {
|
||||
levels[i].oldChild <== 0;
|
||||
levels[i].newChild <== 0;
|
||||
} else {
|
||||
levels[i].oldChild <== levels[i+1].oldRoot;
|
||||
levels[i].newChild <== levels[i+1].newRoot;
|
||||
}
|
||||
}
|
||||
|
||||
levels[0].oldRoot === oldRoot;
|
||||
levels[0].newRoot === newRoot;
|
||||
}
|
||||
76
circuits/smt/smtinsertlevel.circom
Normal file
76
circuits/smt/smtinsertlevel.circom
Normal file
@@ -0,0 +1,76 @@
|
||||
|
||||
|
||||
/******
|
||||
|
||||
SMTInsertLevel
|
||||
|
||||
This circuit has 2 has
|
||||
|
||||
Outputs according to the state.
|
||||
|
||||
State oldRoot newRoot
|
||||
===== ======= =======
|
||||
top H'(oldChild, sibling) H'(newChild, sibling)
|
||||
old1 old1leaf H'(newChild, 0)
|
||||
old0 0 new1leaf
|
||||
bot 0 H'(newChild, 0)
|
||||
new1 0 H'(new1leaf, old1leaf)
|
||||
na 0 0
|
||||
|
||||
H' is the Hash function with the inputs shifted acordingly.
|
||||
|
||||
*****/
|
||||
|
||||
|
||||
template SMTInsertLevel() {
|
||||
signal input st_top;
|
||||
signal input st_old1;
|
||||
signal input st_old0;
|
||||
signal input st_bot;
|
||||
signal input st_new1;
|
||||
signal input st_na;
|
||||
|
||||
signal output oldRoot;
|
||||
signal output newRoot;
|
||||
signal input sibling;
|
||||
signal input old1leaf;
|
||||
signal input new1leaf;
|
||||
signal input newlrbit;
|
||||
signal input oldChild;
|
||||
signal input newChild;
|
||||
|
||||
signal aux[4];
|
||||
|
||||
component oldProofHash = SMTHash2();
|
||||
component newProofHash = SMTHash2();
|
||||
|
||||
component oldSwitcher = Switcher();
|
||||
component newSwitcher = Switcher();
|
||||
|
||||
// Old side
|
||||
|
||||
oldSwitcher.inL <== oldChild;
|
||||
oldSwitcher.inR <== sibling;
|
||||
|
||||
oldSwitcher.sel <== newlrbit;
|
||||
oldProofHash.L <== oldSwitcher.outL;
|
||||
oldProofHash.R <== oldSwitcher.outR;
|
||||
|
||||
aux[0] <== old1 * st_old1;
|
||||
oldRoot <== aux[0] + oldProofHash.out * st_top;
|
||||
|
||||
// New side
|
||||
|
||||
aux[1] <== newChild * ( st_top + st_old1 + st_but);
|
||||
oldSwitcher.inL <== aux[1] + new1leaf*st_new1;
|
||||
|
||||
aux[2] <== sibling*st_top;
|
||||
oldSwitcher.inR <== aux[2] + old1leaf*st_new1;
|
||||
|
||||
newProofHash.sel <== newlrbit;
|
||||
newProofHash.L <== newProofHash.outL;
|
||||
newProofHash.R <== newProofHash.outR;
|
||||
|
||||
aux[3] <== newProofHash.out * (st_top + st_old1 + st_bot + st_new1);
|
||||
newRoot <== aux[3] + new1leaf * st_old0;
|
||||
}
|
||||
58
circuits/smt/smtinsertsm.circom
Normal file
58
circuits/smt/smtinsertsm.circom
Normal file
@@ -0,0 +1,58 @@
|
||||
/***************************************************************************************************
|
||||
Each level on a SMTInsert has a state.
|
||||
|
||||
The state of the level depends on the state of te botom level and on `xor` and
|
||||
`is0` signals.
|
||||
|
||||
`isOldLev` 1 when is the level where oldLeaf is.
|
||||
|
||||
`xor` signal is 0 if the index bit at the current level is the same in the old
|
||||
and the new index, and 1 if it is different.
|
||||
|
||||
`is0` signal, is 1 if we are inserting in an empty leaf and 0 if we are inserting
|
||||
in a leaf that contains an element.
|
||||
|
||||
The states are:
|
||||
|
||||
top: While the index bits of the old and new insex in the top level is the same, whe are in the top state.
|
||||
old0 and old1: When the we reach insert level, we go to old0 and old1 states
|
||||
according to `is0` signal.
|
||||
btn: Once in old1 we go to btn until xor=1
|
||||
new1: This level is reached when xor=1. Here is where we insert the hash of the
|
||||
old and the new trees with just one element.
|
||||
na: Not appliable. After inserting it, we go to the na level.
|
||||
|
||||
|
||||
|
||||
###########
|
||||
levIns==curLevel # #
|
||||
xor=0 is0=1 ┌────────────▶# old0 #────────┐
|
||||
┌─────┐ │ ## ## │
|
||||
│ │ │ ######### │ any
|
||||
│ ▼ │ │
|
||||
│ ########### │ │ ###########
|
||||
│ # # ────────────┘ └────────▶# #
|
||||
└──# top # # na #
|
||||
## ## ────┐ ┌──▶## ##
|
||||
######### │ │ #########
|
||||
│ │
|
||||
│ ########### ########### │ any
|
||||
levIns==curLevel │ # # xor=1 # # │
|
||||
is0=0 └───▶# old1 #─────────────▶# new1 #──┘
|
||||
## ## ## ##
|
||||
#########──┐ #########
|
||||
│ ▲
|
||||
│ ┌─────┘
|
||||
any │ ###########│ xor=1
|
||||
│ # #
|
||||
└─▶# btn #
|
||||
## ##
|
||||
#########◀───────┐
|
||||
│ │
|
||||
│ │
|
||||
└────────────┘
|
||||
xor=0
|
||||
|
||||
***************************************************************************************************/
|
||||
|
||||
state
|
||||
80
circuits/smt/smtlevins.circom
Normal file
80
circuits/smt/smtlevins.circom
Normal file
@@ -0,0 +1,80 @@
|
||||
/*
|
||||
|
||||
This component finds the level where the oldInsert is done.
|
||||
The rules are:
|
||||
|
||||
levIns[i] == 1 if its level and all the child levels have a sibling of 0 and
|
||||
the parent level has a sibling != 0. Considere that the root level always has
|
||||
a parent with a sibling != 0.
|
||||
|
||||
|
||||
┌──────────────┐
|
||||
│ │
|
||||
│ │───▶ levIns[0] <== (1-done[i])
|
||||
│ │
|
||||
└──────────────┘
|
||||
▲
|
||||
│
|
||||
│
|
||||
done[0]
|
||||
|
||||
|
||||
|
||||
done[i-1] <== levIns[i] + done[i]
|
||||
▲
|
||||
│
|
||||
│
|
||||
┌───────────┐ ┌──────────────┐
|
||||
│ │ │ │
|
||||
sibling[i-1]───▶│IsZero[i-1]│─▶│ │───▶ levIns[i] <== (1-done[i])*(1-isZero[i-1].out)
|
||||
│ │ │ │
|
||||
└───────────┘ └──────────────┘
|
||||
▲
|
||||
│
|
||||
│
|
||||
done[i]
|
||||
|
||||
|
||||
|
||||
done[n-2] <== levIns[n-1]
|
||||
▲
|
||||
│
|
||||
│
|
||||
┌───────────┐ ┌──────────────┐
|
||||
│ │ │ │
|
||||
sibling[n-2]───▶│IsZero[n-2]│─▶│ │────▶ levIns[n-1] <== (1-isZero[n-2].out)
|
||||
│ │ │ │
|
||||
└───────────┘ └──────────────┘
|
||||
|
||||
┌───────────┐
|
||||
│ │
|
||||
sibling[n-1]───▶│IsZero[n-1]│────▶ === 0
|
||||
│ │
|
||||
└───────────┘
|
||||
|
||||
*/
|
||||
|
||||
template SMTLevIns(nLevels) {
|
||||
signal input siblins[nLevels];
|
||||
signal output levIns[nLevels];
|
||||
signal done[nLevels-1]; // Indicates if the insLevel has aready been detecetd.
|
||||
|
||||
component isZero[nLevels];
|
||||
|
||||
for (var i=0; i<nLevels; i++) {
|
||||
isZero[i] = IsZero();
|
||||
isZero[i].in <== siblings[i];
|
||||
}
|
||||
|
||||
// The last level must always have a sibling of 0. If not, then it cannot be inserted.
|
||||
isZero[nLevels-2].out === 1;
|
||||
|
||||
levIns[nLevels-1] <== (1-isZero[nLevels-2].out);
|
||||
done[nLevels-2] <== levIns[nLevels-1];
|
||||
for (var i=nLevels-2; i>0; i--) {
|
||||
levIns[i] <== (1-done[i])*(1-isZero[i-1].out)
|
||||
done[i-1] <== levIns[i] + done[i];
|
||||
}
|
||||
|
||||
levIns[0] <== (1-done[0]);
|
||||
}
|
||||
Reference in New Issue
Block a user