val header_encrypt_post
      (a: ea)
      (s: CTR.state (SAEAD.cipher_alg_of_supported_alg a))
      (k: B.buffer Secret.uint8)
      (dst: B.buffer U8.t)
      (h: G.erased Spec.header)
      (is_short is_retry: bool)
      (public_len: U32.t)
      (pn_len: PN.packet_number_length_t)
      (m m': HS.mem)
    : GTot Type0
let header_encrypt_post
  (a: ea)
  (s: CTR.state (SAEAD.cipher_alg_of_supported_alg a))
  (k: B.buffer Secret.uint8)
  (dst:B.buffer U8.t)
  (h: G.erased Spec.header)
  (is_short: bool)
  (is_retry: bool)
  (public_len: U32.t)
  (pn_len: PN.packet_number_length_t)
  (m: HS.mem)
  (m' : HS.mem)
: GTot Type0
= 
  header_encrypt_pre a s k dst h is_short is_retry public_len pn_len m /\
  begin
    let a' = SAEAD.cipher_alg_of_supported_alg a in
    let fmt = Parse.format_header h in
    let header_len = Seq.length fmt in
    let cipher = Seq.slice (B.as_seq m dst) header_len (B.length dst) in
    B.modifies (B.loc_buffer dst `B.loc_union` CTR.footprint m s) m m' /\
    B.as_seq m' dst `Seq.equal`
      Spec.header_encrypt a (B.as_seq m k) h cipher /\
    CTR.invariant m' s /\
    CTR.footprint m s == CTR.footprint m' s
  end
val header_encrypt_post
      (a: ea)
      (s: CTR.state (SAEAD.cipher_alg_of_supported_alg a))
      (k: B.buffer Secret.uint8)
      (dst: B.buffer U8.t)
      (h: G.erased Spec.header)
      (is_short is_retry: bool)
      (public_len: U32.t)
      (pn_len: PN.packet_number_length_t)
      (m m': HS.mem)
    : GTot Type0
let header_encrypt_post
      (a: ea)
      (s: CTR.state (SAEAD.cipher_alg_of_supported_alg a))
      (k: B.buffer Secret.uint8)
      (dst: B.buffer U8.t)
      (h: G.erased Spec.header)
      (is_short is_retry: bool)
      (public_len: U32.t)
      (pn_len: PN.packet_number_length_t)
      (m m': HS.mem)
    : GTot Type0 =
header_encrypt_pre a s k dst h is_short is_retry public_len pn_len m /\
(let a' = SAEAD.cipher_alg_of_supported_alg a in
  let fmt = Parse.format_header h in
  let header_len = Seq.length fmt in
  let cipher = Seq.slice (B.as_seq m dst) header_len (B.length dst) in
  B.modifies ((B.loc_buffer dst) `B.loc_union` (CTR.footprint m s)) m m' /\
  (B.as_seq m' dst) `Seq.equal` (Spec.header_encrypt a (B.as_seq m k) h cipher) /\
  CTR.invariant m' s /\ CTR.footprint m s == CTR.footprint m' s)
QUIC.Impl.Header.fsti.checked
Spec.Agile.Cipher.fsti.checked Spec.Agile.AEAD.fsti.checked QUIC.Spec.PacketNumber.Base.fst.checked QUIC.Spec.Header.Parse.fsti.checked QUIC.Spec.Header.fsti.checked QUIC.Spec.Crypto.fsti.checked QUIC.Secret.Int.fsti.checked QUIC.Impl.Header.Base.fst.checked prims.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked EverCrypt.CTR.fsti.checked
QUIC.Impl.Header.fsti
QUIC.Spec.Crypto.ea NotEverCrypt.CTR.state Spec.Agile.AEAD.cipher_alg_of_supported_alg LowStar.Buffer.buffer Lib.IntTypes.uint8 FStar.UInt8.t FStar.Ghost.erased QUIC.Spec.Header.Base.header Prims.bool FStar.UInt32.t QUIC.Spec.PacketNumber.Base.packet_number_length_t FStar.Monotonic.HyperStack.mem Prims.l_and QUIC.Impl.Header.header_encrypt_pre LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_union LowStar.Monotonic.Buffer.loc_buffer LowStar.Buffer.trivial_preorder NotEverCrypt.CTR.footprint FStar.Seq.Base.equal LowStar.Monotonic.Buffer.as_seq QUIC.Spec.Header.header_encrypt FStar.Ghost.reveal NotEverCrypt.CTR.invariant Prims.eq2 LowStar.Monotonic.Buffer.loc FStar.Seq.Base.seq FStar.Seq.Base.slice LowStar.Monotonic.Buffer.length Prims.nat FStar.Seq.Base.length QUIC.Spec.Base.byte QUIC.Spec.Base.lbytes QUIC.Spec.Header.Base.header_len QUIC.Spec.Header.Parse.format_header Spec.Agile.Cipher.cipher_alg
module QUIC.Impl.Header
include QUIC.Impl.Header.Base

open QUIC.Spec.Crypto

module G = FStar.Ghost
module U8 = FStar.UInt8
module B = LowStar.Buffer
module U32 = FStar.UInt32
module Secret = QUIC.Secret.Int
module PN = QUIC.Spec.PacketNumber.Base
module HST = FStar.HyperStack.ST
module Seq = FStar.Seq
module HS = FStar.HyperStack

module Spec = QUIC.Spec.Header
module Parse = QUIC.Spec.Header.Parse
module SAEAD = Spec.Agile.AEAD
module SCipher = Spec.Agile.Cipher

module CTR = EverCrypt.CTR

unfold
let header_encrypt_pre
  (a: ea)
  (s: CTR.state (SAEAD.cipher_alg_of_supported_alg a))
  (k: B.buffer Secret.uint8)
  (dst:B.buffer U8.t)
  (h: G.erased Spec.header)
  (is_short: bool)
  (is_retry: bool)
  (public_len: U32.t)
  (pn_len: PN.packet_number_length_t)
  (m: HS.mem)
: GTot Type0
=
  let a' = SAEAD.cipher_alg_of_supported_alg a in
  let fmt = Parse.format_header h in
  let header_len = Seq.length fmt in

  B.all_disjoint [
    CTR.footprint m s;
    B.loc_buffer k;
    B.loc_buffer dst;
  ] /\

  CTR.invariant m s /\
  B.live m k /\ B.length k == SCipher.key_length a' /\
  B.live m dst /\

  is_short == Spec.MShort? h /\
  is_retry == Spec.is_retry h /\
  begin if is_retry
  then
    U32.v public_len == header_len /\
    B.length dst == header_len
  else
    let cipher_len = B.length dst - header_len in
    U32.v public_len == Parse.pn_offset h /\
    pn_len == Spec.pn_length h /\
    19 <= cipher_len /\ cipher_len < max_cipher_length
  end /\
  Seq.slice (B.as_seq m dst) 0 header_len `Seq.equal` fmt

unfold
let header_encrypt_post
  (a: ea)
  (s: CTR.state (SAEAD.cipher_alg_of_supported_alg a))
  (k: B.buffer Secret.uint8)
  (dst:B.buffer U8.t)
  (h: G.erased Spec.header)
  (is_short: bool)
  (is_retry: bool)
  (public_len: U32.t)
  (pn_len: PN.packet_number_length_t)
  (m: HS.mem)
  (m' : HS.mem)
: GTot Type0
val header_encrypt_post
      (a: ea)
      (s: CTR.state (SAEAD.cipher_alg_of_supported_alg a))
      (k: B.buffer Secret.uint8)
      (dst: B.buffer U8.t)
      (h: G.erased Spec.header)
      (is_short is_retry: bool)
      (public_len: U32.t)
      (pn_len: PN.packet_number_length_t)
      (m m': HS.mem)
    : GTot Type0

    a: QUIC.Spec.Crypto.ea ->
    s: NotEverCrypt.CTR.state (Spec.Agile.AEAD.cipher_alg_of_supported_alg a) ->
    k: LowStar.Buffer.buffer Lib.IntTypes.uint8 ->
    dst: LowStar.Buffer.buffer FStar.UInt8.t ->
    h: FStar.Ghost.erased QUIC.Spec.Header.Base.header ->
    is_short: Prims.bool ->
    is_retry: Prims.bool ->
    public_len: FStar.UInt32.t ->
    pn_len: QUIC.Spec.PacketNumber.Base.packet_number_length_t ->
    m: FStar.Monotonic.HyperStack.mem ->
    m': FStar.Monotonic.HyperStack.mem
  -> Prims.GTot Type0