Poseidon gkr (#81)

* wip

* wip

* wip

* 2 full rounds

* partial rounds

* wip

* real constants

* stats

* 590K poseidons/s

* fix (still wip)

* works!!

* evaluate_sequential

* typo

* fix deadlock

* experiment-double-internal-layers

* Revert "experiment-double-internal-layers"

This reverts commit cff0334.

* naming

* WOAwwwwwww

* working for real with the pcs

* overhead versus plaintext

* pretty text

* evaluate_univariate_multilinear

* create a dedicated "poseidon_circuit" crate

* wip

* using packed pcs

* simplify

* simplify

* w

* compress

* optional compress

* GKR integration in leanVM, wip

* abstract away the univariate skip from Poseidon GKR api

* fix

* fix

* wip

* fix

* gud

* remove dead code

* fix whir

* Proving_Poseidons_with_GKR.pdf + reset benchmarks + cleanup

* revert reseting benchmarks

* log scale for WHIR recursion graph

---------

Co-authored-by: Tom Wambsgans <[email protected]>

Author: TomWambsgans

Cargo.lock

@@ -51,9 +51,11 @@ lean_prover = { path = "crates/lean_prover" }
 rec_aggregation = { path = "crates/rec_aggregation" }
 witness_generation = { path = "crates/lean_prover/witness_generation" }
 vm_air = { path = "crates/lean_prover/vm_air" }
+poseidon_circuit = { path = "crates/poseidon_circuit" }
 
 # External
 thiserror = "2.0"
+clap = { version = "4.3.10", features = ["derive"] }
 rand = "0.9.2"
 sha3 = "0.10.8"
 rayon = "1.5.1"
@@ -78,26 +80,15 @@ p3-poseidon2-air = { git = "https://github.com/TomWambsgans/Plonky3.git", branch
 p3-goldilocks = { git = "https://github.com/TomWambsgans/Plonky3.git", branch = "lean-multisig" }
 p3-challenger = { git = "https://github.com/TomWambsgans/Plonky3.git", branch = "lean-multisig" }
 p3-util = { git = "https://github.com/TomWambsgans/Plonky3.git", branch = "lean-multisig" }
+p3-monty-31 = { git = "https://github.com/TomWambsgans/Plonky3.git", branch = "lean-multisig" }
 
 whir-p3 = { git = "https://github.com/TomWambsgans/whir-p3", branch = "lean-multisig" }
 multilinear-toolkit = { git = "https://github.com/leanEthereum/multilinear-toolkit.git" }
 
 [dependencies]
-air.workspace = true
-p3-field.workspace = true
-p3-koala-bear.workspace = true
-p3-poseidon2.workspace = true
-rand.workspace = true
-p3-poseidon2-air.workspace = true
-p3-matrix.workspace = true
-p3-challenger.workspace = true
-whir-p3.workspace = true
-p3-uni-stark.workspace = true
-utils.workspace = true
-p3-util.workspace = true
-packed_pcs.workspace = true
-p3-air.workspace = true
-multilinear-toolkit.workspace = true
+clap.workspace = true
+rec_aggregation.workspace = true
+poseidon_circuit.workspace = true
 
 # [patch."https://github.com/TomWambsgans/Plonky3.git"]
 # p3-koala-bear = { path = "../zk/Plonky3/koala-bear" }
@@ -110,28 +101,13 @@ multilinear-toolkit.workspace = true
 # p3-poseidon2-air = { path = "../zk/Plonky3/poseidon2-air" }
 # p3-dft = { path = "../zk/Plonky3/dft" }
 # p3-challenger = { path = "../zk/Plonky3/challenger" }
+# p3-monty-31 = { path = "../zk/Plonky3/monty-31" }
 
 # [patch."https://github.com/TomWambsgans/whir-p3.git"]
 # whir-p3 = { path = "../zk/whir/fork-whir-p3" }
 
 # [patch."https://github.com/leanEthereum/multilinear-toolkit.git"]
 # multilinear-toolkit = { path = "../zk/multilinear-toolkit" }
 
-[dev-dependencies]
-criterion = { version = "0.7", default-features = false, features = ["cargo_bench_support"] }
-rec_aggregation.workspace = true
-
 [profile.release]
 lto = "thin"
-
-[[bench]]
-name = "poseidon2"
-harness = false
-
-[[bench]]
-name = "recursion"
-harness = false
-
-[[bench]]
-name = "xmss"
-harness = false

Cargo.toml

@@ -6,56 +6,54 @@ XMSS + minimal [zkVM](minimal_zkVM.pdf) = lightweight PQ signatures, with unboun
 ## Proving System
 
 
-- AIR tables committed via multilinear polynomial, using [WHIR](https://eprint.iacr.org/2024/1586.pdf)
+- [WHIR](https://eprint.iacr.org/2024/1586.pdf)
 - [SuperSpartan](https://eprint.iacr.org/2023/552.pdf), with AIR-specific optimizations developed by W. Borgeaud in [A simple multivariate AIR argument inspired by SuperSpartan](https://solvable.group/posts/super-air/#fnref:1)
 - [Univariate Skip](https://eprint.iacr.org/2024/108.pdf)
 - [Logup*](https://eprint.iacr.org/2025/946.pdf)
 - ...
 
 The VM design is inspired by the famous [Cairo paper](https://eprint.iacr.org/2021/1063.pdf).
 
-Details on how to prove AIR constraints in the multilinear settings are described in [Whirlaway.pdf](Whirlaway.pdf).
-
-[Deep-wiki](https://deepwiki.com/leanEthereum/leanMultisig/1-overview) (thanks [adust09](https://github.com/adust09))
-
-
 ## Benchmarks
 
-cpu: i9-12900H, ram: 32 gb
-
-> TLDR: Slow, **but there is hope** (cf [TODO](TODO.md))
+Benchmarks are performed on 2 laptops:
+- i9-12900H, 32 gb of RAM
+- mac m4 max
 
-target ≈ 128 bits of security, currently using conjecture: 4.12 of [WHIR](https://eprint.iacr.org/2024/1586.pdf), "up to capacity" (TODO: a version without any conjecture, requires an extension of koala-bear of degree > 5)
+target ≈ 128 bits of security, currently using conjecture: 4.12 of [WHIR](https://eprint.iacr.org/2024/1586.pdf), "up to capacity" (TODO: provable security)
 
 ### Poseidon2
 
+Poseidon2 over 16 KoalaBear field elements.
+
 ```console
-RUSTFLAGS='-C target-cpu=native' cargo run --release
+RUSTFLAGS='-C target-cpu=native' cargo run --release -- poseidon --log-n-perms 20
 ```
 
-50 % over 16 field elements, 50 % over 24 field elements. rate = 1/2
-
 ![Alt text](docs/benchmark_graphs/graphs/raw_poseidons.svg)
 
 ### Recursion
 
-```console
-RUSTFLAGS='-C target-cpu=native' cargo test --release --package rec_aggregation --lib -- recursion::test_whir_recursion --nocapture
-```
 
 The full recursion program is not finished yet. Instead, we prove validity of a WHIR opening, with 25 variables, and rate = 1/4.
 
+```console
+RUSTFLAGS='-C target-cpu=native' cargo run --release -- recursion
+```
+
 ![Alt text](docs/benchmark_graphs/graphs/recursive_whir_opening.svg)
 
 ### XMSS aggregation
 
 ```console
-RUSTFLAGS='-C target-cpu=native' NUM_XMSS_AGGREGATED='500' cargo test --release --package rec_aggregation --lib -- xmss_aggregate::test_xmss_aggregate --nocapture
+RUSTFLAGS='-C target-cpu=native' cargo run --release -- xmss --n-signatures 800
 ```
 
-500 XMSS aggregated. "Trivial encoding" (for now).
+[Trivial encoding](docs/XMSS_trivial_encoding.pdf) (for now).
+
+
+![Alt text](docs/benchmark_graphs/graphs/xmss_aggregated.svg)
 
-![Alt text](docs/benchmark_graphs/graphs/xmss_aggregated_time.svg)
 ![Alt text](docs/benchmark_graphs/graphs/xmss_aggregated_overhead.svg)
 
 ### Proof size
@@ -65,7 +63,7 @@ With conjecture "up to capacity", current proofs with rate = 1/2 are about ≈ 4
 - The remaining 100 - 200 KiB will be significantly reduced in the future (this part has not been optimized at all).
 - WHIR proof size will also be reduced, thanks to merkle pruning (TODO).
 
-Reasonable target: 256 KiB for fast proof, 128 KiB for slower proofs (rate = 1/4 or 1/8).
+Target: 256 KiB for fast proof, 128 KiB for slower proofs (rate = 1/4 or 1/8).
 
 ## Credits
 

README.md

@@ -15,13 +15,8 @@ p3-uni-stark.workspace = true
 p3-matrix.workspace = true
 p3-util.workspace = true
 multilinear-toolkit.workspace = true
-p3-koala-bear.workspace = true
-rand.workspace = true
-whir-p3.workspace = true
-packed_pcs.workspace = true
-
 
 [dev-dependencies]
 p3-koala-bear.workspace = true
 p3-matrix.workspace = true
-rand.workspace = true
+rand.workspace = true