let supported_aead = function
  | AEAD.AES128_GCM | AEAD.AES256_GCM | AEAD.CHACHA20_POLY1305 -> true
  | _ -> false
let supported_aead =
function
| AEAD.AES128_GCM | AEAD.AES256_GCM | AEAD.CHACHA20_POLY1305 -> true
| _ -> false
QUIC.Spec.Crypto.fsti.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.Cipher.fsti.checked Spec.Agile.AEAD.fsti.checked QUIC.Spec.Base.fst.checked QUIC.Secret.Int.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
QUIC.Spec.Crypto.fsti
Spec.Agile.AEAD.alg Prims.bool
module QUIC.Spec.Crypto
include QUIC.Spec.Base

module Seq = FStar.Seq
module HD = Spec.Hash.Definitions
module AEAD = Spec.Agile.AEAD
module Secret = QUIC.Secret.Int
module Cipher = Spec.Agile.Cipher

let supported_hash = function
  | HD.SHA1 | HD.SHA2_256 | HD.SHA2_384 | HD.SHA2_512 -> true
  | _ -> false
val supported_aead : _: Spec.Agile.AEAD.alg -> Prims.bool
_: Spec.Agile.AEAD.alg -> Prims.bool