From a6dd707eecb1942a5f8defd81b2d88056b8fa351 Mon Sep 17 00:00:00 2001
From: Andy Fingerhut <andy_fingerhut@alum.wustl.edu>
Date: Sun, 13 Nov 2022 17:39:52 -0500
Subject: [PATCH] Add descriptions of assert and assume to specification

---
 p4-16/psa/PSA.mdk | 23 ++++++++++++++++++++++-
 p4-16/psa/psa.p4  | 12 ++++++++++++
 2 files changed, 34 insertions(+), 1 deletion(-)

diff --git a/p4-16/psa/PSA.mdk b/p4-16/psa/PSA.mdk
index 4042b41a6f..c07f740047 100644
--- a/p4-16/psa/PSA.mdk
+++ b/p4-16/psa/PSA.mdk
@@ -2648,6 +2648,26 @@ ingress ports of packets that have not been seen before.
 ```
 
 
+## Error checking extern functions `assert` and `assume` {#sec-assert-assume}
+
+The extern function `assert` is provided for similar reasons as it is
+present in languages like C: to enable developers to check whether
+conditions that they believe should be true, are actually true,
+signaling an error if they are false.
+
+```
+[INCLUDE=psa.p4:assert_extern_function]
+```
+
+The extern function `assume` is similar to `assert`, but some
+development tools may treat it slightly differently than `assert`,
+e.g. formal verification tools, or tools that automatically generate
+test cases.
+
+```
+[INCLUDE=psa.p4:assume_extern_function]
+```
+
 
 # Atomicity of control plane API operations {#sec-atomicity-of-control-plane-api-operations}
 
@@ -3616,7 +3636,8 @@ provided in sub-sections below.
   `psa.p4` (all changes in file `psa.p4`).
 + Replace `@noWarnUnused` with standard `@noWarn("unused")`
   annotations in `psa.p4` (all changes in file `psa.p4`).
-+ Add `assert` and `assume` extern functions (all changes in file `psa.p4`).
++ Add `assert` and `assume` extern functions (section
+  [#sec-assert-assume]).
 
 TODO: The list above is complete up to the following commit.  Any
 later commits should be considered for describing as additional
diff --git a/p4-16/psa/psa.p4 b/p4-16/psa/psa.p4
index 1203569d74..bd96adaaa8 100644
--- a/p4-16/psa/psa.p4
+++ b/p4-16/psa/psa.p4
@@ -337,6 +337,7 @@ extern bool psa_recirculate(in psa_egress_output_metadata_t istd,
                             in psa_egress_deparser_input_metadata_t edstd);
 
 
+// BEGIN:assert_extern_function
 /***
  * Calling assert when the argument is true has no effect, except any
  * effect that might occur due to evaluation of the argument (but see
@@ -350,6 +351,10 @@ extern bool psa_recirculate(in psa_egress_output_metadata_t istd,
  * name and line number of the assert statement to be printed, and
  * then the simple_switch_psa process exits.
  *
+ * It is expected that many hardware targets will compile PSA programs
+ * as if all calls to `assert` were not present.  Consult your target
+ * device's documentation for details.
+ *
  * If you use a P4 compiler whose front end is based on the open
  * source p4c front end, then providing the --ndebug command line
  * option to p4c causes the compiled program to behave as if all
@@ -365,13 +370,19 @@ extern bool psa_recirculate(in psa_egress_output_metadata_t istd,
  * same way when assert statements are removed.
  */
 extern void assert(in bool check);
+// END:assert_extern_function
 
+// BEGIN:assume_extern_function
 /***
  * For the purposes of compiling and executing P4 programs on a target
  * device, assert and assume are identical, including the use of the
  * --ndebug option to compilers based on the open source p4c front end
  * to elide them.  See documentation for assert.
  *
+ * It is expected that many hardware targets will compile PSA programs
+ * as if all calls to `assume` were not present.  Consult your target
+ * device's documentation for details.
+ *
  * The reason that assume exists as a separate function from assert is
  * because they are expected to be used differently by formal
  * verification tools.  For some formal tools, the goal is to try to
@@ -401,6 +412,7 @@ extern void assert(in bool check);
  * is likely that your assumption was wrong, and should be reexamined.
  */
 extern void assume(in bool check);
+// END:assume_extern_function
 
 // BEGIN:Match_kinds
 match_kind {