val cipher_of_aead : a: Model.Indexing.ea -> Spec.Agile.Cipher.cipher_alg
let cipher_of_aead (a:ea) =
  match a with
  | AE.AES128_GCM -> C.AES128
  | AE.AES256_GCM -> C.AES256
  | AE.CHACHA20_POLY1305 -> C.CHACHA20
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

let is_supported_aead = function
  | AE.AES128_GCM | AE.AES256_GCM | AE.CHACHA20_POLY1305 -> true
  | _ -> false

let is_supported_cipher = function
  | C.AES128 | C.AES256 | C.CHACHA20 -> true
  | _ -> false

type ha = a:HD.hash_alg{is_supported_hash a}
type ea = a:AE.alg{is_supported_aead a}
type ca = a:C.cipher_alg{is_supported_cipher a}
/
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
a: Model.Indexing.ea -> Spec.Agile.Cipher.cipher_alg
Model.Indexing.ea Spec.Agile.Cipher.AES128 Spec.Agile.Cipher.AES256 Spec.Agile.Cipher.CHACHA20 Spec.Agile.Cipher.cipher_alg
let cipher_of_aead (a: ea) =
  
match a with
| AE.AES128_GCM -> C.AES128
| AE.AES256_GCM -> C.AES256
| AE.CHACHA20_POLY1305 -> C.CHACHA20