val poly1305_init: poly1305_init_st M128
let poly1305_init = poly1305_init #M128
val poly1305_init: poly1305_init_st M128
let poly1305_init =
poly1305_init #M128
Hacl.Poly1305_128.fst.checked
prims.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Meta.Poly1305.fst.checked Hacl.Meta.Poly1305.fst.checked Hacl.Impl.Poly1305.Fields.fst.checked Hacl.Impl.Poly1305.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Poly1305_128.fst
Hacl.Impl.Poly1305.poly1305_init Hacl.Impl.Poly1305.Fields.M128
module Hacl.Poly1305_128

open FStar.HyperStack
open FStar.HyperStack.All

open Lib.IntTypes
open Lib.Buffer

open Hacl.Impl.Poly1305.Fields
open Hacl.Impl.Poly1305
open Hacl.Meta.Poly1305

friend Hacl.Meta.Poly1305
val poly1305_init: poly1305_init_st M128
Hacl.Impl.Poly1305.poly1305_init_st Hacl.Impl.Poly1305.Fields.M128