verified-network-toolchain / petr4

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

Top Declaration Interpreter #425

Closed zachary-kent closed 1 year ago

zachary-kent commented 1 year ago

Implements and verifies the soundness of an interpreter for toplevel P4cub declarations. Now, all that remains to complete the P4cub interpreter is to write the interpreter for modules and programs. However, the module semantics seemed to be stubbed in as an empty relation.