DSpark: bitwise first-divergence diagnostics for batched vs sequential decode

[raveonetter]

Problem

DSpark's generic batched verifier and ordinary sequential decode implement the same mathematical model, but they do not necessarily implement the same floating-point state transition.

Let ordinary sequential decode be

$$S_{t+1}=F_{\mathrm{seq}}(S_t,x_t),$$

and the generic batched verifier be

$$\tilde S_{t+1}=F_{\mathrm{gen}}(\tilde S_t,x_t).$$

The experiment forces both executions to start from the same true state and consume the same token sequence:

$$S_0=\tilde S_0,\qquad x_t=\tilde x_t.$$

For strict replay-free greedy identity, matching the currently accepted argmax is weaker than what is actually required. All future-visible state must remain canonical:

$$F_{\mathrm{gen}}(S,x)=F_{\mathrm{seq}}(S,x)$$

bitwise for every state component that can affect future decode.

This diagnostic framework locates the earliest point where that equality breaks.

Method

The core experiment is:

same true S0
→ Pass A: generic batched verifier
→ same-stream GPU snapshots
→ restore full S0
→ Pass B: ordinary sequential decode
→ force the exact same proposal token IDs
→ GPU completion
→ CPU raw-bit comparison
→ report earliest divergence

Probe non-perturbation is separately gated:

C2B_CONTROL A0_vs_A1 PASS
C2B_PROBE A0_vs_A2 PASS
C2B_RESULT PASS

No synchronous GPU→CPU reads are inserted inside the layer loop. Snapshot copies remain GPU→GPU, and CPU comparison happens only after GPU completion.

The reporter records the first mismatching row/layer/checkpoint/subobject plus mismatch count, first differing bits, absolute/relative/ULP metrics, RMS error, relative L2, cosine similarity, and sign distribution.

The diagnostic chain is:

operator-level numerical identity
→ future-visible state identity
→ logit identity
→ greedy-token identity
→ final byte identity

Output-level tests observe only the end of this chain. This framework identifies where it first breaks.

Proven arithmetic family 1: Q8_0 batched-ext MV vs single MV

The original earliest divergence was layer 0 / row 0 at the Q_A projection, while the normalized attention input was bitwise exact.

Same-input/same-weight isolated A/B proved numerical non-equivalence between:

generic:
kernel_mul_mv_ext_q8_0_f32_r1

sequential:
kernel_mul_mv_q8_0_f32

Representative Q_A result:

elements=1024
mismatch_count=823
mismatch_fraction=0.8037109375
max_abs=5.2154064178466797e-08
rms_abs=1.1096596329135279e-08
relative_l2=1.6302470259513109e-07
cosine_similarity=0.99999999999998823

After diagnostic canonicalization of Q_A, the first divergence moved to raw KV projection. KV reproduced the same primitive-family mismatch:

elements=512
mismatch_count=431
mismatch_fraction=0.841796875
max_abs=4.4703483581542969e-08
rms_abs=1.2926741589862414e-08
relative_l2=1.5454367931804077e-07
cosine_similarity=0.99999999999998945

Further localization showed that Q_B belongs to the same family.

Current adjudication:

FAMILY_Q8_0_BATCH_EXT_VS_SINGLE_MV
sites=QA,KV,QB
status=PROVEN

Three divergent semantic sites therefore collapse to one underlying arithmetic family.

Proven arithmetic family 2: FlashAttention batch-direct vs single vec+reduce

After canonicalizing the Q8_0 projection family, the next independent divergence was localized to raw attention-head output.

generic:
kernel_flash_attn_ext_f16_dk512_dv512

sequential:
kernel_flash_attn_ext_vec_f16_dk512_dv512

• kernel_flash_attn_reduce

This defines:

FAMILY_FLASH_ATTN_BATCH_DIRECT_VS_SINGLE_VEC_REDUCE

After diagnostic canonicalization:

CP4-HEADS-RAW EXACT
CP4-HEADS EXACT

so inverse RoPE does not introduce another independent drift source.

The first divergence then moves to:

CP4 / after_attn_hc

Canonicalizing the FlashAttention family reduces downstream CP4 RMS and relative-L2 error by about 54%, proving a causal contribution to the later hidden-state drift.

Partial arithmetic family 3: attention output / HC tail

