Update with davidben's and Andres' suggestions

13 files changed, 53 insertions, 53 deletions

diff --git a/p224_32.c b/p224_32.c
index bf1df313d..aacad91e5 100644
--- a/p224_32.c
+++ b/p224_32.c
@@ -57,7 +57,7 @@ static void fiat_p224_subborrowx_u32(uint32_t* out1, fiat_p224_uint1* out2, fiat
 }
 
 /*
- * The function fiat_p224_mulx_u32 is an extended multiplication.
+ * The function fiat_p224_mulx_u32 is a multiplication, returning the full double-width result.
  * out1 = (arg1 * arg2) mod 2^32
  * ∧ out2 = ⌊arg1 * arg2 / 2^32⌋
  * Input Bounds:
diff --git a/p224_64.c b/p224_64.c
index d44f0a694..540ddb245 100644
--- a/p224_64.c
+++ b/p224_64.c
@@ -59,7 +59,7 @@ static void fiat_p224_subborrowx_u64(uint64_t* out1, fiat_p224_uint1* out2, fiat
 }
 
 /*
- * The function fiat_p224_mulx_u64 is an extended multiplication.
+ * The function fiat_p224_mulx_u64 is a multiplication, returning the full double-width result.
  * out1 = (arg1 * arg2) mod 2^64
  * ∧ out2 = ⌊arg1 * arg2 / 2^64⌋
  * Input Bounds:
diff --git a/p256_32.c b/p256_32.c
index 1bfabfaa7..b4742b2dd 100644
--- a/p256_32.c
+++ b/p256_32.c
@@ -57,7 +57,7 @@ static void fiat_p256_subborrowx_u32(uint32_t* out1, fiat_p256_uint1* out2, fiat
 }
 
 /*
- * The function fiat_p256_mulx_u32 is an extended multiplication.
+ * The function fiat_p256_mulx_u32 is a multiplication, returning the full double-width result.
  * out1 = (arg1 * arg2) mod 2^32
  * ∧ out2 = ⌊arg1 * arg2 / 2^32⌋
  * Input Bounds:
diff --git a/p256_64.c b/p256_64.c
index b9c091129..1d8b7141c 100644
--- a/p256_64.c
+++ b/p256_64.c
@@ -59,7 +59,7 @@ static void fiat_p256_subborrowx_u64(uint64_t* out1, fiat_p256_uint1* out2, fiat
 }
 
 /*
- * The function fiat_p256_mulx_u64 is an extended multiplication.
+ * The function fiat_p256_mulx_u64 is a multiplication, returning the full double-width result.
  * out1 = (arg1 * arg2) mod 2^64
  * ∧ out2 = ⌊arg1 * arg2 / 2^64⌋
  * Input Bounds:
diff --git a/p384_32.c b/p384_32.c
index f01dc08b2..1ac5b5804 100644
--- a/p384_32.c
+++ b/p384_32.c
@@ -57,7 +57,7 @@ static void fiat_p384_subborrowx_u32(uint32_t* out1, fiat_p384_uint1* out2, fiat
 }
 
 /*
- * The function fiat_p384_mulx_u32 is an extended multiplication.
+ * The function fiat_p384_mulx_u32 is a multiplication, returning the full double-width result.
  * out1 = (arg1 * arg2) mod 2^32
  * ∧ out2 = ⌊arg1 * arg2 / 2^32⌋
  * Input Bounds:
diff --git a/p384_64.c b/p384_64.c
index 831e8b2ad..1f2c4c468 100644
--- a/p384_64.c
+++ b/p384_64.c
@@ -59,7 +59,7 @@ static void fiat_p384_subborrowx_u64(uint64_t* out1, fiat_p384_uint1* out2, fiat
 }
 
 /*
- * The function fiat_p384_mulx_u64 is an extended multiplication.
+ * The function fiat_p384_mulx_u64 is a multiplication, returning the full double-width result.
  * out1 = (arg1 * arg2) mod 2^64
  * ∧ out2 = ⌊arg1 * arg2 / 2^64⌋
  * Input Bounds:
diff --git a/p484_64.c b/p484_64.c
index 33c12b7e8..b0a5afb17 100644
--- a/p484_64.c
+++ b/p484_64.c
@@ -59,7 +59,7 @@ static void fiat_p484_subborrowx_u64(uint64_t* out1, fiat_p484_uint1* out2, fiat
 }
 
 /*
- * The function fiat_p484_mulx_u64 is an extended multiplication.
+ * The function fiat_p484_mulx_u64 is a multiplication, returning the full double-width result.
  * out1 = (arg1 * arg2) mod 2^64
  * ∧ out2 = ⌊arg1 * arg2 / 2^64⌋
  * Input Bounds:
diff --git a/secp256k1_32.c b/secp256k1_32.c
index bf7e4fb7d..354338e62 100644
--- a/secp256k1_32.c
+++ b/secp256k1_32.c
@@ -57,7 +57,7 @@ static void fiat_secp256k1_subborrowx_u32(uint32_t* out1, fiat_secp256k1_uint1*
 }
 
 /*
- * The function fiat_secp256k1_mulx_u32 is an extended multiplication.
+ * The function fiat_secp256k1_mulx_u32 is a multiplication, returning the full double-width result.
  * out1 = (arg1 * arg2) mod 2^32
  * ∧ out2 = ⌊arg1 * arg2 / 2^32⌋
  * Input Bounds:
diff --git a/secp256k1_64.c b/secp256k1_64.c
index 133702645..04bb1c8e8 100644
--- a/secp256k1_64.c
+++ b/secp256k1_64.c
@@ -59,7 +59,7 @@ static void fiat_secp256k1_subborrowx_u64(uint64_t* out1, fiat_secp256k1_uint1*
 }
 
 /*
- * The function fiat_secp256k1_mulx_u64 is an extended multiplication.
+ * The function fiat_secp256k1_mulx_u64 is a multiplication, returning the full double-width result.
  * out1 = (arg1 * arg2) mod 2^64
  * ∧ out2 = ⌊arg1 * arg2 / 2^64⌋
  * Input Bounds:
diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v
index 4d3e9c047..392a63c78 100644
--- a/src/PushButtonSynthesis/Primitives.v
+++ b/src/PushButtonSynthesis/Primitives.v
@@ -576,10 +576,10 @@ Module CorrectnessStringification.
          (only parsing).
 End CorrectnessStringification.
 
-Notation stringify_correctness_with_ctx ctx evalf pre_extra correctness
-  := (CorrectnessStringification.stringify_correctness_with_ctx ctx evalf pre_extra correctness) (only parsing).
-Notation stringify_correctness evalf pre_extra correctness
-  := (CorrectnessStringification.stringify_correctness evalf pre_extra correctness) (only parsing).
+Notation "'stringify_correctness_with_ctx!' ctx evalf pre_extra correctness"
+  := (CorrectnessStringification.stringify_correctness_with_ctx ctx evalf pre_extra correctness) (only parsing, at level 10, ctx at next level, evalf at next level, pre_extra at next level, correctness at next level).
+Notation "'stringify_correctness!' evalf pre_extra correctness"
+  := (CorrectnessStringification.stringify_correctness evalf pre_extra correctness) (only parsing, at level 10, evalf at next level, pre_extra at next level, correctness at next level).
 
 Section __.
   Context (n : nat)
@@ -622,7 +622,7 @@ Section __.
     := Eval cbv beta in
         FromPipelineToString
           prefix "selectznz" selectznz
-          (stringify_correctness
+          (stringify_correctness!
              evalf
              (fun fname : string => ["The function " ++ fname ++ " is a multi-limb conditional select."]%string)
              (selectznz_correct dummy_weight n saturated_bounds_list)).
@@ -642,9 +642,9 @@ Section __.
     := Eval cbv beta in
         FromPipelineToString
           prefix ("mulx_u" ++ decimal_string_of_Z s) (mulx s)
-          (stringify_correctness
+          (stringify_correctness!
              evalf
-             (fun fname : string => ["The function " ++ fname ++ " is an extended multiplication."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " is a multiplication, returning the full double-width result."]%string)
              (mulx_correct s)).
 
   Definition addcarryx (s : Z)
@@ -663,7 +663,7 @@ Section __.
     := Eval cbv beta in
         FromPipelineToString
           prefix ("addcarryx_u" ++ decimal_string_of_Z s) (addcarryx s)
-          (stringify_correctness
+          (stringify_correctness!
              evalf
              (fun fname : string => ["The function " ++ fname ++ " is an addition with carry."]%string)
              (addcarryx_correct s)).
@@ -683,7 +683,7 @@ Section __.
     := Eval cbv beta in
         FromPipelineToString
           prefix ("subborrowx_u" ++ decimal_string_of_Z s) (subborrowx s)
-          (stringify_correctness
+          (stringify_correctness!
              evalf
              (fun fname : string => ["The function " ++ fname ++ " is a subtraction with borrow."]%string)
              (subborrowx_correct s)).
@@ -704,7 +704,7 @@ Section __.
     := Eval cbv beta in
         FromPipelineToString
           prefix ("cmovznz_u" ++ decimal_string_of_Z s) (cmovznz s)
-          (stringify_correctness
+          (stringify_correctness!
              evalf
              (fun fname : string => ["The function " ++ fname ++ " is a single-word conditional move."]%string)
              (cmovznz_correct s)).
diff --git a/src/PushButtonSynthesis/SaturatedSolinas.v b/src/PushButtonSynthesis/SaturatedSolinas.v
index 2549d190a..6de66a50f 100644
--- a/src/PushButtonSynthesis/SaturatedSolinas.v
+++ b/src/PushButtonSynthesis/SaturatedSolinas.v
@@ -138,13 +138,13 @@ Section __.
   Local Notation weightf := (weight machine_wordsize 1).
   Local Notation evalf := (eval weightf n).
   Local Notation initial_ctx := (CorrectnessStringification.dyn_context.nil).
-  Local Notation stringify_correctness pre_extra correctness
-    := (stringify_correctness_with_ctx
+  Local Notation "'stringify_correctness!' pre_extra correctness"
+    := (stringify_correctness_with_ctx!
           initial_ctx
           evalf
           pre_extra
           correctness)
-         (only parsing).
+         (only parsing, at level 10, pre_extra at next level, correctness at next level).
 
   Definition mul
     := Pipeline.BoundsPipeline
@@ -161,7 +161,7 @@ Section __.
     := Eval cbv beta in
         FromPipelineToString
           prefix "mul" mul
-          (stringify_correctness
+          (stringify_correctness!
              (fun fname : string => ["The function " ++ fname ++ " multiplies two field elements."]%string)
              (mul_correct weightf n m boundsn)).
 
diff --git a/src/PushButtonSynthesis/UnsaturatedSolinas.v b/src/PushButtonSynthesis/UnsaturatedSolinas.v
index 9730eb5e4..e443e7296 100644
--- a/src/PushButtonSynthesis/UnsaturatedSolinas.v
+++ b/src/PushButtonSynthesis/UnsaturatedSolinas.v
@@ -261,13 +261,13 @@ else:
   Local Notation weightf := (weight (Qnum limbwidth) (QDen limbwidth)).
   Local Notation evalf := (eval weightf n).
   Local Notation initial_ctx := (CorrectnessStringification.dyn_context.cons m "m"%string CorrectnessStringification.dyn_context.nil).
-  Local Notation stringify_correctness pre_extra correctness
-    := (stringify_correctness_with_ctx
+  Local Notation "'stringify_correctness!' pre_extra correctness"
+    := (stringify_correctness_with_ctx!
           initial_ctx
           evalf
           pre_extra
           correctness)
-         (only parsing).
+         (only parsing, at level 10, pre_extra at next level, correctness at next level).
 
   Definition carry_mul
     := Pipeline.BoundsPipeline
@@ -284,7 +284,7 @@ else:
     := Eval cbv beta in
         FromPipelineToString
           prefix "carry_mul" carry_mul
-          (stringify_correctness
+          (stringify_correctness!
              (fun fname : string => ["The function " ++ fname ++ " multiplies two field elements and reduces the result."]%string)
              (carry_mul_correct weightf n m tight_bounds loose_bounds)).
 
@@ -303,7 +303,7 @@ else:
     := Eval cbv beta in
         FromPipelineToString
           prefix "carry_square" carry_square
-          (stringify_correctness
+          (stringify_correctness!
              (fun fname : string => ["The function " ++ fname ++ " squares a field element and reduces the result."]%string)
              (carry_square_correct weightf n m tight_bounds loose_bounds)).
 
@@ -322,7 +322,7 @@ else:
     := Eval cbv beta in
         FromPipelineToString
           prefix ("carry_scmul_" ++ decimal_string_of_Z x) (carry_scmul_const x)
-          (stringify_correctness
+          (stringify_correctness!
              (fun fname : string => ["The function " ++ fname ++ " multiplies a field element by " ++ decimal_string_of_Z x ++ " and reduces the result."]%string)
              (carry_scmul_const_correct weightf n m tight_bounds loose_bounds x)).
 
@@ -341,7 +341,7 @@ else:
     := Eval cbv beta in
         FromPipelineToString
           prefix "carry" carry
-          (stringify_correctness
+          (stringify_correctness!
              (fun fname : string => ["The function " ++ fname ++ " reduces a field element."]%string)
              (carry_correct weightf n m tight_bounds loose_bounds)).
 
@@ -360,7 +360,7 @@ else:
     := Eval cbv beta in
         FromPipelineToString
           prefix "add" add
-          (stringify_correctness
+          (stringify_correctness!
              (fun fname : string => ["The function " ++ fname ++ " adds two field elements."]%string)
              (add_correct weightf n m tight_bounds loose_bounds)).
 
@@ -379,7 +379,7 @@ else:
     := Eval cbv beta in
         FromPipelineToString
           prefix "sub" sub
-          (stringify_correctness
+          (stringify_correctness!
              (fun fname : string => ["The function " ++ fname ++ " subtracts two field elements."]%string)
              (sub_correct weightf n m tight_bounds loose_bounds)).
 
@@ -398,7 +398,7 @@ else:
     := Eval cbv beta in
         FromPipelineToString
           prefix "opp" opp
-          (stringify_correctness
+          (stringify_correctness!
              (fun fname : string => ["The function " ++ fname ++ " negates a field element."]%string)
              (opp_correct weightf n m tight_bounds loose_bounds)).
 
@@ -417,7 +417,7 @@ else:
     := Eval cbv beta in
         FromPipelineToString
           prefix "to_bytes" to_bytes
-          (stringify_correctness
+          (stringify_correctness!
              (fun fname : string => ["The function " ++ fname ++ " serializes a field element to bytes in little-endian order."]%string)
              (to_bytes_correct weightf n n_bytes m tight_bounds)).
 
@@ -436,7 +436,7 @@ else:
     := Eval cbv beta in
         FromPipelineToString
           prefix "from_bytes" from_bytes
-          (stringify_correctness
+          (stringify_correctness!
              (fun fname : string => ["The function " ++ fname ++ " deserializes a field element from bytes in little-endian order."]%string)
              (from_bytes_correct weightf n n_bytes m s tight_bounds)).
 
@@ -455,7 +455,7 @@ else:
     := Eval cbv beta in
         FromPipelineToString
           prefix "encode" encode
-          (stringify_correctness
+          (stringify_correctness!
              (fun fname : string => ["The function " ++ fname ++ " encodes an integer as a field element."]%string)
              (encode_correct weightf n m tight_bounds)).
 
@@ -474,7 +474,7 @@ else:
     := Eval cbv beta in
         FromPipelineToString
           prefix "zero" zero
-          (stringify_correctness
+          (stringify_correctness!
              (fun fname => ["The function " ++ fname ++ " returns the field element zero."]%string)
              (zero_correct weightf n m tight_bounds)).
 
@@ -493,7 +493,7 @@ else:
     := Eval cbv beta in
         FromPipelineToString
           prefix "one" one
-          (stringify_correctness
+          (stringify_correctness!
              (fun fname => ["The function " ++ fname ++ " returns the field element one."]%string)
              (one_correct weightf n m tight_bounds)).
 
diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v
index d95f35bf4..b368f352e 100644
--- a/src/PushButtonSynthesis/WordByWordMontgomery.v
+++ b/src/PushButtonSynthesis/WordByWordMontgomery.v
@@ -240,13 +240,13 @@ Section __.
                    (@eval 8 n_bytes) "bytes_eval"%string
                    CorrectnessStringification.dyn_context.nil))))
          (only parsing).
-  Local Notation stringify_correctness prefix pre_extra correctness
-    := (stringify_correctness_with_ctx
+  Local Notation "'stringify_correctness!' prefix pre_extra correctness"
+    := (stringify_correctness_with_ctx!
           (initial_ctx prefix)
           evalf
           pre_extra
           correctness)
-         (only parsing).
+         (only parsing, at level 10, prefix at next level, pre_extra at next level, correctness at next level).
 
   Definition mul
     := Pipeline.BoundsPipeline
@@ -263,7 +263,7 @@ Section __.
     := Eval cbv beta in
         FromPipelineToString
           prefix "mul" mul
-          (stringify_correctness
+          (stringify_correctness!
              prefix
              (fun fname : string => ["The function " ++ fname ++ " multiplies two field elements in the Montgomery domain."]%string)
              (mul_correct machine_wordsize n m valid from_montgomery_res)).
@@ -283,7 +283,7 @@ Section __.
     := Eval cbv beta in
         FromPipelineToString
           prefix "square" square
-          (stringify_correctness
+          (stringify_correctness!
              prefix
              (fun fname : string => ["The function " ++ fname ++ " squares a field element in the Montgomery domain."]%string)
              (square_correct machine_wordsize n m valid from_montgomery_res)).
@@ -303,7 +303,7 @@ Section __.
     := Eval cbv beta in
         FromPipelineToString
           prefix "add" add
-          (stringify_correctness
+          (stringify_correctness!
              prefix
              (fun fname : string => ["The function " ++ fname ++ " adds two field elements in the Montgomery domain."]%string)
              (add_correct machine_wordsize n m valid from_montgomery_res)).
@@ -323,7 +323,7 @@ Section __.
     := Eval cbv beta in
         FromPipelineToString
           prefix "sub" sub
-          (stringify_correctness
+          (stringify_correctness!
              prefix
              (fun fname : string => ["The function " ++ fname ++ " subtracts two field elements in the Montgomery domain."]%string)
              (sub_correct machine_wordsize n m valid from_montgomery_res)).
@@ -343,7 +343,7 @@ Section __.
     := Eval cbv beta in
         FromPipelineToString
           prefix "opp" opp
-          (stringify_correctness
+          (stringify_correctness!
              prefix
              (fun fname : string => ["The function " ++ fname ++ " negates a field element in the Montgomery domain."]%string)
              (opp_correct machine_wordsize n m valid from_montgomery_res)).
@@ -363,7 +363,7 @@ Section __.
     := Eval cbv beta in
         FromPipelineToString
           prefix "from_montgomery" from_montgomery
-          (stringify_correctness
+          (stringify_correctness!
              prefix
              (fun fname : string => ["The function " ++ fname ++ " translates a field element out of the Montgomery domain."]%string)
              (from_montgomery_correct machine_wordsize n m r' valid)).
@@ -382,7 +382,7 @@ Section __.
     := Eval cbv beta in
         FromPipelineToString
           prefix "nonzero" nonzero
-          (stringify_correctness
+          (stringify_correctness!
              prefix
              (fun fname : string => ["The function " ++ fname ++ " outputs a single non-zero word if the input is non-zero and zero otherwise."]%string)
              (nonzero_correct machine_wordsize n m valid from_montgomery_res)).
@@ -402,7 +402,7 @@ Section __.
     := Eval cbv beta in
         FromPipelineToString
           prefix "to_bytes" to_bytes
-          (stringify_correctness
+          (stringify_correctness!
              prefix
              (fun fname : string => ["The function " ++ fname ++ " serializes a field element in the Montgomery domain to bytes in little-endian order."]%string)
              (to_bytes_correct machine_wordsize n n_bytes m valid)).
@@ -422,7 +422,7 @@ Section __.
     := Eval cbv beta in
         FromPipelineToString
           prefix "from_bytes" from_bytes
-          (stringify_correctness
+          (stringify_correctness!
              prefix
              (fun fname : string => ["The function " ++ fname ++ " deserializes a field element in the Montgomery domain from bytes in little-endian order."]%string)
              (from_bytes_correct machine_wordsize n n_bytes m valid bytes_valid)).
@@ -442,7 +442,7 @@ Section __.
     := Eval cbv beta in
         FromPipelineToString
           prefix "encode" encode
-          (stringify_correctness
+          (stringify_correctness!
              prefix
              (fun fname : string => ["The function " ++ fname ++ " encodes an integer as a field element in the Montgomery domain."]%string)
              (encode_correct machine_wordsize n m valid from_montgomery_res)).
@@ -462,7 +462,7 @@ Section __.
     := Eval cbv beta in
         FromPipelineToString
           prefix "zero" zero
-          (stringify_correctness
+          (stringify_correctness!
              prefix
              (fun fname => ["The function " ++ fname ++ " returns the field element zero in the Montgomery domain."]%string)
              (zero_correct machine_wordsize n m valid from_montgomery_res)).
@@ -482,7 +482,7 @@ Section __.
     := Eval cbv beta in
         FromPipelineToString
           prefix "one" one
-          (stringify_correctness
+          (stringify_correctness!
              prefix
              (fun fname => ["The function " ++ fname ++ " returns the field element one in the Montgomery domain."]%string)
              (one_correct machine_wordsize n m valid from_montgomery_res)).