val decrypt:
  (#j:id) ->
  (#u:info j) ->
  (st:pne_state u) ->
  (cp:pne_cipherpad) ->
  (s:sample) ->
  ST (l:pne_plain_length & pne_plain u l)
  (requires fun h0 ->
    invariant st h0)
  (ensures fun h0 r h1 ->
    invariant st h1 /\
    B.modifies (footprint st) h0 h1 /\ (
    if is_safe j then
      let entry = entry_for_sample s st h1 in
      Some? entry /\ (
      let Some (Entry _ #l' n' c') = entry in
      r == PNEPlainPkg?.xor u.plain j l' n' (c' `xor_cipherpad` cp)) /\
      (Some? (entry_for_sample s st h0) ==> modifies_none h0 h1)
    else
      let cipher, encrypted_bits = cp in
      r == decrypt_spec u.calg cipher encrypted_bits (key st) s)
  )
val decrypt:
  (#j:id) ->
  (#u:info j) ->
  (st:pne_state u) ->
  (cp:pne_cipherpad) ->
  (s:sample) ->
  ST (l:pne_plain_length & pne_plain u l)
  (requires fun h0 ->
    invariant st h0)
  (ensures fun h0 r h1 ->
    invariant st h1 /\
    B.modifies (footprint st) h0 h1 /\ (
    if is_safe j then
      let entry = entry_for_sample s st h1 in
      Some? entry /\ (
      let Some (Entry _ #l' n' c') = entry in
      r == PNEPlainPkg?.xor u.plain j l' n' (c' `xor_cipherpad` cp)) /\
      (Some? (entry_for_sample s st h0) ==> modifies_none h0 h1)
    else
      let cipher, encrypted_bits = cp in
      r == decrypt_spec u.calg cipher encrypted_bits (key st) s)
  )
let decrypt #j #u st cp s =
  if is_safe j then
    let (| info, p |) = st <: model_state j in
    let log = !*p in
    match Seq.find_l (sample_filter u s) log with
    | Some (Entry _ #l' n' c') ->
        // The sample is present in the table, cipher may or may not match, it's
        // up to the caller to prove that when there's a match (i.e. c' == cp)
        // then c'' == zeroes which then entails that the returns value is the
        // plaintext that was in the table
        let c'' = c' `xor_cipherpad` cp in
        PNEPlainPkg?.xor u.plain j l' n' c''
    | None ->
        // Need to add into the table:
        let bits = random_bits () in
        let l = LowParse.BitFields.get_bitfield bits 0 2 + 1 in
        let c' = random 4, bits in
        // let n' = clip_cipherpad (c' `xor_cipherpad` cp) l in
        let r = random l in
        let n = PNEPlainPkg?.mk u.plain j l r bits in
        let new_log = Seq.snoc log (Entry s #l n c') in
        p *= new_log;
        snoc_find log (sample_filter u s) (Entry s #l n c');
        let h1 = ST.get () in
        let r = PNEPlainPkg?.xor u.plain j l n (c' `xor_cipherpad` cp) in
        assert (
          let entry = entry_for_sample s st h1 in
          Some? entry /\ (
          let Some (Entry _ #l' n' c') = entry in
          r == PNEPlainPkg?.xor u.plain j l' n' (c' `xor_cipherpad` cp)));
        r
  else
    let info, k = st <: unsafe_state j in
    decrypt_spec info.calg (fst cp) (snd cp) k s
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

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

let random_bits ():
  HyperStack.ST.ST bits
    (requires fun h0 -> True)
    (ensures fun h0 _ h1 -> h0 == h1)
=
  let r = random 1 in
  LowParse.BitFields.get_bitfield #8 (UInt8.v (Lib.RawIntTypes.u8_to_UInt8 (Seq.index r 0))) 0 5

let encrypt #j #u st #l n s =
  let h0 = ST.get () in
  if is_safe j then
    let (| u, p |) = st <: model_state j in
    let log = !*p in
    assert (log == table st h0);
    let cipher: pne_cipherpad = random 4, random_bits () in
    p *= Seq.snoc log (Entry s #l n cipher);
    clip_cipherpad cipher l
  else
    let open QUIC.Spec.Lemmas in
    let pn, bits = PNEPlainPkg?.repr u.plain j l n in
    let k = snd (st <: unsafe_state j) in
    let alg = (fst (st <: unsafe_state j)).calg in
    encrypt_spec alg l pn bits s k

#push-options "--fuel 1"
let snoc_find #a (s: Seq.seq a) (f: a -> bool) (x: a): Lemma
  (requires f x /\ None? FStar.Seq.(find_l f s))
  (ensures FStar.Seq.(find_l f (snoc s x)) == Some x)
=
  assert (Seq.snoc s x `Seq.equal` Seq.append s (Seq.create 1 x));
  Seq.find_append_none s (Seq.create 1 x) f;
  ()
#pop-options
/
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
st: Model.PNE.pne_state u450 -> cp: Model.PNE.pne_cipherpad -> s: Model.PNE.sample
  -> FStar.HyperStack.ST.ST
    (Prims.dtuple2 Model.PNE.pne_plain_length (fun l -> Model.PNE.pne_plain u450 l))
Model.PNE.id Model.PNE.info Model.PNE.pne_state Model.PNE.pne_cipherpad Model.PNE.sample Model.PNE.is_safe LowStar.Buffer.pointer Model.PNE.log FStar.Seq.Properties.find_l Model.PNE.entry Model.PNE.sample_filter Model.PNE.pne_plain_length Model.PNE.pne_plain Model.PNE.__proj__PNEPlainPkg__item__xor Model.PNE.__proj__Mkinfo'__item__plain Model.PNE.xor_cipherpad Prims.dtuple2 Prims.unit Prims._assert Prims.l_and Prims.b2t FStar.Pervasives.Native.uu___is_Some Prims.eq2 Model.PNE.__proj__PNEPlainPkg__item__pne_plain Prims.logical FStar.Pervasives.Native.option Model.PNE.entry_for_sample FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Model.PNE.snoc_find Model.PNE.Entry LowStar.BufferOps.op_Star_Equals LowStar.Buffer.trivial_preorder FStar.Seq.Base.seq FStar.Seq.Properties.snoc FStar.Pervasives.Native.tuple2 Model.Helpers.lbytes Model.PNE.length_bits Model.PNE.__proj__PNEPlainPkg__item__as_bytes FStar.Pervasives.Native.Mktuple2 Model.PNE.__proj__PNEPlainPkg__item__mk Model.Helpers.random Model.PNE.bits Prims.int Prims.op_Addition LowParse.BitFields.get_bitfield Model.PNE.random_bits LowStar.BufferOps.op_Bang_Star Model.PNE.model_state Prims.bool Spec.Agile.Cipher.key Model.Indexing.pne_id_ginfo Model.PNE.decrypt_spec Model.PNE.__proj__Mkinfo'__item__calg FStar.Pervasives.Native.fst FStar.Pervasives.Native.snd Model.PNE.unsafe_state
let decrypt #j #u st cp s =
  
if is_safe j
then
  let (| info , p |) = st <: model_state j in
  let log = !*p in
  match Seq.find_l (sample_filter u s) log with
  | Some (Entry _ #l' n' c') ->
    let c'' = c' `xor_cipherpad` cp in
    PNEPlainPkg?.xor u.plain j l' n' c''
  | None ->
    let bits = random_bits () in
    let l = LowParse.BitFields.get_bitfield bits 0 2 + 1 in
    let c' = random 4, bits in
    let r = random l in
    let n = PNEPlainPkg?.mk u.plain j l r bits in
    let new_log = Seq.snoc log (Entry s #l n c') in
    p *= new_log;
    snoc_find log (sample_filter u s) (Entry s #l n c');
    let h1 = ST.get () in
    let r = PNEPlainPkg?.xor u.plain j l n (c' `xor_cipherpad` cp) in
    assert (let entry = entry_for_sample s st h1 in
        Some? entry /\
        (let Some (Entry _ #l' n' c') = entry in
          r == PNEPlainPkg?.xor u.plain j l' n' (c' `xor_cipherpad` cp)));
    r
else
  let info, k = st <: unsafe_state j in
  decrypt_spec info.calg (fst cp) (snd cp) k s