diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-10-22 00:10:30 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-10-22 00:15:41 -0400 |
| commit | e3b4c19f5983e277b53253fe305c3db8d1cef02b (patch) | |
| tree | 9ba184077bcc2f3899990e0ce898d831c84e6de8 /src/Specific/GF25519.v | |
| parent | 31d24dcb9e53cd21d619d403de8933b8fc451ed8 (diff) | |
add arguments that I forgot
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 283f79974..3ea794435 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -492,7 +492,7 @@ Definition freeze_sig (f : fe25519) : Proof. cbv [fe25519] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - eexists; cbv [freeze_opt]. + eexists; cbv [freeze_opt int_width]. cbv [to_list to_list']. cbv [conditional_subtract_modulus_opt]. rewrite !modulus_digits_subst. @@ -545,13 +545,13 @@ Proof. Qed. Definition eqb_sig (f g : fe25519) : - { b | b = eqb f g }. + { b | b = eqb int_width f g }. Proof. cbv [eqb]. cbv [fe25519] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. - cbv [ModularBaseSystem.freeze]. + cbv [ModularBaseSystem.freeze int_width]. rewrite <-!from_list_default_eq with (d := 0). rewrite <-!(freeze_opt_correct c_) by auto using length_to_list. rewrite <-!freeze_correct. @@ -567,7 +567,7 @@ Definition eqb (f g : fe25519) : bool (g0, g1, g2, g3, g4, g5, g6, g7, g8, g9)). Lemma eqb_correct (f g : fe25519) - : eqb f g = ModularBaseSystem.eqb f g. + : eqb f g = ModularBaseSystem.eqb int_width f g. Proof. set (f' := f); set (g' := g). hnf in f, g; destruct_head' prod. @@ -575,10 +575,10 @@ Proof. Qed. Definition sqrt_sig (f : fe25519) : - { f' : fe25519 | f' = sqrt_5mod8_opt k_ c_ one_ sqrt_m1 f}. + { f' : fe25519 | f' = sqrt_5mod8_opt (int_width := int_width) k_ c_ one_ sqrt_m1 f}. Proof. eexists. - cbv [sqrt_5mod8_opt]. + cbv [sqrt_5mod8_opt int_width]. rewrite <- pow_correct. apply Proper_Let_In_nd_changebody; [reflexivity|intro]. set_evars. rewrite <-!mul_correct, <-eqb_correct. subst_evars. @@ -681,4 +681,4 @@ Definition unpack (f : wire_digits) : fe25519 := Definition unpack_correct (f : wire_digits) : unpack f = unpack_opt params25519 wire_widths_nonneg bits_eq f - := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (unpack_sig f). + := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (unpack_sig f).
\ No newline at end of file |