diff --git a/.github/workflows/amd64-linux-main-proof.yml b/.github/workflows/amd64-linux-main-proof.yml
index 52ac84db..4b49558f 100644
--- 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
index 0098e518..1dd46b40 100644
--- 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
index 7b6be3db..c53f721f 100644
--- 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
index b00c9960..7ffcf597 100644
--- 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.