feat: commit the R1CS witness over the base field (proof format 2.0)

provekit/backend/bn254/src/field.rs

@@ -5,23 +5,21 @@
 use {
     crate::{bytes::field_to_bytes_le, FieldElement, TranscriptSponge},
     provekit_common::{Base, Ext, FieldHash, HashConfig, ProofField},
-    whir::{
-        algebra::embedding::Identity,
-        protocols::{whir::Config as GenericWhirConfig, whir_zk::Config as GenericWhirZkConfig},
-    },
+    whir::{algebra::embedding::Identity, protocols::whir::Config as GenericWhirConfig},
 };
 
 /// The WHIR config over the bn254 embedding.
 pub type WhirConfig = GenericWhirConfig<Identity<FieldElement>>;
-/// The zero-knowledge WHIR config over the bn254 extension field.
-pub type WhirZkConfig = GenericWhirZkConfig<FieldElement>;
 
 /// bn254 proof field: the `Identity<Fr>` embedding (base == ext).
 #[derive(Clone, Copy, Debug, PartialEq, Eq)]
 pub struct Bn254Field;
 
 impl ProofField for Bn254Field {
     type Embedding = Identity<FieldElement>;
+
+    // Field tag written into the `.np` proof format header; 0 identifies bn254.
+    const FIELD_ID: u8 = 0;
 }
 
 impl FieldHash for Bn254Field {
@@ -52,6 +50,6 @@ mod tests {
         assert_eq!(bytes_to_field(&bytes), x);
     }
 
-    // Byte-exact public-input hashing is pinned by the KATs in
-    // `crate::field_hash::tests` (the bn254 bit-identical regression gate).
+    // Byte-exact public-input hashing is pinned by the known-answer tests in
+    // `crate::field_hash::tests`.
 }

provekit/backend/bn254/src/lib.rs

