import "Ascon.cry";

for [0,1,2,16,63,64,65,127,128,129,255,256] (\a ->
for [0,1,2,16,63,64,65,127,128,129,255,256] (\p -> do {
    print ("decrypt_encrypt",a,p);
    prove_print (unint_yices ["Ascon::Ascon_p"]) {{
        \K N (A : [0]) (P : [128]) ->
        (T == T'
        where
        (C, T) = AEAD128_encrypt K N A P
        (P', T') = AEAD128_decrypt_raw K N A C)
    }};
}));