diff options
author | 2016-11-14 15:50:12 -0500 | |
---|---|---|
committer | 2016-11-14 15:50:12 -0500 | |
commit | ac116a5b734aba589b923ba00bae56d244360af8 (patch) | |
tree | 47b8c550da866a37b0d674b228c8d56e900e01ce /src/SpecificGen/GF5211_32.v | |
parent | 9f9fa521e29293af46123b1c97fd1426d0cf240a (diff) |
Update bounds things with prefreeze
Diffstat (limited to 'src/SpecificGen/GF5211_32.v')
-rw-r--r-- | src/SpecificGen/GF5211_32.v | 67 |
1 files changed, 58 insertions, 9 deletions
diff --git a/src/SpecificGen/GF5211_32.v b/src/SpecificGen/GF5211_32.v index c2272aa1a..bca4d1050 100644 --- a/src/SpecificGen/GF5211_32.v +++ b/src/SpecificGen/GF5211_32.v @@ -22,8 +22,8 @@ Local Open Scope Z. Definition modulus : Z := Eval compute in 2^521 - 1. Lemma prime_modulus : prime modulus. Admitted. +Definition int_width := Eval compute in (2 * 32)%Z. Definition freeze_input_bound := 32%Z. -Definition int_width := 32%Z. Instance params5211_32 : PseudoMersenneBaseParams modulus. construct_params prime_modulus 20%nat 521. @@ -481,8 +481,37 @@ Proof. assumption. Defined. -Definition freeze_sig (f : fe5211_32) : - { f' : fe5211_32 | f' = from_list_default 0 20 (freeze_opt (int_width := int_width) c_ (to_list 20 f)) }. +Definition prefreeze_sig (f : fe5211_32) : + { f' : fe5211_32 | f' = from_list_default 0 20 (carry_full_3_opt c_ (to_list 20 f)) }. +Proof. + cbv [fe5211_32] 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 : fe5211_32) : fe5211_32 := + Eval cbv beta iota delta [proj1_sig prefreeze_sig] in + let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17, f18, f19) := f in + proj1_sig (prefreeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17, f18, f19)). + +Definition prefreeze_correct (f : fe5211_32) + : prefreeze f = from_list_default 0 20 (carry_full_3_opt c_ (to_list 20 f)). +Proof. + pose proof (proj2_sig (prefreeze_sig f)). + cbv [fe5211_32] in *. + repeat match goal with p : (_ * Z)%type |- _ => destruct p end. + assumption. +Defined. + +Definition postfreeze_sig (f : fe5211_32) : + { f' : fe5211_32 | f' = from_list_default 0 20 (conditional_subtract_modulus_opt (int_width := int_width) (to_list 20 f)) }. Proof. cbv [fe5211_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. @@ -499,20 +528,40 @@ Proof. reflexivity. Defined. -Definition freeze (f : fe5211_32) : fe5211_32 := - Eval cbv beta iota delta [proj1_sig freeze_sig] in +Definition postfreeze (f : fe5211_32) : fe5211_32 := + Eval cbv beta iota delta [proj1_sig postfreeze_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17, f18, f19) := f in - proj1_sig (freeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17, f18, f19)). + proj1_sig (postfreeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17, f18, f19)). -Definition freeze_correct (f : fe5211_32) - : freeze f = from_list_default 0 20 (freeze_opt (int_width := int_width) c_ (to_list 20 f)). +Definition postfreeze_correct (f : fe5211_32) + : postfreeze f = from_list_default 0 20 (conditional_subtract_modulus_opt (int_width := int_width) (to_list 20 f)). Proof. - pose proof (proj2_sig (freeze_sig f)). + pose proof (proj2_sig (postfreeze_sig f)). cbv [fe5211_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Defined. +Definition freeze (f : fe5211_32) : fe5211_32 := + dlet x := prefreeze f in + postfreeze x. + +Local Transparent Let_In. +Definition freeze_correct (f : fe5211_32) + : freeze f = from_list_default 0 20 (freeze_opt (int_width := int_width) c_ (to_list 20 f)). +Proof. + cbv [freeze_opt freeze Let_In]. + rewrite prefreeze_correct. + rewrite postfreeze_correct. + 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 : fe5211_32) : { b | b = @fieldwiseb Z Z 20 Z.eqb f g }. Proof. |