prover: LogUp k4 is the default on the STARK base tables

`LAMBDA_VM_ZF_LOGUP` unset now selects k4 (up to four LogUp interactions per
aux column where the arity rule admits it); `=pair` keeps the previous bytes
and is the rollback. The setting reaches the block's base tables only
(block_base_options); the LFM chips keep pairs. Measured as the opt-in:
median phase B -9.56 s (BIG 600, t -27), 1x base -0.97 s (FAST 861).

Every consumer derives the layout from the options, not from the proof: the
base AIRs pick the arity in AirWithBuses::new from options.format.logup, the
host verifier and the block verifier build those AIRs from
block_base_options, and the tree's leaf programs size each base sub-proof
(aux width, composition parts, constraint program) from the same AIRs.

Tests: the default base options build exactly the k4 programs and the pair
spelling builds the golden pair list; a pair proof is refused under the k4
layout (the reverse of N3); the production-sites test expects the base
format's arity; the pinned tree ids derive under pair, the format they were
recorded under.

Author: MauroToscano

crypto/stark/src/tests/bus_tests/logup_arity_tests.rs

@@ -352,6 +352,19 @@ fn a_k4_proof_is_refused_under_the_pair_layout() {
     assert!(!verifies(&pair, &proof));
 }
 
+/// N3 reversed, now that k4 is the production default: a pair-layout proof
+/// (the rollback) checked against the k4 AIR is refused on shape too, so a
+/// verifier at the default never accepts a proof made at the rollback.
+#[test]
+fn a_pair_proof_is_refused_under_the_k4_layout() {
+    let pair = air(6, 1, &options(4, LogUpPolicy::Pair));
+    let proof = prove(&pair, trace(6, 1, 13));
+    assert!(verifies(&pair, &proof), "the pair control proof verifies");
+    let k4 = air(6, 1, &options(4, LogUpPolicy::K4));
+    assert_eq!(k4.trace_layout().1, 4);
+    assert!(!verifies(&k4, &proof));
+}
+
 /// N4: a proof carrying 3 or 5 part OODs for a 4-part AIR.
 #[test]
 fn a_wrong_composition_part_count_is_refused() {

prover/src/lfm/block_tree_tests.rs

@@ -777,11 +777,30 @@ fn production_height_plan() -> BlockTreePlan {
 
 /// [`spread_fixture_shape`]'s plan under the block base's options.
 fn spread_plan(chunks: usize, cpus: usize) -> BlockTreePlan {
-    let opts = super::proof::block_base_options();
+    spread_plan_under(chunks, cpus, &super::proof::block_base_options())
+}
+
+/// [`spread_plan`] at the default format with the LogUp pair layout — the
+/// format the pinned tree ids were recorded under, before k4 became the
+/// default. The pins guard the program form, which no format choice changes,
+/// so they keep holding at the rollback format.
+fn pinned_spread_plan(chunks: usize, cpus: usize) -> BlockTreePlan {
+    let pair = crate::zf_format::ZfFormat {
+        logup: stark::proof::options::LogUpPolicy::Pair,
+        ..crate::zf_format::ZfFormat::DEFAULT
+    };
+    spread_plan_under(
+        chunks,
+        cpus,
+        &pair.base_options(crate::recursion::Preset::Blowup4.options()),
+    )
+}
+
+fn spread_plan_under(chunks: usize, cpus: usize, opts: &crate::ProofOptions) -> BlockTreePlan {
     let elf_bytes = crate::test_utils::asm_elf_bytes("poc_rodata_commit");
     let elf = executor::elf::Elf::load(&elf_bytes).expect("load the ELF");
     let shape = spread_fixture_shape(&elf, chunks, cpus);
-    BlockTreePlan::derive(&elf_bytes, &opts, &shape).expect("the plan derives")
+    BlockTreePlan::derive(&elf_bytes, opts, &shape).expect("the plan derives")
 }
 
 /// ★ D-ANYBLOCK S5 §4.13 instrument (laptop): a block leaf program's host bytes
@@ -1123,7 +1142,7 @@ fn check_pinned_tree_ids(label: &str, plan: &BlockTreePlan, pins: &[(&str, &[&st
 #[test]
 #[should_panic(expected = "no pinned ids for the fixture ELF's digest")]
 fn pinned_tree_ids_refuse_an_elf_they_do_not_know() {
-    check_pinned_tree_ids("NONE", &spread_plan(2, 4), &[("00", &[])]);
+    check_pinned_tree_ids("NONE", &pinned_spread_plan(2, 4), &[("00", &[])]);
 }
 
 /// The fixture ELF's digest on the laptop (macOS clang) and on FAST.
@@ -1137,7 +1156,7 @@ const FAST_ELF_DIGEST: &str = "f5e120d0eaa369d7ebdec2767b8d0c0559ceeac138edf0970
 #[test]
 #[ignore = "laptop or box: run with --exact"]
 fn the_compact_program_form_keeps_a_small_trees_ids() {
-    check_pinned_tree_ids("SMALL TREE IDS", &spread_plan(2, 4), &SMALL_TREE_IDS);
+    check_pinned_tree_ids("SMALL TREE IDS", &pinned_spread_plan(2, 4), &SMALL_TREE_IDS);
 }
 
 /// The same at production heights ([`production_height_plan`]: 7 leaves, 2
@@ -1148,7 +1167,7 @@ fn the_compact_program_form_keeps_a_small_trees_ids() {
 fn the_compact_program_form_keeps_every_production_height_tree_id() {
     check_pinned_tree_ids(
         "TREE IDS",
-        &production_height_plan(),
+        &pinned_spread_plan(13, 40),
         &PRODUCTION_HEIGHT_TREE_IDS,
     );
 }

prover/src/tests/compiled_constraints.rs

@@ -116,7 +116,7 @@ pub(crate) fn production_programs(
 
 /// The option sets the compiled kernels cover: the legacy format at blowup 2
 /// and 4 (every program the pair layout builds), and the VM tables under
-/// `LAMBDA_VM_ZF_LOGUP=k4` at the block's blowup 4 (the tables the rule moves
+/// k4, the block's default, at its blowup 4 (the tables the rule moves
 /// to four interactions per column get their own programs; the LFM chips keep
 /// pairs under every policy and the local-to-global tables are too narrow to
 /// move, so neither is rebuilt).

prover/src/tests/logup_arity_tests.rs

@@ -140,13 +140,9 @@ fn options(blowup: u8, logup: LogUpPolicy) -> ProofOptions {
     opts
 }
 
-/// ★ T0a: under the pair policy, every production VM table and every LFM chip
-/// has today's widths, part count and constraint program, byte for byte —
-/// the default format moves no compiled-kernel key and no proof. The same
-/// holds for a wide policy at a blowup that cannot hold wider groups.
-#[test]
-fn the_pair_policy_keeps_every_production_program() {
-    let golden: Vec<Program> = PAIR_GOLDEN
+/// [`PAIR_GOLDEN`] as programs.
+fn pair_golden() -> Vec<Program> {
+    PAIR_GOLDEN
         .iter()
         .map(|&(label, main, aux, parts, digest)| Program {
             label: label.to_string(),
@@ -155,7 +151,17 @@ fn the_pair_policy_keeps_every_production_program() {
             parts,
             digest,
         })
-        .collect();
+        .collect()
+}
+
+/// ★ T0a: under the pair policy, every production VM table and every LFM chip
+/// has the widths, part count and constraint program it had before arities
+/// existed, byte for byte — the rollback (`LAMBDA_VM_ZF_LOGUP=pair`) moves no
+/// compiled-kernel key and no proof. The same holds for a wide policy at a
+/// blowup that cannot hold wider groups.
+#[test]
+fn the_pair_policy_keeps_every_production_program() {
+    let golden = pair_golden();
     assert!(!golden.is_empty(), "the golden list is pinned");
     assert_eq!(programs(&options(4, LogUpPolicy::Pair)), golden);
     let legacy = GoldilocksCubicProofOptions::with_blowup(4).expect("blowup 4");
@@ -171,6 +177,27 @@ fn the_pair_policy_keeps_every_production_program() {
     }
 }
 
+/// ★ k4 is the production default: the block's base options with no knob set
+/// ([`crate::zf_format::ZfFormat::DEFAULT`]) build exactly the k4 programs, and
+/// the rollback spelling `LAMBDA_VM_ZF_LOGUP=pair` builds the golden pair list,
+/// byte for byte.
+#[test]
+fn the_default_base_format_is_k4_and_pair_rolls_back() {
+    use crate::zf_format::{ENV_LOGUP, ZfFormat};
+    let base = GoldilocksCubicProofOptions::with_blowup(4).expect("blowup 4");
+    let default = ZfFormat::DEFAULT.base_options(base.clone());
+    assert_eq!(default.format.logup, LogUpPolicy::K4);
+    assert_eq!(programs(&default), programs(&options(4, LogUpPolicy::K4)));
+    assert_ne!(
+        programs(&default),
+        pair_golden(),
+        "k4 moves the switched tables"
+    );
+    let rollback = ZfFormat::from_lookup(|name| (name == ENV_LOGUP).then(|| "pair".to_string()))
+        .expect("the rollback spelling parses");
+    assert_eq!(programs(&rollback.base_options(base)), pair_golden());
+}
+
 /// ★ T0f on the production tables: under `k4` at blowup 4 each table commits
 /// `⌈N/k⌉` aux columns and `max(3, k + 1) − 1` parts for the arity the rule
 /// picks (D-LOGUP §2.2), the LFM chips keep pairs under the production

prover/src/zf_format.rs

@@ -13,7 +13,7 @@
 //!
 //! ★ Every unset knob is [`ZfFormat::DEFAULT`], the MEASURED configuration:
 //! `cap=auto whir_cap=auto fri=dp one_row=auto whir_folds=first6 whir_stack=27 whir_grind=query
-//! logup=pair`.
+//! logup=k4`.
 //! Each lever was measured net positive on block runs before it became the
 //! default (`one_row=auto` on the STARK pipeline: see [`ZfFormat::DEFAULT`]).
 //! Every knob keeps its OFF spelling (`cap=off`, `whir_cap=off`,
@@ -52,7 +52,7 @@
 //! `*_IMPLEMENTED` constant is flipped when its lever is real.
 //!
 //! **The banner prints on every setting, including the default**:
-//! `ZF FORMAT: cap=auto whir_cap=auto fri=dp one_row=auto whir_folds=first6 whir_stack=27 whir_grind=query logup=pair`.
+//! `ZF FORMAT: cap=auto whir_cap=auto fri=dp one_row=auto whir_folds=first6 whir_stack=27 whir_grind=query logup=k4`.
 //! Its absence in a log is then a fact about the run, not an ambiguity.
 
 use std::sync::OnceLock;
@@ -210,6 +210,12 @@ impl ZfFormat {
     /// query grinds and the blowups are the legacy ones. It changes no STARK
     /// proof. `LAMBDA_VM_ZF_WHIR_STACK=25` is the stack's rollback and
     /// `LAMBDA_VM_ZF_WHIR_GRIND=all` the grind's.
+    /// `logup=k4` commits up to four LogUp interactions per aux column on the
+    /// STARK base tables where the rule admits it (degree ≤ blowup + 1): the
+    /// median block's phase B −9.56 s (BIG 600, t −27) and the 1× base −0.97 s
+    /// (FAST 861), most of it from smaller per-table device sets packing under
+    /// the VRAM gate. It reaches the base tables only ([`Self::base_proof_format`]);
+    /// the LFM chips keep pairs. `LAMBDA_VM_ZF_LOGUP=pair` is its rollback.
     pub const DEFAULT: Self = Self {
         cap: CapPolicy::Auto,
         whir_cap: CapPolicy::Auto,
@@ -218,7 +224,7 @@ impl ZfFormat {
         whir_folds: WhirFolds::First(DEFAULT_WHIR_FIRST_FOLD),
         whir_stack: DEFAULT_WHIR_STACK,
         whir_grind: WhirGrind::Query,
-        logup: LogUpPolicy::Pair,
+        logup: LogUpPolicy::K4,
     };
 
     /// The legacy format: every lever off. What all eight knobs at their
@@ -565,13 +571,13 @@ mod tests {
                 whir_folds: WhirFolds::First(FirstFold::new(6).unwrap()),
                 whir_stack: StackVars::new(27).unwrap(),
                 whir_grind: WhirGrind::Query,
-                logup: LogUpPolicy::Pair,
+                logup: LogUpPolicy::K4,
             }
         );
         assert_eq!(
             f.banner(),
             "ZF FORMAT: cap=auto whir_cap=auto fri=dp one_row=auto whir_folds=first6 whir_stack=27 \
-             whir_grind=query logup=pair"
+             whir_grind=query logup=k4"
         );
         assert!(!f.is_legacy());
         assert!(f.unimplemented_levers().is_empty());
@@ -865,7 +871,7 @@ mod tests {
                 .unwrap()
                 .banner(),
             "ZF FORMAT: cap=auto whir_cap=auto fri=dp one_row=auto whir_folds=first6 whir_stack=27 \
-             whir_grind=query logup=pair"
+             whir_grind=query logup=k4"
         );
     }
 
@@ -1150,15 +1156,17 @@ mod tests {
         // No test sets a ZF knob, so the process format is the default and the
         // production constructors must stamp the MEASURED configuration.
         assert_eq!(*ZfFormat::global(), ZfFormat::DEFAULT);
-        let want = ZfFormat::DEFAULT.proof_format();
-        for (site, o) in [
+        // The LFM proofs carry the chips' pair layout; the base, the default arity.
+        for (site, o, want) in [
             (
                 "aggregation_wrap_options",
                 crate::lfm::proof::aggregation_wrap_options(),
+                ZfFormat::DEFAULT.proof_format(),
             ),
             (
                 "block_base_options",
                 crate::lfm::proof::block_base_options(),
+                ZfFormat::DEFAULT.base_proof_format(),
             ),
         ] {
             assert_eq!(o.format, want, "{site}");
@@ -1384,12 +1392,12 @@ mod tests {
     }
 
     /// `LAMBDA_VM_ZF_LOGUP`: every spelling parses to its policy and moves no
-    /// other field; `pair` is the default and the legacy value. A policy whose
+    /// other field; `k4` is the default, `pair` the legacy value and the rollback. A policy whose
     /// device path this build lacks is reported (and so aborts at
     /// [`ZfFormat::global`]), never proved as another format.
     #[test]
     fn the_logup_knob_parses_and_unbuilt_policies_are_refused() {
-        assert_eq!(ZfFormat::DEFAULT.logup, LogUpPolicy::Pair);
+        assert_eq!(ZfFormat::DEFAULT.logup, LogUpPolicy::K4);
         assert_eq!(ZfFormat::LEGACY.logup, LogUpPolicy::Pair);
         for (v, want) in [
             ("pair", LogUpPolicy::Pair),
@@ -1474,10 +1482,10 @@ mod tests {
             );
             assert_eq!(f.proof_format(), ZfFormat::DEFAULT.proof_format());
         }
-        // No knob set: the production base options are the pair layout.
+        // No knob set: the production base options carry k4; the chips, pairs.
         assert_eq!(
             crate::lfm::proof::block_base_options().format.logup,
-            LogUpPolicy::Pair
+            LogUpPolicy::K4
         );
         assert_eq!(
             crate::lfm::proof::aggregation_wrap_options().format.logup,