val is_supported_hash : _: Spec.Hash.Definitions.hash_alg -> Prims.bool
let is_supported_hash = function
  | HD.SHA1 | HD.SHA2_256 | HD.SHA2_384 | HD.SHA2_512 -> true
  | _ -> false
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
/
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.Hash.Definitions.hash_alg -> Prims.bool
Spec.Hash.Definitions.hash_alg Prims.bool
let is_supported_hash =
  
function
| HD.SHA1 | HD.SHA2_256 | HD.SHA2_384 | HD.SHA2_512 -> true
| _ -> false