P4 is a domain-specific language (DSL) designed for programming packet-processing network devices such as switches and NICs. It allows programmers to define custom network protocols by specifying how packets are parsed, processed, and forwarded to other devices.

The P4 language has four main representations of its syntax and semantics: the official specification, formalizations, implementations, and a test suite. The official specification is an informal description of the language in prose, accompanied by code examples. Formalizations can be found in academia, including efforts such as Petr4, P4Light, and HOL4P4. The main reference implementation, p4c, is a compiler written in C++, along with a test suite consisting of P4 programs.

While the four representations are intended to consistently define the P4 language, they often diverge, as each representation is managed by different parties and evolves at a different pace. This problem is not unique to P4; it is common among industry-level programming languages. WebAssembly (Wasm) has recently addressed this issue by adopting the SpecTec framework. SpecTec is a language mechanization framework that provides a DSL for specifying the formal syntax and semantics of Wasm. The mechanized specification acts as a single source of truth, from which other representations, including a specification document and an interpreter, can be automatically generated. This approach helps ensure consistency across different language representations.

Our project, P4-SpecTec, applies the SpecTec framework to the P4 language in order to shape a more consistent P4 language ecosystem. In this presentation, we discuss three key aspects of our ongoing work.

First, we describe how we mechanized the type system of P4 using SpecTec. While previous formalizations exist, they cover only subsets of the language and are no longer up to date. We consolidated prior efforts to build and mechanize a comprehensive and current formal model of the P4 type system. This process revealed gaps between the language specification and the reference compiler, leading to 9 and 13 ongoing issues in the specification and p4c repositories, respectively.

Second, we discuss how we adapted the SpecTec framework to accommodate the P4 language. Intentionally designed for Wasm, SpecTec includes several Wasm-specific design assumptions. In particular, its execution backends assume a small-step operational semantics mechanization, which does not align with our big-step formalization of P4’s type system. We therefore extended and introduced more constraints to SpecTec frontend, resulting in what we call P4-SpecTec, to support execution of big-step semantics. P4-SpecTec can execute our mechanized P4 type system, currently passing against 97% of the p4c type checker test suite.

Third, we discuss our work-in-progress for test generation through the P4-SpecTec framework. By leveraging the mechanized nature – where the specification itself becomes machine-manipulable – and its executability, we aim to automatically generate diverse P4 programs that exercise a wide spectrum of typing rules in the specification.