Overview

This guide walks you through spec mechanization in P4-SpecTec, using its core constructs to describe the semantics of Nano-P4, an educational dialect of P4.

Audience and Scope

Audience. This tutorial is written for the P4 community. It focuses on the practical use of P4-SpecTec for specifying a P4-like language, so a basic familiarity with P4 is recommended. A background in programming-language theory is helpful, but no background in formal methods or proof assistants is required.

What is covered.

• Syntax definition for Nano-P4
• Type-checking and evaluation specifications for Nano-P4
• Prose specification generation
• Hands-on exercises at the end of each section

What is not covered.

• A complete walkthrough of P4-SpecTec. The basics are covered, but P4-SpecTec is treated as a tool throughout, not as the subject of study.
• The full P4 language. Nano-P4 is a deliberately small educational subset, and the tutorial stays within that boundary throughout.

By the end, you will have a full mechanized specification, a reference type checker and interpreter, and natural-language documentation for Nano-P4. Most importantly, you will gain hands-on experience writing a mechanized specification in P4-SpecTec, a skill transferable to any project using the toolchain, including the full P4 language mechanization.

P4-SpecTec

P4-SpecTec is a mechanization toolchain for the P4 programming language. It provides a domain-specific language for writing formal specifications in the form of algorithmic inference rules (Lee et al., 2026).

By writing typing rules with P4-SpecTec, you get a reference type checker. By writing dynamic semantics rules, you get a reference interpreter. The prose backend also generates human-readable documentation from a specification written in P4-SpecTec.

In this chapter

• Installation: how to build and install P4-SpecTec
• Basics: the core syntax and constructs of P4-SpecTec
• Toolchain Pipeline: how the toolchain compiles a spec and a program, then runs one against the other
• Commands: the nano-p4spectec subcommands and their flags
• Standard Library: the built-in utility functions used throughout the spec

Installation

This section shows how to build the nano-p4spectec binary from the P4-SpecTec source. You will use it along with make throughout the tutorial.

Cloning the Repository

$ git clone https://github.com/kaist-plrg/p4-spectec.git
$ cd p4-spectec
$ git checkout gsoc-nano-spec

Note: All exercises and the nano-p4spectec binary used throughout this tutorial are on the gsoc-nano-spec branch. Make sure you are on that branch before building.

Building from Source

Prerequisites

Linux

$ apt-get install opam
$ opam init

macOS

Install opam version 2.0.5 or higher following the instructions at ocaml.org.

You may also need libgmp-dev and pkg-config depending on your system.

NixOS

If you use Nix, a flake.nix is provided that sets up the full development environment automatically:

$ nix develop
$ make release

This drops you into a shell with OCaml 5.1 and all required packages available, without needing to manage opam manually.

OCaml Compiler and Packages

$ opam switch create 5.1.0
$ eval $(opam env)
$ opam install dune bignum 'menhir=20240715' 'menhirLib=20240715' core core_unix bisect_ppx yojson ppx_deriving_yojson

Building

$ make release

This creates the nano-p4spectec executable in the project root.

Basics

P4-SpecTec specifications are written in .watsup files using the P4-SpecTec language. The examples here come from the SpecTecX tutorial, which specifies Typed Imp, a small typed imperative language. Where Typed Imp does not cover a construct, examples from the nano-p4 specification are used.

Comments

Single-line comments start with ;;. Additional semicolons (;;;, ;;;;, …) are used by convention to indicate heading levels in the document structure, but have no semantic difference.

;;--------------------
;; Syntax

;;--- Contexts ---

Primitive Data Types

P4-SpecTec has the following primitive types:

These are the types used in metavariable declarations and function signatures, and are distinct from the types of the object language being specified. For example, INT in the Typed Imp spec is a syntax constructor defined with syntax, not the primitive int of the DSL itself.

Options and Lists

Option types are written by appending ? to a type. The absent case is eps, and a present value is written directly:

dec $lookup<K, V>(map<K, V>, K) : V?

def $lookup<K, V>(eps, K_query) = eps    ;; absent: key not found
def $lookup<K, V>((K_h -> V_h)::_, K_query) = V_h
  -- if K_h = K_query                    ;; present: return the value

An if premise can match on an option result:

rule Check_expr/id:
  tenv |- x : t
  -- if $lookup<id, type>(tenv, x) = t   ;; binds t if present, fails if eps

List types are written by appending * to a type. The empty list is eps, and :: is the cons operator:

syntax map<K,V> = (pair<K,V>)*

Pattern matching on lists follows the same :: notation in def cases:

def $lookup<K, V>(eps, K_query) = eps
def $lookup<K, V>((K_h -> V_h)::(K_t -> V_t)*, K_query) = V_h
  -- if K_h = K_query

A single-element list is written [ x ], and lists are concatenated with ++. Here’s one example from the Nano-P4 spec:

def $flatten_parameterList(parameter) = [ parameter ]
def $flatten_parameterList(nonEmptyParameterList ',' parameter)
  = $flatten_parameterList(nonEmptyParameterList) ++ [ parameter ]

A multi-element list literal [ a, b, c ] is also valid.

Lists also appear in rule conclusions and premises to prepend an entry to a context:

rule Check_command/decl:
  tenv |- (t x '=' e) -| (x -> t)::tenv
  -- Check_expr: tenv |- e : t

Here, (x -> t)::tenv constructs a new typing context with the binding x -> t prepended to tenv.

Tuples

A tuple is an anonymous product of two or more values, written with parentheses and commas: (A, B). Tuples do not need to be declared as a named syntax; they can appear inline wherever a type or value is expected.

The most common use is as the element type of a list. For example, $assoc_ in the stdlib takes a list of pairs as its second argument:

builtin dec $assoc_<X, Y>(X, (X, Y)*) : Y?

Here (X, Y)* is a list of (X, Y) tuples.

Tuples also appear as values constructed on the fly in premises. The member access rules in the Nano-P4 spec build a list of (id, typeIR) pairs to pass to $assoc_:

-- if typeIR = $assoc_<id, typeIR>(id_member, (id_field, typeIR_field)*)

The iteration (id_field, typeIR_field)* zips two parallel lists into a list of pairs.

Records

A record is a product type with named, labeled fields. It is declared with braces and comma-separated LABEL value pairs:

syntax globalTypingLayer =
  { TYPE     typeDefEnv,
    CALLABLE callableTypeDefEnv,
    FRAME    typeFrame }

Record values are constructed with the same brace notation:

-- if globalTypingLayer
    = { TYPE $empty_typeDefEnv,
        CALLABLE $empty_callableTypeDefEnv,
        FRAME $empty_typeFrame }

Fields are accessed with dot notation:

-- if typeFrame = TC.GLOBAL.FRAME

Paths can be chained (TC.GLOBAL.FRAME) to reach fields of nested records.

Records are updated functionally with bracket notation. x[.FIELD = v] produces a copy of x with the named field replaced:

def $enter_t(TC)
  = TC[ .LOCAL.FRAMES = $empty_typeFrame :: TC.LOCAL.FRAMES ]

Nested fields can be updated in a single expression as well:

-- if TC' = TC[.GLOBAL.FRAME = typeFrame']

Variant Definitions

The syntax keyword defines a named type. The most common use is to define a grammar production as a set of variants, which forms the abstract syntax of the language being specified. It can also alias an existing type or name a record type.

syntax type =
  | INT
  | BOOL
  | type '->' type

syntax literal =
  | _NUM int
  | _BOOL bool

syntax expr =
  | literal
  | id
  | '!' expr
  | expr '+' expr
  | expr '<=' expr

Each alternative is prefixed with |. Names starting with a lowercase letter refer to built-in types or non-terminals, which are built-in or previously declared syntax types. Everything else is a terminal, an atom of the object language. Atoms come in a few kinds, each with its own marker:

• Keywords are bare uppercase words, like INT and BOOL. They are written without any marker.
• Silent tags are prefixed with an underscore, like _NUM and _BOOL. These are constructor labels that disambiguate alternatives but do not render in the generated output.
• Operators are glyphs wrapped in single quotes, like '->', '+', and '<='. These are the concrete symbols of the object language.
• Target brackets are backtick-paired and symmetric: `( … `), `{ … `}, and `< … `>. These are the object language’s own brackets. Note that the closing bracket also carries a backtick.

Metavariables

The var keyword declares metavariables and their types. These act as shorthands: wherever e appears unbound in a rule, it is implicitly typed as expr.

var i : int
var b : bool
var x : id
var e : expr
var c : command
var t : type

A variable’s type is inferred from its name by stripping a trailing suffix that begins at the first _ or ' character. For example, given var e : expr, the following names are all valid expr variables:

rule Check_expr/add:
  tenv |- e_l '+' e_r : INT   ;; e_l, e_r -> strip at '_' -> e : expr
  -- Check_expr: tenv |- e_l : INT
  -- Check_expr: tenv |- e_r : INT

rule Check_expr/not:
  tenv |- '!' e' : BOOL        ;; e' -> strip at '\'' -> e : expr
  -- Check_expr: tenv |- e' : BOOL

A suffix of only underscores (e__) or a purely alphanumeric suffix without a separator (eLeft) does not strip, so those would not be recognized as expr variables and would cause an error:

rule Check_expr/not:
  tenv |- '!' eLeft : BOOL     ;; ERROR: eLeft does not resolve to a known variable
  -- Check_expr: tenv |- eLeft : BOOL

Meta-level Operators

P4-SpecTec provides a set of operators that work on meta-level values (the bool, int, and nat primitives), distinct from the operators of the target language being specified.

Boolean operators work on bool meta-values:

These appear in function bodies and if premises:

def $bin_op('&&', _B b_l, _B b_r) = _B (b_l /\ b_r)
def $bin_op('||', _B b_l, _B b_r) = _B (b_l \/ b_r)
def $bin_op('!=', value_l, value_r) = _B (~$bin_eq(value_l, value_r))

-- if direction = OUT \/ direction = INOUT

Note the distinction: '&&' and '||' are target-language terminals (P4 operators in the syntax tree), while /\ and \/ are meta-level boolean operators used to write the spec itself.

Arithmetic expressions on int and nat meta-values are written inside $( ... ):

-- if i' = $($pow2(w) - i - 1)
-- if n'  = $(n - 1)

The $( ... ) delimiter signals that the expression inside uses meta-level arithmetic rather than the target language’s expression grammar.

List length is written with | ... |:

-- if |fieldValue_a*| = |fieldValue_b*|

Set membership is tested with the <- premise, which succeeds if a value matches any element of a list used as a set:

rule Expr_ok/integer:
  scope TC |- unop expression : integerTypeIR
  -- if unop <- [ '~', '-', '+' ]
  -- Expr_ok: scope TC |- expression : integerTypeIR

Function Declarations and Definitions

Functions are declared with dec and defined with def. The declaration gives the name, argument types, and return type. Definitions provide pattern-matched cases. Each of those cases are called clauses.

dec $lookup<K, V>(map<K, V>, K) : V?

;; If map is empty, return empty
def $lookup<K, V>(eps, K_query) = eps

;; If head entry's key matches query, return its value
def $lookup<K, V>((K_h -> V_h)::(K_t -> V_t)*, K_query) = V_h
  -- if K_h = K_query

;; If head entry's key does not match query, recursively call on the rest
def $lookup<K, V>((K_h -> V_h)::(K_t -> V_t)*, K_query)
  = $lookup<K, V>((K_t -> V_t)*, K_query)
  -- otherwise

Key points about function definitions:

• Function names are prefixed with $.
• Angle brackets introduce type parameters (e.g. <K, V>). They must be made explicit in function calls.
• The return type V? means an optional value (eps represents the absent case).
• Each def case can have side conditions introduced with if, or a catch-all otherwise.
• When a function is called, clauses are tried from top to bottom. If pattern match fails or if premises are not satisfied, the clause fails and the next clause is tried.

The builtin modifier marks functions whose implementation is provided by the toolchain rather than defined in the spec:

builtin dec $sum_nat(nat*) : nat

Relations and Rules

A relation defines the signature for a set of rules.

;; Type-check `expr` under context `tenv`
relation Check_expr:
  tenv |- expr : type
  hint(input %0 %1)
  hint(prose_in "typechecking" %1 "under context" %0)

This declares a judgment tenv |- expr : type, meaning “expression expr has type type under typing context tenv.” The |- symbol (turnstile) is conventional notation borrowed from inference rules. In P4-SpecTec, it is just a separator between the context and the subject.