The next interval is asymmetric/fused between the real generic and sequential execution paths, so the online checkpoint sweep intentionally stops rather than splitting fusion or manufacturing a comparison tensor.

An isolated same-input tail A/B proves arithmetic non-equivalence for:

FAMILY_Q8_ATTN_OUTPUT_BATCH_F32_HC_SPLIT_VS_SINGLE_F32_FUSED_HC

and a diagnostic substitution proves causal contribution to CP4 drift.

However, it does not completely explain CP4:

isolated sequential_bits = 0xbb9ce2ac
runtime after substitution = 0xbb9ce2ac
Pass B expected_bits = 0xbb9ce2ad

The substitution is demonstrably active, but the isolated sequential tail is still not numerically identical to the true fused sequential runtime context.

Measured reduction after substitution:

mismatch: 4561 → 1776 (-61.1%)
max_abs: 3.73e-8 → 7.45e-9
RMS: 4.12e-9 → 5.67e-10
relative L2: 1.65e-7 → 2.26e-8
max ULP: 15656 → 728

Formal status:

arithmetic_non_equivalence = PROVEN_BY_TEST
causal_contribution = PROVEN_BY_TEST
complete_CP4_explanation = UNKNOWN

The first divergence remains:

CP4 / after_attn_hc

Current interpretation

The observed numerical drift is deterministic and structured by arithmetic family rather than appearing as unrelated noise everywhere:

FAMILY 1
FAMILY_Q8_0_BATCH_EXT_VS_SINGLE_MV
sites=QA,KV,QB
status=PROVEN

FAMILY 2
FAMILY_FLASH_ATTN_BATCH_DIRECT_VS_SINGLE_VEC_REDUCE
site=CP4-HEADS-RAW
status=PROVEN

FAMILY 3
FAMILY_Q8_ATTN_OUTPUT_BATCH_F32_HC_SPLIT_VS_SINGLE_F32_FUSED_HC
site=CP4
status=PARTIAL_CAUSAL_CONTRIBUTION
complete_attribution=UNKNOWN

The reporter terminology should reflect the distinction between fully crossed first-divergence sources and partial causal contributors:

sources_tested=5
sources_fully_canonicalized=4
partial_causal_families=1
first_divergence=CP4/after_attn_hc

sources_exposed=5 is too strong because the fifth tested family does not move the first-divergence frontier.

Optimization question

Let $\mathcal C$ be the set of arithmetic families replaced with canonical sequential-equivalent arithmetic.

The research objective is to find a small set $\mathcal C_{\min}$ such that

$$F_{\mathcal C_{\min}}(S,x)=F_{\mathrm{seq}}(S,x)$$

for all future-visible state needed for strict greedy identity, while keeping

$$C(\mathcal C_{\min}) \ll C_{\mathrm{full\ replay}}.$$

Equivalently:

Find the smallest set of numerical semantic differences between batched verification and sequential decode such that selectively replacing those arithmetic families causes the two floating-point state trajectories to coincide again.

If only a small number of reusable arithmetic families require canonicalization, strict replay-free speculative decode may be practical.

If the required set expands across many unrelated kernels, selective exactification may approach ordinary decode cost and lose its performance advantage.

Non-goals

This draft does not yet:

remove replay;

directly commit generic verifier state in strict mode;

change DSpark's default correctness contract;

optimize the affected Metal kernels;

claim that CP4 is fully attributed;

claim that the current canonicalization set is minimal;

propose the experimental per-family substitutions as production code.

The immediate purpose is to make numerical state divergence observable and causally testable.

Next steps

Complete source-level analysis of the fused CP4-HEADS → after_attn_hc tail without perturbing the real execution topology.

Reconstruct the true sequential fused-tail numerical context closely enough to explain the remaining CP4 residual, or explicitly classify it as an atomic repair boundary if finer equivalence cannot be established safely.

Continue the first-divergence sweep only after CP4 is made exact, until a sufficient canonicalization set is found or arithmetic-family spread becomes too broad.

Replace site-specific diagnostic substitutions with family-level prototypes.

Perform reverse ablation only after a sufficient set is found, to estimate the minimal repair set.

Compare selective repair against full replay and the no-replay fast-commit performance ceiling.

Only after strict state identity is demonstrated, run long free-running byte-identity and throughput validation.

