ValidationEvidence: Confidence Levels as Types

Three-tier hierarchy confidence < contract < trusted, a promotion trace recording the history of upgrades, and VVRecord, a uniform representation of one cell of the V model.

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

ValidationEvidence P — the verification evidence for a proposition P, organized as a three-tier hierarchy confidence < contract < trusted.

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

  Confidence: probabilistic evidence (early design, expert heuristics).

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

  Contract: conditional guarantee (after test or simulation).

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

  Trusted: adopted as an axiom (hardware test, approved).

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

Confidence value of an evidence, as a Float (for display or sorting).

This Float result is not suitable for equality comparisons due to rounding. For a "is this trusted?" check, use isTrusted, which is structural on the constructor.

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

Whether the evidence was built with the .trusted constructor.

Structural discrimination that avoids Float equality; consumed by boolean checks such as fullyTrusted.

Equations

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

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

Whether the evidence was built with the .contract constructor.

Equations

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

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

Whether the evidence was built with the .confidence constructor.

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

Promotion: 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

Promotion: Contract → Trusted, given a proof that the assumption of the contract actually holds.

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 P — record of the promotion history together with the current evidence for P.

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

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

Initialize a ValidationTrace with a single piece of evidence and an empty history.

Equations

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

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

Record a promotion step in the trace. The previous current evidence is appended to history, and next becomes the new current.

Equations

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

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

Current confidence value of the trace.

Equations

• t.currentLevel = t.current.confidenceLevel

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

Whether the current evidence is .trusted (constructor match).

Equations

• t.isTrusted = t.current.isTrusted

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

Whether the trace has undergone at least one promotion.

Equations

• t.hasBeenPromoted = !t.history.isEmpty

structure VerifiedMBSE.VV.VVRecord : Type

Complete V&V record for a single design item.

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

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

Validation evidence obtained from IO (e.g. test reports, external certifications).

• source_description : String
• declaration : P

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

Construct a .trusted ValidationEvidence from an IOValidationSource.

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 evidence has a confidence level of 1.0.

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

.trusted evidence satisfies isTrusted.

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

.confidence evidence does not satisfy isTrusted.

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

.contract evidence does not satisfy isTrusted.

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

promote extends the history by exactly one entry.