theorem CapabilityRoute.mk.sizeOf_spec
theorem CapabilityRoute.mk.sizeOf_spec
: ∀ (sourceNodeId recipientNodeId capabilityId recipientInterfaceId contextUnits : Nat)
  (interfaceCompatible sufficientContext provenancePresent localValidationPassed : Bool)
  (recipientCorrectionWork validatedUses validatedReuseCount : Nat),
  sizeOf
      (e50am64c.CapabilityRoute.mk sourceNodeId recipientNodeId capabilityId recipientInterfaceId contextUnits
        interfaceCompatible sufficientContext provenancePresent localValidationPassed recipientCorrectionWork
        validatedUses validatedReuseCount) =
    1 + sizeOf sourceNodeId + sizeOf recipientNodeId + sizeOf capabilityId + sizeOf recipientInterfaceId +
                    sizeOf contextUnits +
                  sizeOf interfaceCompatible +
                sizeOf sufficientContext +
              sizeOf provenancePresent +
            sizeOf localValidationPassed +
          sizeOf recipientCorrectionWork +
        sizeOf validatedUses +
      sizeOf validatedReuseCount