logos-storage/logos-storage-proofs-circuits
1
0
Fork 0
mirror of https://github.com/logos-storage/logos-storage-proofs-circuits.git synced 2026-01-08 08:23:05 +00:00
Code Issues Packages Projects Releases Wiki Activity

initial import (copy from the private repo)

Browse Source
This commit is contained in:
Balazs Komuves 2023-10-25 18:12:26 +02:00
parent b0bbb9150e
commit 1f4ae5874d
36 changed files with 2107 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
.gitignore vendored Normal file
View File

@ -0,0 +1,4 @@
.DS_store
*.o
*.hi
build

206
README.md Normal file
View File

@ -0,0 +1,206 @@
Codex Storage Proofs for the MVP
================================
This document describes the storage proof system for the Codex 2023 Q4 MVP.
Setup
-----
We assume that a user dataset is split into `nSlots` number of uniformly sized
"slots" of size `slotSize`, for example 100 GB (for the MVP we may chose
a smaller size). The slots of the same dataset are spread over different
storage nodes, but a single storage node can hold several slots (belonging to
different datasets). The slots themselves can be optionally erasure coded,
but this does not change the proof system, only the robustness of it.
We assume the slots are split into `nCells` number of uniformly sized
"cells" of size `cellSize`, for example 512 bytes. We don't in general assume
that these numbers of powers of two, though in practice `nCells` will be probably
a power of two, and in fact the initial implementation assumes this.
Note that we can simply calculate:
nCells = slotSize / cellSize
We then hash each cell (using the sponge construction with Poseidon2; see below
for details), and build a binary Merkle tree over this hashes. This has depth
`d = ceil[ log2(nCells) ]`. Note: if `nCells` is not a power of two, then we
have to add dummy hashes. The exact conventions for doing this is to be determined
later.
The Merkle root of the cells of a single slot is called the "slot root", and
is denoted by `slotRoot`.
Then for a given dataset, we can build another binary Merkle tree on the top of
its slot roots, resulting in the "dataset root". Grafting these Merkle trees
together we get a big dataset Merkle tree; however one should be careful
about the padding conventions (it makes sense to construct the dataset-level
Merkle tree separately, as `nSlots` may not be a power of two).
The dataset root is a commitment to the whole dataset, and the user will post
it on-chain, to ensure that the nodes really store its data and not something else.
Optionally, the slot roots can be posted on-chain, but this seems to be somewhat
wasteful.
Hash function
-------------
For the MVP we will use the Poseidon2 hash function, specialized to state size
`t = 3` field elements, and to the alt-bn128 elliptic curve's scalar field, which
has size
r = 21888242871839275222246405745257275088548364400416034343698204186575808495617
For more details about this curve, see [BN254 For The Rest Of Us](https://hackmd.io/@jpw/bn254).
Remark: we have `2^253 < r < 2^254`.
For more details about the Poseidon2 hash, see
- [the Poseidon2 paper](https://eprint.iacr.org/2023/323)
- [the reference implementation](https://github.com/HorizenLabs/poseidon2)
### Data encoding convention
Poseidon2 hash works not over sequence of bytes, but field elements. Hence we
need to convert the data to be hashed to a sequence of field elements.
Note that the field size is approximately 254 bits, so a field element can store
31 bytes of data but cannot store 32 bytes. Hence we have to split up our data
into 31 bytes "hash chunks", then encode these as field elements. We will use
little-endian byte convention to get from 31 bytes to the _standard form_ of
a field element, that is, the 31 little-endian bytes encode the number `a`
where `0 <= a < 2^248 < r < 2^254` is the standard representation of a field element.
For padding the last field element just use zero bytes.
It's probably better to choose the standard form, because most standard tools
like circom use that, even though choosing the Montgomery form would be somewhat
more efficient (but the difference is very small, the hashing will dominate).
### Compression and sponge
Poseidon2 offers essentially two API functions: a so called _compression function_
which takes 2 field elements and returns 1; this can be used to build binary
Merkle trees.
The more complex _sponge_ can hash an arbitrary sequence of field elements into
a single (or several) field element(s).
While we can always use a Merkle tree instead of the sponge, if the data to be
hashed does not correspond to a power of two number of field elements, then
the sponge could be more efficient (up to a factor of two). Also we can use
the sponge construction with `rate=2`, which in practice means twice as fast.
Questions:
- should we use the [SAFE sponge](https://hackmd.io/bHgsH6mMStCVibM_wYvb2w)
or the original sponge?
- should we use rate 1 or 2? It seems that even `rate=2` gives an approximately
128 bit of collision and preimage security, per standard cryptographic
assumptions; and higher rate means faster hashing.
I propose to use the SAFE convention and `rate=2`. However the current
implementation uses Poseidon1-style sponge.
Parameters
----------
Parameters should be set based on bechmarks and other external constraints,
but already we can have some preliminary targets. If we use a slot Merkle tree
of depth between 16-32, and sponge hash with a rate of 2, then the Merkle
inclusion proof cost will be approximately in balance with the cell hashing
cost if the cell size is 1024-2048 bytes (34-67 field elements).
If we use 2048 byte cells, then `nCells = 8192*8192 = 2^26` gives a slot size
of 128 Gb, which looks like a good compromise target slot size (we don't want
it to be too small, because then the number of slot proofs per node will be
too big; but we don't want it to be too big either, because that's inflexible)
### 2D erasure coding
We need to use 2D erasure coding inside a slot, because while 1D would be better,
the required K,N parameters of the EC would be too big. Furthermore, we don't
want too big storage overhead, so the idea is to use `K ~= 2/3 * N`
(with `N` being a power of two). With such a setting, we can store the
original `K x K` matrix and the small `(N-K) x (N-K)` matrix, and reconstruct
the rest real-time. This particular parameter setting gives us a storage overhead
of `25%` (of course we can tune the parameters, this is just an example).
Note that the EC rate does not affect the proof system itself, only the required
number of samples to achieve a given target detection probability.
With the above setting (EC rate = 2/3), we need 117 samples to achieve 6 nines
of detection probability. Sampling a single 2048 cell with sponge rate 2
means approx 34 Poseidon2 permutation calls, while computing the root of
a depth 26 Merkle path is another 26 such calls. Finally computing the index
needs 2 calls and an extra cost similar to approx 3 calls, so we have about
65 calls per sample, each about 250 constraints. So in total we have about
`117 * 65 * 250 ~= 1.9 million` constraints, or equivalent to hashing about
`235 kb` of data with a binary Merkle tree or with a sponge of rate 1.
Sampling
--------
Given a slot of a dataset, we want to check `nSamples` randomly selected
cells, to see whether they are still stored by the node. We expect `nSamples`
to be in the range 20-200.
To be able to do this, we need to compute:
- the indices of the selected cells (or Merkle leaves)
- the hashes of the selected cells
- the Merkle paths from these hashes up to the slot root (Merkle proofs)
- the (single) Merkle path from the slot root to the dataset root.
To be able to sample randomly, we need some external source of entropy; for
this, presumably a block hash of some public blockchain (eg. Ethereum) will
be used. It can be convenient to have the entropy in the form a field element;
for this we can simply take the block hash `modulo r`. While this gives a
somewhat non-uniform probability distribution, in practice this should not
cause any issue. Alternatively, we could just keep 31 bytes of the block hash and
interpret it as a field element, giving 248 bits of uniform entropy.
We propose the following function to compute the indices of the selected cells:
idx = H( entropy | slotRoot | counter ) `mod` nCells
where `counter` iterates over the range `[1..nSamples]`, `H` is our hash
function, and `|` denotes concatenation.
Circuit
-------
For the MVP, we build a monolithic circuit / R1CS instance for proving all
the samples in single slot; then use Groth16 to prove it.
Public inputs:
- dataset root
- entropy
- slot index: which slot of the dataset we are talking about; `[1..nSlots]`
Private inputs:
- the slot root
- the underlying data of the cells, as sequences of field elements
- the Merkle paths from the leaves (the cell hashes) to the slot root
- the Merkle path from the slot root to the dataset root
Computation:
- compute the cell indices from the slot root and the entropy
- compute the cell hashes from the cell data
- from the cell hashes, using the provided Merkle paths, recompute the slot root
- compare the reconstructed slot root to the slot root given as private input
- from the slot root, using the provided Merkle path, recompute and check the
dataset root
Note that given the index of a leaf, we can compute the left-right zig-zag
of the corresponding Merkle path, simply by looking at the binary decomposition.
So the Merkle paths will only consist lists of hashes.

1
circuit/.gitignore vendored Normal file
View File

@ -0,0 +1 @@
build

21
circuit/README.md Normal file
View File

@ -0,0 +1,21 @@
Storage proof `circom` circuit
------------------------------
See the [README in the parent dir](../README.md) for the (draft) specification.
### Organization of the circuit code
- `slot_main.circom` - main component, generated by tests
- `sample_cells.circom` - compute cell indices to sample, prove sampled cells
- `single_cell.circom` - prove a single cell
- `extract_bits.circom` - extract lower bits of the *standard representation* of a field element
- `binary_compare.circom` - compare numbers given in binary representation (the point is that they can be bigger than the field size!)
- `misc.circom` - miscellaneous helper funtions
- `poseidon2_hash.circom` - compute Poseidon2 hash with sponge construction
- `poseidon2_sponge.circom` - generic sponge construction
- `poseidon2_merkle.circom` - compute Poseidon2 Merkle root
- `poseidon2_perm.circom` - the Poseidon2 permutation

96
circuit/binary_compare.circom Normal file
View File

@ -0,0 +1,96 @@
pragma circom 2.0.0;
//------------------------------------------------------------------------------
//
// given two numbers in `n`-bit binary decomposition (little-endian), we compute
//
// / -1 if A < B
// out := { 0 if A == B
// \ +1 if A > B
//
// NOTE: we don't check that the digits are indeed binary;
// that's the responsibility of the caller!
//
// This version uses `(3*n-1)` nonlinear constraints.
// Question: can we do better? (note that this has to work with n >= 254 digits too!)
//
template BinaryCompare(n) {
signal input A[n];
signal input B[n];
signal output out;
signal eq[n];
signal aux[n];
signal jump[n+1];
jump[n] <== 1;
var sum = 0;
for(var k=n-1; k>=0; k--) {
var y = A[k] - B[k];
eq[k] <== 1 - y*y; // (A[k] == B[k]) ? 1 : 0
jump[k] <== eq[k] * jump[k+1]; // this jumps from 1 to 0 at the highest inequal digit
aux[k] <== (jump[k+1] - jump[k]) * y; // where we store whether A was greater or less
sum += aux[k];
}
out <== sum;
}
//------------------------------------------------------------------------------
//
// given two numbers in `n`-bit binary decomposition (little-endian), we compute
//
// out := (A <= B) ? 1 : 0
//
// NOTE: we don't check that the digits are indeed binary;
// that's the responsibility of the caller!
//
template BinaryLessOrEqual(n) {
signal input A[n];
signal input B[n];
signal output out;
var phalf = 1/2; // +1/2 as field element
var mhalf = -phalf; // -1/2 as field element
component cmp = BinaryCompare(n);
cmp.A <== A;
cmp.B <== B;
var x = cmp.out;
out <== mhalf * (x-1) * (x+2);
}
//------------------------------------------------------------------------------
//
// given two numbers in `n`-bit binary decomposition (little-endian), we compute
//
// out := (A >= B) ? 1 : 0
//
// NOTE: we don't check that the digits are indeed binary;
// that's the responsibility of the caller!
//
template BinaryGreaterOrEqual(n) {
signal input A[n];
signal input B[n];
signal output out;
var phalf = 1/2; // +1/2 as field element
var mhalf = -phalf; // -1/2 as field element
component cmp = BinaryCompare(n);
cmp.A <== A;
cmp.B <== B;
var x = cmp.out;
out <== mhalf * (x+1) * (x-2);
}
//------------------------------------------------------------------------------

73
circuit/extract_bits.circom Normal file
View File

@ -0,0 +1,73 @@
pragma circom 2.0.0;
include "binary_compare.circom";
include "misc.circom";
//------------------------------------------------------------------------------
//
// extract the lowest `n` bits from a field element.
//
// NOTE: this is rather nontrivial, as everything is computed modulo `r`,
// so naive bit decomposition does not work (there are multiple solutions).
//
template ExtractLowerBits(n) {
signal input inp;
signal output out[n];
// we may have 2 solutions for this
component tb = ToBits(254); // note: 2^253 < r < 2^254
tb.inp <== inp;
// bits of field prime `r` in little-endian order
var primeBits[254] = [1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,1,0,0,1,0,0,1,1,0,1,0,1,1,1,1,1,0,0,0,0,1,1,1,1,1,0,0,0,0,1,0,1,0,0,0,1,0,0,1,0,0,0,0,1,1,1,0,1,0,0,1,1,1,0,1,1,0,0,1,1,1,1,0,0,0,0,1,0,0,1,0,0,0,0,1,0,1,1,1,1,1,0,0,1,1,0,0,0,0,0,1,0,1,0,0,1,0,1,1,1,0,1,0,0,0,0,1,1,0,1,0,1,0,0,0,0,0,0,1,1,0,0,0,0,0,0,1,0,1,1,0,1,1,0,1,1,0,1,0,0,0,1,0,0,0,0,0,1,0,1,0,0,0,0,1,1,1,0,1,1,0,0,1,0,1,0,0,0,0,0,0,0,1,0,1,1,0,0,0,1,1,0,0,1,0,0,0,0,1,1,1,0,1,0,0,1,1,1,0,0,1,1,1,0,0,1,0,0,0,1,0,0,1,1,0,0,0,0,0,1,1];
// enforce that the binary representation is < r
component le = BinaryCompare(254);
le.A <== tb.out;
le.B <== primeBits;
le.out === -1; // enforce `A < B`, that is, `bits < prime`
// extract the lowest `n` bits
for(var i=0; i<n; i++) {
tb.out[i] ==> out[i];
}
}
//------------------------------------------------------------------------------
//
// a version of the above specialized to the test field `p = 65537`
//
// this is used only for testing using the `r1cs-solver` tool
//
template ExtractLowerBits_testfield65537(n) {
signal input inp;
signal output out[n];
// we may have up to 4 solutions for this
component tb = ToBits(18); // note: 2^16 < r < 2^18
tb.inp <== inp;
// bits of field prime `r` in little-endian order
var primeBits[18] = [1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0];
// enforce that the binary representation is < r
component le = BinaryCompare(18);
le.A <== tb.out;
le.B <== primeBits;
le.out === -1; // enforce `A < B`, that is, `bits < prime`
// extract the lowest `n` bits
for(var i=0; i<n; i++) {
tb.out[i] ==> out[i];
}
}
//------------------------------------------------------------------------------

5
circuit/main_test_compare.circom Normal file
View File

@ -0,0 +1,5 @@
pragma circom 2.0.0;
include "binary_compare.circom";
component main {public [A,B]} = BinaryLessOrEqual(8);

62
circuit/misc.circom Normal file
View File

@ -0,0 +1,62 @@
pragma circom 2.0.0;
//------------------------------------------------------------------------------
// compute (compile time) the log2 of a number
function FloorLog2(n) {
return (n==0) ? -1 : (1 + FloorLog2(n>>1));
}
function CeilLog2(n) {
return (n==0) ? 0 : (1 + FloorLog2(n-1));
}
//------------------------------------------------------------------------------
// decompose an n-bit number into bits
template ToBits(n) {
signal input inp;
signal output out[n];
var sum = 0;
for(var i=0; i<n; i++) {
out[i] <-- (inp >> i) & 1;
out[i] * (1-out[i]) === 0;
sum += (1<<i) * out[i];
}
inp === sum;
}
//------------------------------------------------------------------------------
// check equality to zero; that is, compute `(inp==0) ? 1 : 0`
template IsZero() {
signal input inp;
signal output out;
// guess the inverse
signal inv;
inv <-- (inp != 0) ? (1/inp) : 0 ;
// if `inp==0`, then by definition `out==1`
// if `out==0`, then the inverse must must exist, so `inp!=0`
out <== 1 - inp * inv;
// enfore that either `inp` or `out` must be zero
inp*out === 0;
}
//------------------------------------------------------------------------------
// check equality of two field elements; that is, computes `(A==B) ? 1 : 0`
template IsEqual() {
signal input A,B;
signal output out;
component isz = IsZero();
isz.in <== A - B;
isz.out ==> out;
}
//------------------------------------------------------------------------------

32
circuit/poseidon2_hash.circom Normal file
View File

@ -0,0 +1,32 @@
pragma circom 2.0.0;
include "poseidon2_sponge.circom";
//------------------------------------------------------------------------------
// Hash `n` field elements into 1, with approximately 127-254 bits of preimage security
// Note that the output size must be at least twice than the desired security level (?)
// (assuming bn128 scalar field. We use capacity=2, rate=1, t=3).
template Poseidon2_hash_rate1(n) {
signal input inp[n];
signal output out;
component sponge = PoseidonSponge(3,2,n,1);
sponge.inp <== inp;
sponge.out[0] ==> out;
}
//------------------------------------------------------------------------------
// Hash `n` field elements into 1, with approximately 127 bits of preimage security
// (assuming bn128 scalar field. We use capacity=1, rate=2, t=3).
template Poseidon2_hash_rate2(n) {
signal input inp[n];
signal output out;
component sponge = PoseidonSponge(3,1,n,1);
sponge.inp <== inp;
sponge.out[0] ==> out;
}
//------------------------------------------------------------------------------

46
circuit/poseidon2_merkle.circom Normal file
View File

@ -0,0 +1,46 @@
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;
}
//------------------------------------------------------------------------------

217
circuit/poseidon2_perm.circom Normal file
View File

@ -0,0 +1,217 @@
pragma circom 2.0.0;
//
// The Poseidon2 permutation for bn128 and t=3
//
//------------------------------------------------------------------------------
// The S-box
template SBox() {
signal input inp;
signal output out;
signal x2 <== inp*inp;
signal x4 <== x2*x2;
out <== inp*x4;
}
//------------------------------------------------------------------------------
// partial or internal round
template InternalRound(i) {
signal input inp[3];
signal output out[3];
var round_consts[56] =
[ 0x15ce7e5ae220e8623a40b3a3b22d441eff0c9be1ae1d32f1b777af84eea7e38c
, 0x1bf60ac8bfff0f631983c93e218ca0d4a4059c254b4299b1d9984a07edccfaf0
, 0x0fab0c9387cb2bec9dc11b2951088b9e1e1d2978542fc131f74a8f8fdac95b40
, 0x07d085a48750738019784663bccd460656dc62c1b18964a0d27a5bd0c27ee453
, 0x10d57b1fad99da9d3fe16cf7f5dae05be844f67b2e7db3472a2e96e167578bc4
, 0x0c36c40f7bd1934b7d5525031467aa39aeaea461996a70eda5a2a704e1733bb0
, 0x0e4b65a0f3e1f9d3166a2145063c999bd08a4679676d765f4d11f97ed5c080ae
, 0x1ce5561061120d5c7ea09da2528c4c041b9ad0f05d655f38b10d79878b69f29d
, 0x2d323f651c3da8f0e0754391a10fa111b25dfa00471edf5493c44dfc3f28add6
, 0x05a0741ee5bdc3e099fd6bdad9a0865bc9ceecd13ea4e702e536dd370b8f1953
, 0x176a2ec4746fc0e0eca9e5e11d6facaee05524a92e5785c8b8161780a4435136
, 0x0691faf0f42a9ed97629b1ae0dc7f1b019c06dd852cb6efe57f7eeb1aa865aef
, 0x0e46cf138dad09d61b9a7cab95a23b5c8cb276874f3715598bacb55d5ad271de
, 0x0f18c3d95bac1ac424160d240cdffc2c44f7b6315ba65ed3ff2eff5b3e48b4f2
, 0x2eea6af14b592ec45a4119ac1e6e6f0312ecd090a096e340d472283e543ddff7
, 0x06b0d7a8f4ce97d049ae994139f5f71dca4899d4f1cd3dd83a32a89a58c0a8e6
, 0x019df0b9828eed5892dd55c1ad6408196f6293d600ef4491703a1b37e119ba8e
, 0x08ca5e3c93817cdb1c2b2a12d02c779d74c1bb12b6668f3ab3ddd7837f3a4a00
, 0x28382d747e3fd6cb2e0d8e8edd79c5313eed307a3517c11046245b1476e4f701
, 0x0ca89aecd5675b77c8271765da98cfcb6875b3053d4742c9ff502861bd16ad28
, 0x19046bc0b03ca90802ec83f212001e7ffd7f9224cfffae523451deb52eab3787
, 0x036fd7dfa1c05110b3428e6abcc43e1de9abba915320c4a600f843bfb676ca51
, 0x08f0a7abcb1a2f6595a9b7380c5028e3999db4fe5cb21892e5bb5cb11a7757ba
, 0x0b614acc1ce3fbe9048f8385e4ee24c3843deea186bacea3c904c9f6340ad8cb
, 0x00b2d98c5d988f9b41f2c98e017fc954a6ae423b2261575941f8eac8835d985c
, 0x1457f18555b7973ba5b311d57ec5d77e936980b97f5973875f1f7cc765a4fc95
, 0x002b453debc1bee525cb751bc10641a6b86f847d696418cf1144950982591bfa
, 0x0c2af1abcc6ece77218315d2af445ccbfc6647b7af2510682882cc792c6bb8cf
, 0x0e2825d9eb84b59902a1adb49ac0c2c291dee7c45d2e8c30369a4d595039e8ad
, 0x297e2e86a8c672d39f3343b8dfce7a6f20f3571bfd5c8a28e3905aa2dcfeca44
, 0x00d397281d902e49ec6504ba9186e806db9ad4fc8f86e7277aa7f1467eb6f9de
, 0x2fb7c89c372d7e2050e7377ed471000c73544a2b9fd66557f3577c09cac98b4b
, 0x16125247be4387a8c3e62490167f0cffdba02eda4f018d0b40639a13bb0cfef9
, 0x2291fd9d442f2d9b97ab22f7d4d52c2a82e41f852cf620b144612650a39e26e8
, 0x1eec61f16a275ae238540feaeeadfec56d32171b1cc393729d06f37f476fde71
, 0x259ce871ba5dacbb48d8aed3d8513eef51558dc0b360f28c1a15dbfc5e7f6ca2
, 0x2d3376a14ddbf95587e2f7567ff04fe13a3c7cb17363c8b9c5dd1d9262a210cb
, 0x13b843d9f65f4cddd7ce10d9cad9b8b99ac5e9a8c4269288173a91c0f3c3b084
, 0x0b52e9b2f1aa9fd204e4a42c481cc76c704783e34114b8e93e026a50fa9764e8
, 0x1fd083229276c7f27d3ad941476b394ff37bd44d3a1e9caca1400d9077a2056c
, 0x22743c328a6283f3ba7379af22c684c498568fd7ad9fad5151368c913197cbd9
, 0x043007aefd9741070d95caaaba0c1b070e4eec8eef8c1e512c8e579c6ed64f76
, 0x17ab175144f64bc843074f6b3a0c57c5dd2c954af8723c029ee642539496a7b3
, 0x2befcad3d53fba5eeef8cae9668fed5c1e9e596a46e8458e218f7a665fddf4eb
, 0x15151c4116d97de74bfa6ca3178f73c8fe8fe612c70c6f85a7a1551942cb71cc
, 0x2ac40bf6c3176300a6835d5fc7cc4fd5e5d299fb1baa86487268ec1b9eedfa97
, 0x0f151de1f01b4e24ffe04279318f0a68efabb485188f191e37e6915ff6059f6e
, 0x2e43dffc34537535182aebac1ad7bf0a5533b88f65f9652f0ad584e2ffc4dd1f
, 0x2ebabc2c37ef53d8b13b24a2a2b729d536735f58956125a3876da0664c2442d7
, 0x0dc3beceb34e49f5ad7226dd202c5cf879dffcc9a6dd32a300e8f2a4b59edf03
, 0x2f1ddeccce83adf68779c53b639871a8f81d4d00aefe1e812efce8ec999d457d
, 0x1f63e41280ff5c021715d52b19780298ed8bd3d5eb506316b527e24149d4d4f1
, 0x1b8c1252a5888f8cb2672effb5df49c633d3fd7183271488a1c40d0f88e7636e
, 0x0f45697130f5498e2940568ef0d5e9e16b1095a6cdbb6411df20a973c605e70b
, 0x0780ccc403cdd68983acbd34cda41cacfb2cf911a93076bc25587b4b0aed4929
, 0x238d26ca97c691591e929f32199a643550f325f23a85d420080b289d7cecc9d4
];
component sb = SBox();
sb.inp <== inp[0] + round_consts[i];
out[0] <== 2*sb.out + inp[1] + inp[2];
out[1] <== sb.out + 2*inp[1] + inp[2];
out[2] <== sb.out + inp[1] + 3*inp[2];
}
//------------------------------------------------------------------------------
// external rounds
template ExternalRound(i) {
signal input inp[3];
signal output out[3];
var round_consts[8][3] =
[ [ 0x2c4c51fd1bb9567c27e99f5712b49e0574178b41b6f0a476cddc41d242cf2b43
, 0x1c5f8d18acb9c61ec6fcbfcda5356f1b3fdee7dc22c99a5b73a2750e5b054104
, 0x2d3c1988b4541e4c045595b8d574e98a7c2820314a82e67a4e380f1c4541ba90
]
, [ 0x052547dc9e6d936cab6680372f1734c39f490d0cb970e2077c82f7e4172943d3
, 0x29d967f4002adcbb5a6037d644d36db91f591b088f69d9b4257694f5f9456bc2
, 0x0350084b8305b91c426c25aeeecafc83fc5feec44b9636cb3b17d2121ec5b88a
]
, [ 0x1815d1e52a8196127530cc1e79f07a0ccd815fb5d94d070631f89f6c724d4cbe
, 0x17b5ba882530af5d70466e2b434b0ccb15b7a8c0138d64455281e7724a066272
, 0x1c859b60226b443767b73cd1b08823620de310bc49ea48662626014cea449aee
]
, [ 0x1b26e7f0ac7dd8b64c2f7a1904c958bb48d2635478a90d926f5ff2364effab37
, 0x2da7f36850e6c377bdcdd380efd9e7c419555d3062b0997952dfbe5c54b1a22e
, 0x17803c56450e74bc6c7ff97275390c017f682db11f3f4ca6e1f714efdfb9bd66
]
, [ 0x25672a14b5d085e31a30a7e1d5675ebfab034fb04dc2ec5e544887523f98dede
, 0x0cf702434b891e1b2f1d71883506d68cdb1be36fa125674a3019647b3a98accd
, 0x1837e75235ff5d112a5eddf7a4939448748339e7b5f2de683cf0c0ae98bdfbb3
]
, [ 0x1cd8a14cff3a61f04197a083c6485581a7d836941f6832704837a24b2d15613a
, 0x266f6d85be0cef2ece525ba6a54b647ff789785069882772e6cac8131eecc1e4
, 0x0538fde2183c3f5833ecd9e07edf30fe977d28dd6f246d7960889d9928b506b3
]
, [ 0x07a0693ff41476abb4664f3442596aa8399fdccf245d65882fce9a37c268aa04
, 0x11eb49b07d33de2bd60ea68e7f652beda15644ed7855ee5a45763b576d216e8e
, 0x08f8887da6ce51a8c06041f64e22697895f34bacb8c0a39ec12bf597f7c67cfc
]
, [ 0x2a912ec610191eb7662f86a52cc64c0122bd5ba762e1db8da79b5949fdd38092
, 0x2031d7fd91b80857aa1fef64e23cfad9a9ba8fe8c8d09de92b1edb592a44c290
, 0x0f81ebce43c47711751fa64d6c007221016d485641c28c507d04fd3dc7fba1d2
]
];
component sb[3];
for(var j=0; j<3; j++) {
sb[j] = SBox();
sb[j].inp <== inp[j] + round_consts[i][j];
}
out[0] <== 2*sb[0].out + sb[1].out + sb[2].out;
out[1] <== sb[0].out + 2*sb[1].out + sb[2].out;
out[2] <== sb[0].out + sb[1].out + 2*sb[2].out;
}
//------------------------------------------------------------------------------
// the initial linear layer
template LinearLayer() {
signal input inp[3];
signal output out[3];
out[0] <== 2*inp[0] + inp[1] + inp[2];
out[1] <== inp[0] + 2*inp[1] + inp[2];
out[2] <== inp[0] + inp[1] + 2*inp[2];
}
//------------------------------------------------------------------------------
// the Poseidon2 permutation for t=3
template Permutation() {
signal input inp[3];
signal output out[3];
signal aux[65][3];
component ll = LinearLayer();
for(var j=0; j<3; j++) { ll.inp[j] <== inp[j]; }
for(var j=0; j<3; j++) { ll.out[j] ==> aux[0][j]; }
component ext[8];
for(var k=0; k<8; k++) { ext[k] = ExternalRound(k); }
component int[56];
for(var k=0; k<56; k++) { int[k] = InternalRound(k); }
// first 4 external rounds
for(var k=0; k<4; k++) {
for(var j=0; j<3; j++) { ext[k].inp[j] <== aux[k ][j]; }
for(var j=0; j<3; j++) { ext[k].out[j] ==> aux[k+1][j]; }
}
// the 56 internal rounds
for(var k=0; k<56; k++) {
for(var j=0; j<3; j++) { int[k].inp[j] <== aux[k+4][j]; }
for(var j=0; j<3; j++) { int[k].out[j] ==> aux[k+5][j]; }
}
// last 4 external rounds
for(var k=0; k<4; k++) {
for(var j=0; j<3; j++) { ext[k+4].inp[j] <== aux[k+60][j]; }
for(var j=0; j<3; j++) { ext[k+4].out[j] ==> aux[k+61][j]; }
}
for(var j=0; j<3; j++) { out[j] <== aux[64][j]; }
}
//------------------------------------------------------------------------------
// the "compression function" takes 2 field elements as input and produces
// 1 field element as output. It is a trivial application of the permutation.
template Compression() {
signal input inp[2];
signal output out;
component perm = Permutation();
perm.inp[0] <== inp[0];
perm.inp[1] <== inp[1];
perm.inp[2] <== 0;
perm.out[0] ==> out;
}
//------------------------------------------------------------------------------

96
circuit/poseidon2_sponge.circom Normal file
View File

@ -0,0 +1,96 @@
pragma circom 2.0.0;
include "poseidon2_perm.circom";
//------------------------------------------------------------------------------
function min(a,b) {
return (a <= b) ? a : b;
}
//------------------------------------------------------------------------------
//
// Poseidon sponge construction
//
// t = size of state (currently fixed to 3)
// c = capacity (1 or 2)
// r = rate = t - c
//
// everything is measured in number of field elements
//
// we use the padding `10*` from the original Poseidon paper,
// and initial state constant zero. Note that this is different
// from the "SAFE padding" recommended in the Poseidon2 paper
// (which uses `0*` padding and a nontrivial initial state)
//
template PoseidonSponge(t, capacity, input_len, output_len) {
var rate = t - capacity;
assert( t == 3);
assert( capacity > 0 );
assert( rate > 0 );
assert( capacity < t );
assert( rate < t );
signal input inp[ input_len];
signal output out[output_len];
// round up to rate the input + 1 field element ("10*" padding)
var nblocks = ((input_len + 1) + (rate-1)) \ rate;
var nout = (output_len + (rate-1)) \ rate;
var padded_len = nblocks * rate;
signal padded[padded_len];
for(var i=0; i<input_len; i++) { padded[i] <== inp[i]; }
padded[input_len ] <== 1;
for(var i=input_len+1; i<padded_len; i++) { padded[i] <== 0; }
signal state [nblocks+nout][t ];
signal sorbed[nblocks ][rate];
// initialize state
for(var i=0; i<t; i++) { state[0][i] <== 0; }
component absorb [nblocks];
component squeeze[nout-1];
for(var m=0; m<nblocks; m++) {
for(var i=0; i<rate; i++) {
var a = state [m][i];
var b = padded[m*rate+i];
sorbed[m][i] <== a + b;
}
absorb[m] = Permutation();
for(var j=0 ; j<rate; j++) { absorb[m].inp[j] <== sorbed[m][j]; }
for(var j=rate; j<t ; j++) { absorb[m].inp[j] <== state [m][j]; }
absorb[m].out ==> state[m+1];
}
var q = min(rate, output_len);
for(var i=0; i<q; i++) {
state[nblocks][i] ==> out[i];
}
var out_ptr = rate;
for(var n=1; n<nout; n++) {
squeeze[n-1] = Permutation();
squeeze[n-1].inp <== state[nblocks+n-1];
squeeze[n-1].out ==> state[nblocks+n ];
var q = min(rate, output_len-out_ptr);
for(var i=0; i<q; i++) {
state[nblocks+n][i] ==> out[out_ptr+i];
}
out_ptr += rate;
}
}
//------------------------------------------------------------------------------

119
circuit/sample_cells.circom Normal file
View File

@ -0,0 +1,119 @@
pragma circom 2.0.0;
include "single_cell.circom";
include "poseidon2_hash.circom";
include "extract_bits.circom";
include "misc.circom";
//------------------------------------------------------------------------------
//
// calculate the linear index of the k-th cell we want to sample.
// this version return the binary decomposition of the index
// (we need that for the Merkle proof anyway, it's cheaper this way)
//
// the formula for this is:
//
// idx = H( entropy | slotRoot | counter ) `mod` nCells
//
// NOTE: we assume `nCells` is a power of two.
//
template CalculateCellIndexBits( nCells ) {
var log2N = CeilLog2(nCells);
assert( nCells == (1<<log2N) );
signal input entropy;
signal input slotRoot;
signal input counter;
signal output indexBits[log2N];
// calculate the hash
component pos = Poseidon2_hash_rate2(3);
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);
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];
}
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.
//
template SampleAndProveV1( nCells, nFieldElemsPerCell, nSamples ) {
var log2N = CeilLog2(nCells);
assert( nCells == (1<<log2N) );
signal input entropy; // public input
signal input slotRoot; // public input
signal input cellData[nSamples][nFieldElemsPerCell]; // private input
signal input merklePaths[nSamples][log2N]; // private input
component calci[nSamples];
component prove[nSamples];
for(var cnt=0; cnt<nSamples; cnt++) {
calci[cnt] = CalculateCellIndexBits( nCells );
prove[cnt] = ProveSingleCell( nFieldElemsPerCell, log2N );
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].data <== cellData[cnt];
prove[cnt].merklePath <== merklePaths[cnt];
}
}
//------------------------------------------------------------------------------

