val pfadd (x y: pfelem) : pfelem
let pfadd (x:pfelem) (y:pfelem) : pfelem = Scalar.fadd x y
val pfadd (x y: pfelem) : pfelem
let pfadd (x y: pfelem) : pfelem =
Scalar.fadd x y
Hacl.Spec.Poly1305.Vec.fst.checked
Spec.Poly1305.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntVector.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked
Hacl.Spec.Poly1305.Vec.fst
Hacl.Spec.Poly1305.Vec.pfelem Spec.Poly1305.fadd
module Hacl.Spec.Poly1305.Vec

#reset-options "--z3rlimit 60 --initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0"

open FStar.Mul
open Lib.IntTypes
open Lib.Sequence
open Lib.ByteSequence
open Lib.IntVector

module Scalar = Spec.Poly1305

(* Field types and parameters *)
val lemma_pow2_128: n:nat ->
  Lemma
  (requires n <= 128)
  (ensures pow2 n < Scalar.prime)
  [SMTPat (pow2 n)]
let lemma_pow2_128 n =
  Math.Lemmas.pow2_le_compat 128 n;
  assert (pow2 n <= pow2 128);
  assert_norm (pow2 128 < Scalar.prime)

let prime = Scalar.prime
val pfadd (x y: pfelem) : pfelem
x: Hacl.Spec.Poly1305.Vec.pfelem -> y: Hacl.Spec.Poly1305.Vec.pfelem
  -> Hacl.Spec.Poly1305.Vec.pfelem