curve25519: fix ct proof in EasyCrypt (arguments names have changed)

formosa-crypto · Oct 12, 2023 · 900ceec · 900ceec
1 parent e428b8f
commit 900ceec
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 6 deletions.
diff --git a/proof/crypto_scalarmult/curve25519/amd64/mulx/extracted_ct_proof.ec b/proof/crypto_scalarmult/curve25519/amd64/mulx/extracted_ct_proof.ec
@@ -2,14 +2,14 @@ require import Extracted_ct.
 
 equiv jade_scalarmult_curve25519_amd64_mulx : 
   M.jade_scalarmult_curve25519_amd64_mulx ~ M.jade_scalarmult_curve25519_amd64_mulx :
-    ={q, n, p, M.leakages} ==> ={M.leakages}.
+    ={qp, np, pp, M.leakages} ==> ={M.leakages}.
 proof.
 proc; inline *; sim => />.
 qed.
 
 equiv jade_scalarmult_curve25519_amd64_mulx_base : 
   M.jade_scalarmult_curve25519_amd64_mulx_base ~ M.jade_scalarmult_curve25519_amd64_mulx_base :
-    ={q, n, M.leakages} ==> ={M.leakages}.
+    ={qp, np, M.leakages} ==> ={M.leakages}.
 proof.
 proc; inline *; sim => />.
 qed.

diff --git a/proof/crypto_scalarmult/curve25519/amd64/ref4/extracted_ct_proof.ec b/proof/crypto_scalarmult/curve25519/amd64/ref4/extracted_ct_proof.ec
@@ -2,14 +2,14 @@ require import Extracted_ct.
 
 equiv jade_scalarmult_curve25519_amd64_ref4 : 
   M.jade_scalarmult_curve25519_amd64_ref4 ~ M.jade_scalarmult_curve25519_amd64_ref4 :
-    ={q, n, p, M.leakages} ==> ={M.leakages}.
+    ={qp, np, pp, M.leakages} ==> ={M.leakages}.
 proof.
 proc; inline *; sim => />.
 qed.
 
 equiv jade_scalarmult_curve25519_amd64_ref4_base : 
   M.jade_scalarmult_curve25519_amd64_ref4_base ~ M.jade_scalarmult_curve25519_amd64_ref4_base :
-    ={q, n, M.leakages} ==> ={M.leakages}.
+    ={qp, np, M.leakages} ==> ={M.leakages}.
 proof.
 proc; inline *; sim => />.
 qed.

diff --git a/proof/crypto_scalarmult/curve25519/amd64/ref5/extracted_ct_proof.ec b/proof/crypto_scalarmult/curve25519/amd64/ref5/extracted_ct_proof.ec
@@ -2,14 +2,14 @@ require import Extracted_ct.
 
 equiv jade_scalarmult_curve25519_amd64_ref5 : 
   M.jade_scalarmult_curve25519_amd64_ref5 ~ M.jade_scalarmult_curve25519_amd64_ref5 :
-    ={q, n, p, M.leakages} ==> ={M.leakages}.
+    ={qp, np, pp, M.leakages} ==> ={M.leakages}.
 proof.
 proc; inline *; sim => />.
 qed.
 
 equiv jade_scalarmult_curve25519_amd64_ref5_base : 
   M.jade_scalarmult_curve25519_amd64_ref5_base ~ M.jade_scalarmult_curve25519_amd64_ref5_base :
-    ={q, n, M.leakages} ==> ={M.leakages}.
+    ={qp, np, M.leakages} ==> ={M.leakages}.
 proof.
 proc; inline *; sim => />.
 qed.