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)
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)
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.scale64 Lib.IntTypes.uint64 FStar.Math.Lemmas.small_mod Prims.op_Addition Lib.IntTypes.v Lib.IntTypes.U64 Lib.IntTypes.SEC Prims.pow2 Prims.unit FStar.Pervasives.assert_norm Prims.b2t Prims.op_LessThan FStar.Mul.op_Star Hacl.Spec.Poly1305.Field32xN.max26 Prims._assert Prims.op_LessThanOrEqual FStar.Math.Lemmas.lemma_mult_le_right
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)
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)

    ma: Hacl.Spec.Poly1305.Field32xN.scale64 ->
    mb: Hacl.Spec.Poly1305.Field32xN.scale64 ->
    a: Lib.IntTypes.uint64 ->
    b: Lib.IntTypes.uint64
  -> FStar.Pervasives.Lemma
      (requires
        Lib.IntTypes.v a <= ma * Hacl.Spec.Poly1305.Field32xN.max26 /\
        Lib.IntTypes.v b <= mb * Hacl.Spec.Poly1305.Field32xN.max26 /\ ma + mb <= 64)
      (ensures
        Lib.IntTypes.v (a +. b) == Lib.IntTypes.v a + Lib.IntTypes.v b /\
        Lib.IntTypes.v (a +. b) <= (ma + mb) * Hacl.Spec.Poly1305.Field32xN.max26)