HOL4P4

HOL4P4 is a small-step, heapless formalisation and a type system of the P4 language implemented in HOL4. The syntax and semantics is written in the Ott metalanguage, which co-organizes export of definitions to multiple interactive theorem provers.

Content

• Semantics, more specifically:

  • Expression
  • Statement
  • P4 state
  • Architecture-Level
  • Concurrent Architecture-Level

• Proof of determinism for the semantics

• Type system, more specifically:

  • Value
  • Expression
  • Statement
  • Single frame
  • P4 state

• Type preservation proof for:

  • Expression
  • Statement
  • P4 state

• Type progress proof for:

  • Expression
  • Statement
  • P4 state

• Executable semantics, more specifically:

  • Expression
  • Statement
  • Frame
  • Architecture

• Proof of soundness of the executable semantics:

  • Expression
  • Statement
  • Frame
  • Architecture

• .p4 import tool (using Petr4 as backend)

• Case studies:

  • Pipeline interference: Concrete execution, Concurrency theory
  • VSS: Concrete execution, Data non-interference

• Architecture instantiations

  • eBPF
  • VSS
  • V1Model

• Verification, testing and debugging tools

Installation

To set up the development environment, follow the instructions in INSTALL.md.

Papers

A. Alshnakat, D. Lundberg, R. Guanciale, M. Dam and K. Palmskog, "HOL4P4: Semantics for a Verified Data Plane", in P4 Workshop in Europe (EuroP4 '22), 2022.

A. Alshnakat, D. Lundberg, R. Guanciale, and M. Dam "HOL4P4: Mechanized Small-Step Semantics for P4", to appear in (OOPSLA '24).

License

This project is distributed under the terms of the Apache License (Version 2.0), and the BSD 3-Clause License; users may pick which license to apply.

See COPYRIGHT, LICENSE-APACHE and LICENSE-BSD for details.