From a274aac4c069e41dd0f2a3bbc6caabc14b62f109 Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Mon, 5 Dec 2022 17:09:23 +0000 Subject: [PATCH 1/9] args naming : crypto_stream pass --- .../chacha/chacha12/amd64/avx/stream_ct_proof.ec | 4 ++-- .../chacha12/amd64/avx2/stream_ct_proof.ec | 4 ++-- .../chacha/chacha12/amd64/ref/stream_ct_proof.ec | 4 ++-- .../chacha20-ietf/amd64/avx/stream_ct_proof.ec | 4 ++-- .../chacha20-ietf/amd64/avx2/stream_ct_proof.ec | 4 ++-- .../chacha20-ietf/amd64/ref/stream_ct_proof.ec | 4 ++-- .../chacha/chacha20/amd64/avx/stream_ct_proof.ec | 4 ++-- .../chacha20/amd64/avx2/stream_ct_proof.ec | 4 ++-- .../chacha/chacha20/amd64/ref/stream_ct_proof.ec | 4 ++-- .../salsa20/salsa20/amd64/avx/stream_ct_proof.ec | 4 ++-- .../salsa20/amd64/avx2/stream_ct_proof.ec | 4 ++-- .../salsa20/salsa20/amd64/ref/stream_ct_proof.ec | 4 ++-- .../salsa2012/amd64/avx/stream_ct_proof.ec | 4 ++-- .../salsa2012/amd64/avx2/stream_ct_proof.ec | 4 ++-- .../salsa2012/amd64/ref/stream_ct_proof.ec | 4 ++-- .../xsalsa20/amd64/avx/stream_ct_proof.ec | 4 ++-- .../xsalsa20/amd64/avx2/stream_ct_proof.ec | 4 ++-- .../xsalsa20/amd64/ref/stream_ct_proof.ec | 4 ++-- .../chacha/chacha12/amd64/avx/stream.jazz | 8 ++++---- .../chacha/chacha12/amd64/avx2/stream.jazz | 8 ++++---- .../chacha/chacha12/amd64/ref/stream.jazz | 8 ++++---- .../chacha/chacha20-ietf/amd64/avx/stream.jazz | 16 ++++++++-------- .../chacha/chacha20-ietf/amd64/avx2/stream.jazz | 16 ++++++++-------- .../chacha/chacha20-ietf/amd64/ref/stream.jazz | 16 ++++++++-------- .../chacha/chacha20/amd64/avx/stream.jazz | 8 ++++---- .../chacha/chacha20/amd64/avx2/stream.jazz | 8 ++++---- .../chacha/chacha20/amd64/ref/stream.jazz | 8 ++++---- .../salsa20/salsa20/amd64/avx/stream.jazz | 8 ++++---- .../salsa20/salsa20/amd64/avx2/stream.jazz | 8 ++++---- .../salsa20/salsa20/amd64/ref/stream.jazz | 9 +++++---- .../salsa20/salsa2012/amd64/avx/stream.jazz | 8 ++++---- .../salsa20/salsa2012/amd64/avx2/stream.jazz | 8 ++++---- .../salsa20/salsa2012/amd64/ref/stream.jazz | 8 ++++---- src/crypto_stream/xsalsa20/amd64/avx/stream.jazz | 8 ++++---- .../xsalsa20/amd64/avx2/stream.jazz | 8 ++++---- src/crypto_stream/xsalsa20/amd64/ref/stream.jazz | 8 ++++---- 36 files changed, 121 insertions(+), 120 deletions(-) diff --git a/proof/crypto_stream/chacha/chacha12/amd64/avx/stream_ct_proof.ec b/proof/crypto_stream/chacha/chacha12/amd64/avx/stream_ct_proof.ec index 0f305415..ba26d0a8 100644 --- a/proof/crypto_stream/chacha/chacha12/amd64/avx/stream_ct_proof.ec +++ b/proof/crypto_stream/chacha/chacha12/amd64/avx/stream_ct_proof.ec @@ -2,14 +2,14 @@ require import Stream_ct. equiv eq_jade_stream_chacha_chacha12_amd64_avx_xor_ct : M.jade_stream_chacha_chacha12_amd64_avx_xor ~ M.jade_stream_chacha_chacha12_amd64_avx_xor : - ={output, input, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={output, input, input_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. equiv eq_jade_stream_chacha_chacha12_amd64_avx_ct : M.jade_stream_chacha_chacha12_amd64_avx ~ M.jade_stream_chacha_chacha12_amd64_avx : - ={output, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={stream, stream_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_stream/chacha/chacha12/amd64/avx2/stream_ct_proof.ec b/proof/crypto_stream/chacha/chacha12/amd64/avx2/stream_ct_proof.ec index 0e2fde91..830f5ab8 100644 --- a/proof/crypto_stream/chacha/chacha12/amd64/avx2/stream_ct_proof.ec +++ b/proof/crypto_stream/chacha/chacha12/amd64/avx2/stream_ct_proof.ec @@ -2,14 +2,14 @@ require import Stream_ct. equiv eq_jade_stream_chacha_chacha12_amd64_avx2_xor_ct : M.jade_stream_chacha_chacha12_amd64_avx2_xor ~ M.jade_stream_chacha_chacha12_amd64_avx2_xor : - ={output, input, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={output, input, input_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. equiv eq_jade_stream_chacha_chacha12_amd64_avx2_ct : M.jade_stream_chacha_chacha12_amd64_avx2 ~ M.jade_stream_chacha_chacha12_amd64_avx2 : - ={output, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={stream, stream_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_stream/chacha/chacha12/amd64/ref/stream_ct_proof.ec b/proof/crypto_stream/chacha/chacha12/amd64/ref/stream_ct_proof.ec index c5d43699..852a6010 100644 --- a/proof/crypto_stream/chacha/chacha12/amd64/ref/stream_ct_proof.ec +++ b/proof/crypto_stream/chacha/chacha12/amd64/ref/stream_ct_proof.ec @@ -2,14 +2,14 @@ require import Stream_ct. equiv eq_jade_stream_chacha_chacha12_amd64_ref_xor_ct : M.jade_stream_chacha_chacha12_amd64_ref_xor ~ M.jade_stream_chacha_chacha12_amd64_ref_xor : - ={output, input, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={output, input, input_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. equiv eq_jade_stream_chacha_chacha12_amd64_ref_ct : M.jade_stream_chacha_chacha12_amd64_ref ~ M.jade_stream_chacha_chacha12_amd64_ref : - ={output, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={stream, stream_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_stream/chacha/chacha20-ietf/amd64/avx/stream_ct_proof.ec b/proof/crypto_stream/chacha/chacha20-ietf/amd64/avx/stream_ct_proof.ec index 340fd9d8..b67f280d 100644 --- a/proof/crypto_stream/chacha/chacha20-ietf/amd64/avx/stream_ct_proof.ec +++ b/proof/crypto_stream/chacha/chacha20-ietf/amd64/avx/stream_ct_proof.ec @@ -2,14 +2,14 @@ require import Stream_ct. equiv eq_jade_stream_chacha_chacha20_ietf_amd64_avx_xor_ct : M.jade_stream_chacha_chacha20_ietf_amd64_avx_xor ~ M.jade_stream_chacha_chacha20_ietf_amd64_avx_xor : - ={output, input, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={output, input, input_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. equiv eq_jade_stream_chacha_chacha20_ietf_amd64_avx_ct : M.jade_stream_chacha_chacha20_ietf_amd64_avx ~ M.jade_stream_chacha_chacha20_ietf_amd64_avx : - ={output, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={stream, stream_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_stream/chacha/chacha20-ietf/amd64/avx2/stream_ct_proof.ec b/proof/crypto_stream/chacha/chacha20-ietf/amd64/avx2/stream_ct_proof.ec index 6dad44a6..1ecb2bd5 100644 --- a/proof/crypto_stream/chacha/chacha20-ietf/amd64/avx2/stream_ct_proof.ec +++ b/proof/crypto_stream/chacha/chacha20-ietf/amd64/avx2/stream_ct_proof.ec @@ -2,14 +2,14 @@ require import Stream_ct. equiv eq_jade_stream_chacha_chacha20_ietf_amd64_avx2_xor_ct : M.jade_stream_chacha_chacha20_ietf_amd64_avx2_xor ~ M.jade_stream_chacha_chacha20_ietf_amd64_avx2_xor : - ={output, input, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={output, input, input_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. equiv eq_jade_stream_chacha_chacha20_ietf_amd64_avx2_ct : M.jade_stream_chacha_chacha20_ietf_amd64_avx2 ~ M.jade_stream_chacha_chacha20_ietf_amd64_avx2 : - ={output, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={stream, stream_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_stream/chacha/chacha20-ietf/amd64/ref/stream_ct_proof.ec b/proof/crypto_stream/chacha/chacha20-ietf/amd64/ref/stream_ct_proof.ec index 6a7371d6..7ac8fe29 100644 --- a/proof/crypto_stream/chacha/chacha20-ietf/amd64/ref/stream_ct_proof.ec +++ b/proof/crypto_stream/chacha/chacha20-ietf/amd64/ref/stream_ct_proof.ec @@ -2,14 +2,14 @@ require import Stream_ct. equiv eq_jade_stream_chacha_chacha20_ietf_amd64_ref_xor_ct : M.jade_stream_chacha_chacha20_ietf_amd64_ref_xor ~ M.jade_stream_chacha_chacha20_ietf_amd64_ref_xor : - ={output, input, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={output, input, input_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. equiv eq_jade_stream_chacha_chacha20_ietf_amd64_ref_ct : M.jade_stream_chacha_chacha20_ietf_amd64_ref ~ M.jade_stream_chacha_chacha20_ietf_amd64_ref : - ={output, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={stream, stream_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_stream/chacha/chacha20/amd64/avx/stream_ct_proof.ec b/proof/crypto_stream/chacha/chacha20/amd64/avx/stream_ct_proof.ec index ebbd3bca..e2ebdfbf 100644 --- a/proof/crypto_stream/chacha/chacha20/amd64/avx/stream_ct_proof.ec +++ b/proof/crypto_stream/chacha/chacha20/amd64/avx/stream_ct_proof.ec @@ -2,14 +2,14 @@ require import Stream_ct. equiv eq_jade_stream_chacha_chacha20_amd64_avx_xor_ct : M.jade_stream_chacha_chacha20_amd64_avx_xor ~ M.jade_stream_chacha_chacha20_amd64_avx_xor : - ={output, input, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={output, input, input_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. equiv eq_jade_stream_chacha_chacha20_amd64_avx_ct : M.jade_stream_chacha_chacha20_amd64_avx ~ M.jade_stream_chacha_chacha20_amd64_avx : - ={output, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={stream, stream_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_stream/chacha/chacha20/amd64/avx2/stream_ct_proof.ec b/proof/crypto_stream/chacha/chacha20/amd64/avx2/stream_ct_proof.ec index eda64d29..19e922a0 100644 --- a/proof/crypto_stream/chacha/chacha20/amd64/avx2/stream_ct_proof.ec +++ b/proof/crypto_stream/chacha/chacha20/amd64/avx2/stream_ct_proof.ec @@ -2,14 +2,14 @@ require import Stream_ct. equiv eq_jade_stream_chacha_chacha20_amd64_avx2_xor_ct : M.jade_stream_chacha_chacha20_amd64_avx2_xor ~ M.jade_stream_chacha_chacha20_amd64_avx2_xor : - ={output, input, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={output, input, input_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. equiv eq_jade_stream_chacha_chacha20_amd64_avx2_ct : M.jade_stream_chacha_chacha20_amd64_avx2 ~ M.jade_stream_chacha_chacha20_amd64_avx2 : - ={output, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={stream, stream_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_stream/chacha/chacha20/amd64/ref/stream_ct_proof.ec b/proof/crypto_stream/chacha/chacha20/amd64/ref/stream_ct_proof.ec index 211634e5..f9f84896 100644 --- a/proof/crypto_stream/chacha/chacha20/amd64/ref/stream_ct_proof.ec +++ b/proof/crypto_stream/chacha/chacha20/amd64/ref/stream_ct_proof.ec @@ -2,14 +2,14 @@ require import Stream_ct. equiv eq_jade_stream_chacha_chacha20_amd64_ref_xor_ct : M.jade_stream_chacha_chacha20_amd64_ref_xor ~ M.jade_stream_chacha_chacha20_amd64_ref_xor : - ={output, input, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={output, input, input_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. equiv eq_jade_stream_chacha_chacha20_amd64_ref_ct : M.jade_stream_chacha_chacha20_amd64_ref ~ M.jade_stream_chacha_chacha20_amd64_ref : - ={output, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={stream, stream_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_stream/salsa20/salsa20/amd64/avx/stream_ct_proof.ec b/proof/crypto_stream/salsa20/salsa20/amd64/avx/stream_ct_proof.ec index 87a82d4b..9d848589 100644 --- a/proof/crypto_stream/salsa20/salsa20/amd64/avx/stream_ct_proof.ec +++ b/proof/crypto_stream/salsa20/salsa20/amd64/avx/stream_ct_proof.ec @@ -2,14 +2,14 @@ require import Stream_ct. equiv eq_jade_stream_salsa20_salsa20_amd64_avx_xor_ct : M.jade_stream_salsa20_salsa20_amd64_avx_xor ~ M.jade_stream_salsa20_salsa20_amd64_avx_xor : - ={output, input, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={output, input, input_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. equiv eq_jade_stream_salsa20_salsa20_amd64_avx_ct : M.jade_stream_salsa20_salsa20_amd64_avx ~ M.jade_stream_salsa20_salsa20_amd64_avx : - ={output, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={stream, stream_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_stream/salsa20/salsa20/amd64/avx2/stream_ct_proof.ec b/proof/crypto_stream/salsa20/salsa20/amd64/avx2/stream_ct_proof.ec index fd5b4145..a5eb4f3f 100644 --- a/proof/crypto_stream/salsa20/salsa20/amd64/avx2/stream_ct_proof.ec +++ b/proof/crypto_stream/salsa20/salsa20/amd64/avx2/stream_ct_proof.ec @@ -2,14 +2,14 @@ require import Stream_ct. equiv eq_jade_stream_salsa20_salsa20_amd64_avx2_xor_ct : M.jade_stream_salsa20_salsa20_amd64_avx2_xor ~ M.jade_stream_salsa20_salsa20_amd64_avx2_xor : - ={output, input, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={output, input, input_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. equiv eq_jade_stream_salsa20_salsa20_amd64_avx2_ct : M.jade_stream_salsa20_salsa20_amd64_avx2 ~ M.jade_stream_salsa20_salsa20_amd64_avx2 : - ={output, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={stream, stream_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_stream/salsa20/salsa20/amd64/ref/stream_ct_proof.ec b/proof/crypto_stream/salsa20/salsa20/amd64/ref/stream_ct_proof.ec index a77e3509..6f7672fc 100644 --- a/proof/crypto_stream/salsa20/salsa20/amd64/ref/stream_ct_proof.ec +++ b/proof/crypto_stream/salsa20/salsa20/amd64/ref/stream_ct_proof.ec @@ -2,14 +2,14 @@ require import Stream_ct. equiv eq_jade_stream_salsa20_salsa20_amd64_ref_xor_ct : M.jade_stream_salsa20_salsa20_amd64_ref_xor ~ M.jade_stream_salsa20_salsa20_amd64_ref_xor : - ={output, input, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={output, input, input_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. equiv eq_jade_stream_salsa20_salsa20_amd64_ref_ct : M.jade_stream_salsa20_salsa20_amd64_ref ~ M.jade_stream_salsa20_salsa20_amd64_ref : - ={output, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={stream, stream_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_stream/salsa20/salsa2012/amd64/avx/stream_ct_proof.ec b/proof/crypto_stream/salsa20/salsa2012/amd64/avx/stream_ct_proof.ec index 6bcac2e8..fd331718 100644 --- a/proof/crypto_stream/salsa20/salsa2012/amd64/avx/stream_ct_proof.ec +++ b/proof/crypto_stream/salsa20/salsa2012/amd64/avx/stream_ct_proof.ec @@ -2,14 +2,14 @@ require import Stream_ct. equiv eq_jade_stream_salsa20_salsa2012_amd64_avx_xor_ct : M.jade_stream_salsa20_salsa2012_amd64_avx_xor ~ M.jade_stream_salsa20_salsa2012_amd64_avx_xor : - ={output, input, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={output, input, input_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. equiv eq_jade_stream_salsa20_salsa2012_amd64_avx_ct : M.jade_stream_salsa20_salsa2012_amd64_avx ~ M.jade_stream_salsa20_salsa2012_amd64_avx : - ={output, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={stream, stream_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_stream/salsa20/salsa2012/amd64/avx2/stream_ct_proof.ec b/proof/crypto_stream/salsa20/salsa2012/amd64/avx2/stream_ct_proof.ec index 1d06799a..e8a5a99f 100644 --- a/proof/crypto_stream/salsa20/salsa2012/amd64/avx2/stream_ct_proof.ec +++ b/proof/crypto_stream/salsa20/salsa2012/amd64/avx2/stream_ct_proof.ec @@ -2,14 +2,14 @@ require import Stream_ct. equiv eq_jade_stream_salsa20_salsa2012_amd64_avx2_xor_ct : M.jade_stream_salsa20_salsa2012_amd64_avx2_xor ~ M.jade_stream_salsa20_salsa2012_amd64_avx2_xor : - ={output, input, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={output, input, input_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. equiv eq_jade_stream_salsa20_salsa2012_amd64_avx2_ct : M.jade_stream_salsa20_salsa2012_amd64_avx2 ~ M.jade_stream_salsa20_salsa2012_amd64_avx2 : - ={output, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={stream, stream_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_stream/salsa20/salsa2012/amd64/ref/stream_ct_proof.ec b/proof/crypto_stream/salsa20/salsa2012/amd64/ref/stream_ct_proof.ec index da8758e1..11ec6abb 100644 --- a/proof/crypto_stream/salsa20/salsa2012/amd64/ref/stream_ct_proof.ec +++ b/proof/crypto_stream/salsa20/salsa2012/amd64/ref/stream_ct_proof.ec @@ -2,14 +2,14 @@ require import Stream_ct. equiv eq_jade_stream_salsa20_salsa2012_amd64_ref_xor_ct : M.jade_stream_salsa20_salsa2012_amd64_ref_xor ~ M.jade_stream_salsa20_salsa2012_amd64_ref_xor : - ={output, input, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={output, input, input_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. equiv eq_jade_stream_salsa20_salsa2012_amd64_ref_ct : M.jade_stream_salsa20_salsa2012_amd64_ref ~ M.jade_stream_salsa20_salsa2012_amd64_ref : - ={output, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={stream, stream_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_stream/xsalsa20/amd64/avx/stream_ct_proof.ec b/proof/crypto_stream/xsalsa20/amd64/avx/stream_ct_proof.ec index 496ad4de..cc732183 100644 --- a/proof/crypto_stream/xsalsa20/amd64/avx/stream_ct_proof.ec +++ b/proof/crypto_stream/xsalsa20/amd64/avx/stream_ct_proof.ec @@ -2,14 +2,14 @@ require import Stream_ct. equiv eq_jade_stream_xsalsa20_amd64_avx_xor_ct : M.jade_stream_xsalsa20_amd64_avx_xor ~ M.jade_stream_xsalsa20_amd64_avx_xor : - ={output, input, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={output, input, input_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. equiv eq_jade_stream_xsalsa20_amd64_avx_ct : M.jade_stream_xsalsa20_amd64_avx ~ M.jade_stream_xsalsa20_amd64_avx : - ={output, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={stream, stream_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_stream/xsalsa20/amd64/avx2/stream_ct_proof.ec b/proof/crypto_stream/xsalsa20/amd64/avx2/stream_ct_proof.ec index 3a12db28..a80443c7 100644 --- a/proof/crypto_stream/xsalsa20/amd64/avx2/stream_ct_proof.ec +++ b/proof/crypto_stream/xsalsa20/amd64/avx2/stream_ct_proof.ec @@ -2,14 +2,14 @@ require import Stream_ct. equiv eq_jade_stream_xsalsa20_amd64_avx2_xor_ct : M.jade_stream_xsalsa20_amd64_avx2_xor ~ M.jade_stream_xsalsa20_amd64_avx2_xor : - ={output, input, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={output, input, input_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. equiv eq_jade_stream_xsalsa20_amd64_avx2_ct : M.jade_stream_xsalsa20_amd64_avx2 ~ M.jade_stream_xsalsa20_amd64_avx2 : - ={output, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={stream, stream_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_stream/xsalsa20/amd64/ref/stream_ct_proof.ec b/proof/crypto_stream/xsalsa20/amd64/ref/stream_ct_proof.ec index 96f4f1e8..9f77b192 100644 --- a/proof/crypto_stream/xsalsa20/amd64/ref/stream_ct_proof.ec +++ b/proof/crypto_stream/xsalsa20/amd64/ref/stream_ct_proof.ec @@ -2,14 +2,14 @@ require import Stream_ct. equiv eq_jade_stream_xsalsa20_amd64_ref_xor_ct : M.jade_stream_xsalsa20_amd64_ref_xor ~ M.jade_stream_xsalsa20_amd64_ref_xor : - ={output, input, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={output, input, input_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. equiv eq_jade_stream_xsalsa20_amd64_ref_ct : M.jade_stream_xsalsa20_amd64_ref ~ M.jade_stream_xsalsa20_amd64_ref : - ={output, len, nonce, key, M.leakages} ==> ={M.leakages}. + ={stream, stream_length, nonce, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/src/crypto_stream/chacha/chacha12/amd64/avx/stream.jazz b/src/crypto_stream/chacha/chacha12/amd64/avx/stream.jazz index e8167324..54ea736b 100644 --- a/src/crypto_stream/chacha/chacha12/amd64/avx/stream.jazz +++ b/src/crypto_stream/chacha/chacha12/amd64/avx/stream.jazz @@ -2,18 +2,18 @@ param int CHACHA_ROUNDS=12; from Jade require "crypto_stream/chacha/common/amd64/avx/chacha.jinc" -export fn jade_stream_chacha_chacha12_amd64_avx_xor(reg u64 output input len nonce key) -> reg u64 +export fn jade_stream_chacha_chacha12_amd64_avx_xor(reg u64 output input input_length nonce key) -> reg u64 { reg u64 r; - __chacha_xor_avx(output, input, len, nonce, key); + __chacha_xor_avx(output, input, input_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } -export fn jade_stream_chacha_chacha12_amd64_avx(reg u64 output len nonce key) -> reg u64 +export fn jade_stream_chacha_chacha12_amd64_avx(reg u64 stream stream_length nonce key) -> reg u64 { reg u64 r; - __chacha_avx(output, len, nonce, key); + __chacha_avx(stream, stream_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_stream/chacha/chacha12/amd64/avx2/stream.jazz b/src/crypto_stream/chacha/chacha12/amd64/avx2/stream.jazz index ed1b9d8d..69b8105d 100644 --- a/src/crypto_stream/chacha/chacha12/amd64/avx2/stream.jazz +++ b/src/crypto_stream/chacha/chacha12/amd64/avx2/stream.jazz @@ -2,18 +2,18 @@ param int CHACHA_ROUNDS=12; from Jade require "crypto_stream/chacha/common/amd64/avx2/chacha.jinc" -export fn jade_stream_chacha_chacha12_amd64_avx2_xor(reg u64 output input len nonce key) -> reg u64 +export fn jade_stream_chacha_chacha12_amd64_avx2_xor(reg u64 output input input_length nonce key) -> reg u64 { reg u64 r; - __chacha_xor_avx2(output, input, len, nonce, key); + __chacha_xor_avx2(output, input, input_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } -export fn jade_stream_chacha_chacha12_amd64_avx2(reg u64 output len nonce key) -> reg u64 +export fn jade_stream_chacha_chacha12_amd64_avx2(reg u64 stream stream_length nonce key) -> reg u64 { reg u64 r; - __chacha_avx2(output, len, nonce, key); + __chacha_avx2(stream, stream_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_stream/chacha/chacha12/amd64/ref/stream.jazz b/src/crypto_stream/chacha/chacha12/amd64/ref/stream.jazz index d382d281..2a14aacc 100644 --- a/src/crypto_stream/chacha/chacha12/amd64/ref/stream.jazz +++ b/src/crypto_stream/chacha/chacha12/amd64/ref/stream.jazz @@ -2,18 +2,18 @@ param int CHACHA_ROUNDS=12; from Jade require "crypto_stream/chacha/common/amd64/ref/chacha.jinc" -export fn jade_stream_chacha_chacha12_amd64_ref_xor(reg u64 output input len nonce key) -> reg u64 +export fn jade_stream_chacha_chacha12_amd64_ref_xor(reg u64 output input input_length nonce key) -> reg u64 { reg u64 r; - __chacha_xor_ref(output, input, len, nonce, key); + __chacha_xor_ref(output, input, input_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } -export fn jade_stream_chacha_chacha12_amd64_ref(reg u64 output len nonce key) -> reg u64 +export fn jade_stream_chacha_chacha12_amd64_ref(reg u64 stream stream_length nonce key) -> reg u64 { reg u64 r; - __chacha_ref(output, len, nonce, key); + __chacha_ref(stream, stream_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_stream/chacha/chacha20-ietf/amd64/avx/stream.jazz b/src/crypto_stream/chacha/chacha20-ietf/amd64/avx/stream.jazz index 72d2bc0b..3fb8c9a0 100644 --- a/src/crypto_stream/chacha/chacha20-ietf/amd64/avx/stream.jazz +++ b/src/crypto_stream/chacha/chacha20-ietf/amd64/avx/stream.jazz @@ -12,36 +12,36 @@ from Jade require "crypto_stream/chacha/chacha20-ietf/amd64/avx/chacha_entry_v.j from Jade require "crypto_stream/chacha/chacha20-ietf/amd64/avx/_chacha.jinc" -export fn jade_stream_chacha_chacha20_ietf_amd64_avx_xor(reg u64 output input len nonce key) -> reg u64 +export fn jade_stream_chacha_chacha20_ietf_amd64_avx_xor(reg u64 output input input_length nonce key) -> reg u64 { reg u64 r; - __chacha_xor_avx(output, input, len, nonce, key); + __chacha_xor_avx(output, input, input_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } -export fn jade_stream_chacha_chacha20_ietf_amd64_avx(reg u64 output len nonce key) -> reg u64 +export fn jade_stream_chacha_chacha20_ietf_amd64_avx(reg u64 stream stream_length nonce key) -> reg u64 { reg u64 r; - __chacha_avx(output, len, nonce, key); + __chacha_avx(stream, stream_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } // -export fn jade_stream_chacha_chacha20_ietf_amd64_avx_xor_ic(reg u64 output input len nonce, reg u32 counter, reg u64 key) -> reg u64 +export fn jade_stream_chacha_chacha20_ietf_amd64_avx_xor_ic(reg u64 output input input_length nonce, reg u32 counter, reg u64 key) -> reg u64 { reg u64 r; - __chacha_xor_avx_ic(output, input, len, nonce, counter, key); + __chacha_xor_avx_ic(output, input, input_length, nonce, counter, key); _,_,_,_,_,r = #set0(); return r; } -export fn jade_stream_chacha_chacha20_ietf_amd64_avx_ic(reg u64 output len nonce, reg u32 counter, reg u64 key) -> reg u64 +export fn jade_stream_chacha_chacha20_ietf_amd64_avx_ic(reg u64 stream stream_length nonce, reg u32 counter, reg u64 key) -> reg u64 { reg u64 r; - __chacha_avx_ic(output, len, nonce, counter, key); + __chacha_avx_ic(stream, stream_length, nonce, counter, key); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_stream/chacha/chacha20-ietf/amd64/avx2/stream.jazz b/src/crypto_stream/chacha/chacha20-ietf/amd64/avx2/stream.jazz index f08c8d38..e0315562 100644 --- a/src/crypto_stream/chacha/chacha20-ietf/amd64/avx2/stream.jazz +++ b/src/crypto_stream/chacha/chacha20-ietf/amd64/avx2/stream.jazz @@ -12,36 +12,36 @@ from Jade require "crypto_stream/chacha/chacha20-ietf/amd64/avx2/chacha_entry_v. from Jade require "crypto_stream/chacha/chacha20-ietf/amd64/avx2/_chacha.jinc" -export fn jade_stream_chacha_chacha20_ietf_amd64_avx2_xor(reg u64 output input len nonce key) -> reg u64 +export fn jade_stream_chacha_chacha20_ietf_amd64_avx2_xor(reg u64 output input input_length nonce key) -> reg u64 { reg u64 r; - __chacha_xor_avx2(output, input, len, nonce, key); + __chacha_xor_avx2(output, input, input_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } -export fn jade_stream_chacha_chacha20_ietf_amd64_avx2(reg u64 output len nonce key) -> reg u64 +export fn jade_stream_chacha_chacha20_ietf_amd64_avx2(reg u64 stream stream_length nonce key) -> reg u64 { reg u64 r; - __chacha_avx2(output, len, nonce, key); + __chacha_avx2(stream, stream_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } // -export fn jade_stream_chacha_chacha20_ietf_amd64_avx2_xor_ic(reg u64 output input len nonce, reg u32 counter, reg u64 key) -> reg u64 +export fn jade_stream_chacha_chacha20_ietf_amd64_avx2_xor_ic(reg u64 output input input_length nonce, reg u32 counter, reg u64 key) -> reg u64 { reg u64 r; - __chacha_xor_avx2_ic(output, input, len, nonce, counter, key); + __chacha_xor_avx2_ic(output, input, input_length, nonce, counter, key); _,_,_,_,_,r = #set0(); return r; } -export fn jade_stream_chacha_chacha20_ietf_amd64_avx2_ic(reg u64 output len nonce, reg u32 counter, reg u64 key) -> reg u64 +export fn jade_stream_chacha_chacha20_ietf_amd64_avx2_ic(reg u64 stream stream_length nonce, reg u32 counter, reg u64 key) -> reg u64 { reg u64 r; - __chacha_avx2_ic(output, len, nonce, counter, key); + __chacha_avx2_ic(stream, stream_length, nonce, counter, key); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_stream/chacha/chacha20-ietf/amd64/ref/stream.jazz b/src/crypto_stream/chacha/chacha20-ietf/amd64/ref/stream.jazz index a4ea5443..5075fb6a 100644 --- a/src/crypto_stream/chacha/chacha20-ietf/amd64/ref/stream.jazz +++ b/src/crypto_stream/chacha/chacha20-ietf/amd64/ref/stream.jazz @@ -5,36 +5,36 @@ from Jade require "crypto_stream/chacha/common/amd64/ref/chacha_store.jinc" from Jade require "crypto_stream/chacha/common/amd64/ref/chacha_core.jinc" from Jade require "crypto_stream/chacha/chacha20-ietf/amd64/ref/chacha_entry.jinc" -export fn jade_stream_chacha_chacha20_ietf_amd64_ref_xor(reg u64 output input len nonce key) -> reg u64 +export fn jade_stream_chacha_chacha20_ietf_amd64_ref_xor(reg u64 output input input_length nonce key) -> reg u64 { reg u64 r; - __chacha_xor_ref(output, input, len, nonce, key); + __chacha_xor_ref(output, input, input_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } -export fn jade_stream_chacha_chacha20_ietf_amd64_ref(reg u64 output len nonce key) -> reg u64 +export fn jade_stream_chacha_chacha20_ietf_amd64_ref(reg u64 stream stream_length nonce key) -> reg u64 { reg u64 r; - __chacha_ref(output, len, nonce, key); + __chacha_ref(stream, stream_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } // -export fn jade_stream_chacha_chacha20_ietf_amd64_ref_xor_ic(reg u64 output input len nonce, reg u32 counter, reg u64 key) -> reg u64 +export fn jade_stream_chacha_chacha20_ietf_amd64_ref_xor_ic(reg u64 output input input_length nonce, reg u32 counter, reg u64 key) -> reg u64 { reg u64 r; - _chacha_xor_ref_ic_(output, input, len, nonce, counter, key); + _chacha_xor_ref_ic_(output, input, input_length, nonce, counter, key); _,_,_,_,_,r = #set0(); return r; } -export fn jade_stream_chacha_chacha20_ietf_amd64_ref_ic(reg u64 output len nonce, reg u32 counter, reg u64 key) -> reg u64 +export fn jade_stream_chacha_chacha20_ietf_amd64_ref_ic(reg u64 stream stream_length nonce, reg u32 counter, reg u64 key) -> reg u64 { reg u64 r; - _chacha_ref_ic_(output, len, nonce, counter, key); + _chacha_ref_ic_(stream, stream_length, nonce, counter, key); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_stream/chacha/chacha20/amd64/avx/stream.jazz b/src/crypto_stream/chacha/chacha20/amd64/avx/stream.jazz index 74c2c3c0..caa889c0 100644 --- a/src/crypto_stream/chacha/chacha20/amd64/avx/stream.jazz +++ b/src/crypto_stream/chacha/chacha20/amd64/avx/stream.jazz @@ -2,18 +2,18 @@ param int CHACHA_ROUNDS=20; from Jade require "crypto_stream/chacha/common/amd64/avx/chacha.jinc" -export fn jade_stream_chacha_chacha20_amd64_avx_xor(reg u64 output input len nonce key) -> reg u64 +export fn jade_stream_chacha_chacha20_amd64_avx_xor(reg u64 output input input_length nonce key) -> reg u64 { reg u64 r; - __chacha_xor_avx(output, input, len, nonce, key); + __chacha_xor_avx(output, input, input_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } -export fn jade_stream_chacha_chacha20_amd64_avx(reg u64 output len nonce key) -> reg u64 +export fn jade_stream_chacha_chacha20_amd64_avx(reg u64 stream stream_length nonce key) -> reg u64 { reg u64 r; - __chacha_avx(output, len, nonce, key); + __chacha_avx(stream, stream_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_stream/chacha/chacha20/amd64/avx2/stream.jazz b/src/crypto_stream/chacha/chacha20/amd64/avx2/stream.jazz index f3d079ab..ce309fb4 100644 --- a/src/crypto_stream/chacha/chacha20/amd64/avx2/stream.jazz +++ b/src/crypto_stream/chacha/chacha20/amd64/avx2/stream.jazz @@ -2,18 +2,18 @@ param int CHACHA_ROUNDS=20; from Jade require "crypto_stream/chacha/common/amd64/avx2/chacha.jinc" -export fn jade_stream_chacha_chacha20_amd64_avx2_xor(reg u64 output input len nonce key) -> reg u64 +export fn jade_stream_chacha_chacha20_amd64_avx2_xor(reg u64 output input input_length nonce key) -> reg u64 { reg u64 r; - __chacha_xor_avx2(output, input, len, nonce, key); + __chacha_xor_avx2(output, input, input_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } -export fn jade_stream_chacha_chacha20_amd64_avx2(reg u64 output len nonce key) -> reg u64 +export fn jade_stream_chacha_chacha20_amd64_avx2(reg u64 stream stream_length nonce key) -> reg u64 { reg u64 r; - __chacha_avx2(output, len, nonce, key); + __chacha_avx2(stream, stream_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_stream/chacha/chacha20/amd64/ref/stream.jazz b/src/crypto_stream/chacha/chacha20/amd64/ref/stream.jazz index 6b4b57a4..7d211ba5 100644 --- a/src/crypto_stream/chacha/chacha20/amd64/ref/stream.jazz +++ b/src/crypto_stream/chacha/chacha20/amd64/ref/stream.jazz @@ -2,18 +2,18 @@ param int CHACHA_ROUNDS=20; from Jade require "crypto_stream/chacha/common/amd64/ref/chacha.jinc" -export fn jade_stream_chacha_chacha20_amd64_ref_xor(reg u64 output input len nonce key) -> reg u64 +export fn jade_stream_chacha_chacha20_amd64_ref_xor(reg u64 output input input_length nonce key) -> reg u64 { reg u64 r; - __chacha_xor_ref(output, input, len, nonce, key); + __chacha_xor_ref(output, input, input_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } -export fn jade_stream_chacha_chacha20_amd64_ref(reg u64 output len nonce key) -> reg u64 +export fn jade_stream_chacha_chacha20_amd64_ref(reg u64 stream stream_length nonce key) -> reg u64 { reg u64 r; - __chacha_ref(output, len, nonce, key); + __chacha_ref(stream, stream_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_stream/salsa20/salsa20/amd64/avx/stream.jazz b/src/crypto_stream/salsa20/salsa20/amd64/avx/stream.jazz index ed053934..ca074b01 100644 --- a/src/crypto_stream/salsa20/salsa20/amd64/avx/stream.jazz +++ b/src/crypto_stream/salsa20/salsa20/amd64/avx/stream.jazz @@ -2,18 +2,18 @@ param int SALSA20_ROUNDS=20; from Jade require "crypto_stream/salsa20/common/amd64/avx/salsa20.jinc" -export fn jade_stream_salsa20_salsa20_amd64_avx_xor(reg u64 output input len nonce key) -> reg u64 +export fn jade_stream_salsa20_salsa20_amd64_avx_xor(reg u64 output input input_length nonce key) -> reg u64 { reg u64 r; - __salsa20_xor_avx(output, input, len, nonce, key); + __salsa20_xor_avx(output, input, input_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } -export fn jade_stream_salsa20_salsa20_amd64_avx(reg u64 output len nonce key) -> reg u64 +export fn jade_stream_salsa20_salsa20_amd64_avx(reg u64 stream stream_length nonce key) -> reg u64 { reg u64 r; - __salsa20_avx(output, len, nonce, key); + __salsa20_avx(stream, stream_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_stream/salsa20/salsa20/amd64/avx2/stream.jazz b/src/crypto_stream/salsa20/salsa20/amd64/avx2/stream.jazz index b67d64f2..b3d971ad 100644 --- a/src/crypto_stream/salsa20/salsa20/amd64/avx2/stream.jazz +++ b/src/crypto_stream/salsa20/salsa20/amd64/avx2/stream.jazz @@ -2,18 +2,18 @@ param int SALSA20_ROUNDS=20; from Jade require "crypto_stream/salsa20/common/amd64/avx2/salsa20.jinc" -export fn jade_stream_salsa20_salsa20_amd64_avx2_xor(reg u64 output input len nonce key) -> reg u64 +export fn jade_stream_salsa20_salsa20_amd64_avx2_xor(reg u64 output input input_length nonce key) -> reg u64 { reg u64 r; - __salsa20_xor_avx2(output, input, len, nonce, key); + __salsa20_xor_avx2(output, input, input_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } -export fn jade_stream_salsa20_salsa20_amd64_avx2(reg u64 output len nonce key) -> reg u64 +export fn jade_stream_salsa20_salsa20_amd64_avx2(reg u64 stream stream_length nonce key) -> reg u64 { reg u64 r; - __salsa20_avx2(output, len, nonce, key); + __salsa20_avx2(stream, stream_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_stream/salsa20/salsa20/amd64/ref/stream.jazz b/src/crypto_stream/salsa20/salsa20/amd64/ref/stream.jazz index 3fa2ca29..7c259827 100644 --- a/src/crypto_stream/salsa20/salsa20/amd64/ref/stream.jazz +++ b/src/crypto_stream/salsa20/salsa20/amd64/ref/stream.jazz @@ -2,18 +2,19 @@ param int SALSA20_ROUNDS=20; from Jade require "crypto_stream/salsa20/common/amd64/ref/salsa20.jinc" -export fn jade_stream_salsa20_salsa20_amd64_ref_xor(reg u64 output input len nonce key) -> reg u64 +export fn jade_stream_salsa20_salsa20_amd64_ref_xor(reg u64 output input input_length nonce key) -> reg u64 { reg u64 r; - __salsa20_xor_ref(output, input, len, nonce, key); + __salsa20_xor_ref(output, input, input_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } -export fn jade_stream_salsa20_salsa20_amd64_ref(reg u64 output len nonce key) -> reg u64 +export fn jade_stream_salsa20_salsa20_amd64_ref(reg u64 stream stream_length nonce key) -> reg u64 { reg u64 r; - __salsa20_ref(output, len, nonce, key); + __salsa20_ref(stream, stream_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } + diff --git a/src/crypto_stream/salsa20/salsa2012/amd64/avx/stream.jazz b/src/crypto_stream/salsa20/salsa2012/amd64/avx/stream.jazz index 350cde33..d0bfae9d 100644 --- a/src/crypto_stream/salsa20/salsa2012/amd64/avx/stream.jazz +++ b/src/crypto_stream/salsa20/salsa2012/amd64/avx/stream.jazz @@ -2,19 +2,19 @@ param int SALSA20_ROUNDS=12; from Jade require "crypto_stream/salsa20/common/amd64/avx/salsa20.jinc" -export fn jade_stream_salsa20_salsa2012_amd64_avx_xor(reg u64 output input len nonce key) -> reg u64 +export fn jade_stream_salsa20_salsa2012_amd64_avx_xor(reg u64 output input input_length nonce key) -> reg u64 { reg u64 r; - __salsa20_xor_avx(output, input, len, nonce, key); + __salsa20_xor_avx(output, input, input_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } -export fn jade_stream_salsa20_salsa2012_amd64_avx(reg u64 output len nonce key) -> reg u64 +export fn jade_stream_salsa20_salsa2012_amd64_avx(reg u64 stream stream_length nonce key) -> reg u64 { reg u64 r; - __salsa20_avx(output, len, nonce, key); + __salsa20_avx(stream, stream_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_stream/salsa20/salsa2012/amd64/avx2/stream.jazz b/src/crypto_stream/salsa20/salsa2012/amd64/avx2/stream.jazz index a144856b..2bdd27ee 100644 --- a/src/crypto_stream/salsa20/salsa2012/amd64/avx2/stream.jazz +++ b/src/crypto_stream/salsa20/salsa2012/amd64/avx2/stream.jazz @@ -2,18 +2,18 @@ param int SALSA20_ROUNDS=12; from Jade require "crypto_stream/salsa20/common/amd64/avx2/salsa20.jinc" -export fn jade_stream_salsa20_salsa2012_amd64_avx2_xor(reg u64 output input len nonce key) -> reg u64 +export fn jade_stream_salsa20_salsa2012_amd64_avx2_xor(reg u64 output input input_length nonce key) -> reg u64 { reg u64 r; - __salsa20_xor_avx2(output, input, len, nonce, key); + __salsa20_xor_avx2(output, input, input_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } -export fn jade_stream_salsa20_salsa2012_amd64_avx2(reg u64 output len nonce key) -> reg u64 +export fn jade_stream_salsa20_salsa2012_amd64_avx2(reg u64 stream stream_length nonce key) -> reg u64 { reg u64 r; - __salsa20_avx2(output, len, nonce, key); + __salsa20_avx2(stream, stream_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_stream/salsa20/salsa2012/amd64/ref/stream.jazz b/src/crypto_stream/salsa20/salsa2012/amd64/ref/stream.jazz index 9747c8c7..ed8d210d 100644 --- a/src/crypto_stream/salsa20/salsa2012/amd64/ref/stream.jazz +++ b/src/crypto_stream/salsa20/salsa2012/amd64/ref/stream.jazz @@ -2,18 +2,18 @@ param int SALSA20_ROUNDS=12; from Jade require "crypto_stream/salsa20/common/amd64/ref/salsa20.jinc" -export fn jade_stream_salsa20_salsa2012_amd64_ref_xor(reg u64 output input len nonce key) -> reg u64 +export fn jade_stream_salsa20_salsa2012_amd64_ref_xor(reg u64 output input input_length nonce key) -> reg u64 { reg u64 r; - __salsa20_xor_ref(output, input, len, nonce, key); + __salsa20_xor_ref(output, input, input_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } -export fn jade_stream_salsa20_salsa2012_amd64_ref(reg u64 output len nonce key) -> reg u64 +export fn jade_stream_salsa20_salsa2012_amd64_ref(reg u64 stream stream_length nonce key) -> reg u64 { reg u64 r; - __salsa20_ref(output, len, nonce, key); + __salsa20_ref(stream, stream_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_stream/xsalsa20/amd64/avx/stream.jazz b/src/crypto_stream/xsalsa20/amd64/avx/stream.jazz index cdeae29f..03c090a1 100644 --- a/src/crypto_stream/xsalsa20/amd64/avx/stream.jazz +++ b/src/crypto_stream/xsalsa20/amd64/avx/stream.jazz @@ -1,17 +1,17 @@ require "xsalsa20.jinc" -export fn jade_stream_xsalsa20_amd64_avx_xor(reg u64 output input len nonce key) -> reg u64 +export fn jade_stream_xsalsa20_amd64_avx_xor(reg u64 output input input_length nonce key) -> reg u64 { reg u64 r; - __xsalsa20_xor_avx(output, input, len, nonce, key); + __xsalsa20_xor_avx(output, input, input_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } -export fn jade_stream_xsalsa20_amd64_avx(reg u64 output len nonce key) -> reg u64 +export fn jade_stream_xsalsa20_amd64_avx(reg u64 stream stream_length nonce key) -> reg u64 { reg u64 r; - __xsalsa20_avx(output, len, nonce, key); + __xsalsa20_avx(stream, stream_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_stream/xsalsa20/amd64/avx2/stream.jazz b/src/crypto_stream/xsalsa20/amd64/avx2/stream.jazz index d9e1c349..bdf46663 100644 --- a/src/crypto_stream/xsalsa20/amd64/avx2/stream.jazz +++ b/src/crypto_stream/xsalsa20/amd64/avx2/stream.jazz @@ -1,17 +1,17 @@ require "xsalsa20.jinc" -export fn jade_stream_xsalsa20_amd64_avx2_xor(reg u64 output input len nonce key) -> reg u64 +export fn jade_stream_xsalsa20_amd64_avx2_xor(reg u64 output input input_length nonce key) -> reg u64 { reg u64 r; - __xsalsa20_xor_avx2(output, input, len, nonce, key); + __xsalsa20_xor_avx2(output, input, input_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } -export fn jade_stream_xsalsa20_amd64_avx2(reg u64 output len nonce key) -> reg u64 +export fn jade_stream_xsalsa20_amd64_avx2(reg u64 stream stream_length nonce key) -> reg u64 { reg u64 r; - __xsalsa20_avx2(output, len, nonce, key); + __xsalsa20_avx2(stream, stream_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_stream/xsalsa20/amd64/ref/stream.jazz b/src/crypto_stream/xsalsa20/amd64/ref/stream.jazz index 5e6f374a..f067a499 100644 --- a/src/crypto_stream/xsalsa20/amd64/ref/stream.jazz +++ b/src/crypto_stream/xsalsa20/amd64/ref/stream.jazz @@ -1,17 +1,17 @@ require "xsalsa20.jinc" -export fn jade_stream_xsalsa20_amd64_ref_xor(reg u64 output input len nonce key) -> reg u64 +export fn jade_stream_xsalsa20_amd64_ref_xor(reg u64 output input input_length nonce key) -> reg u64 { reg u64 r; - __xsalsa20_xor_ref(output, input, len, nonce, key); + __xsalsa20_xor_ref(output, input, input_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } -export fn jade_stream_xsalsa20_amd64_ref(reg u64 output len nonce key) -> reg u64 +export fn jade_stream_xsalsa20_amd64_ref(reg u64 stream stream_length nonce key) -> reg u64 { reg u64 r; - __xsalsa20_ref(output, len, nonce, key); + __xsalsa20_ref(stream, stream_length, nonce, key); _,_,_,_,_,r = #set0(); return r; } From e592dd6ce7de56c485e39d9e8dd14a36f3e8464f Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Mon, 5 Dec 2022 17:19:09 +0000 Subject: [PATCH 2/9] crypto stream : add chacha20 ietf _ic variants to the extraction and ct proofs --- .../chacha20-ietf/amd64/avx/stream_ct_proof.ec | 17 +++++++++++++++++ .../chacha20-ietf/amd64/avx2/stream_ct_proof.ec | 16 ++++++++++++++++ .../chacha20-ietf/amd64/ref/stream_ct_proof.ec | 16 ++++++++++++++++ .../chacha/chacha20-ietf/amd64/avx/Makefile | 1 + .../chacha/chacha20-ietf/amd64/avx2/Makefile | 1 + .../chacha/chacha20-ietf/amd64/ref/Makefile | 1 + 6 files changed, 52 insertions(+) diff --git a/proof/crypto_stream/chacha/chacha20-ietf/amd64/avx/stream_ct_proof.ec b/proof/crypto_stream/chacha/chacha20-ietf/amd64/avx/stream_ct_proof.ec index b67f280d..5bc7c5fe 100644 --- a/proof/crypto_stream/chacha/chacha20-ietf/amd64/avx/stream_ct_proof.ec +++ b/proof/crypto_stream/chacha/chacha20-ietf/amd64/avx/stream_ct_proof.ec @@ -13,3 +13,20 @@ equiv eq_jade_stream_chacha_chacha20_ietf_amd64_avx_ct : proof. proc; inline *; sim => />. qed. + +(** **) + +equiv eq_jade_stream_chacha_chacha20_ietf_amd64_avx_xor_ic_ct : + M.jade_stream_chacha_chacha20_ietf_amd64_avx_xor_ic ~ M.jade_stream_chacha_chacha20_ietf_amd64_avx_xor_ic : + ={output, input, input_length, nonce, key, M.leakages} ==> ={M.leakages}. +proof. +proc; inline *; sim => />. +qed. + +equiv eq_jade_stream_chacha_chacha20_ietf_amd64_avx_ic_ct : + M.jade_stream_chacha_chacha20_ietf_amd64_avx_ic ~ M.jade_stream_chacha_chacha20_ietf_amd64_avx_ic : + ={stream, stream_length, nonce, key, M.leakages} ==> ={M.leakages}. +proof. +proc; inline *; sim => />. +qed. + diff --git a/proof/crypto_stream/chacha/chacha20-ietf/amd64/avx2/stream_ct_proof.ec b/proof/crypto_stream/chacha/chacha20-ietf/amd64/avx2/stream_ct_proof.ec index 1ecb2bd5..234a471b 100644 --- a/proof/crypto_stream/chacha/chacha20-ietf/amd64/avx2/stream_ct_proof.ec +++ b/proof/crypto_stream/chacha/chacha20-ietf/amd64/avx2/stream_ct_proof.ec @@ -13,3 +13,19 @@ equiv eq_jade_stream_chacha_chacha20_ietf_amd64_avx2_ct : proof. proc; inline *; sim => />. qed. + +(** **) + +equiv eq_jade_stream_chacha_chacha20_ietf_amd64_avx2_xor_ic_ct : + M.jade_stream_chacha_chacha20_ietf_amd64_avx2_xor_ic ~ M.jade_stream_chacha_chacha20_ietf_amd64_avx2_xor_ic : + ={output, input, input_length, nonce, key, M.leakages} ==> ={M.leakages}. +proof. +proc; inline *; sim => />. +qed. + +equiv eq_jade_stream_chacha_chacha20_ietf_amd64_avx2_ic_ct : + M.jade_stream_chacha_chacha20_ietf_amd64_avx2_ic ~ M.jade_stream_chacha_chacha20_ietf_amd64_avx2_ic : + ={stream, stream_length, nonce, key, M.leakages} ==> ={M.leakages}. +proof. +proc; inline *; sim => />. +qed. diff --git a/proof/crypto_stream/chacha/chacha20-ietf/amd64/ref/stream_ct_proof.ec b/proof/crypto_stream/chacha/chacha20-ietf/amd64/ref/stream_ct_proof.ec index 7ac8fe29..f64bb187 100644 --- a/proof/crypto_stream/chacha/chacha20-ietf/amd64/ref/stream_ct_proof.ec +++ b/proof/crypto_stream/chacha/chacha20-ietf/amd64/ref/stream_ct_proof.ec @@ -13,3 +13,19 @@ equiv eq_jade_stream_chacha_chacha20_ietf_amd64_ref_ct : proof. proc; inline *; sim => />. qed. + +(** **) + +equiv eq_jade_stream_chacha_chacha20_ietf_amd64_ref_xor_ic_ct : + M.jade_stream_chacha_chacha20_ietf_amd64_ref_xor_ic ~ M.jade_stream_chacha_chacha20_ietf_amd64_ref_xor_ic : + ={output, input, input_length, nonce, key, M.leakages} ==> ={M.leakages}. +proof. +proc; inline *; sim => />. +qed. + +equiv eq_jade_stream_chacha_chacha20_ietf_amd64_ref_ic_ct : + M.jade_stream_chacha_chacha20_ietf_amd64_ref_ic ~ M.jade_stream_chacha_chacha20_ietf_amd64_ref_ic : + ={stream, stream_length, nonce, key, M.leakages} ==> ={M.leakages}. +proof. +proc; inline *; sim => />. +qed. diff --git a/src/crypto_stream/chacha/chacha20-ietf/amd64/avx/Makefile b/src/crypto_stream/chacha/chacha20-ietf/amd64/avx/Makefile index f248cf79..93b730ec 100644 --- a/src/crypto_stream/chacha/chacha20-ietf/amd64/avx/Makefile +++ b/src/crypto_stream/chacha/chacha20-ietf/amd64/avx/Makefile @@ -1,3 +1,4 @@ +ECFN := -ec namespace -ec namespace_xor -ec namespace_ic -ec namespace_xor_ic SRCS := stream.jazz include ../../../../../crypto_stream/chacha/common/amd64/avx/Flags.mk include ../../../../../Makefile.common diff --git a/src/crypto_stream/chacha/chacha20-ietf/amd64/avx2/Makefile b/src/crypto_stream/chacha/chacha20-ietf/amd64/avx2/Makefile index 7d4186cd..a8f2d37c 100644 --- a/src/crypto_stream/chacha/chacha20-ietf/amd64/avx2/Makefile +++ b/src/crypto_stream/chacha/chacha20-ietf/amd64/avx2/Makefile @@ -1,3 +1,4 @@ +ECFN := -ec namespace -ec namespace_xor -ec namespace_ic -ec namespace_xor_ic SRCS := stream.jazz include ../../../../../crypto_stream/chacha/common/amd64/avx2/Flags.mk include ../../../../../Makefile.common diff --git a/src/crypto_stream/chacha/chacha20-ietf/amd64/ref/Makefile b/src/crypto_stream/chacha/chacha20-ietf/amd64/ref/Makefile index 2cac2294..4184a079 100644 --- a/src/crypto_stream/chacha/chacha20-ietf/amd64/ref/Makefile +++ b/src/crypto_stream/chacha/chacha20-ietf/amd64/ref/Makefile @@ -1,2 +1,3 @@ +ECFN := -ec namespace -ec namespace_xor -ec namespace_ic -ec namespace_xor_ic SRCS := stream.jazz include ../../../../../Makefile.common From 16de60ca007155b567fc073c578eb99857b96744 Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Mon, 5 Dec 2022 17:40:01 +0000 Subject: [PATCH 3/9] args naming : crypto_hash pass --- proof/crypto_hash/sha256/amd64/ref/hash_ct_proof.ec | 2 +- proof/crypto_hash/sha3-224/amd64/avx2/hash_ct_proof.ec | 2 +- proof/crypto_hash/sha3-224/amd64/ref/hash_ct_proof.ec | 2 +- proof/crypto_hash/sha3-256/amd64/avx2/hash_ct_proof.ec | 2 +- proof/crypto_hash/sha3-256/amd64/ref/hash_ct_proof.ec | 2 +- proof/crypto_hash/sha3-384/amd64/avx2/hash_ct_proof.ec | 2 +- proof/crypto_hash/sha3-384/amd64/ref/hash_ct_proof.ec | 2 +- proof/crypto_hash/sha3-512/amd64/avx2/hash_ct_proof.ec | 2 +- proof/crypto_hash/sha3-512/amd64/ref/hash_ct_proof.ec | 2 +- proof/crypto_hash/sha512/amd64/ref/hash_ct_proof.ec | 2 +- src/crypto_hash/sha256/amd64/ref/hash.jazz | 4 ++-- src/crypto_hash/sha3-224/amd64/avx2/hash.jazz | 4 ++-- src/crypto_hash/sha3-224/amd64/ref/hash.jazz | 4 ++-- src/crypto_hash/sha3-256/amd64/avx2/hash.jazz | 4 ++-- src/crypto_hash/sha3-256/amd64/ref/hash.jazz | 4 ++-- src/crypto_hash/sha3-384/amd64/avx2/hash.jazz | 4 ++-- src/crypto_hash/sha3-384/amd64/ref/hash.jazz | 4 ++-- src/crypto_hash/sha3-512/amd64/avx2/hash.jazz | 4 ++-- src/crypto_hash/sha3-512/amd64/ref/hash.jazz | 4 ++-- src/crypto_hash/sha512/amd64/ref/hash.jazz | 4 ++-- 20 files changed, 30 insertions(+), 30 deletions(-) diff --git a/proof/crypto_hash/sha256/amd64/ref/hash_ct_proof.ec b/proof/crypto_hash/sha256/amd64/ref/hash_ct_proof.ec index b8089741..29addcff 100644 --- a/proof/crypto_hash/sha256/amd64/ref/hash_ct_proof.ec +++ b/proof/crypto_hash/sha256/amd64/ref/hash_ct_proof.ec @@ -2,7 +2,7 @@ require import Hash_ct. equiv eq_jade_hash_sha256_amd64_ref_ct : M.jade_hash_sha256_amd64_ref ~ M.jade_hash_sha256_amd64_ref : - ={out, in_0, inlen, M.leakages} ==> ={M.leakages}. + ={hash, input, input_length, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_hash/sha3-224/amd64/avx2/hash_ct_proof.ec b/proof/crypto_hash/sha3-224/amd64/avx2/hash_ct_proof.ec index c6073ee3..2df708e8 100644 --- a/proof/crypto_hash/sha3-224/amd64/avx2/hash_ct_proof.ec +++ b/proof/crypto_hash/sha3-224/amd64/avx2/hash_ct_proof.ec @@ -2,7 +2,7 @@ require import Hash_ct. equiv eq_jade_hash_sha3_224_amd64_avx2_ct : M.jade_hash_sha3_224_amd64_avx2 ~ M.jade_hash_sha3_224_amd64_avx2 : - ={out, in_0, inlen, M.leakages} ==> ={M.leakages}. + ={hash, input, input_length, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_hash/sha3-224/amd64/ref/hash_ct_proof.ec b/proof/crypto_hash/sha3-224/amd64/ref/hash_ct_proof.ec index 415ec41e..b587180b 100644 --- a/proof/crypto_hash/sha3-224/amd64/ref/hash_ct_proof.ec +++ b/proof/crypto_hash/sha3-224/amd64/ref/hash_ct_proof.ec @@ -2,7 +2,7 @@ require import Hash_ct. equiv eq_jade_hash_sha3_224_amd64_ref_ct : M.jade_hash_sha3_224_amd64_ref ~ M.jade_hash_sha3_224_amd64_ref : - ={out, in_0, inlen, M.leakages} ==> ={M.leakages}. + ={hash, input, input_length, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_hash/sha3-256/amd64/avx2/hash_ct_proof.ec b/proof/crypto_hash/sha3-256/amd64/avx2/hash_ct_proof.ec index 10c660ae..31cd62f3 100644 --- a/proof/crypto_hash/sha3-256/amd64/avx2/hash_ct_proof.ec +++ b/proof/crypto_hash/sha3-256/amd64/avx2/hash_ct_proof.ec @@ -2,7 +2,7 @@ require import Hash_ct. equiv eq_jade_hash_sha3_256_amd64_avx2_ct : M.jade_hash_sha3_256_amd64_avx2 ~ M.jade_hash_sha3_256_amd64_avx2 : - ={out, in_0, inlen, M.leakages} ==> ={M.leakages}. + ={hash, input, input_length, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_hash/sha3-256/amd64/ref/hash_ct_proof.ec b/proof/crypto_hash/sha3-256/amd64/ref/hash_ct_proof.ec index 94d1fdaf..c71026e9 100644 --- a/proof/crypto_hash/sha3-256/amd64/ref/hash_ct_proof.ec +++ b/proof/crypto_hash/sha3-256/amd64/ref/hash_ct_proof.ec @@ -2,7 +2,7 @@ require import Hash_ct. equiv eq_jade_hash_sha3_256_amd64_ref_ct : M.jade_hash_sha3_256_amd64_ref ~ M.jade_hash_sha3_256_amd64_ref : - ={out, in_0, inlen, M.leakages} ==> ={M.leakages}. + ={hash, input, input_length, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_hash/sha3-384/amd64/avx2/hash_ct_proof.ec b/proof/crypto_hash/sha3-384/amd64/avx2/hash_ct_proof.ec index 29d7d0c6..34fd8334 100644 --- a/proof/crypto_hash/sha3-384/amd64/avx2/hash_ct_proof.ec +++ b/proof/crypto_hash/sha3-384/amd64/avx2/hash_ct_proof.ec @@ -2,7 +2,7 @@ require import Hash_ct. equiv eq_jade_hash_sha3_384_amd64_avx2_ct : M.jade_hash_sha3_384_amd64_avx2 ~ M.jade_hash_sha3_384_amd64_avx2 : - ={out, in_0, inlen, M.leakages} ==> ={M.leakages}. + ={hash, input, input_length, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_hash/sha3-384/amd64/ref/hash_ct_proof.ec b/proof/crypto_hash/sha3-384/amd64/ref/hash_ct_proof.ec index 3f8a2073..c868a5aa 100644 --- a/proof/crypto_hash/sha3-384/amd64/ref/hash_ct_proof.ec +++ b/proof/crypto_hash/sha3-384/amd64/ref/hash_ct_proof.ec @@ -2,7 +2,7 @@ require import Hash_ct. equiv eq_jade_hash_sha3_384_amd64_ref_ct : M.jade_hash_sha3_384_amd64_ref ~ M.jade_hash_sha3_384_amd64_ref : - ={out, in_0, inlen, M.leakages} ==> ={M.leakages}. + ={hash, input, input_length, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_hash/sha3-512/amd64/avx2/hash_ct_proof.ec b/proof/crypto_hash/sha3-512/amd64/avx2/hash_ct_proof.ec index 5470737e..a32b33ba 100644 --- a/proof/crypto_hash/sha3-512/amd64/avx2/hash_ct_proof.ec +++ b/proof/crypto_hash/sha3-512/amd64/avx2/hash_ct_proof.ec @@ -2,7 +2,7 @@ require import Hash_ct. equiv eq_jade_hash_sha3_512_amd64_avx2_ct : M.jade_hash_sha3_512_amd64_avx2 ~ M.jade_hash_sha3_512_amd64_avx2 : - ={out, in_0, inlen, M.leakages} ==> ={M.leakages}. + ={hash, input, input_length, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_hash/sha3-512/amd64/ref/hash_ct_proof.ec b/proof/crypto_hash/sha3-512/amd64/ref/hash_ct_proof.ec index 9cb2e3f5..a4ab9c03 100644 --- a/proof/crypto_hash/sha3-512/amd64/ref/hash_ct_proof.ec +++ b/proof/crypto_hash/sha3-512/amd64/ref/hash_ct_proof.ec @@ -2,7 +2,7 @@ require import Hash_ct. equiv eq_jade_hash_sha3_512_amd64_ref_ct : M.jade_hash_sha3_512_amd64_ref ~ M.jade_hash_sha3_512_amd64_ref : - ={out, in_0, inlen, M.leakages} ==> ={M.leakages}. + ={hash, input, input_length, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_hash/sha512/amd64/ref/hash_ct_proof.ec b/proof/crypto_hash/sha512/amd64/ref/hash_ct_proof.ec index b135c953..684d723a 100644 --- a/proof/crypto_hash/sha512/amd64/ref/hash_ct_proof.ec +++ b/proof/crypto_hash/sha512/amd64/ref/hash_ct_proof.ec @@ -2,7 +2,7 @@ require import Hash_ct. equiv eq_jade_hash_sha512_amd64_ref_ct : M.jade_hash_sha512_amd64_ref ~ M.jade_hash_sha512_amd64_ref : - ={out, in_0, inlen, M.leakages} ==> ={M.leakages}. + ={hash, input, input_length, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/src/crypto_hash/sha256/amd64/ref/hash.jazz b/src/crypto_hash/sha256/amd64/ref/hash.jazz index fad8e548..8a42629b 100644 --- a/src/crypto_hash/sha256/amd64/ref/hash.jazz +++ b/src/crypto_hash/sha256/amd64/ref/hash.jazz @@ -1,9 +1,9 @@ require "sha256.jinc" -export fn jade_hash_sha256_amd64_ref(reg u64 out in inlen) -> reg u64 +export fn jade_hash_sha256_amd64_ref(reg u64 hash input input_length) -> reg u64 { reg u64 r; - __sha256(out, in, inlen); + __sha256(hash, input, input_length); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_hash/sha3-224/amd64/avx2/hash.jazz b/src/crypto_hash/sha3-224/amd64/avx2/hash.jazz index 9d2a9477..9ddc32db 100644 --- a/src/crypto_hash/sha3-224/amd64/avx2/hash.jazz +++ b/src/crypto_hash/sha3-224/amd64/avx2/hash.jazz @@ -1,9 +1,9 @@ require "sha3-224.jinc" -export fn jade_hash_sha3_224_amd64_avx2(reg u64 out in inlen) -> reg u64 +export fn jade_hash_sha3_224_amd64_avx2(reg u64 hash input input_length) -> reg u64 { reg u64 r; - __sha3_224_avx2(out, in, inlen); + __sha3_224_avx2(hash, input, input_length); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_hash/sha3-224/amd64/ref/hash.jazz b/src/crypto_hash/sha3-224/amd64/ref/hash.jazz index 30db921e..2dcfe49a 100644 --- a/src/crypto_hash/sha3-224/amd64/ref/hash.jazz +++ b/src/crypto_hash/sha3-224/amd64/ref/hash.jazz @@ -1,9 +1,9 @@ require "sha3-224.jinc" -export fn jade_hash_sha3_224_amd64_ref(reg u64 out in inlen) -> reg u64 +export fn jade_hash_sha3_224_amd64_ref(reg u64 hash input input_length) -> reg u64 { reg u64 r; - __sha3_224_ref(out, in, inlen); + __sha3_224_ref(hash, input, input_length); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_hash/sha3-256/amd64/avx2/hash.jazz b/src/crypto_hash/sha3-256/amd64/avx2/hash.jazz index 3ba70f83..b12c4636 100644 --- a/src/crypto_hash/sha3-256/amd64/avx2/hash.jazz +++ b/src/crypto_hash/sha3-256/amd64/avx2/hash.jazz @@ -1,9 +1,9 @@ require "sha3-256.jinc" -export fn jade_hash_sha3_256_amd64_avx2(reg u64 out in inlen) -> reg u64 +export fn jade_hash_sha3_256_amd64_avx2(reg u64 hash input input_length) -> reg u64 { reg u64 r; - __sha3_256_avx2(out, in, inlen); + __sha3_256_avx2(hash, input, input_length); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_hash/sha3-256/amd64/ref/hash.jazz b/src/crypto_hash/sha3-256/amd64/ref/hash.jazz index 0f619e30..d8139544 100644 --- a/src/crypto_hash/sha3-256/amd64/ref/hash.jazz +++ b/src/crypto_hash/sha3-256/amd64/ref/hash.jazz @@ -1,9 +1,9 @@ require "sha3-256.jinc" -export fn jade_hash_sha3_256_amd64_ref(reg u64 out in inlen) -> reg u64 +export fn jade_hash_sha3_256_amd64_ref(reg u64 hash input input_length) -> reg u64 { reg u64 r; - __sha3_256_ref(out, in, inlen); + __sha3_256_ref(hash, input, input_length); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_hash/sha3-384/amd64/avx2/hash.jazz b/src/crypto_hash/sha3-384/amd64/avx2/hash.jazz index afe49112..c46466da 100644 --- a/src/crypto_hash/sha3-384/amd64/avx2/hash.jazz +++ b/src/crypto_hash/sha3-384/amd64/avx2/hash.jazz @@ -1,9 +1,9 @@ require "sha3-384.jinc" -export fn jade_hash_sha3_384_amd64_avx2(reg u64 out in inlen) -> reg u64 +export fn jade_hash_sha3_384_amd64_avx2(reg u64 hash input input_length) -> reg u64 { reg u64 r; - __sha3_384_avx2(out, in, inlen); + __sha3_384_avx2(hash, input, input_length); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_hash/sha3-384/amd64/ref/hash.jazz b/src/crypto_hash/sha3-384/amd64/ref/hash.jazz index 7eb01286..cb53f520 100644 --- a/src/crypto_hash/sha3-384/amd64/ref/hash.jazz +++ b/src/crypto_hash/sha3-384/amd64/ref/hash.jazz @@ -1,9 +1,9 @@ require "sha3-384.jinc" -export fn jade_hash_sha3_384_amd64_ref(reg u64 out in inlen) -> reg u64 +export fn jade_hash_sha3_384_amd64_ref(reg u64 hash input input_length) -> reg u64 { reg u64 r; - __sha3_384_ref(out, in, inlen); + __sha3_384_ref(hash, input, input_length); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_hash/sha3-512/amd64/avx2/hash.jazz b/src/crypto_hash/sha3-512/amd64/avx2/hash.jazz index f6a74ec2..02ac053d 100644 --- a/src/crypto_hash/sha3-512/amd64/avx2/hash.jazz +++ b/src/crypto_hash/sha3-512/amd64/avx2/hash.jazz @@ -1,9 +1,9 @@ require "sha3-512.jinc" -export fn jade_hash_sha3_512_amd64_avx2(reg u64 out in inlen) -> reg u64 +export fn jade_hash_sha3_512_amd64_avx2(reg u64 hash input input_length) -> reg u64 { reg u64 r; - __sha3_512_avx2(out, in, inlen); + __sha3_512_avx2(hash, input, input_length); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_hash/sha3-512/amd64/ref/hash.jazz b/src/crypto_hash/sha3-512/amd64/ref/hash.jazz index 4779076b..0fa5c965 100644 --- a/src/crypto_hash/sha3-512/amd64/ref/hash.jazz +++ b/src/crypto_hash/sha3-512/amd64/ref/hash.jazz @@ -1,9 +1,9 @@ require "sha3-512.jinc" -export fn jade_hash_sha3_512_amd64_ref(reg u64 out in inlen) -> reg u64 +export fn jade_hash_sha3_512_amd64_ref(reg u64 hash input input_length) -> reg u64 { reg u64 r; - __sha3_512_ref(out, in, inlen); + __sha3_512_ref(hash, input, input_length); _,_,_,_,_,r = #set0(); return r; } diff --git a/src/crypto_hash/sha512/amd64/ref/hash.jazz b/src/crypto_hash/sha512/amd64/ref/hash.jazz index f4d948e7..df807244 100644 --- a/src/crypto_hash/sha512/amd64/ref/hash.jazz +++ b/src/crypto_hash/sha512/amd64/ref/hash.jazz @@ -1,9 +1,9 @@ require "sha512.jinc" -export fn jade_hash_sha512_amd64_ref(reg u64 out in inlen) -> reg u64 +export fn jade_hash_sha512_amd64_ref(reg u64 hash input input_length) -> reg u64 { reg u64 r; - __sha512(out, in, inlen); + __sha512(hash, input, input_length); _,_,_,_,_,r = #set0(); return r; } From f0140da607b719f7b80e8773b9a289bfcfacc357 Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Mon, 5 Dec 2022 17:57:18 +0000 Subject: [PATCH 4/9] args naming : crypto_kem pass --- .../kyber/kyber512/amd64/avx2/kem.jazz | 24 +++++++---------- .../kyber/kyber512/amd64/ref/kem.jazz | 25 +++++++----------- .../kyber/kyber768/amd64/avx2/kem.jazz | 26 +++++++------------ .../kyber/kyber768/amd64/ref/kem.jazz | 25 +++++++----------- 4 files changed, 36 insertions(+), 64 deletions(-) diff --git a/src/crypto_kem/kyber/kyber512/amd64/avx2/kem.jazz b/src/crypto_kem/kyber/kyber512/amd64/avx2/kem.jazz index 060754e1..9ff8b83e 100644 --- a/src/crypto_kem/kyber/kyber512/amd64/avx2/kem.jazz +++ b/src/crypto_kem/kyber/kyber512/amd64/avx2/kem.jazz @@ -1,32 +1,26 @@ require "indcpa.jinc" from Jade require "crypto_kem/kyber/common/amd64/kem.jinc" -export fn jade_kem_kyber_kyber512_amd64_avx2_keypair(reg u64 pkp, reg u64 skp) -> reg u64 +export fn jade_kem_kyber_kyber512_amd64_avx2_keypair(reg u64 public_key secret_key) -> reg u64 { reg u64 r; - - __crypto_kem_keypair_jazz(pkp, skp); - - _, _, _, _, _, r = #set0(); + __crypto_kem_keypair_jazz(public_key, secret_key); + ?{}, r = #set0(); return r; } -export fn jade_kem_kyber_kyber512_amd64_avx2_enc(reg u64 ctp, reg u64 shkp, reg u64 pkp) -> reg u64 +export fn jade_kem_kyber_kyber512_amd64_avx2_enc(reg u64 ciphertext shared_secret public_key) -> reg u64 { reg u64 r; - - __crypto_kem_enc_jazz(ctp, shkp, pkp); - - _, _, _, _, _, r = #set0(); + __crypto_kem_enc_jazz(ciphertext, shared_secret, public_key); + ?{}, r = #set0(); return r; } -export fn jade_kem_kyber_kyber512_amd64_avx2_dec(reg u64 shkp, reg u64 ctp, reg u64 skp) -> reg u64 +export fn jade_kem_kyber_kyber512_amd64_avx2_dec(reg u64 shared_secret ciphertext secret_key) -> reg u64 { reg u64 r; - - __crypto_kem_dec_jazz(shkp, ctp, skp); - - _, _, _, _, _, r = #set0(); + __crypto_kem_dec_jazz(shared_secret, ciphertext, secret_key); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_kem/kyber/kyber512/amd64/ref/kem.jazz b/src/crypto_kem/kyber/kyber512/amd64/ref/kem.jazz index b57a56a0..671ed099 100644 --- a/src/crypto_kem/kyber/kyber512/amd64/ref/kem.jazz +++ b/src/crypto_kem/kyber/kyber512/amd64/ref/kem.jazz @@ -1,33 +1,26 @@ require "indcpa.jinc" from Jade require "crypto_kem/kyber/common/amd64/ref/kem.jinc" -export fn jade_kem_kyber_kyber512_amd64_ref_keypair(reg u64 pkp, reg u64 skp) -> reg u64 +export fn jade_kem_kyber_kyber512_amd64_ref_keypair(reg u64 public_key secret_key) -> reg u64 { reg u64 r; - - __crypto_kem_keypair_jazz(pkp, skp); - - _, _, _, _, _, r = #set0(); + __crypto_kem_keypair_jazz(public_key, secret_key); + ?{}, r = #set0(); return r; } - -export fn jade_kem_kyber_kyber512_amd64_ref_enc(reg u64 ctp, reg u64 shkp, reg u64 pkp) -> reg u64 +export fn jade_kem_kyber_kyber512_amd64_ref_enc(reg u64 ciphertext shared_secret public_key) -> reg u64 { reg u64 r; - - __crypto_kem_enc_jazz(ctp, shkp, pkp); - - _, _, _, _, _, r = #set0(); + __crypto_kem_enc_jazz(ciphertext, shared_secret, public_key); + ?{}, r = #set0(); return r; } -export fn jade_kem_kyber_kyber512_amd64_ref_dec(reg u64 shkp, reg u64 ctp, reg u64 skp) -> reg u64 +export fn jade_kem_kyber_kyber512_amd64_ref_dec(reg u64 shared_secret ciphertext secret_key) -> reg u64 { reg u64 r; - - __crypto_kem_dec_jazz(shkp, ctp, skp); - - _, _, _, _, _, r = #set0(); + __crypto_kem_dec_jazz(shared_secret, ciphertext, secret_key); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_kem/kyber/kyber768/amd64/avx2/kem.jazz b/src/crypto_kem/kyber/kyber768/amd64/avx2/kem.jazz index 5921b754..be79a1bd 100644 --- a/src/crypto_kem/kyber/kyber768/amd64/avx2/kem.jazz +++ b/src/crypto_kem/kyber/kyber768/amd64/avx2/kem.jazz @@ -1,34 +1,26 @@ require "indcpa.jinc" from Jade require "crypto_kem/kyber/common/amd64/kem.jinc" -export fn jade_kem_kyber_kyber768_amd64_avx2_keypair(reg u64 pkp, reg u64 skp) -> reg u64 +export fn jade_kem_kyber_kyber768_amd64_avx2_keypair(reg u64 public_key secret_key) -> reg u64 { reg u64 r; - - __crypto_kem_keypair_jazz(pkp, skp); - - _, _, _, _, _, r = #set0(); + __crypto_kem_keypair_jazz(public_key, secret_key); + ?{}, r = #set0(); return r; } - -export fn jade_kem_kyber_kyber768_amd64_avx2_enc(reg u64 ctp, reg u64 shkp, reg u64 pkp) -> reg u64 +export fn jade_kem_kyber_kyber768_amd64_avx2_enc(reg u64 ciphertext shared_secret public_key) -> reg u64 { reg u64 r; - - __crypto_kem_enc_jazz(ctp, shkp, pkp); - - _, _, _, _, _, r = #set0(); + __crypto_kem_enc_jazz(ciphertext, shared_secret, public_key); + ?{}, r = #set0(); return r; } - -export fn jade_kem_kyber_kyber768_amd64_avx2_dec(reg u64 shkp, reg u64 ctp, reg u64 skp) -> reg u64 +export fn jade_kem_kyber_kyber768_amd64_avx2_dec(reg u64 shared_secret ciphertext secret_key) -> reg u64 { reg u64 r; - - __crypto_kem_dec_jazz(shkp, ctp, skp); - - _, _, _, _, _, r = #set0(); + __crypto_kem_dec_jazz(shared_secret, ciphertext, secret_key); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_kem/kyber/kyber768/amd64/ref/kem.jazz b/src/crypto_kem/kyber/kyber768/amd64/ref/kem.jazz index 623dcadd..ca1f9b1f 100644 --- a/src/crypto_kem/kyber/kyber768/amd64/ref/kem.jazz +++ b/src/crypto_kem/kyber/kyber768/amd64/ref/kem.jazz @@ -1,33 +1,26 @@ require "indcpa.jinc" from Jade require "crypto_kem/kyber/common/amd64/ref/kem.jinc" -export fn jade_kem_kyber_kyber768_amd64_ref_keypair(reg u64 pkp, reg u64 skp) -> reg u64 +export fn jade_kem_kyber_kyber768_amd64_ref_keypair(reg u64 public_key secret_key) -> reg u64 { reg u64 r; - - __crypto_kem_keypair_jazz(pkp, skp); - - _, _, _, _, _, r = #set0(); + __crypto_kem_keypair_jazz(public_key, secret_key); + ?{}, r = #set0(); return r; } - -export fn jade_kem_kyber_kyber768_amd64_ref_enc(reg u64 ctp, reg u64 shkp, reg u64 pkp) -> reg u64 +export fn jade_kem_kyber_kyber768_amd64_ref_enc(reg u64 ciphertext shared_secret public_key) -> reg u64 { reg u64 r; - - __crypto_kem_enc_jazz(ctp, shkp, pkp); - - _, _, _, _, _, r = #set0(); + __crypto_kem_enc_jazz(ciphertext, shared_secret, public_key); + ?{}, r = #set0(); return r; } -export fn jade_kem_kyber_kyber768_amd64_ref_dec(reg u64 shkp, reg u64 ctp, reg u64 skp) -> reg u64 +export fn jade_kem_kyber_kyber768_amd64_ref_dec(reg u64 shared_secret ciphertext secret_key) -> reg u64 { reg u64 r; - - __crypto_kem_dec_jazz(shkp, ctp, skp); - - _, _, _, _, _, r = #set0(); + __crypto_kem_dec_jazz(shared_secret, ciphertext, secret_key); + ?{}, r = #set0(); return r; } From e4d90c8d17616c383ac7abcdc749f9e313eab8e3 Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Mon, 5 Dec 2022 18:58:11 +0000 Subject: [PATCH 5/9] args naming : crypto_onetimeauth -- includes fix for avx2 corr. proof. --- .../amd64/avx/onetimeauth_ct_proof.ec | 4 +-- .../amd64/avx2/onetimeauth_ct_proof.ec | 4 +-- .../amd64/avx2/onetimeauth_s_proof.ec | 10 +++--- .../amd64/ref/onetimeauth_ct_proof.ec | 4 +-- .../poly1305/amd64/avx/onetimeauth.jazz | 36 ++++++++++--------- .../poly1305/amd64/avx2/onetimeauth.jazz | 36 ++++++++++--------- .../poly1305/amd64/ref/onetimeauth.jazz | 36 ++++++++++--------- 7 files changed, 71 insertions(+), 59 deletions(-) diff --git a/proof/crypto_onetimeauth/poly1305/amd64/avx/onetimeauth_ct_proof.ec b/proof/crypto_onetimeauth/poly1305/amd64/avx/onetimeauth_ct_proof.ec index 7288ed46..87c7ae90 100644 --- a/proof/crypto_onetimeauth/poly1305/amd64/avx/onetimeauth_ct_proof.ec +++ b/proof/crypto_onetimeauth/poly1305/amd64/avx/onetimeauth_ct_proof.ec @@ -2,14 +2,14 @@ require import Onetimeauth_ct. equiv eq_jade_onetimeauth_poly1305_amd64_avx_ct : M.jade_onetimeauth_poly1305_amd64_avx ~ M.jade_onetimeauth_poly1305_amd64_avx : - ={_out, _in, _inlen, _key, M.leakages} ==> ={M.leakages}. + ={mac, input, input_length, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. equiv eq_jade_onetimeauth_poly1305_amd64_avx_verify_ct : M.jade_onetimeauth_poly1305_amd64_avx_verify ~ M.jade_onetimeauth_poly1305_amd64_avx_verify : - ={_h, _in, _inlen, _key, M.leakages} ==> ={M.leakages}. + ={mac, input, input_length, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_onetimeauth/poly1305/amd64/avx2/onetimeauth_ct_proof.ec b/proof/crypto_onetimeauth/poly1305/amd64/avx2/onetimeauth_ct_proof.ec index 66d60ec4..ac9d7bb1 100644 --- a/proof/crypto_onetimeauth/poly1305/amd64/avx2/onetimeauth_ct_proof.ec +++ b/proof/crypto_onetimeauth/poly1305/amd64/avx2/onetimeauth_ct_proof.ec @@ -2,14 +2,14 @@ require import Onetimeauth_ct. equiv eq_jade_onetimeauth_poly1305_amd64_avx2_ct : M.jade_onetimeauth_poly1305_amd64_avx2 ~ M.jade_onetimeauth_poly1305_amd64_avx2 : - ={_out, _in, _inlen, _key, M.leakages} ==> ={M.leakages}. + ={mac, input, input_length, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. equiv eq_jade_onetimeauth_poly1305_amd64_avx2_verify_ct : M.jade_onetimeauth_poly1305_amd64_avx2_verify ~ M.jade_onetimeauth_poly1305_amd64_avx2_verify : - ={_h, _in, _inlen, _key, M.leakages} ==> ={M.leakages}. + ={mac, input, input_length, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_onetimeauth/poly1305/amd64/avx2/onetimeauth_s_proof.ec b/proof/crypto_onetimeauth/poly1305/amd64/avx2/onetimeauth_s_proof.ec index 3fed6cee..5765d710 100644 --- a/proof/crypto_onetimeauth/poly1305/amd64/avx2/onetimeauth_s_proof.ec +++ b/proof/crypto_onetimeauth/poly1305/amd64/avx2/onetimeauth_s_proof.ec @@ -190,7 +190,7 @@ op poly1305_post (r : zp) (s : int) (m : Zp_msg) (ors : W64.t Array2.t) lemma jade_onetimeauth_poly1305_amd64_avx2 mem rr ss mm outt inn inl kk : phoare [ Onetimeauth_s.M.jade_onetimeauth_poly1305_amd64_avx2 : Glob.mem = mem /\ - _out = outt /\ _in = inn /\ _inlen = inl /\ _key = kk /\ + mac = outt /\ input = inn /\ input_length = inl /\ key = kk /\ inv_ptr_mem (to_uint kk) (to_uint inn) (to_uint outt) (next_multiple inl) /\ poly1305_pre rr ss mm mem inn inl kk ==> poly1305_post_mem rr ss mm (to_uint outt) mem Glob.mem /\ res = W64.zero] = 1%r by @@ -259,13 +259,13 @@ qed. lemma jade_onetimeauth_poly1305_amd64_avx2_verify_h mem hh rr ss mm hhp inn inl kk : hoare [ Onetimeauth_s.M.jade_onetimeauth_poly1305_amd64_avx2_verify : Glob.mem = mem /\ - _h = hhp /\ _in = inn /\ _inlen = inl /\ _key = kk /\ + mac = hhp /\ input = inn /\ input_length = inl /\ key = kk /\ inv_ptr_mem (to_uint kk) (to_uint inn) (to_uint hhp) (next_multiple inl) /\ poly1305_pre_verif rr hh ss mm mem hhp inn inl kk ==> poly1305_post_verif rr hh ss mm (res = W64.zero) mem Glob.mem]. proc => /=. inline 5. - seq 10 : (good_ptr (W64.to_uint hhp) 16 /\ h0 = hhp /\ + seq 10 : (good_ptr (W64.to_uint hhp) 16 /\ h = hhp /\ poly1305_post rr ss mm hc mem Glob.mem /\ hh = to_uint (loadW128 mem (to_uint hhp))); 1: by call(Onetimeauth_s__poly1305_r_avx2_corr_h mem rr ss mm inn inl kk); auto => />. @@ -305,7 +305,7 @@ qed. lemma jade_onetimeauth_poly1305_amd64_avx2_verify_ll mem hh rr ss mm hhp inn inl kk : phoare [ Onetimeauth_s.M.jade_onetimeauth_poly1305_amd64_avx2_verify : Glob.mem = mem /\ - _h = hhp /\ _in = inn /\ _inlen = inl /\ _key = kk /\ + mac = hhp /\ input = inn /\ input_length = inl /\ key = kk /\ inv_ptr_mem (to_uint kk) (to_uint inn) (to_uint hhp) (next_multiple inl) /\ poly1305_pre_verif rr hh ss mm mem hhp inn inl kk ==> true] = 1%r. @@ -356,7 +356,7 @@ op poly1305_post_verif (r : Zp.zp) (h s : int) (m : Zp_msg) (ov : bool) (memO me lemma jade_onetimeauth_poly1305_amd64_avx2_verify mem hh rr ss mm hhp inn inl kk : phoare [ Onetimeauth_s.M.jade_onetimeauth_poly1305_amd64_avx2_verify : Glob.mem = mem /\ - _h = hhp /\ _in = inn /\ _inlen = inl /\ _key = kk /\ + mac = hhp /\ input = inn /\ input_length = inl /\ key = kk /\ inv_ptr_mem (to_uint kk) (to_uint inn) (to_uint hhp) (next_multiple inl) /\ poly1305_pre_verif rr hh ss mm mem hhp inn inl kk ==> poly1305_post_verif rr hh ss mm (res = W64.zero) mem Glob.mem] = 1%r diff --git a/proof/crypto_onetimeauth/poly1305/amd64/ref/onetimeauth_ct_proof.ec b/proof/crypto_onetimeauth/poly1305/amd64/ref/onetimeauth_ct_proof.ec index c1b181bc..87635d30 100644 --- a/proof/crypto_onetimeauth/poly1305/amd64/ref/onetimeauth_ct_proof.ec +++ b/proof/crypto_onetimeauth/poly1305/amd64/ref/onetimeauth_ct_proof.ec @@ -2,14 +2,14 @@ require import Onetimeauth_ct. equiv eq_jade_onetimeauth_poly1305_amd64_ref_ct : M.jade_onetimeauth_poly1305_amd64_ref ~ M.jade_onetimeauth_poly1305_amd64_ref : - ={_out, _in, _inlen, _key, M.leakages} ==> ={M.leakages}. + ={mac, input, input_length, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. equiv eq_jade_onetimeauth_poly1305_amd64_ref_verify_ct : M.jade_onetimeauth_poly1305_amd64_ref_verify ~ M.jade_onetimeauth_poly1305_amd64_ref_verify : - ={_h, _in, _inlen, _key, M.leakages} ==> ={M.leakages}. + ={mac, input, input_length, key, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/src/crypto_onetimeauth/poly1305/amd64/avx/onetimeauth.jazz b/src/crypto_onetimeauth/poly1305/amd64/avx/onetimeauth.jazz index cb224d0d..5d0eb076 100644 --- a/src/crypto_onetimeauth/poly1305/amd64/avx/onetimeauth.jazz +++ b/src/crypto_onetimeauth/poly1305/amd64/avx/onetimeauth.jazz @@ -1,27 +1,31 @@ require "poly1305.jinc" -export fn jade_onetimeauth_poly1305_amd64_avx(reg u64 _out _in _inlen _key) -> reg u64 +export fn jade_onetimeauth_poly1305_amd64_avx(reg u64 mac input input_length key) -> reg u64 { - reg u64 r out in inlen key; - - out = _out; - in = _in; - inlen = _inlen; - key = _key; - __poly1305_avx(out, in, inlen, key); - _,_,_,_,_,r = #set0(); + reg u64 r; + + mac = mac; + input = input; + input_length = input_length; + key = key; + + __poly1305_avx(mac, input, input_length, key); + + ?{}, r = #set0(); return r; } -export fn jade_onetimeauth_poly1305_amd64_avx_verify(reg u64 _h _in _inlen _key) -> reg u64 +export fn jade_onetimeauth_poly1305_amd64_avx_verify(reg u64 mac input input_length key) -> reg u64 { - reg u64 r h in inlen key; + reg u64 r; + + mac = mac; + input = input; + input_length = input_length; + key = key; + + r = __poly1305_verify_avx(mac, input, input_length, key); - h = _h; - in = _in; - inlen = _inlen; - key = _key; - r = __poly1305_verify_avx(h, in, inlen, key); return r; } diff --git a/src/crypto_onetimeauth/poly1305/amd64/avx2/onetimeauth.jazz b/src/crypto_onetimeauth/poly1305/amd64/avx2/onetimeauth.jazz index 20aaac44..71ee3f39 100644 --- a/src/crypto_onetimeauth/poly1305/amd64/avx2/onetimeauth.jazz +++ b/src/crypto_onetimeauth/poly1305/amd64/avx2/onetimeauth.jazz @@ -1,27 +1,31 @@ require "poly1305.jinc" -export fn jade_onetimeauth_poly1305_amd64_avx2(reg u64 _out _in _inlen _key) -> reg u64 +export fn jade_onetimeauth_poly1305_amd64_avx2(reg u64 mac input input_length key) -> reg u64 { - reg u64 r out in inlen key; - - out = _out; - in = _in; - inlen = _inlen; - key = _key; - __poly1305_avx2(out, in, inlen, key); - _,_,_,_,_,r = #set0(); + reg u64 r; + + mac = mac; + input = input; + input_length = input_length; + key = key; + + __poly1305_avx2(mac, input, input_length, key); + + ?{}, r = #set0(); return r; } -export fn jade_onetimeauth_poly1305_amd64_avx2_verify(reg u64 _h _in _inlen _key) -> reg u64 +export fn jade_onetimeauth_poly1305_amd64_avx2_verify(reg u64 mac input input_length key) -> reg u64 { - reg u64 r h in inlen key; + reg u64 r; + + mac = mac; + input = input; + input_length = input_length; + key = key; + + r = __poly1305_verify_avx2(mac, input, input_length, key); - h = _h; - in = _in; - inlen = _inlen; - key = _key; - r = __poly1305_verify_avx2(h, in, inlen, key); return r; } diff --git a/src/crypto_onetimeauth/poly1305/amd64/ref/onetimeauth.jazz b/src/crypto_onetimeauth/poly1305/amd64/ref/onetimeauth.jazz index b9a87b5e..f0179e1c 100644 --- a/src/crypto_onetimeauth/poly1305/amd64/ref/onetimeauth.jazz +++ b/src/crypto_onetimeauth/poly1305/amd64/ref/onetimeauth.jazz @@ -1,27 +1,31 @@ require "poly1305.jinc" -export fn jade_onetimeauth_poly1305_amd64_ref(reg u64 _out _in _inlen _key) -> reg u64 +export fn jade_onetimeauth_poly1305_amd64_ref(reg u64 mac input input_length key) -> reg u64 { - reg u64 r out in inlen key; - - out = _out; - in = _in; - inlen = _inlen; - key = _key; - __poly1305_ref(out, in, inlen, key); - _,_,_,_,_,r = #set0(); + reg u64 r; + + mac = mac; + input = input; + input_length = input_length; + key = key; + + __poly1305_ref(mac, input, input_length, key); + + ?{}, r = #set0(); return r; } -export fn jade_onetimeauth_poly1305_amd64_ref_verify(reg u64 _h _in _inlen _key) -> reg u64 +export fn jade_onetimeauth_poly1305_amd64_ref_verify(reg u64 mac input input_length key) -> reg u64 { - reg u64 r h in inlen key; + reg u64 r; + + mac = mac; + input = input; + input_length = input_length; + key = key; + + r = __poly1305_verify_ref(mac, input, input_length, key); - h = _h; - in = _in; - inlen = _inlen; - key = _key; - r = __poly1305_verify_ref(h, in, inlen, key); return r; } From f2551505941e726145ba30030dfbc0f19e3c16c5 Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Mon, 5 Dec 2022 19:07:36 +0000 Subject: [PATCH 6/9] replace _,_,_,_,_, by ?{} on .jazz files --- src/crypto_hash/sha256/amd64/ref/hash.jazz | 2 +- src/crypto_hash/sha3-224/amd64/avx2/hash.jazz | 2 +- src/crypto_hash/sha3-224/amd64/ref/hash.jazz | 2 +- src/crypto_hash/sha3-256/amd64/avx2/hash.jazz | 2 +- src/crypto_hash/sha3-256/amd64/ref/hash.jazz | 2 +- src/crypto_hash/sha3-384/amd64/avx2/hash.jazz | 2 +- src/crypto_hash/sha3-384/amd64/ref/hash.jazz | 2 +- src/crypto_hash/sha3-512/amd64/avx2/hash.jazz | 2 +- src/crypto_hash/sha3-512/amd64/ref/hash.jazz | 2 +- src/crypto_hash/sha512/amd64/ref/hash.jazz | 2 +- src/crypto_stream/chacha/chacha12/amd64/avx/stream.jazz | 4 ++-- src/crypto_stream/chacha/chacha12/amd64/avx2/stream.jazz | 4 ++-- src/crypto_stream/chacha/chacha12/amd64/ref/stream.jazz | 4 ++-- .../chacha/chacha20-ietf/amd64/avx/stream.jazz | 8 ++++---- .../chacha/chacha20-ietf/amd64/avx2/stream.jazz | 8 ++++---- .../chacha/chacha20-ietf/amd64/ref/stream.jazz | 8 ++++---- src/crypto_stream/chacha/chacha20/amd64/avx/stream.jazz | 4 ++-- src/crypto_stream/chacha/chacha20/amd64/avx2/stream.jazz | 4 ++-- src/crypto_stream/chacha/chacha20/amd64/ref/stream.jazz | 4 ++-- src/crypto_stream/salsa20/salsa20/amd64/avx/stream.jazz | 4 ++-- src/crypto_stream/salsa20/salsa20/amd64/avx2/stream.jazz | 4 ++-- src/crypto_stream/salsa20/salsa20/amd64/ref/stream.jazz | 4 ++-- src/crypto_stream/salsa20/salsa2012/amd64/avx/stream.jazz | 4 ++-- .../salsa20/salsa2012/amd64/avx2/stream.jazz | 4 ++-- src/crypto_stream/salsa20/salsa2012/amd64/ref/stream.jazz | 4 ++-- src/crypto_stream/xsalsa20/amd64/avx/stream.jazz | 4 ++-- src/crypto_stream/xsalsa20/amd64/avx2/stream.jazz | 4 ++-- src/crypto_stream/xsalsa20/amd64/ref/stream.jazz | 4 ++-- src/crypto_xof/shake128/amd64/avx2/xof.jazz | 2 +- src/crypto_xof/shake128/amd64/ref/xof.jazz | 2 +- src/crypto_xof/shake256/amd64/avx2/xof.jazz | 2 +- src/crypto_xof/shake256/amd64/ref/xof.jazz | 2 +- src/crypto_xof/shake256/amd64/ref1/xof.jazz | 2 +- src/crypto_xof/shake256/amd64/spec/xof.jazz | 2 +- 34 files changed, 58 insertions(+), 58 deletions(-) diff --git a/src/crypto_hash/sha256/amd64/ref/hash.jazz b/src/crypto_hash/sha256/amd64/ref/hash.jazz index 8a42629b..83711017 100644 --- a/src/crypto_hash/sha256/amd64/ref/hash.jazz +++ b/src/crypto_hash/sha256/amd64/ref/hash.jazz @@ -4,7 +4,7 @@ export fn jade_hash_sha256_amd64_ref(reg u64 hash input input_length) -> reg u64 { reg u64 r; __sha256(hash, input, input_length); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_hash/sha3-224/amd64/avx2/hash.jazz b/src/crypto_hash/sha3-224/amd64/avx2/hash.jazz index 9ddc32db..77ae780a 100644 --- a/src/crypto_hash/sha3-224/amd64/avx2/hash.jazz +++ b/src/crypto_hash/sha3-224/amd64/avx2/hash.jazz @@ -4,7 +4,7 @@ export fn jade_hash_sha3_224_amd64_avx2(reg u64 hash input input_length) -> reg { reg u64 r; __sha3_224_avx2(hash, input, input_length); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_hash/sha3-224/amd64/ref/hash.jazz b/src/crypto_hash/sha3-224/amd64/ref/hash.jazz index 2dcfe49a..0bda7d05 100644 --- a/src/crypto_hash/sha3-224/amd64/ref/hash.jazz +++ b/src/crypto_hash/sha3-224/amd64/ref/hash.jazz @@ -4,7 +4,7 @@ export fn jade_hash_sha3_224_amd64_ref(reg u64 hash input input_length) -> reg u { reg u64 r; __sha3_224_ref(hash, input, input_length); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_hash/sha3-256/amd64/avx2/hash.jazz b/src/crypto_hash/sha3-256/amd64/avx2/hash.jazz index b12c4636..462c1c0b 100644 --- a/src/crypto_hash/sha3-256/amd64/avx2/hash.jazz +++ b/src/crypto_hash/sha3-256/amd64/avx2/hash.jazz @@ -4,7 +4,7 @@ export fn jade_hash_sha3_256_amd64_avx2(reg u64 hash input input_length) -> reg { reg u64 r; __sha3_256_avx2(hash, input, input_length); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_hash/sha3-256/amd64/ref/hash.jazz b/src/crypto_hash/sha3-256/amd64/ref/hash.jazz index d8139544..6c381cce 100644 --- a/src/crypto_hash/sha3-256/amd64/ref/hash.jazz +++ b/src/crypto_hash/sha3-256/amd64/ref/hash.jazz @@ -4,7 +4,7 @@ export fn jade_hash_sha3_256_amd64_ref(reg u64 hash input input_length) -> reg u { reg u64 r; __sha3_256_ref(hash, input, input_length); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_hash/sha3-384/amd64/avx2/hash.jazz b/src/crypto_hash/sha3-384/amd64/avx2/hash.jazz index c46466da..0be82db3 100644 --- a/src/crypto_hash/sha3-384/amd64/avx2/hash.jazz +++ b/src/crypto_hash/sha3-384/amd64/avx2/hash.jazz @@ -4,7 +4,7 @@ export fn jade_hash_sha3_384_amd64_avx2(reg u64 hash input input_length) -> reg { reg u64 r; __sha3_384_avx2(hash, input, input_length); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_hash/sha3-384/amd64/ref/hash.jazz b/src/crypto_hash/sha3-384/amd64/ref/hash.jazz index cb53f520..fb952862 100644 --- a/src/crypto_hash/sha3-384/amd64/ref/hash.jazz +++ b/src/crypto_hash/sha3-384/amd64/ref/hash.jazz @@ -4,7 +4,7 @@ export fn jade_hash_sha3_384_amd64_ref(reg u64 hash input input_length) -> reg u { reg u64 r; __sha3_384_ref(hash, input, input_length); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_hash/sha3-512/amd64/avx2/hash.jazz b/src/crypto_hash/sha3-512/amd64/avx2/hash.jazz index 02ac053d..49335d0d 100644 --- a/src/crypto_hash/sha3-512/amd64/avx2/hash.jazz +++ b/src/crypto_hash/sha3-512/amd64/avx2/hash.jazz @@ -4,7 +4,7 @@ export fn jade_hash_sha3_512_amd64_avx2(reg u64 hash input input_length) -> reg { reg u64 r; __sha3_512_avx2(hash, input, input_length); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_hash/sha3-512/amd64/ref/hash.jazz b/src/crypto_hash/sha3-512/amd64/ref/hash.jazz index 0fa5c965..aa265621 100644 --- a/src/crypto_hash/sha3-512/amd64/ref/hash.jazz +++ b/src/crypto_hash/sha3-512/amd64/ref/hash.jazz @@ -4,7 +4,7 @@ export fn jade_hash_sha3_512_amd64_ref(reg u64 hash input input_length) -> reg u { reg u64 r; __sha3_512_ref(hash, input, input_length); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_hash/sha512/amd64/ref/hash.jazz b/src/crypto_hash/sha512/amd64/ref/hash.jazz index df807244..7402970b 100644 --- a/src/crypto_hash/sha512/amd64/ref/hash.jazz +++ b/src/crypto_hash/sha512/amd64/ref/hash.jazz @@ -4,7 +4,7 @@ export fn jade_hash_sha512_amd64_ref(reg u64 hash input input_length) -> reg u64 { reg u64 r; __sha512(hash, input, input_length); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_stream/chacha/chacha12/amd64/avx/stream.jazz b/src/crypto_stream/chacha/chacha12/amd64/avx/stream.jazz index 54ea736b..e799626a 100644 --- a/src/crypto_stream/chacha/chacha12/amd64/avx/stream.jazz +++ b/src/crypto_stream/chacha/chacha12/amd64/avx/stream.jazz @@ -6,7 +6,7 @@ export fn jade_stream_chacha_chacha12_amd64_avx_xor(reg u64 output input input_l { reg u64 r; __chacha_xor_avx(output, input, input_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -14,6 +14,6 @@ export fn jade_stream_chacha_chacha12_amd64_avx(reg u64 stream stream_length non { reg u64 r; __chacha_avx(stream, stream_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_stream/chacha/chacha12/amd64/avx2/stream.jazz b/src/crypto_stream/chacha/chacha12/amd64/avx2/stream.jazz index 69b8105d..e2cfd229 100644 --- a/src/crypto_stream/chacha/chacha12/amd64/avx2/stream.jazz +++ b/src/crypto_stream/chacha/chacha12/amd64/avx2/stream.jazz @@ -6,7 +6,7 @@ export fn jade_stream_chacha_chacha12_amd64_avx2_xor(reg u64 output input input_ { reg u64 r; __chacha_xor_avx2(output, input, input_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -14,7 +14,7 @@ export fn jade_stream_chacha_chacha12_amd64_avx2(reg u64 stream stream_length no { reg u64 r; __chacha_avx2(stream, stream_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_stream/chacha/chacha12/amd64/ref/stream.jazz b/src/crypto_stream/chacha/chacha12/amd64/ref/stream.jazz index 2a14aacc..ce97207c 100644 --- a/src/crypto_stream/chacha/chacha12/amd64/ref/stream.jazz +++ b/src/crypto_stream/chacha/chacha12/amd64/ref/stream.jazz @@ -6,7 +6,7 @@ export fn jade_stream_chacha_chacha12_amd64_ref_xor(reg u64 output input input_l { reg u64 r; __chacha_xor_ref(output, input, input_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -14,7 +14,7 @@ export fn jade_stream_chacha_chacha12_amd64_ref(reg u64 stream stream_length non { reg u64 r; __chacha_ref(stream, stream_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_stream/chacha/chacha20-ietf/amd64/avx/stream.jazz b/src/crypto_stream/chacha/chacha20-ietf/amd64/avx/stream.jazz index 3fb8c9a0..bbeb1261 100644 --- a/src/crypto_stream/chacha/chacha20-ietf/amd64/avx/stream.jazz +++ b/src/crypto_stream/chacha/chacha20-ietf/amd64/avx/stream.jazz @@ -16,7 +16,7 @@ export fn jade_stream_chacha_chacha20_ietf_amd64_avx_xor(reg u64 output input in { reg u64 r; __chacha_xor_avx(output, input, input_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -24,7 +24,7 @@ export fn jade_stream_chacha_chacha20_ietf_amd64_avx(reg u64 stream stream_lengt { reg u64 r; __chacha_avx(stream, stream_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -34,7 +34,7 @@ export fn jade_stream_chacha_chacha20_ietf_amd64_avx_xor_ic(reg u64 output input { reg u64 r; __chacha_xor_avx_ic(output, input, input_length, nonce, counter, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -42,7 +42,7 @@ export fn jade_stream_chacha_chacha20_ietf_amd64_avx_ic(reg u64 stream stream_le { reg u64 r; __chacha_avx_ic(stream, stream_length, nonce, counter, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_stream/chacha/chacha20-ietf/amd64/avx2/stream.jazz b/src/crypto_stream/chacha/chacha20-ietf/amd64/avx2/stream.jazz index e0315562..0793ca35 100644 --- a/src/crypto_stream/chacha/chacha20-ietf/amd64/avx2/stream.jazz +++ b/src/crypto_stream/chacha/chacha20-ietf/amd64/avx2/stream.jazz @@ -16,7 +16,7 @@ export fn jade_stream_chacha_chacha20_ietf_amd64_avx2_xor(reg u64 output input i { reg u64 r; __chacha_xor_avx2(output, input, input_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -24,7 +24,7 @@ export fn jade_stream_chacha_chacha20_ietf_amd64_avx2(reg u64 stream stream_leng { reg u64 r; __chacha_avx2(stream, stream_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -34,7 +34,7 @@ export fn jade_stream_chacha_chacha20_ietf_amd64_avx2_xor_ic(reg u64 output inpu { reg u64 r; __chacha_xor_avx2_ic(output, input, input_length, nonce, counter, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -42,7 +42,7 @@ export fn jade_stream_chacha_chacha20_ietf_amd64_avx2_ic(reg u64 stream stream_l { reg u64 r; __chacha_avx2_ic(stream, stream_length, nonce, counter, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_stream/chacha/chacha20-ietf/amd64/ref/stream.jazz b/src/crypto_stream/chacha/chacha20-ietf/amd64/ref/stream.jazz index 5075fb6a..394b79f2 100644 --- a/src/crypto_stream/chacha/chacha20-ietf/amd64/ref/stream.jazz +++ b/src/crypto_stream/chacha/chacha20-ietf/amd64/ref/stream.jazz @@ -9,7 +9,7 @@ export fn jade_stream_chacha_chacha20_ietf_amd64_ref_xor(reg u64 output input in { reg u64 r; __chacha_xor_ref(output, input, input_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -17,7 +17,7 @@ export fn jade_stream_chacha_chacha20_ietf_amd64_ref(reg u64 stream stream_lengt { reg u64 r; __chacha_ref(stream, stream_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -27,7 +27,7 @@ export fn jade_stream_chacha_chacha20_ietf_amd64_ref_xor_ic(reg u64 output input { reg u64 r; _chacha_xor_ref_ic_(output, input, input_length, nonce, counter, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -35,7 +35,7 @@ export fn jade_stream_chacha_chacha20_ietf_amd64_ref_ic(reg u64 stream stream_le { reg u64 r; _chacha_ref_ic_(stream, stream_length, nonce, counter, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_stream/chacha/chacha20/amd64/avx/stream.jazz b/src/crypto_stream/chacha/chacha20/amd64/avx/stream.jazz index caa889c0..91eed766 100644 --- a/src/crypto_stream/chacha/chacha20/amd64/avx/stream.jazz +++ b/src/crypto_stream/chacha/chacha20/amd64/avx/stream.jazz @@ -6,7 +6,7 @@ export fn jade_stream_chacha_chacha20_amd64_avx_xor(reg u64 output input input_l { reg u64 r; __chacha_xor_avx(output, input, input_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -14,6 +14,6 @@ export fn jade_stream_chacha_chacha20_amd64_avx(reg u64 stream stream_length non { reg u64 r; __chacha_avx(stream, stream_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_stream/chacha/chacha20/amd64/avx2/stream.jazz b/src/crypto_stream/chacha/chacha20/amd64/avx2/stream.jazz index ce309fb4..ee5507ac 100644 --- a/src/crypto_stream/chacha/chacha20/amd64/avx2/stream.jazz +++ b/src/crypto_stream/chacha/chacha20/amd64/avx2/stream.jazz @@ -6,7 +6,7 @@ export fn jade_stream_chacha_chacha20_amd64_avx2_xor(reg u64 output input input_ { reg u64 r; __chacha_xor_avx2(output, input, input_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -14,6 +14,6 @@ export fn jade_stream_chacha_chacha20_amd64_avx2(reg u64 stream stream_length no { reg u64 r; __chacha_avx2(stream, stream_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_stream/chacha/chacha20/amd64/ref/stream.jazz b/src/crypto_stream/chacha/chacha20/amd64/ref/stream.jazz index 7d211ba5..09adbe9a 100644 --- a/src/crypto_stream/chacha/chacha20/amd64/ref/stream.jazz +++ b/src/crypto_stream/chacha/chacha20/amd64/ref/stream.jazz @@ -6,7 +6,7 @@ export fn jade_stream_chacha_chacha20_amd64_ref_xor(reg u64 output input input_l { reg u64 r; __chacha_xor_ref(output, input, input_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -14,7 +14,7 @@ export fn jade_stream_chacha_chacha20_amd64_ref(reg u64 stream stream_length non { reg u64 r; __chacha_ref(stream, stream_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_stream/salsa20/salsa20/amd64/avx/stream.jazz b/src/crypto_stream/salsa20/salsa20/amd64/avx/stream.jazz index ca074b01..36c25ef1 100644 --- a/src/crypto_stream/salsa20/salsa20/amd64/avx/stream.jazz +++ b/src/crypto_stream/salsa20/salsa20/amd64/avx/stream.jazz @@ -6,7 +6,7 @@ export fn jade_stream_salsa20_salsa20_amd64_avx_xor(reg u64 output input input_l { reg u64 r; __salsa20_xor_avx(output, input, input_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -14,7 +14,7 @@ export fn jade_stream_salsa20_salsa20_amd64_avx(reg u64 stream stream_length non { reg u64 r; __salsa20_avx(stream, stream_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_stream/salsa20/salsa20/amd64/avx2/stream.jazz b/src/crypto_stream/salsa20/salsa20/amd64/avx2/stream.jazz index b3d971ad..d51807a9 100644 --- a/src/crypto_stream/salsa20/salsa20/amd64/avx2/stream.jazz +++ b/src/crypto_stream/salsa20/salsa20/amd64/avx2/stream.jazz @@ -6,7 +6,7 @@ export fn jade_stream_salsa20_salsa20_amd64_avx2_xor(reg u64 output input input_ { reg u64 r; __salsa20_xor_avx2(output, input, input_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -14,7 +14,7 @@ export fn jade_stream_salsa20_salsa20_amd64_avx2(reg u64 stream stream_length no { reg u64 r; __salsa20_avx2(stream, stream_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_stream/salsa20/salsa20/amd64/ref/stream.jazz b/src/crypto_stream/salsa20/salsa20/amd64/ref/stream.jazz index 7c259827..0888f53e 100644 --- a/src/crypto_stream/salsa20/salsa20/amd64/ref/stream.jazz +++ b/src/crypto_stream/salsa20/salsa20/amd64/ref/stream.jazz @@ -6,7 +6,7 @@ export fn jade_stream_salsa20_salsa20_amd64_ref_xor(reg u64 output input input_l { reg u64 r; __salsa20_xor_ref(output, input, input_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -14,7 +14,7 @@ export fn jade_stream_salsa20_salsa20_amd64_ref(reg u64 stream stream_length non { reg u64 r; __salsa20_ref(stream, stream_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_stream/salsa20/salsa2012/amd64/avx/stream.jazz b/src/crypto_stream/salsa20/salsa2012/amd64/avx/stream.jazz index d0bfae9d..051c0cc1 100644 --- a/src/crypto_stream/salsa20/salsa2012/amd64/avx/stream.jazz +++ b/src/crypto_stream/salsa20/salsa2012/amd64/avx/stream.jazz @@ -6,7 +6,7 @@ export fn jade_stream_salsa20_salsa2012_amd64_avx_xor(reg u64 output input input { reg u64 r; __salsa20_xor_avx(output, input, input_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -15,7 +15,7 @@ export fn jade_stream_salsa20_salsa2012_amd64_avx(reg u64 stream stream_length n { reg u64 r; __salsa20_avx(stream, stream_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_stream/salsa20/salsa2012/amd64/avx2/stream.jazz b/src/crypto_stream/salsa20/salsa2012/amd64/avx2/stream.jazz index 2bdd27ee..c0b01537 100644 --- a/src/crypto_stream/salsa20/salsa2012/amd64/avx2/stream.jazz +++ b/src/crypto_stream/salsa20/salsa2012/amd64/avx2/stream.jazz @@ -6,7 +6,7 @@ export fn jade_stream_salsa20_salsa2012_amd64_avx2_xor(reg u64 output input inpu { reg u64 r; __salsa20_xor_avx2(output, input, input_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -14,7 +14,7 @@ export fn jade_stream_salsa20_salsa2012_amd64_avx2(reg u64 stream stream_length { reg u64 r; __salsa20_avx2(stream, stream_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_stream/salsa20/salsa2012/amd64/ref/stream.jazz b/src/crypto_stream/salsa20/salsa2012/amd64/ref/stream.jazz index ed8d210d..094e8d5a 100644 --- a/src/crypto_stream/salsa20/salsa2012/amd64/ref/stream.jazz +++ b/src/crypto_stream/salsa20/salsa2012/amd64/ref/stream.jazz @@ -6,7 +6,7 @@ export fn jade_stream_salsa20_salsa2012_amd64_ref_xor(reg u64 output input input { reg u64 r; __salsa20_xor_ref(output, input, input_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -14,7 +14,7 @@ export fn jade_stream_salsa20_salsa2012_amd64_ref(reg u64 stream stream_length n { reg u64 r; __salsa20_ref(stream, stream_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_stream/xsalsa20/amd64/avx/stream.jazz b/src/crypto_stream/xsalsa20/amd64/avx/stream.jazz index 03c090a1..5024e253 100644 --- a/src/crypto_stream/xsalsa20/amd64/avx/stream.jazz +++ b/src/crypto_stream/xsalsa20/amd64/avx/stream.jazz @@ -4,7 +4,7 @@ export fn jade_stream_xsalsa20_amd64_avx_xor(reg u64 output input input_length n { reg u64 r; __xsalsa20_xor_avx(output, input, input_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -12,7 +12,7 @@ export fn jade_stream_xsalsa20_amd64_avx(reg u64 stream stream_length nonce key) { reg u64 r; __xsalsa20_avx(stream, stream_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_stream/xsalsa20/amd64/avx2/stream.jazz b/src/crypto_stream/xsalsa20/amd64/avx2/stream.jazz index bdf46663..d9f010b0 100644 --- a/src/crypto_stream/xsalsa20/amd64/avx2/stream.jazz +++ b/src/crypto_stream/xsalsa20/amd64/avx2/stream.jazz @@ -4,7 +4,7 @@ export fn jade_stream_xsalsa20_amd64_avx2_xor(reg u64 output input input_length { reg u64 r; __xsalsa20_xor_avx2(output, input, input_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -12,7 +12,7 @@ export fn jade_stream_xsalsa20_amd64_avx2(reg u64 stream stream_length nonce key { reg u64 r; __xsalsa20_avx2(stream, stream_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_stream/xsalsa20/amd64/ref/stream.jazz b/src/crypto_stream/xsalsa20/amd64/ref/stream.jazz index f067a499..d657545d 100644 --- a/src/crypto_stream/xsalsa20/amd64/ref/stream.jazz +++ b/src/crypto_stream/xsalsa20/amd64/ref/stream.jazz @@ -4,7 +4,7 @@ export fn jade_stream_xsalsa20_amd64_ref_xor(reg u64 output input input_length n { reg u64 r; __xsalsa20_xor_ref(output, input, input_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } @@ -12,7 +12,7 @@ export fn jade_stream_xsalsa20_amd64_ref(reg u64 stream stream_length nonce key) { reg u64 r; __xsalsa20_ref(stream, stream_length, nonce, key); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_xof/shake128/amd64/avx2/xof.jazz b/src/crypto_xof/shake128/amd64/avx2/xof.jazz index 8e05cd26..4a157695 100644 --- a/src/crypto_xof/shake128/amd64/avx2/xof.jazz +++ b/src/crypto_xof/shake128/amd64/avx2/xof.jazz @@ -4,7 +4,7 @@ export fn jade_xof_shake128_amd64_avx2(reg u64 out outlen in inlen) -> reg u64 { reg u64 r; __shake128_avx2(out, outlen, in, inlen); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_xof/shake128/amd64/ref/xof.jazz b/src/crypto_xof/shake128/amd64/ref/xof.jazz index f9bdd6a3..e937aa4c 100644 --- a/src/crypto_xof/shake128/amd64/ref/xof.jazz +++ b/src/crypto_xof/shake128/amd64/ref/xof.jazz @@ -4,7 +4,7 @@ export fn jade_xof_shake128_amd64_ref(reg u64 out outlen in inlen) -> reg u64 { reg u64 r; __shake128_ref(out, outlen, in, inlen); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_xof/shake256/amd64/avx2/xof.jazz b/src/crypto_xof/shake256/amd64/avx2/xof.jazz index 8a9edce6..a5fe24ae 100644 --- a/src/crypto_xof/shake256/amd64/avx2/xof.jazz +++ b/src/crypto_xof/shake256/amd64/avx2/xof.jazz @@ -4,7 +4,7 @@ export fn jade_xof_shake256_amd64_avx2(reg u64 out outlen in inlen) -> reg u64 { reg u64 r; __shake256_avx2(out, outlen, in, inlen); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_xof/shake256/amd64/ref/xof.jazz b/src/crypto_xof/shake256/amd64/ref/xof.jazz index e9da93ee..3c139805 100644 --- a/src/crypto_xof/shake256/amd64/ref/xof.jazz +++ b/src/crypto_xof/shake256/amd64/ref/xof.jazz @@ -4,7 +4,7 @@ export fn jade_xof_shake256_amd64_ref(reg u64 out outlen in inlen) -> reg u64 { reg u64 r; __shake256_ref(out, outlen, in, inlen); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_xof/shake256/amd64/ref1/xof.jazz b/src/crypto_xof/shake256/amd64/ref1/xof.jazz index 8442120e..aa573677 100644 --- a/src/crypto_xof/shake256/amd64/ref1/xof.jazz +++ b/src/crypto_xof/shake256/amd64/ref1/xof.jazz @@ -4,7 +4,7 @@ export fn jade_xof_shake256_amd64_ref1(reg u64 out outlen in inlen) -> reg u64 { reg u64 r; __shake256_ref1(out, outlen, in, inlen); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } diff --git a/src/crypto_xof/shake256/amd64/spec/xof.jazz b/src/crypto_xof/shake256/amd64/spec/xof.jazz index 34fa1c97..27373dcd 100644 --- a/src/crypto_xof/shake256/amd64/spec/xof.jazz +++ b/src/crypto_xof/shake256/amd64/spec/xof.jazz @@ -4,7 +4,7 @@ export fn jade_xof_shake256_amd64_spec(reg u64 out outlen in inlen) -> reg u64 { reg u64 r; __shake256_spec(out, outlen, in, inlen); - _,_,_,_,_,r = #set0(); + ?{}, r = #set0(); return r; } From 0f6d96e62ab50ce518c3839b7bd195a7fc4e44c7 Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Mon, 5 Dec 2022 19:13:37 +0000 Subject: [PATCH 7/9] args naming : crypto_scalarmult pass --- .../curve25519/amd64/mulx/scalarmult_ct_proof.ec | 4 ++-- .../curve25519/amd64/ref4/scalarmult_ct_proof.ec | 4 ++-- .../curve25519/amd64/ref5/scalarmult_ct_proof.ec | 4 ++-- .../curve25519/amd64/mulx/scalarmult.jazz | 8 ++++---- .../curve25519/amd64/ref4/scalarmult.jazz | 8 ++++---- .../curve25519/amd64/ref5/scalarmult.jazz | 8 ++++---- 6 files changed, 18 insertions(+), 18 deletions(-) diff --git a/proof/crypto_scalarmult/curve25519/amd64/mulx/scalarmult_ct_proof.ec b/proof/crypto_scalarmult/curve25519/amd64/mulx/scalarmult_ct_proof.ec index afa74c02..43fcf3ec 100644 --- a/proof/crypto_scalarmult/curve25519/amd64/mulx/scalarmult_ct_proof.ec +++ b/proof/crypto_scalarmult/curve25519/amd64/mulx/scalarmult_ct_proof.ec @@ -2,14 +2,14 @@ require import Scalarmult_ct. equiv jade_scalarmult_curve25519_amd64_mulx : M.jade_scalarmult_curve25519_amd64_mulx ~ M.jade_scalarmult_curve25519_amd64_mulx : - ={rp, kp, up, M.leakages} ==> ={M.leakages}. + ={q, n, p, 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 : - ={rp, kp, M.leakages} ==> ={M.leakages}. + ={q, n, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_scalarmult/curve25519/amd64/ref4/scalarmult_ct_proof.ec b/proof/crypto_scalarmult/curve25519/amd64/ref4/scalarmult_ct_proof.ec index ab736bdf..960533f4 100644 --- a/proof/crypto_scalarmult/curve25519/amd64/ref4/scalarmult_ct_proof.ec +++ b/proof/crypto_scalarmult/curve25519/amd64/ref4/scalarmult_ct_proof.ec @@ -2,14 +2,14 @@ require import Scalarmult_ct. equiv jade_scalarmult_curve25519_amd64_ref4 : M.jade_scalarmult_curve25519_amd64_ref4 ~ M.jade_scalarmult_curve25519_amd64_ref4 : - ={rp, kp, up, M.leakages} ==> ={M.leakages}. + ={q, n, p, 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 : - ={rp, kp, M.leakages} ==> ={M.leakages}. + ={q, n, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_scalarmult/curve25519/amd64/ref5/scalarmult_ct_proof.ec b/proof/crypto_scalarmult/curve25519/amd64/ref5/scalarmult_ct_proof.ec index a9eaf7d5..09e4bf14 100644 --- a/proof/crypto_scalarmult/curve25519/amd64/ref5/scalarmult_ct_proof.ec +++ b/proof/crypto_scalarmult/curve25519/amd64/ref5/scalarmult_ct_proof.ec @@ -2,14 +2,14 @@ require import Scalarmult_ct. equiv jade_scalarmult_curve25519_amd64_ref5 : M.jade_scalarmult_curve25519_amd64_ref5 ~ M.jade_scalarmult_curve25519_amd64_ref5 : - ={rp, kp, up, M.leakages} ==> ={M.leakages}. + ={q, n, p, 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 : - ={rp, kp, M.leakages} ==> ={M.leakages}. + ={q, n, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/src/crypto_scalarmult/curve25519/amd64/mulx/scalarmult.jazz b/src/crypto_scalarmult/curve25519/amd64/mulx/scalarmult.jazz index 9822a01a..04672100 100644 --- a/src/crypto_scalarmult/curve25519/amd64/mulx/scalarmult.jazz +++ b/src/crypto_scalarmult/curve25519/amd64/mulx/scalarmult.jazz @@ -1,17 +1,17 @@ require "curve25519.jinc" -export fn jade_scalarmult_curve25519_amd64_mulx(reg u64 rp kp up) -> reg u64 +export fn jade_scalarmult_curve25519_amd64_mulx(reg u64 q n p) -> reg u64 { reg u64 r; - __curve25519_mulx(rp, kp, up); + __curve25519_mulx(q, n, p); ?{}, r = #set0(); return r; } -export fn jade_scalarmult_curve25519_amd64_mulx_base(reg u64 rp kp) -> reg u64 +export fn jade_scalarmult_curve25519_amd64_mulx_base(reg u64 q n) -> reg u64 { reg u64 r; - __curve25519_mulx_base(rp, kp); + __curve25519_mulx_base(q, n); ?{}, r = #set0(); return r; } diff --git a/src/crypto_scalarmult/curve25519/amd64/ref4/scalarmult.jazz b/src/crypto_scalarmult/curve25519/amd64/ref4/scalarmult.jazz index cb3c9707..9fb9ac00 100644 --- a/src/crypto_scalarmult/curve25519/amd64/ref4/scalarmult.jazz +++ b/src/crypto_scalarmult/curve25519/amd64/ref4/scalarmult.jazz @@ -1,17 +1,17 @@ require "curve25519.jinc" -export fn jade_scalarmult_curve25519_amd64_ref4(reg u64 rp kp up) -> reg u64 +export fn jade_scalarmult_curve25519_amd64_ref4(reg u64 q n p) -> reg u64 { reg u64 r; - __curve25519_ref4(rp, kp, up); + __curve25519_ref4(q, n, p); ?{}, r = #set0(); return r; } -export fn jade_scalarmult_curve25519_amd64_ref4_base(reg u64 rp kp) -> reg u64 +export fn jade_scalarmult_curve25519_amd64_ref4_base(reg u64 q n) -> reg u64 { reg u64 r; - __curve25519_ref4_base(rp, kp); + __curve25519_ref4_base(q, n); ?{}, r = #set0(); return r; } diff --git a/src/crypto_scalarmult/curve25519/amd64/ref5/scalarmult.jazz b/src/crypto_scalarmult/curve25519/amd64/ref5/scalarmult.jazz index cdb1b4ef..f171a571 100644 --- a/src/crypto_scalarmult/curve25519/amd64/ref5/scalarmult.jazz +++ b/src/crypto_scalarmult/curve25519/amd64/ref5/scalarmult.jazz @@ -1,17 +1,17 @@ require "curve25519.jinc" -export fn jade_scalarmult_curve25519_amd64_ref5(reg u64 rp kp up) -> reg u64 +export fn jade_scalarmult_curve25519_amd64_ref5(reg u64 q n p) -> reg u64 { reg u64 r; - __curve25519_ref5(rp, kp, up); + __curve25519_ref5(q, n, p); ?{}, r = #set0(); return r; } -export fn jade_scalarmult_curve25519_amd64_ref5_base(reg u64 rp kp) -> reg u64 +export fn jade_scalarmult_curve25519_amd64_ref5_base(reg u64 q n) -> reg u64 { reg u64 r; - __curve25519_ref5_base(rp, kp); + __curve25519_ref5_base(q, n); ?{}, r = #set0(); return r; } From 499d342c38b08c1209151af6e1ed56161b726581 Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Mon, 5 Dec 2022 19:23:31 +0000 Subject: [PATCH 8/9] args naming : crypto_secretbox pass --- .../xsalsa20poly1305/amd64/avx/secretbox.jazz | 10 +++++----- .../xsalsa20poly1305/amd64/avx2/secretbox.jazz | 10 +++++----- .../xsalsa20poly1305/amd64/ref/secretbox.jazz | 10 +++++----- 3 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/crypto_secretbox/xsalsa20poly1305/amd64/avx/secretbox.jazz b/src/crypto_secretbox/xsalsa20poly1305/amd64/avx/secretbox.jazz index cfe15e42..4347319d 100644 --- a/src/crypto_secretbox/xsalsa20poly1305/amd64/avx/secretbox.jazz +++ b/src/crypto_secretbox/xsalsa20poly1305/amd64/avx/secretbox.jazz @@ -1,17 +1,17 @@ require "xsalsa20poly1305.jinc" -export fn jade_secretbox_xsalsa20poly1305_amd64_avx(reg u64 c m mlen nonce key) -> reg u64 +export fn jade_secretbox_xsalsa20poly1305_amd64_avx(reg u64 ciphertext plaintext plaintext_length nonce key) -> reg u64 { reg u64 r; - mlen = mlen; - r = __xsalsa20poly1305_avx(c, m, mlen, nonce, key); + plaintext_length = plaintext_length; + r = __xsalsa20poly1305_avx(ciphertext, plaintext, plaintext_length, nonce, key); return r; } -export fn jade_secretbox_xsalsa20poly1305_amd64_avx_open(reg u64 m c clen nonce key) -> reg u64 +export fn jade_secretbox_xsalsa20poly1305_amd64_avx_open(reg u64 plaintext ciphertext ciphertext_length nonce key) -> reg u64 { reg u64 r; - r = __xsalsa20poly1305_avx_open(m, c, clen, nonce, key); + r = __xsalsa20poly1305_avx_open(plaintext, ciphertext, ciphertext_length, nonce, key); return r; } diff --git a/src/crypto_secretbox/xsalsa20poly1305/amd64/avx2/secretbox.jazz b/src/crypto_secretbox/xsalsa20poly1305/amd64/avx2/secretbox.jazz index 6f7ceab1..5b9a648a 100644 --- a/src/crypto_secretbox/xsalsa20poly1305/amd64/avx2/secretbox.jazz +++ b/src/crypto_secretbox/xsalsa20poly1305/amd64/avx2/secretbox.jazz @@ -1,17 +1,17 @@ require "xsalsa20poly1305.jinc" -export fn jade_secretbox_xsalsa20poly1305_amd64_avx2(reg u64 c m mlen nonce key) -> reg u64 +export fn jade_secretbox_xsalsa20poly1305_amd64_avx2(reg u64 ciphertext plaintext plaintext_length nonce key) -> reg u64 { reg u64 r; - mlen = mlen; - r = __xsalsa20poly1305_avx2(c, m, mlen, nonce, key); + plaintext_length = plaintext_length; + r = __xsalsa20poly1305_avx2(ciphertext, plaintext, plaintext_length, nonce, key); return r; } -export fn jade_secretbox_xsalsa20poly1305_amd64_avx2_open(reg u64 m c clen nonce key) -> reg u64 +export fn jade_secretbox_xsalsa20poly1305_amd64_avx2_open(reg u64 plaintext ciphertext ciphertext_length nonce key) -> reg u64 { reg u64 r; - r = __xsalsa20poly1305_avx2_open(m, c, clen, nonce, key); + r = __xsalsa20poly1305_avx2_open(plaintext, ciphertext, ciphertext_length, nonce, key); return r; } diff --git a/src/crypto_secretbox/xsalsa20poly1305/amd64/ref/secretbox.jazz b/src/crypto_secretbox/xsalsa20poly1305/amd64/ref/secretbox.jazz index 9e112e08..15db96f4 100644 --- a/src/crypto_secretbox/xsalsa20poly1305/amd64/ref/secretbox.jazz +++ b/src/crypto_secretbox/xsalsa20poly1305/amd64/ref/secretbox.jazz @@ -1,17 +1,17 @@ require "xsalsa20poly1305.jinc" -export fn jade_secretbox_xsalsa20poly1305_amd64_ref(reg u64 c m mlen nonce key) -> reg u64 +export fn jade_secretbox_xsalsa20poly1305_amd64_ref(reg u64 ciphertext plaintext plaintext_length nonce key) -> reg u64 { reg u64 r; - mlen = mlen; - r = __xsalsa20poly1305_ref(c, m, mlen, nonce, key); + plaintext_length = plaintext_length; + r = __xsalsa20poly1305_ref(ciphertext, plaintext, plaintext_length, nonce, key); return r; } -export fn jade_secretbox_xsalsa20poly1305_amd64_ref_open(reg u64 m c clen nonce key) -> reg u64 +export fn jade_secretbox_xsalsa20poly1305_amd64_ref_open(reg u64 plaintext ciphertext ciphertext_length nonce key) -> reg u64 { reg u64 r; - r = __xsalsa20poly1305_ref_open(m, c, clen, nonce, key); + r = __xsalsa20poly1305_ref_open(plaintext, ciphertext, ciphertext_length, nonce, key); return r; } From 62be589964cd55e486c6cecd0551a7bc6d018720 Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Mon, 5 Dec 2022 19:31:50 +0000 Subject: [PATCH 9/9] args naming : crypto_xof pass --- proof/crypto_xof/shake128/amd64/avx2/xof_ct_proof.ec | 2 +- proof/crypto_xof/shake128/amd64/ref/xof_ct_proof.ec | 2 +- proof/crypto_xof/shake256/amd64/avx2/xof_ct_proof.ec | 2 +- proof/crypto_xof/shake256/amd64/ref/xof_ct_proof.ec | 2 +- proof/crypto_xof/shake256/amd64/ref1/xof_ct_proof.ec | 2 +- proof/crypto_xof/shake256/amd64/spec/xof_ct_proof.ec | 2 +- src/crypto_xof/shake128/amd64/avx2/xof.jazz | 4 ++-- src/crypto_xof/shake128/amd64/ref/xof.jazz | 4 ++-- src/crypto_xof/shake256/amd64/avx2/xof.jazz | 4 ++-- src/crypto_xof/shake256/amd64/ref/xof.jazz | 5 ++--- src/crypto_xof/shake256/amd64/ref1/xof.jazz | 4 ++-- src/crypto_xof/shake256/amd64/spec/xof.jazz | 4 ++-- 12 files changed, 18 insertions(+), 19 deletions(-) diff --git a/proof/crypto_xof/shake128/amd64/avx2/xof_ct_proof.ec b/proof/crypto_xof/shake128/amd64/avx2/xof_ct_proof.ec index 857bf227..a0e60680 100644 --- a/proof/crypto_xof/shake128/amd64/avx2/xof_ct_proof.ec +++ b/proof/crypto_xof/shake128/amd64/avx2/xof_ct_proof.ec @@ -2,7 +2,7 @@ require import Xof_ct. equiv eq_jade_xof_shake128_amd64_avx2_ct : M.jade_xof_shake128_amd64_avx2 ~ M.jade_xof_shake128_amd64_avx2 : - ={out, outlen, in_0, inlen, M.leakages} ==> ={M.leakages}. + ={output, output_length, input, input_length, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_xof/shake128/amd64/ref/xof_ct_proof.ec b/proof/crypto_xof/shake128/amd64/ref/xof_ct_proof.ec index 562018fe..f3c9818e 100644 --- a/proof/crypto_xof/shake128/amd64/ref/xof_ct_proof.ec +++ b/proof/crypto_xof/shake128/amd64/ref/xof_ct_proof.ec @@ -2,7 +2,7 @@ require import Xof_ct. equiv eq_jade_xof_shake128_amd64_ref_ct : M.jade_xof_shake128_amd64_ref ~ M.jade_xof_shake128_amd64_ref : - ={out, outlen, in_0, inlen, M.leakages} ==> ={M.leakages}. + ={output, output_length, input, input_length, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_xof/shake256/amd64/avx2/xof_ct_proof.ec b/proof/crypto_xof/shake256/amd64/avx2/xof_ct_proof.ec index 03050f6c..b3a60a40 100644 --- a/proof/crypto_xof/shake256/amd64/avx2/xof_ct_proof.ec +++ b/proof/crypto_xof/shake256/amd64/avx2/xof_ct_proof.ec @@ -2,7 +2,7 @@ require import Xof_ct. equiv eq_jade_xof_shake256_amd64_avx2_ct : M.jade_xof_shake256_amd64_avx2 ~ M.jade_xof_shake256_amd64_avx2 : - ={out, outlen, in_0, inlen, M.leakages} ==> ={M.leakages}. + ={output, output_length, input, input_length, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_xof/shake256/amd64/ref/xof_ct_proof.ec b/proof/crypto_xof/shake256/amd64/ref/xof_ct_proof.ec index 8871a4be..49f188b4 100644 --- a/proof/crypto_xof/shake256/amd64/ref/xof_ct_proof.ec +++ b/proof/crypto_xof/shake256/amd64/ref/xof_ct_proof.ec @@ -2,7 +2,7 @@ require import Xof_ct. equiv eq_jade_xof_shake256_amd64_ref_ct : M.jade_xof_shake256_amd64_ref ~ M.jade_xof_shake256_amd64_ref : - ={out, outlen, in_0, inlen, M.leakages} ==> ={M.leakages}. + ={output, output_length, input, input_length, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_xof/shake256/amd64/ref1/xof_ct_proof.ec b/proof/crypto_xof/shake256/amd64/ref1/xof_ct_proof.ec index 7f69d645..8c8811dd 100644 --- a/proof/crypto_xof/shake256/amd64/ref1/xof_ct_proof.ec +++ b/proof/crypto_xof/shake256/amd64/ref1/xof_ct_proof.ec @@ -2,7 +2,7 @@ require import Xof_ct. equiv eq_jade_xof_shake256_amd64_ref1_ct : M.jade_xof_shake256_amd64_ref1 ~ M.jade_xof_shake256_amd64_ref1 : - ={out, outlen, in_0, inlen, M.leakages} ==> ={M.leakages}. + ={output, output_length, input, input_length, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/proof/crypto_xof/shake256/amd64/spec/xof_ct_proof.ec b/proof/crypto_xof/shake256/amd64/spec/xof_ct_proof.ec index b2a84cbc..d659c6f4 100644 --- a/proof/crypto_xof/shake256/amd64/spec/xof_ct_proof.ec +++ b/proof/crypto_xof/shake256/amd64/spec/xof_ct_proof.ec @@ -2,7 +2,7 @@ require import Xof_ct. equiv eq_jade_xof_shake256_amd64_spec_ct : M.jade_xof_shake256_amd64_spec ~ M.jade_xof_shake256_amd64_spec : - ={out, outlen, in_0, inlen, M.leakages} ==> ={M.leakages}. + ={output, output_length, input, input_length, M.leakages} ==> ={M.leakages}. proof. proc; inline *; sim => />. qed. diff --git a/src/crypto_xof/shake128/amd64/avx2/xof.jazz b/src/crypto_xof/shake128/amd64/avx2/xof.jazz index 4a157695..23dd3b45 100644 --- a/src/crypto_xof/shake128/amd64/avx2/xof.jazz +++ b/src/crypto_xof/shake128/amd64/avx2/xof.jazz @@ -1,9 +1,9 @@ require "shake128.jinc" -export fn jade_xof_shake128_amd64_avx2(reg u64 out outlen in inlen) -> reg u64 +export fn jade_xof_shake128_amd64_avx2(reg u64 output output_length input input_length) -> reg u64 { reg u64 r; - __shake128_avx2(out, outlen, in, inlen); + __shake128_avx2(output, output_length, input, input_length); ?{}, r = #set0(); return r; } diff --git a/src/crypto_xof/shake128/amd64/ref/xof.jazz b/src/crypto_xof/shake128/amd64/ref/xof.jazz index e937aa4c..ad386786 100644 --- a/src/crypto_xof/shake128/amd64/ref/xof.jazz +++ b/src/crypto_xof/shake128/amd64/ref/xof.jazz @@ -1,9 +1,9 @@ require "shake128.jinc" -export fn jade_xof_shake128_amd64_ref(reg u64 out outlen in inlen) -> reg u64 +export fn jade_xof_shake128_amd64_ref(reg u64 output output_length input input_length) -> reg u64 { reg u64 r; - __shake128_ref(out, outlen, in, inlen); + __shake128_ref(output, output_length, input, input_length); ?{}, r = #set0(); return r; } diff --git a/src/crypto_xof/shake256/amd64/avx2/xof.jazz b/src/crypto_xof/shake256/amd64/avx2/xof.jazz index a5fe24ae..169f7701 100644 --- a/src/crypto_xof/shake256/amd64/avx2/xof.jazz +++ b/src/crypto_xof/shake256/amd64/avx2/xof.jazz @@ -1,9 +1,9 @@ require "shake256.jinc" -export fn jade_xof_shake256_amd64_avx2(reg u64 out outlen in inlen) -> reg u64 +export fn jade_xof_shake256_amd64_avx2(reg u64 output output_length input input_length) -> reg u64 { reg u64 r; - __shake256_avx2(out, outlen, in, inlen); + __shake256_avx2(output, output_length, input, input_length); ?{}, r = #set0(); return r; } diff --git a/src/crypto_xof/shake256/amd64/ref/xof.jazz b/src/crypto_xof/shake256/amd64/ref/xof.jazz index 3c139805..8eb4e643 100644 --- a/src/crypto_xof/shake256/amd64/ref/xof.jazz +++ b/src/crypto_xof/shake256/amd64/ref/xof.jazz @@ -1,11 +1,10 @@ require "shake256.jinc" -export fn jade_xof_shake256_amd64_ref(reg u64 out outlen in inlen) -> reg u64 +export fn jade_xof_shake256_amd64_ref(reg u64 output output_length input input_length) -> reg u64 { reg u64 r; - __shake256_ref(out, outlen, in, inlen); + __shake256_ref(output, output_length, input, input_length); ?{}, r = #set0(); return r; } - diff --git a/src/crypto_xof/shake256/amd64/ref1/xof.jazz b/src/crypto_xof/shake256/amd64/ref1/xof.jazz index aa573677..2051d26f 100644 --- a/src/crypto_xof/shake256/amd64/ref1/xof.jazz +++ b/src/crypto_xof/shake256/amd64/ref1/xof.jazz @@ -1,9 +1,9 @@ require "shake256.jinc" -export fn jade_xof_shake256_amd64_ref1(reg u64 out outlen in inlen) -> reg u64 +export fn jade_xof_shake256_amd64_ref1(reg u64 output output_length input input_length) -> reg u64 { reg u64 r; - __shake256_ref1(out, outlen, in, inlen); + __shake256_ref1(output, output_length, input, input_length); ?{}, r = #set0(); return r; } diff --git a/src/crypto_xof/shake256/amd64/spec/xof.jazz b/src/crypto_xof/shake256/amd64/spec/xof.jazz index 27373dcd..f7045070 100644 --- a/src/crypto_xof/shake256/amd64/spec/xof.jazz +++ b/src/crypto_xof/shake256/amd64/spec/xof.jazz @@ -1,9 +1,9 @@ require "shake256.jinc" -export fn jade_xof_shake256_amd64_spec(reg u64 out outlen in inlen) -> reg u64 +export fn jade_xof_shake256_amd64_spec(reg u64 output output_length input input_length) -> reg u64 { reg u64 r; - __shake256_spec(out, outlen, in, inlen); + __shake256_spec(output, output_length, input, input_length); ?{}, r = #set0(); return r; }