@@ -24,7 +24,7 @@ pub use {
     acir::FieldElement as NoirElement,
     ark_bn254::Fr as FieldElement,
     compress::CompressedLayers,
-    field::{Bn254Field, WhirConfig, WhirZkConfig},
+    field::{Bn254Field, WhirConfig},
     frontend::{noir_to_native, NoirWitnessGenerator, PrintAbi},
     ntt::RSFr,
     prove::Prove,

provekit/backend/bn254/src/mavros_prove.rs

@@ -1,8 +1,10 @@
-//! Mavros WHIR proving, welded to bn254 (the Mavros VM's automatic-
-//! differentiation pass returns `ark_bn254::Fr`). It composes the generic
-//! proving primitives from `provekit-prover` (`run_zk_sumcheck_prover`,
-//! `prove_from_alphas`) rather than living in the field-generic spine, and
-//! folds back into `WhirR1CSProver<P>` once the Mavros VM is field-agnostic.
+//! Mavros WHIR proving for bn254. The Mavros VM's automatic-differentiation
+//! pass returns `ark_bn254::Fr`, so this proving path is bn254-specific; it
+//! composes the generic proving primitives from `provekit-prover`
+//! (`run_zk_sumcheck_prover`, `prove_from_alphas`).
+//!
+//! TODO: make field-generic and fold into `WhirR1CSProver<P>` when the Mavros
+//! VM is field-agnostic.
 
 use {
     crate::{Bn254Field, FieldElement, TranscriptSponge},
@@ -49,18 +51,19 @@ impl MavrosR1CSProver for WhirR1CSScheme<Bn254Field> {
         let blinding = commitments[0]
             .blinding
             .as_ref()
-            .expect("c1 must carry blinding state");
+            .ok_or_else(|| anyhow::anyhow!("c1 must carry blinding state"))?;
 
         let [a, b, c] = [witgen.out_a, witgen.out_b, witgen.out_c];
+        // `g` is committed separately in the extension field; open `blinding_eval`
+        // against the blinding vector (g flattened at offset 0).
         let (alpha, blinding_eval) = run_zk_sumcheck_prover(
             a,
             b,
             c,
             &mut merlin,
             self.m_0,
             &blinding.polynomial,
-            &commitments[0].polynomial,
-            blinding.offset,
+            &blinding.vector,
         );
 
         let eq_alpha =
@@ -73,15 +76,13 @@ impl MavrosR1CSProver for WhirR1CSScheme<Bn254Field> {
         )?;
         let alphas = [ad_a, ad_b, ad_c];
 
-        let blinding_offset = blinding.offset;
         let blinding_weights = expand_powers::<4, _>(&alpha);
 
         prove_from_alphas(
             self,
             merlin,
             alphas,
             blinding_eval,
-            blinding_offset,
             blinding_weights,
             commitments,
             public_inputs,

provekit/backend/goldilocks/src/field.rs

@@ -1,35 +1,76 @@
-//! The Goldilocks degree-3 extension proof field and its `FieldHash` glue.
+//! The Goldilocks proof fields (base-leaf and ext-leaf) and their shared
+//! `FieldHash` glue.
 
 use {
     crate::{bytes::field_to_bytes_le, field_hash::hash_field_elements, TranscriptSponge},
     provekit_common::{Base, Ext, FieldHash, HashConfig, ProofField},
-    whir::algebra::{embedding::Identity, fields::Field64_3},
+    whir::algebra::{
+        embedding::{Basefield, Identity},
+        fields::Field64_3,
+    },
 };
 
-/// Goldilocks degree-3 extension proof field.
+/// The Goldilocks proof field: `Basefield<Field64_3>`.
+///
+/// Commits the witness in the base field `Field64` and uses the degree-3
+/// extension `Field64_3` only for challenges and sumcheck.
 #[derive(Clone, Copy, Debug, PartialEq, Eq)]
 pub struct GoldilocksField;
 
 impl ProofField for GoldilocksField {
+    type Embedding = Basefield<Field64_3>;
+
+    const FIELD_ID: u8 = 1;
+}
+
+/// Goldilocks proof field with the identity embedding (`Identity<Field64_3>`,
+/// base == ext): challenges are both drawn from and committed in the full
+/// `Field64_3` extension.
+///
+/// Serves challenge-bearing circuits, where an extension challenge cannot be
+/// stored in a base-field (`Field64`) witness slot; committing in the extension
+/// keeps 128-bit soundness.
+// TODO: `GoldilocksField` (base-committed) can subsume this once it binds
+// challenges directly — needs (1) a base transcript codec so base challenges can
+// be drawn from Fiat-Shamir (the `FieldHash` `Source` byte bridge), and (2)
+// k-fold repetition, since a single `Field64` challenge is only ~64-bit sound.
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub struct GoldilocksEfField;
+
+impl ProofField for GoldilocksEfField {
     type Embedding = Identity<Field64_3>;
+
+    // Distinct from `GoldilocksField`: the ext-leaf base layout (`Field64_3`)
+    // differs from its base-commit layout (`Field64`), so their serialized bytes
+    // differ.
+    const FIELD_ID: u8 = 2;
 }
 
-impl FieldHash for GoldilocksField {
-    fn hash_public_inputs(config: HashConfig, inputs: &[Base<Self>]) -> Ext<Self> {
-        hash_field_elements(config, inputs)
-    }
+/// Both Goldilocks fields share the same hash/byte glue: the challenge field is
+/// `Field64_3` either way, and the public-input hash is base-generic.
+macro_rules! impl_goldilocks_field_hash {
+    ($field:ty) => {
+        impl FieldHash for $field {
+            fn hash_public_inputs(config: HashConfig, inputs: &[Base<Self>]) -> Ext<Self> {
+                hash_field_elements(config, inputs)
+            }
 
-    fn ext_to_bytes_le(x: &Ext<Self>) -> Vec<u8> {
-        field_to_bytes_le(*x).to_vec()
-    }
+            fn ext_to_bytes_le(x: &Ext<Self>) -> Vec<u8> {
+                field_to_bytes_le(*x).to_vec()
+            }
 
-    type Sponge = TranscriptSponge;
+            type Sponge = TranscriptSponge;
 
-    fn transcript_sponge(config: HashConfig) -> Self::Sponge {
-        TranscriptSponge::from_config(config)
-    }
+            fn transcript_sponge(config: HashConfig) -> Self::Sponge {
+                TranscriptSponge::from_config(config)
+            }
+        }
+    };
 }
 
+impl_goldilocks_field_hash!(GoldilocksField);
+impl_goldilocks_field_hash!(GoldilocksEfField);
+
 #[cfg(test)]
 mod tests {
     use {super::*, crate::bytes::bytes_to_field};

provekit/backend/goldilocks/src/lib.rs

@@ -6,7 +6,10 @@ mod field;
 mod field_hash;
 mod transcript_sponge;
 
-pub use {field::GoldilocksField, transcript_sponge::TranscriptSponge};
+pub use {
+    field::{GoldilocksEfField, GoldilocksField},
+    transcript_sponge::TranscriptSponge,
+};
 
 /// Register the Goldilocks engines in whir's global registries.
 ///

provekit/common/src/field.rs

@@ -9,14 +9,20 @@ use {
 /// Algebra carrier for a proof field: `Embedding::Source` is the base
 /// (committed) field, `Embedding::Target` the extension (challenge) field.
 ///
-/// bn254 uses `Identity<Fr>` (base == ext); goldilocks uses
-/// `Identity<Field64_3>` pre-v3, `Basefield<Field64_3>` once zkWHIR v3 lands.
+/// bn254 uses `Identity<Fr>` (base == ext); a field with a genuine
+/// extension uses an embedding whose source and target differ (e.g.
+/// `Basefield<Field64_3>`).
 pub trait ProofField: Copy + Debug + Eq + Send + Sync {
     /// `Default` lets the spine construct the embedding instance for mixed
     /// base×ext products (`Identity`/`Basefield` both derive it). The extension
     /// (`Target`) must be FFT-friendly and transcript-codec-able — WHIR's
     /// requirement for any challenge/commitment field.
     type Embedding: Embedding<Target: FftField + Codec> + Default;
+
+    /// Per-field tag folded into the `.np` proof magic so one field's proof is
+    /// rejected by another field's verifier. Must be unique per field; bn254
+    /// reserves `0` to keep its legacy magic byte-identical.
+    const FIELD_ID: u8;
 }
 
 /// Base (committed) field of a [`ProofField`].
@@ -44,6 +50,5 @@ pub trait FieldHash: ProofField {
     /// Construct the transcript sponge matching `config`.
     fn transcript_sponge(config: crate::HashConfig) -> Self::Sponge;
 
-    // TODO(base-bridge): add a base (`Source`) bridge when base commitment lands
-    // (V-stage).
+    // TODO: add a base-field (`Source`) byte bridge when one is needed.
 }

provekit/common/src/file/binary_format.rs

@@ -12,16 +12,19 @@ pub const XZ_MAGIC: [u8; 6] = [0xfd, 0x37, 0x7a, 0x58, 0x5a, 0x00];
 
 // ---------------------------------------------------------------------------
 // Per-format identifiers and versions
+//
+// Major must match exactly on read (an incompatible layout is rejected); a
+// reader accepts any file whose minor is >= its own.
 // ---------------------------------------------------------------------------
 
 pub const PROVER_FORMAT: [u8; 8] = *b"PrvKitPr";
-pub const PROVER_VERSION: (u16, u16) = (1, 3);
+pub const PROVER_VERSION: (u16, u16) = (2, 0);
 
 pub const VERIFIER_FORMAT: [u8; 8] = *b"PrvKitVr";
-pub const VERIFIER_VERSION: (u16, u16) = (1, 3);
+pub const VERIFIER_VERSION: (u16, u16) = (2, 0);
 
 pub const NOIR_PROOF_SCHEME_FORMAT: [u8; 8] = *b"NrProScm";
-pub const NOIR_PROOF_SCHEME_VERSION: (u16, u16) = (1, 3);
+pub const NOIR_PROOF_SCHEME_VERSION: (u16, u16) = (2, 0);
 
 pub const NOIR_PROOF_FORMAT: [u8; 8] = *b"NPSProof";
-pub const NOIR_PROOF_VERSION: (u16, u16) = (1, 1);
+pub const NOIR_PROOF_VERSION: (u16, u16) = (2, 0);

provekit/common/src/prefix_covector.rs

@@ -1,6 +1,6 @@
 use {
-    ark_ff::Field,
-    whir::algebra::{dot, linear_form::LinearForm, multilinear_extend},
+    ark_ff::{Field, One, Zero},
+    whir::algebra::{embedding::Embedding, linear_form::LinearForm, mixed_dot, multilinear_extend},
 };
 
 /// A covector that stores only a power-of-two prefix, with the rest
@@ -207,26 +207,32 @@ pub fn build_prefix_covectors<const N: usize, F: Field>(
 /// allocating [`PrefixCovector`] weights. Used to write transcript hints
 /// before deferring weight construction (saves memory in dual-commit).
 #[must_use]
-pub fn compute_alpha_evals<const N: usize, F: Field>(
-    polynomial: &[F],
-    alphas: &[Vec<F>; N],
-) -> Vec<F> {
+pub fn compute_alpha_evals<const N: usize, M: Embedding>(
+    embedding: &M,
+    polynomial: &[M::Source],
+    alphas: &[Vec<M::Target>; N],
+) -> Vec<M::Target> {
     alphas
         .iter()
-        .map(|w| dot(w, &polynomial[..w.len()]))
+        .map(|w| mixed_dot(embedding, w, &polynomial[..w.len()]))
         .collect()
 }
 
 /// Compute the public weight evaluation `⟨[1, x, x², …, x^N], poly[0..=N]⟩`
 /// without allocating a [`PrefixCovector`]. Covers the R1CS constant at
 /// position 0 and `num_public_inputs` public input positions.
 #[must_use]
-pub fn compute_public_eval<F: Field>(x: F, num_public_inputs: usize, polynomial: &[F]) -> F {
+pub fn compute_public_eval<M: Embedding>(
+    embedding: &M,
+    x: M::Target,
+    num_public_inputs: usize,
+    polynomial: &[M::Source],
+) -> M::Target {
     let n = num_public_inputs + 1;
-    let mut eval = F::zero();
-    let mut x_pow = F::one();
+    let mut eval = M::Target::zero();
+    let mut x_pow = M::Target::one();
     for &p in polynomial.iter().take(n) {
-        eval += x_pow * p;
+        eval += embedding.mixed_mul(x_pow, p);
         x_pow *= x;
     }
     eval
@@ -321,11 +327,16 @@ pub fn make_challenge_weight<F: Field>(
 /// `⟨[1, x, x², …], poly[offsets[0]], poly[offsets[1]], …⟩` without
 /// allocating a [`SparseCovector`].
 #[must_use]
-pub fn compute_challenge_eval<F: Field>(x: F, challenge_offsets: &[usize], polynomial: &[F]) -> F {
-    let mut eval = F::zero();
-    let mut x_pow = F::one();
+pub fn compute_challenge_eval<M: Embedding>(
+    embedding: &M,
+    x: M::Target,
+    challenge_offsets: &[usize],
+    polynomial: &[M::Source],
+) -> M::Target {
+    let mut eval = M::Target::zero();
+    let mut x_pow = M::Target::one();
     for &offset in challenge_offsets {
-        eval += x_pow * polynomial[offset];
+        eval += embedding.mixed_mul(x_pow, polynomial[offset]);
         x_pow *= x;
     }
     eval
@@ -605,7 +616,8 @@ mod tests {
         poly[5] = fe(99);
         poly[11] = fe(17);
 
-        let eval = compute_challenge_eval(x, &offsets, &poly);
+        let embedding = whir::algebra::embedding::Identity::<FieldElement>::new();
+        let eval = compute_challenge_eval(&embedding, x, &offsets, &poly);
         let expected = fe(42) + fe(7) * fe(99) + fe(49) * fe(17);
         assert_eq!(eval, expected);
     }