merge MontgomeryEquivalence into MontgomeryLadder, use in GaragDoor (#1841)

Author: andres-erbsen

src/Bedrock/End2End/X25519/GarageDoor.v

@@ -220,7 +220,7 @@ Definition garagedoor_iteration : state -> list (lightbulb_spec.OP _) -> state -
      udp_local ++ udp_remote ++
      be2 udp_length ++ be2 0 ++
      garagedoor_header ++
-     le_split 32 (F.to_Z (x25519_gallina (le_combine sk) (F.of_Z Field.M_pos 9)))))
+     le_split 32 (F.to_Z (x25519_gallina (le_combine sk) (F.of_Z _ 9)))))
   ioh /\ SEED=seed /\ SK=sk.
 
 Local Instance spec_of_recvEthernet : spec_of "recvEthernet" := spec_of_recvEthernet.
@@ -387,7 +387,7 @@ Proof.
     subst pPPP.
     seprewrite_in_by (Array.bytearray_append cmp1) H33 SepAutoArray.listZnWords.
 
-    remember (le_split 32 (F.to_Z (x25519_gallina (le_combine sk) (Field.feval_bytes _)))) as vv.
+    set (k := (Field.feval_bytes _)); remember (le_split 32 (F.to_Z (x25519_gallina (le_combine sk) k))) as vv; subst k.
     repeat straightline.
     pose proof (List.firstn_skipn 16 vv) as Hvv.
     pose proof (@firstn_length_le _ vv 16 ltac:(subst vv; rewrite ?length_le_split; ZnWords)).
@@ -852,7 +852,7 @@ Optimize Proof. Optimize Heap.
   { rewrite ?app_length, ?length_le_split. SepAutoArray.listZnWords. }
   { ZnWords. }
 
-  pose proof length_le_split 32 (F.to_Z (x25519_gallina (le_combine sk) (F.of_Z Field.M_pos 9))) as Hpkl.
+  pose proof length_le_split 32 (F.to_Z (x25519_gallina (le_combine sk) (F.of_Z _ 9))) as Hpkl.
   seprewrite_in_by (fun xs ys=>@bytearray_address_merge _ _ _ _ _ xs ys buf) H37 SepAutoArray.listZnWords.
   seprewrite_in_by (fun xs ys=>@bytearray_address_merge _ _ _ _ _ xs ys buf) H37 SepAutoArray.listZnWords.
 

src/Bedrock/End2End/X25519/MontgomeryLadder.v

@@ -53,7 +53,9 @@ Require Import coqutil.Map.OfListWord Coq.Init.Byte coqutil.Byte.
 Import ProgramLogic.Coercions.
 Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment*).
 Local Notation "xs $@ a" := (Array.array ptsto (word.of_Z 1) a xs) (at level 10, format "xs $@ a").
