Nano-P4

Nano-P4 is an educational dialect of P4 designed for this tutorial. P4 in its entirety has a large surface area, so mechanizing it from scratch would be an overwhelming first project. Nano-P4 intentionally strips away the more complex corners of the language and keeps only enough to illustrate every step of the spec-authoring workflow end to end.

By the end of this chapter, you will have a clear picture of what you are specifying before writing a single line of P4-SpecTec.

In this chapter

• Scope: which P4 features Nano-P4 includes and which it leaves out
• Syntax Definition in P4-SpecTec: how the Nano-P4 grammar is expressed as P4-SpecTec syntax rules
• NanoSwitch Architecture: the target architecture that Nano-P4 programs run on
• Test Suite: Nano-P4 programs used to verify spec correctness