val size_tag:size_nat
let size_tag : size_nat = size_block
val size_tag:size_nat
let size_tag:size_nat =
size_block
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.Chacha20Poly1305.size_block
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 *)
val size_tag:size_nat
n: Prims.nat{n <= Prims.pow2 32 - 1}