Commit df05eaa1 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

better rfc

parent 2c6d59cf
Require Import ssreflect.
From Tweetnacl.Libs Require Import Export.
From Tweetnacl.Gen Require Import Get_abcdef.
From Tweetnacl.Gen Require Import AMZubSqSel.
From Tweetnacl.Gen Require Import ABCDEF.
Section Montgomery_Rec.
Context {T : Type}.
Context {T' : Type}.
Context {Mod : T -> T}.
Context {O : Ops T T' Mod}.
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).
Fixpoint montgomery_rec_swap (m : nat) (z : T')
(a: T) (b: T) (c: T) (d: T) (e: T) (f: T) (x: T) (swap:Z):
(* 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 =>
let (a, b) := (Sel25519 swap a b, Sel25519 swap b a) in
(* (x_2, x_3) = cswap(swap, x_2, x_3) *)
let (c, d) := (Sel25519 swap c d, Sel25519 swap d c) in
(* (z_2, z_3) = cswap(swap, z_2, z_3) *)
(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 swap := Z.lxor swap r in
let (a, b) := (Sel25519 swap a b, Sel25519 swap b a) in
(* (x_2, x_3) = cswap(swap, x_2, x_3) *)
let (c, d) := (Sel25519 swap c d, Sel25519 swap 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_swap n z a b c d e f x r
end.
Close Scope Z.
End Montgomery_Rec.
\ No newline at end of file
Require Import ssreflect.
From Tweetnacl.Libs Require Import Export.
From Tweetnacl.Gen Require Import Get_abcdef.
From Tweetnacl.Gen Require Import AMZubSqSel.
From Tweetnacl.Gen Require Import ABCDEF.
From Tweetnacl.Gen Require Import montgomery_rec.
From Tweetnacl.Gen Require Import montgomery_rec_swap.
Open Scope Z.
Section Montgomery_Rec_Swap_Eq.
Context {T : Type}.
Context {T' : Type}.
Context {Mod : T -> T}.
Context {O : Ops T T' Mod}.
Hypothesis Getbit_01 : forall n z, Getbit n z = 0 \/ Getbit n z = 1.
Hypothesis Sel25519_1 : forall p q, Sel25519 1 p q = q.
Hypothesis Sel25519_0 : forall p q, Sel25519 0 p q = p.
Local Lemma Zlxor_1_1 : Z.lxor 1 1 = 0.
Proof. trivial. Qed.
Opaque Z.lxor.
Ltac rewritesXorSel := rewrite ?Z.lxor_0_l ?Z.lxor_0_r ?Zlxor_1_1 ?Sel25519_1 ?Sel25519_0.
Lemma montgomery_rec_swap_01 : forall (n:nat) z a b c d e f x,
montgomery_rec_swap n z a b c d e f x 0 =
montgomery_rec_swap n z b a d c e f x 1.
Proof.
induction n as [|n IHn] => z a b c d e f x /=.
2: assert(Hgetbit := Getbit_01 (. n) z).
2: move: Hgetbit => [] ->.
all: rewritesXorSel ; reflexivity.
Qed.
Theorem montgomery_rec_swap_eq: forall n z a b c d e f x,
montgomery_rec_swap n z a b c d e f x 0 =
montgomery_rec n z a b c d e f x.
Proof.
induction n as [|n IHn] ; move=> z a b c d e f x /=.
- rewritesXorSel => //.
- assert(Hgetbit := Getbit_01 (. n) z).
move: Hgetbit => [] ->.
rewritesXorSel.
apply IHn.
rewritesXorSel.
rewrite -montgomery_rec_swap_01.
apply IHn.
Qed.
End Montgomery_Rec_Swap_Eq.
\ No newline at end of file
......@@ -6,12 +6,16 @@ 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 Gen.montgomery_rec_swap.
From Tweetnacl Require Import Gen.montgomery_rec_swap_eq.
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 Mod.
From Tweetnacl Require Import Mid.AMZubSqSel.
From Tweetnacl Require Import Instances.
From Tweetnacl Require Import Mid.Crypto_Scalarmult.
From Tweetnacl Require Import Low.Crypto_Scalarmult.
......@@ -41,7 +45,7 @@ Definition encodeUCoordinate (x: Z) : list Z :=
Definition RFC (n: list Z) (p: list Z) : list Z :=
let k := decodeScalar25519 n in
let u := decodeUCoordinate p in
let t := montgomery_rec
let t := montgomery_rec_swap
255 (* iterate 255 times *)
k (* clamped n *)
1 (* x_2 *)
......@@ -50,7 +54,8 @@ Definition RFC (n: list Z) (p: list Z) : list Z :=
1 (* z_3 *)
0 (* dummy *)
0 (* dummy *)
u (* x_1 *) in
u (* x_1 *)
0 (*initial value of swap *) in
let a := get_a t in
let c := get_c t in
let o := ZPack25519 (Z.mul a (ZInv25519 c))
......@@ -66,12 +71,20 @@ Proof.
move => n p Hln Hlp Hbn Hbp.
rewrite /RFC /encodeUCoordinate /decodeUCoordinate /decodeScalar25519.
rewrite Crypto_Scalarmult_Eq2 ; try assumption.
rewrite (@montgomery_rec_swap_eq Z Z modP Z_Ops).
apply f_equal.
rewrite /ZCrypto_Scalarmult.
rewrite Unpack25519'_Zlength.
rewrite clamp_ZofList_eq_Zlength.
reflexivity.
all: assumption.
all: try assumption.
all: clear; simpl.
- rewrite /GetBit.Mid.getbit.
move => n' z ; flatten.
+ left => //.
+ assert(Hland:= and_0_or_1 z) ; omega.
+ assert(Hland:= and_0_or_1 (Z.shiftr z n')) ; omega.
all: rewrite /Mid.Sel25519 => //=.
Qed.
Open Scope ring_scope.
......
Supports Markdown
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