safety-critical-patterns

Safety-Critical Coding Patterns

NASA の Power of 10 ルールをもとにした、安全性が重要なソフトウェア向けのガイドラインです。

適用する場面

厳格に適用：安全性が重要なシステム、金融取引、データ整合性に関わるコード
選択的に適用：ビジネスロジック、API ハンドラー、コアアルゴリズム
軽く適用：スクリプト、プロトタイプ、重要度の低いユーティリティ

「リスクの大きさに応じて厳格さを調整する」— これが実際のエンジニアリング原則です

適用しない場面

• prefer-invariants-over-fallbacks が対象とする過剰な防御チェックによってコードが肥大化するような、通常のアプリケーションコード（conserve:code-quality-principles を使用してください）

10 のルール（適用版）

1. 制御フローを制限する

goto、setjmp/longjmp を避け、再帰を制限します。

理由：ツールで検証可能な非巡回の呼び出しグラフを保証します。
適用方法：終了性を証明できる場合（末尾再帰、深さの上限がある場合）は、再帰を許容します。

2. ループの上限を固定する

すべてのループに、検証可能な上限を設けます。

# Good - bound is clear
for i in range(min(len(items), MAX_ITEMS)):
    process(item)

# Risky - unbounded
while not_done:  # When does this end?
    process_next()

適用方法：想定される上限を文書化し、上限が定まらない可能性のあるループには安全上の上限を追加します。

3. 初期化後に動的メモリを確保しない

起動後の重要な処理では、ヒープ割り当てを避けます。

理由：実行時のメモリ割り当て失敗を防ぎます。
適用方法：プールを事前に確保し、頻繁に実行される処理ではオブジェクトを再利用するパターンを使います。

4. 関数の長さは約 60 行にする

関数は画面またはページ 1 枚に収まるようにします。

理由：理解における認知的な限界は今も変わりません。
適用方法：宣言的なコードでは柔軟に、複雑なロジックでは厳格に適用します。

5. アサーションの密度

期待される動作を明記する防御的なアサーションを含めます。

def transfer_funds(from_acct, to_acct, amount):
    assert from_acct != to_acct, "Cannot transfer to same account"
    assert amount > 0, "Transfer amount must be positive"
    assert from_acct.balance >= amount, "Insufficient funds"
    # ... implementation

適用方法：任意の数を満たすことではなく、境界条件と不変条件に注目します。

6. 変数のスコープを最小限にする

可能な限り狭いスコープで変数を宣言します。

# Good - scoped tightly
for item in items:
    total = calculate(item)  # Only exists in loop
    results.append(total)

# Avoid - unnecessarily broad
total = 0  # Why is this outside?
for item in items:
    total = calculate(item)
    results.append(total)

7. 戻り値とパラメーターを確認する

入力を検証し、戻り値を無視しないでください。

# Good
result = parse_config(path)
if result is None:
    raise ConfigError(f"Failed to parse {path}")

# Bad
parse_config(path)  # Ignored return

8. プリプロセッサーとメタプログラミングを制限する

マクロ、デコレーター、コード生成を制限します。

理由：静的解析が可能になります。
適用方法：メタプログラミングを十分に文書化し、暗黙的な仕組みより明示的な記述を優先します。

9. ポインターと参照を適切に扱う

間接参照のレベルを制限し、所有権を明確にします。

適用方法：型ヒントを使い、オプショナル型の深いネストを避け、不変データを優先します。

10. すべての警告を有効にする

初日から最も厳格な設定でコンパイルまたはリントを実行します。

# Python
ruff check --select=ALL
mypy --strict

# TypeScript
tsc --strict --noImplicitAny

適用しない場合があるルール

ルール	緩和する場面
再帰を使わない	木の走査、深さに上限のあるパーサーコンビネーター
動的メモリを使わない	GC 言語、短時間だけ動作するプロセス
関数を 60 行以内にする	宣言的な設定、状態機械
関数ポインターを使わない	コールバック、イベントハンドラー、ストラテジー

統合

次のスキルからこのスキルを参照します：

• pensive:code-refinement - クリーンコードと品質の観点
• sanctum:pr-review - コード品質のフェーズ
• /harden - ハードニングパイプライン内で組み合わせて使用
• /full-review safety-critical - 焦点を絞ったエントリーポイント。また、アサーション密度が低い場合、ループに上限がない場合、または再帰の終了性が証明されていない場合に、自動検出の対象として追加

違反の出力形式

ルール違反ごとに、次の内容を報告します：

Rule N: <rule name>
Location: file.py:42
Anchor: `<verbatim source text at line 42>`
Issue: <what violates the rule>
Fix: <concrete remediation>

検出結果が根拠に基づいていることを確認する（safety-critical:findings-verified）

検出結果を .review/findings.json に書き込み、引用検証ツール（Skill(imbue:review-core) のステップ 5）を実行します。検証ツールが却下したものは削除するか、UNVERIFIED とラベル付けします。

終了条件

• 10項目すべてについて、対象に対する明示的な判定（該当／違反／該当なし）がある。黙って省略しない
• 報告するすべての違反に、具体的な file:line と違反するルール番号が記載されている
• 該当なしと判定したルールには、理由（例：「このモジュールでは動的割り当てを使用していない」）が明記されている。省略しない
• ルール 2 に基づいて指摘されたループは、静的に証明可能な上限があるか確認されている。上限のないループは報告されている
• ルール 1 に基づいて指摘された再帰は、終了性の根拠がない場合に報告されている
• 対象がセーフティクリティカルな用途に適しているか、またはその判断を妨げるルールを要約に記載している
• 報告するすべての違反に、citation_verifier.py で確認済み（終了コード 0）の Location と逐語的な Anchor が付いている。または、未確認の違反は削除するか UNVERIFIED と表示されている

参照元

• NASA JPL Power of 10 Rules（Gerard Holzmann、2006年）
• MISRA C ガイドライン
• 実践的な適用に関する HN の議論から得られた知見