let poly1305_padded_st (w:field_spec) =
    ctx:Poly.poly1305_ctx w
  -> len:size_t
  -> text:lbuffer uint8 len ->
  Stack unit
  (requires fun h ->
    live h ctx /\ live h text /\ disjoint ctx text /\
    Poly.state_inv_t h ctx)
  (ensures fun h0 _ h1 ->
    modifies (loc ctx) h0 h1 /\
    Poly.state_inv_t h1 ctx /\
    Poly.as_get_r h0 ctx == Poly.as_get_r h1 ctx /\
    Poly.as_get_acc h1 ctx ==
      Spec.poly1305_padded (Poly.as_get_r h0 ctx) (as_seq h0 text) (Poly.as_get_acc h0 ctx))
let poly1305_padded_st (w: field_spec) =
ctx: Poly.poly1305_ctx w -> len: size_t -> text: lbuffer uint8 len
  -> Stack unit
      (requires fun h -> live h ctx /\ live h text /\ disjoint ctx text /\ Poly.state_inv_t h ctx)
      (ensures
        fun h0 _ h1 ->
          modifies (loc ctx) h0 h1 /\ Poly.state_inv_t h1 ctx /\
          Poly.as_get_r h0 ctx == Poly.as_get_r h1 ctx /\
          Poly.as_get_acc h1 ctx ==
          Spec.poly1305_padded (Poly.as_get_r h0 ctx) (as_seq h0 text) (Poly.as_get_acc h0 ctx))
Hacl.Impl.Chacha20Poly1305.PolyCore.fst.checked
Spec.Chacha20Poly1305.fst.checked prims.fst.checked Meta.Attribute.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Impl.Poly1305.Fields.fst.checked Hacl.Impl.Poly1305.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.Chacha20Poly1305.PolyCore.fst
Hacl.Impl.Poly1305.Fields.field_spec Hacl.Impl.Poly1305.poly1305_ctx Lib.IntTypes.size_t Lib.Buffer.lbuffer Lib.IntTypes.uint8 Prims.unit FStar.Monotonic.HyperStack.mem Prims.l_and Lib.Buffer.live Lib.Buffer.MUT Hacl.Impl.Poly1305.Fields.limb Lib.Buffer.disjoint Hacl.Impl.Poly1305.state_inv_t Lib.Buffer.modifies Lib.Buffer.loc Prims.eq2 Spec.Poly1305.felem Hacl.Impl.Poly1305.as_get_r Hacl.Impl.Poly1305.as_get_acc Spec.Chacha20Poly1305.poly1305_padded Lib.Buffer.as_seq
module Hacl.Impl.Chacha20Poly1305.PolyCore

open FStar.HyperStack
open FStar.HyperStack.All
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer

open Hacl.Impl.Poly1305.Fields

module ST = FStar.HyperStack.ST
module Spec = Spec.Chacha20Poly1305
module Poly = Hacl.Impl.Poly1305


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

inline_for_extraction noextract
val poly1305_padded_st : w: Hacl.Impl.Poly1305.Fields.field_spec -> Type0
w: Hacl.Impl.Poly1305.Fields.field_spec -> Type0