Address code review comments to improve docstrings

4 files changed, 32 insertions, 30 deletions

diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v
index e45940369..ee2793c40 100644
--- a/src/PushButtonSynthesis/Primitives.v
+++ b/src/PushButtonSynthesis/Primitives.v
@@ -660,7 +660,7 @@ Section __.
           prefix ("addcarryx_u" ++ decimal_string_of_Z s) (addcarryx s)
           (stringify_correctness
              evalf
-             (fun fname : string => ["The function " ++ fname ++ " is an add with carry."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " is an addition with carry."]%string)
              (addcarryx_correct s)).
 
   Definition subborrowx (s : Z)
@@ -680,7 +680,7 @@ Section __.
           prefix ("subborrowx_u" ++ decimal_string_of_Z s) (subborrowx s)
           (stringify_correctness
              evalf
-             (fun fname : string => ["The function " ++ fname ++ " is a sub with borrow."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " is a subtraction with borrow."]%string)
              (subborrowx_correct s)).
 
 
diff --git a/src/PushButtonSynthesis/SaturatedSolinas.v b/src/PushButtonSynthesis/SaturatedSolinas.v
index 7ff799c80..2549d190a 100644
--- a/src/PushButtonSynthesis/SaturatedSolinas.v
+++ b/src/PushButtonSynthesis/SaturatedSolinas.v
@@ -162,7 +162,7 @@ Section __.
         FromPipelineToString
           prefix "mul" mul
           (stringify_correctness
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " multiplies two field elements."]%string)
              (mul_correct weightf n m boundsn)).
 
   Local Ltac solve_extra_bounds_side_conditions :=
diff --git a/src/PushButtonSynthesis/UnsaturatedSolinas.v b/src/PushButtonSynthesis/UnsaturatedSolinas.v
index 75e430a24..9730eb5e4 100644
--- a/src/PushButtonSynthesis/UnsaturatedSolinas.v
+++ b/src/PushButtonSynthesis/UnsaturatedSolinas.v
@@ -285,7 +285,7 @@ else:
         FromPipelineToString
           prefix "carry_mul" carry_mul
           (stringify_correctness
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (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)).
 
   Definition carry_square
@@ -304,7 +304,7 @@ else:
         FromPipelineToString
           prefix "carry_square" carry_square
           (stringify_correctness
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (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)).
 
   Definition carry_scmul_const (x : Z)
@@ -323,7 +323,7 @@ else:
         FromPipelineToString
           prefix ("carry_scmul_" ++ decimal_string_of_Z x) (carry_scmul_const x)
           (stringify_correctness
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (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)).
 
   Definition carry
@@ -342,7 +342,7 @@ else:
         FromPipelineToString
           prefix "carry" carry
           (stringify_correctness
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " reduces a field element."]%string)
              (carry_correct weightf n m tight_bounds loose_bounds)).
 
   Definition add
@@ -361,7 +361,7 @@ else:
         FromPipelineToString
           prefix "add" add
           (stringify_correctness
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " adds two field elements."]%string)
              (add_correct weightf n m tight_bounds loose_bounds)).
 
   Definition sub
@@ -380,7 +380,7 @@ else:
         FromPipelineToString
           prefix "sub" sub
           (stringify_correctness
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " subtracts two field elements."]%string)
              (sub_correct weightf n m tight_bounds loose_bounds)).
 
   Definition opp
@@ -399,7 +399,7 @@ else:
         FromPipelineToString
           prefix "opp" opp
           (stringify_correctness
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (fun fname : string => ["The function " ++ fname ++ " negates a field element."]%string)
              (opp_correct weightf n m tight_bounds loose_bounds)).
 
   Definition to_bytes
@@ -418,7 +418,7 @@ else:
         FromPipelineToString
           prefix "to_bytes" to_bytes
           (stringify_correctness
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (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)).
 
   Definition from_bytes
@@ -437,7 +437,7 @@ else:
         FromPipelineToString
           prefix "from_bytes" from_bytes
           (stringify_correctness
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (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)).
 
   Definition encode
