val decrypt_post
      (i: index)
      (s: state i)
      (dst: B.pointer QImpl.result)
      (packet: B.buffer U8.t)
      (len: U32.t)
      (cid_len: U8.t)
      (h0: HS.mem)
      (res: error_code)
      (h1: HS.mem)
    : Pure Type0
      (requires
        U8.v cid_len <= 20 /\ U32.v len == B.length packet /\ invariant h0 s /\ receivable s h0)
      (ensures fun _ -> True)
let decrypt_post (i: index)
  (s:state i)
  (dst: B.pointer QImpl.result)
  (packet: B.buffer U8.t)
  (len: U32.t)
  (cid_len: U8.t)
  (h0: HS.mem)
  (res: error_code)
  (h1: HS.mem): Pure Type0
  (requires
    U8.v cid_len <= 20 /\
    U32.v len == B.length packet /\
    invariant h0 s /\
    receivable s h0)
  (ensures fun _ -> True)
=
  let s0 = g_traffic_secret s h0 in
  let k = QSpec.(derive_secret (halg i) s0 label_key (Spec.Agile.AEAD.key_length (alg i))) in
  let iv = QSpec.(derive_secret (halg i) s0 label_iv 12) in
  let pne = QSpec.(derive_secret (halg i) s0 label_hp (cipher_keysize (alg i))) in
  let prev = g_last_packet_number s h0 in
  invariant h1 s /\
  footprint h1 s == footprint h0 s /\
  begin
    let r = B.deref h1 dst in
    let x = g_last_packet_number in
    let y = packet in
    let open QImpl in
    let packet = y in
    let g_last_packet_number = x in
    match res with
    | Success ->
      // prev is known to be >= g_initial_packet_number (see lemma invariant_packet_number)
      Secret.v (g_last_packet_number s h1) == FStar.Math.Lib.max (Secret.v prev) (Secret.v r.QImplBase.pn) /\ (

      // Lengths
      r.header_len == header_len r.header /\
      Secret.v r.header_len + Secret.v r.plain_len <= Secret.v r.total_len /\
      Secret.v r.total_len <= B.length packet /\
      B.(loc_includes (loc_buffer (B.gsub packet 0ul (Secret.reveal r.header_len))) (header_footprint r.header)) /\
      header_live r.header h1 /\
      Secret.v r.total_len <= B.length packet /\

      // Contents
      (
      let fmt = B.as_seq h1 (B.gsub packet 0ul (Secret.reveal r.header_len)) in
      let plain =
        B.as_seq h1 (B.gsub packet (Secret.reveal r.header_len) (Secret.reveal r.plain_len)) in
      let rem = B.as_seq h0 (B.gsub packet (Secret.reveal r.total_len) (B.len packet `U32.sub `Secret.reveal r.total_len)) in
      match QSpec.decrypt (alg i) k iv pne (Secret.v prev) (U8.v cid_len) (B.as_seq h0 packet) with
      | QSpec.Success h' plain' rem' ->
        h' == g_header r.header h1 r.pn /\
        fmt == QUIC.Spec.Header.Parse.format_header h' /\
        plain' == plain /\
        rem' == rem
      | _ -> False
    ))
    | DecodeError ->
      QSpec.Failure? (QSpec.decrypt (alg i) k iv pne (Secret.v prev) (U8.v cid_len) (B.as_seq h0 packet))
    | AuthenticationFailure ->
      QSpec.Failure? (QSpec.decrypt (alg i) k iv pne (Secret.v prev) (U8.v cid_len) (B.as_seq h0 packet)) /\
      Secret.v r.total_len <= B.length packet
    | _ ->
      False
  end
val decrypt_post
      (i: index)
      (s: state i)
      (dst: B.pointer QImpl.result)
      (packet: B.buffer U8.t)
      (len: U32.t)
      (cid_len: U8.t)
      (h0: HS.mem)
      (res: error_code)
      (h1: HS.mem)
    : Pure Type0
      (requires
        U8.v cid_len <= 20 /\ U32.v len == B.length packet /\ invariant h0 s /\ receivable s h0)
      (ensures fun _ -> True)
