From 23ee5e7c7003f5bcff46c1901fa7a46130479b03 Mon Sep 17 00:00:00 2001 From: Steffen Smolka Date: Fri, 4 Aug 2023 18:24:26 -0700 Subject: [PATCH 1/4] Update language-specification.md @jonathan-dilorenzo PTAL. FYI, we should also update the section on "metdata" in case we rename it. --- docs/language-specification.md | 41 +++++++++++++++++++++++++--------- 1 file changed, 31 insertions(+), 10 deletions(-) diff --git a/docs/language-specification.md b/docs/language-specification.md index 08f8063..a6ccbff 100644 --- a/docs/language-specification.md +++ b/docs/language-specification.md @@ -68,21 +68,21 @@ with `k` being of type `bit`. Then the fields that can be accessed using the `::` operator together with their types are summarized in the following table: -| | field | field type | -|--------------|------------------|------------| -| exact | k::value | bit\ | -| ternary | k::value | bit\ | +| | field | field type | assumed P4Runtime well-formedness constraints | +|--------------|------------------|------------|-----------------------------------------------| +| exact | k::value | bit\ | +| ternary | k::value | bit\ | masked-off bits are zero: `value & !mask == 0` | | k::mask | bit\ | -| optional | k::value | bit\ | -| | k::mask | bit\ | -| lpm | k::value | bit\ | -| | k::prefix_length | int | -| range | k::low | bit\ | +| optional | k::value | bit\ | masked-off bits are zero: `value & !mask == 0` +| | k::mask | bit\ | wildcad or exact match: `mask == -1 \|\| mask == 0` +| lpm | k::value | bit\ | masked-off bits are zero:`value & !prefix_mask == 0`
where `prefix_mask` is a `W`-bit vector whose upper `prefix_length` bits are 1 and the lower bits are 0 +| | k::prefix_length | int | `0 <= prefix_length && prefix_length <= W` +| range | k::low | bit\ | `low < high \|\| (low == 0 & high == 0)` | | k::high | bit\ | Note that an `optional` match is just a restricted kind of `ternary` match whose mask always satisfies the following constraint: ``` -// Exact match or wildcard match. +// Wildcard match or wildcard match. optional_match_key::mask == 0 || optional_match_key::mask == -1 ``` @@ -90,6 +90,27 @@ When `k` is of type `bool`, everything behaves precisely as if `k` was of type `bit<1>`, with the boolean constant `true` and `false` being mapped to `1` and `0`, respectively. + +### Assumed P4runtime Well-Formedness Constraints + +In p4-constraints, we assume that all table entries we consider satisify certain +*well-formedness constraints* that do not require an explicit +`@entry_restriction`. +These well-formedness constraints are shown in the table above and essentially +say that the entries are valid [according to the P4Runtime standard]. +This includes *canonicity constraints* that rule out distinct but semanitcally +equivalent representations of table entries. For example, using +[P4's mask notation], the ternaries `10 &&& 10` and `11 &&& 11` are equivalent, +as both match the set of bitvectors `{10, 11}`. But only `10 &&& 10` is legal +[according to the P4Runtime standard], which says that masked-off bits must be +0. In general, this is captured by the constraint `value & !mask == 0`. + +*CAUTION:* As of May 2024, p4-constraint's implementation *assumes*, but +*does not enforce* these P4Runtime well-formedness constraints. + +[according to the P4Runtime standard]: https://p4.org/p4-spec/p4runtime/v1.3.0/P4Runtime-Spec.html#sec-match-format +[P4's mask notation]: https://p4.org/p4-spec/docs/P4-16-v1.2.4.html#sec-cubes + ### Attribute access A table entry might include data other than the values for the keys. From 2afa17588b8bb67c788ccb39a84081d8a0d8f5c7 Mon Sep 17 00:00:00 2001 From: Steffen Smolka Date: Mon, 6 May 2024 11:40:56 -0700 Subject: [PATCH 2/4] Update language-specification.md --- docs/language-specification.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/language-specification.md b/docs/language-specification.md index a6ccbff..3bb8557 100644 --- a/docs/language-specification.md +++ b/docs/language-specification.md @@ -74,7 +74,7 @@ table: | ternary | k::value | bit\ | masked-off bits are zero: `value & !mask == 0` | | k::mask | bit\ | | optional | k::value | bit\ | masked-off bits are zero: `value & !mask == 0` -| | k::mask | bit\ | wildcad or exact match: `mask == -1 \|\| mask == 0` +| | k::mask | bit\ | wildcard or exact match: `mask == -1 \|\| mask == 0` | lpm | k::value | bit\ | masked-off bits are zero:`value & !prefix_mask == 0`
where `prefix_mask` is a `W`-bit vector whose upper `prefix_length` bits are 1 and the lower bits are 0 | | k::prefix_length | int | `0 <= prefix_length && prefix_length <= W` | range | k::low | bit\ | `low < high \|\| (low == 0 & high == 0)` From 081abfd0ea7d9cf02c25100bdff3c4ec5b9bc27b Mon Sep 17 00:00:00 2001 From: Steffen Smolka Date: Mon, 6 May 2024 11:42:15 -0700 Subject: [PATCH 3/4] Update language-specification.md --- docs/language-specification.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/language-specification.md b/docs/language-specification.md index 3bb8557..b42b957 100644 --- a/docs/language-specification.md +++ b/docs/language-specification.md @@ -100,7 +100,7 @@ These well-formedness constraints are shown in the table above and essentially say that the entries are valid [according to the P4Runtime standard]. This includes *canonicity constraints* that rule out distinct but semanitcally equivalent representations of table entries. For example, using -[P4's mask notation], the ternaries `10 &&& 10` and `11 &&& 11` are equivalent, +[P4's mask notation], the ternaries `10 &&& 10` and `11 &&& 10` are equivalent, as both match the set of bitvectors `{10, 11}`. But only `10 &&& 10` is legal [according to the P4Runtime standard], which says that masked-off bits must be 0. In general, this is captured by the constraint `value & !mask == 0`. From ce39ef1898ebd28b297f7e35ef5b212c4a7988f1 Mon Sep 17 00:00:00 2001 From: Steffen Smolka Date: Mon, 6 May 2024 13:11:28 -0700 Subject: [PATCH 4/4] Update language-specification.md --- docs/language-specification.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/language-specification.md b/docs/language-specification.md index b42b957..eeb0563 100644 --- a/docs/language-specification.md +++ b/docs/language-specification.md @@ -82,7 +82,7 @@ table: Note that an `optional` match is just a restricted kind of `ternary` match whose mask always satisfies the following constraint: ``` -// Wildcard match or wildcard match. +// Wildcard match or exact match. optional_match_key::mask == 0 || optional_match_key::mask == -1 ``` @@ -98,7 +98,7 @@ In p4-constraints, we assume that all table entries we consider satisify certain `@entry_restriction`. These well-formedness constraints are shown in the table above and essentially say that the entries are valid [according to the P4Runtime standard]. -This includes *canonicity constraints* that rule out distinct but semanitcally +This includes *canonicity constraints* that rule out distinct but semantically equivalent representations of table entries. For example, using [P4's mask notation], the ternaries `10 &&& 10` and `11 &&& 10` are equivalent, as both match the set of bitvectors `{10, 11}`. But only `10 &&& 10` is legal