# 機能設計書: DrNim (No.28)

## 1. 機能概要

### 1.1 機能名
DrNim (drnim/drnim.nim)

### 1.2 機能説明
Nimコードの静的検証ツール。Z3 SMTソルバーを使用して、コード内の表明（assert）、事前条件（requires）、事後条件（ensures）、不変条件（invariant）を形式的に検証する。コンパイル時にプログラムの正しさを数学的に証明する。

### 1.3 関連画面
- CLI（コマンドラインインターフェース）

## 2. 機能詳細

### 2.1 入力
| 項目 | 型 | 必須 | 説明 |
|------|-----|------|------|
| projectfile | string | Yes | 検証対象のNimプロジェクトファイル |
| --assumeUnique | flag | No | ref pointerのユニーク性を仮定 |
| (Nimコンパイラオプション) | - | No | コード生成に影響しないNimオプション |

### 2.2 検証対象
| プラグマ | 説明 |
|----------|------|
| {.requires: cond.} | 事前条件 |
| {.ensures: cond.} | 事後条件 |
| {.invariant: cond.} | ループ不変条件 |
| assert cond | 表明 |

### 2.3 処理フロー
1. **初期化**
   - Z3コンテキスト作成
   - Nimコンパイラパス初期化
   - モジュールグラフ構築

2. **AST解析**
   - セマンティック解析（sem）実行
   - 制御フロー解析

3. **Z3変換**
   - NimのASTをZ3 ASTに変換
   - 変数のSSA形式管理
   - ファクトデータベース構築

4. **検証実行**
   - Z3ソルバーで充足可能性チェック
   - 反例検出時はエラー報告

5. **結果報告**
   - 検証成功/失敗をレポート
   - 反例があれば詳細表示

### 2.4 出力
| 項目 | 型 | 説明 |
|------|-----|------|
| 検証結果 | message | 成功/失敗メッセージ |
| 反例 | message | 失敗時の反例情報 |
| 終了コード | int | 0=成功, 1=失敗 |

### 2.5 エラーハンドリング
| エラー条件 | 処理 |
|------------|------|
| Z3マッピング不可 | CannotMapToZ3Error |
| 検証失敗 | 反例と共にエラー報告 |
| Z3エラー | Z3Exception |

## 3. ビジネスルール

### 3.1 型のZ3マッピング
| Nim型 | Z3型 |
|-------|------|
| int, int8..int64 | Z3 Int |
| bool | Z3 Bool |
| float | Z3 FPA Double |
| char, uint | Z3 BitVector(64) |
| enum | Z3 Int |

### 3.2 SSA（Static Single Assignment）
変数の各代入にバージョン番号を付与:
```nim
var x = 1     # x`0
x = x + 1     # x`1
x = x * 2     # x`2
```

### 3.3 サポートされる演算
| カテゴリ | 演算 |
|----------|------|
| 算術 | +, -, *, div, mod |
| 比較 | <, <=, ==, !=, >=, > |
| 論理 | and, or, not, implies |
| 配列 | len, high, low, [] |

## 4. 技術仕様

### 4.1 使用ライブラリ
- z3/z3_api（Z3 SMTソルバー）
- compiler/ast, types, sem, modules
- std/parseopt, strutils, os, tables

### 4.2 主要データ構造
```nim
type
  DrnimContext = ref object
    z3: Z3_context           # Z3コンテキスト
    graph: ModuleGraph       # モジュールグラフ
    idgen: IdGenerator       # ID生成器
    facts: seq[(PNode, VersionScope)]  # 既知の事実
    varVersions: seq[int]    # 変数バージョン管理
    varSyms: seq[PSym]       # 変数シンボル
    o: Operators             # 演算子情報
    hasUnstructedCf: int     # 非構造化制御フロー
    currOptions: TOptions
    owner: PSym
    mangler: seq[PSym]
    opImplies: PSym

  DrCon = object
    graph: ModuleGraph
    idgen: IdGenerator
    mapping: Table[string, Z3_ast]  # 名前→Z3 ASTマッピング
    canonParameterNames: bool
    assumeUniqueness: bool
    up: DrnimContext
