From b28d236a545605e116a1efe08570027a979960aa Mon Sep 17 00:00:00 2001 From: jadep Date: Fri, 11 Nov 2016 16:06:20 -0500 Subject: separate freeze into two parts --- src/ModularArithmetic/ModularBaseSystemOpt.v | 82 ++++++++++++++-------------- src/Specific/GF25519.v | 66 +++++++++++++++++++--- 2 files changed, 98 insertions(+), 50 deletions(-) diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 7480db3b0..121e605a3 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -916,48 +916,27 @@ Section Canonicalization. (preconditions : FreezePreconditions freeze_input_bound int_width). Local Notation digits := (tuple Z (length limb_widths)). - Definition carry_full_3_opt_cps_sig - {T} (f : list Z -> T) + Definition carry_full_3_opt_sig (us : list Z) - : { d : T | length us = length limb_widths - -> d = f (carry_full (carry_full (carry_full us))) }. + : { d : list Z | length us = length limb_widths + -> d = carry_full (carry_full (carry_full us)) }. Proof. eexists. - transitivity (carry_full_opt_cps c_ (carry_full_opt_cps c_ (carry_full_opt_cps c_ f)) us). + transitivity (carry_full_opt_cps c_ (carry_full_opt_cps c_ (carry_full_opt c_)) us). Focus 2. { - rewrite !carry_full_opt_cps_correct; repeat (autorewrite with distr_length; rewrite ?length_carry_full; auto). + rewrite !carry_full_opt_cps_correct; try rewrite carry_full_opt_correct; repeat (autorewrite with distr_length; rewrite ?length_carry_full; auto). } Unfocus. reflexivity. Defined. - Definition carry_full_3_opt_cps {T} (f : list Z -> T) (us : list Z) : T - := Eval cbv [proj1_sig carry_full_3_opt_cps_sig] in proj1_sig (carry_full_3_opt_cps_sig f us). + Definition carry_full_3_opt (us : list Z) : list Z + := Eval cbv [proj1_sig carry_full_3_opt_sig] in proj1_sig (carry_full_3_opt_sig us). - Definition carry_full_3_opt_cps_correct {T} (f : list Z -> T) us + Definition carry_full_3_opt_correct us : length us = length limb_widths - -> carry_full_3_opt_cps f us = f (carry_full (carry_full (carry_full us))) - := proj2_sig (carry_full_3_opt_cps_sig f us). - - Definition conditional_subtract_modulus_opt_sig (f : list Z) (cond : Z) : - { g | g = conditional_subtract_modulus int_width f cond}. - Proof. - eexists. - cbv [conditional_subtract_modulus]. - let LHS := match goal with |- ?LHS = ?RHS => LHS end in - let RHS := match goal with |- ?LHS = ?RHS => RHS end in - let RHSf := match (eval pattern (neg int_width cond) in RHS) with ?RHSf _ => RHSf end in - change (LHS = Let_In (neg int_width cond) RHSf). - cbv [map2 map]. - reflexivity. - Defined. - - Definition conditional_subtract_modulus_opt f cond : list Z - := Eval cbv [proj1_sig conditional_subtract_modulus_opt_sig] in proj1_sig (conditional_subtract_modulus_opt_sig f cond). - - Definition conditional_subtract_modulus_opt_correct f cond - : conditional_subtract_modulus_opt f cond = conditional_subtract_modulus int_width f cond - := Eval cbv [proj2_sig conditional_subtract_modulus_opt_sig] in proj2_sig (conditional_subtract_modulus_opt_sig f cond). + -> carry_full_3_opt us = carry_full (carry_full (carry_full us)) + := proj2_sig (carry_full_3_opt_sig us). Lemma ge_modulus'_cps : forall {A} (f : Z -> A) (us : list Z) i b, f (ge_modulus' id us b i) = ge_modulus' f us b i. @@ -984,6 +963,33 @@ Section Canonicalization. ge_modulus_opt us= ge_modulus us := Eval cbv [proj2_sig ge_modulus_opt_sig] in proj2_sig (ge_modulus_opt_sig us). + Definition conditional_subtract_modulus_opt_sig (f : list Z): + { g | g = conditional_subtract_modulus int_width f (ge_modulus f) }. + Proof. + eexists. + cbv [conditional_subtract_modulus]. + let LHS := match goal with |- ?LHS = ?RHS => LHS end in + let RHS := match goal with |- ?LHS = ?RHS => RHS end in + let RHSf := match (eval pattern (neg int_width (ge_modulus f)) in RHS) with ?RHSf _ => RHSf end in + change (LHS = Let_In (neg int_width (ge_modulus f)) RHSf). + cbv [ge_modulus]. + rewrite ge_modulus'_cps. + cbv beta iota delta [ge_modulus ge_modulus']. + change length with length_opt. + change nth_default with @nth_default_opt. + change @Pow2Base.base_from_limb_widths with base_from_limb_widths_opt. + change minus with minus_opt. + reflexivity. + Defined. + + Definition conditional_subtract_modulus_opt f : list Z + := Eval cbv [proj1_sig conditional_subtract_modulus_opt_sig] in proj1_sig (conditional_subtract_modulus_opt_sig f). + + Definition conditional_subtract_modulus_opt_correct f + : conditional_subtract_modulus_opt f = conditional_subtract_modulus int_width f (ge_modulus f) + := Eval cbv [proj2_sig conditional_subtract_modulus_opt_sig] in proj2_sig (conditional_subtract_modulus_opt_sig f). + + Definition freeze_opt_sig (us : list Z) : { b : list Z | length us = length limb_widths -> b = ModularBaseSystemList.freeze int_width us }. @@ -992,19 +998,11 @@ Section Canonicalization. cbv [ModularBaseSystemList.freeze]. rewrite <-conditional_subtract_modulus_opt_correct. intros. - cbv [ge_modulus]. - rewrite ge_modulus'_cps. + rewrite <-carry_full_3_opt_correct by auto. let LHS := match goal with |- ?LHS = ?RHS => LHS end in let RHS := match goal with |- ?LHS = ?RHS => RHS end in - let RHSf := match (eval pattern (carry_full (carry_full (carry_full us))) in RHS) with ?RHSf _ => RHSf end in - rewrite <-carry_full_3_opt_cps_correct with (f := RHSf) by auto. - cbv [carry_full_3_opt_cps carry_full_opt_cps carry_sequence_opt_cps]. - cbv [ge_modulus']. - cbv beta iota delta [ge_modulus ge_modulus']. - change length with length_opt. - change nth_default with @nth_default_opt. - change @Pow2Base.base_from_limb_widths with base_from_limb_widths_opt. - change minus with minus_opt. + let RHSf := match (eval pattern (carry_full_3_opt us) in RHS) with ?RHSf _ => RHSf end in + change (LHS = Let_In (carry_full_3_opt us) RHSf). reflexivity. Defined. diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 2c0365fd2..de6a47c01 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -499,8 +499,37 @@ Proof. assumption. Defined. -Definition freeze_sig (f : fe25519) : - { f' : fe25519 | f' = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)) }. +Definition prefreeze_sig (f : fe25519) : + { f' : fe25519 | f' = from_list_default 0 10 (carry_full_3_opt c_ (to_list 10 f)) }. +Proof. + cbv [fe25519] in *. + repeat match goal with p : (_ * Z)%type |- _ => destruct p end. + eexists. + cbv - [from_list_default]. + (* TODO(jgross,jadep): use Reflective linearization here? *) + repeat ( + set_evars; rewrite app_Let_In_nd; subst_evars; + eapply Proper_Let_In_nd_changebody; [reflexivity|intro]). + cbv [from_list_default from_list_default']. + reflexivity. +Defined. + +Definition prefreeze (f : fe25519) : fe25519 := + Eval cbv beta iota delta [proj1_sig prefreeze_sig] in + let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in + proj1_sig (prefreeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)). + +Definition prefreeze_correct (f : fe25519) + : prefreeze f = from_list_default 0 10 (carry_full_3_opt c_ (to_list 10 f)). +Proof. + pose proof (proj2_sig (prefreeze_sig f)). + cbv [fe25519] in *. + repeat match goal with p : (_ * Z)%type |- _ => destruct p end. + assumption. +Defined. + +Definition postfreeze_sig (f : fe25519) : + { f' : fe25519 | f' = from_list_default 0 10 (conditional_subtract_modulus_opt (int_width := int_width) (to_list 10 f)) }. Proof. cbv [fe25519] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. @@ -517,20 +546,41 @@ Proof. reflexivity. Defined. -Definition freeze (f : fe25519) : fe25519 := - Eval cbv beta iota delta [proj1_sig freeze_sig] in +Definition postfreeze (f : fe25519) : fe25519 := + Eval cbv beta iota delta [proj1_sig postfreeze_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in - proj1_sig (freeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)). + proj1_sig (postfreeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)). -Definition freeze_correct (f : fe25519) - : freeze f = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)). +Definition postfreeze_correct (f : fe25519) + : postfreeze f = from_list_default 0 10 (conditional_subtract_modulus_opt (int_width := int_width) (to_list 10 f)). Proof. - pose proof (proj2_sig (freeze_sig f)). + pose proof (proj2_sig (postfreeze_sig f)). cbv [fe25519] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Defined. +Definition freeze (f : fe25519) : fe25519 := + dlet x := prefreeze f in + postfreeze x. + +Local Transparent Let_In. +Definition freeze_correct (f : fe25519) + : freeze f = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)). +Proof. + cbv [freeze_opt freeze Let_In]. + rewrite prefreeze_correct. + rewrite postfreeze_correct. + Check from_list_default_eq. + match goal with + |- appcontext [to_list _ (from_list_default _ ?n ?xs)] => + assert (length xs = n) as pf; [ | rewrite from_list_default_eq with (pf0 := pf) ] end. + { rewrite carry_full_3_opt_correct; repeat rewrite ModularBaseSystemListProofs.length_carry_full; auto using length_to_list. } + rewrite to_list_from_list. + reflexivity. +Qed. +Local Opaque Let_In. + Definition fieldwiseb_sig (f g : fe25519) : { b | b = @fieldwiseb Z Z 10 Z.eqb f g }. Proof. -- cgit v1.2.3