val poly1305_update: poly1305_update_st M32
let poly1305_update = poly1305_update #M32
val poly1305_update: poly1305_update_st M32
let poly1305_update =
poly1305_update #M32
Hacl.Poly1305_32.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_32.fst
Hacl.Impl.Poly1305.poly1305_update Hacl.Impl.Poly1305.Fields.M32
module Hacl.Poly1305_32

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

let poly1305_init = poly1305_init #M32

let poly1305_update1 = poly1305_update1 #M32
val poly1305_update: poly1305_update_st M32
Hacl.Impl.Poly1305.poly1305_update_st Hacl.Impl.Poly1305.Fields.M32