rename PCS to WHIR

Author: TomWambsgans

AGENTS.md

@@ -21,7 +21,7 @@ Dependency order, leaves first:
 | `zk_alloc`        | proving arena (below)                                    |
 | `primitives`      | field kernels (NEON/AVX), bit transposes, multilinear helpers, `bench` |
 | `fiat_shamir`     | VM-native sponge + prover/verifier transcript                          |
-| `pcs`             | additive NTT, Merkle, ring switch, stacked Ligerito                    |
+| `pcs`             | additive NTT, Merkle, ring switch, stacked WHIR                    |
 | `flock`           | batched R1CS over GF(2) for BLAKE3: zerocheck + lincheck               |
 | `lean_vm`         | arithmetization: tables, bus, constraints, `cpu::prove`/`verify`       |
 | `lean_compiler`   | zkDSL (Python subset) → ISA                                            |
@@ -41,7 +41,7 @@ cargo clippy --release --all-targets
 cargo fmt --all                   # max_width = 120
 ```
 
-Heavy benches and measurement harnesses are `#[ignore]`d; run by name with `-- --ignored --nocapture`: `blake3_batch_prove_verify`, `pcs_throughput`, `recursion_soundness_binds`, `recursion_generic_many`, `recursion_guest_profile`, `print_ligerito_query_counts`, `encoding_grinding_bits`.
+Heavy benches and measurement harnesses are `#[ignore]`d; run by name with `-- --ignored --nocapture`: `blake3_batch_prove_verify`, `pcs_throughput`, `recursion_soundness_binds`, `recursion_generic_many`, `recursion_guest_profile`, `print_whir_query_counts`, `encoding_grinding_bits`.
 
 ## Benchmarking
 
