val rinvariant: #k:id -> #w:stream_writer k -> r:stream_reader w -> h:mem ->
  t:Type0{t ==> invariant w h}
val rinvariant: #k:id -> #w:stream_writer k -> r:stream_reader w -> h:mem ->
  t:Type0{t ==> invariant w h}
let rinvariant #k #w r h = invariant w h /\
  h `HS.contains` r.last /\
  AEAD.wfootprint w.ae `B.loc_disjoint` (B.loc_mreference w.ctr)
module Model.QUIC

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

friend QUIC.TotSpec

module Spec = QUIC.Spec
module TSpec = QUIC.TotSpec
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
module B = LowStar.Buffer

open FStar.HyperStack.ST
open FStar.UInt32
open Mem

let pne_plain (j:PNE.id) (l:pnl) : eqtype = Spec.lbytes l & PNE.length_bits l
let as_bytes (j:PNE.id) (l:pnl) (x:pne_plain j l) : GTot (Helpers.lbytes l & PNE.length_bits l) = let (n,b) = x in (Helpers.hide n, b)
let repr (j:PNE.unsafe_id) (l:pnl) (x:pne_plain j l) : b:(Helpers.lbytes l & PNE.length_bits l){b == as_bytes j l x} =
  let (n,b)=x in (Helpers.hide n, b)
let mk (j:PNE.id) (l:pnl) (n:Helpers.lbytes l) (b:PNE.length_bits l) : p:pne_plain j l{as_bytes j l p == (n,b)} = Helpers.reveal n,b