let decrypt_post
      (i: index)
      (s: state i)
      (dst: B.pointer QImpl.result)
      (packet: B.buffer U8.t)
      (len: U32.t)
      (cid_len: U8.t)
      (h0: HS.mem)
      (res: error_code)
      (h1: HS.mem)
    : Pure Type0
      (requires
        U8.v cid_len <= 20 /\ U32.v len == B.length packet /\ invariant h0 s /\ receivable s h0)
      (ensures fun _ -> True) =
let s0 = g_traffic_secret s h0 in
let k =
  let open QSpec in derive_secret (halg i) s0 label_key (Spec.Agile.AEAD.key_length (alg i))
in
let iv = let open QSpec in derive_secret (halg i) s0 label_iv 12 in
let pne = let open QSpec in derive_secret (halg i) s0 label_hp (cipher_keysize (alg i)) in
let prev = g_last_packet_number s h0 in
invariant h1 s /\ footprint h1 s == footprint h0 s /\
(let r = B.deref h1 dst in
  let x = g_last_packet_number in
  let y = packet in
  let open QImpl in
  let packet = y in
  let g_last_packet_number = x in
  match res with
  | Success ->
    Secret.v (g_last_packet_number s h1) ==
    FStar.Math.Lib.max (Secret.v prev) (Secret.v r.QImplBase.pn) /\
    (r.header_len == header_len r.header /\
      Secret.v r.header_len + Secret.v r.plain_len <= Secret.v r.total_len /\
      Secret.v r.total_len <= B.length packet /\
      B.(loc_includes (loc_buffer (B.gsub packet 0ul (Secret.reveal r.header_len)))
          (header_footprint r.header)) /\ header_live r.header h1 /\
      Secret.v r.total_len <= B.length packet /\
      (let fmt = B.as_seq h1 (B.gsub packet 0ul (Secret.reveal r.header_len)) in
        let plain =
          B.as_seq h1 (B.gsub packet (Secret.reveal r.header_len) (Secret.reveal r.plain_len))
        in
        let rem =
          B.as_seq h0
            (B.gsub packet
                (Secret.reveal r.total_len)
                ((B.len packet) `U32.sub` (Secret.reveal r.total_len)))
        in
        match
          QSpec.decrypt (alg i) k iv pne (Secret.v prev) (U8.v cid_len) (B.as_seq h0 packet)
        with
        | QSpec.Success h' plain' rem' ->
          h' == g_header r.header h1 r.pn /\ fmt == QUIC.Spec.Header.Parse.format_header h' /\
          plain' == plain /\ rem' == rem
        | _ -> False))
  | DecodeError ->
    QSpec.Failure? (QSpec.decrypt (alg i)
          k
          iv
          pne
          (Secret.v prev)
          (U8.v cid_len)
          (B.as_seq h0 packet))
  | AuthenticationFailure ->
    QSpec.Failure? (QSpec.decrypt (alg i)
          k
          iv
          pne
          (Secret.v prev)
          (U8.v cid_len)
          (B.as_seq h0 packet)) /\ Secret.v r.total_len <= B.length packet
  | _ -> False)
