From 0803746ae4cc556e06e3ba5fadb98bbbcbf638ab Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 24 Dec 2018 15:35:21 -0500 Subject: from_montgomery{_ => }mod, for consistency with other naming --- src/Experiments/NewPipeline/Arithmetic.v | 56 ++++++++++++++++---------------- src/Experiments/NewPipeline/Toplevel1.v | 46 +++++++++++++------------- 2 files changed, 51 insertions(+), 51 deletions(-) diff --git a/src/Experiments/NewPipeline/Arithmetic.v b/src/Experiments/NewPipeline/Arithmetic.v index ad4c4ea75..9e452b5b2 100644 --- a/src/Experiments/NewPipeline/Arithmetic.v +++ b/src/Experiments/NewPipeline/Arithmetic.v @@ -4080,36 +4080,36 @@ Module WordByWordMontgomery. t_fin. Qed. - Definition from_montgomery_mod (v : list Z) : list Z + Definition from_montgomerymod (v : list Z) : list Z := mulmod v onemod. - Lemma from_montgomery_mod_correct (v : list Z) - : valid v -> eval (from_montgomery_mod v) mod m = (eval v * r'^n) mod m - /\ valid (from_montgomery_mod v). + Lemma from_montgomerymod_correct (v : list Z) + : valid v -> eval (from_montgomerymod v) mod m = (eval v * r'^n) mod m + /\ valid (from_montgomerymod v). Proof using r'_correct n_nz m_small m_big m'_correct bitwidth_big. clear -r'_correct n_nz m_small m_big m'_correct bitwidth_big. - intro Hv; cbv [from_montgomery_mod valid] in *; destruct_head'_and. + intro Hv; cbv [from_montgomerymod valid] in *; destruct_head'_and. replace (eval v * r'^n) with (eval v * eval onemod * r'^n) by (rewrite (proj1 onemod_correct); lia). repeat apply conj; apply mulmod_correct0; auto; try apply onemod_correct; rewrite (proj1 onemod_correct); omega. Qed. - Lemma eval_from_montgomery_mod (v : list Z) : valid v -> eval (from_montgomery_mod v) mod m = (eval v * r'^n) mod m. + Lemma eval_from_montgomerymod (v : list Z) : valid v -> eval (from_montgomerymod v) mod m = (eval v * r'^n) mod m. Proof using r'_correct n_nz m_small m_big m'_correct bitwidth_big. - intros; apply from_montgomery_mod_correct; assumption. + intros; apply from_montgomerymod_correct; assumption. Qed. - Lemma valid_from_montgomery_mod (v : list Z) - : valid v -> valid (from_montgomery_mod v). + Lemma valid_from_montgomerymod (v : list Z) + : valid v -> valid (from_montgomerymod v). Proof using r'_correct n_nz m_small m_big m'_correct bitwidth_big. - intros; apply from_montgomery_mod_correct; assumption. + intros; apply from_montgomerymod_correct; assumption. Qed. Lemma mulmod_correct - : (forall a (_ : valid a) b (_ : valid b), eval (from_montgomery_mod (mulmod a b)) mod m - = (eval (from_montgomery_mod a) * eval (from_montgomery_mod b)) mod m) + : (forall a (_ : valid a) b (_ : valid b), eval (from_montgomerymod (mulmod a b)) mod m + = (eval (from_montgomerymod a) * eval (from_montgomerymod b)) mod m) /\ (forall a (_ : valid a) b (_ : valid b), valid (mulmod a b)). Proof using r'_correct r' n_nz m_small m_big m'_correct bitwidth_big. repeat apply conj; intros; - push_Zmod; rewrite ?eval_from_montgomery_mod; pull_Zmod; repeat apply conj; + push_Zmod; rewrite ?eval_from_montgomerymod; pull_Zmod; repeat apply conj; try apply mulmod_correct0; cbv [valid] in *; destruct_head'_and; auto; []. rewrite !Z.mul_assoc. apply Z.mul_mod_Proper; [ | reflexivity ]. @@ -4117,8 +4117,8 @@ Module WordByWordMontgomery. Qed. Lemma squaremod_correct - : (forall a (_ : valid a), eval (from_montgomery_mod (squaremod a)) mod m - = (eval (from_montgomery_mod a) * eval (from_montgomery_mod a)) mod m) + : (forall a (_ : valid a), eval (from_montgomerymod (squaremod a)) mod m + = (eval (from_montgomerymod a) * eval (from_montgomerymod a)) mod m) /\ (forall a (_ : valid a), valid (squaremod a)). Proof using r'_correct n_nz m_small m_big m'_correct bitwidth_big. split; intros; cbv [squaremod]; apply mulmod_correct; assumption. @@ -4136,12 +4136,12 @@ Module WordByWordMontgomery. rewrite ?(Z.mod_small v) by (subst r; Z.div_mod_to_quot_rem; lia); try apply Z.mod_pos_bound; subst r; try lia; try reflexivity. Lemma encodemod_correct - : (forall v, 0 <= v < m -> eval (from_montgomery_mod (encodemod v)) mod m = v mod m) + : (forall v, 0 <= v < m -> eval (from_montgomerymod (encodemod v)) mod m = v mod m) /\ (forall v, 0 <= v < m -> valid (encodemod v)). Proof using r'_correct n_nz m_small m_big m'_correct bitwidth_big. split; intros v ?; cbv [encodemod R2mod]; [ rewrite (proj1 mulmod_correct) | apply mulmod_correct ]; [ | now t_valid v.. ]. - push_Zmod; rewrite !eval_from_montgomery_mod; [ | now t_valid v.. ]. + push_Zmod; rewrite !eval_from_montgomerymod; [ | now t_valid v.. ]. cbv [eval]; autorewrite with push_eval; auto. rewrite ?UniformWeight.uweight_eq_alt by omega. rewrite ?(Z.mod_small v) by (subst r; Z.div_mod_to_quot_rem; lia). @@ -4155,12 +4155,12 @@ Module WordByWordMontgomery. Qed. Lemma addmod_correct - : (forall a (_ : valid a) b (_ : valid b), eval (from_montgomery_mod (addmod a b)) mod m - = (eval (from_montgomery_mod a) + eval (from_montgomery_mod b)) mod m) + : (forall a (_ : valid a) b (_ : valid b), eval (from_montgomerymod (addmod a b)) mod m + = (eval (from_montgomerymod a) + eval (from_montgomerymod b)) mod m) /\ (forall a (_ : valid a) b (_ : valid b), valid (addmod a b)). Proof using r'_correct n_nz m_small m_big m'_correct bitwidth_big. repeat apply conj; intros; - push_Zmod; rewrite ?eval_from_montgomery_mod; pull_Zmod; repeat apply conj; + push_Zmod; rewrite ?eval_from_montgomerymod; pull_Zmod; repeat apply conj; cbv [valid addmod] in *; destruct_head'_and; auto; try rewrite m_enc_correct_montgomery; try (eapply small_add || eapply add_bound); @@ -4171,12 +4171,12 @@ Module WordByWordMontgomery. Qed. Lemma submod_correct - : (forall a (_ : valid a) b (_ : valid b), eval (from_montgomery_mod (submod a b)) mod m - = (eval (from_montgomery_mod a) - eval (from_montgomery_mod b)) mod m) + : (forall a (_ : valid a) b (_ : valid b), eval (from_montgomerymod (submod a b)) mod m + = (eval (from_montgomerymod a) - eval (from_montgomerymod b)) mod m) /\ (forall a (_ : valid a) b (_ : valid b), valid (submod a b)). Proof using r'_correct n_nz m_small m_big m'_correct bitwidth_big. repeat apply conj; intros; - push_Zmod; rewrite ?eval_from_montgomery_mod; pull_Zmod; repeat apply conj; + push_Zmod; rewrite ?eval_from_montgomerymod; pull_Zmod; repeat apply conj; cbv [valid submod] in *; destruct_head'_and; auto; try rewrite m_enc_correct_montgomery; try (eapply small_sub || eapply sub_bound); @@ -4187,12 +4187,12 @@ Module WordByWordMontgomery. Qed. Lemma oppmod_correct - : (forall a (_ : valid a), eval (from_montgomery_mod (oppmod a)) mod m - = (-eval (from_montgomery_mod a)) mod m) + : (forall a (_ : valid a), eval (from_montgomerymod (oppmod a)) mod m + = (-eval (from_montgomerymod a)) mod m) /\ (forall a (_ : valid a), valid (oppmod a)). Proof using r'_correct n_nz m_small m_big m'_correct bitwidth_big. repeat apply conj; intros; - push_Zmod; rewrite ?eval_from_montgomery_mod; pull_Zmod; repeat apply conj; + push_Zmod; rewrite ?eval_from_montgomerymod; pull_Zmod; repeat apply conj; cbv [valid oppmod] in *; destruct_head'_and; auto; try rewrite m_enc_correct_montgomery; try (eapply small_opp || eapply opp_bound); @@ -4203,9 +4203,9 @@ Module WordByWordMontgomery. Qed. Lemma nonzeromod_correct - : (forall a (_ : valid a), (nonzeromod a = 0) <-> ((eval (from_montgomery_mod a)) mod m = 0)). + : (forall a (_ : valid a), (nonzeromod a = 0) <-> ((eval (from_montgomerymod a)) mod m = 0)). Proof using r'_correct n_nz m_small m_big m'_correct bitwidth_big. - intros a Ha; rewrite eval_from_montgomery_mod by assumption. + intros a Ha; rewrite eval_from_montgomerymod by assumption. cbv [nonzeromod valid] in *; destruct_head'_and. rewrite eval_nonzero; try eassumption; [ | subst r; apply conj; try eassumption; omega.. ]. split; intro H'; [ rewrite H'; autorewrite with zsimplify_const; reflexivity | ]. diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index b1eee614e..0dae1e863 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -313,19 +313,19 @@ Module MontgomeryStyleRing. Context (m_eq : Z.pos m = s - Associational.eval c) (sc_pos : 0 < s - Associational.eval c) (valid : list Z -> Prop) - (from_montgomery_mod : list Z -> list Z) - (Hfrom_montgomery_mod - : forall v, valid v -> valid (from_montgomery_mod v)) + (from_montgomerymod : list Z -> list Z) + (Hfrom_montgomerymod + : forall v, valid v -> valid (from_montgomerymod v)) (Interp_rfrom_montgomeryv : list Z -> list Z) (HInterp_rfrom_montgomeryv : forall arg1 arg2, is_eq1 arg1 arg2 -> is_bounded_by1 bounds arg1 = true -> is_bounded_by bounds (Interp_rfrom_montgomeryv (fst arg1)) = true - /\ Interp_rfrom_montgomeryv (fst arg1) = from_montgomery_mod (fst arg2)) + /\ Interp_rfrom_montgomeryv (fst arg1) = from_montgomerymod (fst arg2)) (mulmod : list Z -> list Z -> list Z) (Hmulmod - : (forall a (_ : valid a) b (_ : valid b), eval (from_montgomery_mod (mulmod a b)) mod (s - Associational.eval c) - = (eval (from_montgomery_mod a) * eval (from_montgomery_mod b)) mod (s - Associational.eval c)) + : (forall a (_ : valid a) b (_ : valid b), eval (from_montgomerymod (mulmod a b)) mod (s - Associational.eval c) + = (eval (from_montgomerymod a) * eval (from_montgomerymod b)) mod (s - Associational.eval c)) /\ (forall a (_ : valid a) b (_ : valid b), valid (mulmod a b))) (Interp_rmulv : list Z -> list Z -> list Z) (HInterp_rmulv : forall arg1 arg2, @@ -335,8 +335,8 @@ Module MontgomeryStyleRing. /\ Interp_rmulv (fst arg1) (fst (snd arg1)) = mulmod (fst arg2) (fst (snd arg2))) (addmod : list Z -> list Z -> list Z) (Haddmod - : (forall a (_ : valid a) b (_ : valid b), eval (from_montgomery_mod (addmod a b)) mod (s - Associational.eval c) - = (eval (from_montgomery_mod a) + eval (from_montgomery_mod b)) mod (s - Associational.eval c)) + : (forall a (_ : valid a) b (_ : valid b), eval (from_montgomerymod (addmod a b)) mod (s - Associational.eval c) + = (eval (from_montgomerymod a) + eval (from_montgomerymod b)) mod (s - Associational.eval c)) /\ (forall a (_ : valid a) b (_ : valid b), valid (addmod a b))) (Interp_raddv : list Z -> list Z -> list Z) (HInterp_raddv : forall arg1 arg2, @@ -346,8 +346,8 @@ Module MontgomeryStyleRing. /\ Interp_raddv (fst arg1) (fst (snd arg1)) = addmod (fst arg2) (fst (snd arg2))) (submod : list Z -> list Z -> list Z) (Hsubmod - : (forall a (_ : valid a) b (_ : valid b), eval (from_montgomery_mod (submod a b)) mod (s - Associational.eval c) - = (eval (from_montgomery_mod a) - eval (from_montgomery_mod b)) mod (s - Associational.eval c)) + : (forall a (_ : valid a) b (_ : valid b), eval (from_montgomerymod (submod a b)) mod (s - Associational.eval c) + = (eval (from_montgomerymod a) - eval (from_montgomerymod b)) mod (s - Associational.eval c)) /\ (forall a (_ : valid a) b (_ : valid b), valid (submod a b))) (Interp_rsubv : list Z -> list Z -> list Z) (HInterp_rsubv : forall arg1 arg2, @@ -357,8 +357,8 @@ Module MontgomeryStyleRing. /\ Interp_rsubv (fst arg1) (fst (snd arg1)) = submod (fst arg2) (fst (snd arg2))) (oppmod : list Z -> list Z) (Hoppmod - : (forall a (_ : valid a), eval (from_montgomery_mod (oppmod a)) mod (s - Associational.eval c) - = (-eval (from_montgomery_mod a)) mod (s - Associational.eval c)) + : (forall a (_ : valid a), eval (from_montgomerymod (oppmod a)) mod (s - Associational.eval c) + = (-eval (from_montgomerymod a)) mod (s - Associational.eval c)) /\ (forall a (_ : valid a), valid (oppmod a))) (Interp_roppv : list Z -> list Z) (HInterp_roppv : forall arg1 arg2, @@ -368,7 +368,7 @@ Module MontgomeryStyleRing. /\ Interp_roppv (fst arg1) = oppmod (fst arg2)) (zeromod : list Z) (Hzeromod - : (eval (from_montgomery_mod zeromod)) mod (s - Associational.eval c) + : (eval (from_montgomerymod zeromod)) mod (s - Associational.eval c) = 0 mod (s - Associational.eval c) /\ valid zeromod) (Interp_rzerov : list Z) @@ -376,7 +376,7 @@ Module MontgomeryStyleRing. /\ Interp_rzerov = zeromod) (onemod : list Z) (Honemod - : (eval (from_montgomery_mod onemod)) mod (s - Associational.eval c) + : (eval (from_montgomerymod onemod)) mod (s - Associational.eval c) = 1 mod (s - Associational.eval c) /\ valid onemod) (Interp_ronev : list Z) @@ -384,7 +384,7 @@ Module MontgomeryStyleRing. /\ Interp_ronev = onemod) (encodemod : Z -> list Z) (Hencodemod - : (forall v, 0 <= v < s - Associational.eval c -> eval (from_montgomery_mod (encodemod v)) mod (s - Associational.eval c) = v mod (s - Associational.eval c)) + : (forall v, 0 <= v < s - Associational.eval c -> eval (from_montgomerymod (encodemod v)) mod (s - Associational.eval c) = v mod (s - Associational.eval c)) /\ (forall v, 0 <= v < s - Associational.eval c -> valid (encodemod v))) (Interp_rencodev : Z -> list Z) (HInterp_rencodev : forall arg1 arg2, @@ -2426,9 +2426,9 @@ Module WordByWordMontgomery. (m : Z) (m' : Z) (f : list Z), - Interp (t:=reify_type_of from_montgomery_mod) + Interp (t:=reify_type_of from_montgomerymod) from_montgomery_gen bitwidth n m m' f - = from_montgomery_mod bitwidth n m m' f) + = from_montgomerymod bitwidth n m m' f) /\ Wf from_montgomery_gen) As from_montgomery_gen_correct. Proof. @@ -2436,14 +2436,14 @@ Module WordByWordMontgomery. (* we would do something faster, but it breaks extraction COQBUG(https://github.com/coq/coq/issues/7954) *) (* split. - { intros; etransitivity; [ | cbv [from_montgomery_mod]; apply mul_gen_correct ]. + { intros; etransitivity; [ | cbv [from_montgomerymod]; apply mul_gen_correct ]. subst from_montgomery_gen. instantiate (1:=ltac:(let r := Reify (fun F (bitwidth:Z) (n:nat) (m m' : Z) (f : list Z) => (F bitwidth n m m' f (onemod bitwidth n)):list Z) in refine (r @ mul_gen)%Expr)). reflexivity. } { prove_Wf (). } *) Qed. - Hint Extern 1 (_ = from_montgomery_mod _ _ _ _ _) => simple apply (proj1 from_montgomery_gen_correct) : reify_gen_cache. + Hint Extern 1 (_ = from_montgomerymod _ _ _ _ _) => simple apply (proj1 from_montgomery_gen_correct) : reify_gen_cache. Hint Immediate (proj2 from_montgomery_gen_correct) : wf_gen_cache. Definition zeromod bitwidth n m m' := encodemod bitwidth n m m' 0. @@ -2737,7 +2737,7 @@ Module WordByWordMontgomery. := BoundsPipeline_correct (Some bounds, tt) (Some bounds) - (from_montgomery_mod machine_wordsize n m m'). + (from_montgomerymod machine_wordsize n m m'). Definition srnonzero prefix := BoundsPipelineToStrings @@ -2957,7 +2957,7 @@ Module WordByWordMontgomery. = type.app_curried (t:=from_bytesT) (from_bytesmod machine_wordsize 1 n) f)) /\ (Positional.eval (weight machine_wordsize 1) n (type.app_curried (t:=from_bytesT) (from_bytesmod machine_wordsize 1 n) f)) = (Positional.eval (weight 8 1) n_bytes (fst f)))) /\ (forall f - (Hf : type.andb_bool_for_each_lhs_of_arrow (t:=(base.type.list base.type.Z -> base.type.Z)%etype) (@ZRange.type.option.is_bounded_by) (Some bounds, tt) f = true) (Hfvalid : valid machine_wordsize n m (fst f)), (Interp rnonzerov (fst f) = 0) <-> ((@eval machine_wordsize n (from_montgomery_mod machine_wordsize n m m' (fst f))) mod m = 0)). + (Hf : type.andb_bool_for_each_lhs_of_arrow (t:=(base.type.list base.type.Z -> base.type.Z)%etype) (@ZRange.type.option.is_bounded_by) (Some bounds, tt) f = true) (Hfvalid : valid machine_wordsize n m (fst f)), (Interp rnonzerov (fst f) = 0) <-> ((@eval machine_wordsize n (from_montgomerymod machine_wordsize n m m' (fst f))) mod m = 0)). (** XXX TODO: MOVE ME *) Lemma is_bounded_by_repeat_In_iff {rg n'} {ls : list Z} @@ -2992,7 +2992,7 @@ Module WordByWordMontgomery. Qed. (** XXX TODO MOVE ME *) - Local Opaque valid addmod submod oppmod encodemod mulmod from_montgomery_mod nonzeromod. + Local Opaque valid addmod submod oppmod encodemod mulmod from_montgomerymod nonzeromod. Theorem Good : GoodT. Proof. pose proof use_curve_good; destruct_head'_and; destruct_head_hnf' ex. @@ -3013,7 +3013,7 @@ Module WordByWordMontgomery. | eapply submod_correct | eapply oppmod_correct | eapply encodemod_correct - | eapply from_montgomery_mod_correct + | eapply from_montgomerymod_correct | eapply nonzeromod_correct | intros; apply conj | omega ]. } -- cgit v1.2.3