diff options
author | Jason Gross <jagro@google.com> | 2016-09-07 11:55:45 -0700 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2016-09-07 11:55:45 -0700 |
commit | 3e4736375dd59570c30d647dd9b760dc030ebd3f (patch) | |
tree | c1e1e077a72ad0ec69bc7aa85e2e92331e176cc1 /src | |
parent | e4e860f8b10a1b8ce1ab207f12c7ef50e36332c4 (diff) |
Better spec in Montgomery.ZBounded
Diffstat (limited to 'src')
-rw-r--r-- | src/ModularArithmetic/Montgomery/ZBounded.v | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/ModularArithmetic/Montgomery/ZBounded.v b/src/ModularArithmetic/Montgomery/ZBounded.v index d01a48d89..2da20ddcf 100644 --- a/src/ModularArithmetic/Montgomery/ZBounded.v +++ b/src/ModularArithmetic/Montgomery/ZBounded.v @@ -78,7 +78,7 @@ Section montgomery. eauto 6 using reduce_via_partial_correct, reduce_via_partial_in_range, decode_small_valid. Qed. - Theorem reduce_via_partial_correct + Lemma reduce_via_partial_correct'' : Z.equiv_modulo modulus (decode_small (proj1_sig (reduce_via_partial v))) (decode_large v * R') @@ -88,5 +88,13 @@ Section montgomery. apply decode_small_valid in H'. destruct reduce_via_partial_correct'; split; eauto; omega. Qed. + + Theorem reduce_via_partial_correct + : decode_small (proj1_sig (reduce_via_partial v)) = (decode_large v * R') mod modulus. + Proof. + rewrite <- (proj1 reduce_via_partial_correct''). + rewrite Z.mod_small by apply reduce_via_partial_correct''. + reflexivity. + Qed. End correctness. End montgomery. |