# Rei-Solver 設計仕様書 v0.1

Rei-AIOS に「AI より正確かつ厳密な道具」を接続するための統合層。
Claude Code に追加実装を投げる際は、この文書を仕様の基準とすること。

---

## 0. 設計原則

この 4 つは実装上の好みではなく、破ると必ず後で壊れる制約である。

### 原則 1 — 実装しない、包む

SAT / SMT / 定理証明 / 数値計算の中核を自前で書いてはならない。
数十年の検証実績があるエンジンを呼ぶ。Rei の価値は数値計算そのものではなく、
**どの道具に何を投げるかの判断と、入力の組み立て、結果の解釈**にある。

### 原則 2 — 全てのツールは非同期ジョブ

Z3 は数ミリ秒で返る。DFT や CFD は数時間から数日かかる。
軽いエンジンに合わせて同期 API を作ると、重いエンジンを足した瞬間に
全面書き直しになる。最初から `submit → poll` に統一する。
`solver_run` は内部で同じ経路を通る糖衣にすぎず、別系統ではない。

### 原則 3 — 実行前に同期検証する

**ソルバは入力を疑わない。** メッシュの切り方、境界条件、力場、基底関数を
間違えても、もっともらしい数値を自信満々に返す。
LLM が入力を組み立てる以上、ここが唯一の防御線になる。
`solver_validate` は必ず `solver_submit` の内部でも走る。

### 原則 4 — 保証の種類を必ず返す

全ての結果は `assurance` フィールドを持つ。

| 値 | 意味 | 例 |
|---|---|---|
| `proof` | 機械証明。反証が存在しないことが確定 | SMT unsat、SAT unsat、恒等式の成立 |
| `witness` | 具体的証拠つき。第三者が独立に検算可能 | SAT のモデル、反例入力ベクタ |
| `numeric` | 数値近似。離散化誤差・収束条件に依存 | FEM、DFT、MD（将来） |
| `heuristic` | 探索打ち切り等。保証なし | unknown、timeout |

`proof` と `heuristic` を呼び出し側が取り違えると、この統合層の意味が
消える。TS 側には `isProved(job)` ガードを用意してある。

---

## 1. アーキテクチャ

```
  Rei-AIOS (TypeScript or Python)
        │
        ├── MCP stdio (rei_solver.server)      ← Python 側が MCP を持つ場合
        └── ReiSolverBridge (bridge/*.ts)      ← TS 側が MCP を持つ場合
                │  execFile → rei_solver.cli（単発・常駐不要）
                ▼
        ┌───────────────────────────────┐
        │ api.py  — 唯一のツール面        │
        │   validate / submit / poll     │
        └───────────────────────────────┘
                │
        ┌───────┴────────┐
        │ jobs.py        │  SQLite(WAL) にジョブ状態を永続化
        └───────┬────────┘
                │ spawn (start_new_session=True → 独立プロセスグループ)
                ▼
        ┌───────────────────────────────┐
        │ worker.py  supervisor          │  純 Python・常に暇・待つ/殺す/書く
        │      └── child process         │  エンジン実行のみ
        └───────────────────────────────┘
                │
        ┌───────┴────────┐
        │ registry.py    │  engine 名 → Engine 実装（遅延ロード）
        └───────┬────────┘
                ▼
        engines/  z3 · sympy · pysat  [· lean · openmm · pyscf · fenicsx · openfoam]
```

### なぜ supervisor / child の 2 プロセスなのか（実測に基づく）

最初はワーカー内の `threading.Timer` でタイムアウトを見ていた。**動かない。**
PySAT や Z3 の探索は C 拡張の中で GIL を握ったまま回るため、
Python のタイマースレッドも signal ハンドラも一切スケジュールされない。
3 秒で止まるはずが 18 秒（DB リーパー頼み）かかった。

supervisor は `Queue.get(timeout=…)` で待つだけなので GIL に縛られず、
確実に `SIGTERM → SIGKILL` を送れる。実測 3.28 秒で停止するようになった。
CFD や DFT を足したとき、この分離が「暴走ジョブを確実に止められる」保証になる。

### プロセス停止はグループ単位で行う

supervisor だけを殺すと、fork された子が孤児として CPU を回し続ける
（実測で確認済み）。`spawn_worker` が `start_new_session=True` で
独立したプロセスグループを作っているので、`os.killpg` でまとめて落とす。
`jobs._kill_tree` がこれを担う。

### ゾンビ回収

起動した supervisor の `Popen` 参照は `_SPAWNED` に保持し、
submit と poll のたびに `poll()` で終了済みを回収する。
参照を捨てると常駐 MCP サーバにゾンビが溜まり続ける。

---

## 2. ジョブモデル

### 状態遷移

```
queued ──> running ──┬──> succeeded
                     ├──> failed      （エンジン例外 / 検証エラー）
                     ├──> timeout     （supervisor が子を強制終了）
                     └──> cancelled   （利用者による停止）
```

