val iv_for_encrypt_decrypt_pre
      (a: ea)
      (siv dst: B.buffer Secret.uint8)
      (h: G.erased Spec.header {~(Spec.is_retry h)})
      (pn_len: PN.packet_number_length_t)
      (pn: PN.packet_number_t)
      (m: HS.mem)
    : GTot Type0
let iv_for_encrypt_decrypt_pre
  (a: ea)
  (siv: B.buffer Secret.uint8)
  (dst: B.buffer Secret.uint8)
  (h: G.erased Spec.header { ~ (Spec.is_retry h) })
  (pn_len: PN.packet_number_length_t)
  (pn: PN.packet_number_t)
  (m: HS.mem)
: GTot Type0
=
  let a' = SAEAD.cipher_alg_of_supported_alg a in
  B.all_disjoint [
    B.loc_buffer siv;
    B.loc_buffer dst;
  ] /\
  B.live m siv /\ B.length siv == 12 /\
  B.live m dst /\ B.length dst == 12 /\
  pn_len == Spec.pn_length h /\
  pn == Spec.packet_number h
val iv_for_encrypt_decrypt_pre
      (a: ea)
      (siv dst: B.buffer Secret.uint8)
      (h: G.erased Spec.header {~(Spec.is_retry h)})
      (pn_len: PN.packet_number_length_t)
      (pn: PN.packet_number_t)
      (m: HS.mem)
    : GTot Type0
let iv_for_encrypt_decrypt_pre
      (a: ea)
      (siv dst: B.buffer Secret.uint8)
      (h: G.erased Spec.header {~(Spec.is_retry h)})
      (pn_len: PN.packet_number_length_t)
      (pn: PN.packet_number_t)
      (m: HS.mem)
    : GTot Type0 =
let a' = SAEAD.cipher_alg_of_supported_alg a in
B.all_disjoint [B.loc_buffer siv; B.loc_buffer dst] /\ B.live m siv /\ B.length siv == 12 /\
B.live m dst /\ B.length dst == 12 /\ pn_len == Spec.pn_length h /\ pn == Spec.packet_number h
QUIC.Impl.fst.checked
Spec.Agile.HKDF.fsti.checked Spec.Agile.Cipher.fsti.checked Spec.Agile.AEAD.fsti.checked QUIC.Spec.Header.Parse.fsti.checked QUIC.Spec.Header.fsti.checked QUIC.Spec.fst.checked QUIC.Secret.Seq.fsti.checked QUIC.Secret.Buffer.fsti.checked QUIC.Impl.Lemmas.fsti.checked QUIC.Impl.Header.Parse.fsti.checked QUIC.Impl.Header.Base.fst.checked QUIC.Impl.Header.fsti.checked prims.fst.checked LowStar.ImmutableBuffer.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.RawIntTypes.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Endianness.fsti.checked EverCrypt.HKDF.fsti.checked EverCrypt.Helpers.fsti.checked EverCrypt.Error.fsti.checked EverCrypt.CTR.fsti.checked EverCrypt.Cipher.fsti.checked EverCrypt.AEAD.fsti.checked
QUIC.Impl.fst
QUIC.Spec.Crypto.ea LowStar.Buffer.buffer Lib.IntTypes.uint8 FStar.Ghost.erased QUIC.Spec.Header.Base.header Prims.l_not Prims.b2t QUIC.Spec.Header.Base.is_retry FStar.Ghost.reveal QUIC.Spec.PacketNumber.Base.packet_number_length_t QUIC.Spec.PacketNumber.Base.packet_number_t FStar.Monotonic.HyperStack.mem Prims.l_and LowStar.Monotonic.Buffer.all_disjoint Prims.Cons LowStar.Monotonic.Buffer.loc LowStar.Monotonic.Buffer.loc_buffer LowStar.Buffer.trivial_preorder Prims.Nil LowStar.Monotonic.Buffer.live Prims.eq2 Prims.int LowStar.Monotonic.Buffer.length QUIC.Spec.Header.Base.pn_length QUIC.Spec.Header.Base.packet_number Spec.Agile.Cipher.cipher_alg Spec.Agile.AEAD.cipher_alg_of_supported_alg
module QUIC.Impl

// This MUST be kept in sync with QUIC.Impl.fsti...
module G = FStar.Ghost
module B = LowStar.Buffer
module IB = LowStar.ImmutableBuffer
module Seq = QUIC.Secret.Seq
module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST
module HST = FStar.HyperStack.ST

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

open FStar.HyperStack
open FStar.HyperStack.ST

open EverCrypt.Helpers
open EverCrypt.Error

module Cipher = EverCrypt.Cipher
module AEAD = EverCrypt.AEAD
module HKDF = EverCrypt.HKDF
module CTR = EverCrypt.CTR

friend QUIC.Spec

open QUIC.Impl.Lemmas

open LowStar.BufferOps

//module HeaderS = QUIC.Spec.Header
//module HeaderI = QUIC.Impl.Header

#set-options "--z3rlimit 64 --query_stats"

#restart-solver

module SAEAD = Spec.Agile.AEAD
module SCipher = Spec.Agile.Cipher
module SHKDF = Spec.Agile.HKDF

module SecretBuffer = QUIC.Secret.Buffer


(* There are a few places where EverCrypt needs public data whereas it
could/should be secret. Thus, we may need some declassification
locally using Lib.RawIntTypes, but we definitely don't want to make
secret integers globally transparent using friend *)

module ADMITDeclassify = Lib.RawIntTypes

unfold
let iv_for_encrypt_decrypt_pre
  (a: ea)
  (siv: B.buffer Secret.uint8)
  (dst: B.buffer Secret.uint8)
  (h: G.erased Spec.header { ~ (Spec.is_retry h) })
  (pn_len: PN.packet_number_length_t)
  (pn: PN.packet_number_t)
  (m: HS.mem)
val iv_for_encrypt_decrypt_pre
      (a: ea)
      (siv dst: B.buffer Secret.uint8)
      (h: G.erased Spec.header {~(Spec.is_retry h)})
      (pn_len: PN.packet_number_length_t)
      (pn: PN.packet_number_t)
      (m: HS.mem)
    : GTot Type0

    a: QUIC.Spec.Crypto.ea ->
    siv: LowStar.Buffer.buffer Lib.IntTypes.uint8 ->
    dst: LowStar.Buffer.buffer Lib.IntTypes.uint8 ->
    h:
      FStar.Ghost.erased QUIC.Spec.Header.Base.header
        {~(QUIC.Spec.Header.Base.is_retry (FStar.Ghost.reveal h))} ->
    pn_len: QUIC.Spec.PacketNumber.Base.packet_number_length_t ->
    pn: QUIC.Spec.PacketNumber.Base.packet_number_t ->
    m: FStar.Monotonic.HyperStack.mem
  -> Prims.GTot Type0