Commit 5c754263 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

define real RFC in coq

parent 5ad9b788
......@@ -16,37 +16,54 @@ Open Scope Z.
Local Notation "X + Y" := (A X Y) (only parsing).
Local Notation "X - Y" := (Zub X Y) (only parsing).
Local Notation "X * Y" := (M X Y) (only parsing).
Local Notation "X ^2" := (Sq X) (at level 40, only parsing, left associativity).
Local Notation "X ^2" := (Sq X) (at level 40,
only parsing, left associativity).
Fixpoint montgomery_rec (m : nat) (z : T') (a b c d e f x : T) : (T * T * T * T * T * T) :=
match m with
| 0%nat => (a,b,c,d,e,f)
| S n =>
let r := Getbit (Z.of_nat n) z in
let (a, b) := (Sel25519 r a b, Sel25519 r b a) in
let (c, d) := (Sel25519 r c d, Sel25519 r d c) in
let e := a + c in
let a := a - c in
let c := b + d in
let b := b - d in
let d := e ^2 in
let f := a ^2 in
let a := c * a in
let c := b * e in
let e := a + c in
let a := a - c in
let b := a ^2 in
let c := d - f in
let a := c * C_121665 in
let a := a + d in
let c := c * a in
let a := d * f in
let d := b * x in
let b := e ^2 in
let (a, b) := (Sel25519 r a b, Sel25519 r b a) in
let (c, d) := (Sel25519 r c d, Sel25519 r d c) in
montgomery_rec n z a b c d e f x
end.
Fixpoint montgomery_rec (m : nat) (z : T')
(a: T) (b: T) (c: T) (d: T) (e: T) (f: T) (x: T) :
(* a: x2 *)
(* b: x3 *)
(* c: z2 *)
(* d: z3 *)
(* e: temporary var *)
(* f: temporary var *)
(* x: x1 *)
(T * T * T * T * T * T) :=
match m with
| 0%nat => (a,b,c,d,e,f)
| S n =>
let r := Getbit (Z.of_nat n) z in
(* k_t = (k >> t) & 1 *)
(* swap <- k_t *)
let (a, b) := (Sel25519 r a b, Sel25519 r b a) in
(* (x_2, x_3) = cswap(swap, x_2, x_3) *)
let (c, d) := (Sel25519 r c d, Sel25519 r d c) in
(* (z_2, z_3) = cswap(swap, z_2, z_3) *)
let e := a + c in (* A = x_2 + z_2 *)
let a := a - c in (* B = x_2 - z_2 *)
let c := b + d in (* C = x_3 + z_3 *)
let b := b - d in (* D = x_3 - z_3 *)
let d := e ^2 in (* AA = A^2 *)
let f := a ^2 in (* BB = B^2 *)
let a := c * a in (* CB = C * B *)
let c := b * e in (* DA = D * A *)
let e := a + c in (* x_3 = (DA + CB)^2 *)
let a := a - c in (* z_3 = x_1 * (DA - CB)^2 *)
let b := a ^2 in (* z_3 = x_1 * (DA - CB)^2 *)
let c := d - f in (* E = AA - BB *)
let a := c * C_121665 in
(* z_2 = E * (AA + a24 * E) *)
let a := a + d in (* z_2 = E * (AA + a24 * E) *)
let c := c * a in (* z_2 = E * (AA + a24 * E) *)
let a := d * f in (* x_2 = AA * BB *)
let d := b * x in (* z_3 = x_1 * (DA - CB)^2 *)
let b := e ^2 in (* x_3 = (DA + CB)^2 *)
let (a, b) := (Sel25519 r a b, Sel25519 r b a) in
(* (x_2, x_3) = cswap(swap, x_2, x_3) *)
let (c, d) := (Sel25519 r c d, Sel25519 r d c) in
(* (z_2, z_3) = cswap(swap, z_2, z_3) *)
montgomery_rec n z a b c d e f x
end.
Close Scope Z.
......
......@@ -111,15 +111,15 @@ Proof.
Qed.
(* this is a truncation, meaning we do not have the garantee that y = 0 *)
Definition cFp_to_Fp2 p := match p with
Definition cFp2_to_Fp p := match p with
| Zmodp2.Zmodp2 x y => x
end.
Lemma cFp_to_Fp2_cancel : forall p: mc curve25519_Fp_mcuType,
p#x0 = cFp_to_Fp2 ((curve25519_Fp_to_Fp2 p)#x0).
Lemma cFp2_to_Fp_cancel : forall p: mc curve25519_Fp_mcuType,
p#x0 = cFp2_to_Fp ((curve25519_Fp_to_Fp2 p)#x0).
Proof. by case ; case. Qed.
Local Notation "p '/p'" := (cFp_to_Fp2 p) (at level 40).
Local Notation "p '/p'" := (cFp2_to_Fp p) (at level 40).
From mathcomp Require Import ssrnat.
......@@ -130,12 +130,12 @@ Theorem curve25519_ladder_Fp_Fp2 (n : nat) x :
curve25519_Fp_ladder n x = ((curve25519_Fp_to_Fp2 p) *+ n)#x0 /p.
Proof.
move => Hn p Hp.
have Hp' := cFp_to_Fp2_cancel p.
have Hp' := cFp2_to_Fp_cancel p.
have Hp'' : p #x0 = x.
move: Hp'; rewrite Hp => //=.
rewrite (curve25519_Fp_ladder_ok n x Hn p Hp'').
rewrite -nP_is_nP2.
rewrite cFp_to_Fp2_cancel //.
rewrite cFp2_to_Fp_cancel //.
Qed.
Close Scope ring_scope.
\ No newline at end of file
......@@ -69,17 +69,17 @@ Proof.
- apply ontwist25519_Fp.
Qed.
Definition Fp_to_Fp2 p := match p with
Definition Fp2_to_Fp p := match p with
| Zmodp2.Zmodp2 x y => x
end.
Lemma Fp_to_Fp2_eq_C: Fp_to_Fp2 = cFp_to_Fp2.
Lemma Fp2_to_Fp_eq_C: Fp2_to_Fp = cFp2_to_Fp.
Proof. reflexivity. Qed.
Lemma Fp_to_Fp2_eq_T: Fp_to_Fp2 = tFp_to_Fp2.
Lemma Fp2_to_Fp_eq_T: Fp2_to_Fp = tFp2_to_Fp.
Proof. reflexivity. Qed.
Local Notation "p '/p'" := (Fp_to_Fp2 p) (at level 40).
Local Notation "p '/p'" := (Fp2_to_Fp p) (at level 40).
......@@ -107,7 +107,7 @@ move: Hxy.
done.
Qed.
Lemma Fp2_to_Fp :
Lemma Fp2_to_Fp_eq :
forall (x: Zmodp.type) (p : mc curve25519_Fp2_mcuType),
p #x0 = Zmodp2.Zmodp2 x 0 ->
(exists c:mc curve25519_Fp_mcuType, curve25519_Fp_to_Fp2 c = p) \/ (exists t:mc twist25519_Fp_mcuType, twist25519_Fp_to_Fp2 t = p).
......@@ -142,12 +142,12 @@ Lemma curve25519_Fp2_ladder_ok (n : nat) (x:Zmodp.type) :
curve25519_Fp_ladder n x = (p *+ n)#x0 /p.
Proof.
move => Hn p Hp.
have [[c] Hc|[t] Ht] := Fp2_to_Fp x p Hp.
have [[c] Hc|[t] Ht] := Fp2_to_Fp_eq x p Hp.
+ have Hcx0: curve25519_Fp_to_Fp2 c #x0 = Zmodp2.Zmodp2 x 0 by rewrite Hc.
rewrite (curve25519_ladder_Fp_Fp2 n x Hn c Hcx0) -Fp_to_Fp2_eq_C Hc //.
rewrite (curve25519_ladder_Fp_Fp2 n x Hn c Hcx0) -Fp2_to_Fp_eq_C Hc //.
+ have Htx0: twist25519_Fp_to_Fp2 t #x0 = Zmodp2.Zmodp2 x 0 by rewrite Ht.
rewrite curve25519_twist25519_Fp_eq.
rewrite (twist25519_ladder_Fp_Fp2 n x Hn t Htx0) -Fp_to_Fp2_eq_T Ht //.
rewrite (twist25519_ladder_Fp_Fp2 n x Hn t Htx0) -Fp2_to_Fp_eq_T Ht //.
Qed.
Close Scope ring_scope.
\ No newline at end of file
......@@ -110,15 +110,15 @@ Proof.
by rewrite ?GRing.mulrS -IHn twist25519_add_Fp_to_Fp2.
Qed.
Definition tFp_to_Fp2 p := match p with
Definition tFp2_to_Fp p := match p with
| Zmodp2.Zmodp2 x y => x
end.
Lemma tFp_to_Fp2_cancel : forall (p: mc twist25519_Fp_mcuType),
p#x0 = tFp_to_Fp2 ((twist25519_Fp_to_Fp2 p)#x0).
Lemma tFp2_to_Fp_cancel : forall (p: mc twist25519_Fp_mcuType),
p#x0 = tFp2_to_Fp ((twist25519_Fp_to_Fp2 p)#x0).
Proof. by case; case. Qed.
Local Notation "p '/p'" := (tFp_to_Fp2 p) (at level 40).
Local Notation "p '/p'" := (tFp2_to_Fp p) (at level 40).
From mathcomp Require Import ssrnat.
......@@ -129,12 +129,12 @@ Theorem twist25519_ladder_Fp_Fp2 (n : nat) x :
twist25519_Fp_ladder n x = ((twist25519_Fp_to_Fp2 p) *+ n)#x0 /p.
Proof.
move => Hn p Hp.
have Hp' := tFp_to_Fp2_cancel p.
have Hp' := tFp2_to_Fp_cancel p.
have Hp'' : p #x0 = x.
rewrite Hp' Hp //.
rewrite (twist25519_Fp_ladder_ok n x Hn p Hp'').
rewrite -nP_is_nP2.
rewrite tFp_to_Fp2_cancel //.
rewrite tFp2_to_Fp_cancel //.
Qed.
Close Scope ring_scope.
\ No newline at end of file
......@@ -216,6 +216,39 @@ rewrite /montgomery_fn clamp_ZofList_eq ?Unpack25519_eq_ZUnpack25519 => // ; try
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.
Lemma Crypto_Scalarmult_Zlength : forall (n p:list Z),
Zlength n = 32 ->
Zlength p = 32 ->
Forall (λ x : , 0 x x < 2 ^ 8) n ->
Forall (λ x : , 0 x x < 2 ^ 8) p ->
Zlength (Crypto_Scalarmult n p) = 32.
Proof.
move => n p Hln Hlp HBn HBp.
rewrite -Crypto_Scalarmult_eq.
rewrite /Crypto_Scalarmult_proof.
rewrite Pack25519_Zlength //.
apply M_Zlength.
apply Zlength_a ; assumption.
apply Inv25519_Zlength ; apply Zlength_c ; assumption.
Qed.
Lemma Crypto_Scalarmult_Bound : forall (n p:list Z),
Zlength n = 32 ->
Zlength p = 32 ->
Forall (λ x : , 0 x x < 2 ^ 8) n ->
Forall (λ x : , 0 x x < 2 ^ 8) p ->
Forall (λ x : , 0 x x < 2 ^ 8) (Crypto_Scalarmult n p).
Proof.
move => n p Hln Hlp HBn HBp.
rewrite -Crypto_Scalarmult_eq.
rewrite /Crypto_Scalarmult_proof.
apply Pack25519_bound.
apply M_Zlength.
apply Zlength_a ; assumption.
apply Inv25519_Zlength ; apply Zlength_c ; assumption.
apply M_bounded ; assumption.
Qed.
Theorem Crypto_Scalarmult_Eq : forall (n p:list Z),
Zlength n = 32 ->
Zlength p = 32 ->
......@@ -268,17 +301,8 @@ Proof.
move => n p Hn Hp Hbn Hbp.
rewrite -Crypto_Scalarmult_Eq => //.
rewrite ListofZ32_ZofList_Zlength => //.
all: rewrite -Crypto_Scalarmult_eq.
all: rewrite /Crypto_Scalarmult_proof.
2: rewrite /Pack25519.
2: apply Pack.pack_for_Zlength_32_16.
2: apply Reduce_by_P.get_t_subst_select_Zlength => //=.
2: do 3 apply car25519_Zlength.
apply Pack25519_bound.
2: apply M_bounded ; assumption.
all: apply M_Zlength.
1,3: apply Zlength_a ; assumption.
all: apply Inv25519_Zlength ; apply Zlength_c ; assumption.
apply Crypto_Scalarmult_Bound => //.
apply Crypto_Scalarmult_Zlength => //.
Qed.
Close Scope Z.
\ No newline at end of file
Local Set Warnings "-notation-overridden".
From Tweetnacl.Libs Require Import Export.
From Tweetnacl.ListsOp Require Import Export.
From mathcomp Require Import ssreflect eqtype ssralg ssrnat ssrbool.
......@@ -49,7 +50,7 @@ Open Scope ring_scope.
Import GRing.Theory.
Local Notation "p '#x0'" := (point_x0 p) (at level 30).
Local Notation "p '/p'" := (Fp_to_Fp2 p) (at level 40).
Local Notation "p '/p'" := (Fp2_to_Fp p) (at level 40).
Local Lemma expn_pown : forall n x, Nat.pow x n = expn x n.
Proof.
......
......@@ -77,4 +77,15 @@ Proof.
apply car25519_bound ; assumption.
Qed.
Lemma Pack25519_Zlength : forall (l:list Z),
Zlength l = 16 ->
Zlength (Pack25519 l) = 32.
Proof.
move => l Hl.
rewrite /Pack25519.
apply Pack.pack_for_Zlength_32_16.
apply Reduce_by_P.get_t_subst_select_Zlength => //=.
do 3 apply car25519_Zlength => //.
Qed.
Close Scope Z.
......@@ -124,4 +124,10 @@ repeat rewrite Z.lor_0_r.
reflexivity.
Qed.
Close Scope Z.
\ No newline at end of file
Lemma clamp_ZofList_eq_Zlength : forall l,
Zlength l = 32 ->
Forall (λ x : , 0 x x < 2 ^ 8) l ->
Zclamp (ZofList 8 l) = ZofList 8 (clamp l).
Proof. convert_length_to_Zlength clamp_ZofList_eq. Qed.
Local Close Scope Z.
\ No newline at end of file
......@@ -242,4 +242,10 @@ Proof.
reflexivity.
Qed.
Lemma Unpack25519_eq_ZUnpack25519_Zlength : forall l,
Zlength l = 32 ->
Forall (λ x : , 0 x x < 2 ^ 8) l ->
ZUnpack25519 (ZofList 8 l) = ZofList 16 (Unpack25519 l).
Proof. convert_length_to_Zlength Unpack25519_eq_ZUnpack25519. Qed.
Close Scope Z.
......@@ -35,9 +35,21 @@ Definition ZCrypto_Scalarmult_rev_gen n p :=
End ZCrypto_Scalarmult_gen.
(* instantiate montgomery_rec with Z_Ops *)
Definition ZCrypto_Scalarmult 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))).
let t := montgomery_rec
255 (* iterate 255 times *)
(Zclamp n) (* clamped n *)
1 (* x_2 *)
(ZUnpack25519 p) (* x_3 *)
0 (* z_2 *)
1 (* z_3 *)
0 (* dummy *)
0 (* dummy *)
(ZUnpack25519 p) (* x_1 *) in
let a := get_a t in
let c := get_c t in
ZPack25519 (Z.mul a (ZInv25519 c)).
(* This is the equivalence between ladders defined as fn with type class and ladders defined as recursive *)
Theorem ZCrypto_Scalarmult_eq : forall (n p : Z),
......
Local Set Warnings "-notation-overridden".
From mathcomp Require Import ssreflect eqtype ssralg ssrnat ssrbool.
From Tweetnacl Require Import Libs.Export.
From Tweetnacl Require Import ListsOp.Export.
From Tweetnacl Require Import Gen.Get_abcdef.
From Tweetnacl Require Import Gen.montgomery_rec.
From Tweetnacl Require Import Low.Prep_n.
From Tweetnacl Require Import Low.Unpack25519.
From Tweetnacl Require Import Mid.Pack25519.
From Tweetnacl Require Import Mid.Inv25519.
From Tweetnacl Require Import Mid.Unpack25519.
From Tweetnacl Require Import Mid.Prep_n.
From Tweetnacl Require Import Instances.
From Tweetnacl Require Import Mid.Crypto_Scalarmult.
From Tweetnacl Require Import Low.Crypto_Scalarmult.
From Tweetnacl Require Import Low.Crypto_Scalarmult_.
From Tweetnacl.High Require Import Zmodp.
From Tweetnacl.High Require Import Zmodp2.
From Tweetnacl.High Require Import curve25519_Fp2.
From Tweetnacl.High Require Import curve25519_twist25519_Fp_incl_Fp2.
(* From Tweetnacl.High Require Import prime_and_legendre. *)
From Tweetnacl.High Require Import montgomery.
From Tweetnacl.High Require Import mc.
From Tweetnacl.High Require Import mcgroup.
Local Open Scope Z.
Definition decodeScalar25519 (l: list Z) : Z :=
ZofList 8 (clamp l).
Definition decodeUCoordinate (l: list Z) : Z :=
ZofList 16 (Unpack25519 l).
Definition encodeUCoordinate (x: Z) : list Z :=
ListofZ32 8 x.
Definition RFC (n: list Z) (p: list Z) : list Z :=
let k := decodeScalar25519 n in
let u := decodeUCoordinate p in
let t := montgomery_rec
255 (* iterate 255 times *)
k (* clamped n *)
1 (* x_2 *)
u (* x_3 *)
0 (* z_2 *)
1 (* z_3 *)
0 (* dummy *)
0 (* dummy *)
u (* x_1 *) in
let a := get_a t in
let c := get_c t in
let o := ZPack25519 (Z.mul a (ZInv25519 c))
in encodeUCoordinate o.
Lemma Crypto_Scalarmult_RFC_eq : forall n p,
Zlength n = 32 ->
Zlength p = 32 ->
Forall (fun x => 0 <= x /\ x < 2 ^ 8) n ->
Forall (fun x => 0 <= x /\ x < 2 ^ 8) p ->
Crypto_Scalarmult n p = RFC n p.
Proof.
move => n p Hln Hlp Hbn Hbp.
rewrite /RFC /encodeUCoordinate /decodeUCoordinate /decodeScalar25519.
rewrite Crypto_Scalarmult_Eq2 ; try assumption.
apply f_equal.
rewrite /ZCrypto_Scalarmult.
rewrite Unpack25519_eq_ZUnpack25519_Zlength.
rewrite clamp_ZofList_eq_Zlength.
reflexivity.
all: assumption.
Qed.
(* Local Close Scope Z. *)
Open Scope ring_scope.
Import GRing.Theory.
Local Notation "p '#x0'" := (point_x0 p) (at level 30).
Local Notation "'Fp2_x' P" := (Zmodp2.Zmodp2 (Zmodp.pi P) 0) (at level 30).
Local Notation "P '_x0'" := (val (Fp2_to_Fp (P #x0))) (at level 30).
Theorem RFC_Correct: forall (n p : list Z) (P:mc curve25519_Fp2_mcuType),
Zlength n = 32 ->
Zlength p = 32 ->
Forall (fun x => 0 <= x /\ x < 2 ^ 8) n ->
Forall (fun x => 0 <= x /\ x < 2 ^ 8) p ->
Fp2_x (decodeUCoordinate p) = P#x0 ->
RFC n p = encodeUCoordinate ((P *+ (Z.to_nat (decodeScalar25519 n))) _x0).
Proof.
move => n p P Hln Hlp HBn HBp.
rewrite /encodeUCoordinate /decodeUCoordinate /decodeScalar25519.
rewrite -Unpack25519_eq_ZUnpack25519_Zlength => //.
rewrite -clamp_ZofList_eq_Zlength => //.
move => HP.
rewrite -(Crypto_Scalarmult_Correct n p P) => //.
rewrite -Crypto_Scalarmult_RFC_eq => //.
rewrite ListofZ32_ZofList_Zlength => //.
apply Crypto_Scalarmult_Bound => //.
apply Crypto_Scalarmult_Zlength => //.
Qed.
Close Scope ring_scope.
Local Close Scope Z.
......@@ -77,6 +77,7 @@ Require Import Tweetnacl.Low.ScalarMult_gen_small.
Require Import Tweetnacl.Low.ScalarMult_rev.
Require Import Tweetnacl.Mid.Instances.
Require Import Tweetnacl.Gen.ABCDEF.
Require Import Tweetnacl.rfc.rfc.
Open Scope Z.
......@@ -910,9 +911,10 @@ replace (force_val
thaw F.
replace (Pack25519 (Low.M aa ccc)) with (Crypto_Scalarmult n p).
deadvars!.
rewrite Crypto_Scalarmult_RFC_eq ; try assumption.
unfold POSTCONDITION.
unfold abbreviate.
remember (Crypto_Scalarmult n p) as sc.
remember (RFC n p) as sc.
eapply (semax_return_Some _ _ _ _ _ (stackframe_of f_crypto_scalarmult_curve25519_tweet)
[Tsh [{v_a}]<<( lg16 )-- undef16; Tsh [{v_c}]<<( lg16 )-- undef16;
Tsh [{v_z}]<<( uch32 )-- undef32; Tsh [{v_b}]<<( lg16 )-- undef16; Tsh [{v_d}]<<( lg16 )-- undef16;
......@@ -954,6 +956,7 @@ Tsh [{v_e}]<<( lg16 )-- undef16; Tsh [{v_f}]<<( lg16 )-- undef16; Tsh [{v_x}]<<(
2: cancel. (* Q |-- Q *)
2: subst aa ccc m cc a b c d x z.
subst sc.
rewrite -Crypto_Scalarmult_RFC_eq ; try assumption.
all: rewrite -Crypto_Scalarmult_eq.
2: reflexivity.
split ; [|split]; rewrite /Crypto_Scalarmult_proof.
......
......@@ -67,9 +67,10 @@ Require Import Tweetnacl_verif.verif_crypto_scalarmult_lemmas.
Require Import Tweetnacl.Low.Get_abcdef.
Require Import Tweetnacl.Low.ScalarMult_rev.
Require Import Tweetnacl.Low.Constant.
Require Import Tweetnacl.Low.Crypto_Scalarmult.
Require Import Tweetnacl.Low.Crypto_Scalarmult_.
(* Require Import Tweetnacl.Low.Crypto_Scalarmult. *)
(* Require Import Tweetnacl.Low.Crypto_Scalarmult_. *)
Require Import Tweetnacl.Mid.Instances.
Require Import Tweetnacl.rfc.rfc.
Open Scope Z.
Import Low.
......@@ -97,10 +98,10 @@ Definition crypto_scalarmult_spec :=
Ews [{ c121665 }] <<(lg16)-- mVI64 C_121665)
POST [ tint ]
PROP (
Forall (fun x => 0 <= x < Z.pow 2 8) (Crypto_Scalarmult n p);
Zlength (Crypto_Scalarmult n p) = 32)
Forall (fun x => 0 <= x < Z.pow 2 8) (RFC n p);
Zlength (RFC n p) = 32)
LOCAL(temp ret_temp (Vint Int.zero))
SEP (sh [{ v_q }] <<(uch32)-- mVI (Crypto_Scalarmult n p);
SEP (sh [{ v_q }] <<(uch32)-- mVI (RFC n p);
sh [{ v_n }] <<(uch32)-- mVI n;
sh [{ v_p }] <<(uch32)-- mVI p;
Ews [{ c121665 }] <<(lg16)-- mVI64 C_121665
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment