val keysized : a: QUIC.Spec.Crypto.ha -> l: Prims.nat -> Prims.logical
let keysized (a:ha) (l:nat) =
  l `HD.less_than_max_input_length` a /\ l + HD.block_length a < pow2 32
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)
} =
  AEAD.cipher_alg_of_supported_alg a

let cipher_keysize (a:ea) =
  Spec.Agile.Cipher.key_length (Spec.Agile.AEAD.cipher_alg_of_supported_alg a)
/
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
a: QUIC.Spec.Crypto.ha -> l: Prims.nat -> Prims.logical
QUIC.Spec.Crypto.ha Prims.nat Prims.l_and Prims.b2t Spec.Hash.Definitions.less_than_max_input_length Prims.op_LessThan Prims.op_Addition Spec.Hash.Definitions.block_length Prims.pow2 Prims.logical
let keysized (a: ha) (l: nat) =
  
l `HD.less_than_max_input_length` a /\ l + HD.block_length a < pow2 32