let is_supported_aead = function
  | AE.AES128_GCM | AE.AES256_GCM | AE.CHACHA20_POLY1305 -> true
  | _ -> false
let is_supported_aead =
function
| AE.AES128_GCM | AE.AES256_GCM | AE.CHACHA20_POLY1305 -> true
| _ -> false
Model.Indexing.fsti.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.Cipher.fsti.checked Spec.Agile.AEAD.fsti.checked prims.fst.checked Model.Flags.fsti.checked Mem.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Model.Indexing.fsti
Spec.Agile.AEAD.alg Prims.bool
module Model.Indexing

(*
This module provides the functions that the QUIC
record layer security model expect to be provided
by the TLS handshake security model. In particular,
it assumes that the indexes contain the history of
the derivation of each key, including the implicit
authentication of algorithms to use.
*)

open Mem
include Model.Flags

module C = Spec.Agile.Cipher
module AE = Spec.Agile.AEAD
module HD = Spec.Hash.Definitions
module G = FStar.Ghost

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