From 1f36ebc229080fb8edd8f7903cc0466395cbdd43 Mon Sep 17 00:00:00 2001 From: jadep Date: Fri, 17 Jun 2016 15:30:41 -0400 Subject: Specific version of freeze for GF25519 (automation still needs a little work) --- src/ModularArithmetic/ModularBaseSystemOpt.v | 159 +++++++++++++++++++++++---- src/Specific/GF25519.v | 67 ++++++++++- 2 files changed, 202 insertions(+), 24 deletions(-) (limited to 'src') diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 4fd9748c5..8ac8c95c5 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -27,9 +27,9 @@ Definition Z_shiftl_by_opt := Eval compute in Z_shiftl_by. Definition nth_default_opt {A} := Eval compute in @nth_default A. Definition set_nth_opt {A} := Eval compute in @set_nth A. Definition map_opt {A B} := Eval compute in @map A B. -Definition base_from_limb_widths_opt := Eval compute in base_from_limb_widths. Definition full_carry_chain_opt := Eval compute in @full_carry_chain. Definition length_opt := Eval compute in length. +Definition base_opt := Eval compute in @base. Definition Let_In {A P} (x : A) (f : forall y : A, P y) := let y := x in f y. @@ -115,8 +115,9 @@ Section Carries. rewrite <- pull_app_if_sumbool. cbv beta delta [carry carry_and_reduce carry_simple add_to_nth log_cap - pow2_mod Z.ones Z.pred base + pow2_mod Z.ones Z.pred PseudoMersenneBaseParams.limb_widths]. + change @base with @base_opt. change @nth_default with @nth_default_opt in *. change @set_nth with @set_nth_opt in *. lazymatch goal with @@ -131,7 +132,6 @@ Section Carries. change @set_nth with @set_nth_opt. change @map with @map_opt. rewrite <- @beq_nat_eq_nat_dec. - change base_from_limb_widths with base_from_limb_widths_opt. reflexivity. Defined. @@ -193,6 +193,39 @@ Section Carries. @carry_opt_cps T i f b = f (carry i b) := proj2_sig (carry_opt_cps_sig i f b). + Definition carry_sequence_opt_cps2_sig {T} (is : list nat) (us : digits) + (f : digits -> T) + : { b : T | (forall i, In i is -> i < length base)%nat -> b = f (carry_sequence is us) }. + Proof. + eexists. + cbv [carry_sequence]. + transitivity (fold_right carry_opt_cps f (List.rev is) us). + Focus 2. + { + assert (forall i, In i (rev is) -> i < length base)%nat as Hr. { + subst. intros. rewrite <- in_rev in *. auto. } + remember (rev is) as ris eqn:Heq. + rewrite <- (rev_involutive is), <- Heq. + clear H Heq is. + rewrite fold_left_rev_right. + revert us; induction ris; [ reflexivity | ]; intros. + { simpl. + rewrite <- IHris; clear IHris; [|intros; apply Hr; right; assumption]. + rewrite carry_opt_cps_correct; [reflexivity|]. + apply Hr; left; reflexivity. + } } + Unfocus. + reflexivity. + Defined. + + Definition carry_sequence_opt_cps2 {T} is us (f : digits -> T) := + Eval cbv [proj1_sig carry_sequence_opt_cps2_sig] in + proj1_sig (carry_sequence_opt_cps2_sig is us f). + + Definition carry_sequence_opt_cps2_correct {T} is us (f : digits -> T) + : (forall i, In i is -> i < length base)%nat -> carry_sequence_opt_cps2 is us f = f (carry_sequence is us) + := proj2_sig (carry_sequence_opt_cps2_sig is us f). + Definition carry_sequence_opt_cps_sig (is : list nat) (us : digits) : { b : digits | (forall i, In i is -> i < length base)%nat -> b = carry_sequence is us }. Proof. @@ -234,8 +267,7 @@ Section Carries. rewrite carry_sequence_opt_cps_correct by assumption. apply carry_sequence_rep; eauto using rep_length. Qed. - - + Lemma full_carry_chain_bounds : forall i, In i full_carry_chain -> (i < length base)%nat. Proof. unfold full_carry_chain; rewrite <-base_length; intros. @@ -257,6 +289,27 @@ Section Carries. Definition carry_full_opt_correct us : carry_full_opt us = carry_full us := proj2_sig (carry_full_opt_sig us). + Definition carry_full_opt_cps_sig + {T} + (f : digits -> T) + (us : digits) + : { d : T | d = f (carry_full us) }. + Proof. + eexists. + rewrite <- carry_full_opt_correct. + cbv beta iota delta [carry_full_opt]. + rewrite carry_sequence_opt_cps_correct by apply full_carry_chain_bounds. + rewrite <-carry_sequence_opt_cps2_correct by apply full_carry_chain_bounds. + reflexivity. + Defined. + + Definition carry_full_opt_cps {T} (f : digits -> T) (us : digits) : T + := Eval cbv [proj1_sig carry_full_opt_cps_sig] in proj1_sig (carry_full_opt_cps_sig f us). + + Definition carry_full_opt_cps_correct {T} us (f : digits -> T) : + carry_full_opt_cps f us = f (carry_full us) := + proj2_sig (carry_full_opt_cps_sig f us). + End Carries. Section Addition. @@ -439,12 +492,11 @@ Section Multiplication. eexists. cbv [BaseSystem.mul mul mul_each mul_bi mul_bi' zeros ext_base reduce]. rewrite <- mul'_opt_correct. - cbv [base PseudoMersenneBaseParams.limb_widths]. + change @base with base_opt. rewrite map_shiftl by apply k_nonneg. rewrite c_subst. rewrite k_subst. - change @map with @map_opt. - change base_from_limb_widths with base_from_limb_widths_opt. + change @map with @map_opt. change @Z_shiftl_by with @Z_shiftl_by_opt. reflexivity. Defined. @@ -505,6 +557,8 @@ Section Canonicalization. eexists. cbv [isFull']. change max_bound with max_bound_opt. + rewrite c_subst. + change Z.sub with Z_sub_opt. reflexivity. Defined. @@ -514,35 +568,96 @@ Section Canonicalization. Definition isFull'_opt_correct us full i: isFull'_opt us full i = isFull' us full i := proj2_sig (isFull'_opt_sig us full i). - Definition and_term_opt_sig (us : T) : { b : Z | b = and_term us }. + Definition and_term_opt_sig (us : list Z) : { b : Z | b = and_term us }. Proof. eexists. cbv [and_term isFull]. change length with length_opt. rewrite <-isFull'_opt_correct. change max_ones with max_ones_opt. + change @base with base_opt. + change minus with minus_opt. reflexivity. Defined. - Definition and_term_opt (us : T) : Z + Definition and_term_opt (us : digits) : Z := Eval cbv [proj1_sig and_term_opt_sig] in proj1_sig (and_term_opt_sig us). Definition and_term_opt_correct us : and_term_opt us = and_term us := - proj2_sig (and_term_opt_sig us). + proj2_sig (and_term_opt_sig us). + + Definition modulus_digits_opt_sig : + { b : digits | b = modulus_digits }. + Proof. + eexists. + cbv beta iota delta [modulus_digits modulus_digits' app]. + change max_bound with max_bound_opt. + rewrite c_subst. + change length with length_opt. + change minus with minus_opt. + change Z.add with Z_add_opt. + change Z.sub with Z_sub_opt. + change @base with base_opt. + reflexivity. + Defined. + + Definition modulus_digits_opt : digits + := Eval cbv [proj1_sig modulus_digits_opt_sig] in proj1_sig (modulus_digits_opt_sig). + + Definition modulus_digits_opt_correct + : modulus_digits_opt = modulus_digits + := proj2_sig (modulus_digits_opt_sig). + + + Definition carry_full_3_opt_cps_sig + {T} (f : digits -> T) + (us : digits) + : { d : T | d = f (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). + Focus 2. { + rewrite !carry_full_opt_cps_correct by assumption; reflexivity. + } + Unfocus. + reflexivity. + Defined. + + Definition carry_full_3_opt_cps {T} (f : digits -> T) (us : digits) : 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_cps_correct {T} (f : digits -> T) us : + 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 freeze_opt_sig (us : T) : { b : digits | b = freeze us }. Proof. eexists. - cbv beta iota delta [freeze map2]. - repeat erewrite <-carry_full_opt_correct by eauto. - change and_term with and_term_opt. + cbv [freeze]. + cbv [and_term]. + 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 (isFull (carry_full (carry_full (carry_full us)))) in RHS) with ?RHSf _ => RHSf end in + change (LHS = Let_In (isFull(carry_full (carry_full (carry_full us)))) RHSf). + 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). + cbv beta iota delta [and_term isFull isFull']. + change length with length_opt. + change max_bound with max_bound_opt. + rewrite c_subst. + change max_ones with max_ones_opt. + change @base with base_opt. + change minus with minus_opt. + rewrite <-modulus_digits_opt_correct. change @map with @map_opt. reflexivity. Defined. Definition freeze_opt (us : T) : digits - := Eval cbv [proj1_sig freeze_opt_sig] in proj1_sig (freeze_opt_sig us). + := Eval cbv beta iota delta [proj1_sig freeze_opt_sig] in proj1_sig (freeze_opt_sig us). Definition freeze_opt_correct us : freeze_opt us = freeze us @@ -565,14 +680,14 @@ Section Canonicalization. eauto using freeze_preserves_rep. Qed. - Lemma freeze_opt_spec : forall us x, rep us x -> - rep (freeze_opt us) x /\ - (forall vs, rep vs x -> - @pre_carry_bounds _ _ int_width us -> - @pre_carry_bounds _ _ int_width vs -> - freeze_opt us = freeze_opt vs). + Lemma freeze_opt_spec : forall us vs x, rep us x -> rep vs x -> + @pre_carry_bounds _ _ int_width us -> + @pre_carry_bounds _ _ int_width vs -> + (PseudoMersenneBaseRep.rep (freeze_opt us) x /\ freeze_opt us = freeze_opt vs). Proof. - split; eauto using freeze_opt_preserves_rep; eauto using freeze_opt_canonical. + split; eauto using freeze_opt_canonical. + change PseudoMersenneBaseRep.rep with rep. + auto using freeze_opt_preserves_rep. Qed. End Canonicalization. \ No newline at end of file diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 37e0c08db..2ec338625 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -32,11 +32,30 @@ Defined. (* Precompute k and c *) Definition k_ := Eval compute in k. Definition c_ := Eval compute in c. +Definition base_ := Eval compute in base. +Definition limb_widths_ := Eval compute in limb_widths. + +Definition c_subst : c = c_ := eq_refl c_. + +Lemma c_reduce1 : (c * Z.ones (32 - log_cap (pred (length base))) < max_bound 0 + 1)%Z. +Proof. + cbv; congruence. +Qed. + +Lemma c_reduce2 : c <= max_bound 0 - c. +Proof. + cbv; congruence. +Qed. + +Lemma two_pow_k_le_2modulus : (2 ^ k <= 2 * modulus)%Z. +Proof. + cbv; congruence. +Qed. (* Makes Qed not take forever *) Opaque Z.shiftr Pos.iter Z.div2 Pos.div2 Pos.div2_up Pos.succ Z.land Z.of_N Pos.land N.ldiff Pos.pred_N Pos.pred_double Z.opp Z.mul Pos.mul - Let_In digits Z.add Pos.add Z.pos_sub. + Let_In digits Z.add Pos.add Z.pos_sub andb Z.eqb Z.ltb. Local Open Scope nat_scope. Lemma GF25519Base25Point5_mul_reduce_formula : @@ -47,7 +66,7 @@ Lemma GF25519Base25Point5_mul_reduce_formula : -> rep ls (f*g)%F}. Proof. eexists; intros ? ? Hf Hg. - pose proof (carry_mul_opt_rep k_ c_ (eq_refl k_) (eq_refl c_) _ _ _ _ Hf Hg) as Hfg. + pose proof (carry_mul_opt_rep k_ c_ (eq_refl k_) c_subst _ _ _ _ Hf Hg) as Hfg. compute_formula. Time Defined. @@ -84,6 +103,50 @@ Proof. compute_formula. Defined. +Lemma GF25519Base25Point5_freeze_formula : + forall f0 f1 f2 f3 f4 f5 f6 f7 f8 f9, + {ls | forall x, rep [f0;f1;f2;f3;f4;f5;f6;f7;f8;f9] x + -> rep ls x}. +Proof. + eexists. + intros x Hf. + assert (1 < length base)%nat as lt_1_length_base by (cbv; repeat constructor). + assert (0 < 32)%Z by omega. + assert (forall w : Z, In w limb_widths -> (w <= 32)%Z) by + (cbv [limb_widths params25519 limb_widths_from_len In]; intros w w_cases; + repeat (destruct w_cases as [ ? | w_cases]; [ subst; omega | ]); exfalso; assumption). + assert (0 < c)%Z by (change c with c_; cbv; congruence). + pose proof c_reduce1. + pose proof c_reduce2. + pose proof two_pow_k_le_2modulus. + pose proof (@freeze_opt_preserves_rep modulus params25519 subCoeff c_ (eq_refl c_) lt_1_length_base 32) as Hfreeze_rep. + repeat match goal with H : ?P, H' : ?P -> _ |- _ => specialize (H' H) end. + specialize (Hfreeze_rep _ _ Hf). + change ModularBaseSystem.rep with rep in Hfreeze_rep. + match goal with H : @rep ?M ?P (?f ?l) ?result |- _ => + let m := fresh "m" in + set (m := M) in H at 1; change M with m in |- * at 1; + (let p := fresh "p" in + set (p := P) in H at 1; change P with p in |- * at 1; + (let r := fresh "r" in + set (r := result) in H |- *)) + end. + cbv [freeze_opt] in Hfreeze_rep. + cbv [carry_full_3_opt_cps] in Hfreeze_rep. + cbv -[m p r rep] in Hfreeze_rep. + exact Hfreeze_rep. +Defined. + +(* Uncomment the below to see pretty-printed freeze function *) +(* +Local Transparent Let_In. +Infix "<<" := Z.shiftr (at level 50). +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. -- cgit v1.2.3