val value_vprops_prefix_suffix_get
      (#k: eqtype)
      (#v: Type0)
      (#contents: Type)
      (h: hash_fn k)
      (vp: vp_t k v contents)
      (s: Seq.seq (option (k & v)))
      (m: repr k contents)
      (borrows: Map.t k v)
      (idx: nat{idx < Seq.length s})
    : Lemma (requires Some? (Seq.index s idx) /\ seq_props h s)
      (ensures
        (let Some (i, x) = Seq.index s idx in
          let upd_borrows = Map.upd borrows i x in
          value_vprops vp (seq_until s idx) m borrows ==
          value_vprops vp (seq_until s idx) m upd_borrows /\
          value_vprops vp (seq_from s idx) m borrows ==
          value_vprops vp (seq_from s idx) m upd_borrows))
let value_vprops_prefix_suffix_get
  (#k:eqtype)
  (#v:Type0)
  (#contents:Type)
  (h:hash_fn k)
  (vp:vp_t k v contents)
  (s:Seq.seq (option (k & v)))
  (m:repr k contents)
  (borrows:Map.t k v)
  (idx:nat{idx < Seq.length s})
  : Lemma (requires Some? (Seq.index s idx) /\
                    seq_props h s)
          (ensures (let Some (i, x) = Seq.index s idx in
                    let upd_borrows = Map.upd borrows i x in
                    value_vprops vp (seq_until s idx) m borrows ==
                    value_vprops vp (seq_until s idx) m upd_borrows /\
                    value_vprops vp (seq_from s idx) m borrows ==
                    value_vprops vp (seq_from s idx) m upd_borrows))
  = let Some (i, x) = Seq.index s idx in
    let upd_borrows = Map.upd borrows i x in
    assert (Seq.equal (value_vprops_seq vp (seq_until s idx) m borrows)
                      (value_vprops_seq vp (seq_until s idx) m upd_borrows));
    assert (Seq.equal (value_vprops_seq vp (seq_from s idx) m borrows)
                      (value_vprops_seq vp (seq_from s idx) m upd_borrows))
val value_vprops_prefix_suffix_get
      (#k: eqtype)
      (#v: Type0)
      (#contents: Type)
      (h: hash_fn k)
      (vp: vp_t k v contents)
      (s: Seq.seq (option (k & v)))
      (m: repr k contents)
      (borrows: Map.t k v)
      (idx: nat{idx < Seq.length s})
    : Lemma (requires Some? (Seq.index s idx) /\ seq_props h s)
      (ensures
        (let Some (i, x) = Seq.index s idx in
          let upd_borrows = Map.upd borrows i x in
          value_vprops vp (seq_until s idx) m borrows ==
          value_vprops vp (seq_until s idx) m upd_borrows /\
          value_vprops vp (seq_from s idx) m borrows ==
          value_vprops vp (seq_from s idx) m upd_borrows))
let value_vprops_prefix_suffix_get
      (#k: eqtype)
      (#v: Type0)
      (#contents: Type)
      (h: hash_fn k)
      (vp: vp_t k v contents)
      (s: Seq.seq (option (k & v)))
      (m: repr k contents)
      (borrows: Map.t k v)
      (idx: nat{idx < Seq.length s})
    : Lemma (requires Some? (Seq.index s idx) /\ seq_props h s)
      (ensures
        (let Some (i, x) = Seq.index s idx in
          let upd_borrows = Map.upd borrows i x in
          value_vprops vp (seq_until s idx) m borrows ==
          value_vprops vp (seq_until s idx) m upd_borrows /\
          value_vprops vp (seq_from s idx) m borrows ==
          value_vprops vp (seq_from s idx) m upd_borrows)) =
let Some (i, x) = Seq.index s idx in
let upd_borrows = Map.upd borrows i x in
assert (Seq.equal (value_vprops_seq vp (seq_until s idx) m borrows)
      (value_vprops_seq vp (seq_until s idx) m upd_borrows));
assert (Seq.equal (value_vprops_seq vp (seq_from s idx) m borrows)
      (value_vprops_seq vp (seq_from s idx) m upd_borrows))
Steel.ST.EphemeralHashtbl.fst.checked
Steel.ST.Util.fsti.checked Steel.ST.Reference.fsti.checked Steel.ST.Effect.Ghost.fsti.checked Steel.ST.Effect.Atomic.fsti.checked Steel.ST.Effect.fsti.checked Steel.ST.Array.fsti.checked Steel.Memory.fsti.checked Steel.FractionalPermission.fst.checked Steel.Effect.Common.fsti.checked prims.fst.checked FStar.SizeT.fsti.checked FStar.Seq.Permutation.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.PartialMap.fsti.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked FStar.Algebra.CommMonoid.Equiv.fst.checked
Steel.ST.EphemeralHashtbl.fst
Prims.eqtype Steel.ST.EphemeralHashtbl.hash_fn Steel.ST.EphemeralHashtbl.vp_t FStar.Seq.Base.seq FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 Steel.ST.EphemeralHashtbl.repr FStar.PartialMap.t Prims.nat Prims.b2t Prims.op_LessThan FStar.Seq.Base.length Prims._assert FStar.Seq.Base.equal Steel.Effect.Common.vprop Steel.ST.EphemeralHashtbl.value_vprops_seq Steel.ST.EphemeralHashtbl.seq_from Prims.unit Steel.ST.EphemeralHashtbl.seq_until FStar.PartialMap.upd FStar.Seq.Base.index Prims.l_and FStar.Pervasives.Native.uu___is_Some Steel.ST.EphemeralHashtbl.seq_props Prims.squash Prims.eq2 Steel.ST.EphemeralHashtbl.value_vprops Prims.Nil FStar.Pervasives.pattern
(*
   Copyright 2021 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.

   Authors: Aseem Rastogi
*)

module Steel.ST.EphemeralHashtbl

open Steel.FractionalPermission
open Steel.Memory
open Steel.ST.Effect.Ghost
open Steel.ST.Effect.Atomic
open Steel.ST.Effect
open Steel.ST.Util

module G = FStar.Ghost
module Seq = FStar.Seq
module Map = FStar.PartialMap
module US = FStar.SizeT
module R = Steel.ST.Reference
module A = Steel.ST.Array


/// `store` is the concrete store implemented as an array
///
/// The hashing scheme we use is as follows:
///   for key `k`, its slot in the array is `(h k) mod n`

noeq
type tbl #k #v #contents (vp:vp_t k v contents) (h:hash_fn k) = {
  store_len    : n:us{US.v n > 0};
  store        : A.array (option (k & v));
  store_len_pf : squash (A.length store == US.v store_len);
}

/// Property of the logical view of the store
///
/// For each (Some (k, v)) in the sequence, (h k) mod n == i

let seq_props (#k:eqtype) (#v:Type0) (h:hash_fn k) (s:Seq.seq (option (k & v))) : prop =
  0 < Seq.length s /\ US.fits (Seq.length s) /\

  (forall (i:nat{i < Seq.length s}).
     Some? (Seq.index s i) ==> (let Some (x, _) = Seq.index s i in
                                US.v (h x) `US.mod_spec` Seq.length s == i))

/// Using seq_props, we can derive that all the keys in the sequence are distinct

let seq_keys_distinct (#k:eqtype) (#v:Type0) (s:Seq.seq (option (k & v))) : prop =
  forall (i j:(k:nat{k < Seq.length s})).{:pattern Seq.index s i; Seq.index s j}
    (i =!= j /\ Some? (Seq.index s i) /\ Some? (Seq.index s j)) ==>
    (fst (Some?.v (Seq.index s i)) =!= fst (Some?.v (Seq.index s j)))

let seq_props_implies_keys_distinct (#k:eqtype) (#v:Type0) (h:hash_fn k) (s:Seq.seq (option (k & v)))
  : Lemma (requires seq_props h s) (ensures seq_keys_distinct s)
  = ()

/// For each (Some (k, v)) in the sequence, k must be in the repr map

let store_and_repr_related
  (#k:eqtype)
  (#v:Type0)
  (#contents:Type)
  (s:Seq.seq (option (k & v)))
  (m:repr k contents)
  : prop
  = forall (i:nat{i < Seq.length s}).
      match Seq.index s i with
      | None -> True
      | Some (k, _) -> Map.contains m k

/// For each (Some (k, v)) in the sequence,
///   either borrows does not contain k, or it maps k to v

let store_and_borrows_related
  (#k:eqtype)
  (#v:Type0)
  (s:Seq.seq (option (k & v)))
  (borrows:Map.t k v)
  : prop
  = forall (i:nat{i < Seq.length s}).
      match Seq.index s i with
      | None -> True
      | Some (k, x) ->
        Map.sel borrows k == None \/
        Map.sel borrows k == Some x

module CE = FStar.Algebra.CommMonoid.Equiv
module SeqPerm = FStar.Seq.Permutation

/// Setup for maintaining the value vprops in the table invariant
///
/// High-level idea is that, we take the store sequence,
///   map it to a sequence of vprops,
///   and fold the vprop monoid (with `star` as the multiplication) on this sequence
///
/// Each value contributes a `vp i x c`, unless it is in the borrows map

let vprop_monoid : CE.cm vprop Steel.Effect.Common.req = Steel.Effect.Common.rm

/// Function to map over the store sequence

let value_vprops_mapping_fn
  (#k:eqtype)
  (#v:Type0)
  (#contents:Type)
  (vp:vp_t k v contents)
  (m:repr k contents)
  (borrows:Map.t k v)
  : option (k & v) -> vprop
  = fun e ->
    match e with
    | None -> emp
    | Some (i, x) ->
      (match Map.sel m i, Map.sel borrows i with
       | None, _ -> pure False
       | _, Some _ -> emp
       | Some c, None -> vp i x c)

/// The corresponding sequence of vprops for a store sequence

[@@__reduce__]
let value_vprops_seq
  (#k:eqtype)
  (#v:Type0)
  (#contents:Type)
  (vp:vp_t k v contents)
  (s:Seq.seq (option (k & v)))
  (m:repr k contents)
  (borrows:Map.t k v)
  : Seq.seq vprop
  = Seq.map_seq (value_vprops_mapping_fn vp m borrows) s

/// Value vprops

[@@__reduce__]
let value_vprops
  (#k:eqtype)
  (#v:Type0)
  (#contents:Type)
  (vp:vp_t k v contents)
  (s:Seq.seq (option (k & v)))
  (m:repr k contents)
  (borrows:Map.t k v)
  : vprop
  = SeqPerm.foldm_snoc vprop_monoid (value_vprops_seq vp s m borrows)

let pure_invariant
  (#k:eqtype)
  (#v:Type0)
  (#contents:Type)
  (#vp:vp_t k v contents)
  (#h:hash_fn k)
  (arr:tbl vp h)
  (m:repr k contents)
  (borrows:Map.t k v)
  (s:Seq.seq (option (k & v)))
  : prop
  = seq_props h s /\
    store_and_repr_related s m /\
    A.is_full_array arr.store /\
    store_and_borrows_related s borrows

/// The main invariant is defined as an existential for the store sequence

[@@__reduce__]
let store_contents_pred
  (#k:eqtype)
  (#v:Type0)
  (#contents:Type)
  (#vp:vp_t k v contents)
  (#h:hash_fn k)
  (arr:tbl vp h)
  (m:repr k contents)
  (borrows:Map.t k v)
  : Seq.seq (option (k & v)) -> vprop
  = fun s ->
    A.pts_to arr.store full_perm s
      `star`
    pure (pure_invariant arr m borrows s)
      `star`
    value_vprops vp s m borrows

/// Main invariant

[@@__reduce__]
let tperm arr m borrows = exists_ (store_contents_pred arr m borrows)


/// map_seq lemmas, with smt pats on them

let map_seq_len (#a #b:Type) (f:a -> Tot b) (s:Seq.seq a)
  : Lemma (ensures Seq.length (Seq.map_seq f s) == Seq.length s)
          [SMTPat (Seq.length (Seq.map_seq f s))]
  = Seq.map_seq_len f s

let map_seq_index (#a #b:Type) (f:a -> Tot b) (s:Seq.seq a) (i:nat{i < Seq.length s})
  : Lemma (ensures Seq.index (Seq.map_seq f s) i == f (Seq.index s i))
          [SMTPat (Seq.index (Seq.map_seq f s) i)]
  = Seq.map_seq_index f s i

let map_seq_append (#a #b:Type) (f:a -> Tot b) (s1 s2:Seq.seq a)
  : Lemma (ensures (Seq.map_seq f (Seq.append s1 s2) ==
                    Seq.append (Seq.map_seq f s1) (Seq.map_seq f s2)))
          [SMTPat (Seq.map_seq f (Seq.append s1 s2))]
  = Seq.map_seq_append f s1 s2


/// Helper function to pack a tperm assertion

let pack_tperm (#opened:_)
  (#k:eqtype)
  (#v:Type0)
  (#contents:Type)
  (#vp:vp_t k v contents)
  (#h:hash_fn k)
  (s:Seq.seq (option (k & v)))
  (m:repr k contents)
  (borrows:Map.t k v)
  (a:tbl vp h)
  : STGhost unit opened
      (A.pts_to a.store full_perm s
         `star`
       value_vprops vp s m borrows)
      (fun _ -> tperm a m borrows)
      (requires pure_invariant a m borrows s)
      (ensures fun _ -> True)
  = intro_pure (pure_invariant a m borrows s);
    intro_exists s (store_contents_pred a m borrows)

let create #k #v #contents vp h n =
  let store = A.alloc #(option (k & v)) None n in
  let arr : tbl #k #v #contents vp h = {
    store_len = n;
    store = store;
    store_len_pf = () } in

  //
  //rewrite in terms of projections from the arr record
  //
  rewrite (A.pts_to store _ (Seq.create #(option (k & v)) (US.v n) None))
          (A.pts_to arr.store _ (Seq.create #(option (k & v)) (US.v n) None));

  //
  //The value vprops at this point are all emp
  //
  //A lemma that tells us that folding a monoid over a sequence of units
  //  is monoid-equivalent to the unit
  //
  SeqPerm.foldm_snoc_unit_seq
    vprop_monoid
    (value_vprops_seq vp (Seq.create (US.v n) None)
                         (Map.empty k contents)
                         (Map.empty k v));
  rewrite_equiv emp (value_vprops vp (Seq.create (US.v n) None)
                                     (Map.empty k contents)
                                     (Map.empty k v));

  pack_tperm (Seq.create (US.v n) None)
             (Map.empty k contents)
             (Map.empty k v)
             arr;

  return arr

/// Similar to create, except that the repr map is a const map

let create_v #k #v #contents vp h n c =
  let store = A.alloc #(option (k & v)) None n in
  let arr : tbl #k #v #contents vp h = {
    store_len = n;
    store = store;
    store_len_pf = () } in

  //
  //rewrite in terms of projections from the arr record
  //
  rewrite (A.pts_to store _ (Seq.create #(option (k & v)) (US.v n) None))
          (A.pts_to arr.store _ (Seq.create #(option (k & v)) (US.v n) None));

  //
  //The value vprops at this point are all emp
  //
  //A lemma that tells us that folding a monoid over a sequence of units
  //  is monoid-equivalent to the unit
  //
  SeqPerm.foldm_snoc_unit_seq
    vprop_monoid
    (value_vprops_seq vp (Seq.create (US.v n) None)
                         (Map.const k (G.reveal c))
                         (Map.empty k v));
  rewrite_equiv emp (value_vprops vp (Seq.create (US.v n) None)
                                     (Map.const k (G.reveal c))
                                     (Map.empty k v));

  pack_tperm (Seq.create (US.v n) None)
             (Map.const k (G.reveal c))
             (Map.empty k v)
             arr;

  return arr

/// Makes it easy to write subsequences

let seq_until (#a:Type) (s:Seq.seq a) (idx:nat{idx < Seq.length s})
  : Seq.seq a
  = Seq.slice s 0 idx

let seq_at (#a:Type) (s:Seq.seq a) (idx:nat{idx < Seq.length s})
  : Seq.seq a
  = Seq.create 1 (Seq.index s idx)

let seq_from (#a:Type) (s:Seq.seq a) (idx:nat{idx < Seq.length s})
  : Seq.seq a
  = Seq.slice s (idx + 1) (Seq.length s)

let elim_equiv_laws ()
  : Lemma (
          (forall x. x `equiv` x) /\
          (forall x y. x `equiv` y ==> y `equiv` x) /\
          (forall x y z. (x `equiv` y /\ y `equiv` z) ==> x `equiv` z)
          )
  = let open Steel.Effect.Common in
    assert (req.eq == equiv);
    CE.elim_eq_laws req

/// This is one of the workhorses of this library
///
/// It splits value vprops for a store sequence into `star` of value vprops for subsequences
///
/// Since `get`, `put`, `with_key` manipulate one entry at a time,
///   we split the sequence at that i (prefix, at i, suffix)

let value_vprops_split3
  (#k:eqtype)
  (#v:Type0)
  (#contents:Type)
  (vp:vp_t k v contents)
  (s:Seq.seq (option (k & v)))
  (m:Map.t k contents)
  (borrows:Map.t k v)
  (i:nat{i < Seq.length s})
  : Lemma (value_vprops vp s m borrows
             `equiv`
           (value_vprops vp (seq_until s i) m borrows
              `star`
            value_vprops vp (seq_at s i) m borrows
              `star`
            value_vprops vp (seq_from s i) m borrows))
  = elim_equiv_laws ();
    Classical.forall_intro_3 star_associative;

    assert (Seq.equal s (Seq.append (seq_until s i)
                                    (Seq.append (seq_at s i) (seq_from s i))));
    let vps s = value_vprops_seq vp s m borrows in

    calc (equiv) {
      value_vprops vp s m borrows;
      (equiv) { }
      value_vprops vp (Seq.append (seq_until s i)
                                  (Seq.append (seq_at s i) (seq_from s i))) m borrows;
      (equiv) { SeqPerm.foldm_snoc_append vprop_monoid
                  (vps (seq_until s i))
                  (Seq.append
                     (vps (seq_at s i))
                     (vps (seq_from s i))) }
      value_vprops vp (seq_until s i) m borrows
        `star`
      value_vprops vp (Seq.append (seq_at s i) (seq_from s i)) m borrows;
      (equiv) { SeqPerm.foldm_snoc_append vprop_monoid
                  (vps (seq_at s i))
                  (vps (seq_from s i));
                star_congruence
                  (value_vprops vp (seq_until s i) m borrows)
                  (value_vprops vp (Seq.append (seq_at s i) (seq_from s i)) m borrows)
                  (value_vprops vp (seq_until s i) m borrows)
                  (value_vprops vp (seq_at s i) m borrows `star` value_vprops vp (seq_from s i) m borrows) }
      value_vprops vp (seq_until s i) m borrows
        `star`
      (value_vprops vp (seq_at s i) m borrows
         `star`
       value_vprops vp (seq_from s i) m borrows);
    }

/// Once we have split value vprops into (prefix, at i, suffix),
///   in all the API (`get`, `put`, `ghost_put`, `remove`), the action happens at (at i)
///
/// The value vprops for prefix and suffix remain same
///
/// We have lemmas for each of the functions to prove that
///
/// The lemmas prove equality of value vprops before and after
///   what each of the functions do to the arrays and maps


let value_vprops_prefix_suffix_get
  (#k:eqtype)
  (#v:Type0)
  (#contents:Type)
  (h:hash_fn k)
  (vp:vp_t k v contents)
  (s:Seq.seq (option (k & v)))
  (m:repr k contents)
  (borrows:Map.t k v)
  (idx:nat{idx < Seq.length s})
  : Lemma (requires Some? (Seq.index s idx) /\
                    seq_props h s)
          (ensures (let Some (i, x) = Seq.index s idx in
                    let upd_borrows = Map.upd borrows i x in
                    value_vprops vp (seq_until s idx) m borrows ==
                    value_vprops vp (seq_until s idx) m upd_borrows /\
                    value_vprops vp (seq_from s idx) m borrows ==
val value_vprops_prefix_suffix_get
      (#k: eqtype)
      (#v: Type0)
      (#contents: Type)
      (h: hash_fn k)
      (vp: vp_t k v contents)
      (s: Seq.seq (option (k & v)))
      (m: repr k contents)
      (borrows: Map.t k v)
      (idx: nat{idx < Seq.length s})
    : Lemma (requires Some? (Seq.index s idx) /\ seq_props h s)
      (ensures
        (let Some (i, x) = Seq.index s idx in
          let upd_borrows = Map.upd borrows i x in
          value_vprops vp (seq_until s idx) m borrows ==
          value_vprops vp (seq_until s idx) m upd_borrows /\
          value_vprops vp (seq_from s idx) m borrows ==
          value_vprops vp (seq_from s idx) m upd_borrows))

    h: Steel.ST.EphemeralHashtbl.hash_fn k ->
    vp: Steel.ST.EphemeralHashtbl.vp_t k v contents ->
    s: FStar.Seq.Base.seq (FStar.Pervasives.Native.option (k * v)) ->
    m: Steel.ST.EphemeralHashtbl.repr k contents ->
    borrows: FStar.PartialMap.t k v ->
    idx: Prims.nat{idx < FStar.Seq.Base.length s}
  -> FStar.Pervasives.Lemma
      (requires Some? (FStar.Seq.Base.index s idx) /\ Steel.ST.EphemeralHashtbl.seq_props h s)
      (ensures
        (let _ = FStar.Seq.Base.index s idx in
          (let FStar.Pervasives.Native.Some #_ (FStar.Pervasives.Native.Mktuple2 #_ #_ i x) = _ in
            let upd_borrows = FStar.PartialMap.upd borrows i x in
            Steel.ST.EphemeralHashtbl.value_vprops vp
              (Steel.ST.EphemeralHashtbl.seq_until s idx)
              m
              borrows ==
            Steel.ST.EphemeralHashtbl.value_vprops vp
              (Steel.ST.EphemeralHashtbl.seq_until s idx)
              m
              upd_borrows /\
            Steel.ST.EphemeralHashtbl.value_vprops vp
              (Steel.ST.EphemeralHashtbl.seq_from s idx)
              m
              borrows ==
            Steel.ST.EphemeralHashtbl.value_vprops vp
              (Steel.ST.EphemeralHashtbl.seq_from s idx)
              m
              upd_borrows)
          <:
          Type0))