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.

Name check. Each target name in the case list is resolved to a nameIR_case and checked against nameIR_state* via membership. The results are collected into b_contains*, and $forall_ asserts that every element is true. This ensures every case target is a known parser state.

Parser States

ParserState_ok

relation ParserState_ok:
  typingContext nameIR* |- parserState
  hint(input %0 %1 %2)

rule ParserState_ok:
  TC_0 nameIR_state* |- STATE name `{ statementList transitionStatement `}
  -- if TC_1 = $enter_t(TC_0)
  -- if statement* = $flatten_statementList(statementList)
  -- Statements_ok: TC_1 |- statement* -| TC_2
  -- ParserTransition_ok: TC_2 nameIR_state* |- transitionStatement
  -- if TC_3 = $exit_t(TC_2)

A parser state has a name, a sequence of statements, and a transition statement. The rule:

1. Pushes a new scope frame with $enter_t, producing TC_1.
2. Flattens and type-checks the statements inside the state under TC_1, threading the context through to produce TC_2.
3. Type-checks the transition statement under TC_2, passing in the full set of valid state names nameIR_state*.
4. Pops the scope frame with $exit_t.

The relation takes the set of valid state names nameIR_state* as an extra input parameter alongside the typing context. This is how ParserState_ok knows which target names are legal in transitions. The set is computed once by ParserStateList_ok and threaded down to every state.

ParserStateList_ok

rule ParserStateList_ok:
  TC |- parserStateList
  -- if parserState* = $flatten_parserStateList(parserStateList)
  -- if (STATE name `{ _ _ `} = parserState)*
  -- if (nameIR_state = $id(name))*
  ---- ;; it is illegal to explicitly define states named 'accept' and 'reject'
  -- if ~("accept" <- nameIR_state*) /\ ~("reject" <- nameIR_state*)
  -- if nameIR_state_all* = "accept"::"reject"::nameIR_state*
  -- (ParserState_ok: TC nameIR_state_all* |- parserState)*

ParserStateList_ok validates the collection of parser states as a whole and then checks each one individually. The rule proceeds as follows:

1. The state list is flattened and each state’s name is extracted, yielding nameIR_state*.
2. One membership check enforces a P4 structural rule for parsers:
   • ~("accept" <- nameIR_state*) /\ ~("reject" <- nameIR_state*): the names accept and reject are reserved built-in states and may not be defined explicitly.
3. accept and reject are prepended to nameIR_state* to form nameIR_state_all*, the complete set of valid transition targets (user-defined states plus the two built-in sinks).
4. Finally, (ParserState_ok: TC nameIR_state_all* |- parserState)* applies ParserState_ok to every state in parallel, passing the full name set so that each state’s transition can reference any other state, including accept and reject.

Exercise

Branch: exercise/3.7

Check out the exercise branch in the spec submodule:

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

One of the rules presented in this section is faulty: two premises have been removed from it in 5.09-typing-parser.watsup. The checker now accepts programs it should reject. Find the faulty rule and restore the missing premises.

There are three tests for this exercise: 3.7.p4 is a positive test (should pass); 3.7.1.p4 and 3.7.2.p4 are negative tests (should fail).

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

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

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

When you are done, restore the original branch:

git -C nano-p4/spec checkout main