```

### 4.3 静的リンク（Unix）
```nim
when not defined(windows):
  {.passL: "dist/z3/build/libz3.a".}
```

### 4.4 stableName関数
Nim式をZ3変数名に変換する安定した命名:
```nim
proc stableName(c: DrnimContext; n: PNode; version: VersionScope): string
# 例: "x`1" (xの1番目のバージョン)
# 例: "arr[i]" (配列アクセス)
```

## 5. コードリーディングガイド

### 5.1 推奨読解順序

#### 5.1.1 データ構造の理解
1. **drnim.nim 64-89行目**: 主要型定義
   - DrnimContext, DrCon, VersionScope
   - CannotMapToZ3Error, Z3Exception

2. **drnim.nim 39-53行目**: 定数とUsage
   - HelpMessage, Usage

#### 5.1.2 エントリーポイント
3. **drnim.nim main関数**（ファイル末尾）
   - コマンドライン解析
   - モジュールコンパイル起動

#### 5.1.3 コア処理
4. **drnim.nim 283-296行目**: typeToZ3
   - Nim型からZ3ソートへの変換

5. **drnim.nim 160-255行目**: stableName
   - Nim ASTから安定した文字列名生成

6. **drnim.nim 99-137行目**: isLoc
   - "location"（推論可能な場所）の判定

### 5.2 読解のコツ

#### Z3 APIの理解
```nim
# ソート（型）の作成
Z3_mk_int_sort(ctx)    # 整数型
Z3_mk_bool_sort(ctx)   # ブール型

# 定数の作成
Z3_mk_int(ctx, value, sort)

# 論理式の作成
Z3_mk_and(ctx, count, arr)
Z3_mk_or(ctx, count, arr)
```

#### SSAバージョン管理
```nim
proc currentVarVersion(c: DrnimContext; s: PSym; begin: VersionScope): int
proc previousVarVersion(c: DrnimContext; s: PSym; begin: VersionScope): int
```

### 5.3 プログラム呼び出し階層図

```
drnim [options] projectfile.nim
  |
  +-- コマンドライン解析
  +-- Z3コンテキスト初期化
  |     +-- Z3_mk_context()
  |
  +-- モジュールグラフ構築
  |     +-- compileProject()
  |           +-- sem()
  |
  +-- 検証パス実行
        |
        +-- [各関数に対して]
              |
              +-- {.requires.} 事前条件収集
              +-- 本体のAST走査
              |     +-- stableName() - 変数名生成
              |     +-- typeToZ3() - 型変換
              |     +-- nodeToZ3() - AST変換
              |
              +-- {.ensures.} 事後条件検証
              |     +-- Z3_solver_check()
              |
              +-- 結果報告
                    +-- [SAT] 反例あり→エラー
                    +-- [UNSAT] 検証成功
```

### 5.4 データフロー図

```
[Nimソースコード]
        |
        v
[パーサー/セマンティック解析]
        |
        v
[AST (PNode)]
        |
        +-- [stableName()]
        |     変数の安定名生成
        |     SSAバージョン付与
        |
        +-- [typeToZ3()]
        |     型変換
        |
        +-- [nodeToZ3()]
              AST→Z3 AST変換
        |
        v
[Z3 Assertions]
        |
        v
[Z3_solver_check()]
        |
        +-- [SAT] 反例発見 --> エラー報告
        +-- [UNSAT] 検証成功 --> OK
```

### 5.5 関連ファイル一覧

| ファイルパス | 種別 | 役割 |
|-------------|------|------|
| drnim/drnim.nim | メイン | 検証ツール本体 |
| dist/z3/ | ライブラリ | Z3 SMTソルバー |
| dist/nimz3/ | バインディング | Z3 Nimバインディング |
| compiler/guards.nim | コンパイラ | ガード条件処理 |
| compiler/sem.nim | コンパイラ | セマンティック解析 |
| koch.nim (566-587行目) | ビルド | buildDrNim関数 |

## 6. 変更履歴

| 日付 | 変更者 | 変更内容 |
|------|--------|----------|
| 2026-02-17 | Claude | 初版作成 |
