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)
  })
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 g_next_packet_number #i s h =
  assert_norm (pow2 62 - 1 < pow2 64);
  if I.model then
    Lib.IntTypes.u64 (QModel.wctrT #(mid i) (mstate s).writer h)
  else
    QImpl.g_last_packet_number (B.deref h (istate s)) h
module QUIC

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

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

// The switch only makes sense in the non-ideal case. (Unsurprisingly: if we
// replace data by random values, functional correctness no longer holds!)
let index =
  if I.model then i:QModel.id { QModel.unsafe i } else QImpl.index

let mid (i:index{I.model}) = i <: QModel.id
let iid (i:index{not I.model}) = i <: QImpl.index

let alg (i:index) =
  if I.model then I.ae_id_ginfo (dfst (mid i))
  else (iid i).QImpl.aead_alg

let halg (i:index) =
  if I.model then I.ae_id_ghash (dfst (mid i))
  else (iid i).QImpl.hash_alg

let itraffic_secret (i:QModel.id) =
  Spec.Hash.Definitions.bytes_hash (I.ae_id_ghash (dfst i))

module MH = Model.Helpers

let derived (#i:QModel.id) (#w:QModel.stream_writer i) (r:QModel.stream_reader w) (ts:itraffic_secret i) =
  if I.model && QModel.unsafe i then
    let ha = I.ae_id_hash (dfst i) in
    let ea = I.ae_id_info (dfst i) in
    let (k1, k2) = QModel.reader_leak r in
    MH.hide (QModel.writer_static_iv w) ==
      QSpec.derive_secret ha ts QSpec.label_iv 12 /\
    MH.hide k1 == QSpec.derive_secret ha ts
        QSpec.label_key (QSpec.cipher_keysize ea) /\
    MH.hide k2 == QUIC.Spec.derive_secret ha ts
        QUIC.Spec.label_hp (QSpec.cipher_keysize ea)
  else True

noeq type mstate_t i =
| Ideal:
  writer: QModel.stream_writer i ->
  reader: QModel.stream_reader writer ->
  ts: itraffic_secret i{derived reader ts} -> // FIXME erased
  mstate_t i

let istate_t i = QImpl.state i

noeq
type raise (i: index { not I.model }): Type u#1 = | Raise: s:istate_t i -> raise i

let state i =
  if I.model then mstate_t (mid i)
  else raise (iid i)

let mstate (#i:index{I.model}) (s:state i) = s <: mstate_t (mid i)
let istate (#i:index{not I.model}) (s:state i) = (s <: raise (iid i)).s

let footprint #i h s =
  if I.model then
    QModel.rfootprint (mstate s).reader `B.loc_union` QModel.footprint (mstate s).writer
  else QImpl.footprint h (istate s)

let invariant #i h s =
  if I.model then
    let Ideal writer reader _ = mstate s in
    QModel.invariant writer h /\ QModel.rinvariant reader h /\
    B.loc_disjoint (QModel.rfootprint (mstate s).reader) (QModel.footprint (mstate s).writer)
  else QImpl.invariant h (istate s)

let g_traffic_secret #i s h =
  if I.model then (mstate s).ts
  else
    QImpl.g_traffic_secret (B.deref h (istate s))

let g_initial_packet_number #i s h =
  assert_norm (pow2 62 - 1 < pow2 64);
  if I.model then
    Lib.IntTypes.u64 (QModel.writer_offset #(mid i) (mstate s).writer)
  else
    QImpl.g_initial_packet_number (B.deref h (istate s))

let g_last_packet_number #i s h =
  assert_norm (pow2 62 - 1 < pow2 64);
  if I.model then
    Lib.IntTypes.u64 (QModel.expected_pnT #(mid i) (mstate s).reader h)
  else
    QImpl.g_last_packet_number (B.deref h (istate s)) h
/
Spec.Hash.Definitions.fst.checked Spec.Agile.AEAD.fsti.checked QUIC.State.fsti.checked QUIC.Spec.Header.Base.fst.checked QUIC.Spec.fsti.checked QUIC.Secret.Seq.fsti.checked QUIC.Impl.Header.Base.fst.checked QUIC.Impl.fsti.checked prims.fst.checked Model.QUIC.fsti.checked Model.Indexing.fsti.checked Model.Helpers.fsti.checked Model.AEAD.fsti.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked LowParse.SLow.Base.fst.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Calc.fsti.checked FStar.Bytes.fsti.checked EverCrypt.Helpers.fsti.checked EverCrypt.Error.fsti.checked
QUIC.fst
s: QUIC.state i -> h: FStar.Monotonic.HyperStack.mem{QUIC.invariant h s}
  -> Prims.GTot
    (pn:
      QUIC.Spec.PacketNumber.Base.packet_number_t
        {QUIC.Secret.Int.Base.v pn >= QUIC.Secret.Int.Base.v (QUIC.g_initial_packet_number s h)})
QUIC.index QUIC.state FStar.Monotonic.HyperStack.mem QUIC.invariant Model.Flags.model Lib.IntTypes.u64 Model.QUIC.wctrT QUIC.mid QUIC.__proj__Ideal__item__writer QUIC.mstate Prims.bool QUIC.State.g_last_packet_number QUIC.iid LowStar.Monotonic.Buffer.deref QUIC.State.state_s LowStar.Buffer.trivial_preorder QUIC.istate QUIC.Spec.PacketNumber.Base.packet_number_t Prims.b2t Prims.op_GreaterThanOrEqual QUIC.Secret.Int.Base.v Lib.IntTypes.U64 Lib.IntTypes.SEC QUIC.g_initial_packet_number Prims.unit FStar.Pervasives.assert_norm Prims.op_LessThan Prims.op_Subtraction Prims.pow2
let g_next_packet_number #i s h =
  
assert_norm (pow2 62 - 1 < pow2 64);
if I.model
then Lib.IntTypes.u64 (QModel.wctrT #(mid i) (mstate s).writer h)
else QImpl.g_last_packet_number (B.deref h (istate s)) h