mirror of
https://github.com/logos-storage/logos-storage-proofs-circuits.git
synced 2026-01-02 13:33:07 +00:00
the circuit seems to work
This commit is contained in:
Balazs Komuves
parent
0ae539a0ed
commit
55015008e7
@ -11,6 +11,8 @@ include "misc.circom";
|
||||
// NOTE: this is rather nontrivial, as everything is computed modulo `r`,
|
||||
// so naive bit decomposition does not work (there are multiple solutions).
|
||||
//
|
||||
// TODO: optimize this
|
||||
//
|
||||
|
||||
template ExtractLowerBits(n) {
|
||||
|
||||
|
||||
@ -42,11 +42,13 @@ template Log2(n) {
|
||||
|
||||
//------------------------------------------------------------------------------
|
||||
//
|
||||
// given an input `inp`, this template computes `k` such that 2^k <= inp < 2^{k+1}
|
||||
// given an input `inp`, this template computes `out := k` such that 2^k <= inp < 2^{k+1}
|
||||
// it also returns the binary decomposition of `inp-1`, and the binary deocmpositiom
|
||||
// of the mask `(2^k-1)`
|
||||
//
|
||||
// we also output a mask vector which is 1 for i=0..out-1, and 0 elsewhere
|
||||
// we also output a mask vector which is 1 for i=0..k-1, and 0 elsewhere
|
||||
//
|
||||
// we require `k <= n`, otherwise this will fail.
|
||||
//
|
||||
|
||||
template CeilingLog2(n) {
|
||||
@ -54,7 +56,7 @@ template CeilingLog2(n) {
|
||||
signal input inp;
|
||||
signal output out;
|
||||
signal output bits[n];
|
||||
signal output mask[n];
|
||||
signal output mask[n+1];
|
||||
|
||||
component tb = ToBits(n);
|
||||
tb.inp <== inp - 1;
|
||||
@ -68,6 +70,7 @@ template CeilingLog2(n) {
|
||||
mask[i] <== 1 - aux[i];
|
||||
sum = sum + (aux[i+1] - aux[i]) * (i+1);
|
||||
}
|
||||
mask[n] <== 0;
|
||||
|
||||
out <== sum;
|
||||
}
|
||||
|
||||
87
circuit/merkle.circom
Normal file
87
circuit/merkle.circom
Normal file
@ -0,0 +1,87 @@
|
||||
pragma circom 2.0.0;
|
||||
|
||||
include "poseidon2_perm.circom";
|
||||
include "poseidon2_hash.circom";
|
||||
|
||||
include "misc.circom";
|
||||
|
||||
//------------------------------------------------------------------------------
|
||||
|
||||
//
|
||||
// reconstruct the Merkle root using a Merkle inclusion proof
|
||||
//
|
||||
// parameters:
|
||||
// - depth: the depth of the Merkle tree = log2( numberOfLeaves )
|
||||
//
|
||||
// inputs and outputs:
|
||||
// - leaf: the leaf hash
|
||||
// - pathBits: the linear index of the leaf, in binary decomposition (little-endian)
|
||||
// - lastBits: the index of the last leaf (= nLeaves-1), in binary decomposition
|
||||
// - maskBits: the bits of the the mask `2^ceilingLog2(size) - 1`
|
||||
// - merklePath: the Merkle inclusion proof (required hashes, starting from the leaf and ending near the root)
|
||||
// - recRoot: the reconstructod Merkle root
|
||||
//
|
||||
// NOTE: we don't check whether the bits are really bits, that's the
|
||||
// responsability of the caller!
|
||||
//
|
||||
|
||||
template RootFromMerklePath( maxDepth ) {
|
||||
|
||||
signal input leaf;
|
||||
signal input pathBits[ maxDepth ]; // bits of the linear index
|
||||
signal input lastBits[ maxDepth ]; // bits of the last linear index `= size-1`
|
||||
signal input maskBits[ maxDepth+1 ]; // bit mask for `2^ceilingLog(size) - 1`
|
||||
signal input merklePath[ maxDepth ];
|
||||
signal output recRoot;
|
||||
|
||||
// the sequence of reconstructed hashes along the path
|
||||
signal aux[ maxDepth+1 ];
|
||||
aux[0] <== leaf;
|
||||
|
||||
// compute which prefixes (in big-endian) of the index is
|
||||
// the same as the corresponding prefix of the last index
|
||||
component eq[ maxDepth ];
|
||||
signal isLast[ maxDepth+1 ];
|
||||
isLast[ maxDepth ] <== 1;
|
||||
for(var i=maxDepth-1; i>=0; i--) {
|
||||
eq[i] = IsEqual();
|
||||
eq[i].A <== pathBits[i];
|
||||
eq[i].B <== lastBits[i];
|
||||
isLast[i] <== isLast[i+1] * eq[i].out;
|
||||
}
|
||||
|
||||
// compute the sequence of hashes
|
||||
signal switch[ maxDepth ];
|
||||
component comp[ maxDepth ];
|
||||
for(var i=0; i<maxDepth; i++) {
|
||||
|
||||
var bottom = (i==0) ? 1 : 0; // is it the bottom layer?
|
||||
var odd = isLast[i] * (1-pathBits[i]); // is it an odd node?
|
||||
|
||||
comp[i] = KeyedCompression();
|
||||
|
||||
var L = aux[i];
|
||||
var R = merklePath[i];
|
||||
|
||||
// based on pathBits[i], we switch or not
|
||||
|
||||
switch[i] <== (R-L) * pathBits[i];
|
||||
comp[i].key <== bottom + 2*odd;
|
||||
comp[i].inp[0] <== L + switch[i];
|
||||
comp[i].inp[1] <== R - switch[i];
|
||||
|
||||
comp[i].out ==> aux[i+1];
|
||||
}
|
||||
|
||||
// now we need to select the right layer from the sequence of hashes
|
||||
var sum = 0;
|
||||
signal prods[maxDepth];
|
||||
for(var i=0; i<maxDepth; i++) {
|
||||
prods[i] <== (maskBits[i] - maskBits[i+1]) * aux[i+1];
|
||||
sum += prods[i];
|
||||
}
|
||||
recRoot <== sum;
|
||||
}
|
||||
|
||||
//------------------------------------------------------------------------------
|
||||
|
||||
@ -55,7 +55,7 @@ template IsEqual() {
|
||||
signal output out;
|
||||
|
||||
component isz = IsZero();
|
||||
isz.in <== A - B;
|
||||
isz.inp <== A - B;
|
||||
isz.out ==> out;
|
||||
}
|
||||
|
||||
|
||||
@ -1,46 +0,0 @@
|
||||
pragma circom 2.0.0;
|
||||
|
||||
include "poseidon2_perm.circom";
|
||||
|
||||
//------------------------------------------------------------------------------
|
||||
// Merkle tree built using the Poseidon2 permutation
|
||||
//
|
||||
// The number of leaves is `2**nlevels`
|
||||
//
|
||||
|
||||
template PoseidonMerkle(nlevels) {
|
||||
|
||||
var nleaves = 2**nlevels;
|
||||
|
||||
signal input inp[nleaves];
|
||||
signal output out_root;
|
||||
|
||||
component hsh[ nleaves-1];
|
||||
signal aux[2*nleaves-1];
|
||||
|
||||
for(var k=0; k<nleaves; k++) { aux[k] <== inp[k]; }
|
||||
|
||||
var a = 0; // aux[a..b) = input layer
|
||||
var u = 0; // hsh[u..v) = hash compression components
|
||||
|
||||
for(var lev=0; lev<nlevels; lev++) {
|
||||
|
||||
var b = a + 2**(nlevels-lev );
|
||||
var v = u + 2**(nlevels-lev-1);
|
||||
|
||||
var ncherries = 2**(nlevels-lev-1);
|
||||
for(var k=0; k<ncherries; k++) {
|
||||
hsh[u+k] = Compression();
|
||||
hsh[u+k].inp[0] <== aux[a+2*k ];
|
||||
hsh[u+k].inp[1] <== aux[a+2*k+1];
|
||||
hsh[u+k].out ==> aux[b+ k ];
|
||||
}
|
||||
|
||||
a = b;
|
||||
u = v;
|
||||
}
|
||||
|
||||
aux[2*nleaves-2] ==> out_root;
|
||||
}
|
||||
|
||||
//------------------------------------------------------------------------------
|
||||
@ -213,5 +213,20 @@ template Compression() {
|
||||
perm.out[0] ==> out;
|
||||
}
|
||||
|
||||
//--------------------------------------
|
||||
|
||||
template KeyedCompression() {
|
||||
signal input key;
|
||||
signal input inp[2];
|
||||
signal output out;
|
||||
|
||||
component perm = Permutation();
|
||||
perm.inp[0] <== inp[0];
|
||||
perm.inp[1] <== inp[1];
|
||||
perm.inp[2] <== key;
|
||||
|
||||
perm.out[0] ==> out;
|
||||
}
|
||||
|
||||
//------------------------------------------------------------------------------
|
||||
|
||||
|
||||
@ -51,9 +51,14 @@ template PoseidonSponge(t, capacity, input_len, output_len) {
|
||||
|
||||
signal state [nblocks+nout][t ];
|
||||
signal sorbed[nblocks ][rate];
|
||||
|
||||
|
||||
// domain separation, capacity IV := 2^64 + 256*t + rate
|
||||
var civ = 2**64 + 256*t + rate;
|
||||
// log("capacity IV = ",civ);
|
||||
|
||||
// initialize state
|
||||
for(var i=0; i<t; i++) { state[0][i] <== 0; }
|
||||
for(var i=0; i<t-1; i++) { state[0][i] <== 0; }
|
||||
state[0][t-1] <== civ;
|
||||
|
||||
component absorb [nblocks];
|
||||
component squeeze[nout-1];
|
||||
|
||||
@ -3,6 +3,7 @@ pragma circom 2.0.0;
|
||||
include "single_cell.circom";
|
||||
include "poseidon2_hash.circom";
|
||||
include "extract_bits.circom";
|
||||
include "log2.circom";
|
||||
include "misc.circom";
|
||||
|
||||
//------------------------------------------------------------------------------
|
||||
@ -19,96 +20,116 @@ include "misc.circom";
|
||||
// NOTE: we assume `nCells` is a power of two.
|
||||
//
|
||||
|
||||
template CalculateCellIndexBits( nCells ) {
|
||||
template CalculateCellIndexBits( maxLog2N ) {
|
||||
|
||||
var log2N = CeilLog2(nCells);
|
||||
assert( nCells == (1<<log2N) );
|
||||
|
||||
signal input entropy;
|
||||
signal input slotRoot;
|
||||
signal input counter;
|
||||
signal output indexBits[log2N];
|
||||
signal input cellIndexBitMask[maxLog2N]; // bit mask for the cell index range
|
||||
|
||||
signal output indexBits[maxLog2N];
|
||||
|
||||
// calculate the hash
|
||||
component pos = Poseidon2_hash_rate2(3);
|
||||
component pos = Poseidon2_hash_rate2( 3 ); // input is 3 field elements
|
||||
signal hash;
|
||||
pos.inp[0] <== entropy;
|
||||
pos.inp[1] <== slotRoot;
|
||||
pos.inp[2] <== counter;
|
||||
pos.out ==> hash;
|
||||
|
||||
// extract the lowest `log2(nCells)` bits
|
||||
component md = ExtractLowerBits(log2N);
|
||||
// extract the lowest `maxLog2N = 32` bits
|
||||
component md = ExtractLowerBits(maxLog2N);
|
||||
md.inp <== hash;
|
||||
md.out ==> indexBits;
|
||||
|
||||
}
|
||||
|
||||
//------------------------------------------------------------------------------
|
||||
|
||||
//
|
||||
// same as above, but returns an integer index instead of its binary decomposition.
|
||||
//
|
||||
|
||||
template CalculateCellIndexInteger( nCells ) {
|
||||
|
||||
var log2N = CeilLog2(nCells);
|
||||
assert( nCells == (1<<log2N) );
|
||||
|
||||
signal input entropy;
|
||||
signal input slotRoot;
|
||||
signal input counter;
|
||||
signal output linearIndex;
|
||||
|
||||
component calc = CalculateCellIndexBits( nCells );
|
||||
calc.entropy <== entropy;
|
||||
calc.slotRoot <== slotRoot;
|
||||
calc.counter <== counter;
|
||||
|
||||
var sum = 0;
|
||||
for(var i=0; i<log2N; i++) {
|
||||
sum += (1<<i) * calc.indexBits[i];
|
||||
for(var i=0; i<maxLog2N; i++ ) {
|
||||
indexBits[i] <== cellIndexBitMask[i] * md.out[i];
|
||||
}
|
||||
|
||||
linearIndex <== sum;
|
||||
}
|
||||
|
||||
//------------------------------------------------------------------------------
|
||||
|
||||
//
|
||||
// sample `nSamples` number of cells; calculate their hashes;
|
||||
// reconstruct the slot root using the Merkle pathes, and
|
||||
// checks if it matches the externally given slot root.
|
||||
//
|
||||
// NOTE: difference between V1 and V2 is whether we use the slot root
|
||||
// or the dataset root.
|
||||
// reconstruct the slot root using the Merkle paths, then
|
||||
// the dataset root too, and checks if everything is consistent.
|
||||
//
|
||||
|
||||
template SampleAndProveV1( nCells, nFieldElemsPerCell, nSamples ) {
|
||||
template SampleAndProve( maxDepth, maxLog2NSlots, blockTreeDepth, nFieldElemsPerCell, nSamples ) {
|
||||
|
||||
var log2N = CeilLog2(nCells);
|
||||
assert( nCells == (1<<log2N) );
|
||||
// var maxDepth = 32; // maximum depth of the slot Merkle tree (so max `2^maxDepth` cells in a slot)
|
||||
// var maxLog2NSlots = 8; // maximum depth of the dataset-level Merkle tree (so max 2^8 slots per dataset)
|
||||
// var blockTreeDepth = 5; // depth of the "network block tree" (= log2(64k / 2k))
|
||||
|
||||
signal input entropy; // public input
|
||||
signal input slotRoot; // public input
|
||||
signal input entropy; // public input
|
||||
signal input dataSetRoot; // public input
|
||||
signal input slotIndex; // must be public, otherwise we could prove a different slot
|
||||
|
||||
signal input cellData[nSamples][nFieldElemsPerCell]; // private input
|
||||
signal input merklePaths[nSamples][log2N]; // private input
|
||||
signal input slotRoot; // can be private input
|
||||
signal input nCellsPerSlot; // can be private input (Merkle tree is safe)
|
||||
signal input nSlotsPerDataSet; // can be private input (Merkle tree is safe)
|
||||
|
||||
signal input slotProof[maxLog2NSlots]; // path from the slot root the the dataset root (private input)
|
||||
|
||||
signal input cellData[nSamples][nFieldElemsPerCell]; // private input
|
||||
signal input merklePaths[nSamples][maxDepth]; // private input
|
||||
|
||||
// -------------------------------------------------------
|
||||
//
|
||||
// first we prove the inclusion of the slot root in the dataset-level
|
||||
// (small) Merkle tree
|
||||
|
||||
component tbtp = ToBits( maxLog2NSlots );
|
||||
component clog = CeilingLog2( maxLog2NSlots );
|
||||
component mtop = RootFromMerklePath( maxLog2NSlots );
|
||||
|
||||
tbtp.inp <== slotIndex;
|
||||
clog.inp <== nSlotsPerDataSet;
|
||||
mtop.leaf <== slotRoot;
|
||||
mtop.pathBits <== tbtp.out;
|
||||
mtop.lastBits <== clog.bits;
|
||||
mtop.maskBits <== clog.mask;
|
||||
mtop.merklePath <== slotProof;
|
||||
|
||||
log("top root check = ", mtop.recRoot == dataSetRoot);
|
||||
|
||||
mtop.recRoot === dataSetRoot;
|
||||
|
||||
// -------------------------------------------------------
|
||||
//
|
||||
// then we prove the individual sampled cells
|
||||
|
||||
signal log2N;
|
||||
component lg = Log2(maxDepth); // we allow at most 2^32 cells per slot
|
||||
lg.inp <== nCellsPerSlot;
|
||||
lg.out ==> log2N;
|
||||
|
||||
// NOTE: in general we need the for Merkle prover the binary decomposition
|
||||
// of `nLeaves - 1`. But currently this is in fact a power of two, so we
|
||||
// can reuse the binary mask for this. Later we may change this?
|
||||
//
|
||||
signal lastBits[maxDepth];
|
||||
for(var i=0; i<maxDepth; i++) { lastBits[i] <== lg.mask[i]; }
|
||||
|
||||
component calci[nSamples];
|
||||
component prove[nSamples];
|
||||
|
||||
for(var cnt=0; cnt<nSamples; cnt++) {
|
||||
|
||||
calci[cnt] = CalculateCellIndexBits( nCells );
|
||||
prove[cnt] = ProveSingleCell( nFieldElemsPerCell, log2N );
|
||||
calci[cnt] = CalculateCellIndexBits( maxDepth );
|
||||
prove[cnt] = ProveSingleCell( nFieldElemsPerCell, blockTreeDepth, maxDepth );
|
||||
|
||||
// calci[cnt].cellIndexBitMask <== lg.mask;
|
||||
for(var i=0; i<maxDepth; i++) { calci[cnt].cellIndexBitMask[i] <== lg.mask[i]; }
|
||||
|
||||
calci[cnt].entropy <== entropy;
|
||||
calci[cnt].slotRoot <== slotRoot;
|
||||
calci[cnt].counter <== cnt + 1;
|
||||
calci[cnt].indexBits ==> prove[cnt].indexBits;
|
||||
calci[cnt].entropy <== entropy;
|
||||
calci[cnt].slotRoot <== slotRoot;
|
||||
calci[cnt].counter <== cnt + 1;
|
||||
calci[cnt].indexBits ==> prove[cnt].indexBits;
|
||||
|
||||
prove[cnt].slotRoot <== slotRoot;
|
||||
prove[cnt].lastBits <== lastBits;
|
||||
prove[cnt].maskBits <== lg.mask;
|
||||
prove[cnt].data <== cellData[cnt];
|
||||
prove[cnt].merklePath <== merklePaths[cnt];
|
||||
|
||||
|
||||
@ -3,124 +3,74 @@ pragma circom 2.0.0;
|
||||
include "poseidon2_perm.circom";
|
||||
include "poseidon2_hash.circom";
|
||||
|
||||
include "merkle.circom";
|
||||
include "misc.circom";
|
||||
|
||||
//------------------------------------------------------------------------------
|
||||
|
||||
//
|
||||
// reconstruct the Merkle root using a Merkle inclusion proof
|
||||
//
|
||||
// parameters:
|
||||
// - depth: the depth of the Merkle tree = log2( numberOfLeaves )
|
||||
//
|
||||
// inputs and outputs:
|
||||
// - leaf: the leaf hash
|
||||
// - pathBits: the linear index of the leaf, in binary decomposition (little-endian)
|
||||
// - merklePath: the Merkle inclusion proof (required hashes, starting from the leaf and ending near the root)
|
||||
// - recRoot: the reconstructod Merkle root
|
||||
//
|
||||
// NOTE: we don't check whether the bits are really bits, that's the
|
||||
// responsability of the caller!
|
||||
//
|
||||
|
||||
template MerklePathBits( depth ) {
|
||||
|
||||
signal input leaf;
|
||||
signal input pathBits[ depth ];
|
||||
signal input merklePath[ depth ];
|
||||
signal output recRoot;
|
||||
|
||||
// the sequence of reconstructed hashes along the path
|
||||
signal aux[ depth+1 ];
|
||||
aux[0] <== leaf;
|
||||
|
||||
signal switch[ depth];
|
||||
|
||||
component comp[ depth ];
|
||||
for(var i=0; i<depth; i++) {
|
||||
comp[i] = Compression();
|
||||
|
||||
var L = aux[i];
|
||||
var R = merklePath[i];
|
||||
|
||||
// based on pathBits[i], we switch or not
|
||||
|
||||
switch[i] <== (R-L) * pathBits[i];
|
||||
comp[i].inp[0] <== L + switch[i];
|
||||
comp[i].inp[1] <== R - switch[i];
|
||||
|
||||
comp[i].out ==> aux[i+1];
|
||||
}
|
||||
|
||||
aux[depth] ==> recRoot;
|
||||
}
|
||||
|
||||
//--------------------------------------
|
||||
|
||||
//
|
||||
// a version of the above where the leaf index is given as an integer
|
||||
// instead of a sequence of bits
|
||||
//
|
||||
|
||||
template MerklePathIndex( depth ) {
|
||||
|
||||
signal input leaf;
|
||||
signal input linearIndex;
|
||||
signal input merklePath[ depth ];
|
||||
signal output recRoot;
|
||||
|
||||
// decompose the linear cell index into bits (0 = left, 1 = right)
|
||||
component tb = ToBits( depth );
|
||||
component path = MerklePathBits( depth );
|
||||
|
||||
tb.inp <== linearIndex;
|
||||
tb.out ==> path.pathBits;
|
||||
|
||||
path.leaf <== leaf;
|
||||
path.merklePath <== merklePath;
|
||||
path.recRoot ==> recRoot;
|
||||
}
|
||||
|
||||
//------------------------------------------------------------------------------
|
||||
|
||||
//
|
||||
// calculates a single cell's hash and reconstructs the Merkle root,
|
||||
// checking whether it matches the given slot root
|
||||
//
|
||||
// parameters:
|
||||
// - nFieldElemsPerCell: how many field elements a cell consists of
|
||||
// - merkleDepth: the depth of slot subtree = log2(nCellsPerSlot)
|
||||
// - nFieldElemsPerCell: how many field elements a cell consists of (= 2048/31 = 67)
|
||||
// - botDepth: the depth of the per-block minitree (= 5)
|
||||
// - maxDepth: the maximum depth of slot subtree (= 32)
|
||||
//
|
||||
// inputs and outputs:
|
||||
// - indexBits: the linear index of the cell, within the slot subtree, in binary
|
||||
// - data: the cell data (already encoded as field elements)
|
||||
// - merklePath: the Merkle inclusion proof
|
||||
// - slotRoot: the expected slot root
|
||||
// - indexBits: the linear index of the cell, within the slot subtree, in binary
|
||||
// - lastBits: the index of the last cell (size - 1), in binary (required for odd-even node key)
|
||||
// - maskBits: the binary mask of the size rounded up to a power of two
|
||||
// - data: the cell data (already encoded as field elements)
|
||||
// - merklePath: the Merkle inclusion proof
|
||||
// - slotRoot: the expected slot root
|
||||
//
|
||||
// NOTE: we don't check whether the bits are really bits, that's the
|
||||
// responsability of the caller!
|
||||
// responsability of the caller!
|
||||
//
|
||||
|
||||
template ProveSingleCell( nFieldElemsPerCell, merkleDepth ) {
|
||||
template ProveSingleCell( nFieldElemsPerCell, botDepth, maxDepth ) {
|
||||
|
||||
signal input slotRoot;
|
||||
signal input data[ nFieldElemsPerCell ];
|
||||
signal input lastBits [ maxDepth ];
|
||||
signal input indexBits [ maxDepth ];
|
||||
signal input maskBits [ maxDepth + 1 ];
|
||||
signal input merklePath[ maxDepth ];
|
||||
|
||||
signal input indexBits [ merkleDepth ];
|
||||
signal input merklePath[ merkleDepth ];
|
||||
// these will reconstruct the Merkle path up to the slot root
|
||||
// in two steps: first the block-level ("bottom"), then the slot-level ("middle")
|
||||
component pbot = RootFromMerklePath( botDepth );
|
||||
component pmid = RootFromMerklePath( maxDepth - botDepth );
|
||||
|
||||
// this will reconstruct the Merkle path up to the slot root
|
||||
component path = MerklePathBits( merkleDepth );
|
||||
path.pathBits <== indexBits;
|
||||
path.merklePath <== merklePath;
|
||||
for(var i=0; i<maxDepth; i++) {
|
||||
if (i<botDepth) {
|
||||
pbot.pathBits[i] <== indexBits[i];
|
||||
pbot.maskBits[i] <== maskBits[i];
|
||||
pbot.lastBits[i] <== lastBits[i];
|
||||
pbot.merklePath[i] <== merklePath[i];
|
||||
}
|
||||
else {
|
||||
var j = i - botDepth;
|
||||
pmid.pathBits[j] <== indexBits[i];
|
||||
pmid.maskBits[j] <== maskBits[i];
|
||||
pmid.lastBits[j] <== lastBits[i];
|
||||
pmid.merklePath[j] <== merklePath[i];
|
||||
}
|
||||
}
|
||||
pbot.maskBits[ botDepth ] <== 0;
|
||||
pmid.maskBits[ maxDepth - botDepth ] <== 0;
|
||||
|
||||
// compute the cell hash
|
||||
component hash = Poseidon2_hash_rate2( nFieldElemsPerCell );
|
||||
hash.inp <== data;
|
||||
hash.out ==> path.leaf;
|
||||
hash.inp <== data;
|
||||
hash.out ==> pbot.leaf;
|
||||
pmid.leaf <== pbot.recRoot;
|
||||
|
||||
log("middle bottom root check = ", pmid.recRoot == slotRoot);
|
||||
|
||||
// check if the reconstructed root matches the actual slot root
|
||||
path.recRoot === slotRoot;
|
||||
pmid.recRoot === slotRoot;
|
||||
|
||||
}
|
||||
|
||||
|
||||
@ -1,3 +1,4 @@
|
||||
pragma circom 2.0.0;
|
||||
include "sample_cells.circom";
|
||||
component main {public [entropy,slotRoot]} = SampleAndProveV1(1024, 5, 10);
|
||||
// SampleAndProven( maxDepth, maxLog2NSlots, blockTreeDepth, nFieldElemsPerCell, nSamples )
|
||||
component main {public [entropy,dataSetRoot,slotIndex]} = SampleAndProve(16, 5, 3, 5, 10);
|
||||
|
||||
35
circuit/test_prove.sh
Executable file
35
circuit/test_prove.sh
Executable file
@ -0,0 +1,35 @@
|
||||
#!/bin/bash
|
||||
|
||||
ORIG=`pwd`
|
||||
|
||||
PTAU_DIR="/Users/bkomuves/zk/ptau/"
|
||||
PTAU_FILE="${PTAU_DIR}/powersOfTau28_hez_final_20.ptau"
|
||||
|
||||
NAME="slot_main"
|
||||
|
||||
# --- setup ---
|
||||
|
||||
cd $ORIG/build
|
||||
echo "circuit-specific ceremony..."
|
||||
snarkjs groth16 setup ${NAME}.r1cs ${PTAU_FILE} ${NAME}_0000.zkey
|
||||
echo "some_entropy_xxx" | snarkjs zkey contribute ${NAME}_0000.zkey ${NAME}_0001.zkey --name="1st Contributor Name"
|
||||
rm ${NAME}_0000.zkey
|
||||
mv ${NAME}_0001.zkey ${NAME}.zkey
|
||||
snarkjs zkey export verificationkey ${NAME}.zkey ${NAME}_verification_key.json
|
||||
|
||||
# --- prove ---
|
||||
|
||||
echo ""
|
||||
echo "trying to prove... (with snarkjs)"
|
||||
|
||||
cd $ORIG/build
|
||||
time snarkjs groth16 prove ${NAME}.zkey ${NAME}.wtns ${NAME}_proof.json ${NAME}_public.json
|
||||
|
||||
# --- verify ---
|
||||
|
||||
echo ""
|
||||
echo "verifyng proof..."
|
||||
snarkjs groth16 verify ${NAME}_verification_key.json ${NAME}_public.json ${NAME}_proof.json
|
||||
|
||||
cd $ORIG
|
||||
cd $ORIG
|
||||
@ -1,21 +1,25 @@
|
||||
#!/bin/bash
|
||||
|
||||
ORIG=`pwd`
|
||||
mkdir -p build
|
||||
|
||||
cd ../reference/haskell
|
||||
runghc testMain.hs || { echo "ghc failed"; exit 101; }
|
||||
mkdir -p json
|
||||
cabal v1-run cli/testMain.hs || { echo "ghc failed"; cd $ORIG; exit 101; }
|
||||
|
||||
mv input_example.json ${ORIG}/build/
|
||||
mv slot_main.circom ${ORIG}
|
||||
mv json/input_example.json ${ORIG}/build/
|
||||
mv json/slot_main.circom ${ORIG}
|
||||
|
||||
cd ${ORIG}/build
|
||||
|
||||
NAME="slot_main"
|
||||
circom ../${NAME}.circom --r1cs --wasm || { echo "circom failed"; exit 102; }
|
||||
circom ../${NAME}.circom --r1cs --wasm || { echo "circom failed"; cd $ORIG; exit 102; }
|
||||
|
||||
echo "generating witness... (WASM)"
|
||||
cd ${NAME}_js
|
||||
node generate_witness.js ${NAME}.wasm ../input_example.json ../${NAME}_witness.wtns || { echo "witness gen failed"; exit 101; }
|
||||
node generate_witness.js ${NAME}.wasm ../input_example.json ../${NAME}.wtns || { echo "witness gen failed"; cd $ORIG; exit 101; }
|
||||
cd ..
|
||||
|
||||
echo "witness generation succeeded"
|
||||
|
||||
cd $ORIG
|
||||
|
||||
@ -11,17 +11,21 @@ import Sampling
|
||||
|
||||
smallDataSetCfg :: DataSetCfg
|
||||
smallDataSetCfg = MkDataSetCfg
|
||||
{ _nSlots = 5
|
||||
{ _maxDepth = 16
|
||||
, _maxLog2NSlots = 5
|
||||
, _nSlots = 5
|
||||
, _cellSize = 128
|
||||
, _blockSize = 4096
|
||||
, _nCells = 256
|
||||
, _nSamples = 5
|
||||
, _blockSize = 1024
|
||||
, _nCells = 64
|
||||
, _nSamples = 10
|
||||
, _dataSrc = FakeData (Seed 12345)
|
||||
}
|
||||
|
||||
bigDataSetCfg :: DataSetCfg
|
||||
bigDataSetCfg = MkDataSetCfg
|
||||
{ _nSlots = 13
|
||||
{ _maxDepth = 32
|
||||
, _maxLog2NSlots = 8
|
||||
, _nSlots = 13
|
||||
, _cellSize = 2048
|
||||
, _blockSize = 65536
|
||||
, _nCells = 512
|
||||
|
||||
@ -4,19 +4,24 @@ module DataSet where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import Data.List
|
||||
import System.FilePath
|
||||
|
||||
import Slot hiding ( MkSlotCfg(..) )
|
||||
import qualified Slot as Slot
|
||||
|
||||
import Misc
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data DataSetCfg = MkDataSetCfg
|
||||
{ _nSlots :: Int -- ^ number of slots per dataset
|
||||
, _cellSize :: Int
|
||||
, _blockSize :: Int
|
||||
, _nCells :: Int
|
||||
, _nSamples :: Int
|
||||
{ _maxDepth :: Int -- ^ @nCells@ must fit into this many bits
|
||||
, _maxLog2NSlots :: Int -- ^ @nSlots@ must fit into this many bits
|
||||
, _nSlots :: Int -- ^ number of slots per dataset
|
||||
, _cellSize :: Int -- ^ cell size in bytes
|
||||
, _blockSize :: Int -- ^ slot size in bytes
|
||||
, _nCells :: Int -- ^ number of cells per slot
|
||||
, _nSamples :: Int -- ^ number of cells we sample in a proof
|
||||
, _dataSrc :: DataSource
|
||||
}
|
||||
deriving Show
|
||||
@ -57,12 +62,20 @@ loadDataSetBlock dsetCfg slotIdx@(SlotIdx idx) blockidx
|
||||
circomMainComponent :: DataSetCfg -> FilePath -> IO ()
|
||||
circomMainComponent dsetCfg circomFile = do
|
||||
|
||||
let params = show (DataSet.fieldElemsPerCell dsetCfg)
|
||||
++ ", " ++ show (DataSet._nSamples dsetCfg)
|
||||
let cellsPerBlock = (DataSet._blockSize dsetCfg) `div` (DataSet._cellSize dsetCfg)
|
||||
let blockDepth = ceilingLog2 (fromIntegral cellsPerBlock)
|
||||
|
||||
let params = intercalate ", " $ map show
|
||||
[ DataSet._maxDepth dsetCfg
|
||||
, DataSet._maxLog2NSlots dsetCfg
|
||||
, blockDepth
|
||||
, DataSet.fieldElemsPerCell dsetCfg
|
||||
, DataSet._nSamples dsetCfg
|
||||
]
|
||||
writeFile circomFile $ unlines
|
||||
[ "pragma circom 2.0.0;"
|
||||
, "include \"sample_cells.circom\";"
|
||||
, "// SampleAndProven( maxDepth, maxLog2NSlots, blockTreeDepth, nFieldElemsPerCell, nSamples ) "
|
||||
, "component main {public [entropy,dataSetRoot,slotIndex]} = SampleAndProve(" ++ params ++ ");"
|
||||
]
|
||||
|
||||
|
||||
@ -36,6 +36,15 @@ sampleCellIndex cfg entropy slotRoot counter = CellIdx (fromInteger idx) where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
padWithZeros :: Int -> [Fr] -> [Fr]
|
||||
padWithZeros n xs
|
||||
| m <= n = xs ++ replicate (n-m) Fr.zero
|
||||
| otherwise = error "padWithZeros: input too long"
|
||||
where
|
||||
m = length xs
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data CircuitInput = MkInput
|
||||
{ _entropy :: Entropy -- ^ public input
|
||||
, _dataSetRoot :: Hash -- ^ public input
|
||||
@ -72,11 +81,11 @@ calculateCircuitInput dataSetCfg slotIdx@(SlotIdx sidx) entropy = do
|
||||
, _dataSetRoot = dsetRoot
|
||||
, _slotIndex = sidx
|
||||
, _slotRoot = ourSlotRoot
|
||||
, _slotProof = extractMerkleProof_ dsetTree sidx
|
||||
, _slotProof = padWithZeros (_maxLog2NSlots dataSetCfg) $ extractMerkleProof_ dsetTree sidx
|
||||
, _slotsPerDSet = nslots
|
||||
, _cellsPerSlot = Slot._nCells ourSlotCfg
|
||||
, _cellData = cellData
|
||||
, _merklePaths = merklePaths
|
||||
, _merklePaths = map (padWithZeros (_maxDepth dataSetCfg)) merklePaths
|
||||
}
|
||||
|
||||
-- | Export the inputs of the storage proof circuits in JSON format,
|
||||
|
||||
@ -30,12 +30,12 @@ type TestCase = Integer
|
||||
type Output = (Int,[Bool],[Bool])
|
||||
|
||||
semantics :: GP -> TestCase -> Expected Output
|
||||
semantics n a
|
||||
| a >0 && k >= 0 && k < n = Expecting (k,bits,mask)
|
||||
| otherwise = ShouldFail
|
||||
semantics n a
|
||||
| a > 0 && k >= 0 && k <= n = Expecting (k,bits,mask)
|
||||
| otherwise = ShouldFail
|
||||
where
|
||||
k = ceilingLog2 a
|
||||
mask = [ i < k | i<-[0..n-1] ]
|
||||
mask = [ i < k | i<-[0..n] ]
|
||||
bits = [ testBit (a-1) i | i<-[0..n-1] ]
|
||||
|
||||
-- | Smallest integer @k@ such that @2^k@ is larger or equal to @n@
|
||||
|
||||
@ -40,5 +40,5 @@ testSimple' verbosity = do
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
main = do
|
||||
testSimple' Silent -- Verbose -- Silent
|
||||
testSimple' Info --Silent -- Verbose -- Silent
|
||||
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user