remove swapping a and i in inversion

paper/tweetnacl.diff

 8c8
 < typedef long long i64;
 ---
-> typedef long long i64
->  __attribute__((aligned(8)));
-37c37,38
-<   u64 i,u=0;
----
->   //u64 i,u=0; Original code
->   int i; u64 u=0; //VerifiableC (for now)
-277,281c278,280
+> typedef long long i64 __attribute__((aligned(8)));
+277,281c277,279
 <   FOR(i,16) {
 <     o[i]+=(1LL<<16);
 <     c=o[i]>>16;
@@ -18,19 +12,19 @@
 >   FOR(i,15) {
 >     o[(i+1)]+=o[i]>>16;
 >     o[i]&=0xffff;
-282a282,283
+282a281,282
 >   o[0]+=38*(o[15]>>16);
 >   o[15]&=0xffff;
-285c286
+285c285
 < sv sel25519(gf p,gf q,int b)
 ---
 > sv sel25519(gf p,gf q,i64 b)
-287c288,289
+287c287,288
 <   i64 t,i,c=~(b-1);
 ---
 >   int i;
 >   i64 t,c=~(b-1);
-297,299c299,302
+297,299c298,301
 <   int i,j,b;
 <   gf m,t;
 <   FOR(i,16) t[i]=n[i];
@@ -39,18 +33,18 @@
 >   i64 b;
 >   gf t,m={0};
 >   set25519(t,n);
-310d312
+310d311
 <     b=(m[15]>>16)&1;
-312c314,315
+312c313,314
 <     sel25519(t,m,1-b);
 ---
->     b=1-((m[15]>>16)&1);
+>     b=1-(m[15]>>16)&1;
 >     sel25519(t,m,b);
-332c335
+332c334
 <   return d[0]&1;
 ---
->   return d[0]&(unsigned char)1;
-356,359c359,366
+>   return d[0]&(u8)1;
+356,359c358,365
 <   i64 i,j,t[31];
 <   FOR(i,31) t[i]=0;
 <   FOR(i,16) FOR(j,16) t[i+j]+=a[i]*b[j];
@@ -64,60 +58,18 @@
 >     FOR(j,16) t[i+j]+=aux*b[j];
 >   }
 >   FOR(i,15) t[i]+=(i64)38*t[i+16];
-370c377
-@@ we are swaping the variable
-@@ names between a and i
-< sv inv25519(gf o,const gf i)
----
-> sv inv25519(gf o,const gf a)
-373,375c380,382
-<   int a;
+374c380
 <   FOR(a,16) c[a]=i[a];
-<   for(a=253;a>=0;a--) {
----
->   int i;
->   set25519(c,a);
->   for(i=253;i>=0;i--) {
-377c384
-<     if(a!=2&&a!=4) M(c,c,i);
----
->     if(i!=2&&i!=4) M(c,c,a);
-379c386
-<   FOR(a,16) o[a]=c[a];
----
->   FOR(i,16) o[i]=c[i];
-382c389
-@@ we are swaping the variable
-@@ names between a and i
-< sv pow2523(gf o,const gf i)
----
-> sv pow2523(gf o,const gf a)
-385,387c392,394
-<   int a;
-<   FOR(a,16) c[a]=i[a];
-<   for(a=250;a>=0;a--) {
----
->   int i;
->   set25519(c,a);
->   for(i=250;i>=0;i--) {
-389c396
-<     if(a!=1) M(c,c,i);
----
->     if(i!=1) M(c,c,a);
-391c398
-<   FOR(a,16) o[a]=c[a];
 ---
->   FOR(i,16) o[i]=c[i];
-397,398c404,406
-@@ x does not need to be that big
+>   set25519(c,i);
+397,398c403,405
 <   i64 x[80],r,i;
 <   gf a,b,c,d,e,f;
 ---
 >   i64 r;
 >   int i;
 >   gf x,a,b,c,d,e,f;
-433,441c441,443
-@@ we can directly use a and c
+433,441c440,442
 <   FOR(i,16) {
 <     x[i+16]=a[i];
 <     x[i+32]=c[i];

proofs/vst/c/tweetnacl.diff

@@ -2,12 +2,7 @@
 < typedef long long i64;
 ---
 > typedef long long i64 __attribute__((aligned(8)));
-37c37,38
-<   u64 i,u=0;
----
->   //u64 i,u=0; Original code
->   int i; u64 u=0; //VerifiableC (for now)
-277,281c278,280
+277,281c277,279
 <   FOR(i,16) {
 <     o[i]+=(1LL<<16);
 <     c=o[i]>>16;
@@ -17,19 +12,19 @@
 >   FOR(i,15) {
 >     o[(i+1)]+=o[i]>>16;
 >     o[i]&=0xffff;
-282a282,283
+282a281,282
 >   o[0]+=38*(o[15]>>16);
 >   o[15]&=0xffff;
-285c286
+285c285
 < sv sel25519(gf p,gf q,int b)
 ---
 > sv sel25519(gf p,gf q,i64 b)
-287c288,289
+287c287,288
 <   i64 t,i,c=~(b-1);
 ---
 >   int i;
 >   i64 t,c=~(b-1);
-297,299c299,302
+297,299c298,301
 <   int i,j,b;
 <   gf m,t;
 <   FOR(i,16) t[i]=n[i];
@@ -38,18 +33,18 @@
 >   i64 b;
 >   gf t,m={0};
 >   set25519(t,n);
-310d312
+310d311
 <     b=(m[15]>>16)&1;
-312c314,315
+312c313,314
 <     sel25519(t,m,1-b);
 ---
->     b=1-((m[15]>>16)&1);
+>     b=1-(m[15]>>16)&1;
 >     sel25519(t,m,b);
-332c335
+332c334
 <   return d[0]&1;
 ---
->   return d[0]&(unsigned char)1;
-356,359c359,366
+>   return d[0]&(u8)1;
+356,359c358,365
 <   i64 i,j,t[31];
 <   FOR(i,31) t[i]=0;
 <   FOR(i,16) FOR(j,16) t[i+j]+=a[i]*b[j];
@@ -63,54 +58,18 @@
 >     FOR(j,16) t[i+j]+=aux*b[j];
 >   }
 >   FOR(i,15) t[i]+=(i64)38*t[i+16];
-370c377
-< sv inv25519(gf o,const gf i)
----
-> sv inv25519(gf o,const gf a)
-373,375c380,382
-<   int a;
+374c380
 <   FOR(a,16) c[a]=i[a];
-<   for(a=253;a>=0;a--) {
----
->   int i;
->   set25519(c,a);
->   for(i=253;i>=0;i--) {
-377c384
-<     if(a!=2&&a!=4) M(c,c,i);
----
->     if(i!=2&&i!=4) M(c,c,a);
-379c386
-<   FOR(a,16) o[a]=c[a];
----
->   FOR(i,16) o[i]=c[i];
-382c389
-< sv pow2523(gf o,const gf i)
----
-> sv pow2523(gf o,const gf a)
-385,387c392,394
-<   int a;
-<   FOR(a,16) c[a]=i[a];
-<   for(a=250;a>=0;a--) {
----
->   int i;
->   set25519(c,a);
->   for(i=250;i>=0;i--) {
-389c396
-<     if(a!=1) M(c,c,i);
----
->     if(i!=1) M(c,c,a);
-391c398
-<   FOR(a,16) o[a]=c[a];
 ---
->   FOR(i,16) o[i]=c[i];
-397,398c404,406
+>   set25519(c,i);
+397,398c403,405
 <   i64 x[80],r,i;
 <   gf a,b,c,d,e,f;
 ---
 >   i64 r;
 >   int i;
 >   gf x,a,b,c,d,e,f;
-433,441c441,443
+433,441c440,442
 <   FOR(i,16) {
 <     x[i+16]=a[i];
 <     x[i+32]=c[i];

proofs/vst/c/tweetnaclVerifiableC.c

@@ -34,8 +34,7 @@ static u32 ld32(const u8 *x)
 
 static u64 dl64(const u8 *x)
 {
-  //u64 i,u=0; Original code
-  int i; u64 u=0; //VerifiableC (for now)
+  u64 i,u=0;
   FOR(i,8) u=(u<<8)|x[i];
   return u;
 }
@@ -304,14 +303,14 @@ sv pack25519(u8 *o,const gf n)
   car25519(t);
   car25519(t);
   FOR(j,2) {
-    m[0]=t[0]- 0xffed;
+    m[0]=t[0]-0xffed;
     for(i=1;i<15;i++) {
       m[i]=t[i]-0xffff-((m[i-1]>>16)&1);
       m[i-1]&=0xffff;
     }
     m[15]=t[15]-0x7fff-((m[14]>>16)&1);
     m[14]&=0xffff;
-    b=1-((m[15]>>16)&1);
+    b=1-(m[15]>>16)&1;
     sel25519(t,m,b);
   }
   FOR(i,16) {
@@ -332,7 +331,7 @@ static u8 par25519(const gf a)
 {
   u8 d[32];
   pack25519(d,a);
-  return d[0]&(unsigned char)1;
+  return d[0]&(u8)1;
 }
 
 sv unpack25519(gf o, const u8 *n)
@@ -374,28 +373,28 @@ sv S(gf o,const gf a)
   M(o,a,a);
 }
 
-sv inv25519(gf o,const gf a)
+sv inv25519(gf o,const gf i)
 {
   gf c;
-  int i;
-  set25519(c,a);
-  for(i=253;i>=0;i--) {
+  int a;
+  set25519(c,i);
+  for(a=253;a>=0;a--) {
     S(c,c);
-    if(i!=2&&i!=4) M(c,c,a);
+    if(a!=2&&a!=4) M(c,c,i);
   }
-  FOR(i,16) o[i]=c[i];
+  FOR(a,16) o[a]=c[a];
 }
 
-sv pow2523(gf o,const gf a)
+sv pow2523(gf o,const gf i)
 {
   gf c;
-  int i;
-  set25519(c,a);
-  for(i=250;i>=0;i--) {
+  int a;
+  FOR(a,16) c[a]=i[a];
+  for(a=250;a>=0;a--) {
     S(c,c);
-    if(i!=1) M(c,c,a);
+    if(a!=1) M(c,c,i);
   }
-  FOR(i,16) o[i]=c[i];
+  FOR(a,16) o[a]=c[a];
 }
 
 int crypto_scalarmult(u8 *q,const u8 *n,const u8 *p)

proofs/vst/proofs/verif_inv25519.v

@@ -10,16 +10,16 @@ Require Import Tweetnacl.Low.S.
 
 Open Scope Z.
 (*
-sv inv25519(gf o,const gf a)
+sv inv25519(gf o,const gf i)
 {
   gf c;
-  int i;
-  FOR(a,16) c[a]=a[i];
-  for(i=253;i>=0;i--) {
+  int a;
+  FOR(a,16) c[a]=i[a];
+  for(a=253;a>=0;a--) {
     S(c,c);
-    if(i!=2&&i!=4) M(c,c,a);
+    if(a!=2&&a!=4) M(c,c,i);
   }
-  FOR(i,16) o[i]=c[i];
+  FOR(a,16) o[a]=c[a];
 }
 *)
 
@@ -34,25 +34,25 @@ start_function.
 rewrite /data_at_ /field_at_ /default_val ; simpl.
 unfold nm_overlap_array_sep_2.
 flatten ; Intros.
-subst o v_a.
-1: forward_call (v_c,v_o,Tsh,sho,undef16,a).
-2: forward_call (v_c,v_a,Tsh,sha,undef16,a).
+subst o v_i.
+1: forward_call (v_c,v_o,Tsh,sho,undef16,i).
+2: forward_call (v_c,v_i,Tsh,shi,undef16,i).
 
 1: forward_for 
 (* Loop Invariant *)
-(inv25519_Inv sho sho Tsh v_o v_o v_c (mVI64 a) a 0)
+(inv25519_Inv sho sho Tsh v_o v_o v_c (mVI64 i) i 0)
 (* PreInc invariant *)
-(inv25519_PreIncInv sho sho Tsh v_o v_o v_c (mVI64 a) a 0)
+(inv25519_PreIncInv sho sho Tsh v_o v_o v_c (mVI64 i) i 0)
 (* Loop postcondition *)
-(inv25519_PostInv sho sho Tsh v_o v_o v_c (mVI64 a) a 0).
+(inv25519_PostInv sho sho Tsh v_o v_o v_c (mVI64 i) i 0).
 7: forward_for 
 (* Loop Invariant *)
-(inv25519_Inv sho sha Tsh v_o v_a v_c o a 1)
+(inv25519_Inv sho shi Tsh v_o v_i v_c o i 1)
 (* PreInc invariant *)
-(inv25519_PreIncInv sho sha Tsh v_o v_a v_c o a 1)
+(inv25519_PreIncInv sho shi Tsh v_o v_i v_c o i 1)
 (* Loop postcondition *)
-(inv25519_PostInv sho sha Tsh v_o v_a v_c o a 1).
-all: try rename a0 into i.
+(inv25519_PostInv sho shi Tsh v_o v_i v_c o i 1).
+all: try rename a0 into a.
 
 (* 6 goals generated *)
 (* 1 *)
@@ -73,12 +73,12 @@ all: try rename a0 into i.
 1: change (0 =? 0) with true.
 2: change (1 =? 0) with false.
 1,2: flatten ; Intros.
-1,2: assert(Forall (fun x : ℤ => -38 <= x < 2 ^ 16 + 38) (pow_fn_rev (253 - i) 254 a a)) 
+1,2: assert(Forall (fun x : ℤ => -38 <= x < 2 ^ 16 + 38) (pow_fn_rev (253 - a) 254 i i)) 
   by (apply pow_fn_rev_bound_Zlength ; assumption).
-1,2: assert(Zlength (pow_fn_rev (253 - i) 254 a a) = 16) by (apply pow_fn_rev_Zlength ; assumption).
+1,2: assert(Zlength (pow_fn_rev (253 - a) 254 i i) = 16) by (apply pow_fn_rev_Zlength ; assumption).
 all: assert(HWTsh:= writable_share_top).
 all: assert(HRTsh:= writable_readable_share HWTsh).
-1,2: remember (pow_fn_rev (253 - i) 254 a a) as c0.
+1,2: remember (pow_fn_rev (253 - a) 254 i i) as c0.
 1,2: assert(Zlength (mVI64 c0) = 16) by (rewrite ?Zlength_map ; assumption).
 
 1,2: forward_call (v_c, v_c, Tsh, Tsh, mVI64 c0, c0, 0).
@@ -87,17 +87,17 @@ all: assert(HRTsh:= writable_readable_share HWTsh).
 1,2: solve_bounds_by_values_Forall_impl.
 1,2: unfold_nm_overlap_array_sep; simpl.
 
-1,2: assert(Hi: i = 2 \/ i = 4 \/ (i <> 2 /\ i <> 4)) by omega.
+1,2: assert(Ha: a = 2 \/ a = 4 \/ (a <> 2 /\ a <> 4)) by omega.
 
 (* case analysis *)
 (* i = 2 *)
-1,2: destruct Hi as [Hi|Hi] ; try subst i.
+1,2: destruct Ha as [Ha|Ha] ; try subst a.
 1: forward_if (PROP ( )
-   LOCAL (temp _i (Vint (Int.repr 2)); temp _t'1 (Vint (Int.repr 0)); temp _o v_o; temp _a v_o; lvar _c (tarray tlg 16) v_c)
-   SEP (Tsh [{v_c}]<<( lg16 )-- mVI64 (Low.S c0); sho [{v_o}]<<( lg16 )-- mVI64 a)).
+   LOCAL (temp _a (Vint (Int.repr 2)); temp _t'1 (Vint (Int.repr 0)); temp _o v_o; temp _i v_o; lvar _c (tarray tlg 16) v_c)
+   SEP (Tsh [{v_c}]<<( lg16 )-- mVI64 (Low.S c0); sho [{v_o}]<<( lg16 )-- mVI64 i)).
 5: forward_if (PROP ( )
-   LOCAL (temp _i (Vint (Int.repr 2)); temp _t'1 (Vint (Int.repr 0)); temp _o v_o; temp _a v_a; lvar _c (tarray tlg 16) v_c)
-   SEP (Tsh [{v_c}]<<( lg16 )-- mVI64 (Low.S c0); sho [{v_o}]<<( lg16 )-- o; sha [{v_a}]<<( lg16 )-- mVI64 a)).
+   LOCAL (temp _a (Vint (Int.repr 2)); temp _t'1 (Vint (Int.repr 0)); temp _o v_o; temp _i v_i; lvar _c (tarray tlg 16) v_c)
+   SEP (Tsh [{v_c}]<<( lg16 )-- mVI64 (Low.S c0); sho [{v_o}]<<( lg16 )-- o; shi [{v_i}]<<( lg16 )-- mVI64 i)).
 1,5: exfalso; match goal with [ H : ?A <> ?A |- _ ] => by apply H end.
 1,4: forward.
 1,2: entailer!.

proofs/vst/spec/spec_inv25519.v

@@ -3,80 +3,73 @@ Require Import Tweetnacl_verif.init_tweetnacl.
 Require Import Tweetnacl.Low.Inv25519.
 
 (*
-sv inv25519(gf o,const gf a)
+sv inv25519(gf o,const gf i)
 {
   gf c;
-  int i;
-  FOR(a,16) c[a]=a[i];
-  for(i=253;i>=0;i--) {
+  int a;
+  FOR(a,16) c[a]=i[a];
+  for(a=253;a>=0;a--) {
     S(c,c);
-    if(i!=2&&i!=4) M(c,c,a);
+    if(a!=2&&a!=4) M(c,c,i);
   }
-  FOR(i,16) o[i]=c[i];
-}
-*)
+  FOR(a,16) o[a]=c[a];
+}*)
 
 Open Scope Z.
 
 Definition inv25519_spec := 
  DECLARE _inv25519
-  WITH v_o: val, v_a: val, sho : share, sha : share, o : list val, a : list Z, k : Z
-  PRE [ _o OF (tptr tlg), _a OF (tptr tlg)]
-        PROP  (writable_share sho; readable_share sha;
-                Forall (fun x : ℤ => -38 <= x < 2 ^ 16 + 38) a;
-                Zlength a = 16;
+  WITH v_o: val, v_i: val, sho : share, shi : share, o : list val, i : list Z, k : Z
+  PRE [ _o OF (tptr tlg), _i OF (tptr tlg)]
+        PROP  (writable_share sho; readable_share shi;
+                Forall (fun x : ℤ => -38 <= x < 2 ^ 16 + 38) i;
+                Zlength i = 16;
                 Zlength o = 16)
-        LOCAL (temp _o v_o; temp _a v_a)
-        SEP   (nm_overlap_array_sep_2 sho sha o (mVI64 a) v_o v_a k)
+        LOCAL (temp _o v_o; temp _i v_i)
+        SEP   (nm_overlap_array_sep_2 sho shi o (mVI64 i) v_o v_i k)
   POST [ tvoid ]
         PROP (
-                Zlength (Inv25519 a) = 16;
-                Forall (fun x : ℤ => -38 <= x < 2 ^ 16 + 38) (Inv25519 a)
+                Zlength (Inv25519 i) = 16;
+                Forall (fun x : ℤ => -38 <= x < 2 ^ 16 + 38) (Inv25519 i)
              )
         LOCAL()
-        SEP  (nm_overlap_array_sep_2' sho sha (mVI64 (Inv25519 a)) (mVI64 a) v_o v_a k).
+        SEP  (nm_overlap_array_sep_2' sho shi (mVI64 (Inv25519 i)) (mVI64 i) v_o v_i k).
 
-(* Definition init_Inv (L:list localdef) sho sha shc v_o v_a v_c o (a:list Z) k := 
-  EX i : Z,
-   PROP  ()
-   (LOCALx L
-   SEP   (nm_overlap_array_sep_2 sho sha o (mVI64 a) v_o v_a k;
-          shc [{ v_c }] <<(lg16)-- (list.take (nat_of_Z i) (mVI64 a) ++ list.drop (nat_of_Z i) undef16))).
- *)
-Definition inv25519_Inv sho sha shc v_o v_a v_c o (a:list Z) k :=
+
+Definition inv25519_Inv sho shi shc v_o v_i v_c o (i:list Z) k :=
 (* Loop Invariant *)
-fun i:Z => 
-  PROP (-1 <= i <= 253)
-  LOCAL ((temp _i (Vint (Int.repr i)));
-      temp _o v_o; temp _a v_a;
+fun a:Z => 
+  PROP (-1 <= a <= 253)
+  LOCAL ((temp _a (Vint (Int.repr a)));
+      temp _o v_o; temp _i v_i;
       lvar _c (tarray tlg 16) v_c)
-  SEP ( nm_overlap_array_sep_2 sho sha o (mVI64 a) v_o v_a k;
-        shc [{ v_c }] <<(lg16)-- (mVI64 (pow_fn_rev (253 - i) 254 a a))).
+  SEP ( nm_overlap_array_sep_2 sho shi o (mVI64 i) v_o v_i k;
+        shc [{ v_c }] <<(lg16)-- (mVI64 (pow_fn_rev (253 - a) 254 i i))).
 
-Definition inv25519_PreIncInv sho sha shc v_o v_a v_c o (a:list Z) k :=
+Definition inv25519_PreIncInv sho shi shc v_o v_i v_c o (i:list Z) k :=
 (* PreDec invariant *)
-  fun i:Z =>
-  PROP (0 <= i <= 253)
-  LOCAL ((temp _i (Vint (Int.repr i)));
-      temp _o v_o; temp _a v_a;
+  fun a:Z =>
+  PROP (0 <= a <= 253)
+  LOCAL ((temp _a (Vint (Int.repr a)));
+      temp _o v_o; temp _i v_i;
       lvar _c (tarray tlg 16) v_c)
-  SEP ( nm_overlap_array_sep_2 sho sha o (mVI64 a) v_o v_a k;
-        shc [{ v_c }] <<(lg16)-- mVI64 (pow_fn_rev (253 - (i - 1)) 254 a a)).
+  SEP ( nm_overlap_array_sep_2 sho shi o (mVI64 i) v_o v_i k;
+        shc [{ v_c }] <<(lg16)-- mVI64 (pow_fn_rev (253 - (a - 1)) 254 i i)).
 
-Definition inv25519_PostInv sho sha shc v_o v_a v_c o (a:list Z) k :=
+Definition inv25519_PostInv sho shi shc v_o v_i v_c o (i:list Z) k :=
 (* Loop postcondition *)
  PROP ()
  LOCAL (
-      temp _o v_o; temp _a v_a;
+      temp _o v_o; temp _i v_i;
       lvar _c (tarray tlg 16) v_c)
-  SEP ( nm_overlap_array_sep_2 sho sha o (mVI64 a) v_o v_a k;
-        shc [{ v_c }] <<(lg16)-- mVI64 (pow_fn_rev 254 254 a a)).
+  SEP ( nm_overlap_array_sep_2 sho shi o (mVI64 i) v_o v_i k;
+        shc [{ v_c }] <<(lg16)-- mVI64 (pow_fn_rev 254 254 i i)).
 
-Definition copy_Inv (L:list localdef) sho sha shc v_o v_a v_c o (a:list Z) (c:list Z) k := 
-  EX i : Z,
+Definition copy_Inv (L:list localdef) sho shi shc v_o v_i v_c o (i:list Z) (c:list Z) k := 
+  EX a : Z,
    PROP  ()
    (LOCALx L
-   SEP   ( nm_overlap_array_sep_2' sho sha (list.take (nat_of_Z i) (mVI64 c) ++ (list.drop (nat_of_Z i) o)) (mVI64 a) v_o v_a k; 
+   SEP   ( nm_overlap_array_sep_2' sho shi (list.take (nat_of_Z a) (mVI64 c) ++ (list.drop (nat_of_Z a) o)) (mVI64 i) v_o v_i k; 
            shc [{v_c}] <<(lg16)-- (mVI64 c))).
 
 Close Scope Z.
\ No newline at end of file