@@ -456,7 +456,7 @@ else:
         FromPipelineToString
           prefix "encode" encode
           (stringify_correctness
-             (fun fname : string => [fname ++ ":"]%string)
+             (fun fname : string => ["The function " ++ fname ++ " encodes an integer as a field element."]%string)
              (encode_correct weightf n m tight_bounds)).
 
   Definition zero
@@ -475,7 +475,7 @@ else:
         FromPipelineToString
           prefix "zero" zero
           (stringify_correctness
-             (fun fname : string => @nil string)
+             (fun fname => ["The function " ++ fname ++ " returns the field element zero."]%string)
              (zero_correct weightf n m tight_bounds)).
 
   Definition one
@@ -494,7 +494,7 @@ else:
         FromPipelineToString
           prefix "one" one
           (stringify_correctness
-             (fun fname : string => @nil string)
+             (fun fname => ["The function " ++ fname ++ " returns the field element one."]%string)
              (one_correct weightf n m tight_bounds)).
 
   Definition selectznz : Pipeline.ErrorT _ := Primitives.selectznz n machine_wordsize.
diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v
index f64e4a8c3..46ffa083f 100644
--- a/src/PushButtonSynthesis/WordByWordMontgomery.v
+++ b/src/PushButtonSynthesis/WordByWordMontgomery.v
@@ -233,10 +233,12 @@ Section __.
     := (CorrectnessStringification.dyn_context.cons
           m "m"%string
           (CorrectnessStringification.dyn_context.cons
-             from_montgomery_res (prefix ++ "from_montgomery")%string
+             r' ("((2^" ++ decimal_string_of_Z machine_wordsize ++ ")⁻¹ mod m)")%string
              (CorrectnessStringification.dyn_context.cons
-                (@eval 8 n_bytes) "bytes_eval"%string
-                CorrectnessStringification.dyn_context.nil))).
+                from_montgomery_res (prefix ++ "from_montgomery")%string
+                (CorrectnessStringification.dyn_context.cons
+                   (@eval 8 n_bytes) "bytes_eval"%string
+                   CorrectnessStringification.dyn_context.nil)))).
   Local Notation stringify_correctness prefix pre_extra correctness
     := (stringify_correctness_with_ctx
           (initial_ctx prefix)
@@ -262,7 +264,7 @@ Section __.
           prefix "mul" mul
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (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)).
 
   Definition square
@@ -282,7 +284,7 @@ Section __.
           prefix "square" square
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (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)).
 
   Definition add
@@ -302,7 +304,7 @@ Section __.
           prefix "add" add
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (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)).
 
   Definition sub
@@ -322,7 +324,7 @@ Section __.
           prefix "sub" sub
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (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)).
 
   Definition opp
@@ -342,7 +344,7 @@ Section __.
           prefix "opp" opp
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (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)).
 
   Definition from_montgomery
@@ -362,7 +364,7 @@ Section __.
           prefix "from_montgomery" from_montgomery
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (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)).
 
   Definition nonzero
@@ -381,7 +383,7 @@ Section __.
           prefix "nonzero" nonzero
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (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)).
 
   Definition to_bytes
@@ -401,7 +403,7 @@ Section __.
           prefix "to_bytes" to_bytes
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (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)).
 
   Definition from_bytes
@@ -421,7 +423,7 @@ Section __.
           prefix "from_bytes" from_bytes
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (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)).
 
   Definition encode
@@ -441,7 +443,7 @@ Section __.
           prefix "encode" encode
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (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)).
 
   Definition zero
@@ -461,7 +463,7 @@ Section __.
           prefix "zero" zero
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (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)).
 
   Definition one
@@ -481,7 +483,7 @@ Section __.
           prefix "one" one
           (stringify_correctness
              prefix
-             (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string)
+             (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)).
 
   Definition selectznz : Pipeline.ErrorT _ := Primitives.selectznz n machine_wordsize.