Add constant time spec for point addition

Author: miriampolzer

src/Bedrock/P256.v

@@ -148,6 +148,7 @@ Proof.
   pose_correctness p256_point_add_nz_nz_neq_ok.
 
   pose_correctness p256_point_add_vartime_if_doubling_ok.
+  pose_correctness p256_point_add_constant_time_ok.
 
   pose_correctness p256_point_add_affine_nz_nz_neq_ok.
   pose_correctness p256_point_add_affinenz_conditional_vartime_if_doubling_ok.

src/Bedrock/P256/Jacobian.v

@@ -41,7 +41,6 @@ Local Open Scope list_scope.
 
 Import (notations) coqutil.Map.Memory.
 
-
 Import Coq.micromega.Lia.
 Import coqutil.Tactics.Tactics.
 
@@ -305,8 +304,6 @@ rewrite ?app_length, ?length_coord in *.
     trivial. }
 Qed.
 
-Import coqutil.Tactics.Tactics.
-
 Definition p256_point_add_vartime_if_doubling := func!(p_out, p_P, p_Q) {
   unpack! zeroP = p256_point_iszero(p_P);
   unpack! zeroQ = p256_point_iszero(p_Q);
@@ -322,66 +319,72 @@ Definition p256_point_add_vartime_if_doubling := func!(p_out, p_P, p_Q) {
   br_memcpy(p_out, p_sel, $(3*32))
 }.
 
+#[local] Ltac ensure_map m := lazymatch type of m with | @Interface.map.rep _ _ _ => true | _ => false end.
+#[local] Ltac newest_memory_hyp := match goal with | H: ?G ?m |- _ =>
+match (ensure_map m) with true => H | false => fail end end.
+
 Import memcpy.
-Lemma p256_point_add_vartime_if_doubling_ok : program_logic_goal_for_function! p256_point_add_vartime_if_doubling.
+Lemma p256_point_add_vartime_if_doubling_ok :
+  let spec := spec_of_p256_point_add_vartime_if_doubling in
+  program_logic_goal_for_function! p256_point_add_vartime_if_doubling.
 Proof.
   cbv [spec_of_p256_point_add_vartime_if_doubling].
   repeat straightline.
+  pose proof (length_point P) as HlengthP. pose proof (length_point Q) as HlengthQ.
   straightline_call; repeat straightline. (*iszero*)
-  { letexists. ecancel_assumption. }
+  { eexists. ecancel_assumption. }
   straightline_call; repeat straightline. (*iszero*)
-  { letexists. ecancel_assumption. }
+  { eexists. ecancel_assumption. }
   (* stackalloc *)
-  seprewrite_in_by (@Array.array1_iff_eq_of_list_word_at) H9 ltac:(lia).
+  seprewrite_in_by (@Array.array1_iff_eq_of_list_word_at) ltac:(newest_memory_hyp) ltac:(lia).
   straightline_call; ssplit. (*add*)
   { ecancel_assumption. }
-  { rewrite length_point; lia. }
+  { lia. }
   repeat straightline.
   straightline_call; repeat straightline (* br_declassify *).
   (* stackalloc *)
-  seprewrite_in_by (@Array.array1_iff_eq_of_list_word_at) H17 ltac:(lia).
+  seprewrite_in_by (@Array.array1_iff_eq_of_list_word_at) ltac:(newest_memory_hyp) ltac:(lia).
   straightline_call; ssplit. (* memset *)
   { ecancel_assumption. }
-  { ZnWords.ZnWords. }
+  { ZnWords. }
   repeat straightline.
   straightline_call; repeat straightline; ssplit (* memcxor *).
   { ecancel_assumption. }
   { rewrite ?repeat_length; trivial. }
-  { rewrite H18, length_point; trivial. }
+  { ZnWords. }
   straightline_call; repeat straightline; ssplit (* memcxor *).
   { ecancel_assumption. }
   { rewrite ?repeat_length; trivial. }
-  { rewrite length_point; trivial. }
+  { ZnWords. }
   straightline_call; repeat straightline; ssplit (* memcxor *).
   { ecancel_assumption. }
   { rewrite ?repeat_length; trivial. }
-  { rewrite length_point; trivial. }
-
+  { ZnWords. }
   subst x x0 x3.
-  letexists; ssplit; repeat straightline; subst v (* if ok *).
+  eexists; ssplit; repeat straightline. (* if ok *)
   { straightline_call; repeat straightline; ssplit (* memcpy *).
     { ecancel_assumption. }
-    { rewrite H10, length_point; trivial. }
+    { ZnWords. }
     { trivial. }
-    { clear; ZnWords.ZnWords. }
+    { clear; ZnWords. }
     repeat straightline.
     (* stackdealloc *)
-    progress repeat seprewrite_in_by (symmetry! @Array.array1_iff_eq_of_list_word_at) H42 ltac:(rewrite ?length_point in *; lia || ZnWords.ZnWords).
-    progress repeat match type of H42 with context [Array.array ptsto _ _ (point.to_bytes ?x)] =>
-    unique pose proof (length_point x) end.
+    progress repeat seprewrite_in_by (symmetry! @Array.array1_iff_eq_of_list_word_at) ltac:(newest_memory_hyp)
+        ltac:(rewrite ?length_point in *; lia || ZnWords).
     assert (Datatypes.length x6 = 96%nat) by ZnWords.ZnWords.
     repeat straightline.
-    progress repeat seprewrite_in_by (@Array.array1_iff_eq_of_list_word_at) H42 ltac:(rewrite ?length_point in *; lia || ZnWords.ZnWords).
-
-    rewrite <-word.unsigned_of_Z_0, !word.unsigned_inj_iff in H27 by exact _.
-    rewrite !word.lor_0_iff, !word.broadcast_0_iff in H27.
+    progress repeat seprewrite_in_by (@Array.array1_iff_eq_of_list_word_at)
+        ltac:(newest_memory_hyp) ltac:(lia || ZnWords.ZnWords).
+    let Hzero := match goal with H: _ <> 0 |- _ => H end in
+      rewrite <-word.unsigned_of_Z_0, !word.unsigned_inj_iff in Hzero by exact _;
+      rewrite !word.lor_0_iff, !word.broadcast_0_iff in Hzero.
     destruct (iszero P) eqn:HP, (iszero Q) eqn:HQ in *; try intuition discriminate;
       repeat match goal with
              | H : _ = _ -> _ |- _ => specialize (H eq_refl)
              | H : ?x = ?y -> _ |- _ => assert (x = y -> False) as _ by inversion 1; clear H
              end;
       subst x4; subst x5; subst x6;
-      rewrite ?Byte.map_xor_0_l in * by (rewrite ?length_point; ZnWords.ZnWords).
+      rewrite ?Byte.map_xor_0_l in * by (ZnWords).
     { (* 0 + 0 *)
       eexists (exist _ (0,0,0)%F I); split.
       { use_sep_assumption; cancel. reflexivity. }
@@ -393,7 +396,6 @@ Proof.
       eexists; split. { ecancel_assumption. }
       apply Decidable.dec_bool, Jacobian.iszero_iff in HP.
       rewrite Jacobian.eq_iff, Jacobian.to_affine_add, HP.
-Import Curves.Weierstrass.AffineProofs.
       symmetry.
       eapply Hierarchy.left_identity. }
     { (* P + 0 *)
@@ -406,7 +408,8 @@ Import Curves.Weierstrass.AffineProofs.
       rewrite <-Bool.not_true_iff_false in HP, HQ.
       (* Decidable.dec_iff? *)
       cbv [iszero] in HP, HQ; case Decidable.dec in HP; case Decidable.dec in HQ; try congruence.
-      destruct (H19 ltac:(trivial) ltac:(trivial)) as [HE|]; [|intuition fail].
+      match goal with H : ~ Jacobian.iszero ?P -> _ |- _ =>
+        destruct (H ltac:(trivial) ltac:(trivial)) as [HE|]; [|intuition fail] end.
       case HE as [_ (?&HE)].
       repeat straightline_cleanup.
       eexists; split; [ecancel_assumption|].
@@ -428,7 +431,7 @@ Import Curves.Weierstrass.AffineProofs.
     straightline_call; repeat straightline.
     { split. { ecancel_assumption. }
       rewrite ?map_length, ?combine_length, ?repeat_length.
-      rewrite H18, length_point. clear; ZnWords.ZnWords. }
+      rewrite H18, length_point. clear; reflexivity. }
 
     straightline_call; repeat straightline; ssplit (* memcpy *).
     { ecancel_assumption. }
@@ -437,18 +440,34 @@ Import Curves.Weierstrass.AffineProofs.
     { clear; ZnWords.ZnWords. }
     repeat straightline.
     (* stackdealloc *)
-    progress repeat seprewrite_in_by (symmetry! @Array.array1_iff_eq_of_list_word_at) H31 ltac:(rewrite ?length_point in *; lia || ZnWords.ZnWords).
+    progress repeat seprewrite_in_by (symmetry! @Array.array1_iff_eq_of_list_word_at)
+        ltac:(newest_memory_hyp) ltac:(rewrite ?length_point in *; lia || ZnWords.ZnWords).
     progress repeat match type of H31 with context [Array.array ptsto _ _ (point.to_bytes ?x)] =>
     unique pose proof (length_point x) end.
     repeat straightline.
-    progress repeat seprewrite_in_by (@Array.array1_iff_eq_of_list_word_at) H31 ltac:(rewrite ?length_point in *; lia || ZnWords.ZnWords).
+    progress repeat seprewrite_in_by (@Array.array1_iff_eq_of_list_word_at)
+        ltac:(newest_memory_hyp) ltac:(rewrite ?length_point in *; lia || ZnWords.ZnWords).
 
     eexists; ssplit. { ecancel_assumption. }
     rewrite <-HE, <-Jacobian.double_minus_3_eq_double.
     rewrite Jacobian.eq_iff, Jacobian.to_affine_double, Jacobian.to_affine_add.
     reflexivity. }
 Qed.
 
+Lemma p256_point_add_constant_time_ok :
+  let spec := spec_of_p256_point_add_constant_time in
+  program_logic_goal_for_function! p256_point_add_vartime_if_doubling.
+Proof.
+  unfold spec_of_p256_point_add_constant_time.
+  pose proof p256_point_add_vartime_if_doubling_ok as Hvartime.
+  unfold spec_of_p256_point_add_vartime_if_doubling in Hvartime.
+  cbv [program_logic_goal_for] in *.
+  do 21 intros ?. intros (?, (?, ?)).
+  eapply Semantics.weaken_call.
+  { eapply Hvartime; try trivial. split; eassumption. }
+  cbv [id]. intros. assumption.
+Qed.
+
 Definition p256_point_double := func!(out, in1) {
   stackalloc 32 as D;
   stackalloc 32 as A;

src/Bedrock/P256/PrecomputedMultiples.v

@@ -58,12 +58,11 @@ Definition p256_precompute_multiples := func! (p_table, p_P) {
   i = $2;
   while ($17 - i) {
     if (i & $1) {
-      unpack! ok = p256_point_add_nz_nz_neq(
+      p256_point_add_vartime_if_doubling(
         p_table + ($sizeof_point * i),
         p_table + ($sizeof_point * (i - $1)),
         p_P
-      );
-      $(cmd.unset "ok")
+      )
     } else {
       p256_point_double(
         p_table + ($sizeof_point * i),
@@ -142,8 +141,7 @@ Qed.
   fnspec! "p256_precompute_multiples" p_table p_P / out (P : point) R,
   { requires t m :=
       m =* out$@p_table * P$@p_P * R /\
-      length out = (sizeof_point * 17)%nat /\
-      ~ Jacobian.iszero P;
+      length out = (sizeof_point * 17)%nat;
     ensures t' m := t' = t /\ exists out,
       m =* pointarray p_table out * P$@p_P * R /\
       List.Forall2 W.eq (map to_affine out) (W.multiples 17 (to_affine P))
@@ -421,7 +419,8 @@ Proof.
   { etransitivity; [eassumption|]. repeat Morphisms.f_equiv. lia. }
 Qed.
 
-Lemma p256_precompute_multiples_ok : program_logic_goal_for_function! p256_precompute_multiples.
+Lemma p256_precompute_multiples_ok :
+  let spec := spec_of_p256_point_add_constant_time in program_logic_goal_for_function! p256_precompute_multiples.
 Proof.
   repeat straightline.
 
@@ -489,7 +488,7 @@ Proof.
     rewrite ?map.of_list_word_nil in *.
     seprewrite_in @sepclause_of_map_empty ltac:(hyp_containing m0).
     eexists; ssplit; [ecancel_assumption|].
-    eqapply H12. f_equal. ZnWords.
+    eqapply H11. f_equal. ZnWords.
   }
 
   (* Loop invariant is preserved. *)
@@ -530,38 +529,26 @@ Proof.
       eapply ListUtil.Forall2_forall_iff'; [solve_num|assumption|solve_num].
     }
 
-    (* p256_point_add_nz_nz_neq *)
+    (* Point addition in constant time. *)
     straightline_call; ssplit.
     { use_sep_assumption; cancel.
       (* Set Ltac Profiling. *)
       cancel_seps_at_indices 3%nat 0%nat; [match_up_pointers; exact eq_refl|]. (* 0.4s *)
       cancel_seps_at_indices 1%nat 0%nat; [match_up_pointers; exact eq_refl|]. (* 0.5s *)
       cbv [seps]; ecancel. }
     { solve_num. }
+    { rewrite <-(ScalarMult.scalarmult_1_l (eq:=W.eq) (to_affine P)).
+      rewrite Hvm1P. intros Hzero.
+      rewrite p256_mul_mod_n. {
+      cbv [p256_group_order]; PreOmega.Z.div_mod_to_equations. lia. }
+      { intros HPzero. apply Hzero. rewrite HPzero.
+        rewrite ScalarMult.scalarmult_zero_r, ScalarMult.scalarmult_1_l.
+        split; reflexivity. } }
 
     repeat straightline.
 
-    let h := hyp_containing @Forall2 in rename h into Hf2.
-
-    unshelve (match goal with H : ~ Jacobian.iszero ?P -> _ |- _ =>
-        repeat (let HH := fresh in assert (~ Jacobian.iszero P);
-        [shelve|specialize (H HH)]); trivial;
-        rename H into Hadd end).
-    { rewrite Jacobian.iszero_iff. rewrite Hvm1P.
-       rewrite <- (ScalarMult.scalarmult_0_l (eq:=W.eq) (Jacobian.to_affine P)), p256_mul_mod_n.
-        cbv [p256_group_order]; PreOmega.Z.div_mod_to_equations; lia. }
-
-    destruct Hadd as [(?&?&?)|[? Hadd] ]; trivial; [|contradict Hadd]; cycle 1.
-    { (* no doubling *)
-      rewrite Jacobian.eq_iff. rewrite Hvm1P.
-        rewrite <- (ScalarMult.scalarmult_1_l (eq:=W.eq) (to_affine P)) at 2.
-        rewrite p256_mul_mod_n.
-        cbv [p256_group_order]; PreOmega.Z.div_mod_to_equations; lia. }
-
-    repeat straightline.
-
-     eexists (S v); split.
-    { subst i. subst x0.
+    eexists (S v); split.
+    { subst i.
       eexists (multiples ++ [_]), (skipn sizeof_point todo); ssplit.
       { rewrite (pointlist_firstn_nth_skipn multiples (v - 1)) by solve_num.
         repeat seprewrite @array_append; repeat seprewrite @array_cons;
@@ -575,7 +562,8 @@ Proof.
         apply Forall2_app.
         { assumption. }
         repeat constructor.
-        rewrite Jacobian.to_affine_add_inequal_nz_nz by assumption.
+        let H := hyp_containing (add vm1P P) in rewrite H.
+        rewrite Jacobian.to_affine_add.
         rewrite Hvm1P.
         rewrite <- (ScalarMult.scalarmult_1_l (mul:=W.mul) (eq:=W.eq) (Jacobian.to_affine P)) at 2.
         rewrite <-ScalarMult.scalarmult_add_l.

src/Bedrock/P256/Specs.v

@@ -313,13 +313,31 @@ Context {ext_spec : Semantics.ExtSpec}.
       m =* out$@p_out * P$@p_P * R
   }%sep.
 
-#[export] Instance spec_of_p256_point_add_vartime_if_doubling : spec_of "p256_point_add_vartime_if_doubling" :=
-  fnspec! "p256_point_add_vartime_if_doubling" p_out p_P p_Q / out (P Q : point),
-  { requires t m := m =* out$@p_out * P$@p_P * Q$@p_Q /\ length out = length P;
+(* Two specs exist as Definitions for p256_point_add_vartime_if_doubling:
+     1. General: Variable-time, supports equal points.
+     2. Constant-time: Requires points equal only if both are zero.
+     Select the constant-time spec to enforce its preconditions. Note:
+     This ensures conditional safety, not a proof of constant-time execution. *)
+
+#[global] Definition spec_of_p256_point_add_vartime_if_doubling : spec_of "p256_point_add_vartime_if_doubling" :=
+  fnspec! "p256_point_add_vartime_if_doubling" p_out p_P p_Q / out (P Q : point) R,
+  { requires t m := m =* out$@p_out * P$@p_P * Q$@p_Q * R /\ length out = length P;
     ensures t' m := t' = t /\ exists out : point,
-      m =* out$@p_out * P$@p_P * Q$@p_Q /\ Jacobian.eq out (Jacobian.add P Q)
+      m =* out$@p_out * P$@p_P * Q$@p_Q * R /\ Jacobian.eq out (Jacobian.add P Q)
   }%sep.
 
+#[global] Definition spec_of_p256_point_add_constant_time : spec_of "p256_point_add_vartime_if_doubling" :=
+  fnspec! "p256_point_add_vartime_if_doubling" p_out p_P p_Q / out (P Q : point) R,
+  { requires t m :=
+      m =* out$@p_out * P$@p_P * Q$@p_Q * R /\
+      length out = length P /\
+      (~ (W.eq (Jacobian.to_affine P) W.zero /\ W.eq (Jacobian.to_affine Q) W.zero) ->
+        ~ W.eq (Jacobian.to_affine P) (Jacobian.to_affine Q));
+    ensures T M := T = t /\ exists (out : point),
+      M =* out$@p_out * P$@p_P * Q$@p_Q * R /\
+      Jacobian.eq out (Jacobian.add P Q)
+  }.
+
 #[export] Instance spec_of_p256_point_add_affine_nz_nz_neq : spec_of "p256_point_add_affine_nz_nz_neq" :=
   fnspec! "p256_point_add_affine_nz_nz_neq" p_out p_P p_Q / out (P : point) (Q : affine_point) R ~> ok,
   { requires t m := m =* out$@p_out * P$@p_P * (Jacobian.of_affine Q)$@p_Q * R /\ length out = length P;

src/Curves/Weierstrass/P256.v

@@ -79,6 +79,7 @@ Proof.
 Qed.
 
 Lemma p256_mul_mod_n (a b : Z) (P : Wpoint) :
+  ~ W.eq P W.zero ->
   W.eq (W.mul a P) (W.mul b P) <->
   a mod p256_group_order = b mod p256_group_order.
 Proof. Admitted.