Tighten CollectiveSpec system research gates

docs/collectivespec-pilot-design-20260713.md

@@ -155,3 +155,48 @@ collective ordinal 相同；若最后仍 padding 到 global max，就没有可
   做任何大实现前进行逐项复现/排除。
 - trace 的 `sampling_u` 是 proxy；最终结论必须在固定 arrival trace、真实请求长度和
   至少一个不同 workload 上复现。
+
+## 2026-07-13 系统重审：收紧主张和后续 gate
+
+本轮查阅 [vLLM Dynamic SD 限制](https://docs.vllm.ai/en/latest/features/speculative_decoding/dynamic_speculative_decoding/)
+与 [DSpark](https://arxiv.org/abs/2607.05147) 后，原先“dynamic K 会使 collective
+diverge，因此做 ragged verifier”这一表述太宽，不能作为实现前提：
+
+- DSpark 已公开主张按请求动态 verification length、跨请求 token flatten 与 ragged
+  physical execution；这些本身不再构成新颖性。
+- dash0 当前实际 import 的 vLLM wheel 与本地 checkout 不同。实验中的运行日志称
+  `v0.11.1`，而 wheel metadata 为 `0.13.0rc2.dev2111+gb44b43f43.d20260309`；后续任何
+  hook 必须对这个 live source 做 provenance pin，不能把本地 v0.24 API 当作证据。
+- 这个 live runtime 已原生使用 per-request `list[list[int]]` draft token IDs，并将真实
+  长度送入 scheduler/metadata；EP all-to-all 也具有 variable-split data path。因此
+  **per-request horizon 不等于 collective divergence**。必须先观测到不同 DP replica
+  的 collective call count、phase 或 branch trace 的真实不一致。
+
+修订后的唯一可能研究命题是更窄的：
+
+> 对共享一个 EP collective domain 的独立 DP scheduler，如何将异构 verification plan
+> 编译为可证明 liveness 的 canonical execution trace，同时在同一逻辑 plan 下回收
+> global physical-max padding 的关键路径成本。
+
+它有四个顺序严格的停止门槛：
+
+1. **P0 / 真实 premise**：以预先给定的 `k_i ∈ {0,1,2,3}` replay 表截断已生成的
+   EAGLE candidates，在每个 DP/TP rank 记录 target、EAGLE 和 EP phase signature。若
+   没有 trace mismatch、强制 global padding 或 liveness 问题，就停止把 plan header 当作
+   研究贡献。
+2. **P1 / 机会量**：即使存在 mismatch，也必须证明 rank-local oracle 相对 best static
+   或 globally synchronized K 有至少 10% 的 SLO-goodput headroom；全局同步若恢复 90%
+   以上 gap，则只值得做 upstream patch。
+3. **P2 / 因果物理对照**：同一个 `k_i` replay plan 必须对比
+   `PaddedSync-semantic`（物理 `N × (1 + max k_i)` rows）与 `CompactSync`
+   （物理 `Σ_i(1+k_i)` rows）。static K=3 不是 PaddedSync，因为二者 logical algorithm
+   不同。若实际 target/EP work 与关键路径未减少，停止。
+4. **P3 / 正确性与部署**：所有 TP peers 的 plan digest 相同、所有 EP ranks 观察到同一
+   header vector、每 epoch 的 target/EAGLE/MoE signature 一致；greedy output token-exact，
+   并通过 empty-rank、`{0,3}` 交替、长时间 stress。只有随后在两个 session-coherent
+   workload 上重现 SLO-goodput 才能讨论论文。
+
+若 P0--P3 任一项失败，合理结论是停止 CollectiveSpec，而不是继续调 controller、K 或
+queue policy。若全部通过，最小原型的边界也只应是 verifier-side compaction：当前
+EAGLE 仍按 Kmax 产生 candidate，短 `k_i` 不会自动消除 draft-side work，不能把 verifier
+节省误报为完整 draft+verify speedup。