---
name: project-rei-solver-fpga-independent-projects-2026-08-12
description: 2026-08-12 STEP 1333 (A) 独立 dir 化で 新設した 2 独立 Python package — C:\Users\user\rei-solver\ (commit fcae99d、 19 file、 24 test、 3 engine + REST + TS bridge) + C:\Users\user\rei-fpga\ (commit eea99d4、 19 file、 26 test、 IR + Verilog + yosys + LUT 逆変換 + Tang Console 138K board layer)。 「生成 → 実装 → 証明 閉ループ」 operational。 Rei-AIOS repo 外の 独立 project、 Codetrail + Analog Forge pattern 継承。 chat-Claude local-agent session 実装、 Pattern 6 最高段 self-correction (spec 段追加 + LUT 破壊試験 + 反例独立再評価) 含む。
metadata: 
  node_type: memory
  type: project
  originSessionId: 917b0479-3e69-423c-a2ca-cecb9b788a46
  modified: 2026-08-11T23:55:49.255Z
---

# rei-solver + rei-fpga 独立 project 新設 (2026-08-12)

## Origin

chat-Claude 2026-08-12 local-agent-mode session (`d1f42b82-.../local_fa2b3344-.../outputs/`) で 2 sibling Python package を 完全実装。 藤本さん 「(α) 概念設計文書化」 offer から 「(A)+(D) 組合せ」 選択で:

