From a9086dc1863e4ee193c7f591a878b0cfeb601712 Mon Sep 17 00:00:00 2001 From: jadep Date: Tue, 12 Jul 2016 18:06:28 -0400 Subject: re-cleaned operations in Specific and updated GF25519 to match GF1305 --- src/Specific/GF1305.v | 114 +++++++++++++++++++------------------------------ src/Specific/GF25519.v | 79 ++++++++++++++++++++++++++++++---- 2 files changed, 115 insertions(+), 78 deletions(-) (limited to 'src/Specific') diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v index 5fefcae24..2bc42b68e 100644 --- a/src/Specific/GF1305.v +++ b/src/Specific/GF1305.v @@ -53,104 +53,78 @@ Definition fe1305 : Type := Eval cbv in fe. Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Let_In phi. - - -Definition add_formula_sig (f0 f1 f2 f3 f4 g0 g1 g2 g3 g4: Z) : - { fg | fg = ModularBaseSystemInterface.add (f0,f1,f2,f3,f4) (g0,g1,g2,g3,g4) }. +Definition add_sig (f g : fe1305) : + { fg : fe1305 | fg = ModularBaseSystemInterface.add f g}. Proof. + cbv [fe1305] in *. + repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. eexists. cbv. reflexivity. Defined. -Definition add_formula_correct := Eval cbv [proj2_sig] in -(fun f0 f1 f2 f3 f4 g0 g1 g2 g3 g4 => proj2_sig (add_formula_sig f0 f1 f2 f3 f4 g0 g1 g2 g3 g4)). - -Definition add (f g : fe1305) : fe1305 := Eval cbv beta iota delta [proj1_sig add_formula_sig] in - let (f03, f4) := f in - let (f02, f3) := f03 in - let (f01, f2) := f02 in - let (f0, f1) := f01 in - let (g03, g4) := g in - let (g02, g3) := g03 in - let (g01, g2) := g02 in - let (g0, g1) := g01 in - proj1_sig (add_formula_sig f0 f1 f2 f3 f4 g0 g1 g2 g3 g4). - -Definition add_correct f g : add f g = ModularBaseSystemInterface.add f g. +Definition add (f g : fe1305) : fe1305 := + Eval cbv beta iota delta [proj1_sig add_sig] in + let '(f0,f1,f2,f3,f4) := f in + let '(g0,g1,g2,g3,g4) := g in + proj1_sig (add_sig (f0,f1,f2,f3,f4) (g0,g1,g2,g3,g4)). + +Definition add_correct (f g : fe1305) + : add f g = ModularBaseSystemInterface.add f g := + let '(f0,f1,f2,f3,f4) := f in + let '(g0,g1,g2,g3,g4) := g in + proj2_sig (add_sig (f0,f1,f2,f3,f4) (g0,g1,g2,g3,g4)). + +Definition sub_sig (f g : fe1305) : + { fg : fe1305 | fg = ModularBaseSystemInterface.sub f g}. Proof. cbv [fe1305] in *. repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. - rewrite <-add_formula_correct. - reflexivity. -Qed. - -Definition sub_formula_sig (f0 f1 f2 f3 f4 g0 g1 g2 g3 g4: Z) : - { fg | fg = ModularBaseSystemInterface.sub (f0,f1,f2,f3,f4) (g0,g1,g2,g3,g4) }. -Proof. eexists. cbv. reflexivity. Defined. -Definition sub_formula_correct := Eval cbv [proj2_sig] in -(fun f0 f1 f2 f3 f4 g0 g1 g2 g3 g4 => proj2_sig (sub_formula_sig f0 f1 f2 f3 f4 g0 g1 g2 g3 g4)). - -Definition sub (f g : fe1305) : fe1305 := Eval cbv beta iota delta [proj1_sig sub_formula_sig] in - let (f03, f4) := f in - let (f02, f3) := f03 in - let (f01, f2) := f02 in - let (f0, f1) := f01 in - let (g03, g4) := g in - let (g02, g3) := g03 in - let (g01, g2) := g02 in - let (g0, g1) := g01 in - proj1_sig (sub_formula_sig f0 f1 f2 f3 f4 g0 g1 g2 g3 g4). - -Definition sub_correct f g : sub f g = ModularBaseSystemInterface.sub f g. +Definition sub (f g : fe1305) : fe1305 := + Eval cbv beta iota delta [proj1_sig sub_sig] in + let '(f0,f1,f2,f3,f4) := f in + let '(g0,g1,g2,g3,g4) := g in + proj1_sig (sub_sig (f0,f1,f2,f3,f4) (g0,g1,g2,g3,g4)). + +Definition sub_correct (f g : fe1305) + : sub f g = ModularBaseSystemInterface.sub f g := + let '(f0,f1,f2,f3,f4) := f in + let '(g0,g1,g2,g3,g4) := g in + proj2_sig (sub_sig (f0,f1,f2,f3,f4) (g0,g1,g2,g3,g4)). + +Definition mul_sig (f g : fe1305) : + { fg : fe1305 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}. Proof. cbv [fe1305] in *. repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. - rewrite <-sub_formula_correct. - reflexivity. -Qed. - -Definition mul_formula_sig (f0 f1 f2 f3 f4 g0 g1 g2 g3 g4: Z) : - { fg | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) (f0,f1,f2,f3,f4) (g0,g1,g2,g3,g4) }. -Proof. eexists. cbv. autorewrite with zsimplify. reflexivity. Defined. -Definition mul_formula_correct := Eval cbv [proj2_sig] in -(fun f0 f1 f2 f3 f4 g0 g1 g2 g3 g4 => proj2_sig (mul_formula_sig f0 f1 f2 f3 f4 g0 g1 g2 g3 g4)). - -Definition mul (f g : fe1305) : fe1305 := Eval cbv beta iota delta [proj1_sig mul_formula_sig] in - let (f03, f4) := f in - let (f02, f3) := f03 in - let (f01, f2) := f02 in - let (f0, f1) := f01 in - let (g03, g4) := g in - let (g02, g3) := g03 in - let (g01, g2) := g02 in - let (g0, g1) := g01 in - proj1_sig (mul_formula_sig f0 f1 f2 f3 f4 g0 g1 g2 g3 g4). - -Definition mul_correct f g : mul f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g. -Proof. - cbv [fe1305] in *. - repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. - rewrite <-mul_formula_correct. - reflexivity. -Qed. +Definition mul (f g : fe1305) : fe1305 := + Eval cbv beta iota delta [proj1_sig mul_sig] in + let '(f0,f1,f2,f3,f4) := f in + let '(g0,g1,g2,g3,g4) := g in + proj1_sig (mul_sig (f0,f1,f2,f3,f4) (g0,g1,g2,g3,g4)). + +Definition mul_correct (f g : fe1305) + : mul f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g := + let '(f0,f1,f2,f3,f4) := f in + let '(g0,g1,g2,g3,g4) := g in + proj2_sig (mul_sig (f0,f1,f2,f3,f4) (g0,g1,g2,g3,g4)). Import Morphisms. Lemma field1305 : @field fe eq zero one opp add sub mul inv div. Proof. - pose proof Equivalence_Reflexive. + pose proof (Equivalence_Reflexive : Reflexive eq). eapply (Field.equivalent_operations_field (fieldR := modular_base_system_field k_subst c_subst)). Grab Existential Variables. + reflexivity. diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index a361e7207..261b6f4fe 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -2,11 +2,12 @@ Require Import Crypto.ModularArithmetic.ModularBaseSystem. Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. -Require Import Crypto.ModularArithmetic.ModularBaseSystemInterface. Require Import Coq.Lists.List Crypto.Util.ListUtil. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.ModularArithmetic.ModularBaseSystemInterface. Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.BaseSystem. +Require Import Algebra. Import ListNotations. Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. Require Import Crypto.Util.Notations. @@ -48,29 +49,91 @@ Definition fe25519 : Type := Eval cbv in fe. Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Let_In. -Definition add (f g:fe25519) : { fg | phi fg = @ModularArithmetic.add modulus (phi f) (phi g) }. +Definition add_sig (f g : fe25519) : + { fg : fe25519 | fg = ModularBaseSystemInterface.add f g}. Proof. cbv [fe25519] in *. repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. eexists. - rewrite <-add_phi. - apply f_equal. cbv. reflexivity. -Qed. +Defined. + +Definition add (f g : fe25519) : fe25519 := + Eval cbv beta iota delta [proj1_sig add_sig] in + let '(f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) := f in + let '(g0,g1,g2,g3,g4,g5,g6,g7,g8,g9) := g in + proj1_sig (add_sig (f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) (g0,g1,g2,g3,g4,g5,g6,g7,g8,g9)). + +Definition add_correct (f g : fe25519) + : add f g = ModularBaseSystemInterface.add f g := + let '(f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) := f in + let '(g0,g1,g2,g3,g4,g5,g6,g7,g8,g9) := g in + proj2_sig (add_sig (f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) (g0,g1,g2,g3,g4,g5,g6,g7,g8,g9)). -Definition mul (f g:fe25519) : { fg | phi fg = @ModularArithmetic.mul modulus (phi f) (phi g) }. +Definition sub_sig (f g : fe25519) : + { fg : fe25519 | fg = ModularBaseSystemInterface.sub f g}. +Proof. + cbv [fe25519] in *. + repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. + eexists. + cbv. + reflexivity. +Defined. + +Definition sub (f g : fe25519) : fe25519 := + Eval cbv beta iota delta [proj1_sig sub_sig] in + let '(f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) := f in + let '(g0,g1,g2,g3,g4,g5,g6,g7,g8,g9) := g in + proj1_sig (sub_sig (f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) (g0,g1,g2,g3,g4,g5,g6,g7,g8,g9)). + +Definition sub_correct (f g : fe25519) + : sub f g = ModularBaseSystemInterface.sub f g := + let '(f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) := f in + let '(g0,g1,g2,g3,g4,g5,g6,g7,g8,g9) := g in + proj2_sig (sub_sig (f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) (g0,g1,g2,g3,g4,g5,g6,g7,g8,g9)). + +Definition mul_sig (f g : fe25519) : + { fg : fe25519 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}. Proof. cbv [fe25519] in *. repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. eexists. - rewrite <-(mul_phi (c_ := c_) (k_ := k_)) by auto using k_subst,c_subst. - apply f_equal. cbv. autorewrite with zsimplify. reflexivity. +Defined. + +Definition mul (f g : fe25519) : fe25519 := + Eval cbv beta iota delta [proj1_sig mul_sig] in + let '(f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) := f in + let '(g0,g1,g2,g3,g4,g5,g6,g7,g8,g9) := g in + proj1_sig (mul_sig (f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) (g0,g1,g2,g3,g4,g5,g6,g7,g8,g9)). + +Definition mul_correct (f g : fe25519) + : mul f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g := + let '(f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) := f in + let '(g0,g1,g2,g3,g4,g5,g6,g7,g8,g9) := g in + proj2_sig (mul_sig (f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) (g0,g1,g2,g3,g4,g5,g6,g7,g8,g9)). + +Import Morphisms. + +Lemma field25519 : @field fe25519 eq zero one opp add sub mul inv div. +Proof. + pose proof (Equivalence_Reflexive : Reflexive eq). + eapply (Field.equivalent_operations_field (fieldR := modular_base_system_field k_subst c_subst)). + Grab Existential Variables. + + reflexivity. + + reflexivity. + + reflexivity. + + intros; rewrite mul_correct; reflexivity. + + intros; rewrite sub_correct; reflexivity. + + intros; rewrite add_correct; reflexivity. + + reflexivity. + + reflexivity. Qed. + (* Local Transparent Let_In. Eval cbv iota beta delta [proj1_sig mul Let_In] in (fun f0 f1 f2 f3 f4 g0 g1 g2 g3 g4 => proj1_sig (mul (f4,f3,f2,f1,f0) (g4,g3,g2,g1,g0))). -- cgit v1.2.3