diff options
| author |  jadep <jade.philipoom@gmail.com> | 2017-06-29 21:32:04 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2017-06-29 21:32:04 -0400 |
| commit | 2876f7c688590a64189f47b439f7edf26c91c5de (patch) | |
| tree | fffe55bc24e83105fca356a81a352e1fa4309999 /src/Arithmetic/MontgomeryReduction | |
| parent | b291707642db5986240b3e9eb9a80839d81ffe42 (diff) | |
Reorganization of saturated arithmetic
Diffstat (limited to 'src/Arithmetic/MontgomeryReduction')
| -rw-r--r-- | src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v | 6 | ||||
| -rw-r--r-- | src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v | 11 |
2 files changed, 9 insertions, 8 deletions
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v index f344cb7de..9affa82fa 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v @@ -5,7 +5,7 @@ of the algorithm; note that it may be that none of the algorithms there exactly match what we're doing here. *) Require Import Coq.ZArith.ZArith. -Require Import Crypto.Arithmetic.Saturated. +Require Import Crypto.Arithmetic.Saturated.MontgomeryAPI. Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Abstract.Dependent.Definition. Require Import Crypto.Util.Notations. Require Import Crypto.Util.LetIn. @@ -22,8 +22,8 @@ Section WordByWordMontgomery. (N : T R_numlimbs). Local Notation scmul := (@scmul (Z.pos r)). - Local Notation addT' := (@Saturated.add_S1 (Z.pos r)). - Local Notation addT := (@Saturated.add (Z.pos r)). + Local Notation addT' := (@MontgomeryAPI.add_S1 (Z.pos r)). + Local Notation addT := (@MontgomeryAPI.add (Z.pos r)). Local Notation conditional_sub_cps := (fun V => @conditional_sub_cps (Z.pos r) _ V N _). Local Notation conditional_sub := (fun V => @conditional_sub (Z.pos r) _ V N). Local Notation sub_then_maybe_add_cps := diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v index 747280fe6..83791ec5f 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v @@ -1,7 +1,8 @@ (*** Word-By-Word Montgomery Multiplication Proofs *) Require Import Coq.ZArith.BinInt. Require Import Coq.micromega.Lia. -Require Import Crypto.Arithmetic.Saturated. +Require Import Crypto.Arithmetic.Saturated.UniformWeight. +Require Import Crypto.Arithmetic.Saturated.MontgomeryAPI. Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Abstract.Dependent.Definition. Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Abstract.Dependent.Proofs. Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition. @@ -16,8 +17,8 @@ Section WordByWordMontgomery. (R_numlimbs : nat). Local Notation small := (@small (Z.pos r)). Local Notation eval := (@eval (Z.pos r)). - Local Notation addT' := (@Saturated.add_S1 (Z.pos r)). - Local Notation addT := (@Saturated.add (Z.pos r)). + Local Notation addT' := (@MontgomeryAPI.add_S1 (Z.pos r)). + Local Notation addT := (@MontgomeryAPI.add (Z.pos r)). Local Notation scmul := (@scmul (Z.pos r)). Local Notation eval_zero := (@eval_zero (Z.pos r)). Local Notation small_zero := (@small_zero r (Zorder.Zgt_pos_0 _)). @@ -61,11 +62,11 @@ Section WordByWordMontgomery. Qed. Local Lemma small_addT : forall n a b, small a -> small b -> small (@addT n a b). Proof. - intros; apply Saturated.small_add; auto; lia. + intros; apply MontgomeryAPI.small_add; auto; lia. Qed. Local Lemma small_addT' : forall n a b, small a -> small b -> small (@addT' n a b). Proof. - intros; apply Saturated.small_add_S1; auto; lia. + intros; apply MontgomeryAPI.small_add_S1; auto; lia. Qed. Local Notation conditional_sub_cps := (fun V : T (S R_numlimbs) => @conditional_sub_cps (Z.pos r) _ V N _). |