128
circuit/single_cell.circom Normal file
View File

@ -0,0 +1,128 @@
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)
// - 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)
//
// 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
//
// NOTE: we don't check whether the bits are really bits, that's the
// responsability of the caller!
//
template ProveSingleCell( nFieldElemsPerCell, merkleDepth ) {
signal input slotRoot;
signal input data[ nFieldElemsPerCell ];
signal input indexBits [ merkleDepth ];
signal input merklePath[ merkleDepth ];
// this will reconstruct the Merkle path up to the slot root
component path = MerklePathBits( merkleDepth );
path.pathBits <== indexBits;
path.merklePath <== merklePath;
// compute the cell hash
component hash = Poseidon2_hash_rate2( nFieldElemsPerCell );
hash.inp <== data;
hash.out ==> path.leaf;
// check if the reconstructed root matches the actual slot root
path.recRoot === slotRoot;
}
//------------------------------------------------------------------------------

3
circuit/slot_main.circom Normal file
View File

@ -0,0 +1,3 @@
pragma circom 2.0.0;
include "sample_cells.circom";
component main {public [entropy,slotRoot]} = SampleAndProveV1(1024, 9, 20);

14
circuit/test_compare.sh Executable file
View File

@ -0,0 +1,14 @@
#!/bin/bash
NAME="main_test_compare"
INPUT="input_test_compare"
cd build
circom ../${NAME}.circom --r1cs --wasm || { echo "circom failed"; exit 102; }
echo "{ \"A\":[1,1,1,0,1,1,0,1], \"B\":[1,1,1,0,1,1,0,1] }" >${INPUT}.json
echo "generating witness... (WASM)"
cd ${NAME}_js
node generate_witness.js ${NAME}.wasm ../${INPUT}.json ../${NAME}_witness.wtns || { echo "witness gen failed"; exit 101; }
cd ..

