val load_precompute_r_post:
    #w:lanes
  -> h:mem
  -> p:precomp_r w
  -> Type0
let load_precompute_r_post #w h p =
  assert_norm (pow2 128 < Vec.prime);
  let r = gsub p 0ul 5ul in
  let rn = gsub p 10ul 5ul in
  let rn_5 = gsub p 15ul 5ul in
  fmul_precomp_r_pre h p /\
  felem_fits h rn (2, 2, 2, 2, 2) /\
  felem_fits h rn_5 (10, 10, 10, 10, 10) /\
  as_tup5 h rn_5 == precomp_r5 (as_tup5 h rn) /\
  feval h rn == Vec.compute_rw (feval h r).[0]
val load_precompute_r_post:
    #w:lanes
  -> h:mem
  -> p:precomp_r w
  -> Type0
let load_precompute_r_post #w h p =
assert_norm (pow2 128 < Vec.prime);
let r = gsub p 0ul 5ul in
let rn = gsub p 10ul 5ul in
let rn_5 = gsub p 15ul 5ul in
fmul_precomp_r_pre h p /\ felem_fits h rn (2, 2, 2, 2, 2) /\ felem_fits h rn_5 (10, 10, 10, 10, 10) /\
as_tup5 h rn_5 == precomp_r5 (as_tup5 h rn) /\ feval h rn == Vec.compute_rw (feval h r).[ 0 ]
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.precomp_r Prims.l_and Hacl.Impl.Poly1305.Field32xN.fmul_precomp_r_pre Hacl.Impl.Poly1305.Field32xN.felem_fits FStar.Pervasives.Native.Mktuple5 Prims.nat Prims.eq2 Hacl.Spec.Poly1305.Field32xN.felem5 Hacl.Impl.Poly1305.Field32xN.as_tup5 Hacl.Spec.Poly1305.Field32xN.precomp_r5 Lib.Sequence.lseq Hacl.Spec.Poly1305.Vec.pfelem Hacl.Impl.Poly1305.Field32xN.feval Hacl.Spec.Poly1305.Vec.compute_rw Hacl.Impl.Poly1305.Field32xN.op_String_Access Lib.Buffer.lbuffer_t Lib.Buffer.MUT Hacl.Spec.Poly1305.Field32xN.uint64xN FStar.UInt32.uint_to_t FStar.UInt32.t Lib.Buffer.gsub FStar.UInt32.__uint_to_t Prims.unit FStar.Pervasives.assert_norm Prims.b2t Prims.op_LessThan Prims.pow2 Hacl.Spec.Poly1305.Vec.prime
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
let felem_fits #w h f m =
  felem_fits5 (as_tup5 h f) m

noextract
val felem_wide_fits: #w:lanes -> h:mem -> f:felem w -> m:scale32_5 -> Type0
let felem_wide_fits #w h f m =
  felem_wide_fits5 (as_tup5 h f) m

noextract
let feval (#w:lanes) (h:mem) (f:felem w) : GTot (LSeq.lseq Vec.pfelem w) =
  feval5 (as_tup5 h f)

noextract
let fas_nat (#w:lanes) (h:mem) (f:felem w) : GTot (LSeq.lseq nat w) =
  fas_nat5 (as_tup5 h f)

noextract
let felem_less (#w:lanes) (h:mem) (f:felem w) (max:nat) : Type0 =
  felem_less5 (as_tup5 h f) max

val lemma_feval_is_fas_nat:
    #w:lanes
  -> h:mem
  -> f:felem w
  -> Lemma
    (requires felem_less h f (pow2 128))
    (ensures  (forall (i:nat). i < w ==> (feval h f).[i] == (fas_nat h f).[i]))
let lemma_feval_is_fas_nat #w h f =
  lemma_feval_is_fas_nat (as_tup5 h f)

inline_for_extraction noextract
val fmul_precomp_r_pre:
    #w:lanes
  -> h:mem
  -> precomp:precomp_r w
  -> Type0
let fmul_precomp_r_pre #w h precomp =
  let r = gsub precomp 0ul 5ul in
  let r_5 = gsub precomp 5ul 5ul in
  felem_fits h r (1, 1, 1, 1, 1) /\
  felem_fits h r_5 (5, 5, 5, 5, 5) /\
  as_tup5 h r_5 == precomp_r5 (as_tup5 h r)

noextract
val load_precompute_r_post:
    #w:lanes
  -> h:mem
  -> p:precomp_r w
  -> Type0
val load_precompute_r_post:
    #w:lanes
  -> h:mem
  -> p:precomp_r w
  -> Type0
h: FStar.Monotonic.HyperStack.mem -> p: Hacl.Impl.Poly1305.Field32xN.precomp_r w -> Type0