From 6453f0876458d016a02a869bef12e110e14a6896 Mon Sep 17 00:00:00 2001
From: Dev-next-gen <leo.camus23@gmail.com>
Date: Fri, 30 Oct 2026 17:57:59 +0000
Subject: [PATCH] Check that commands, events, parameters, and telemetry fit in
 framework buffers

F Prime serializes command arguments, event arguments, parameter values,
and telemetry values into fixed-size buffers (FW_CMD_ARG_BUFFER_MAX_SIZE,
FW_LOG_BUFFER_MAX_SIZE, FW_PARAM_BUFFER_MAX_SIZE, FW_TLM_BUFFER_MAX_SIZE).
When a definition does not fit, the model passes every check, the C++
compiles, and the generated code fails an FW_ASSERT at run time, or the
command cannot be carried at all. See #679.

These buffer sizes are now framework constants, so the analyzer can check
them. When a buffer size constant is defined, check that the minimum
serialized size of each command's parameters, each event's parameters,
each parameter, and each telemetry channel fits in the buffer. The minimum
size counts every string as empty, so the check reports an error only
when no value can fit. A model in which some values fit and others do
not, which F Prime handles at run time, is still valid; in particular
the default F Prime configuration passes.

In an F Prime build, each module is analyzed with only its dependencies.
Make commands, events, parameters, and telemetry channels depend on the
buffer size constants when they have location specifiers, so the check
runs there too. The constants stay optional: a model that does not define
them is not checked.
---
 .../CheckSemantics/CheckComponentDefs.scala   |   1 +
 .../CheckFrameworkBufferSizes.scala           | 148 ++++++++++++++++++
 .../ComputeDependencies/AddDependencies.scala |  50 ++++++
 compiler/lib/src/main/scala/util/Error.scala  |  15 ++
 .../fpp-check/test/command/buffer_size_ok.fpp |  22 +++
 .../test/command/buffer_size_ok.ref.txt       |   0
 .../test/command/buffer_size_too_large.fpp    |  21 +++
 .../command/buffer_size_too_large.ref.txt     |   9 ++
 .../tools/fpp-check/test/command/tests.sh     |   2 +
 .../fpp-check/test/event/buffer_size_ok.fpp   |  24 +++
 .../test/event/buffer_size_ok.ref.txt         |   0
 .../event/buffer_size_string_in_struct.fpp    |  26 +++
 .../buffer_size_string_in_struct.ref.txt      |   9 ++
 .../test/event/buffer_size_too_large.fpp      |  21 +++
 .../test/event/buffer_size_too_large.ref.txt  |   9 ++
 compiler/tools/fpp-check/test/event/tests.sh  |   3 +
 .../fpp-check/test/param/buffer_size_ok.fpp   |  28 ++++
 .../test/param/buffer_size_ok.ref.txt         |   0
 .../test/param/buffer_size_too_large.fpp      |  27 ++++
 .../test/param/buffer_size_too_large.ref.txt  |   9 ++
 compiler/tools/fpp-check/test/param/tests.sh  |   2 +
 .../test/tlm_channel/buffer_size_ok.fpp       |  20 +++
 .../test/tlm_channel/buffer_size_ok.ref.txt   |   0
 .../tlm_channel/buffer_size_too_large.fpp     |  19 +++
 .../tlm_channel/buffer_size_too_large.ref.txt |   9 ++
 .../tools/fpp-check/test/tlm_channel/tests.sh |   2 +
 .../test/framework_buffer_sizes.fpp           |  16 ++
 .../test/framework_buffer_sizes.ref.txt       |   4 +
 compiler/tools/fpp-depend/test/tests.sh       |   1 +
 .../Definitions/Framework-Definitions.adoc    |  59 +++++++
 docs/spec/Specifiers/Command-Specifiers.adoc  |   2 +
 docs/spec/Specifiers/Event-Specifiers.adoc    |   2 +
 .../spec/Specifiers/Parameter-Specifiers.adoc |   2 +
 .../Telemetry-Channel-Specifiers.adoc         |   2 +
 docs/users-guide/Defining-Constants.adoc      |  44 ++++++
 35 files changed, 608 insertions(+)
 create mode 100644 compiler/lib/src/main/scala/analysis/CheckSemantics/CheckFrameworkBufferSizes.scala
 create mode 100644 compiler/tools/fpp-check/test/command/buffer_size_ok.fpp
 create mode 100644 compiler/tools/fpp-check/test/command/buffer_size_ok.ref.txt
 create mode 100644 compiler/tools/fpp-check/test/command/buffer_size_too_large.fpp
 create mode 100644 compiler/tools/fpp-check/test/command/buffer_size_too_large.ref.txt
 create mode 100644 compiler/tools/fpp-check/test/event/buffer_size_ok.fpp
 create mode 100644 compiler/tools/fpp-check/test/event/buffer_size_ok.ref.txt
 create mode 100644 compiler/tools/fpp-check/test/event/buffer_size_string_in_struct.fpp
 create mode 100644 compiler/tools/fpp-check/test/event/buffer_size_string_in_struct.ref.txt
 create mode 100644 compiler/tools/fpp-check/test/event/buffer_size_too_large.fpp
 create mode 100644 compiler/tools/fpp-check/test/event/buffer_size_too_large.ref.txt
 create mode 100644 compiler/tools/fpp-check/test/param/buffer_size_ok.fpp
 create mode 100644 compiler/tools/fpp-check/test/param/buffer_size_ok.ref.txt
 create mode 100644 compiler/tools/fpp-check/test/param/buffer_size_too_large.fpp
 create mode 100644 compiler/tools/fpp-check/test/param/buffer_size_too_large.ref.txt
 create mode 100644 compiler/tools/fpp-check/test/tlm_channel/buffer_size_ok.fpp
 create mode 100644 compiler/tools/fpp-check/test/tlm_channel/buffer_size_ok.ref.txt
 create mode 100644 compiler/tools/fpp-check/test/tlm_channel/buffer_size_too_large.fpp
 create mode 100644 compiler/tools/fpp-check/test/tlm_channel/buffer_size_too_large.ref.txt
 create mode 100644 compiler/tools/fpp-depend/test/framework_buffer_sizes.fpp
 create mode 100644 compiler/tools/fpp-depend/test/framework_buffer_sizes.ref.txt

