prettify Crypto_Scalarmult

proofs/spec/Low/Crypto_Scalarmult.v

@@ -30,7 +30,6 @@ From Tweetnacl.Mid Require Import Prep_n.
 From Tweetnacl.Mid Require Import GetBit.
 From Tweetnacl.Mid Require Import Crypto_Scalarmult.
 From Tweetnacl.Mid Require Import AMZubSqSel.
-From Tweetnacl.Mid Require Import ScalarMult.
 From Tweetnacl.Low Require Import Crypto_Scalarmult_lemmas.
 From Tweetnacl.Mid Require Import Mod.
 From Tweetnacl.Mid Require Import Instances.
@@ -175,7 +174,7 @@ get_a
               (Unpack25519 p))) `mod` (2 ^ 255 - 19).
 Proof.
 move => Hln Hlp Hbn Hbp HUnpack HCn HUnpackEx HlUnpackP.
-rewrite /Zmontgomery_fn /montgomery_fn.
+rewrite /montgomery_fn.
 have H255: 0 <= 255 by omega.
 rewrite Zlength_correct in Hln.
 rewrite Zlength_correct in Hlp.
@@ -213,7 +212,7 @@ f_equal ; f_equal.
 have H255: 0 <= 255 by omega.
 rewrite Zlength_correct in Hln.
 rewrite Zlength_correct in Hlp.
-rewrite /Zmontgomery_fn /montgomery_fn clamp_ZofList_eq ?Unpack25519_eq_ZUnpack25519 => // ; try omega.
+rewrite /montgomery_fn clamp_ZofList_eq ?Unpack25519_eq_ZUnpack25519 => // ; try omega.
 apply (abstract_fn_rev_eq_List_Z_c (fun x => Z.modulo x (Z.pow 2 255 - 19)) Z_Ops List_Z_Ops List_Z_Ops_Prop List_Z_Ops_Prop_Correct) => //.
 Qed.
 
@@ -222,9 +221,10 @@ Theorem Crypto_Scalarmult_Eq : forall (n p:list Z),
   Zlength p = 32 ->
   Forall (λ x : ℤ, 0 ≤ x ∧ x < 2 ^ 8) n ->
   Forall (λ x : ℤ, 0 ≤ x ∧ x < 2 ^ 8) p ->
-  ZofList 8 (Crypto_Scalarmult_proof n p) = ZCrypto_Scalarmult (ZofList 8 n) (ZofList 8 p).
+  ZofList 8 (Crypto_Scalarmult n p) = ZCrypto_Scalarmult (ZofList 8 n) (ZofList 8 p).
 Proof.
   intros n p Hln Hlp Hbn Hbp.
+  rewrite -Crypto_Scalarmult_eq.
   rewrite /Crypto_Scalarmult_proof ZCrypto_Scalarmult_eq /ZCrypto_Scalarmult_rev_gen.
   have HUnpack:= Unpack25519_bounded p Hbp.
   have HCn:= clamp_bound n Hbn.

proofs/spec/Low/Crypto_Scalarmult_.v

@@ -38,17 +38,13 @@ Lemma CSM_Eq : forall (n p:list Z),
   Zlength p = 32 ->
   Forall (fun x => 0 <= x /\ x < 2 ^ 8) n ->
   Forall (fun x => 0 <= x /\ x < 2 ^ 8) p ->
-  ZofList 8 (Crypto_Scalarmult_proof n p) = val (curve25519_Fp_ladder (Z.to_nat (Zclamp (ZofList 8 n))) (Zmodp.pi (modP (ZUnpack25519 (ZofList 8 p))))).
+  ZofList 8 (Crypto_Scalarmult n p) = val (curve25519_Fp_ladder (Z.to_nat (Zclamp (ZofList 8 n))) (Zmodp.pi (modP (ZUnpack25519 (ZofList 8 p))))).
 Proof.
 move => n p Hln Hlp HBn HBp.
 rewrite -ZCrypto_Scalarmult_curve25519_ladder.
 apply Crypto_Scalarmult_Eq => //.
 Qed.
 
-(* Theorem curve25519_ladder_ok (n : nat) x :
-  (n < 2^255)%nat -> x != 0 ->
-  forall (p : mc curve25519_mcuType), p#x0 = x -> curve25519_ladder n x = (p *+ n)#x0.
- *)
 Open Scope ring_scope.
 Import GRing.Theory.
 
