diff options
author | Jason Gross <jgross@mit.edu> | 2017-06-29 13:05:21 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-06-29 13:05:21 -0400 |
commit | ff89c5cc3fb7240c1e87d4234ab8b84859fc23ea (patch) | |
tree | 31454e48d61359099ec89d7250dc2587508cde33 /src/Arithmetic | |
parent | 0ff642cd6a6901c3fb0805092df40f5432280ef1 (diff) |
Adapt to new arguments of saturated things
Diffstat (limited to 'src/Arithmetic')
-rw-r--r-- | src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v | 18 | ||||
-rw-r--r-- | src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v | 8 |
2 files changed, 13 insertions, 13 deletions
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v index d1221d006..f344cb7de 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v @@ -22,8 +22,8 @@ Section WordByWordMontgomery. (N : T R_numlimbs). Local Notation scmul := (@scmul (Z.pos r)). - Local Notation addT' := (fun n => @Saturated.add (Z.pos r) (S n) n (S n)). - Local Notation addT := (fun n => @Saturated.add (Z.pos r) n n n). + Local Notation addT' := (@Saturated.add_S1 (Z.pos r)). + Local Notation addT := (@Saturated.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 := @@ -32,23 +32,23 @@ Section WordByWordMontgomery. Definition redc_body_no_cps (B : T R_numlimbs) (k : Z) {pred_A_numlimbs} (A_S : T (S pred_A_numlimbs) * T (S R_numlimbs)) : T pred_A_numlimbs * T (S R_numlimbs) - := @redc_body T (@divmod) r R_numlimbs (@scmul) addT addT' (@drop_high (S R_numlimbs)) N B k _ A_S. + := @redc_body T (@divmod) r R_numlimbs (@scmul) (@addT) (@addT') (@drop_high (S R_numlimbs)) N B k _ A_S. Definition redc_loop_no_cps (B : T R_numlimbs) (k : Z) (count : nat) (A_S : T count * T (S R_numlimbs)) : T 0 * T (S R_numlimbs) - := @redc_loop T (@divmod) r R_numlimbs (@scmul) addT addT' (@drop_high (S R_numlimbs)) N B k count A_S. + := @redc_loop T (@divmod) r R_numlimbs (@scmul) (@addT) (@addT') (@drop_high (S R_numlimbs)) N B k count A_S. Definition pre_redc_no_cps {A_numlimbs} (A : T A_numlimbs) (B : T R_numlimbs) (k : Z) : T (S R_numlimbs) - := @pre_redc T (@zero) (@divmod) r R_numlimbs (@scmul) addT addT' (@drop_high (S R_numlimbs)) N _ A B k. + := @pre_redc T (@zero) (@divmod) r R_numlimbs (@scmul) (@addT) (@addT') (@drop_high (S R_numlimbs)) N _ A B k. Definition redc_no_cps {A_numlimbs} (A : T A_numlimbs) (B : T R_numlimbs) (k : Z) : T R_numlimbs - := @redc T (@zero) (@divmod) r R_numlimbs (@scmul) addT addT' (@drop_high (S R_numlimbs)) conditional_sub N _ A B k. + := @redc T (@zero) (@divmod) r R_numlimbs (@scmul) (@addT) (@addT') (@drop_high (S R_numlimbs)) conditional_sub N _ A B k. Definition redc_body_cps {pred_A_numlimbs} (A : T (S pred_A_numlimbs)) (B : T R_numlimbs) (k : Z) (S' : T (S R_numlimbs)) {cpsT} (rest : T pred_A_numlimbs * T (S R_numlimbs) -> cpsT) : cpsT := divmod_cps A (fun '(A, a) => - @scmul_cps r _ a B _ (fun aB => @add_cps r _ _ (S R_numlimbs) S' aB _ (fun S1 => + @scmul_cps r _ a B _ (fun aB => @add_cps r _ S' aB _ (fun S1 => divmod_cps S1 (fun '(_, s) => dlet q := fst (Z.mul_split r s k) in - @scmul_cps r _ q N _ (fun qN => @add_cps r _ _ _ S1 qN _ (fun S2 => + @scmul_cps r _ q N _ (fun qN => @add_S1_cps r _ S1 qN _ (fun S2 => divmod_cps S2 (fun '(S3, _) => @drop_high_cps (S R_numlimbs) S3 _ (fun S4 => rest (A, S4))))))))). @@ -85,7 +85,7 @@ Section WordByWordMontgomery. := @opp T (@zero) R_numlimbs (@sub_then_maybe_add) A. Definition add_cps (A B : T R_numlimbs) {cpsT} (rest : T R_numlimbs -> cpsT) : cpsT - := @add_cps r _ _ R_numlimbs A B + := @add_cps r _ A B _ (fun v => conditional_sub_cps v rest). Definition add (A B : T R_numlimbs) : T R_numlimbs := add_cps A B id. diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v index a55f9cffe..747280fe6 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v @@ -16,8 +16,8 @@ Section WordByWordMontgomery. (R_numlimbs : nat). Local Notation small := (@small (Z.pos r)). Local Notation eval := (@eval (Z.pos r)). - Local Notation addT' := (fun n => @Saturated.add (Z.pos r) (S n) n (S n)). - Local Notation addT := (fun n => @Saturated.add (Z.pos r) n n n). + Local Notation addT' := (@Saturated.add_S1 (Z.pos r)). + Local Notation addT := (@Saturated.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 _)). @@ -65,7 +65,7 @@ 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 Saturated.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 _). @@ -225,7 +225,7 @@ Section WordByWordMontgomery. Local Notation eval_sub_then_maybe_add := (fun p q smp smq => @eval_sub_then_maybe_add (Z.pos r) (Zorder.Zgt_pos_0 _) _ (Z.pos r - 1) p q N smp smq small_N N_mask). Local Notation small_sub_then_maybe_add := - (fun p q => @small_sub_then_maybe_add (Z.pos r) (Zorder.Zgt_pos_0 _) _ (Z.pos r - 1) p q N). + (fun p q => @small_sub_then_maybe_add (Z.pos r) (*(Zorder.Zgt_pos_0 _)*) _ (Z.pos r - 1) p q N). Definition add_no_cps_bound : 0 <= eval add_no_cps < eval N := @add_bound T (@eval) r R R_numlimbs (@small) (@addT) (@eval_addT) (@small_addT) N N_lt_R (@conditional_sub) (@eval_conditional_sub) Av Bv small_Av small_Bv Av_bound Bv_bound. |