improve specification of carry to match code

proofs/spec/Low/Car25519.v

@@ -228,24 +228,19 @@ Proof.
   change (0 + z0) with z0 => Eq.
   repeat (destruct l0; tryfalse).
   move: Eq ; rewrite ?ListSame => Eq ; jauto_set ; try reflexivity.
-(*   clear H H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 H13 H14 H15 H16 H18. *)
-  unfold nth.
-  - subst z30.
-    rewrite getCarry16_256.
+  all:   clear H H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 H13 H14 H15 H16 H18.
+  all: unfold nth; subst z30.
+  - rewrite getCarry16_256.
     assert(getCarry 256 (ℤ16.lst [z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12; z13; z14; z15]) = 0).
     apply getCarry_impl_0 ; omega.
+    rewrite H.
     omega.
-  - unfold getResidue.
-  erewrite (getCarry_16_eq_256 z0 z1 z2 z3 z4 z5 z6 z7 z8 z9 z10 z11 z12 z13 z14 z15).
-  2: rewrite ?Carry_n_step2 Carry_n_step_02 ; change (0 + z0) with z0; rewrite ?ListSame ; jauto_set ; try assumption.
-    assert(getCarry 256 (ℤ16.lst [z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12; z13; z14; z15]) = 0).
-    apply getCarry_impl_0 ; omega.
-  clear H19 H18 H17 H16 H15 H14 H13 H13 H12 H11 H10 H9 H8 H7 H6 H5 H4 H3 H2 H.
-    simpl nth.
-    assert(getCarry 256 (ℤ16.lst [z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12; z13; z14; z15]) = 0).
-    apply getCarry_impl_0 ; omega.
-  rewrite H.
-  change (0 ≪ 16) with 0. omega.
+  - rewrite getCarry16_240.
+    remember (ℤ16.lst [z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12; z13; z14; z15]) as M.
+    rewrite /getCarry Z.shiftr_div_pow2 => //.
+    assert(0 ≤ M `div` 2 ^ 240) by apply Z_div_pos => //=.
+    assert(M `div` 2^240 < 2^16) by apply Zdiv_lt_upper_bound => //=.
+    rewrite getResidue_mod_eq /getResidue_mod //= Z.mod_small //.
 Qed.
 
 Lemma BackCarry_fix_Zlength: forall l, Zlength l = 16 -> 0 <= ℤ16.lst l < 2^256 -> car25519 l = Carrying_n 16 15 0 l.

proofs/spec/Low/Carry_n.v

@@ -113,7 +113,7 @@ Proof.
     | [ |- -2^62 < getCarry _ _ ∧ _ < _ ] => apply getCarry_bound_str63
   end.
 Qed.
-(* THIS QED IS REALLY SLOW... should be improved by reflection ... *)
+(* THIS QED IS REALLY SLOW... could be improved by reflection ... *)
 
 Lemma Carry_n_length_False: forall (h:Z) (q:list Z), Carrying_n 16 15 0 (h :: q) = [] -> False.
 Proof. intros ; rewrite Carry_n_step in H ; false. Qed.

proofs/spec/Mid/Reduce.v

@@ -58,7 +58,8 @@ Qed.
 
 Definition getCarry (m:Z) : Z :=  Z.shiftr m n.
 
-Definition getResidue (m:Z) : Z := m - Z.shiftl (getCarry m) n.
+Definition getResidue (m:Z) : Z := Z.land (Z.ones n) m.
+(*  - Z.shiftl (getCarry m) n. *)
 
 Definition getResidue_mod (m:Z) : Z := m mod 2^n.
 
@@ -68,14 +69,8 @@ Proof.
   symmetry.
   unfold getResidue.
   unfold getResidue_mod.
-  unfold getCarry.
-  orewrite Z.shiftr_div_pow2.
-  orewrite Z.shiftl_mul_pow2.
-  apply Zplus_minus_eq.
-  rewrite Z.mul_comm.
-  apply Z_div_mod_eq.
-  apply pown0.
-  assumption.
+  rewrite Z.land_comm Z.land_ones //=.
+  omega.
 Qed.
 
 Lemma getResidue_0 : getResidue 0 = 0.
@@ -97,12 +92,11 @@ Qed.
 Lemma residuteCarry: forall m:Z, getResidue m + 2^n *getCarry m = m.
 Proof.
   intro m.
-  unfold getResidue.
+  rewrite getResidue_mod_eq.
+  unfold getResidue_mod.
   unfold getCarry.
   orewrite Z.shiftr_div_pow2.
-  orewrite Z.shiftl_mul_pow2.
-  rewrite Z.mul_comm.
-  omega.
+  apply mod_div => //.
 Qed.
 
 Lemma getCarryMonotone_pos: forall m,

proofs/spec/Mid/ZCarry.v

@@ -326,15 +326,10 @@ Lemma secondIterCar:
 Proof.
   assert(0 < 2^256 ) by reflexivity.
   assert(2 ^ 256 - 38 + 2 ^ 256 < 2 ^ 257) by Psatz.nia.
