Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

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