val payload_encrypt_post
      (a: ea)
      (s: AEAD.state a)
      (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)
      (header_len: Secret.uint32)
      (plain: B.buffer Secret.uint8)
      (plain_len: Secret.uint32)
      (m: HS.mem)
      (res: error_code)
      (m': HS.mem)
    : GTot Type0
val payload_encrypt_post
      (a: ea)
      (s: AEAD.state a)
      (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)
      (header_len: Secret.uint32)
      (plain: B.buffer Secret.uint8)
      (plain_len: Secret.uint32)
      (m: HS.mem)
      (res: error_code)
      (m': HS.mem)
    : GTot Type0
let payload_encrypt_post
  (a: ea)
  (s: AEAD.state a)
  (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)
  (header_len: Secret.uint32)
  (plain: B.buffer Secret.uint8)
  (plain_len: Secret.uint32)
  (m: HS.mem)
  (res: error_code)
  (m' : HS.mem)
: GTot Type0
=
  let fmt = SParse.format_header h in
  payload_encrypt_pre a s siv dst h pn_len pn header_len plain plain_len m /\
  B.modifies (B.loc_buffer (B.gsub dst (Secret.reveal header_len) (B.len dst ` U32.sub` Secret.reveal header_len)) `B.loc_union` AEAD.footprint m s) m m' /\
  AEAD.invariant m' s /\ AEAD.footprint m' s == AEAD.footprint m s /\
  AEAD.preserves_freeable s m m' /\
  AEAD.as_kv (B.deref m' s) == AEAD.as_kv (B.deref m s) /\
  B.as_seq m' (B.gsub dst (Secret.reveal header_len) (B.len dst `U32.sub` Secret.reveal header_len)) `Seq.equal` Seq.seq_hide (Spec.payload_encrypt a (AEAD.as_kv (B.deref m s)) (B.as_seq m siv) h (Seq.seq_reveal (B.as_seq m plain))) /\
  res == Success
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)
: 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

unfold
let iv_for_encrypt_decrypt_post
  (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)
  (m' : HS.mem)
: GTot Type0
=
  iv_for_encrypt_decrypt_pre a siv dst h pn_len pn m /\
  begin
    B.modifies (B.loc_buffer dst) m m' /\
    B.as_seq m' dst `Seq.equal`
      Spec.iv_for_encrypt_decrypt a (B.as_seq m siv) h
  end

let iv_for_encrypt_decrypt
  (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)
: HST.Stack unit
  (requires (fun m ->
    iv_for_encrypt_decrypt_pre a siv dst h pn_len pn m
  ))
  (ensures (fun m _ m' ->
    iv_for_encrypt_decrypt_post a siv dst h pn_len pn m m'
  ))
= let m0 = HST.get () in
  B.fill dst (Secret.to_u8 0uy) 12ul;
  let pnb_store = B.sub dst 4ul 8ul in
  SecretBuffer.store64_be pnb_store pn;
  let m2 = HST.get () in
  assert (Seq.seq_reveal (B.as_seq m2 (B.gsub dst 0ul 4ul)) `Seq.equal` Seq.create 4 0uy);
  assert (Seq.seq_reveal (B.as_seq m2 dst) `Seq.equal` (Seq.create 4 0uy `Seq.append` FStar.Endianness.n_to_be 8 (Secret.v pn)));
  QUIC.Impl.Lemmas.n_to_be_lower' 8 12 (Secret.v pn);
  assert (Seq.seq_reveal (B.as_seq m2 dst) == FStar.Endianness.n_to_be 12 (Secret.v pn));
  QUIC.Impl.Lemmas.op_inplace dst siv 12ul 0ul (Secret.logxor #Secret.U8 #Secret.SEC);
  QUIC.Impl.Lemmas.secret_xor_inplace_eq (B.as_seq m2 dst) (B.as_seq m2 siv) 0

module SParse = QUIC.Spec.Header.Parse

unfold
let payload_encrypt_pre
  (a: ea)
  (s: AEAD.state a)
  (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)
  (header_len: Secret.uint32)
  (plain: B.buffer Secret.uint8)
  (plain_len: Secret.uint32) // should be secret, because otherwise one can compute the packet number length
  (m: HS.mem)
: GTot Type0
=
  let fmt = SParse.format_header h in

  B.all_disjoint [
    AEAD.footprint m s;
    B.loc_buffer siv;
    B.loc_buffer dst;
    B.loc_buffer plain;
  ] /\

  AEAD.invariant m s /\
  B.live m siv /\ B.length siv == 12 /\
  Secret.v header_len == Seq.length fmt /\
  B.live m dst /\ B.length dst == Secret.v header_len + Secret.v plain_len + SAEAD.tag_length a /\
  pn_len == Spec.pn_length h /\
  pn == Spec.packet_number h /\
  B.live m plain /\ B.length plain == Secret.v plain_len /\ 3 <= Secret.v plain_len /\ Secret.v plain_len < max_plain_length /\
  B.as_seq m (B.gsub dst 0ul (Secret.reveal header_len)) `Seq.equal` Seq.seq_hide fmt
/
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

    a: QUIC.Spec.Crypto.ea ->
    s: EverCrypt.AEAD.state a ->
    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 ->
    header_len: Lib.IntTypes.uint32 ->
    plain: LowStar.Buffer.buffer Lib.IntTypes.uint8 ->
    plain_len: Lib.IntTypes.uint32 ->
    m: FStar.Monotonic.HyperStack.mem ->
    res: EverCrypt.Error.error_code ->
    m': FStar.Monotonic.HyperStack.mem
  -> Prims.GTot Type0
QUIC.Spec.Crypto.ea EverCrypt.AEAD.state 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 Lib.IntTypes.uint32 FStar.Monotonic.HyperStack.mem EverCrypt.Error.error_code Prims.l_and QUIC.Impl.payload_encrypt_pre LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_union LowStar.Monotonic.Buffer.loc_buffer LowStar.Buffer.trivial_preorder LowStar.Buffer.gsub QUIC.Secret.Int.reveal Lib.IntTypes.U32 Lib.IntTypes.SEC FStar.UInt32.sub LowStar.Monotonic.Buffer.len EverCrypt.AEAD.footprint EverCrypt.AEAD.invariant Prims.eq2 LowStar.Monotonic.Buffer.loc EverCrypt.AEAD.preserves_freeable Spec.Agile.AEAD.kv EverCrypt.AEAD.as_kv LowStar.Monotonic.Buffer.deref EverCrypt.AEAD.state_s FStar.Seq.Base.equal LowStar.Monotonic.Buffer.as_seq QUIC.Secret.Seq.seq_hide Lib.IntTypes.U8 QUIC.Spec.payload_encrypt QUIC.Secret.Seq.seq_reveal EverCrypt.Error.Success QUIC.Spec.Base.lbytes QUIC.Spec.Header.Base.header_len QUIC.Spec.Header.Parse.format_header
let payload_encrypt_post
      (a: ea)
      (s: AEAD.state a)
      (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)
      (header_len: Secret.uint32)
      (plain: B.buffer Secret.uint8)
      (plain_len: Secret.uint32)
      (m: HS.mem)
      (res: error_code)
      (m': HS.mem)
    : GTot Type0 =
  
let fmt = SParse.format_header h in
payload_encrypt_pre a s siv dst h pn_len pn header_len plain plain_len m /\
B.modifies ((B.loc_buffer (B.gsub dst
            (Secret.reveal header_len)
            ((B.len dst) `U32.sub` (Secret.reveal header_len))))
    `B.loc_union`
    (AEAD.footprint m s))
  m
  m' /\ AEAD.invariant m' s /\ AEAD.footprint m' s == AEAD.footprint m s /\
AEAD.preserves_freeable s m m' /\ AEAD.as_kv (B.deref m' s) == AEAD.as_kv (B.deref m s) /\
(B.as_seq m'
    (B.gsub dst (Secret.reveal header_len) ((B.len dst) `U32.sub` (Secret.reveal header_len))))
`Seq.equal`
(Seq.seq_hide (Spec.payload_encrypt a
        (AEAD.as_kv (B.deref m s))
        (B.as_seq m siv)
        h
        (Seq.seq_reveal (B.as_seq m plain)))) /\ res == Success