val pnenc (j: PNE.id) (l: pnl) (p: pne_plain j l) (c: PNE.pne_cipherpad)
    : (l': pnl & pne_plain j l')
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') |)
val pnenc (j: PNE.id) (l: pnl) (p: pne_plain j l) (c: PNE.pne_cipherpad)
    : (l': pnl & pne_plain j l')
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') |)
Model.QUIC.fst.checked
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
Model.PNE.id Model.QUIC.pnl Model.QUIC.pne_plain Model.PNE.pne_cipherpad QUIC.Spec.Base.lbytes Model.PNE.length_bits Model.Helpers.lbytes Model.PNE.bits Prims.Mkdtuple2 FStar.Pervasives.Native.Mktuple2 QUIC.Spec.Base.bytes QUIC.Spec.Lemmas.xor_inplace FStar.Seq.Base.slice QUIC.Spec.Base.byte Model.Helpers.reveal Model.QUIC.extend Prims.op_Addition LowParse.BitFields.get_bitfield LowParse.BitFields.set_bitfield Prims.unit LowParse.BitFields.set_bitfield_bound LowParse.BitFields.ubitfield Prims.op_Subtraction FStar.UInt.logxor QUIC.UInt.lemma_logxor_lt Prims.dtuple2
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
val pnenc (j: PNE.id) (l: pnl) (p: pne_plain j l) (c: PNE.pne_cipherpad)
    : (l': pnl & pne_plain j l')
j: Model.PNE.id -> l: Model.QUIC.pnl -> p: Model.QUIC.pne_plain j l -> c: Model.PNE.pne_cipherpad
  -> Prims.dtuple2 Model.QUIC.pnl (fun l' -> Model.QUIC.pne_plain j l')