val encrypt_post
      (a: ea)
      (aead: AEAD.state a)
      (siv: B.buffer Secret.uint8)
      (ctr: CTR.state (SAEAD.cipher_alg_of_supported_alg a))
      (hpk: B.buffer Secret.uint8)
      (dst: B.buffer U8.t)
      (h: header)
      (pn: PN.packet_number_t)
      (plain: B.buffer Secret.uint8)
      (plain_len: Secret.uint32)
      (m: HS.mem)
      (res: error_code)
      (m': HS.mem)
    : GTot Type0
let encrypt_post
  (a: ea)
  (aead: AEAD.state a)
  (siv: B.buffer Secret.uint8)
  (ctr: CTR.state (SAEAD.cipher_alg_of_supported_alg a))
  (hpk: B.buffer Secret.uint8)
  (dst: B.buffer U8.t)
  (h: header)
  (pn: PN.packet_number_t)
  (plain: B.buffer Secret.uint8)
  (plain_len: Secret.uint32)
  (m: HS.mem)
  (res: error_code)
  (m' : HS.mem)
: GTot Type0
=
  encrypt_pre a aead siv ctr hpk dst h pn plain plain_len m /\
  B.modifies (B.loc_buffer dst `B.loc_union` AEAD.footprint m aead `B.loc_union` CTR.footprint m ctr) m m' /\
  AEAD.invariant m' aead /\ AEAD.footprint m' aead == AEAD.footprint m aead /\
  AEAD.preserves_freeable aead m m' /\
  AEAD.as_kv (B.deref m' aead) == AEAD.as_kv (B.deref m aead) /\
  CTR.invariant m' ctr /\ CTR.footprint m' ctr == CTR.footprint m ctr /\
  B.as_seq m' dst `Seq.equal` Spec.encrypt a (AEAD.as_kv (B.deref m aead)) (B.as_seq m siv) (B.as_seq m hpk) (g_header h m pn) (Seq.seq_reveal (B.as_seq m plain)) /\
  res == Success
val encrypt_post
      (a: ea)
      (aead: AEAD.state a)
      (siv: B.buffer Secret.uint8)
      (ctr: CTR.state (SAEAD.cipher_alg_of_supported_alg a))
      (hpk: B.buffer Secret.uint8)
      (dst: B.buffer U8.t)
      (h: header)
      (pn: PN.packet_number_t)
      (plain: B.buffer Secret.uint8)
      (plain_len: Secret.uint32)
      (m: HS.mem)
      (res: error_code)
      (m': HS.mem)
    : GTot Type0
let encrypt_post
      (a: ea)
      (aead: AEAD.state a)
      (siv: B.buffer Secret.uint8)
      (ctr: CTR.state (SAEAD.cipher_alg_of_supported_alg a))
      (hpk: B.buffer Secret.uint8)
      (dst: B.buffer U8.t)
      (h: header)
      (pn: PN.packet_number_t)
      (plain: B.buffer Secret.uint8)
      (plain_len: Secret.uint32)
      (m: HS.mem)
      (res: error_code)
      (m': HS.mem)
    : GTot Type0 =
encrypt_pre a aead siv ctr hpk dst h pn plain plain_len m /\
B.modifies (((B.loc_buffer dst) `B.loc_union` (AEAD.footprint m aead))
    `B.loc_union`
    (CTR.footprint m ctr))
  m
  m' /\ AEAD.invariant m' aead /\ AEAD.footprint m' aead == AEAD.footprint m aead /\
AEAD.preserves_freeable aead m m' /\ AEAD.as_kv (B.deref m' aead) == AEAD.as_kv (B.deref m aead) /\
CTR.invariant m' ctr /\ CTR.footprint m' ctr == CTR.footprint m ctr /\
(B.as_seq m' dst)
`Seq.equal`
(Spec.encrypt a
    (AEAD.as_kv (B.deref m aead))
    (B.as_seq m siv)
    (B.as_seq m hpk)
    (g_header h m pn)
    (Seq.seq_reveal (B.as_seq m plain))) /\ res == Success
QUIC.Impl.fsti.checked
Spec.Agile.HKDF.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.fsti.checked QUIC.Secret.Seq.fsti.checked QUIC.Secret.Int.fsti.checked QUIC.Impl.Header.Base.fst.checked QUIC.Impl.Crypto.fsti.checked prims.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.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.HKDF.fsti.checked EverCrypt.Helpers.fsti.checked EverCrypt.Error.fsti.checked EverCrypt.CTR.fsti.checked EverCrypt.Cipher.fsti.checked EverCrypt.AEAD.fsti.checked
QUIC.Impl.fsti
QUIC.Spec.Crypto.ea EverCrypt.AEAD.state LowStar.Buffer.buffer Lib.IntTypes.uint8 NotEverCrypt.CTR.state Spec.Agile.AEAD.cipher_alg_of_supported_alg FStar.UInt8.t QUIC.Impl.Header.Base.header QUIC.Spec.PacketNumber.Base.packet_number_t Lib.IntTypes.uint32 FStar.Monotonic.HyperStack.mem EverCrypt.Error.error_code Prims.l_and QUIC.Impl.encrypt_pre LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_union LowStar.Monotonic.Buffer.loc_buffer LowStar.Buffer.trivial_preorder EverCrypt.AEAD.footprint NotEverCrypt.CTR.footprint EverCrypt.AEAD.invariant Prims.eq2 LowStar.Monotonic.Buffer.loc EverCrypt.AEAD.preserves_freeable Spec.Agile.AEAD.kv EverCrypt.AEAD.as_kv LowStar.Monotonic.Buffer.deref EverCrypt.AEAD.state_s NotEverCrypt.CTR.invariant FStar.Seq.Base.equal LowStar.Monotonic.Buffer.as_seq QUIC.Spec.encrypt QUIC.Impl.Header.Base.g_header QUIC.Secret.Seq.seq_reveal Lib.IntTypes.U8 Lib.IntTypes.SEC EverCrypt.Error.Success
/// An implementation of QUIC.Spec.fst that is concerned only with functional
/// correctness and side-channel resistance (no notion of model for now).
module QUIC.Impl
include QUIC.Impl.Crypto
include QUIC.Impl.Header.Base

module Spec = QUIC.Spec
module PN = QUIC.Spec.PacketNumber.Base
module Secret = QUIC.Secret.Int
module Seq = QUIC.Secret.Seq
module Parse = QUIC.Spec.Header.Parse

// This MUST be kept in sync with QUIC.Impl.fst...
module G = FStar.Ghost
module B = LowStar.Buffer
module S = FStar.Seq
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST


module Cipher = EverCrypt.Cipher
module AEAD = EverCrypt.AEAD
module HKDF = EverCrypt.HKDF
module CTR = EverCrypt.CTR

module SAEAD = Spec.Agile.AEAD
module SCipher = Spec.Agile.Cipher
module SHKDF = Spec.Agile.HKDF

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 "--z3rlimit 16"

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

type u2 = n:U8.t{U8.v n < 4}
type u4 = n:U8.t{U8.v n < 16}
type u62 = n:UInt64.t{UInt64.v n < pow2 62}

val dummy: unit

unfold
let encrypt_pre
  (a: ea)
  (aead: AEAD.state a)
  (siv: B.buffer Secret.uint8)
  (ctr: CTR.state (SAEAD.cipher_alg_of_supported_alg a))
  (hpk: B.buffer Secret.uint8)
  (dst: B.buffer U8.t)
  (h: header)
  (pn: PN.packet_number_t)
  (plain: B.buffer Secret.uint8)
  (plain_len: Secret.uint32) // should be secret, because otherwise one can compute the packet number length
  (m: HS.mem)
: GTot Type0
=
  let a' = SAEAD.cipher_alg_of_supported_alg a in
  B.all_disjoint [
    AEAD.footprint m aead;
    B.loc_buffer siv;
    CTR.footprint m ctr;
    B.loc_buffer hpk;
    B.loc_buffer dst;
    header_footprint h;
    B.loc_buffer plain;
  ] /\
  AEAD.invariant m aead /\
  B.live m siv /\ B.length siv == 12 /\
  CTR.invariant m ctr /\
  B.live m hpk /\ B.length hpk == SCipher.key_length a' /\
  B.live m dst /\
  header_live h m /\
  B.live m plain /\ B.length plain == Secret.v plain_len /\
  begin
    if is_retry h
    then
      B.length plain == 0 /\
      B.length dst == Secret.v (header_len h)
    else
      B.length dst == Secret.v (header_len h) + Secret.v plain_len + SAEAD.tag_length a /\
      3 <= Secret.v plain_len /\ Secret.v plain_len < max_plain_length
  end

unfold
let encrypt_post
  (a: ea)
  (aead: AEAD.state a)
  (siv: B.buffer Secret.uint8)
  (ctr: CTR.state (SAEAD.cipher_alg_of_supported_alg a))
  (hpk: B.buffer Secret.uint8)
  (dst: B.buffer U8.t)
  (h: header)
  (pn: PN.packet_number_t)
  (plain: B.buffer Secret.uint8)
  (plain_len: Secret.uint32)
  (m: HS.mem)
  (res: error_code)
  (m' : HS.mem)
: GTot Type0
val encrypt_post
      (a: ea)
      (aead: AEAD.state a)
      (siv: B.buffer Secret.uint8)
      (ctr: CTR.state (SAEAD.cipher_alg_of_supported_alg a))
      (hpk: B.buffer Secret.uint8)
      (dst: B.buffer U8.t)
      (h: header)
      (pn: PN.packet_number_t)
      (plain: B.buffer Secret.uint8)
      (plain_len: Secret.uint32)
      (m: HS.mem)
      (res: error_code)
      (m': HS.mem)
    : GTot Type0

    a: QUIC.Spec.Crypto.ea ->
    aead: EverCrypt.AEAD.state a ->
    siv: LowStar.Buffer.buffer Lib.IntTypes.uint8 ->
    ctr: NotEverCrypt.CTR.state (Spec.Agile.AEAD.cipher_alg_of_supported_alg a) ->
    hpk: LowStar.Buffer.buffer Lib.IntTypes.uint8 ->
    dst: LowStar.Buffer.buffer FStar.UInt8.t ->
    h: QUIC.Impl.Header.Base.header ->
    pn: QUIC.Spec.PacketNumber.Base.packet_number_t ->
    plain: LowStar.Buffer.buffer Lib.IntTypes.uint8 ->
    plain_len: Lib.IntTypes.uint32 ->
    m: FStar.Monotonic.HyperStack.mem ->
    res: EverCrypt.Error.error_code ->
    m': FStar.Monotonic.HyperStack.mem
  -> Prims.GTot Type0