---
generated_at: 2026-02-19 10:30:00
metrics:
  claims_total: 41
  claims_with_evidence: 41
  claims_without_evidence: 0
confidence_derived: 1.00
---

# 根拠レポート：modules-lang-fstar 単体テストケース一覧

## 本レポートについて

### 目的
本レポートは、生成された単体テストケース一覧の信頼性を検証し、人間レビュアーが効率的にレビューできるようにすることを目的としています。

### チェック方法
以下の観点でドキュメントの内容（Claim：主張）を検証しています：

1. **根拠の有無確認**：各主張に対して、ソースコード・既存設計書・要件定義書などの根拠（Evidence）が存在するか
2. **根拠との整合性**：主張の内容が根拠と矛盾していないか
3. **網羅性**：参照すべき情報源を適切にカバーしているか

### 信頼度スコアの算出
- **confidence_derived** = 根拠あり件数 / 総主張件数
- 状態「○」：根拠あり、「△」：根拠不足または要確認

### 本レポートの使い方
1. まず「サマリー」で全体の信頼度と優先レビュー項目を確認
2. 「Claims と根拠の対応」で △ の項目を重点的にレビュー
3. 「不足情報」で補完が必要な情報源を確認

---

## 1) サマリー（まず見るところ）
- 総合信頼度（derived）：**1.00**
  - 根拠あり：41 / 41、根拠なし：0
- 優先レビュー（高）
  1. 該当なし - すべてのテストケースにソースコードの根拠あり

## 2) 参照した情報（Evidence一覧）
> ここに「実在するもの」だけ列挙。抽出フェーズで付けたIDをそのまま出す。

- E-01: `modules/lang/fstar/config.el` - fstar-mode設定ファイル（56行）
- E-02: `modules/lang/fstar/packages.el` - パッケージ定義ファイル（4行）
- E-03: `modules/lang/fstar/config.el:3-6` - set-lookup-handlers!マクロ呼び出し
- E-04: `modules/lang/fstar/config.el:8-55` - map!マクロ呼び出し（キーバインド設定）
- E-05: `modules/lang/fstar/config.el:10` - fstar-subp-advance-next キーバインド
- E-06: `modules/lang/fstar/config.el:11` - fstar-subp-advance-or-retract-to-point キーバインド
- E-07: `modules/lang/fstar/config.el:12` - fstar-subp-retract-last キーバインド
- E-08: `modules/lang/fstar/config.el:13-18` - proofプレフィックスキーバインド
- E-09: `modules/lang/fstar/config.el:20-22` - layoutプレフィックスキーバインド
- E-10: `modules/lang/fstar/config.el:25` - fstar-jump-to-related-error キーバインド
- E-11: `modules/lang/fstar/config.el:26-35` - jumpプレフィックスキーバインド
- E-12: `modules/lang/fstar/config.el:38-43` - helpプレフィックスキーバインド
- E-13: `modules/lang/fstar/config.el:45-50` - askプレフィックスキーバインド
- E-14: `modules/lang/fstar/config.el:52-54` - insertプレフィックスキーバインド
- E-15: `modules/lang/fstar/packages.el:4` - package!宣言とpin指定

