verified-network-toolchain / petr4

Petr4: Formal Semantics for P4
Apache License 2.0
73 stars 20 forks source link

P4 formalization #442

Open pataei opened 1 year ago

pataei commented 1 year ago

A stand-alone (yet incomplete) draft of the formalized spec. This version is consistent with our discussion for the P4 workshop and follows the informal and formal format of web assembly spec. The goal is to provide a simple formalization along with an informal description of the type system and guidance on how to implement it.

The readme in docs/petr4spec explains how to build the spec.

Feedback is appreciated. I highly recommend trying to put yourself in the developers' shoes while reading it by relying more on the informal description to guide you through the formalization and see if the informal format actually helps you understand the type system to the extent that you'd be able to implement it.