val felem_fits: #w:lanes -> h:mem -> f:felem w -> m:scale32_5 -> Type0
let felem_fits #w h f m =
  felem_fits5 (as_tup5 h f) m
val felem_fits: #w:lanes -> h:mem -> f:felem w -> m:scale32_5 -> Type0
let felem_fits #w h f m =
felem_fits5 (as_tup5 h f) m
Hacl.Impl.Poly1305.Field32xN.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.IntVector.fsti.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.Field32xN.fst.checked Hacl.Impl.Poly1305.Lemmas.fst.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.Field32xN.fst
Hacl.Spec.Poly1305.Field32xN.lanes FStar.Monotonic.HyperStack.mem Hacl.Impl.Poly1305.Field32xN.felem Hacl.Spec.Poly1305.Field32xN.scale32_5 Hacl.Spec.Poly1305.Field32xN.felem_fits5 Hacl.Impl.Poly1305.Field32xN.as_tup5
module Hacl.Impl.Poly1305.Field32xN

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

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

include Hacl.Spec.Poly1305.Field32xN
open Hacl.Spec.Poly1305.Field32xN.Lemmas
open Hacl.Impl.Poly1305.Lemmas

module Vec = Hacl.Spec.Poly1305.Vec
module ST = FStar.HyperStack.ST
module LSeq = Lib.Sequence
module BSeq = Lib.ByteSequence

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

inline_for_extraction noextract
let felem (w:lanes) = lbuffer (uint64xN w) 5ul
inline_for_extraction noextract
let felem_wide (w:lanes) = felem w
inline_for_extraction noextract
let precomp_r (w:lanes) = lbuffer (uint64xN w) 20ul

unfold noextract
let op_String_Access #a #len = LSeq.index #a #len

noextract
val as_tup5: #w:lanes -> h:mem -> f:felem w -> GTot (felem5 w)
let as_tup5 #w h f =
  let s = as_seq h f in
  let s0 = s.[0] in
  let s1 = s.[1] in
  let s2 = s.[2] in
  let s3 = s.[3] in
  let s4 = s.[4] in
  (s0,s1,s2,s3,s4)

noextract
val felem_fits: #w:lanes -> h:mem -> f:felem w -> m:scale32_5 -> Type0
val felem_fits: #w:lanes -> h:mem -> f:felem w -> m:scale32_5 -> Type0

    h: FStar.Monotonic.HyperStack.mem ->
    f: Hacl.Impl.Poly1305.Field32xN.felem w ->
    m: Hacl.Spec.Poly1305.Field32xN.scale32_5
  -> Type0