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