@@ -24,10 +24,15 @@ Module M.
2424 Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
2525 {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
2626 {Feq_dec:Decidable.DecidableRel Feq}
27- {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3}
28- {char_ge_5:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 5}
29- {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12}
3027 {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}.
28+
29+ Lemma Private_char_ge_3: @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3.
30+ Proof . clear -char_ge_28; eapply Algebra.Hierarchy.char_ge_weaken; eauto; vm_decide. Qed .
31+ Context {char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3}. (* appears in statement *)
32+ Local Instance char_ge_5: @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 5.
33+ Proof . clear -char_ge_28; eapply Algebra.Hierarchy.char_ge_weaken; eauto; vm_decide. Qed .
34+ Local Instance char_ge_12: @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12.
35+ Proof . clear -char_ge_28; eapply Algebra.Hierarchy.char_ge_weaken; eauto; vm_decide. Qed .
3136 Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
3237 Local Infix "+" := Fadd. Local Infix "*" := Fmul.
3338 Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
@@ -40,6 +45,7 @@ Module M.
4045 Local Notation Madd := (M.add(a:=a)(b_nonzero:=b_nonzero)(char_ge_3:=char_ge_3)).
4146 Local Notation Mopp := (M.opp(a:=a)(b_nonzero:=b_nonzero)).
4247 Local Notation Mpoint := (@M.point F Feq Fadd Fmul a b).
48+ Local Notation X0 := (M.X0(Fzero:=Fzero)(Feq:=Feq)(Fadd:=Fadd)(Fmul:=Fmul)(a:=a)(b:=b)).
4349 Local Notation to_xz := (M.to_xz(Fzero:=Fzero)(Fone:=Fone)(Feq:=Feq)(Fadd:=Fadd)(Fmul:=Fmul)(a:=a)(b:=b)).
4450 Local Notation xzladderstep := (M.xzladderstep(a24:=a24)(Fadd:=Fadd)(Fsub:=Fsub)(Fmul:=Fmul)).
4551
@@ -226,10 +232,7 @@ Module M.
226232 if dec (snd xz = 0) then 0 else fst xz / snd xz.
227233 Hint Unfold to_x : points_as_coordinates.
228234
229- Lemma to_x_to_xz Q : to_x (to_xz Q) = match M.coordinates Q with
230- | ∞ => 0
231- | (x,y) => x
232- end .
235+ Lemma to_x_to_xz Q : to_x (to_xz Q) = X0 Q.
233236 Proof . t. Qed .
234237
235238 Lemma proper_to_x_projective xz x'z'
@@ -269,17 +272,11 @@ Module M.
269272 Lemma Z_shiftr_testbit_1 n i: Logic.eq (n>>i)%Z (Z.div2 (n >> i) + Z.div2 (n >> i) + Z.b2z (Z.testbit n i))%Z.
270273 Proof . rewrite ?Z.testbit_odd, ?Z.add_diag, <-?Z.div2_odd; reflexivity. Qed .
271274
275+ Context (HFinv : Finv 0 = 0) (scalarbits : Z) (Hscalarbits : (0 <= scalarbits)%Z).
276+
272277 (* We prove montladder correct by considering the zero and non-zero case
273278 separately. *)
274-
275- Lemma montladder_correct_0
276- (HFinv : Finv 0 = 0)
277- (n : Z)
278- (scalarbits : Z) (point : F)
279- (Hz : point = 0)
280- (Hn : (0 <= n < 2^scalarbits)%Z)
281- (Hscalarbits : (0 <= scalarbits)%Z)
282- : montladder scalarbits (Z.testbit n) point = 0.
279+ Lemma montladder_correct_0 n x (Hx : Feq x 0) : montladder scalarbits (Z.testbit n) x = 0.
283280 Proof .
284281 cbv beta delta [M.montladder].
285282 (* [while.by_invariant] expects a goal like [?P (while _ _ _ _)], make it so: *)
@@ -292,7 +289,7 @@ Module M.
292289 (fun s => Z.to_nat (Z.succ (snd s)))).
293290 { split.
294291 (* invariant holds in the beginning *)
295- { cbn; split; [lia|split;[reflexivity|t]]. }
292+ { cbn; split; [lia|split;[reflexivity|try t]]. }
296293 { (* fuel <= measure *) cbn. rewrite Z.succ_pred. reflexivity. } }
297294 { intros [ [ [ [ [x2 z2] x3] z3] swap] i] [Hi [Hz2 Hx3z3]].
298295 destruct (i >=? 0)%Z eqn:Hbranch; (* did the loop continue? *)
@@ -313,44 +310,40 @@ Module M.
313310 cbv [M.cswap]; break_match; break_match_hyps; setoid_subst_rel Feq; fsatz. } }
314311 Qed .
315312
316- Lemma montladder_correct_nz
317- (HFinv : Finv 0 = 0)
318- (n : Z) (P : M.point)
319- (scalarbits : Z) (point : F)
320- (Hnz : point <> 0)
321- (Hn : (0 <= n < 2^scalarbits)%Z)
322- (Hscalarbits : (0 <= scalarbits)%Z)
323- (Hpoint : point = to_x (to_xz P))
324- : montladder scalarbits (Z.testbit n) point = to_x (to_xz (scalarmult n P)).
313+ Lemma montladder_correct_nz n P (Hnz : X0 P <> 0)
314+ : montladder scalarbits (Z.testbit n) (X0 P) = X0 (scalarmult (n mod 2^scalarbits) P).
325315 Proof .
326316 pose proof (let (_, h, _, _) := AffineInstances.M.MontgomeryWeierstrassIsomorphism b_nonzero (a:=a) a2m4_nz in h) as commutative_group.
327317 cbv beta delta [M.montladder].
328318 (* [while.by_invariant] expects a goal like [?P (while _ _ _ _)], make it so: *)
329319 lazymatch goal with |- context [while ?t ?b ?l ?i] => pattern (while t b l i) end.
330320 eapply (while.by_invariant_fuel
331321 (fun '(x2, z2, x3, z3, swap, i) =>
332- (i >= -1 )%Z /\
322+ (-1 <= i < scalarbits )%Z /\
333323 projective (pair x2 z2) /\
334324 projective (pair x3 z3) /\
335325 let q := if (swap:bool) then (pair x3 z3) else (pair x2 z2) in
336326 let q' := if (swap:bool) then (pair x2 z2) else (pair x3 z3) in
337- let r := (n >> Z.succ i)%Z in
327+ let r := ((n mod 2^scalarbits) >> Z.succ i)%Z in
338328 eq q (to_xz (scalarmult r P)) /\
339329 eq q' (to_xz (scalarmult (Z.succ r) P)) /\
340- ladder_invariant point (scalarmult r P) (scalarmult (Z.succ r) P))
330+ ladder_invariant (X0 P) (scalarmult r P) (scalarmult (Z.succ r) P))
341331 (fun s => Z.to_nat (Z.succ (snd s))) (* decreasing measure *) ).
342332 { split; cbn.
343333 { (* invariant holds in the beginning *)
344- rewrite ?Z.succ_pred, ?Z.lt_pow_2_shiftr, <-?Z.one_succ by tauto .
345- repeat split; [lia|t..]. }
334+ rewrite ?Z.succ_pred, ?Z.lt_pow_2_shiftr, <-?Z.one_succ by (apply Z.mod_pos_bound; lia) .
335+ repeat split; [lia|lia| t..]. }
346336 { (* sufficient fuel *) rewrite Z.succ_pred. reflexivity. } }
347337 { intros [ [ [ [ [x2 z2] x3] z3] swap] i] [Hi [Hx2z2 [Hx3z3 [Hq [Hq' Hladder]]]]].
348338 destruct (i >=? 0)%Z eqn:Hbranch; (* did the loop continue? *)
349339 rewrite Z.geb_ge_iff in Hbranch.
350340 split.
351341 { (* if loop continued, invariant is preserved *)
342+ remember (Z.testbit n i) as bit eqn:Hbit; symmetry in Hbit.
343+ erewrite <-(Z.mod_pow2_bits_low _ scalarbits) in Hbit by tauto.
344+ set (n mod 2 ^ scalarbits)%Z as n' in *.
352345 let group _ := ltac:(repeat rewrite ?scalarmult_add_l, ?scalarmult_0_l, ?scalarmult_1_l, ?Hierarchy.left_identity, ?Hierarchy.right_identity, ?Hierarchy.associative, ?(Hierarchy.commutative _ P); reflexivity) in
353- destruct (Z.testbit n i) eqn:Hbit in *;
346+ destruct bit in *;
354347 destruct swap eqn:Hswap in *;
355348 repeat match goal with
356349 | _ => solve [ congruence | assumption | lia ]
@@ -367,8 +360,8 @@ Module M.
367360 => let pf := constr:(to_xz_add p xz x'z' _ _ H G HQ HQ' ltac:(auto using ladder_invariant_swap)) in
368361 unique pose proof (proj1 pf); destruct (proj2 pf) as [? [? [? ?]]] (* because there is no unique destruct *)
369362 | _ => progress rewrite ?Z.succ_pred, ?Z.shiftr_succ, <-?Z.div2_spec, <-?Z.add_1_r in *
370- | |- context [scalarmult (n>>i) ] => rewrite (Z_shiftr_testbit_1 n i), Hbit; cbn [Z.b2z]
371- | |- context [scalarmult (n>>i+1) ] => rewrite (Z_shiftr_testbit_1 n i), Hbit; cbn [Z.b2z]
363+ | |- context [scalarmult (n' >>i) ] => rewrite (Z_shiftr_testbit_1 n' i), Hbit; cbn [Z.b2z]
364+ | |- context [scalarmult (n' >>i+1) ] => rewrite (Z_shiftr_testbit_1 n' i), Hbit; cbn [Z.b2z]
372365 | |- ?P => match type of P with Prop => split end
373366 | H: eq (?f _) (to_xz ?LHS) |- eq (?f _) (to_xz ?RHS)
374367 => eapply (transitive_eq (to_xz LHS) ltac:(auto using projective_to_xz) H); f_equiv; group ()
@@ -381,71 +374,41 @@ Module M.
381374 { (* measure decreases *)
382375 cbv [Let_In]; break_match; cbn; rewrite Z.succ_pred; apply Znat.Z2Nat.inj_lt; lia. }
383376 { (* if loop exited, invariant implies postcondition *)
384- destruct_head' @and; autorewrite with cancel_pair in *.
385377 replace i with ((-(1))%Z) in * by lia; clear Hi Hbranch.
386378 rewrite Z.succ_m1, Z.shiftr_0_r in *.
387379 cbv [M.cswap];
388380 destruct swap eqn:Hswap; rewrite <-!to_x_inv00 by assumption;
381+ etransitivity; try eapply to_x_to_xz; f_equal;
389382 eauto using projective_to_xz, proper_to_x_projective. } }
390383 Qed .
391384
392385 (* Using montladder_correct_0 in the combined correctness theorem requires
393386 additionally showing that the right-hand-side is 0. This comes from there
394387 being two points such that to_x gives 0: infinity and (0, 0). *)
395388
396- Lemma opp_to_x_to_xz_0
397- (P : M.point)
398- (H : 0 = to_x (to_xz P))
399- : 0 = to_x (to_xz (Mopp P)).
389+ Lemma X0_opp_0 (P : M.point) (H : X0 P = 0) : X0 (Mopp P) = 0.
400390 Proof . t. Qed .
401391
402- Lemma add_to_x_to_xz_0
403- (P Q : M.point)
404- (HP : 0 = to_x (to_xz P))
405- (HQ : 0 = to_x (to_xz Q))
406- : 0 = to_x (to_xz (Madd P Q)).
407- Proof . t. Qed .
392+ Lemma X0_add_0 (P Q : M.point) (HP : X0 P = 0) (HQ : X0 Q = 0) : X0(Madd P Q) = 0.
393+ Proof . cbv [X0] in *; t. Qed .
408394
409- Lemma scalarmult_to_x_to_xz_0
410- (n : Z) (P : M.point)
411- (H : 0 = to_x (to_xz P))
412- : 0 = to_x (to_xz (scalarmult n P)).
395+ Lemma X0_scalarmult_0 (n : Z) (P : M.point) (H : X0 P = 0) : X0 (scalarmult n P) = 0.
413396 Proof .
414- induction n using Z.peano_rect_strong.
415- { cbn. t. }
416- { (* Induction case from n to Z.succ n. *)
417- unfold scalarmult_ref.
418- rewrite Z.peano_rect_succ by lia.
419- fold (scalarmult n P).
420- apply add_to_x_to_xz_0; trivial. }
421- { (* Induction case from n to Z.pred n. *)
422- unfold scalarmult_ref.
423- rewrite Z.peano_rect_pred by lia.
424- fold (scalarmult n P).
425- apply add_to_x_to_xz_0.
426- { apply opp_to_x_to_xz_0; trivial. }
427- { trivial. } }
397+ clear dependent scalarbits.
398+ induction n using Z.peano_rect_strong; try t.
399+ { unfold scalarmult_ref. rewrite Z.peano_rect_succ by lia. fold (scalarmult n P).
400+ auto using X0_add_0. }
401+ { unfold scalarmult_ref. rewrite Z.peano_rect_pred by lia. fold (scalarmult n P).
402+ auto using X0_add_0, X0_opp_0. }
428403 Qed .
429404
430405 (* Combine the two cases together. *)
431406
432- Lemma montladder_correct
433- (HFinv : Finv 0 = 0)
434- (n : Z) (P : M.point)
435- (scalarbits : Z) (point : F)
436- (Hn : (0 <= n < 2^scalarbits)%Z)
437- (Hscalarbits : (0 <= scalarbits)%Z)
438- (Hpoint : point = to_x (to_xz P))
439- : montladder scalarbits (Z.testbit n) point = to_x (to_xz (scalarmult n P)).
407+ Lemma montladder_correct n P :
408+ montladder scalarbits (Z.testbit n) (X0 P) = X0 (scalarmult (n mod 2^scalarbits) P).
440409 Proof .
441- destruct (dec (point = 0)) as [Hz|Hnz].
442- { rewrite (montladder_correct_0 HFinv _ _ _ Hz Hn Hscalarbits).
443- setoid_subst_rel Feq.
444- apply scalarmult_to_x_to_xz_0.
445- trivial. }
446- { apply (montladder_correct_nz HFinv _ _ _ _ Hnz Hn Hscalarbits).
447- trivial. }
410+ destruct (dec (X0 P = 0)) as [Hz|?]; auto using montladder_correct_nz .
411+ rewrite montladder_correct_0, X0_scalarmult_0 by trivial; reflexivity.
448412 Qed .
449-
450413 End MontgomeryCurve.
451414End M.
0 commit comments