From f670e48c3b74fbb3a9f21d6c9351b08593af311f Mon Sep 17 00:00:00 2001 From: jadep Date: Tue, 1 Nov 2016 16:57:04 -0400 Subject: Changes to sqrt for easier bounds proofs; currently blocked on broken proof in GF25519Bounded --- src/Specific/GF25519.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'src/Specific/GF25519.v') diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index a39755eee..16ce7a545 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -584,23 +584,23 @@ Proof. exact (proj2_sig (eqb_sig f' g')). Qed. -Definition sqrt_sig (f : fe25519) : - { f' : fe25519 | f' = sqrt_5mod8_opt (int_width := int_width) k_ c_ one_ sqrt_m1 f}. +Print sqrt_5mod8_opt. +Definition sqrt_sig (powf powf_squared f : fe25519) : + { f' : fe25519 | f' = sqrt_5mod8_opt (int_width := int_width) k_ c_ sqrt_m1 powf powf_squared f}. Proof. eexists. 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. reflexivity. Defined. -Definition sqrt (f : fe25519) : fe25519 - := Eval cbv beta iota delta [proj1_sig sqrt_sig] in proj1_sig (sqrt_sig f). +Definition sqrt (powf powf_squared f : fe25519) : fe25519 + := Eval cbv beta iota delta [proj1_sig sqrt_sig] in proj1_sig (sqrt_sig powf powf_squared f). -Definition sqrt_correct (f : fe25519) - : sqrt f = sqrt_5mod8_opt k_ c_ one_ sqrt_m1 f - := Eval cbv beta iota delta [proj2_sig sqrt_sig] in proj2_sig (sqrt_sig f). +Definition sqrt_correct (powf powf_squared f : fe25519) + : sqrt powf powf_squared f = sqrt_5mod8_opt k_ c_ sqrt_m1 powf powf_squared f + := Eval cbv beta iota delta [proj2_sig sqrt_sig] in proj2_sig (sqrt_sig powf powf_squared f). Definition pack_simpl_sig (f : fe25519) : { f' | f' = pack_opt params25519 wire_widths_nonneg bits_eq f }. -- cgit v1.2.3