fiat-crypto
fiat-crypto copied to clipboard
mit-plv
Investigate coqprime dependency
Since we do not generate primality proofs (because they are slow), where do we depend on coqprime anyway? I think we might be using Fermat's Little Theorem from it, but is there anything else?
$ git grep Coqprime
Makefile: $(MAKE) --no-print-directory -C $(COQPRIME_FOLDER) src/Coqprime/PrimalityTest/Zp.vo
src/Util/NumTheoryUtil.v:Require Coqprime.PrimalityTest.Euler Coqprime.PrimalityTest.Zp Coqprime.PrimalityTest.IGroup Coqprime.PrimalityTest.EGroup Coqprime.PrimalityTest.FGroup Coqprime.List.UList.
src/Util/NumTheoryUtil.v:(* TODO: move somewhere else for lemmas about Coqprime.PrimalityTest? *)
src/Util/NumTheoryUtil.v: List.In p (Coqprime.PrimalityTest.FGroup.s (Coqprime.PrimalityTest.Zp.ZPGroup n n_pos)) -> 1 <= p < n.
src/Util/NumTheoryUtil.v:unfold Coqprime.PrimalityTest.Zp.ZPGroup; simpl; intros Hin.
src/Util/NumTheoryUtil.v:pose proof (Coqprime.PrimalityTest.IGroup.isupport_incl Z (Coqprime.PrimalityTest.Zp.pmult n) (Coqprime.PrimalityTest.Zp.mkZp n) 1 Z.eq_dec) as H.
src/Util/NumTheoryUtil.v:apply Coqprime.PrimalityTest.Zp.in_mkZp in H; auto.
src/Util/NumTheoryUtil.v:apply Coqprime.PrimalityTest.IGroup.isupport_is_inv_true in Hin.
src/Util/NumTheoryUtil.v:rewrite Coqprime.PrimalityTest.Zp.rel_prime_is_inv in Hin by auto.
src/Util/NumTheoryUtil.v: (List.In y (Coqprime.PrimalityTest.FGroup.s (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p))
src/Util/NumTheoryUtil.v: /\ Coqprime.PrimalityTest.EGroup.e_order Z.eq_dec y (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p) = Coqprime.PrimalityTest.FGroup.g_order (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p))
src/Util/NumTheoryUtil.v: -> forall a, List.In a (Coqprime.PrimalityTest.FGroup.s (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p)) ->
src/Util/NumTheoryUtil.v: List.In a (Coqprime.PrimalityTest.EGroup.support Z.eq_dec y (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p)).
src/Util/NumTheoryUtil.v: pose proof (Coqprime.PrimalityTest.EGroup.support_incl_G Z Z.eq_dec (Coqprime.PrimalityTest.Zp.pmult p) y (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p) in_ZPGroup_y).
src/Util/NumTheoryUtil.v: eapply Coqprime.List.UList.ulist_eq_permutation; try apply Coqprime.PrimalityTest.EGroup.support_ulist; eauto.
src/Util/NumTheoryUtil.v: unfold Coqprime.PrimalityTest.EGroup.e_order, Coqprime.PrimalityTest.FGroup.g_order in y_order.
src/Util/NumTheoryUtil.v:Lemma mod_p_order : Coqprime.PrimalityTest.FGroup.g_order (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p) = p - 1.
src/Util/NumTheoryUtil.v: intros; rewrite <- Coqprime.PrimalityTest.Zp.phi_is_order.
src/Util/NumTheoryUtil.v: apply Coqprime.PrimalityTest.Euler.prime_phi_n_minus_1; auto.
src/Util/NumTheoryUtil.v: rewrite (Coqprime.PrimalityTest.Zp.Zpower_mod_is_gpow _ _ _ lt_1_p) by (auto || Z.prime_bound).
src/Util/NumTheoryUtil.v: apply Coqprime.PrimalityTest.EGroup.fermat_gen; try apply Z.eq_dec.
src/Util/NumTheoryUtil.v: apply Coqprime.PrimalityTest.Zp.in_mod_ZPGroup; auto.
src/Util/NumTheoryUtil.v: (exists y, List.In y (Coqprime.PrimalityTest.FGroup.s (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p))
src/Util/NumTheoryUtil.v: /\ Coqprime.PrimalityTest.EGroup.e_order Z.eq_dec y (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p) = Coqprime.PrimalityTest.FGroup.g_order (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p)
src/Util/NumTheoryUtil.v: destruct (Coqprime.PrimalityTest.Zp.Zp_cyclic p lt_1_p prime_p) as [y [y_in_ZPGroup y_order]].
src/Util/NumTheoryUtil.v: assert (List.In a (Coqprime.PrimalityTest.FGroup.s (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p))) as a_in_ZPGroup by (apply Coqprime.PrimalityTest.Zp.in_ZPGroup; omega || auto).
src/Util/NumTheoryUtil.v: destruct (Coqprime.PrimalityTest.EGroup.support_gpow Z Z.eq_dec (Coqprime.PrimalityTest.Zp.pmult p) y (Coqprime.PrimalityTest.Zp.ZPGroup p lt_1_p) y_in_ZPGroup a)
src/Util/NumTheoryUtil.v: unfold Coqprime.PrimalityTest.EGroup.e_order in y_order.
src/Util/NumTheoryUtil.v: rewrite <- (Coqprime.PrimalityTest.Zp.Zpower_mod_is_gpow y k p lt_1_p) in gpow_y_k by (omega || auto).
src/Util/NumTheoryUtil.v: rewrite <- Coqprime.PrimalityTest.Zp.phi_is_order in y_order.
src/Util/NumTheoryUtil.v: rewrite Coqprime.PrimalityTest.Euler.prime_phi_n_minus_1 in y_order by auto.
src/Util/NumTheoryUtil.v: ereplace (p-1); try eapply Coqprime.PrimalityTest.EGroup.e_order_divide_gpow; eauto with zarith.
src/Util/NumTheoryUtil.v: erewrite <- Coqprime.PrimalityTest.Zp.Zpower_mod_is_gpow; eauto.
$ git grep NumTheoryUtil
_CoqProject:src/Util/NumTheoryUtil.v
src/Arithmetic/ModularArithmeticPre.v:Require Import Crypto.Util.NumTheoryUtil.
src/Arithmetic/PrimeFieldTheorems.v:Require Import Crypto.Util.NumTheoryUtil.
src/Arithmetic/PrimeFieldTheorems.v:Require Import Crypto.Util.NumTheoryUtil.
$ git grep 'ModularArithmeticPre\|PrimeFieldTheorems'
_CoqProject:src/Arithmetic/ModularArithmeticPre.v
_CoqProject:src/Arithmetic/PrimeFieldTheorems.v
src/Arithmetic.v:Require Import Crypto.Arithmetic.PrimeFieldTheorems.
src/Arithmetic/ModularArithmeticTheorems.v:Require Import Crypto.Arithmetic.ModularArithmeticPre.
src/Arithmetic/ModularArithmeticTheorems.v: rewrite ModularArithmeticPre.N_pos_1plus at 1.
src/Arithmetic/ModularArithmeticTheorems.v: rewrite <-IHp, Pos.pred_N_succ, ModularArithmeticPre.N_pos_1plus, HS.
src/Arithmetic/PrimeFieldTheorems.v:Require Import Crypto.Arithmetic.ModularArithmeticPre.
src/Arithmetic/PrimeFieldTheorems.v: (* TODO: move to PrimeFieldTheorems *)
src/COperationSpecifications.v:Require Import Crypto.Arithmetic.PrimeFieldTheorems.
src/Primitives/EdDSARepChange.v:Require Import Crypto.Spec.ModularArithmetic Crypto.Arithmetic.PrimeFieldTheorems.
src/Spec/Ed25519.v:Require Crypto.Arithmetic.PrimeFieldTheorems. (* to know that Z mod p is a field *)
src/Spec/Ed25519.v: Proof using Type. pose (@PrimeFieldTheorems.F.Decidable_square q _ ltac:(Crypto.Util.Decidable.vm_decide) a); Crypto.Util.Decidable.vm_decide. Qed.
src/Spec/Ed25519.v: Proof using Type. pose (@PrimeFieldTheorems.F.Decidable_square q _ ltac:(Crypto.Util.Decidable.vm_decide) d); Crypto.Util.Decidable.vm_decide. Qed.
src/Spec/ModularArithmetic.v:Require Crypto.Arithmetic.ModularArithmeticPre.
src/Spec/ModularArithmetic.v: Local Obligation Tactic := cbv beta; auto using ModularArithmeticPre.Z_mod_mod.
src/Spec/ModularArithmetic.v: } := ModularArithmeticPre.inv_impl.
src/Spec/ModularArithmetic.v: } := ModularArithmeticPre.pow_impl.
Investigated a little further on this; we do indeed use it to prove Fermat's Little Theorem, which we then use to prove the implementation of inverses. Seems like maybe we could prove Fermat's little theorem another way, but it doesn't seem trivial, and until we do we do rely on Coqprime (unless we're not using inverses anywhere, but I think we are).
I posted a proof (with minor admits) of Fermat's little theorem at https://github.com/mit-plv/fiat-crypto/commit/b5f28537647784d02d97b0fc29ece766dc9a5e67, so shedding coqprime is now just some engineering effort away.
On further investigation, we unfortunately are also using an Euler's criterion proof that depends on Coqprime (we use it in square roots). Unclear to me how we would eliminate this one -- the main thing I think we'd need is the notion of primitive roots.