ValidationEvidence: Confidence Levels as Types

Confidence < Contract < Trusted の三層階層、昇格トレース、および V モデルの セルを統一的に表す VVRecord を定義する。

inductive VerifiedMBSE.VV.ValidationEvidence (P : Prop) : Type

ValidationEvidence: 命題 P の検証根拠を表す型。 三層階層: confidence < contract < trusted。

• confidence {P : Prop} : Float → ValidationEvidence P

  Confidence: 確率的な根拠（初期設計、専門家ヒューリスティクス）。

• contract {P : Prop} (assumption : Prop) : (assumption → P) → ValidationEvidence P

  Contract: 条件付き保証（試験・シミュレーション後）。

• trusted {P : Prop} : P → ValidationEvidence P

  Trusted: 公理として採用（ハードウェア試験、承認済み）。

def VerifiedMBSE.VV.ValidationEvidence.confidenceLevel {P : Prop} : ValidationEvidence P → Float

根拠の信頼度を数値で返す（表示・ソート用）。

注意: この Float を使った比較は丸め誤差の観点で推奨されない。 「trusted かどうか」の判定には isTrusted を使うこと（F2 参照）。

Equations

• (VerifiedMBSE.VV.ValidationEvidence.confidence p).confidenceLevel = p
• (VerifiedMBSE.VV.ValidationEvidence.contract assumption a).confidenceLevel = 0.95
• (VerifiedMBSE.VV.ValidationEvidence.trusted a).confidenceLevel = 1.0

def VerifiedMBSE.VV.ValidationEvidence.isTrusted {P : Prop} : ValidationEvidence P → Bool

ValidationEvidence が .trusted 構造子であるかを判定する。 Float 等号を介さない構造的判別で、fullyTrusted 等の Bool 計算で用いる。

Equations

• (VerifiedMBSE.VV.ValidationEvidence.trusted a).isTrusted = true
• x✝.isTrusted = false

def VerifiedMBSE.VV.ValidationEvidence.isContract {P : Prop} : ValidationEvidence P → Bool

ValidationEvidence が .contract 構造子であるかを判定する。

Equations

• (VerifiedMBSE.VV.ValidationEvidence.contract assumption a).isContract = true
• x✝.isContract = false

def VerifiedMBSE.VV.ValidationEvidence.isConfidence {P : Prop} : ValidationEvidence P → Bool

ValidationEvidence が .confidence 構造子であるかを判定する。

Equations

• (VerifiedMBSE.VV.ValidationEvidence.confidence a).isConfidence = true
• x✝.isConfidence = false

def VerifiedMBSE.VV.ValidationEvidence.promoteToContract {P : Prop} : ValidationEvidence P → (a : Prop) → (ev : a → P) → ValidationEvidence P

昇格: Confidence → Contract。

Equations

• x✝.promoteToContract a ev = VerifiedMBSE.VV.ValidationEvidence.contract a ev

def VerifiedMBSE.VV.ValidationEvidence.promoteToTrusted {P : Prop} (c : ValidationEvidence P) (h : match c with | contract a a_1 => a | x => True) : ValidationEvidence P

昇格: Contract → Trusted（仮定が実際に成立する場合）。

Equations

• (VerifiedMBSE.VV.ValidationEvidence.contract assumption ev).promoteToTrusted h_2 = VerifiedMBSE.VV.ValidationEvidence.trusted ⋯
• (VerifiedMBSE.VV.ValidationEvidence.confidence p).promoteToTrusted x = VerifiedMBSE.VV.ValidationEvidence.confidence p
• (VerifiedMBSE.VV.ValidationEvidence.trusted p).promoteToTrusted x = VerifiedMBSE.VV.ValidationEvidence.trusted p

structure VerifiedMBSE.VV.ValidationTrace (P : Prop) : Type

ValidationTrace: 昇格履歴を保持するレコード。

• history : List (ValidationEvidence P)
• current : ValidationEvidence P

def VerifiedMBSE.VV.ValidationTrace.init {P : Prop} (ev : ValidationEvidence P) : ValidationTrace P

ValidationTrace の初期化。

Equations

• VerifiedMBSE.VV.ValidationTrace.init ev = { history := [], current := ev }

def VerifiedMBSE.VV.ValidationTrace.promote {P : Prop} (t : ValidationTrace P) (next : ValidationEvidence P) : ValidationTrace P

ValidationTrace に昇格を記録する。

Equations

• t.promote next = { history := t.history ++ [t.current], current := next }

def VerifiedMBSE.VV.ValidationTrace.currentLevel {P : Prop} (t : ValidationTrace P) : Float

現時点の信頼度を取得する。

Equations

• t.currentLevel = t.current.confidenceLevel

def VerifiedMBSE.VV.ValidationTrace.isTrusted {P : Prop} (t : ValidationTrace P) : Bool

現時点の根拠が .trusted かを判定する（構造子一致）。

Equations

• t.isTrusted = t.current.isTrusted

def VerifiedMBSE.VV.ValidationTrace.hasBeenPromoted {P : Prop} (t : ValidationTrace P) : Bool

trace が昇格済みかを判定する。

Equations

• t.hasBeenPromoted = !t.history.isEmpty

structure VerifiedMBSE.VV.VVRecord : Type

VVRecord: 単一の設計項目に対する完全な V&V レコード。

• layer : Layer
• spec_name : String
• verification : Prop
• verified : self.verification
• validation : ValidationTrace self.verification

structure VerifiedMBSE.VV.IOValidationSource (P : Prop) : Type

IOValidationSource: IO から得られた検証根拠。

• source_description : String
• declaration : P

def VerifiedMBSE.VV.fromIOValidation {P : Prop} (src : IOValidationSource P) : ValidationEvidence P

IO 由来の Trusted ValidationEvidence を構築する。

Equations

• VerifiedMBSE.VV.fromIOValidation src = VerifiedMBSE.VV.ValidationEvidence.trusted ⋯

theorem VerifiedMBSE.VV.trusted_is_full_confidence {P : Prop} (h : P) : (ValidationEvidence.trusted h).confidenceLevel = 1.0

trusted の confidenceLevel は 1.0。

theorem VerifiedMBSE.VV.trusted_isTrusted {P : Prop} (h : P) : (ValidationEvidence.trusted h).isTrusted = true

trusted は isTrusted を true にする。

theorem VerifiedMBSE.VV.confidence_not_isTrusted {P : Prop} (p : Float) : (ValidationEvidence.confidence p).isTrusted = false

confidence は isTrusted を true にしない。

theorem VerifiedMBSE.VV.contract_not_isTrusted {P : Prop} (a : Prop) (ev : a → P) : (ValidationEvidence.contract a ev).isTrusted = false

contract は isTrusted を true にしない。

theorem VerifiedMBSE.VV.promote_extends_history {P : Prop} (t : ValidationTrace P) (next : ValidationEvidence P) : (t.promote next).history.length = t.history.length + 1

promote は履歴を 1 つ増やす。