A guided tutorial for learning P4-SpecTec by mechanizing the semantics of Nano-P4, an educational dialect of P4. Covers the basics of P4-SpecTec, static semantics, dynamic semantics, and prose generation.
Use the flake.nix provided in the repository, or install cargo and mdbook
to build and serve the book. cargo is necessary to build the code highlighting
preprocessor for P4 and P4-SpecTec.
make serve