Tables

5.11-typing-table.watsup type-checks table declarations. A table bundles a key, an action list, and optional constant entries, each with distinct checking requirements. The spec handles this by building a table context (TBLC) from the key and action list and using it to validate entries.

The overall structure is:

TableKey_ok checks the key expression and resolves the match kind.
TableAction_ok / TableActionList_ok check each action reference and build the action list.
TableEntry_ok / TableEntries_ok validate optional constant entries against the table context.
TableProperties_ok orchestrates the above and produces the table context.
TableDecl_ok wraps everything and registers the table name in the typing context.

Table Key

A Nano-P4 table has exactly one key field of the form `{ expression ':' name_matchKind ';' `}.

rule TableKey_ok:
  TC |- `{ expression ':' name_matchKind ';' `} : matchKey
  -- Expr_ok: BLOCK TC |- expression : typeIR
  ---- ;; check match kind
  -- if id = $id(name_matchKind)
  -- if _EMPTY MATCH_KIND = $find_var_t(GLOBAL, TC, id)
  ---- ;; create key name
  -- if nameIR = $strip_all_whitespace($print_<expression>(expression))
  -- if matchKey = typeIR ':' nameIR

The rule proceeds in three phases.

Key expression. Expr_ok type-checks the key expression at BLOCK scope, yielding typeIR. This is the type that entry keys must match.

Match kind. The match kind name is converted to an id and looked up in the global frame of the typing context. A valid match kind is declared with match_kind { exact; lpm; ternary; ... }, which registers each name as a variable of type EMPTY MATCH_KIND (see the Decl_ok/matchKindDeclaration rule in Section 3.6). The lookup $find_var_t(GLOBAL, TC, id) must return exactly EMPTY MATCH_KIND; any other result would cause the rule to fail.

