val get_precomp_r (#s: _) (ctx: poly1305_ctx s)
    : Stack (precomp_r s)
      (requires fun h -> live h ctx)
      (ensures fun h0 pre h1 -> h0 == h1 /\ live h1 pre /\ pre == gsub ctx (nlimb s) (precomplen s))
let get_precomp_r #s (ctx:poly1305_ctx s) : Stack (precomp_r s)
  (requires fun h -> live h ctx)
  (ensures  fun h0 pre h1 -> h0 == h1 /\ live h1 pre /\ pre == gsub ctx (nlimb s) (precomplen s))
  = sub ctx (nlimb s) (precomplen s)
val get_precomp_r (#s: _) (ctx: poly1305_ctx s)
    : Stack (precomp_r s)
      (requires fun h -> live h ctx)
      (ensures fun h0 pre h1 -> h0 == h1 /\ live h1 pre /\ pre == gsub ctx (nlimb s) (precomplen s))
let get_precomp_r #s (ctx: poly1305_ctx s)
    : Stack (precomp_r s)
      (requires fun h -> live h ctx)
      (ensures fun h0 pre h1 -> h0 == h1 /\ live h1 pre /\ pre == gsub ctx (nlimb s) (precomplen s)) =
sub ctx (nlimb s) (precomplen s)
Hacl.Impl.Poly1305.fst.checked
Spec.Poly1305.fst.checked prims.fst.checked Meta.Attribute.fst.checked Lib.Sequence.fsti.checked Lib.Loops.fsti.checked Lib.LoopCombinators.fst.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Poly1305.Vec.fst.checked Hacl.Spec.Poly1305.Field32xN.Lemmas.fst.checked Hacl.Spec.Poly1305.Equiv.fst.checked Hacl.Impl.Poly1305.Lemmas.fst.checked Hacl.Impl.Poly1305.Fields.fst.checked Hacl.Impl.Poly1305.Field32xN.fst.checked Hacl.Impl.Poly1305.Bignum128.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.Poly1305.fst
Hacl.Impl.Poly1305.Fields.field_spec Hacl.Impl.Poly1305.poly1305_ctx Lib.Buffer.sub Lib.Buffer.MUT Hacl.Impl.Poly1305.Fields.limb Lib.IntTypes.op_Plus_Bang Lib.IntTypes.U32 Lib.IntTypes.PUB Hacl.Impl.Poly1305.Fields.nlimb Hacl.Impl.Poly1305.Fields.precomplen Lib.Buffer.lbuffer_t Hacl.Impl.Poly1305.Fields.precomp_r FStar.Monotonic.HyperStack.mem Lib.Buffer.live Prims.l_and Prims.eq2 Lib.Buffer.gsub
module Hacl.Impl.Poly1305

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

open Lib.IntTypes
open Lib.Buffer
open Lib.ByteBuffer

open Hacl.Impl.Poly1305.Fields
open Hacl.Impl.Poly1305.Bignum128

module ST = FStar.HyperStack.ST
module BSeq = Lib.ByteSequence
module LSeq = Lib.Sequence

module S = Spec.Poly1305
module Vec = Hacl.Spec.Poly1305.Vec
module Equiv = Hacl.Spec.Poly1305.Equiv
module F32xN = Hacl.Impl.Poly1305.Field32xN

friend Lib.LoopCombinators


let _: squash (inversion field_spec) = allow_inversion field_spec


#reset-options "--z3rlimit 50 --max_fuel 0 --max_ifuel 0 --using_facts_from '* -FStar.Seq' --record_options"

inline_for_extraction noextract
let get_acc #s (ctx:poly1305_ctx s) : Stack (felem s)
  (requires fun h -> live h ctx)
  (ensures  fun h0 acc h1 -> h0 == h1 /\ live h1 acc /\ acc == gsub ctx 0ul (nlimb s))
  = sub ctx 0ul (nlimb s)


inline_for_extraction noextract
let get_precomp_r #s (ctx:poly1305_ctx s) : Stack (precomp_r s)
  (requires fun h -> live h ctx)
val get_precomp_r (#s: _) (ctx: poly1305_ctx s)
    : Stack (precomp_r s)
      (requires fun h -> live h ctx)
      (ensures fun h0 pre h1 -> h0 == h1 /\ live h1 pre /\ pre == gsub ctx (nlimb s) (precomplen s))
ctx: Hacl.Impl.Poly1305.poly1305_ctx s
  -> FStar.HyperStack.ST.Stack (Hacl.Impl.Poly1305.Fields.precomp_r s)