Overview

This guide walks you through spec mechanization in P4-SpecTec, using its core constructs to describe the semantics of Nano-P4, an educational dialect of P4.

Audience and Scope

Audience. This tutorial is written for the P4 community. It focuses on the practical use of P4-SpecTec for specifying a P4-like language, so a basic familiarity with P4 is recommended. A background in programming-language theory is helpful, but no background in formal methods or proof assistants is required.

What is covered.

• Syntax definition for Nano-P4
• Type-checking and evaluation specifications for Nano-P4
• Prose specification generation
• Hands-on exercises at the end of each section

What is not covered.

• A complete walkthrough of P4-SpecTec. The basics are covered, but P4-SpecTec is treated as a tool throughout, not as the subject of study.
• The full P4 language. Nano-P4 is a deliberately small educational subset, and the tutorial stays within that boundary throughout.

By the end, you will have a full mechanized specification, a reference type checker and interpreter, and natural-language documentation for Nano-P4. Most importantly, you will gain hands-on experience writing a mechanized specification in P4-SpecTec, a skill transferable to any project using the toolchain, including the full P4 language mechanization.