P4Cub: A Little Language for Big Routers
Published in CPP 2023, 2023
Recommended citation: Rudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parisa Ataei, and Nate Foster. 2023. P4Cub: A Little Language for Big Routers. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2023). Association for Computing Machinery, New York, NY, USA, 303–319. https://doi.org/10.1145/3573105.3575670 http://rudynicolop.github.io/files/p4cub.pdf
P4Cub is a new intermediate representation (IR) for the P4 programming language. It has been designed with the goal of facilitating development of certified tools. To achieve this, P4Cub is organized around a small set of core constructs and avoids side effects in expressions, which avoids mutual recursion between the semantics of expressions and statements. Still, it retains the essential domain-specific features of P4 itself. P4Cub has a front-end based on Petr4, and has been fully mechanized in Coq including big-step and small-step semantics and a type system. As case studies, we have engineered several certified tools with P4Cub including proofs of type soundness, a verified compilation pass, and an automated verification tool.
Here is the talk I gave in Boston.