@@ -112,5 +112,5 @@ The third is worth understanding before touching the verifier. `guests/recursion
 | `LEANVM_XMSS_N`, `LEANVM_HASH_N`, `LEANVM_HASH_UNROLL`                                                  | workload sizes in tests                          |
 | `FLOCK_N_LOG`, `FLOCK_PROVE_TRACE`, `FLOCK_ZC_TIMING`, `LINCHECK_TRACE`                                 | flock batch size, stage traces                   |
 | `PCS_LOG_N`, `PCS_LOG_INV_RATE`, `PCS_MIN_MU`, `PCS_SAMPLES`                                            | PCS throughput bench                             |
-| `LIGERITO_TRACE`, `LIGERITO_NUM_VARS`, `LIGERITO_LOG_INV_RATE`                                          | Ligerito NTT/Merkle split                        |
+| `WHIR_TRACE`, `WHIR_NUM_VARS`, `WHIR_LOG_INV_RATE`                                          | WHIR NTT/Merkle split                        |
 | `DBG_PROF{,_DUMP}`, `DBG_LOOPS`, `DBG_DISASM`, `DBG_LOWER`, `DBG_CSE`, `DBG_NO_CSE`, `DBG_PLACEHOLDERS` | compiler / guest-cycle attribution               |

README.md

@@ -63,7 +63,12 @@ Fibonacci (in the exponent, i.e. modulo 2^64 - 1), N = 2,000,000
 
 ## Security
 
-- 128-bit proven (LDR Johnson)
+- 128-bit (LDR Johnson, no proximity gaps conjecture)
+
+## Snark machinery
+
+- Binary field of 192 bits
+- PCS: [WHIR](https://eprint.iacr.org/2024/1586) (aka [Ligerito](https://eprint.iacr.org/2025/1187))
 
 ## Credits
 

crates/fiat_shamir/src/sponge.rs

@@ -279,7 +279,7 @@ pub enum TraceOp {
         bits: u32,
         digest: F64,
     },
-    /// An opening hint consumed (the Ligerito hint channel).
+    /// An opening hint consumed (the WHIR hint channel).
     Opening,
 }
 

crates/fiat_shamir/src/transcript.rs

@@ -15,7 +15,7 @@
 //!   binding it twice silently desynchronizes the two sides. A challenge is just
 //!   `sample()`d, bound to everything seeded/sent so far.
 //! - **`hint_*` (prover) / `next_*` (verifier)**: transport that is NOT absorbed
-//!   here, hash-bearing data (the Ligerito `openings`, like leanVM's
+//!   here, hash-bearing data (the WHIR `openings`, like leanVM's
 //!   `merkle_paths`) whose binding is the Merkle structure itself.
 //! - **`sample` / `sample_vec`**: squeeze a challenge.
 //!
@@ -25,13 +25,13 @@
 use crate::sponge::{Sponge, TraceOp, trace};
 use primitives::field::{F64, F192};
 
-/// A complete proof: the scalar transcript stream plus the Ligerito opening hint
+/// A complete proof: the scalar transcript stream plus the WHIR opening hint
 /// channel: **two** channels, no bolted-on side field. The commitment root and
-/// every transmitted scalar ride `stream`; the hash-bearing Ligerito openings
+/// every transmitted scalar ride `stream`; the hash-bearing WHIR openings
 /// ride `openings`. flock's BLAKE3 sub-proof is carried the same way: its
 /// zerocheck / lincheck / ring-switch scalars are ordinary `add_scalar` words on
 /// `stream` (transmitted AND bound at their protocol points, like every other
-/// scalar) and its one Ligerito opening rides `openings`.
+/// scalar) and its one WHIR opening rides `openings`.
 ///
 /// `Deserialize` as well as `Serialize`, so a proof round-trips over the wire and
 /// an independent verifier process reconstructs it: everything lives in these two
@@ -42,7 +42,7 @@ pub struct Proof<O> {
     /// Every transmitted field scalar, in protocol order (plus flock's scalar
     /// sub-proof as trailing raw transport words).
     pub stream: Vec<F192>,
-    /// Ligerito openings (sumcheck messages + Merkle roots/paths), in order.
+    /// WHIR openings (sumcheck messages + Merkle roots/paths), in order.
     pub openings: Vec<O>,
 }
 
@@ -121,7 +121,7 @@ impl<O> ProverState<O> {
     }
 
     /// The raw sponge, for side-agnostic sub-steps shared by prover and
-    /// verifier (e.g. the Ligerito query sampler).
+    /// verifier (e.g. the WHIR query sampler).
     pub fn sponge_mut(&mut self) -> &mut Sponge {
         &mut self.sponge
     }

crates/flock/src/blake3.rs

@@ -1553,7 +1553,7 @@ mod tests {
 }
 
 // The zerocheck, lincheck, and ring-switch scalars use the shared transcript;
-// the caller carries the Ligerito opening.
+// the caller carries the WHIR opening.
 
 /// One claim on the committed packed BLAKE3 witness `q_pkd`, as left by the
 /// Flock reduction and handed to the PCS. `claim` is the `ẑ(point) = value`

crates/flock/src/zerocheck/univariate_skip_optimized.rs

@@ -62,7 +62,7 @@ const N_MEDIUM: usize = 4;
 /// four medium constants returned by [`medium_challenges`] — must be
 /// **F₂-linearly independent** in F₁₉₂. Zerocheck soundness relies on this
 /// (a witness aligned with the friendly subspace would otherwise let the
-/// prover cancel the URM message), and so does Ligerito's L0 list-collapse
+/// prover cancel the URM message), and so does WHIR's L0 list-collapse
 /// argument (the SZ bound `(m−7)/|F|` for MLE collisions at `r` requires
 /// the seven friendly coords to span a 7-dim F₂-subspace). Asserted by
 /// `tests::friendly_challenges_f2_independent`.
@@ -1101,15 +1101,15 @@ mod tests {
         }
     }
 
-    /// **Soundness assumption.** Zerocheck and the Ligerito PCS opening at
+    /// **Soundness assumption.** Zerocheck and the WHIR PCS opening at
     /// L0 both depend on the seven "friendly" constants — three small
     /// (`φ_8(SMALL_CHAL_F8[k])`, k ∈ 0..3) and four medium
     /// (`γ^{2^i}/(1+γ^{2^i})`, i ∈ 0..4) — being **F₂-linearly independent**
     /// in F₁₉₂.
     ///
     /// Zerocheck needs this so that the prover's URM message can't be
     /// trivially canceled by a malicious witness aligned with the friendly
-    /// subspace. Ligerito's L0 list-collapse argument (which leans on the
+    /// subspace. WHIR's L0 list-collapse argument (which leans on the
     /// zerocheck `(r, v)` claim as an OOD-equivalent) also depends on it
     /// — see the soundness writeup. If any subset of these seven values is
     /// F₂-dependent, the SZ bound `(m−7)/|F|` for collisions between
@@ -1153,7 +1153,7 @@ mod tests {
         assert_eq!(
             rank, 7,
             "friendly challenges must be F₂-linearly independent in F₁₉₂; \
-             zerocheck and Ligerito L0 soundness depend on it"
+             zerocheck and WHIR L0 soundness depend on it"
         );
     }
 

crates/flock/tests/blake3_batch.rs

@@ -2,7 +2,7 @@
 //!
 //! This exercises only Flock's BLAKE3 path over `N` compressions: witness
 //! generation, F64 commitment, zerocheck + lincheck reduction, the stacked
-//! ring-switch/Ligerito opening, and verification. Circuit construction is
+//! ring-switch/WHIR opening, and verification. Circuit construction is
 //! outside the timed region, matching the VM's warmed-setup convention.
 //!
 //! Run with the XMSS-sized workload:
@@ -24,13 +24,13 @@ use flock::blake3::{
     min_n_blocks_log, pinned_compression,
 };
 use flock::proof::ZClaim;
-use pcs::ligerito::{INITIAL_FOLDING_FACTOR, LOG_INV_RATE_0};
-use pcs::ligerito::{commit, configs_for};
 use pcs::pack::{LOG_PACKING, PACKING_WIDTH};
 use pcs::stack_open::{
-    RingSwitchClaim, RingSwitchOpen, RingSwitchVerify, open_batch_mixed_ligerito_stacked,
-    verify_opening_batch_mixed_ligerito_stacked,
+    RingSwitchClaim, RingSwitchOpen, RingSwitchVerify, open_batch_mixed_whir_stacked,
+    verify_opening_batch_mixed_whir_stacked,
 };
+use pcs::whir::{INITIAL_FOLDING_FACTOR, LOG_INV_RATE_0};
+use pcs::whir::{commit, configs_for};
 use primitives::bench::{Plan, Timing};
 use primitives::multilinear::lagrange_weights_naive;
 use primitives::{
@@ -125,7 +125,7 @@ fn blake3_batch_prove_verify() {
     let setup = Blake3Setup::new(n);
     let setup_ms = t.elapsed().as_secs_f64() * 1e3;
 
-    let (prover_config, verifier_config) = configs_for(mu).expect("Ligerito configuration");
+    let (prover_config, verifier_config) = configs_for(mu).expect("WHIR configuration");
 
     // One full prove pass: witness generation, commitment, and the reduction +
     // stacked opening. Deterministic in `blocks`, so every pass is the same work
@@ -156,8 +156,7 @@ fn blake3_batch_prove_verify() {
         let reduced = setup.prove_reduction_precomputed(&z_packed, &a_packed, &b_packed, &z_lincheck, &mut ps);
         drop((z_packed, a_packed, b_packed, z_lincheck));
         let ring = prover_ring(&reduced, mu);
-        let opening =
-            open_batch_mixed_ligerito_stacked(ps.sponge_mut(), &q_pkd, &prover_data, &prover_config, &[], &ring);
+        let opening = open_batch_mixed_whir_stacked(ps.sponge_mut(), &q_pkd, &prover_data, &prover_config, &[], &ring);
         let open_s = t.elapsed().as_secs_f64();
         let prove_s = t_prove.elapsed().as_secs_f64();
 
@@ -189,7 +188,7 @@ fn blake3_batch_prove_verify() {
         let root = pcs::merkle::scalars_to_hash(&vs.next_scalars(2).expect("commitment root"));
         let replay = setup.verify_reduction(&mut vs).expect("Flock reduction verifies");
         let ring = verifier_ring(&replay.ab, &replay.c, mu);
-        verify_opening_batch_mixed_ligerito_stacked(vs.sponge_mut(), &verifier_config, mu, &root, &[], &ring, &opening)
+        verify_opening_batch_mixed_whir_stacked(vs.sponge_mut(), &verifier_config, mu, &root, &[], &ring, &opening)
             .expect("stacked PCS opening verifies");
         vs.finish().expect("transcript fully consumed");
     });

crates/lean_vm/src/blake3_flock.rs

@@ -4,7 +4,7 @@
 //! as a column in leanVM-b's ONE stacked `F64` witness (§3.1), with no separate flock
 //! commitment. The VM's `BLAKE3` table binds to it by point-eval equality (its
 //! value columns and `q_pkd`'s slots are point-evals of the same committed
-//! stack), and flock's R1CS validity is discharged by the same stacked Ligerito:
+//! stack), and flock's R1CS validity is discharged by the same stacked WHIR:
 //! the reduction's two tower-field claims pass through
 //! [`ring_switch_open`] / [`ring_switch_verify`] and join the batch-mixed
 //! opening ([`::pcs::stack_open`]).
@@ -530,7 +530,7 @@ mod tests {
         }
     }
 
-    /// flock's validity claims, discharged by ONE stacked Ligerito over a
+    /// flock's validity claims, discharged by ONE stacked WHIR over a
     /// hand-stacked witness containing `q_pkd` (plus a dummy column) together
     /// with an ordinary point claim: the full prove_reduction → ring-switch →
     /// stack_open seam without the VM pipeline. Proves and verifies on the

crates/lean_vm/src/cpu/layout.rs

@@ -21,7 +21,7 @@ pub const BFCNT: usize = 4; // per-pc bytecode execution count, g^{A[pc]}
 // SOLE copy of the input/output words: the VM's BLAKE3 value columns are
 // virtual and their memory-bus claims route to `q_pkd` slots (§blake3_flock), so
 // nothing duplicates them. flock's R1CS validity is discharged by the single
-// stacked Ligerito opening over this commitment.
+// stacked WHIR opening over this commitment.
 pub const QPKD: usize = 5;
 pub const N_SHARED: usize = 6;
 

crates/lean_vm/src/cpu/mod.rs

@@ -192,7 +192,7 @@ fn read_public(vs: &mut VerifierState, prog: &Program, public_input: &[F192; 2])
         || bytecode_size > (1usize << MAX_LOG_BYTECODE)
         || !(MIN_LOG_MEM..=MAX_LOG_MEM).contains(&log_mem)
         || row_counts.iter().any(|&r| r >= (1usize << MAX_LOG_ROWS))
-        || ::pcs::ligerito::validate_log_inv_rate(log_inv_rate).is_err()
+        || ::pcs::whir::validate_log_inv_rate(log_inv_rate).is_err()
     {
         return Err(Error::PublicInput);
     }
@@ -492,7 +492,7 @@ impl Stats {
 /// Fiat-Shamir transcript before the commitment.
 #[tracing::instrument(name = "Prove", skip_all, fields(log_inv_rate))]
 pub fn prove(program: &Program, public_input: [F192; 2], log_inv_rate: usize) -> (Proof, Stats) {
-    ::pcs::ligerito::validate_log_inv_rate(log_inv_rate).expect("valid log_inv_rate");
+    ::pcs::whir::validate_log_inv_rate(log_inv_rate).expect("valid log_inv_rate");
     // One proof is one arena phase: every transient buffer below is bump-allocated
     // and reclaimed wholesale here, rather than faulted in and unmapped again per
     // proof. Bound first so it outlives them; inert unless `init_prover` opted in.
@@ -535,7 +535,7 @@ pub fn prove(program: &Program, public_input: [F192; 2], log_inv_rate: usize) ->
     // `w.q` (≥1 instance, a program with no BLAKE3 carries one padding instance,
     // so the proof shape is uniform and there is no has/hasn't-BLAKE3 fork). flock's
     // R1CS validity and EVERY leanVM point claim are discharged together by ONE
-    // Ligerito over this commitment (below). The input/output words bind via the
+    // WHIR over this commitment (below). The input/output words bind via the
     // memory bus (virtual value columns route to q_pkd); the constant pins reuse a
     // bus point, so no dedicated binding challenge is drawn. Mirrored in `verify`.
     let l = &w.layout;
@@ -582,7 +582,7 @@ pub fn prove(program: &Program, public_input: [F192; 2], log_inv_rate: usize) ->
     // Run flock's reduction (zerocheck + lincheck) over the prepared native
     // layouts retained from the fused q_pkd build pass; it returns the `(ab, c)`
     // validity claims on the committed `q_pkd`, discharged by the PCS below in the
-    // SAME Ligerito as every leanVM point claim (the point claims become the
+    // SAME WHIR as every leanVM point claim (the point claims become the
     // opener's `point_claims`).
     let flock_reduction = w
         .flock_reduction
@@ -667,7 +667,7 @@ fn bind_pi_claim(
 /// Everything a recursion harness needs from an accepting verify run, named
 /// and typed: the deferred bytecode claims, the count-channel root, flock's
 /// reduction claims, and the stacked-opening summary (ring-switch challenges +
-/// Ligerito fold/query data). The sub-proof scalars themselves live on
+/// WHIR fold/query data). The sub-proof scalars themselves live on
 /// `proof.stream` at fixed offsets from its tail. Ordinary callers just
 /// `?`-discard it.
 pub struct VerifySummary {
@@ -691,7 +691,7 @@ pub fn verify(program: &Program, public_input: &[F192; 2], proof: &Proof) -> Res
     let root = pcs::read_commitment(&mut vs).map_err(Error::Transcript)?;
 
     // BLAKE3 ↔ flock (single PCS): flock's R1CS validity and every leanVM point
-    // claim are verified together by ONE Ligerito opening at the end. The executed-
+    // claim are verified together by ONE WHIR opening at the end. The executed-
     // BLAKE3 count is public (announced); its flock sub-proof rides the shared
     // `stream`/`openings`, and presence is enforced by consumption below plus
     // `vs.finish()` (a proof with `n_b3 = 0` but trailing flock data, or vice versa,
@@ -728,7 +728,7 @@ pub fn verify(program: &Program, public_input: &[F192; 2], proof: &Proof) -> Res
 
     // Replay flock's reduction straight off the shared stream (each scalar bound
     // as it is read) to recover its `(ab, c)` validity claims on q_pkd, then
-    // verify them alongside every point claim in the ONE Ligerito opening
+    // verify them alongside every point claim in the ONE WHIR opening
     // (mirroring `prove`). `n_blocks = max(n_b3, 1)`, always ≥ 1 instance.
     let n_blocks = n_b3.max(1);
     let offset = l.placements[QPKD].offset;
@@ -811,7 +811,7 @@ mod tests {
     /// cell), hash them into the output `c` (cells 6,7), pad with filler SETs so
     /// the last executed instruction lands one before the sentinel, and halt
     /// there. The flock validity sub-proof plus the memory / state / bytecode bus
-    /// interactions are verified end-to-end (the proof carries the Ligerito
+    /// interactions are verified end-to-end (the proof carries the WHIR
     /// opening they assert on).
     fn blake3_program(a: [F64; 4], b: [F64; 4]) -> Program {
         // a → cells 2,3 and b → cells 4,5 (two flock lanes per BLAKE3 cell).
@@ -882,9 +882,9 @@ mod tests {
 
         let (proof, stats) = prove(&program, pi, pcs::LOG_INV_RATE);
         assert_eq!(stats.counts[5], 1, "one BLAKE3 row");
-        // flock's sub-proof rides the shared channels: its Ligerito is the proof's
+        // flock's sub-proof rides the shared channels: its WHIR is the proof's
         // one opening, its scalar reduction trails the `stream`.
-        assert!(!proof.openings.is_empty(), "BLAKE3 program carries a Ligerito opening");
+        assert!(!proof.openings.is_empty(), "BLAKE3 program carries a WHIR opening");
         verify(&program, &pi, &proof).expect("BLAKE3 program verifies");
     }
 
@@ -953,7 +953,7 @@ mod tests {
         verify(&program, &pi, &proof).expect("self-hash BLAKE3 verifies");
     }
 
-    /// Tampering flock's validity sub-proof (its Ligerito, opened over the same
+    /// Tampering flock's validity sub-proof (its WHIR, opened over the same
     /// stacked commitment) must make verification fail.
     #[test]
     fn blake3_rejects_tampered_validity() {
@@ -967,8 +967,8 @@ mod tests {
 
         // The stacked opening is the proof's one hint; tamper a sumcheck
         // round message (the inner-product transcript); must be rejected.
-        let lig = proof.openings.last_mut().expect("stacked Ligerito opening");
-        lig.ligerito.sumcheck_transcript[0].u_0 += F192::ONE;
+        let lig = proof.openings.last_mut().expect("stacked WHIR opening");
+        lig.whir.sumcheck_transcript[0].u_0 += F192::ONE;
         assert!(
             verify(&program, &pi, &proof).is_err(),
             "tampered BLAKE3 validity proof must be rejected"
@@ -980,7 +980,7 @@ mod tests {
     /// the verifier's reduction/opening replay, so tampering a transport word
     /// diverges the recovered `(ab, c)` claims (or breaks decoding) and
     /// verification must reject. (Complements `blake3_rejects_tampered_validity`,
-    /// which tampers the Ligerito opening.)
+    /// which tampers the WHIR opening.)
     #[test]
     fn blake3_rejects_tampered_reduction() {
         let program = blake3_program(
@@ -1019,7 +1019,7 @@ mod tests {
         let pi = [F192::new(1, 2, 3), F192::new(4, 5, 6)];
         let (proof, stats) = prove(&program, pi, pcs::LOG_INV_RATE);
         assert_eq!(stats.counts[5], 0, "no real BLAKE3 rows");
-        // The proof still carries exactly one Ligerito opening (over the padding).
+        // The proof still carries exactly one WHIR opening (over the padding).
         assert_eq!(proof.openings.len(), 1, "unified path: one opening always");
         verify(&program, &pi, &proof).expect("non-BLAKE3 program verifies");
     }