val size_key:size_nat
let size_key   : size_nat = 32
val size_key:size_nat
let size_key:size_nat =
32
Spec.Poly1305.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked
Spec.Poly1305.fst
module Spec.Poly1305

#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

/// Constants and Types

(* Field types and parameters *)
let prime : pos =
  let p = pow2 130 - 5 in
  assert_norm (p > 0);
  p

let felem = x:nat{x < prime}
let fadd (x:felem) (y:felem) : felem = (x + y) % prime
let fmul (x:felem) (y:felem) : felem = (x * y) % prime

let to_felem (x:nat{x < prime}) : felem = x
let from_felem (x:felem) : nat = x
let zero : felem = to_felem 0

(* Poly1305 parameters *)
val size_key:size_nat
n: Prims.nat{n <= Prims.pow2 32 - 1}