diff --git a/compiler/lib/src/main/scala/analysis/CheckSemantics/CheckComponentDefs.scala b/compiler/lib/src/main/scala/analysis/CheckSemantics/CheckComponentDefs.scala
index aba2d0a269..7d2fb4f9c4 100644
--- a/compiler/lib/src/main/scala/analysis/CheckSemantics/CheckComponentDefs.scala
+++ b/compiler/lib/src/main/scala/analysis/CheckSemantics/CheckComponentDefs.scala
@@ -18,6 +18,7 @@ object CheckComponentDefs
     for {
       a <- super.defComponentAnnotatedNode(a1, aNode)
       c <- a.component.get.complete
+      _ <- CheckFrameworkBufferSizes.component(a, c)
     }
     yield {
       val symbol = Symbol.Component(aNode)
diff --git a/compiler/lib/src/main/scala/analysis/CheckSemantics/CheckFrameworkBufferSizes.scala b/compiler/lib/src/main/scala/analysis/CheckSemantics/CheckFrameworkBufferSizes.scala
new file mode 100644
index 0000000000..e9d6ab62bf
--- /dev/null
+++ b/compiler/lib/src/main/scala/analysis/CheckSemantics/CheckFrameworkBufferSizes.scala
@@ -0,0 +1,148 @@
+package fpp.compiler.analysis
+
+import fpp.compiler.ast._
+import fpp.compiler.util._
+
+/** Check that the commands, events, telemetry channels, and parameters
+ *  of a component fit in the F Prime framework buffers that carry them */
+object CheckFrameworkBufferSizes {
+
+  /** A framework buffer, given by the framework constant that specifies
+   *  its size */
+  case class Buffer(sizeName: String)
+
+  /** The buffer that carries the arguments of a command */
+  val cmdArgBuffer = Buffer("FW_CMD_ARG_BUFFER_MAX_SIZE")
+
+  /** The buffer that carries the arguments of an event */
+  val logBuffer = Buffer("FW_LOG_BUFFER_MAX_SIZE")
+
+  /** The buffer that carries the value of a parameter */
+  val paramBuffer = Buffer("FW_PARAM_BUFFER_MAX_SIZE")
+
+  /** The buffer that carries the value of a telemetry channel */
+  val tlmBuffer = Buffer("FW_TLM_BUFFER_MAX_SIZE")
+
+  /** Check a component */
+  def component(a: Analysis, c: Component): Result.Result[Unit] =
+    for {
+      _ <- Result.foldLeft (sortById(c.commandMap)) (()) ((_, command) =>
+        command match {
+          case command: Command.NonParam =>
+            val data = command.aNode._2.data
+            checkSize(
+              a,
+              command.getLoc,
+              s"arguments of command ${command.getName}",
+              data.params.map(aNode => a.typeMap(aNode._2.data.typeName.id)),
+              cmdArgBuffer
+            )
+          case _: Command.Param => Right(())
+        }
+      )
+      _ <- Result.foldLeft (sortById(c.eventMap)) (()) ((_, event) =>
+        checkSize(
+          a,
+          event.getLoc,
+          s"arguments of event ${event.getName}",
+          event.aNode._2.data.params.map(
+            aNode => a.typeMap(aNode._2.data.typeName.id)
+          ),
+          logBuffer
+        )
+      )
+      _ <- Result.foldLeft (sortById(c.tlmChannelMap)) (()) ((_, channel) =>
+        checkSize(
+          a,
+          channel.getLoc,
+          s"value of telemetry channel ${channel.getName}",
+          List(channel.channelType),
+          tlmBuffer
+        )
+      )
+      _ <- Result.foldLeft (sortById(c.paramMap)) (()) ((_, param) =>
+        checkSize(
+          a,
+          param.getLoc,
+          s"value of parameter ${param.getName}",
+          List(param.paramType),
+          paramBuffer
+        )
+      )
+    } yield ()
+
+  /** Check that values of the types ts, serialized in sequence,
+   *  can fit in a framework buffer. If the buffer size constant is not
+   *  defined, there is nothing to check. The check uses the minimum
+   *  serialized size, in which every string is empty: it reports an
+   *  error only when no value of the types can fit in the buffer. */
+  private def checkSize(
+    a: Analysis,
+    loc: Location,
+    msg: String,
+    ts: List[Type],
+    buffer: Buffer
+  ): Result.Result[Unit] =
+    getFrameworkConstant(a, buffer.sizeName) match {
+      case None => Right(())
+      case Some((bufferSymbol, bufferSize)) =>
+        val sizeOpt = ts.foldLeft (Some(BigInt(0)): Option[BigInt]) ((sizeOpt, t) =>
+          for {
+            s1 <- sizeOpt
+            s2 <- getMinSerializedSize(a, t)
+          } yield s1 + s2
+        )
+        sizeOpt match {
+          case Some(size) if size > bufferSize =>
+            Left(
+              SemanticError.SerializedSizeTooLarge(
+                loc,
+                msg,
+                size,
+                buffer.sizeName,
+                bufferSize,
+                Locations.get(bufferSymbol.getNodeId)
+              )
+            )
+          case _ => Right(())
+        }
+    }
+
+  /** Get the minimum serialized size of a value of type t.
+   *  A string value is serialized as its length followed by its
+   *  characters, so its minimum size is the size of its length. */
+  private def getMinSerializedSize(a: Analysis, t: Type): Option[BigInt] =
+    t.getUnderlyingType match {
+      case _: Type.String => Some(getStringLengthSize(a))
+      case t: Type.Array =>
+        val n = BigInt(t.getArraySize.get)
+        getMinSerializedSize(a, t.anonArray.eltType).map(n * _)
+      case t: Type.Struct =>
+        t.anonStruct.members.foldLeft (Some(BigInt(0)): Option[BigInt]) {
+          case (sizeOpt, (m, t1)) =>
+            for {
+              s1 <- sizeOpt
+              s2 <- getMinSerializedSize(a, t1)
+            } yield s1 + s2 * t.sizes.getOrElse(m, 1)
+        }
+      case t => Type.SerializedSize.ty(a, t)
+    }
+
+  /** Get the serialized size of the length of a string */
+  private def getStringLengthSize(a: Analysis): BigInt = {
+    val symbol = a.frameworkDefinitions.typeMap("FwSizeStoreType")
+    Type.SerializedSize.ty(a, a.typeMap(symbol.getNodeId)).get
+  }
+
+  /** Get a framework constant and its value, if it is defined */
+  private def getFrameworkConstant(a: Analysis, name: String):
+    Option[(Symbol.Constant, BigInt)] =
+    a.frameworkDefinitions.constantMap.get(name).map(
+      symbol => (symbol, a.getBigIntValue(symbol.getNodeId))
+    )
+
+  /** Get the values of a map in order of their identifiers */
+  private def sortById[T](map: Map[BigInt, T]): List[T] =
+    map.toList.sortBy(_._1).map(_._2)
+
+}
diff --git a/compiler/lib/src/main/scala/analysis/ComputeDependencies/AddDependencies.scala b/compiler/lib/src/main/scala/analysis/ComputeDependencies/AddDependencies.scala
index cd769f4246..1cfd950dac 100644
--- a/compiler/lib/src/main/scala/analysis/ComputeDependencies/AddDependencies.scala
+++ b/compiler/lib/src/main/scala/analysis/ComputeDependencies/AddDependencies.scala
@@ -52,6 +52,42 @@ object AddDependencies
     } yield a
   }
 
