Modify QuickCheck tests to be runnable to eqc-mini.

This involves:
- Removing calls to conjunction function
- Modifying fault* functions to _always_ return "Good" generator
- Commenting-out the eqc_parallelize parse_transform
This commit is contained in:
Zane Beckwith 2017-08-16 21:17:28 +00:00
parent 05420f8a6b
commit 207ec85f8c

View File

@ -2,7 +2,11 @@
-include_lib("eqc/include/eqc.hrl"). -include_lib("eqc/include/eqc.hrl").
-compile(export_all). -compile(export_all).
-compile({parse_transform, eqc_parallelize}). %% -compile({parse_transform, eqc_parallelize}).
z_fault(_Bad, Good) -> Good.
z_fault_rate(_1, _2, Gen) -> Gen.
non_byte_int() -> non_byte_int() ->
oneof([ oneof([
@ -14,7 +18,7 @@ g_iolist() ->
?SIZED(Sz, g_iolist(Sz)). ?SIZED(Sz, g_iolist(Sz)).
g_iolist(0) -> g_iolist(0) ->
fault( z_fault(
oneof([ oneof([
elements([a,b,c]), elements([a,b,c]),
real(), real(),
@ -22,7 +26,7 @@ g_iolist(0) ->
]), ]),
return([])); return([]));
g_iolist(N) -> g_iolist(N) ->
fault( z_fault(
oneof([ oneof([
elements([a,b,c]), elements([a,b,c]),
real(), real(),
@ -34,7 +38,7 @@ g_iolist(N) ->
])). ])).
g_iodata() -> g_iodata() ->
fault( z_fault(
oneof([elements([a,b,c]), real()]), oneof([elements([a,b,c]), real()]),
oneof([binary(), g_iolist(), eqc_gen:largebinary(64*1024)])). oneof([binary(), g_iolist(), eqc_gen:largebinary(64*1024)])).
@ -50,7 +54,7 @@ v_iodata(Structure) -> v_iolist(Structure).
%% Generator for binaries of a given size with different properties and fault injection: %% Generator for binaries of a given size with different properties and fault injection:
g_binary(Sz) -> g_binary(Sz) ->
fault(g_binary_bad(Sz), g_binary_good(Sz)). z_fault(g_binary_bad(Sz), g_binary_good(Sz)).
g_binary_good(Sz) when Sz =< 32 -> binary(Sz); g_binary_good(Sz) when Sz =< 32 -> binary(Sz);
g_binary_good(Sz) -> eqc_gen:largebinary(Sz). g_binary_good(Sz) -> eqc_gen:largebinary(Sz).
@ -74,7 +78,7 @@ nonce_valid(N) -> v_binary(enacl:box_nonce_size(), N).
%% Generator of natural numbers %% Generator of natural numbers
g_nat() -> g_nat() ->
fault(g_nat_bad(), nat()). z_fault(g_nat_bad(), nat()).
g_nat_bad() -> g_nat_bad() ->
oneof([ oneof([
@ -106,7 +110,7 @@ keypair_bad() ->
end). end).
keypair() -> keypair() ->
fault(keypair_bad(), keypair_good()). z_fault(keypair_bad(), keypair_good()).
%% CRYPTO BOX %% CRYPTO BOX
%% --------------------------- %% ---------------------------
@ -158,10 +162,10 @@ failure(X) -> {failure, X}.
prop_box_correct() -> prop_box_correct() ->
?FORALL({Msg, Nonce, {PK1, SK1}, {PK2, SK2}}, ?FORALL({Msg, Nonce, {PK1, SK1}, {PK2, SK2}},
{fault_rate(1, 40, g_iodata()), {z_fault_rate(1, 40, g_iodata()),
fault_rate(1, 40, nonce()), z_fault_rate(1, 40, nonce()),
fault_rate(1, 40, keypair()), z_fault_rate(1, 40, keypair()),
fault_rate(1, 40, keypair())}, z_fault_rate(1, 40, keypair())},
begin begin
case v_iodata(Msg) andalso nonce_valid(Nonce) andalso keypair_valid(PK1, SK1) andalso keypair_valid(PK2, SK2) of case v_iodata(Msg) andalso nonce_valid(Nonce) andalso keypair_valid(PK1, SK1) andalso keypair_valid(PK2, SK2) of
true -> true ->
@ -182,10 +186,10 @@ prop_box_correct() ->
prop_box_failure_integrity() -> prop_box_failure_integrity() ->
?FORALL({Msg, Nonce, {PK1, SK1}, {PK2, SK2}}, ?FORALL({Msg, Nonce, {PK1, SK1}, {PK2, SK2}},
{fault_rate(1, 40, g_iodata()), {z_fault_rate(1, 40, g_iodata()),
fault_rate(1, 40, nonce()), z_fault_rate(1, 40, nonce()),
fault_rate(1, 40, keypair()), z_fault_rate(1, 40, keypair()),
fault_rate(1, 40, keypair())}, z_fault_rate(1, 40, keypair())},
begin begin
case v_iodata(Msg) case v_iodata(Msg)
andalso nonce_valid(Nonce) andalso nonce_valid(Nonce)
@ -207,7 +211,7 @@ prop_box_failure_integrity() ->
end). end).
prop_seal_box_failure_integrity() -> prop_seal_box_failure_integrity() ->
?FORALL({Msg, {PK1, SK1}}, {fault_rate(1,40,g_iodata()), fault_rate(1,40,keypair())}, ?FORALL({Msg, {PK1, SK1}}, {z_fault_rate(1,40,g_iodata()), z_fault_rate(1,40,keypair())},
begin begin
case v_iodata(Msg) andalso keypair_valid(PK1, SK1) of case v_iodata(Msg) andalso keypair_valid(PK1, SK1) of
true -> true ->
@ -225,8 +229,8 @@ prop_seal_box_failure_integrity() ->
prop_seal_box_correct() -> prop_seal_box_correct() ->
?FORALL({Msg, {PK1, SK1}}, ?FORALL({Msg, {PK1, SK1}},
{fault_rate(1, 40, g_iodata()), {z_fault_rate(1, 40, g_iodata()),
fault_rate(1, 40, keypair())}, z_fault_rate(1, 40, keypair())},
begin begin
case v_iodata(Msg) andalso keypair_valid(PK1, SK1) of case v_iodata(Msg) andalso keypair_valid(PK1, SK1) of
true -> true ->
@ -243,7 +247,7 @@ prop_seal_box_correct() ->
%% PRECOMPUTATIONS %% PRECOMPUTATIONS
beforenm_key() -> beforenm_key() ->
?LET([{PK1, SK1}, {PK2, SK2}], [fault_rate(1, 40, keypair()), fault_rate(1, 40, keypair())], ?LET([{PK1, SK1}, {PK2, SK2}], [z_fault_rate(1, 40, keypair()), z_fault_rate(1, 40, keypair())],
case keypair_valid(PK1, SK1) andalso keypair_valid(PK2, SK2) of case keypair_valid(PK1, SK1) andalso keypair_valid(PK2, SK2) of
true -> true ->
enacl:box_beforenm(PK1, SK2); enacl:box_beforenm(PK1, SK2);
@ -259,7 +263,7 @@ v_key(K) when is_binary(K) -> byte_size(K) == enacl:box_beforenm_bytes();
v_key(_) -> false. v_key(_) -> false.
prop_beforenm_correct() -> prop_beforenm_correct() ->
?FORALL([{PK1, SK1}, {PK2, SK2}], [fault_rate(1, 40, keypair()), fault_rate(1, 40, keypair())], ?FORALL([{PK1, SK1}, {PK2, SK2}], [z_fault_rate(1, 40, keypair()), z_fault_rate(1, 40, keypair())],
case keypair_valid(PK1, SK1) andalso keypair_valid(PK2, SK2) of case keypair_valid(PK1, SK1) andalso keypair_valid(PK2, SK2) of
true -> true ->
equals(enacl:box_beforenm(PK1, SK2), enacl:box_beforenm(PK2, SK1)); equals(enacl:box_beforenm(PK1, SK2), enacl:box_beforenm(PK2, SK1));
@ -272,9 +276,9 @@ prop_beforenm_correct() ->
prop_afternm_correct() -> prop_afternm_correct() ->
?FORALL([Msg, Nonce, Key], ?FORALL([Msg, Nonce, Key],
[fault_rate(1, 40, g_iodata()), [z_fault_rate(1, 40, g_iodata()),
fault_rate(1, 40, nonce()), z_fault_rate(1, 40, nonce()),
fault_rate(1, 40, beforenm_key())], z_fault_rate(1, 40, beforenm_key())],
begin begin
case v_iodata(Msg) andalso nonce_valid(Nonce) andalso v_key(Key) of case v_iodata(Msg) andalso nonce_valid(Nonce) andalso v_key(Key) of
true -> true ->
@ -325,7 +329,7 @@ sign_keypair_good() ->
return(enacl:sign_keypair()). return(enacl:sign_keypair()).
sign_keypair() -> sign_keypair() ->
fault(sign_keypair_bad(), sign_keypair_good()). z_fault(sign_keypair_bad(), sign_keypair_good()).
sign_keypair_public_valid(#{ public := Public }) sign_keypair_public_valid(#{ public := Public })
when is_binary(Public) -> when is_binary(Public) ->
@ -342,8 +346,8 @@ sign_keypair_valid(KP) ->
prop_sign_detached() -> prop_sign_detached() ->
?FORALL({Msg, KeyPair}, ?FORALL({Msg, KeyPair},
{fault_rate(1, 40, g_iodata()), {z_fault_rate(1, 40, g_iodata()),
fault_rate(1, 40, sign_keypair())}, z_fault_rate(1, 40, sign_keypair())},
begin begin
case v_iodata(Msg) andalso sign_keypair_secret_valid(KeyPair) of case v_iodata(Msg) andalso sign_keypair_secret_valid(KeyPair) of
true -> true ->
@ -358,8 +362,8 @@ prop_sign_detached() ->
prop_sign() -> prop_sign() ->
?FORALL({Msg, KeyPair}, ?FORALL({Msg, KeyPair},
{fault_rate(1, 40, g_iodata()), {z_fault_rate(1, 40, g_iodata()),
fault_rate(1, 40, sign_keypair())}, z_fault_rate(1, 40, sign_keypair())},
begin begin
case v_iodata(Msg) andalso sign_keypair_secret_valid(KeyPair) of case v_iodata(Msg) andalso sign_keypair_secret_valid(KeyPair) of
true -> true ->
@ -403,10 +407,10 @@ signed_message_bad_d() ->
{binary(), oneof([a, int(), ?SUCHTHAT(B, binary(Sz), byte_size(B) /= Sz)])}. {binary(), oneof([a, int(), ?SUCHTHAT(B, binary(Sz), byte_size(B) /= Sz)])}.
signed_message(M) -> signed_message(M) ->
fault(signed_message_bad(), signed_message_good(M)). z_fault(signed_message_bad(), signed_message_good(M)).
signed_message_d(M) -> signed_message_d(M) ->
fault(signed_message_bad(), signed_message_good(M)). z_fault(signed_message_bad(), signed_message_good(M)).
signed_message_valid({valid, _}, _) -> true; signed_message_valid({valid, _}, _) -> true;
signed_message_valid({invalid, _}, _) -> true; signed_message_valid({invalid, _}, _) -> true;
@ -451,18 +455,18 @@ prop_sign_open() ->
key_sz(Sz) -> key_sz(Sz) ->
equals(enacl:secretbox_key_size(), Sz). equals(enacl:secretbox_key_size(), Sz).
prop_key_sizes() -> %% prop_key_sizes() ->
conjunction([{secret, key_sz(enacl:secretbox_key_size())}, %% conjunction([{secret, key_sz(enacl:secretbox_key_size())},
{stream, key_sz(enacl:stream_key_size())}, %% {stream, key_sz(enacl:stream_key_size())},
{auth, key_sz(enacl:auth_key_size())}, %% {auth, key_sz(enacl:auth_key_size())},
{onetimeauth, key_sz(enacl:onetime_auth_key_size())}]). %% {onetimeauth, key_sz(enacl:onetime_auth_key_size())}]).
nonce_sz(Sz) -> nonce_sz(Sz) ->
equals(enacl:secretbox_nonce_size(), Sz). equals(enacl:secretbox_nonce_size(), Sz).
prop_nonce_sizes() -> %% prop_nonce_sizes() ->
conjunction([{secret, nonce_sz(enacl:secretbox_nonce_size())}, %% conjunction([{secret, nonce_sz(enacl:secretbox_nonce_size())},
{stream, nonce_sz(enacl:stream_nonce_size())}]). %% {stream, nonce_sz(enacl:stream_nonce_size())}]).
secret_key_good() -> secret_key_good() ->
Sz = enacl:secretbox_key_size(), Sz = enacl:secretbox_key_size(),
@ -474,7 +478,7 @@ secret_key_bad() ->
?SUCHTHAT(B, binary(), byte_size(B) /= enacl:secretbox_key_size())]). ?SUCHTHAT(B, binary(), byte_size(B) /= enacl:secretbox_key_size())]).
secret_key() -> secret_key() ->
fault(secret_key_bad(), secret_key_good()). z_fault(secret_key_bad(), secret_key_good()).
secret_key_valid(SK) when is_binary(SK) -> secret_key_valid(SK) when is_binary(SK) ->
Sz = enacl:secretbox_key_size(), Sz = enacl:secretbox_key_size(),
@ -497,9 +501,9 @@ secretbox_open(Msg, Nonce, Key) ->
prop_secretbox_correct() -> prop_secretbox_correct() ->
?FORALL({Msg, Nonce, Key}, ?FORALL({Msg, Nonce, Key},
{fault_rate(1, 40, g_iodata()), {z_fault_rate(1, 40, g_iodata()),
fault_rate(1, 40, nonce()), z_fault_rate(1, 40, nonce()),
fault_rate(1, 40, secret_key())}, z_fault_rate(1, 40, secret_key())},
begin begin
case v_iodata(Msg) andalso nonce_valid(Nonce) andalso secret_key_valid(Key) of case v_iodata(Msg) andalso nonce_valid(Nonce) andalso secret_key_valid(Key) of
true -> true ->
@ -527,8 +531,8 @@ prop_secretbox_failure_integrity() ->
prop_stream_correct() -> prop_stream_correct() ->
?FORALL({Len, Nonce, Key}, ?FORALL({Len, Nonce, Key},
{int(), {int(),
fault_rate(1, 40, nonce()), z_fault_rate(1, 40, nonce()),
fault_rate(1, 40, secret_key())}, z_fault_rate(1, 40, secret_key())},
case Len >= 0 andalso nonce_valid(Nonce) andalso secret_key_valid(Key) of case Len >= 0 andalso nonce_valid(Nonce) andalso secret_key_valid(Key) of
true -> true ->
CipherStream = enacl:stream(Len, Nonce, Key), CipherStream = enacl:stream(Len, Nonce, Key),
@ -541,29 +545,29 @@ xor_bytes(<<A, As/binary>>, <<B, Bs/binary>>) ->
[A bxor B | xor_bytes(As, Bs)]; [A bxor B | xor_bytes(As, Bs)];
xor_bytes(<<>>, <<>>) -> []. xor_bytes(<<>>, <<>>) -> [].
prop_stream_xor_correct() -> %% prop_stream_xor_correct() ->
?FORALL({Msg, Nonce, Key}, %% ?FORALL({Msg, Nonce, Key},
{fault_rate(1, 40, g_iodata()), %% {z_fault_rate(1, 40, g_iodata()),
fault_rate(1, 40, nonce()), %% z_fault_rate(1, 40, nonce()),
fault_rate(1, 40, secret_key())}, %% z_fault_rate(1, 40, secret_key())},
case v_iodata(Msg) andalso nonce_valid(Nonce) andalso secret_key_valid(Key) of %% case v_iodata(Msg) andalso nonce_valid(Nonce) andalso secret_key_valid(Key) of
true -> %% true ->
Stream = enacl:stream(iolist_size(Msg), Nonce, Key), %% Stream = enacl:stream(iolist_size(Msg), Nonce, Key),
CipherText = enacl:stream_xor(Msg, Nonce, Key), %% CipherText = enacl:stream_xor(Msg, Nonce, Key),
StreamXor = enacl:stream_xor(CipherText, Nonce, Key), %% StreamXor = enacl:stream_xor(CipherText, Nonce, Key),
conjunction([ %% conjunction([
{'xor', equals(iolist_to_binary(Msg), StreamXor)}, %% {'xor', equals(iolist_to_binary(Msg), StreamXor)},
{stream, equals(iolist_to_binary(xor_bytes(Stream, iolist_to_binary(Msg))), CipherText)} %% {stream, equals(iolist_to_binary(xor_bytes(Stream, iolist_to_binary(Msg))), CipherText)}
]); %% ]);
false -> %% false ->
badargs(fun() -> enacl:stream_xor(Msg, Nonce, Key) end) %% badargs(fun() -> enacl:stream_xor(Msg, Nonce, Key) end)
end). %% end).
%% CRYPTO AUTH %% CRYPTO AUTH
prop_auth_correct() -> prop_auth_correct() ->
?FORALL({Msg, Key}, ?FORALL({Msg, Key},
{fault_rate(1, 40, g_iodata()), {z_fault_rate(1, 40, g_iodata()),
fault_rate(1, 40, secret_key())}, z_fault_rate(1, 40, secret_key())},
case v_iodata(Msg) andalso secret_key_valid(Key) of case v_iodata(Msg) andalso secret_key_valid(Key) of
true -> true ->
Authenticator = enacl:auth(Msg, Key), Authenticator = enacl:auth(Msg, Key),
@ -588,7 +592,7 @@ authenticator_good(_Msg, _Key) ->
binary(enacl:auth_size()). binary(enacl:auth_size()).
authenticator(Msg, Key) -> authenticator(Msg, Key) ->
fault(authenticator_bad(), authenticator_good(Msg, Key)). z_fault(authenticator_bad(), authenticator_good(Msg, Key)).
authenticator_valid({valid, _}) -> true; authenticator_valid({valid, _}) -> true;
authenticator_valid({invalid, _}) -> true; authenticator_valid({invalid, _}) -> true;
@ -596,8 +600,8 @@ authenticator_valid(_) -> false.
prop_auth_verify_correct() -> prop_auth_verify_correct() ->
?FORALL({Msg, Key}, ?FORALL({Msg, Key},
{fault_rate(1, 40, g_iodata()), {z_fault_rate(1, 40, g_iodata()),
fault_rate(1, 40, secret_key())}, z_fault_rate(1, 40, secret_key())},
?FORALL(Authenticator, authenticator(Msg, Key), ?FORALL(Authenticator, authenticator(Msg, Key),
case v_iodata(Msg) andalso secret_key_valid(Key) andalso authenticator_valid(Authenticator) of case v_iodata(Msg) andalso secret_key_valid(Key) andalso authenticator_valid(Authenticator) of
true -> true ->
@ -614,8 +618,8 @@ prop_auth_verify_correct() ->
%% CRYPTO ONETIME AUTH %% CRYPTO ONETIME AUTH
prop_onetimeauth_correct() -> prop_onetimeauth_correct() ->
?FORALL({Msg, Key}, ?FORALL({Msg, Key},
{fault_rate(1, 40, g_iodata()), {z_fault_rate(1, 40, g_iodata()),
fault_rate(1, 40, secret_key())}, z_fault_rate(1, 40, secret_key())},
case v_iodata(Msg) andalso secret_key_valid(Key) of case v_iodata(Msg) andalso secret_key_valid(Key) of
true -> true ->
Authenticator = enacl:onetime_auth(Msg, Key), Authenticator = enacl:onetime_auth(Msg, Key),
@ -640,7 +644,7 @@ ot_authenticator_good(_Msg, _Key) ->
binary(enacl:auth_size()). binary(enacl:auth_size()).
ot_authenticator(Msg, Key) -> ot_authenticator(Msg, Key) ->
fault(ot_authenticator_bad(), ot_authenticator_good(Msg, Key)). z_fault(ot_authenticator_bad(), ot_authenticator_good(Msg, Key)).
ot_authenticator_valid({valid, _}) -> true; ot_authenticator_valid({valid, _}) -> true;
ot_authenticator_valid({invalid, _}) -> true; ot_authenticator_valid({invalid, _}) -> true;
@ -648,8 +652,8 @@ ot_authenticator_valid(_) -> false.
prop_onetime_auth_verify_correct() -> prop_onetime_auth_verify_correct() ->
?FORALL({Msg, Key}, ?FORALL({Msg, Key},
{fault_rate(1, 40, g_iodata()), {z_fault_rate(1, 40, g_iodata()),
fault_rate(1, 40, secret_key())}, z_fault_rate(1, 40, secret_key())},
?FORALL(Authenticator, ot_authenticator(Msg, Key), ?FORALL(Authenticator, ot_authenticator(Msg, Key),
case v_iodata(Msg) andalso secret_key_valid(Key) andalso ot_authenticator_valid(Authenticator) of case v_iodata(Msg) andalso secret_key_valid(Key) andalso ot_authenticator_valid(Authenticator) of
true -> true ->
@ -706,7 +710,7 @@ verify_pair_good(Sz) ->
?SUCHTHAT({X, Y}, {binary(Sz), binary(Sz)}, X /= Y)]). ?SUCHTHAT({X, Y}, {binary(Sz), binary(Sz)}, X /= Y)]).
verify_pair(Sz) -> verify_pair(Sz) ->
fault(verify_pair_bad(Sz), verify_pair_good(Sz)). z_fault(verify_pair_bad(Sz), verify_pair_good(Sz)).
verify_pair_valid(Sz, X, Y) -> verify_pair_valid(Sz, X, Y) ->
byte_size(X) == Sz andalso byte_size(Y) == Sz. byte_size(X) == Sz andalso byte_size(Y) == Sz.