val max_cipher_length:n:
nat
  { forall a. {:pattern AEAD.max_length a\/AEAD.tag_length a}
      n <= AEAD.max_length a + AEAD.tag_length a }
let max_cipher_length : n:nat {
  forall a. {:pattern AEAD.max_length a \/ AEAD.tag_length a }
    n <= AEAD.max_length a + AEAD.tag_length a
} =
  pow2 32 - header_len_bound
val max_cipher_length:n:
nat
  { forall a. {:pattern AEAD.max_length a\/AEAD.tag_length a}
      n <= AEAD.max_length a + AEAD.tag_length a }
let max_cipher_length:n:
nat
  { forall a. {:pattern AEAD.max_length a\/AEAD.tag_length a}
      n <= AEAD.max_length a + AEAD.tag_length a } =
pow2 32 - header_len_bound
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
Prims.op_Subtraction Prims.pow2 QUIC.Spec.Base.header_len_bound
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)

// Move from Hashing.Spec to Spec.Hash?
let keysized (a:ha) (l:nat) =
  l `HD.less_than_max_input_length` a /\ l + HD.block_length a < pow2 32
let hashable (a:ha) (l:nat) = l `HD.less_than_max_input_length` a

// AEAD plain and ciphertext. We want to guarantee that regardless
// of the header size (max is 54), the neader + ciphertext + tag fits in a buffer
// : perhaps cleaner with a separate lemma; any reason for putting this in a refinement?
let max_plain_length: n:nat {
  forall a. {:pattern AEAD.max_length a} n <= AEAD.max_length a
} =
  pow2 32 - header_len_bound - 16

let max_cipher_length : n:nat {
  forall a. {:pattern AEAD.max_length a \/ AEAD.tag_length a }
    n <= AEAD.max_length a + AEAD.tag_length a
val max_cipher_length:n:
nat
  { forall a. {:pattern AEAD.max_length a\/AEAD.tag_length a}
      n <= AEAD.max_length a + AEAD.tag_length a }
n:
Prims.nat
  { forall (a: Spec.Agile.AEAD.alg{Spec.Agile.AEAD.is_supported_alg a}).
      {:pattern Spec.Agile.AEAD.max_length a\/Spec.Agile.AEAD.tag_length a}
      n <= Spec.Agile.AEAD.max_length a + Spec.Agile.AEAD.tag_length a }