diff options
Diffstat (limited to 'src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v')
| -rw-r--r-- | src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v index 9affa82fa..fd4869f23 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v @@ -10,6 +10,7 @@ Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Abstract.Depende Require Import Crypto.Util.Notations. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.CPS. Local Open Scope Z_scope. @@ -47,10 +48,11 @@ Section WordByWordMontgomery. := divmod_cps A (fun '(A, a) => @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 + Z.mul_split_cps' r s k (fun mul_split_r_s_k => + dlet q := fst mul_split_r_s_k in @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))))))))). + @drop_high_cps (S R_numlimbs) S3 _ (fun S4 => rest (A, S4)))))))))). Section loop. Context {A_numlimbs} (A : T A_numlimbs) (B : T R_numlimbs) (k : Z) {cpsT : Type}. |