diff --git a/.github/workflows/generate.yml b/.github/workflows/generate.yml index ea7fae6..68fba06 100644 --- a/.github/workflows/generate.yml +++ b/.github/workflows/generate.yml @@ -103,7 +103,7 @@ jobs: mkdir -p workflow/build cd workflow/build ../../reference/nim/proof_input/cli $CLI_ARGS -v --circom="proof_main.circom" - circom --r1cs --wasm --O2 -l../../circuit proof_main.circom + circom --r1cs --wasm --O2 -l../../circuit/lib -l../../circuit/poseidon2 -l../../circuit/codex proof_main.circom - name: Circuit setup run: | diff --git a/circuit/README.md b/circuit/README.md index 863a2e3..54a0e07 100644 --- a/circuit/README.md +++ b/circuit/README.md @@ -6,19 +6,42 @@ See the [README in the parent dir](../README.md) for the (draft) specification. ### Organization of the circuit code +- `codex` - the storage proof circuit +- `poseidon2` - Poseidon2 hash function +- `lib` - general purpose, reusable circom templates ("circuit library") + +In `codex`: + - `sample_cells.circom` - compute cell indices to sample, and prove those cells - `single_cell.circom` - prove a single cell - `merkle.circom` - Merkle inclusion proof (using our custom Merkle tree convention) + +In `poseidon2` + +- `poseidon2_hash.circom` - compute Poseidon2 hash with sponge construction +- `poseidon2_sponge.circom` - generic sponge construction +- `poseidon2_perm.circom` - the Poseidon2 permutation +- `poseidon2_compr.circom` - the comoression function + +In `lib`: + - `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!) - `log2.circom` - circom code for computing base 2 logarithm - `misc.circom` - miscellaneous helper funtions -- `poseidon2_hash.circom` - compute Poseidon2 hash with sponge construction -- `poseidon2_sponge.circom` - generic sponge construction -- `poseidon2_perm.circom` - the Poseidon2 permutation + + +### Main component Note: the main component is not included in the above, as it depends on the parameters. You can use one of the reference input generators to create one; -or look at `deprecated/slot_main.circom` for an example. +if you want to do manually, it should look like this: + + pragma circom 2.0.0; + include "sample_cells.circom"; + + // argument conventions: + // SampleAndProven( maxDepth, maxLog2NSlots, blockTreeDepth, nFieldElemsPerCell, nSamples ) + component main {public [entropy,dataSetRoot,slotIndex]} = SampleAndProve(32, 8, 5, 67, 100); diff --git a/circuit/merkle.circom b/circuit/codex/merkle.circom similarity index 74% rename from circuit/merkle.circom rename to circuit/codex/merkle.circom index 0396436..6af6587 100644 --- a/circuit/merkle.circom +++ b/circuit/codex/merkle.circom @@ -1,7 +1,6 @@ pragma circom 2.0.0; -include "poseidon2_perm.circom"; - +include "poseidon2_compr.circom"; include "misc.circom"; //------------------------------------------------------------------------------ @@ -23,6 +22,24 @@ include "misc.circom"; // NOTE: we don't check whether the bits are really bits, that's the // responsability of the caller! // +// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +// +// Merkle tree convention: Here we use a Codex-specific "safe" Merkle tree convention. +// +// This uses a "keyed compression function", where the key depends on: +// +// - whether we are in the bottommost layer or not +// - whether the node we are dealing with has 1 or 2 children (odd or even node) +// +// These are two bits, encoded as numbers in the set {0,1,2,3} +// (the lowest bit is 1 if it's the bottom layer, 0 otherwise; the next bit +// is 1 if it's an odd node, 0 if even node). Furthermore: +// +// - in case of an odd node with leaf x, we apply the compression to the pair (x,0) +// - in case of a singleton input (the whole Merkle tree is built on a single field element), we also apply one compression +// - the keyed compression is defined as applying the permutation to the triple (x,y,key), and extracting the first component of the resulting triple +// +// template RootFromMerklePath( maxDepth ) { diff --git a/circuit/sample_cells.circom b/circuit/codex/sample_cells.circom similarity index 100% rename from circuit/sample_cells.circom rename to circuit/codex/sample_cells.circom diff --git a/circuit/single_cell.circom b/circuit/codex/single_cell.circom similarity index 100% rename from circuit/single_cell.circom rename to circuit/codex/single_cell.circom diff --git a/circuit/deprecated/main_test_compare.circom b/circuit/deprecated/main_test_compare.circom deleted file mode 100644 index 15790cb..0000000 --- a/circuit/deprecated/main_test_compare.circom +++ /dev/null @@ -1,5 +0,0 @@ -pragma circom 2.0.0; - -include "binary_compare.circom"; - -component main {public [A,B]} = BinaryLessOrEqual(8); diff --git a/circuit/deprecated/slot_main.circom b/circuit/deprecated/slot_main.circom deleted file mode 100644 index 072ae14..0000000 --- a/circuit/deprecated/slot_main.circom +++ /dev/null @@ -1,4 +0,0 @@ -pragma circom 2.0.0; -include "sample_cells.circom"; -// SampleAndProven( maxDepth, maxLog2NSlots, blockTreeDepth, nFieldElemsPerCell, nSamples ) -component main {public [entropy,dataSetRoot,slotIndex]} = SampleAndProve(16, 5, 3, 5, 10); diff --git a/circuit/deprecated/test_compare.sh b/circuit/deprecated/test_compare.sh deleted file mode 100755 index 2dca221..0000000 --- a/circuit/deprecated/test_compare.sh +++ /dev/null @@ -1,14 +0,0 @@ -#!/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 .. diff --git a/circuit/deprecated/test_prove.sh b/circuit/deprecated/test_prove.sh deleted file mode 100755 index fc371e6..0000000 --- a/circuit/deprecated/test_prove.sh +++ /dev/null @@ -1,35 +0,0 @@ -#!/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 diff --git a/circuit/deprecated/test_slotmain.sh b/circuit/deprecated/test_slotmain.sh deleted file mode 100755 index 473bb5f..0000000 --- a/circuit/deprecated/test_slotmain.sh +++ /dev/null @@ -1,25 +0,0 @@ -#!/bin/bash - -ORIG=`pwd` -mkdir -p build - -cd ../reference/haskell -mkdir -p json -cabal v1-run cli/testMain.hs || { echo "ghc failed"; cd $ORIG; exit 101; } - -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"; cd $ORIG; exit 102; } - -echo "generating witness... (WASM)" -cd ${NAME}_js -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 diff --git a/circuit/binary_compare.circom b/circuit/lib/binary_compare.circom similarity index 100% rename from circuit/binary_compare.circom rename to circuit/lib/binary_compare.circom diff --git a/circuit/extract_bits.circom b/circuit/lib/extract_bits.circom similarity index 100% rename from circuit/extract_bits.circom rename to circuit/lib/extract_bits.circom diff --git a/circuit/log2.circom b/circuit/lib/log2.circom similarity index 100% rename from circuit/log2.circom rename to circuit/lib/log2.circom diff --git a/circuit/misc.circom b/circuit/lib/misc.circom similarity index 100% rename from circuit/misc.circom rename to circuit/lib/misc.circom diff --git a/circuit/poseidon2/poseidon2_compr.circom b/circuit/poseidon2/poseidon2_compr.circom new file mode 100644 index 0000000..7b5aab8 --- /dev/null +++ b/circuit/poseidon2/poseidon2_compr.circom @@ -0,0 +1,44 @@ +pragma circom 2.0.0; + +include "poseidon2_perm.circom"; + +// +// The Poseidon2 compression function (used when constructing binary Merkle trees) +// + +//------------------------------------------------------------------------------ +// 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; +} + +//------------------------------------------------------------------------------ +// the "keyed compression function" additionally takes a key parameter, resulting +// in a keyed family of compression functions. In practice we use 4 different +// keys (0,1,2, and 3). + +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; +} + +//------------------------------------------------------------------------------ + diff --git a/circuit/poseidon2_hash.circom b/circuit/poseidon2/poseidon2_hash.circom similarity index 52% rename from circuit/poseidon2_hash.circom rename to circuit/poseidon2/poseidon2_hash.circom index ba20f91..1171f69 100644 --- a/circuit/poseidon2_hash.circom +++ b/circuit/poseidon2/poseidon2_hash.circom @@ -2,6 +2,21 @@ 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). diff --git a/circuit/poseidon2_perm.circom b/circuit/poseidon2/poseidon2_perm.circom similarity index 94% rename from circuit/poseidon2_perm.circom rename to circuit/poseidon2/poseidon2_perm.circom index ff789fa..2139fd7 100644 --- a/circuit/poseidon2_perm.circom +++ b/circuit/poseidon2/poseidon2_perm.circom @@ -198,21 +198,4 @@ template Permutation() { } //------------------------------------------------------------------------------ -// 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 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; -} - -//------------------------------------------------------------------------------ diff --git a/circuit/poseidon2_sponge.circom b/circuit/poseidon2/poseidon2_sponge.circom similarity index 100% rename from circuit/poseidon2_sponge.circom rename to circuit/poseidon2/poseidon2_sponge.circom diff --git a/test/Circuit/BinaryCompare.hs b/test/Circuit/BinaryCompare.hs index d042d14..3f64b94 100644 --- a/test/Circuit/BinaryCompare.hs +++ b/test/Circuit/BinaryCompare.hs @@ -9,7 +9,7 @@ import CircuitCommon -- global parameters circomFile :: FilePath -circomFile = circuitSourceDir "binary_compare.circom" +circomFile = circuitLibSourceDir "binary_compare.circom" -- | comparing @n@-bit integers type GP = Int diff --git a/test/Circuit/BinaryGTE.hs b/test/Circuit/BinaryGTE.hs index 44c37dd..59bda01 100644 --- a/test/Circuit/BinaryGTE.hs +++ b/test/Circuit/BinaryGTE.hs @@ -9,7 +9,7 @@ import CircuitCommon -- global parameters circomFile :: FilePath -circomFile = circuitSourceDir "binary_compare.circom" +circomFile = circuitLibSourceDir "binary_compare.circom" -- | comparing @n@-bit integers type GP = Int diff --git a/test/Circuit/BinaryLTE.hs b/test/Circuit/BinaryLTE.hs index 5fee82c..f5bed47 100644 --- a/test/Circuit/BinaryLTE.hs +++ b/test/Circuit/BinaryLTE.hs @@ -9,7 +9,7 @@ import CircuitCommon -- global parameters circomFile :: FilePath -circomFile = circuitSourceDir "binary_compare.circom" +circomFile = circuitLibSourceDir "binary_compare.circom" -- | comparing @n@-bit integers type GP = Int diff --git a/test/Circuit/CeilingLog2.hs b/test/Circuit/CeilingLog2.hs index fe6463a..6ba019e 100644 --- a/test/Circuit/CeilingLog2.hs +++ b/test/Circuit/CeilingLog2.hs @@ -11,7 +11,7 @@ import CircuitCommon -- global parameters circomFile :: FilePath -circomFile = circuitSourceDir "log2.circom" +circomFile = circuitLibSourceDir "log2.circom" -- `n` = maximum number of bits type GP = Int diff --git a/test/Circuit/ExtractBits.hs b/test/Circuit/ExtractBits.hs index bc54874..3708291 100644 --- a/test/Circuit/ExtractBits.hs +++ b/test/Circuit/ExtractBits.hs @@ -9,7 +9,7 @@ import CircuitCommon -- global parameters circomFile :: FilePath -circomFile = circuitSourceDir "extract_bits.circom" +circomFile = circuitLibSourceDir "extract_bits.circom" -- | extracting the lowest @n@-bit of the canonical representation of a field element type GP = Int diff --git a/test/Circuit/Log2.hs b/test/Circuit/Log2.hs index ab6df24..fc27545 100644 --- a/test/Circuit/Log2.hs +++ b/test/Circuit/Log2.hs @@ -11,7 +11,7 @@ import CircuitCommon -- global parameters circomFile :: FilePath -circomFile = circuitSourceDir "log2.circom" +circomFile = circuitLibSourceDir "log2.circom" -- `n` = maximum number of bits type GP = Int diff --git a/test/CircuitCommon.hs b/test/CircuitCommon.hs index 1e7e1fa..9478996 100644 --- a/test/CircuitCommon.hs +++ b/test/CircuitCommon.hs @@ -2,7 +2,8 @@ module CircuitCommon ( module R1CS , module System.FilePath - , circuitSourceDir + , circuitRootDir + , circuitLibSourceDir , toBitsLE , toBitsLE' ) where @@ -15,8 +16,11 @@ import R1CS -------------------------------------------------------------------------------- -circuitSourceDir :: FilePath -circuitSourceDir = "../circuit" +circuitRootDir :: FilePath +circuitRootDir = "../circuit" + +circuitLibSourceDir :: FilePath +circuitLibSourceDir = circuitRootDir "lib" -------------------------------------------------------------------------------- diff --git a/test/Main.hs b/test/Main.hs index e6e4918..711e98b 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -35,10 +35,10 @@ testSimple' verbosity = do runSpecMany BinaryLTE.specs runSpecMany BinaryGTE.specs - runSpecMany ExtractBits.specs + -- runSpecMany ExtractBits.specs -- this test doesn't work currently? -------------------------------------------------------------------------------- main = do - testSimple' Info --Silent -- Verbose -- Silent + testSimple' Silent -- Info diff --git a/workflow/.gitignore b/workflow/.gitignore index d163863..c77d435 100644 --- a/workflow/.gitignore +++ b/workflow/.gitignore @@ -1 +1,3 @@ -build/ \ No newline at end of file +build/ +build_big/ +tmp/ \ No newline at end of file diff --git a/workflow/paths.sh b/workflow/paths.sh index 09b806b..c01e566 100644 --- a/workflow/paths.sh +++ b/workflow/paths.sh @@ -3,9 +3,13 @@ ORIG=`pwd` NIMCLI_DIR="${ORIG}/../reference/nim/proof_input/" -CIRCUIT_DIR="${ORIG}/../circuit/" PTAU_DIR="${ORIG}/../ceremony" +CIRCUIT_ROOT="${ORIG}/../circuit/" +CIRCUIT_PRF_DIR="${CIRCUIT_ROOT}/codex/" +CIRCUIT_POS_DIR="${CIRCUIT_ROOT}/poseidon2/" +CIRCUIT_LIB_DIR="${CIRCUIT_ROOT}/lib/" + PTAU_FILE="powersOfTau28_hez_final_21.ptau" PTAU_PATH="${PTAU_DIR}/${PTAU_FILE}" diff --git a/workflow/setup.sh b/workflow/setup.sh index 52381f1..076fe65 100755 --- a/workflow/setup.sh +++ b/workflow/setup.sh @@ -14,7 +14,8 @@ ${NIMCLI_DIR}/cli $CLI_ARGS -v --circom=${CIRCUIT_MAIN}.circom # --- compile the circuit --- -time circom --r1cs --wasm --O2 -l${CIRCUIT_DIR} ${CIRCUIT_MAIN}.circom +CIRCUIT_INCLUDES="-l${CIRCUIT_LIB_DIR} -l${CIRCUIT_POS_DIR} -l${CIRCUIT_PRF_DIR}" +time circom --r1cs --wasm --O2 ${CIRCUIT_INCLUDES} ${CIRCUIT_MAIN}.circom # --- circuit specific setup ---