val encrypt_length:
  a: ea ->
  k: AEAD.kv a ->
  static_iv: iv_t a ->
  hpk: Cipher.key (AEAD.cipher_alg_of_supported_alg a) ->
  h: header ->
  plain: pbytes' (is_retry h) ->
  Lemma
  (ensures (
    Seq.length (encrypt a k static_iv hpk h plain) ==
    header_len h +
      begin if is_retry h
      then Seq.length plain
      else AEAD.tag_length a + Seq.length plain
      end
  ))
let encrypt_length
  a k siv hpk h plain
=
  let c =
    if is_retry h
    then plain
    else payload_encrypt a k siv h plain
  in
  H.header_encrypt_length a hpk h c
val encrypt_length:
  a: ea ->
  k: AEAD.kv a ->
  static_iv: iv_t a ->
  hpk: Cipher.key (AEAD.cipher_alg_of_supported_alg a) ->
  h: header ->
  plain: pbytes' (is_retry h) ->
  Lemma
  (ensures (
    Seq.length (encrypt a k static_iv hpk h plain) ==
    header_len h +
      begin if is_retry h
      then Seq.length plain
      else AEAD.tag_length a + Seq.length plain
      end
  ))
let encrypt_length a k siv hpk h plain =
let c = if is_retry h then plain else payload_encrypt a k siv h plain in
H.header_encrypt_length a hpk h c
QUIC.Spec.fst.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.HKDF.fsti.checked Spec.Agile.Hash.fsti.checked Spec.Agile.Cipher.fsti.checked Spec.Agile.AEAD.fsti.checked QUIC.Spec.Lemmas.fst.checked QUIC.Spec.Header.Parse.fsti.checked QUIC.Spec.Header.Base.fst.checked QUIC.Spec.Header.fsti.checked QUIC.Secret.Seq.fsti.checked QUIC.Secret.Int.fsti.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Endianness.fsti.checked
QUIC.Spec.fst
QUIC.Spec.Crypto.ea Spec.Agile.AEAD.kv QUIC.Spec.iv_t Spec.Agile.Cipher.key Spec.Agile.AEAD.cipher_alg_of_supported_alg QUIC.Spec.Header.Base.header QUIC.Spec.Crypto.pbytes' QUIC.Spec.Header.Base.is_retry QUIC.Spec.Header.header_encrypt_length QUIC.Spec.Crypto.cbytes' Prims.bool QUIC.Spec.payload_encrypt Prims.unit
module QUIC.Spec

open QUIC.Spec.Lemmas
open QUIC.Spec.Header.Base

module Seq = QUIC.Secret.Seq
module U32 = FStar.UInt32
module U8 = FStar.UInt8
module H = Spec.Agile.Hash
module HD = Spec.Hash.Definitions
module Cipher = Spec.Agile.Cipher
module AEAD = Spec.Agile.AEAD
module HKDF = Spec.Agile.HKDF
module Parse = QUIC.Spec.Header.Parse
module H = QUIC.Spec.Header
module Secret = QUIC.Secret.Int

/// encryption of a packet

let iv_for_encrypt_decrypt
  (a: ea)
  (siv: iv_t a)
  (h: header { ~ (is_retry h) })
: GTot (iv_t a)
=
  let pn_len = Secret.v (pn_length h) - 1 in
  let seqn = packet_number h in
  let _ = assert_norm(pow2 62 < pow2 (8 `op_Multiply` 12)) in
  let pnb = FStar.Endianness.n_to_be 12 (Secret.v seqn) in
  Seq.seq_hide #Secret.U8 (xor_inplace pnb (Seq.seq_reveal siv) 0)

let payload_encrypt
  (a: ea)
  (k: AEAD.kv a)
  (siv: iv_t a)
  (h: header { ~ (is_retry h) })
  (plain: pbytes)
: GTot (cbytes)
=
  let aad = Parse.format_header h in
  let iv = iv_for_encrypt_decrypt a siv h in
  Seq.seq_reveal (AEAD.encrypt #a k iv (Seq.seq_hide aad) (Seq.seq_hide plain))

let encrypt
  a k siv hpk h plain
=
  let cipher =
    if is_retry h
    then plain
    else payload_encrypt a k siv h plain
  in
  H.header_encrypt a hpk h cipher

let encrypt_length
val encrypt_length:
  a: ea ->
  k: AEAD.kv a ->
  static_iv: iv_t a ->
  hpk: Cipher.key (AEAD.cipher_alg_of_supported_alg a) ->
  h: header ->
  plain: pbytes' (is_retry h) ->
  Lemma
  (ensures (
    Seq.length (encrypt a k static_iv hpk h plain) ==
    header_len h +
      begin if is_retry h
      then Seq.length plain
      else AEAD.tag_length a + Seq.length plain
      end
  ))

    a: QUIC.Spec.Crypto.ea ->
    k: Spec.Agile.AEAD.kv a ->
    static_iv: QUIC.Spec.iv_t a ->
    hpk: Spec.Agile.Cipher.key (Spec.Agile.AEAD.cipher_alg_of_supported_alg a) ->
    h: QUIC.Spec.Header.Base.header ->
    plain: QUIC.Spec.Crypto.pbytes' (QUIC.Spec.Header.Base.is_retry h)
  -> FStar.Pervasives.Lemma
    (ensures
      FStar.Seq.Base.length (QUIC.Spec.encrypt a k static_iv hpk h plain) ==
      QUIC.Spec.Header.Base.header_len h +
      (match QUIC.Spec.Header.Base.is_retry h with
        | true -> FStar.Seq.Base.length plain
        | _ -> Spec.Agile.AEAD.tag_length a + FStar.Seq.Base.length plain))