+  override def specCommandAnnotatedNode(
+    a: Analysis,
+    node: Ast.Annotated[AstNode[Ast.SpecCommand]]
+  ) =
+    for {
+      a <- super.specCommandAnnotatedNode(a, node)
+      a <- frameworkBufferUses(a, CheckFrameworkBufferSizes.cmdArgBuffer)
+    } yield a
+
+  override def specEventAnnotatedNode(
+    a: Analysis,
+    node: Ast.Annotated[AstNode[Ast.SpecEvent]]
+  ) =
+    for {
+      a <- super.specEventAnnotatedNode(a, node)
+      a <- frameworkBufferUses(a, CheckFrameworkBufferSizes.logBuffer)
+    } yield a
+
+  override def specParamAnnotatedNode(
+    a: Analysis,
+    node: Ast.Annotated[AstNode[Ast.SpecParam]]
+  ) =
+    for {
+      a <- super.specParamAnnotatedNode(a, node)
+      a <- frameworkBufferUses(a, CheckFrameworkBufferSizes.paramBuffer)
+    } yield a
+
+  override def specTlmChannelAnnotatedNode(
+    a: Analysis,
+    node: Ast.Annotated[AstNode[Ast.SpecTlmChannel]]
+  ) =
+    for {
+      a <- super.specTlmChannelAnnotatedNode(a, node)
+      a <- frameworkBufferUses(a, CheckFrameworkBufferSizes.tlmBuffer)
+    } yield a
+
   override def stateMachineUse(a: Analysis, node: AstNode[Ast.QualIdent], use: Name.Qualified) =
     analyzeUse(a, Ast.SpecLoc.StateMachine, use, node.data.isAbsolute)
 
@@ -142,6 +178,20 @@ object AddDependencies
       isAbsolute
     ).map(addDependencies (a)).getOrElse(Right(a))
 
