The formal semantics of the P4 programming language is defined in the P4light folder of the Petr4 project. It has 4 sub-folders:
This folder contains the semantics of different targets supported by the current system, such as V1 Model and Tofino.
This folder contains the definition of abstract syntax tree (AST) and the value type of the P4 programming language used in the Verifiable P4. It corresponds to Section 3.1 of the paper.
This folder corresponds to Section 3.2 of the paper. In particular,
-
Semantics.v contains the big-step operational semantics.
-
Interpreter.v is the reference interpreter.
-
InterpreterSafe.v is the correctness proof of the reference interpreter.
TODO
The program logic and related tactics are defined in the core folder. It corresponds to Section 3.3 of the paper.
Theorem 1 in Section 2.1 is scattered in
LightFilter.v,
named query_insert_same, query_insert_other, query_clear,
ok_insert, ok_clear and ok_empty.
Theorem 2 in Section 2.2 is scattered in
verif_Filter_all.v,
named Filter_insert_body, Filter_query_body and
Filter_clear_body.
This folder is about our another example, the
count-min-sketch. Theorems similar to Theorem 1 and Theorem 2
can be found in
LightModel.v
and
verif_CMS_all.v