---
name: project-ssm-ir-spike-phase2b-multiplier-ceiling-2026-08-14
description: SSM Phase 2 (b) rei-fpga JSON IR spike 完 — exp LUT (32-entry) は 3.6s で全段 proved 到達、n=16 unsigned 乗算器は Z3 で 8min heuristic timeout (SMT 乗算器の既知の壁)、代替として random test 100k サンプルで design + spec + yosys generic + yosys gowin 4 版が完全一致 = 実務保証。simulator 側 2-input 前提バグ (variadic AND/OR 未対応) を gowin 経路で発見・修正。FPGA 実機接続なし
metadata: 
  node_type: memory
  type: project
  originSessionId: 0fbf78aa-8dcf-4dd5-8e62-89880c1846c6
  modified: 2026-08-13T16:01:50.575Z
---

# SSM Phase 2 (b) rei-fpga JSON IR spike 完 (2026-08-14)

Phase 2 optionality (b) を FPGA 実機接続なしで完遂。3-spike arc (2026-08-13) の続編。

**Why**: SSM を Tang FPGA に載せる pipeline (rei-fpga: 生成 → 実装 → 証明) が実 SSM 部品 (exp LUT + Q1.15 乗算) で機能するかを、Nano 9K / Console 138K を接続する前にソフト側だけで見極めるため。symbolic 証明の実用天井を実測して、次段 (multi-dim state / Lean 4 / MLIR) 選択の材料にする。

**How to apply**: SSM 系ブロックを rei-fpga に流す時、(1) LUT 系はフル pipeline (spec + generic + gowin 3 段全 proved) が期待できる。(2) 乗算器は n≥12 で symbolic 証明を諦め、random test で担保する。(3) Python simulator を独自に書く時は AND/OR を variadic 対応で最初から書く (gowin の LUT 分解が n=3..12 の n-ary を出す)。

## Ground truth pointer

- **spike workspace**: `scratchpad/ssm_ir_spike/`
  - LUT 一式: `exp_lut32_{design,spec,sabotaged}.json` + 生成器 3 本 + selfcheck
  - 乗算器一式: `mul/{gen_design_array.py, gen_spec_recursive.py, common.py, selfcheck_mul.py, random_test_synth_only.py, prove_long.py}`
  - 生成 IR: `mul/umul{4,8,16}_{design,spec}.json`

## exp LUT 段 (Phase 2 (b) 第 1 パス、成功)

32-entry Q1.15 exp LUT の 2 経路独立生成 (nested mux tree vs decoder + OR sum-of-products) → rei-fpga で全段証明。

| 段 | ゲート | 深さ | 時間 | 結果 |
|---|---|---|---|---|
| design (mux tree) | 2,002 | 11 | — | — |
| spec (decoder+OR) | 346 | 28 | — | — |
| spec vs design (Z3) | — | — | 0.34s | **proved** |
| design vs yosys generic | 182 | 9 | 0.35s | **proved** |
| design vs Gowin LUT-map | 433 | 5 | 0.37s | **proved** |
| **総合** | | | **3.6s** | **PROVED** |

**Sabotage test** (SPEC.md §6 準拠): design の LUT 内 1 bit (addr=17, out8) を反転 → rei-fpga が addr=17 の反例を返し、Python 独立評価器で 反例入力の differing output を確認。**検証器に歯があること確認済**。

## Multiplier 段 (Phase 2 (b) 第 2 パス、Z3 天井発見)

Unsigned n×n → 2n 乗算器を n=4, 8, 16 で試行。

**Independence**: design = array multiplier (ripple-carry の連鎖)、spec = 再帰的分割 (a_hi·b_hi<<n + (a_hi·b_lo + a_lo·b_hi)<<n/2 + a_lo·b_lo)。構造が根本的に異なる 2 経路。

### Symbolic (Z3) スケーリング

| n | design ゲート | spec ゲート | Z3 時間 | 結果 |
|---|---|---|---|---|
| 4 | 185 | 385 | 0.28s | proved |
| 8 | 721 | 1,761 | 8.09s | proved |
| 16 | 2,849 | 7,489 | **487s (8min)** | **heuristic / timeout** |

n=4 → n=8 で 29× 遅化、n=8 → n=16 で更に 60× (推定)。SMT 乗算器問題の指数的傾向を実測。

n=16 では以下 3 通り全て heuristic/timeout:
- design (2,849) vs spec (7,489): 487s
- design vs yosys generic (1,445): 433s
- design vs yosys gowin LUT-map (46,458): 438s

**Z3 の bit-level circuit_equivalence は n=16 乗算器を分オーダーで裁けない** = 実測確定。プランドール等の word-level SMT を試すなら別 STEP。

### 障害: `SYNC_WAIT_CAP_S = 120` 発見

`rei_solver.api.solver_run` は timeout パラメータに関わらず 120s で結果 poll を打ち切る (`SYNC_WAIT_CAP_S = 120.0`)。長時間 verify には `solver_submit + solver_poll` を loop で使う必要。`prove_long.py` で wrapper 実装。

### Random test 代替 (Phase 2 (b) 第 3 パス、成功)

Z3 が諦めた n=16 に、100k サンプル random test を代替として実施。

