:- module(types, [
    is_xchacha20_key/1, is_xchacha20_nonce/1, is_xchacha20_counter/1,
    is_chacha20_key/1, is_chacha20_nonce/1, is_chacha20_counter/1,
    is_hchacha20_hash/1,
    is_chacha20_block/1,
    is_poly1305_key/1, is_poly1305_tag/1,
    is_u8s/1, is_u32s/1,
    is_u8/1, is_u32/1,
    trunc_8/2, trunc_32/2,
    zeros/2,
    u8s_to_u32s_le/2,
    print_hexlist/1
]).

is_xchacha_poly1305_key(K) :- is_xchacha20_key(K).
is_xchacha_poly1305_iv(K) :- is_xchacha20_key(K).

is_xchacha20_key(K) :- is_chacha20_key(K).
is_xchacha20_nonce(N) :- is_u8s(N), length(N, 24).
is_xchacha20_counter(C) :- is_chacha20_counter(C).

is_chacha20_key(K) :- is_u8s(K), length(K, 32).
is_chacha20_nonce(N) :- is_u8s(N), length(N, 8).
is_chacha20_counter(C) :- ground(C), Top is 1<<64, 0 =< C, C < Top.

is_hchacha20_hash(H) :- is_u8s(H), length(H, 32).
is_chacha20_block(B) :- is_u32s(B), length(B, 16).

is_poly1305_key(K) :- is_u8s(K), length(K, 32).
is_poly1305_tag(T) :- is_u8s(T), length(T, 16).

is_u8s(Xs) :- ground(Xs), is_list(Xs), forall(member(X, Xs), is_u8(X)).
is_u32s(Xs) :- ground(Xs), is_list(Xs), forall(member(X, Xs), is_u32(X)).

is_u8(X) :- trunc_8(X, X).
is_u32(X) :- trunc_32(X, X).

trunc_8(A, X) :- A >= 0, X is A /\ 0xFF.
trunc_32(A, X) :- A >= 0, X is A /\ 0xFFFFFFFF.

zeros(N, Lst) :- length(Lst, N), maplist(=(0), Lst).

u8s_to_u32s_le([], []).
u8s_to_u32s_le([A, B, C, D|U8s], [ABCD|U32s]) :- 
    as_int_le(4, [A, B, C, D], ABCD), 
    u8s_to_u32s_le(U8s, U32s).


print_hexlist(Xs) :- forall(member(X, Xs), format("~16r ", X)).