Skip to content

chore: make binius-mayo zk #76

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
rymnc merged 1 commit into from
Jun 25, 2026
Merged

chore: make binius-mayo zk #76

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
353 changes: 199 additions & 154 deletions libs/binius-mayo/Cargo.lock
View file
Open in desktop

Large diffs are not rendered by default.

17 changes: 9 additions & 8 deletions libs/binius-mayo/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,19 +5,20 @@ edition = "2024"
rust-version = "1.95"

[dependencies]
binius-core = { git = "https://github.com/binius-zk/binius64", rev = "363e3ae52739679a77dbfa328b849c6441d5ea99" }
binius-frontend = { git = "https://github.com/binius-zk/binius64", rev = "363e3ae52739679a77dbfa328b849c6441d5ea99" }
binius-circuits = { git = "https://github.com/binius-zk/binius64", rev = "363e3ae52739679a77dbfa328b849c6441d5ea99" }
binius-transcript = { git = "https://github.com/binius-zk/binius64", rev = "363e3ae52739679a77dbfa328b849c6441d5ea99" }
binius-prover = { git = "https://github.com/binius-zk/binius64", rev = "363e3ae52739679a77dbfa328b849c6441d5ea99" }
binius-verifier = { git = "https://github.com/binius-zk/binius64", rev = "363e3ae52739679a77dbfa328b849c6441d5ea99" }
binius-hash = { git = "https://github.com/binius-zk/binius64", rev = "363e3ae52739679a77dbfa328b849c6441d5ea99" }
binius-core = { git = "https://github.com/binius-zk/binius64", rev = "3bc7451dc3c52af6383fcd99892c6892f57e89b0" }
binius-frontend = { git = "https://github.com/binius-zk/binius64", rev = "3bc7451dc3c52af6383fcd99892c6892f57e89b0" }
binius-circuits = { git = "https://github.com/binius-zk/binius64", rev = "3bc7451dc3c52af6383fcd99892c6892f57e89b0" }
binius-transcript = { git = "https://github.com/binius-zk/binius64", rev = "3bc7451dc3c52af6383fcd99892c6892f57e89b0" }
binius-prover = { git = "https://github.com/binius-zk/binius64", rev = "3bc7451dc3c52af6383fcd99892c6892f57e89b0" }
binius-verifier = { git = "https://github.com/binius-zk/binius64", rev = "3bc7451dc3c52af6383fcd99892c6892f57e89b0" }
binius-hash = { git = "https://github.com/binius-zk/binius64", rev = "3bc7451dc3c52af6383fcd99892c6892f57e89b0" }
sha3 = "=0.10.9"
aes = "=0.8.4"
rand = "0.10"

[dev-dependencies]
hex = "0.4"
rand = "0.8"
rand = "0.10"
criterion = "0.5"

[[bench]]
Expand Down
8 changes: 5 additions & 3 deletions libs/binius-mayo/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,11 +45,11 @@ The counterparty receives `(c, pk_id, π)` and verifies the SNARK. They learn th
| `c` (32 B commitment) | ✓ | ✓ (recomputed) | ✓ (bundle) |
| SNARK proof `π` | ✓ | ✓ | ✓ (bundle) |