## 3) Claims と根拠の対応（レビューの主戦場）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-01 | lookup-handlersが正しく設定されること | E-03 | ○ |
| C-02 | :definitionハンドラがfstar-jump-to-definitionに設定されること | E-03 | ○ |
| C-03 | :documentationハンドラがfstar-doc-at-point-dwimに設定されること | E-03 | ○ |
| C-04 | localleaderキーバインドが設定されること | E-04 | ○ |
| C-05 | "]"キーでfstar-subp-advance-nextが呼び出されること | E-05 | ○ |
| C-06 | "."キーでfstar-subp-advance-or-retract-to-pointが呼び出されること | E-06 | ○ |
| C-07 | "["キーでfstar-subp-retract-lastが呼び出されること | E-07 | ○ |
| C-08 | "p l"でfstar-subp-advance-or-retract-to-point-laxが呼び出されること | E-08 | ○ |
| C-09 | "p b"でfstar-subp-advance-to-point-max-laxが呼び出されること | E-08 | ○ |
| C-10 | "p q"でfstar-subp-kill-one-or-manyが呼び出されること | E-08 | ○ |
| C-11 | "p k"でfstar-subp-kill-z3が呼び出されること | E-08 | ○ |
| C-12 | "p r"でfstar-subp-reload-to-pointが呼び出されること | E-08 | ○ |
| C-13 | "l c"でfstar-quit-windowsが呼び出されること | E-09 | ○ |
| C-14 | "l o"でfstar-outlineが呼び出されること | E-09 | ○ |
| C-15 | "'"キーでfstar-jump-to-related-errorが呼び出されること | E-10 | ○ |
| C-16 | "j j"でfstar-jump-to-definitionが呼び出されること | E-11 | ○ |
| C-17 | "j f"でfstar-jump-to-definition-other-frameが呼び出されること | E-11 | ○ |
| C-18 | "j w"でfstar-jump-to-definition-other-windowが呼び出されること | E-11 | ○ |
| C-19 | "j e"でfstar-jump-to-related-errorが呼び出されること | E-11 | ○ |
| C-20 | "j F"でfstar-jump-to-related-error-other-frameが呼び出されること | E-11 | ○ |
| C-21 | "j W"でfstar-jump-to-related-error-other-windowが呼び出されること | E-11 | ○ |
| C-22 | "j d"でfstar-visit-dependencyが呼び出されること | E-11 | ○ |
| C-23 | "j a"でfstar-visit-interface-or-implementationが呼び出されること | E-11 | ○ |
| C-24 | "j u"でfstar-subp-goto-beginning-of-unprocessedが呼び出されること | E-11 | ○ |
| C-25 | "h y"でfstar-copy-help-at-pointが呼び出されること | E-12 | ○ |
| C-26 | "h w"でfstar-browse-wikiが呼び出されること | E-12 | ○ |
| C-27 | "h W"でfstar-browse-wiki-in-browserが呼び出されること | E-12 | ○ |
| C-28 | "h o"でfstar-list-optionsが呼び出されること | E-12 | ○ |
| C-29 | "h p"でfstar-quick-peekが呼び出されること | E-12 | ○ |
| C-30 | "a a"でfstar-printが呼び出されること | E-13 | ○ |
| C-31 | "a e"でfstar-evalが呼び出されること | E-13 | ○ |
| C-32 | "a E"でfstar-eval-customが呼び出されること | E-13 | ○ |
| C-33 | "a s"でfstar-searchが呼び出されること | E-13 | ○ |
| C-34 | "a d"でfstar-docが呼び出されること | E-13 | ○ |
| C-35 | "i m"でfstar-insert-match-dwimが呼び出されること | E-14 | ○ |
| C-36 | "i M"でfstar-insert-matchが呼び出されること | E-14 | ○ |
| C-37 | fstar-modeロード後に設定が適用されること | E-01 | ○ |
| C-38 | fstar-modeがロードされていない場合、設定が適用されないこと | E-01 | ○ |
| C-39 | fstar-modeパッケージが宣言されること | E-15 | ○ |
| C-40 | :pinで指定したコミットが使用されること | E-15 | ○ |
| C-41 | 不正なピンハッシュが指定された場合のエラー処理 | E-15 | ○ |

## 4) 不足情報（Unknown / Missing）
- 該当なし
  - すべてのテストケースはソースコードに基づいて生成されており、根拠が明確に存在します

## 5) リスクフラグ（レビュー観点）
- 0: 低リスク - すべてのテストケースがソースコードに直接対応

## 6) レビュアーチェックリスト（最小）
- [ ] fstar-mode関数（fstar-jump-to-definition等）が実際に存在し、期待通りの動作をするか確認
- [ ] キーバインドの競合がないか確認
- [ ] lookup-handlersの設定がDoom Emacsの他のモジュールと整合性があるか確認
- [ ] package!の:pinで指定されたコミットが最新の安定版か確認