%0, %1, etc. refer to the positional components of the judgment. hint(input ...) specifies which components are inputs to the relation. Here, %0 (tenv) and %1 (expr) are inputs, and %2 (type) is the output.

Rules define when a relation holds. Each rule has a conclusion (the judgment being established) and zero or more premises (the conditions that must hold), introduced with --:

;; If expression is integer literal, it has type INT
rule Check_expr/num:
  tenv |- (_NUM i) : INT

;; If expression is logical not,
;;   Check if the operand is BOOL, then it has type BOOL
rule Check_expr/not:
  tenv |- '!' e : BOOL
  -- Check_expr: tenv |- e : BOOL

;; If expression is binary addition,
;;   Check if both operands are INT, then it has type INT
rule Check_expr/add:
  tenv |- e_l '+' e_r : INT
  -- Check_expr: tenv |- e_l : INT
  -- Check_expr: tenv |- e_r : INT

The first rule has no premises; integer literals always have type INT. The second and third rules invoke Check_expr recursively as premises.

Unlike traditional declarative inference rules where premises are unordered and existential witnesses may be guessed non-deterministically, P4-SpecTec rules are algorithmic: premises are executed in order, from top to bottom, and every value must be computed from already-known inputs. This makes rules directly executable as a type checker or interpreter.

An if premise introduces a boolean-valued side condition:

rule Check_expr/id:
  tenv |- x : t
  -- if $lookup<id, type>(tenv, x) = t

The = in an if premise is overloaded: if the right-hand side is already known, it is a check; if it is an unbound metavariable, it becomes a binding that computes the value from the left-hand side. Here, t is unbound, so $lookup is called and its result is bound to t, which is then used in the conclusion tenv |- x : t. If $lookup returns eps (absent), the rule fails and the next rule is tried.

Rules can mix if and relation premises freely:

rule Check_command/assign:
  tenv |- (x '=' e) -| tenv
  -- Check_expr: tenv |- e : t
  -- if $lookup<id, type>(tenv, x) = t

Here the relation premise Check_expr runs first and binds t, then the if premise checks that x is already declared with that same type.

How Rules are Executed

When the inputs to a relation arrive, the interpreter works through the candidate rules one by one until one succeeds. Understanding this dispatch process matters for writing correct specs and for debugging when something goes wrong:

• Rules are tried in declaration order. When a relation or function has multiple rules or clauses, P4-SpecTec tries them from top to bottom. The first one whose premises all hold wins. This means that the order of clauses in the spec matters.
• A failed premise aborts the current clause. If a pattern match fails or an if condition is not satisfied, that clause is abandoned immediately and the interpreter moves on to the next one. No error is reported at this point; the failure is silent.
• If no clause matches, the relation fails. When every candidate clause has been tried and none succeeded, the interpreter reports a runtime error. A missing rule and a wrong pattern produce the same symptom, which is why the debugging techniques in Chapter 6 focus on narrowing down which clause was the last to be attempted.

Rule Groups

When several rules share the same conclusion shape but differ only in their premises, they can be grouped under a single rulegroup heading. This is purely organizational: the toolchain treats each case inside a rulegroup as an independent rule.

For example, the typing rules for unary expressions in the nano-p4 spec are written as a rule group:

rulegroup Expr_ok/unaryExpression {

  rule Expr_ok/boolean:
    scope TC |- '!' expression : BOOL
    -- Expr_ok: scope TC |- expression : BOOL

  rule Expr_ok/integer:
    scope TC |- unop expression : integerTypeIR
    -- if unop <- [ '~', '-', '+' ]
    -- Expr_ok: scope TC |- expression : integerTypeIR

}

The outer rulegroup Expr_ok/unaryExpression { ... } names the group but adds no semantics. Each rule inside is a full, independent rule with its own name and premises.

Iteration

The (pattern)* syntax applies a pattern element-wise over a list.

For example, the following clause (from the Nano-P4 spec) extracts the third component of every element in parameterIR* into a new list nameIR*:

def $distinct_params(parameterIR*)
  = $distinct_<nameIR>(nameIR*)
  -- if (_ _ nameIR = parameterIR)*

The if premise runs the pattern _ _ nameIR = parameterIR once per element, binding nameIR at each position and collecting the results into nameIR*.

More advanced usages of iteration are to be demonstrated further into the tutorial.

Prose Hints

Prose hints are metadata annotations that guide the prose backend when generating human-readable documentation.

relation Eval_expr:
  env |- expr ==> value
  hint(input %0 %1)
  hint(prose_in "evaluating" %1 "in environment" %0)

hint(prose_in ...) controls the generated prose description.

Individual rules can also carry hints:

syntax literal =
  | _NUM int   hint(prose "the integer" %0)
  | _BOOL bool hint(prose "the boolean" %0)

The prose backend is covered in more detail in Generating Prose Specification.

Exercise

For a more hands-on introduction, we strongly recommend the SpecTecX tutorial.

Toolchain Pipeline

When you run nano-p4spectec, two separate artifacts are at play: a specification (your .watsup files) and a program (a .p4 source file).

Overview

                      .watsup files                    .p4 file
                           │                              │
                           ▼                              ▼
                      ┌─────────┐                    ┌─────────┐
                      │  elab   │                    │  parse  │
                      └────┬────┘                    └────┬────┘
                           │                              │
                           ▼                              │
                       spec (IL)                          │
                           │                              │
                           ▼                              │
                      ┌─────────┐                         │
                      │  algo   │                         │
                      └────┬────┘                         │
                           │                              │
                           ▼                              ▼
                       spec (AL)                   program (meta-value)
                           │                              │
                           └───────────────┬──────────────┘
                                           │
                                           ▼
                                    ┌─────────────┐
                                    │ interpreter │
                                    └──────┬──────┘
                                           │
                                           ▼
                                     relation result
                                  (pass / fail / packets)

There are two independent compilation steps, and the interpreter joins their outputs.

Step 1: Elaborate the spec

The .watsup files are parsed and elaborated into IL (Internal Language), a type-checked and desugared representation of the spec.

Elaboration checks that the spec itself is well-formed: syntax definitions are consistent, rule conclusions match their relation signatures, function clauses are well-typed, and so on.

$ ./nano-p4spectec elab nano-p4/spec

Step 2: Check algorithmic executability

The elaborated IL is analyzed to verify that every rule is algorithmically executable: each variable in a rule’s conclusion and premises must be computable from the declared inputs, with no existential guessing required. The output of this step is AL (Algorithmic Language), the representation that the interpreter actually runs.

$ ./nano-p4spectec algo nano-p4/spec

If any rule cannot be made algorithmic, an AlgoError is reported here before the interpreter ever runs.

Step 3: Parse the program

The .p4 source file is parsed by the Nano-P4 parser into a P4-SpecTec meta-value (the given P4 program is represented as a value in the P4-SpecTec meta-language). It is a tree of constructor tags and nested values that directly mirrors the syntax definitions in the spec. Because it is a value in the same language that the spec is written in, the interpreter can pass it directly to spec relations.

You can inspect this value with:

$ ./nano-p4spectec parse -p <file> -i nano-p4/include

The -t flag prints it as an indented tree, which is easier to read:

$ ./nano-p4spectec parse -t -p <file> -i nano-p4/include

$ cat action.p4
action MyAction() {
    bit<8> x = 8w42;
}

$ ./nano-p4spectec parse \
    -i nano-p4/include \
    -p action.p4 \
    -t
program % %
├── declarationList /* empty */
└── actionDeclaration ACTION % (%) %
    ├── identifier `ID %
    │   └── "MyAction"
    ├── parameterList /* empty */
    └── blockStatement {%}
        └── statementList % %
            ├── statementList /* empty */
            └── variableDeclaration % % % ;
                ├── baseType BIT <%>
                │   └── +8
                ├── identifier `ID %
                │   └── "x"
                └── initializer = %
                    └── integerLiteral % W %
                        ├── 8
                        └── +42

Step 4: Interpret

The interpreter takes the elaborated spec and the program value and executes a relation against the program. The check command runs the Program_ok relation:

$ ./nano-p4spectec check nano-p4/spec \
    -i nano-p4/include \
    -p <file>

This command converts a .p4 program to an IL value and passes it to the Program_ok relation, which type-checks the entire program.

What this means in practice

• A spec error (syntax, type, or rule error in .watsup) surfaces during elaboration, before the program is touched.
• An algo error means a rule cannot be made algorithmically executable: some variable is not computable from the declared inputs.
• A parse error means the .p4 file is not valid Nano-P4 syntax.
• A runtime error means the interpreter got stuck executing the spec against the program. This is typically due to a rule that has no matching case for the given input.
• A test failure from eval means the spec’s dynamic semantics produced different output packets than the STF file expected.

Commands

All commands assume you are running from the root of the nano-spec repository with nano-p4spectec already built (see Installation). The spec files live in nano-p4/spec and example Nano-P4 programs live in nano-p4/testdata/.

elab

Elaborates the spec and prints the resulting IL.

$ ./nano-p4spectec elab nano-p4/spec

Tip: During active spec development, run elab in a watch loop so errors surface immediately:

$ watchexec -w nano-p4/spec ./nano-p4spectec elab nano-p4/spec

algo

Elaborates the spec and checks that every rule is algorithmically executable, then prints the resulting AL (Algorithmic Language) representation.

$ ./nano-p4spectec algo nano-p4/spec

A rule is algorithmic if every variable in its conclusion and premises can be computed from the declared inputs — no existential guessing is required. If any rule violates this, algo reports an AlgoError. Passing algo is a prerequisite for the interpreter to run the spec.

parse

Parses a Nano-P4 source file and prints its IL value. Does not load the spec.

$ ./nano-p4spectec parse -t \
    -p nano-p4/testdata/positive/action-call.p4 \
    -i nano-p4/include

check

Elaborates the spec and type-checks a Nano-P4 program against the Program_ok relation.

$ ./nano-p4spectec check nano-p4/spec \
    -i nano-p4/include \
    -p nano-p4/testdata/positive/action-call.p4

On success, prints passed. On failure, prints an error message.

eval

Runs an end-to-end simulation against a program and an STF test file.

$ ./nano-p4spectec eval nano-p4/spec \
    -i nano-p4/include \
    -p nano-p4/testdata/positive/action-call.p4 \
    -stf nano-p4/testdata/positive/action-call.stf

On success, prints passed.

STF file format

STF (Simple Test Framework) describes packets to inject and the expected output. Nano-P4 supports two directives:

packet <port> <hex-payload>: send a packet on the given port.

expect <port> <hex-payload>: assert a packet is emitted on the given port. A packet with no following expect is expected to be dropped.

packet 0 010000
expect 0 010000

packet 0 020000

packet 0 030000
expect 0 030000

test-check

Batch-typechecks all .p4 files in one or more directories against Program_ok and prints a per-file PASS/FAIL summary.

$ ./nano-p4spectec test-check nano-p4/spec \
    -i nano-p4/include \
    -p4-dir nano-p4/testdata/positive

Use -neg with a directory of intentionally invalid programs to verify that your spec correctly rejects them:

$ ./nano-p4spectec test-check nano-p4/spec \
    -i nano-p4/include \
    -neg \
    -p4-dir nano-p4/testdata/negative

test-eval

Batch-runs all .p4/.stf pairs found in one or more directories and prints a per-test PASS/FAIL summary.

$ ./nano-p4spectec test-eval nano-p4/spec \
    -i nano-p4/include \
    -p4-dir nano-p4/testdata/positive

Only .p4 files with a matching .stf file (same base name) are run; others are silently skipped.

Quick reference

Standard Library

The spec files make heavy use of a set of utility functions defined in 0-stdlib.watsup. These are not specific to Nano-P4; they are generic building blocks for working with sequences, sets, and maps in P4-SpecTec.

Note: This page is a reference you can return to as you read through Sections 3 and 5. You do not need to memorize everything here; skim it once so the names are familiar, then come back when you need a reminder.

Sequences

A sequence (written X*) is an ordered list of elements. The empty sequence is eps, and :: is the cons operator.

builtin dec $rev_<X>(X*) : X*

$rev_ reverses a sequence.

builtin dec $distinct_<K>(K*) : bool

$distinct_ returns true if all elements in the sequence are unique. It is used to enforce no-duplicate-name constraints, for example checking that a parameter list does not repeat a name.

builtin dec $assoc_<X, Y>(X, (X, Y)*) : Y?

$assoc_ looks up a key in an association list (a sequence of pairs) and returns the associated value, or eps if not found.

dec $repeat_<X>(X, nat) : X*

$repeat_ produces a sequence of nat copies of a value.

