val g_traffic_secret: #i:index -> (s: state_s i) ->
  GTot (Spec.Hash.Definitions.bytes_hash i.hash_alg)
let g_traffic_secret #i s =
  // Automatic reveal insertion doesn't work here
  G.reveal (State?.traffic_secret s)
val g_traffic_secret: #i:index -> (s: state_s i) ->
  GTot (Spec.Hash.Definitions.bytes_hash i.hash_alg)
let g_traffic_secret #i s =
G.reveal (State?.traffic_secret s)
QUIC.State.fst.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.HKDF.fsti.checked Spec.Agile.Hash.fsti.checked Spec.Agile.AEAD.fsti.checked QUIC.Spec.fsti.checked QUIC.Secret.Seq.fsti.checked QUIC.Secret.Buffer.fsti.checked QUIC.Impl.Lemmas.fsti.checked QUIC.Impl.fsti.checked prims.fst.checked LowStar.ImmutableBuffer.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked EverCrypt.HKDF.fsti.checked EverCrypt.CTR.fsti.checked EverCrypt.Cipher.fsti.checked EverCrypt.AEAD.fsti.checked
QUIC.State.fst
QUIC.State.index QUIC.State.state_s FStar.Ghost.reveal Spec.Hash.Definitions.bytes_hash QUIC.State.__proj__State__item__the_hash_alg QUIC.State.__proj__State__item__traffic_secret QUIC.State.__proj__Mkindex__item__hash_alg
module QUIC.State

module Cipher = EverCrypt.Cipher
module AEAD = EverCrypt.AEAD
module HKDF = EverCrypt.HKDF
module CTR = EverCrypt.CTR
module IB = LowStar.ImmutableBuffer
module U32 = FStar.UInt32

module Seq = QUIC.Secret.Seq
module SecretBuffer = QUIC.Secret.Buffer

module SHKDF = Spec.Agile.HKDF
module SHD = Spec.Hash.Definitions

open LowStar.BufferOps (* for the !* notation *)

module Spec = QUIC.Spec
module Impl = QUIC.Impl
module Lemmas = QUIC.Impl.Lemmas


/// Helpers
/// -------

let key_len (a: ea): x:U8.t { U8.v x = Spec.Agile.AEAD.key_length a } =
  let open Spec.Agile.AEAD in
  match a with
  | AES128_GCM -> 16uy
  | AES256_GCM -> 32uy
  | CHACHA20_POLY1305 -> 32uy

let key_len32 a = FStar.Int.Cast.uint8_to_uint32 (key_len a)


/// https://tools.ietf.org/html/draft-ietf-quic-tls-23#section-5
///
/// We perform the three key derivations (AEAD key; AEAD iv; header protection
/// key) when ``create`` is called. We thus store the original traffic secret
/// only ghostly.
///
/// We retain the AEAD state, in order to perform the packet payload encryption.
///
/// We retain the Cipher state, in order to compute the mask for header protection.
noeq
type state_s (i: index) =
  | State:
      the_hash_alg:ha { the_hash_alg == i.hash_alg } ->
      the_aead_alg:ea { the_aead_alg == i.aead_alg } ->
      traffic_secret:G.erased (Spec.Hash.Definitions.bytes_hash the_hash_alg) ->
      initial_pn:G.erased PN.packet_number_t ->
      aead_state:EverCrypt.AEAD.state the_aead_alg ->
      iv:EverCrypt.AEAD.iv_p the_aead_alg { B.length iv == 12 } ->
      hp_key:B.buffer Secret.uint8 { B.length hp_key = QUIC.Spec.cipher_keysize the_aead_alg } ->
      pn:B.pointer PN.packet_number_t ->
      ctr_state:CTR.state (as_cipher_alg the_aead_alg) ->
      state_s i

let footprint_s #i h s =
  let open LowStar.Buffer in
  AEAD.footprint h (State?.aead_state s) `loc_union`
  CTR.footprint h (State?.ctr_state s) `loc_union`
  loc_buffer (State?.iv s) `loc_union`
  loc_buffer (State?.hp_key s) `loc_union`
  loc_buffer (State?.pn s)

let g_traffic_secret #i s =
val g_traffic_secret: #i:index -> (s: state_s i) ->
  GTot (Spec.Hash.Definitions.bytes_hash i.hash_alg)
s: QUIC.State.state_s i -> Prims.GTot (Spec.Hash.Definitions.bytes_hash (Mkindex?.hash_alg i))