P4Cub: A Little Language for Big Routers
summary
P4Cub is an IR for P4 with a Petr4 front end and a claim of easier mechanized metatheory: it is mechanized in Coq with both large- and small-step semantics and a type system, uses nameless representation and heapless, expression-pure semantics to avoid fresh-name proofs, and hoists table applications to statements. Case studies include a verified compilation pass that lifts side-effecting expressions and type soundness proofs, and an automated verifier via GCL and Z3; the verifier backend takes months not years to build.
AI-written summary · about
chapters (13)
- 0:00Introduction to P4Cub
- 0:21Design principles for IRs
- 1:48Formalizing network languages
- 3:33Criteria for mechanized IR
- 4:56P4Cub design goals
- 5:17P4Cub transformation example
- 7:02Simplifying P4 data types
- 8:04P4Cub syntax
- 8:24Verified compilation passes
- 11:56Type soundness proofs in P4Cub
- 12:37Automated verification backend
- 12:58Summary and future work
- 13:41Q&A on induction schemes
related talks
01h 08mThe Network is the Computer: A Programming Language Perspective
27mPetr4: Formal Foundations for P4 Data Planes
22mDependently-Typed Data Plane Programming
19mHOL4P4: mechanized small-step semantics for P4
19mP4R-Type: A Verified API for P4 Control Plane Programs
16mCetus: Releasing P4 Programmers from the Chore of Trial and Error Compiling
25mFormal Verification of a Software Defined Delay-Tolerant Network
25mP4-SpecTec: A Language Mechanization Framework for P4