# rei-fpga

回路化パイプラインの出力を FPGA に落とし、**元の設計と等価であることを機械証明する**。

```
生成（回路化） → 実装（yosys / GOWIN） → 証明（rei-solver）
```

設計は [SPEC.md](SPEC.md)。Claude Code に追加を投げるときはそちらを渡す。

---

## 30 秒で動かす

```bash
pip install yowasp-yosys              # WASM 版 yosys、追加依存なし
export REI_SOLVER_ROOT=../rei-solver  # rei-solver の場所
python examples/build_examples.py
python -m rei_fpga.cli prove examples/adder4.json --spec examples/adder4.json
```

```
回路: adder4  入力 9 / 出力 5 / ゲート 25 / 段数 9
  [spec   ] ゲート   25 / 段数  9  等価を証明  assurance=proof  0.13s
  [generic] ゲート   25 / 段数  9  等価を証明  assurance=proof  0.15s
  [gowin  ] ゲート  296 / 段数  9  等価を証明  assurance=proof  0.18s
判定: PROVED
```

`gowin` 段の 296 ゲートは、GOWIN の LUT に詰め込まれた後の姿を展開したもの。
**元の 25 ゲートと論理が完全に一致することが証明されている。**

```bash
python -m unittest discover -s tests   # 26 件
```

---

## 壊れているとどうなるか

```bash
python -m rei_fpga.cli prove examples/broken_adder4.json --spec examples/adder4.json
```

```
  [spec   ] 反例あり  assurance=witness
            反例入力: a0=0, a1=0, a2=0, a3=1, b0=1, b1=1, b2=1, b3=0, cin=0
            食い違う出力: ['s1', 's2', 's3', 'cout']
  [generic] 等価を証明  assurance=proof
  [gowin  ] 等価を証明  assurance=proof
判定: REFUTED
```

推測ではなく、**どの入力で壊れるかが具体的に出ます**。

---

## 最重要 — 何を証明していないか

`generic` と `gowin` が証明するのは「**道具が回路を変えなかった**」ことだけです。
**「回路が正しい」ことは証明していません。**

上の例がまさにそれで、壊れた加算器も合成段は両方 proof で通っています。
道具は忠実に、誤った設計を誤ったまま実装したからです。

設計の正しさを見るには `--spec` に**独立に書いた参照仕様**を渡してください。
同じ生成器の出力を両方に渡すのは、自分の答案を自分で採点する行為です。

---

## 検証器に歯があること

`PROVED` が意味を持つのは、検証器が壊れた実装を実際に弾ける場合だけです。
`TestTeeth` がそれを確認しています。

1. `adder4` を GOWIN 合成して LUT ネットリストを得る
2. LUT の `INIT` を **1 ビットだけ** 反転する
3. 逆変換して検証にかける → **反例が返ることを確認**
4. 返った反例を、証明器から**独立した素朴な評価器**で再計算し、
   本当に出力が食い違うことを確認

4 が肝です。証明器の言い分を鵜呑みにせず、第二の実装で照合しています。

---

## コマンド

| コマンド | 用途 |
|---|---|
| `check design.json` | IR を検証して統計を出す |
| `verilog design.json -o out.v` | 合成可能 Verilog を出力 |
| `prove design.json [--spec s.json]` | 合成して等価性を証明 |
| `compare a.json b.json` | 2 つの IR を直接比較 |
| `cst design.json --pins pins.json` | GOWIN 制約ファイルを生成 |

終了コード: `0` proved / `1` refuted / `2` inconclusive

---

## 回路 IR

rei-solver の `circuit_equivalence` と同一形式です。

```json
{
  "name": "half_adder",
  "inputs": ["a", "b"],
  "gates": [{"op": "xor", "out": "s", "args": ["a", "b"]},
            {"op": "and", "out": "co", "args": ["a", "b"]}],
  "outputs": ["s", "co"]
}
```

回路化パイプライン側からは `Builder` で組み立てられます。

```python
from rei_fpga.ir import Builder
b = Builder("half_adder", ["a", "b"])
ckt = b.finish({"s": b.gate("xor", "a", "b"), "co": b.gate("and", "a", "b")})
```

ゲート種は `and or not xor nand nor xnor buf const0 const1`。

---

## Tang Console 138K で走らせる

**ピン番号はこのパッケージに入っていません。** 推測で書いた番号は合成も
配置配線も通ってしまい、実機で初めて誤りに気づきます。しかも証明器は
ピン割当を検証しません。ここだけは公式のピン定義と突き合わせてください。

```bash
python -m rei_fpga.cli prove   design.json            # 先に証明を通す
python -m rei_fpga.cli verilog design.json -o design.v
python -m rei_fpga.cli cst     design.json --pins pins.json -o design.cst
# GOWIN EDA で design.v + design.cst を配置配線 → ビットストリーム
```

証明を通してから実機に行くこと。逆にすると、実機の不具合が論理の誤りか
配線の誤りか切り分けられなくなります。

---

## ファイル構成

```
rei-fpga/
├── SPEC.md                  設計仕様書
├── rei_fpga/
│   ├── ir.py                回路 IR・検証・トポロジカル整列・Builder
│   ├── verilog.py           IR → 合成可能 Verilog
│   ├── synth.py             yosys 実行（generic / gowin）
│   ├── netlist.py           ネットリスト → IR（LUT を最小項に展開）
│   ├── prove.py             rei-solver 呼び出し
│   ├── flow.py              生成→実装→証明の一括パイプライン
│   ├── boards.py            Tang Console 138K・.cst 生成
│   └── cli.py
├── examples/build_examples.py
└── tests/test_rei_fpga.py   26 件
```

## 限界

- 組合せ回路のみ。順序回路（DFF）は明示的に拒否します
- 配置配線後のビットストリームに対する検証は未実装
- 数万ゲート規模は未検証。構造ハッシュと切り出しが必要になります
- Linux / macOS / WSL（rei-solver 側の制約）