diff options
Diffstat (limited to 'src/COperationSpecifications.v')
-rw-r--r-- | src/COperationSpecifications.v | 606 |
1 files changed, 606 insertions, 0 deletions
diff --git a/src/COperationSpecifications.v b/src/COperationSpecifications.v new file mode 100644 index 000000000..e8ae7d11e --- /dev/null +++ b/src/COperationSpecifications.v @@ -0,0 +1,606 @@ +(** * C Operation Specifications *) +(** The specifications for the various operations to be synthesized. *) +Require Import Coq.ZArith.ZArith Coq.micromega.Lia. +Require Import Coq.Lists.List. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.Bool. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.ListUtil.FoldBool. +Require Import Crypto.Util.Tactics.SpecializeBy. +Require Import Crypto.Util.Tactics.SplitInContext. +Require Import Crypto.Util.Tactics.UniquePose. +Require Import Crypto.Arithmetic. +Local Open Scope Z_scope. Local Open Scope bool_scope. + +(** These Imports are only needed for the ring proof *) +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Algebra.Ring. +Require Import Crypto.Algebra.SubsetoidRing. + +Local Notation is_bounded_by0 r v +:= ((lower r%zrange <=? v) && (v <=? upper r%zrange)). +Local Notation is_bounded_by2 r v + := (let '(v1, v2) := v in is_bounded_by0 (fst r) v1 && is_bounded_by0 (snd r) v2). +Local Notation is_bounded_by0o r + := (match r with Some r' => fun v' => is_bounded_by0 r' v' | None => fun _ => true end). +Local Notation is_bounded_by bounds ls + := (fold_andb_map (fun r v'' => is_bounded_by0o r v'') bounds ls). + +Section list_Z_bounded. + Definition list_Z_bounded_by + (bounds : list (option zrange)) + (v : list Z) + := is_bounded_by bounds v = true. + + Lemma length_list_Z_bounded_by bounds ls + : list_Z_bounded_by bounds ls -> length ls = length bounds. + Proof using Type. + intro H. + apply fold_andb_map_length in H; congruence. + Qed. + + Lemma eval_list_Z_bounded_by wt n' bounds bounds' f + (H : list_Z_bounded_by bounds f) + (Hb : bounds = List.map (@Some _) bounds') + (Hblen : length bounds' = n') + (Hwt : forall i, List.In i (seq 0 n') -> 0 <= wt i) + : Positional.eval wt n' (List.map lower bounds') <= Positional.eval wt n' f <= Positional.eval wt n' (List.map upper bounds'). + Proof using Type. + setoid_rewrite in_seq in Hwt. + subst bounds. + pose proof H as H'; apply fold_andb_map_length in H'. + revert dependent bounds'; intro bounds'. + revert dependent f; intro f. + rewrite <- (List.rev_involutive bounds'), <- (List.rev_involutive f); + generalize (List.rev bounds') (List.rev f); clear bounds' f; intros bounds f; revert bounds f. + induction n' as [|n IHn], bounds as [|b bounds], f as [|f fs]; intros; + cbn [length rev map] in *; distr_length. + { rewrite !map_app in *; cbn [map] in *. + erewrite !Positional.eval_snoc by (distr_length; eauto). + cbv [list_Z_bounded_by] in *. + specialize_by (intros; auto with omega). + specialize (Hwt n); specialize_by omega. + repeat first [ progress Bool.split_andb + | rewrite Nat.add_1_r in * + | rewrite fold_andb_map_snoc in * + | rewrite Nat.succ_inj_wd in * + | progress Z.ltb_to_lt + | progress cbn [In seq] in * + | match goal with + | [ H : length _ = ?v |- _ ] => rewrite H in * + | [ H : ?v = length _ |- _ ] => rewrite <- H in * + end ]. + split; apply Z.add_le_mono; try apply IHn; auto; distr_length; nia. } + Qed. +End list_Z_bounded. + +Ltac pose_proof_length_list_Z_bounded_by := + repeat match goal with + | [ H : list_Z_bounded_by _ _ |- _ ] => unique pose proof (length_list_Z_bounded_by _ _ H) + end. + +Module Primitives. + Definition mulx_correct s + (mulx : Z -> Z -> Z * Z) + := forall x y, + is_bounded_by0 r[0~>2^s-1] x = true + -> is_bounded_by0 r[0~>2^s-1] y = true + -> mulx x y = ((x * y) mod 2^s, (x * y) / 2^s) + /\ is_bounded_by2 (r[0~>2^s-1], r[0~>2^s-1]) (mulx x y) = true. + + Definition addcarryx_correct s + (addcarryx : Z -> Z -> Z -> Z * Z) + := forall c x y, + is_bounded_by0 r[0~>1] c = true + -> is_bounded_by0 r[0~>2^s-1] x = true + -> is_bounded_by0 r[0~>2^s-1] y = true + -> addcarryx c x y = ((c + x + y) mod 2^s, (c + x + y) / 2^s) + /\ is_bounded_by2 (r[0~>2^s-1], r[0~>1]) (addcarryx c x y) = true. + + Definition subborrowx_correct s + (subborrowx : Z -> Z -> Z -> Z * Z) + := forall b x y, + is_bounded_by0 r[0~>1] b = true + -> is_bounded_by0 r[0~>2^s-1] x = true + -> is_bounded_by0 r[0~>2^s-1] y = true + -> subborrowx b x y = ((-b + x + -y) mod 2^s, -((-b + x + -y) / 2^s)) + /\ is_bounded_by2 (r[0~>2^s-1], r[0~>1]) (subborrowx b x y) = true. + + Definition cmovznz_correct s + (cmovznz : Z -> Z -> Z -> Z) + := forall cond z nz, + is_bounded_by0 r[0~>1] cond = true + -> is_bounded_by0 r[0~>2^s-1] z = true + -> is_bounded_by0 r[0~>2^s-1] nz = true + -> cmovznz cond z nz = (if Decidable.dec (cond = 0) then z else nz) + /\ is_bounded_by0 r[0~>2^s-1] (cmovznz cond z nz) = true. +End Primitives. + +Module selectznz. + Section __. + Context (wt : nat -> Z) + (n : nat) + (saturated_bounds : list (option zrange)) + (length_saturated_bounds : length saturated_bounds = n). + Local Notation eval := (Positional.eval wt n). + + Definition selectznz_correct + (selectznz : Z -> list Z -> list Z -> list Z) + := forall cond x y, + is_bounded_by0 r[0~>1] cond = true + -> list_Z_bounded_by saturated_bounds x + -> list_Z_bounded_by saturated_bounds y + -> eval (selectznz cond x y) = (if Decidable.dec (cond = 0) then eval x else eval y) + /\ list_Z_bounded_by saturated_bounds (selectznz cond x y). + End __. +End selectznz. + +Module Solinas. + (** re-export [selectznz_correct] and the primitives. We + semi-arbitrarily choose to allow [Solinas.selectznz_correct] to + exist, but have the full name of the primitive operations start + with [Primitives.] *) + Export Primitives. + Include selectznz. + + Section __. + Context (wt : nat -> Z) + (n : nat) + (n_bytes : nat) + (m : Z) + (s : Z) (* only for prime_bytes *) + (tight_bounds : list (option zrange)) + (length_tight_bounds : length tight_bounds = n) + (loose_bounds : list (option zrange)) + (length_loose_bounds : length loose_bounds = n) + (saturated_bounds : list (option zrange)) + (length_saturated_bounds : length saturated_bounds = n) + (m_pos : 0 < m). + Local Notation eval := (Positional.eval wt n). + Local Notation bytes_eval := (Positional.eval (weight 8 1) n_bytes). + + Let prime_bytes_upperbound_list : list Z + := Positional.encode_no_reduce (weight 8 1) n_bytes (s-1). + Let prime_bytes_bounds : list (option zrange) + := List.map (fun v => Some r[0 ~> v]%zrange) prime_bytes_upperbound_list. + Let prime_bound : zrange + := r[0~>(m - 1)]%zrange. + + Definition from_bytes_correct + (from_bytes : list Z -> list Z) + := forall x, + list_Z_bounded_by prime_bytes_bounds x + -> eval (from_bytes x) mod m = bytes_eval x mod m + /\ list_Z_bounded_by tight_bounds (from_bytes x). + + Definition to_bytes_correct + (to_bytes : list Z -> list Z) + := forall x, + list_Z_bounded_by tight_bounds x + -> to_bytes x = Partition.partition (weight 8 1) n_bytes (eval x mod m). + + Definition carry_mul_correct + (carry_mul : list Z -> list Z -> list Z) + := forall x y, + list_Z_bounded_by loose_bounds x + -> list_Z_bounded_by loose_bounds y + -> eval (carry_mul x y) mod m = (Z.mul (eval x) (eval y)) mod m + /\ list_Z_bounded_by tight_bounds (carry_mul x y). + + Definition carry_square_correct + (carry_square : list Z -> list Z) + := forall x, + list_Z_bounded_by loose_bounds x + -> eval (carry_square x) mod m = (eval x * eval x) mod m + /\ list_Z_bounded_by tight_bounds (carry_square x). + + Definition carry_scmul_const_correct + (a : Z) + (carry_scmul_const : list Z -> list Z) + := forall x, + list_Z_bounded_by loose_bounds x + -> eval (carry_scmul_const x) mod m = (a * eval x) mod m + /\ list_Z_bounded_by tight_bounds (carry_scmul_const x). + + Definition add_correct + (add : list Z -> list Z -> list Z) + := forall x y, + list_Z_bounded_by tight_bounds x + -> list_Z_bounded_by tight_bounds y + -> eval (add x y) mod m = (Z.add (eval x) (eval y)) mod m + /\ list_Z_bounded_by loose_bounds (add x y). + + Definition sub_correct + (sub : list Z -> list Z -> list Z) + := forall x y, + list_Z_bounded_by tight_bounds x + -> list_Z_bounded_by tight_bounds y + -> eval (sub x y) mod m = (Z.sub (eval x) (eval y)) mod m + /\ list_Z_bounded_by loose_bounds (sub x y). + + Definition opp_correct + (opp : list Z -> list Z) + := forall x, + list_Z_bounded_by tight_bounds x + -> eval (opp x) mod m = (Z.opp (eval x)) mod m + /\ list_Z_bounded_by loose_bounds (opp x). + + Definition carry_correct + (carry : list Z -> list Z) + := forall x, + list_Z_bounded_by loose_bounds x + -> eval (carry x) mod m = (eval x) mod m + /\ list_Z_bounded_by tight_bounds (carry x). + + Definition zero_correct + (zero : list Z) + := eval zero mod m = 0 + /\ list_Z_bounded_by tight_bounds zero. + + Definition one_correct + (one : list Z) + := eval one mod m = 1 mod m + /\ list_Z_bounded_by tight_bounds one. + + Definition encode_correct + (encode : Z -> list Z) + := forall x, + is_bounded_by0 prime_bound x = true + -> eval (encode x) mod m = x mod m + /\ list_Z_bounded_by tight_bounds (encode x). + + Section ring. + Context carry_mul (Hcarry_mul : carry_mul_correct carry_mul) + add (Hadd : add_correct add) + sub (Hsub : sub_correct sub) + opp (Hopp : opp_correct opp) + carry (Hcarry : carry_correct carry) + encode (Hencode : encode_correct encode) + zero (Hzero : zero_correct zero) + one (Hone : one_correct one) + (Hrelax : forall x, list_Z_bounded_by tight_bounds x -> list_Z_bounded_by loose_bounds x). + + Let m' := Z.to_pos m. + + Local Notation T := (list Z) (only parsing). + Local Notation encoded_ok ls + := (is_bounded_by tight_bounds ls = true) (only parsing). + Local Notation encoded_okf := (fun ls => encoded_ok ls) (only parsing). + + Definition Fdecode (v : T) : F m' + := F.of_Z m' (eval v). + Definition T_eq (x y : T) + := Fdecode x = Fdecode y. + + Definition encodedT := sig encoded_okf. + + Definition ring_mul (x y : T) : T := carry_mul x y. + Definition ring_add (x y : T) : T := carry (add x y). + Definition ring_sub (x y : T) : T := carry (sub x y). + Definition ring_opp (x : T) : T := carry (opp x). + Definition ring_encode (x : F m') : T := encode (F.to_Z x). + + Definition GoodT : Prop + := @subsetoid_ring + (list Z) encoded_okf T_eq + zero one ring_opp ring_add ring_sub ring_mul + /\ @is_subsetoid_homomorphism + (F m') (fun _ => True) eq 1%F F.add F.mul + (list Z) encoded_okf T_eq one ring_add ring_mul ring_encode + /\ @is_subsetoid_homomorphism + (list Z) encoded_okf T_eq one ring_add ring_mul + (F m') (fun _ => True) eq 1%F F.add F.mul + Fdecode. + + Hint Rewrite ->@F.to_Z_add : push_FtoZ. + Hint Rewrite ->@F.to_Z_mul : push_FtoZ. + Hint Rewrite ->@F.to_Z_opp : push_FtoZ. + Hint Rewrite ->@F.to_Z_of_Z : push_FtoZ. + + Lemma Fm_bounded_alt (x : F m') + : is_bounded_by0 prime_bound (F.to_Z x) = true. + Proof using m_pos. + clear -m_pos. + destruct x as [x H]; cbn [F.to_Z proj1_sig]. + pose proof (Z.mod_pos_bound x (Z.pos m')). + subst m'; rewrite Z2Pos.id in * by lia. + cbv [prime_bound lower upper]. + rewrite Bool.andb_true_iff; split; Z.ltb_to_lt; lia. + Qed. + + Lemma Good : GoodT. + Proof. + split_and; simpl in *. + repeat match goal with + | [ H : context[andb _ true] |- _ ] => setoid_rewrite andb_true_r in H + end. + all: cbv [carry_mul_correct add_correct sub_correct opp_correct carry_correct encode_correct zero_correct one_correct] in *; split_and. + eapply subsetoid_ring_by_ring_isomorphism; + cbv [ring_opp ring_add ring_sub ring_mul ring_encode F.sub list_Z_bounded_by Fdecode m' F.one] in *; auto. + all: repeat first [ progress intros + | reflexivity + | progress autorewrite with push_FtoZ + | rewrite Z2Pos.id + | apply Fm_bounded_alt + | match goal with + | [ |- _ = _ :> F _ ] => apply F.eq_to_Z_iff + | [ |- _ mod _ = F.to_Z ?x ] + => etransitivity; [ | apply (F.mod_to_Z x) ] + | [ H : _ |- _ ] => apply H; clear H + | [ H : context[eval (?f _) mod ?m = _] |- context[eval (?f _) mod ?m] ] + => rewrite H + | [ H : context[eval (?f _ _) mod ?m = _] |- context[eval (?f _ _) mod ?m] ] + => rewrite H + end + | progress (push_Zmod; pull_Zmod); try (f_equal; lia) ]. + Qed. + End ring. + End __. +End Solinas. + +Module SaturatedSolinas. + Section __. + Context (wt : nat -> Z) + (n : nat) + (m : Z) + (saturated_bounds : list (option zrange)) + (length_saturated_bounds : length saturated_bounds = n). + Local Notation eval := (Positional.eval wt n). + + Definition mul_correct + (mul : list Z -> list Z -> list Z * Z) + := forall x y, + list_Z_bounded_by saturated_bounds x + -> list_Z_bounded_by saturated_bounds y + -> (eval (fst (mul x y)) + wt n * snd (mul x y)) mod m + = (eval x * eval y) mod m + /\ ((let '(v, c) := mul x y in + (is_bounded_by saturated_bounds v) + && true(*Should be: is_bounded_by0 r[0~>0] c, but bounds analysis is not good enough*)) + = true). + End __. +End SaturatedSolinas. + +Module WordByWordMontgomery. + Import Arithmetic.WordByWordMontgomery. + Local Coercion Z.of_nat : nat >-> Z. + Section __. + Context (bitwidth : Z) + (n : nat) + (n_bytes : nat) + (m r' : Z) + (s : Z) (* only for prime_bytes *) + (bounds : list (option zrange)) + (length_bounds : length bounds = n) + (valid : list Z -> Prop) + (bytes_valid : list Z -> Prop) + (m_pos : 0 < m) + (from_montgomery : list Z -> list Z) + (* saturated_bounds is only for selectznz *) + (saturated_bounds : list (option zrange)) + (length_saturated_bounds : length saturated_bounds = n). + Local Notation eval := (@WordByWordMontgomery.eval bitwidth n). + Local Notation bytes_eval := (Positional.eval (weight 8 1) n_bytes). + Let prime_bound : zrange + := r[0~>(m - 1)]%zrange. + + Definition from_montgomery_correct + := forall v, + valid v + -> eval (from_montgomery v) mod m = (eval v * r'^n) mod m + /\ valid (from_montgomery v). + + Definition mul_correct + (mul : list Z -> list Z -> list Z) + := forall a b, + valid a + -> valid b + -> eval (from_montgomery (mul a b)) mod m = (Z.mul (eval (from_montgomery a)) (eval (from_montgomery b))) mod m + /\ valid (mul a b). + + Definition add_correct + (add : list Z -> list Z -> list Z) + := forall a b, + valid a + -> valid b + -> eval (from_montgomery (add a b)) mod m = (Z.add (eval (from_montgomery a)) (eval (from_montgomery b))) mod m + /\ valid (add a b). + + Definition sub_correct + (sub : list Z -> list Z -> list Z) + := forall a b, + valid a + -> valid b + -> eval (from_montgomery (sub a b)) mod m = (Z.sub (eval (from_montgomery a)) (eval (from_montgomery b))) mod m + /\ valid (sub a b). + + Definition opp_correct + (opp : list Z -> list Z) + := forall a, + valid a + -> eval (from_montgomery (opp a)) mod m = (Z.opp (eval (from_montgomery a))) mod m + /\ valid (opp a). + + Definition square_correct + (square : list Z -> list Z) + := forall a, + valid a + -> eval (from_montgomery (square a)) mod m = (eval (from_montgomery a) * eval (from_montgomery a)) mod m + /\ valid (square a). + + Definition zero_correct + (zero : list Z) + := eval (from_montgomery zero) mod m = 0 + /\ valid zero. + + Definition one_correct + (one : list Z) + := eval (from_montgomery one) mod m = 1 mod m + /\ valid one. + + Definition encode_correct + (encode : Z -> list Z) + := forall x, + is_bounded_by0 prime_bound x = true + -> eval (from_montgomery (encode x)) mod m = x mod m + /\ valid (encode x). + + Definition nonzero_correct + (nonzero : list Z -> Z) + := forall x, + valid x + -> (nonzero x = 0) <-> (eval (from_montgomery x) mod m = 0). + + Definition to_bytes_correct + (to_bytes : list Z -> list Z) + := forall x, + valid x + -> to_bytes x = Partition.partition (weight 8 1) n_bytes (eval x mod m). + + Definition from_bytes_correct + (from_bytes : list Z -> list Z) + := forall x, + bytes_valid x + -> eval (from_bytes x) mod m = bytes_eval x mod m + /\ valid (from_bytes x). + + Definition selectznz_correct + (selectznz : Z -> list Z -> list Z -> list Z) + : Prop + := selectznz.selectznz_correct + (UniformWeight.uweight bitwidth) + n + saturated_bounds + selectznz. + + Section ring. + Context mul (Hmul : mul_correct mul) + add (Hadd : add_correct add) + sub (Hsub : sub_correct sub) + opp (Hopp : opp_correct opp) + encode (Hencode : encode_correct encode) + zero (Hzero : zero_correct zero) + one (Hone : one_correct one). + + Let m' := Z.to_pos m. + + Local Notation T := (list Z) (only parsing). + Local Notation encoded_ok ls + := (valid ls) (only parsing). + Local Notation encoded_okf := (fun ls => encoded_ok ls) (only parsing). + + Definition Fdecode (v : T) : F m' + := F.of_Z m' (eval (from_montgomery v)). + Definition T_eq (x y : T) + := Fdecode x = Fdecode y. + + Definition encodedT := sig encoded_okf. + + Definition ring_mul (x y : T) : T := mul x y. + Definition ring_add (x y : T) : T := add x y. + Definition ring_sub (x y : T) : T := sub x y. + Definition ring_opp (x : T) : T := opp x. + Definition ring_encode (x : F m') : T := encode (F.to_Z x). + + Definition GoodT : Prop + := @subsetoid_ring + (list Z) encoded_okf T_eq + zero one ring_opp ring_add ring_sub ring_mul + /\ @is_subsetoid_homomorphism + (F m') (fun _ => True) eq 1%F F.add F.mul + (list Z) encoded_okf T_eq one ring_add ring_mul ring_encode + /\ @is_subsetoid_homomorphism + (list Z) encoded_okf T_eq one ring_add ring_mul + (F m') (fun _ => True) eq 1%F F.add F.mul + Fdecode. + + Hint Rewrite ->@F.to_Z_add : push_FtoZ. + Hint Rewrite ->@F.to_Z_mul : push_FtoZ. + Hint Rewrite ->@F.to_Z_opp : push_FtoZ. + Hint Rewrite ->@F.to_Z_of_Z : push_FtoZ. + + Lemma Fm_bounded_alt (x : F m') + : is_bounded_by0 prime_bound (F.to_Z x) = true. + Proof using m_pos. + clear -m_pos. + destruct x as [x H]; cbn [F.to_Z proj1_sig]. + pose proof (Z.mod_pos_bound x (Z.pos m')). + subst m'; rewrite Z2Pos.id in * by lia. + cbv [prime_bound lower upper]. + rewrite Bool.andb_true_iff; split; Z.ltb_to_lt; lia. + Qed. + + Lemma Good : GoodT. + Proof. + split_and; simpl in *. + repeat match goal with + | [ H : context[andb _ true] |- _ ] => setoid_rewrite andb_true_r in H + end. + all: cbv [mul_correct add_correct sub_correct opp_correct encode_correct zero_correct one_correct] in *; split_and. + eapply subsetoid_ring_by_ring_isomorphism; + cbv [ring_opp ring_add ring_sub ring_mul ring_encode F.sub list_Z_bounded_by Fdecode m' F.one] in *; auto. + all: repeat first [ progress intros + | reflexivity + | progress autorewrite with push_FtoZ + | rewrite Z2Pos.id + | apply Fm_bounded_alt + | match goal with + | [ |- _ = _ :> F _ ] => apply F.eq_to_Z_iff + | [ |- _ mod _ = F.to_Z ?x ] + => etransitivity; [ | apply (F.mod_to_Z x) ] + | [ H : _ |- _ ] => apply H; clear H + | [ H : context[eval (?f _) mod ?m = _] |- context[eval (?f _) mod ?m] ] + => rewrite H + | [ H : context[eval (?f _ _) mod ?m = _] |- context[eval (?f _ _) mod ?m] ] + => rewrite H + end + | progress (push_Zmod; pull_Zmod); try (f_equal; lia) ]. + Qed. + End ring. + End __. +End WordByWordMontgomery. + +(* +Module BarrettReduction. + Section __. + (** TODO(jadep, from jgross): Remove any of these not needed to state the spec *) + Context (k M muLow : Z) + (n nout : nat) + (k_bound : 2 <= k) + (M_pos : 0 < M) + (muLow_eq : muLow + 2 ^ k = 2 ^ (2 * k) / M) + (muLow_bounds : 0 <= muLow < 2 ^ k) + (M_bound1 : 2 ^ (k - 1) < M < 2 ^ k) + (M_bound2 : 2 * (2 ^ (2 * k) mod M) <= 2 ^ (k + 1) - (muLow + 2 ^ k)) + (Hn_nz : n <> 0%nat) + (n_le_k : Z.of_nat n <= k) + (Hnout : nout = 2%nat). + + Definition barrett_red_correct + (barrett_red : Z -> Z -> Z) + := forall xLow xHigh, + 0 <= xLow < 2 ^ k + -> 0 <= xHigh < M + -> barrett_red xLow xHigh = (xLow + 2 ^ k * xHigh) mod M. + End __. +End BarrettReduction. + +Module MontgomeryReduction. + Section __. + Context (N R N' R' : Z). + + Definition montred_correct + Context (T R R' N + Lemma montred'_correct lo_hi T (HT_range: 0 <= T < R * N) + (Hlo: fst lo_hi = T mod R) (Hhi: snd lo_hi = T / R): montred' lo_hi = (T * R') mod N. + Proof. + erewrite montred'_eq by eauto. + apply Z.equiv_modulo_mod_small; auto using reduce_via_partial_correct. + replace 0 with (Z.min 0 (R-N)) by (apply Z.min_l; omega). + apply reduce_via_partial_in_range; omega. + Qed. + + End MontgomeryReduction. +*) |