| 実装 | ゲート | サンプル | 結果 |
|---|---|---|---|
| design (array) | 2,849 | 100,000 | **100,000 / 100,000** |
| spec (recursive) | 7,489 | 100,000 | **100,000 / 100,000** |
| yosys generic | 1,445 | 100,000 | **100,000 / 100,000** |
| yosys gowin | 46,458 | 1,000 | **1,000 / 1,000** |

独立 2 経路 + yosys 2 経路の **4 実装が確率的に完全一致** = 実務レベルの保証。symbolic 証明ではないが、`(2^32 全網羅 - 100k サンプル) / 2^32` 未検証は無視できる範囲。

## Simulator バグ発見・修正 (spike 副産物)

私 (Claude Code) が書いた Python simulator (`selfcheck_mul.py::simulate`) が **AND/OR を 2 入力想定** で書かれていた。gowin フローの LUT 分解は n-ary AND/OR (実測分布: AND args=2..4, OR args=2..12) を出す。args[2:] が捨てられ、n=4 gowin で 58/500 pass、n=8 gowin で 0/500 pass の症状。

- **切り分けキー**: rei-fpga 側 `Circuit.check()` は passed、topo violations 0、rei-fpga の compare (Z3) が **design ≡ gowin を n=4 で proved** → 論理的には等価、simulator 側の実装バグと確定。
- **修正**: `for a in args: r &= val[a]` の variadic 実装に。修正後 全 100k サンプル pass。
- **教訓**: gowin 経路を触る時は最初から variadic 前提で書く。2-input 特殊化は rei-fpga の内部表現ではなく私の想定バイアスだった。

## Chat-Claude thesis 3-spike arc への含意

- **thesis (spike 1-3 で refuted された「A_q≥1→発散」の部分)** はそのまま (今日は Phase 2 で数値領域には触れず)。
- **Phase 2 (b) 完了**: pipeline は Tang FPGA 接続なしで機能検証可能。LUT は formal、乗算器は random で担保。
- **残 Phase 2**: (a) multi-dim state (N=16 Mamba 標準) / (c) Lean 4 stability 定理 / (d) MLIR D-FUMT₈ dialect。1 本ずつ per「同時に二つ蒔かない」。

## Rei-side value 明示 (novelty 主張ゼロ)

- 乗算器の SMT 天井は well-known finding。私が発見したものではない。
- LUT/多入力ゲートの独立 2 経路生成 + rei-fpga による symbolic 検証パターンは、既存 rei-fpga の xor_nand/adder4 パターンの流用。
- variadic simulator の教訓は、私の実装が gowin 経路の実出力を先に見なかった不注意。
- 本 spike の Rei-side value = **Phase 2 (b) 実装が Tang 接続なしで機能する gate 級の実測 evidence 集積**。

## Chat-Claude thesis / external-verify > internal-review への追加証拠

本 STEP は [[feedback-external-verify-beats-internal-review-4patterns-2026-08-13]] の 7 例目候補 = 「自分の書いた simulator を実 gowin 出力にぶつけて初めて 2-input 前提バグに気付いた」。Design と spec だけ回している間 (100k/100k) は simulator バグは見えず、yosys gowin 出力 (私が生成していない、独立ソース) にぶつけて初めて表出 = external-verify の教訓の直接 example。

## Open threads

1. **Word-level SMT の実験** (rei-solver に BitVec 直接扱いの equivalence op を追加): 数時間実装、n=16 が数秒で解ける可能性。Phase 2 (b') 候補として保持。
2. **Q1.15 signed 化 + 切り詰め (Q1.15 * Q1.15 → Q1.15)**: 本 spike は unsigned のみ。signed wrapper + `>> 15` truncation は加算・比較の組み合わせ、別 STEP で追加可能。
3. **Verilator ベース simulation** (Python simulator の 46k gates で 27ms/sample = 遅い): C 実行なら 100 倍速く、100M サンプル/分オーダー。実務でよりタイトな random test をしたい時に。
4. **Selective scan 全体 (h_t = A_t * h_{t-1} + B_t * x_t)** の sequential 対応: rei-fpga IR は現状組合せ回路のみ (DFF 未対応)。BMC が rei-solver に追加されるのが前提条件。SPEC.md §8 拡張の第 2 項目に対応。

## 関連

- [[project-ssm-qformat-3spike-arc-2026-08-13]] — 前 arc、本 STEP は Phase 2 (b) 実装
- [[reference-ssm-zoh-lut-fpga-config-2026-08-13]] — FPGA config 決定 (512 × Q1.15 × linear、1 BRAM)、本 STEP は Q1.15 演算部の下地
- [[project-rei-fpga-4stage-loop-penetration-2026-08-13]] — rei-fpga 4段閉ループ (xor_nand で貫通済み)、本 STEP は同 pipeline で SSM 部品の可行性実測
- [[feedback-external-verify-beats-internal-review-4patterns-2026-08-13]] — 7 例目候補 (自作 simulator の 2-input 前提バグは gowin 独立出力にぶつけて初めて出た)
- [[feedback-no-rush-publication]] — Phase 2 は 1 本ずつ per「急がずゆっくりと」
- [[feedback-world-uniqueness-claim-controllable]] — Z3 乗算器天井は well-known、novelty 主張ゼロ

## Version

- v1 initial: 2026-08-14 深夜、Phase 2 (b) arc close 時、藤本さん (A) + (E) signal per 保存。exp LUT proved + 乗算器 Z3 天井実測 + random test 4 版完全一致 + simulator variadic bug 発見修正 の完全記録。