From 6fbafbb3a90a5491103e0044042bfc726b9eab7b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 30 Jan 2019 23:04:35 -0500 Subject: Address code review comments to improve docstrings --- src/PushButtonSynthesis/Primitives.v | 4 ++-- src/PushButtonSynthesis/SaturatedSolinas.v | 2 +- src/PushButtonSynthesis/UnsaturatedSolinas.v | 24 +++++++++---------- src/PushButtonSynthesis/WordByWordMontgomery.v | 32 ++++++++++++++------------ 4 files changed, 32 insertions(+), 30 deletions(-) (limited to 'src/PushButtonSynthesis') 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. -- cgit v1.2.3