Commit 075c3539 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

better proof of M

parent 5f0b8548
--- tweetnacl.c 2019-07-31 14:05:27.916394829 +0200
+++ tweetnaclVerifiableC.c 2019-12-28 16:31:25.596762941 +0100
+++ tweetnaclVerifiableC.c 2020-01-15 17:54:36.240162283 +0100
@@ -5,7 +5,7 @@
typedef unsigned char u8;
typedef unsigned long u32;
typedef unsigned long long u64;
@@ We tell VST that long long
@@ are aligned on 8 bytes.
-typedef long long i64;
+typedef long long i64 __attribute__((aligned(8)));
typedef i64 gf[16];
extern void randombytes(u8 *,u64);
@@ -273,18 +273,16 @@
@@ We remove the undefined behavior and
@@ simplify the carry propagation.
sv car25519(gf o)
{
int i;
......@@ -28,11 +24,9 @@
}
}
@@ b is a mask of 64 bits.
-sv sel25519(gf p,gf q,int b)
+sv sel25519(gf p,gf q,i64 b)
{
@@ For-loop indexes have to be int.
- i64 t,i,c=~(b-1);
+ int i;
+ i64 t,c=~(b-1);
......@@ -43,9 +37,6 @@
sv pack25519(u8 *o,const gf n)
{
@@ For-loop indexes have to be int.
@@ b is a 64 bit mask.
@@ Initialize m to simplify verification.
- int i,j,b;
- gf m,t;
- FOR(i,16) t[i]=n[i];
......@@ -62,8 +53,6 @@
m[15]=t[15]-0x7fff-((m[14]>>16)&1);
- b=(m[15]>>16)&1;
m[14]&=0xffff;
@@ Computations in arguments
@@ are not allowed in VST.
- sel25519(t,m,1-b);
+ b=1-((m[15]>>16)&1);
+ sel25519(t,m,b);
......@@ -74,50 +63,39 @@
{
u8 d[32];
pack25519(d,a);
@@ Force the casting.
- return d[0]&1;
+ return d[0]&(u8)1;
}
sv unpack25519(gf o, const u8 *n)
@@ -353,10 +352,14 @@
@@ -353,10 +352,11 @@
sv M(gf o,const gf a,const gf b)
{
@@ For-loop indexes have to be int.
@@ introduce an auxiliary variable to
@@ simplify verification (loop invariants).
- i64 i,j,t[31];
- FOR(i,31) t[i]=0;
- FOR(i,16) FOR(j,16) t[i+j]+=a[i]*b[j];
- FOR(i,15) t[i]+=38*t[i+16];
+ int i,j;
+ i64 t[31], aux;
+ i64 t[31];
+ FOR(i,31) t[i]= 0;
+ FOR(i,16) {
+ aux = a[i];
+ FOR(j,16) t[i+j]+=aux*b[j];
+ }
FOR(i,16) FOR(j,16) t[i+j]+=a[i]*b[j];
- FOR(i,15) t[i]+=38*t[i+16];
+ FOR(i,15) t[i]+=(i64)38*t[i+16];
FOR(i,16) o[i]=t[i];
car25519(o);
car25519(o);
@@ -371,7 +374,7 @@
@@ -371,7 +371,7 @@
{
gf c;
int a;
- FOR(a,16) c[a]=i[a];
@@ gain 5 bytes.
+ set25519(c,i);
for(a=253;a>=0;a--) {
S(c,c);
if(a!=2&&a!=4) M(c,c,i);
@@ -394,8 +397,9 @@
@@ -394,8 +394,9 @@
int crypto_scalarmult(u8 *q,const u8 *n,const u8 *p)
{
u8 z[32];
@@ x only needs gf.
@@ For-loop indexes have to be int.
- i64 x[80],r,i;
- gf a,b,c,d,e,f;
+ i64 r;
......@@ -126,11 +104,10 @@
FOR(i,31) z[i]=n[i];
z[31]=(n[31]&127)|64;
z[0]&=248;
@@ -430,15 +434,9 @@
@@ -430,15 +431,9 @@
sel25519(a,b,r);
sel25519(c,d,r);
}
@@ simplify
- FOR(i,16) {
- x[i+16]=a[i];
- x[i+32]=c[i];
......
......@@ -353,12 +353,9 @@ sv Z(gf o,const gf a,const gf b)
sv M(gf o,const gf a,const gf b)
{
int i,j;
i64 t[31], aux;
i64 t[31];
FOR(i,31) t[i]= 0;
FOR(i,16) {
aux = a[i];
FOR(j,16) t[i+j]+=aux*b[j];
}
FOR(i,16) FOR(j,16) t[i+j]+=a[i]*b[j];
FOR(i,15) t[i]+=(i64)38*t[i+16];
FOR(i,16) o[i]=t[i];
car25519(o);
......
......@@ -45,16 +45,19 @@ thaw_local.
by (intros ; erewrite (Znth_map Int64.zero); [eexists; reflexivity|rewrite Zlength_map outer_M_fix_Zlength] ; omega).
assert(Haux2: forall j, 0 <= j < 16 -> exists aux2, Vlong aux2 = Znth j (map Vlong (map Int64.repr b)) Vundef)
by (intros; erewrite (Znth_map Int64.zero); [eexists; reflexivity | rewrite Zlength_map]; omega).
rewrite /nm_overlap_array_sep_3 ; flatten; Intros.
all: destruct Haux1 as [aux1 Haux1].
1: subst o v_o.
2: subst o v_o.
3: subst b v_b.
4: subst o a v_o v_a.
all: forward ; rewrite -Haux1.
(* all: forward ; rewrite -Haux1.
1,3,5,7,9: entailer!.
Ltac solve_first_loop_last i := rewrite /nm_overlap_array_sep_3 /nm_overlap_array_sep_3'; repeat match goal with
*)
Ltac solve_first_loop_last i := rewrite /nm_overlap_array_sep_3 /nm_overlap_array_sep_3'; repeat match goal with
| [ H : (_ =? _ ) = true |- _ ] => rewrite H
| [ H : (_ =? _ ) = false |- _ ] => rewrite H
end;
......@@ -62,15 +65,15 @@ thaw_local.
destruct ( i + 1 <=? 0) eqn:Heq0; try apply Zle_bool_imp_le in Heq0 ; try omega;
replace (i + 1 - 1) with i by omega;
rewrite inner_M_fix_equation; entailer!.
1: forward_for_simple_bound 16 (M1_inner_Inv sho sha shb v_a v_a v_b v_t i (Vlong aux1) (mVI64 a) a b t 0);
1: forward_for_simple_bound 16 (M1_inner_Inv sho sha shb v_a v_a v_b v_t i (mVI64 a) a b t 0);
[unfold nm_overlap_array_sep_3 ; entailer! | | solve_first_loop_last i].
2: forward_for_simple_bound 16 (M1_inner_Inv sho sha shb v_b v_a v_b v_t i (Vlong aux1) (mVI64 b) a b t 1);
2: forward_for_simple_bound 16 (M1_inner_Inv sho sha shb v_b v_a v_b v_t i (mVI64 b) a b t 1);
[unfold nm_overlap_array_sep_3 ; entailer! | | solve_first_loop_last i].
3: forward_for_simple_bound 16 (M1_inner_Inv sho sha shb v_o v_a v_a v_t i (Vlong aux1) o a a t 2);
3: forward_for_simple_bound 16 (M1_inner_Inv sho sha shb v_o v_a v_a v_t i o a a t 2);
[unfold nm_overlap_array_sep_3 ; entailer! | | solve_first_loop_last i].
4: forward_for_simple_bound 16 (M1_inner_Inv sho sha shb v_b v_b v_b v_t i (Vlong aux1) (mVI64 b) b b t 3);
4: forward_for_simple_bound 16 (M1_inner_Inv sho sha shb v_b v_b v_b v_t i (mVI64 b) b b t 3);
[unfold nm_overlap_array_sep_3 ; entailer! | | solve_first_loop_last i].
5: forward_for_simple_bound 16 (M1_inner_Inv sho sha shb v_o v_a v_b v_t i (Vlong aux1) o a b t 4);
5: forward_for_simple_bound 16 (M1_inner_Inv sho sha shb v_o v_a v_b v_t i o a b t 4);
[unfold nm_overlap_array_sep_3 ; entailer! | | solve_first_loop_last i].
all: rewrite /nm_overlap_array_sep_3 ; simpl; Intros.
all: rename i0 into j ; rename H6 into Hj.
......@@ -78,6 +81,8 @@ thaw_local.
all: destruct (Haux2 j Hj) as [aux2 HHaux2].
all: forward ; rewrite -HHaux.
1,3,5,7,9: entailer!.
all: forward ; rewrite -Haux1.
1,3,5,7,9: entailer!.
all: forward ; rewrite -HHaux2.
1,3,5,7,9: entailer!.
all: forward ; entailer!.
......
......@@ -40,87 +40,30 @@ Definition M_Tinit_Inv F L t :=
Definition M1_outer_Inv sho sha shb L v_o v_a v_b v_t o a b t k :=
EX i : Z,
PROP (
(* Forall (fun x => -Z.pow 2 26 < x < Z.pow 2 26) contents_a;
Forall (fun x => -Z.pow 2 26 < x < Z.pow 2 26) contents_b;
Zlength contents_a = 16;
Zlength contents_b = 16;
Zlength contents_o = 16;
Zlength contents_t = 31; *)
(* i >= 0 *)
)
PROP ()
(LOCALx L
SEP (Tsh [{ v_t }] <<(tarray tlg 31)-- mVI64 (outer_M_fix i 0 a b t);
nm_overlap_array_sep_3 sho sha shb o a b v_o v_a v_b k)).
Definition M1_inner_Inv sho sha shb v_o v_a v_b v_t i aux1 o a b t k :=
Definition M1_inner_Inv sho sha shb v_o v_a v_b v_t i o a b t k :=
EX j : Z,
PROP (
(* writable_share sho; writable_share sha; writable_share shb;
Forall (fun x => -Z.pow 2 26 < x < Z.pow 2 26) contents_a;
Forall (fun x => -Z.pow 2 26 < x < Z.pow 2 26) contents_b;
Zlength contents_a = 16;
Zlength contents_b = 16;
Zlength contents_o = 16;
Zlength contents_t = 31; *)
(* j >= 0 *)
)
LOCAL (temp _i (Vint (Int.repr i)); temp _aux aux1; lvar _t (tarray tlg 31) v_t;
PROP ()
LOCAL (temp _i (Vint (Int.repr i)); lvar _t (tarray tlg 31) v_t;
temp _a v_a; temp _b v_b; temp _o v_o)
SEP (
Tsh [{ v_t }] <<(tarray tlg 31)-- mVI64 (outer_M_fix i j a b t);
nm_overlap_array_sep_3 sho sha shb o a b v_o v_a v_b k).
(* Definition M2_Inv sho sha shb o a b t contents_o contents_a contents_b contents_t k :=
EX i : Z,
PROP (
(* writable_share sho; writable_share sha; writable_share shb;
Forall (fun x => -Z.pow 2 26 < x < Z.pow 2 26) contents_a;
Forall (fun x => -Z.pow 2 26 < x < Z.pow 2 26) contents_b;
Zlength contents_a = 16;
Zlength contents_b = 16;
Zlength contents_o = 16;
Zlength contents_t = 31;
i >= 0
*)
)
LOCAL (lvar _t (tarray tlg 31) t; temp _a a; temp _b b; temp _o o)
SEP (
Tsh [{ t }] <<(tarray tlg 31)-- mVI64 (M2_fix i contents_t);
nm_overlap_array_sep_3s sho sha shb contents_o contents_a contents_b o a b). *)
Definition M2_Inv F L v_t t :=
EX i : Z,
PROP (
(* writable_share sho; writable_share sha; writable_share shb;
Forall (fun x => -Z.pow 2 26 < x < Z.pow 2 26) contents_a;
Forall (fun x => -Z.pow 2 26 < x < Z.pow 2 26) contents_b;
Zlength contents_a = 16;
Zlength contents_b = 16;
Zlength contents_o = 16;
Zlength contents_t = 31;
i >= 0
*)
)
PROP ()
(LOCALx L
SEP (FRZL F ;
(* LOCAL (lvar _t (tarray tlg 31) t; temp _a a; temp _b b; temp _o o)
SEP (F
*)
Tsh [{ v_t }] <<(tarray tlg 31)-- mVI64 (M2_fix i t))).
SEP (FRZL F ; Tsh [{ v_t }] <<(tarray tlg 31)-- mVI64 (M2_fix i t))).
Definition M3_Inv sho sha shb o a b t contents_o contents_a contents_b contents_t k :=
EX i : Z,
PROP (
(* writable_share sho; writable_share sha; writable_share shb; *)
(* Forall (fun x => -Z.pow 2 26 < x < Z.pow 2 26) contents_a; *)
(* Forall (fun x => -Z.pow 2 26 < x < Z.pow 2 26) contents_b; *)
(* Zlength contents_a = 16; *)
(* Zlength contents_b = 16; *)
(* Zlength contents_o = 16; *)
(* Zlength contents_t = 31; *)
(* i >= 0 *)
)
PROP ()
LOCAL (lvar _t (tarray tlg 31) t; temp _a a; temp _b b; temp _o o)
SEP (
Tsh [{ t }] <<(tarray tlg 31)-- mVI64 contents_t;
......
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