Mode-Dependent Power Consumption and Power Budget

Defines ModePowerSpec and PowerBudgetOK₂, and derives budget satisfaction across all mode combinations from the sum of per-subsystem max power.

structure VerifiedMBSE.VV.ModePowerSpec (S : Type) : Type

ModePowerSpec: mode-dependent power consumption specification.

• modePower : S → Nat

  Power consumption function per mode

• maxPower : Nat

  Maximum power consumption (max over all modes)

• maxPower_bound (s : S) : self.modePower s ≤ self.maxPower

  maxPower is an upper bound for all modes

def VerifiedMBSE.VV.PowerBudgetOK₂ {S₁ S₂ : Type} (pw₁ : ModePowerSpec S₁) (pw₂ : ModePowerSpec S₂) (budget : Nat) (m₁ : S₁) (m₂ : S₂) : Prop

Proposition that the combined power of two subsystems is within budget.

Equations

• VerifiedMBSE.VV.PowerBudgetOK₂ pw₁ pw₂ budget m₁ m₂ = (pw₁.modePower m₁ + pw₂.modePower m₂ ≤ budget)

theorem VerifiedMBSE.VV.powerBudget₂_from_max {S₁ S₂ : Type} (pw₁ : ModePowerSpec S₁) (pw₂ : ModePowerSpec S₂) (budget : Nat) (h : pw₁.maxPower + pw₂.maxPower ≤ budget) (m₁ : S₁) (m₂ : S₂) : PowerBudgetOK₂ pw₁ pw₂ budget m₁ m₂

If the sum of maxPower values is within budget, then all mode combinations are within budget.