21
circuit/test_slotmain.sh Executable file
View File

@ -0,0 +1,21 @@
#!/bin/bash
ORIG=`pwd`
cd ../reference/haskell
runghc testMain.hs || { echo "ghc failed"; exit 101; }
mv input_example.json ${ORIG}/build/
mv slot_main.circom ${ORIG}
cd ${ORIG}/build
NAME="slot_main"
circom ../${NAME}.circom --r1cs --wasm || { echo "circom failed"; 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; }
cd ..
cd $ORIG

7
reference/README.md Normal file
View File

@ -0,0 +1,7 @@
Reference implementations
-------------------------
Computing cell hashes, slot root, and producing Merkle proofs for small
amount of fake data.

1
reference/haskell/.gitignore vendored Normal file
View File

@ -0,0 +1 @@
*.json

23
reference/haskell/Poseidon2.hs Normal file
View File

@ -0,0 +1,23 @@
-- | Poseidon2 hash function for the bn128 curve's scalar field and t=3.
module Poseidon2
( Fr
, sponge1 , sponge2
, calcMerkleRoot , calcMerkleTree
, MerkleTree(..) , depthOf , merkleRootOf
, MerkleProof(..) , extractMerkleProof , extractMerkleProof_ , reconstructMerkleRoot
, compression
, permutation
)
where
--------------------------------------------------------------------------------
import ZK.Algebra.Curves.BN128.Fr.Mont (Fr)
import Poseidon2.Sponge
import Poseidon2.Merkle
import Poseidon2.Permutation
--------------------------------------------------------------------------------

