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

Example output

$ 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.

Keyboard shortcuts