Rei-AIOS · STEP 1333 · archive spec
rei-fpga-loop — 生成 → 実装 → 証明 の 閉ループ
回路化パイプラインが 生成した 論理回路を FPGA で 実体化し、 それが 元の設計と等価であることを rei-solver で 機械証明する 3 段配線。 2 独立 Python package (rei-solver + rei-fpga) の spec + readme を Rei-AIOS site 上に archival preservation として 反映。
この配線が閉じるもの
回路化パイプライン ──> 論理回路を生成する (生成)
│
FPGA ──────────────> その回路を実体化する (実装)
│
rei-solver ────────> 実体が仕様と一致することを証明する (証明)
circuit_equivalence
実装 status (2026-08-12 時点)
| package | role | file 数 | tests | 依存 |
|---|
rei-solver | circuit_equivalence engine + 3 backend (PySAT / Z3 / SymPy) + REST server + TS bridge | 19 | 24 定義 (全 pass 報告) | Python 3.10+ / z3-solver / python-sat / sympy |
rei-fpga | IR → Verilog → yosys 合成 → LUT 逆変換 → rei-solver で 等価証明 の pipeline | 19 | 26 定義 (全 pass 報告) | yowasp-yosys (WASM 版、 pip only) |
3 段判定の意味 (最重要)
| 段 | 比較対象 | 証明すること |
|---|
spec | 参照仕様 × 設計 | 設計が正しい |
generic | 設計 × 汎用合成後 | 合成器が論理を変えていない |
gowin | 設計 × LUT マッピング後 | LUT に詰めても同じ |
chat-Claude 実装中に 自ら発見した 設計上の穴: generic と gowin が証明するのは 「道具が回路を変えなかった」 ことだけ、 「回路が正しい」 ことは 証明していない。 壊れた設計を 合成すれば 壊れたまま 忠実に実装される (実測: broken_adder4 が spec なしで PROVED 通過)。 → spec 段を追加、 独立に書いた参照仕様との 比較で 「設計の正しさ」 を 別 layer で 検証。 これは Rei stack discipline feedback_zero_sorry_floor_not_ceiling.md + feedback_one_reproduction_over_ten_unverified.md と 深く整合する Pattern 6 最高段 self-correction。
Archive 内容 (このページ配下)
Rei stack 位置付け
- 従来 /tools/rei-solver/ = rei-solver v0.4 spec のみ (STEP 1297 backlog #6)、 実 dispatch 統合は defer records #1 で conditional defer 中 (2026-08-10 「SaaS Phase 2+ pilot customer 獲得後」 判定)
- 本 archive = chat-Claude 2026-08-12 session で 実 implementation 完成 (Rei-AIOS repo 外、 独立 dir
C:\Users\user\rei-solver\ + C:\Users\user\rei-fpga\、 Codetrail + Analog Forge pattern 継承)
- defer #1 status = 「local-agent output で 実装完了、 但し Rei-AIOS repo 外の 独立 project」 に 更新 (完全解消ではない: SaaS Phase 2+ pilot customer 経路 は 未着手)
- Phase C silicon (Tang Console 138K + Tang Nano 9K = STEP 1029/1039) の 直接 downstream candidate、 但し 実機 ビットストリーム programming は 藤本さん 手動 required (rei-fpga SPEC §7 明示)
Honest scope (SPEC.md + README.md の 核心を 集約)
- 組合せ回路のみ、 順序回路 (DFF / latch) は 明示的に拒否 (BMC 別途要)
- 配置配線後の bitstream に対する等価性検証は 未実装 (商用 LEC の 領域: Cadence Palladium / Siemens Veloce / Synopsys ZeBu — 前 turn chat-Claude 指摘 「同 3 社が 独占」)
- ピン番号は hardcoded しない (Tang Console 138K 実ピン は 藤本さん 公式資料と 突き合わせ必須、 未割当で
.cst 生成拒否)
- 「参照仕様を 回路化パイプラインとは 独立な 経路で 生成する」 gap 未埋め (chat-Claude 次段 offer、 現状 「設計の正しさ」 は 人間 (藤本さん) が 保証)
- 数万ゲート規模は 未検証 (構造ハッシュ + partitioning 要)
- Rei stack novelty ゼロ: yosys + Z3 + PySAT + SymPy は 全 well-established tool、 rei-fpga の 貢献 = 3 段判定 discipline (spec / generic / gowin の 意味論的 分離) + 「検証器に歯があるか」 meta-verification (LUT INIT 1-bit flip 破壊試験 + 反例独立再評価) のみ
次 gap (chat-Claude 提案)
「参照仕様を 回路化パイプラインとは 独立な 経路で 生成する」 = 別 arc、 現状 conditional defer (「急がずゆっくりと」 continuation)。