-Definition x25519_gallina := montladder_gallina (Field.M_pos(FieldParameters:=field_parameters)) Field.a24 (Z.to_nat (Z.log2 (Z.pos order))).
+Definition x25519_gallina K U : F (2^255-19) := 
+  @XZ.M.montladder _ F.zero F.one F.add F.sub F.mul F.inv (F.div (F.of_Z _ 486662 - F.of_Z _ 2) (F.of_Z _ 4))
+  (Z.to_nat (Z.log2 (Z.pos order))) (Z.testbit K) U.
 Global Instance spec_of_x25519 : spec_of "x25519" :=
   fnspec! "x25519" out sk pk / (o s p : list Byte.byte) (R : _ -> Prop),
   { requires t m := m =* s$@sk * p$@pk * o$@out * R /\

src/Bedrock/End2End/X25519/MontgomeryLadderProperties.v

@@ -42,7 +42,7 @@ Definition montladder_post (pOUT pK pU : word.rep (word:=Naive.word32))
          (BW:=BW32)
          (field_representaton:=field_representation n s c)
          (Some Field.tight_bounds) pOUT
-         (montladder_gallina Field.M_pos Field.a24 (Z.to_nat (Z.log2 Curve25519.order)) K U)
+         (@XZ.M.montladder _ F.zero F.one F.add F.sub F.mul F.inv a24 (Z.log2 Curve25519.order) (Z.testbit K) U)
          ⋆ Array.array ptsto (word.of_Z 1) pK Kbytes
          ⋆ FElem (BW:=BW32)
                  (field_representaton:=field_representation n s c)

src/Bedrock/Group/ScalarMult/MontgomeryEquivalence.v

@@ -1,3 +1,5 @@
+Require Crypto.Bedrock.Group.Loops.
+Require Import Crypto.Curves.Montgomery.XZ.
 Require Import Rupicola.Lib.Api.
 Require Import Rupicola.Lib.Alloc.
 Require Import Rupicola.Lib.SepLocals.
@@ -43,7 +45,8 @@ Notation "'let/n' ( v , w , x , y , z ) := val 'in' body" :=
 
 Section Gallina.
   Local Open Scope F_scope.
-  Definition montladder_gallina (m : positive) (a24 : F m) (count : nat) (k : Z) (u : F m)
+  Context (m : positive) (a24 : F m) (count : nat).
+  Definition montladder_gallina (k : Z) (u : F m)
     : F m :=
     let/n X1 := stack 1 in
     let/n Z1 := stack 0 in
@@ -69,6 +72,62 @@ Section Gallina.
     let/n OUT := (F.inv Z1) in
     let/n OUT := (X1 * OUT) in
     OUT.
+
+  (*TODO: which of ladderstep_gallina and M.xzladderstep should we change? either?*)
+  Definition reorder_pairs {A B C D} (p : \<<A , B , C , D\>>) : (A*B)*(C*D) :=
+    (P2.car p, P2.car (P2.cdr p),((P2.car (P2.cdr (P2.cdr p))),(P2.cdr (P2.cdr (P2.cdr p))))).
+
+  (* TODO: should M.montladder change to accomodate this? *)
+  Definition to_pair {A B} p : A*B := (P2.car p, P2.cdr p).
+
+  Lemma invert_reorder_pairs {A B C D} (p : \<<A , B , C , D\>>) w x y z
+    : reorder_pairs p = (w,x, (y,z)) <-> p = \<w,x,y,z\>.
+  Proof.
+    destruct p as [? [? [? ?]]].
+    cbv.
+    intuition congruence.
+  Qed.
+  
+  Lemma ladderstep_gallina_equiv X1 P1 P2 :
+    reorder_pairs (ladderstep_gallina _ a24 X1 (fst P1) (snd P1) (fst P2) (snd P2)) =
+    @M.xzladderstep _ F.add F.sub F.mul a24 X1 P1 P2.
+  Proof.
+    intros. cbv [ladderstep_gallina M.xzladderstep].
+    destruct P1 as [x1 z1]. destruct P2 as [x2 z2].
+    cbv [Rewriter.Util.LetIn.Let_In nlet]. cbn [fst snd].
+    rewrite !F.pow_2_r; trivial.
+  Qed.
+
+  Lemma montladder_gallina_equiv n point :
+    montladder_gallina n point =
+    @M.montladder _ F.zero F.one F.add F.sub F.mul F.inv a24 (Z.of_nat count) (Z.testbit n) point.
+  Proof.
+    cbv [montladder_gallina M.montladder Rewriter.Util.LetIn.Let_In stack].
+    do 5 (unfold nlet at 1); cbn [fst snd P2.car P2.cdr].
+    rewrite Loops.downto_while.
+    match goal with
+    | |- ?lhs = ?rhs =>
+      match lhs with context [Loops.while ?ltest ?lbody ?fuel ?linit] =>
+      match rhs with context [Loops.while ?rtest ?rbody ?fuel ?rinit] =>
+      rewrite (Loops.while.preservation ltest lbody rtest rbody
+        (fun s1 s2 => s1 = let '(x2, z2, x3, z3, swap, i) := s2 in
+        (\<x2, z2, x3, z3, swap\>, i))) with (init2:=rinit)
+    end end end.
+    { rewrite !Nat2Z.id. destruct (Loops.while _ _ _ _) eqn:? at 1 2.
+      destruct_products. case b; reflexivity. }
+    { intros. destruct_products. congruence. }
+    { intros. destruct_products. Prod.inversion_prod. LtbToLt.Z.ltb_to_lt. subst.
+      rewrite !Z2Nat.id by lia.
+      cbv [nlet M.cswap].
+      repeat match goal with
+             | H : (_,_) = (_,_) |- _ => inversion H; subst; clear H
+             | _ => progress BreakMatch.break_match
+             | _ => progress BreakMatch.break_match_hyps
+             end;
+      rewrite <- ladderstep_gallina_equiv, invert_reorder_pairs in Heqp0;
+      cbn [fst snd to_pair] in Heqp0; inversion_clear Heqp0; trivial. }
+    { reflexivity. }
+  Qed.
 End Gallina.
 
 Section __.
@@ -101,7 +160,7 @@ Section __.
            *  R)%sep mem;
         ensures tr' mem' :=
           tr' = tr
