let op_String_Access #a #len = LSeq.index #a #len
let op_String_Access #a #len =
LSeq.index #a #len
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
Lib.IntTypes.size_nat Lib.Sequence.index Lib.Sequence.lseq Prims.nat Prims.b2t Prims.op_LessThanOrEqual Prims.op_Subtraction Prims.pow2 Prims.op_LessThan Prims.eq2 FStar.Seq.Base.index Lib.Sequence.to_seq
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
val op_String_Access : s: Lib.Sequence.lseq a len -> i: (n: Prims.nat{n <= Prims.pow2 32 - 1}){i < len}
  -> r: a{r == FStar.Seq.Base.index (Lib.Sequence.to_seq s) i}
s: Lib.Sequence.lseq a len -> i: (n: Prims.nat{n <= Prims.pow2 32 - 1}){i < len}
  -> r: a{r == FStar.Seq.Base.index (Lib.Sequence.to_seq s) i}