let extend (#l:pnl) (b:Spec.lbytes l) (l':pnl)
  : Spec.lbytes l' =
  if l' <= l then Seq.slice b 0 l'
  else Seq.append (Seq.create (l'-l) 0z) b

let pnenc (j:PNE.id) (l:pnl) (p:pne_plain j l) (c:PNE.pne_cipherpad)
  : (l':pnl & pne_plain j l') =
  let npn, bits = p in
  let pnm, bm = c in
  QUIC.UInt.lemma_logxor_lt #8 bits bm 5;
  let v = BF.get_bitfield #8 (bits `FStar.UInt.logxor` bm) 0 5 in
  BF.set_bitfield_bound bits 5 0 5 v;
  let bits' : PNE.bits = BF.set_bitfield bits 0 5 v in
  let ln : pnl = BF.get_bitfield bits' 0 2 + 1 in
  let npn' : Spec.lbytes ln = extend #l npn ln in    
  let npn'' = QUIC.Spec.Lemmas.xor_inplace npn' (Seq.slice (Helpers.reveal pnm) 0 ln) 0 in
  (| ln, (npn', bits') |)

let lemma_xor (j:PNE.id) (l:pnl) (p:(Spec.lbytes l & PNE.length_bits l)) (c:PNE.pne_cipherpad)
  : Lemma (requires True)
  (ensures (let (| l', b' |) = pnenc j l p c in
    let _, bits = as_bytes j l' b' in
    let l:pnl = LowParse.BitFields.get_bitfield bits 0 2 + 1 in
    l == (l' <: pnl)))
  = ()

// The (abstract) type of encrypted QUIC headers,
let pne_pkg =
  PNE.PNEPlainPkg pne_plain as_bytes repr mk pnenc lemma_xor

type _ctr (offset:pn) = p:pn{p >= offset}

noeq type stream_writer' (i:id) = 
| Writer:
  info: info ->
  offset: pn ->
  siv: Spec.lbytes 12 ->
  ae: AE.aead_writer (dfst i){(AEAD.wgetinfo ae).AEAD.min_len == 3} ->
  pne_info: PNE.info (dsnd i){
    pne_info.PNE.calg == Spec.Agile.AEAD.cipher_alg_of_supported_alg (AEAD.wgetinfo ae).AEAD.alg /\
    pne_info.PNE.halg == (AEAD.wgetinfo ae).AEAD.halg /\
    pne_info.PNE.plain == pne_pkg} ->
  pne: PNE.pne_state pne_info ->
  ctr: reference (_ctr offset) ->
  stream_writer' i

let stream_writer = stream_writer'

type _last (offset:pn) = p:nat{p >= offset /\ p < max_ctr}

noeq type stream_reader' (#i:id) (w:stream_writer i) = 
| Reader:
  aer: AE.aead_reader (w.ae) ->
  last: reference (_last w.offset) ->
  stream_reader' w

let stream_reader = stream_reader'

let writer_info #k w = w.info
let reader_info #k #w r = w.info

let writer_ae_info #k w = AEAD.wgetinfo w.ae
let reader_ae_info #k #w r = AEAD.rgetinfo r.aer
let writer_pne_info #k w = w.pne_info
let reader_pne_info #k #w r = w.pne_info

let writer_aead_state #k w = w.ae
let reader_aead_state #k #w r = r.aer

let writer_pne_state #k w = w.pne
let reader_pne_state #k #w r = w.pne

let nonce_of_ctr #i (w:stream_writer i) (n:nat{n < pow2 62 /\ n>=w.offset})
  : Tot AEAD.nonce
  =
  let _ = assert_norm(pow2 62 < pow2 (8 `op_Multiply` 12)) in
  let pn = FStar.Endianness.n_to_be 12 n in
  QUIC.Spec.Lemmas.xor_inplace pn w.siv 0

let nonce_of_ctr_injective
  #i (w:stream_writer i)
  (n1:nat{n1 < pow2 62 /\ n1>=w.offset})
  (n2:nat{n2 < pow2 62 /\ n2>=w.offset})
: Lemma
  (requires (nonce_of_ctr w n1 == nonce_of_ctr w n2))
  (ensures (n1 == n2))
=
  let _ = assert_norm(pow2 62 < pow2 (8 `op_Multiply` 12)) in
  let pn1 = FStar.Endianness.n_to_be 12 n1 in
  let pn2 = FStar.Endianness.n_to_be 12 n2 in
  QUIC.Spec.Lemmas.xor_inplace_involutive pn1 w.siv 0;
  QUIC.Spec.Lemmas.xor_inplace_involutive pn2 w.siv 0

let nonce_of_ctr_injective'
  #i (w:stream_writer i)
  (n1:nat{n1 < pow2 62 /\ n1>=w.offset})
  (n2:nat{n2 < pow2 62 /\ n2>=w.offset})
: Lemma
  (n1 <> n2 ==> nonce_of_ctr w n1 <> nonce_of_ctr w n2)
=
  Classical.move_requires (nonce_of_ctr_injective w n1) n2

let fresh_nonces_from
  (j: nat)
  (#k:id)
  (w:stream_writer k)
  (h:mem)
: GTot Type0
=
  (forall i. (i > j /\ safe k) ==>
    AEAD.fresh_nonce w.ae (nonce_of_ctr w i) h)

let fresh_nonces
  (#k:id)
  (w:stream_writer k)
  (h:mem)
: GTot Type0
= fresh_nonces_from (HS.sel h w.ctr) w h

let invariant #k w h =
  AEAD.winvariant w.ae h /\
  PNE.invariant w.pne h /\
  h `HS.contains` w.ctr /\
  fresh_nonces w h /\
  AEAD.wfootprint w.ae `B.loc_disjoint` (B.loc_mreference w.ctr) /\
  PNE.footprint w.pne `B.loc_disjoint` (B.loc_mreference w.ctr) /\
  PNE.footprint w.pne `B.loc_disjoint` AEAD.wfootprint w.ae
/
Spec.Agile.Cipher.fsti.checked Spec.Agile.AEAD.fsti.checked QUIC.UInt62.fst.checked QUIC.UInt.fst.checked QUIC.TotSpec.fst.checked QUIC.Spec.Lemmas.fst.checked QUIC.Spec.Header.Parse.fsti.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 LowStar.Buffer.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.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Endianness.fsti.checked FStar.Classical.fsti.checked
Model.QUIC.fst
r: Model.QUIC.stream_reader w -> h: FStar.Monotonic.HyperStack.mem
  -> t: Type0{t ==> Model.QUIC.invariant w h}
Model.QUIC.id Model.QUIC.stream_writer Model.QUIC.stream_reader FStar.Monotonic.HyperStack.mem Prims.l_and Model.QUIC.invariant FStar.Monotonic.HyperStack.contains Model.QUIC._last Model.QUIC.__proj__Writer__item__offset FStar.Heap.trivial_preorder Model.QUIC.__proj__Reader__item__last LowStar.Monotonic.Buffer.loc_disjoint Model.AEAD.wfootprint FStar.Pervasives.dfst Model.AEAD.id Model.PNE.id Prims.l_iff Prims.b2t Model.PNE.is_safe Model.AEAD.is_safe Model.QUIC.__proj__Writer__item__ae LowStar.Monotonic.Buffer.loc_mreference Model.QUIC._ctr Model.QUIC.__proj__Writer__item__ctr Prims.l_imp
let rinvariant #k #w r h =
  
invariant w h /\ h `HS.contains` r.last /\
(AEAD.wfootprint w.ae) `B.loc_disjoint` (B.loc_mreference w.ctr)