Writing Static Semantics Rules

Static semantics defines what it means for a Nano-P4 program to be well-typed. Before a program runs, the type checker walks through every declaration, statement, and expression to verify that types are used consistently and that names refer to things that actually exist.

In this chapter, we read through the static semantics specification of Nano-P4 piece by piece. Rather than building the spec from scratch, we take a functioning spec apart and understand what it means. There are curated exercises at the end of every section where you debug or extend a faulty version of the spec. Each section explains what a piece of the spec says, why it is written that way, and how it connects to the P4-SpecTec constructs you saw in the previous chapter.

By the end of this chapter, the full type-checking relation for an entire program is:

relation Program_ok:
  |- program -| typingContext
  hint(input %0)

Program_ok takes a program as input and, if the program is well-typed, produces a typingContext as output; otherwise it fails.

In this chapter

• Typing Context: the data structures that hold type information as the checker walks the program
• Types: rules for validating type expressions and checking type equality
• Expressions and L-values: how the type of an expression is derived from its parts, and how assignable locations are checked
• Statements: how statements are checked and how variable declarations extend the context
• Parameters and Arguments: how function signatures are elaborated and how call sites are validated against them
• Declarations: how top-level declarations such as actions, externs, type definitions, parsers, and controls are checked and registered
• Parser Block: how parser local declarations and parser states are type-checked
• Control Block: how control local declarations are type-checked
• Tables: how table keys, action lists, and constant entries are validated