let poly1305_do_32 = chacha20poly1305_poly1305_do_higher #M32 True poly1305_finish poly1305_init poly1305_padded_32
let poly1305_do_32 =
chacha20poly1305_poly1305_do_higher #M32 True poly1305_finish poly1305_init poly1305_padded_32
Hacl.Chacha20Poly1305_32.fst.checked
prims.fst.checked Hacl.Poly1305_32.fsti.checked Hacl.Meta.Chacha20Poly1305.fst.checked Hacl.Impl.Poly1305.Fields.fst.checked Hacl.Impl.Chacha20Poly1305.PolyCore.fst.checked Hacl.Impl.Chacha20Poly1305.fst.checked Hacl.Chacha20.fst.checked FStar.Pervasives.fsti.checked
Hacl.Chacha20Poly1305_32.fst
Hacl.Meta.Chacha20Poly1305.chacha20poly1305_poly1305_do_higher Hacl.Impl.Poly1305.Fields.M32 Prims.l_True Hacl.Poly1305_32.poly1305_finish Hacl.Poly1305_32.poly1305_init Hacl.Chacha20Poly1305_32.poly1305_padded_32
module Hacl.Chacha20Poly1305_32

open Hacl.Meta.Chacha20Poly1305
open Hacl.Impl.Chacha20Poly1305
open Hacl.Impl.Poly1305.Fields
open Hacl.Poly1305_32

#set-options "--z3rlimit 50 --max_fuel 0 --max_ifuel 0"

[@CInline]
private
let poly1305_padded_32 = Hacl.Impl.Chacha20Poly1305.PolyCore.poly1305_padded #M32

[@CInline]
val poly1305_do_32 : Hacl.Meta.Chacha20Poly1305.chacha20poly1305_poly1305_do_higher_t Prims.l_True
Hacl.Meta.Chacha20Poly1305.chacha20poly1305_poly1305_do_higher_t Prims.l_True