QUIC.fsti.checked
Spec.Hash.Definitions.fst.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.fsti.checked QUIC.Secret.Seq.fsti.checked QUIC.Secret.Int.fsti.checked QUIC.Impl.Header.Base.fst.checked QUIC.Impl.fsti.checked prims.fst.checked Model.QUIC.fsti.checked Model.Indexing.fsti.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lib.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked EverCrypt.Helpers.fsti.checked EverCrypt.Error.fsti.checked
QUIC.fsti
QUIC.index QUIC.state LowStar.Buffer.pointer QUIC.Impl.Header.Base.result LowStar.Buffer.buffer FStar.UInt8.t FStar.UInt32.t FStar.Monotonic.HyperStack.mem EverCrypt.Error.error_code Prims.l_and QUIC.invariant Prims.eq2 LowStar.Monotonic.Buffer.loc QUIC.footprint Prims.int Prims.l_or Lib.IntTypes.range Lib.IntTypes.U64 Prims.l_imp Prims.b2t Prims.op_GreaterThanOrEqual QUIC.Secret.Int.Base.v Lib.IntTypes.SEC QUIC.Impl.Header.Base.__proj__Mkresult__item__pn Prims.op_Equality Prims.op_LessThan FStar.Math.Lib.max Lib.IntTypes.uint32 QUIC.Impl.Header.Base.__proj__Mkresult__item__header_len QUIC.Impl.Header.Base.header_len QUIC.Impl.Header.Base.__proj__Mkresult__item__header Prims.op_LessThanOrEqual Prims.op_Addition Lib.IntTypes.U32 QUIC.Impl.Header.Base.__proj__Mkresult__item__plain_len QUIC.Impl.Header.Base.__proj__Mkresult__item__total_len LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder LowStar.Monotonic.Buffer.loc_includes LowStar.Monotonic.Buffer.loc_buffer LowStar.Buffer.gsub FStar.UInt32.__uint_to_t QUIC.Secret.Int.reveal QUIC.Impl.Header.Base.header_footprint QUIC.Impl.Header.Base.header_live QUIC.Spec.decrypt QUIC.alg FStar.UInt8.v LowStar.Monotonic.Buffer.as_seq QUIC.Spec.Header.Base.header QUIC.Spec.Base.bytes QUIC.Impl.Header.Base.g_header FStar.Seq.Base.seq QUIC.Spec.Base.byte QUIC.Spec.Header.Parse.format_header QUIC.Spec.result Prims.l_False Prims.logical FStar.UInt32.sub LowStar.Monotonic.Buffer.len QUIC.Spec.uu___is_Failure QUIC.Spec.PacketNumber.Base.packet_number_t Lib.IntTypes.v QUIC.g_initial_packet_number QUIC.g_last_packet_number LowStar.Monotonic.Buffer.deref Lib.IntTypes.int_t Lib.IntTypes.U8 QUIC.Spec.Crypto.derive_secret QUIC.halg QUIC.Spec.Crypto.label_hp QUIC.Spec.Crypto.cipher_keysize QUIC.Spec.Crypto.label_iv QUIC.Spec.Crypto.label_key Spec.Agile.AEAD.key_length QUIC.traffic_secret QUIC.g_traffic_secret FStar.UInt.size FStar.UInt32.n FStar.UInt32.v QUIC.receivable Prims.l_True
module QUIC

module QSpec = QUIC.Spec
module QImpl = QUIC.Impl
module QImplBase = QUIC.Impl.Header.Base
module QModel = Model.QUIC
module PN = QUIC.Spec.PacketNumber.Base

module Secret = QUIC.Secret.Int

module I = Model.Indexing
module G = FStar.Ghost
module B = LowStar.Buffer
module S = FStar.Seq
module HS = FStar.HyperStack
module ST = 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

#set-options "--fuel 0 --ifuel 0"

type nat62 = n:nat{n < pow2 62}

let cipher_keysize (a:QSpec.ea) =
  Spec.Agile.Cipher.key_length (Spec.Agile.AEAD.cipher_alg_of_supported_alg a)

/// Low-level types used in this API
/// --------------------------------

let u2 = QImpl.u2
let u4 = QImpl.u4
let u62 = QImpl.u62

val index:eqtype

val alg: index -> GTot QSpec.ea
val halg: index -> GTot QSpec.ha

let traffic_secret i =
  Spec.Hash.Definitions.bytes_hash (halg i)

// Switch state: either QModel or QImpl
val state: index -> Type u#1

val footprint: #i:index -> HS.mem -> state i -> GTot B.loc
val invariant: #i:index -> HS.mem -> state i -> Type0

val g_traffic_secret: #i:index -> state i -> HS.mem -> GTot (traffic_secret i)
val g_initial_packet_number: #i:index -> (s: state i) -> (h: HS.mem) -> GTot PN.packet_number_t
val g_last_packet_number: #i:index -> (s:state i) -> (h: HS.mem { invariant h s }) ->
  GTot (pn: PN.packet_number_t {
    let open Lib.IntTypes in
    Secret.v pn >= Secret.v #U64 #SEC (g_initial_packet_number s h)
  })
val g_next_packet_number: #i:index -> (s:state i) -> (h: HS.mem { invariant h s }) ->
  GTot (pn: PN.packet_number_t {
    let open Lib.IntTypes in
    Secret.v pn >= Secret.v #U64 #SEC (g_initial_packet_number s h)
  })