+  /** Add a dependency for the framework constant that specifies the size
+   *  of a framework buffer. The constant is optional: if it has no
+   *  location specifier, then there is no dependency. */
+  private def frameworkBufferUses(
+    a: Analysis,
+    buffer: CheckFrameworkBufferSizes.Buffer
+  ): Result =
+    analyzeUse(
+      a,
+      Ast.SpecLoc.Constant,
+      Name.Qualified.fromIdentList(List(buffer.sizeName)),
+      true
+    )
+
   private def addDependenciesForFile(a: Analysis, file: File): Result =
     val scopeNameList = a.scopeNameList
     val result = for {
diff --git a/compiler/lib/src/main/scala/util/Error.scala b/compiler/lib/src/main/scala/util/Error.scala
index 01f2858e31..a3df464478 100644
--- a/compiler/lib/src/main/scala/util/Error.scala
+++ b/compiler/lib/src/main/scala/util/Error.scala
@@ -339,6 +339,12 @@ sealed trait Error {
         Error.print (Some(loc)) (s"redefinition of symbol ${name}")
         System.err.println("previous definition is here:")
         System.err.println(prevLoc)
+      case SemanticError.SerializedSizeTooLarge(loc, msg, size, constName, constSize, constLoc) =>
+        Error.print (Some(loc)) (
+          s"$msg: at least $size bytes are required, but $constName is $constSize bytes"
+        )
+        System.err.println(s"$constName is defined here:")
+        System.err.println(constLoc)
       case SemanticError.StateMachine.CallSiteTypeMismatch(
         loc,
         teKind,
@@ -839,6 +845,15 @@ object SemanticError {
     loc: Location,
     prevLoc: Location
   ) extends Error
+  /** Serialized size too large for a framework buffer */
+  final case class SerializedSizeTooLarge(
+    loc: Location,
+    msg: String,
+    size: BigInt,
+    constName: String,
+    constSize: BigInt,
+    constLoc: Location
+  ) extends Error
   /** State machine semantic errors */
   object StateMachine {
     /** Call site type mismatch */
diff --git a/compiler/tools/fpp-check/test/command/buffer_size_ok.fpp b/compiler/tools/fpp-check/test/command/buffer_size_ok.fpp
new file mode 100644
index 0000000000..b992fa9342
--- /dev/null
+++ b/compiler/tools/fpp-check/test/command/buffer_size_ok.fpp
@@ -0,0 +1,22 @@
+type FwSizeStoreType = U16
+
+constant FW_CMD_ARG_BUFFER_MAX_SIZE = 6
+
+module Fw {
+
+  port Cmd
+  port CmdReg
+  port CmdResponse
+
+}
+
+passive component C {
+
+  command recv port cmdIn
+  command reg port cmdRegOut
+  command resp port cmdResponseOut
+
+  @ 4 bytes for x, plus at least 2 bytes for s
+  sync command C(x: U32, s: string size 100)
+
+}
diff --git a/compiler/tools/fpp-check/test/command/buffer_size_ok.ref.txt b/compiler/tools/fpp-check/test/command/buffer_size_ok.ref.txt
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/compiler/tools/fpp-check/test/command/buffer_size_too_large.fpp b/compiler/tools/fpp-check/test/command/buffer_size_too_large.fpp
new file mode 100644
index 0000000000..43b853966d
--- /dev/null
+++ b/compiler/tools/fpp-check/test/command/buffer_size_too_large.fpp
@@ -0,0 +1,21 @@
+constant FW_CMD_ARG_BUFFER_MAX_SIZE = 8
+
+module Fw {
+
+  port Cmd
+  port CmdReg
+  port CmdResponse
+
+}
+
+array A = [3] U32
+
+passive component C {
+
+  command recv port cmdIn
+  command reg port cmdRegOut
+  command resp port cmdResponseOut
+
+  sync command C(a: A)
+
+}
diff --git a/compiler/tools/fpp-check/test/command/buffer_size_too_large.ref.txt b/compiler/tools/fpp-check/test/command/buffer_size_too_large.ref.txt
new file mode 100644
index 0000000000..3111a835ac
--- /dev/null
+++ b/compiler/tools/fpp-check/test/command/buffer_size_too_large.ref.txt
@@ -0,0 +1,9 @@
+fpp-check
+[ local path prefix ]/compiler/tools/fpp-check/test/command/buffer_size_too_large.fpp:19.3
+  sync command C(a: A)
+  ^
+error: arguments of command C: at least 12 bytes are required, but FW_CMD_ARG_BUFFER_MAX_SIZE is 8 bytes
+FW_CMD_ARG_BUFFER_MAX_SIZE is defined here:
+[ local path prefix ]/compiler/tools/fpp-check/test/command/buffer_size_too_large.fpp:1.1
+constant FW_CMD_ARG_BUFFER_MAX_SIZE = 8
+^
diff --git a/compiler/tools/fpp-check/test/command/tests.sh b/compiler/tools/fpp-check/test/command/tests.sh
index 70bed34fe2..d355f7a94b 100644
--- a/compiler/tools/fpp-check/test/command/tests.sh
+++ b/compiler/tools/fpp-check/test/command/tests.sh
@@ -2,6 +2,8 @@ tests="
 async_passive
 bad_opcode
 bad_priority
+buffer_size_ok
+buffer_size_too_large
 duplicate_name
 duplicate_name_param_save
 duplicate_name_param_set
diff --git a/compiler/tools/fpp-check/test/event/buffer_size_ok.fpp b/compiler/tools/fpp-check/test/event/buffer_size_ok.fpp
new file mode 100644
index 0000000000..c476bc3b09
--- /dev/null
+++ b/compiler/tools/fpp-check/test/event/buffer_size_ok.fpp
@@ -0,0 +1,24 @@
+type FwSizeStoreType = U16
+
+constant FW_LOG_BUFFER_MAX_SIZE = 6
+
+module Fw {
+
+  port Log
+  port LogText
+  port Time
+
+}
+
+passive component C {
+
+  event port eventOut
+  text event port textEventOut
+  time get port timeGetOut
+
+  @ 4 bytes for x, plus at least 2 bytes for s
+  event E(x: U32, s: string size 100) \
+    severity activity low \
+    format "{} {}"
+
+}
diff --git a/compiler/tools/fpp-check/test/event/buffer_size_ok.ref.txt b/compiler/tools/fpp-check/test/event/buffer_size_ok.ref.txt
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/compiler/tools/fpp-check/test/event/buffer_size_string_in_struct.fpp b/compiler/tools/fpp-check/test/event/buffer_size_string_in_struct.fpp
new file mode 100644
index 0000000000..cecbceaa08
--- /dev/null
+++ b/compiler/tools/fpp-check/test/event/buffer_size_string_in_struct.fpp
@@ -0,0 +1,26 @@
+type FwSizeStoreType = U16
+
+constant FW_LOG_BUFFER_MAX_SIZE = 9
+
+module Fw {
+
+  port Log
+  port LogText
+  port Time
+
+}
+
+@ At least 2 bytes for s, plus 8 bytes for x
+struct S { s: string size 100, x: U64 }
+
+passive component C {
+
+  event port eventOut
+  text event port textEventOut
+  time get port timeGetOut
+
+  event E(s: S) \
+    severity activity low \
+    format "{}"
+
+}
diff --git a/compiler/tools/fpp-check/test/event/buffer_size_string_in_struct.ref.txt b/compiler/tools/fpp-check/test/event/buffer_size_string_in_struct.ref.txt
new file mode 100644
index 0000000000..5c632b13bd
--- /dev/null
+++ b/compiler/tools/fpp-check/test/event/buffer_size_string_in_struct.ref.txt
@@ -0,0 +1,9 @@
+fpp-check
+[ local path prefix ]/compiler/tools/fpp-check/test/event/buffer_size_string_in_struct.fpp:22.3
+  event E(s: S) \
+  ^
+error: arguments of event E: at least 10 bytes are required, but FW_LOG_BUFFER_MAX_SIZE is 9 bytes
+FW_LOG_BUFFER_MAX_SIZE is defined here:
+[ local path prefix ]/compiler/tools/fpp-check/test/event/buffer_size_string_in_struct.fpp:3.1
+constant FW_LOG_BUFFER_MAX_SIZE = 9
+^
diff --git a/compiler/tools/fpp-check/test/event/buffer_size_too_large.fpp b/compiler/tools/fpp-check/test/event/buffer_size_too_large.fpp
new file mode 100644
index 0000000000..9705fe962d
--- /dev/null
+++ b/compiler/tools/fpp-check/test/event/buffer_size_too_large.fpp
@@ -0,0 +1,21 @@
+constant FW_LOG_BUFFER_MAX_SIZE = 8
+
+module Fw {
+
+  port Log
+  port LogText
+  port Time
+
+}
+
+passive component C {
+
+  event port eventOut
+  text event port textEventOut
+  time get port timeGetOut
+
+  event E(x: U32, y: U64) \
+    severity activity low \
+    format "{} {}"
+
+}
diff --git a/compiler/tools/fpp-check/test/event/buffer_size_too_large.ref.txt b/compiler/tools/fpp-check/test/event/buffer_size_too_large.ref.txt
new file mode 100644
index 0000000000..1639550f30
--- /dev/null
+++ b/compiler/tools/fpp-check/test/event/buffer_size_too_large.ref.txt
@@ -0,0 +1,9 @@
+fpp-check
+[ local path prefix ]/compiler/tools/fpp-check/test/event/buffer_size_too_large.fpp:17.3
+  event E(x: U32, y: U64) \
+  ^
+error: arguments of event E: at least 12 bytes are required, but FW_LOG_BUFFER_MAX_SIZE is 8 bytes
+FW_LOG_BUFFER_MAX_SIZE is defined here:
+[ local path prefix ]/compiler/tools/fpp-check/test/event/buffer_size_too_large.fpp:1.1
+constant FW_LOG_BUFFER_MAX_SIZE = 8
+^
diff --git a/compiler/tools/fpp-check/test/event/tests.sh b/compiler/tools/fpp-check/test/event/tests.sh
index 8a5fe397a8..c7ba8bfc4f 100644
--- a/compiler/tools/fpp-check/test/event/tests.sh
+++ b/compiler/tools/fpp-check/test/event/tests.sh
@@ -6,6 +6,9 @@ bad_throttle_interval_useconds
 bad_throttle_interval
 bad_throttle_seconds
 bad_throttle
+buffer_size_ok
+buffer_size_string_in_struct
+buffer_size_too_large
 duplicate_id_explicit
 duplicate_id_implicit
 duplicate_name
diff --git a/compiler/tools/fpp-check/test/param/buffer_size_ok.fpp b/compiler/tools/fpp-check/test/param/buffer_size_ok.fpp
new file mode 100644
index 0000000000..512cb159e5
--- /dev/null
+++ b/compiler/tools/fpp-check/test/param/buffer_size_ok.fpp
@@ -0,0 +1,28 @@
+type FwSizeStoreType = U16
+
+constant FW_PARAM_BUFFER_MAX_SIZE = 2
+
+module Fw {
+
+  port Cmd
+  port CmdReg
+  port CmdResponse
+
+  port PrmGet
+  port PrmSet
+
+}
+
+passive component C {
+
+  command recv port cmdIn
+  command reg port cmdRegOut
+  command resp port cmdResponseOut
+
+  param get port prmGetOut
+  param set port prmSetOut
+
+  @ At least 2 bytes, for an empty string
+  param P: string size 100
+
+}
diff --git a/compiler/tools/fpp-check/test/param/buffer_size_ok.ref.txt b/compiler/tools/fpp-check/test/param/buffer_size_ok.ref.txt
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/compiler/tools/fpp-check/test/param/buffer_size_too_large.fpp b/compiler/tools/fpp-check/test/param/buffer_size_too_large.fpp
new file mode 100644
index 0000000000..8ccf351055
--- /dev/null
+++ b/compiler/tools/fpp-check/test/param/buffer_size_too_large.fpp
@@ -0,0 +1,27 @@
+constant FW_PARAM_BUFFER_MAX_SIZE = 8
+
+module Fw {
+
+  port Cmd
+  port CmdReg
+  port CmdResponse
+
+  port PrmGet
+  port PrmSet
+
+}
+
+array F64x3 = [3] F64
+
+passive component C {
+
+  command recv port cmdIn
+  command reg port cmdRegOut
+  command resp port cmdResponseOut
+
+  param get port prmGetOut
+  param set port prmSetOut
+
+  param P: F64x3
+
+}
diff --git a/compiler/tools/fpp-check/test/param/buffer_size_too_large.ref.txt b/compiler/tools/fpp-check/test/param/buffer_size_too_large.ref.txt
new file mode 100644
index 0000000000..349fb0e0bc
--- /dev/null
+++ b/compiler/tools/fpp-check/test/param/buffer_size_too_large.ref.txt
@@ -0,0 +1,9 @@
+fpp-check
+[ local path prefix ]/compiler/tools/fpp-check/test/param/buffer_size_too_large.fpp:25.3
+  param P: F64x3
+  ^
+error: value of parameter P: at least 24 bytes are required, but FW_PARAM_BUFFER_MAX_SIZE is 8 bytes
+FW_PARAM_BUFFER_MAX_SIZE is defined here:
+[ local path prefix ]/compiler/tools/fpp-check/test/param/buffer_size_too_large.fpp:1.1
+constant FW_PARAM_BUFFER_MAX_SIZE = 8
+^
diff --git a/compiler/tools/fpp-check/test/param/tests.sh b/compiler/tools/fpp-check/test/param/tests.sh
index 884f7c14eb..d2293da633 100644
--- a/compiler/tools/fpp-check/test/param/tests.sh
+++ b/compiler/tools/fpp-check/test/param/tests.sh
@@ -3,6 +3,8 @@ bad_default
 bad_id
 bad_save_opcode
 bad_set_opcode
+buffer_size_ok
+buffer_size_too_large
 duplicate_id_explicit
 duplicate_id_implicit
 duplicate_name
diff --git a/compiler/tools/fpp-check/test/tlm_channel/buffer_size_ok.fpp b/compiler/tools/fpp-check/test/tlm_channel/buffer_size_ok.fpp
new file mode 100644
index 0000000000..a41dd52a25
--- /dev/null
+++ b/compiler/tools/fpp-check/test/tlm_channel/buffer_size_ok.fpp
@@ -0,0 +1,20 @@
+type FwSizeStoreType = U16
+
+constant FW_TLM_BUFFER_MAX_SIZE = 2
+
+module Fw {
+
+  port Time
+  port Tlm
+
+}
+
+passive component C {
+
+  telemetry port tlmOut
+  time get port timeGetOut
+
+  @ At least 2 bytes, for an empty string
+  telemetry T: string size 100
+
+}
diff --git a/compiler/tools/fpp-check/test/tlm_channel/buffer_size_ok.ref.txt b/compiler/tools/fpp-check/test/tlm_channel/buffer_size_ok.ref.txt
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/compiler/tools/fpp-check/test/tlm_channel/buffer_size_too_large.fpp b/compiler/tools/fpp-check/test/tlm_channel/buffer_size_too_large.fpp
new file mode 100644
index 0000000000..56081b638c
--- /dev/null
+++ b/compiler/tools/fpp-check/test/tlm_channel/buffer_size_too_large.fpp
@@ -0,0 +1,19 @@
+constant FW_TLM_BUFFER_MAX_SIZE = 8
+
+module Fw {
+
+  port Time
+  port Tlm
+
+}
+
+struct S { x: U32, y: F64 }
+
+passive component C {
+
+  telemetry port tlmOut
+  time get port timeGetOut
+
+  telemetry T: S
+
+}
diff --git a/compiler/tools/fpp-check/test/tlm_channel/buffer_size_too_large.ref.txt b/compiler/tools/fpp-check/test/tlm_channel/buffer_size_too_large.ref.txt
new file mode 100644
index 0000000000..206c328d10
--- /dev/null
+++ b/compiler/tools/fpp-check/test/tlm_channel/buffer_size_too_large.ref.txt
@@ -0,0 +1,9 @@
+fpp-check
+[ local path prefix ]/compiler/tools/fpp-check/test/tlm_channel/buffer_size_too_large.fpp:17.3
+  telemetry T: S
+  ^
+error: value of telemetry channel T: at least 12 bytes are required, but FW_TLM_BUFFER_MAX_SIZE is 8 bytes
+FW_TLM_BUFFER_MAX_SIZE is defined here:
+[ local path prefix ]/compiler/tools/fpp-check/test/tlm_channel/buffer_size_too_large.fpp:1.1
+constant FW_TLM_BUFFER_MAX_SIZE = 8
+^
diff --git a/compiler/tools/fpp-check/test/tlm_channel/tests.sh b/compiler/tools/fpp-check/test/tlm_channel/tests.sh
index 9d6eb40e44..25d77bbdcb 100644
--- a/compiler/tools/fpp-check/test/tlm_channel/tests.sh
+++ b/compiler/tools/fpp-check/test/tlm_channel/tests.sh
@@ -1,6 +1,8 @@
 tests="
 bad_id
 bad_limit_type
+buffer_size_ok
+buffer_size_too_large
 duplicate_id_explicit
 duplicate_id_implicit
 duplicate_limit_high
diff --git a/compiler/tools/fpp-depend/test/framework_buffer_sizes.fpp b/compiler/tools/fpp-depend/test/framework_buffer_sizes.fpp
new file mode 100644
index 0000000000..152a8402d0
--- /dev/null
+++ b/compiler/tools/fpp-depend/test/framework_buffer_sizes.fpp
@@ -0,0 +1,16 @@
+locate constant FW_CMD_ARG_BUFFER_MAX_SIZE at "cmd_arg_buffer.fpp"
+locate constant FW_LOG_BUFFER_MAX_SIZE at "log_buffer.fpp"
+locate constant FW_PARAM_BUFFER_MAX_SIZE at "param_buffer.fpp"
+locate constant FW_TLM_BUFFER_MAX_SIZE at "tlm_buffer.fpp"
+
+active component C {
+
+  sync command C
+
+  event E severity activity low format ""
+
+  param P: U32
+
+  telemetry T: U32
+
+}
diff --git a/compiler/tools/fpp-depend/test/framework_buffer_sizes.ref.txt b/compiler/tools/fpp-depend/test/framework_buffer_sizes.ref.txt
new file mode 100644
index 0000000000..42bef84957
--- /dev/null
+++ b/compiler/tools/fpp-depend/test/framework_buffer_sizes.ref.txt
@@ -0,0 +1,4 @@
+[ local path prefix ]/compiler/tools/fpp-depend/test/cmd_arg_buffer.fpp
+[ local path prefix ]/compiler/tools/fpp-depend/test/log_buffer.fpp
+[ local path prefix ]/compiler/tools/fpp-depend/test/param_buffer.fpp
+[ local path prefix ]/compiler/tools/fpp-depend/test/tlm_buffer.fpp
diff --git a/compiler/tools/fpp-depend/test/tests.sh b/compiler/tools/fpp-depend/test/tests.sh
index dec1d36d1d..bcc8b29085 100644
--- a/compiler/tools/fpp-depend/test/tests.sh
+++ b/compiler/tools/fpp-depend/test/tests.sh
@@ -29,6 +29,7 @@ filenames_auto
 filenames_include
 filenames_include_auto
 framework
+framework_buffer_sizes
 framework_include
 include
 included_dep
diff --git a/docs/spec/Definitions/Framework-Definitions.adoc b/docs/spec/Definitions/Framework-Definitions.adoc
index 78e4b416d8..12a3448512 100644
--- a/docs/spec/Definitions/Framework-Definitions.adoc
+++ b/docs/spec/Definitions/Framework-Definitions.adoc
@@ -236,3 +236,62 @@ with the following qualified names:
 * `Fw.Time`
 
 * `Fw.Tlm`
+
+==== Buffer Sizes
+
+The F Prime framework serializes the arguments of commands and
+events and the values of parameters and telemetry channels into
+buffers of fixed size.
+The table below lists the data serialized for each kind of
+<<Specifiers,specifier>> and the framework constant _B_ that specifies the
+size of the buffer.
+
+|===
+|Specifier|Serialized Data|_B_
+
+|<<Specifiers_Command-Specifiers,Command specifier>>
+|The command parameters
+|`FW_CMD_ARG_BUFFER_MAX_SIZE`
+
+|<<Specifiers_Event-Specifiers,Event specifier>>
+|The event parameters
+|`FW_LOG_BUFFER_MAX_SIZE`
+
+|<<Specifiers_Parameter-Specifiers,Parameter specifier>>
+|The parameter value
+|`FW_PARAM_BUFFER_MAX_SIZE`
+
+|<<Specifiers_Telemetry-Channel-Specifiers,Telemetry channel specifier>>
+|The channel value
+|`FW_TLM_BUFFER_MAX_SIZE`
+
+|===
+
+If the model contains a framework constant definition _B_ with value _b_,
+then for each specifier of the corresponding kind,
+the *minimum serialized size* of the serialized data must be at most _b_.
+The minimum serialized size of the serialized data is the sum of the
+minimum serialized sizes of its types, where the minimum serialized size
+of a type _T_ is defined as follows:
+
+* If the <<Types_Underlying-Types,underlying type>> of _T_ is a
+<<Types_String-Types,string type>>, then the minimum serialized size
+of _T_ is the serialized size of the framework type `FwSizeStoreType`.
+This is the size of an empty string.
+
+* If the underlying type of _T_ is an array type with size _n_ and
+element type _T'_, then the minimum serialized size of _T_ is _n_ times
+the minimum serialized size of _T'_.
+
+* If the underlying type of _T_ is a struct type, then the minimum
+serialized size of _T_ is the sum of the minimum serialized sizes of
+its members, where a member with a size _n_ counts _n_ times.
+
+* Otherwise the minimum serialized size of _T_ is the
+<<Types_Serialized-Sizes,serialized size>> of _T_.
+
+So the check reports an error only when no value of the serialized
+data can fit in the buffer.
+The minimum serialized size does not include data that depends on
+the configuration of the F Prime C++ framework, such as the
+argument sizes stored in an event when `FW_AMPCS_COMPATIBLE` is enabled.
diff --git a/docs/spec/Specifiers/Command-Specifiers.adoc b/docs/spec/Specifiers/Command-Specifiers.adoc
index ecccb0958a..fbf455081f 100644
--- a/docs/spec/Specifiers/Command-Specifiers.adoc
+++ b/docs/spec/Specifiers/Command-Specifiers.adoc
@@ -44,6 +44,8 @@ If there are command parameters, each parameter must be
 a <<Types_Displayable-Types,displayable type>>.
 If there are no parameters, the list may be omitted.
 `ref` may not appear in any of the parameters.
+The serialized parameters must fit in the
+<<Definitions_Framework-Definitions_Buffer-Sizes,framework buffer>> for command arguments.
 
 * The optional expression _e_ following `opcode` specifies the numeric
 opcode for the command.
diff --git a/docs/spec/Specifiers/Event-Specifiers.adoc b/docs/spec/Specifiers/Event-Specifiers.adoc
index 5779b5a648..8ff61d4526 100644
--- a/docs/spec/Specifiers/Event-Specifiers.adoc
+++ b/docs/spec/Specifiers/Event-Specifiers.adoc
@@ -49,6 +49,8 @@ If there are event parameters, each parameter must be
 a <<Types_Displayable-Types,displayable type>>.
 If there are no parameters, the list may be omitted.
 `ref` may not appear in any of the parameters.
+The serialized parameters must fit in the
+<<Definitions_Framework-Definitions_Buffer-Sizes,framework buffer>> for event arguments.
 
 * The optional expression _e_ following `id` specifies the numeric
 identifier for instances of the event.
diff --git a/docs/spec/Specifiers/Parameter-Specifiers.adoc b/docs/spec/Specifiers/Parameter-Specifiers.adoc
index 1bcba61ff6..2e16183fab 100644
--- a/docs/spec/Specifiers/Parameter-Specifiers.adoc
+++ b/docs/spec/Specifiers/Parameter-Specifiers.adoc
@@ -35,6 +35,8 @@ access parameter values in an efficient way.
 
 * The type name specifies the type _T_ of the parameter.
 _T_ must be a <<Types_Displayable-Types,displayable type>>.
+A serialized value of type _T_ must fit in the
+<<Definitions_Framework-Definitions_Buffer-Sizes,framework buffer>> for parameter values.
 
 * The optional expression _e_ following the keyword `default`
 specifies a default value for the parameter.
diff --git a/docs/spec/Specifiers/Telemetry-Channel-Specifiers.adoc b/docs/spec/Specifiers/Telemetry-Channel-Specifiers.adoc
index 540fc09b62..7694bd2c88 100644
--- a/docs/spec/Specifiers/Telemetry-Channel-Specifiers.adoc
+++ b/docs/spec/Specifiers/Telemetry-Channel-Specifiers.adoc
@@ -47,6 +47,8 @@ A telemetry limit is one of the following:
 
 . The type name specifies the type _T_ of the telemetry channel.
 _T_ must be a <<Types_Displayable-Types,displayable type>>.
+A serialized value of type _T_ must fit in the
+<<Definitions_Framework-Definitions_Buffer-Sizes,framework buffer>> for telemetry values.
 
 . The optional expression _e_ after the keyword `id` specifies the
 numeric identifier for the channel.
diff --git a/docs/users-guide/Defining-Constants.adoc b/docs/users-guide/Defining-Constants.adoc
index 7a54f8f6c6..c5b72b5e05 100644
--- a/docs/users-guide/Defining-Constants.adoc
+++ b/docs/users-guide/Defining-Constants.adoc
@@ -811,3 +811,47 @@ constant FW_FIXED_LENGTH_STRING_SIZE = "abc"
 ^
 error: the F Prime framework constant FW_FIXED_LENGTH_STRING_SIZE must have an integer type
 ----
+
+The analyzer also uses framework constants to check that
+the commands, events, parameters, and telemetry channels of a
+component fit in the buffers that F Prime uses to carry them.
+For example, `FW_TLM_BUFFER_MAX_SIZE` specifies the size
+of the buffer that carries the value of a telemetry channel.
+If this constant is defined, then the analyzer checks that a
+serialized value of every telemetry channel can fit in the buffer.
+So this model is invalid, because a value of type `A` requires
+16 bytes:
+
+[source,fpp]
+--------
+constant FW_TLM_BUFFER_MAX_SIZE = 8
+
+module Fw {
+
+  port Time
+  port Tlm
+
+}
+
+passive component C {
+
+  telemetry port tlmOut
+  time get port timeGetOut
+
+  array A = [2] F64
+
+  telemetry T: A
+
+}
+--------
+
+A string can be serialized with any length up to its size,
+so the analyzer counts each string as empty.
+It reports an error only when no value can fit in the buffer.
+The rules are spelled out in detail in the
+https://nasa.github.io/fpp/fpp-spec.html#Definitions_Framework-Definitions_Buffer-Sizes[_The
+FPP Language Specification_].
+This check catches at compile time a definition whose serialized size
+always exceeds the buffer, which would otherwise cause a
+run-time assertion failure, for example when a mission reduces
+`FW_COM_BUFFER_MAX_SIZE` to fit a smaller link.