d8_verify に cross-impl-drift claim 追加

緑完全停止 — TS vs Verilog snapshot、 差分検出時 fail 固定
STEP 1779 · 2026-09-06 · commit e35c4de35

目的

STEP 1776 で d8_verify payload の 誤 label は 訂正済 (source: 'ts-side-self-check-only' 等)、 但し tool は 依然 allChecksPass: true を 返し続けていた。 「読まれずに 信用される tool の 緑」 が 消えていなかった。

本 STEP で 新 claim cross-impl-drift を 追加、 TS seven-logic vs Verilog dfumt8_alu.v の baked snapshot を 全 136 entry 比較、 80 divergence を 初めて 実測検出、 d8Verify('all') = matchCount: 6/7, allChecksPass: false 固定 で 藤本さん hard constraint 「defer 中も tool が 緑を返さないように」 完全実現。

藤本さん hard discipline 5 全対応

指示 (turn 4-5)実装
差分検出時 match=false 固定 checkCrossImplDrift() = totalDiffs === 0 の 場合のみ true
「expected 扱い」 禁止 = structural gate test assert(c.match === false)、 未来 update は 明示 STEP + test 併修正 必須
差分の 件数と 分類を 出力 totalDiffs + fourValueSubsetDiffs: 12 (bilattice-order-diagnosed) + eightValueExtensionDiffs: 68 (undiagnosed)
tableProvenance 常時出力 + snapshot 明示 5 field: bakedFromCommit/bakedFromDumpJson/bakeDate/currentVerilogNotCompared: true/warning
Sample 選び方 決め打ち固定 Sort by (op, a, b) → 4-value 4 + 8-value 6 = 10 deterministic sample、 test で 分類バランス gate

「緑を止める」 具体形

d8Verify('all'):
  allChecksPass: false    ← STEP 1776 では true だった (STEP 1778 訂正で 明示)
  matchCount: 6/7
  checks[6] (cross-impl-drift):
    match: false
    actual: "80/136 entries differ from baked Verilog snapshot
             (12 in 4-value subset [bilattice-order-diagnosed],
              68 in 8-value extensions [undiagnosed])"
    detail:
      totalDiffs: 80
      fourValueSubsetDiffs: 12
      eightValueExtensionDiffs: 68
      sampleDiffs: [ ... 10 deterministic entries ... ]
      tableProvenance:
        bakedFromCommit: "c0256729e"
        currentVerilogNotCompared: true    ← 常に true (「照合していない」 明示)
        warning: "⚠ This VERILOG_*_TABLE constant is a SNAPSHOT baked
                   at STEP 1779 from data/verilog/dfumt8_alu.v..."

MCP 経由 consumer が allChecksPass を 単独読みしただけで 緑 が 出ない state。 藤本さん の 「読まれずに信用される tool の 緑」 の 危険が 消失。

Discovery — STEP 1772 audit の 78 → 80 訂正

「照合していないのに 照合していると 名乗る」 pattern の 実例

実装中に f4 tab の dump_verilog_tables.py line 59-60 で NOT table を hardcode (seven-logic 一致 shortcut、 「matches Verilog」 コメント付き) している事実を 検出。

実 Verilog line 85-86 は: 

DFUMT8_ZERO:    not_result = DFUMT8_INFINITY;
DFUMT8_INFINITY:not_result = DFUMT8_ZERO;

= ZERO ↔ INFINITY swap (自己双対でなく 極性反転) → STEP 1772 audit の 78 は NOT-side に 2 undercount、 実 total 80。 4-value 12 不変、 8-value 66 → 68。

tableProvenance.step1772AuditDiscrepancyNote field に 恒久記録。

Test 結果

npx tsx test/step1397-d8-fixpoints-verify-test.ts = 194 passed, 0 failed (STEP 1776 baseline 162 + 追加 32 assertion incl. structural gate 2、 Part 11 の 7 claims 対応 + Part 11b の 24 assertion + Part 12 訂正)

Smoke test: cross-impl-drift 単独 = match=false, 80/136 diffs (12 four-value + 68 eight-value); 'all' = allChecksPass=false, matchCount=6/7 = 藤本さん 「緑を止める」 完全実現

使用例

# MCP 経由 (rei-aios v2.8.5+)
d8_verify claim="cross-impl-drift"

# ローカル test
npx tsx test/step1397-d8-fixpoints-verify-test.ts

# Smoke test (a6 tab sidecar)
npx tsx data/tabs/rei-aios-a6/d8-route-d-audit/scratch/smoke_cross_impl_drift.ts

Honest scope

主張しないこと:
  • 66-68 差分 の 「意図的 vs 実装齟齬」 判定 (STEP 1784 で 診断 = 全て 意図的、 別 site 対象)
  • Verilog dfumt8_alu.v が 実装当初 (STEP 1006) から 変わっていない こと (bake は 2026-09-06 snapshot、 現行 .v との 一致 は tool で 保証されない = currentVerilogNotCompared: true)
  • Lean 4 file の 実 theorem 内容 と TS/Verilog の 一致 (Lean 4 file は runtime parse せず、 lean4Reference は 静的 metadata)
  • MCP tool の 外部 consumer の 影響範囲 (payload 変化: 新 claim entry + 'all' の allChecksPass が false 化、 breaking 可能性)

Cross-refs