let incrementable (#i: index) (s: state i) (h: HS.mem { invariant h s }) =
  Secret.v (g_next_packet_number s h) + 1 < pow2 62

let receivable (#i: index) (s: state i) (h: HS.mem { invariant h s }) =
  Secret.v (g_last_packet_number s h) + 1 < pow2 62

#push-options "--z3rlimit 15"

val encrypt: #i:(*G.erased *)index -> (
  //let i = G.reveal i in
  s: state i ->
  dst: B.buffer U8.t ->
  dst_pn: B.pointer PN.packet_number_t ->
  h: QImplBase.header ->
  plain: B.buffer Secret.uint8 ->
  plain_len: U32.t ->
  ST error_code
    (requires fun h0 ->
      not (QImpl.is_retry h) /\ // until it's supported in Model.QUIC
      // Memory & preservation
      B.live h0 plain /\ B.live h0 dst /\ B.live h0 dst_pn /\
      QImplBase.header_live h h0 /\
      B.(all_disjoint [ footprint h0 s; loc_buffer dst; loc_buffer dst_pn; QImpl.header_footprint h; loc_buffer plain ]) /\
      invariant h0 s /\
      incrementable s h0 /\
      B.length plain == U32.v plain_len /\ (
      let clen =
        if QImplBase.is_retry h then
          0
        else
          U32.v plain_len + Spec.Agile.AEAD.tag_length (alg i)
      in
      (if QImplBase.is_retry h then U32.v plain_len == 0 else 3 <= U32.v plain_len /\ U32.v plain_len < QSpec.max_plain_length) /\
      (QImplBase.has_payload_length h ==> Secret.v (QImplBase.payload_length h) == clen) /\
      B.length dst == Secret.v (QImplBase.header_len h) + clen
    ))
    (ensures fun h0 r h1 ->
      match r with
      | Success ->
          // Memory & preservation
          B.(modifies (footprint h0 s `loc_union` loc_buffer dst `loc_union` loc_buffer dst_pn)) h0 h1 /\
          invariant h1 s /\
          footprint h1 s == footprint h0 s /\ (
          // Functional correctness
          let ts = g_traffic_secret s h0 in
          let open QUIC.Spec in
          let k = derive_secret (halg i) ts label_key (Spec.Agile.AEAD.key_length (alg i)) in
          let iv = derive_secret (halg i) ts label_iv 12 in
          let pne = derive_secret (halg i) ts label_hp (cipher_keysize (alg i)) in
          let plain = B.as_seq h0 plain in
          let packet: packet = B.as_seq h1 dst in
          let pn = g_next_packet_number s h0 `Secret.add` Secret.to_u64 1uL in
          B.deref h1 dst_pn == pn /\
          packet `Seq.equal` encrypt (alg i) k iv pne (QImpl.g_header h h0 pn) (QUIC.Secret.Seq.seq_reveal plain) /\
          g_next_packet_number s h1 == pn)
      | _ ->
          False))

#pop-options

unfold
let decrypt_post (i: index)
  (s:state i)
  (dst: B.pointer QImpl.result)
  (packet: B.buffer U8.t)
  (len: U32.t)
  (cid_len: U8.t)
  (h0: HS.mem)
  (res: error_code)
  (h1: HS.mem): Pure Type0
  (requires
    U8.v cid_len <= 20 /\
    U32.v len == B.length packet /\
    invariant h0 s /\
    receivable s h0)
val decrypt_post
      (i: index)
      (s: state i)
      (dst: B.pointer QImpl.result)
      (packet: B.buffer U8.t)
      (len: U32.t)
      (cid_len: U8.t)
      (h0: HS.mem)
      (res: error_code)
      (h1: HS.mem)
    : Pure Type0
      (requires
        U8.v cid_len <= 20 /\ U32.v len == B.length packet /\ invariant h0 s /\ receivable s h0)
      (ensures fun _ -> True)

    i: QUIC.index ->
    s: QUIC.state i ->
    dst: LowStar.Buffer.pointer QUIC.Impl.Header.Base.result ->
    packet: LowStar.Buffer.buffer FStar.UInt8.t ->
    len: FStar.UInt32.t ->
    cid_len: FStar.UInt8.t ->
    h0: FStar.Monotonic.HyperStack.mem ->
    res: EverCrypt.Error.error_code ->
    h1: FStar.Monotonic.HyperStack.mem
  -> Prims.Pure Type0