Skip to content

Commit

Permalink
Merge pull request #34 from formosa-crypto/rename_args
Browse files Browse the repository at this point in the history
Rename args
  • Loading branch information
tfaoliveira authored Dec 5, 2022
2 parents 2e4427e + 62be589 commit 6181b30
Show file tree
Hide file tree
Showing 91 changed files with 419 additions and 383 deletions.
2 changes: 1 addition & 1 deletion proof/crypto_hash/sha256/amd64/ref/hash_ct_proof.ec
Original file line number Diff line number Diff line change
Expand Up @@ -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.
2 changes: 1 addition & 1 deletion proof/crypto_hash/sha3-224/amd64/avx2/hash_ct_proof.ec
Original file line number Diff line number Diff line change
Expand Up @@ -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.
2 changes: 1 addition & 1 deletion proof/crypto_hash/sha3-224/amd64/ref/hash_ct_proof.ec
Original file line number Diff line number Diff line change
Expand Up @@ -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.
2 changes: 1 addition & 1 deletion proof/crypto_hash/sha3-256/amd64/avx2/hash_ct_proof.ec
Original file line number Diff line number Diff line change
Expand Up @@ -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.
2 changes: 1 addition & 1 deletion proof/crypto_hash/sha3-256/amd64/ref/hash_ct_proof.ec
Original file line number Diff line number Diff line change
Expand Up @@ -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.
2 changes: 1 addition & 1 deletion proof/crypto_hash/sha3-384/amd64/avx2/hash_ct_proof.ec
Original file line number Diff line number Diff line change
Expand Up @@ -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.
2 changes: 1 addition & 1 deletion proof/crypto_hash/sha3-384/amd64/ref/hash_ct_proof.ec
Original file line number Diff line number Diff line change
Expand Up @@ -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.
2 changes: 1 addition & 1 deletion proof/crypto_hash/sha3-512/amd64/avx2/hash_ct_proof.ec
Original file line number Diff line number Diff line change
Expand Up @@ -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.
2 changes: 1 addition & 1 deletion proof/crypto_hash/sha3-512/amd64/ref/hash_ct_proof.ec
Original file line number Diff line number Diff line change
Expand Up @@ -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.
2 changes: 1 addition & 1 deletion proof/crypto_hash/sha512/amd64/ref/hash_ct_proof.ec
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 => />.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Original file line number Diff line number Diff line change
Expand Up @@ -2,14 +2,31 @@ 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.

(** **)

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.

Original file line number Diff line number Diff line change
Expand Up @@ -2,14 +2,30 @@ 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.

(** **)

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.
Original file line number Diff line number Diff line change
Expand Up @@ -2,14 +2,30 @@ 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.

(** **)

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.
Loading

0 comments on commit 6181b30

Please sign in to comment.