feat(qwen35): Qwen3.5 / Qwen3.8 hybrid GGUFs run on the CPU — apr run + apr chat (#3091)

contracts/qwen35-e2e-verification-v1.yaml

@@ -93,11 +93,33 @@ proof_obligations:
   property: Parameter count matches architecture
   formal: P(Qwen3.5-9B) ∈ [9.0B, 9.2B]
   applies_to: all
+  note: >-
+    #3091: the 9B instantiation is NOT proved, and is not asserted anywhere. This
+    contract's own model_parameter_count formula, evaluated on the in-tree
+    constants (contracts/model-families/qwen3_5.yaml size_variants.9b: V=248320,
+    d=4096, L=32, n_h=16, d_k=256, intermediate_dim=12288, untied lm_head), sums to
+    8,208,535,552 = 8.209B -- outside [9.0B, 9.2B]. That descriptor's
+    tensor_template states no Gated DeltaNet tensors, so the ~0.8B difference has no
+    in-tree shape to come from, and whether the range or the descriptor is wrong is
+    open. qe2e_inv_001_parameter_sum_matches_tensor_inventory discharges the
+    model_parameter_count EQUATION (the config-derived sum equals the measured
+    tensor inventory) on the real Qwen3.5 layer structures; the range instantiation
+    stays unproved rather than being widened to fit.
 - id: QE2E-BND-002
   type: bound
   property: FLOPs bounded by 2P
-  formal: F <= 2 * P + O(seq_len * d * L)
+  formal: F(s) <= 2*P + 4*L_attn*d_kv*s
   applies_to: all
+  note: >-
+    ont-delta (#3091): tightened from 'F <= 2 * P + O(seq_len * d * L)'. An O()
+    with no constant states no bound at all -- every F satisfies it, so no input
+    could falsify the obligation and FALSIFY-QE2E-002 had nothing to assert. The
+    constant is now named: s = cached positions, L_attn = full-attention layers
+    (a Gated DeltaNet layer carries a fixed-size recurrent state, so its cost does
+    not grow with s), d_kv = num_kv_heads * head_dim, and QK^T and A*V each cost
+    2*d_kv per cached position per such layer. The slope is asserted as an
+    EQUALITY by qe2e_bnd_002_flops_bounded_by_2p_plus_attention_term, so the
+    constant cannot be lowered either.
 - id: QE2E-ORD-003
   type: ordering
   property: Quantization memory ordering
@@ -140,17 +162,17 @@ falsification_tests:
 - id: FALSIFY-QE2E-002
   rule: FLOPs estimate
   prediction: 2P FLOPs per forward token
-  test: Deterministic with Qwen3.5-9B constants
+  test: qe2e_bnd_002_flops_bounded_by_2p_plus_attention_term
   if_fails: Missing layer in FLOP count
 - id: FALSIFY-QE2E-003
   rule: Memory ordering
   prediction: Q4K < Q6K < F16 < F32 memory
-  test: proptest with random tensor dimensions
+  test: qe2e_ord_003_quantization_memory_ordering
   if_fails: Quantization byte formula wrong
 - id: FALSIFY-QE2E-004
   rule: Throughput roofline
   prediction: tok/s bounded by bandwidth and compute
-  test: proptest with random hardware specs
+  test: qe2e_mon_004_throughput_is_monotone_in_bandwidth
   if_fails: Roofline formula error
 - id: FALSIFY-QE2E-005
   rule: Coverage completeness
@@ -160,12 +182,12 @@ falsification_tests:
 - id: FALSIFY-QE2E-006
   rule: Compositional proof structure
   prediction: 'Each block preserves shape: shape(block_l(x)) = shape(x)'
-  test: 'proptest: verify shape(block(x)) = shape(x) for random blocks'
+  test: qe2e_inv_006_every_block_preserves_d_model
   if_fails: Block l breaks shape invariant
 - id: FALSIFY-QE2E-007
   rule: End-to-end shape conservation
   prediction: tokens → [seq_len, d] → ... → [seq_len, V]
-  test: 'proptest: trace shapes through mock pipeline'
+  test: qe2e_con_007_tokens_in_logits_out_shape
   if_fails: Shape break in layer composition
 kani_harnesses:
 - id: KANI-QE2E-001

crates/apr-cli/src/commands/chat_generate_session_02.rs

@@ -264,47 +264,8 @@ impl ChatSession {
                 }
             }
 
-            // CPU path — create fresh OwnedQuantizedModel from cached or fresh mapped
-            let model = OwnedQuantizedModel::from_mapped(mapped)
-                .map_err(|e| format!("Failed to create GGUF model: {e}"))?;
-
-            // APR-TRACE-001: Use traced generation when --trace is enabled
-            let output_tokens = if config.trace {
-                use realizar::{InferenceTracer, ModelInfo, TraceConfig};
-
-                let trace_config = TraceConfig {
-                    enabled: true,
-                    verbose: false,
-                    output: config.trace_output.clone(),
-                    ..Default::default()
-                };
-
-                let mut tracer = InferenceTracer::new(trace_config);
-                tracer.set_model_info(ModelInfo {
-                    name: "GGUF Model (CPU)".to_string(),
-                    num_layers: model.config().num_layers,
-                    hidden_dim: model.config().hidden_dim,
-                    vocab_size: model.config().vocab_size,
-                    num_heads: model.config().num_heads,
-                    quant_type: None,
-                });
-
-                eprintln!("Warning: CPU traced generation not implemented, using non-traced path");
-
-                let result = model
-                    .generate_with_cache(&prompt_tokens, &gen_config)
-                    .map_err(|e| format!("GGUF generate failed: {e}"))?;
-
-                if let Err(e) = tracer.write_output() {
-                    eprintln!("Warning: Failed to write trace output: {e}");
-                }
-
-                result
-            } else {
-                model
-                    .generate_with_cache(&prompt_tokens, &gen_config)
-                    .map_err(|e| format!("GGUF generate failed: {e}"))?
-            };
+            let output_tokens =
+                Self::generate_gguf_cpu_tokens(mapped, &prompt_tokens, &gen_config, config)?;
 
             let new_tokens = if output_tokens.len() > prompt_len {
                 &output_tokens[prompt_len..]
@@ -316,6 +277,75 @@ impl ChatSession {
             Ok(decoded)
         }
 
+        /// CPU generation for one GGUF chat turn: the Qwen3.5 hybrid forward (#3091), which the
+        /// dense `OwnedQuantizedModel` loader refuses, or the dense model. Returns the prompt
+        /// followed by the generated tokens.
+        fn generate_gguf_cpu_tokens(
+            mapped: &realizar::gguf::MappedGGUFModel,
+            prompt_tokens: &[u32],
+            gen_config: &realizar::gguf::QuantizedGenerateConfig,
+            config: &ChatConfig,
+        ) -> Result<Vec<u32>, String> {
+            use realizar::gguf::OwnedQuantizedModel;
+
+            if mapped.model.architecture() == Some("qwen35") {
+                let base = realizar::gguf::forward_qwen35::Qwen35Model::create_base_model(
+                    &mapped.model,
+                    mapped.data(),
+                )
+                .map_err(|e| format!("Failed to load the Qwen3.5 base model: {e}"))?;
+                return realizar::gguf::forward_qwen35::run_qwen35_generate(
+                    mapped,
+                    &base,
+                    prompt_tokens,
+                    gen_config,
+                )
+                .map_err(|e| format!("Qwen3.5 generate failed: {e}"));
+            }
+
+                // CPU path — create fresh OwnedQuantizedModel from cached or fresh mapped
+                let model = OwnedQuantizedModel::from_mapped(mapped)
+                    .map_err(|e| format!("Failed to create GGUF model: {e}"))?;
+
+                // APR-TRACE-001: Use traced generation when --trace is enabled
+                if config.trace {
+                    use realizar::{InferenceTracer, ModelInfo, TraceConfig};
+
+                    let trace_config = TraceConfig {
+                        enabled: true,
+                        verbose: false,
+                        output: config.trace_output.clone(),
+                        ..Default::default()
+                    };
+
+                    let mut tracer = InferenceTracer::new(trace_config);
+                    tracer.set_model_info(ModelInfo {
+                        name: "GGUF Model (CPU)".to_string(),
+                        num_layers: model.config().num_layers,
+                        hidden_dim: model.config().hidden_dim,
+                        vocab_size: model.config().vocab_size,
+                        num_heads: model.config().num_heads,
+                        quant_type: None,
+                    });
+
+                    eprintln!("Warning: CPU traced generation not implemented, using non-traced path");
+
+                    let result = model
+                        .generate_with_cache(prompt_tokens, gen_config)
+                        .map_err(|e| format!("GGUF generate failed: {e}"))?;
+
+                    if let Err(e) = tracer.write_output() {
+                        eprintln!("Warning: Failed to write trace output: {e}");
+                    }
+
+                    Ok(result)
+                } else {
+                    model
+                        .generate_with_cache(prompt_tokens, gen_config)
+                        .map_err(|e| format!("GGUF generate failed: {e}"))
+                }
+        }
+
         fn generate_apr(
             &mut self,
             prompt: &[u32],

crates/apr-cli/src/commands/chat_load_tokenizers.rs

@@ -137,6 +137,13 @@ fn try_init_gguf_cuda(
     mapped: &realizar::gguf::MappedGGUFModel,
 ) -> Result<(Option<realizar::gguf::OwnedQuantizedModelCuda>, bool), crate::error::CliError> {
     use realizar::gguf::{OwnedQuantizedModel, OwnedQuantizedModelCuda};
+    // #3091: Qwen3.5/Qwen3.8 hybrids have a CPU forward but no GPU one yet (#3090). Skip the
+    // CUDA attempt instead of failing it, so chat does not report a load error for a model
+    // it can run.
+    if mapped.model.architecture() == Some("qwen35") {
+        eprintln!("[qwen35: Gated DeltaNet runs on the CPU; the GPU backend does not implement it yet (#3090)]");
+        return Ok((None, false));
+    }
     if !OwnedQuantizedModelCuda::is_available() {
         return Ok((None, false));
     }

crates/aprender-serve/examples/qwen35_parity.rs

@@ -0,0 +1,188 @@
+//! Qwen3.5 CPU parity against llama.cpp (#3091): greedy free-running and teacher-forced.
+//!
+//! Reads `PROMPT_TOKENS:` / `OUTPUT_TOKENS:` pairs that llama.cpp master produced greedily
+//! from the evidence file, runs the same prompts through realizar's Qwen3.5 CPU forward, and
+//! writes `parity.json` next to the evidence file.
+//!
+//! Gate: at every teacher-forced step llama.cpp's token must be realizar's argmax, or a
+//! near-tie, meaning realizar's rank 2 with a logit gap of at most `QWEN35_PARITY_TAU`
+//! (default 0.25). Exact greedy equality between two backends with different accumulation
+//! precision is a coin flip at a near-tie (#2359), so the gaps are recorded, never hidden.
+//!
+//! Usage: `cargo run --release -p aprender-serve --example qwen35_parity -- <model.gguf> [tokens.txt]`
+
+use realizar::gguf::forward_qwen35::{Qwen35Model, Qwen35State};
+use realizar::gguf::MappedGGUFModel;
+use serde::Serialize;
+use std::io::{BufRead, BufReader};
+use std::path::Path;
+
+#[derive(Serialize)]
+struct Disagreement {
+    step: usize,
+    llama: u32,
+    realizar: u32,
+    gap: f32,
+    rank: usize,
+}
+
+#[derive(Serialize)]
+struct PromptParity {
+    prompt_len: usize,
+    llama_tokens: Vec<u32>,
+    greedy_tokens: Vec<u32>,
+    greedy_divergence: Option<usize>,
+    teacher_forced_agree: usize,
+    teacher_forced_steps: usize,
+    disagreements: Vec<Disagreement>,
+    min_agreeing_margin: f32,
+}
+
+#[derive(Serialize)]
+struct Report {
+    model: String,
+    tau: f32,
+    pass: bool,
+    prompts: Vec<PromptParity>,
+}
+
+/// (argmax, best logit, second-best logit)
+fn top2(logits: &[f32]) -> (u32, f32, f32) {
+    let (mut best, mut best_v, mut second) = (0usize, f32::MIN, f32::MIN);
+    for (j, &v) in logits.iter().enumerate() {
+        if v > best_v {
+            second = best_v;
+            best = j;
+            best_v = v;
+        } else if v > second {
+            second = v;
+        }
+    }
+    (u32::try_from(best).unwrap_or(u32::MAX), best_v, second)
+}
+
+fn read_pairs(path: &Path) -> std::io::Result<Vec<(Vec<u32>, Vec<u32>)>> {
+    let parse = |s: &str| {
+        s.split_whitespace()
+            .filter_map(|t| t.parse::<u32>().ok())
+            .collect::<Vec<_>>()
+    };
+    let (mut prompts, mut outputs) = (Vec::new(), Vec::new());
+    for line in BufReader::new(std::fs::File::open(path)?).lines() {
+        let line = line?;
+        if let Some(rest) = line.strip_prefix("PROMPT_TOKENS:") {
+            prompts.push(parse(rest));
+        } else if let Some(rest) = line.strip_prefix("OUTPUT_TOKENS:") {
+            outputs.push(parse(rest));
+        }
+    }
+    Ok(prompts.into_iter().zip(outputs).collect())
+}
+
+fn main() -> Result<(), Box<dyn std::error::Error>> {
+    let mut args = std::env::args().skip(1);
+    let model_path = args
+        .next()
+        .ok_or("usage: qwen35_parity <model.gguf> [tokens.txt]")?;
+    let tokens_path = args
+        .next()
+        .unwrap_or_else(|| "evidence/parity/qwen35/lambda/llama_tokens.txt".to_string());
+    let tau: f32 = std::env::var("QWEN35_PARITY_TAU")
+        .ok()
+        .and_then(|v| v.parse().ok())
+        .unwrap_or(0.25);
+
+    let mapped = MappedGGUFModel::from_path(&model_path)?;
+    let base = Qwen35Model::create_base_model(&mapped.model, mapped.data())?;
+    let qwen = Qwen35Model::from_model_and_layers(&base, &mapped.model, mapped.data())?;
+    let new_state = |max_seq_len: usize| qwen.new_state(max_seq_len);
+
+    let mut prompts = Vec::new();
+    for (prompt, want) in read_pairs(Path::new(&tokens_path))? {
+        let steps = want.len().min(32);
+        let prefill = |state: &mut Qwen35State| -> realizar::error::Result<Vec<f32>> {
+            let mut logits = Vec::new();
+            for (pos, &token) in prompt.iter().enumerate() {
+                logits = qwen.forward_single_qwen35(token, state, pos)?;
+            }
+            Ok(logits)
+        };
+
+        // Free-running greedy: realizar feeds back its own argmax.
+        let mut state = new_state(prompt.len() + steps + 1);
+        let mut logits = prefill(&mut state)?;
+        let mut greedy = Vec::with_capacity(steps);
+        for i in 0..steps {
+            let (next, _, _) = top2(&logits);
+            greedy.push(next);
+            if i + 1 < steps {
+                logits = qwen.forward_single_qwen35(next, &mut state, prompt.len() + i)?;
+            }
+        }
+        let greedy_divergence = greedy.iter().zip(&want).position(|(a, b)| a != b);
+
+        // Teacher-forced: realizar is fed llama.cpp's tokens, so every step is judged.
+        let mut state = new_state(prompt.len() + steps + 1);
+        let mut logits = prefill(&mut state)?;
+        let (mut agree, mut min_margin, mut disagreements) = (0usize, f32::MAX, Vec::new());
+        for (i, &llama) in want.iter().take(steps).enumerate() {
+            let (best, best_v, second) = top2(&logits);
+            if best == llama {
+                agree += 1;
+                min_margin = min_margin.min(best_v - second);
+            } else {
+                let llama_v = logits.get(llama as usize).copied().unwrap_or(f32::MIN);
+                let rank = logits.iter().filter(|&&v| v > llama_v).count() + 1;
+                disagreements.push(Disagreement {
+                    step: i,
+                    llama,
+                    realizar: best,
+                    gap: best_v - llama_v,
+                    rank,
+                });
+            }
+            if i + 1 < steps {
+                logits = qwen.forward_single_qwen35(llama, &mut state, prompt.len() + i)?;
+            }
+        }
+        println!(
+            "prompt {} ({} tokens): greedy divergence {:?}; teacher-forced {agree}/{steps}; disagreements {:?}",
+            prompts.len(),
+            prompt.len(),
+            greedy_divergence,
+            disagreements.iter().map(|d| (d.step, d.rank, d.gap)).collect::<Vec<_>>()
+        );
+        prompts.push(PromptParity {
+            prompt_len: prompt.len(),
+            llama_tokens: want[..steps].to_vec(),
+            greedy_tokens: greedy,
+            greedy_divergence,
+            teacher_forced_agree: agree,
+            teacher_forced_steps: steps,
+            disagreements,
+            min_agreeing_margin: min_margin,
+        });
+    }
+
+    let pass = !prompts.is_empty()
+        && prompts
+            .iter()
+            .all(|p| p.disagreements.iter().all(|d| d.rank <= 2 && d.gap <= tau));
+    let report = Report {
+        model: model_path,
+        tau,
+        pass,
+        prompts,
+    };
+    let out = Path::new(&tokens_path).with_file_name("parity.json");
+    std::fs::write(&out, serde_json::to_string_pretty(&report)?)?;
+    println!(
+        "{} (tau {tau}); wrote {}",
+        if pass { "PASS" } else { "FAIL" },
+        out.display()
+    );
+    if !pass {
+        std::process::exit(1);
+    }
+    Ok(())
+}