From 7d3f54c975d24dc2f5fd8a0e31e004d74d7a3dd0 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 5 Aug 2016 19:30:44 -0700 Subject: Specify a type of bounded integers for mod arith Also use it to implement Montgomery reduction and Barrett reduction. --- _CoqProject | 3 + src/ModularArithmetic/BarrettReduction/ZBounded.v | 48 +++++++ src/ModularArithmetic/Montgomery/ZBounded.v | 43 ++++++ src/ModularArithmetic/ZBounded.v | 165 ++++++++++++++++++++++ 4 files changed, 259 insertions(+) create mode 100644 src/ModularArithmetic/BarrettReduction/ZBounded.v create mode 100644 src/ModularArithmetic/Montgomery/ZBounded.v create mode 100644 src/ModularArithmetic/ZBounded.v diff --git a/_CoqProject b/_CoqProject index 307a752fd..2840c3b91 100644 --- a/_CoqProject +++ b/_CoqProject @@ -50,10 +50,13 @@ src/ModularArithmetic/PrimeFieldTheorems.v src/ModularArithmetic/PseudoMersenneBaseParamProofs.v src/ModularArithmetic/PseudoMersenneBaseParams.v src/ModularArithmetic/Tutorial.v +src/ModularArithmetic/ZBounded.v src/ModularArithmetic/BarrettReduction/Z.v +src/ModularArithmetic/BarrettReduction/ZBounded.v src/ModularArithmetic/BarrettReduction/ZGeneralized.v src/ModularArithmetic/BarrettReduction/ZHandbook.v src/ModularArithmetic/Montgomery/Z.v +src/ModularArithmetic/Montgomery/ZBounded.v src/ModularArithmetic/Montgomery/ZProofs.v src/Spec/CompleteEdwardsCurve.v src/Spec/EdDSA.v diff --git a/src/ModularArithmetic/BarrettReduction/ZBounded.v b/src/ModularArithmetic/BarrettReduction/ZBounded.v new file mode 100644 index 000000000..bcebd6ea7 --- /dev/null +++ b/src/ModularArithmetic/BarrettReduction/ZBounded.v @@ -0,0 +1,48 @@ +(*** Barrett Reduction *) +(** This file implements Barrett Reduction on [ZLikeOps]. We follow + [BarretReduction/ZHandbook.v]. *) +Require Import Coq.ZArith.ZArith Coq.Lists.List Coq.Classes.Morphisms Coq.micromega.Psatz. +Require Import Crypto.ModularArithmetic.BarrettReduction.ZHandbook. +Require Import Crypto.ModularArithmetic.Pow2Base. +Require Import Crypto.ModularArithmetic.ExtendedBaseVector. +Require Import Crypto.ModularArithmetic.ZBounded. +Require Import Crypto.BaseSystem. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Notations. + +Local Open Scope small_zlike_scope. +Local Open Scope large_zlike_scope. +Local Open Scope Z_scope. + +Section barrett. + Context (m b k μ offset : Z) + (m_pos : 0 < m) + (base_pos : 0 < b) + (k_good : m < b^k) + (μ_good : μ = b^(2*k) / m) (* [/] is [Z.div], which is truncated *) + (offset_nonneg : 0 <= offset) + (k_big_enough : offset <= k) + (m_small : 3 * m <= b^(k+offset)) + (m_large : b^(k-offset) <= m + 1). + Context {ops : ZLikeOps (b^(k+offset)) (b^(k-offset)) m} {props : ZLikeProperties ops} + (μ' : SmallT) + (μ'_good : small_valid μ') + (μ'_eq : decode_small μ' = μ). + + Definition barrett_reduce : forall x : LargeT, + { barrett_reduce : SmallT + | medium_valid x + -> decode_small barrett_reduce = (decode_large x) mod m + /\ small_valid barrett_reduce }. + Proof. + intro x. evar (pr : SmallT); exists pr. intros x_valid. + assert (0 <= decode_large x < b^(k+offset) * b^(k-offset)) by auto using decode_medium_valid. + assert (0 <= decode_large x < b^(2 * k)) by (autorewrite with pull_Zpow zsimplify in *; omega). + assert ((decode_large x) mod b^(k-offset) < b^(k-offset)) by auto with zarith omega. + rewrite (barrett_reduction_small m b (decode_large x) k μ offset) by omega. + rewrite <- μ'_eq. + pull_zlike_decode. + subst pr; split; [ reflexivity | exact _ ]. + Defined. +End barrett. diff --git a/src/ModularArithmetic/Montgomery/ZBounded.v b/src/ModularArithmetic/Montgomery/ZBounded.v new file mode 100644 index 000000000..9295d5bc4 --- /dev/null +++ b/src/ModularArithmetic/Montgomery/ZBounded.v @@ -0,0 +1,43 @@ +(*** Montgomery Multiplication *) +(** This file implements Montgomery Form, Montgomery Reduction, and + Montgomery Multiplication on [ZLikeOps]. We follow [Montgomery/Z.v]. *) +Require Import Coq.ZArith.ZArith Coq.Lists.List Coq.Classes.Morphisms Coq.micromega.Psatz. +Require Import Crypto.ModularArithmetic.Montgomery.Z. +Require Import Crypto.ModularArithmetic.Montgomery.ZProofs. +Require Import Crypto.ModularArithmetic.Pow2Base. +Require Import Crypto.ModularArithmetic.ExtendedBaseVector. +Require Import Crypto.ModularArithmetic.ZBounded. +Require Import Crypto.BaseSystem. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Notations. + +Local Open Scope small_zlike_scope. +Local Open Scope large_zlike_scope. +Local Open Scope Z_scope. + +Section montgomery. + Context (small_bound modulus : Z) {ops : ZLikeOps small_bound small_bound modulus} {props : ZLikeProperties ops} + (modulus' : SmallT) + (modulus'_valid : small_valid modulus') + (modulus_nonzero : modulus <> 0). + + Definition partial_reduce : forall v : LargeT, + { partial_reduce : SmallT + | large_valid v + -> decode_small partial_reduce = Montgomery.Z.partial_reduce modulus small_bound (decode_small modulus') (decode_large v) + /\ small_valid partial_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). + 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 new file mode 100644 index 000000000..84c0f7645 --- /dev/null +++ b/src/ModularArithmetic/ZBounded.v @@ -0,0 +1,165 @@ +(*** Bounded ℤ-Like Types *) +(** This file specifies a ℤ-like type of bounded integers, with + operations for Montgomery Reduction and Barrett Reduction. *) +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Notations. + +Local Open Scope Z_scope. + +Class ZLikeOps (small_bound smaller_bound : Z) (modulus : Z) := + { + LargeT : Type; + SmallT : Type; + modulus_digits : SmallT; + decode_large : LargeT -> Z; + decode_small : SmallT -> Z; + Mod_SmallBound : LargeT -> SmallT; + DivBy_SmallBound : LargeT -> SmallT; + DivBy_SmallerBound : LargeT -> SmallT; + Mul : SmallT -> SmallT -> LargeT; + CarryAdd : LargeT -> LargeT -> bool * LargeT; + CarrySubSmall : SmallT -> SmallT -> bool * SmallT; + ConditionalSubtract : bool -> SmallT -> SmallT; + ConditionalSubtractModulus : SmallT -> SmallT + }. + +Delimit Scope small_zlike_scope with small_zlike. +Delimit Scope large_zlike_scope with large_zlike. +Local Open Scope small_zlike_scope. +Local Open Scope large_zlike_scope. +Local Open Scope Z_scope. +Bind Scope small_zlike_scope with SmallT. +Bind Scope large_zlike_scope with LargeT. +Arguments decode_large (_ _ _)%Z _ _%large_zlike. +Arguments decode_small (_ _ _)%Z _ _%small_zlike. +Arguments Mod_SmallBound (_ _ _)%Z _ _%large_zlike. +Arguments DivBy_SmallBound (_ _ _)%Z _ _%large_zlike. +Arguments DivBy_SmallerBound (_ _ _)%Z _ _%large_zlike. +Arguments Mul (_ _ _)%Z _ (_ _)%small_zlike. +Arguments CarryAdd (_ _ _)%Z _ (_ _)%large_zlike. +Arguments CarrySubSmall (_ _ _)%Z _ (_ _)%large_zlike. +Arguments ConditionalSubtract (_ _ _)%Z _ _%bool _%small_zlike. +Arguments ConditionalSubtractModulus (_ _ _)%Z _ _%small_zlike. + +Infix "*" := Mul : large_zlike_scope. +Notation "x + y" := (snd (CarryAdd x y)) : large_zlike_scope. + +Class ZLikeProperties {small_bound smaller_bound modulus : Z} (Zops : ZLikeOps small_bound smaller_bound modulus) := + { + large_valid : LargeT -> Prop; + medium_valid : LargeT -> Prop; + small_valid : SmallT -> Prop; + decode_large_valid : forall v, large_valid v -> 0 <= decode_large v < small_bound * small_bound; + decode_medium_valid : forall v, medium_valid v -> 0 <= decode_large v < small_bound * smaller_bound; + medium_to_large_valid : forall v, medium_valid v -> large_valid v; + decode_small_valid : forall v, small_valid v -> 0 <= decode_small v < small_bound; + modulus_digits_valid : small_valid modulus_digits; + modulus_digits_correct : decode_small modulus_digits = modulus; + Mod_SmallBound_valid : forall v, large_valid v -> small_valid (Mod_SmallBound v); + Mod_SmallBound_correct + : forall v, large_valid v -> decode_small (Mod_SmallBound v) = decode_large v mod small_bound; + DivBy_SmallBound_valid : forall v, large_valid v -> small_valid (DivBy_SmallBound v); + DivBy_SmallBound_correct + : forall v, large_valid v -> decode_small (DivBy_SmallBound v) = decode_large v / small_bound; + DivBy_SmallerBound_valid : forall v, medium_valid v -> small_valid (DivBy_SmallerBound v); + DivBy_SmallerBound_correct + : forall v, medium_valid v -> decode_small (DivBy_SmallerBound v) = decode_large v / smaller_bound; + Mul_valid : forall x y, small_valid x -> small_valid y -> large_valid (Mul x y); + Mul_correct + : forall x y, small_valid x -> small_valid y -> decode_large (Mul x y) = decode_small x * decode_small y; + CarryAdd_valid : forall x y, large_valid x -> large_valid y -> large_valid (snd (CarryAdd x y)); + CarryAdd_correct_fst + : forall x y, large_valid x -> large_valid y -> fst (CarryAdd x y) = (small_bound * small_bound <=? decode_large x + decode_large y); + CarryAdd_correct_snd + : forall x y, large_valid x -> large_valid y -> decode_large (snd (CarryAdd x y)) = (decode_large x + decode_large y) mod (small_bound * small_bound); + CarrySubSmall_valid : forall x y, small_valid x -> small_valid y -> small_valid (snd (CarrySubSmall x y)); + CarrySubSmall_correct_fst + : forall x y, small_valid x -> small_valid y -> fst (CarrySubSmall x y) = (decode_small x - decode_small y small_valid y -> decode_small (snd (CarrySubSmall x y)) = (decode_small x - decode_small y) mod small_bound; + ConditionalSubtract_valid : forall b x, small_valid x -> small_valid (ConditionalSubtract b x); + ConditionalSubtract_correct + : forall b x, small_valid x -> decode_small (ConditionalSubtract b x) + = if b then (decode_small x - decode_small modulus_digits) mod small_bound else decode_small x; + ConditionalSubtractModulus_valid : forall x, small_valid x -> small_valid (ConditionalSubtractModulus x); + ConditionalSubtractModulus_correct + : forall x, small_valid x -> decode_small (ConditionalSubtractModulus x) + = if (decode_small x large_valid y -> + decode_large (snd (CarryAdd x y)) + (small_bound * small_bound) * (if fst (CarryAdd x y) then 1 else 0) + = decode_large x + decode_large y. +Proof. + intros x y Hx Hy; rewrite CarryAdd_correct_fst, CarryAdd_correct_snd by assumption. + apply decode_large_valid in Hx. apply decode_large_valid in Hy. + rewrite (Z.add_comm (_ mod _)). + symmetry; etransitivity; [ eapply Z.div_mod | apply f_equal2; [ | reflexivity ] ]; + [ omega | ]. + generalize dependent (decode_large x); clear x; intro x. + generalize dependent (decode_large y); clear y; intro y. + intros. + assert (x + y < 2 * (small_bound * small_bound)) by omega. + break_match; Z.ltb_to_lt; + autorewrite with zsimplify; reflexivity. +Abort. + +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. + rewrite modulus_digits_correct in H. + omega. +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 @modulus_digits_correct using solve [ typeclasses eauto ] : pull_zlike_decode. + +Ltac get_modulus := + match goal with + | [ _ : ZLikeOps _ _ ?modulus |- _ ] => modulus + end. + +Ltac push_zlike_decode := + let modulus := get_modulus in + repeat first [ erewrite !Mod_SmallBound_correct by typeclasses eauto + | erewrite !DivBy_SmallBound_correct by typeclasses eauto + | erewrite !DivBy_SmallerBound_correct by typeclasses eauto + | erewrite !Mul_correct by typeclasses eauto + | erewrite !CarryAdd_correct_fst by typeclasses eauto + | erewrite !CarryAdd_correct_snd by typeclasses eauto + | erewrite !CarrySubSmall_correct_fst by typeclasses eauto + | erewrite !CarrySubSmall_correct_snd by typeclasses eauto + | erewrite !ConditionalSubtract_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 + repeat first [ match goal with + | [ |- context G[modulus] ] + => let G' := context G[decode_small modulus_digits] in + cut G'; [ rewrite !modulus_digits_correct by typeclasses eauto; exact (fun x => x) | ] + end + | erewrite <- !Mod_SmallBound_correct by typeclasses eauto + | erewrite <- !DivBy_SmallBound_correct by typeclasses eauto + | erewrite <- !DivBy_SmallerBound_correct by typeclasses eauto + | erewrite <- !Mul_correct by typeclasses eauto + | erewrite <- !CarryAdd_correct_fst by typeclasses eauto + | erewrite <- !CarryAdd_correct_snd by typeclasses eauto + | erewrite <- !ConditionalSubtract_correct by typeclasses eauto + | erewrite <- !CarrySubSmall_correct_fst by typeclasses eauto + | erewrite <- !CarrySubSmall_correct_snd by typeclasses eauto + | erewrite <- !ConditionalSubtractModulus_correct by typeclasses eauto + | erewrite <- !(@modulus_digits_correct _ modulus _ _) by typeclasses eauto ]. -- cgit v1.2.3 From 3da2a1ce9d25da66f2f317dea68179b96bc71849 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 9 Aug 2016 17:06:48 -0700 Subject: Remove unused code (still in vcs history, in case we want it later) --- src/ModularArithmetic/ZBounded.v | 19 ------------------- 1 file changed, 19 deletions(-) diff --git a/src/ModularArithmetic/ZBounded.v b/src/ModularArithmetic/ZBounded.v index 84c0f7645..def7dcb77 100644 --- a/src/ModularArithmetic/ZBounded.v +++ b/src/ModularArithmetic/ZBounded.v @@ -96,25 +96,6 @@ 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. -(** TODO: Remove me *) -Lemma CarryAdd_correct {small_bound smaller_bound modulus} {Zops : ZLikeOps small_bound smaller_bound modulus} {_ : ZLikeProperties Zops} - : forall x y, large_valid x -> large_valid y -> - decode_large (snd (CarryAdd x y)) + (small_bound * small_bound) * (if fst (CarryAdd x y) then 1 else 0) - = decode_large x + decode_large y. -Proof. - intros x y Hx Hy; rewrite CarryAdd_correct_fst, CarryAdd_correct_snd by assumption. - apply decode_large_valid in Hx. apply decode_large_valid in Hy. - rewrite (Z.add_comm (_ mod _)). - symmetry; etransitivity; [ eapply Z.div_mod | apply f_equal2; [ | reflexivity ] ]; - [ omega | ]. - generalize dependent (decode_large x); clear x; intro x. - generalize dependent (decode_large y); clear y; intro y. - intros. - assert (x + y < 2 * (small_bound * small_bound)) by omega. - break_match; Z.ltb_to_lt; - autorewrite with zsimplify; reflexivity. -Abort. - 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. -- cgit v1.2.3 From 3c888a6584b8872f179782a9a2b2d07f9b7076f1 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 10 Aug 2016 11:54:27 -0700 Subject: Work around bug #4165 (broken context) in 8.4 This is https://coq.inria.fr/bugs/show_bug.cgi?id=4165, context replacement is broken (in the presence of [let]). --- src/ModularArithmetic/BarrettReduction/ZBounded.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ModularArithmetic/BarrettReduction/ZBounded.v b/src/ModularArithmetic/BarrettReduction/ZBounded.v index bcebd6ea7..0c4142573 100644 --- a/src/ModularArithmetic/BarrettReduction/ZBounded.v +++ b/src/ModularArithmetic/BarrettReduction/ZBounded.v @@ -42,7 +42,7 @@ Section barrett. assert ((decode_large x) mod b^(k-offset) < b^(k-offset)) by auto with zarith omega. rewrite (barrett_reduction_small m b (decode_large x) k μ offset) by omega. rewrite <- μ'_eq. - pull_zlike_decode. + pull_zlike_decode; cbv zeta; pull_zlike_decode. (* Extra [cbv iota; pull_zlike_decode] to work around bug #4165 (https://coq.inria.fr/bugs/show_bug.cgi?id=4165) in 8.4 *) subst pr; split; [ reflexivity | exact _ ]. Defined. End barrett. -- cgit v1.2.3