val s64x5 (x: scale64) : scale64_5
let s64x5 (x:scale64) : scale64_5 = (x,x,x,x,x)
val s64x5 (x: scale64) : scale64_5
let s64x5 (x: scale64) : scale64_5 =
(x, x, x, x, x)
Hacl.Spec.Poly1305.Field32xN.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.IntVector.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.Poly1305.Vec.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Hacl.Spec.Poly1305.Field32xN.fst
Hacl.Spec.Poly1305.Field32xN.scale64 FStar.Pervasives.Native.Mktuple5 Prims.nat Hacl.Spec.Poly1305.Field32xN.scale64_5
module Hacl.Spec.Poly1305.Field32xN

open Lib.IntTypes
open Lib.IntVector
open Lib.Sequence
open FStar.Mul

open Hacl.Spec.Poly1305.Vec

#reset-options "--z3rlimit 100 --using_facts_from '* -FStar.Seq'"


let scale32 = s:nat{s <= 64}
let scale64 = s:nat{s <= 4096}
let nat5 = (nat & nat & nat & nat & nat)

let scale32_5 = x:nat5{let (x1,x2,x3,x4,x5) = x in
		       x1 <= 64 /\ x2 <= 64 /\ x3 <= 64 /\ x4 <= 64 /\ x5 <= 64}
let scale64_5 = x:nat5{let (x1,x2,x3,x4,x5) = x in
		       x1 <= 4096 /\ x2 <= 4096 /\ x3 <= 4096 /\ x4 <= 4096 /\ x5 <= 4096}
val s64x5 (x: scale64) : scale64_5
x: Hacl.Spec.Poly1305.Field32xN.scale64 -> Hacl.Spec.Poly1305.Field32xN.scale64_5