let iv_t (a: ea) = (x: AEAD.iv a { Seq.length x == 12 })
let iv_t (a: ea) =
(x: AEAD.iv a {Seq.length x == 12})
QUIC.Spec.fsti.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.Cipher.fsti.checked Spec.Agile.AEAD.fsti.checked QUIC.Spec.PacketNumber.Base.fst.checked QUIC.Spec.Header.Base.fst.checked QUIC.Spec.Crypto.fsti.checked QUIC.Secret.Int.fsti.checked prims.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
QUIC.Spec.fsti
QUIC.Spec.Crypto.ea Spec.Agile.AEAD.iv Prims.eq2 Prims.int FStar.Seq.Base.length Spec.Agile.AEAD.uint8
module QUIC.Spec

include QUIC.Spec.Header.Base
include QUIC.Spec.Crypto

module Seq = FStar.Seq
module HD = Spec.Hash.Definitions
module AEAD = Spec.Agile.AEAD
module Cipher = Spec.Agile.Cipher
module PN = QUIC.Spec.PacketNumber.Base
module Secret = QUIC.Secret.Int

noeq
type h_result =
| H_Success:
  h: header ->
  cipher: cbytes' (is_retry h) ->
  rem: bytes ->
  h_result
| H_Failure

// TODO: add a prefix lemma on header_decrypt, if ever useful

module U32 = FStar.UInt32
module U64 = FStar.UInt64


noeq
type result =
| Success: 
  h: header ->
  plain: bytes ->
  remainder: bytes ->
  result
| Failure
val iv_t : a: QUIC.Spec.Crypto.ea -> Type0
a: QUIC.Spec.Crypto.ea -> Type0