val as_get_acc: #s:field_spec -> h:mem -> ctx:poly1305_ctx s -> GTot S.felem
let as_get_acc #s h ctx = (feval h (gsub ctx 0ul (nlimb s))).[0]
val as_get_acc: #s:field_spec -> h:mem -> ctx:poly1305_ctx s -> GTot S.felem
let as_get_acc #s h ctx =
(feval h (gsub ctx 0ul (nlimb s))).[ 0 ]
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 FStar.Monotonic.HyperStack.mem Hacl.Impl.Poly1305.poly1305_ctx Hacl.Impl.Poly1305.op_String_Access Spec.Poly1305.felem Hacl.Impl.Poly1305.Fields.width Hacl.Impl.Poly1305.Fields.feval Lib.Buffer.gsub 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 FStar.UInt32.__uint_to_t
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)
  (ensures  fun h0 pre h1 -> h0 == h1 /\ live h1 pre /\ pre == gsub ctx (nlimb s) (precomplen s))
  = sub ctx (nlimb s) (precomplen s)


unfold
let op_String_Access #a #len = LSeq.index #a #len
val as_get_acc: #s:field_spec -> h:mem -> ctx:poly1305_ctx s -> GTot S.felem
h: FStar.Monotonic.HyperStack.mem -> ctx: Hacl.Impl.Poly1305.poly1305_ctx s
  -> Prims.GTot Spec.Poly1305.felem