-          /\ (let OUT := montladder_gallina M_pos a24 scalarbits K U in
+          /\ (let OUT := @M.montladder _ F.zero F.one F.add F.sub F.mul F.inv a24 (Z.of_nat scalarbits) (Z.testbit K) U in
               (FElem (Some tight_bounds) pOUT OUT * Kbytes$@pK
                * FElem (Some tight_bounds) pU U
                * R)%sep mem') }.
@@ -311,6 +370,9 @@ Section __.
            As montladder_correct.
     Proof.
       pose proof scalarbits_bound.
+      cbv [spec_of_montladder]; intros; eapply Semantics.weaken_call; cycle 1; intros.
+      { rewrite <-montladder_gallina_equiv. match goal with H : ?e t' m' rets |- _ => exact H end. }
+
       compile_setup.
       repeat compile_step.
       eapply compile_nlet_as_nlet_eq.

src/Bedrock/Group/ScalarMult/MontgomeryLadder.v

@@ -4,7 +4,6 @@ Require Import coqutil.Byte.
 Require Import Crypto.Algebra.Hierarchy.
 Require Import Crypto.Algebra.ScalarMult.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Bedrock.Group.ScalarMult.MontgomeryEquivalence.
 Require Import Crypto.Bedrock.Group.ScalarMult.MontgomeryLadder.
 Require Import Crypto.Bedrock.Specs.Field.
 Require Import Crypto.Bedrock.Specs.Group.

src/Bedrock/Group/ScalarMult/ScalarMult.v

@@ -113,7 +113,7 @@ Module M.
         ((x2, z2), (x3, z3))%core
       end.
 
-    Context {cswap:bool->F->F->F*F}.
+    Definition cswap (b : bool) (x y : F) := if b then pair y x else pair x y.
     Local Notation xor := Coq.Init.Datatypes.xorb.
     Local Open Scope core_scope.
 

src/Curves/Montgomery/XZ.v

@@ -257,7 +257,7 @@ Module M.
     Global Instance Proper_ladder_invariant : Proper (Feq ==> MontgomeryCurve.M.eq ==> MontgomeryCurve.M.eq ==> iff) ladder_invariant.
     Proof. t. Qed.
 
-    Local Notation montladder := (M.montladder(a24:=a24)(Fadd:=Fadd)(Fsub:=Fsub)(Fmul:=Fmul)(Fzero:=Fzero)(Fone:=Fone)(Finv:=Finv)(cswap:=fun b x y => if b then pair y x else pair x y)).
+    Local Notation montladder := (M.montladder(a24:=a24)(Fadd:=Fadd)(Fsub:=Fsub)(Fmul:=Fmul)(Fzero:=Fzero)(Fone:=Fone)(Finv:=Finv)).
     Local Notation scalarmult := (@ScalarMult.scalarmult_ref Mpoint Madd M.zero Mopp).
 
     Import Crypto.Util.Loops.
@@ -310,7 +310,7 @@ Module M.
         { (* measure decreases *)
           cbv [Let_In]; break_match; cbn; rewrite Z.succ_pred; apply Znat.Z2Nat.inj_lt; lia. } }
         { (* if loop exited, invariant implies postcondition *)
-          break_match; break_match_hyps; setoid_subst_rel Feq; fsatz. } }
+          cbv [M.cswap]; break_match; break_match_hyps; setoid_subst_rel Feq; fsatz. } }
     Qed.
 
     Lemma montladder_correct_nz
@@ -384,6 +384,7 @@ Module M.
           destruct_head' @and; autorewrite with cancel_pair in *.
           replace i with ((-(1))%Z) in * by lia; clear Hi Hbranch.
           rewrite Z.succ_m1, Z.shiftr_0_r in *.
+          cbv [M.cswap];
           destruct swap eqn:Hswap; rewrite <-!to_x_inv00 by assumption;
             eauto using projective_to_xz, proper_to_x_projective. } }
     Qed.