let update = F.update (poly1305 M32) (G.hide ()) (t M32) (poly1305_key.I.s ())
let update =
F.update (poly1305 M32) (G.hide ()) (t M32) (poly1305_key.I.s ())
Hacl.Streaming.Poly1305_32.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_32.fst
Hacl.Streaming.Functor.update Prims.unit Hacl.Streaming.Poly1305.poly1305 Hacl.Impl.Poly1305.Fields.M32 FStar.Ghost.hide Hacl.Streaming.Poly1305.t Hacl.Streaming.Interface.__proj__Stateful__item__s Hacl.Streaming.Poly1305.poly1305_key
module Hacl.Streaming.Poly1305_32

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_32_state = F.state_s (poly1305 M32) () (t M32) (poly1305_key.I.s ())

noextract
let alloca = F.alloca (poly1305 M32) () (t M32) (poly1305_key.I.s ())
let create_in = F.create_in (poly1305 M32) () (t M32) (poly1305_key.I.s ())
let init = F.init (poly1305 M32) (G.hide ()) (t M32) (poly1305_key.I.s ())
val update : Hacl.Streaming.Functor.update_st (Hacl.Streaming.Poly1305.poly1305 Hacl.Impl.Poly1305.Fields.M32)
  (FStar.Ghost.reveal (FStar.Ghost.hide ()))
  (Hacl.Streaming.Poly1305.t Hacl.Impl.Poly1305.Fields.M32)
  (Stateful?.s Hacl.Streaming.Poly1305.poly1305_key ())
Hacl.Streaming.Functor.update_st (Hacl.Streaming.Poly1305.poly1305 Hacl.Impl.Poly1305.Fields.M32)
  (FStar.Ghost.reveal (FStar.Ghost.hide ()))
  (Hacl.Streaming.Poly1305.t Hacl.Impl.Poly1305.Fields.M32)
  (Stateful?.s Hacl.Streaming.Poly1305.poly1305_key ())