val lemma_encrypt_correct:
  a: ea ->
  k: AEAD.kv a ->
  siv: iv_t a ->
  hpk: Cipher.key (AEAD.cipher_alg_of_supported_alg a) ->
  h: header ->
  cid_len: nat { cid_len <= 20 /\ (MShort? h ==> cid_len == dcid_len h) } ->
  last: nat{last+1 < pow2 62 } ->
  p: pbytes' (is_retry h)  { has_payload_length h ==> Secret.v (payload_length h) == Seq.length p + AEAD.tag_length a } -> Lemma
  (requires (
    (~ (is_retry h)) ==> (
      PN.in_window (Secret.v (pn_length h) - 1) last (Secret.v (packet_number h))
  )))
  (ensures (
    decrypt a k siv hpk last cid_len
      (encrypt a k siv hpk h p)
    == Success h p Seq.empty
  ))
let lemma_encrypt_correct
  a k siv hpk h cid_len last plain
=
  let packet = encrypt a k siv hpk h plain in
  let aad = Seq.seq_hide (Parse.format_header h) in
  let cipher = if is_retry h then plain else
    let iv = iv_for_encrypt_decrypt a siv h in
    Seq.seq_reveal (AEAD.encrypt #a k iv aad (Seq.seq_hide plain))
  in
  assert (packet == H.header_encrypt a hpk h cipher);
  H.lemma_header_encryption_correct a hpk h cid_len last cipher;
  if is_retry h
  then ()
  else begin
    let iv = iv_for_encrypt_decrypt a siv h in
    let dc = H.header_decrypt a hpk cid_len last packet in
    assert (H.H_Success? dc);
    let H.H_Success h' c' rem' = dc in
    assert (h == h' /\ cipher == c');
    let clen = Seq.length cipher in
    assert (19 <= clen && clen < max_cipher_length);
    AEAD.correctness #a k iv aad (Seq.seq_hide plain)
  end
val lemma_encrypt_correct:
  a: ea ->
  k: AEAD.kv a ->
  siv: iv_t a ->
  hpk: Cipher.key (AEAD.cipher_alg_of_supported_alg a) ->
  h: header ->
  cid_len: nat { cid_len <= 20 /\ (MShort? h ==> cid_len == dcid_len h) } ->
  last: nat{last+1 < pow2 62 } ->
  p: pbytes' (is_retry h)  { has_payload_length h ==> Secret.v (payload_length h) == Seq.length p + AEAD.tag_length a } -> Lemma
  (requires (
    (~ (is_retry h)) ==> (
      PN.in_window (Secret.v (pn_length h) - 1) last (Secret.v (packet_number h))
  )))
  (ensures (
    decrypt a k siv hpk last cid_len
      (encrypt a k siv hpk h p)
    == Success h p Seq.empty
  ))
let lemma_encrypt_correct a k siv hpk h cid_len last plain =
let packet = encrypt a k siv hpk h plain in
let aad = Seq.seq_hide (Parse.format_header h) in
let cipher =
  if is_retry h
  then plain
  else
    let iv = iv_for_encrypt_decrypt a siv h in
    Seq.seq_reveal (AEAD.encrypt #a k iv aad (Seq.seq_hide plain))
in
assert (packet == H.header_encrypt a hpk h cipher);
H.lemma_header_encryption_correct a hpk h cid_len last cipher;
if is_retry h
then ()
else
  let iv = iv_for_encrypt_decrypt a siv h in
  let dc = H.header_decrypt a hpk cid_len last packet in
  assert (H.H_Success? dc);
  let H.H_Success h' c' rem' = dc in
  assert (h == h' /\ cipher == c');
  let clen = Seq.length cipher in
  assert (19 <= clen && clen < max_cipher_length);
  AEAD.correctness #a k iv aad (Seq.seq_hide plain)
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 Prims.nat Prims.l_and Prims.b2t Prims.op_LessThanOrEqual Prims.l_imp QUIC.Spec.Header.Base.uu___is_MShort Prims.eq2 QUIC.Spec.Header.Base.dcid_len Prims.op_LessThan Prims.op_Addition Prims.pow2 QUIC.Spec.Crypto.pbytes' QUIC.Spec.Header.Base.is_retry QUIC.Spec.Header.Base.has_payload_length Prims.int QUIC.Secret.Int.Base.v Lib.IntTypes.U64 Lib.IntTypes.SEC QUIC.Spec.Header.Base.payload_length FStar.Seq.Base.length QUIC.Spec.Base.byte Spec.Agile.AEAD.tag_length Prims.bool QUIC.Spec.Base.bytes QUIC.Spec.Crypto.max_cipher_length Spec.Agile.AEAD.correctness QUIC.Secret.Seq.seq_hide Lib.IntTypes.U8 Prims.unit Prims._assert Prims.op_AmpAmp FStar.Seq.Base.seq Prims.l_or Prims.logical Lib.IntTypes.range Prims.op_GreaterThanOrEqual QUIC.Spec.Header.h_result Prims.l_True QUIC.Spec.Header.Base.is_valid_header FStar.Seq.Base.equal FStar.Seq.Base.slice Prims.op_Subtraction QUIC.Spec.Header.uu___is_H_Success QUIC.Spec.Header.header_decrypt QUIC.Spec.iv_for_encrypt_decrypt QUIC.Spec.Header.lemma_header_encryption_correct QUIC.Spec.Crypto.packet QUIC.Spec.Header.header_encrypt Lib.IntTypes.v QUIC.Secret.Seq.seq_reveal Spec.Agile.AEAD.encrypt Lib.IntTypes.int_t QUIC.Spec.Header.Parse.format_header QUIC.Spec.encrypt
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
  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

#restart-solver

let payload_decrypt
  (a: ea)
  (k: AEAD.kv a)
  (siv: iv_t a)
  (h: header { ~ (is_retry h) })
  (c: Seq.seq Secret.uint8 { 16 <= Seq.length c /\ Seq.length c < max_cipher_length })
: GTot (option (AEAD.decrypted c))
= 
  let iv = iv_for_encrypt_decrypt a siv h in
  let aad = Parse.format_header h in
  AEAD.decrypt #a k iv (Seq.seq_hide aad) c

let decrypt
  a k siv hpk last cid_len packet
=
  let open FStar.Math.Lemmas in
  let open FStar.Endianness in
  match H.header_decrypt a hpk cid_len last packet with
  | H.H_Failure -> Failure
  | H.H_Success h c rem ->
    if is_retry h
    then Success h c rem
    else
      match payload_decrypt a k siv h (Seq.seq_hide c) with
      | None -> Failure
      | Some plain -> Success h (Seq.seq_reveal plain) rem

#push-options "--z3rlimit 20"

let lemma_encrypt_correct
val lemma_encrypt_correct:
  a: ea ->
  k: AEAD.kv a ->
  siv: iv_t a ->
  hpk: Cipher.key (AEAD.cipher_alg_of_supported_alg a) ->
  h: header ->
  cid_len: nat { cid_len <= 20 /\ (MShort? h ==> cid_len == dcid_len h) } ->
  last: nat{last+1 < pow2 62 } ->
  p: pbytes' (is_retry h)  { has_payload_length h ==> Secret.v (payload_length h) == Seq.length p + AEAD.tag_length a } -> Lemma
  (requires (
    (~ (is_retry h)) ==> (
      PN.in_window (Secret.v (pn_length h) - 1) last (Secret.v (packet_number h))
  )))
  (ensures (
    decrypt a k siv hpk last cid_len
      (encrypt a k siv hpk h p)
    == Success h p Seq.empty
  ))

    a: QUIC.Spec.Crypto.ea ->
    k: Spec.Agile.AEAD.kv a ->
    siv: 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 ->
    cid_len: Prims.nat{cid_len <= 20 /\ (MShort? h ==> cid_len == QUIC.Spec.Header.Base.dcid_len h)} ->
    last: Prims.nat{last + 1 < Prims.pow2 62} ->
    p:
      QUIC.Spec.Crypto.pbytes' (QUIC.Spec.Header.Base.is_retry h)
        { QUIC.Spec.Header.Base.has_payload_length h ==>
          QUIC.Secret.Int.Base.v (QUIC.Spec.Header.Base.payload_length h) ==
          FStar.Seq.Base.length p + Spec.Agile.AEAD.tag_length a }
  -> FStar.Pervasives.Lemma
      (requires
        ~(QUIC.Spec.Header.Base.is_retry h) ==>
        QUIC.Spec.PacketNumber.Base.in_window (QUIC.Secret.Int.Base.v (QUIC.Spec.Header.Base.pn_length
                  h) -
            1)
          last
          (QUIC.Secret.Int.Base.v (QUIC.Spec.Header.Base.packet_number h)))
      (ensures
        QUIC.Spec.decrypt a k siv hpk last cid_len (QUIC.Spec.encrypt a k siv hpk h p) ==
        QUIC.Spec.Success h p FStar.Seq.Base.empty)