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_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);
}
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.Calc.calc_finish Prims.eq2 Hacl.Spec.Poly1305.Lemmas.op_Plus_Percent Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step Prims.op_Modulus Prims.op_Addition Hacl.Spec.Poly1305.Lemmas.prime FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash FStar.Math.Lemmas.lemma_mod_plus_distr_l FStar.Math.Lemmas.lemma_mod_plus_distr_r FStar.Pervasives.normalize_term_spec Prims.pos
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))
val add_associativity: a:pfelem -> b:pfelem -> c:pfelem
  -> Lemma (a +% b +% c == a +% (b +% c))

    a: Hacl.Spec.Poly1305.Lemmas.pfelem ->
    b: Hacl.Spec.Poly1305.Lemmas.pfelem ->
    c: Hacl.Spec.Poly1305.Lemmas.pfelem
  -> FStar.Pervasives.Lemma (ensures a +% b +% c == a +% (b +% c))