SubSystemVVBundle: Automated VVRecord Construction

Defines mkComponentRecord and SubSystemVVBundle, which batch-construct VVRecords from a SubSystemSpec.

Because SubSystemSpec is parameterized over [ToKripke α S D] {x : α}, SubSystemVVBundle inherits the same parameterization and covers both StateMachine and ProductStateMachine cases through one uniform type.

def VerifiedMBSE.VV.mkComponentRecord (subsysName : String) (idx : ℕ) (pd : Core.PartDef) (proof : pd.invariant) : VVRecord

Helper to construct a component-level VVRecord.

Equations

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

structure VerifiedMBSE.VV.SubSystemVVBundle {α S D : Type} [Behavior.ToKripke α S D] {x : α} (spec : SubSystemSpec x) : Type

SubSystemVVBundle: bundle of VVRecords constructed from a SubSystemSpec.

The implicit parameters {α : Type} {S D : Type} [ToKripke α S D] {x : α} mirror those of SubSystemSpec, so the bundle applies uniformly to both StateMachine-based and ProductStateMachine-based subsystem specifications.

• componentRecords : List VVRecord

  List of component-level VVRecords

• extraSystemRecords : List VVRecord

  Additional system-level VVRecords (e.g. power budget)

def VerifiedMBSE.VV.SubSystemVVBundle.allRecords {α S D : Type} [Behavior.ToKripke α S D] {x : α} {spec : SubSystemSpec x} (bundle : SubSystemVVBundle spec) : List VVRecord

Get all VVRecords.

Equations

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

theorem VerifiedMBSE.VV.SubSystemVVBundle.allRecords_length {α S D : Type} [Behavior.ToKripke α S D] {x : α} {spec : SubSystemSpec x} (bundle : SubSystemVVBundle spec) : bundle.allRecords.length = bundle.componentRecords.length + 3 + bundle.extraSystemRecords.length

Theorem on VVRecord count.