val mstate : s: QUIC.state i -> QUIC.mstate_t (QUIC.mid i)
let mstate (#i:index{I.model}) (s:state i) = s <: mstate_t (mid i)
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)
/
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 -> QUIC.mstate_t (QUIC.mid i)
QUIC.index Prims.b2t Model.Flags.model QUIC.state QUIC.mstate_t QUIC.mid
let mstate (#i: index{I.model}) (s: state i) =
  
s <: mstate_t (mid i)