Dependently-Typed Data Plane Programming
summary
A dependently-typed P4 called pi4 dependently-typed P4 defines heap types and refinement transformers (a “chomp” Brzozowski derivative) to track bit-level packet layout and header validity, proves decidability by bounding bitvectors with the MTU, and encodes subtyping to SMT. An OCaml SMT-based checker with Liquid Haskell–style refinements and a Petra front end validates real P4 fragments; examples up to ~50 commands type-check in milliseconds and it expresses protocols like “ether type 0x0800 implies IPv4 present” and IPv4/IPv6 mutual exclusion.
AI-written summary · about
chapters (14)
- 0:00Start
- 3:36A More Realistic Program
- 3:56Verification of Data Plane Programs
- 4:46Requirements
- 5:3214 in a Nutshell
- 6:50Typechecking with 14
- 8:18Parsing: Output Type
- 11:32Parsing cont.
- 11:48Modular Reasoning
- 13:00Decidability
- 14:29Implementation
- 15:20Applications
- 15:58Mutual Exclusion of Headers
- 17:22Summary
related talks
27mPetr4: Formal Foundations for P4 Data Planes
19mP4R-Type: A Verified API for P4 Control Plane Programs
18mP4Cub: A Little Language for Big Routers
19mHOL4P4: mechanized small-step semantics for P4
15mOn Temporal Verification of Stateful P4 Programs
01h 08mThe Network is the Computer: A Programming Language Perspective
12mFlightplan: Dataplane Disaggregation and Placement for P4 Programs
25mP4-SpecTec: A Language Mechanization Framework for P4