val poly1305_encode_r (rb: block) : Tot felem
let poly1305_encode_r (rb:block) : Tot felem =
  let lo = uint_from_bytes_le (sub rb 0 8) in
  let hi = uint_from_bytes_le (sub rb 8 8) in
  let mask0 = u64 0x0ffffffc0fffffff in
  let mask1 = u64 0x0ffffffc0ffffffc in
  let lo = lo &. mask0 in
  let hi = hi &. mask1 in
  assert_norm (pow2 128 < prime);
  to_felem (uint_v hi * pow2 64 + uint_v lo)
val poly1305_encode_r (rb: block) : Tot felem
let poly1305_encode_r (rb: block) : Tot felem =
let lo = uint_from_bytes_le (sub rb 0 8) in
let hi = uint_from_bytes_le (sub rb 8 8) in
let mask0 = u64 0x0ffffffc0fffffff in
let mask1 = u64 0x0ffffffc0ffffffc in
let lo = lo &. mask0 in
let hi = hi &. mask1 in
assert_norm (pow2 128 < prime);
to_felem (uint_v hi * pow2 64 + uint_v lo)
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
Spec.Poly1305.block Spec.Poly1305.to_felem Prims.op_Addition FStar.Mul.op_Star Lib.IntTypes.uint_v Lib.IntTypes.U64 Lib.IntTypes.SEC Prims.pow2 Prims.unit FStar.Pervasives.assert_norm Prims.b2t Prims.op_LessThan Spec.Poly1305.prime Lib.IntTypes.int_t Lib.IntTypes.op_Amp_Dot Prims.eq2 Prims.int Lib.IntTypes.range Lib.IntTypes.v Lib.IntTypes.u64 Lib.ByteSequence.uint_from_bytes_le Lib.Sequence.sub Lib.IntTypes.uint_t Lib.IntTypes.U8 Spec.Poly1305.size_block Spec.Poly1305.felem
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 *)
let size_block : size_nat = 16
let size_key   : size_nat = 32

type block = lbytes size_block
type tag   = lbytes size_block
type key   = lbytes size_key

/// Specification
val poly1305_encode_r (rb: block) : Tot felem
rb: Spec.Poly1305.block -> Spec.Poly1305.felem