@@ -90,7 +86,6 @@ Theorem Crypto_Scalarmult_Correct: forall (n p:list Z) (P:mc curve25519_Fp2_mcuT
   ZofList 8 (Crypto_Scalarmult n p) = (P *+ (Z.to_nat (Zclamp (ZofList 8 n)))) _x0.
 Proof.
   move=> n p P Hn Hp Hbn Hbp HP.
-  rewrite -Crypto_Scalarmult_eq. (* move translate pretty to proof *)
   rewrite CSM_Eq //.
   f_equal.
   apply curve25519_Fp2_ladder_ok => //.

proofs/spec/Mid/Crypto_Scalarmult.v

@@ -14,7 +14,6 @@ From Tweetnacl Require Import Mid.Unpack25519.
 From Tweetnacl Require Import Mid.Pack25519.
 From Tweetnacl Require Import Mid.Car25519.
 From Tweetnacl Require Import Mid.Inv25519.
-From Tweetnacl Require Import Mid.ScalarMult.
 From Tweetnacl Require Import Mid.Crypto_Scalarmult_Fp.
 From Tweetnacl Require Import Mid.Crypto_Scalarmult_Mod.
 
@@ -34,14 +33,10 @@ Definition ZCrypto_Scalarmult_rev_gen n p :=
   let t := abstract_fn_rev 255 254 (Zclamp n) 1 (ZUnpack25519 p) 0 1 0 0 (ZUnpack25519 p) in
   ZPack25519 (Z.mul (get_a t) (ZInv25519 (get_c t))).
 
-Definition ZCrypto_Scalarmult_rec_gen n p :=
-  let t := montgomery_rec 255 (Zclamp n) 1 (ZUnpack25519 p) 0 1 0 0 (ZUnpack25519 p) in
-  ZPack25519 (Z.mul (get_a t) (ZInv25519 (get_c t))).
-
 End ZCrypto_Scalarmult_gen.
 
 Definition ZCrypto_Scalarmult n p :=
-  let t := @Zmontgomery_rec 255 (Zclamp n) 1 (ZUnpack25519 p) 0 1 0 0 (ZUnpack25519 p) in
+  let t := montgomery_rec 255 (Zclamp n) 1 (ZUnpack25519 p) 0 1 0 0 (ZUnpack25519 p) in
   ZPack25519 (Z.mul (get_a t) (ZInv25519 (get_c t))).
 
 (* This is the equivalence between ladders defined as fn with type class and ladders defined as recursive *)
@@ -50,7 +45,6 @@ Theorem ZCrypto_Scalarmult_eq : forall (n p : Z),
 Proof.
   intros.
   rewrite /ZCrypto_Scalarmult /ZCrypto_Scalarmult_rev_gen.
-  rewrite /Zmontgomery_rec.
   replace (montgomery_rec 255 (Zclamp n) 1 (ZUnpack25519 p) 0 1 0 0 (ZUnpack25519 p)) with
   (montgomery_rec (S (Z.to_nat 254)) (Zclamp n) 1 (ZUnpack25519 p) 0 1 0 0 (ZUnpack25519 p)).
   2: change (S (Z.to_nat 254)) with 255%nat.
@@ -75,7 +69,6 @@ rewrite /ZInv25519.
 rewrite Zmult_mod.
 rewrite pow_mod.
 2: by compute.
-rewrite /Zmontgomery_rec.
 rewrite /Fp_Crypto_Scalarmult_rec_gen.
 rewrite /val /Zmodp_subType.
 rewrite -modZp /p -lock.

proofs/spec/Mid/Crypto_Scalarmult_Fp.v

@@ -14,7 +14,6 @@ From Tweetnacl Require Import Mid.Unpack25519.
 From Tweetnacl Require Import Mid.Pack25519.
 From Tweetnacl Require Import Mid.Car25519.
 From Tweetnacl Require Import Mid.Inv25519.
-From Tweetnacl Require Import Mid.ScalarMult.
 From Tweetnacl Require Import Mid.Mod.
 From Tweetnacl.Gen Require Import abstract_fn_rev_eq.
 From Tweetnacl.Gen Require Import abstract_fn_rev_abcdef.

proofs/spec/Mid/Crypto_Scalarmult_Mod.v

@@ -14,7 +14,6 @@ From Tweetnacl Require Import Mid.Unpack25519.
 From Tweetnacl Require Import Mid.Pack25519.
 From Tweetnacl Require Import Mid.Car25519.
 From Tweetnacl Require Import Mid.Inv25519.
-From Tweetnacl Require Import Mid.ScalarMult.
 From Tweetnacl Require Import Mid.Mod.
 From Tweetnacl.Gen Require Import abstract_fn_rev_eq.
 From Tweetnacl.Gen Require Import abstract_fn_rev_abcdef.

proofs/spec/Mid/GetBit.v

@@ -3,14 +3,14 @@ Require Import Tweetnacl.Libs.Export.
 Open Scope Z.
 
 Module Mid.
-Definition getbit (i:Z) (l: Z) := 
-  if (Z.ltb l 0) then
+Definition getbit (i:Z) (a: Z) := 
+  if (Z.ltb a 0) then
     0
   else
   if (Z.ltb i 0) then
-  Z.land l 1
+  Z.land a 1
   else
-  Z.land (Z.shiftr l i) 1.
+  Z.land (Z.shiftr a i) 1.
 
 End Mid.
 Close Scope Z.
\ No newline at end of file

proofs/spec/Mid/ScalarMult.v

-From Tweetnacl Require Import Libs.Export.
-From Tweetnacl Require Import Gen.Get_abcdef.
-From Tweetnacl Require Import Gen.AMZubSqSel.
-From Tweetnacl Require Import Gen.abstract_fn_rev.
-From Tweetnacl Require Import Gen.montgomery_rec.
-From Tweetnacl Require Import Mid.AMZubSqSel.
-From Tweetnacl Require Import Mid.Reduce.
-From Tweetnacl Require Import Mid.GetBit.
-From Tweetnacl Require Import Mid.Mod.
-From Tweetnacl Require Import Mid.Instances.
-
-Require Import ssreflect.
-
-Open Scope Z.
-
-(* Local Instance Z_Ops : (Ops Z Z (fun x => Z.modulo x ((Z.pow 2 255) - 19))) := {}.
-Proof.
-apply A.
-apply M.
-apply Zub.
-apply Sq.
-apply C_0.
-apply C_1.
-apply C_121665.
-apply Sel25519.
-apply Zgetbit.
-intros b p q ; rewrite /Sel25519 ; flatten.
-intros ; apply A_mod_eq.
-intros ; apply M_mod_eq.
-intros ; apply Zub_mod_eq.
-intros ; apply Sq_mod_eq.
-intros ; apply Zmod_mod.
-Defined.
- *)
-
-Definition Zmontgomery_rec := @montgomery_rec _ _ modP Z_Ops.
-Definition Zmontgomery_fn := @abstract_fn_rev _ _ modP Z_Ops.
-
-Close Scope Z.
\ No newline at end of file