Merge pull request #5 from codex-storage/review

Code review of the circom circuit
This commit is contained in:
Balazs Komuves 2024-03-12 10:53:39 +01:00 committed by GitHub
commit 2a4a71acf6
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
10 changed files with 60 additions and 90 deletions

View File

@ -3,7 +3,8 @@ pragma circom 2.0.0;
//------------------------------------------------------------------------------ //------------------------------------------------------------------------------
// //
// given two numbers in `n`-bit binary decomposition (little-endian), we compute // given two numbers in `n`-bit binary decomposition
// (least significant bit first), we compute
// //
// / -1 if A < B // / -1 if A < B
// out := { 0 if A == B // out := { 0 if A == B

View File

@ -23,7 +23,7 @@ template ExtractLowerBits(n) {
component tb = ToBits(254); // note: 2^253 < r < 2^254 component tb = ToBits(254); // note: 2^253 < r < 2^254
tb.inp <== inp; tb.inp <== inp;
// bits of field prime `r` in little-endian order // bits of field prime `r`, least significant bit first
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]; 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 // enforce that the binary representation is < r
@ -56,7 +56,7 @@ template ExtractLowerBits_testfield65537(n) {
component tb = ToBits(18); // note: 2^16 < r < 2^18 component tb = ToBits(18); // note: 2^16 < r < 2^18
tb.inp <== inp; tb.inp <== inp;
// bits of field prime `r` in little-endian order // bits of field prime `r`, least significant bit first
var primeBits[18] = [1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0]; 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 // enforce that the binary representation is < r

View File

@ -17,7 +17,7 @@ template Log2(n) {
signal output mask[n+1]; signal output mask[n+1];
// mask will be a vector [1,1,1,...1,0,...,0,0] // mask will be a vector [1,1,1,...1,0,...,0,0]
// which can change only where inp == 2^out // which can change only where index == out
var log2 = -1; var log2 = -1;
for(var i=0; i<=n; i++) { for(var i=0; i<=n; i++) {
@ -43,7 +43,7 @@ template Log2(n) {
//------------------------------------------------------------------------------ //------------------------------------------------------------------------------
// //
// given an input `inp`, this template computes `out := 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 // it also returns the binary decomposition of `inp-1`, and the binary decomposition
// of the mask `(2^k-1)` // of the mask `(2^k-1)`
// //
// we also output a mask vector which is 1 for i=0..k-1, and 0 elsewhere // we also output a mask vector which is 1 for i=0..k-1, and 0 elsewhere

View File

@ -1,7 +1,6 @@
pragma circom 2.0.0; pragma circom 2.0.0;
include "poseidon2_perm.circom"; include "poseidon2_perm.circom";
include "poseidon2_hash.circom";
include "misc.circom"; include "misc.circom";
@ -15,7 +14,7 @@ include "misc.circom";
// //
// inputs and outputs: // inputs and outputs:
// - leaf: the leaf hash // - leaf: the leaf hash
// - pathBits: the linear index of the leaf, in binary decomposition (little-endian) // - pathBits: the linear index of the leaf, in binary decomposition (least significant bit first)
// - lastBits: the index of the last leaf (= nLeaves-1), in binary decomposition // - lastBits: the index of the last leaf (= nLeaves-1), in binary decomposition
// - maskBits: the bits of the the mask `2^ceilingLog2(size) - 1` // - 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) // - merklePath: the Merkle inclusion proof (required hashes, starting from the leaf and ending near the root)
@ -38,8 +37,11 @@ template RootFromMerklePath( maxDepth ) {
signal aux[ maxDepth+1 ]; signal aux[ maxDepth+1 ];
aux[0] <== leaf; aux[0] <== leaf;
// compute which prefixes (in big-endian) of the index is // Determine whether nodes from the path are last in their row and are odd,
// the same as the corresponding prefix of the last index // by computing which binary prefixes of the index are the same as the
// corresponding prefix of the last index.
// This is done in reverse bit order, because pathBits and lastBits have the
// least significant bit first.
component eq[ maxDepth ]; component eq[ maxDepth ];
signal isLast[ maxDepth+1 ]; signal isLast[ maxDepth+1 ];
isLast[ maxDepth ] <== 1; isLast[ maxDepth ] <== 1;

View File

@ -1,7 +1,6 @@
pragma circom 2.0.0; pragma circom 2.0.0;
//------------------------------------------------------------------------------ //------------------------------------------------------------------------------
// compute (compile time) the log2 of a number
function FloorLog2(n) { function FloorLog2(n) {
return (n==0) ? -1 : (1 + FloorLog2(n>>1)); return (n==0) ? -1 : (1 + FloorLog2(n>>1));
@ -12,7 +11,7 @@ function CeilLog2(n) {
} }
//------------------------------------------------------------------------------ //------------------------------------------------------------------------------
// decompose an n-bit number into bits // decompose an n-bit number into bits (least significant bit first)
template ToBits(n) { template ToBits(n) {
signal input inp; signal input inp;

View File

@ -2,20 +2,6 @@ pragma circom 2.0.0;
include "poseidon2_sponge.circom"; 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 // 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). // (assuming bn128 scalar field. We use capacity=1, rate=2, t=3).

View File

@ -201,20 +201,6 @@ template Permutation() {
// the "compression function" takes 2 field elements as input and produces // the "compression function" takes 2 field elements as input and produces
// 1 field element as output. It is a trivial application of the permutation. // 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;
}
//--------------------------------------
template KeyedCompression() { template KeyedCompression() {
signal input key; signal input key;
signal input inp[2]; signal input inp[2];

View File

@ -99,12 +99,10 @@ log("top root check = ", mtop.recRoot == dataSetRoot);
// //
// then we prove the individual sampled cells // then we prove the individual sampled cells
signal log2N;
component lg = Log2(maxDepth); // we allow at most 2^32 cells per slot component lg = Log2(maxDepth); // we allow at most 2^32 cells per slot
lg.inp <== nCellsPerSlot; lg.inp <== nCellsPerSlot;
lg.out ==> log2N;
// NOTE: in general we need the for Merkle prover the binary decomposition // NOTE: in general we need for the Merkle prover the binary decomposition
// of `nLeaves - 1`. But currently this is in fact a power of two, so we // 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? // can reuse the binary mask for this. Later we may change this?
// //

View File

@ -1,10 +1,8 @@
pragma circom 2.0.0; pragma circom 2.0.0;
include "poseidon2_perm.circom";
include "poseidon2_hash.circom"; include "poseidon2_hash.circom";
include "merkle.circom"; include "merkle.circom";
include "misc.circom";
//------------------------------------------------------------------------------ //------------------------------------------------------------------------------