diff --git a/eqc_test/enacl_ext_eqc.erl b/eqc_test/enacl_ext_eqc.erl new file mode 100644 index 0000000..ee0eab2 --- /dev/null +++ b/eqc_test/enacl_ext_eqc.erl @@ -0,0 +1,24 @@ +-module(enacl_ext_eqc). + +-include_lib("eqc/include/eqc.hrl"). +-compile(export_all). + +public_keypair() -> + ?LET(#{ public := PK, secret := SK}, enacl_ext:curve25519_keypair(), + {PK, SK}). + +prop_public_key() -> + ?FORALL({PK, SK}, public_keypair(), + begin + equals(PK, enacl_ext:curve25519_public_key(SK)) + end). + +prop_shared_secret() -> + ?FORALL([{PK1, SK1}, {PK2, SK2}], + [public_keypair(), public_keypair()], + begin + Alice = enacl_ext:curve25519_shared(SK1, PK2), + Bob = enacl_ext:curve25519_shared(SK2, PK1), + equals(Alice, Bob) + end). +