val pne_pkg: PNE.pne_plain_pkg
val pne_pkg: PNE.pne_plain_pkg
let pne_pkg =
  PNE.PNEPlainPkg pne_plain as_bytes repr mk pnenc lemma_xor
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)))
  = ()
/
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.pne_plain_pkg
Model.PNE.PNEPlainPkg Model.QUIC.pne_plain Model.QUIC.as_bytes Model.QUIC.repr Model.QUIC.mk Model.QUIC.pnenc Model.QUIC.lemma_xor
let pne_pkg =
  
PNE.PNEPlainPkg pne_plain as_bytes repr mk pnenc lemma_xor