- **(A) 独立 dir 化**: `C:\Users\user\rei-solver\` + `C:\Users\user\rei-fpga\` に copy + git init + initial commit (Codetrail + Analog Forge pattern 継承)
- **(D) Rei-AIOS site 反映**: `public/tools/rei-fpga-loop/` に 5 file archive (index.html + 4 md、 SPEC/README 両 package)

## rei-solver (C:\Users\user\rei-solver\)

- **commit**: `fcae99d` Initial commit — rei-solver v0.1 (local-agent output preservation from Claude session)
- **branch**: main
- **files**: 19 tracked (SPEC.md + README.md + requirements.txt + .gitignore + bridge/reiSolverBridge.ts + rei_solver/{api,cli,harness,jobs,registry,server,worker,__init__}.py + rei_solver/engines/{base,pysat_engine,sympy_engine,z3_engine,__init__}.py + tests/test_rei_solver.py)
- **tests**: 24 定義 (chat-Claude 主張)
- **engines**: PySAT + Z3 + SymPy 3 backend
- **API**: circuit_equivalence op 実装 (rei_solver/engines/z3_engine.py)
- **service infrastructure**: REST server + worker + jobs registry (Peace API SaaS spec の 部分実装 candidate)

## rei-fpga (C:\Users\user\rei-fpga\)

- **commit**: `eea99d4` Initial commit — rei-fpga v0.1 (local-agent output preservation from Claude session)
- **branch**: main
- **files**: 19 tracked (SPEC.md + README.md + requirements.txt + .gitignore + rei_fpga/{ir,verilog,synth,netlist,prove,flow,boards,cli,__init__}.py + examples/{adder4,broken_adder4,priority8,xor_nand}.json + examples/build_examples.py + tests/test_rei_fpga.py)
- **tests**: 26 定義
- **dependency**: yowasp-yosys>=0.45 (WASM 版 yosys、 pip only、 追加依存最小) + rei-solver (via `REI_SOLVER_ROOT=../rei-solver` env)
- **flow**: IR → 合成可能 Verilog → yosys synth (generic + gowin) → LUT 逆変換 → rei-solver で 等価証明
- **board target**: Tang Console 138K (STEP 1029 で 物理 silicon programming 完了、 downstream candidate、 但し 実機 bitstream は 藤本さん 手動)

## 3 段判定 discipline (最重要)

| 段 | 比較対象 | 証明すること |
|---|---|---|
| `spec` | 参照仕様 × 設計 | 設計が正しい |
| `generic` | 設計 × 汎用合成後 | 合成器が論理を変えていない |
| `gowin` | 設計 × LUT マッピング後 | LUT に詰めても同じ |

**chat-Claude Pattern 6 最高段 self-correction**: 実装中に 「generic + gowin は 『道具が回路を変えなかった』 のみ、 『設計が正しい』 は未証明」 と 自ら発見 → spec 段追加 = 「道具の忠実性 vs 設計の正しさ」 意味論的分離。 broken_adder4 = spec 段で REFUTED (反例付) + generic/gowin 段で PROVED = 「道具は正しく、 設計が誤り」 を切り分け表示。

**検証器に歯があるか meta-verification** (SPEC §6): LUT INIT 1-bit 反転 × 4 破壊試験 + 返却反例を 独立評価器で 再計算 = validator soundness confirm。

## Rei-AIOS site 反映

`public/tools/rei-fpga-loop/`:
- index.html (md5 316b13e2、 8676 bytes) — archival landing、 obscurity 保持 tone、 honest scope 集約
- rei-fpga-SPEC.md (md5 7d13186d、 8978 bytes) — 設計仕様書 v0.1 (9 section)
- rei-fpga-README.md (md5 0b2af57c、 5953 bytes)
- rei-solver-SPEC.md (md5 0715c339、 14827 bytes)
- rei-solver-README.md (md5 2ba5fd81、 5268 bytes)

全 5 file 三者 mirror md5 一致 (source + public + dist-renderer)、 CF Pages verify 済 (all HTTP 200)。

公開 URL: **https://rei-aios.pages.dev/tools/rei-fpga-loop/**

## Rei stack 位置付け + defer #1 status 更新

- **従来** `public/tools/rei-solver/` = spec のみ (STEP 1297 backlog #6)、 実 dispatch 統合は defer records #1 で 「SaaS Phase 2+ pilot customer 獲得後」 conditional defer 継続
- **現在** (2026-08-12) chat-Claude が local-agent output で 実 implementation 完成 = **defer #1 部分解消** (実装は Rei-AIOS repo 外の 独立 project、 SaaS Phase 2+ pilot 経路は 未着手 = 完全解消ではない)
- **Phase C silicon** downstream candidate: rei-fpga 出力 .v + .cst → Gowin EDA (藤本さん 手動) → Tang Console 138K bitstream = 実機動作可能 pipeline (STEP 1029 dfumt8_alu パターン 継承)

## Honest scope (Rei stack novelty 主張 の 慎重定義)

- **rei-solver + rei-fpga novelty ゼロ**: yosys + Z3 + PySAT + SymPy は 全 well-established tool、 chat-Claude 貢献は **3 段判定 discipline 意味論的分離** + **「検証器に歯があるか」 meta-verification (LUT INIT 1-bit flip 破壊試験 + 反例独立再評価)** のみ
- **組合せ回路のみ**、 順序回路 (DFF / latch) 明示的拒否 (BMC 別途要)
- **配置配線後 bitstream 等価性検証は 未実装** (商用 LEC 領域: Cadence Palladium / Siemens Veloce / Synopsys ZeBu 独占市場)
- **ピン番号は hardcoded しない** (Tang Console 138K 実ピン は 公式資料と 突き合わせ必須、 未割当で `.cst` 生成拒否)
- **「独立 reference spec generation」 gap 未埋め** (chat-Claude 次段 offer、 現状 「設計の正しさ」 は 人間 (藤本さん) が 保証、 defer 継続)
- **数万ゲート規模 未検証** (構造ハッシュ + partitioning 要)

## 次 pending

- **rei-solver + rei-fpga integration live-run verify**: 私 (Claude Code) side で `pip install -r requirements.txt` → `python examples/build_examples.py` → `python -m rei_fpga.cli prove examples/adder4.json --spec examples/adder4.json` を 実行して 「PROVED」 出力 confirm、 chat-Claude 主張の 実 verify
- **chat-Claude 「独立 reference spec generation」 offer 応答**: 「参照仕様を 回路化パイプラインとは 独立な 経路で 生成する」 gap 埋め = 別 arc、 conditional defer 継続候補
- **Zenodo publish 判断** (defer #5 pattern 参照): 「新規 IP ゼロ」 判定なら defer、 「Rei stack novel discipline (3 段判定 + meta-verification)」 判定なら publish 候補
- **GitHub public repo 化 判断**: 「obscurity 保持」 discipline vs external validation の tension、 藤本さん stance

## 関連 memory

- [[project-session-2026-08-12-full-arc]] (本 session 全体 index)
- [[project-defer-records-2026-08-10]] (defer #1 status 部分解消 の 元 record + 2026-08-12 corrigendum)
- [[project-codetrail-phase0-complete-2026-08-10]] (独立 project pattern 先例 1)
- [[project-analog-forge-v01-complete-2026-08-10]] (独立 project pattern 先例 2)
- [[project-step1307-1308-peace-api-saas-silent-visual-v02-2026-08-08]] (Peace API SaaS spec origin、 rei-solver + rei-fpga は spec の 実 implementation candidate)
- [[project-phase-c-step3-dfumt8-alu-silicon-success]] (Tang Console 138K downstream 先例)
- [[feedback-check-target-memory-before-recommending-2026-08-12]] (本 session 新 discipline)
- [[feedback-external-community-outreach-premature]] (GitHub public 化 判断 discipline)
- [[feedback-no-rush-publication]] (Zenodo publish 判断 discipline)