val fas_nat5 (#w: lanes) (f: felem5 w) : lseq nat w
let fas_nat5 (#w:lanes) (f:felem5 w) : lseq nat w =
  map as_nat5 (transpose f)
val fas_nat5 (#w: lanes) (f: felem5 w) : lseq nat w
let fas_nat5 (#w: lanes) (f: felem5 w) : lseq nat w =
map as_nat5 (transpose f)
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.lanes Hacl.Spec.Poly1305.Field32xN.felem5 Lib.Sequence.map Hacl.Spec.Poly1305.Field32xN.tup64_5 Prims.nat Hacl.Spec.Poly1305.Field32xN.as_nat5 Hacl.Spec.Poly1305.Field32xN.transpose Lib.Sequence.lseq
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}

let s64x5 (x:scale64) : scale64_5 = (x,x,x,x,x)

noextract
let ( *^ ) (x:scale32) (y:scale32_5) : scale64_5 =
  assert_norm (64 * 64 = 4096);
  let (y1,y2,y3,y4,y5) = y in
  (x * y1 ,
   x * y2 ,
   x * y3 ,
   x * y4 ,
   x * y5)

noextract
let ( +* ) (x:nat5) (y:nat5) : nat5 =
  let (x1,x2,x3,x4,x5) = x in
  let (y1,y2,y3,y4,y5) = y in
  (x1 + y1 ,
   x2 + y2 ,
   x3 + y3 ,
   x4 + y4 ,
   x5 + y5)

noextract
let ( <=* ) (x:nat5) (y:nat5) : Type =
  let (x1,x2,x3,x4,x5) = x in
  let (y1,y2,y3,y4,y5) = y in
  (x1 <= y1) /\
  (x2 <= y2) /\
  (x3 <= y3) /\
  (x4 <= y4) /\
  (x5 <= y5)

//abstract
let pow26: (pow26: pos { pow2 32 == 64 * pow26 /\ pow2 64 == 4096 * pow26 * pow26 /\ pow26 == pow2 26 }) =
  let pow26: pos = pow2 26 in
  assert_norm (pow2 32 == 64 * pow26);
  assert_norm (pow2 64 == 4096 * pow26 * pow26);
  pow26

let pow52: (pow52:pos {pow52 == pow2 52}) = normalize_term (pow2 52)
let pow78: (pow78:pos {pow78 == pow2 78}) = normalize_term (pow2 78)
let pow104: (pow104:pos {pow104 == pow2 104}) = normalize_term (pow2 104)

inline_for_extraction
let max26 = pow26 - 1


let tup64_5 = (uint64 & uint64 & uint64 & uint64 & uint64)

let tup64_fits1 (f:uint64) (m:scale32) =
  uint_v f <= m * max26

let tup64_wide_fits1 (f:uint64) (m:scale64) =
  uint_v f <= m * max26 * max26

let tup64_fits5 (f:tup64_5) (m:scale32_5) =
  let (x0, x1, x2, x3, x4) = f in
  let (m0, m1, m2, m3, m4) = m in
  tup64_fits1 x0 m0 /\
  tup64_fits1 x1 m1 /\
  tup64_fits1 x2 m2 /\
  tup64_fits1 x3 m3 /\
  tup64_fits1 x4 m4

let tup64_wide_fits5 (f:tup64_5) (m:scale64_5) =
  let (x0, x1, x2, x3, x4) = f in
  let (m0, m1, m2, m3, m4) = m in
  tup64_wide_fits1 x0 m0 /\
  tup64_wide_fits1 x1 m1 /\
  tup64_wide_fits1 x2 m2 /\
  tup64_wide_fits1 x3 m3 /\
  tup64_wide_fits1 x4 m4

noextract
val as_nat5: f:tup64_5 -> nat
let as_nat5  f =
  let (s0, s1, s2, s3, s4) = f in
  v s0 + v s1 * pow26 + v s2 * pow52 + v s3 * pow78 + v s4 * pow104

noextract
let as_pfelem5 (f:tup64_5) : pfelem =
  (as_nat5 f) % prime


let lanes = w:width{w == 1 \/ w == 2 \/ w == 4}
inline_for_extraction
let uint64xN (w:lanes) = vec_t U64 w

inline_for_extraction
let zero (w:lanes) = vec_zero U64 w
inline_for_extraction
let mask26 (w:lanes) = vec_load (u64 0x3ffffff) w
inline_for_extraction
let mask14 (w:lanes) = vec_load (u64 0x3fff) w

inline_for_extraction
let felem5 (w:lanes) = (uint64xN w & uint64xN w & uint64xN w & uint64xN w & uint64xN w)
inline_for_extraction
let felem_wide5 (w:lanes) = felem5 w

let felem_fits1 (#w:lanes) (x:uint64xN w) (m:scale32) =
  forall (i:nat). {:pattern (vec_v x).[i] } i < w ==> uint_v (vec_v x).[i] <= m * max26

let felem_wide_fits1 (#w:lanes) (x:uint64xN w) (m:scale64) =
  forall (i:nat). {:pattern (vec_v x).[i] } i < w ==> uint_v (vec_v x).[i] <= m * max26 * max26

let felem_fits5 (#w:lanes) (f:felem5 w) (m:scale32_5) =
  let (x1,x2,x3,x4,x5) = f in
  let (m1,m2,m3,m4,m5) = m in
  felem_fits1 x1 m1 /\
  felem_fits1 x2 m2 /\
  felem_fits1 x3 m3 /\
  felem_fits1 x4 m4 /\
  felem_fits1 x5 m5

let felem_wide_fits5 (#w:lanes) (f:felem_wide5 w) (m:scale64_5) =
  let (x1,x2,x3,x4,x5) = f in
  let (m1,m2,m3,m4,m5) = m in
  felem_wide_fits1 x1 m1 /\
  felem_wide_fits1 x2 m2 /\
  felem_wide_fits1 x3 m3 /\
  felem_wide_fits1 x4 m4 /\
  felem_wide_fits1 x5 m5

noextract
let transpose (#w:lanes) (f:felem5 w) : lseq tup64_5 w =
  let (f0,f1,f2,f3,f4) = f in
  let v0 = vec_v f0 in
  let v1 = vec_v f1 in
  let v2 = vec_v f2 in
  let v3 = vec_v f3 in
  let v4 = vec_v f4 in
  createi #tup64_5 w (fun i -> (v0.[i],v1.[i],v2.[i],v3.[i],v4.[i]))

noextract
let as_tup64_i (#w:lanes) (f:felem5 w) (i:nat{i < w}): tup64_5 =
  (transpose #w f).[i]

noextract
let feval5 (#w:lanes) (f:felem5 w) : lseq pfelem w =
  map as_pfelem5 (transpose f)

noextract
val fas_nat5 (#w: lanes) (f: felem5 w) : lseq nat w
f: Hacl.Spec.Poly1305.Field32xN.felem5 w -> Lib.Sequence.lseq Prims.nat w