val clip_cipherpad : (cp:pne_cipherpad) -> (l:pne_plain_length) -> pne_cipher l
val clip_cipherpad : (cp:pne_cipherpad) -> (l:pne_plain_length) -> pne_cipher l
let clip_cipherpad cp l =
  let cipher, bits = cp in
  Seq.slice cipher 0 l, bits
module Model.PNE

module B = LowStar.Buffer
module HS = FStar.HyperStack
module I = Model.Indexing
module U32 = FStar.UInt32
module U128 = FStar.UInt128
module Spec = Spec.Agile.Cipher

module ST = FStar.HyperStack.ST

#set-options "--fuel 0 --ifuel 0"

open FStar.HyperStack
open Mem
open Model.Helpers
open LowStar.BufferOps
/
Spec.Agile.Cipher.fsti.checked QUIC.Spec.Lemmas.fst.checked QUIC.Spec.fsti.checked prims.fst.checked Model.Indexing.fsti.checked Model.Helpers.fsti.checked Mem.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked LowParse.BitFields.fsti.checked Lib.RawIntTypes.fsti.checked FStar.UInt8.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.ST.fsti.checked FStar.HyperStack.fst.checked
Model.PNE.fst
cp: Model.PNE.pne_cipherpad -> l: Model.PNE.pne_plain_length -> Model.PNE.pne_cipher l
Model.PNE.pne_cipherpad Model.PNE.pne_plain_length Model.Helpers.lbytes Model.PNE.bits FStar.Pervasives.Native.Mktuple2 FStar.Seq.Base.slice Lib.IntTypes.uint8 Model.PNE.pne_cipher
let clip_cipherpad cp l =
  
let cipher, bits = cp in
Seq.slice cipher 0 l, bits