val create_in_core:
  i:index ->
  r:HS.rid ->
  dst: B.pointer (B.pointer_or_null (state_s i)) ->
  initial_pn:PN.packet_number_t ->
  traffic_secret:B.buffer Secret.uint8 {
    B.length traffic_secret = Spec.Hash.Definitions.hash_length i.hash_alg
  } ->
  aead_state:AEAD.state i.aead_alg ->
  ctr_state:CTR.state (as_cipher_alg i.aead_alg) ->
  HST.ST unit
    (requires fun h0 ->
      Lemmas.hash_is_keysized_ i.hash_alg; (
      HST.is_eternal_region r /\
      B.live h0 dst /\ B.live h0 traffic_secret /\
      B.(all_disjoint [ AEAD.footprint h0 aead_state; CTR.footprint h0 ctr_state;
        loc_buffer dst; loc_buffer traffic_secret ]) /\
      B.(loc_includes (loc_region_only true r) (AEAD.footprint h0 aead_state)) /\
      B.(loc_includes (loc_region_only true r) (CTR.footprint h0 ctr_state)) /\

      // Whatever from the invariant ought to be established already.
      AEAD.invariant h0 aead_state /\
      not (B.g_is_null aead_state) /\
      CTR.invariant h0 ctr_state /\
      not (B.g_is_null ctr_state) /\
      AEAD.as_kv (B.deref h0 aead_state) ==
        QUIC.Spec.(derive_secret i.hash_alg (B.as_seq h0 traffic_secret) label_key
          (Spec.Agile.AEAD.key_length i.aead_alg))))
    (ensures (fun h0 _ h1 ->
      let s = B.deref h1 dst in
      not (B.g_is_null s) /\
      invariant h1 s /\

      B.(modifies (loc_buffer dst) h0 h1) /\ (
      let State _ _ _ initial_pn' aead_state' iv' hp_key' pn' ctr_state' = B.deref h1 s in
      aead_state' == aead_state /\
      ctr_state' == ctr_state /\
      B.(fresh_loc (loc_buffer iv') h0 h1) /\
      B.(fresh_loc (loc_buffer hp_key') h0 h1) /\
      B.(fresh_loc (loc_buffer pn') h0 h1) /\
      B.(fresh_loc (loc_addr_of_buffer s) h0 h1) /\

      g_traffic_secret (B.deref h1 s) == B.as_seq h0 traffic_secret /\ 
      g_last_packet_number (B.deref h1 s) h1 == initial_pn /\

      G.reveal initial_pn' == initial_pn)))
let create_in_core i r dst initial_pn traffic_secret aead_state ctr_state =
  LowStar.ImmutableBuffer.recall Impl.label_key;
  LowStar.ImmutableBuffer.recall_contents Impl.label_key Spec.label_key;
  LowStar.ImmutableBuffer.recall Impl.label_iv;
  LowStar.ImmutableBuffer.recall_contents Impl.label_iv Spec.label_iv;
  LowStar.ImmutableBuffer.recall Impl.label_hp;
  LowStar.ImmutableBuffer.recall_contents Impl.label_hp Spec.label_hp;

  (**) let h0 = HST.get () in
  (**) assert_norm FStar.Mul.(8 * 12 <= pow2 64 - 1);

  // The modifies clauses that we will transitively carry across this function body.
  let mloc = G.hide (B.(loc_buffer dst `loc_union` loc_unused_in h0)) in
  let e_traffic_secret: G.erased (Spec.Hash.Definitions.bytes_hash i.hash_alg) =
    G.hide (B.as_seq h0 traffic_secret) in
  let e_initial_pn: G.erased PN.packet_number_t = G.hide (initial_pn) in

  let iv = B.malloc r (Secret.to_u8 0uy) 12ul in
  let hp_key = B.malloc r (Secret.to_u8 0uy) (key_len32 i.aead_alg) in
  let pn = B.malloc r initial_pn 1ul in
  (**) let h1 = HST.get () in
  (**) B.(modifies_loc_includes (G.reveal mloc) h0 h1 loc_none);
  (**) assert (B.length hp_key = QUIC.Spec.cipher_keysize i.aead_alg);

  let s: state_s i = State #i
    i.hash_alg i.aead_alg e_traffic_secret e_initial_pn
    aead_state iv hp_key pn ctr_state
  in

  let s:B.pointer_or_null (state_s i) = B.malloc r s 1ul in
  (**) let h2 = HST.get () in
  (**) B.(modifies_loc_includes (G.reveal mloc) h1 h2 loc_none);
  (**) B.(modifies_trans (G.reveal mloc) h0 h1 (G.reveal mloc) h2);

  Impl.derive_secret i.hash_alg iv 12uy traffic_secret Impl.label_iv 2uy;
  (**) let h3 = HST.get () in
  (**) B.(modifies_loc_includes (G.reveal mloc) h2 h3 (loc_buffer iv));
  (**) B.(modifies_trans (G.reveal mloc) h0 h2 (G.reveal mloc) h3);

  Impl.derive_secret i.hash_alg hp_key (key_len i.aead_alg) traffic_secret Impl.label_hp 2uy;
  (**) let h4 = HST.get () in
  (**) B.(modifies_loc_includes (G.reveal mloc) h3 h4 (loc_buffer hp_key));
  (**) B.(modifies_trans (G.reveal mloc) h0 h3 (G.reveal mloc) h4);

  dst *= s;
  (**) let h5 = HST.get () in
  (**) B.(modifies_loc_includes (G.reveal mloc) h4 h5 (loc_buffer dst));
  (**) B.(modifies_trans (G.reveal mloc) h0 h4 (G.reveal mloc) h5);
  (**) B.(modifies_only_not_unused_in (loc_buffer dst) h0 h5)
val create_in_core:
  i:index ->
  r:HS.rid ->
  dst: B.pointer (B.pointer_or_null (state_s i)) ->
  initial_pn:PN.packet_number_t ->
  traffic_secret:B.buffer Secret.uint8 {
    B.length traffic_secret = Spec.Hash.Definitions.hash_length i.hash_alg
  } ->
  aead_state:AEAD.state i.aead_alg ->
  ctr_state:CTR.state (as_cipher_alg i.aead_alg) ->
  HST.ST unit
    (requires fun h0 ->
      Lemmas.hash_is_keysized_ i.hash_alg; (
      HST.is_eternal_region r /\
      B.live h0 dst /\ B.live h0 traffic_secret /\
      B.(all_disjoint [ AEAD.footprint h0 aead_state; CTR.footprint h0 ctr_state;
        loc_buffer dst; loc_buffer traffic_secret ]) /\
      B.(loc_includes (loc_region_only true r) (AEAD.footprint h0 aead_state)) /\
      B.(loc_includes (loc_region_only true r) (CTR.footprint h0 ctr_state)) /\

      // Whatever from the invariant ought to be established already.
      AEAD.invariant h0 aead_state /\
      not (B.g_is_null aead_state) /\
      CTR.invariant h0 ctr_state /\
      not (B.g_is_null ctr_state) /\
      AEAD.as_kv (B.deref h0 aead_state) ==
        QUIC.Spec.(derive_secret i.hash_alg (B.as_seq h0 traffic_secret) label_key
          (Spec.Agile.AEAD.key_length i.aead_alg))))
    (ensures (fun h0 _ h1 ->
      let s = B.deref h1 dst in
      not (B.g_is_null s) /\
      invariant h1 s /\

      B.(modifies (loc_buffer dst) h0 h1) /\ (
      let State _ _ _ initial_pn' aead_state' iv' hp_key' pn' ctr_state' = B.deref h1 s in
      aead_state' == aead_state /\
      ctr_state' == ctr_state /\
      B.(fresh_loc (loc_buffer iv') h0 h1) /\
      B.(fresh_loc (loc_buffer hp_key') h0 h1) /\
      B.(fresh_loc (loc_buffer pn') h0 h1) /\
      B.(fresh_loc (loc_addr_of_buffer s) h0 h1) /\

      g_traffic_secret (B.deref h1 s) == B.as_seq h0 traffic_secret /\ 
      g_last_packet_number (B.deref h1 s) h1 == initial_pn /\

      G.reveal initial_pn' == initial_pn)))
let create_in_core i r dst initial_pn traffic_secret aead_state ctr_state =
LowStar.ImmutableBuffer.recall Impl.label_key;
LowStar.ImmutableBuffer.recall_contents Impl.label_key Spec.label_key;
LowStar.ImmutableBuffer.recall Impl.label_iv;
LowStar.ImmutableBuffer.recall_contents Impl.label_iv Spec.label_iv;
LowStar.ImmutableBuffer.recall Impl.label_hp;
LowStar.ImmutableBuffer.recall_contents Impl.label_hp Spec.label_hp;
let h0 = HST.get () in
assert_norm FStar.Mul.(8 * 12 <= pow2 64 - 1);
let mloc = G.hide (let open B in (loc_buffer dst) `loc_union` (loc_unused_in h0)) in
let e_traffic_secret:G.erased (Spec.Hash.Definitions.bytes_hash i.hash_alg) =
  G.hide (B.as_seq h0 traffic_secret)
in
let e_initial_pn:G.erased PN.packet_number_t = G.hide (initial_pn) in
let iv = B.malloc r (Secret.to_u8 0uy) 12ul in
let hp_key = B.malloc r (Secret.to_u8 0uy) (key_len32 i.aead_alg) in
let pn = B.malloc r initial_pn 1ul in
let h1 = HST.get () in
(let open B in modifies_loc_includes (G.reveal mloc) h0 h1 loc_none);
assert (B.length hp_key = QUIC.Spec.cipher_keysize i.aead_alg);
let s:state_s i =
  State #i i.hash_alg i.aead_alg e_traffic_secret e_initial_pn aead_state iv hp_key pn ctr_state
in
let s:B.pointer_or_null (state_s i) = B.malloc r s 1ul in
let h2 = HST.get () in
(let open B in modifies_loc_includes (G.reveal mloc) h1 h2 loc_none);
(let open B in modifies_trans (G.reveal mloc) h0 h1 (G.reveal mloc) h2);
Impl.derive_secret i.hash_alg iv 12uy traffic_secret Impl.label_iv 2uy;
let h3 = HST.get () in
(let open B in modifies_loc_includes (G.reveal mloc) h2 h3 (loc_buffer iv));
(let open B in modifies_trans (G.reveal mloc) h0 h2 (G.reveal mloc) h3);
Impl.derive_secret i.hash_alg hp_key (key_len i.aead_alg) traffic_secret Impl.label_hp 2uy;
let h4 = HST.get () in
(let open B in modifies_loc_includes (G.reveal mloc) h3 h4 (loc_buffer hp_key));
(let open B in modifies_trans (G.reveal mloc) h0 h3 (G.reveal mloc) h4);
dst *= s;
let h5 = HST.get () in
(let open B in modifies_loc_includes (G.reveal mloc) h4 h5 (loc_buffer dst));
(let open B in modifies_trans (G.reveal mloc) h0 h4 (G.reveal mloc) h5);
let open B in modifies_only_not_unused_in (loc_buffer dst) h0 h5
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 FStar.Monotonic.HyperHeap.rid LowStar.Buffer.pointer LowStar.Buffer.pointer_or_null QUIC.State.state_s QUIC.Spec.PacketNumber.Base.packet_number_t LowStar.Buffer.buffer Lib.IntTypes.uint8 Prims.b2t Prims.op_Equality Prims.nat LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder Spec.Hash.Definitions.hash_length QUIC.State.__proj__Mkindex__item__hash_alg EverCrypt.AEAD.state QUIC.State.__proj__Mkindex__item__aead_alg NotEverCrypt.CTR.state QUIC.Spec.Crypto.as_cipher_alg LowStar.Monotonic.Buffer.modifies_only_not_unused_in LowStar.Monotonic.Buffer.loc_buffer Prims.unit LowStar.Monotonic.Buffer.modifies_trans FStar.Ghost.reveal LowStar.Monotonic.Buffer.loc LowStar.Monotonic.Buffer.modifies_loc_includes FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get LowStar.BufferOps.op_Star_Equals QUIC.Impl.Crypto.derive_secret QUIC.State.key_len QUIC.Impl.Crypto.label_hp FStar.UInt8.__uint_to_t Spec.Agile.AEAD.uint8 QUIC.Impl.Crypto.label_iv LowStar.Monotonic.Buffer.loc_none LowStar.Buffer.malloc FStar.UInt32.__uint_to_t LowStar.Monotonic.Buffer.mbuffer Prims.l_and Prims.eq2 FStar.UInt32.v Prims.op_Negation LowStar.Monotonic.Buffer.g_is_null LowStar.Monotonic.Buffer.frameOf LowStar.Monotonic.Buffer.freeable QUIC.State.State Prims._assert QUIC.Spec.Crypto.cipher_keysize FStar.UInt32.uint_to_t FStar.UInt32.t Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC QUIC.State.key_len32 Lib.IntTypes.to_u8 Lib.IntTypes.U1 Lib.IntTypes.PUB FStar.Ghost.erased FStar.Ghost.hide Spec.Hash.Definitions.bytes_hash LowStar.Monotonic.Buffer.as_seq LowStar.Monotonic.Buffer.loc_union LowStar.Monotonic.Buffer.loc_unused_in FStar.Pervasives.assert_norm Prims.op_LessThanOrEqual FStar.Mul.op_Star Prims.op_Subtraction Prims.pow2 LowStar.ImmutableBuffer.recall_contents FStar.UInt8.t QUIC.Spec.Crypto.label_hp LowStar.Monotonic.Buffer.recall LowStar.ImmutableBuffer.immutable_preorder QUIC.Spec.Crypto.label_iv QUIC.Impl.Crypto.label_key QUIC.Spec.Crypto.label_key
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)

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

let aead_alg_of_state #i s =
  let State _ the_aead_alg _ _ _ _ _ _ _ = !*s in
  the_aead_alg

let hash_alg_of_state #i s =
  let open FStar.HyperStack.ST in (* for the !* notation *)
  let State the_hash_alg _ _ _ _ _ _ _ _ = !*s in
  the_hash_alg

let last_packet_number_of_state #i s =
  let State _ _ _ _ _ _ _ pn _ = !*s in
  !*pn


/// For functions that perform allocations, or even functions that need
/// temporary state, a style we adopt here is to write the core (i.e. what would
/// normally go in-between push and pop frame) as a separate function. If
/// needed, the core of the function takes its temporary allocations as
/// parameters, and reasons abstractly against a region where the temporary
/// allocations live. This gives significantly better proof performance.
///
/// Another bit of style: after every stateful operation, we restore manually:
/// the modifies clause (going directly for the one we want); the invariant; the
/// footprint preservation; then the functional correctness propertise we are
/// seeking.

val create_in_core:
  i:index ->
  r:HS.rid ->
  dst: B.pointer (B.pointer_or_null (state_s i)) ->
  initial_pn:PN.packet_number_t ->
  traffic_secret:B.buffer Secret.uint8 {
    B.length traffic_secret = Spec.Hash.Definitions.hash_length i.hash_alg
  } ->
  aead_state:AEAD.state i.aead_alg ->
  ctr_state:CTR.state (as_cipher_alg i.aead_alg) ->
  HST.ST unit
    (requires fun h0 ->
      Lemmas.hash_is_keysized_ i.hash_alg; (
      HST.is_eternal_region r /\
      B.live h0 dst /\ B.live h0 traffic_secret /\
      B.(all_disjoint [ AEAD.footprint h0 aead_state; CTR.footprint h0 ctr_state;
        loc_buffer dst; loc_buffer traffic_secret ]) /\
      B.(loc_includes (loc_region_only true r) (AEAD.footprint h0 aead_state)) /\
      B.(loc_includes (loc_region_only true r) (CTR.footprint h0 ctr_state)) /\

      // Whatever from the invariant ought to be established already.
      AEAD.invariant h0 aead_state /\
      not (B.g_is_null aead_state) /\
      CTR.invariant h0 ctr_state /\
      not (B.g_is_null ctr_state) /\
      AEAD.as_kv (B.deref h0 aead_state) ==
        QUIC.Spec.(derive_secret i.hash_alg (B.as_seq h0 traffic_secret) label_key
          (Spec.Agile.AEAD.key_length i.aead_alg))))
    (ensures (fun h0 _ h1 ->
      let s = B.deref h1 dst in
      not (B.g_is_null s) /\
      invariant h1 s /\

      B.(modifies (loc_buffer dst) h0 h1) /\ (
      let State _ _ _ initial_pn' aead_state' iv' hp_key' pn' ctr_state' = B.deref h1 s in
      aead_state' == aead_state /\
      ctr_state' == ctr_state /\
      B.(fresh_loc (loc_buffer iv') h0 h1) /\
      B.(fresh_loc (loc_buffer hp_key') h0 h1) /\
      B.(fresh_loc (loc_buffer pn') h0 h1) /\
      B.(fresh_loc (loc_addr_of_buffer s) h0 h1) /\

      g_traffic_secret (B.deref h1 s) == B.as_seq h0 traffic_secret /\ 
      g_last_packet_number (B.deref h1 s) h1 == initial_pn /\

      G.reveal initial_pn' == initial_pn)))

#push-options "--z3rlimit 50"
val create_in_core:
  i:index ->
  r:HS.rid ->
  dst: B.pointer (B.pointer_or_null (state_s i)) ->
  initial_pn:PN.packet_number_t ->
  traffic_secret:B.buffer Secret.uint8 {
    B.length traffic_secret = Spec.Hash.Definitions.hash_length i.hash_alg
  } ->
  aead_state:AEAD.state i.aead_alg ->
  ctr_state:CTR.state (as_cipher_alg i.aead_alg) ->
  HST.ST unit
    (requires fun h0 ->
      Lemmas.hash_is_keysized_ i.hash_alg; (
      HST.is_eternal_region r /\
      B.live h0 dst /\ B.live h0 traffic_secret /\
      B.(all_disjoint [ AEAD.footprint h0 aead_state; CTR.footprint h0 ctr_state;
        loc_buffer dst; loc_buffer traffic_secret ]) /\
      B.(loc_includes (loc_region_only true r) (AEAD.footprint h0 aead_state)) /\
      B.(loc_includes (loc_region_only true r) (CTR.footprint h0 ctr_state)) /\

      // Whatever from the invariant ought to be established already.
      AEAD.invariant h0 aead_state /\
      not (B.g_is_null aead_state) /\
      CTR.invariant h0 ctr_state /\
      not (B.g_is_null ctr_state) /\
      AEAD.as_kv (B.deref h0 aead_state) ==
        QUIC.Spec.(derive_secret i.hash_alg (B.as_seq h0 traffic_secret) label_key
          (Spec.Agile.AEAD.key_length i.aead_alg))))
    (ensures (fun h0 _ h1 ->
      let s = B.deref h1 dst in
      not (B.g_is_null s) /\
      invariant h1 s /\

      B.(modifies (loc_buffer dst) h0 h1) /\ (
      let State _ _ _ initial_pn' aead_state' iv' hp_key' pn' ctr_state' = B.deref h1 s in
      aead_state' == aead_state /\
      ctr_state' == ctr_state /\
      B.(fresh_loc (loc_buffer iv') h0 h1) /\
      B.(fresh_loc (loc_buffer hp_key') h0 h1) /\
      B.(fresh_loc (loc_buffer pn') h0 h1) /\
      B.(fresh_loc (loc_addr_of_buffer s) h0 h1) /\

      g_traffic_secret (B.deref h1 s) == B.as_seq h0 traffic_secret /\ 
      g_last_packet_number (B.deref h1 s) h1 == initial_pn /\

      G.reveal initial_pn' == initial_pn)))

    i: QUIC.State.index ->
    r: FStar.Monotonic.HyperHeap.rid ->
    dst: LowStar.Buffer.pointer (LowStar.Buffer.pointer_or_null (QUIC.State.state_s i)) ->
    initial_pn: QUIC.Spec.PacketNumber.Base.packet_number_t ->
    traffic_secret:
      LowStar.Buffer.buffer Lib.IntTypes.uint8
        { LowStar.Monotonic.Buffer.length traffic_secret =
          Spec.Hash.Definitions.hash_length (Mkindex?.hash_alg i) } ->
    aead_state: EverCrypt.AEAD.state (Mkindex?.aead_alg i) ->
    ctr_state: NotEverCrypt.CTR.state (QUIC.Spec.Crypto.as_cipher_alg (Mkindex?.aead_alg i))
  -> FStar.HyperStack.ST.ST Prims.unit