24
reference/haskell/Poseidon2/Example.hs Normal file
View File

@ -0,0 +1,24 @@
module Ref.Poseidon2.Example where
--------------------------------------------------------------------------------
import ZK.Algebra.Curves.BN128.Fr.Mont (Fr)
import Poseidon2.Permutation
--------------------------------------------------------------------------------
-- BN254 example test vector
exInput, exOutput :: (Fr,Fr,Fr)
exInput = (0,1,2)
exOutput =
( 0x30610a447b7dec194697fb50786aa7421494bd64c221ba4d3b1af25fb07bd103
, 0x13f731d6ffbad391be22d2ac364151849e19fa38eced4e761bcd21dbdc600288
, 0x1433e2c8f68382c447c5c14b8b3df7cbfd9273dd655fe52f1357c27150da786f
)
kats :: Bool
kats = permutation exInput == exOutput
--------------------------------------------------------------------------------

118
reference/haskell/Poseidon2/Merkle.hs Normal file
View File

@ -0,0 +1,118 @@
-- | Merkle tree built from Poseidon2 permutation
{-# LANGUAGE BangPatterns #-}
module Poseidon2.Merkle where
--------------------------------------------------------------------------------
import Data.Array
import Data.Bits
import ZK.Algebra.Curves.BN128.Fr.Mont (Fr)
import Poseidon2.Permutation
-- import Debug.Trace
-- debug s x y = trace (s ++ " ~> " ++ show x) y
--------------------------------------------------------------------------------
-- | A Merkle tree.
--
-- Note the first layer is the bottom (widest) layer, and the last layer is the top (root).
--
newtype MerkleTree
= MkMerkleTree (Array Int (Array Int Fr))
deriving Show
merkleRootOf :: MerkleTree -> Fr
merkleRootOf (MkMerkleTree outer)
| c == d = inner ! c
| otherwise = error "merkleRootOf: topmost layer is not singleton"
where
(a,b) = bounds outer
inner = outer ! b
(c,d) = bounds inner
-- | @log2( number-of-leaves )@.
--
-- NOTE: this is one less than the actual number of layers!
--
depthOf :: MerkleTree -> Int
depthOf (MkMerkleTree outer) = b-a where
(a,b) = bounds outer
calcMerkleTree' :: [Fr] -> [[Fr]]
calcMerkleTree' = go where
go :: [Fr] -> [[Fr]]
go [] = error "calcMerkleTree': input is empty"
go [x] = [[x]]
go xs = xs : go (map compressPair $ pairs xs)
calcMerkleTree :: [Fr] -> MerkleTree
calcMerkleTree = MkMerkleTree . go1 . calcMerkleTree' where
go1 outer = listArray (0, length outer-1) (map go2 outer)
go2 inner = listArray (0, length inner-1) inner
data MerkleProof = MkMerkleProof
{ _leafIndex :: Int
, _leafHash :: Fr
, _merklePath :: [Fr]
}
deriving (Eq,Show)
-- | Returns the leaf and Merkle path of the given leaf
extractMerkleProof :: MerkleTree -> Int -> MerkleProof
extractMerkleProof tree@(MkMerkleTree outer) idx = MkMerkleProof idx leaf path where
leaf = (outer!0)!idx
depth = depthOf tree
path = worker depth idx
worker 0 0 = []
worker 0 _ = error "extractMerkleProof: this should not happen"
worker level j = this : worker (level-1) (shiftR j 1) where
this = outer ! (depth-level) ! (j `xor` 1)
extractMerkleProof_ :: MerkleTree -> Int -> [Fr]
extractMerkleProof_ tree idx = _merklePath (extractMerkleProof tree idx)
reconstructMerkleRoot :: MerkleProof -> Fr
reconstructMerkleRoot (MkMerkleProof idx leaf path) = go idx leaf path where
go 0 !h [] = h
go !j !h !(p:ps) = case j .&. 1 of
0 -> go (shiftR j 1) (compression h p) ps
1 -> go (shiftR j 1) (compression p h) ps
--------------------------------------------------------------------------------
calcMerkleRoot :: [Fr] -> Fr
calcMerkleRoot = go where
go [] = error "calcMerkleRoot: input is empty"
go [x] = x
go xs = go (map compressPair $ pairs xs)
compressPair :: (Fr,Fr) -> Fr
compressPair (x,y) = compression x y
compression :: Fr -> Fr -> Fr
compression x y = case permutation (x,y,0) of (z,_,_) -> z
pairs :: [Fr] -> [(Fr,Fr)]
pairs [] = []
pairs [x] = (x,x) : []
pairs (x:y:rest) = (x,y) : pairs rest
--------------------------------------------------------------------------------
printExampleMerkleRoots :: IO ()
printExampleMerkleRoots = do
putStrLn $ "Merkle root for [1.. 1] = " ++ show (calcMerkleRoot $ map fromInteger [1.. 1])
putStrLn $ "Merkle root for [1.. 2] = " ++ show (calcMerkleRoot $ map fromInteger [1.. 2])
putStrLn $ "Merkle root for [1.. 4] = " ++ show (calcMerkleRoot $ map fromInteger [1.. 4])
putStrLn $ "Merkle root for [1.. 16] = " ++ show (calcMerkleRoot $ map fromInteger [1.. 16])
putStrLn $ "Merkle root for [1.. 64] = " ++ show (calcMerkleRoot $ map fromInteger [1.. 64])
putStrLn $ "Merkle root for [1.. 256] = " ++ show (calcMerkleRoot $ map fromInteger [1.. 256])
putStrLn $ "Merkle root for [1..1024] = " ++ show (calcMerkleRoot $ map fromInteger [1..1024])
--------------------------------------------------------------------------------

47
reference/haskell/Poseidon2/Permutation.hs Normal file
View File

@ -0,0 +1,47 @@
-- | The Poseidon2 permutation
module Poseidon2.Permutation where
--------------------------------------------------------------------------------
import ZK.Algebra.Curves.BN128.Fr.Mont (Fr)
import Poseidon2.RoundConsts
--------------------------------------------------------------------------------
sbox :: Fr -> Fr
sbox x = x4*x where
x2 = x *x
x4 = x2*x2
internalRound :: Fr -> (Fr,Fr,Fr) -> (Fr,Fr,Fr)
internalRound c (x,y,z) =
( 2*x' + y + z
, x' + 2*y + z
, x' + y + 3*z
)
where
x' = sbox (x + c)
externalRound :: (Fr,Fr,Fr) -> (Fr,Fr,Fr) -> (Fr,Fr,Fr)
externalRound (cx,cy,cz) (x,y,z) = (x'+s , y'+s , z'+s) where
x' = sbox (x + cx)
y' = sbox (y + cy)
z' = sbox (z + cz)
s = x' + y' + z'
linearLayer :: (Fr,Fr,Fr) -> (Fr,Fr,Fr)
linearLayer (x,y,z) = (x+s, y+s, z+s) where s = x+y+z
--------------------------------------------------------------------------------
permutation :: (Fr,Fr,Fr) -> (Fr,Fr,Fr)
permutation
= (\state -> foldl (flip externalRound) state finalRoundConsts )
. (\state -> foldl (flip internalRound) state internalRoundConsts)
. (\state -> foldl (flip externalRound) state initialRoundConsts )
. linearLayer
--------------------------------------------------------------------------------

131
reference/haskell/Poseidon2/RoundConsts.hs Normal file
View File

@ -0,0 +1,131 @@
-- | BN256 prime, and t = 3
module Poseidon2.RoundConsts where
--------------------------------------------------------------------------------
import ZK.Algebra.Curves.BN128.Fr.Mont
--------------------------------------------------------------------------------
{-
matDiag3 :: [[Fr]]
matDiag3 =
[ [1,0,0]
, [0,1,0]
, [0,0,2]
]
matInternal3 :: [[Fr]]
matInternal3 =
[ [2,1,1]
, [1,2,1]
, [1,1,3]
]
-}
--------------------------------------------------------------------------------
initialRoundConsts :: [(Fr,Fr,Fr)]
initialRoundConsts =
[ ( 0x2c4c51fd1bb9567c27e99f5712b49e0574178b41b6f0a476cddc41d242cf2b43
, 0x1c5f8d18acb9c61ec6fcbfcda5356f1b3fdee7dc22c99a5b73a2750e5b054104
, 0x2d3c1988b4541e4c045595b8d574e98a7c2820314a82e67a4e380f1c4541ba90
)
, ( 0x052547dc9e6d936cab6680372f1734c39f490d0cb970e2077c82f7e4172943d3
, 0x29d967f4002adcbb5a6037d644d36db91f591b088f69d9b4257694f5f9456bc2
, 0x0350084b8305b91c426c25aeeecafc83fc5feec44b9636cb3b17d2121ec5b88a
)
, ( 0x1815d1e52a8196127530cc1e79f07a0ccd815fb5d94d070631f89f6c724d4cbe
, 0x17b5ba882530af5d70466e2b434b0ccb15b7a8c0138d64455281e7724a066272
, 0x1c859b60226b443767b73cd1b08823620de310bc49ea48662626014cea449aee
)
, ( 0x1b26e7f0ac7dd8b64c2f7a1904c958bb48d2635478a90d926f5ff2364effab37
, 0x2da7f36850e6c377bdcdd380efd9e7c419555d3062b0997952dfbe5c54b1a22e
, 0x17803c56450e74bc6c7ff97275390c017f682db11f3f4ca6e1f714efdfb9bd66
)
]
internalRoundConsts :: [Fr]
internalRoundConsts =
[ 0x15ce7e5ae220e8623a40b3a3b22d441eff0c9be1ae1d32f1b777af84eea7e38c
, 0x1bf60ac8bfff0f631983c93e218ca0d4a4059c254b4299b1d9984a07edccfaf0
, 0x0fab0c9387cb2bec9dc11b2951088b9e1e1d2978542fc131f74a8f8fdac95b40
, 0x07d085a48750738019784663bccd460656dc62c1b18964a0d27a5bd0c27ee453
, 0x10d57b1fad99da9d3fe16cf7f5dae05be844f67b2e7db3472a2e96e167578bc4
, 0x0c36c40f7bd1934b7d5525031467aa39aeaea461996a70eda5a2a704e1733bb0
, 0x0e4b65a0f3e1f9d3166a2145063c999bd08a4679676d765f4d11f97ed5c080ae
, 0x1ce5561061120d5c7ea09da2528c4c041b9ad0f05d655f38b10d79878b69f29d
, 0x2d323f651c3da8f0e0754391a10fa111b25dfa00471edf5493c44dfc3f28add6
, 0x05a0741ee5bdc3e099fd6bdad9a0865bc9ceecd13ea4e702e536dd370b8f1953
, 0x176a2ec4746fc0e0eca9e5e11d6facaee05524a92e5785c8b8161780a4435136
, 0x0691faf0f42a9ed97629b1ae0dc7f1b019c06dd852cb6efe57f7eeb1aa865aef
, 0x0e46cf138dad09d61b9a7cab95a23b5c8cb276874f3715598bacb55d5ad271de
, 0x0f18c3d95bac1ac424160d240cdffc2c44f7b6315ba65ed3ff2eff5b3e48b4f2
, 0x2eea6af14b592ec45a4119ac1e6e6f0312ecd090a096e340d472283e543ddff7
, 0x06b0d7a8f4ce97d049ae994139f5f71dca4899d4f1cd3dd83a32a89a58c0a8e6
, 0x019df0b9828eed5892dd55c1ad6408196f6293d600ef4491703a1b37e119ba8e
, 0x08ca5e3c93817cdb1c2b2a12d02c779d74c1bb12b6668f3ab3ddd7837f3a4a00
, 0x28382d747e3fd6cb2e0d8e8edd79c5313eed307a3517c11046245b1476e4f701
, 0x0ca89aecd5675b77c8271765da98cfcb6875b3053d4742c9ff502861bd16ad28
, 0x19046bc0b03ca90802ec83f212001e7ffd7f9224cfffae523451deb52eab3787
, 0x036fd7dfa1c05110b3428e6abcc43e1de9abba915320c4a600f843bfb676ca51
, 0x08f0a7abcb1a2f6595a9b7380c5028e3999db4fe5cb21892e5bb5cb11a7757ba
, 0x0b614acc1ce3fbe9048f8385e4ee24c3843deea186bacea3c904c9f6340ad8cb
, 0x00b2d98c5d988f9b41f2c98e017fc954a6ae423b2261575941f8eac8835d985c
, 0x1457f18555b7973ba5b311d57ec5d77e936980b97f5973875f1f7cc765a4fc95
, 0x002b453debc1bee525cb751bc10641a6b86f847d696418cf1144950982591bfa
, 0x0c2af1abcc6ece77218315d2af445ccbfc6647b7af2510682882cc792c6bb8cf
, 0x0e2825d9eb84b59902a1adb49ac0c2c291dee7c45d2e8c30369a4d595039e8ad
, 0x297e2e86a8c672d39f3343b8dfce7a6f20f3571bfd5c8a28e3905aa2dcfeca44
, 0x00d397281d902e49ec6504ba9186e806db9ad4fc8f86e7277aa7f1467eb6f9de
, 0x2fb7c89c372d7e2050e7377ed471000c73544a2b9fd66557f3577c09cac98b4b
, 0x16125247be4387a8c3e62490167f0cffdba02eda4f018d0b40639a13bb0cfef9
, 0x2291fd9d442f2d9b97ab22f7d4d52c2a82e41f852cf620b144612650a39e26e8
, 0x1eec61f16a275ae238540feaeeadfec56d32171b1cc393729d06f37f476fde71
, 0x259ce871ba5dacbb48d8aed3d8513eef51558dc0b360f28c1a15dbfc5e7f6ca2
, 0x2d3376a14ddbf95587e2f7567ff04fe13a3c7cb17363c8b9c5dd1d9262a210cb
, 0x13b843d9f65f4cddd7ce10d9cad9b8b99ac5e9a8c4269288173a91c0f3c3b084
, 0x0b52e9b2f1aa9fd204e4a42c481cc76c704783e34114b8e93e026a50fa9764e8
, 0x1fd083229276c7f27d3ad941476b394ff37bd44d3a1e9caca1400d9077a2056c
, 0x22743c328a6283f3ba7379af22c684c498568fd7ad9fad5151368c913197cbd9
, 0x043007aefd9741070d95caaaba0c1b070e4eec8eef8c1e512c8e579c6ed64f76
, 0x17ab175144f64bc843074f6b3a0c57c5dd2c954af8723c029ee642539496a7b3
, 0x2befcad3d53fba5eeef8cae9668fed5c1e9e596a46e8458e218f7a665fddf4eb
, 0x15151c4116d97de74bfa6ca3178f73c8fe8fe612c70c6f85a7a1551942cb71cc
, 0x2ac40bf6c3176300a6835d5fc7cc4fd5e5d299fb1baa86487268ec1b9eedfa97
, 0x0f151de1f01b4e24ffe04279318f0a68efabb485188f191e37e6915ff6059f6e
, 0x2e43dffc34537535182aebac1ad7bf0a5533b88f65f9652f0ad584e2ffc4dd1f
, 0x2ebabc2c37ef53d8b13b24a2a2b729d536735f58956125a3876da0664c2442d7
, 0x0dc3beceb34e49f5ad7226dd202c5cf879dffcc9a6dd32a300e8f2a4b59edf03
, 0x2f1ddeccce83adf68779c53b639871a8f81d4d00aefe1e812efce8ec999d457d
, 0x1f63e41280ff5c021715d52b19780298ed8bd3d5eb506316b527e24149d4d4f1
, 0x1b8c1252a5888f8cb2672effb5df49c633d3fd7183271488a1c40d0f88e7636e
, 0x0f45697130f5498e2940568ef0d5e9e16b1095a6cdbb6411df20a973c605e70b
, 0x0780ccc403cdd68983acbd34cda41cacfb2cf911a93076bc25587b4b0aed4929
, 0x238d26ca97c691591e929f32199a643550f325f23a85d420080b289d7cecc9d4
]
finalRoundConsts :: [(Fr,Fr,Fr)]
finalRoundConsts =
[ ( 0x25672a14b5d085e31a30a7e1d5675ebfab034fb04dc2ec5e544887523f98dede
, 0x0cf702434b891e1b2f1d71883506d68cdb1be36fa125674a3019647b3a98accd
, 0x1837e75235ff5d112a5eddf7a4939448748339e7b5f2de683cf0c0ae98bdfbb3
)
, ( 0x1cd8a14cff3a61f04197a083c6485581a7d836941f6832704837a24b2d15613a
, 0x266f6d85be0cef2ece525ba6a54b647ff789785069882772e6cac8131eecc1e4
, 0x0538fde2183c3f5833ecd9e07edf30fe977d28dd6f246d7960889d9928b506b3
)
, ( 0x07a0693ff41476abb4664f3442596aa8399fdccf245d65882fce9a37c268aa04
, 0x11eb49b07d33de2bd60ea68e7f652beda15644ed7855ee5a45763b576d216e8e
, 0x08f8887da6ce51a8c06041f64e22697895f34bacb8c0a39ec12bf597f7c67cfc
)
, ( 0x2a912ec610191eb7662f86a52cc64c0122bd5ba762e1db8da79b5949fdd38092
, 0x2031d7fd91b80857aa1fef64e23cfad9a9ba8fe8c8d09de92b1edb592a44c290
, 0x0f81ebce43c47711751fa64d6c007221016d485641c28c507d04fd3dc7fba1d2
)
]
--------------------------------------------------------------------------------

40
reference/haskell/Poseidon2/Sponge.hs Normal file
View File

@ -0,0 +1,40 @@
module Poseidon2.Sponge where
--------------------------------------------------------------------------------
import ZK.Algebra.Curves.BN128.Fr.Mont (Fr)
import Poseidon2.Permutation
--------------------------------------------------------------------------------
-- | Sponge construction with rate=1 (capacity=2), zero IV and 10* padding
sponge1 :: [Fr] -> Fr
sponge1 input = go (0,0,0) (pad input) where
pad :: [Fr] -> [Fr]
pad (x:xs) = x : pad xs
pad [] = [1]
go (sx,_ ,_ ) [] = sx
go (sx,sy,sz) (a:as) = go state' as where
state' = permutation (sx+a, sy, sz)
--------------------------------------------------------------------------------
-- | Sponge construction with rate=2 (capacity=1), zero IV and 10* padding
sponge2 :: [Fr] -> Fr
sponge2 input = go (0,0,0) (pad input) where
pad :: [Fr] -> [Fr]
pad (x:y:rest) = x : y : pad rest
pad [x] = [x,1]
pad [] = [1,0]
go (sx,_ ,_ ) [] = sx
go (sx,sy,sz) (a:b:rest) = go state' rest where
state' = permutation (sx+a, sy+b, sz)
--------------------------------------------------------------------------------

101
reference/haskell/Sampling.hs Normal file
View File

@ -0,0 +1,101 @@
module Sampling where
--------------------------------------------------------------------------------
import Control.Monad
import System.IO
import Poseidon2
import Slot
import qualified ZK.Algebra.Curves.BN128.Fr.Mont as Fr
--------------------------------------------------------------------------------
samplingTest :: FilePath -> IO ()
samplingTest fpath = do
let entropy = 123456789 :: Fr
input <- calculateCircuitInput exSlotCfg entropy
exportCircuitInput fpath input
--------------------------------------------------------------------------------
type Entropy = Fr
-- | Given an entropy source, the slot root, and a counter, we compute a
-- cell index to sample
sampleCellIndex :: SlotConfig -> Entropy -> Hash -> Int -> Int
sampleCellIndex cfg entropy slotRoot counter = fromInteger idx where
u = sponge2 [entropy , slotRoot , fromIntegral counter] :: Fr
idx = (Fr.from u) `mod` n :: Integer
n = (fromIntegral $ _nCells cfg) :: Integer
--------------------------------------------------------------------------------
data CircuitInput = MkInput
{ _entropy :: Entropy -- ^ public input
, _slotRoot :: Hash -- ^ public input
, _cellData :: [[Fr]] -- ^ private input
, _merklePaths :: [[Fr]] -- ^ private input
}
deriving Show
-- | Calculate the the inputs for the storage proof circuit
calculateCircuitInput :: SlotConfig -> Entropy -> IO CircuitInput
calculateCircuitInput slotCfg entropy = do
slotTree <- calcSlotTree slotCfg
let slotRoot = merkleRootOf slotTree
let idxs = [ sampleCellIndex slotCfg entropy slotRoot j | j <- [1..(_nSamples slotCfg)] ]
cellData <- forM idxs $ \idx -> (cellDataToFieldElements <$> loadCellData slotCfg idx)
let merklePaths = [ extractMerkleProof_ slotTree idx | idx <- idxs ]
return $ MkInput
{ _entropy = entropy
, _slotRoot = slotRoot
, _cellData = cellData
, _merklePaths = merklePaths
}
-- | Export the inputs of the storage proof circuits in JSON format,
-- which @circom@ can consume.
--
exportCircuitInput :: FilePath -> CircuitInput -> IO ()
exportCircuitInput fpath input = do
h <- openFile fpath WriteMode
hPutStrLn h $ "{ \"entropy\": " ++ show (_entropy input)
hPutStrLn h $ ", \"slotRoot\": " ++ show (_slotRoot input)
hPutStrLn h $ ", \"cellData\": "
hPrintListOfLists h (_cellData input)
hPutStrLn h $ ", \"merklePaths\": "
hPrintListOfLists h (_merklePaths input)
hPutStrLn h $ "}"
hClose h
--------------------------------------------------------------------------------
trueFalses :: [Bool]
trueFalses = True : repeat False
indent :: Int -> String
indent k = replicate k ' '
hPrintList' :: Show a => Handle -> (Bool -> String) -> [a] -> IO ()
hPrintList' h indentation xs = do
forM_ (zip trueFalses xs) $ \(b,x) -> do
hPutStrLn h (indentation b ++ (if b then "[ " else ", ") ++ show x)
hPutStrLn h (indentation False ++ "]")
hPrintList :: Show a => Handle -> Int -> [a] -> IO ()
hPrintList h indentBy xs = hPrintList' h (\_ -> indent indentBy) xs
hPrintListOfLists :: Show a => Handle -> [[a]] -> IO ()
hPrintListOfLists h xss =
do
forM_ (zip trueFalses xss) $ \(b,xs) -> hPrintList' h (myIndentation b) xs
hPutStrLn h (" ]")
where
myIndentation True True = " [ "
myIndentation False True = " , "
myIndentation _ False = " "
--------------------------------------------------------------------------------

130
reference/haskell/Slot.hs Normal file
View File

@ -0,0 +1,130 @@
module Slot where
--------------------------------------------------------------------------------
import Data.Bits
import Data.Word
import Data.ByteString (ByteString)
import qualified Data.ByteString as B
import qualified Data.ByteString.Char8 as C
import Control.Monad
import System.IO
import Poseidon2
--------------------------------------------------------------------------------
type Seed = Int
type CellIdx = Int
type Hash = Fr
data DataSource
= SlotFile FilePath
| FakeData Seed
deriving Show
data SlotConfig = MkSlotCfg
{ _cellSize :: Int -- ^ cell size in bytes
, _nCells :: Int -- ^ number of cells per slot (should be power of two)
, _nSamples :: Int -- ^ how many cells we sample
, _dataSrc :: DataSource -- ^ slot data source
}
deriving Show
-- | Example slot configuration
exSlotCfg :: SlotConfig
exSlotCfg = MkSlotCfg
{ _cellSize = 256
, _nCells = 1024
, _nSamples = 20
, _dataSrc = FakeData 12345
}
fieldElemsPerCell :: SlotConfig -> Int
fieldElemsPerCell cfg = (_cellSize cfg + 30) `div` 31
--------------------------------------------------------------------------------
-- | Writes a @circom@ main component with the given parameters
--
-- > template SampleAndProveV1( nCells, nFieldElemsPerCell, nSamples ) { ... }
--
circomMainComponentV1 :: FilePath -> SlotConfig -> IO ()
circomMainComponentV1 circomFile slotCfg = do
let params = show (_nCells slotCfg)
++ ", " ++ show (fieldElemsPerCell slotCfg)
++ ", " ++ show (_nSamples slotCfg)
writeFile circomFile $ unlines
[ "pragma circom 2.0.0;"
, "include \"sample_cells.circom\";"
, "component main {public [entropy,slotRoot]} = SampleAndProveV1(" ++ params ++ ");"
]
--------------------------------------------------------------------------------
-- * load data
genFakeCell :: SlotConfig -> Seed -> CellIdx -> ByteString
genFakeCell cfg seed1 seed2 = B.pack list where
list = go (_cellSize cfg) 1
go :: Int -> Int -> [Word8]
go 0 _ = []
go cnt state = fromIntegral state' : go (cnt-1) state' where
state' = state*state + seed1*state + (seed2 + 17)
loadCellData :: SlotConfig -> CellIdx -> IO ByteString
loadCellData cfg idx = case _dataSrc cfg of
FakeData seed -> return $ genFakeCell cfg seed idx
SlotFile fname -> do
h <- openBinaryFile fname ReadMode
hSeek h AbsoluteSeek (fromIntegral (_cellSize cfg) * fromIntegral idx)
bs <- B.hGet h (_cellSize cfg)
hClose h
return bs
--------------------------------------------------------------------------------
calcSlotTree :: SlotConfig -> IO MerkleTree
calcSlotTree cfg = calcMerkleTree <$> calcCellHashes cfg
calcCellHashes :: SlotConfig -> IO [Hash]
calcCellHashes cfg = do
forM [0..(_nCells cfg - 1)] $ \idx -> do
cell <- loadCellData cfg idx
return (hashCell cell)
--------------------------------------------------------------------------------
-- | Split bytestring into smaller pieces
splitByteString :: Int -> ByteString -> [ByteString]
splitByteString k = go where
go bs
| B.null bs = []
| otherwise = B.take k bs : go (B.drop k bs)
-- | Chunk a ByteString into a sequence of field elements
cellDataToFieldElements :: ByteString -> [Fr]
cellDataToFieldElements rawdata = map chunkToField pieces where
chunkSize = 31
pieces = splitByteString chunkSize rawdata
-- | Hash a cell
hashCell :: ByteString -> Hash
hashCell rawdata = sponge2 (cellDataToFieldElements rawdata)
chunkToField :: ByteString -> Fr
chunkToField chunk
| B.length chunk <= 31 = fromInteger (chunkToIntegerLE chunk)
| otherwise = error "chunkToField: chunk is too big (expecting at most 31 bytes)"
-- | Interpret a ByteString as an integer (little-endian)
chunkToIntegerLE :: ByteString -> Integer
chunkToIntegerLE chunk = go (B.unpack chunk) where
go [] = 0
go (w:ws) = fromIntegral w + shiftL (go ws) 8
--------------------------------------------------------------------------------

11
reference/haskell/testMain.hs Normal file
View File

@ -0,0 +1,11 @@
module Main where
import Slot
import Sampling
main :: IO ()
main = do
let slotCfg = exSlotCfg
circomMainComponentV1 "slot_main.circom" slotCfg
samplingTest "input_example.json"

61
test/Circuit/BinaryCompare.hs Normal file
View File

@ -0,0 +1,61 @@
module Circuit.BinaryCompare where
--------------------------------------------------------------------------------
import CircuitCommon
--------------------------------------------------------------------------------
-- global parameters
circomFile :: FilePath
circomFile = circuitSourceDir </> "binary_compare.circom"
-- | comparing @n@-bit integers
type GP = Int
mainComponent :: GP -> MainComponent
mainComponent n = MainComponent
{ _templateName = "BinaryCompare"
, _templateParams = [n]
, _publicInputs = ["A","B"]
}
--------------------------------------------------------------------------------
-- test cases and expected semantics
type TestCase = (Integer,Integer)
type Output = Int
cmp :: Integer -> Integer -> Int
cmp a b = case compare a b of
LT -> -1
EQ -> 0
GT -> 1
semantics :: GP -> TestCase -> Expected Output
semantics n (a,b) = Expecting $ cmp a b
testCases :: GP -> [TestCase]
testCases n = [ (a,b) | a<-[0..2^n-1] , b<-[0..2^n-1] ]
--------------------------------------------------------------------------------
-- inputs and outputs
inputs :: GP -> TestCase -> Inputs Name Integer
inputs n (a,b) = Inputs $ toMapping "A" (toBitsLE' n a)
<> toMapping "B" (toBitsLE' n b)
outputs :: Output -> Outputs Name Integer
outputs y = Outputs $ toMapping "out" y
--------------------------------------------------------------------------------
spec :: GP -> TestSpec TestCase Output
spec n = TestSpec circomFile (mainComponent n) (inputs n) outputs (semantics n) (testCases n)
specs :: [ ( GP, TestSpec TestCase Output) ]
specs = [ (n, spec n) | n <- [4,5,7] ]
--------------------------------------------------------------------------------

58
test/Circuit/BinaryGTE.hs Normal file
View File

@ -0,0 +1,58 @@
module Circuit.BinaryGTE where
--------------------------------------------------------------------------------
import CircuitCommon
--------------------------------------------------------------------------------
-- global parameters
circomFile :: FilePath
circomFile = circuitSourceDir </> "binary_compare.circom"
-- | comparing @n@-bit integers
type GP = Int
mainComponent :: GP -> MainComponent
mainComponent n = MainComponent
{ _templateName = "BinaryGreaterOrEqual"
, _templateParams = [n]
, _publicInputs = ["A","B"]
}
--------------------------------------------------------------------------------
-- test cases and expected semantics
type TestCase = (Integer,Integer)
type Output = Bool
cmp :: Integer -> Integer -> Bool
cmp a b = (a >= b)
semantics :: GP -> TestCase -> Expected Output
semantics n (a,b) = Expecting $ cmp a b
testCases :: GP -> [TestCase]
testCases n = [ (a,b) | a<-[0..2^n-1] , b<-[0..2^n-1] ]
--------------------------------------------------------------------------------
-- inputs and outputs
inputs :: GP -> TestCase -> Inputs Name Integer
inputs n (a,b) = Inputs $ toMapping "A" (toBitsLE' n a)
<> toMapping "B" (toBitsLE' n b)
outputs :: Output -> Outputs Name Integer
outputs y = Outputs $ toMapping "out" y
--------------------------------------------------------------------------------
spec :: GP -> TestSpec TestCase Output
spec n = TestSpec circomFile (mainComponent n) (inputs n) outputs (semantics n) (testCases n)
specs :: [ ( GP, TestSpec TestCase Output) ]
specs = [ (n, spec n) | n <- [3,4,6] ]
--------------------------------------------------------------------------------

58
test/Circuit/BinaryLTE.hs Normal file
View File

@ -0,0 +1,58 @@
module Circuit.BinaryLTE where
--------------------------------------------------------------------------------
import CircuitCommon
--------------------------------------------------------------------------------
-- global parameters
circomFile :: FilePath
circomFile = circuitSourceDir </> "binary_compare.circom"
-- | comparing @n@-bit integers
type GP = Int
mainComponent :: GP -> MainComponent
mainComponent n = MainComponent
{ _templateName = "BinaryLessOrEqual"
, _templateParams = [n]
, _publicInputs = ["A","B"]
}
--------------------------------------------------------------------------------
-- test cases and expected semantics
type TestCase = (Integer,Integer)
type Output = Bool
cmp :: Integer -> Integer -> Bool
cmp a b = (a <= b)
semantics :: GP -> TestCase -> Expected Output
semantics n (a,b) = Expecting $ cmp a b
testCases :: GP -> [TestCase]
testCases n = [ (a,b) | a<-[0..2^n-1] , b<-[0..2^n-1] ]
--------------------------------------------------------------------------------
-- inputs and outputs
inputs :: GP -> TestCase -> Inputs Name Integer
inputs n (a,b) = Inputs $ toMapping "A" (toBitsLE' n a)
<> toMapping "B" (toBitsLE' n b)
outputs :: Output -> Outputs Name Integer
outputs y = Outputs $ toMapping "out" y
--------------------------------------------------------------------------------
spec :: GP -> TestSpec TestCase Output
spec n = TestSpec circomFile (mainComponent n) (inputs n) outputs (semantics n) (testCases n)
specs :: [ ( GP, TestSpec TestCase Output) ]
specs = [ (n, spec n) | n <- [3,5,6] ]
--------------------------------------------------------------------------------

56
test/Circuit/ExtractBits.hs Normal file
View File

@ -0,0 +1,56 @@
module Circuit.ExtractBits where
--------------------------------------------------------------------------------
import CircuitCommon
--------------------------------------------------------------------------------
-- global parameters
circomFile :: FilePath
circomFile = circuitSourceDir </> "extract_bits.circom"
-- | extracting the lowest @n@-bit of the canonical representation of a field element
type GP = Int
mainComponent :: GP -> MainComponent
mainComponent n = MainComponent
{ _templateName = "ExtractLowerBits_testfield65537"
, _templateParams = [n]
, _publicInputs = ["inp"]
}
--------------------------------------------------------------------------------
-- test cases and expected semantics
type TestCase = Integer
type Output = Int
semantics :: GP -> TestCase -> Expected Output
semantics n a = Expecting $ fromInteger (mod a (2^n))
testCases :: GP -> [TestCase]
testCases n = [0..20]
--testCases n = [ a | a<-[0..2^(n+3)+7] ]
-- ++ [ - a | a<-[1..2^(n+3)+7] ]
--------------------------------------------------------------------------------
-- inputs and outputs
inputs :: GP -> TestCase -> Inputs Name Integer
inputs n a = Inputs $ toMapping "inp" a
outputs :: Output -> Outputs Name Integer
outputs y = Outputs $ toMapping "out" y
--------------------------------------------------------------------------------
spec :: GP -> TestSpec TestCase Output
spec n = TestSpec circomFile (mainComponent n) (inputs n) outputs (semantics n) (testCases n)
specs :: [ ( GP, TestSpec TestCase Output) ]
specs = [ (n, spec n) | n <- [2,3,4,5] ]
--------------------------------------------------------------------------------

31
test/CircuitCommon.hs Normal file
View File

@ -0,0 +1,31 @@
module CircuitCommon
( module R1CS
, module System.FilePath
, circuitSourceDir
, toBitsLE , toBitsLE'
)
where
--------------------------------------------------------------------------------
import Data.Bits
import System.FilePath
import R1CS
--------------------------------------------------------------------------------
circuitSourceDir :: FilePath
circuitSourceDir = "../circuit"
--------------------------------------------------------------------------------
toBitsLE :: Integer -> [Int]
toBitsLE = go where
go 0 = []
go n = fromInteger (n .&. 1) : go (shiftR n 1)
toBitsLE' :: Int -> Integer -> [Int]
toBitsLE' n what = take n (toBitsLE what ++ repeat 0)
--------------------------------------------------------------------------------

39
test/Main.hs Normal file
View File

@ -0,0 +1,39 @@
-- | Testing some sub-circuits
--
module Main where
--------------------------------------------------------------------------------
import R1CS.Misc ( Verbosity(..) )
import qualified R1CS.Test.Spec as Spec
import qualified Circuit.BinaryLTE as BinaryLTE
import qualified Circuit.BinaryGTE as BinaryGTE
import qualified Circuit.BinaryCompare as BinaryCmp
import qualified Circuit.ExtractBits as ExtractBits
--------------------------------------------------------------------------------
testSimple :: IO ()
testSimple = testSimple' Silent
testSimple' :: Verbosity -> IO ()
testSimple' verbosity = do
let runSpec what = Spec.testSemantics what verbosity
let runSpecMany what = Spec.testSemanticsMany what verbosity
runSpecMany BinaryCmp.specs
runSpecMany BinaryLTE.specs
runSpecMany BinaryGTE.specs
runSpecMany ExtractBits.specs
--------------------------------------------------------------------------------
main = do
testSimple' Silent

19
test/Params.hs Normal file
View File

@ -0,0 +1,19 @@
module Params where
--------------------------------------------------------------------------------
import Data.Bits
--------------------------------------------------------------------------------
-- | The size of the scalar field
r :: Integer
r = 21888242871839275222246405745257275088548364400416034343698204186575808495617
toBitsLE :: Integer -> [Int]
toBitsLE = go where
go 0 = []
go n = fromInteger (n .&. 1) : go (shiftR n 1)
--------------------------------------------------------------------------------

8
test/README.md Normal file
View File

@ -0,0 +1,8 @@
Tests for the circuits
----------------------
Some templates can be tested with [`r1cs-solver`](https://github.com/faulhornlabs/r1cs-solver).
We can also test compatibility of conventions by generating a proof from
a given piece of data, and checking if it verifies correctly.