val g_last_packet_number: #i:index -> (s: state_s i) -> (h: HS.mem { invariant_s h s }) ->
  GTot (pn: PN.packet_number_t {
    Secret.v pn >= Secret.v (g_initial_packet_number s)
  })
let g_last_packet_number #i s h =
  B.deref h (State?.pn s)
val g_last_packet_number: #i:index -> (s: state_s i) -> (h: HS.mem { invariant_s h s }) ->
  GTot (pn: PN.packet_number_t {
    Secret.v pn >= Secret.v (g_initial_packet_number s)
  })
let g_last_packet_number #i s h =
B.deref h (State?.pn 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.Monotonic.HyperStack.mem QUIC.State.invariant_s LowStar.Monotonic.Buffer.deref QUIC.Spec.PacketNumber.Base.packet_number_t LowStar.Buffer.trivial_preorder QUIC.State.__proj__State__item__pn Prims.b2t Prims.op_GreaterThanOrEqual QUIC.Secret.Int.Base.v Lib.IntTypes.U64 Lib.IntTypes.SEC QUIC.State.g_initial_packet_number
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 =
  // Automatic reveal insertion doesn't work here
  G.reveal (State?.traffic_secret s)

let g_initial_packet_number #i s =
  // New style: automatic insertion of reveal
  State?.initial_pn s

let invariant_s #i h s =
  let open QUIC.Spec in
  let State hash_alg aead_alg traffic_secret initial_pn aead_state iv hp_key pn ctr_state =
    s in
  hash_is_keysized s; (
  AEAD.invariant h aead_state /\
  not (B.g_is_null aead_state) /\
  CTR.invariant h ctr_state /\
  not (B.g_is_null ctr_state) /\
  B.(all_live h [ buf iv; buf hp_key; buf pn ])  /\
  B.(all_disjoint [ CTR.footprint h ctr_state;
    AEAD.footprint h aead_state; loc_buffer iv; loc_buffer hp_key; loc_buffer pn ]) /\
  // : automatic insertion of reveal does not work here
  Secret.v initial_pn <= Secret.v (B.deref h pn) /\
  AEAD.as_kv (B.deref h aead_state) ==
    derive_secret i.hash_alg (G.reveal traffic_secret) label_key (Spec.Agile.AEAD.key_length aead_alg) /\
  (B.as_seq h iv) ==
    derive_secret i.hash_alg (G.reveal traffic_secret) label_iv 12 /\
  B.as_seq h hp_key ==
    derive_secret i.hash_alg (G.reveal traffic_secret) label_hp (QUIC.Spec.cipher_keysize aead_alg)
  )

let invariant_loc_in_footprint #_ _ _ = ()
val g_last_packet_number: #i:index -> (s: state_s i) -> (h: HS.mem { invariant_s h s }) ->
  GTot (pn: PN.packet_number_t {
    Secret.v pn >= Secret.v (g_initial_packet_number s)
  })
s: QUIC.State.state_s i -> h: FStar.Monotonic.HyperStack.mem{QUIC.State.invariant_s h s}
  -> Prims.GTot
    (pn:
      QUIC.Spec.PacketNumber.Base.packet_number_t
        {QUIC.Secret.Int.Base.v pn >= QUIC.Secret.Int.Base.v (QUIC.State.g_initial_packet_number s)}
    )