val as_cipher_alg (a: ea)
    : a: Cipher.cipher_alg{let open Cipher in a == AES128 \/ a == AES256 \/ a == CHACHA20}
let as_cipher_alg (a: ea): a:Cipher.cipher_alg {
  Cipher.(a == AES128 \/ a == AES256 \/ a == CHACHA20)
} =
  AEAD.cipher_alg_of_supported_alg a
val as_cipher_alg (a: ea)
    : a: Cipher.cipher_alg{let open Cipher in a == AES128 \/ a == AES256 \/ a == CHACHA20}
let as_cipher_alg (a: ea)
    : a: Cipher.cipher_alg{let open Cipher in a == AES128 \/ a == AES256 \/ a == CHACHA20} =
AEAD.cipher_alg_of_supported_alg a
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
QUIC.Spec.Crypto.ea Spec.Agile.AEAD.cipher_alg_of_supported_alg Spec.Agile.Cipher.cipher_alg Prims.l_or Prims.eq2 Spec.Agile.Cipher.AES128 Spec.Agile.Cipher.AES256 Spec.Agile.Cipher.CHACHA20
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

let supported_aead = function
  | AEAD.AES128_GCM | AEAD.AES256_GCM | AEAD.CHACHA20_POLY1305 -> true
  | _ -> false

type ha = a:HD.hash_alg{supported_hash a}
type ea = a:AEAD.alg{supported_aead a}


inline_for_extraction noextract
let as_cipher_alg (a: ea): a:Cipher.cipher_alg {
  Cipher.(a == AES128 \/ a == AES256 \/ a == CHACHA20)
val as_cipher_alg (a: ea)
    : a: Cipher.cipher_alg{let open Cipher in a == AES128 \/ a == AES256 \/ a == CHACHA20}
a: QUIC.Spec.Crypto.ea
  -> a:
    Spec.Agile.Cipher.cipher_alg
      { a == Spec.Agile.Cipher.AES128 \/ a == Spec.Agile.Cipher.AES256 \/
        a == Spec.Agile.Cipher.CHACHA20 }