let poly1305_padded_128 = Hacl.Impl.Chacha20Poly1305.PolyCore.poly1305_padded #M128
let poly1305_padded_128 =
Hacl.Impl.Chacha20Poly1305.PolyCore.poly1305_padded #M128
Hacl.Chacha20Poly1305_128.fst.checked
prims.fst.checked Hacl.Poly1305_128.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.Vec128.fst.checked FStar.Pervasives.fsti.checked
Hacl.Chacha20Poly1305_128.fst
Hacl.Impl.Chacha20Poly1305.PolyCore.poly1305_padded Hacl.Impl.Poly1305.Fields.M128
module Hacl.Chacha20Poly1305_128


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

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

[@CInline]
val poly1305_padded_128 : Hacl.Impl.Chacha20Poly1305.PolyCore.poly1305_padded_st Hacl.Impl.Poly1305.Fields.M128
Hacl.Impl.Chacha20Poly1305.PolyCore.poly1305_padded_st Hacl.Impl.Poly1305.Fields.M128