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

Wip

parent 84a0d100
Require Export SumList. Require Export SumList.
Require Export ZofList. Require Export Forall_extended.
Import ListNotations. Import ListNotations.
Open Scope Z. Open Scope Z.
......
...@@ -443,6 +443,7 @@ Proof. ...@@ -443,6 +443,7 @@ Proof.
rewrite Z.shiftr_div_pow2 by omega. rewrite Z.shiftr_div_pow2 by omega.
(* SearchAbout Z.div 0.*) (* SearchAbout Z.div 0.*)
apply Zdiv_small. apply Zdiv_small.
Check Zdiv_small.
admit. admit.
admit. admit.
- change ([z16; z17; z18; z19; z20; z21; z22; z23; z24; z25; z26; z27; z28; z29; z30]) with - change ([z16; z17; z18; z19; z20; z21; z22; z23; z24; z25; z26; z27; z28; z29; z30]) with
......
...@@ -52,22 +52,33 @@ Proof. ...@@ -52,22 +52,33 @@ Proof.
unfold mult_2. unfold mult_2.
apply ZsumList_pos ; auto. apply ZsumList_pos ; auto.
apply ZscalarMult_pos ; try omega. apply ZscalarMult_pos ; try omega.
apply Forall_tail.
assumption.
Qed.
Definition mult_3 (a:list Z) : list Z := slice 16 a. Definition mult_3 (a:list Z) : list Z := slice 16 a.
Lemma mult_3_pos : forall a, ZList_pos a -> ZList_pos (mult_3 a).
Proof.
intros.
unfold mult_3.
apply Forall_slice.
assumption.
Qed.
Definition M (a b:list Z) : list Z := Definition M (a b:list Z) : list Z :=
let m1 := mult_1 a b in let m1 := mult_1 a b in
let m2 := mult_2 m1 in let m2 := mult_2 m1 in
mult_3 m2. mult_3 m2.
Lemma mult_pos: forall a b, ZList_pos a -> ZList_pos b -> ZList_pos (M a b).
Proof.
intros a b Ha Hb.
unfold M.
apply mult_3_pos.
apply mult_2_pos.
apply mult_1_pos ; assumption.
Qed.
Section Integer. Section Integer.
...@@ -171,75 +182,39 @@ destruct Hlength. ...@@ -171,75 +182,39 @@ destruct Hlength.
Qed. Qed.
Lemma Zsucc16 : Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ 0))))))))))))))) = 16. Lemma Zsucc16 : Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ 0))))))))))))))) = 16.
Proof. Proof. compute ; reflexivity. Qed.
compute ; reflexivity.
Qed.
Corollary mult_GF: forall a b, . length a = 16 -> . length b = 16 -> (16.lst M a b) :𝓖𝓕 = (16.lst a) * (16.lst b) :𝓖𝓕. Corollary mult_GF: forall a b, . length a = 16 -> . length b = 16 -> (16.lst M a b) :𝓖𝓕 = (16.lst a) * (16.lst b) :𝓖𝓕.
Proof. Proof.
intros a b Hla Hlb. intros a b Hla Hlb.
unfold M. unfold M.
rewrite reduce_slice_GF. rewrite reduce_slice_GF.
f_equal. f_equal.
rewrite mult1_correct. rewrite mult1_correct.
go. go.
rewrite <- Zlength_correct in *. rewrite <- Zlength_correct in *.
destruct a ; [inversion Hla|]. (* 0 *) do 16 (destruct a ; tryfalse).
destruct a ; [inversion Hla|]. (* 1 *) destruct a.
destruct a ; [inversion Hla|]. (* 2 *) - do 16 (destruct b ; tryfalse).
destruct a ; [inversion Hla|]. (* 3 *) destruct b.
destruct a ; [inversion Hla|]. (* 4 *) + go.
destruct a ; [inversion Hla|]. (* 5 *) + clear Hla. exfalso. (* lets get a bit of visibility *)
destruct a ; [inversion Hla|]. (* 6 *) repeat rewrite Zlength_cons in Hlb.
destruct a ; [inversion Hla|]. (* 7 *) rewrite <- Zsucc16 in Hlb ;
destruct a ; [inversion Hla|]. (* 8 *) repeat (rewrite Z.succ_inj_wd in Hlb).
destruct a ; [inversion Hla|]. (* 9 *) rewrite Zlength_correct in Hlb.
destruct a ; [inversion Hla|]. (* 10 *) rewrite <- Nat2Z.inj_succ in Hlb.
destruct a ; [inversion Hla|]. (* 11 *) rewrite <- Nat2Z.inj_0 in Hlb.
destruct a ; [inversion Hla|]. (* 12 *) rewrite Nat2Z.inj_iff in Hlb.
destruct a ; [inversion Hla|]. (* 13 *) inversion Hlb.
destruct a ; [inversion Hla|]. (* 14 *) - clear Hlb. exfalso. (* lets get a bit of visibility *)
destruct a ; [inversion Hla|]. (* 15 *) repeat rewrite Zlength_cons in Hla.
destruct a ; [inversion Hla|]. (* 16 *) rewrite <- Zsucc16 in Hla ;
- destruct b ; [inversion Hlb|]. (* 0 *) repeat (rewrite Z.succ_inj_wd in Hla).
destruct b ; [inversion Hlb|]. (* 1 *) rewrite Zlength_correct in Hla.
destruct b ; [inversion Hlb|]. (* 2 *) rewrite <- Nat2Z.inj_succ in Hla.
destruct b ; [inversion Hlb|]. (* 3 *) rewrite <- Nat2Z.inj_0 in Hla.
destruct b ; [inversion Hlb|]. (* 4 *) rewrite Nat2Z.inj_iff in Hla.
destruct b ; [inversion Hlb|]. (* 5 *) inversion Hla.
destruct b ; [inversion Hlb|]. (* 6 *)
destruct b ; [inversion Hlb|]. (* 7 *)
destruct b ; [inversion Hlb|]. (* 8 *)
destruct b ; [inversion Hlb|]. (* 9 *)
destruct b ; [inversion Hlb|]. (* 10 *)
destruct b ; [inversion Hlb|]. (* 11 *)
destruct b ; [inversion Hlb|]. (* 12 *)
destruct b ; [inversion Hlb|]. (* 13 *)
destruct b ; [inversion Hlb|]. (* 14 *)
destruct b ; [inversion Hlb|]. (* 15 *)
destruct b. (* 16 *)
+ simpl.
rewrite! Zlength_cons.
rewrite Zlength_nil.
compute. (* LOL ! Thx God ! *)
reflexivity.
+ clear Hla. exfalso. (* lets get a bit of visibility *)
rewrite! Zlength_cons in Hlb.
rewrite <- Zsucc16 in Hlb ;
repeat (rewrite Z.succ_inj_wd in Hlb).
rewrite Zlength_correct in Hlb.
rewrite <- Nat2Z.inj_succ in Hlb.
rewrite <- Nat2Z.inj_0 in Hlb.
rewrite Nat2Z.inj_iff in Hlb.
inversion Hlb.
- clear Hlb. exfalso. (* lets get a bit of visibility *)
rewrite! Zlength_cons in Hla.
rewrite <- Zsucc16 in Hla ;
repeat (rewrite Z.succ_inj_wd in Hla).
rewrite Zlength_correct in Hla.
rewrite <- Nat2Z.inj_succ in Hla.
rewrite <- Nat2Z.inj_0 in Hla.
rewrite Nat2Z.inj_iff in Hla.
inversion Hla.
Qed. Qed.
Require Export Tools. Require Export Tools.
Require Export Forall_extended.
Require Export notations. Require Export notations.
Open Scope Z. Open Scope Z.
......
...@@ -8,8 +8,8 @@ all: ...@@ -8,8 +8,8 @@ all:
${COQ} Tools.v ${COQ} Tools.v
${COQ} notations.v ${COQ} notations.v
${COQ} Forall.v ${COQ} Forall.v
${COQ} Forall_extended.v
${COQ} ZofList.v ${COQ} ZofList.v
${COQ} Forall_extended.v
${COQ} Reduce.v ${COQ} Reduce.v
${COQ} Carry.v ${COQ} Carry.v
${COQ} SumList.v ${COQ} SumList.v
......
...@@ -337,12 +337,18 @@ static void car25519(gf o) ...@@ -337,12 +337,18 @@ static void car25519(gf o)
{ {
int i; int i;
i64 c; i64 c;
for (i = 0;i < 16;++i) { for (i = 0;i < 15;++i) {
o[i]+=(1LL<<16); // o[i]+=(1LL<<16);
c=o[i]>>16; c=o[i]>>16;
o[(i+1)*(i<15)]+=c-1+37*(c-1)*(i==15); // o[(i+1)*(i<15)]+=c-1+37*(c-1)*(i==15);
// o[i+1]+=c-1;
o[i+1]+=c;
o[i]-=c<<16; o[i]-=c<<16;
} }
o[15]+=(1LL<<16);
// c=o[15]>>16;
o[0]+=38*(c);
o[15]-=c<<16;
} }
static void sel25519(gf p,gf q,int b) static void sel25519(gf p,gf q,int b)
...@@ -360,7 +366,9 @@ static void pack25519(u8 *o,const gf n) ...@@ -360,7 +366,9 @@ static void pack25519(u8 *o,const gf n)
int i,j,b; int i,j,b;
gf m,t; gf m,t;
for (i = 0;i < 16;++i) t[i]=n[i]; for (i = 0;i < 16;++i) t[i]=n[i];
// forall i, -2^16 <= t[i] < 2^302
car25519(t); car25519(t);
// forall i, 0 <= t[i] < 2^16
car25519(t); car25519(t);
car25519(t); car25519(t);
for (j = 0;j < 2;++j) { for (j = 0;j < 2;++j) {
...@@ -473,7 +481,9 @@ int crypto_scalarmult_curve25519_tweet(u8 *q,const u8 *n,const u8 *p) ...@@ -473,7 +481,9 @@ int crypto_scalarmult_curve25519_tweet(u8 *q,const u8 *n,const u8 *p)
sel25519(a,b,r); sel25519(a,b,r);
sel25519(c,d,r); sel25519(c,d,r);
A(e,a,c); A(e,a,c);
// e < 2^17
Z(a,a,c); Z(a,a,c);
// a < 2^17
A(c,b,d); A(c,b,d);
Z(b,b,d); Z(b,b,d);
S(d,e); S(d,e);
......
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