From 0e90c2595d0882b8cf8c6ae99052db53df2302ea Mon Sep 17 00:00:00 2001 From: Didrik Lundberg Date: Tue, 16 Dec 2025 21:42:27 +0100 Subject: [PATCH 1/4] Fixes to README, et cetera --- INSTALL.md | 4 ++-- README.md | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/INSTALL.md b/INSTALL.md index a8e585c5..0bcf70cc 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -96,7 +96,7 @@ First, navigate to the directory where you want to put the source code of Poly/M Finally, do cd .. - make hol + Holmake This will build the HOL4 theories and associated libraries. @@ -106,7 +106,7 @@ First, navigate to the directory where you want to put the source code of Poly/M opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev opam pin add ott dev -k version - This will allow you to re-export the HOL4 definitions in `hol/p4Script.sml` as well as the documentation in `docs/semantics/p4_defs.tex` from the Ott files in the `ott` directory. + This will allow you to re-export the HOL4 definitions in `hol/p4Script.sml` as well as the documentation in `docs/semantics/p4_defs.tex` from the Ott files in the `ott` directory using `make hol`. You may need to repeat `eval $(opam env)` depending on your choice in step 4 in order to use `ott` in the terminal. diff --git a/README.md b/README.md index 9673c2c0..7cb47fbd 100644 --- a/README.md +++ b/README.md @@ -8,8 +8,8 @@ HOL4P4 is a small-step, heapless formalisation and a type system of the P4 langu * [Expression](ott/p4_sem.ott#L2494-L2847) * [Statement](ott/p4_sem.ott#L2858-L2986) * [P4 state](ott/p4_sem.ott#L2994-L3026) - * [Architecture-Level](ott/p4_sem.ott#L3033-L3102) - * [Concurrent Architecture-Level](ott/p4_sem.ott#L3116-L3132) + * [Architecture-level](ott/p4_sem.ott#L3033-L3102) + * [Concurrent architecture-level](ott/p4_sem.ott#L3116-L3132) * [Proof of determinism for the semantics](hol/p4_deterScript.sml) @@ -66,9 +66,9 @@ To set up the development environment, follow the instructions in [INSTALL.md](I ## 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, M. Dam and K. Palmskog, "HOL4P4: Semantics for a Verified Data Plane" (EuroP4 '22). -A. Alshnakat, D. Lundberg, R. Guanciale, and M. Dam "HOL4P4: Mechanized Small-Step Semantics for P4", to appear in (OOPSLA '24). +A. Alshnakat, D. Lundberg, R. Guanciale, and M. Dam "HOL4P4: Mechanized Small-Step Semantics for P4" (OOPSLA '24). ## License From 47593a77f9a125ccc9400e50f5ea857f36f6dbd4 Mon Sep 17 00:00:00 2001 From: Didrik Lundberg Date: Thu, 30 Apr 2026 21:50:52 +0200 Subject: [PATCH 2/4] Clean-up of README --- README.md | 64 ++++++++----------------------------------------------- 1 file changed, 9 insertions(+), 55 deletions(-) diff --git a/README.md b/README.md index 7cb47fbd..c60e7cb6 100644 --- a/README.md +++ b/README.md @@ -4,71 +4,25 @@ HOL4P4 is a small-step, heapless formalisation and a type system of the P4 langu ## Content -* [Semantics](ott/p4_sem.ott), more specifically: - * [Expression](ott/p4_sem.ott#L2494-L2847) - * [Statement](ott/p4_sem.ott#L2858-L2986) - * [P4 state](ott/p4_sem.ott#L2994-L3026) - * [Architecture-level](ott/p4_sem.ott#L3033-L3102) - * [Concurrent architecture-level](ott/p4_sem.ott#L3116-L3132) - +* [Semantics](ott/p4_sem.ott) and [type system](ott/p4_types.ott) in Ott. * [Proof of determinism for the semantics](hol/p4_deterScript.sml) - - -* [Type system](ott/p4_types.ott), more specifically: - * [Value](ott/p4_types.ott#L402-L447) - * [Expression](ott/p4_types.ott#L542-L661) - * [Statement](ott/p4_types.ott#L693-L780) - * [Single frame](ott/p4_types.ott#L855-L896) - * [P4 state](ott/p4_types.ott#L1454-L1484) - - -* Type preservation proof for: - * [Expression](hol/p4_e_subject_reductionScript.sml#L5262-L6682) - * [Statement](hol/p4_stmt_subject_reductionScript.sml#L4499-L4598) - * [P4 state](hol/p4_frames_subject_reductionScript.sml#L2958-L3440) - -* Type progress proof for: - * [Expression](hol/p4_e_progressScript.sml#L1479-L2367) - * [Statement](hol/p4_stmt_progressScript.sml#L885-L923) - * [P4 state](hol/p4_frames_progressScript.sml#L996-L1295) - - -* [Executable semantics](hol/p4_exec_semScript.sml), more specifically: - * [Expression](hol/p4_exec_semScript.sml#L279-L457) - * [Statement](hol/p4_exec_semScript.sml#L504-L671) - * [Frame](hol/p4_exec_semScript.sml#L2171-L2249) - * [Architecture](hol/p4_exec_semScript.sml#L2324-L2424) - -* Proof of soundness of the executable semantics: - * [Expression](hol/p4_exec_sem_e_soundnessScript.sml#L755-L833) - * [Statement](hol/p4_exec_sem_stmt_soundnessScript.sml#L458-L475) - * [Frame](hol/p4_exec_sem_frames_soundnessScript.sml#L16-L155) - * [Architecture](hol/p4_exec_sem_arch_soundnessScript.sml#L17-L268) - +* [Type preservation](hol/p4_frames_subject_reductionScript.sml) and [progress](hol/p4_frames_progressScript.sml) proofs up to the frame level +* [Executable semantics](hol/p4_exec_semScript.sml) with [soundness proof](hol/p4_exec_sem_arch_soundnessScript.sml) * [.p4 import tool (using Petr4 as backend)](hol/p4_from_json) - -* Case studies: - * Pipeline interference: [Concrete execution](hol/p4_from_json/concurrency_tests/concur1_interferenceScript.sml), [Concurrency theory](hol/p4_concurrentScript.sml) - * VSS: [Concrete execution](hol/test-vss.sml), [Data non-interference](hol/test-vss-ttl.sml) - - -* Architecture instantiations +* [Symbolic execution tool](hol/symb_exec) +* Architecture models * [eBPF](hol/p4_ebpfScript.sml) * [VSS](hol/p4_vssScript.sml) * [V1Model](hol/p4_v1modelScript.sml) - -* [Verification, testing and debugging tools](hol/p4_testLib.sml) - - ## Installation -To set up the development environment, follow the instructions in [INSTALL.md](INSTALL.md). +Follow the instructions in [INSTALL.md](INSTALL.md). The [CI scripts](scripts) may also provide some guidance. ## Papers -A. Alshnakat, D. Lundberg, R. Guanciale, M. Dam and K. Palmskog, "HOL4P4: Semantics for a Verified Data Plane" (EuroP4 '22). - -A. Alshnakat, D. Lundberg, R. Guanciale, and M. Dam "HOL4P4: Mechanized Small-Step Semantics for P4" (OOPSLA '24). +* A. Alshnakat, D. Lundberg, R. Guanciale, M. Dam and K. Palmskog, ["HOL4P4: Semantics for a Verified Data Plane"](https://doi.org/10.1145/3565475.3569081) (EuroP4 '22). +* A. Alshnakat, D. Lundberg, R. Guanciale, and M. Dam, ["HOL4P4: Mechanized Small-Step Semantics for P4"](https://doi.org/10.1145/3649819) (OOPSLA '24). +* D. Lundberg, R. Guanciale, and M. Dam, ["Proof-Producing Symbolic Execution for P4"](https://doi.org/10.1145/3649819) (VSTTE '24). ## License From 2f4bd2de62941231161d261263ca4675a322fab0 Mon Sep 17 00:00:00 2001 From: Didrik Lundberg Date: Thu, 30 Apr 2026 21:58:11 +0200 Subject: [PATCH 3/4] Typos in README --- README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index c60e7cb6..8b882f53 100644 --- a/README.md +++ b/README.md @@ -4,13 +4,13 @@ HOL4P4 is a small-step, heapless formalisation and a type system of the P4 langu ## Content -* [Semantics](ott/p4_sem.ott) and [type system](ott/p4_types.ott) in Ott. +* [Semantics](ott/p4_sem.ott) and [type system](ott/p4_types.ott) in Ott * [Proof of determinism for the semantics](hol/p4_deterScript.sml) * [Type preservation](hol/p4_frames_subject_reductionScript.sml) and [progress](hol/p4_frames_progressScript.sml) proofs up to the frame level * [Executable semantics](hol/p4_exec_semScript.sml) with [soundness proof](hol/p4_exec_sem_arch_soundnessScript.sml) * [.p4 import tool (using Petr4 as backend)](hol/p4_from_json) * [Symbolic execution tool](hol/symb_exec) -* Architecture models +* Architecture models: * [eBPF](hol/p4_ebpfScript.sml) * [VSS](hol/p4_vssScript.sml) * [V1Model](hol/p4_v1modelScript.sml) @@ -22,7 +22,7 @@ Follow the instructions in [INSTALL.md](INSTALL.md). The [CI scripts](scripts) m * A. Alshnakat, D. Lundberg, R. Guanciale, M. Dam and K. Palmskog, ["HOL4P4: Semantics for a Verified Data Plane"](https://doi.org/10.1145/3565475.3569081) (EuroP4 '22). * A. Alshnakat, D. Lundberg, R. Guanciale, and M. Dam, ["HOL4P4: Mechanized Small-Step Semantics for P4"](https://doi.org/10.1145/3649819) (OOPSLA '24). -* D. Lundberg, R. Guanciale, and M. Dam, ["Proof-Producing Symbolic Execution for P4"](https://doi.org/10.1145/3649819) (VSTTE '24). +* D. Lundberg, R. Guanciale, and M. Dam, ["Proof-Producing Symbolic Execution for P4"](https://doi.org/10.1007/978-3-031-86695-1_5) (VSTTE '24). ## License From d18ce4f30f7f162e821c00afe269150706908087 Mon Sep 17 00:00:00 2001 From: Didrik Lundberg Date: Thu, 30 Apr 2026 22:00:37 +0200 Subject: [PATCH 4/4] CI badge --- README.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/README.md b/README.md index 8b882f53..3ec44ccb 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,10 @@ # HOL4P4 +[![Build Status][workflow-badge]][workflow-link] + +[workflow-badge]: https://github.com/kth-step/HOL4P4/actions/workflows/build.yaml/badge.svg?branch=main +[workflow-link]: https://github.com/kth-step/HOL4P4/actions/workflows/build.yaml + 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