let alloca = F.alloca (poly1305 M256) () (t M256) (poly1305_key.I.s ())
let alloca =
F.alloca (poly1305 M256) () (t M256) (poly1305_key.I.s ())
Hacl.Streaming.Poly1305_256.fst.checked
prims.fst.checked Hacl.Streaming.Poly1305.fst.checked Hacl.Streaming.Interface.fsti.checked Hacl.Streaming.Functor.fsti.checked Hacl.Impl.Poly1305.Fields.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Hacl.Streaming.Poly1305_256.fst
Hacl.Streaming.Functor.alloca Prims.unit Hacl.Streaming.Poly1305.poly1305 Hacl.Impl.Poly1305.Fields.M256 Hacl.Streaming.Poly1305.t Hacl.Streaming.Interface.__proj__Stateful__item__s Hacl.Streaming.Poly1305.poly1305_key
module Hacl.Streaming.Poly1305_256

module G = FStar.Ghost
module F = Hacl.Streaming.Functor
module I = Hacl.Streaming.Interface

open Hacl.Impl.Poly1305.Fields
open Hacl.Streaming.Poly1305

#set-options "--fuel 0 --ifuel 0 --z3rlimit 100"

/// Type abbreviation - makes KaRaMeL use pretty names in the generated code
let poly1305_256_state = F.state_s (poly1305 M256) () (t M256) (poly1305_key.I.s ())
val alloca : Hacl.Streaming.Functor.alloca_st (Hacl.Streaming.Poly1305.poly1305 Hacl.Impl.Poly1305.Fields.M256)
  ()
  (Hacl.Streaming.Poly1305.t Hacl.Impl.Poly1305.Fields.M256)
  (Stateful?.s Hacl.Streaming.Poly1305.poly1305_key ())
Hacl.Streaming.Functor.alloca_st (Hacl.Streaming.Poly1305.poly1305 Hacl.Impl.Poly1305.Fields.M256)
  ()
  (Hacl.Streaming.Poly1305.t Hacl.Impl.Poly1305.Fields.M256)
  (Stateful?.s Hacl.Streaming.Poly1305.poly1305_key ())