val smul_felem5_eval_lemma:
    #w:lanes
  -> #m1:scale32
  -> #m2:scale32_5
  -> u1:uint64xN w{felem_fits1 u1 m1}
  -> f2:felem5 w{felem_fits5 f2 m2} ->
  Lemma (fas_nat5 (smul_felem5 #w u1 f2) ==
    map2 #nat #nat #nat (fun a b -> a * b) (uint64xN_v u1) (fas_nat5 f2))
let smul_felem5_eval_lemma #w #m1 #m2 u1 f2 =
  FStar.Classical.forall_intro (smul_felem5_eval_lemma_i #w #m1 #m2 u1 f2);
  eq_intro (fas_nat5 (smul_felem5 #w u1 f2))
    (map2 #nat #nat #nat (fun a b -> a * b) (uint64xN_v u1) (fas_nat5 f2))
val smul_felem5_eval_lemma:
    #w:lanes
  -> #m1:scale32
  -> #m2:scale32_5
  -> u1:uint64xN w{felem_fits1 u1 m1}
  -> f2:felem5 w{felem_fits5 f2 m2} ->
  Lemma (fas_nat5 (smul_felem5 #w u1 f2) ==
    map2 #nat #nat #nat (fun a b -> a * b) (uint64xN_v u1) (fas_nat5 f2))
let smul_felem5_eval_lemma #w #m1 #m2 u1 f2 =
FStar.Classical.forall_intro (smul_felem5_eval_lemma_i #w #m1 #m2 u1 f2);
eq_intro (fas_nat5 (smul_felem5 #w u1 f2))
  (map2 #nat #nat #nat (fun a b -> a * b) (uint64xN_v u1) (fas_nat5 f2))
Hacl.Poly1305.Field32xN.Lemmas0.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.IntVector.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.Poly1305.Vec.fst.checked Hacl.Spec.Poly1305.Field32xN.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Hacl.Poly1305.Field32xN.Lemmas0.fst
Hacl.Spec.Poly1305.Field32xN.lanes Hacl.Spec.Poly1305.Field32xN.scale32 Hacl.Spec.Poly1305.Field32xN.scale32_5 Hacl.Spec.Poly1305.Field32xN.uint64xN Hacl.Spec.Poly1305.Field32xN.felem_fits1 Hacl.Spec.Poly1305.Field32xN.felem5 Hacl.Spec.Poly1305.Field32xN.felem_fits5 Lib.Sequence.eq_intro Prims.nat Hacl.Spec.Poly1305.Field32xN.fas_nat5 Hacl.Spec.Poly1305.Field32xN.smul_felem5 Lib.Sequence.map2 FStar.Mul.op_Star Hacl.Spec.Poly1305.Field32xN.uint64xN_v Prims.unit FStar.Classical.forall_intro Prims.b2t Prims.op_LessThan Prims.eq2 Prims.int Lib.Sequence.op_String_Access Hacl.Poly1305.Field32xN.Lemmas0.smul_felem5_eval_lemma_i
module Hacl.Poly1305.Field32xN.Lemmas0

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

open Hacl.Spec.Poly1305.Vec
include Hacl.Spec.Poly1305.Field32xN

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

val lemma_prime: unit -> Lemma (pow2 130 % prime = 5)
let lemma_prime () =
  assert_norm (pow2 130 % prime = 5 % prime);
  assert_norm (5 < prime);
  FStar.Math.Lemmas.modulo_lemma 5 prime

val lemma_mult_le: a:nat -> b:nat -> c:nat -> d:nat -> Lemma
  (requires a <= b /\ c <= d)
  (ensures  a * c <= b * d)
let lemma_mult_le a b c d = ()

val lemma_mul5_distr_l: a:nat -> b:nat -> c:nat -> d:nat -> e:nat -> f:nat -> Lemma
  (a * (b + c + d + e + f) == a * b + a * c + a * d + a * e + a * f)
let lemma_mul5_distr_l a b c d e f = ()

val lemma_mul5_distr_r: a:nat -> b:nat -> c:nat -> d:nat -> e:nat -> f:nat -> Lemma
  ((a + b + c + d + e) * f == a * f + b * f + c * f + d * f + e * f)
let lemma_mul5_distr_r a b c d e f = ()


val smul_mod_lemma:
    #m1:scale32
  -> #m2:scale32
  -> a:nat{a <= m1 * max26}
  -> b:nat{b <= m2 * max26} ->
  Lemma (a * b % pow2 64 == a * b)

let smul_mod_lemma #m1 #m2 a b =
  lemma_mult_le a (m1 * max26) b (m2 * max26);
  assert (a * b <= m1 * m2 * max26 * max26);
  FStar.Math.Lemmas.modulo_lemma (a * b) (pow2 64)


val smul_add_mod_lemma:
    #m1:scale32
  -> #m2:scale32
  -> #m3:scale64{m3 + m1 * m2 <= 4096}
  -> a:nat{a <= m1 * max26}
  -> b:nat{b <= m2 * max26}
  -> c:nat{c <= m3 * max26 * max26} ->
  Lemma ((c + a * b % pow2 64) % pow2 64 == c + a * b)

let smul_add_mod_lemma #m1 #m2 #m3 a b c =
  assert_norm ((m3 + m1 * m2) * max26 * max26 < pow2 64);
  lemma_mult_le a (m1 * max26) b (m2 * max26);
  assert (c + a * b <= m3 * max26 * max26 + m1 * m2 * max26 * max26);
  FStar.Math.Lemmas.modulo_lemma (c + a * b) (pow2 64)


val add5_lemma1: ma:scale64 -> mb:scale64 -> a:uint64 -> b:uint64 -> Lemma
  (requires v a <= ma * max26 /\ v b <= mb * max26 /\ ma + mb <= 64)
  (ensures  v (a +. b) == v a + v b /\ v (a +. b) <= (ma + mb) * max26)

let add5_lemma1 ma mb a b =
  assert (v a + v b <= (ma + mb) * max26);
  Math.Lemmas.lemma_mult_le_right max26 (ma + mb) 64;
  assert (v a + v b <= 64 * max26);
  assert_norm (64 * max26 < pow2 32);
  Math.Lemmas.small_mod (v a + v b) (pow2 32)


#set-options "--ifuel 1"

val fadd5_eval_lemma_i:
    #w:lanes
  -> f1:felem5 w{felem_fits5 f1 (2,2,2,2,2)}
  -> f2:felem5 w{felem_fits5 f2 (1,1,1,1,1)}
  -> i:nat{i < w} ->
  Lemma ((feval5 (fadd5 f1 f2)).[i] == pfadd (feval5 f1).[i] (feval5 f2).[i])

let fadd5_eval_lemma_i #w f1 f2 i =
  let o = fadd5 f1 f2 in
  let (f10, f11, f12, f13, f14) = as_tup64_i f1 i in
  let (f20, f21, f22, f23, f24) = as_tup64_i f2 i in
  let (o0, o1, o2, o3, o4) = as_tup64_i o i in

  add5_lemma1 2 1 f10 f20;
  add5_lemma1 2 1 f11 f21;
  add5_lemma1 2 1 f12 f22;
  add5_lemma1 2 1 f13 f23;
  add5_lemma1 2 1 f14 f24;
  assert (as_nat5 (o0, o1, o2, o3, o4) ==
    as_nat5 (f10, f11, f12, f13, f14) + as_nat5 (f20, f21, f22, f23, f24));
  FStar.Math.Lemmas.lemma_mod_plus_distr_l
    (as_nat5 (f10, f11, f12, f13, f14)) (as_nat5 (f20, f21, f22, f23, f24)) prime;
  FStar.Math.Lemmas.lemma_mod_plus_distr_r
    (as_nat5 (f10, f11, f12, f13, f14) % prime) (as_nat5 (f20, f21, f22, f23, f24)) prime


val smul_felem5_fits_lemma_i:
    #w:lanes
  -> #m1:scale32
  -> #m2:scale32
  -> u1:uint64xN w{felem_fits1 u1 m1}
  -> f2:uint64xN w{felem_fits1 f2 m2}
  -> i:nat{i < w} ->
  Lemma ((uint64xN_v (vec_mul_mod f2 u1)).[i] <= m1 * m2 * max26 * max26)

let smul_felem5_fits_lemma_i #w #m1 #m2 u1 f2 i =
  let o = vec_mul_mod f2 u1 in
  smul_mod_lemma #m1 #m2 (uint64xN_v u1).[i] (uint64xN_v f2).[i];
  assert ((uint64xN_v o).[i] == (uint64xN_v u1).[i] * (uint64xN_v f2).[i]);
  lemma_mult_le (uint64xN_v u1).[i] (m1 * max26) (uint64xN_v f2).[i] (m2 * max26)


val smul_felem5_eval_lemma_i:
    #w:lanes
  -> #m1:scale32
  -> #m2:scale32_5
  -> u1:uint64xN w{felem_fits1 u1 m1}
  -> f2:felem5 w{felem_fits5 f2 m2}
  -> i:nat{i < w} ->
  Lemma ((fas_nat5 (smul_felem5 #w u1 f2)).[i] == (uint64xN_v u1).[i] * (fas_nat5 f2).[i])

let smul_felem5_eval_lemma_i #w #m1 #m2 u1 f2 i =
  let o = smul_felem5 #w u1 f2 in
  let (m20, m21, m22, m23, m24) = m2 in
  let vu1 = (uint64xN_v u1).[i] in
  let (tf20, tf21, tf22, tf23, tf24) = as_tup64_i f2 i in
  let (to0, to1, to2, to3, to4) = as_tup64_i o i in

  smul_mod_lemma #m1 #m20 vu1 (v tf20);
  smul_mod_lemma #m1 #m21 vu1 (v tf21);
  smul_mod_lemma #m1 #m22 vu1 (v tf22);
  smul_mod_lemma #m1 #m23 vu1 (v tf23);
  smul_mod_lemma #m1 #m24 vu1 (v tf24);

  assert ((fas_nat5 o).[i] == vu1 * v tf20 + vu1 * v tf21 * pow26 + vu1 * v tf22 * pow52 +
    vu1 * v tf23 * pow78 + vu1 * v tf24 * pow104);

  calc (==) {
    vu1 * (fas_nat5 f2).[i];
  (==) { }
    vu1 * (v tf20 + v tf21 * pow26 + v tf22 * pow52 + v tf23 * pow78 + v tf24 * pow104);
  (==) { lemma_mul5_distr_l vu1 (v tf20) (v tf21 * pow26) (v tf22 * pow52) (v tf23 * pow78) (v tf24 * pow104)}
    vu1 * v tf20 + vu1 * (v tf21 * pow26) + vu1 * (v tf22 * pow52) + vu1 * (v tf23 * pow78) + vu1 * (v tf24 * pow104);
  (==) {
    FStar.Math.Lemmas.paren_mul_right vu1 (v tf21) pow26;
    FStar.Math.Lemmas.paren_mul_right vu1 (v tf22) pow52;
    FStar.Math.Lemmas.paren_mul_right vu1 (v tf23) pow78;
    FStar.Math.Lemmas.paren_mul_right vu1 (v tf24) pow104}
    vu1 * v tf20 + vu1 * v tf21 * pow26 + vu1 * v tf22 * pow52 + vu1 * v tf23 * pow78 + vu1 * v tf24 * pow104;
    };
  assert (vu1 * (fas_nat5 f2).[i] == (fas_nat5 o).[i])


val smul_felem5_fits_lemma1:
    #w:lanes
  -> #m1:scale32
  -> #m2:scale32
  -> u1:uint64xN w{felem_fits1 u1 m1}
  -> f2:uint64xN w{felem_fits1 f2 m2} ->
  Lemma (felem_wide_fits1 (vec_mul_mod f2 u1) (m1 * m2))

let smul_felem5_fits_lemma1 #w #m1 #m2 u1 f2 =
  match w with
  | 1 ->
    smul_felem5_fits_lemma_i #w #m1 #m2 u1 f2 0
  | 2 ->
    smul_felem5_fits_lemma_i #w #m1 #m2 u1 f2 0;
    smul_felem5_fits_lemma_i #w #m1 #m2 u1 f2 1
  | 4 ->
    smul_felem5_fits_lemma_i #w #m1 #m2 u1 f2 0;
    smul_felem5_fits_lemma_i #w #m1 #m2 u1 f2 1;
    smul_felem5_fits_lemma_i #w #m1 #m2 u1 f2 2;
    smul_felem5_fits_lemma_i #w #m1 #m2 u1 f2 3


val smul_felem5_fits_lemma:
    #w:lanes
  -> #m1:scale32
  -> #m2:scale32_5
  -> u1:uint64xN w{felem_fits1 u1 m1}
  -> f2:felem5 w{felem_fits5 f2 m2} ->
  Lemma (felem_wide_fits5 (smul_felem5 #w u1 f2) (m1 *^ m2))

let smul_felem5_fits_lemma #w #m1 #m2 u1 f2 =
  let (f20, f21, f22, f23, f24) = f2 in
  let (m20, m21, m22, m23, m24) = m2 in
  smul_felem5_fits_lemma1 #w #m1 #m20 u1 f20;
  smul_felem5_fits_lemma1 #w #m1 #m21 u1 f21;
  smul_felem5_fits_lemma1 #w #m1 #m22 u1 f22;
  smul_felem5_fits_lemma1 #w #m1 #m23 u1 f23;
  smul_felem5_fits_lemma1 #w #m1 #m24 u1 f24


val smul_felem5_eval_lemma:
    #w:lanes
  -> #m1:scale32
  -> #m2:scale32_5
  -> u1:uint64xN w{felem_fits1 u1 m1}
  -> f2:felem5 w{felem_fits5 f2 m2} ->
  Lemma (fas_nat5 (smul_felem5 #w u1 f2) ==
    map2 #nat #nat #nat (fun a b -> a * b) (uint64xN_v u1) (fas_nat5 f2))
val smul_felem5_eval_lemma:
    #w:lanes
  -> #m1:scale32
  -> #m2:scale32_5
  -> u1:uint64xN w{felem_fits1 u1 m1}
  -> f2:felem5 w{felem_fits5 f2 m2} ->
  Lemma (fas_nat5 (smul_felem5 #w u1 f2) ==
    map2 #nat #nat #nat (fun a b -> a * b) (uint64xN_v u1) (fas_nat5 f2))

    u1: Hacl.Spec.Poly1305.Field32xN.uint64xN w {Hacl.Spec.Poly1305.Field32xN.felem_fits1 u1 m1} ->
    f2: Hacl.Spec.Poly1305.Field32xN.felem5 w {Hacl.Spec.Poly1305.Field32xN.felem_fits5 f2 m2}
  -> FStar.Pervasives.Lemma
    (ensures
      Hacl.Spec.Poly1305.Field32xN.fas_nat5 (Hacl.Spec.Poly1305.Field32xN.smul_felem5 u1 f2) ==
      Lib.Sequence.map2 (fun a b -> a * b)
        (Hacl.Spec.Poly1305.Field32xN.uint64xN_v u1)
        (Hacl.Spec.Poly1305.Field32xN.fas_nat5 f2))