let info (j:id) =
  info:info'{
    I.pne_id_ginfo j == info.calg /\
    I.pne_id_ghash j == info.halg
  }
let info (j: id) =
info: info'{I.pne_id_ginfo j == info.calg /\ I.pne_id_ghash j == info.halg}
Model.PNE.fsti.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.Cipher.fsti.checked QUIC.UInt.fst.checked QUIC.TotSpec.fsti.checked QUIC.Spec.Lemmas.fst.checked QUIC.Spec.Header.fsti.checked QUIC.Spec.fsti.checked prims.fst.checked Model.Indexing.fsti.checked Model.Helpers.fsti.checked Mem.fst.checked LowStar.Buffer.fst.checked LowParse.BitFields.fsti.checked Lib.IntTypes.fsti.checked FStar.UInt8.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.fst.checked
Model.PNE.fsti
Model.PNE.id Model.PNE.info' Prims.l_and Prims.eq2 Model.Indexing.ca Model.Indexing.pne_id_ginfo Model.PNE.__proj__Mkinfo'__item__calg Model.Indexing.ha Model.Indexing.pne_id_ghash Model.PNE.__proj__Mkinfo'__item__halg
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


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

open FStar.HyperStack
open Mem
open Model.Helpers

/// Abbreviations for idealization
/// ------------------------------

type id = I.pne_id
type alg = I.ca

let is_safe (i:id) =
  I.is_pne_honest i && I.ideal_PNE

type safe_id =
  i:id{is_safe i}

type unsafe_id =
  i:id{not (is_safe i)}

/// QUIC payload sampling
/// --------------------

// For simplicity, we do not distinguish between long and short headers; caller
// of this module will just 0-left-pad the protected bits in the case of a long
// header.
let bits: Type0 = LowParse.BitFields.ubitfield 8 5

// Note: the sample is PUBLIC so is using QUIC.Spec.lbytes which do not operate over secret integers.
let sample_length = 16
let sample = QUIC.Spec.lbytes sample_length
let pne_plain_length = l:nat {l >= 1 /\ l <= 4}

let length_bits (l: pne_plain_length) =
  b:bits { LowParse.BitFields.get_bitfield b 0 2 + 1 == l }

let pne_cipher (l:pne_plain_length) = lbytes l & bits
let pne_cipherpad = lbytes 4 & bits

/// Restrict a generated cipherpad to the length of the encoded packet number.
val clip_cipherpad : (cp:pne_cipherpad) -> (l:pne_plain_length) -> pne_cipher l

// We define a separate package type here (different from the one in AEAD). We
// idealize them separately, and there's a specific part here that's about the
// protected bits of the header.
noeq type pne_plain_pkg =
  | PNEPlainPkg:
    pne_plain: (j:id -> l:pne_plain_length -> t:eqtype) ->
    as_bytes: (j:id -> l:pne_plain_length -> pne_plain j l -> GTot (lbytes l & length_bits l)) ->
    repr: (j:unsafe_id -> l:pne_plain_length -> n:pne_plain j l ->
      Tot (b:(lbytes l & length_bits l) {b == as_bytes j l n})) ->
    mk: (j:id -> l:pne_plain_length -> n:lbytes l -> b:length_bits l -> p:pne_plain j l { as_bytes j l p == (n, b) }) ->
    xor: (j:id -> l:pne_plain_length -> p:pne_plain j l -> cp:pne_cipherpad ->
      (l': pne_plain_length & pne_plain j l')) ->
    lemma_xor: (j:id -> l:pne_plain_length -> p:pne_plain j l -> cp:pne_cipherpad -> Lemma
        (requires True)
        (ensures (
          let (| l', p' |) = xor j l p cp in
          let _, bits = as_bytes j l' p' in
          let l: pne_plain_length = LowParse.BitFields.get_bitfield bits 0 2 + 1 in
          let l': pne_plain_length = l' in
          l == l'
        ))) ->
    pne_plain_pkg

noeq type info' = {
  calg: alg;
  halg: I.ha;
  plain: pne_plain_pkg;
}
val info : j: Model.PNE.id -> Type
j: Model.PNE.id -> Type