val derived : r: Model.QUIC.stream_reader w -> ts: QUIC.itraffic_secret i -> Prims.logical
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
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
/
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
r: Model.QUIC.stream_reader w -> ts: QUIC.itraffic_secret i -> Prims.logical
Model.QUIC.id Model.QUIC.stream_writer Model.QUIC.stream_reader QUIC.itraffic_secret Prims.op_AmpAmp Model.Flags.model Model.QUIC.unsafe QUIC.Spec.Base.lbytes Spec.Agile.AEAD.key_length Model.AEAD.__proj__Mkinfo'__item__alg Model.QUIC.writer_ae_info Model.PNE.key_len FStar.Pervasives.dsnd Model.AEAD.id Model.PNE.id Prims.l_iff Prims.b2t Model.PNE.is_safe Model.AEAD.is_safe Model.QUIC.writer_pne_info Prims.l_and Prims.eq2 FStar.Seq.Base.seq Lib.IntTypes.uint8 Model.Helpers.hide Model.QUIC.writer_static_iv QUIC.Spec.Crypto.derive_secret QUIC.Spec.Crypto.label_iv QUIC.Spec.Crypto.label_key QUIC.Spec.Crypto.cipher_keysize QUIC.Spec.Crypto.label_hp Prims.logical Model.QUIC.key_t Model.QUIC.reader_leak Model.Indexing.ea Model.Indexing.ae_id_ginfo FStar.Pervasives.dfst Model.Indexing.ae_id_info Model.Indexing.ha Model.Indexing.ae_id_ghash Model.Indexing.ae_id_hash Prims.bool Prims.l_True
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