val poly1305_do:
    k:Poly.key
  -> m:bytes{length m <= maxint U64}
  -> aad:bytes{length aad <= maxint U64} ->
  Tot Poly.tag
let poly1305_do k m aad =
  let acc, r = Poly.poly1305_init k in
  let acc = if (length aad <> 0) then poly1305_padded r aad acc else acc in
  let acc = if (length m <> 0) then poly1305_padded r m acc else acc in
  let aad_len8 = uint_to_bytes_le #U64 (u64 (length aad)) in
  let ciphertext_len8 = uint_to_bytes_le #U64 (u64 (length m)) in
  let block = aad_len8 @| ciphertext_len8 in
  let acc = Poly.poly1305_update1 r 16 block acc in
  Poly.poly1305_finish k acc
val poly1305_do:
    k:Poly.key
  -> m:bytes{length m <= maxint U64}
  -> aad:bytes{length aad <= maxint U64} ->
  Tot Poly.tag
let poly1305_do k m aad =
let acc, r = Poly.poly1305_init k in
let acc = if (length aad <> 0) then poly1305_padded r aad acc else acc in
let acc = if (length m <> 0) then poly1305_padded r m acc else acc in
let aad_len8 = uint_to_bytes_le #U64 (u64 (length aad)) in
let ciphertext_len8 = uint_to_bytes_le #U64 (u64 (length m)) in
let block = aad_len8 @| ciphertext_len8 in
let acc = Poly.poly1305_update1 r 16 block acc in
Poly.poly1305_finish k acc
Spec.Chacha20Poly1305.fst.checked
Spec.Poly1305.fst.checked Spec.Chacha20.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Spec.Chacha20Poly1305.fst
Spec.Poly1305.key Lib.ByteSequence.bytes Prims.b2t Prims.op_LessThanOrEqual Lib.Sequence.length Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.IntTypes.maxint Lib.IntTypes.U64 Spec.Poly1305.felem Spec.Poly1305.poly1305_finish Spec.Poly1305.poly1305_update1 Lib.Sequence.lseq Lib.IntTypes.int_t Prims.op_Addition Prims.eq2 FStar.Seq.Base.seq Lib.Sequence.to_seq FStar.Seq.Base.append Lib.Sequence.op_At_Bar Lib.IntTypes.numbytes Lib.ByteSequence.uint_to_bytes_le Lib.IntTypes.u64 Prims.op_disEquality Prims.int Spec.Chacha20Poly1305.poly1305_padded Prims.bool Spec.Poly1305.tag FStar.Pervasives.Native.tuple2 Spec.Poly1305.poly1305_init
module Spec.Chacha20Poly1305

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

module Poly = Spec.Poly1305

(* RFC7539: https://tools.ietf.org/html/rfc7539#section-2.8 *)
#set-options "--max_fuel 0 --z3rlimit 30"

/// Constants

let size_key : size_nat =   32 (* in bytes *)
let size_nonce : size_nat = 12 (* in bytes *)
let size_block : size_nat = Poly.size_block
let size_tag : size_nat = size_block

/// Types

type key = lbytes size_key
type nonce = lbytes size_nonce
type tag = lbytes size_tag

/// Specification

val poly1305_padded:
    r_elem:Poly.felem
  -> text:bytes
  -> acc:Poly.felem ->
  Tot Poly.felem
let poly1305_padded r_elem text acc =
  let len = length text in
  let n = len / Poly.size_block in
  let r = len % Poly.size_block in
  let blocks = Seq.slice text 0 (n * Poly.size_block) in
  let rem = Seq.slice text (n * Poly.size_block) len in
  let acc = Poly.poly1305_update blocks acc r_elem in

  let tmp = create Poly.size_block (u8 0) in
  let tmp = update_sub tmp 0 r rem in
  // Only run the padded block if the initial text needed padding
  let acc = if r > 0 then Poly.poly1305_update1 r_elem Poly.size_block tmp acc else acc in
  acc

val poly1305_do:
    k:Poly.key
  -> m:bytes{length m <= maxint U64}
  -> aad:bytes{length aad <= maxint U64} ->
val poly1305_do:
    k:Poly.key
  -> m:bytes{length m <= maxint U64}
  -> aad:bytes{length aad <= maxint U64} ->
  Tot Poly.tag

    k: Spec.Poly1305.key ->
    m: Lib.ByteSequence.bytes{Lib.Sequence.length m <= Lib.IntTypes.maxint Lib.IntTypes.U64} ->
    aad: Lib.ByteSequence.bytes{Lib.Sequence.length aad <= Lib.IntTypes.maxint Lib.IntTypes.U64}
  -> Spec.Poly1305.tag