Conference Proceeding talk on P4cub
Conference proceedings talk, Certified Proofs and Programs, Boston, MA
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.