dec $exists_(bool*) : bool
dec $forall_(bool*) : bool

$exists_ returns true if at least one element is true. $forall_ returns true if all elements are true.

Sets

A set is written as `{ K* }, a collection of unique keys with no ordering.

dec $empty_set<K> : set<K>
dec $in_set<K>(set<K>, K) : bool

$empty_set produces an empty set. $in_set checks whether a key is a member of a set.

builtin dec $intersect_set<K>(set<K>, set<K>) : set<K>
builtin dec $union_set<K>(set<K>, set<K>)     : set<K>
builtin dec $unions_set<K>(set<K>*)            : set<K>
builtin dec $diff_set<K>(set<K>, set<K>)       : set<K>
builtin dec $sub_set<K>(set<K>, set<K>)        : bool
builtin dec $eq_set<K>(set<K>, set<K>)         : bool

Standard set operations: intersection, union, union of a sequence of sets, difference, subset check, and equality.

Maps

A map is a set of key-value pairs, written { (K : V)* }.

dec $empty_map<K, V> : map<K, V>

$empty_map produces an empty map.

dec $dom_map<K, V>(map<K, V>) : set<K>
dec $codom_map<K, V>(map<K, V>) : set<V>

$dom_map returns the set of keys. $codom_map returns the set of values. $dom_map appears frequently in the spec to check whether a name is already bound before adding it.

builtin dec $find_map<K, V>(map<K, V>, K) : V?
builtin dec $find_maps<K, V>(map<K, V>*, K) : V?

$find_map looks up a key in a single map and returns the value, or eps if not found. $find_maps searches a sequence of maps from left to right, returning the first match. This is used for variable lookup across a stack of frames.

builtin dec $add_map<K, V>(map<K, V>, K, V) : map<K, V>
builtin dec $update_map<K, V>(map<K, V>, K, V) : map<K, V>

$add_map inserts a new key-value pair. The spec always checks that the key is not already present before calling $add_map, so it is effectively a no-overwrite insert. $update_map updates the value for an existing key. One use is writing to a variable already in scope.

Nano-P4

Nano-P4 is an educational dialect of P4 designed for this tutorial. P4 in its entirety has a large surface area, so mechanizing it from scratch would be an overwhelming first project. Nano-P4 intentionally strips away the more complex corners of the language and keeps only enough to illustrate every step of the spec-authoring workflow end to end.

By the end of this chapter, you will have a clear picture of what you are specifying before writing a single line of P4-SpecTec.

In this chapter

• Scope: which P4 features Nano-P4 includes and which it leaves out
• Syntax Definition in P4-SpecTec: how the Nano-P4 grammar is expressed as P4-SpecTec syntax rules
• NanoSwitch Architecture: the target architecture that Nano-P4 programs run on
• Test Suite: Nano-P4 programs used to verify spec correctness

Scope of Nano-P4

This section describes what Nano-P4 includes and what it leaves out. For a complete grammar reference, see Appendix A: Nano-P4 Grammar.

What Nano-P4 includes

Types

Nano-P4 supports the following types:

• Boolean : bool
• Fixed-width integers : bit<N> and int<N> where N is a compile-time constant
• match_kind : the built-in kind used to annotate table key fields
• Struct types : declared with struct
• Header types : declared with header

Named types (structs and headers) can be used anywhere a type is expected.

Expressions

Nano-P4 supports a standard set of expressions:

• Boolean and integer literals
• Variable references
• Unary operators: !, ~, -, +
• Binary operators: arithmetic (*, +, -), comparison (<, <=, >, >=, ==, !=), and bitwise/logical (&, |, ^, &&, ||)
• Member access: expr.field
• Function and extern calls: f(args)
• Parenthesized expressions

Statements

Inside parser states, control apply blocks, and action bodies, the following statements are available:

• Empty statement (;)
• Variable declaration with mandatory initializer: type name = expr;
• Assignment: lvalue = expr;
• Call statement: lvalue(args);
• Block: { ... }
• Conditional: if (expr) { ... } else { ... } : both branches are required

Actions

Top-level action declarations are supported:

action drop(inout Header hdr) {
    hdr.nanonet.drop = true;
}

Actions must be declared at the top level of the program. Action declarations inside a control block are not supported.

Tables

Tables are supported in a limited form. A table must have a key property and an actions property, and may optionally have a const entries property:

table t {
    key = { hdr.nanonet.drop : exact; }
    actions = { drop(hdr); }
    const entries = {
        (true) : drop(hdr);
    }
}

Restrictions compared to full P4:

• Exactly one key field (the key block takes a single expr : match_kind entry)
• Control plane operations are not supported, so table entries cannot be extended at runtime.
• No default_action, size, or other table properties
• Tables can only be declared inside a control block as a local declaration, not at the top level

Parser block

Parser declarations are fully supported, including multiple named states and select expressions for branching:

parser MyParser(packet_in pkt, out Header hdr) {
    state start {
        pkt.extract(hdr.nanonet);
        transition select(hdr.nanonet.drop) {
            true : drop_state;
            false : accept;
        }
    }
    state drop_state {
        transition accept;
    }
}

A parser state body consists of zero or more variable declarations followed by a transition statement.

Control block

Control declarations are supported. A control may contain local variable declarations and table declarations, followed by an apply block:

control MyControl(inout Header hdr, out bool pass) {
    table t { ... }
    apply {
        t.apply();
    }
}

Extern declarations

Extern object types (used to declare things like packet_in) can be declared with method prototypes, but not constructors:

extern packet_in {
    void extract(out Nanonet hdr);
}

This is how the architecture model exposes built-in operations to the program.

Instantiation

Top-level instantiation is supported and is how the main package is assembled:

NanoSwitch(MyParser(), MyControl()) main;

What Nano-P4 excludes

These features are absent to keep the spec tractable and the type-checking rules focused. The following P4 features are intentionally absent from Nano-P4.

Types

• Header stacks (header[N])
• enum types
• header_union
• list and tuple types
• Generic types
• Arbitrary-width integer literals

Statements and control flow

• for loops
• switch statement
• if without an else

Declarations and scoping

• Type aliases (typedef, type)
• Constructor parameters on parsers/controls
• Nested action declarations

Expressions and operators

• Implicit type casting
• Explicit type casting ((T) expr)
• Method overloading
• Dot-prefix notation (.field without a receiver)

Table features

• The return value of table.apply() (.hit, .action_run)
• default_action
• size and other table properties
• Multiple key fields

Header built-in methods

• isValid(), setValid(), setInvalid(), and similar header methods

Syntax Definition in P4-SpecTec

With the scope of Nano-P4 in mind, let us see how its syntax is expressed in P4-SpecTec. The full syntax is defined in 1-syntax.watsup. Reading it gives a feel for what P4-SpecTec syntax definitions look like at scale, before the type-checking and evaluation rules in later chapters.

Terminals and Non-terminals

Every syntax production in P4-SpecTec is built from two kinds of atoms.

Non-terminals are references to other syntax productions. They appear as lowercase names, for example expression, type, or name.

Terminals are concrete tokens of the language being specified. They appear in two forms:

• Keyword terminals are written in ALL_CAPS: IF, ELSE, STRUCT, PARSER, CONTROL, and so on. These correspond to reserved keywords in Nano-P4.
• Punctuation terminals are written with a leading backtick: `(, `), `{, `}, `;, `., `=, and so on. The backtick distinguishes a literal token from the syntax of P4-SpecTec.

For example, the production for an assignment statement:

syntax assignmentStatement = lvalue '=' expression ';'

reads as: an assignment is an lvalue non-terminal, followed by the literal = token, followed by an expression non-terminal, followed by the literal ; token.

Literals

The two literal forms in Nano-P4 are booleans and integers.

syntax booleanLiteral =
  | TRUE
  | FALSE

syntax integerLiteral =
  | nat W int
  | nat S int

TRUE and FALSE are terminals. Integer literals carry two pieces of metadata: a width nat and a value int. The W terminal marks an unsigned bit-string and S a signed integer. These correspond to bit<N> and int<N> literals in source Nano-P4.

Identifiers

Nano-P4 uses two distinct identifier categories:

syntax identifier = _ID text
syntax typeIdentifier = _TID text

identifier carries the ID tag and a text payload; typeIdentifier uses TID. This split mirrors the official P4 grammar, where the lexer distinguishes regular identifiers from type names already declared.

From these two primitives, several name non-terminals are derived:

syntax nonTypeName =
  | identifier
  | APPLY | KEY | ACTIONS | STATE

syntax typeName = typeIdentifier

syntax name = nonTypeName

nonTypeName adds the contextual keywords APPLY, KEY, ACTIONS, and STATE as valid identifiers: they are reserved in some positions but can appear as plain names in others. typeName is just a typeIdentifier wrapped for clarity. name collapses to nonTypeName, which is what most of the spec refers to.

Types

syntax integerType =
  | BIT `< int `>
  | INT `< int `>

syntax baseType =
  | integerType
  | BOOL
  | MATCH_KIND

syntax type =
  | baseType
  | namedType

integerType captures bit<N> and int<N> with the width stored as an int meta-value directly in the syntax tree. baseType bundles integer types with the two keyword types BOOL and MATCH_KIND. type is the union of base types and named types (structs and headers resolved by name).

Parameters

syntax parameter =
  direction type name

syntax direction = _EMPTY | IN | OUT | INOUT

A parameter is a direction, a type, and a name, laid out in sequence. direction has four cases: the three P4 keywords and _EMPTY for the directionless case (parameters with no direction annotation).

The parameterList production handles the empty-or-nonempty split:

syntax parameterList =
  | _EMPTY
  | nonEmptyParameterList

The _EMPTY here is a P4-SpecTec internal sentinel, not a P4 keyword. It is a terminal token in the grammar, but never appears in a real Nano-P4 source file.

syntax nonEmptyParameterList =
  | parameter
  | nonEmptyParameterList ',' parameter

Any sequence production such as nonEmptyParameterList uses left-recursive form, matching the Yacc/Bison style of the P4 grammar.

However, the spec must convert these to right-recursive lists to access elements in order. Therefore, alongside the syntax, the spec defines a helper function to flatten a parameterList into a flat list parameter*:

dec $flatten_parameterList(parameterList) : parameter*
def $flatten_parameterList(_EMPTY) = eps
def $flatten_parameterList(parameter) = [ parameter ]
def $flatten_parameterList(nonEmptyParameterList ',' parameter)
  = $flatten_parameterList(nonEmptyParameterList) ++ [ parameter ]

This pattern, a dec / def pair that recursively accumulates elements into a list, appears throughout 1-syntax.watsup for every list-valued production: nameList, argumentList, statementList, and so on. The type checker and evaluator call these helpers instead of pattern-matching on the recursive list syntax directly.

Expressions

Expressions form the most layered part of the grammar. The spec defines them in named groups before assembling them under expression:

syntax expression =
  | literalExpression
  | referenceExpression
  | unaryExpression
  | binaryExpression
  | memberAccessExpression
  | callExpression
  | parenthesizedExpression

A few sub-productions are worth noting.

Unary and binary expressions encode their operators as separate syntax productions:

syntax unop = '!' | '~' | '-' | '+'

syntax binop =
  | '*' | '+' | '-'
  | '<=' | '>=' | '<' | '>' | '!=' | '=='
  | '&' | '^' | '|' | '&&' | '||'

Member access and call expressions break a mutual recursion problem: expression needs to refer to memberAccessBase, but memberAccessBase must itself refer back to expression. P4-SpecTec resolves this with forward declarations:

syntax memberAccessBase           ;; forward declaration

syntax memberAccessExpression = memberAccessBase '.' member
syntax callExpression = callTarget `( argumentList `)

;; ... expression is now fully defined ...

syntax memberAccessBase = expression
syntax callTarget = namedType

P4-SpecTec requires a syntax declaration before first use, so these are declared with no alternatives and then given their full definition later in the file after expression itself is complete.

L-values

syntax lvalue =
  | referenceExpression
  | lvalue '.' member
  | `( lvalue `)

L-values are a strict subset of expressions: a variable reference, a member access rooted at an l-value, or a parenthesized l-value. The spec keeps lvalue separate from expression so the typechecker can restrict what appears on the left-hand side of an assignment without inspecting expression structure at every assignment site.

Statements

syntax statement =
  | emptyStatement
  | variableDeclaration
  | assignmentStatement
  | callStatement
  | blockStatement
  | conditionalStatement

conditionalStatement requires both branches:

syntax conditionalStatement =
  IF `( expression `) blockStatement ELSE blockStatement