-  repeat match goal with
-    | _ => progress intros
-    | _ => progress unfold Mid.car25519
-    | _ => progress unfold getResidue
-    | _ => progress unfold getCarry
-    | _ => progress orewrite Z.shiftl_mul_pow2
-    | _ => progress orewrite Z.shiftr_div_pow2
-    | [  |- context[?x/2^256] ] => progress orewrite (eq_1_div256 x)
-  end.
+  intros.
+  rewrite /Mid.car25519 getResidue_mod_eq //.
+  rewrite /getResidue_mod Zmod_eq /getCarry //.
+  rewrite Z.shiftr_div_pow2 // (eq_1_div256 x) ; omega.
 Qed.
 
 Lemma doubleCar_str_case:

proofs/vst/proofs/verif_car25519_compute.v

@@ -56,15 +56,9 @@ Proof.
   eapply Zcarry_n_bounds_length ; go.
   intros ; simpl in H ; solve_bounds_by_values.
   }
-  rewrite /sem_and.
-  rewrite /tint.
-  rewrite /sem_binarith.
-  rewrite /classify_binarith.
+  rewrite /sem_and /tint /sem_binarith /classify_binarith.
   simpl sem_cast.
-  rewrite /sem_cast_i2l.
-  rewrite /sem_cast_l2l.
-  rewrite /both_long.
-  rewrite /force_val.
+  rewrite /sem_cast_i2l /sem_cast_l2l /both_long /force_val.
   rewrite /cast_int_long.
   rewrite and64_repr.
   rewrite upd_Znth_map.
@@ -74,9 +68,7 @@ Proof.
   rewrite Int.signed_repr.
   2: solve_bounds_by_values.
   change 65535 with (Z.ones 16).
-  rewrite Z.land_ones.
-  rewrite /sem_and.
-  2: omega.
+  rewrite Z.land_comm.
   repeat orewrite upd_Znth_upd_nth.
   repeat orewrite Znth_nth.
   unfold nat_of_Z.
@@ -87,16 +79,14 @@ Proof.
   rewrite Zlength_correct in Hlengthcontents_o.
   assert(Ho' : (length contents_o = 16)%nat) by go.
   repeat (destruct contents_o ; tryfalse).
-  rewrite Zmod_eq_full.
 
   repeat match goal with
       | [H : _ \/ _ |- _ ] => destruct H ; subst
       | _ => idtac
-    end; Grind_add_Z; change_Z_to_nat ; repeat rewrite Carry_n_step ; repeat rewrite Carry_n_step_0 ; unfold upd_nth ; unfold nth;
-  unfold getResidue;
-  unfold getCarry ; 
-  repeat orewrite Int64.Zshiftl_mul_two_p ; repeat orewrite Int64.Zshiftr_div_two_p; change_Z_to_nat ; simpl ; try reflexivity.
-  compute; intro ; omega.
+    end; Grind_add_Z; repeat change_Z_to_nat ; repeat rewrite Carry_n_step ; repeat rewrite Carry_n_step_0 ; unfold upd_nth ; unfold nth;
+  unfold getResidue ;
+  unfold getCarry ;
+  repeat orewrite Int64.Zshiftl_mul_two_p ; repeat orewrite Int64.Zshiftr_div_two_p ; reflexivity.
 Qed.
 
 Lemma car25519low_level: forall o, Forall (fun x : ℤ => - 2 ^ 62 < x < 2 ^ 62) o ->
@@ -144,16 +134,9 @@ Proof.
   rewrite upd_Znth_map.
   rewrite (Znth_map Int64.zero).
   2: rewrite upd_Znth_Zlength Zlength_map ; omega.
-  rewrite /sem_and.
-  rewrite /tint.
-  rewrite /sem_binarith.
-  rewrite /classify_binarith.
+  rewrite /sem_and /tint /sem_binarith /classify_binarith.
   simpl sem_cast.
-  rewrite /sem_cast_i2l.
-  rewrite /sem_cast_l2l.
-  rewrite /both_long.
-  rewrite /force_val.
-  rewrite /cast_int_long.
+  rewrite /sem_cast_i2l /sem_cast_l2l /both_long /force_val /cast_int_long.
   rewrite upd_Znth_map.
   rewrite upd_Znth_map.
   rewrite (Znth_map 0).
@@ -188,12 +171,8 @@ Proof.
   unfold getResidue;
   unfold getCarry.
   change 65535 with (Z.ones 16).
-  rewrite Z.land_ones; [|omega].
-  orewrite Int64.Zshiftl_mul_two_p;
-  orewrite Int64.Zshiftr_div_two_p.
-  rewrite -Zmod_eq_full.
-  2: compute ; intro; discriminate.
-  fequals.
+  rewrite Z.land_comm.
+  orewrite Int64.Zshiftr_div_two_p => //.
 Qed.
 
 Close Scope Z.
\ No newline at end of file

proofs/vst/proofs/verif_unpack25519.v

 Set Warnings "-notation-overridden,-parsing".
 Require Import Tweetnacl.Low.Unpack25519.
-Require Import Tweetnacl.Mid.ScalarMult.
 Require Import Tweetnacl_verif.init_tweetnacl.
 Require Import Tweetnacl_verif.spec_unpack25519.