let pne_bits_eq #l (x y: pne_cipher l) =
  fst x `lbytes_eq` fst y && snd x = snd y
let pne_bits_eq #l (x: pne_cipher l) (y: pne_cipher l) =
(fst x) `lbytes_eq` (fst y) && snd x = snd y
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.pne_plain_length Model.PNE.pne_cipher Prims.op_AmpAmp Model.Helpers.lbytes_eq FStar.Pervasives.Native.fst Model.Helpers.lbytes Model.PNE.bits Prims.op_Equality FStar.Pervasives.Native.snd Prims.bool
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;
}

let info (j:id) =
  info:info'{
    I.pne_id_ginfo j == info.calg /\
    I.pne_id_ghash j == info.halg
  }

let pne_plain (#j:id) (u:info j) (l:pne_plain_length) =
  PNEPlainPkg?.pne_plain u.plain j l

noeq
type entry (#j:id) (u:info j) =
  | Entry :
    s:sample ->
    #l:pne_plain_length ->
    n:pne_plain u l ->
    // We do not perform truncation at encryption-time, but rather at decryption-time
    c:pne_cipherpad ->
    entry u

val pne_state : (#j:id) -> (u:info j) -> Type u#1

val table : (#j:safe_id) -> (#u:info j) -> (st:pne_state u) -> (h:mem) -> GTot (Seq.seq (entry u))

// Header protection key
let key_len (#j:id) (u:info j) = Spec.Agile.Cipher.key_length u.calg
val key: #j:unsafe_id -> #u:info j -> st:pne_state u -> lbytes (key_len u)

val footprint : #j:id -> #u:info j -> st:pne_state u -> GTot B.loc

val invariant: #j:id -> #u:info j -> st:pne_state u -> mem -> Type0

val frame_invariant: #j:id -> #u:info j -> st:pne_state u -> l:B.loc -> h0:mem -> h1:mem -> Lemma
  (requires (
    invariant st h0 /\
    B.modifies l h0 h1 /\
    B.loc_disjoint l (footprint st)))
  (ensures (
    invariant st h1))

val frame_table: #j:safe_id -> #u:info j -> st:pne_state u ->
  r:B.loc -> h0:mem -> h1:mem ->
  Lemma
    (requires
      invariant st h0 /\
      B.modifies r h0 h1 /\
      r `B.loc_disjoint` (footprint st))
    (ensures table st h1 == table st h0)

// Equality for the pair of (pne, protected_bits) we manipulate in this module.
val pne_bits_eq : x: Model.PNE.pne_cipher l -> y: Model.PNE.pne_cipher l -> Prims.bool
x: Model.PNE.pne_cipher l -> y: Model.PNE.pne_cipher l -> Prims.bool