PartDef Semantics and ConnectorSemantic

Defines interpretation-based extent of PartDef, PartInstance (dependent record), semanticSpecializes at the PartDef level, and categorical laws for ConnectorSemantic (associativity, identity).

def VerifiedMBSE.Core.PortInstance (I : Interpretation) (p : PortDef) : Type

PortInstance: instance type of a port under interpretation I.

Equations

• VerifiedMBSE.Core.PortInstance I p = I p.flowType

structure VerifiedMBSE.Core.PartInstance (I : Interpretation) (pd : PartDef) : Type

PartInstance: instance of a PartDef under interpretation I. A dependent record with a carrier value and proof of the invariant.

• carrier : I pd.baseType
• inv_holds : pd.invariant

def VerifiedMBSE.Core.PartDef.extent (I : Interpretation) (pd : PartDef) : Type

Extent of a PartDef: the type of PartInstances.

Equations

• VerifiedMBSE.Core.PartDef.extent I pd = VerifiedMBSE.Core.PartInstance I pd

def VerifiedMBSE.Core.PartDef.semanticSpecializes (I : Interpretation) (pdA pdB : PartDef) : Prop

Semantic specialization at the PartDef level.

Equations

• VerifiedMBSE.Core.PartDef.semanticSpecializes I pdA pdB = ∃ (f : VerifiedMBSE.Core.PartDef.extent I pdA → VerifiedMBSE.Core.PartDef.extent I pdB), Function.Injective f

theorem VerifiedMBSE.Core.PartDef.semanticSpecializes_refl (I : Interpretation) (pd : PartDef) : semanticSpecializes I pd pd

PartDef.semanticSpecializes is reflexive.

theorem VerifiedMBSE.Core.PartDef.semanticSpecializes_trans (I : Interpretation) {pdA pdB pdC : PartDef} (hAB : semanticSpecializes I pdA pdB) (hBC : semanticSpecializes I pdB pdC) : semanticSpecializes I pdA pdC

PartDef.semanticSpecializes is transitive.

def VerifiedMBSE.Core.InvariantInheritance (pdA pdB : PartDef) : Prop

Invariant inheritance relation.

Equations

• VerifiedMBSE.Core.InvariantInheritance pdA pdB = (pdA.invariant → pdB.invariant)

theorem VerifiedMBSE.Core.PartDef.semanticSpecializes_from_base (I : Interpretation) (pdA pdB : PartDef) (hBase : Core.semanticSpecializes I pdA.baseType pdB.baseType) (hInv : InvariantInheritance pdA pdB) : semanticSpecializes I pdA pdB

Derive PartDef-level semanticSpecializes from baseType semanticSpecializes and InvariantInheritance.

theorem VerifiedMBSE.Core.partDef_soundness (I : Interpretation) (hI : InterpretationRespects I) (pdA pdB : PartDef) (hSyn : specializes pdA.baseType pdB.baseType) (hInv : InvariantInheritance pdA pdB) : PartDef.semanticSpecializes I pdA pdB

Soundness theorem at the PartDef level.

def VerifiedMBSE.Core.ConnectorSemantic (I : Interpretation) (c : Connector) : Type

ConnectorSemantic: connector semantics (type of value transfer functions).

Equations

• VerifiedMBSE.Core.ConnectorSemantic I c = (I c.source.port.flowType → I c.target.port.flowType)

def VerifiedMBSE.Core.Connector.Composable (c1 c2 : Connector) : Prop

Serial composability condition.

Equations

• c1.Composable c2 = (c1.target.port.flowType = c2.source.port.flowType)

def VerifiedMBSE.Core.ConnectorSemantic.compose (I : Interpretation) (c1 c2 : Connector) (h : c1.Composable c2) (f1 : ConnectorSemantic I c1) (f2 : ConnectorSemantic I c2) : I c1.source.port.flowType → I c2.target.port.flowType

Serial composition of ConnectorSemantics.

Equations

• VerifiedMBSE.Core.ConnectorSemantic.compose I c1 c2 h f1 f2 v = f2 (h ▸ f1 v)

def VerifiedMBSE.Core.ConnectorSemantic.id_of_eq (I : Interpretation) (c : Connector) (h : c.source.port.flowType = c.target.port.flowType) : ConnectorSemantic I c

Identity ConnectorSemantic (when source and target flowTypes are equal).

Equations

• VerifiedMBSE.Core.ConnectorSemantic.id_of_eq I c h v = h ▸ v

theorem VerifiedMBSE.Core.ConnectorSemantic.compose_assoc (I : Interpretation) (c1 c2 c3 : Connector) (h12 : c1.Composable c2) (h23 : c2.Composable c3) (f1 : ConnectorSemantic I c1) (f2 : ConnectorSemantic I c2) (f3 : ConnectorSemantic I c3) (v : I c1.source.port.flowType) : f3 (h23 ▸ compose I c1 c2 h12 f1 f2 v) = compose I c2 c3 h23 f2 f3 (h12 ▸ f1 v)

Associativity of ConnectorSemantic.

theorem VerifiedMBSE.Core.ConnectorSemantic.compose_id_right (I : Interpretation) (c1 c2 : Connector) (h12 : c1.Composable c2) (heq : c2.source.port.flowType = c2.target.port.flowType) (f : ConnectorSemantic I c1) (v : I c1.source.port.flowType) : compose I c1 c2 h12 f (id_of_eq I c2 heq) v = ⋯ ▸ f v

Right identity law of ConnectorSemantic.

theorem VerifiedMBSE.Core.ConnectorSemantic.compose_id_left (I : Interpretation) (c1 c2 : Connector) (h12 : c1.Composable c2) (heq : c1.source.port.flowType = c1.target.port.flowType) (f : ConnectorSemantic I c2) (v : I c1.source.port.flowType) : compose I c1 c2 h12 (id_of_eq I c1 heq) f v = f (⋯ ▸ v)

Left identity law of ConnectorSemantic.

theorem VerifiedMBSE.Core.ConnectorSemantic.compose_id_left_assoc (I : Interpretation) (c1 c2 c3 : Connector) (h12 : c1.Composable c2) (h23 : c2.Composable c3) (heq : c1.source.port.flowType = c1.target.port.flowType) (f : ConnectorSemantic I c2) (g : ConnectorSemantic I c3) (v : I c1.source.port.flowType) : compose I c2 c3 h23 f g (h12 ▸ id_of_eq I c1 heq v) = compose I c2 c3 h23 f g (⋯ ▸ v)

Corollary: when the leftmost connector in a triple composition is identity.