diff --git a/.cargo/config.toml b/.cargo/config.toml
new file mode 100644
index 000000000..983e89ba0
--- /dev/null
+++ b/.cargo/config.toml
@@ -0,0 +1,5 @@
+[target.wasm32-unknown-unknown]
+runner = 'wasm-bindgen-test-runner'
+
+[target.wasm32-wasip2]
+runner = 'wasmtime'
diff --git a/.github/scripts/wasm-target-test-build.sh b/.github/scripts/wasm-target-test-build.sh
deleted file mode 100644
index 3c42427cd..000000000
--- a/.github/scripts/wasm-target-test-build.sh
+++ /dev/null
@@ -1,30 +0,0 @@
-#!/bin/sh
-
-GIT_ROOT=$(pwd)
-
-cd /tmp
-
-# create test project
-cargo new foobar
-cd foobar
-
-# set rust-toolchain same as "sonobe"
-cp "${GIT_ROOT}/rust-toolchain" .
-
-# add wasm32-* targets
-rustup target add wasm32-unknown-unknown wasm32-wasip1
-
-# add dependencies
-cargo add --path "${GIT_ROOT}/frontends" --features wasm, parallel
-cargo add --path "${GIT_ROOT}/folding-schemes" --features parallel
-cargo add getrandom --features wasm_js --target wasm32-unknown-unknown
-
-# test build for wasm32-* targets
-cargo build --release --target wasm32-unknown-unknown
-cargo build --release --target wasm32-wasip1
-# Emscripten would require to fetch the `emcc` tooling. Hence we don't build the lib as a dep for it.
-# cargo build --release --target wasm32-unknown-emscripten
-
-# delete test project
-cd ../
-rm -rf foobar
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index a4b70d0cc..9ca52f736 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -1,5 +1,6 @@
name: CI Check
on:
+ workflow_dispatch:
merge_group:
pull_request:
push:
@@ -36,44 +37,45 @@ concurrency:
jobs:
test:
if: github.event.pull_request.draft == false
- name: Test
+ name: Test ${{ matrix.target }} (${{ matrix.features }})
runs-on: ubuntu-latest
strategy:
matrix:
- feature_set: [basic]
include:
- - feature_set: basic
- features: --features default,light-test
+ # x64: both parallel and no-parallel
+ - target: x86_64-unknown-linux-gnu
+ features: parallel
+ args: "--features parallel"
+ - target: x86_64-unknown-linux-gnu
+ features: no-parallel
+ args: ""
+ # wasm: no-parallel only
+ - target: wasm32-unknown-unknown
+ features: no-parallel
+ args: ""
+ - target: wasm32-wasip2
+ features: no-parallel
+ args: ""
steps:
- - uses: actions/checkout@v2
- - uses: actions-rs/toolchain@v1
- - uses: noir-lang/noirup@v0.1.3
- with:
- toolchain: 0.36.0
- - name: Download Circom
- run: |
- mkdir -p $HOME/bin
- curl -sSfL https://github.com/iden3/circom/releases/download/v2.1.6/circom-linux-amd64 -o $HOME/bin/circom
- chmod +x $HOME/bin/circom
- echo "$HOME/bin" >> $GITHUB_PATH
- - name: Download solc
- run: |
- curl -sSfL https://github.com/ethereum/solidity/releases/download/v0.8.4/solc-static-linux -o /usr/local/bin/solc
- chmod +x /usr/local/bin/solc
- - name: Execute compile.sh to generate .r1cs and .wasm from .circom
- run: ./experimental-frontends/src/circom/test_folder/compile.sh
- - name: Execute compile.sh to generate .json from noir
- run: ./experimental-frontends/src/noir/test_folder/compile.sh
- - name: Run tests
- uses: actions-rs/cargo@v1
- with:
- command: test
- args: --release --workspace --no-default-features ${{ matrix.features }}
- - name: Run Doc-tests
- uses: actions-rs/cargo@v1
+ - uses: actions/checkout@v4
+ - uses: dtolnay/rust-toolchain@stable
with:
- command: test
- args: --doc
+ targets: ${{ matrix.target }}
+ - uses: Swatinem/rust-cache@v2
+ - name: Install wasm-bindgen-cli
+ if: matrix.target == 'wasm32-unknown-unknown'
+ run: cargo install wasm-bindgen-cli
+ - name: Install wasmtime-cli
+ if: matrix.target == 'wasm32-wasip2'
+ run: cargo install wasmtime-cli
+ - name: Test sonobe-primitives
+ run: cargo test --release -p sonobe-primitives --target ${{ matrix.target }} ${{ matrix.args }}
+ - name: Test sonobe-fs
+ run: cargo test --release -p sonobe-fs --target ${{ matrix.target }} ${{ matrix.args }}
+ - name: Test sonobe-ivc
+ run: cargo test --release -p sonobe-ivc --target ${{ matrix.target }} ${{ matrix.args }}
+ - name: Test documentation examples
+ run: cargo test --doc --target ${{ matrix.target }} ${{ matrix.args }}
build:
if: github.event.pull_request.draft == false
@@ -82,79 +84,21 @@ jobs:
strategy:
matrix:
target:
+ - x86_64-unknown-linux-gnu
- wasm32-unknown-unknown
- - wasm32-wasip1
- # Ignoring until clear usage is required
- # - wasm32-unknown-emscripten
-
- steps:
- - uses: actions/checkout@v3
- - uses: actions-rs/toolchain@v1
- with:
- override: false
- default: true
- - name: Add target
- run: rustup target add ${{ matrix.target }}
- - name: Wasm-compat experimental-frontends build
- uses: actions-rs/cargo@v1
- with:
- command: build
- args: -p experimental-frontends --no-default-features --target ${{ matrix.target }} --features "wasm, parallel"
- - name: Wasm-compat folding-schemes build
- uses: actions-rs/cargo@v1
- with:
- command: build
- args: -p folding-schemes --no-default-features --target ${{ matrix.target }} --features "default,light-test"
- - name: Run wasm-compat script
- run: |
- chmod +x .github/scripts/wasm-target-test-build.sh
- .github/scripts/wasm-target-test-build.sh
- shell: bash
-
- examples:
- if: github.event.pull_request.draft == false
- name: Run examples & examples tests
- runs-on: ubuntu-latest
+ - wasm32-wasip2
steps:
- - uses: actions/checkout@v2
- - uses: actions-rs/toolchain@v1
- - uses: noir-lang/noirup@v0.1.3
+ - uses: actions/checkout@v4
+ - uses: dtolnay/rust-toolchain@stable
with:
- toolchain: 0.36.0
- - name: Download Circom
- run: |
- mkdir -p $HOME/bin
- curl -sSfL https://github.com/iden3/circom/releases/download/v2.1.6/circom-linux-amd64 -o $HOME/bin/circom
- chmod +x $HOME/bin/circom
- echo "$HOME/bin" >> $GITHUB_PATH
- - name: Download solc
- run: |
- curl -sSfL https://github.com/ethereum/solidity/releases/download/v0.8.4/solc-static-linux -o /usr/local/bin/solc
- chmod +x /usr/local/bin/solc
- - name: Execute compile.sh to generate .r1cs and .wasm from .circom
- run: ./experimental-frontends/src/circom/test_folder/compile.sh
- - name: Execute compile.sh to generate .json from noir
- run: ./experimental-frontends/src/noir/test_folder/compile.sh
- - name: Run examples tests
- run: cargo test --examples
- - name: Run examples
- run: cargo run --release --example 2>&1 | grep -E '^ ' | xargs -n1 cargo run --release --example
-
- # run the benchmarks with the flag `--no-run` to ensure that they compile,
- # but without executing them.
- bench:
- if: github.event.pull_request.draft == false
- name: Bench compile
- timeout-minutes: 30
- runs-on: ubuntu-latest
- steps:
- - uses: actions/checkout@v2
- - uses: actions-rs/toolchain@v1
+ targets: ${{ matrix.target }}
- uses: Swatinem/rust-cache@v2
- - uses: actions-rs/cargo@v1
- with:
- command: bench
- args: -p folding-schemes --no-run
+ - name: Build sonobe-primitives
+ run: cargo build -p sonobe-primitives --target ${{ matrix.target }}
+ - name: Build sonobe-fs
+ run: cargo build -p sonobe-fs --target ${{ matrix.target }}
+ - name: Build sonobe-ivc
+ run: cargo build -p sonobe-ivc --target ${{ matrix.target }}
fmt:
if: github.event.pull_request.draft == false
@@ -162,41 +106,33 @@ jobs:
timeout-minutes: 30
runs-on: ubuntu-latest
steps:
- - uses: actions/checkout@v2
- - uses: actions-rs/toolchain@v1
- - uses: Swatinem/rust-cache@v2
- - run: rustup component add rustfmt
- - uses: actions-rs/cargo@v1
+ - uses: actions/checkout@v4
+ - uses: dtolnay/rust-toolchain@stable
with:
- command: fmt
- args: --all --check
+ components: rustfmt
+ - uses: Swatinem/rust-cache@v2
+ - name: Run rustfmt
+ run: cargo fmt --all --check
clippy:
if: github.event.pull_request.draft == false
- name: Clippy lint checks
+ name: Clippy (${{ matrix.target }})
runs-on: ubuntu-latest
strategy:
matrix:
- feature_set: [basic, wasm]
- include:
- - feature_set: basic
- features: --features default
- # We only want to test `experimental-frontends` package with `wasm` feature.
- - feature_set: wasm
- features: -p experimental-frontends --features wasm,parallel --target wasm32-unknown-unknown
+ target:
+ - x86_64-unknown-linux-gnu
+ - wasm32-unknown-unknown
+ - wasm32-wasip2
steps:
- - uses: actions/checkout@v2
- - uses: actions-rs/toolchain@v1
+ - uses: actions/checkout@v4
+ - uses: dtolnay/rust-toolchain@stable
with:
components: clippy
+ targets: ${{ matrix.target }}
- uses: Swatinem/rust-cache@v2
- - name: Add target
- run: rustup target add wasm32-unknown-unknown
- name: Run clippy
- uses: actions-rs/cargo@v1
- with:
- command: clippy
- args: --no-default-features ${{ matrix.features }} -- -D warnings
+ run: cargo clippy --workspace --all-targets --target ${{ matrix.target }} -- -D warnings
typos:
if: github.event.pull_request.draft == false
diff --git a/Cargo.toml b/Cargo.toml
index e8fe65f39..d1b8c62ac 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -1,10 +1,50 @@
[workspace]
members = [
"crates/primitives",
- "crates/traits",
+ "crates/fs",
+ "crates/ivc",
]
resolver = "2"
+[workspace.package]
+edition = "2024"
+license = "MIT"
+repository = "https://github.com/privacy-scaling-explorations/sonobe/"
+rust-version = "1.85.1"
+
+[workspace.dependencies]
+num-bigint = { version = "0.4.3" }
+num-integer = { version = "0.1" }
+num-traits = { version = "0.2" }
+sha3 = { version = "0.10" }
+rayon = { version = "1" }
+thiserror = { version = "2.0.16" }
+wasm-bindgen-test = { version = "0.3" }
+
+# Arkworks family
+ark-crypto-primitives = { git = "https://github.com/arkworks-rs/crypto-primitives", default-features = false }
+ark-ec = { git = "https://github.com/arkworks-rs/algebra", default-features = false }
+ark-ff = { git = "https://github.com/arkworks-rs/algebra", default-features = false }
+ark-groth16 = { git = "https://github.com/arkworks-rs/groth16", default-features = false }
+ark-poly = { git = "https://github.com/arkworks-rs/algebra", default-features = false }
+ark-poly-commit = { git = "https://github.com/arkworks-rs/poly-commit", default-features = false }
+ark-r1cs-std = { git = "https://github.com/arkworks-rs/r1cs-std", default-features = false }
+ark-relations = { git = "https://github.com/arkworks-rs/snark", default-features = false }
+ark-serialize = { git = "https://github.com/arkworks-rs/algebra", default-features = false }
+ark-snark = { git = "https://github.com/arkworks-rs/snark", default-features = false }
+ark-std = { git = "https://github.com/arkworks-rs/std", default-features = false }
+
+# Ark curves
+ark-bn254 = { git = "https://github.com/arkworks-rs/algebra", default-features = false }
+ark-grumpkin = { git = "https://github.com/arkworks-rs/algebra", default-features = false }
+ark-pallas = { git = "https://github.com/arkworks-rs/algebra", default-features = false }
+ark-vesta = { git = "https://github.com/arkworks-rs/algebra", default-features = false }
+
+# Local crates
+sonobe-primitives = { path = "crates/primitives", default-features = false }
+sonobe-fs = { path = "crates/fs", default-features = false }
+sonobe-ivc = { path = "crates/ivc", default-features = false }
+
[patch.crates-io]
# We depend on git versions of arkworks crates, but some of our dependencies
# depend on crates.io versions, so we need to override them here to avoid
@@ -19,64 +59,9 @@ ark-r1cs-std = { git = "https://github.com/winderica/r1cs-std", rev = "ae8283a"
# Curve crates also need git versions
ark-bn254 = { git = "https://github.com/arkworks-rs/algebra" }
-ark-grumpkin = { git = "https://github.com/arkworks-rs/algebra" }
[patch."https://github.com/arkworks-rs/crypto-primitives"]
ark-crypto-primitives = { git = "https://github.com/winderica/crypto-primitives", rev = "af003fc" }
[patch."https://github.com/arkworks-rs/r1cs-std"]
-ark-r1cs-std = { git = "https://github.com/winderica/r1cs-std", rev = "ae8283a" } # "sw-fix-updated" branch
-
-[workspace.package]
-edition = "2021"
-license = "MIT"
-repository = "https://github.com/privacy-scaling-explorations/sonobe/"
-
-[workspace.dependencies]
-acvm = { git = "https://github.com/winderica/noir", rev = "fc9e99", default-features = false } # "arkworks-next" branch
-askama = { version = "0.12.0", default-features = false }
-clap = { version = "4.4" }
-clap-verbosity-flag = { version = "2.1" }
-criterion = { version = "0.5" }
-env_logger = { version = "0.10" }
-getrandom = { version = "0.2" }
-log = { version = "0.4" }
-noname = { git = "https://github.com/dmpierre/noname", rev = "c34f17" }
-num-bigint = { version = "0.4.3" }
-num-integer = { version = "0.1" }
-num-traits = { version = "0.2" }
-pprof = { version = "0.13" }
-serde = { version = "^1.0.0" }
-serde_json = { version = "^1.0.0" }
-sha3 = { version = "0.10" }
-rand = { version = "0.8.5" }
-rayon = { version = "1" }
-revm = { version = "19.5.0", default-features = false }
-rust-crypto = { version = "0.2" }
-thiserror = { version = "1.0" }
-tokio = "1.44.1"
-wasmer = { version = "6.1.0", default-features = false }
-
-# Arkworks family
-ark-bn254 = { version = "^0.5.0", default-features = false }
-ark-circom = { git = "https://github.com/arkworks-rs/circom-compat", default-features = false }
-ark-crypto-primitives = { version = "^0.5.0", default-features = false }
-ark-ec = { version = "^0.5.0", default-features = false }
-ark-ff = { version = "^0.5.0", default-features = false }
-ark-groth16 = { git = "https://github.com/arkworks-rs/groth16" }
-ark-grumpkin = { version = "^0.5.0", default-features = false }
-ark-mnt4-298 = { version = "^0.5.0" }
-ark-mnt6-298 = { version = "^0.5.0" }
-ark-pallas = { version = "^0.5.0" }
-ark-poly = { version = "^0.5.0", default-features = false }
-ark-poly-commit = { version = "^0.5.0" }
-ark-r1cs-std = { version = "^0.5.0", default-features = false }
-ark-relations = { git = "https://github.com/arkworks-rs/snark", default-features = false }
-ark-serialize = { version = "^0.5.0" }
-ark-snark = { git = "https://github.com/arkworks-rs/snark", default-features = false }
-ark-std = { version = "^0.5.0", default-features = false }
-ark-vesta = { version = "^0.5.0" }
-
-# Local crates
-sonobe-primitives = { path = "crates/primitives", default-features = false }
-sonobe-traits = { path = "crates/traits" }
\ No newline at end of file
+ark-r1cs-std = { git = "https://github.com/winderica/r1cs-std", rev = "ae8283a" } # "sw-fix-updated" branch
\ No newline at end of file
diff --git a/README.md b/README.md
index bb9ee6f10..19ca77b10 100644
--- a/README.md
+++ b/README.md
@@ -2,7 +2,7 @@
Experimental folding schemes library implemented jointly by [0xPARC](https://0xparc.org/) and [PSE](https://pse.dev).
-
+
Sonobe is a modular library to fold arithmetic circuit instances in an Incremental Verifiable computation (IVC) style. It features multiple folding schemes and decider setups, allowing users to pick the scheme which best fits their needs.
@@ -67,7 +67,7 @@ Once the IVC iterations are completed, the IVC proof is compressed into the Deci
-
+
Where $w_i$ are the external witnesses used at each iterative step.
@@ -87,14 +87,14 @@ The development flow using Sonobe looks like:
4. Generate the decider verifier
-
+
The folding scheme and decider used can be swapped with a few lines of code (eg. switching from a Decider that uses two Spartan proofs over a cycle of curves, to a Decider that uses a single Groth16 proof over the BN254 to be verified in an Ethereum smart contract).
The [Sonobe docs](https://privacy-scaling-explorations.github.io/sonobe-docs/) contain more details about the usage and design of the library.
-Complete examples can be found at [folding-schemes/examples](https://github.com/privacy-scaling-explorations/sonobe/tree/main/examples)
+Complete examples can be found at [folding-schemes/examples](https://github.com/privacy-scaling-explorations/sonobeAcknowledgments/tree/main/examples)
## License
diff --git a/crates/fs/Cargo.toml b/crates/fs/Cargo.toml
new file mode 100644
index 000000000..772f4e47d
--- /dev/null
+++ b/crates/fs/Cargo.toml
@@ -0,0 +1,37 @@
+[package]
+name = "sonobe-fs"
+version = "0.1.0"
+edition.workspace = true
+license.workspace = true
+repository.workspace = true
+
+[dependencies]
+ark-crypto-primitives = { workspace = true, features = ["constraints", "sponge", "crh"] }
+ark-ec = { workspace = true }
+ark-ff = { workspace = true, features = ["asm"] }
+ark-poly = { workspace = true }
+ark-r1cs-std = { workspace = true }
+ark-relations = { workspace = true }
+ark-std = { workspace = true, features = ["getrandom"] }
+ark-serialize = { workspace = true }
+num-bigint = { workspace = true, features = ["rand"] }
+thiserror = { workspace = true }
+rayon = { workspace = true }
+
+sonobe-primitives = { workspace = true }
+
+[dev-dependencies]
+ark-bn254 = { workspace = true, features = ["curve", "r1cs"] }
+ark-pallas = { workspace = true, features = ["curve", "r1cs"] }
+
+[target.'cfg(all(target_arch = "wasm32", target_os = "unknown"))'.dependencies]
+getrandom = { version = "0.2", features = ["js"] }
+
+[target.'cfg(all(target_arch = "wasm32", target_os = "unknown"))'.dev-dependencies]
+wasm-bindgen-test = { workspace = true }
+
+[features]
+default = []
+parallel = [
+ "sonobe-primitives/parallel",
+]
diff --git a/crates/fs/src/definitions/algorithms.rs b/crates/fs/src/definitions/algorithms.rs
new file mode 100644
index 000000000..a4238a038
--- /dev/null
+++ b/crates/fs/src/definitions/algorithms.rs
@@ -0,0 +1,120 @@
+//! Traits that define out-of-circuit widgets for folding scheme algorithms
+//! (preprocessing, key generation, proof generation, proof verification, and
+//! deciding).
+
+use ark_std::{borrow::Borrow, rand::RngCore};
+use sonobe_primitives::{relations::Relation, transcripts::Transcript};
+
+use super::{FoldingSchemeDef, errors::Error, keys::DeciderKey};
+
+/// [`FoldingSchemePreprocessor`] is the trait for folding scheme preprocessor.
+pub trait FoldingSchemePreprocessor: FoldingSchemeDef {
+ /// [`FoldingSchemePreprocessor::preprocess`] defines the preprocessing
+ /// algorithm, which is a randomized algorithm that takes as input the
+ /// config / parameterization `config` of the folding scheme (e.g., size
+ /// bounds of the folding scheme) and outputs the public parameters.
+ ///
+ /// Here, the randomness source is controlled by `rng`.
+ ///
+ /// The security parameter is implicitly specified by the size of underlying
+ /// fields and groups.
+ fn preprocess(config: Self::Config, rng: impl RngCore) -> Result;
+}
+
+/// [`FoldingSchemeKeyGenerator`] is the trait for folding scheme key generator.
+pub trait FoldingSchemeKeyGenerator: FoldingSchemeDef {
+ /// [`FoldingSchemeKeyGenerator::generate_keys`] defines the key generation
+ /// algorithm, which is a deterministic algorithm that takes as input the
+ /// public parameters `pp` and the arithmetization `arith`, and outputs a
+ /// prover key and a verifier key.
+ fn generate_keys(pp: Self::PublicParam, arith: Self::Arith) -> Result;
+}
+
+/// [`FoldingSchemeProver`] is the trait for folding scheme prover.
+pub trait FoldingSchemeProver: FoldingSchemeDef {
+ /// [`FoldingSchemeProver::prove`] defines the proof generation algorithm,
+ /// which is a (probably) randomized algorithm that takes as input the
+ /// prover key `pk`, the transcript `transcript` between the prover and the
+ /// verifier, `M` running witnesses `Ws`, `M` running instances `Us`, `N`
+ /// incoming witnesses `ws`, and `N` incoming instances `us`, and outputs
+ /// the folded witness and instance, the proof, and the challenges.
+ ///
+ /// Here, although the challenges can usually be derived by `transcript` and
+ /// thus do not necessarily need to be returned for verification, we still
+ /// have the prover return them explicitly so that they can be used for the
+ /// construction of CycleFold circuits in our CycleFold-based folding-to-IVC
+ /// compiler without re-deriving them from the transcript.
+ ///
+ /// The prover may further use `rng` as the randomness source, e.g., for
+ /// the hiding/zero-knowledge property.
+ #[allow(non_snake_case, clippy::type_complexity)]
+ fn prove(
+ pk: &::ProverKey,
+ transcript: &mut impl Transcript,
+ Ws: &[impl Borrow; M],
+ Us: &[impl Borrow; M],
+ ws: &[impl Borrow; N],
+ us: &[impl Borrow; N],
+ rng: impl RngCore,
+ ) -> Result<(Self::RW, Self::RU, Self::Proof, Self::Challenge), Error>;
+}
+
+/// [`FoldingSchemeVerifier`] is the trait for folding scheme verifier.
+pub trait FoldingSchemeVerifier: FoldingSchemeDef {
+ /// [`FoldingSchemeVerifier::verify`] defines the proof verification
+ /// algorithm, which is a deterministic algorithm that takes as input the
+ /// verifier key `vk`, the transcript `transcript` between the prover and
+ /// the verifier, `M` running instances `Us`, `N` incoming instances `us`,
+ /// and the proof `proof`, and outputs the folded instance.
+ #[allow(non_snake_case)]
+ fn verify(
+ vk: &::VerifierKey,
+ transcript: &mut impl Transcript,
+ Us: &[impl Borrow; M],
+ us: &[impl Borrow; N],
+ proof: &Self::Proof,
+ ) -> Result;
+}
+
+/// [`FoldingSchemeDecider`] is the trait for folding scheme decider.
+pub trait FoldingSchemeDecider: FoldingSchemeDef {
+ /// [`FoldingSchemeDecider::decide_running`] defines the deciding algorithm
+ /// for running witness-instance pairs, which is a deterministic algorithm
+ /// that takes as input the decider key `dk`, a running witness `W` and a
+ /// running instance `U`, and outputs whether the witness-instance pair
+ /// satisfies the running relation.
+ #[allow(non_snake_case)]
+ fn decide_running(dk: &Self::DeciderKey, W: &Self::RW, U: &Self::RU) -> Result<(), Error> {
+ Relation::::check_relation(dk, W, U)
+ }
+
+ /// [`FoldingSchemeDecider::decide_running`] defines the deciding algorithm
+ /// for incoming witness-instance pairs, which is a deterministic algorithm
+ /// that takes as input the decider key `dk`, an incoming witness `W` and an
+ /// incoming instance `U`, and outputs whether the witness-instance pair
+ /// satisfies the incoming relation.
+ fn decide_incoming(dk: &Self::DeciderKey, w: &Self::IW, u: &Self::IU) -> Result<(), Error> {
+ Relation::::check_relation(dk, w, u)
+ }
+}
+
+impl FoldingSchemeDecider for FS {}
+
+/// [`FoldingSchemeOps`] is a convenience super-trait bundling all algorithms.
+pub trait FoldingSchemeOps:
+ FoldingSchemePreprocessor
+ + FoldingSchemeKeyGenerator
+ + FoldingSchemeProver
+ + FoldingSchemeVerifier
+ + FoldingSchemeDecider
+{
+}
+
+impl FoldingSchemeOps for FS where
+ FS: FoldingSchemePreprocessor
+ + FoldingSchemeKeyGenerator
+ + FoldingSchemeProver
+ + FoldingSchemeVerifier
+ + FoldingSchemeDecider
+{
+}
diff --git a/crates/fs/src/definitions/circuits.rs b/crates/fs/src/definitions/circuits.rs
new file mode 100644
index 000000000..68d1be5f5
--- /dev/null
+++ b/crates/fs/src/definitions/circuits.rs
@@ -0,0 +1,60 @@
+//! Traits that define in-circuit gadgets for folding scheme algorithms, mainly
+//! for proof verification.
+
+use ark_relations::gr1cs::SynthesisError;
+use sonobe_primitives::{commitments::CommitmentDefGadget, transcripts::TranscriptGadget};
+
+use super::{FoldingSchemeDefGadget, algorithms::FoldingSchemeOps};
+
+/// [`FoldingSchemePartialVerifierGadget`] is the partial in-circuit verifier.
+///
+/// For schemes that have circuit-unfriendly parts in their verification, the
+/// implementation can choose to only implement this partial verifier gadget and
+/// use some other techniques for the remaining verification work.
+/// For example, group-based folding schemes can defer the expensive elliptic
+/// curve operations on commitments to an external CycleFold circuit.
+pub trait FoldingSchemePartialVerifierGadget:
+ FoldingSchemeDefGadget>
+{
+ /// [`FoldingSchemePartialVerifierGadget::verify_hinted`] defines the proof
+ /// verification gadget that matches its out-of-circuit widget
+ /// [`crate::FoldingSchemeVerifier::verify`].
+ ///
+ /// The implementation is allowed to create hints for the missing parts of
+ /// the verification that are not performed inside the constraint system,
+ /// and it is unnecessary to constrain these hints inside the circuit.
+ /// However, it is the caller's responsibility to ensure that these hints
+ /// are later verified using other techniques (e.g., CycleFold helper).
+ #[allow(non_snake_case)]
+ fn verify_hinted(
+ vk: &Self::VerifierKey,
+ transcript: &mut impl TranscriptGadget<::ConstraintField>,
+ Us: [&Self::RU; M],
+ us: [&Self::IU; N],
+ proof: &Self::Proof,
+ ) -> Result<(Self::RU, Self::Challenge), SynthesisError>;
+}
+
+/// [`FoldingSchemeFullVerifierGadget`] is the full in-circuit verifier.
+///
+/// Extends [`FoldingSchemePartialVerifierGadget`] by performing everything
+/// required for proof verification inside the constraint system.
+pub trait FoldingSchemeFullVerifierGadget:
+ FoldingSchemePartialVerifierGadget
+{
+ /// [`FoldingSchemeFullVerifierGadget::verify`] defines the proof
+ /// verification gadget that matches its out-of-circuit widget
+ /// [`crate::FoldingSchemeVerifier::verify`].
+ ///
+ /// Unlike [`FoldingSchemePartialVerifierGadget::verify_hinted`], the
+ /// implementation is expected to perform all necessary verification steps
+ /// and constrain all required variables inside the circuit.
+ #[allow(non_snake_case)]
+ fn verify(
+ vk: &Self::VerifierKey,
+ transcript: &mut impl TranscriptGadget<::ConstraintField>,
+ Us: [&Self::RU; M],
+ us: [&Self::IU; N],
+ proof: &Self::Proof,
+ ) -> Result;
+}
diff --git a/crates/fs/src/definitions/errors.rs b/crates/fs/src/definitions/errors.rs
new file mode 100644
index 000000000..d721a88dc
--- /dev/null
+++ b/crates/fs/src/definitions/errors.rs
@@ -0,0 +1,49 @@
+//! Error definitions for folding schemes.
+
+use ark_relations::gr1cs::SynthesisError;
+use sonobe_primitives::{
+ arithmetizations::Error as ArithError, commitments::Error as CommitmentError,
+ sumcheck::Error as SumCheckError,
+};
+use thiserror::Error;
+
+/// [`Error`] enumerates possible errors during folding scheme operations.
+#[derive(Debug, Error)]
+pub enum Error {
+ /// [`Error::ArithError`] indicates an error from the underlying constraint
+ /// system.
+ #[error(transparent)]
+ ArithError(#[from] ArithError),
+ /// [`Error::CommitmentError`] indicates an error from the underlying
+ /// commitment scheme.
+ #[error(transparent)]
+ CommitmentError(#[from] CommitmentError),
+ /// [`Error::SynthesisError`] indicates an error during constraint
+ /// synthesis.
+ #[error(transparent)]
+ SynthesisError(#[from] SynthesisError),
+ /// [`Error::SumCheckError`] indicates an error from the underlying sumcheck
+ /// protocol.
+ #[error(transparent)]
+ SumCheckError(#[from] SumCheckError),
+ /// [`Error::Unsupported`] indicates that a certain use case is not
+ /// supported.
+ #[error("Unsupported use case: {0}")]
+ Unsupported(String),
+ /// [`Error::DomainCreationFailure`] indicates a failure in creating
+ /// evaluation domains.
+ #[error("Failed to create domain")]
+ DomainCreationFailure,
+ /// [`Error::IndivisibleByVanishingPoly`] indicates that a polynomial is
+ /// not divisible by the vanishing polynomial of a certain domain.
+ #[error("Indivisible by vanishing polynomial")]
+ IndivisibleByVanishingPoly,
+ /// [`Error::UnsatisfiedRelation`] indicates that a certain relation is not
+ /// satisfied.
+ #[error("Unsatisfied relation: {0}")]
+ UnsatisfiedRelation(String),
+ /// [`Error::InvalidPublicParameters`] indicates that the provided public
+ /// parameters are invalid.
+ #[error("Invalid public parameters: {0}")]
+ InvalidPublicParameters(String),
+}
diff --git a/crates/fs/src/definitions/instances.rs b/crates/fs/src/definitions/instances.rs
new file mode 100644
index 000000000..cd431c448
--- /dev/null
+++ b/crates/fs/src/definitions/instances.rs
@@ -0,0 +1,114 @@
+//! Traits and abstractions for folding scheme instances.
+
+use ark_r1cs_std::{GR1CSVar, alloc::AllocVar, select::CondSelectGadget};
+use ark_relations::gr1cs::{Namespace, SynthesisError};
+use ark_std::fmt::Debug;
+use sonobe_primitives::{
+ arithmetizations::ArithConfig,
+ commitments::{CommitmentDef, CommitmentDefGadget},
+ traits::Dummy,
+ transcripts::{Absorbable, AbsorbableVar},
+};
+
+use super::utils::TaggedVec;
+
+/// [`FoldingInstance`] defines the operations that a folding scheme's instance
+/// should support.
+pub trait FoldingInstance: Clone + Debug + PartialEq + Eq + Absorbable {
+ /// [`FoldingInstance::N_COMMITMENTS`] defines the number of commitments
+ /// contained in the instance.
+ const N_COMMITMENTS: usize;
+
+ /// [`FoldingInstance::commitments`] returns the commitments contained in
+ /// the instance.
+ // TODO (@winderica): consider the scenario where the instance has multiple
+ // commitments of different types.
+ fn commitments(&self) -> Vec<&CM::Commitment>;
+
+ /// [`FoldingInstance::public_inputs`] returns the reference to the public
+ /// inputs contained in the instance.
+ fn public_inputs(&self) -> &[CM::Scalar];
+
+ /// [`FoldingInstance::public_inputs_mut`] returns the mutable reference to
+ /// the public inputs contained in the instance.
+ fn public_inputs_mut(&mut self) -> &mut [CM::Scalar];
+}
+
+/// [`PlainInstance`] is a vector of field elements that are the statements /
+/// public inputs to a constraint system.
+/// We provide this type for folding schemes that support such simple instances,
+/// enabling compatibility with the definition of accumulation schemes (i.e.,
+/// running x plain -> running).
+///
+/// To distinguish it from the witness vector, we use a tagged vector with tag
+/// `'u'` for it.
+pub type PlainInstance = TaggedVec;
+
+impl Dummy<&A> for PlainInstance {
+ fn dummy(cfg: &A) -> Self {
+ vec![V::default(); cfg.n_public_inputs()].into()
+ }
+}
+
+impl FoldingInstance for PlainInstance {
+ const N_COMMITMENTS: usize = 0;
+
+ fn commitments(&self) -> Vec<&CM::Commitment> {
+ vec![]
+ }
+
+ fn public_inputs(&self) -> &[CM::Scalar] {
+ self
+ }
+
+ fn public_inputs_mut(&mut self) -> &mut [CM::Scalar] {
+ self
+ }
+}
+
+/// [`FoldingInstanceVar`] is the in-circuit variable of [`FoldingInstance`].
+pub trait FoldingInstanceVar:
+ AllocVar
+ + GR1CSVar>
+ + AbsorbableVar
+ + CondSelectGadget
+{
+ /// [`FoldingInstanceVar::commitments`] returns the commitments contained in
+ /// the instance variable.
+ fn commitments(&self) -> Vec<&CM::CommitmentVar>;
+
+ /// [`FoldingInstanceVar::public_inputs`] returns the reference to the
+ /// public inputs contained in the instance variable.
+ fn public_inputs(&self) -> &Vec;
+
+ /// [`FoldingInstanceVar::new_witness_with_public_inputs`] allocates a
+ /// folding instance in the circuit as a witness variable, with the given
+ /// pre-allocated public inputs.
+ fn new_witness_with_public_inputs(
+ cs: impl Into>,
+ u: &Self::Value,
+ x: Vec,
+ ) -> Result;
+}
+
+impl FoldingInstanceVar for PlainInstanceVar {
+ fn commitments(&self) -> Vec<&CM::CommitmentVar> {
+ vec![]
+ }
+
+ fn public_inputs(&self) -> &Vec {
+ self
+ }
+
+ fn new_witness_with_public_inputs(
+ _cs: impl Into>,
+ _u: &Self::Value,
+ x: Vec,
+ ) -> Result {
+ Ok(Self(x))
+ }
+}
+
+/// [`PlainInstanceVar`] is the in-circuit variable of [`PlainInstance`].
+// TODO (@winderica): use a different tag?
+pub type PlainInstanceVar = PlainInstance;
diff --git a/crates/fs/src/definitions/keys.rs b/crates/fs/src/definitions/keys.rs
new file mode 100644
index 000000000..a71d7f0b7
--- /dev/null
+++ b/crates/fs/src/definitions/keys.rs
@@ -0,0 +1,25 @@
+//! Traits and abstractions for folding scheme keys.
+
+use sonobe_primitives::arithmetizations::ArithConfig;
+
+/// [`DeciderKey`] defines the information that a folding scheme's decider key
+/// should include or provide access to.
+pub trait DeciderKey {
+ /// [`DeciderKey::ProverKey`] is the type of the prover key contained in the
+ /// decider key.
+ type ProverKey;
+ /// [`DeciderKey::VerifierKey`] is the type of the verifier key contained in
+ /// the decider key.
+ type VerifierKey;
+ /// [`DeciderKey::ArithConfig`] is the constraint system configuration
+ /// associated with the folding scheme.
+ type ArithConfig: ArithConfig;
+
+ /// [`DeciderKey::to_pk`] returns the reference to the prover key.
+ fn to_pk(&self) -> &Self::ProverKey;
+ /// [`DeciderKey::to_vk`] returns the reference to the verifier key.
+ fn to_vk(&self) -> &Self::VerifierKey;
+ /// [`DeciderKey::to_arith_config`] returns the reference to the constraint
+ /// system configuration.
+ fn to_arith_config(&self) -> &Self::ArithConfig;
+}
diff --git a/crates/fs/src/definitions/mod.rs b/crates/fs/src/definitions/mod.rs
new file mode 100644
index 000000000..38a737027
--- /dev/null
+++ b/crates/fs/src/definitions/mod.rs
@@ -0,0 +1,137 @@
+//! Shared traits for folding schemes, including definitions of related
+//! cryptographic objects and algorithms in and out of circuit.
+
+pub mod algorithms;
+pub mod circuits;
+pub mod errors;
+pub mod instances;
+pub mod keys;
+pub mod utils;
+pub mod variants;
+pub mod witnesses;
+
+use ark_r1cs_std::{GR1CSVar, alloc::AllocVar};
+use sonobe_primitives::{
+ arithmetizations::Arith,
+ circuits::AssignmentsOwned,
+ commitments::{CommitmentDef, CommitmentDefGadget},
+ relations::{Relation, WitnessInstanceSampler},
+ traits::{Dummy, SonobeField},
+};
+
+use self::{
+ errors::Error,
+ instances::{FoldingInstance, FoldingInstanceVar},
+ keys::DeciderKey,
+ witnesses::FoldingWitness,
+};
+
+/// [`FoldingSchemeDef`] provides the core type definitions of a folding scheme.
+///
+/// A folding scheme is a cryptographic primitive that folds multiple instances
+/// of computations into a single instance while preserving the validity of the
+/// computations.
+/// More specifically, a folding scheme in general considers two relations `R1`
+/// and `R2`.
+/// The folding prover folds `M` witness-instance pairs satisfying `R1` and `N`
+/// witness-instance pairs satisfying `R2` into a single witness-instance pair
+/// satisfying `R1`, along with a proof that the folding was done correctly.
+/// The folding verifier folds `M` instances of `R1` and `N` instances of `R2`
+/// into a single instance of `R1` under the help of the proof.
+///
+/// While folding schemes can be applied in various contexts, we primarily focus
+/// on their use in constructing recursive proof systems, and thus we refer to
+/// `R1` as the "running relation" and `R2` as the "incoming relation" in the
+/// codebase.
+/// A witness-instance pair `(W, U)` of type `(RW, RU)` for `R1` is called a
+/// "running" witness-instance pair, while a witness-instance pair `(w, u)` of
+/// type `(IW, IU)` for `R2` is called an "incoming" witness-instance pair.
+///
+/// Different folding schemes support different running and incoming relations,
+/// as well as the number of witness-instance pairs that can be folded at once.
+pub trait FoldingSchemeDef {
+ /// [`FoldingSchemeDef::CM`] is the commitment scheme used by the folding
+ /// scheme.
+ type CM: CommitmentDef;
+ /// [`FoldingSchemeDef::RW`] is the type of running witness.
+ type RW: FoldingWitness + for<'a> Dummy<&'a ::Config>;
+ /// [`FoldingSchemeDef::RU`] is the type of running instance.
+ type RU: FoldingInstance + for<'a> Dummy<&'a ::Config>;
+ /// [`FoldingSchemeDef::IW`] is the type of incoming witness.
+ type IW: FoldingWitness + for<'a> Dummy<&'a ::Config>;
+ /// [`FoldingSchemeDef::IU`] is the type of incoming instance.
+ type IU: FoldingInstance + for<'a> Dummy<&'a ::Config>;
+ /// [`FoldingSchemeDef::TranscriptField`] is the field type used in the
+ /// transcript of the folding scheme.
+ type TranscriptField: SonobeField;
+ /// [`FoldingSchemeDef::Arith`] is the constraint system supported by the
+ /// folding scheme.
+ type Arith: Arith::ArithConfig>;
+ /// [`FoldingSchemeDef::Config`] is the type of configuration required to
+ /// generate the public parameters of the folding scheme.
+ type Config;
+ /// [`FoldingSchemeDef::PublicParam`] is the type of public parameters of
+ /// the folding scheme.
+ type PublicParam;
+ /// [`FoldingSchemeDef::DeciderKey`] is the type of decider key of the
+ /// folding scheme, which is used to determine the satisfiability of a
+ /// witness-instance pair.
+ type DeciderKey: DeciderKey
+ + Clone
+ + Relation
+ + Relation
+ + WitnessInstanceSampler
+ + WitnessInstanceSampler<
+ Self::IW,
+ Self::IU,
+ Source = AssignmentsOwned<::Scalar>,
+ Error = Error,
+ >;
+ /// [`FoldingSchemeDef::Challenge`] is the type of challenge generated
+ /// during the folding process.
+ type Challenge;
+ /// [`FoldingSchemeDef::Proof`] is the type of proof generated by the
+ /// folding prover.
+ type Proof: Clone
+ + for<'a> Dummy<&'a ::Config>;
+}
+
+/// [`FoldingSchemeDefGadget`] specifies the in-circuit associated types for a
+/// folding scheme gadget.
+pub trait FoldingSchemeDefGadget {
+ /// [`FoldingSchemeDefGadget::Widget`] points to the out-of-circuit folding
+ /// scheme widget.
+ type Widget: FoldingSchemeDef;
+
+ /// [`FoldingSchemeDefGadget::CM`] is the commitment scheme gadget.
+ type CM: CommitmentDefGadget::CM>;
+ /// [`FoldingSchemeDefGadget::RU`] is the type of in-circuit running
+ /// instance variable.
+ type RU: FoldingInstanceVar::RU>;
+ /// [`FoldingSchemeDefGadget::IU`] is the type of in-circuit incoming
+ /// instance variable.
+ type IU: FoldingInstanceVar::IU>;
+
+ /// [`FoldingSchemeDefGadget::VerifierKey`] is the type of in-circuit
+ /// verifier key variable.
+ type VerifierKey;
+
+ /// [`FoldingSchemeDefGadget::Challenge`] is the type of in-circuit
+ /// challenge variable.
+ type Challenge: AllocVar<
+ ::Challenge,
+ ::ConstraintField,
+ > + GR1CSVar<
+ ::ConstraintField,
+ Value = ::Challenge,
+ >;
+ /// [`FoldingSchemeDefGadget::Proof`] is the type of in-circuit proof
+ /// variable.
+ type Proof: AllocVar<
+ ::Proof,
+ ::ConstraintField,
+ > + GR1CSVar<
+ ::ConstraintField,
+ Value = ::Proof,
+ >;
+}
diff --git a/crates/fs/src/definitions/utils.rs b/crates/fs/src/definitions/utils.rs
new file mode 100644
index 000000000..f4d27acb8
--- /dev/null
+++ b/crates/fs/src/definitions/utils.rs
@@ -0,0 +1,107 @@
+//! Utility types shared across folding scheme definitions.
+
+use ark_ff::{Field, PrimeField};
+use ark_r1cs_std::{
+ GR1CSVar,
+ alloc::{AllocVar, AllocationMode},
+ fields::fp::FpVar,
+ prelude::Boolean,
+ select::CondSelectGadget,
+};
+use ark_relations::gr1cs::{ConstraintSystemRef, Namespace, SynthesisError};
+use ark_std::{
+ borrow::Borrow,
+ ops::{Deref, DerefMut},
+};
+use sonobe_primitives::transcripts::{Absorbable, AbsorbableVar};
+
+/// [`TaggedVec`] is a wrapper around a vector that additionally carries a
+/// compile-time `char` tag.
+///
+/// This is used to create nominally distinct vector types that are structurally
+/// identical.
+#[derive(Clone, Debug, Default, PartialEq, Eq)]
+pub struct TaggedVec(pub Vec);
+
+impl Deref for TaggedVec {
+ type Target = Vec;
+
+ fn deref(&self) -> &Self::Target {
+ &self.0
+ }
+}
+
+impl DerefMut for TaggedVec {
+ fn deref_mut(&mut self) -> &mut Self::Target {
+ &mut self.0
+ }
+}
+
+impl From> for TaggedVec {
+ fn from(v: Vec) -> Self {
+ Self(v)
+ }
+}
+
+impl From> for Vec {
+ fn from(val: TaggedVec) -> Self {
+ val.0
+ }
+}
+
+impl Absorbable for TaggedVec {
+ fn absorb_into(&self, dest: &mut Vec) {
+ self.0.absorb_into(dest)
+ }
+}
+
+impl, const TAG: char> AbsorbableVar for TaggedVec {
+ fn absorb_into(&self, dest: &mut Vec>) -> Result<(), SynthesisError> {
+ self.0.absorb_into(dest)
+ }
+}
+
+impl, Y, const TAG: char> AllocVar, F>
+ for TaggedVec
+{
+ fn new_variable>>(
+ cs: impl Into>,
+ f: impl FnOnce() -> Result,
+ mode: AllocationMode,
+ ) -> Result {
+ let v = f()?;
+ Vec::new_variable(cs, || Ok(&v.borrow()[..]), mode).map(Self)
+ }
+}
+
+impl, const TAG: char> CondSelectGadget
+ for TaggedVec
+{
+ fn conditionally_select(
+ cond: &Boolean,
+ true_value: &Self,
+ false_value: &Self,
+ ) -> Result {
+ if true_value.len() != false_value.len() {
+ return Err(SynthesisError::Unsatisfiable);
+ }
+ true_value
+ .iter()
+ .zip(false_value.iter())
+ .map(|(t, f)| cond.select(t, f))
+ .collect::>()
+ .map(Self)
+ }
+}
+
+impl, const TAG: char> GR1CSVar for TaggedVec {
+ type Value = TaggedVec;
+
+ fn cs(&self) -> ConstraintSystemRef {
+ self.0.cs()
+ }
+
+ fn value(&self) -> Result {
+ self.0.value().map(TaggedVec)
+ }
+}
diff --git a/crates/fs/src/definitions/variants.rs b/crates/fs/src/definitions/variants.rs
new file mode 100644
index 000000000..b3655f37d
--- /dev/null
+++ b/crates/fs/src/definitions/variants.rs
@@ -0,0 +1,68 @@
+//! Traits that define variants of folding schemes based on different underlying
+//! mathematical structures.
+
+use sonobe_primitives::{
+ commitments::{CommitmentDef, GroupBasedCommitment},
+ traits::CF2,
+};
+
+use crate::{
+ FoldingSchemeDef, FoldingSchemeDefGadget, FoldingSchemeFullVerifierGadget, FoldingSchemeOps,
+ FoldingSchemePartialVerifierGadget,
+};
+
+/// [`GroupBasedFoldingSchemePrimaryDef`] defines a folding scheme based on
+/// groups (elliptic curves), whose transcript field is the scalar field of its
+/// group-based commitment scheme.
+pub trait GroupBasedFoldingSchemePrimaryDef:
+ FoldingSchemeDef<
+ CM: GroupBasedCommitment,
+ TranscriptField = <::CM as CommitmentDef>::Scalar,
+ >
+{
+ /// [`GroupBasedFoldingSchemePrimaryDef::Gadget`] is the in-circuit gadget
+ /// that defines the folding scheme.
+ type Gadget: FoldingSchemeDefGadget::Gadget2>;
+}
+
+/// [`GroupBasedFoldingSchemePrimary`] is a convenience trait that combines the
+/// definition [`GroupBasedFoldingSchemePrimaryDef`] and operations
+/// [`FoldingSchemeOps`].
+pub trait GroupBasedFoldingSchemePrimary:
+ GroupBasedFoldingSchemePrimaryDef>
+ + FoldingSchemeOps
+{
+}
+
+impl GroupBasedFoldingSchemePrimary for FS where
+ FS: GroupBasedFoldingSchemePrimaryDef>
+{
+}
+
+/// [`GroupBasedFoldingSchemeSecondaryDef`] defines a folding scheme based on
+/// groups (elliptic curves), whose transcript field is the base field of its
+/// group-based commitment scheme.
+pub trait GroupBasedFoldingSchemeSecondaryDef:
+ FoldingSchemeDef<
+ CM: GroupBasedCommitment,
+ TranscriptField = CF2<<::CM as CommitmentDef>::Commitment>,
+ >
+{
+ /// [`GroupBasedFoldingSchemeSecondaryDef::Gadget`] is the in-circuit gadget
+ /// that defines the folding scheme.
+ type Gadget: FoldingSchemeDefGadget::Gadget1>;
+}
+
+/// [`GroupBasedFoldingSchemeSecondary`] is a convenience trait that combines
+/// the definition [`GroupBasedFoldingSchemeSecondaryDef`] and operations
+/// [`FoldingSchemeOps`].
+pub trait GroupBasedFoldingSchemeSecondary:
+ GroupBasedFoldingSchemeSecondaryDef>
+ + FoldingSchemeOps
+{
+}
+
+impl GroupBasedFoldingSchemeSecondary for FS where
+ FS: GroupBasedFoldingSchemeSecondaryDef>
+{
+}
diff --git a/crates/fs/src/definitions/witnesses.rs b/crates/fs/src/definitions/witnesses.rs
new file mode 100644
index 000000000..95da4b78b
--- /dev/null
+++ b/crates/fs/src/definitions/witnesses.rs
@@ -0,0 +1,65 @@
+//! Traits and abstractions for folding scheme witnesses.
+
+use ark_r1cs_std::{GR1CSVar, alloc::AllocVar};
+use ark_std::fmt::Debug;
+use sonobe_primitives::{
+ arithmetizations::ArithConfig,
+ commitments::{CommitmentDef, CommitmentDefGadget},
+ traits::Dummy,
+};
+
+use super::utils::TaggedVec;
+
+/// [`FoldingWitness`] defines the operations that a folding scheme's witness
+/// should support.
+pub trait FoldingWitness: Debug {
+ /// [`FoldingWitness::N_OPENINGS`] defines the number of openings contained
+ /// in the witness.
+ const N_OPENINGS: usize;
+
+ /// [`FoldingWitness::openings`] returns the reference to all openings
+ /// contained in the witness, where each opening a tuple of the values being
+ /// committed to and the randomness used in the commitment.
+ fn openings(&self) -> Vec<(&[CM::Scalar], &CM::Randomness)>;
+}
+
+/// [`PlainWitness`] is a vector of field elements that are the witnesses to a
+/// constraint system.
+/// We provide this type for folding schemes that support such simple witnesses,
+/// enabling compatibility with the definition of accumulation schemes (i.e.,
+/// running x plain -> running).
+///
+/// To distinguish it from the instance vector, we use a tagged vector with tag
+/// `'w'` for it.
+pub type PlainWitness = TaggedVec;
+
+impl Dummy<&A> for PlainWitness {
+ fn dummy(cfg: &A) -> Self {
+ vec![V::default(); cfg.n_witnesses()].into()
+ }
+}
+
+impl FoldingWitness for PlainWitness {
+ const N_OPENINGS: usize = 0;
+
+ fn openings(&self) -> Vec<(&[CM::Scalar], &CM::Randomness)> {
+ vec![]
+ }
+}
+
+/// [`FoldingWitnessVar`] is the in-circuit variable of [`FoldingWitness`].
+pub trait FoldingWitnessVar:
+ AllocVar
+ + GR1CSVar>
+{
+}
+
+impl FoldingWitnessVar for T where
+ T: AllocVar
+ + GR1CSVar>
+{
+}
+
+/// [`PlainWitnessVar`] is the in-circuit variable of [`PlainWitness`].
+// TODO (@winderica): use a different tag?
+pub type PlainWitnessVar = PlainWitness;
diff --git a/crates/fs/src/hypernova/algorithms/key_generator.rs b/crates/fs/src/hypernova/algorithms/key_generator.rs
new file mode 100644
index 000000000..7c5c709e9
--- /dev/null
+++ b/crates/fs/src/hypernova/algorithms/key_generator.rs
@@ -0,0 +1,42 @@
+//! Key generation for HyperNova.
+
+use ark_std::sync::Arc;
+use sonobe_primitives::{
+ arithmetizations::{Arith, ArithConfig, ccs::CCSVariant},
+ commitments::{CommitmentKey, GroupBasedCommitment},
+};
+
+use crate::{
+ Error, FoldingSchemeKeyGenerator,
+ hypernova::{HyperNova, HyperNova2},
+};
+
+impl FoldingSchemeKeyGenerator
+ for HyperNova
+{
+ fn generate_keys(ck: Self::PublicParam, ccs: Self::Arith) -> Result {
+ let ck = Arc::new(ck);
+ let ccs = Arc::new(ccs);
+ if ck.max_scalars_len() < ccs.config().n_witnesses() {
+ return Err(Error::InvalidPublicParameters(
+ "The commitment key is too short for the CCS instance".into(),
+ ));
+ }
+ Ok(Self::DeciderKey { arith: ccs, ck })
+ }
+}
+
+impl FoldingSchemeKeyGenerator
+ for HyperNova2
+{
+ fn generate_keys(ck: Self::PublicParam, ccs: Self::Arith) -> Result {
+ let ck = Arc::new(ck);
+ let ccs = Arc::new(ccs);
+ if ck.max_scalars_len() < ccs.config().n_witnesses() {
+ return Err(Error::InvalidPublicParameters(
+ "The commitment key is too short for the CCS instance".into(),
+ ));
+ }
+ Ok(Self::DeciderKey { arith: ccs, ck })
+ }
+}
diff --git a/crates/fs/src/hypernova/algorithms/mod.rs b/crates/fs/src/hypernova/algorithms/mod.rs
new file mode 100644
index 000000000..2b6a65a6e
--- /dev/null
+++ b/crates/fs/src/hypernova/algorithms/mod.rs
@@ -0,0 +1,6 @@
+//! Implementations folding scheme algorithms for HyperNova.
+
+pub mod key_generator;
+pub mod preprocessor;
+pub mod prover;
+pub mod verifier;
diff --git a/crates/fs/src/hypernova/algorithms/preprocessor.rs b/crates/fs/src/hypernova/algorithms/preprocessor.rs
new file mode 100644
index 000000000..f4624318d
--- /dev/null
+++ b/crates/fs/src/hypernova/algorithms/preprocessor.rs
@@ -0,0 +1,27 @@
+//! Preprocessing for HyperNova.
+
+use ark_std::rand::RngCore;
+use sonobe_primitives::{arithmetizations::ccs::CCSVariant, commitments::GroupBasedCommitment};
+
+use crate::{
+ Error, FoldingSchemePreprocessor,
+ hypernova::{HyperNova, HyperNova2},
+};
+
+impl FoldingSchemePreprocessor
+ for HyperNova
+{
+ fn preprocess(ck_len: usize, mut rng: impl RngCore) -> Result {
+ let ck = CM::generate_key(ck_len, &mut rng)?;
+ Ok(ck)
+ }
+}
+
+impl FoldingSchemePreprocessor
+ for HyperNova2
+{
+ fn preprocess(ck_len: usize, mut rng: impl RngCore) -> Result {
+ let ck = CM::generate_key(ck_len, &mut rng)?;
+ Ok(ck)
+ }
+}
diff --git a/crates/fs/src/hypernova/algorithms/prover.rs b/crates/fs/src/hypernova/algorithms/prover.rs
new file mode 100644
index 000000000..4ee5ba037
--- /dev/null
+++ b/crates/fs/src/hypernova/algorithms/prover.rs
@@ -0,0 +1,324 @@
+//! Proof generation for HyperNova.
+
+use ark_ff::One;
+use ark_poly::{DenseMultilinearExtension as MLE, MultilinearExtension};
+use ark_std::{borrow::Borrow, rand::RngCore};
+use sonobe_primitives::{
+ algebra::ops::{
+ bits::FromBits,
+ pow::Pow,
+ rlc::{ScalarRLC, SliceRLC},
+ },
+ arithmetizations::{Arith, ArithConfig, ccs::CCSVariant},
+ commitments::GroupBasedCommitment,
+ sumcheck::{
+ SumCheck,
+ utils::{EqPoly, VPAuxInfo, VirtualPolynomial},
+ },
+ transcripts::Transcript,
+};
+
+use crate::{
+ Error, FoldingSchemeProver,
+ hypernova::{HyperNova, HyperNova2, HyperNovaKey, NIMFSProof},
+};
+
+impl<
+ CM: GroupBasedCommitment,
+ V: CCSVariant,
+ const M: usize,
+ const N: usize,
+ const CHALLENGE_BITS: usize,
+> FoldingSchemeProver for HyperNova
+{
+ #[allow(non_snake_case)]
+ fn prove(
+ pk: &HyperNovaKey,
+ transcript: &mut impl Transcript,
+ Ws: &[impl Borrow; M],
+ Us: &[impl Borrow; M],
+ ws: &[impl Borrow; N],
+ us: &[impl Borrow; N],
+ _rng: impl RngCore,
+ ) -> Result<(Self::RW, Self::RU, Self::Proof, Self::Challenge), Error> {
+ let Ws = &Ws.iter().map(|i| i.borrow()).collect::>();
+ let Us = &Us.iter().map(|i| i.borrow()).collect::>();
+ let ws = &ws.iter().map(|i| i.borrow()).collect::>();
+ let us = &us.iter().map(|i| i.borrow()).collect::>();
+
+ let ccs = &pk.arith;
+ let d = V::degree();
+ let s = ccs.config().log_constraints();
+ let t = V::n_matrices();
+ let S = &V::multisets_vec();
+ let c = &V::coefficients_vec::();
+
+ // absorb instances to transcript
+ transcript.add(&Us[..]);
+ transcript.add(&us[..]);
+
+ // Step 1: Get some challenges
+ let gamma = transcript.challenge_field_element();
+ let beta = transcript.challenge_field_elements(s);
+
+ let gamma_powers = gamma.powers(M * t + N);
+ let (running_gammas, incoming_gammas) = gamma_powers.split_at(M * t);
+
+ // Compute g(x)
+ let running_mles = Ws
+ .iter()
+ .zip(Us)
+ .flat_map(|(W, U)| ccs.mles((U.u, &U.x, &W.w).into()));
+ let incoming_mles = ws
+ .iter()
+ .zip(us)
+ .flat_map(|(w, u)| ccs.mles((One::one(), &u.x, &w.w).into()));
+ let eq_mles = Us
+ .iter()
+ .map(|U| &U.r_x)
+ .chain([&beta])
+ .map(|r| MLE::from_evaluations_vec(s, EqPoly::fix_y_evals(r)));
+
+ let running_products = running_gammas
+ .iter()
+ .enumerate()
+ .map(|(i, &gamma)| (gamma, vec![i, (M + N) * t + i / t]));
+ let incoming_products = incoming_gammas.iter().enumerate().flat_map(|(k, gamma)| {
+ S.iter().zip(c).map(move |(S_i, &c_i)| {
+ (
+ c_i * gamma,
+ S_i.iter()
+ .map(|j| (M + k) * t + j)
+ .chain([(M + N) * t + M])
+ .collect(),
+ )
+ })
+ });
+
+ let g = VirtualPolynomial {
+ aux_info: VPAuxInfo {
+ num_variables: s,
+ max_degree: d + 1,
+ },
+ flattened_ml_extensions: running_mles.chain(incoming_mles).chain(eq_mles).collect(),
+ products: running_products.chain(incoming_products).collect(),
+ };
+
+ // Step 3: Run the sumcheck prover
+ // Step 2: dig into the sumcheck and extract r_x_prime
+ let (sumcheck_proof, r_x_prime, mles) = SumCheck::prove(g, transcript)?;
+
+ // Step 4: compute sigmas and thetas
+ let sigmas = mles[0..t * M]
+ .iter()
+ .map(|mle| mle.fix_variables(&[])[0])
+ .collect::>();
+ let thetas = mles[t * M..t * (M + N)]
+ .iter()
+ .map(|mle| mle.fix_variables(&[])[0])
+ .collect::>();
+
+ // Step 6: Get the folding challenge
+ let rho_bits = transcript.challenge_bits(CHALLENGE_BITS);
+ let rho = CM::Scalar::from_bits_le(&rho_bits);
+
+ let rho_powers = rho.powers(M + N);
+
+ Ok((
+ Self::RW {
+ w: Ws
+ .iter()
+ .map(|w| &w.w[..])
+ .chain(ws.iter().map(|w| &w.w[..]))
+ .slice_rlc(&rho_powers),
+ r: Ws
+ .iter()
+ .map(|w| w.r)
+ .chain(ws.iter().map(|w| w.r))
+ .scalar_rlc(&rho_powers),
+ },
+ Self::RU {
+ cm: Us
+ .iter()
+ .map(|u| u.cm)
+ .chain(us.iter().map(|u| u.cm))
+ .scalar_rlc(&rho_powers),
+ u: Us
+ .iter()
+ .map(|u| u.u)
+ .chain([CM::Scalar::one(); N])
+ .scalar_rlc(&rho_powers),
+ x: Us
+ .iter()
+ .map(|u| &u.x[..])
+ .chain(us.iter().map(|u| &u.x[..]))
+ .slice_rlc(&rho_powers),
+ r_x: r_x_prime,
+ v: sigmas
+ .chunks(t)
+ .chain(thetas.chunks(t))
+ .slice_rlc(&rho_powers),
+ },
+ NIMFSProof {
+ sc_proof: sumcheck_proof,
+ sigmas,
+ thetas,
+ },
+ rho_bits.try_into().unwrap(),
+ ))
+ }
+}
+
+impl<
+ CM: GroupBasedCommitment,
+ V: CCSVariant,
+ const M: usize,
+ const N: usize,
+ const CHALLENGE_BITS: usize,
+> FoldingSchemeProver for HyperNova2
+{
+ #[allow(non_snake_case)]
+ fn prove(
+ pk: &HyperNovaKey,
+ transcript: &mut impl Transcript,
+ Ws: &[impl Borrow; M],
+ Us: &[impl Borrow; M],
+ ws: &[impl Borrow; N],
+ us: &[impl Borrow; N],
+ mut rng: impl RngCore,
+ ) -> Result<(Self::RW, Self::RU, Self::Proof, Self::Challenge), Error> {
+ let Ws = &Ws.iter().map(|i| i.borrow()).collect::>();
+ let Us = &Us.iter().map(|i| i.borrow()).collect::>();
+ let ws = &ws.iter().map(|i| i.borrow()).collect::>();
+ let us = &us.iter().map(|i| i.borrow()).collect::>();
+
+ let ccs = &pk.arith;
+ let d = V::degree();
+ let s = ccs.config().log_constraints();
+ let t = V::n_matrices();
+ let S = &V::multisets_vec();
+ let c = &V::coefficients_vec::();
+
+ let mut cms = [CM::Commitment::default(); N];
+ let mut rs = [CM::Randomness::default(); N];
+ for i in 0..N {
+ let (cm, r) = CM::commit(&pk.ck, ws[i], &mut rng)?;
+ cms[i] = cm;
+ rs[i] = r;
+ }
+
+ // absorb instances to transcript
+ transcript.add(&Us[..]);
+ transcript.add(&us[..]);
+ transcript.add(&cms[..]);
+
+ // Step 1: Get some challenges
+ let gamma = transcript.challenge_field_element();
+ let beta = transcript.challenge_field_elements(s);
+
+ let gamma_powers = gamma.powers(M * t + N);
+ let (running_gammas, incoming_gammas) = gamma_powers.split_at(M * t);
+
+ // Compute g(x)
+ let running_mles = Ws
+ .iter()
+ .zip(Us)
+ .flat_map(|(W, U)| ccs.mles((U.u, &U.x, &W.w).into()));
+ let incoming_mles = ws
+ .iter()
+ .zip(us)
+ .flat_map(|(w, u)| ccs.mles((One::one(), &u[..], &w[..]).into()));
+ let eq_mles = Us
+ .iter()
+ .map(|U| &U.r_x)
+ .chain([&beta])
+ .map(|r| MLE::from_evaluations_vec(s, EqPoly::fix_y_evals(r)));
+
+ let running_products = running_gammas
+ .iter()
+ .enumerate()
+ .map(|(i, &gamma)| (gamma, vec![i, (M + N) * t + i / t]));
+ let incoming_products = incoming_gammas.iter().enumerate().flat_map(|(k, gamma)| {
+ S.iter().zip(c).map(move |(S_i, &c_i)| {
+ (
+ c_i * gamma,
+ S_i.iter()
+ .map(|j| (M + k) * t + j)
+ .chain([(M + N) * t + M])
+ .collect(),
+ )
+ })
+ });
+
+ let g = VirtualPolynomial {
+ aux_info: VPAuxInfo {
+ num_variables: s,
+ max_degree: d + 1,
+ },
+ flattened_ml_extensions: running_mles.chain(incoming_mles).chain(eq_mles).collect(),
+ products: running_products.chain(incoming_products).collect(),
+ };
+
+ // Step 3: Run the sumcheck prover
+ // Step 2: dig into the sumcheck and extract r_x_prime
+ let (sumcheck_proof, r_x_prime, mles) = SumCheck::prove(g, transcript)?;
+
+ // Step 4: compute sigmas and thetas
+ let sigmas = mles[0..t * M]
+ .iter()
+ .map(|mle| mle.fix_variables(&[])[0])
+ .collect::>();
+ let thetas = mles[t * M..t * (M + N)]
+ .iter()
+ .map(|mle| mle.fix_variables(&[])[0])
+ .collect::>();
+
+ // Step 6: Get the folding challenge
+ let rho_bits = transcript.challenge_bits(CHALLENGE_BITS);
+ let rho = CM::Scalar::from_bits_le(&rho_bits);
+
+ let rho_powers = rho.powers(M + N);
+
+ Ok((
+ Self::RW {
+ w: Ws
+ .iter()
+ .map(|w| &w.w[..])
+ .chain(ws.iter().map(|w| &w[..]))
+ .slice_rlc(&rho_powers),
+ r: Ws.iter().map(|w| w.r).chain(rs).scalar_rlc(&rho_powers),
+ },
+ Self::RU {
+ cm: Us
+ .iter()
+ .map(|u| u.cm)
+ .chain(cms.iter().copied())
+ .scalar_rlc(&rho_powers),
+ u: Us
+ .iter()
+ .map(|u| u.u)
+ .chain([CM::Scalar::one(); N])
+ .scalar_rlc(&rho_powers),
+ x: Us
+ .iter()
+ .map(|u| &u.x[..])
+ .chain(us.iter().map(|u| &u[..]))
+ .slice_rlc(&rho_powers),
+ r_x: r_x_prime,
+ v: sigmas
+ .chunks(t)
+ .chain(thetas.chunks(t))
+ .slice_rlc(&rho_powers),
+ },
+ (
+ cms,
+ NIMFSProof {
+ sc_proof: sumcheck_proof,
+ sigmas,
+ thetas,
+ },
+ ),
+ rho_bits.try_into().unwrap(),
+ ))
+ }
+}
diff --git a/crates/fs/src/hypernova/algorithms/verifier.rs b/crates/fs/src/hypernova/algorithms/verifier.rs
new file mode 100644
index 000000000..324e8e4a6
--- /dev/null
+++ b/crates/fs/src/hypernova/algorithms/verifier.rs
@@ -0,0 +1,244 @@
+//! Proof verification for HyperNova.
+
+use ark_ff::One;
+use ark_std::borrow::Borrow;
+use sonobe_primitives::{
+ algebra::ops::{
+ bits::FromBits,
+ pow::Pow,
+ rlc::{ScalarRLC, SliceRLC},
+ },
+ arithmetizations::ccs::CCSVariant,
+ commitments::GroupBasedCommitment,
+ sumcheck::{
+ Error as SumCheckError, SumCheck,
+ utils::{EqPoly, VPAuxInfo},
+ },
+ transcripts::Transcript,
+};
+
+use crate::{
+ Error, FoldingSchemeVerifier,
+ hypernova::{HyperNova, HyperNova2},
+};
+
+impl<
+ CM: GroupBasedCommitment,
+ V: CCSVariant,
+ const M: usize,
+ const N: usize,
+ const CHALLENGE_BITS: usize,
+> FoldingSchemeVerifier for HyperNova
+{
+ #[allow(non_snake_case)]
+ fn verify(
+ _vk: &(),
+ transcript: &mut impl Transcript,
+ Us: &[impl Borrow; M],
+ us: &[impl Borrow; N],
+ proof: &Self::Proof,
+ ) -> Result {
+ let Us = &Us.iter().map(|i| i.borrow()).collect::>();
+ let us = &us.iter().map(|i| i.borrow()).collect::>();
+
+ let d = V::degree();
+ let s = proof.sc_proof.len();
+ let t = V::n_matrices();
+ let S = &V::multisets_vec();
+ let c = &V::coefficients_vec::();
+
+ // absorb instances to transcript
+ transcript.add(&Us[..]);
+ transcript.add(&us[..]);
+
+ // Step 1: Get some challenges
+ let gamma = transcript.challenge_field_element();
+ let beta = transcript.challenge_field_elements(s);
+
+ let gamma_powers = gamma.powers(M * t + N);
+
+ let vp_aux_info = VPAuxInfo {
+ max_degree: d + 1,
+ num_variables: s,
+ };
+
+ // Step 3: Start verifying the sumcheck
+ // First, compute the expected sumcheck sum: \sum gamma^j v_j
+ let sum_v_j_gamma = Us
+ .iter()
+ .zip(gamma_powers.chunks(t))
+ .flat_map(|(U, gammas)| U.v.iter().zip(gammas).map(|(&v, &g)| v * g))
+ .sum();
+
+ // Verify the interactive part of the sumcheck
+ // Step 2: Dig into the sumcheck claim and extract the randomness used
+ let (claimed_eval, r_x_prime) =
+ SumCheck::verify(sum_v_j_gamma, &proof.sc_proof, &vp_aux_info, transcript)?;
+
+ // Step 5: Finish verifying sumcheck (verify the claim c)
+ let e_beta = EqPoly::fix_xy_eval(&beta, &r_x_prime);
+ let c = proof
+ .sigmas
+ .chunks(t)
+ .zip(Us)
+ .flat_map(|(sigmas, u)| {
+ let e_lcccs = EqPoly::fix_xy_eval(&u.r_x, &r_x_prime);
+ sigmas.iter().map(move |sigma_j| e_lcccs * sigma_j)
+ })
+ .chain(proof.thetas.chunks(t).map(|thetas| {
+ S.iter()
+ .zip(c)
+ .map(|(S_i, &c_i)| c_i * S_i.iter().map(|&j| thetas[j]).product::())
+ .sum::()
+ * e_beta
+ }))
+ .zip(gamma_powers)
+ .map(|(val, gamma_i)| val * gamma_i)
+ .sum::();
+ // check that the g(r_x') from the sumcheck proof is equal to the computed c from sigmas&thetas
+ (c == claimed_eval).then_some(()).ok_or_else(|| {
+ SumCheckError::IncorrectEvaluation(claimed_eval.to_string(), c.to_string())
+ })?;
+
+ // Step 6: Get the folding challenge
+ let rho_bits = transcript.challenge_bits(CHALLENGE_BITS);
+ let rho = CM::Scalar::from_bits_le(&rho_bits);
+
+ let rho_powers = rho.powers(M + N);
+
+ Ok(Self::RU {
+ cm: Us
+ .iter()
+ .map(|u| u.cm)
+ .chain(us.iter().map(|u| u.cm))
+ .scalar_rlc(&rho_powers),
+ u: Us
+ .iter()
+ .map(|u| u.u)
+ .chain([CM::Scalar::one(); N])
+ .scalar_rlc(&rho_powers),
+ x: Us
+ .iter()
+ .map(|u| &u.x[..])
+ .chain(us.iter().map(|u| &u.x[..]))
+ .slice_rlc(&rho_powers),
+ r_x: r_x_prime,
+ v: proof
+ .sigmas
+ .chunks(t)
+ .chain(proof.thetas.chunks(t))
+ .slice_rlc(&rho_powers),
+ })
+ }
+}
+
+impl<
+ CM: GroupBasedCommitment,
+ V: CCSVariant,
+ const M: usize,
+ const N: usize,
+ const CHALLENGE_BITS: usize,
+> FoldingSchemeVerifier for HyperNova2
+{
+ #[allow(non_snake_case)]
+ fn verify(
+ _vk: &(),
+ transcript: &mut impl Transcript,
+ Us: &[impl Borrow; M],
+ us: &[impl Borrow; N],
+ (cms, proof): &Self::Proof,
+ ) -> Result {
+ let Us = &Us.iter().map(|i| i.borrow()).collect::>();
+ let us = &us.iter().map(|i| i.borrow()).collect::>();
+
+ let d = V::degree();
+ let s = proof.sc_proof.len();
+ let t = V::n_matrices();
+ let S = &V::multisets_vec();
+ let c = &V::coefficients_vec::();
+
+ // absorb instances to transcript
+ transcript.add(&Us[..]);
+ transcript.add(&us[..]);
+ transcript.add(&cms[..]);
+
+ // Step 1: Get some challenges
+ let gamma = transcript.challenge_field_element();
+ let beta = transcript.challenge_field_elements(s);
+
+ let gamma_powers = gamma.powers(M * t + N);
+
+ let vp_aux_info = VPAuxInfo {
+ max_degree: d + 1,
+ num_variables: s,
+ };
+
+ // Step 3: Start verifying the sumcheck
+ // First, compute the expected sumcheck sum: \sum gamma^j v_j
+ let sum_v_j_gamma = Us
+ .iter()
+ .zip(gamma_powers.chunks(t))
+ .flat_map(|(U, gammas)| U.v.iter().zip(gammas).map(|(&v, &g)| v * g))
+ .sum();
+
+ // Verify the interactive part of the sumcheck
+ // Step 2: Dig into the sumcheck claim and extract the randomness used
+ let (claimed_eval, r_x_prime) =
+ SumCheck::verify(sum_v_j_gamma, &proof.sc_proof, &vp_aux_info, transcript)?;
+
+ // Step 5: Finish verifying sumcheck (verify the claim c)
+ let e_beta = EqPoly::fix_xy_eval(&beta, &r_x_prime);
+ let c = proof
+ .sigmas
+ .chunks(t)
+ .zip(Us)
+ .flat_map(|(sigmas, u)| {
+ let e_lcccs = EqPoly::fix_xy_eval(&u.r_x, &r_x_prime);
+ sigmas.iter().map(move |sigma_j| e_lcccs * sigma_j)
+ })
+ .chain(proof.thetas.chunks(t).map(|thetas| {
+ S.iter()
+ .zip(c)
+ .map(|(S_i, &c_i)| c_i * S_i.iter().map(|&j| thetas[j]).product::())
+ .sum::()
+ * e_beta
+ }))
+ .zip(gamma_powers)
+ .map(|(val, gamma_i)| val * gamma_i)
+ .sum::();
+ // check that the g(r_x') from the sumcheck proof is equal to the computed c from sigmas&thetas
+ (c == claimed_eval).then_some(()).ok_or_else(|| {
+ SumCheckError::IncorrectEvaluation(claimed_eval.to_string(), c.to_string())
+ })?;
+
+ // Step 6: Get the folding challenge
+ let rho_bits = transcript.challenge_bits(CHALLENGE_BITS);
+ let rho = CM::Scalar::from_bits_le(&rho_bits);
+
+ let rho_powers = rho.powers(M + N);
+
+ Ok(Self::RU {
+ cm: Us
+ .iter()
+ .map(|u| u.cm)
+ .chain(cms.iter().copied())
+ .scalar_rlc(&rho_powers),
+ u: Us
+ .iter()
+ .map(|u| u.u)
+ .chain([CM::Scalar::one(); N])
+ .scalar_rlc(&rho_powers),
+ x: Us
+ .iter()
+ .map(|u| &u.x[..])
+ .chain(us.iter().map(|u| &u[..]))
+ .slice_rlc(&rho_powers),
+ r_x: r_x_prime,
+ v: proof
+ .sigmas
+ .chunks(t)
+ .chain(proof.thetas.chunks(t))
+ .slice_rlc(&rho_powers),
+ })
+ }
+}
diff --git a/crates/fs/src/hypernova/circuits/mod.rs b/crates/fs/src/hypernova/circuits/mod.rs
new file mode 100644
index 000000000..9367afad7
--- /dev/null
+++ b/crates/fs/src/hypernova/circuits/mod.rs
@@ -0,0 +1,3 @@
+//! In-circuit gadgets for HyperNova.
+
+pub mod verifier;
diff --git a/crates/fs/src/hypernova/circuits/verifier.rs b/crates/fs/src/hypernova/circuits/verifier.rs
new file mode 100644
index 000000000..38d35c2aa
--- /dev/null
+++ b/crates/fs/src/hypernova/circuits/verifier.rs
@@ -0,0 +1,153 @@
+//! Partial in-circuit verifier implementation for HyperNova.
+
+use ark_r1cs_std::{
+ GR1CSVar,
+ alloc::AllocVar,
+ eq::EqGadget,
+ fields::{FieldVar, fp::FpVar},
+ prelude::Boolean,
+};
+use ark_relations::gr1cs::SynthesisError;
+use sonobe_primitives::{
+ algebra::ops::{
+ pow::PowGadget,
+ rlc::{ScalarRLC, SliceRLC},
+ },
+ arithmetizations::ccs::CCSVariant,
+ commitments::GroupBasedCommitment,
+ sumcheck::{
+ circuits::SumCheckGadget,
+ utils::{EqPolyGadget, VPAuxInfo},
+ },
+ transcripts::TranscriptGadget,
+};
+
+use crate::{FoldingSchemePartialVerifierGadget, hypernova::HyperNovaGadget};
+
+impl<
+ CM: GroupBasedCommitment,
+ V: CCSVariant,
+ const M: usize,
+ const N: usize,
+ const CHALLENGE_BITS: usize,
+> FoldingSchemePartialVerifierGadget for HyperNovaGadget
+{
+ #[allow(non_snake_case)]
+ fn verify_hinted(
+ _vk: &Self::VerifierKey,
+ transcript: &mut impl TranscriptGadget,
+ Us: [&Self::RU; M],
+ us: [&Self::IU; N],
+ proof: &Self::Proof,
+ ) -> Result<(Self::RU, Self::Challenge), SynthesisError> {
+ let d = V::degree();
+ let s = proof.sc_proof.len();
+ let t = V::n_matrices();
+ let S = &V::multisets_vec();
+ let c = &V::coefficients_vec::();
+
+ // absorb instances to transcript
+ transcript.add(&Us[..])?;
+ transcript.add(&us[..])?;
+
+ // Step 1: Get some challenges
+ let gamma = transcript.challenge_field_element()?;
+ let beta = transcript.challenge_field_elements(s)?;
+
+ let gamma_powers = gamma.powers(M * t + N);
+
+ let vp_aux_info = VPAuxInfo {
+ max_degree: d + 1,
+ num_variables: s,
+ };
+
+ // Step 3: Start verifying the sumcheck
+ // First, compute the expected sumcheck sum: \sum gamma^j v_j
+ let mut sum_v_j_gamma = FpVar::zero();
+ for (i, U) in Us.iter().enumerate() {
+ for j in 0..U.v.len() {
+ sum_v_j_gamma += &U.v[j] * &gamma_powers[i * t + j];
+ }
+ }
+
+ // Verify the interactive part of the sumcheck
+ // Step 2: Dig into the sumcheck claim and extract the randomness used
+ let (expected_eval, r_x_prime) =
+ SumCheckGadget::verify(sum_v_j_gamma, &proof.sc_proof, &vp_aux_info, transcript)?;
+
+ // Step 5: Finish verifying sumcheck (verify the claim c)
+ let c = {
+ let e2 = EqPolyGadget::fix_xy_eval(&beta, &r_x_prime);
+ proof
+ .sigmas
+ .chunks(t)
+ .zip(Us)
+ .flat_map(|(sigmas, u)| {
+ let e_lcccs = EqPolyGadget::fix_xy_eval(&u.r_x, &r_x_prime);
+ sigmas.iter().map(move |sigma_j| &e_lcccs * sigma_j)
+ })
+ .chain(proof.thetas.chunks(t).map(|thetas| {
+ &e2 * S
+ .iter()
+ .zip(c)
+ .map(|(S_i, &c_i)| {
+ let mut prod = FpVar::one();
+ for &j in S_i {
+ prod *= &thetas[j];
+ }
+ prod * c_i
+ })
+ .sum::>()
+ }))
+ .zip(gamma_powers.iter())
+ .map(|(val, gamma_i)| val * gamma_i)
+ .sum::>()
+ };
+
+ // check that the g(r_x') from the sumcheck proof is equal to the computed c from sigmas&thetas
+ c.enforce_equal(&expected_eval)?;
+
+ // Step 6: Get the folding challenge
+ let rho_bits = transcript.challenge_bits(CHALLENGE_BITS)?;
+ let rho = Boolean::le_bits_to_fp(&rho_bits)?;
+
+ let rho_powers = rho.powers(M + N);
+
+ Ok((
+ Self::RU {
+ cm: {
+ let cms = Us
+ .iter()
+ .map(|u| &u.cm)
+ .chain(us.iter().map(|u| &u.cm))
+ .collect::>();
+
+ AllocVar::new_witness(cms.cs().or(rho_powers.cs()), || {
+ let cms = cms.value().unwrap_or(vec![Default::default(); M + N]);
+ let rho_powers = rho_powers
+ .value()
+ .unwrap_or(vec![Default::default(); M + N]);
+ Ok(cms.into_iter().scalar_rlc(&rho_powers))
+ })?
+ },
+ u: Us
+ .iter()
+ .map(|u| u.u.clone())
+ .chain(vec![FpVar::one(); N])
+ .scalar_rlc(&rho_powers),
+ x: Us
+ .iter()
+ .map(|u| &u.x[..])
+ .chain(us.iter().map(|u| &u.x[..]))
+ .slice_rlc(&rho_powers),
+ r_x: r_x_prime,
+ v: proof
+ .sigmas
+ .chunks(t)
+ .chain(proof.thetas.chunks(t))
+ .slice_rlc(&rho_powers),
+ },
+ rho_bits.try_into().unwrap(),
+ ))
+ }
+}
diff --git a/crates/fs/src/hypernova/instances/circuits.rs b/crates/fs/src/hypernova/instances/circuits.rs
new file mode 100644
index 000000000..384f1b7e7
--- /dev/null
+++ b/crates/fs/src/hypernova/instances/circuits.rs
@@ -0,0 +1,247 @@
+//! In-circuit variables for HyperNova instances.
+use ark_r1cs_std::{
+ GR1CSVar,
+ alloc::{AllocVar, AllocationMode},
+ boolean::Boolean,
+ fields::fp::FpVar,
+ select::CondSelectGadget,
+};
+use ark_relations::gr1cs::{ConstraintSystemRef, Namespace, SynthesisError};
+use ark_std::borrow::Borrow;
+use sonobe_primitives::{commitments::CommitmentDefGadget, transcripts::AbsorbableVar};
+
+use super::{CCCSInstance, LCCCSInstance};
+use crate::FoldingInstanceVar;
+
+/// [`LCCCSInstanceVar`] defines HyperNova's running instance variable.
+#[derive(Clone, Debug, PartialEq)]
+pub struct LCCCSInstanceVar {
+ /// [`LCCCSInstanceVar::cm`] is the witness commitment.
+ pub cm: CM::CommitmentVar,
+ /// [`LCCCSInstanceVar::u`] is the constant term.
+ pub u: CM::ScalarVar,
+ /// [`LCCCSInstanceVar::x`] is the vector of public inputs (to the circuit).
+ pub x: Vec,
+ /// [`LCCCSInstanceVar::r_x`] is the random evaluation point.
+ pub r_x: Vec,
+ /// [`LCCCSInstanceVar::v`] is the vector of sums of MLE evaluations defined
+ /// in Definition 2.
+ pub v: Vec,
+}
+
+impl AllocVar, CM::ConstraintField>
+ for LCCCSInstanceVar
+{
+ fn new_variable>>(
+ cs: impl Into