This directly encodes the Nano-P4 restriction from the Scope section: if without else is not allowed.

Unlike P4, variableDeclaration requires an initializer:

syntax initializer = '=' expression

syntax variableDeclaration =
  type name initializer ';'

Declarations

Nano-P4 has the following top-level declaration forms, each with its own production:

syntax declaration =
  | instantiation
  | actionDeclaration
  | matchKindDeclaration
  | externDeclaration
  | parserDeclaration
  | controlDeclaration
  | typeDeclaration

A few representative examples:

syntax actionDeclaration =
  ACTION name `( parameterList `) blockStatement

syntax externObjectDeclaration =
  EXTERN name `{ externMethodPrototypeList `}

syntax controlDeclaration =
  CONTROL name
    `( parameterList `)
    `{ controlLocalDeclarationList APPLY controlBody `}

controlDeclaration places APPLY inside the body braces, which matches the actual P4 syntax.

Parser and control declarations follow the split-body pattern seen in the scope section: local declarations come first, then states (for parsers) or the apply body (for controls).

Putting It Together

At the top level, a Nano-P4 program is a sequence of declarations:

syntax program =
  | _EMPTY
  | program declaration

As with all list productions, a $flatten_program helper converts it to a flat declaration* that the rest of the spec consumes.

With this syntax definition in hand, the typechecker and evaluator can refer to every Nano-P4 construct by name, and the spec stays readable as the rules grow more complex in later chapters.

NanoSwitch Architecture

NanoSwitch is the target architecture for Nano-P4. It is a minimal packet-filtering pipeline heavily inspired by the eBPF architecture.

Package declaration

The NanoSwitch architecture is declared in nano_model.p4:

parser parse(packet_in packet, out Header hdr);
control filter(inout Header hdr, out bool accept);

package NanoSwitch(parse p, filter f);

A Nano-P4 program must instantiate this package at the top level, providing a concrete parser and filter:

NanoSwitch(MyParser(), MyFilter()) main;

Pipeline

                 ┌──────────────────────────────────────────────┐
                 │               NanoSwitch                     │
                 │                                              │
  packet_in      │   ┌────────┐   accept   ┌────────┐           │
─────────────────┼──►│ Parser ├───────────►│ Filter ├───────┐   │
                 │   └────────┘            └────────┘       │   │
                 │        │                    │            │   │
                 │        │ reject             │            ▼   │
                 │        │                   accept?  forward/drop
                 │        ▼                             │       │
                 │       DROP                           └───────┼──► packet_out
                 │                                              │    (or dropped)
                 └──────────────────────────────────────────────┘

The pipeline has two stages:

1. Parser: Reads the packet and extracts the Header.
2. Filter: Receives the parsed header and an accept flag (initialized to false). The control block sets accept based on header fields and table lookups. After the filter runs, the pipeline reads accept and either forwards or drops the packet.

Unlike more complex P4 architectures, NanoSwitch has no inter-block behaviors or shared logic between stages.

Core definitions

The architecture also provides a fixed set of core definitions in nano_core.p4.

The Nanonet header

header Nanonet {
    bool     drop;
    bit<7>   packetType;
    bit<8>   src;
    bit<8>   dst;
}

This is the only header type in NanoSwitch. It is 24 bits (3 bytes) wide. The drop field is the primary signal used by filtering programs, though the actual forwarding decision is controlled by the accept flag output from the filter.

The Header struct

struct Header {
    Nanonet nanonet;
}

The top-level header struct holds exactly one Nanonet header. This is what the parser extracts into and what the filter operates on.

The packet_in extern

extern packet_in {
    void extract(out Nanonet hdr);
}

packet_in is the only extern object available to the parser. Calling extract reads the next 24 bits from the incoming packet into the provided header. If fewer than 24 bits remain, the call does nothing and the read cursor does not advance.

Built-in action and match kind

action NoAction() {}

match_kind { exact }

NoAction is a no-op action available for use in table action lists. exact is the only supported match kind for table key fields.

Test Suite

The Nano-P4 test suite lives in nano-p4/testdata/ and is split into two directories:

• positive/: 32 nano-p4 programs that are expected to type-check and produce correct output
• negative/: 21 nano-p4 programs that are expected to be rejected by the type checker

Positive tests

Each positive test is a pair of files with the same base name:

• <name>.p4: a valid Nano-P4 program
• <name>.stf: a packet test that drives the program and checks its output

For example, table-const-entries.p4 installs an ACL table and exercises it with packets of different packet types:

#include <nano_model.p4>

action drop(out bool pass) {
    pass = false;
}

action fwd(out bool pass) {
    pass = true;
}

parser Parser(packet_in pkt, out Header hdr) {
    state start {
        pkt.extract(hdr.nanonet);
        transition accept;
    }
}

control Filter(inout Header hdr, out bool pass) {
    table acl {
        key = { hdr.nanonet.packetType : exact; }
        actions = { drop(pass); fwd(pass); }
        const entries = {
            (7w1) : fwd(pass);
            (7w2) : fwd(pass);
            (7w0) : drop(pass);
        }
    }
    apply {
        pass = true;
        acl.apply();
    }
}

NanoSwitch(Parser(), Filter()) main;

Its companion table-const-entries.stf sends three packets and asserts which ones are forwarded:

packet 0 010000
expect 0 010000

packet 0 000000

packet 0 050000
expect 0 050000

The first packet (packetType = 0x01) matches entry 7w1 and is forwarded, so the .stf file includes an expect directive echoing it back. The second packet (packetType = 0x00) matches entry 7w0 and is dropped, so there is no corresponding expect. The third packet (packetType = 0x05) has no matching entry; pass stays true from the initializer and the packet is forwarded.

Negative tests

Negative tests are .p4 files only. There is no .stf companion because the program should not get past typechecking.

For example, bit-arith-mixed-widths.p4 attempts arithmetic between operands of different widths:

#include <nano_model.p4>

parser Parser(packet_in pkt, out Header hdr) {
    state start {
        transition accept;
    }
}

control Filter(inout Header hdr, out bool pass) {
    apply {
        bit<8> x = 8w10;
        bit<16> y = 16w3;
        bit<8> sum = x + y;
        pass = sum == 8w13;
    }
}

NanoSwitch(Parser(), Filter()) main;

This should be rejected because x + y mixes bit<8> and bit<16>, which the type system does not allow.

Running the suite

Run all positive tests (type-check + simulate):

$ ./nano-p4spectec test-check nano-p4/spec \
    -i nano-p4/include \
    -p4-dir nano-p4/testdata/positive

$ ./nano-p4spectec test-eval nano-p4/spec \
    -i nano-p4/include \
    -p4-dir nano-p4/testdata/positive

Run all negative tests (expect rejection):

$ ./nano-p4spectec test-check nano-p4/spec \
    -i nano-p4/include \
    -neg \
    -p4-dir nano-p4/testdata/negative

As you write new spec rules, re-running these commands is the primary way to verify correctness. Keep them handy throughout the tutorial.

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

Typing Context

Before writing a single typing rule, we need somewhere to store what the checker knows so far: which type names exist, which actions and parsers have been declared, and which variables are in scope. That storage is the typing context, defined in 5.00-typing-context.watsup.

The Three Layers

The typing context is not a single flat map. It is split into three layers, each serving a different scoping purpose.

syntax typingContext =
  { GLOBAL globalTypingLayer,
    BLOCK  blockTypingLayer,
    LOCAL  localTypingLayer }

The global layer holds information visible everywhere in the program: type definitions (structs, headers, externs, parsers, controls, packages), callable definitions (actions, parsers, controls), and global variables.

syntax globalTypingLayer =
  { TYPE     typeDefEnv,
    CALLABLE callableTypeDefEnv,
    FRAME    typeFrame }

The block layer holds the parameters of the current parser or control block. Parameters are declared once at the top of a block and visible throughout it, but they must be kept separate from local variables so that scoping rules can be enforced correctly. This layer also holds variables declared at block level declarations in parser and control blocks.

syntax blockTypingLayer =
  { FRAME typeFrame }

The local layer holds local variables declared inside a block body. It is a stack of frames rather than a single frame, because P4 allows nested block statements, each of which introduces its own scope.

syntax localTypingLayer =
  { FRAMES typeFrame* }

A typeFrame is a map from variable names to their types and directions:

syntax varTypeIR  = direction typeIR
syntax typeFrame  = map<id, varTypeIR>

The direction (IN, OUT, INOUT, or EMPTY for directionless) is stored alongside the type because the checker needs it to enforce l-value rules, such as only OUT and INOUT variables being allowed on the left side of an assignment.

Callables and Type Definitions

Two environments in the global layer deserve a closer look.

typeDefEnv maps type names to their internal representations (typeDefIR). When the checker sees a named type like Header, it looks it up here to resolve it to its full struct or header definition.

callableTypeDefEnv maps callable names to their callable type definitions:

syntax callableTypeDef =
  | ACTION parameterIR*
  | PARSER parameterIR*
  | CONTROL parameterIR*

This is what the checker looks up when it sees an action call or a constructor invocation such as MyAction() or Filter(). The full P4 spec separates callables and constructors into distinct environments; Nano-P4 merges them into a single callableTypeDefEnv for simplicity.

The scope Tag

Many functions in this file take a scope argument:

syntax scope = GLOBAL | BLOCK | LOCAL

This tag is how the spec selects which layer to read from or write to. Rather than writing three separate functions for each operation, the spec uses one function with three pattern-matched cases dispatching on the scope. You will see this pattern throughout the static semantics.

Frame Entry and Exit

When the checker enters a block statement, it pushes a new empty frame onto the local stack. When it exits, it pops that frame and discards any variables declared inside.

def $enter_t(TC)
  = TC[ .LOCAL.FRAMES = $empty_typeFrame :: TC.LOCAL.FRAMES ]

def $exit_t(TC) = TC[ .LOCAL.FRAMES = typeFrame_t* ]
  -- if typeFrame_h :: typeFrame_t* = TC.LOCAL.FRAMES

$enter_t prepends an empty frame with ::. $exit_t discards the head frame by pattern-matching the stack as typeFrame_h :: typeFrame_t* and reconstructing the context with only the tail.

This pair is used together around a block body, ensuring that variables declared inside a block cannot escape it.

Adders

The adder functions insert a new binding into the appropriate layer, first checking that the name is not already bound, then adding the new entry.

def $add_var_t(LOCAL, TC, id, varTypeIR) = TC'
  -- if typeFrame_h :: typeFrame_t* = TC.LOCAL.FRAMES
  -- if ~$in_set<id>($dom_map<id, varTypeIR>(typeFrame_h), id)
  -- if typeFrame_h' = $add_map<id, varTypeIR>(typeFrame_h, id, varTypeIR)
  -- if TC' = TC[ .LOCAL.FRAMES = typeFrame_h' :: typeFrame_t* ]

The local adder only touches the head frame, pointing to the innermost scope. This is intentional: a variable declared in a nested block should not be visible in the enclosing block.

There are three adder families:

• $add_var_t(scope, typingContext, id, varTypeIR): adds a variable to a frame
• $add_callableDef_t(typingContext, callableId, callableTypeDef): adds an action, parser, or control to the callable env
• $add_typeDef_t(typingContext, typeId, typeDefIR): adds a struct, header, extern, or other type to the type def env

The latter two always write to the global layer, so they take no scope argument.

Finders

The finder functions look up a name and return its associated type. Variable lookup follows a scope chain: local stack first, then the block frame, then the global frame.

def $find_var_t(LOCAL, TC, id) = varTypeIR
  -- if typeFrame* = TC.LOCAL.FRAMES
  -- if varTypeIR = $find_maps<id, varTypeIR>(typeFrame*, id)

def $find_var_t(LOCAL, TC, id) = $find_var_t(BLOCK, TC, id)
  -- if typeFrame* = TC.LOCAL.FRAMES
  -- if eps = $find_maps<id, varTypeIR>(typeFrame*, id)

The two clauses for LOCAL form a conditional: the first succeeds if the variable is found in the local frames; the second fires when the first returns eps (not found) and delegates to BLOCK. The BLOCK finder applies the same pattern to fall through to GLOBAL if the variable is not in the block frame.

This chain means a local variable can shadow a block parameter, and a block parameter can shadow a global variable.

The TC Meta-variable

After the syntax definitions, 5.00 also declares:

var TC : typingContext

TC is shorthand for the typing context threaded through nearly every rule in the static semantics. Rather than writing typingContext in full each time, the spec declares TC once as a typed meta-variable of type typingContext. The elaborator then recognizes TC, TC', TC_1, and any other suffix variant as standing for a value of that type, wherever they appear in rule bodies or function definitions across all spec files.

