@@ -83,8 +83,8 @@ v_binary(_, _) -> false.
83
83
84
84
85
85
% % Typical generators based on the binaries
86
- nonce () -> g_binary (enacl :box_nonce_size ()).
87
- nonce_valid (N ) -> v_binary (enacl :box_nonce_size (), N ).
86
+ nonce () -> g_binary (enacl :box_NONCEBYTES ()).
87
+ nonce_valid (N ) -> v_binary (enacl :box_NONCEBYTES (), N ).
88
88
89
89
% % Generator of natural numbers
90
90
g_nat () ->
@@ -111,10 +111,10 @@ keypair_bad() ->
111
111
#{ public := PK , secret := SK } = enacl :box_keypair (),
112
112
case X of
113
113
pk ->
114
- PKBytes = enacl :box_public_key_bytes (),
114
+ PKBytes = enacl :box_PUBLICKEYBYTES (),
115
115
{oneof ([return (a ), nat (), ? SUCHTHAT (B , binary (), byte_size (B ) /= PKBytes )]), SK };
116
116
sk ->
117
- SKBytes = enacl :box_secret_key_bytes (),
117
+ SKBytes = enacl :box_SECRETKEYBYTES (),
118
118
{PK , oneof ([return (a ), nat (), ? SUCHTHAT (B , binary (), byte_size (B ) /= SKBytes )])}
119
119
end
120
120
end ).
@@ -159,8 +159,8 @@ g_generichash_size() ->
159
159
% % * box_afternm/3
160
160
% % * box_open_afternm/3
161
161
keypair_valid (PK , SK ) when is_binary (PK ), is_binary (SK ) ->
162
- PKBytes = enacl :box_public_key_bytes (),
163
- SKBytes = enacl :box_secret_key_bytes (),
162
+ PKBytes = enacl :box_PUBLICKEYBYTES (),
163
+ SKBytes = enacl :box_SECRETKEYBYTES (),
164
164
byte_size (PK ) == PKBytes andalso byte_size (SK ) == SKBytes ;
165
165
keypair_valid (_PK , _SK ) -> false .
166
166
@@ -264,11 +264,11 @@ beforenm_key() ->
264
264
oneof ([
265
265
elements ([a ,b ,c ]),
266
266
real (),
267
- ? SUCHTHAT (X , binary (), byte_size (X ) /= enacl :box_beforenm_bytes ())
267
+ ? SUCHTHAT (X , binary (), byte_size (X ) /= enacl :box_BEFORENMBYTES ())
268
268
])
269
269
end ).
270
270
271
- v_key (K ) when is_binary (K ) -> byte_size (K ) == enacl :box_beforenm_bytes ();
271
+ v_key (K ) when is_binary (K ) -> byte_size (K ) == enacl :box_BEFORENMBYTES ();
272
272
v_key (_ ) -> false .
273
273
274
274
prop_beforenm_correct () ->
@@ -324,11 +324,11 @@ sign_keypair_bad() ->
324
324
KP = enacl :sign_keypair (),
325
325
case X of
326
326
pk ->
327
- Sz = enacl :sign_keypair_public_size (),
327
+ Sz = enacl :sign_PUBLICBYTES (),
328
328
? LET (Wrong , oneof ([a , int (), ? SUCHTHAT (B , binary (), byte_size (B ) /= Sz )]),
329
329
KP #{ public := Wrong });
330
330
sk ->
331
- Sz = enacl :sign_keypair_secret_size (),
331
+ Sz = enacl :sign_SECRETBYTES (),
332
332
? LET (Wrong , oneof ([a , int (), ? SUCHTHAT (B , binary (), byte_size (B ) /= Sz )]),
333
333
KP #{ secret := Wrong })
334
334
end
@@ -342,12 +342,12 @@ sign_keypair() ->
342
342
343
343
sign_keypair_public_valid (#{ public := Public })
344
344
when is_binary (Public ) ->
345
- byte_size (Public ) == enacl :sign_keypair_public_size ();
345
+ byte_size (Public ) == enacl :sign_PUBLICBYTES ();
346
346
sign_keypair_public_valid (_ ) -> false .
347
347
348
348
sign_keypair_secret_valid (#{ secret := Secret })
349
349
when is_binary (Secret ) ->
350
- byte_size (Secret ) == enacl :sign_keypair_secret_size ();
350
+ byte_size (Secret ) == enacl :sign_SECRETBYTES ();
351
351
sign_keypair_secret_valid (_ ) -> false .
352
352
353
353
sign_keypair_valid (KP ) ->
@@ -408,11 +408,11 @@ signed_message_good_d(M) ->
408
408
end )}]).
409
409
410
410
signed_message_bad () ->
411
- Sz = enacl :sign_keypair_public_size (),
411
+ Sz = enacl :sign_PUBLICBYTES (),
412
412
{binary (), oneof ([a , int (), ? SUCHTHAT (B , binary (Sz ), byte_size (B ) /= Sz )])}.
413
413
414
414
signed_message_bad_d () ->
415
- Sz = enacl :sign_keypair_public_size (),
415
+ Sz = enacl :sign_PUBLICBYTES (),
416
416
{binary (), oneof ([a , int (), ? SUCHTHAT (B , binary (Sz ), byte_size (B ) /= Sz )])}.
417
417
418
418
signed_message (M ) ->
@@ -496,19 +496,19 @@ prop_seal_box_correct() ->
496
496
% % * secretbox/3
497
497
% % * secretbo_open/3
498
498
secret_key_good () ->
499
- Sz = enacl :secretbox_key_size (),
499
+ Sz = enacl :secretbox_KEYBYTES (),
500
500
binary (Sz ).
501
501
502
502
secret_key_bad () ->
503
503
oneof ([return (a ),
504
504
nat (),
505
- ? SUCHTHAT (B , binary (), byte_size (B ) /= enacl :secretbox_key_size ())]).
505
+ ? SUCHTHAT (B , binary (), byte_size (B ) /= enacl :secretbox_KEYBYTES ())]).
506
506
507
507
secret_key () ->
508
508
? FAULT (secret_key_bad (), secret_key_good ()).
509
509
510
510
secret_key_valid (SK ) when is_binary (SK ) ->
511
- Sz = enacl :secretbox_key_size (),
511
+ Sz = enacl :secretbox_KEYBYTES (),
512
512
byte_size (SK ) == Sz ;
513
513
secret_key_valid (_SK ) -> false .
514
514
@@ -618,6 +618,27 @@ xor_bytes(<<A, As/binary>>, <<B, Bs/binary>>) ->
618
618
[A bxor B | xor_bytes (As , Bs )];
619
619
xor_bytes (<<>>, <<>>) -> [].
620
620
621
+ positive () ->
622
+ ? LET (N , nat (), N + 1 ).
623
+
624
+ chacha20_nonce () ->
625
+ Sz = enacl :stream_chacha20_NONCEBYTES (),
626
+ binary (Sz ).
627
+
628
+ chacha20_key () ->
629
+ Sz = enacl :stream_chacha20_KEYBYTES (),
630
+ binary (Sz ).
631
+
632
+ prop_stream_chacha20_correct () ->
633
+ ? FORALL (Len , positive (),
634
+ ? FORALL ({Msg , Nonce , Key }, {binary (Len ), chacha20_nonce (), chacha20_key ()},
635
+ begin
636
+ CT = enacl :stream_chacha20_xor (Msg , Nonce , Key ),
637
+ Stream = enacl :stream_chacha20 (Len , Nonce , Key ),
638
+ CT2 = list_to_binary (xor_bytes (Stream , Msg )),
639
+ equals (CT , CT2 )
640
+ end )).
641
+
621
642
% % CRYPTO AUTH
622
643
% % ------------------------------------------------------------
623
644
% % * auth/2
@@ -635,19 +656,19 @@ prop_auth_correct() ->
635
656
end ).
636
657
637
658
authenticator_bad () ->
638
- oneof ([a , int (), ? SUCHTHAT (X , binary (), byte_size (X ) /= enacl :auth_size ())]).
659
+ oneof ([a , int (), ? SUCHTHAT (X , binary (), byte_size (X ) /= enacl :auth_BYTES ())]).
639
660
640
661
authenticator_good (Msg , Key ) when is_binary (Key ) ->
641
- Sz = enacl :secretbox_key_size (),
662
+ Sz = enacl :secretbox_KEYBYTES (),
642
663
case v_iodata (Msg ) andalso byte_size (Key ) == Sz of
643
664
true ->
644
- frequency ([{1 , ? LAZY ({invalid , binary (enacl :auth_size ())})},
665
+ frequency ([{1 , ? LAZY ({invalid , binary (enacl :auth_BYTES ())})},
645
666
{3 , return ({valid , enacl :auth (Msg , Key )})}]);
646
667
false ->
647
- binary (enacl :auth_size ())
668
+ binary (enacl :auth_BYTES ())
648
669
end ;
649
670
authenticator_good (_Msg , _Key ) ->
650
- binary (enacl :auth_size ()).
671
+ binary (enacl :auth_BYTES ()).
651
672
652
673
authenticator (Msg , Key ) ->
653
674
? FAULT (authenticator_bad (), authenticator_good (Msg , Key )).
@@ -690,19 +711,19 @@ prop_onetimeauth_correct() ->
690
711
end ).
691
712
692
713
ot_authenticator_bad () ->
693
- oneof ([a , int (), ? SUCHTHAT (X , binary (), byte_size (X ) /= enacl :onetime_auth_size ())]).
714
+ oneof ([a , int (), ? SUCHTHAT (X , binary (), byte_size (X ) /= enacl :onetime_auth_BYTES ())]).
694
715
695
716
ot_authenticator_good (Msg , Key ) when is_binary (Key ) ->
696
- Sz = enacl :secretbox_key_size (),
717
+ Sz = enacl :secretbox_KEYBYTES (),
697
718
case v_iodata (Msg ) andalso byte_size (Key ) == Sz of
698
719
true ->
699
- frequency ([{1 , ? LAZY ({invalid , binary (enacl :onetime_auth_size ())})},
720
+ frequency ([{1 , ? LAZY ({invalid , binary (enacl :onetime_auth_BYTES ())})},
700
721
{3 , return ({valid , enacl :onetime_auth (Msg , Key )})}]);
701
722
false ->
702
- binary (enacl :onetime_auth_size ())
723
+ binary (enacl :onetime_auth_BYTES ())
703
724
end ;
704
725
ot_authenticator_good (_Msg , _Key ) ->
705
- binary (enacl :auth_size ()).
726
+ binary (enacl :auth_BYTES ()).
706
727
707
728
ot_authenticator (Msg , Key ) ->
708
729
? FAULT (ot_authenticator_bad (), ot_authenticator_good (Msg , Key )).
0 commit comments