[Copilot]

Pull request overview

This PR adds the low-level infrastructure and model-free tests needed to perform bitwise “first-divergence” diagnostics between DSpark’s batched verifier path and the canonical sequential decode path, with a strict GPU→GPU snapshot transport path on Metal and a CPU-side exact float comparator for reporting.

Changes:

• Introduces a CPU-only IEEE-754 binary32 exact comparator (ds4_float_compare) and unit tests.
• Adds a generic first-divergence capture/reporting layer (first_divergence_capture) plus a unit test that validates ordering/tracing behavior.
• Implements ds4_gpu_tensor_copy_f32_inline() (strict same-compute-encoder copy on Metal; linkage-compatible fallback on CUDA/ROCm) and a Metal regression test to ensure raw-bit preservation across edge bit patterns.

Reviewed changes

Copilot reviewed 44 out of 45 changed files in this pull request and generated no comments.

Show a summary per file

File	Description
tests/test_metal_f32_inline_copy.c	Model-free Metal regression test for strict inline F32 checkpoint copy bit-preservation and encoder reuse.
tests/test_float_compare.c	Unit tests for the new CPU float bit-exact comparator behavior (NaNs, infinities, signed zero, ULP, etc.).
tests/test_first_divergence.c	Unit test for first-divergence capture/report ordering and trace emitters.
skill/test_exact_rows_contract_template.c	Scaffold for a future exact-row kernel contract test (currently an intentional skip).
skill/TASK_BEFORE_GGUF.md	DSpark investigation checklist / handoff guidance.
skill/PROGRESS-P1.md	Investigation progress log and collected notes.
skill/PROGRESS-P0.md	Initial skill/handoff archiving progress notes.
skill/PROBE-P2-DESIGN.md	Design document for a runtime first-divergence probe integration plan.
skill/PROBE-P2-AUDIT.md	Audit notes on S0 restoration and probe integration constraints.
skill/PR_REFERENCE_NOTES.md	Historical PR reference notes relevant to DSpark exactness work.
skill/PLAN-ds4-investigation.md	Multi-phase investigation plan and gates.
skill/hy_locate_dspark_paths.sh	Helper script to locate DSpark-related symbols in ds4.c.
skill/HY_HANDOFF.md	Handoff doc describing pre-GGUF work and constraints.
skill/hy_extract_dspark_context.py	Helper script to generate an offline symbol/context map from ds4.c.
skill/hy_dspark_supplement/TASK_BEFORE_GGUF.md	Supplemental copy of the pre-GGUF task list.
skill/hy_dspark_supplement/hy_locate_dspark_paths.sh	Supplemental copy of the symbol-locate helper script.
skill/hy_dspark_supplement/hy_extract_dspark_context.py	Supplemental copy of the offline context extractor script.
skill/hy_dspark_supplement/EMPIRICAL_FACTS.md	Supplemental empirical performance/behavior context notes.
skill/hy_dspark_supplement/CURRENT_MAIN_REFERENCE.md	Supplemental notes about current-main reference points.
skill/FIRST-DIVERGENCE-EXPERIMENT-SPEC-V1.md	Frozen experiment specification for the first-divergence framework.
skill/EMPIRICAL_FACTS.md	Empirical performance/behavior context notes.
skill/ds4_exactness_probe.h	Probe helper header (skill bundle) for tensor comparison/printing.
skill/ds4_exactness_probe.c	Probe helper implementation (skill bundle) for chunked tensor comparisons.
skill/CURRENT_MAIN_REFERENCE.md	Notes on current-main reference code paths and exact-row primitives.
skill/CODEX-QA-PRIMITIVE-ROOT-CAUSE.md	Writeup of QA primitive A/B evidence and canonicalization approach.
skill/CODEX-Q-PROJECTION-DIVERGENCE-LOCALIZATION.md	Writeup localizing divergence to the first Q projection output boundary.
skill/CODEX-P2-C0-AUDIT.md	Static re-audit notes/gates for the diagnostic probe design.
skill/CODEX-CANONICALIZATION-SWEEP.md	Plan/results writeup for composable canonicalization sweeps.
skill/CODEX-C4-C5-IMPLEMENTATION-NOTE.md	Implementation note for forced-token Pass B + comparison/reporting.
skill/CODEX-C2B-IMPLEMENTATION-NOTE.md	Implementation note for Pass-A capture and non-perturbation gate.
skill/CODEX-C2B-HANDOFF.md	Handoff doc for implementing the C2b gate.
rocm/ds4_rocm_runtime.cuh	Adds ROCm-side linkage-compatible ds4_gpu_tensor_copy_f32_inline() implementation.
Makefile	Wires in new comparator + first-divergence objects, adds test targets, and uses non-fast-math flags for comparison code.
first_divergence_capture.h	Declares capture, report, and trace APIs for first-divergence diagnostics.
first_divergence_capture.c	Implements capture storage, ordering, CPU comparisons, and trace/report emitters.
ds4_metal.m	Implements strict Metal ds4_gpu_tensor_copy_f32_inline() using the cached compute encoder (no blit fallback).
ds4_gpu.h	Declares ds4_gpu_tensor_copy_f32_inline() and documents its strict semantics.
ds4_float_compare.h	Declares CPU-only exact float comparison API + result structure.
ds4_float_compare.c	Implements IEEE-754 binary32 exact comparison + metrics and ULP distance logic.
ds4_cuda.cu	Adds CUDA-side linkage-compatible ds4_gpu_tensor_copy_f32_inline() implementation.
AGENTS.md	Adds/updates the DSpark exactness investigation operational contract.
.claude/claude.md	Agent workflow and investigation/implementation rules documentation.
.claude/AGENT.md	Repository-specific agent notes and testing guidance.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[Copilot]