`succeeded` `failed` `timeout` `cancelled` が終端状態。
終端に達したジョブは二度と書き換わらない（`finish` が状態を保護する）。

### テーブル

```sql
CREATE TABLE jobs (
    id           TEXT PRIMARY KEY,   -- uuid4 先頭 16 桁
    engine       TEXT NOT NULL,
    op           TEXT NOT NULL,
    payload      TEXT NOT NULL,      -- JSON
    status       TEXT NOT NULL,
    timeout_s    REAL NOT NULL,
    created_at   REAL NOT NULL,
    started_at   REAL,
    finished_at  REAL,
    pid          INTEGER,            -- supervisor の pid（= プロセスグループ ID）
    result       TEXT,               -- JSON
    error        TEXT,
    label        TEXT
);
```

保存先は `$REI_SOLVER_HOME`（既定 `~/.rei-solver/jobs.db`）。
WAL モード、`busy_timeout=30s`。プロセスが死んでもジョブ状態は残る。

### タイムアウトの三重防御

1. **エンジン内部制限** — `timeout_s × 0.9` をソルバ自身に伝える。
   強制終了より先にソルバが `unknown` を返してくれた方が情報量が多い。
2. **supervisor** — `Queue.get(timeout)` 失敗で `SIGTERM → SIGKILL`。通常経路。
3. **DB リーパー** — `timeout_s + 10s` を超えた `running` を回収。
   supervisor 自体が落ちた場合の最終防衛線であり、ここに落ちてきたら異常。

上限は `MAX_TIMEOUT_S = 86400`（24 時間）。CFD / DFT を見据えた値。

---

## 3. ツール I/F

8 ツール。MCP の `tools/list` がそのまま以下を返す。

| ツール | 同期性 | 用途 |
|---|---|---|
| `solver_capabilities` | 同期 | エンジン・操作・保証レベル・想定実行時間の一覧 |
| `solver_validate` | 同期 | 実行せず入力だけ検査 |
| `solver_submit` | 非同期 | ジョブ投入。即座に `job_id` を返す |
| `solver_poll` | 同期 | 状態と結果を取得。`wait_s` で待てる |
| `solver_run` | 準同期 | submit+poll の糖衣。数秒で終わる問題のみ |
| `solver_cancel` | 同期 | プロセスグループごと停止 |
| `solver_jobs` | 同期 | ジョブ一覧 |
| `solver_verify` | 同期 | 既知解ハーネス実行 |

### 呼び出し規約

Rei は次の順で呼ぶこと。

1. `solver_capabilities` — どのエンジンに投げるか決める
2. `solver_validate` — 入力を組み立てたら**必ず**通す
3. `typical_runtime` が `ms`/`s` なら `solver_run`、`min`/`hour` なら `solver_submit`
4. `submit` した場合は `job_id` を Rei 側の状態として保持し、`solver_poll` で追跡

### 結果エンベロープ

成功時の `result` は必ず次を含む。

```json
{
  "engine": "z3",
  "engine_version": "5.0.0",
  "op": "circuit_equivalence",
  "assurance": "proof",
  "...": "op ごとの本体"
}
```

---

## 4. エンジン別の操作一覧

### z3 — SMT ソルバ

| op | 保証 | 内容 |
|---|---|---|
| `check_sat` | proof / witness | SMT-LIB2 の充足可能性判定 |
| `prove` | proof / witness | 恒真性の証明。偽なら反例モデル |
| `circuit_equivalence` | proof / witness | 組合せ回路の等価性証明。非等価なら反例入力 |
| `optimize` | witness | 制約下での最大化・最小化 |

対応ゲート: `and or not xor nand nor xnor buf const0 const1`。
ゲートはトポロジカル順で与えること。未駆動の出力信号はエラーになる
（黙って通さない）。

### sympy — 数式処理（Mathematica の代替）

| op | 保証 | 内容 |
|---|---|---|
| `simplify` | proof | 簡約 |
| `solve` | witness | 方程式（系）の厳密解 |
| `integrate` | proof | 不定積分・定積分 |
| `differentiate` | proof | 微分 |
| `limit` | proof | 極限 |
| `verify_identity` | proof / witness | 恒等式の検証。偽なら数値反例を探索 |

`verify_identity` が `identical=false` かつ反例なしの場合、
assurance は `heuristic` になる。これは「非恒等の証明」ではなく
「simplify が 0 に落とせなかった」だけである。取り違えないこと。

### pysat — SAT / MaxSAT

| op | 保証 | 内容 |
|---|---|---|
| `solve_cnf` | proof / witness | CNF の充足可能性。assumptions 指定で unsat core |
| `solve_dimacs` | proof / witness | DIMACS テキストを直接 |
| `enumerate_models` | witness | 充足解の列挙（最大 10000） |
| `maxsat` | witness / proof | 重み付き MaxSAT（RC2） |

バックエンドは `cadical195 → cadical153 → glucose42 → glucose4 → minisat22`
の順で自動選択。