Exercise

Branch: exercise/3.1

Check out the exercise branch in the spec submodule:

git -C nano-p4/spec checkout exercise/3.1

Run the following test to observe the failure:

./nano-p4spectec check nano-p4/spec -i nano-p4/include -p nano-p4/testdata/exercise/3.1.p4

The test should pass (it is a valid program), but it does not. If you get stuck, Chapter 6 walks through this exercise as a worked example. The Lvalue_ok/referenceExpression rule attempts to find the block variable pass but the call to $find_var_t fails.

;; 5.04-typing-lvalue.watsup

rule Lvalue_ok/referenceExpression:
  scope TC |- referenceExpression : typeIR
  -- if id = $id(referenceExpression)
  -- if direction typeIR = $find_var_t(scope, TC, id) ;; <- fails!
  -- if direction = OUT \/ direction = INOUT

Add the missing clause to $find_var_t in 5.00-typing-context.watsup.

When you are done, restore the original branch:

git -C nano-p4/spec checkout main

Types

This section covers how the type checker reasons about types, focusing on two concerns: well-formedness and equivalence.

The type checker needs to know two things about any type it encounters: whether the type is well-formed, and whether two types are the same. These two jobs are handled by two relations defined in 5.02-typing-type.watsup.

Type Elaboration: Type_ok

The Type_ok relation elaborates a surface-syntax type into its internal representation (typeIR).

relation Type_ok:
  typingContext |- type ~> typeIR
  hint(input %0 %1)

Read typingContext |- type ~> typeIR as: “under typingContext, the type type elaborates to the internal type typeIR.”

For base types, the rule is trivial: the surface type is already its own internal representation.

rule Type_ok/signed:   TC |- INT `< n `>    ~> INT `< n `>
rule Type_ok/unsigned: TC |- BIT `< n `>    ~> BIT `< n `>
rule Type_ok/boolType: TC |- BOOL          ~> BOOL
rule Type_ok/matchKindType: TC |- MATCH_KIND ~> MATCH_KIND

Named types require a lookup.

rule Type_ok/typeName:
  TC |- (_TID typeId) ~> typeIR
  -- if typeDefIR = $find_typeDef_t(TC, typeId)
  -- if typeIR = $typeIR_of_typeDefIR(typeDefIR)

When the checker sees a named type such as Header, it:

1. Looks up Header in the typing context TC via $find_typeDef_t, retrieving a typeDefIR.
2. Converts that typeDefIR to a typeIR with $typeIR_of_typeDefIR.

$typeIR_of_typeDefIR is a two-clause function defined in 5.00:

def $typeIR_of_typeDefIR(dataTypeIR)       = dataTypeIR
def $typeIR_of_typeDefIR(objectTypeDefIR)  = objectTypeDefIR

Both clauses are identity-like: a typeDefIR is either a dataTypeIR or an objectTypeDefIR, and both are subtypes of typeIR, so the conversion just changes the tag. The function exists to make the type explicit to the elaboration rule.

When a named type is resolved into its underlying type, not only do we know that it is a valid type, but the resolved information can be used somewhere else along the type checking process.

What typeIR looks like

Understanding elaboration requires knowing what the internal type universe looks like.

Base types need no further structure:

syntax baseTypeIR =
  | INT `< nat `>
  | BIT `< nat `>
  | BOOL
  | MATCH_KIND

Data types are user-defined and carry their full field list:

syntax structTypeIR = STRUCT typeId `{ fieldTypeIR* `}
syntax headerTypeIR = HEADER typeId `{ fieldTypeIR* `}

Structs and headers carry both a typeId (the name the programmer gave them) and the full field list fieldTypeIR*. The name matters for equality, as discussed in Type Equality below.

Object types represent instantiable components (parsers, controls, packages, externs, tables):

syntax parserObjectTypeIR  = PARSER  typeId `( parameterIR* `)
syntax controlObjectTypeIR = CONTROL typeId `( parameterIR* `)
syntax packageObjectTypeIR = PACKAGE typeId `( parameterIR* `)
syntax externObjectTypeIR  = EXTERN  typeId externMethodTypeDefEnv
syntax tableObjectTypeIR   = TABLE   typeId

Each carries its name and its parameter list (or method map, for externs).

Type Equality: Type_eq

Type_eq decides whether two internal types are the same.

relation Type_eq:
  typeIR ~~ typeIR
  hint(input %0 %1)

Read typeIR_a ~~ typeIR_b as: “typeIR_a and typeIR_b are equal types.”

Base types

rule Type_eq/baseTypeIR:
  baseTypeIR ~~ baseTypeIR

Two base types are equal if and only if they are syntactically identical. INT<8> is not equal to INT<16>, and BOOL is not equal to BIT<1>. Pattern matching handles this: the same variable baseTypeIR appears on both sides, so the rule only fires when the two sides are the same term.

Structs and headers

rule Type_eq/structTypeIR:
  (STRUCT typeId `{ _ `}) ~~ (STRUCT typeId `{ _ `})

rule Type_eq/headerTypeIR:
  (HEADER typeId `{ _ `}) ~~ (HEADER typeId `{ _ `})

Two struct/header types are equal when they share the same typeId. The field lists on both sides are wildcarded with _ and ignored entirely.

This is nominal equality, not structural equality. If two independent structs happen to have identical fields but different names, they are not considered equal by this relation. P4 treats struct and header types as distinct by name; the spec reflects this by comparing type names rather than structural content.

Externs

rule Type_eq/externObjectTypeIR:
  (EXTERN typeId _) ~~ (EXTERN typeId _)

Extern types are also compared by name only. As with structs, the global type environment guarantees that the same name always resolves to the same extern declaration.

Parsers, controls, and packages

rule Type_eq/parserObjectTypeIR:
  (PARSER _ `( parameterIR_a* `)) ~~ (PARSER _ `( parameterIR_b* `))
  -- (ParameterType_eq: parameterIR_a ~~ parameterIR_b)*

rule Type_eq/controlObjectTypeIR:
  (CONTROL _ `( parameterIR_a* `)) ~~ (CONTROL _ `( parameterIR_b* `))
  -- (ParameterType_eq: parameterIR_a ~~ parameterIR_b)*

rule Type_eq/packageObjectTypeIR:
  (PACKAGE _ `( parameterIR_a* `)) ~~ (PACKAGE _ `( parameterIR_b* `))
  -- (ParameterType_eq: parameterIR_a ~~ parameterIR_b)*

Parsers, controls, and packages are compared structurally: their names (the _) are ignored, and equality holds when the parameter lists are equal pairwise under ParameterType_eq.

This contrasts with how structs and headers are compared: a type name is a declaration, so two values have the same type only if they were declared under that exact name. Parsers and controls are different: a control type declaration describes an interface, and any control block that satisfies that interface is a valid implementation. The name of the implementing block is irrelevant; what matters is that its parameter list matches.

Consider:

// control type declaration (in nano_model.p4)
control filter(inout Header hdr, out bool accept);

// control block declaration (user-written)
control Filter(inout Header hdr, out bool pass) {
    apply { pass = true; }
}

// package instantiation
NanoSwitch(MyParser(), Filter()) main;

filter and Filter are two different names, yet Filter is a valid implementation of the filter interface because their parameter lists match. Structural comparison is what captures this.

Parameter equality

All three iterated premises above delegate to ParameterType_eq:

rule ParameterType_eq:
  (direction typeIR_a _) ~~ (direction typeIR_b _)
  -- Type_eq: typeIR_a ~~ typeIR_b

Two parameters are equal when they share the same direction and have equal types under Type_eq. The parameter name (the trailing _) is ignored.

Tables

rule Type_eq/tableObjectTypeIR:
  (TABLE typeId) ~~ (TABLE typeId)

Tables are compared by name only, consistent with structs and externs.

Exercise

Branch: exercise/3.2

Check out the exercise branch in the spec submodule:

git -C nano-p4/spec checkout exercise/3.2

Run the following test to observe the failure:

./nano-p4spectec check nano-p4/spec -i nano-p4/include -p nano-p4/testdata/exercise/3.2.p4

The test program declares two variables with the same struct type and tries to assign one to the other. The checker should accept this, but it rejects it.

Find the bug/missing rule in 5.02-typing-type.watsup and fix it accordingly.

When you are done, restore the original branch:

git -C nano-p4/spec checkout main

Expressions and L-values

Two spec files handle the type-checking of expressions and l-values: 5.03-typing-expression.watsup and 5.04-typing-lvalue.watsup.

The relation defined in 5.03 is Expr_ok:

relation Expr_ok:
  scope typingContext |- expression : typeIR
  hint(input %0 %1 %2)

Read scope TC |- e : T as: “under context TC at scope scope, expression e has type T.”

The scope argument threads through many rules so that variable lookup (which delegates to $find_var_t) can consult the right layers of the typing context.

Literal Expressions

The simplest rules are the literal cases. Boolean literals always have type BOOL:

rule Expr_ok/boolean:
  scope TC |- booleanLiteral : BOOL

Integer literals carry their width and signedness, and discard their values:

rule Expr_ok/integer-unsigned:
  scope TC |- nat W int : BIT `< nat `>

rule Expr_ok/integer-signed:
  scope TC |- nat S int : INT `< nat `>

As for what TC means, refer to The TC Meta-variable.

Reference Expressions

A reference expression is just a name used as a value:

rule Expr_ok/referenceExpression:
  scope TC |- name : typeIR
  -- if id = $id(name)
  -- if _ typeIR = $find_var_t(scope, TC, id)

The two premises are:

1. Convert name to an id using $id. id is an alias for text.
2. Look it up via $find_var_t, returning a varTypeIR pair of direction and typeIR. The direction is wildcarded with _ because reading a variable has no direction constraint.

The scope argument to $find_var_t is the same one passed into Expr_ok, so lookup follows the correct scope chain automatically.

Unary Expressions

Nano-P4 has two kinds of unary operators: boolean negation and integer operators.

rulegroup Expr_ok/unaryExpression {

  rule Expr_ok/boolean:
    scope TC |- '!' expression : BOOL
    -- Expr_ok: scope TC |- expression : BOOL

  rule Expr_ok/integer:
    scope TC |- unop expression : integerTypeIR
    -- if unop <- [ '~', '-', '+' ]
    -- Expr_ok: scope TC |- expression : integerTypeIR

}

Both rules check that the operand has the expected type and propagate the same type to the result. ! only works on booleans; ~, -, and + work on any integer type (BIT<n> or INT<n>), and the result has the same integer type.

The if unop <- [...] premise is a membership check: it confirms that the operator in question is one of the listed tokens.

Binary Expressions

Five groups of binary operators are defined, each with its own rule:

rule Expr_ok/arithmetic:
  scope TC |- expression_l binop expression_r : integerTypeIR
  -- if binop <- [ '*', '+', '-' ]
  -- Expr_ok: scope TC |- expression_l : integerTypeIR
  -- Expr_ok: scope TC |- expression_r : integerTypeIR

Arithmetic operators (*, +, -) require both operands to have the same integer type and produce that type. The variable integerTypeIR appears in all three positions, so pattern matching enforces that both operands share exactly the same type.

rule Expr_ok/comparison:
  scope TC |- expression_l binop expression_r : BOOL
  -- if binop <- [ '<=', '>=', '<', '>' ]
  -- Expr_ok: scope TC |- expression_l : integerTypeIR
  -- Expr_ok: scope TC |- expression_r : integerTypeIR

Comparison operators consume integers and produce BOOL. The same variable integerTypeIR appears in both premises, so both operands must have exactly the same integer type, just as with arithmetic operators.

rule Expr_ok/equality:
  scope TC |- expression_l binop expression_r : BOOL
  -- if binop <- [ '!=', '==' ]
  -- Expr_ok: scope TC |- expression_l : baseTypeIR
  -- Expr_ok: scope TC |- expression_r : baseTypeIR

Equality operators accept any base type (INT<n>, BIT<n>, BOOL, MATCH_KIND), not just integers, and return BOOL. The same variable baseTypeIR appears in both premises, so both operands must have exactly the same base type.

rule Expr_ok/bitwise:
  scope TC |- expression_l binop expression_r : integerTypeIR
  -- if binop <- [ '&', '^', '|' ]
  -- Expr_ok: scope TC |- expression_l : integerTypeIR
  -- Expr_ok: scope TC |- expression_r : integerTypeIR

Bitwise operators mirror arithmetic: same-type integers in, same type out.

