val header_decrypt_post
      (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)
      (res: h_result)
      (m': HS.mem)
    : GTot Type0
let header_decrypt_post
  (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)
  (res: h_result)
  (m' : HS.mem)
: GTot Type0
= 
  header_decrypt_pre a s k cid_len last dst dst_len m /\
  CTR.footprint m' s == CTR.footprint m s /\
  CTR.invariant m' s /\
  begin match res, Spec.header_decrypt a (B.as_seq m k) (U32.v cid_len) (Secret.v last) (B.as_seq m dst) with
  | H_Failure, Spec.H_Failure ->
    B.modifies B.loc_none m m'
  | H_Success h pn cipher_len, Spec.H_Success gh gcipher grem ->
    header_live h m' /\
    gh == g_header h m' pn /\
    Secret.v (header_len h) + Secret.v cipher_len <= B.length dst /\
    B.loc_buffer (B.gsub dst 0ul (public_header_len h)) `B.loc_includes` header_footprint h /\
    B.modifies (B.loc_buffer (B.gsub dst 0ul (Secret.reveal (header_len h))) `B.loc_union` CTR.footprint m s) m m' /\
    Seq.length gcipher == Secret.v cipher_len /\
    B.as_seq m' dst `Seq.equal` (Parse.format_header gh `Seq.append` gcipher `Seq.append` grem) /\
    B.as_seq m' (B.gsub dst 0ul (Secret.reveal (header_len h))) == Parse.format_header gh /\
    B.as_seq m' (B.gsub dst (Secret.reveal (header_len h)) (Secret.reveal cipher_len)) == gcipher /\
    B.as_seq m' (B.gsub dst (Secret.reveal (header_len h) `U32.add` Secret.reveal cipher_len) (B.len dst `U32.sub` (Secret.reveal (header_len h) `U32.add` Secret.reveal cipher_len))) == grem
  | _ -> False
  end
val header_decrypt_post
      (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)
      (res: h_result)
      (m': HS.mem)
    : GTot Type0
let header_decrypt_post
      (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)
      (res: h_result)
      (m': HS.mem)
    : GTot Type0 =
header_decrypt_pre a s k cid_len last dst dst_len m /\ CTR.footprint m' s == CTR.footprint m s /\
CTR.invariant m' s /\
(match
    res, Spec.header_decrypt a (B.as_seq m k) (U32.v cid_len) (Secret.v last) (B.as_seq m dst)
  with
  | H_Failure, Spec.H_Failure -> B.modifies B.loc_none m m'
  | H_Success h pn cipher_len, Spec.H_Success gh gcipher grem ->
    header_live h m' /\ gh == g_header h m' pn /\
    Secret.v (header_len h) + Secret.v cipher_len <= B.length dst /\
    (B.loc_buffer (B.gsub dst 0ul (public_header_len h))) `B.loc_includes` (header_footprint h) /\
    B.modifies ((B.loc_buffer (B.gsub dst 0ul (Secret.reveal (header_len h))))
        `B.loc_union`
        (CTR.footprint m s))
      m
      m' /\ Seq.length gcipher == Secret.v cipher_len /\
    (B.as_seq m' dst)
    `Seq.equal`
    (((Parse.format_header gh) `Seq.append` gcipher) `Seq.append` grem) /\
    B.as_seq m' (B.gsub dst 0ul (Secret.reveal (header_len h))) == Parse.format_header gh /\
    B.as_seq m' (B.gsub dst (Secret.reveal (header_len h)) (Secret.reveal cipher_len)) == gcipher /\
    B.as_seq m'
      (B.gsub dst
          ((Secret.reveal (header_len h)) `U32.add` (Secret.reveal cipher_len))
          ((B.len dst)
            `U32.sub`
            ((Secret.reveal (header_len h)) `U32.add` (Secret.reveal cipher_len)))) ==
    grem
  | _ -> False)
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 QUIC.Impl.Header.h_result Prims.l_and QUIC.Impl.Header.header_decrypt_pre Prims.eq2 LowStar.Monotonic.Buffer.loc NotEverCrypt.CTR.footprint NotEverCrypt.CTR.invariant FStar.Pervasives.Native.Mktuple2 QUIC.Spec.Header.h_result QUIC.Spec.Header.header_decrypt LowStar.Monotonic.Buffer.as_seq LowStar.Buffer.trivial_preorder FStar.UInt32.v QUIC.Secret.Int.Base.v Lib.IntTypes.U64 Lib.IntTypes.SEC LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_none QUIC.Impl.Header.Base.header QUIC.Spec.PacketNumber.Base.packet_number_t Lib.IntTypes.uint32 QUIC.Spec.Header.Base.header QUIC.Spec.Base.bytes QUIC.Spec.Header.Base.is_retry Prims.int Prims.bool Prims.b2t Prims.op_LessThanOrEqual Prims.op_LessThan QUIC.Spec.Crypto.max_cipher_length Prims.nat FStar.Seq.Base.length QUIC.Spec.Base.byte QUIC.Impl.Header.Base.header_live QUIC.Impl.Header.Base.g_header Prims.op_Addition Lib.IntTypes.U32 QUIC.Impl.Header.Base.header_len LowStar.Monotonic.Buffer.length LowStar.Monotonic.Buffer.loc_includes LowStar.Monotonic.Buffer.loc_buffer LowStar.Buffer.gsub FStar.UInt32.__uint_to_t QUIC.Impl.Header.Base.public_header_len QUIC.Impl.Header.Base.header_footprint LowStar.Monotonic.Buffer.loc_union QUIC.Secret.Int.reveal Prims.l_or Prims.op_GreaterThanOrEqual Lib.IntTypes.range FStar.Seq.Base.equal FStar.Seq.Base.append QUIC.Spec.Header.Parse.format_header FStar.Seq.Base.seq FStar.UInt32.add FStar.UInt32.sub LowStar.Monotonic.Buffer.len FStar.Pervasives.Native.tuple2 Prims.l_False Prims.logical
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)
: 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

unfold
let header_decrypt_post
  (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)
  (res: h_result)
  (m' : HS.mem)
: GTot Type0
val header_decrypt_post
      (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)
      (res: h_result)
      (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 ->
    res: QUIC.Impl.Header.h_result ->
    m': FStar.Monotonic.HyperStack.mem
  -> Prims.GTot Type0