Merge pull request #103 from formosa-crypto/fix/remove_unused_variabl…

…e_warning Fix/remove unused variable warning
formosa-crypto · Jan 17, 2024 · 0daf13f · 0daf13f
2 parents ef67bd2 + b688b07
commit 0daf13f
Show file tree

Hide file tree

Showing 4 changed files with 20 additions and 18 deletions.
diff --git a/.github/workflows/amd64-linux-main-proof.yml b/.github/workflows/amd64-linux-main-proof.yml
@@ -1,9 +1,11 @@
 name: amd64-linux-main-proof
 
 on:
-  workflow_run:
-    workflows: [amd64-linux-main]
-    types: [completed]
+  workflow_dispatch:
+  push:
+    branches:
+      - main
+  pull_request:
 
 jobs:
 

diff --git a/proof/crypto_onetimeauth/poly1305/amd64/avx2/Poly1305_savx2.ec b/proof/crypto_onetimeauth/poly1305/amd64/avx2/Poly1305_savx2.ec
@@ -573,8 +573,8 @@ module M = {
   }
 
   proc add_mulmod_avx2 (h:W256.t Array5.t, m:W256.t Array5.t,
-                        s_r:W256.t Array5.t, s_rx5:W256.t Array4.t,
-                        s_mask26:W256.t, s_bit25:W256.t) : W256.t Array5.t = {
+                        s_r:W256.t Array5.t, s_rx5:W256.t Array4.t
+                       ) : W256.t Array5.t = {
 
     var r0:W256.t;
     var r1:W256.t;
@@ -775,11 +775,11 @@ module M = {
 
   proc final_avx2_v0 (h:W256.t Array5.t, m:W256.t Array5.t,
                       s_r:W256.t Array5.t, s_rx5:W256.t Array4.t,
-                      s_mask26:W256.t, s_bit25:W256.t) : W256.t Array5.t = {
+                      s_mask26:W256.t) : W256.t Array5.t = {
 
     var mask26:W256.t;
 
-    h <@ add_mulmod_avx2 (h, m, s_r, s_rx5, s_mask26, s_bit25);
+    h <@ add_mulmod_avx2 (h, m, s_r, s_rx5);
     mask26 <- s_mask26;
     h <@ carry_reduce_avx2 (h, mask26);
     return (h);
@@ -820,7 +820,7 @@ module M = {
       len <- (len - (W64.of_int 64));
     }
     len <- (len - (W64.of_int 64));
-    h <@ final_avx2_v0 (h, m, r1234, r1234x5, s_mask26, s_bit25);
+    h <@ final_avx2_v0 (h, m, r1234, r1234x5, s_mask26);
     h64 <@ pack_avx2 (h);
     return (in_0, len, h64);
   }

diff --git a/proof/crypto_onetimeauth/poly1305/amd64/avx2/Poly1305_savx2_prevec.ec b/proof/crypto_onetimeauth/poly1305/amd64/avx2/Poly1305_savx2_prevec.ec
@@ -273,8 +273,8 @@ module Mprevec = {
   }
 
   proc add_mulmod_avx2 (h:t4u64 Array5.t,m:t4u64 Array5.t,
-                        s_r:t4u64 Array5.t,s_rx5:t4u64 Array4.t,
-                        s_mask26:t4u64,s_bit25:t4u64) : t4u64 Array5.t = {
+                        s_r:t4u64 Array5.t,s_rx5:t4u64 Array4.t
+                       ) : t4u64 Array5.t = {
     var r0:t4u64;
     var r1:t4u64;
     var r4x5:t4u64;
@@ -473,11 +473,11 @@ module Mprevec = {
 
   proc final_avx2_v0 (h:t4u64 Array5.t,m:t4u64 Array5.t,
                       s_r:t4u64 Array5.t,s_rx5:t4u64 Array4.t,
-                      s_mask26:t4u64,s_bit25:t4u64) : t4u64 Array5.t = {
+                      s_mask26:t4u64) : t4u64 Array5.t = {
 
     var mask26:t4u64;
 
-    h <@ add_mulmod_avx2 (h,m,s_r,s_rx5,s_mask26,s_bit25);
+    h <@ add_mulmod_avx2 (h,m,s_r,s_rx5);
     mask26 <- s_mask26;
     h <@ carry_reduce_avx2 (h,mask26);
     return (h);
@@ -520,7 +520,7 @@ module Mprevec = {
       len <- (len - (W64.of_int 64));
     }
     len <- (len - (W64.of_int 64));
-    h <@ final_avx2_v0 (h,m,r1234,r1234x5,s_mask26,s_bit25);
+    h <@ final_avx2_v0 (h,m,r1234,r1234x5,s_mask26);
     h64 <@ pack_avx2 (h);
     return (in_0,len,h64);
   }

diff --git a/proof/crypto_onetimeauth/poly1305/amd64/avx2/Poly1305_savx2_vec.ec b/proof/crypto_onetimeauth/poly1305/amd64/avx2/Poly1305_savx2_vec.ec
@@ -272,7 +272,7 @@ module Mvec = {
 
   proc add_mulmod_avx2 (h:vt4u64 Array5.t,m:vt4u64 Array5.t,
                         s_r:vt4u64 Array5.t,s_rx5:vt4u64 Array4.t,
-                        s_mask26:vt4u64,s_bit25:vt4u64) : vt4u64 Array5.t = {
+                        s_mask26:vt4u64) : vt4u64 Array5.t = {
     var r0:vt4u64;
     var r1:vt4u64;
     var r4x5:vt4u64;
@@ -470,11 +470,11 @@ module Mvec = {
 
   proc final_avx2_v0 (h:vt4u64 Array5.t,m:vt4u64 Array5.t,
                       s_r:vt4u64 Array5.t,s_rx5:vt4u64 Array4.t,
-                      s_mask26:vt4u64,s_bit25:vt4u64) : vt4u64 Array5.t = {
+                      s_mask26:vt4u64) : vt4u64 Array5.t = {
 
     var mask26:vt4u64;
 
-    h <@ add_mulmod_avx2 (h,m,s_r,s_rx5,s_mask26,s_bit25);
+    h <@ add_mulmod_avx2 (h,m,s_r,s_rx5,s_mask26);
     mask26 <- s_mask26;
     h <@ carry_reduce_avx2 (h,mask26);
     return (h);
@@ -516,7 +516,7 @@ module Mvec = {
       len <- (len - (W64.of_int 64));
     }
     len <- (len - (W64.of_int 64));
-    h <@ final_avx2_v0 (h,m,r1234,r1234x5,s_mask26,s_bit25);
+    h <@ final_avx2_v0 (h,m,r1234,r1234x5,s_mask26);
     h64 <@ pack_avx2 (h);
     return (in_0,len,h64);
   }
@@ -584,7 +584,7 @@ proof.
 qed.
 
 equiv eq_add_mulmod_avx2 :  Mprevec.add_mulmod_avx2 ~ Mvec.add_mulmod_avx2 : 
-  is4u64_5 h{1} h{2} /\ is4u64_5 m{1} m{2} /\ is4u64_5 s_r{1} s_r{2} /\ is4u64_4 s_rx5{1} s_rx5{2} /\ is4u64 s_mask26{1} s_mask26{2} /\ is4u64 s_bit25{1} s_bit25{2} ==>
+  is4u64_5 h{1} h{2} /\ is4u64_5 m{1} m{2} /\ is4u64_5 s_r{1} s_r{2} /\ is4u64_4 s_rx5{1} s_rx5{2} ==>
   is4u64_5 res{1} res{2}.
 proof.
   proc;wp.