Key IR. The key expression is pretty-printed and stripped of whitespace to produce nameIR, a human-readable label. The result matchKey bundles the type and label as typeIR `: nameIR.

Table Actions

`$split_dataplane_parameters`

Before looking at action checking, it helps to understand the helper that separates an action’s parameters into two groups:

dec $split_dataplane_parameters(parameterIR*)
  : (parameterIR*, parameterIR*)

An action may have both data-plane parameters (those with an explicit direction like in, out, inout) and control-plane parameters (those with direction EMPTY, i.e., directionless).

The function walks the parameter list and partitions them: the first element of the pair is the data-plane parameters, the second is the control-plane parameters. This distinction matters when checking table action references: the actions list in a table supplies control-plane arguments at compile time, while data-plane arguments come from table entries. This distinction is clearer in P4, since NanoSwitch does not support control-plane operations.

`TableAction_ok`

relation TableAction_ok:
  typingContext |- tableAction : matchAction
  hint(input %0 %1)

A table action reference in the actions property can appear either without arguments or with a parenthesized argument list. There is one rule for each form.

Without arguments: The action name is looked up in the callable environment, which must resolve to an ACTION parameterIR* entry. All parameters must be directionless (_EMPTY), enforced by the $forall_ check. The resulting matchAction records the callable id and parameter list with an empty data-plane argument sequence (eps).

rule TableAction_ok/no-argumentList:
  TC |- tableAction : matchAction
  -- if nonTypeName ';' = tableAction
  -- if callableId = $id(nonTypeName)
  -- if ACTION parameterIR* = $find_callableTypeDef_t(TC, callableId)
  -- if (direction _ _ = parameterIR)*
  -- if $forall_((direction = _EMPTY)*)
  -- if matchAction = callableId `( parameterIR* '@' eps `)

With arguments: When arguments are present, they supply the data-plane parameters. The rule first type-checks the arguments, then splits the action’s parameters into data-plane and control-plane groups. Call_convention_ok verifies the provided arguments against the data-plane parameters only. The control-plane parameters are not passed here but are instead bound by the argument list.

rule TableAction_ok/argumentList:
  TC |- tableAction : matchAction
  -- if (nonTypeName `( argumentList `)) ';' = tableAction
  -- if callableId = $id(nonTypeName)
  -- if argument* = $flatten_argumentList(argumentList)
  -- (Argument_ok: BLOCK TC |- argument : argumentIR)*
  -- if ACTION parameterIR* = $find_callableTypeDef_t(TC, callableId)
  -- if (parameterIR_data*, parameterIR_control*)
      = $split_dataplane_parameters(parameterIR*)
  -- Call_convention_ok: parameterIR_data* '@' argumentIR*
  -- if matchAction = callableId `( parameterIR* '@' argumentIR* `)

The resulting matchAction stores the full parameter list alongside the control-plane arguments. TableEntry_ok will later use this to reconcile per-entry data-plane arguments against what was registered here.

`TableActionList_ok`

rule TableActionList_ok:
  TC |- tableActionList : matchAction*
  -- if tableAction* = $flatten_tableActionList(tableActionList)
  -- TableActions_ok: TC |- tableAction* : matchAction*
  -- if (callableId `( _ '@' _ `) = matchAction)*
  -- if $distinct_<callableId>(callableId*)

The rule flattens the action list, checks each action via TableActions_ok (which sequences TableAction_ok over the list), extracts the callable ids, and enforces that action names are distinct. The resulting matchAction* is stored in the table context.

Table Entries

Table entries are optional constant rules that match a key value to a specific action invocation.

relation TableEntry_ok:
  typingContext tableContext |- tableEntry
  hint(input %0 %1 %2)

Unlike relations seen so far, TableEntry_ok takes two separate context arguments: the ordinary typing context TC (for expression and argument checking) and the table context TBLC (for key type and action list lookup).

Entry without arguments

rule TableEntry_ok/action-no-argumentList:
  TC TBLC |- `( expression `) ':' name ';'
  ---- ;; check key
  -- Expr_ok: BLOCK TC |- expression : typeIR
  -- if typeIR_key ':' _ = TBLC.KEY
  -- Type_eq: typeIR ~~ typeIR_key
  ---- ;; check action
  -- if callableId = $id(name)
  -- if (eps, eps) = $find_action(TBLC, callableId)

The key expression is type-checked and compared against TBLC.KEY’s type via Type_eq. The action name is resolved through $find_action, which searches the TBLC.ACTIONS list. For an argument-free entry, the action registered in the actions list must itself have no data-plane or control-plane arguments ((eps, eps)).

Entry with arguments

rule TableEntry_ok/action-argumentList:
  TC TBLC |- `( expression `) ':' (name `( argumentList `)) ';'
  ---- ;; check key
  -- Expr_ok: BLOCK TC |- expression : typeIR
  -- if typeIR_key ':' _ = TBLC.KEY
  -- Type_eq: typeIR ~~ typeIR_key
  -- if callableId = $id(name)
  -- if (parameterIR_action*, argumentIR_action*)
      = $find_action(TBLC, callableId)
  -- ArgumentList_ok: BLOCK TC |- argumentList : argumentIR_entry*
  ---- ;; check call convention for entry
  -- Call_convention_ok: parameterIR_action* '@' argumentIR_entry*
  ---- ;; check alignment with action
  -- if (parameterIR_data*, parameterIR_control*)
      = $split_dataplane_parameters(parameterIR_action*)
  -- if argumentIR_action_data* = argumentIR_action*[0 : |parameterIR_data*|]
  -- if argumentIR_entry_data*
      = argumentIR_entry*[0 : |parameterIR_data*|]
  -- if (argumentIR_action_data = argumentIR_entry_data)*

This rule applies when the entry supplies arguments to the action. After checking the key, $find_action retrieves both the registered parameter list and the control-plane arguments previously bound in the actions list. The entry’s argument list is type-checked and verified against the action’s full parameter list via Call_convention_ok.

The trailing block enforces alignment: the data-plane arguments in the entry must be syntactically identical to those already bound in the actions list. Both sides are sliced to the length of parameterIR_data* and compared element-wise.

Table Properties

TableProperties_ok orchestrates the key and action checks and produces the table context that entry checking depends on.

rule TableProperties_ok/no-entries:
  TC |- (KEY '=' tableKey)
        (ACTIONS '=' `{ tableActionList `}) : TBLC
  -- TableKey_ok: TC |- tableKey : matchKey
  -- TableActionList_ok: TC |- tableActionList : matchAction*
  -- if TBLC = { KEY matchKey, ACTIONS matchAction* }

rule TableProperties_ok/entries:
  TC |- (KEY '=' tableKey)
        (ACTIONS '=' `{ tableActionList `})
        (CONST ENTRIES '=' `{ tableEntryList `}) : TBLC
  -- TableKey_ok: TC |- tableKey : matchKey
  -- TableActionList_ok: TC |- tableActionList : matchAction*
  -- if TBLC = { KEY matchKey, ACTIONS matchAction* }
  -- if tableEntry* = $flatten_tableEntryList(tableEntryList)
  -- TableEntries_ok: TC TBLC |- tableEntry*

Both rules check the key and action list first, then assemble TBLC from the results. The entries variant additionally flattens and validates each constant entry via TableEntries_ok, passing TBLC so that entry checking can cross-reference key types and action registrations.

Table Declaration

rule TableDecl_ok:
  TC_0 |- TABLE name `{ tableProperties `} -| TC_1
  -- TableProperties_ok:
      TC_0 |- tableProperties : TBLC
  -- if typeId = $id(name)
  -- if tableObjectTypeIR = TABLE typeId
  -- if varTypeIR = _EMPTY tableObjectTypeIR
  -- if TC_1 = $add_var_t(BLOCK, TC_0, typeId, varTypeIR)

TableDecl_ok delegates all property checking to TableProperties_ok, then registers the table name as a variable of type EMPTY (TABLE typeId) at BLOCK scope. The EMPTY direction means the table is a read-only object, consistent with how externs and other non-directional values are typed. After this, the name is visible in the apply block of the enclosing control as a table object that can be invoked with .apply().

Exercise

Branch: exercise/3.9

Check out the exercise branch in the spec submodule:

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

The alignment check has been removed from TableEntry_ok/action-argumentList in 5.11-typing-table.watsup on this branch. Write a Nano-P4 program that exposes the missing check: it should pass on the exercise branch but be rejected by the full spec. You may use 3.9.p4 as your starting point.

Your program must use const entries and have at least one entry that invokes an action with arguments. Think about what the alignment block is comparing, and what a const entries entry could supply that would differ from what the actions list registered.

Check out the exercise branch and verify your program passes on the faulty spec:

git -C nano-p4/spec checkout exercise/3.9
./nano-p4spectec check nano-p4/spec -i nano-p4/include -p <your-program.p4>
# should pass!

Then restore the original branch and verify it is rejected:

git -C nano-p4/spec checkout main
./nano-p4spectec check nano-p4/spec -i nano-p4/include -p <your-program.p4>
# should fail!

Keyboard shortcuts

Mechanizing the Nano-P4 specification with P4-SpecTec