Pull request overview

Copilot reviewed 44 out of 45 changed files in this pull request and generated no new comments.

Suppressed comments (1)

Makefile:446

• The aggregate test target builds and runs tests/test_first_divergence but never runs tests/test_float_compare, even though the dedicated test-float-compare target and its edge-case suite (NaN payloads, infinities, signed zero, subnormal ULP distances) were added in this PR. Other unit tests (test_layer_pack, test_engine_mgpu_placement, test_gpu_args, test_first_divergence) are all wired into make test, so the foundational ds4_float_compare comparator is the only new module whose dedicated tests won't run in a standard make test. Since it is a pure-CPU, cross-platform suite, consider adding it here so its behavior is exercised in CI. (Optional / minor.)

test: ds4_test ds4_agent_test ds4-eval q4k-dot-test mxfp4-dot-test \
	tests/test_first_divergence tests/test_layer_pack tests/test_engine_mgpu_placement tests/test_gpu_args \
	$(SAMPLING_TEST) ds4 ds4-server ds4-bench ds4-agent
	./tests/test_first_divergence

[Flor1an-B]

Complementary angle from #756, in case cross-referencing is useful.

This PR localizes the earliest bitwise point where F_gen(S,x) and F_seq(S,x) diverge — the strong, future-visible-state requirement. #756 comes at the same phenomenon from the surface: it teacher-forces the committed speculative stream back through ordinary decode and reports the rate + severity histogram of greedy-token divergence (committed token ≠ autoregressive argmax) over real generations. So they're the white-box (where/why the state first breaks) and black-box (how often the output greedy token actually flips, and by how much) views of the same thing.

Your point that argmax-match is weaker than bitwise state identity is exactly right — #756 deliberately measures only the visible greedy consequence, so its rate is a lower bound on the underlying state divergence you localize.

A concrete surface data point that might help correlate. On current main (84cc882), after 0e89a0e "commit accepted verifier state directly" removed the replay-through-ordinary-decode, the surface divergence becomes non-zero and path-dependent (M5 Max, Metal, same 1024-token open-ended prompt):

path	divergence	worst gap	histogram (≤0.1 / ≤0.5 / ≤2.0 / >2.0)
DSpark	31/1024 (3.03%)	1.363	12 / 15 / 4 / 0
MTP (draft=4, generic verifier)	24/1024 (2.34%)	1.010	10 / 12 / 2 / 0

Both are entirely sub-catastrophic (< 2.0), so the existing worst_gap ≤ 2.0 acceptance-depth check still reports clean. DSpark was 0/1024 before 0e89a0e — the replay was silently correcting it — so that ~3% is presumably the state divergence your framework would now localize as reaching the output. Happy to run the #756 instrument against a specific prompt/seed if a matched surface-vs-bitwise comparison is useful.