val mul_identity: a:pfelem -> Lemma (one *% a == a)
let mul_identity a = normalize_term_spec prime
val mul_identity: a:pfelem -> Lemma (one *% a == a)
let mul_identity a =
normalize_term_spec prime
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.normalize_term_spec Prims.pos Hacl.Spec.Poly1305.Lemmas.prime 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)
a: Hacl.Spec.Poly1305.Lemmas.pfelem
  -> FStar.Pervasives.Lemma (ensures Hacl.Spec.Poly1305.Lemmas.one *% a == a)