let poly1305_padded_32 = Hacl.Impl.Chacha20Poly1305.PolyCore.poly1305_padded #M32
let poly1305_padded_32 =
Hacl.Impl.Chacha20Poly1305.PolyCore.poly1305_padded #M32
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.Impl.Chacha20Poly1305.PolyCore.poly1305_padded Hacl.Impl.Poly1305.Fields.M32
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]
val poly1305_padded_32 : Hacl.Impl.Chacha20Poly1305.PolyCore.poly1305_padded_st Hacl.Impl.Poly1305.Fields.M32
Hacl.Impl.Chacha20Poly1305.PolyCore.poly1305_padded_st Hacl.Impl.Poly1305.Fields.M32