From 1c8bb0e753f757b5f7cac38b1e681cf20bd6134f Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Tue, 5 Dec 2017 11:42:56 -0500 Subject: Curves.Montgomery.XZ: add+check boringssl ladderstep (#278) --- src/Curves/Montgomery/XZ.v | 25 +++++++++++++++++++++++++ src/Curves/Montgomery/XZProofs.v | 7 +++++++ 2 files changed, 32 insertions(+) (limited to 'src/Curves') diff --git a/src/Curves/Montgomery/XZ.v b/src/Curves/Montgomery/XZ.v index 735e6ac76..87a53b7fe 100644 --- a/src/Curves/Montgomery/XZ.v +++ b/src/Curves/Montgomery/XZ.v @@ -85,6 +85,31 @@ Module M. ((x2, z2), (x3, z3))%core end. + Context {ap2d4:F} {ap2d4_correct:(1+1+1+1)*a24 = a+1+1}. + Definition boringladderstep (x1:F) (Q Q':F*F) : (F*F)*(F*F) := + match Q, Q' with + pair x2 z2, pair x3 z3 => + dlet tmp0l := x3 - z3 in + dlet tmp1l := x2 - z2 in + dlet x2l := x2 + z2 in + dlet z2l := x3 + z3 in + dlet z3 := tmp0l * x2l in + dlet z2 := z2l * tmp1l in + dlet tmp0 := tmp1l^2 in + dlet tmp1 := x2l^2 in + dlet x3l := z3 + z2 in + dlet z2l := z3 - z2 in + dlet x2 := tmp1 * tmp0 in + dlet tmp1l := tmp1 - tmp0 in + dlet z2 := z2l^2 in + dlet z3 := ap2d4 * tmp1l in + dlet x3 := x3l^2 in + dlet tmp0l := tmp0 + z3 in + dlet z3 := x1 * z2 in + dlet z2 := tmp1l * tmp0l in + ((x2, z2), (x3, z3))%core + end. + Context {cswap:bool->F*F->F*F->(F*F)*(F*F)}. Local Notation xor := Coq.Init.Datatypes.xorb. diff --git a/src/Curves/Montgomery/XZProofs.v b/src/Curves/Montgomery/XZProofs.v index d3fd486d8..71d30919c 100644 --- a/src/Curves/Montgomery/XZProofs.v +++ b/src/Curves/Montgomery/XZProofs.v @@ -29,11 +29,13 @@ Module M. Context {a b: F} {b_nonzero:b <> 0}. Context {a24:F} {a24_correct:(1+1+1+1)*a24 = a-(1+1)}. + Context {ap2d4:F} {ap2d4_correct:(1+1+1+1)*a24 = a+1+1}. Local Notation Madd := (M.add(a:=a)(b_nonzero:=b_nonzero)(char_ge_3:=char_ge_3)). Local Notation Mopp := (M.opp(a:=a)(b_nonzero:=b_nonzero)). Local Notation Mpoint := (@M.point F Feq Fadd Fmul a b). Local Notation xzladderstep := (M.xzladderstep(a24:=a24)(Fadd:=Fadd)(Fsub:=Fsub)(Fmul:=Fmul)). Local Notation donnaladderstep := (M.donnaladderstep(a24:=a24)(Fadd:=Fadd)(Fsub:=Fsub)(Fmul:=Fmul)). + Local Notation boringladderstep := (M.boringladderstep(ap2d4:=ap2d4)(Fadd:=Fadd)(Fsub:=Fsub)(Fmul:=Fmul)). Local Notation to_xz := (M.to_xz(Fzero:=Fzero)(Fone:=Fone)(Feq:=Feq)(Fadd:=Fadd)(Fmul:=Fmul)(a:=a)(b:=b)). Lemma donnaladderstep_ok x1 Q Q' : @@ -41,6 +43,11 @@ Module M. eq (xzladderstep x1 Q Q') (donnaladderstep x1 Q Q'). Proof. cbv; break_match; repeat split; fsatz. Qed. + Lemma boringladderstep_ok x1 Q Q' : + let eq := fieldwise (n:=2) (fieldwise (n:=2) Feq) in + eq (xzladderstep x1 Q Q') (boringladderstep x1 Q Q'). + Proof. cbv; break_match; repeat split; fsatz. Qed. + Definition projective (P:F*F) := if dec (snd P = 0) then fst P <> 0 else True. Definition eq (P Q:F*F) := fst P * snd Q = fst Q * snd P. -- cgit v1.2.3