The verifier's view of `payload` is application-dependent: in an attestation flow they know it (and recompute `c` locally); in a blinded flow they only know `c`. A public observer learns only the bundle and nothing about `cpk`, `sig`, or `payload`. Hiding of `cpk` is informal, not provably zero-knowledge; see [Limitations](#limitations).
The verifier's view of `payload` is application-dependent: in an attestation flow they know it (and recompute `c` locally); in a blinded flow they only know `c`. The SNARK proof `π` is zero-knowledge (binius64's ZK prover/verifier): it reveals nothing about `cpk`, `sig`, or `payload` beyond what `c` and `pk_id` already commit to. Those two commitments are binding but not hiding, so an observer who can guess `payload`, or who holds a candidate `cpk`, can confirm the guess by recomputing them; see [Limitations](#limitations).

## Build & test

The crate pins [`binius-zk/binius64`](https://github.com/binius-zk/binius64) at commit `363e3ae`. Toolchain: **Rust ≥ 1.95**, edition 2024.
The crate pins [`binius-zk/binius64`](https://github.com/binius-zk/binius64) at commit `3bc7451`, which includes binius64's zero-knowledge prover/verifier. Toolchain: **Rust ≥ 1.95**, edition 2024.

```bash
# Build the library
Expand Down Expand Up @@ -87,6 +87,8 @@ assert_eq!(bundle.pk_id, pk_id_local);
verifier.verify(&bundle)?;
```

Proofs are zero-knowledge and randomized: each `prove` call draws fresh blinding randomness from the OS CSPRNG, so proofs over identical input are not byte-identical. Use `prove_with_rng` to supply your own cryptographically-secure RNG (for reproducible test vectors, say).

The example at `examples/mayo2_e2e.rs` walks through the full flow end-to-end against the first NIST KAT entry.

### Advanced: low-level escape hatch
Expand Down Expand Up @@ -136,7 +138,7 @@ Highlights:

This is a **proof of concept** for research and evaluation. Known limitations:

1. **Hidden-pk hiding is informal, not provable.** Binius64 itself is not zero-knowledge as of `363e3ae` (per its `ARCHITECTURE.md`), and no formal hiding analysis was performed for this construction. Pk-hiding rests on the entropy of the MAYO-2 public key and the assumption that the proof transcript does not leak structured information about the witness; an attacker who can extract witness data from a Binius64 proof can recover the public key. Do not rely on this primitive for confidentiality without an independent analysis.
1. **The proof is zero-knowledge; the public commitments are not hiding.** The SNARK uses binius64's zero-knowledge prover/verifier (`zk_config::{ZKProver, ZKVerifier}`: a Spartan ZK wrapper over a blinded FRI-Binius commitment with masked sumcheck, per Diamond, [eprint 2025/1015](https://eprint.iacr.org/2025/1015)). The proof transcript reveals nothing about the witness data (the expanded pk, the signature, or the message digest). The residual exposure is the two public inputs: `c = keccak256(DOMAIN_C ‖ m)` and `pk_id = keccak256(DOMAIN_PK ‖ canonical_packed(P))` are binding but not hiding, so an adversary who can enumerate candidate payloads, or who holds a candidate `cpk`, can confirm a guess by recomputing them. For payload confidentiality against enumeration, fold a high-entropy salt into `payload` before proving (it flows into `c` with no circuit change); `pk_id` is a public identifier. Soundness is binius64's 96-bit target (`SECURITY_BITS`); see the `soundness` test.

2. **`pk_id` binds the expanded pk, not the 4912-byte compact form.** Off-circuit AES-128-CTR expansion is required by the signer once at keypair publication. Any external system holding "the prover's MAYO-2 pk" must hash the expanded form, not the cpk.

Expand Down
82 changes: 59 additions & 23 deletions libs/binius-mayo/src/api.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,16 +36,11 @@ use aes::cipher::generic_array::GenericArray;
use aes::cipher::{BlockEncrypt, KeyInit};
use binius_core::word::Word;
use binius_frontend::{Circuit, CircuitBuilder};
use binius_prover::{
OptimalPackedB128, Prover as BiniusProver,
hash::parallel_compression::ParallelCompressionAdaptor,
};
use binius_hash::sha256::Sha256HashSuite;
use binius_prover::{OptimalPackedB128, zk_config::ZKProver as BiniusProver};
use binius_transcript::{ProverTranscript, VerifierTranscript};
use binius_verifier::{
Verifier as BiniusVerifier,
config::StdChallenger,
hash::{StdCompression, StdDigest},
};
use binius_verifier::{config::StdChallenger, zk_config::ZKVerifier as BiniusVerifier};
use rand::CryptoRng;
use sha3::Shake256;
use sha3::digest::{ExtendableOutput, Update, XofReader};
use sha3::{Digest, Keccak256};
Expand Down Expand Up @@ -364,6 +359,11 @@ pub(crate) const DOMAIN_TAG_C_WORD: u64 = u64::from_le_bytes(DOMAIN_TAG_C);
/// `DOMAIN_TAG_PK` packed as a little-endian `u64` for in-circuit use.
pub(crate) const DOMAIN_TAG_PK_WORD: u64 = u64::from_le_bytes(DOMAIN_TAG_PK);

/// Log of the inverse Reed-Solomon rate for the binius prover/verifier.
///
/// Soundness is fixed by binius's `SECURITY_BITS` (96), not by this value
const LOG_INV_RATE: usize = 3;

/// Compiled SNARK prover for the MAYO-2 verifier circuit.
///
/// Compile once with [`Prover::compile`] (around 3 s in release mode) and
Expand All @@ -372,8 +372,7 @@ pub(crate) const DOMAIN_TAG_PK_WORD: u64 = u64::from_le_bytes(DOMAIN_TAG_PK);
pub struct Prover {
inner: Mayo2Verify,
circuit: Circuit,
binius_prover:
BiniusProver<OptimalPackedB128, ParallelCompressionAdaptor<StdCompression>, StdDigest>,
binius_prover: BiniusProver<OptimalPackedB128, Sha256HashSuite>,
}

/// Compiled SNARK verifier for the MAYO-2 verifier circuit.
Expand All @@ -382,7 +381,7 @@ pub struct Prover {
/// [`Verifier::verify`] calls.
#[must_use = "a `Verifier` is the result of an expensive compile step; drop it only when you're done verifying"]
pub struct Verifier {
binius_verifier: BiniusVerifier<StdDigest, StdCompression>,
binius_verifier: BiniusVerifier<Sha256HashSuite>,
/// Constants from the constraint system, copied into the public-input
/// slice prefix at verify time.
constants: Vec<Word>,
Expand All @@ -402,12 +401,10 @@ impl Prover {
let circuit = builder.build();
let cs = circuit.constraint_system();

let binius_verifier =
BiniusVerifier::<StdDigest, _>::setup(cs.clone(), 1, StdCompression::default())
.map_err(|e| Error::Setup(Box::new(e)))?;
let compression = ParallelCompressionAdaptor::new(StdCompression::default());
let binius_verifier = BiniusVerifier::<Sha256HashSuite>::setup(cs.clone(), LOG_INV_RATE)
.map_err(|e| Error::Setup(Box::new(e)))?;
let binius_prover =
BiniusProver::<OptimalPackedB128, _, StdDigest>::setup(binius_verifier, compression)
BiniusProver::<OptimalPackedB128, Sha256HashSuite>::setup(binius_verifier)
.map_err(|e| Error::Setup(Box::new(e)))?;

Ok(Self {
Expand All @@ -417,9 +414,29 @@ impl Prover {
})
}

/// Produce a proof bundle for the signed message.
/// Produce a proof bundle for the signed message, drawing zero-knowledge
/// blinding randomness from the OS CSPRNG.
///
/// The proof is zero-knowledge: it reveals nothing about the witness beyond
/// what the public commitments `c` and `pk_id` already commit to. Each call
/// draws fresh randomness, so proofs over identical input differ byte-wise.
#[must_use = "the returned `ProofBundle` is the only output; dropping it discards the proof"]
pub fn prove(&self, signed: &SignedMessage<'_>) -> Result<ProofBundle> {
self.prove_with_rng(signed, rand::rng())
}

/// Like [`Prover::prove`] but draws the zero-knowledge blinding randomness
/// from a caller-supplied source. Use this for reproducible proofs in tests
/// or to bind a specific entropy source.
///
/// The RNG must be cryptographically secure. Low-entropy or reused blinding
/// randomness breaks the zero-knowledge property.
#[must_use = "the returned `ProofBundle` is the only output; dropping it discards the proof"]
pub fn prove_with_rng(
&self,
signed: &SignedMessage<'_>,
rng: impl CryptoRng,
) -> Result<ProofBundle> {
// 1. Off-circuit: lift the variable-length payload to the 32-byte
// MAYO digest the signature actually authenticates.
let m = shake256_32(signed.payload);
Expand All @@ -434,11 +451,12 @@ impl Prover {
.populate_wire_witness(&mut w)
.map_err(|e| Error::Prove(Box::new(e)))?;

// 4. Run the binius64 prover and finalize the transcript.
// 4. Run the binius64 ZK prover and finalize the transcript. The RNG
// supplies the masking randomness that hides the witness.
let value_vec = w.into_value_vec();
let mut transcript = ProverTranscript::new(StdChallenger::default());
self.binius_prover
.prove(value_vec, &mut transcript)
.prove(value_vec, rng, &mut transcript)
.map_err(|e| Error::Prove(Box::new(e)))?;
let proof_bytes = transcript.finalize();

Expand Down Expand Up @@ -469,9 +487,8 @@ impl Verifier {
let circuit = builder.build();
let cs = circuit.constraint_system();

let binius_verifier =
BiniusVerifier::<StdDigest, _>::setup(cs.clone(), 1, StdCompression::default())
.map_err(|e| Error::Setup(Box::new(e)))?;
let binius_verifier = BiniusVerifier::<Sha256HashSuite>::setup(cs.clone(), LOG_INV_RATE)
.map_err(|e| Error::Setup(Box::new(e)))?;

let constants = cs.constants.clone();
let offset_inout = cs.value_vec_layout.offset_inout;
Expand Down Expand Up @@ -670,3 +687,22 @@ fn unpack_m_vec_array(packed: &[u8], n_entries: usize) -> Vec<[u8; M]> {
}
out
}

#[cfg(test)]
mod soundness {
use super::LOG_INV_RATE;

#[test]
fn binius_security_target_is_at_least_96_bits() {
assert!(
binius_verifier::SECURITY_BITS >= 96,
"binius soundness target dropped to {} bits",
binius_verifier::SECURITY_BITS,
);
let n_queries = binius_verifier::fri::calculate_n_test_queries(
binius_verifier::SECURITY_BITS,
LOG_INV_RATE,
);
assert!(n_queries >= binius_verifier::SECURITY_BITS);
}
}
8 changes: 4 additions & 4 deletions libs/binius-mayo/src/gf16/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,7 @@ impl BitslicedGf16Mvec {
mod tests {
use super::*;
use binius_core::verify::verify_constraints;
use rand::{Rng, SeedableRng, rngs::StdRng};
use rand::{RngExt, SeedableRng, rngs::StdRng};

/// Round-trip: populate a bitsliced m-vec from random lanes, evaluate
/// the (empty) circuit, and read the lanes back.
Expand All @@ -103,7 +103,7 @@ mod tests {
let mut w = circuit.new_witness_filler();
let mut lanes = [0u8; 64];
for x in lanes.iter_mut() {
*x = rng.gen_range(0..16);
*x = rng.random_range(0..16);
}
v.populate(&mut w, &lanes);
circuit.populate_wire_witness(&mut w).unwrap();
Expand All @@ -129,8 +129,8 @@ mod tests {
let mut a_lanes = [0u8; 64];
let mut b_lanes = [0u8; 64];
for i in 0..64 {
a_lanes[i] = rng.gen_range(0..16);
b_lanes[i] = rng.gen_range(0..16);
a_lanes[i] = rng.random_range(0..16);
b_lanes[i] = rng.random_range(0..16);
}
let c_lanes: [u8; 64] = core::array::from_fn(|i| scalar::add(a_lanes[i], b_lanes[i]));
a.populate(&mut w, &a_lanes);
Expand Down
14 changes: 7 additions & 7 deletions libs/binius-mayo/src/gf16/mul.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -174,7 +174,7 @@ mod tests {
use super::*;
use crate::gf16::scalar;
use binius_core::verify::verify_constraints;
use rand::{Rng, SeedableRng, rngs::StdRng};
use rand::{RngExt, SeedableRng, rngs::StdRng};

/// 100 random 64-lane pairs: in-circuit Karatsuba == lanewise scalar mul.
#[test]
Expand All @@ -193,8 +193,8 @@ mod tests {
let mut a_lanes = [0u8; 64];
let mut b_lanes = [0u8; 64];
for i in 0..64 {
a_lanes[i] = rng.gen_range(0..16);
b_lanes[i] = rng.gen_range(0..16);
a_lanes[i] = rng.random_range(0..16);
b_lanes[i] = rng.random_range(0..16);
}
let c_lanes: [u8; 64] = core::array::from_fn(|i| scalar::mul(a_lanes[i], b_lanes[i]));
a.populate(&mut w, &a_lanes);
Expand All @@ -215,7 +215,7 @@ mod tests {
let circuit = builder.build();

for _ in 0..50 {
let s: u8 = rng.gen_range(0..16);
let s: u8 = rng.random_range(0..16);
let mut w = circuit.new_witness_filler();
w[scalar_w] = Word(s as u64);
circuit.populate_wire_witness(&mut w).unwrap();
Expand Down Expand Up @@ -243,9 +243,9 @@ mod tests {

for _ in 0..20 {
let mut w = circuit.new_witness_filler();
let s_lanes: [u8; 64] = core::array::from_fn(|_| rng.gen_range(0..16));
let v_lanes: [u8; 64] = core::array::from_fn(|_| rng.gen_range(0..16));
let acc_lanes: [u8; 64] = core::array::from_fn(|_| rng.gen_range(0..16));
let s_lanes: [u8; 64] = core::array::from_fn(|_| rng.random_range(0..16));
let v_lanes: [u8; 64] = core::array::from_fn(|_| rng.random_range(0..16));
let acc_lanes: [u8; 64] = core::array::from_fn(|_| rng.random_range(0..16));
let exp_lanes: [u8; 64] = core::array::from_fn(|i| {
scalar::add(acc_lanes[i], scalar::mul(s_lanes[i], v_lanes[i]))
});
Expand Down
18 changes: 9 additions & 9 deletions libs/binius-mayo/src/gf16/scalar.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,7 @@ pub(crate) fn bitsliced_to_lanes(planes: &[u64; 4]) -> [u8; 64] {
#[cfg(test)]
mod tests {
use super::*;
use rand::{Rng, SeedableRng, rngs::StdRng};
use rand::{RngExt, SeedableRng, rngs::StdRng};

/// Independent scalar reference: schoolbook multiply via shift-XOR, then
/// reduce by directly applying x^4 = x + 1 to each high bit of the product.
Expand Down Expand Up @@ -160,9 +160,9 @@ mod tests {
fn given_random_triples_when_mul_then_associative() {
let mut rng = StdRng::seed_from_u64(0xCAFE_BABE);
for _ in 0..1000 {
let a: u8 = rng.gen_range(0..16);
let b: u8 = rng.gen_range(0..16);
let c: u8 = rng.gen_range(0..16);
let a: u8 = rng.random_range(0..16);
let b: u8 = rng.random_range(0..16);
let c: u8 = rng.random_range(0..16);
assert_eq!(mul(mul(a, b), c), mul(a, mul(b, c)));
}
}
Expand All @@ -171,9 +171,9 @@ mod tests {
fn given_random_triples_when_mul_then_distributive_over_add() {
let mut rng = StdRng::seed_from_u64(0xDEAD_BEEF);
for _ in 0..1000 {
let a: u8 = rng.gen_range(0..16);
let b: u8 = rng.gen_range(0..16);
let c: u8 = rng.gen_range(0..16);
let a: u8 = rng.random_range(0..16);
let b: u8 = rng.random_range(0..16);
let c: u8 = rng.random_range(0..16);
// a * (b + c) = a*b + a*c
assert_eq!(mul(a, add(b, c)), add(mul(a, b), mul(a, c)));
}
Expand All @@ -185,7 +185,7 @@ mod tests {
for _ in 0..50 {
let mut lanes = [0u8; 64];
for v in lanes.iter_mut() {
*v = rng.gen_range(0..16);
*v = rng.random_range(0..16);
}
let packed = pack_lanes(&lanes);
let back = unpack_lanes(&packed);
Expand Down Expand Up @@ -223,7 +223,7 @@ mod tests {
for _ in 0..50 {
let mut lanes = [0u8; 64];
for v in lanes.iter_mut() {
*v = rng.gen_range(0..16);
*v = rng.random_range(0..16);
}
let planes = lanes_to_bitsliced(&lanes);
let back = bitsliced_to_lanes(&planes);
Expand Down
8 changes: 4 additions & 4 deletions libs/binius-mayo/src/gf16/transpose.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -182,7 +182,7 @@ mod tests {
use super::*;
use crate::gf16::scalar;
use binius_core::verify::verify_constraints;
use rand::{Rng, SeedableRng, rngs::StdRng};
use rand::{RngExt, SeedableRng, rngs::StdRng};

/// Round-trip: packed → bitsliced → packed = identity, in-circuit.
#[test]
Expand All @@ -202,7 +202,7 @@ mod tests {
let mut w = circuit.new_witness_filler();
let mut lanes = [0u8; 64];
for v in lanes.iter_mut() {
*v = rng.gen_range(0..16);
*v = rng.random_range(0..16);
}
let pk = scalar::pack_lanes(&lanes);
for i in 0..4 {
Expand All @@ -229,7 +229,7 @@ mod tests {
let mut w = circuit.new_witness_filler();
let mut lanes = [0u8; 64];
for v in lanes.iter_mut() {
*v = rng.gen_range(0..16);
*v = rng.random_range(0..16);
}
let pk = scalar::pack_lanes(&lanes);
for i in 0..4 {
Expand All @@ -256,7 +256,7 @@ mod tests {
let mut w = circuit.new_witness_filler();
let mut lanes = [0u8; 64];
for v in lanes.iter_mut() {
*v = rng.gen_range(0..16);
*v = rng.random_range(0..16);
}
bv.populate(&mut w, &lanes);
circuit.populate_wire_witness(&mut w).unwrap();
Expand Down
Loading