Inter-Layer V&V Propagation

Defines Layer.supports (an inclusion relation between layers) and LayerPropagation (transitive propagation of V&V results from a lower layer to an upper layer).

Depth-based supports

Layer.supports l1 l2 is defined as l1.depth > l2.depth:

Layer.supports l1 l2 ⟺ l1.depth > l2.depth

A single depth comparison gives the relation uniformly across all eight layers. supports_trans and supports_irrefl are proved once via the corresponding properties of Nat.lt, with no per-layer case analysis.

def VerifiedMBSE.VV.Layer.supports (l1 l2 : Layer) : Prop

Layer inclusion: a lower layer "supports" an upper layer.

Defined by depth comparison: when l1.depth > l2.depth, l1 is lower (more decomposed) and supports the V&V of the upper layer l2.

Equations

• l1.supports l2 = (l1.depth > l2.depth)

@[implicit_reducible]

instance VerifiedMBSE.VV.instDecidableSupports (l1 l2 : Layer) : Decidable (l1.supports l2)

supports is decidable via Nat.lt.

Equations

• VerifiedMBSE.VV.instDecidableSupports l1 l2 = l2.depth.decLt l1.depth

theorem VerifiedMBSE.VV.Layer.supports_trans {l1 l2 l3 : Layer} (h12 : l1.supports l2) (h23 : l2.supports l3) : l1.supports l3

supports is transitive, inherited from Nat.lt.

theorem VerifiedMBSE.VV.Layer.supports_irrefl (l : Layer) : ¬l.supports l

supports is irreflexive, inherited from Nat.lt.

structure VerifiedMBSE.VV.LayerPropagation : Type

LayerPropagation: relation where lower-layer V&V implies upper-layer V&V.

• lower_layer : Layer
• upper_layer : Layer
• supports : self.lower_layer.supports self.upper_layer
• lower_prop : Prop
• upper_prop : Prop
• propagates : self.lower_prop → self.upper_prop

def VerifiedMBSE.VV.LayerPropagation.compose (lp1 lp2 : LayerPropagation) (hchain : lp1.upper_prop → lp2.lower_prop) (hsup : lp1.lower_layer.supports lp2.upper_layer) : LayerPropagation

Composition of transitive propagation.

Equations

• lp1.compose lp2 hchain hsup = { lower_layer := lp1.lower_layer, upper_layer := lp2.upper_layer, supports := hsup, lower_prop := lp1.lower_prop, upper_prop := lp2.upper_prop, propagates := ⋯ }

theorem VerifiedMBSE.VV.trusted_gives_full_confidence (r : VVRecord) (h : r.validation.current = ValidationEvidence.trusted ⋯) : r.validation.currentLevel = 1.0

If all VVRecord validations are trusted, then currentLevel = 1.0.