val mul_zero_l: mult_zero_l_lemma pfelem pfelem_add_cm pfelem_mul_cm
let mul_zero_l a = assert_norm (forall x. zero *% x == zero)
val mul_zero_l: mult_zero_l_lemma pfelem pfelem_add_cm pfelem_mul_cm
let mul_zero_l a =
assert_norm (forall x. zero *% x == zero)
Hacl.Spec.Poly1305.Lemmas.fst.checked
Spec.Poly1305.fst.checked prims.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.CanonCommSemiring.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked FStar.Algebra.CommMonoid.fst.checked
Hacl.Spec.Poly1305.Lemmas.fst
Hacl.Spec.Poly1305.Lemmas.pfelem FStar.Pervasives.assert_norm Prims.l_Forall Prims.eq2 Hacl.Spec.Poly1305.Lemmas.op_Star_Percent Hacl.Spec.Poly1305.Lemmas.zero Prims.unit
module Hacl.Spec.Poly1305.Lemmas

open FStar.Mul
module Scalar = Spec.Poly1305

open FStar.Algebra.CommMonoid
open FStar.Tactics.CanonCommSemiring

/// Semiring for Poly1305

#set-options "--z3rlimit 5 --max_fuel 0 --max_ifuel 0 --z3cliopt smt.arith.nl=false"

let prime: pos = Scalar.prime

let pfelem : eqtype = a:nat{a < prime}

[@canon_attr]
let zero : pfelem = 0

[@canon_attr]
let one : pfelem = normalize_term_spec prime; 1

//[@(strict_on_arguments [0;1])]
let ( +% ) (a b:pfelem) : pfelem = (a + b) % prime

//[@(strict_on_arguments [0;1])]
let ( *% ) (a b:pfelem) : pfelem = (a * b) % prime

//[@(strict_on_arguments [0])]
let ( ~% ) (a:pfelem) : pfelem = (-a) % prime

val add_identity: a:pfelem -> Lemma (zero +% a == a)
let add_identity a = normalize_term_spec prime

val mul_identity: a:pfelem -> Lemma (one *% a == a)
let mul_identity a = normalize_term_spec prime

val add_associativity: a:pfelem -> b:pfelem -> c:pfelem
  -> Lemma (a +% b +% c == a +% (b +% c))
let add_associativity a b c =
  normalize_term_spec prime;
  calc (==) {
    a +% b +% c;
    == { }
    ((a + b) % prime + c) % prime;
    == { Math.Lemmas.lemma_mod_plus_distr_l (a + b) c prime }
    ((a + b) + c) % prime;
    == { }
    (a + (b + c)) % prime;
    == { Math.Lemmas.lemma_mod_plus_distr_r a (b + c) prime }
    a +% (b +% c);
  }

val add_commutativity: a:pfelem -> b:pfelem -> Lemma (a +% b == b +% a)
let add_commutativity a b = ()

val mul_associativity: a:pfelem -> b:pfelem -> c:pfelem
  -> Lemma (a *% b *% c == a *% (b *% c))
let mul_associativity a b c =
  calc (==) {
    a *% b *% c;
    == { }
    (((a * b) % prime) * c) % prime;
    == { Math.Lemmas.lemma_mod_mul_distr_l (a * b) c prime }
    ((a * b) * c) % prime;
    == { Math.Lemmas.paren_mul_right a b c }
    (a * (b * c)) % prime;
    == { Math.Lemmas.lemma_mod_mul_distr_r a (b * c) prime }
    (a * ((b * c) % prime)) % prime;
    == { }
    a *% (b *% c);
  }

val mul_commutativity: a:pfelem -> b:pfelem -> Lemma (a *% b == b *% a)
let mul_commutativity a b = ()

[@canon_attr]
let pfelem_add_cm : cm pfelem =
  CM zero ( +% ) add_identity add_associativity add_commutativity

[@canon_attr]
let pfelem_mul_cm : cm pfelem =
  CM one ( *% ) mul_identity mul_associativity mul_commutativity

val mul_add_distr: distribute_left_lemma pfelem pfelem_add_cm pfelem_mul_cm
let mul_add_distr a b c =
  normalize_term_spec prime;
  calc (==) {
    a *% (b +% c);
    == { }
    (a * (b +% c)) % prime;
    == { Math.Lemmas.lemma_mod_add_distr a (b + c) prime }
    (a * ((b + c) % prime)) % prime;
    == { Math.Lemmas.lemma_mod_mul_distr_r a (b + c) prime }
    (a * (b + c)) % prime;
    == { Math.Lemmas.distributivity_add_right a b c }
    (a * b + a * c) % prime;
    == { Math.Lemmas.lemma_mod_add_distr (a * b) (a * c) prime }
    (a * b + a *% c) % prime;
    == { }
    (a *% c + a * b) % prime;
    == { Math.Lemmas.lemma_mod_add_distr (a *% c) (a * b) prime }
    (a *% c + a *% b) % prime;
    == { }
    (a *% b + a *% c) % prime;
    == { }
    a *% b +% a *% c;
  }
val mul_zero_l: mult_zero_l_lemma pfelem pfelem_add_cm pfelem_mul_cm
FStar.Tactics.CanonCommSemiring.mult_zero_l_lemma Hacl.Spec.Poly1305.Lemmas.pfelem
  Hacl.Spec.Poly1305.Lemmas.pfelem_add_cm
  Hacl.Spec.Poly1305.Lemmas.pfelem_mul_cm