VColumn: A Single Column of the V-Matrix

Defines the subsystem identifier, the VColumn structure, per-layer filters, and the Complete predicate.

structure VerifiedMBSE.Matrix.VColumn : Type

One V-matrix column, corresponding to a single subsystem.

subsystem is stored as a String to avoid committing to a domain-specific enumeration.

• subsystem : String
• records : List VV.VVRecord

def VerifiedMBSE.Matrix.VColumn.atLayer (col : VColumn) (l : VV.Layer) : List VV.VVRecord

VVRecords in this column at the given layer.

Equations

• col.atLayer l = List.filter (fun (r : VerifiedMBSE.VV.VVRecord) => r.layer == l) col.records

def VerifiedMBSE.Matrix.VColumn.hasLayer (col : VColumn) (l : VV.Layer) : Bool

Whether the column has at least one VVRecord at the given layer.

Equations

• col.hasLayer l = !(col.atLayer l).isEmpty

def VerifiedMBSE.Matrix.VColumn.allLayersCovered (col : VColumn) : Bool

Whether the column covers the system / subsystem / component layers.

Equations

• col.allLayersCovered = (col.hasLayer VerifiedMBSE.VV.Layer.system && col.hasLayer VerifiedMBSE.VV.Layer.subsystem && col.hasLayer VerifiedMBSE.VV.Layer.component)

def VerifiedMBSE.Matrix.VColumn.Complete (col : VColumn) : Prop

Column completeness: at least one VVRecord exists at each of the system / subsystem / component layers.

Equations

• col.Complete = ((col.atLayer VerifiedMBSE.VV.Layer.system).length > 0 ∧ (col.atLayer VerifiedMBSE.VV.Layer.subsystem).length > 0 ∧ (col.atLayer VerifiedMBSE.VV.Layer.component).length > 0)

def VerifiedMBSE.Matrix.VColumn.fullyTrusted (col : VColumn) : Bool

Whether every record in the column is .trusted (constructor match).

The check uses the structural ValidationTrace.isTrusted constructor-based discriminator rather than an equality against 1.0, avoiding IEEE 754 float equality. A column that mixes .trusted with any other evidence constructor returns false.

Equations

• col.fullyTrusted = col.records.all fun (r : VerifiedMBSE.VV.VVRecord) => r.validation.isTrusted

def VerifiedMBSE.Matrix.VColumn.merge (c1 c2 : VColumn) : c1.subsystem = c2.subsystem → VColumn

Merge two columns that refer to the same subsystem.

Equations

• c1.merge c2 x✝ = { subsystem := c1.subsystem, records := c1.records ++ c2.records }