val quic_coerce (j:unsafe_id) (u:info j)
  (ts:traffic_secret u.halg)
  : ST (pne_state #j u)
  (requires fun _ -> True)
  (ensures fun h0 st h1 ->
    invariant st h1 /\
    B.modifies B.loc_none h0 h1 /\
    B.fresh_loc (footprint st) h0 h1 /\
    B.(loc_includes (loc_pne_region ()) (footprint st)) /\
    key st ==
      QUIC.Spec.derive_secret u.halg ts
        QUIC.Spec.label_hp (key_len u))
val quic_coerce (j:unsafe_id) (u:info j)
  (ts:traffic_secret u.halg)
  : ST (pne_state #j u)
  (requires fun _ -> True)
  (ensures fun h0 st h1 ->
    invariant st h1 /\
    B.modifies B.loc_none h0 h1 /\
    B.fresh_loc (footprint st) h0 h1 /\
    B.(loc_includes (loc_pne_region ()) (footprint st)) /\
    key st ==
      QUIC.Spec.derive_secret u.halg ts
        QUIC.Spec.label_hp (key_len u))
let quic_coerce j u ts =
  let k =
    (QUIC.Spec.derive_secret u.halg ts
        QUIC.Spec.label_hp (key_len u)) in
  coerce j u k
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

let clip_cipherpad cp l =
  let cipher, bits = cp in
  Seq.slice cipher 0 l, bits

let log (#i: id) (u: info i): Type0 =
  Seq.seq (entry #i u)

let model_state j =
  u:info j & B.pointer (log #j u)

let unsafe_state j =
  // I don't understand why we have to go through model.indexing here when
  // the algorithm is readily available in the info
  info j & Spec.key (I.pne_id_ginfo j)

// why is this type parameterized over the info?
let pne_state #j u =
  if is_safe j then
    s:model_state j { dfst s == u }
  else
    s:unsafe_state j { fst s == u }

let table #j #u st h =
  let (| u, p |) = st <: model_state j in
  B.deref h p

let key #j #u st =
  snd (st <: unsafe_state j)

let footprint #i #u w =
  if is_safe i then
    B.loc_addr_of_buffer (dsnd (w <: model_state i))
  else
    B.loc_none

let invariant #i #u st h =
  if is_safe i then
    B.live h (dsnd (st <: model_state i))
  else
    True

let frame_invariant #_ #_ _ _ _ _ =
  ()

let frame_table #_ #_ _ _ _ _ =
  ()

let create j u =
  if is_safe j then
    let l: log #j u = Seq.empty #(entry #j u) in
    ((| u, B.malloc q_pne_region l 1ul |) <: model_state j)
  else
    (u, random (Spec.key_length u.calg)) <: unsafe_state j

let coerce j u k =
  (u, k) <: unsafe_state j
/
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

    j: Model.PNE.unsafe_id ->
    u373: Model.PNE.info j ->
    ts: Model.PNE.traffic_secret (Mkinfo'?.halg u373)
  -> FStar.HyperStack.ST.ST (Model.PNE.pne_state u373)
Model.PNE.unsafe_id Model.PNE.info Model.PNE.traffic_secret Model.PNE.__proj__Mkinfo'__item__halg Model.PNE.coerce Model.PNE.pne_state FStar.Seq.Base.seq Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC QUIC.Spec.Crypto.derive_secret QUIC.Spec.Crypto.label_hp Model.PNE.key_len
let quic_coerce j u ts =
  
let k = (QUIC.Spec.derive_secret u.halg ts QUIC.Spec.label_hp (key_len u)) in
coerce j u k