P4's semantic core as an architecture-free IR, with independent Lean and Python implementations. This personal, educational prototype explores a serialized core that frontends and architectures can share.
Project website · Quickstart · Design · Assurance
Author typed Parser, Control and Deparser blocks independently, combine them in libraries, or bind them to the supplied six-stage v1model packet profile. The project includes a validator, interpreter, P4 printer, scoped P4-SpecTec importer, and runnable router, firewall and load-balancer examples.
Lean proofs cover selected architecture-free core properties under explicit premises. Architecture adapters, concrete externs, Python execution and applications are tested, with independent expected answers and P4-SpecTec/BMv2 comparisons. This is not full P4 support, a verified frontend, a proof of Python–Lean equivalence, or a performance or hardware implementation claim. Read the supported profile and guarantees and known oracle differences for the boundaries.
Install uv, then run from the repository root:
uv sync --locked
uv run python -m examples.router.demo
uv run pytest tests/programs/examples -m "not lean and not oracle".python-version selects Python 3.13; uv can download it if needed. The locked
environment includes the package, tests, linter and type checker. These demos
need no compiler, Docker or external oracle.
Continue with the applications, the tested quickstart, or the Python authoring guide. The design explains the architecture and source layout; core semantics, architecture support and P4 coverage define the supported behavior.
Commands throughout the documentation assume the required tools are on PATH. Choose how to install them; the project does not require a particular system package manager.
| Work | Additional tools |
|---|---|
| Python examples and application tests | None beyond the uv environment above |
| Full Python/schema/workflow gate | Node.js, buf, protoc, actionlint |
| Lean packages and real differential tests | elan/lake; the checked-in lean-toolchain files select the compiler |
| P4-SpecTec oracle | Git, Make, opam, a C toolchain, pkg-config, GMP and zstd development files; builder details |
| BMv2 and P4 printer typechecks | Docker and the corresponding pinned images; workflow details |
Optional: Nix provides pinned development tools
through flake.nix and flake.lock. With direnv shell
integration enabled, run direnv allow once: .envrc loads the environment
when you enter the repository, so commands need no prefix. Alternatively,
enter the environment once with nix develop (add .#oracle to select the
shell with optional OCaml build prerequisites).
For repository checks after installing their tools:
scripts/check.sh # Python/schema gate; external oracles excluded
scripts/check-lean.sh # both Lean packages, core proof audits and tests
For dependency markers, oracle setup, pins and change-specific checks, see workflows and the test guide.
Apache-2.0. See LICENSE.