rule Expr_ok/logical:
  scope TC |- expression_l binop expression_r : BOOL
  -- if binop <- [ '&&', '||' ]
  -- Expr_ok: scope TC |- expression_l : BOOL
  -- Expr_ok: scope TC |- expression_r : BOOL

Logical operators require both operands to be BOOL and return BOOL.

Member Access

Member access is written expr.field. The result type is determined by looking up the field name in the struct or header definition:

rule Expr_ok/struct:
  scope TC |- memberAccessBase '.' member : typeIR
  -- Expr_ok: scope TC |- memberAccessBase : typeIR_base
  -- if STRUCT _ `{ (typeIR_field id_field ';')* `} = typeIR_base
  -- if id_member = $id(member)
  -- if typeIR = $assoc_<id, typeIR>(id_member, (id_field, typeIR_field)*)

rule Expr_ok/header:
  scope TC |- memberAccessBase '.' member : typeIR
  -- Expr_ok: scope TC |- memberAccessBase : typeIR_base
  -- if HEADER _ `{ (typeIR_field id_field ';')* `} = typeIR_base
  -- if id_member = $id(member)
  -- if typeIR = $assoc_<id, typeIR>(id_member, (id_field, typeIR_field)*)

Both rules follow the same shape:

1. Type-check the base expression and get back a struct or header type typeIR_base.
2. Destructure typeIR_base to extract its field list (typeIR_field id_field)*.
3. Convert the member token to an id_member.
4. Look up id_member in the field association list with $assoc_<id, typeIR>.

The struct and header cases are separate rules because the pattern in step 2 matches STRUCT _ { ... } or HEADER _ { ... } but not both simultaneously.

Call Expressions

Nano-P4 only supports two kinds of call expressions: parser and control instantiation via constructor invocation. These appear in the package argument list (e.g., NanoSwitch(Parser(), Filter())).

rule Expr_ok/parser:
  scope TC |- (_TID typeId) `( _EMPTY `) : parserObjectTypeIR
  -- if PARSER parameterIR* = $find_callableTypeDef_t(TC, typeId)
  -- if parserObjectTypeIR = PARSER typeId `( parameterIR* `)

rule Expr_ok/control:
  scope TC |- (_TID typeId) `( _EMPTY `) : controlObjectTypeIR
  -- if CONTROL parameterIR* = $find_callableTypeDef_t(TC, typeId)
  -- if controlObjectTypeIR = CONTROL typeId `( parameterIR* `)

Both rules look up typeId in the callable type definition environment with $find_callableTypeDef_t. By the time these rules fire, the parser/control declaration must have been registered as a callable. If the callable is a parser, the result is a PARSER object type; if it is a control, the result is a CONTROL object type. Both carry the type name and the parameter list, used later when checking the enclosing package instantiation.

The argument list is always EMPTY here because parser/control blocks in Nano-P4 do not have constructor parameters, and therefore do not accept arguments during instantiation.

Parenthesized Expressions

rule Expr_ok/parenthesizedExpression:
  scope TC |- `( expression `) : typeIR
  -- Expr_ok: scope TC |- expression : typeIR

Parentheses are transparent: they add no type information and simply propagate the type of the inner expression.

L-values

An l-value names a storage location and can appear on the left-hand side of an assignment. The Lvalue_ok relation in 5.04-typing-lvalue.watsup determines whether an expression qualifies as an l-value and what type it holds:

relation Lvalue_ok:
  scope typingContext |- lvalue : typeIR
  hint(input %0 %1 %2)

Only three forms of l-values exist in Nano-P4:

syntax lvalue =
  | referenceExpression
  | lvalue '.' member
  | `( lvalue `)

Reference L-values

rule Lvalue_ok/referenceExpression:
  scope TC |- referenceExpression : typeIR
  -- if id = $id(referenceExpression)
  -- if direction typeIR = $find_var_t(scope, TC, id)
  -- if direction = OUT \/ direction = INOUT

This rule adds a constraint that Expr_ok/referenceExpression does not have: the direction must be OUT or INOUT. IN and directionless (EMPTY) variables cannot appear on the left of an assignment because they are read-only.

Member Access L-values

The rules for member access l-values are left as an exercise. Have fun!

Parenthesized L-values

rule Lvalue_ok/parenthesized:
  scope TC |- `( lvalue `) : typeIR
  -- Lvalue_ok: scope TC |- lvalue : typeIR

Like parenthesized expressions, parentheses around an l-value are transparent.

Exercise

Branch: exercise/3.3

Check out the exercise branch in the spec submodule:

git -C nano-p4/spec checkout exercise/3.3

Run the following test to observe the failure:

./nano-p4spectec check nano-p4/spec -i nano-p4/include -p nano-p4/testdata/exercise/3.3.p4

The test program assigns to a member of a struct field that is an INOUT parameter. The checker should accept this, but results in an error instead.

The Lvalue_ok/structTypeIR and Lvalue_ok/headerTypeIR rules are missing from 5.04-typing-lvalue.watsup.

Hint: Write them by analogy with Expr_ok/struct and Expr_ok/header in 5.03-typing-expression.watsup.

When you are done, restore the original branch:

git -C nano-p4/spec checkout main

Statements

5.05-typing-statement.watsup type-checks all statements in Nano-P4.

Statement_ok uses a threading pattern: each rule takes an incoming context and produces an outgoing one, though only variable declarations extend the context; all others pass it through unchanged.

relation Statement_ok:
  scope typingContext |- statement -| typingContext
  hint(input %0 %1 %2)

Read scope TC_0 |- s -| TC_1 as: “under context TC_0 at scope scope, statement s is well-typed and produces context TC_1.”

Empty Statement

rule Statement_ok/emptyStatement:
  scope TC |- emptyStatement -| TC

An empty statement is always well-typed and leaves the context unchanged.

Variable Declaration

Variable declarations are handled by a dedicated relation VarDecl_ok before being wrapped by Statement_ok:

rule VarDecl_ok:
  scope TC_0 |- type name ('=' expression) ';' -| TC_1
  -- Type_ok: TC_0 |- type ~> typeIR
  -- Expr_ok: scope TC_0 |- expression : typeIR'
  -- Type_eq: typeIR ~~ typeIR'
  -- if id = $id(name)
  -- if varTypeIR = INOUT typeIR
  -- if TC_1 = $add_var_t(scope, TC_0, id, varTypeIR)

rule Statement_ok/variableDeclaration:
  scope TC_0 |- variableDeclaration -| TC_1
  -- VarDecl_ok: scope TC_0 |- variableDeclaration -| TC_1

VarDecl_ok performs four checks and one update:

1. Elaborate the declared type type.
2. Type-check the initializer expression.
3. Check that both types are equal via Type_eq.
4. Compute id from the name token.
5. Add the new variable to the context with $add_var_t, recording its direction as INOUT.

The direction INOUT is unconditional here: all local variables in Nano-P4 are read-write by default. This is distinct from parameters, which carry an explicit direction from their declaration.

The outgoing context TC_1 is what the rest of the block sees, so any subsequent statement can refer to the newly declared variable.

Assignment Statement

The rule for assignment statements is left as the exercise for this section.

Here is what Statement_ok/assignmentStatement should perform:

1. Check that the left-hand side is a valid l-value
2. Check that the right-hand side type-checks.
3. Check that both types are equal.

Call Statement

There are three kinds of call statements: action call, extern method call, and table apply method call.

Action

rule Statement_ok/callStatement-name:
  scope TC |- referenceExpression `( argumentList `) ';' -| TC
  -- if callableId = $id(referenceExpression)
  -- if ACTION parameterIR* = $find_callableTypeDef_t(TC, callableId)
  -- ArgumentList_ok: scope TC |- argumentList : argumentIR*
  -- Call_convention_ok: parameterIR* '@' argumentIR*

An action call like myAction() looks up the callable in the context, extracts its parameter list, type-checks the arguments, and checks the calling convention.

ArgumentList_ok type-checks each argument expression in argumentList and yields argumentIR*, where argumentIR is a pair of the argument expression and its resolved typeIR. Call_convention_ok verifies that argument directions and types match the parameters. Both of these relations are covered in the next section.

Extern Method

rule Statement_ok/callStatement-member:
  scope TC |- (lvalue_base '.' member) `( argumentList `) ';' -| TC
  -- if expression_base = $expression_of_lvalue(lvalue_base)
  -- Expr_ok: scope TC |- expression_base : typeIR_base
  -- if EXTERN typeId externMethodTypeDefEnv = typeIR_base
  -- if callableId = $id(member)
  -- if VOID callableId `( parameterIR* `)
      = $find_map<callableId, externMethodTypeDefIR>(
          externMethodTypeDefEnv,
          callableId
        )
  -- ArgumentList_ok: scope TC |- argumentList : argumentIR*
  -- Call_convention_ok: parameterIR* '@' argumentIR*

A method call like pkt.extract(hdr) resolves the base expression to an extern type, looks up the method name in the extern’s method environment, and then checks arguments against the method’s parameter list.

$expression_of_lvalue converts the syntactic lvalue_base into an expression before passing it to Expr_ok, since the two are distinct syntactic sorts.

All extern methods in Nano-P4 return VOID, so there is no return type to propagate.

Table Apply Method

rule Statement_ok/callStatement-table-apply:
  scope TC |- (lvalue_base '.' APPLY) `( argumentList `) ';' -| TC
  -- if expression_base = $expression_of_lvalue(lvalue_base)
  -- Expr_ok: scope TC |- expression_base : (TABLE typeId)

A table apply call like tbl.apply() only needs to confirm that the base expression has a table type. No argument or parameter checking is needed: table apply takes no arguments in Nano-P4.

Block Statement

rule Statement_ok/blockStatement:
  scope TC_0 |- blockStatement -| TC_2
  -- if TC_1 = $enter_t(TC_0)
  -- Block_ok: TC_1 |- blockStatement
  -- if TC_2 = $exit_t(TC_1)

A block statement pushes a new scope frame with $enter_t before checking the body, then pops it with $exit_t afterward. The outgoing context TC_2 has the same shape as TC_0: any variables declared inside the block are discarded.

The body is checked by Block_ok, which flattens the statementList and threads the context through each statement in sequence:

rule Block_ok:
  TC_0 |- `{ statementList `}
  -- if statement* = $flatten_statementList(statementList)
  -- Statements_ok: TC_0 |- statement* -| TC_1

rule Statements_ok/nil:
  TC_0 |- eps -| TC_0

rule Statements_ok/cons:
  TC_0 |- statement_h :: statement_t* -| TC_2
  -- Statement_ok: LOCAL TC_0 |- statement_h  -| TC_1
  -- Statements_ok:      TC_1 |- statement_t* -| TC_2

Statements_ok threads the context left to right: each statement receives the context produced by the previous one. Notice that Statement_ok is always called with LOCAL scope inside Statements_ok/cons, because statements inside a block body live in the local scope layer.

Note that Block_ok does not call $enter_t/$exit_t itself: the frame push and pop happen in Statement_ok/blockStatement, one level up. Block_ok receives a context that already has the new frame on the stack.

Conditional Statement

rule Statement_ok/conditionalStatement:
  scope TC |- IF `( expression `) blockStatement_then
              ELSE blockStatement_else -| TC
  -- Expr_ok: scope TC |- expression : BOOL
  -- Block_ok: TC |- blockStatement_then
  -- Block_ok: TC |- blockStatement_else

An if/else statement checks that the condition has type BOOL, then checks both branches independently under the same incoming context TC. The two branches do not see each other’s declarations, and neither introduces names into the enclosing scope: each Block_ok premise calls $enter_t/$exit_t internally via Statement_ok/blockStatement.

The outgoing context is the same TC that came in.

Exercise

Branch: exercise/3.4

Check out the exercise branch in the spec submodule:

git -C nano-p4/spec checkout exercise/3.4

Run the following test to observe the failure:

./nano-p4spectec check nano-p4/spec -i nano-p4/include -p nano-p4/testdata/exercise/3.4.p4

The test program contains a valid assignment statement, but the checker rejects it.

The Statement_ok/assignmentStatement rule in 5.05-typing-statement.watsup has been omitted entirely. Write the rule from scratch.

There are three tests for this exercise: 3.4.p4, 3.4.1.p4, 3.4.2.p4. The latter two tests are negative tests, so they must be rejected by the typechecker.

./nano-p4spectec check nano-p4/spec -i nano-p4/include -p nano-p4/testdata/exercise/3.4.p4
# should pass!

