val frame_invariant: #i:index -> l:B.loc -> s:state i -> h0:HS.mem -> h1:HS.mem -> Lemma
  (requires (
    invariant h0 s /\
    B.loc_disjoint l (footprint h0 s) /\
    B.modifies l h0 h1))
  (ensures (
    invariant h1 s /\
    footprint h0 s == footprint h1 s /\
    g_last_packet_number (B.deref h0 s) h0 == g_last_packet_number (B.deref h1 s) h0 /\
    g_traffic_secret (B.deref h0 s) == g_traffic_secret (B.deref h1 s)
    ))
  // Assertion failure: unexpected pattern term
  [ SMTPatOr [
    [ SMTPat (B.modifies l h0 h1); SMTPat (invariant h1 s) ];
    [ SMTPat (B.modifies l h0 h1); SMTPat (footprint h1 s) ];
    [ SMTPat (B.modifies l h0 h1); SMTPat (g_last_packet_number (B.deref h1 s)) ];
    [ SMTPat (B.modifies l h0 h1); SMTPat (g_traffic_secret (B.deref h1 s)) ]
  ] ]
let frame_invariant #i l s h0 h1 =
  AEAD.frame_invariant l (State?.aead_state (B.deref h0 s)) h0 h1;
  CTR.frame_invariant l (State?.ctr_state (B.deref h0 s)) h0 h1
val frame_invariant: #i:index -> l:B.loc -> s:state i -> h0:HS.mem -> h1:HS.mem -> Lemma
  (requires (
    invariant h0 s /\
    B.loc_disjoint l (footprint h0 s) /\
    B.modifies l h0 h1))
  (ensures (
    invariant h1 s /\
    footprint h0 s == footprint h1 s /\
    g_last_packet_number (B.deref h0 s) h0 == g_last_packet_number (B.deref h1 s) h0 /\
    g_traffic_secret (B.deref h0 s) == g_traffic_secret (B.deref h1 s)
    ))
  // Assertion failure: unexpected pattern term
  [ SMTPatOr [
    [ SMTPat (B.modifies l h0 h1); SMTPat (invariant h1 s) ];
    [ SMTPat (B.modifies l h0 h1); SMTPat (footprint h1 s) ];
    [ SMTPat (B.modifies l h0 h1); SMTPat (g_last_packet_number (B.deref h1 s)) ];
    [ SMTPat (B.modifies l h0 h1); SMTPat (g_traffic_secret (B.deref h1 s)) ]
  ] ]
let frame_invariant #i l s h0 h1 =
AEAD.frame_invariant l (State?.aead_state (B.deref h0 s)) h0 h1;
CTR.frame_invariant l (State?.ctr_state (B.deref h0 s)) h0 h1
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 LowStar.Monotonic.Buffer.loc QUIC.State.state FStar.Monotonic.HyperStack.mem NotEverCrypt.CTR.frame_invariant QUIC.Spec.Crypto.as_cipher_alg QUIC.State.__proj__State__item__the_aead_alg LowStar.Monotonic.Buffer.deref QUIC.State.state_s LowStar.Buffer.trivial_preorder QUIC.State.__proj__State__item__ctr_state Prims.unit EverCrypt.AEAD.frame_invariant QUIC.State.__proj__State__item__aead_state
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 #_ _ _ = ()

let g_last_packet_number #i s h =
  B.deref h (State?.pn s)
val frame_invariant: #i:index -> l:B.loc -> s:state i -> h0:HS.mem -> h1:HS.mem -> Lemma
  (requires (
    invariant h0 s /\
    B.loc_disjoint l (footprint h0 s) /\
    B.modifies l h0 h1))
  (ensures (
    invariant h1 s /\
    footprint h0 s == footprint h1 s /\
    g_last_packet_number (B.deref h0 s) h0 == g_last_packet_number (B.deref h1 s) h0 /\
    g_traffic_secret (B.deref h0 s) == g_traffic_secret (B.deref h1 s)
    ))
  // Assertion failure: unexpected pattern term
  [ SMTPatOr [
    [ SMTPat (B.modifies l h0 h1); SMTPat (invariant h1 s) ];
    [ SMTPat (B.modifies l h0 h1); SMTPat (footprint h1 s) ];
    [ SMTPat (B.modifies l h0 h1); SMTPat (g_last_packet_number (B.deref h1 s)) ];
    [ SMTPat (B.modifies l h0 h1); SMTPat (g_traffic_secret (B.deref h1 s)) ]
  ] ]

    l: LowStar.Monotonic.Buffer.loc ->
    s: QUIC.State.state i ->
    h0: FStar.Monotonic.HyperStack.mem ->
    h1: FStar.Monotonic.HyperStack.mem
  -> FStar.Pervasives.Lemma
      (requires
        QUIC.State.invariant h0 s /\
        LowStar.Monotonic.Buffer.loc_disjoint l (QUIC.State.footprint h0 s) /\
        LowStar.Monotonic.Buffer.modifies l h0 h1)
      (ensures
        QUIC.State.invariant h1 s /\ QUIC.State.footprint h0 s == QUIC.State.footprint h1 s /\
        QUIC.State.g_last_packet_number (LowStar.Monotonic.Buffer.deref h0 s) h0 ==
        QUIC.State.g_last_packet_number (LowStar.Monotonic.Buffer.deref h1 s) h0 /\
        QUIC.State.g_traffic_secret (LowStar.Monotonic.Buffer.deref h0 s) ==
        QUIC.State.g_traffic_secret (LowStar.Monotonic.Buffer.deref h1 s))
      [
        SMTPatOr [
            [SMTPat (LowStar.Monotonic.Buffer.modifies l h0 h1); SMTPat (QUIC.State.invariant h1 s)];
            [SMTPat (LowStar.Monotonic.Buffer.modifies l h0 h1); SMTPat (QUIC.State.footprint h1 s)];
            [
              SMTPat (LowStar.Monotonic.Buffer.modifies l h0 h1);
              SMTPat (QUIC.State.g_last_packet_number (LowStar.Monotonic.Buffer.deref h1 s))
            ];
            [
              SMTPat (LowStar.Monotonic.Buffer.modifies l h0 h1);
              SMTPat (QUIC.State.g_traffic_secret (LowStar.Monotonic.Buffer.deref h1 s))
            ]
          ]
      ]