val 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)}
val 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)}
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
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} =
/
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
j: Model.PNE.id -> l: Model.QUIC.pnl -> n: Model.Helpers.lbytes l -> b: Model.PNE.length_bits l
  -> p: Model.QUIC.pne_plain j l {Model.QUIC.as_bytes j l p == (n, b)}
Model.PNE.id Model.QUIC.pnl Model.Helpers.lbytes Model.PNE.length_bits FStar.Pervasives.Native.Mktuple2 QUIC.Spec.Base.lbytes Model.Helpers.reveal Model.QUIC.pne_plain Prims.eq2 FStar.Pervasives.Native.tuple2 Model.QUIC.as_bytes
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