From ad2af1d46963f9496d56a6185100fb34199854e7 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 30 Jan 2019 23:32:26 -0500 Subject: Drop `map λ` bits in docstrings MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit They are redundant with the bounds pre- and post-conditions in WBW montgomery. Also drop the fiat_p... prefix from the `from_montgomery` bits in most of the docstrings, under the assumption that shorter strings with less repetition are more readable. --- src/PushButtonSynthesis/Primitives.v | 9 +++++++-- src/PushButtonSynthesis/WordByWordMontgomery.v | 5 +++-- 2 files changed, 10 insertions(+), 4 deletions(-) (limited to 'src/PushButtonSynthesis') diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v index ee2793c40..4d3e9c047 100644 --- a/src/PushButtonSynthesis/Primitives.v +++ b/src/PushButtonSynthesis/Primitives.v @@ -183,6 +183,9 @@ Module CorrectnessStringification. => strip_bounds_info T | list_Z_bounded_by _ _ -> ?T => strip_bounds_info T + | (_ = List.map (fun z => (_ mod _) / _) (List.seq _ _)) /\ (?a <= ?b < ?c) -> ?T + => let T := strip_bounds_info T in + constr:(a <= b < c -> T) | ?T /\ list_Z_bounded_by _ _ => T | ?T /\ (match _ with pair _ _ => _ end = true) @@ -191,8 +194,10 @@ Module CorrectnessStringification. => T | iff _ _ => correctness - | _ = _ /\ (_ = _ /\ (_ <= _ < _)) - => correctness + | ?x = ?y /\ (_ = List.map (fun z => (_ mod _) / _) (List.seq _ _)) /\ (?a <= ?b < ?c) + => constr:(x = y /\ a <= b < c) + | (_ = List.map (fun z => (_ mod _) / _) (List.seq _ _)) /\ (?a <= ?b < ?c) + => constr:(a <= b < c) | _ = _ :> list Z => correctness | forall x : ?T, ?f diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v index 46ffa083f..d95f35bf4 100644 --- a/src/PushButtonSynthesis/WordByWordMontgomery.v +++ b/src/PushButtonSynthesis/WordByWordMontgomery.v @@ -235,10 +235,11 @@ Section __. (CorrectnessStringification.dyn_context.cons r' ("((2^" ++ decimal_string_of_Z machine_wordsize ++ ")⁻¹ mod m)")%string (CorrectnessStringification.dyn_context.cons - from_montgomery_res (prefix ++ "from_montgomery")%string + from_montgomery_res "from_montgomery"%string (CorrectnessStringification.dyn_context.cons (@eval 8 n_bytes) "bytes_eval"%string - CorrectnessStringification.dyn_context.nil)))). + CorrectnessStringification.dyn_context.nil)))) + (only parsing). Local Notation stringify_correctness prefix pre_extra correctness := (stringify_correctness_with_ctx (initial_ctx prefix) -- cgit v1.2.3