val 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 is_retry: bool)
      (public_len: U32.t)
      (pn_len: PN.packet_number_length_t)
      (m: HS.mem)
    : GTot Type0
val 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 is_retry: bool)
      (public_len: U32.t)
      (pn_len: PN.packet_number_length_t)
      (m: HS.mem)
    : GTot Type0
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
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
/
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

    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
  -> Prims.GTot Type0
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 LowStar.Monotonic.Buffer.all_disjoint Prims.Cons LowStar.Monotonic.Buffer.loc NotEverCrypt.CTR.footprint LowStar.Monotonic.Buffer.loc_buffer LowStar.Buffer.trivial_preorder Prims.Nil NotEverCrypt.CTR.invariant LowStar.Monotonic.Buffer.live Prims.eq2 Prims.nat LowStar.Monotonic.Buffer.length Spec.Agile.Cipher.key_length QUIC.Spec.Header.Base.uu___is_MShort FStar.Ghost.reveal QUIC.Spec.Header.Base.is_retry Prims.int Prims.l_or FStar.UInt.size FStar.UInt32.n Prims.b2t Prims.op_GreaterThanOrEqual FStar.UInt32.v Prims.op_LessThan Prims.op_Addition QUIC.Secret.Int.Base.v Lib.IntTypes.U32 Lib.IntTypes.SEC QUIC.Spec.Header.Base.pn_length QUIC.Spec.Header.Base.header_len QUIC.Spec.Header.Parse.pn_offset Prims.op_LessThanOrEqual QUIC.Spec.Crypto.max_cipher_length Prims.op_Subtraction Prims.logical FStar.Seq.Base.equal FStar.Seq.Base.slice LowStar.Monotonic.Buffer.as_seq FStar.Seq.Base.length QUIC.Spec.Base.byte QUIC.Spec.Base.lbytes QUIC.Spec.Header.Parse.format_header Spec.Agile.Cipher.cipher_alg
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 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 /\
(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) /\ (Seq.slice (B.as_seq m dst) 0 header_len) `Seq.equal` fmt