diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/ModularArithmetic/Montgomery/ZBounded.v | 20 | ||||
-rw-r--r-- | src/ModularArithmetic/ZBounded.v | 14 |
2 files changed, 33 insertions, 1 deletions
diff --git a/src/ModularArithmetic/Montgomery/ZBounded.v b/src/ModularArithmetic/Montgomery/ZBounded.v index 9295d5bc4..9d54b167a 100644 --- a/src/ModularArithmetic/Montgomery/ZBounded.v +++ b/src/ModularArithmetic/Montgomery/ZBounded.v @@ -40,4 +40,24 @@ Section montgomery. pull_zlike_decode. subst pr; split; [ reflexivity | exact _ ]. Defined. + + Definition reduce_via_partial : forall v : LargeT, + { reduce : SmallT + | large_valid v + -> decode_small reduce = Montgomery.Z.reduce_via_partial modulus small_bound (decode_small modulus') (decode_large v) + /\ small_valid reduce }. + Proof. + intro T. evar (pr : SmallT); exists pr. intros T_valid. + assert (0 <= decode_large T < small_bound * small_bound) by auto using decode_large_valid. + assert (0 <= decode_small (Mod_SmallBound T) < small_bound) by auto using decode_small_valid, Mod_SmallBound_valid. + assert (0 <= decode_small modulus' < small_bound) by auto using decode_small_valid. + assert (0 <= decode_small modulus_digits < small_bound) by auto using decode_small_valid, modulus_digits_valid. + assert (0 <= modulus) by apply (modulus_nonneg _). + assert (modulus < small_bound) by (rewrite <- modulus_digits_correct; omega). + unfold reduce_via_partial. + rewrite <- partial_reduce_alt_eq by omega. + cbv [Montgomery.Z.partial_reduce Montgomery.Z.partial_reduce_alt Montgomery.Z.prereduce]. + pull_zlike_decode. + subst pr; split; [ reflexivity | exact _ ]. + Defined. End montgomery. diff --git a/src/ModularArithmetic/ZBounded.v b/src/ModularArithmetic/ZBounded.v index def7dcb77..cd4444dcf 100644 --- a/src/ModularArithmetic/ZBounded.v +++ b/src/ModularArithmetic/ZBounded.v @@ -96,6 +96,16 @@ Existing Class medium_valid. Existing Class small_valid. Existing Instances Mod_SmallBound_valid DivBy_SmallerBound_valid DivBy_SmallBound_valid Mul_valid CarryAdd_valid CarrySubSmall_valid ConditionalSubtract_valid ConditionalSubtractModulus_valid modulus_digits_valid medium_to_large_valid. +Lemma ConditionalSubtractModulus_correct' + {small_bound smaller_bound modulus : Z} {Zops : ZLikeOps small_bound smaller_bound modulus} + {Zprops : ZLikeProperties Zops} + : forall x, small_valid x -> decode_small (ConditionalSubtractModulus x) + = if (decode_small modulus_digits <=? decode_small x) then decode_small x - decode_small modulus_digits else decode_small x. +Proof. + intros; rewrite ConditionalSubtractModulus_correct by assumption. + break_match; Z.ltb_to_lt; omega. +Qed. + Lemma modulus_nonneg {small_bound smaller_bound modulus} (Zops : ZLikeOps small_bound smaller_bound modulus) {_ : ZLikeProperties Zops} : 0 <= modulus. Proof. pose proof (decode_small_valid _ modulus_digits_valid) as H. @@ -105,7 +115,7 @@ Qed. Create HintDb push_zlike_decode discriminated. Create HintDb pull_zlike_decode discriminated. -Hint Rewrite @Mod_SmallBound_correct @DivBy_SmallBound_correct @DivBy_SmallerBound_correct @Mul_correct @CarryAdd_correct_fst @CarryAdd_correct_snd @CarrySubSmall_correct_fst @CarrySubSmall_correct_snd @ConditionalSubtract_correct @ConditionalSubtractModulus_correct @modulus_digits_correct using solve [ typeclasses eauto ] : push_zlike_decode. +Hint Rewrite @Mod_SmallBound_correct @DivBy_SmallBound_correct @DivBy_SmallerBound_correct @Mul_correct @CarryAdd_correct_fst @CarryAdd_correct_snd @CarrySubSmall_correct_fst @CarrySubSmall_correct_snd @ConditionalSubtract_correct @ConditionalSubtractModulus_correct @ConditionalSubtractModulus_correct' @modulus_digits_correct using solve [ typeclasses eauto ] : push_zlike_decode. Hint Rewrite <- @Mod_SmallBound_correct @DivBy_SmallBound_correct @DivBy_SmallerBound_correct @Mul_correct @CarryAdd_correct_fst @CarryAdd_correct_snd @CarrySubSmall_correct_fst @CarrySubSmall_correct_snd @ConditionalSubtract_correct @ConditionalSubtractModulus_correct @modulus_digits_correct using solve [ typeclasses eauto ] : pull_zlike_decode. Ltac get_modulus := @@ -125,6 +135,7 @@ Ltac push_zlike_decode := | erewrite !CarrySubSmall_correct_snd by typeclasses eauto | erewrite !ConditionalSubtract_correct by typeclasses eauto | erewrite !ConditionalSubtractModulus_correct by typeclasses eauto + | erewrite !ConditionalSubtractModulus_correct' by typeclasses eauto | erewrite !(@modulus_digits_correct _ modulus _ _) by typeclasses eauto ]. Ltac pull_zlike_decode := let modulus := get_modulus in @@ -143,4 +154,5 @@ Ltac pull_zlike_decode := | erewrite <- !CarrySubSmall_correct_fst by typeclasses eauto | erewrite <- !CarrySubSmall_correct_snd by typeclasses eauto | erewrite <- !ConditionalSubtractModulus_correct by typeclasses eauto + | erewrite <- !ConditionalSubtractModulus_correct' by typeclasses eauto | erewrite <- !(@modulus_digits_correct _ modulus _ _) by typeclasses eauto ]. |