---

## 5. 検証ハーネス

**省略してはならない。** 解析解が独立に分かっている問題を常時走らせることが、
「動いているのか壊れているのか」を機械的に判定できる唯一の手段である。

現在 21 ケース（z3: 7、sympy: 8、pysat: 6）。すべて既知の正解を持つ。

- ガウス積分 `∫e^{-x²}dx = √π`
- `lim_{x→0} sin x / x = 1`
- 鳩の巣原理 PHP(3,2) は UNSAT
- XOR ≡ NAND 4 段構成
- 線形計画の既知最適値
- **偽の命題には反例が返ること**（正しく失敗するかの確認）

実行:

```bash
python -m rei_solver.harness            # 全エンジン
python -m rei_solver.harness z3 --json  # 個別・JSON
```

終了コード 0 = 全通過、1 = 失敗あり。
**起動時・CI・定期実行（1 日 1 回）の 3 箇所で回すこと。**
新しいエンジンを足したら、そのエンジンの `golden()` を実装するまで
本番投入してはならない。

---

## 6. 新エンジンの追加手順

1. `engines/<name>_engine.py` に `Engine` サブクラスを書く
2. `ops` に `OpSpec` を定義（`assurance` と `typical_runtime` を正しく設定）
3. `extra_validate` にそのドメイン固有の検証を書く — **ここが本体**
4. `golden()` に解析解が既知のケースを最低 3 件
5. `registry.py` の `_LOADERS` に 1 行追加
6. `python -m rei_solver.harness <name>` が緑になったら投入

### 追加順の推奨

| 優先 | エンジン | 実装量 | 実行時間 | 主な障壁 |
|---|---|---|---|---|
| 1 | **Lean 4 + mathlib** | 中 | s〜min | REPL 連携。証明探索の失敗ループ設計 |
| 2 | **OpenMM**（分子動力学） | 中 | min〜hour | 力場の選択。GPU |
| 3 | **PySCF**（DFT） | 中 | min〜hour | 基底関数・汎関数・収束判定 |
| 4 | **FEniCSx / CalculiX**（FEM） | 大 | min〜hour | メッシュ生成と境界条件 |
| 5 | **OpenFOAM**（CFD） | 大 | hour〜day | メッシュ、乱流モデル、並列実行 |

3 以降は `assurance="numeric"` を返すこと。`proof` を返してはならない。

### 重いエンジンで追加が必要になるもの

現在の実装は 1 ジョブ 1 ローカルプロセス。HPC を使う段になったら
`jobs.spawn_worker` を差し替えて Slurm / k8s に投げる。
ジョブテーブルと API 面は変更不要——これが原則 2 を最初から守った見返りである。

- 中間進捗の書き戻し（`progress` 列の追加）
- 作業ディレクトリの管理（メッシュ・トラジェクトリ等の大容量成果物）
- 収束判定の自動チェックと `assurance` の格下げ

---

## 7. セキュリティ

| 項目 | 現状 | 残存リスク |
|---|---|---|
| SymPy 式パーサ | トークン検査 + 記号の local_dict 限定 + 別プロセス | 完全な eval サンドボックスではない |
| SMT-LIB 入力 | Z3 のパーサに委譲 | パーサ自体の脆弱性 |
| リソース枯渇 | timeout + プロセス分離 | メモリ上限は未設定 |
| ファイルアクセス | エンジンは FS に触らない | 将来 FEM/CFD で必須になる |

信頼できない入力を扱うなら、worker をコンテナか seccomp 下で動かすこと。
メモリ上限は `resource.setrlimit(RLIMIT_AS)` を子プロセスに追加するのが最短。

---

## 8. 既知の限界

- **Windows 非対応** — `os.killpg` と `fork` に依存。WSL / Linux / macOS で動く。
- **並列度の制御なし** — submit した分だけプロセスが立つ。重いエンジンを
  足す前にセマフォか実行キューが必要。
- **進捗報告なし** — 長時間ジョブの途中経過が見えない。`progress` 列の追加待ち。
- **`verify_identity` の非恒等判定は証明ではない**（§4 参照）。
- **Mathematica 非対応** — 商用ライセンスのため。SymPy / Maxima / SageMath で代替。

---

## 9. 検証済みの事実（実測）

| 項目 | 結果 |
|---|---|
| 既知解ハーネス | 21/21 通過 |
| 統合テスト | 24/24 通過 |
| ハードタイムアウト（PHP(11,10)、3 秒指定） | 3.28 秒で停止 |
| キャンセル後の孤児プロセス | 0 |
| タイムアウト後の孤児プロセス | 0 |
| 12 ジョブ連続実行後のゾンビ | 0 |
| 大容量結果（5000 モデル）のデッドロック | なし |
| SymPy インジェクション（`__import__` 等 4 種） | 全て検証段階で拒否 |
| MCP ハンドシェイク + tools/list + tools/call | 正常 |