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_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)
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.scale32 Prims.nat Prims.b2t Prims.op_LessThanOrEqual FStar.Mul.op_Star Hacl.Spec.Poly1305.Field32xN.max26 FStar.Math.Lemmas.modulo_lemma Prims.pow2 Prims.unit Prims._assert Hacl.Poly1305.Field32xN.Lemmas0.lemma_mult_le
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)
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)

    a: Prims.nat{a <= m1 * Hacl.Spec.Poly1305.Field32xN.max26} ->
    b: Prims.nat{b <= m2 * Hacl.Spec.Poly1305.Field32xN.max26}
  -> FStar.Pervasives.Lemma (ensures a * b % Prims.pow2 64 == a * b)