diff options
| -rw-r--r-- | _CoqProject | 3 | ||||
| -rw-r--r-- | src/Experiments/DerivationsOptionRectLetInEncoding.v (renamed from src/Experiments/DerivationsOptionRectLetInFqPowEncoding.v) | 38 | ||||
| -rw-r--r-- | src/Rep.v | 13 | ||||
| -rw-r--r-- | src/Specific/GF25519.v | 98 |
4 files changed, 4 insertions, 148 deletions
diff --git a/_CoqProject b/_CoqProject index a3458ed1e..14179cb3d 100644 --- a/_CoqProject +++ b/_CoqProject @@ -6,7 +6,6 @@ src/Algebra.v src/BaseSystem.v src/BaseSystemProofs.v src/Nsatz.v -src/Rep.v src/Testbit.v src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -14,7 +13,7 @@ src/CompleteEdwardsCurve/Pre.v src/Encoding/EncodingTheorems.v src/Encoding/ModularWordEncodingPre.v src/Encoding/ModularWordEncodingTheorems.v -src/Experiments/DerivationsOptionRectLetInFqPowEncoding.v +src/Experiments/DerivationsOptionRectLetInEncoding.v src/Experiments/GenericFieldPow.v src/Experiments/SpecEd25519.v src/ModularArithmetic/ExtendedBaseVector.v diff --git a/src/Experiments/DerivationsOptionRectLetInFqPowEncoding.v b/src/Experiments/DerivationsOptionRectLetInEncoding.v index 146059ca4..9a6873bba 100644 --- a/src/Experiments/DerivationsOptionRectLetInFqPowEncoding.v +++ b/src/Experiments/DerivationsOptionRectLetInEncoding.v @@ -8,7 +8,7 @@ Require Import Crypto.Spec.CompleteEdwardsCurve. Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding. Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Import Crypto.Util.IterAssocOp Crypto.Util.WordUtil Crypto.Rep. +Require Import Crypto.Util.IterAssocOp Crypto.Util.WordUtil. Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence. Require Import Zdiv. Require Import Crypto.Util.Tuple. @@ -339,38 +339,4 @@ Qed. Lemma F_eqb_iff {q} : forall x y : F q, F_eqb x y = true <-> x = y. Proof. split; eauto using F_eqb_eq, F_eqb_complete. -Qed. - -Section FSRepOperations. - Context {q:Z} {prime_q:Znumtheory.prime q} {two_lt_q:(2 < q)%Z}. - Context {l:Z} {two_lt_l:(2 < l)%Z}. - Context `{rcS:RepConversions (F l) SRep} {rcSOK:RepConversionsOK rcS}. - Context `(rcF:RepConversions (F q) FRep) (rcFOK:RepConversionsOK rcF). - Context (FRepAdd FRepSub FRepMul:FRep->FRep->FRep) (FRepAdd_correct:RepBinOpOK rcF add FRepMul). - Context (FRepSub_correct:RepBinOpOK rcF sub FRepSub) (FRepMul_correct:RepBinOpOK rcF mul FRepMul). - Axiom SRep_testbit : SRep -> nat -> bool. - Axiom SRep_testbit_correct : forall (x0 : SRep) (i : nat), SRep_testbit x0 i = N.testbit_nat (FieldToN (unRep x0)) i. - - Definition FSRepPow width x n := iter_op FRepMul (toRep 1%F) SRep_testbit n x width. - Lemma FSRepPow_correct : forall width x n, (N.size_nat (FieldToN (unRep n)) <= width)%nat -> (unRep x ^ FieldToN (unRep n))%F = unRep (FSRepPow width x n). - Proof. (* this proof derives the required formula, which I copy-pasted above to be able to reference it without the length precondition *) - unfold FSRepPow; intros. - erewrite <-pow_nat_iter_op_correct by auto. - erewrite <-(fun x => iter_op_spec (scalar := SRep) mul F_mul_assoc _ F_mul_1_l _ _ SRep_testbit_correct n x width) by auto. - rewrite <-(rcFOK 1%F) at 1. - erewrite <-iter_op_proj; - [apply eq_refl - |eauto with typeclass_instances - |symmetry; eapply FRepMul_correct]. - Qed. - - Context (q_minus_2_lt_l:(q - 2 < l)%Z). - Definition FRepInv x : FRep := FSRepPow (COMPILETIME (N.size_nat (Z.to_N (q - 2)))) x (COMPILETIME (toRep (ZToField (q - 2)))). - Lemma FRepInv_correct : forall x, inv (unRep x)%F = unRep (FRepInv x). - unfold FRepInv, COMPILETIME; intros. - rewrite <-FSRepPow_correct; rewrite FieldToN_correct, rcSOK, FieldToZ_ZToField, Zmod_small by omega; trivial. - pose proof @Fq_inv_fermat_correct as Hf; unfold inv_fermat in Hf; rewrite Hf by - auto using prime_q, two_lt_q. - reflexivity. - Qed. -End FSRepOperations.
\ No newline at end of file +Qed.
\ No newline at end of file diff --git a/src/Rep.v b/src/Rep.v deleted file mode 100644 index b7e7f10c5..000000000 --- a/src/Rep.v +++ /dev/null @@ -1,13 +0,0 @@ -Class RepConversions (T:Type) (RT:Type) : Type := - { - toRep : T -> RT; - unRep : RT -> T - }. - -Definition RepConversionsOK {T RT} (RC:RepConversions T RT) := forall x, unRep (toRep x) = x. - -Definition RepFunOK {T RT} `(RC:RepConversions T RT) (f:T->T) (rf : RT -> RT) := - forall x, f (unRep x) = unRep (rf x). - -Definition RepBinOpOK {T RT} `(RC:RepConversions T RT) (op:T->T->T) (rop : RT -> RT -> RT) := - forall x y, op (unRep x) (unRep y) = unRep (rop x y). diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index ff7bff8e1..471c1d548 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -7,7 +7,6 @@ Require Import Coq.Lists.List Crypto.Util.ListUtil. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.BaseSystem. -Require Import Crypto.Rep. Import ListNotations. Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. Local Open Scope Z. @@ -128,99 +127,4 @@ Infix "&" := Z.land (at level 50). Eval cbv beta iota delta [proj1_sig GF25519Base25Point5_freeze_formula Let_In] in fun f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 => proj1_sig ( GF25519Base25Point5_freeze_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9). -*) - -Definition F25519Rep := (Z * Z * Z * Z * Z * Z * Z * Z * Z * Z)%type. - -Definition F25519toRep (x:F (2^255 - 19)) : F25519Rep := (0, 0, 0, 0, 0, 0, 0, 0, 0, FieldToZ x)%Z. -Definition F25519unRep (rx:F25519Rep) := - let '(x9, x8, x7, x6, x5, x4, x3, x2, x1, x0) := rx in - ModularBaseSystem.decode [x0;x1;x2;x3;x4;x5;x6;x7;x8;x9]. - -Global Instance F25519RepConversions : RepConversions (F (2^255 - 19)) F25519Rep := - { - toRep := F25519toRep; - unRep := F25519unRep - }. - -Lemma F25519RepConversionsOK : RepConversionsOK F25519RepConversions. -Proof. - unfold F25519RepConversions, RepConversionsOK, unRep, toRep, F25519toRep, F25519unRep; intros. - change (ModularBaseSystem.decode (ModularBaseSystem.encode x) = x). - eauto using ModularBaseSystemProofs.rep_decode, ModularBaseSystemProofs.encode_rep. -Qed. - -Definition F25519Rep_mul (f g:F25519Rep) : F25519Rep. - refine ( - let '(f9, f8, f7, f6, f5, f4, f3, f2, f1, f0) := f in - let '(g9, g8, g7, g6, g5, g4, g3, g2, g1, g0) := g in _). - (* FIXME: the r should not be present in generated code *) - pose (r := proj1_sig (GF25519Base25Point5_mul_reduce_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 - g0 g1 g2 g3 g4 g5 g6 g7 g8 g9)). - simpl in r. - unfold F25519Rep. - repeat let t' := (eval cbv beta delta [r] in r) in - lazymatch t' with Let_In ?arg ?f => - let x := fresh "x" in - refine (let x := arg in _); - let t'' := (eval cbv beta in (f x)) in - change (Let_In arg f) with t'' in r - end. - let t' := (eval cbv beta delta [r] in r) in - lazymatch t' with [?r0;?r1;?r2;?r3;?r4;?r5;?r6;?r7;?r8;?r9] => - clear r; - exact (r9, r8, r7, r6, r5, r4, r3, r2, r1, r0) - end. -(*Time*) Defined. - -Lemma F25519_mul_OK : RepBinOpOK F25519RepConversions ModularArithmetic.mul F25519Rep_mul. - cbv iota beta delta [RepBinOpOK F25519RepConversions F25519Rep_mul toRep unRep F25519toRep F25519unRep]. - destruct x as [[[[[[[[[x9 x8] x7] x6] x5] x4] x3] x2] x1] x0]. - destruct y as [[[[[[[[[y9 y8] y7] y6] y5] y4] y3] y2] y1] y0]. - let E := constr:(GF25519Base25Point5_mul_reduce_formula x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in - transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl; apply f_equal; reflexivity]]; - destruct E as [? r]; cbv [proj1_sig]. - cbv [rep ModularBaseSystem.rep PseudoMersenneBase modulus] in r; edestruct r; eauto. -Qed. - -Definition F25519Rep_add (f g:F25519Rep) : F25519Rep. - refine ( - let '(f9, f8, f7, f6, f5, f4, f3, f2, f1, f0) := f in - let '(g9, g8, g7, g6, g5, g4, g3, g2, g1, g0) := g in _). - let t' := (eval simpl in (proj1_sig (GF25519Base25Point5_add_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 - g0 g1 g2 g3 g4 g5 g6 g7 g8 g9))) in - lazymatch t' with [?r0;?r1;?r2;?r3;?r4;?r5;?r6;?r7;?r8;?r9] => - exact (r9, r8, r7, r6, r5, r4, r3, r2, r1, r0) - end. -Defined. - -Definition F25519Rep_sub (f g:F25519Rep) : F25519Rep. - refine ( - let '(f9, f8, f7, f6, f5, f4, f3, f2, f1, f0) := f in - let '(g9, g8, g7, g6, g5, g4, g3, g2, g1, g0) := g in _). - let t' := (eval simpl in (proj1_sig (GF25519Base25Point5_sub_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 - g0 g1 g2 g3 g4 g5 g6 g7 g8 g9))) in - lazymatch t' with [?r0;?r1;?r2;?r3;?r4;?r5;?r6;?r7;?r8;?r9] => - exact (r9, r8, r7, r6, r5, r4, r3, r2, r1, r0) - end. -Defined. - -Lemma F25519_add_OK : RepBinOpOK F25519RepConversions ModularArithmetic.add F25519Rep_add. - cbv iota beta delta [RepBinOpOK F25519RepConversions F25519Rep_add toRep unRep F25519toRep F25519unRep]. - destruct x as [[[[[[[[[x9 x8] x7] x6] x5] x4] x3] x2] x1] x0]. - destruct y as [[[[[[[[[y9 y8] y7] y6] y5] y4] y3] y2] y1] y0]. - let E := constr:(GF25519Base25Point5_add_formula x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in - transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl; apply f_equal; reflexivity]]; - destruct E as [? r]; cbv [proj1_sig]. - cbv [rep ModularBaseSystem.rep PseudoMersenneBase modulus] in r; edestruct r; eauto. -Qed. - -Lemma F25519_sub_OK : RepBinOpOK F25519RepConversions ModularArithmetic.sub F25519Rep_sub. - cbv iota beta delta [RepBinOpOK F25519RepConversions F25519Rep_sub toRep unRep F25519toRep F25519unRep]. - destruct x as [[[[[[[[[x9 x8] x7] x6] x5] x4] x3] x2] x1] x0]. - destruct y as [[[[[[[[[y9 y8] y7] y6] y5] y4] y3] y2] y1] y0]. - let E := constr:(GF25519Base25Point5_sub_formula x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in - transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl; apply f_equal; reflexivity]]; - destruct E as [? r]; cbv [proj1_sig]. - cbv [rep ModularBaseSystem.rep PseudoMersenneBase modulus] in r; edestruct r; eauto. -Qed. +*)
\ No newline at end of file |