val decrypt_post
      (i: index)
      (s: state i)
      (dst: B.pointer 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 /\ incrementable s h0)
      (ensures fun _ -> True)
val decrypt_post
      (i: index)
      (s: state i)
      (dst: B.pointer 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 /\ incrementable s h0)
      (ensures fun _ -> True)
let decrypt_post (i: index)
  (s:state i)
  (dst: B.pointer 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 /\
    incrementable s h0)
  (ensures fun _ -> True)
=
  let max (x y: nat) : Tot nat = if x >= y then x else y in
  let k = derive_k i s h0 in
  let iv = derive_iv i s h0 in
  let pne = derive_pne i s h0 in
  let prev = g_last_packet_number (B.deref h0 s) h0 in
  invariant h1 s /\
  footprint_s h1 (B.deref h1 s) == footprint_s h0 (B.deref h0 s) /\
  begin
    let r = B.deref h1 dst 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 (B.deref h1 s) h1) == max (Secret.v prev) (Secret.v r.Base.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 Spec.decrypt i.aead_alg k iv pne (Secret.v prev) (U8.v cid_len) (B.as_seq h0 packet) with
      | Spec.Success h' plain' rem' ->
        h' == g_header r.header h1 r.Base.pn /\
        fmt == QUIC.Spec.Header.Parse.format_header h' /\
        plain' == plain /\
        rem' == rem
      | _ -> False
    ))
    | DecodeError ->
      Spec.Failure? (Spec.decrypt i.aead_alg k iv pne (Secret.v prev) (U8.v cid_len) (B.as_seq h0 packet))
    | AuthenticationFailure ->
      Spec.Failure? (Spec.decrypt i.aead_alg 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
module QUIC.State

open EverCrypt.Error
include QUIC.Spec.Crypto
include QUIC.Impl.Header.Base

module B = LowStar.Buffer
module HS = FStar.HyperStack
module Seq = QUIC.Secret.Seq
module PN = QUIC.Spec.PacketNumber.Base
module HST = FStar.HyperStack.ST
module Secret = QUIC.Secret.Int
module G = FStar.Ghost
module U8 = FStar.UInt8
module U32 = FStar.UInt32
module Base = QUIC.Impl.Header.Base
module Spec = QUIC.Spec

#set-options "--z3rlimit 16"

/// This is not a cryptographic index; rather, this is just a regular type
/// index, where instead of indexing on a single algorithm (like, say, AEAD), we
/// index on two values.
///
/// The record is here to limit the profileration of hide/reveal in the stateful
/// functions, and to give easier projectors (, ).
type index = {
  hash_alg: ha;
  aead_alg: ea
}


/// Boilerplate
/// -----------

[@CAbstractStruct]
val state_s: index -> Type0

let state i = B.pointer (state_s i)

val footprint_s: #i:index -> HS.mem -> state_s i -> GTot B.loc
let footprint (#i:index) (m: HS.mem) (s: state i) =
  B.(loc_union (loc_addr_of_buffer s) (footprint_s m (B.deref m s)))

let loc_includes_union_l_footprint_s
  (m: HS.mem)
  (l1 l2: B.loc) (#a: index) (s: state_s a)
: Lemma
  (requires (
    B.loc_includes l1 (footprint_s m s) \/ B.loc_includes l2 (footprint_s m s)
  ))
  (ensures (B.loc_includes (B.loc_union l1 l2) (footprint_s m s)))
  [SMTPat (B.loc_includes (B.loc_union l1 l2) (footprint_s m s))]
= B.loc_includes_union_l l1 l2 (footprint_s m s)

/// Ghost accessors (not needing the invariant)
/// -------------------------------------------
///
/// We need to define those, so that we can state a framing lemma for them.
/// Attempting a new convention to distinguish ghost accessors from stateful
/// functions: a ``g_`` prefix.

/// See remark for ``g_initial_packet_number`` below.
val g_traffic_secret: #i:index -> (s: state_s i) ->
  GTot (Spec.Hash.Definitions.bytes_hash i.hash_alg)

#push-options "--max_ifuel 1" // inversion on hash_alg
let hash_is_keysized #i (s: state_s i): Lemma
  (ensures (keysized i.hash_alg (Seq.length (g_traffic_secret s))))
  [ SMTPat (g_traffic_secret s) ]
=
  assert_norm (512 < pow2 61);
  assert_norm (512 < pow2 125)
#pop-options

/// Note that this one does *NOT* take the memory as an argument. (This is
/// because the initial packet number is erased in the concrete state.) Callers
/// should be able to derive, from this, that the initial packet number remains
/// the same, thanks to the precise use of footprint_s in encrypt/decrypt.
val g_initial_packet_number: #i:index -> (s: state_s i) -> GTot PN.packet_number_t

/// Invariant
/// ---------

val invariant_s: (#i:index) -> HS.mem -> state_s i -> Type0
let invariant (#i:index) (m: HS.mem) (s: state i) =
  let r = B.frameOf s in
  HST.is_eternal_region r /\
  B.loc_includes (B.loc_region_only true r) (footprint m s) /\
  B.live m s /\
  B.(loc_disjoint (loc_addr_of_buffer s) (footprint_s m (B.deref m s))) /\
  invariant_s m (B.get m s 0)

val invariant_loc_in_footprint
  (#i: index)
  (s: state i)
  (m: HS.mem)
: Lemma
  (requires (invariant m s))
  (ensures (B.loc_in (footprint m s) m))
  [SMTPat (invariant m s)]


/// Ghost accessors needing the invariant
/// -------------------------------------

val g_last_packet_number: #i:index -> (s: state_s i) -> (h: HS.mem { invariant_s h s }) ->
  GTot (pn: PN.packet_number_t {
    Secret.v pn >= Secret.v (g_initial_packet_number s)
  })

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

/// Preserving all the ghost accessors via a single framing lemma only works
/// because we don't do stack allocation. See comments in
/// EverCrypt.Hash.Incremental.
val frame_invariant: #i:index -> l:B.loc -> s:state i -> h0:HS.mem -> h1:HS.mem -> Lemma
  (requires (
    invariant h0 s /\
    B.loc_disjoint l (footprint h0 s) /\
    B.modifies l h0 h1))
  (ensures (
    invariant h1 s /\
    footprint h0 s == footprint h1 s /\
    g_last_packet_number (B.deref h0 s) h0 == g_last_packet_number (B.deref h1 s) h0 /\
    g_traffic_secret (B.deref h0 s) == g_traffic_secret (B.deref h1 s)
    ))
  // Assertion failure: unexpected pattern term
  [ SMTPatOr [
    [ SMTPat (B.modifies l h0 h1); SMTPat (invariant h1 s) ];
    [ SMTPat (B.modifies l h0 h1); SMTPat (footprint h1 s) ];
    [ SMTPat (B.modifies l h0 h1); SMTPat (g_last_packet_number (B.deref h1 s)) ];
    [ SMTPat (B.modifies l h0 h1); SMTPat (g_traffic_secret (B.deref h1 s)) ]
  ] ]



/// Actual stateful API
/// -------------------

val aead_alg_of_state (#i: G.erased index) (s: state (G.reveal i)): HST.Stack ea
  (requires (fun h0 -> invariant #(G.reveal i) h0 s))
  (ensures (fun h0 a h1 ->
    a == (G.reveal i).aead_alg /\
    h0 == h1))

val hash_alg_of_state (#i: G.erased index) (s: state (G.reveal i)): HST.Stack ha
  (requires (fun h0 -> invariant #(G.reveal i) h0 s))
  (ensures (fun h0 a h1 ->
    a == (G.reveal i).hash_alg /\
    h0 == h1))

val last_packet_number_of_state (#i: G.erased index) (s: state (G.reveal i)): HST.Stack PN.packet_number_t
  (requires fun h0 -> invariant h0 s)
  (ensures fun h0 ctr h1 ->
    ctr == g_last_packet_number (B.deref h0 s) h0 /\
    h0 == h1)

// : we could be defensive and allow callers to pass potentially unsupported
// algorithms; however, this would require a lot more machinery as we would not
// even be able to state the index type, since index currently has a refinement
// that the two algorithms are supported. We would have to separate index into
// index0 and a well-formedness refinement. Not sure it's worth it. We can
// always perform redundant tests inside the definition of create to be fully
// defensive.
inline_for_extraction noextract
let create_in_st (i:index) =
  r:HS.rid ->
  dst: B.pointer (B.pointer_or_null (state_s i)) ->
  initial_pn:PN.packet_number_t ->
  traffic_secret:B.buffer Secret.uint8 {
    B.length traffic_secret = Spec.Hash.Definitions.hash_length i.hash_alg
  } ->
  HST.ST error_code
    (requires fun h0 ->
      // : we could require that ``dst`` point to NULL prior to calling
      // ``create`` (otherwise, it's a memory leak). Other modules don't enforce
      // this (see AEAD) so for now, let's make the caller's life easier and not
      // demand anything.
      HST.is_eternal_region r /\
      B.live h0 dst /\ B.live h0 traffic_secret /\
      B.disjoint dst traffic_secret)
    (ensures (fun h0 e h1 ->
      match e with
      | UnsupportedAlgorithm ->
          B.(modifies loc_none h0 h1)
      | Success ->
          let s = B.deref h1 dst in
          not (B.g_is_null s) /\
          invariant h1 s /\

          B.(modifies (loc_buffer dst) h0 h1) /\
          B.fresh_loc (footprint h1 s) h0 h1 /\

          g_traffic_secret (B.deref h1 s) == B.as_seq h0 traffic_secret /\ 
          g_last_packet_number (B.deref h1 s) h1 == initial_pn /\

          g_initial_packet_number (B.deref h1 s) == initial_pn
      | _ ->
          False))

// The index is passed at run-time.
val create_in: i:index -> create_in_st i


(* Useful shortcuts *)

let derive_k
  (i: index)
  (s: state i)
  (h: HS.mem)
: GTot (Seq.seq Secret.uint8)
=
  let s0 = g_traffic_secret (B.deref h s) in
  Spec.derive_secret i.hash_alg s0 Spec.label_key (Spec.Agile.AEAD.key_length i.aead_alg)

let derive_iv
  (i: index)
  (s: state i)
  (h: HS.mem)
: GTot (Seq.seq Secret.uint8)
= let s0 = g_traffic_secret (B.deref h s) in
  Spec.derive_secret i.hash_alg s0 Spec.label_iv 12

let derive_pne
  (i: index)
  (s: state i)
  (h: HS.mem)
: GTot (Seq.seq Secret.uint8)
= let s0 = g_traffic_secret (B.deref h s) in
  Spec.derive_secret i.hash_alg s0 Spec.label_hp (cipher_keysize i.aead_alg)

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: header ->
  plain: B.buffer Secret.uint8 ->
  plain_len: U32.t ->
  HST.Stack error_code
    (requires fun h0 ->
      // Memory & preservation
      B.live h0 plain /\ B.live h0 dst /\ B.live h0 dst_pn /\
      header_live h h0 /\
      B.(all_disjoint [ footprint h0 s; loc_buffer dst; loc_buffer dst_pn; header_footprint h; loc_buffer plain ]) /\
      invariant h0 s /\
      incrementable s h0 /\
      B.length plain == U32.v plain_len /\ (
      let clen = if is_retry h then 0 else U32.v plain_len + Spec.Agile.AEAD.tag_length i.aead_alg in
      (if is_retry h then U32.v plain_len == 0 else 3 <= U32.v plain_len /\ U32.v plain_len < Spec.max_plain_length) /\
      (has_payload_length h ==> Secret.v (payload_length h) == clen) /\
      B.length dst == Secret.v (header_len h) + clen
    ))
    (ensures fun h0 r h1 ->
      match r with
      | Success ->
          // Memory & preservation
          B.(modifies (footprint_s h0 (deref h0 s) `loc_union` loc_buffer dst `loc_union` loc_buffer dst_pn)) h0 h1 /\
          invariant h1 s /\
          footprint_s h1 (B.deref h1 s) == footprint_s h0 (B.deref h0 s) /\ (
          // Functional correctness
          let k = derive_k i s h0 in
          let iv = derive_iv i s h0 in
          let pne = derive_pne i s h0 in
          let plain = B.as_seq h0 plain in
          let packet: packet = B.as_seq h1 dst in
          let pn = g_last_packet_number (B.deref h0 s) h0 `Secret.add` Secret.to_u64 1uL in
          B.deref h1 dst_pn == pn /\
          packet == Spec.encrypt i.aead_alg k iv pne (g_header h h0 pn) (Seq.seq_reveal plain) /\
          g_last_packet_number (B.deref h1 s) h1 == pn)
      | _ ->
          False))

val initial_secrets (dst_client: B.buffer Secret.uint8)
  (dst_server: B.buffer Secret.uint8)
  (cid: B.buffer Secret.uint8)
  (cid_len: U32.t):
  HST.Stack unit
    (requires (fun h0 ->
      B.(all_live h0 [ buf dst_client; buf dst_server; buf cid ]) /\
      B.length dst_client = Spec.Agile.Hash.(hash_length SHA2_256) /\
      B.length dst_server = Spec.Agile.Hash.(hash_length SHA2_256) /\
      B.length cid = U32.v cid_len /\
      U32.v cid_len <= 20 /\
      B.(all_disjoint [ loc_buffer dst_client; loc_buffer dst_server; loc_buffer cid ])))
    (ensures (fun h0 _ h1 ->
      B.(modifies (loc_buffer dst_client `loc_union` loc_buffer dst_server) h0 h1)))
/
Spec.Hash.Definitions.fst.checked Spec.Agile.Hash.fsti.checked Spec.Agile.AEAD.fsti.checked QUIC.Spec.PacketNumber.Base.fst.checked QUIC.Spec.Header.Parse.fsti.checked QUIC.Spec.Crypto.fsti.checked QUIC.Spec.fsti.checked QUIC.Secret.Seq.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.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked EverCrypt.Error.fsti.checked
QUIC.State.fsti

    i: QUIC.State.index ->
    s: QUIC.State.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
QUIC.State.index QUIC.State.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.State.invariant Prims.eq2 LowStar.Monotonic.Buffer.loc QUIC.State.footprint_s LowStar.Monotonic.Buffer.deref QUIC.State.state_s LowStar.Buffer.trivial_preorder Prims.int Prims.l_or Lib.IntTypes.range Lib.IntTypes.U64 Prims.b2t Prims.op_GreaterThanOrEqual QUIC.Secret.Int.Base.v Lib.IntTypes.SEC QUIC.State.g_last_packet_number QUIC.Impl.Header.Base.__proj__Mkresult__item__pn 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.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.State.__proj__Mkindex__item__aead_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.State.g_initial_packet_number LowStar.Monotonic.Buffer.get Lib.IntTypes.int_t Lib.IntTypes.U8 QUIC.State.derive_pne QUIC.State.derive_iv QUIC.State.derive_k Prims.nat Prims.bool FStar.UInt.size FStar.UInt32.n FStar.UInt32.v QUIC.State.incrementable Prims.l_True
let decrypt_post
      (i: index)
      (s: state i)
      (dst: B.pointer 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 /\ incrementable s h0)
      (ensures fun _ -> True) =
  
let max (x y: nat) : Tot nat = if x >= y then x else y in
let k = derive_k i s h0 in
let iv = derive_iv i s h0 in
let pne = derive_pne i s h0 in
let prev = g_last_packet_number (B.deref h0 s) h0 in
invariant h1 s /\ footprint_s h1 (B.deref h1 s) == footprint_s h0 (B.deref h0 s) /\
(let r = B.deref h1 dst in
  match res with
  | Success ->
    Secret.v (g_last_packet_number (B.deref h1 s) h1) == max (Secret.v prev) (Secret.v r.Base.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
          Spec.decrypt i.aead_alg k iv pne (Secret.v prev) (U8.v cid_len) (B.as_seq h0 packet)
        with
        | Spec.Success h' plain' rem' ->
          h' == g_header r.header h1 r.Base.pn /\ fmt == QUIC.Spec.Header.Parse.format_header h' /\
          plain' == plain /\ rem' == rem
        | _ -> False))
  | DecodeError ->
    Spec.Failure? (Spec.decrypt i.aead_alg
          k
          iv
          pne
          (Secret.v prev)
          (U8.v cid_len)
          (B.as_seq h0 packet))
  | AuthenticationFailure ->
    Spec.Failure? (Spec.decrypt i.aead_alg
          k
          iv
          pne
          (Secret.v prev)
          (U8.v cid_len)
          (B.as_seq h0 packet)) /\ Secret.v r.total_len <= B.length packet
  | _ -> False)