val header_decrypt_pre
      (a: ea)
      (s: CTR.state (SAEAD.cipher_alg_of_supported_alg a))
      (k: B.buffer Secret.uint8)
      (cid_len: short_dcid_len_t)
      (last: PN.last_packet_number_t)
      (dst: B.buffer U8.t)
      (dst_len: U32.t)
      (m: HS.mem)
    : GTot Type0
let header_decrypt_pre
  (a: ea)
  (s: CTR.state (SAEAD.cipher_alg_of_supported_alg a))
  (k: B.buffer Secret.uint8)
  (cid_len: short_dcid_len_t)
  (last: PN.last_packet_number_t)
  (dst:B.buffer U8.t)
  (dst_len: U32.t)
  (m: HS.mem)
: GTot Type0
=
  let a' = SAEAD.cipher_alg_of_supported_alg a 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 /\ B.length dst == U32.v dst_len
val header_decrypt_pre
      (a: ea)
      (s: CTR.state (SAEAD.cipher_alg_of_supported_alg a))
      (k: B.buffer Secret.uint8)
      (cid_len: short_dcid_len_t)
      (last: PN.last_packet_number_t)
      (dst: B.buffer U8.t)
      (dst_len: U32.t)
      (m: HS.mem)
    : GTot Type0
let header_decrypt_pre
      (a: ea)
      (s: CTR.state (SAEAD.cipher_alg_of_supported_alg a))
      (k: B.buffer Secret.uint8)
      (cid_len: short_dcid_len_t)
      (last: PN.last_packet_number_t)
      (dst: B.buffer U8.t)
      (dst_len: U32.t)
      (m: HS.mem)
    : GTot Type0 =
let a' = SAEAD.cipher_alg_of_supported_alg a 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 /\ B.length dst == U32.v dst_len
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 QUIC.Spec.Base.short_dcid_len_t QUIC.Spec.PacketNumber.Base.last_packet_number_t FStar.UInt8.t FStar.UInt32.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 Prims.int Prims.l_or FStar.UInt.size FStar.UInt32.n Prims.b2t Prims.op_GreaterThanOrEqual FStar.UInt32.v 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
= 
  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: 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 ->
  HST.Stack unit
    (requires (fun h0 ->
      header_encrypt_pre a s k dst h is_short is_retry public_len pn_len h0
    ))
    (ensures fun h0 _ h1 ->
      header_encrypt_post a s k dst h is_short is_retry public_len pn_len h0 h1
    )

noeq
type h_result =
| H_Failure
| H_Success:
    (h: header) ->
    (pn: PN.packet_number_t) ->
    (cipher_length: Secret.uint32) ->
    h_result

unfold
let header_decrypt_pre
  (a: ea)
  (s: CTR.state (SAEAD.cipher_alg_of_supported_alg a))
  (k: B.buffer Secret.uint8)
  (cid_len: short_dcid_len_t)
  (last: PN.last_packet_number_t)
  (dst:B.buffer U8.t)
  (dst_len: U32.t)
  (m: HS.mem)
val header_decrypt_pre
      (a: ea)
      (s: CTR.state (SAEAD.cipher_alg_of_supported_alg a))
      (k: B.buffer Secret.uint8)
      (cid_len: short_dcid_len_t)
      (last: PN.last_packet_number_t)
      (dst: B.buffer U8.t)
      (dst_len: U32.t)
      (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 ->
    cid_len: QUIC.Spec.Base.short_dcid_len_t ->
    last: QUIC.Spec.PacketNumber.Base.last_packet_number_t ->
    dst: LowStar.Buffer.buffer FStar.UInt8.t ->
    dst_len: FStar.UInt32.t ->
    m: FStar.Monotonic.HyperStack.mem
  -> Prims.GTot Type0