Model Boundary: Explicit Declaration of What Is Not Verified

形式検証はモデルの 内側 の性質を保証するに過ぎない。本モジュールはモデルの 外側 を第一級の対象として扱い、「V&V マトリクスが緑である」ことと 「実システムが安全である」ことを混同しないようにする。

ModelBoundary は以下を記録する:

• 形式的に検証された性質、
• 証明ではなく試験・解析で裏付けられた性質、
• 意図的にモデル化しない残留リスク（rationale と mitigation を含む）。

意図は帳簿付けではなく epistemic honesty（認識論的誠実さ）にある。 システムに変更が入った際は境界記述も見直すべきである。

F6 の変更点

旧実装では ModelBoundary が文字列 systemName と手動同期される verifiedCount : Nat を持つフラット構造体で、対象 VMatrix との型上の 紐付けがなかった。本版では ModelBoundary (vm : VMatrix) として依存型化し、 verifiedCount は vm.totalRecords からの関数に置き換わる。これにより 他システム用の境界記述を誤って流用すると型エラーになる。

ファイルは VV から Matrix に移動した（VMatrix への依存のため）。 namespace も VerifiedMBSE.Matrix に変更されている。

inductive VerifiedMBSE.Matrix.RiskCategory : Type

未モデル化リスクのカテゴリ。

• physical : RiskCategory

  形式モデルの外側にある物理現象（宇宙線 SEU、微小隕石衝突、材料疲労等）。

• environmental : RiskCategory

  環境要因（太陽活動、熱極値、放射線）。

• human : RiskCategory

  ヒューマンファクタ（運用者エラー、手順誤用、訓練不足）。

• software : RiskCategory

  検証境界の外側にあるソフトウェアリスク（COTS、ファームウェア、OS）。

• hardware : RiskCategory

  ハードウェアリスク（製造不良、経年劣化、部品差替え）。

• organizational : RiskCategory

  組織・プロセスリスク（変更管理、サプライチェーン）。

@[implicit_reducible]

instance VerifiedMBSE.Matrix.instReprRiskCategory : Repr RiskCategory

Equations

• VerifiedMBSE.Matrix.instReprRiskCategory = { reprPrec := VerifiedMBSE.Matrix.instReprRiskCategory.repr }

def VerifiedMBSE.Matrix.instReprRiskCategory.repr : RiskCategory → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance VerifiedMBSE.Matrix.instBEqRiskCategory : BEq RiskCategory

Equations

• VerifiedMBSE.Matrix.instBEqRiskCategory = { beq := VerifiedMBSE.Matrix.instBEqRiskCategory.beq }

def VerifiedMBSE.Matrix.instBEqRiskCategory.beq : RiskCategory → RiskCategory → Bool

Equations

• VerifiedMBSE.Matrix.instBEqRiskCategory.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance VerifiedMBSE.Matrix.instDecidableEqRiskCategory : DecidableEq RiskCategory

Equations

• VerifiedMBSE.Matrix.instDecidableEqRiskCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def VerifiedMBSE.Matrix.RiskCategory.toString : RiskCategory → String

人間可読のカテゴリ名。

Equations

• VerifiedMBSE.Matrix.RiskCategory.physical.toString = "Physical"
• VerifiedMBSE.Matrix.RiskCategory.environmental.toString = "Environmental"
• VerifiedMBSE.Matrix.RiskCategory.human.toString = "Human"
• VerifiedMBSE.Matrix.RiskCategory.software.toString = "Software"
• VerifiedMBSE.Matrix.RiskCategory.hardware.toString = "Hardware"
• VerifiedMBSE.Matrix.RiskCategory.organizational.toString = "Organizational"

@[implicit_reducible]

instance VerifiedMBSE.Matrix.instToStringRiskCategory : ToString RiskCategory

Equations

• VerifiedMBSE.Matrix.instToStringRiskCategory = { toString := VerifiedMBSE.Matrix.RiskCategory.toString }

inductive VerifiedMBSE.Matrix.EvidenceKind : Type

性質を裏付ける根拠の強さ。証明と試験・解析を区別し、 ModelBoundary がその差を隠さないようにする。

• verified : EvidenceKind

  Lean での形式証明。

• tested : EvidenceKind

  試験キャンペーン（ユニット試験、HIL、認定試験）による裏付け。

• analyzed : EvidenceKind

  解析手法（FMEA、FTA、Monte Carlo）による裏付け。

def VerifiedMBSE.Matrix.instReprEvidenceKind.repr : EvidenceKind → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance VerifiedMBSE.Matrix.instReprEvidenceKind : Repr EvidenceKind

Equations

• VerifiedMBSE.Matrix.instReprEvidenceKind = { reprPrec := VerifiedMBSE.Matrix.instReprEvidenceKind.repr }

def VerifiedMBSE.Matrix.instBEqEvidenceKind.beq : EvidenceKind → EvidenceKind → Bool

Equations

• VerifiedMBSE.Matrix.instBEqEvidenceKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance VerifiedMBSE.Matrix.instBEqEvidenceKind : BEq EvidenceKind

Equations

• VerifiedMBSE.Matrix.instBEqEvidenceKind = { beq := VerifiedMBSE.Matrix.instBEqEvidenceKind.beq }

@[implicit_reducible]

instance VerifiedMBSE.Matrix.instDecidableEqEvidenceKind : DecidableEq EvidenceKind

