DS4Server/docs/issue109-verify-gate/README.md

Issue 109: compiled verification gates

Qwen target forwards inside the MTP loop now carry the pinned MTPLX decode_verify phase through attention, eager HC injection, captured-prefix repair and final-primary commit. Draft/history and ordinary prefill/AR retain their existing phase. Compiled layer replay keys include the phase to prevent reuse of a graph with the other gate law.

The BF16 attention gate compiles exactly output * sigmoid(gate.astype(f32).astype(bf16)); the casts select the fused lowering and do not move the sigmoid to F32. F32 uses its separate compiled expression; FP16 remains standalone. The existing native Rust graph compiler and Metal execution implement these expressions. No global sigmoid, compiler math flags, DS4/GLM implementation, or shared family helper changed.

Two actual eager GatedResidual._verify_inject calls also demonstrated a phase/site failure (the adjacent active-hc-sites.jsonl records inputs and both outputs). That sibling therefore satisfies this issue's explicit scope rule: its verify-only divide/sigmoid/multiply now compiles as pinned MTPLX does. Unrelated PLE/shared-expert gates remain unchanged. This is oracle parity, not a new DS4Server feature or a full fixed-M4 verifier.

Persisted MTP snapshots without the new gate policy are rejected before restoration; old AR snapshots remain compatible. Tests use both a constructed old manifest and an actual pre-fix MTP file, and verify failed restoration leaves the current live state intact. New checkpoints reproduce resident warm state exactly after reset/reopen.

Verification and boundaries

The pinned oracle is MTPLX 9882703f3105363ddc37eca9f97aa09a1d387112 with MLX 0.32.2. The installed Bare-Speed artifact and hardware are recorded in ../issue104-ar/environment.json.

• Exhaustive finite BF16 (65,280) and FP16 (63,488), plus 65,536 dense F32 gate values, compare every output byte in all three phases. BF16 also covers all three HC-injection phases. The owned original active_attention_gate and bf16_gate regressions require the corrected expression and neighbors.
• Real cold/warm MTP requests compare each target forward's input IDs and all logits/hidden bytes, generated tokens, cache offsets, final logits/hidden and trunk/MTP state arrays. Native resident and disk-reopened full state hashes must agree exactly.
• The complete final-primary test covers greedy/sampled, depths 1–3, stop/max-token termination and failure/cancellation controls.
• Existing whole-attention fixtures exercise both TF32 modes and prepared/lazy input routes; hyper fixtures control the unchanged non-verify route.

The real-model comparison explicitly sets the oracle's MTPLX_QWEN4_VERIFY_SDPA_HEAD_CHUNK=0 to isolate this gate change with the same attention consumer. Independent default-oracle comparison exposed a missing head-chunked consumer before the gate, tracked separately in #113. This controlled run does not establish default-route model parity. default-route-mismatch.jsonl retains the evidence.

Cache receipts retain raw hashes as well as value hashes with zero signs canonicalized. A first-position prefill key has one signed-zero bit difference; this is reported explicitly rather than hidden by a tolerance, and is tracked separately in #114. Target outputs, final logits/hidden and resident-versus-reopened state use raw byte exactness.

All four mandatory gates and serial Metal/oracle checks are listed in checks.json. These are correctness receipts, not performance measurements.

Reproduction

local-eval-results/mtplx-reference-env-0.32.2/bin/python \
  tools/issue109-gate-reference.py /path/to/pinned/mtplx /tmp/issue109-gate
cargo test --all-features --bin ds4-server --no-run
cargo build --bin test-supervisor
export DS4_ISSUE109_GATE=/tmp/issue109-gate
# Resolve TEST_EXECUTABLE from cargo; run Metal processes serially.
target/debug/test-supervisor 4096 60 120 --command TEST_EXECUTABLE \
  issue109_gate_phase_and_dtype_laws --ignored --nocapture --test-threads=1
export MTPLX_CONTEXT_COPY=0
export DS4_QWEN38_ARTIFACTS=/path/to/model
export DS4_ISSUE109_DIR=/tmp/issue109-product
export DS4_ISSUE109_OLD=/path/to/pre-fix-mtp-checkpoint
target/debug/test-supervisor 114688 60 120 --command TEST_EXECUTABLE \
  issue109_verify_rows_and_warm_checkpoint --ignored --nocapture --test-threads=1
MTPLX_QWEN4_VERIFY_SDPA_HEAD_CHUNK=0 \
  local-eval-results/mtplx-reference-env-0.32.2/bin/python \
  tools/issue109-model-reference.py /path/to/pinned/mtplx \
  "$DS4_QWEN38_ARTIFACTS" "$DS4_ISSUE109_DIR" /tmp/issue109-model-oracle

Snapshot comparison correction (#114)

The historical zero-sign receipt above measured an extra deep oracle snapshot against a lazy native bank entry. The deep clone adds zero; this alone creates the reported bit change. The raw/live and matching lazy snapshots agree exactly. The corrected shared oracle now compares the server's actual snapshot stages, requires every raw cache bit to match, and has no signed-zero exception. See the isolated trace and regression. The original receipts remain unchanged as evidence of the measurement error.