./nano-p4spectec check nano-p4/spec -i nano-p4/include -p nano-p4/testdata/exercise/3.4.1.p4
# should fail!

./nano-p4spectec check nano-p4/spec -i nano-p4/include -p nano-p4/testdata/exercise/3.4.2.p4
# should fail!

When you are done, restore the original branch:

git -C nano-p4/spec checkout main

Parameters and Arguments

Three spec files cover the static semantics of function-like calls in Nano-P4: how parameter lists are elaborated, how argument expressions are typed, and how the two sides are matched at a call site: 5.06-typing-parameter.watsup, 5.07-typing-argument.watsup, and 5.13-typing-call-convention.watsup.

Parameters

Parameter_ok

A single parameter is checked by Parameter_ok:

relation Parameter_ok:
  scope typingContext |- parameter : parameterIR -| typingContext
  hint(input %0 %1 %2)

The relation takes an incoming context and produces an outgoing one: each parameter adds a new variable binding visible to subsequent parameters.

rule Parameter_ok:
  scope TC_0 |- direction type name : parameterIR -| TC_1
  -- Type_ok: TC_0 |- type ~> typeIR
  -- if nameIR = $id(name)
  -- if parameterIR = direction typeIR nameIR
  -- if varTypeIR = direction typeIR
  -- if TC_1 = $add_var_t(scope, TC_0, nameIR, varTypeIR)

The rule elaborates the declared type, packages the result into a parameterIR triple of (direction, typeIR, nameIR), and extends the context with the new variable. Unlike local variables (which are unconditionally INOUT), a parameter’s direction comes directly from its declaration and is stored as-is.

Parameters_ok and ParameterList_ok

Multiple parameters are threaded left to right, exactly like statements in Section 3.4:

rule Parameters_ok/nil:
  scope TC |- eps : eps -| TC

rule Parameters_ok/cons:
  scope TC_0 |- parameter_h :: parameter_t* : parameterIR_h :: parameterIR_t* -| TC_2
  -- Parameter_ok: scope TC_0 |- parameter_h : parameterIR_h -| TC_1
  -- Parameters_ok: scope TC_1 |- parameter_t* : parameterIR_t* -| TC_2

ParameterList_ok is a thin wrapper that flattens the left-recursive syntax before delegating to Parameters_ok, and also enforces that no two parameters share the same name:

rule ParameterList_ok:
  scope TC_0 |- parameterList : parameterIR* -| TC_1
  -- if parameter* = $flatten_parameterList(parameterList)
  -- Parameters_ok: scope TC_0 |- parameter* : parameterIR* -| TC_1
  -- if $distinct_params(parameterIR*)

$distinct_params extracts the name fields from each parameterIR and checks them for uniqueness using the standard-library predicate $distinct_.

Helper predicates

Two helper predicates guard parameter lists in declaration rules (covered in Section 3.6):

dec $is_object_typeIR(typeIR) : bool
dec $no_object_params(parameterIR*) : bool

$is_object_typeIR returns true for parser, control, and package object types. $no_object_params confirms that no parameter in a list has an object type. This enforces the Nano-P4 restriction that actions and controls may not take other programmable-block objects as parameters.

Arguments

Argument_ok

An argument is a call-site expression paired with its elaborated type:

relation Argument_ok:
  scope typingContext |- argument : argumentIR
  hint(input %0 %1 %2)

rule Argument_ok:
  scope TC |- expression : argumentIR
  -- Expr_ok: scope TC |- expression : typeIR
  -- if argumentIR = expression '#' typeIR

The rule type-checks the expression and bundles it with its type into an argumentIR pair expression '#' typeIR. The expression itself is kept because the call-convention check below needs to inspect it structurally.

ArgumentList_ok

rule ArgumentList_ok:
  scope TC |- argumentList : argumentIR*
  -- if argument* = $flatten_argumentList(argumentList)
  -- (Argument_ok: scope TC |- argument : argumentIR)*

The iteration premise (Argument_ok: ...)* checks each argument independently under the same context TC. Unlike parameters, arguments do not bind anything, so there is no threading.

Call Convention

Call_convention_ok pairs up a parameter list parameterIR* with an argument list argumentIR* and performs a pairwise check.

rule Call_convention_ok/nil:
  eps '@' eps

rule Call_convention_ok/cons:
  (parameterIR_h :: parameterIR_t*) '@' (argumentIR_h :: argumentIR_t*)
  -- Call_convention_arg_ok: parameterIR_h '@' argumentIR_h
  -- Call_convention_ok:     parameterIR_t* '@' argumentIR_t*

The structural recursion over the two lists in lockstep requires equal lengths: there is no wildcard rule for mismatched lengths, so an arity mismatch has no applicable rule and the check fails.

Each pair is checked by Call_convention_arg_ok, which has three cases based on the parameter’s direction:

rule Call_convention_arg_ok/empty:
  parameterIR '@' argumentIR
  -- if _EMPTY typeIR_param _ = parameterIR
  -- if expression_arg '#' typeIR_arg = argumentIR
  -- Type_eq: typeIR_param ~~ typeIR_arg

rule Call_convention_arg_ok/in:
  parameterIR '@' argumentIR
  -- if IN typeIR_param _ = parameterIR
  -- if expression_arg '#' typeIR_arg = argumentIR
  -- Type_eq: typeIR_param ~~ typeIR_arg

rule Call_convention_arg_ok/out-inout:
  parameterIR '@' argumentIR
  ---- ;; Left for exercise!

EMPTY and IN parameters only require a type match.

OUT and INOUT parameters additionally require the argument expression to be an l-value, enforced by $expression_is_lvalue. This rule is left for you as exercise for this section.

Exercise

Branch: exercise/3.5

Check out the exercise branch in the spec submodule:

git -C nano-p4/spec checkout exercise/3.5

Run the following test to observe the failure:

./nano-p4spectec check nano-p4/spec -i nano-p4/include -p nano-p4/testdata/exercise/3.5.p4

The test program passes a literal integer to an OUT parameter. The checker should reject this, but it does not.

The Call_convention_arg_ok/out-inout rule in 5.13-typing-call-convention.watsup has been omitted entirely. Write the rule from scratch. There are three tests for this exercise: 3.5.p4, 3.5.1.p4, 3.5.2.p4. The latter two tests are negative tests, so they must be rejected by the typechecker.

./nano-p4spectec check nano-p4/spec -i nano-p4/include -p nano-p4/testdata/exercise/3.5.p4
# should pass!

./nano-p4spectec check nano-p4/spec -i nano-p4/include -p nano-p4/testdata/exercise/3.5.1.p4
# should fail!

./nano-p4spectec check nano-p4/spec -i nano-p4/include -p nano-p4/testdata/exercise/3.5.2.p4
# should fail!

When you are done, restore the original branch:

git -C nano-p4/spec checkout main

Declarations

This section covers two spec files: 5.08-typing-declaration.watsup and 5.12-typing-extern.watsup.

Together they handle the top-level declarations that make up a Nano-P4 program:

• instantiations
• action declarations
• extern declarations
• type declarations
  • structs
  • headers
  • parser/control/package type signatures
  • match-kind declarations
• parser declaration
• control declaration

The section also covers the top-level entry point Program_ok, which sequences all declarations and builds the final typing context.

A recurring theme in this section is the threading pattern seen in earlier sections: most relations take an incoming context TC_0 and produce an outgoing context TC_1 after adding whatever names the declaration introduces.

Action Declaration

ActionDecl_ok

relation ActionDecl_ok:
  typingContext |- actionDeclaration -| typingContext
  hint(input %0 %1)

rule ActionDecl_ok:
  TC_0 |- actionDeclaration -| TC_1
  -- if ACTION name_action `( parameterList `) blockStatement = actionDeclaration
  -- if parameter* = $flatten_parameterList(parameterList)
  -- if (direction _ name = parameter)*
  -- if $directionless_trailing(direction*)
  -- Parameters_ok: LOCAL TC_0 |- parameter* : parameterIR* -| TC_body
  -- Block_ok: TC_body |- blockStatement
  -- if callableId = $id(name_action)
  -- if callableTypeDef = ACTION parameterIR*
  -- if TC_1 = $add_callableDef_t(TC_0, callableId, callableTypeDef)

The rule proceeds in three phases.

Structural extraction and direction check. The action is unpacked to obtain its name, parameter list, and body. The parameter directions are extracted and passed to $directionless_trailing, which enforces a P4 rule: all directionless (EMPTY) parameters must appear at the end of the parameter list.

Type-checking the body. Parameters_ok is invoked at LOCAL scope to elaborate the parameter list and produce TC_body, the context in which the action body is checked. Note that TC_0 is the outer context passed to Parameters_ok, so existing names remain visible inside the action. Block_ok then verifies the body under TC_body.

Registering the action. The action is stored in TC_0’s callable environment under callableId with type ACTION parameterIR*. The action is registered in TC_0, not TC_body: the bindings introduced by the parameters are not visible outside the action.

$directionless_trailing

The helper scans the direction list from the end to enforce the trailing rule:

def $directionless_trailing(direction*)
  = $directionless_trailing'(true, $rev_<direction>(direction*))

def $directionless_trailing'(_, eps) = true
def $directionless_trailing'(true, _EMPTY :: direction_t*)
  = $directionless_trailing'(true, direction_t*)
def $directionless_trailing'(false, _EMPTY :: direction_t*) = false
def $directionless_trailing'(_, direction_h :: direction_t*)
  = $directionless_trailing'(false, direction_t*)
  -- if direction_h =/= _EMPTY

The reversed list is walked left to right carrying a boolean flag. The flag starts as true and flips to false the moment a non-_EMPTY direction is seen. Any _EMPTY direction encountered after the flag flips signals that a directionless parameter follows a directional one, which fails the check. The reversal means “the end” of the original list is seen first.

Extern Declaration

Extern checking is split across the two spec files: ExternMethod_ok lives in 5.12-typing-extern.watsup and ExternDecl_ok lives in 5.08-typing-declaration.watsup.

ExternMethod_ok

rule ExternMethod_ok:
  TC |- functionPrototype ';' : externMethodTypeDefIR
  -- if VOID name `( parameterList `) = functionPrototype
  -- ParameterList_ok: LOCAL TC |- parameterList : parameterIR* -| TC_body
  -- if callableId = $id(name)
  -- if externMethodTypeDefIR = VOID callableId `( parameterIR* `)

Each method prototype in an extern block is individually checked by ExternMethod_ok. Nano-P4 restricts extern methods to return VOID, so the only information extracted is the method name and its elaborated parameter list. The result is an externMethodTypeDefIR value: VOID callableId `( parameterIR* `).

Note that this relation produces externMethodTypeDefIR rather than an updated typing context. The caller, ExternDecl_ok, is responsible for assembling all method types into a method environment.

ExternDecl_ok

rule ExternDecl_ok:
  TC_0 |- EXTERN name `{ externMethodPrototypeList `} -| TC_1
  -- if externMethodPrototype*
      = $flatten_externMethodPrototypeList(externMethodPrototypeList)
  -- (ExternMethod_ok : TC_0 |- externMethodPrototype : externMethodTypeDefIR)*
  -- if (VOID callableId_method `( _ `) = externMethodTypeDefIR)*
  -- if $distinct_<callableId>(callableId_method*)
  -- if externMethodTypeDefEnv = `{ (callableId_method ':' externMethodTypeDefIR)* `}
  -- if typeId = $id(name)
  -- if typeDefIR = EXTERN typeId externMethodTypeDefEnv
  -- if TC_1 = $add_typeDef_t(TC_0, typeId, typeDefIR)

The rule flattens the method prototype list, checks each prototype independently under TC_0 via an iteration premise (ExternMethod_ok: ...)*, and collects the resulting externMethodTypeDefIR*. It then enforces that all method names are distinct with $distinct_<callableId>, assembles them into a method environment externMethodTypeDefEnv, and registers the entire extern type in TC_0’s type definition environment under the extern’s name.

Type Declaration

TypeDecl_ok is a rulegroup with one rule for each kind of type declaration.

Struct and Header

rule TypeDecl_ok/structTypeDeclaration:
  TC_0 |- STRUCT name_struct `{ typeFieldList `} -| TC_1
  -- if typeField* = $flatten_typeFieldList(typeFieldList)
  -- if (type name ';' = typeField)*
  -- (Type_ok: TC_0 |- type ~> typeIR)*
  -- if (id_field = $id(name))*
  -- if $distinct_<id>(id_field*)
  -- if typeId = $id(name_struct)
  -- if fieldTypeIR* = (typeIR id_field ';')*
  -- if typeDefIR = STRUCT typeId `{ fieldTypeIR* `}
  -- if TC_1 = $add_typeDef_t(TC_0, typeId, typeDefIR)