Equations

• VerifiedMBSE.Matrix.instDecidableEqEvidenceKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def VerifiedMBSE.Matrix.EvidenceKind.toString : EvidenceKind → String

人間可読の種別名。

Equations

• VerifiedMBSE.Matrix.EvidenceKind.verified.toString = "Verified"
• VerifiedMBSE.Matrix.EvidenceKind.tested.toString = "Tested"
• VerifiedMBSE.Matrix.EvidenceKind.analyzed.toString = "Analyzed"

@[implicit_reducible]

instance VerifiedMBSE.Matrix.instToStringEvidenceKind : ToString EvidenceKind

Equations

• VerifiedMBSE.Matrix.instToStringEvidenceKind = { toString := VerifiedMBSE.Matrix.EvidenceKind.toString }

structure VerifiedMBSE.Matrix.UnmodeledRisk : Type

UnmodeledRisk: 形式モデルがカバーしないリスク。rationale と mitigation を 明示的に要求することで、エンジニアにそのギャップを命名・正当化させる。

• description : String

  リスクの短い説明。

• category : RiskCategory

  リスクのカテゴリ。

• rationale : String

  なぜこのリスクを形式化しないかの根拠。

• mitigation : String

  非形式の緩和策（プロセス、試験、冗長化、運用制約）。

def VerifiedMBSE.Matrix.instReprUnmodeledRisk.repr : UnmodeledRisk → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance VerifiedMBSE.Matrix.instReprUnmodeledRisk : Repr UnmodeledRisk

Equations

• VerifiedMBSE.Matrix.instReprUnmodeledRisk = { reprPrec := VerifiedMBSE.Matrix.instReprUnmodeledRisk.repr }

structure VerifiedMBSE.Matrix.NonFormalProperty : Type

NonFormalProperty: 試験・解析で裏付けられているが証明されていない性質。

• description : String

  性質の説明。

• kind : EvidenceKind

  非形式根拠の種別（.tested または .analyzed）。

• source : String

  根拠ソースの参照（報告書 ID、試験キャンペーン名など）。

def VerifiedMBSE.Matrix.instReprNonFormalProperty.repr : NonFormalProperty → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance VerifiedMBSE.Matrix.instReprNonFormalProperty : Repr NonFormalProperty

Equations

• VerifiedMBSE.Matrix.instReprNonFormalProperty = { reprPrec := VerifiedMBSE.Matrix.instReprNonFormalProperty.repr }

structure VerifiedMBSE.Matrix.ModelBoundary (vm : VMatrix) : Type

ModelBoundary: モデルがカバーする範囲と外側のリスクを合わせた全体像。

対象 VMatrix を型パラメータとして持つことで、他システム用の境界記述を 誤って流用すると型エラーになる（F6）。verifiedCount は関数として vm.totalRecords から導出されるため、手動同期は不要。

• systemName : String

  この境界の識別子（典型的にはシステム名）。

• nonFormal : List NonFormalProperty

  試験・解析で裏付けられているが証明されていない性質。

• unmodeled : List UnmodeledRisk

  意図的に形式化しないリスク。

@[implicit_reducible]

instance VerifiedMBSE.Matrix.instReprModelBoundary {vm✝ : VMatrix} : Repr (ModelBoundary vm✝)

Equations

• VerifiedMBSE.Matrix.instReprModelBoundary = { reprPrec := VerifiedMBSE.Matrix.instReprModelBoundary.repr }

def VerifiedMBSE.Matrix.instReprModelBoundary.repr {vm✝ : VMatrix} : ModelBoundary vm✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def VerifiedMBSE.Matrix.ModelBoundary.verifiedCount {vm : VMatrix} : ModelBoundary vm → Nat

形式的に検証された性質の数。対象 VMatrix の全レコード数から自動導出される。

Equations

• x✝.verifiedCount = vm.totalRecords

def VerifiedMBSE.Matrix.ModelBoundary.unmodeledCount {vm : VMatrix} (mb : ModelBoundary vm) : Nat

未モデル化リスクの件数。

Equations

• mb.unmodeledCount = mb.unmodeled.length

def VerifiedMBSE.Matrix.ModelBoundary.nonFormalCount {vm : VMatrix} (mb : ModelBoundary vm) : Nat

非形式性質の件数。

Equations

• mb.nonFormalCount = mb.nonFormal.length

def VerifiedMBSE.Matrix.ModelBoundary.totalItems {vm : VMatrix} (mb : ModelBoundary vm) : Nat

追跡している項目の総数（verified + non-formal + unmodeled）。

Equations

• mb.totalItems = mb.verifiedCount + mb.nonFormalCount + mb.unmodeledCount

def VerifiedMBSE.Matrix.ModelBoundary.risksInCategory {vm : VMatrix} (mb : ModelBoundary vm) (cat : RiskCategory) : List UnmodeledRisk

未モデル化リスクをカテゴリで絞り込む。

Equations

• mb.risksInCategory cat = List.filter (fun (r : VerifiedMBSE.Matrix.UnmodeledRisk) => r.category == cat) mb.unmodeled

def VerifiedMBSE.Matrix.ModelBoundary.summary {vm : VMatrix} (mb : ModelBoundary vm) : String

ModelBoundary を人間可読な要約文字列にレンダリングする。

Equations

• One or more equations did not get rendered due to their size.