val writer_leak (#k: unsafe_id) (w: stream_writer k) : key_t w
let writer_leak (#k:unsafe_id) (w:stream_writer k) : key_t w =
  Model.Helpers.reveal #(SAE.key_length (writer_ae_info w).AEAD.alg) (AEAD.wkey (writer_aead_state w)),
  Model.Helpers.reveal #(PNE.key_len (writer_pne_info w)) (PNE.key (writer_pne_state w))
val writer_leak (#k: unsafe_id) (w: stream_writer k) : key_t w
let writer_leak (#k: unsafe_id) (w: stream_writer k) : key_t w =
Model.Helpers.reveal #(SAE.key_length (writer_ae_info w).AEAD.alg) (AEAD.wkey (writer_aead_state w)),
Model.Helpers.reveal #(PNE.key_len (writer_pne_info w)) (PNE.key (writer_pne_state w))
Model.QUIC.fsti.checked
Spec.Agile.Cipher.fsti.checked Spec.Agile.AEAD.fsti.checked QUIC.UInt62.fst.checked QUIC.Spec.PacketNumber.Base.fst.checked QUIC.Spec.Header.Parse.fsti.checked QUIC.Spec.Header.Base.fst.checked QUIC.Spec.Header.fsti.checked QUIC.Spec.fsti.checked QUIC.Secret.Int.fsti.checked prims.fst.checked Model.PNE.fsti.checked Model.Indexing.fsti.checked Model.Helpers.fsti.checked Model.AEAD.fsti.checked Mem.fst.checked LowStar.Modifies.fst.checked LowParse.BitFields.fsti.checked Lib.RawIntTypes.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt128.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.fst.checked
Model.QUIC.fsti
Model.QUIC.unsafe_id Model.QUIC.stream_writer FStar.Pervasives.Native.Mktuple2 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 Model.Helpers.reveal Model.AEAD.wkey FStar.Pervasives.dfst Model.QUIC.writer_aead_state Model.PNE.key Model.QUIC.writer_pne_state Model.QUIC.key_t
module Model.QUIC

module HS = FStar.HyperStack
module I = Model.Indexing
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module U128 = FStar.UInt128
module M = LowStar.Modifies

module Spec = QUIC.Spec
module QH = QUIC.Spec.Header
module AE = Model.AEAD
module SAE = Spec.Agile.AEAD
module PNE = Model.PNE
module SPNE = Spec.Agile.Cipher
module BF = LowParse.BitFields
module U62 = QUIC.UInt62
module Secret = QUIC.Secret.Int

open FStar.UInt32
open Mem

type id = i:AE.id & j:PNE.id{PNE.is_safe j <==> AEAD.is_safe i}

let safe (i:id) = AEAD.is_safe (dfst i)
let safe_id = i:id{safe i}
let unsafe (i:id) = not (safe i)
let unsafe_id = i:id{unsafe i}

/// Package for QUIC plaintexts
/// (i.e. the payload of QUIC packets)
/// This would be implemented as a serializable list of frames
/// (using EverParse refined lists)

type qplain_len = n:AEAD.plain_length_at_least 3{n < Spec.max_plain_length}
let pnl = PNE.pne_plain_length

val pne_pkg: PNE.pne_plain_pkg

noeq type info = {
  region: r:subq{r `HS.disjoint` q_ae_region};
}

let max_ctr = pow2 62 - 1
type epn (nl:pnl) = Spec.lbytes nl
type pn = n:nat{n <= max_ctr}
type rpn = n:U64.t{U64.v n < max_ctr}
let rpn_of_nat (j:nat{j < max_ctr}) : rpn = U64.uint_to_t j

val stream_writer: (k:id) -> Type u#1
val stream_reader: #k:id -> w:stream_writer k -> Type u#1
val writer_info: #k:id -> w:stream_writer k -> info
val reader_info: #k:id -> #w:stream_writer k -> r:stream_reader w -> i:info{i == writer_info w}

val writer_ae_info: #k:id -> w:stream_writer k -> a:AEAD.info (dfst k){a.AEAD.min_len == 3}
val reader_ae_info: #k:id -> #w:stream_writer k -> r:stream_reader w -> a:AEAD.info (dfst k){a.AEAD.min_len == 3}
val writer_pne_info: #k:id -> w:stream_writer k -> a:PNE.info (dsnd k){a.PNE.calg == Spec.Agile.AEAD.cipher_alg_of_supported_alg (writer_ae_info w).AEAD.alg /\ a.PNE.halg == (writer_ae_info w).AEAD.halg}
val reader_pne_info: #k:id -> #w:stream_writer k -> r:stream_reader w -> a:PNE.info (dsnd k){a.PNE.calg == Spec.Agile.AEAD.cipher_alg_of_supported_alg (reader_ae_info r).AEAD.alg /\ a.PNE.halg == (reader_ae_info r).AEAD.halg}

val writer_aead_state : (#k:id) -> (w:stream_writer k) ->
  aw:AEAD.aead_writer (dfst k)
val reader_aead_state : #k:id -> #w:stream_writer k -> r:stream_reader w ->
  ar:AEAD.aead_reader (writer_aead_state w)
val writer_pne_state : #k:id -> w:stream_writer k -> PNE.pne_state (writer_pne_info w)
val reader_pne_state : #k:id -> #w:stream_writer k -> r:stream_reader w -> PNE.pne_state (reader_pne_info r)

type key_t #i (w:stream_writer i) =
  Spec.lbytes (SAE.key_length (writer_ae_info w).AEAD.alg) &
  Spec.lbytes (PNE.key_len (writer_pne_info w))
val writer_leak (#k: unsafe_id) (w: stream_writer k) : key_t w
w: Model.QUIC.stream_writer k -> Model.QUIC.key_t w