The struct rule extracts each field, elaborates each type, checks that field names are distinct, and registers the resulting struct type definition. The header rule is identical in structure with HEADER substituted for STRUCT.

Parser, Control, and Package Type Declarations

These three rules follow the same pattern; here is the parser case:

rule TypeDecl_ok/parserTypeDeclaration:
  TC_0 |- PARSER name `( parameterList `) ';' -| TC_1
  -- ParameterList_ok: BLOCK TC_0 |- parameterList : parameterIR* -| TC_body
  -- if $no_object_params(parameterIR*)
  -- if typeId = $id(name)
  -- if typeDefIR = PARSER typeId `( parameterIR* `)
  -- if TC_1 = $add_typeDef_t(TC_0, typeId, typeDefIR)

A parser, control, or package type declaration (as opposed to a full parser or control definition) is just a signature: a name and a parameter list with no body. The parameter list is elaborated under BLOCK scope, and $no_object_params (from Section 3.5) ensures that none of the parameters have object types.

The type definition registered in TC_1 is PARSER typeId `( parameterIR* `), CONTROL typeId `( parameterIR* `), or PACKAGE typeId `( parameterIR* `) depending on the variant. These type definitions are what the type checker looks up during package instantiation.

Top-Level Declarations

Decl_ok is the dispatch relation for individual top-level declarations. Most rules simply delegate to one of the specialized relations above. A few are worth examining directly.

Instantiation

rule Decl_ok/instantiation:
  TC_0 |- (_TID typeId_target) `( argumentList `) name ';' -| TC_0
  -- if PACKAGE typeId `( parameterIR* `) = $find_typeDef_t(TC_0, typeId_target)
  -- ArgumentList_ok: GLOBAL TC_0 |- argumentList : argumentIR*
  -- Call_convention_ok: parameterIR* '@' argumentIR*
  -- if typeId_object = $id(name)
  -- if typeId_object = "main"
  -- if packageObjectTypeIR = PACKAGE typeId_object `( parameterIR* `)
  -- if varTypeIR = _EMPTY packageObjectTypeIR
  -- if TC_1 = $add_var_t(GLOBAL, TC_0, typeId_object, varTypeIR)

Instantiation connects parsers, controls, and externs into the main package. In Nano-P4, the only instantiable type at the top level is a PACKAGE type. The rule looks up the target type, checks that the arguments match the package’s parameters via Call_convention_ok, and verifies that the object name is literally "main". The resulting variable is registered in the global frame with direction _EMPTY.

Match-Kind Declaration

rule Decl_ok/matchKindDeclaration:
  TC_0 |- MATCH_KIND `{ nameList `} -| TC_1
  -- if name* = $flatten_nameList(nameList)
  -- if (id = $id(name))*
  -- if $distinct_<id>(id*)
  -- if varTypeIR* = $repeat_<varTypeIR>(_EMPTY MATCH_KIND, |id*|)
  -- if TC_1 = $add_vars_t(GLOBAL, TC_0, id*, varTypeIR*)

A match_kind declaration introduces a set of named constants of type MATCH_KIND. The rule checks for name collisions with $distinct_<id>, then creates one _EMPTY MATCH_KIND variable for each name and adds them all to the global frame using $add_vars_t.

Parser Declaration

rule Decl_ok/parserDeclaration:
  TC_0 |- parserDeclaration -| TC_2
  -- if PARSER name `( parameterList `)
      `{ parserLocalDeclarationList parserStateList `} = parserDeclaration
  -- ParameterList_ok: BLOCK TC_0 |- parameterList : parameterIR* -| TC_body
  -- ParserLocalDeclList_ok: TC_body |- parserLocalDeclarationList -| TC_1
  -- ParserStateList_ok: TC_1 |- parserStateList
  -- if callableId = $id(name)
  -- if callableTypeDef = PARSER parameterIR*
  -- if TC_2 = $add_callableDef_t(TC_0, callableId, callableTypeDef)

A full parser declaration is checked in three stages: the parameter list is elaborated to produce TC_body, the local declarations are threaded through to extend it into TC_1, and the parser states are checked under TC_1. Finally, the callable type PARSER parameterIR* is added to TC_0’s callable environment.

The parser-specific relations ParserLocalDeclList_ok and ParserStateList_ok are covered in Section 3.7.

Control Declaration

rule Decl_ok/controlDeclaration:
  TC_0 |- controlDeclaration -| TC_2
  -- if CONTROL name
      `( parameterList `)
      `{ controlLocalDeclarationList APPLY controlBody `} = controlDeclaration
  -- ParameterList_ok: BLOCK TC_0 |- parameterList : parameterIR* -| TC_body
  -- ControlLocalDeclList_ok: TC_body |- controlLocalDeclarationList -| TC_1
  -- Block_ok: TC_1 |- controlBody
  -- if callableId = $id(name)
  -- if callableTypeDef = CONTROL parameterIR*
  -- if TC_2 = $add_callableDef_t(TC_0, callableId, callableTypeDef)

A full control declaration follows a similar three-stage structure as a parser declaration: the parameter list is elaborated to produce TC_body, the control-local declarations are threaded through to extend TC_body into TC_1, and the apply block is checked under TC_1 via Block_ok. After all that, the control’s callable type CONTROL parameterIR* is added to TC_0’s callable environment.

The control-specific relation ControlLocalDeclList_ok is covered in Section 3.8.

Sequencing Declarations: Decls_ok and Program_ok

All top-level declarations are sequenced by Decls_ok:

rule Decls_ok/nil:
  TC_0 |- eps -| TC_0

rule Decls_ok/cons:
  TC_0 |- declaration_h :: declaration_t* -| TC_2
  -- Decl_ok: TC_0 |- declaration_h -| TC_1
  -- Decls_ok: TC_1 |- declaration_t* -| TC_2

This is the same threading pattern used by Statements_ok in Section 3.4 and Parameters_ok in Section 3.5.

Program_ok is the entry point for the entire program:

rule Program_ok:
  |- program -| TC'
  -- if declaration* = $flatten_program(program)
  -- if TC = $empty_typingContext
  -- Decls_ok: TC |- declaration* -| TC'

It starts from an empty typing context, flattens the top-level declaration list, and threads the declarations through Decls_ok. The resulting context TC' holds all top-level type definitions, callable types, and global variables after the program has been fully checked.

Exercise

Branch: exercise/3.6

Check out the exercise branch in the spec submodule:

git -C nano-p4/spec checkout exercise/3.6

Run the following test to observe the failure:

./nano-p4spectec check nano-p4/spec -i nano-p4/include -p nano-p4/testdata/exercise/3.6.p4

The checker will report that directionless_trailing is undefined. The entire $directionless_trailing definition has been removed from 5.08-typing-declaration.watsup. Write it from scratch. Use $rev_<direction> to reverse the list, and $directionless_trailing' as the recursive worker that carries a boolean flag.

There are four tests for this exercise: 3.6.p4 and 3.6.1.p4 are positive tests (should pass); 3.6.2.p4 and 3.6.3.p4 are negative tests (should fail).

./nano-p4spectec check nano-p4/spec \
    -i nano-p4/include \
    -p nano-p4/testdata/exercise/3.6.p4
# should pass!

./nano-p4spectec check nano-p4/spec \
    -i nano-p4/include \
    -p nano-p4/testdata/exercise/3.6.1.p4
# should pass!

./nano-p4spectec check nano-p4/spec \
    -i nano-p4/include \
    -p nano-p4/testdata/exercise/3.6.2.p4
# should fail!

./nano-p4spectec check nano-p4/spec \
    -i nano-p4/include \
    -p nano-p4/testdata/exercise/3.6.3.p4
# should fail!

When you are done, restore the original branch:

git -C nano-p4/spec checkout main

Parser Block

This section covers 5.09-typing-parser.watsup, which type-checks the body of a parser declaration.

Recall from Section 3.6 that Decl_ok/parserDeclaration decomposes a parser declaration into three parts and delegates each to a separate relation:

rule Decl_ok/parserDeclaration:
  TC_0 |- parserDeclaration -| TC_2
  -- if PARSER name `( parameterList `)
      `{ parserLocalDeclarationList parserStateList `} = parserDeclaration
  -- ParameterList_ok: BLOCK TC_0 |- parameterList : parameterIR* -| TC_body
  -- ParserLocalDeclList_ok: TC_body |- parserLocalDeclarationList -| TC_1
  -- ParserStateList_ok: TC_1 |- parserStateList
  -- ...

The parameter list is handled by ParameterList_ok (covered in Section 3.5). The remaining two relations, ParserLocalDeclList_ok and ParserStateList_ok, are defined in 5.09-typing-parser.watsup and are covered here.

Parser Local Declarations

A parser may declare local variables before its states. These declarations are handled by ParserLocalDecl_ok:

relation ParserLocalDecl_ok:
  typingContext |- parserLocalDeclaration -| typingContext
  hint(input %0 %1)

rule ParserLocalDecl_ok:
  TC_0 |- variableDeclaration -| TC_1
  -- VarDecl_ok: BLOCK TC_0 |- variableDeclaration -| TC_1

In Nano-P4, parser local declarations are restricted to variable declarations. The rule simply delegates to VarDecl_ok at BLOCK scope, which elaborates the type, checks the initializer, and extends the context with the new binding (see Section 3.4 for VarDecl_ok).

Multiple local declarations are threaded left to right by ParserLocalDecls_ok, which follows the same nil/cons pattern used throughout the spec:

rule ParserLocalDecls_ok/nil:
  TC_0 |- eps -| TC_0

rule ParserLocalDecls_ok/cons:
  TC_0 |- parserLocalDeclaration_h :: parserLocalDeclaration_t* -| TC_2
  -- ParserLocalDecl_ok: TC_0 |- parserLocalDeclaration_h -| TC_1
  -- ParserLocalDecls_ok: TC_1 |- parserLocalDeclaration_t* -| TC_2

ParserLocalDeclList_ok is a thin wrapper that flattens the left-recursive syntax before delegating to ParserLocalDecls_ok:

rule ParserLocalDeclList_ok:
  TC_0 |- parserLocalDeclarationList -| TC_1
  -- if parserLocalDeclaration*
    = $flatten_parserLocalDeclarationList(parserLocalDeclarationList)
  -- ParserLocalDecls_ok: TC_0 |- parserLocalDeclaration* -| TC_1

The context TC_1 that ParserLocalDeclList_ok produces is the context passed to ParserStateList_ok, so local variable bindings are visible inside all parser states.

Parser Transitions

Each parser state ends with a transition statement, which names the next state to enter. There are two forms: a direct name transition and a select expression.

ParserTransition_ok/name

rule ParserTransition_ok/name:
  TC nameIR_state* |- TRANSITION (name ';')
  -- if nameIR = $id(name)
  -- if nameIR <- nameIR_state*

A simple transition foo; checks that foo refers to a known parser state. The set of valid target names is passed in as nameIR_state*. The membership check nameIR <- nameIR_state* enforces that the target is a known state, including the built-in accept and reject states, which are prepended to nameIR_state* by ParserStateList_ok before any per-state check is performed (See ParserStateList_ok).

ParserTransition_ok/expression

Here’s an example of a select expression in a parser block in Nano-P4 code.

transition select(hdr.nanonet.packetType) {
    7w1 : parse_data;
    7w0 : reject;
}

The following is the corresponding rule:

rule ParserTransition_ok/expression:
  TC_0 nameIR_state* |- TRANSITION selectExpression
  -- if SELECT `( expression `) `{ selectCaseList `} = selectExpression
  -- Expr_ok: LOCAL TC_0 |- expression : typeIR
  -- if selectCase* = $flatten_selectCaseList(selectCaseList)
  -- if (expression_case ':' name_case ';' = selectCase)*
  ---- ;; expression
  -- (Expr_ok: LOCAL TC_0 |- expression_case : typeIR_case)*
  -- (Type_eq: typeIR ~~ typeIR_case)*
  ---- ;; name
  -- if (nameIR_case = $id(name_case))*
  -- if (b_contains = nameIR_case <- nameIR_state*)*
  -- if $forall_(b_contains*)

A select transition dispatches to different states based on the value of an expression. The rule performs two independent checks over the case list.

Expression check. The selector expression expression is type-checked to produce typeIR. Each case label expression_case is also type-checked, and its type typeIR_case must equal typeIR via Type_eq.