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_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
let acc = if r > 0 then Poly.poly1305_update1 r_elem Poly.size_block tmp acc else acc in
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.felem Lib.ByteSequence.bytes Prims.op_GreaterThan Spec.Poly1305.poly1305_update1 Spec.Poly1305.size_block Prims.bool Lib.Sequence.lseq Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Prims.l_and Prims.eq2 Lib.Sequence.sub Prims.l_Forall Prims.nat Prims.l_or Prims.b2t Prims.op_LessThanOrEqual Prims.op_LessThan Prims.op_Addition FStar.Seq.Base.index Lib.Sequence.to_seq Lib.Sequence.index Lib.Sequence.update_sub Lib.IntTypes.uint_t FStar.Seq.Base.seq FStar.Seq.Base.create Lib.IntTypes.mk_int Prims.l_imp Lib.Sequence.create Lib.IntTypes.u8 Spec.Poly1305.poly1305_update FStar.Seq.Base.slice FStar.Mul.op_Star Prims.int Prims.op_Modulus Prims.op_Division Lib.Sequence.length
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 ->
val poly1305_padded:
    r_elem:Poly.felem
  -> text:bytes
  -> acc:Poly.felem ->
  Tot Poly.felem
r_elem: Spec.Poly1305.felem -> text: Lib.ByteSequence.bytes -> acc: Spec.Poly1305.felem
  -> Spec.Poly1305.felem