val ghost_put (#opened:_)
  (#k:eqtype)
  (#v:Type0)
  (#contents:Type)
  (#vp:vp_t k v contents)
  (#h:hash_fn k)
  (#m:G.erased (repr k contents))
  (#borrows:G.erased (Map.t k v))
  (a:tbl vp h)
  (i:k)
  (x:v)
  (c:G.erased contents)
  : STGhost unit
            opened
            (tperm a m borrows `star` vp i x c)
            (fun _ -> tperm a (Map.upd m i c) (Map.remove borrows i))
            (requires Map.sel borrows i == Some x)
            (ensures fun _ -> True)
let ghost_put #_ #k #v #contents #vp #h #m #borrows a i x c =
  let s = elim_exists () in
  elim_pure (pure_invariant a m borrows s);
  A.pts_to_length a.store s;
  let idx = h i `US.rem` a.store_len in

  //reestablish the invariant

  match Seq.index s (US.v idx)
    returns STGhostT _
                     _
                     _
                     (fun _ -> tperm a (Map.upd m i c) (Map.remove borrows i)) with
  | None ->
    //
    //The sequence slot was not set
    //
    //So we can't keep the input vp permission, drop it
    //
    drop (vp i x c);
    assert (Seq.equal (value_vprops_seq vp s m borrows)
                      (value_vprops_seq vp s (Map.upd m i c) (Map.remove borrows i)));
    rewrite (value_vprops vp s m borrows)
            (value_vprops vp s (Map.upd m i c) (Map.remove borrows i));
    pack_tperm s (Map.upd m i c) (Map.remove borrows i) a
  | Some (i', _) ->
    if i' <> i
      returns STGhostT _
                       _
                       _
                       (fun _ -> tperm a (Map.upd m i c) (Map.remove borrows i))
    then begin
      //
      //The sequence slot is set, but contains a different key
      //
      //Again, drop the input vp
      //
      drop (vp i x c);
      assert (Seq.equal (value_vprops_seq vp s m borrows)
                        (value_vprops_seq vp s (Map.upd m i c) (Map.remove borrows i)));
      rewrite (value_vprops vp s m borrows)
              (value_vprops vp s (Map.upd m i c) (Map.remove borrows i));
      pack_tperm s (Map.upd m i c) (Map.remove borrows i) a
    end
    else begin
      //
      //The sequence slot is set and contains the same key
      //
      //We also know that borrows contains the key (the precondition)
      //
      //So, unpack with emp and pack with vp at i
      unpack_value_vprops vp s m borrows idx emp;

      value_vprops_prefix_suffix_put h vp s m borrows (US.v idx) i x c;
      rewrite_value_vprops_prefix_and_suffix vp
        s s
        m (Map.upd m i c)
        borrows (Map.remove borrows i)
        idx;

      pack_value_vprops vp
        s
        (Map.upd m i c)
        (Map.remove borrows i)
        idx
        (vp i x c);

      pack_tperm
        s
        (Map.upd m i c)
        (Map.remove borrows i)
        a
    end
val ghost_put (#opened:_)
  (#k:eqtype)
  (#v:Type0)
  (#contents:Type)
  (#vp:vp_t k v contents)
  (#h:hash_fn k)
  (#m:G.erased (repr k contents))
  (#borrows:G.erased (Map.t k v))
  (a:tbl vp h)
  (i:k)
  (x:v)
  (c:G.erased contents)
  : STGhost unit
            opened
            (tperm a m borrows `star` vp i x c)
            (fun _ -> tperm a (Map.upd m i c) (Map.remove borrows i))
            (requires Map.sel borrows i == Some x)
            (ensures fun _ -> True)
let ghost_put #_ #k #v #contents #vp #h #m #borrows a i x c =
let s = elim_exists () in
elim_pure (pure_invariant a m borrows s);
A.pts_to_length a.store s;
let idx = (h i) `US.rem` a.store_len in
match
  Seq.index s (US.v idx)
     returns STGhostT _ _ _ (fun _ -> tperm a (Map.upd m i c) (Map.remove borrows i))
with
| None ->
  drop (vp i x c);
  assert (Seq.equal (value_vprops_seq vp s m borrows)
        (value_vprops_seq vp s (Map.upd m i c) (Map.remove borrows i)));
  rewrite (value_vprops vp s m borrows) (value_vprops vp s (Map.upd m i c) (Map.remove borrows i));
  pack_tperm s (Map.upd m i c) (Map.remove borrows i) a
| Some (i', _) ->
  if i' <> i

  returns STGhostT _ _ _ (fun _ -> tperm a (Map.upd m i c) (Map.remove borrows i))
  then
    (drop (vp i x c);
      assert (Seq.equal (value_vprops_seq vp s m borrows)
            (value_vprops_seq vp s (Map.upd m i c) (Map.remove borrows i)));
      rewrite (value_vprops vp s m borrows)
        (value_vprops vp s (Map.upd m i c) (Map.remove borrows i));
      pack_tperm s (Map.upd m i c) (Map.remove borrows i) a)
  else
    (unpack_value_vprops vp s m borrows idx emp;
      value_vprops_prefix_suffix_put h vp s m borrows (US.v idx) i x c;
      rewrite_value_vprops_prefix_and_suffix vp
        s
        s
        m
        (Map.upd m i c)
        borrows
        (Map.remove borrows i)
        idx;
      pack_value_vprops vp s (Map.upd m i c) (Map.remove borrows i) idx (vp i x c);
      pack_tperm s (Map.upd m i c) (Map.remove borrows i) a)
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
Steel.Memory.inames Prims.eqtype Steel.ST.EphemeralHashtbl.vp_t Steel.ST.EphemeralHashtbl.hash_fn FStar.Ghost.erased Steel.ST.EphemeralHashtbl.repr FStar.PartialMap.t Steel.ST.EphemeralHashtbl.tbl FStar.Seq.Base.index FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 FStar.Ghost.reveal FStar.Seq.Base.seq FStar.SizeT.v Prims.unit Steel.Effect.Common.VStar FStar.Seq.Permutation.foldm_snoc Steel.Effect.Common.vprop Steel.Effect.Common.req Steel.ST.EphemeralHashtbl.vprop_monoid FStar.Seq.Properties.map_seq Steel.ST.EphemeralHashtbl.value_vprops_mapping_fn Steel.ST.Array.pts_to Steel.ST.EphemeralHashtbl.__proj__Mktbl__item__store Steel.FractionalPermission.full_perm Steel.ST.EphemeralHashtbl.tperm FStar.PartialMap.upd FStar.PartialMap.remove Steel.ST.EphemeralHashtbl.pack_tperm Steel.ST.Util.rewrite Steel.ST.EphemeralHashtbl.value_vprops Prims._assert FStar.Seq.Base.equal Steel.ST.EphemeralHashtbl.value_vprops_seq Steel.ST.Util.drop Prims.op_disEquality Prims.bool Steel.ST.EphemeralHashtbl.pack_value_vprops Steel.ST.EphemeralHashtbl.rewrite_value_vprops_prefix_and_suffix Steel.ST.EphemeralHashtbl.value_vprops_prefix_suffix_put Steel.ST.EphemeralHashtbl.unpack_value_vprops Steel.Effect.Common.emp FStar.SizeT.t FStar.SizeT.rem Steel.ST.EphemeralHashtbl.__proj__Mktbl__item__store_len Steel.ST.Array.pts_to_length Steel.ST.Util.elim_pure Steel.ST.EphemeralHashtbl.pure_invariant Steel.ST.Util.elim_exists Steel.ST.Util.pure
(*
   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 ==
                    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))

let value_vprops_prefix_suffix_put
  (#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})
  (x:k) (y:v) (c:G.erased contents)
  : Lemma (requires seq_props h s /\
                    seq_props h (Seq.upd s idx (Some (x, y))))
          (ensures (let s1 = Seq.upd s idx (Some (x, y)) in
                    let m1 = Map.upd m x c in
                    let borrows1 = Map.remove borrows x in
                    value_vprops vp (seq_until s idx) m borrows ==
                    value_vprops vp (seq_until s1 idx) m1 borrows1 /\
                    value_vprops vp (seq_from s idx) m borrows ==
                    value_vprops vp (seq_from s1 idx) m1 borrows1))
  = let s1 = Seq.upd s idx (Some (x, y)) in
    let m1 = Map.upd m x c in
    let borrows1 = Map.remove borrows x in
    assert (Seq.index s1 idx == Some (x, y));
    assert (Seq.equal (value_vprops_seq vp (seq_until s idx) m borrows)
                      (value_vprops_seq vp (seq_until s1 idx) m1 borrows1));
    assert (Seq.equal (value_vprops_seq vp (seq_from s idx) m borrows)
                      (value_vprops_seq vp (seq_from s1 idx) m1 borrows1))

let value_vprops_prefix_suffix_remove
  (#k:eqtype)
  (#v:Type0)
  (#contents:Type)
  (h:hash_fn k)
  (vp:vp_t k v contents)
  (s:Seq.seq (option (k & v)){seq_props h s})
  (m:repr k contents)
  (borrows:Map.t k v)
  (idx:nat)
  (i:k{US.v (h i) `US.mod_spec` Seq.length s == idx})
  : Lemma (requires Some? (Seq.index s idx))
          (ensures (let s1 = Seq.upd s idx None in
                    let borrows1 = Map.remove borrows i in
                    value_vprops vp (seq_until s idx) m borrows ==
                    value_vprops vp (seq_until s1 idx) m borrows1 /\
                    value_vprops vp (seq_from s idx) m borrows ==
                    value_vprops vp (seq_from s1 idx) m borrows1))
  = let s1 = Seq.upd s idx None in
    let borrows1 = Map.remove borrows i in
    assert (Seq.equal (value_vprops_seq vp (seq_until s idx) m borrows)
                      (value_vprops_seq vp (seq_until s1 idx) m borrows1));
    assert (Seq.equal (value_vprops_seq vp (seq_from s idx) m borrows)
                      (value_vprops_seq vp (seq_from s1 idx) m borrows1))


/// A common utility that we use in all APIs
///
/// It first splits the value vprops intro (prefix, at i, suffix)
///
/// Then, given a vprop p, such that vprop seq at i is proven to be p by the client,
///   it rewrites the (at i) part with p

let unpack_value_vprops (#opened:_)
  (#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)
  (idx:US.t{US.v idx < Seq.length s})
  (p:vprop)
  : STGhost unit opened
      (value_vprops vp s m borrows)
      (fun _ ->
       value_vprops vp (seq_until s (US.v idx)) m borrows
         `star`
       p
         `star`
       value_vprops vp (seq_from s (US.v idx)) m borrows)
      (requires Seq.index (value_vprops_seq vp s m borrows) (US.v idx) == p)
      (ensures fun _ -> True)
  = value_vprops_split3 vp s m borrows (US.v idx);
    rewrite_equiv _
      (value_vprops vp (seq_until s (US.v idx)) m borrows
         `star`
       value_vprops vp (seq_at s (US.v idx)) m borrows
         `star`
       value_vprops vp (seq_from s (US.v idx)) m borrows);
    SeqPerm.foldm_snoc_singleton vprop_monoid p;
    assert (Seq.equal (value_vprops_seq vp (Seq.create 1 (Seq.index s (US.v idx))) m borrows)
                      (Seq.create 1 p));
    rewrite_equiv (value_vprops vp (seq_at s (US.v idx)) m borrows) p

/// A wrapper over two rewrites
///  (used to rewrite the prefix and suffix parts of value vprops)

let rewrite_value_vprops_prefix_and_suffix (#opened:_)
  (#k:eqtype)
  (#v:Type0)
  (#contents:Type)
  (vp:vp_t k v contents)
  (s1 s2:Seq.seq (option (k & v)))
  (m1 m2:Map.t k contents)
  (borrows1 borrows2:Map.t k v)
  (idx:US.t{Seq.length s1 == Seq.length s2 /\ US.v idx < Seq.length s1})
  : STGhost unit opened
      (value_vprops vp (seq_until s1 (US.v idx)) m1 borrows1
         `star`
       value_vprops vp (seq_from s1 (US.v idx)) m1 borrows1)
      (fun _ ->
       value_vprops vp (seq_until s2 (US.v idx)) m2 borrows2
         `star`
       value_vprops vp (seq_from s2 (US.v idx)) m2 borrows2)
      (requires value_vprops vp (seq_until s1 (US.v idx)) m1 borrows1 ==
                value_vprops vp (seq_until s2 (US.v idx)) m2 borrows2 /\
                value_vprops vp (seq_from s1 (US.v idx)) m1 borrows1 ==
                value_vprops vp (seq_from s2 (US.v idx)) m2 borrows2)
      (ensures fun _ -> True)
  = rewrite
      (value_vprops vp (seq_until s1 (US.v idx)) m1 borrows1
         `star`
       value_vprops vp (seq_from s1 (US.v idx)) m1 borrows1)
      (value_vprops vp (seq_until s2 (US.v idx)) m2 borrows2
         `star`
       value_vprops vp (seq_from s2 (US.v idx)) m2 borrows2)


/// The opposite direction of unpack_value_vprops

let pack_value_vprops (#opened:_)
  (#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)
  (idx:US.t{US.v idx < Seq.length s})
  (p:vprop)
  : STGhost unit opened
      (value_vprops vp (seq_until s (US.v idx)) m borrows
         `star`
       p
         `star`
       value_vprops vp (seq_from s (US.v idx)) m borrows)
      (fun _ -> value_vprops vp s m borrows)
      (requires Seq.index (value_vprops_seq vp s m borrows) (US.v idx) == p)
      (ensures fun _ -> True)
  = SeqPerm.foldm_snoc_singleton vprop_monoid p;
    assert (Seq.equal (value_vprops_seq vp (Seq.create 1 (Seq.index s (US.v idx))) m borrows)
                      (Seq.create 1 p));
    rewrite_equiv p (value_vprops vp (seq_at s (US.v idx)) m borrows);
    value_vprops_split3 vp s m borrows (US.v idx);
    rewrite_equiv
      (value_vprops vp (seq_until s (US.v idx)) m borrows
         `star`
       value_vprops vp (seq_at s (US.v idx)) m borrows
         `star`
       value_vprops vp (seq_from s (US.v idx)) m borrows)
      (value_vprops vp s m borrows)

/// `get`

let get #k #v #contents #vp #h #m #borrows a i =
  let s = elim_exists () in
  elim_pure (pure_invariant a m borrows s);
  A.pts_to_length a.store s;
  let idx = h i `US.rem` a.store_len in
  let vopt = A.read a.store idx in
  let r = match vopt with
          | None -> Absent
          | Some (i', x) ->
            if i <> i' then Missing i'
            else Present x in
  (match vopt with
   | None ->  //Nothing at the slot, return Absent
     pack_tperm s m borrows a;
     rewrite (tperm a m borrows) (get_post m borrows a i r)
   | Some (i', x) ->
     if i <> i'
     then begin  //A different key, return Missing
       intro_pure (map_contains_prop i' m);
       pack_tperm s m borrows a;
       rewrite (tperm a m borrows
                  `star`
                pure (map_contains_prop i' m))
               (get_post m borrows a i r)
     end
     else begin
       //
       //Unpack value vprops to get (vp i x c)
       //
       //Rewrite prefix and suffix
       //
       //Rewrite (at i) with empty
       //
       //Pack value vprops
       //
       unpack_value_vprops vp s m borrows idx (vp i x (Some?.v (Map.sel m i)));

       value_vprops_prefix_suffix_get h vp s m borrows (US.v idx);
       rewrite_value_vprops_prefix_and_suffix vp s s m m
         borrows (Map.upd borrows i x) idx;

       pack_value_vprops vp s m (Map.upd borrows i x) idx emp;

       pack_tperm s m (Map.upd borrows i x) a;

       rewrite (tperm a m (Map.upd borrows i x)
                 `star`
                vp i x (Some?.v (Map.sel m i)))
               (get_post m borrows a i r)
     end);
     return r


/// `put` helper, `put` writes to the ghost and concrete state
///   and calls it to establish the invariant

let put_vprops_aux (#opened:_)
  (#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)))
  (i:k)
  (x:v)
  (c:contents)
  (idx:US.t)
  (_:squash (Seq.length s == A.length arr.store /\ idx == h i `US.rem` arr.store_len))
  : STGhost unit opened
      (A.pts_to arr.store full_perm (Seq.upd s (US.v idx) (Some (i, x)))
         `star`
       value_vprops vp s m borrows
         `star`
       vp i x c)
      (fun _ -> tperm arr (Map.upd m i c) (Map.remove borrows i))
      (requires pure_invariant arr m borrows s)
      (ensures fun _ -> True)
  = let vopt = Seq.index s (US.v idx) in
    match vopt with
    | None ->
      //
      //The sequence slot earlier was None, meaning no entry
      //
      //This means there was nothing in the value vprops
      //
      //Unpack value vprops with emp at i
      //
      //Rewrite prefix and suffix
      //
      //Rewrite (at i) with (vp i x c)
      //
      //Pack value vprops
      //
      unpack_value_vprops vp s m borrows idx emp;

      value_vprops_prefix_suffix_put h vp s m borrows (US.v idx) i x c;
      rewrite_value_vprops_prefix_and_suffix vp
        s (Seq.upd s (US.v idx) (Some (i, x)))
        m (Map.upd m i c)
        borrows (Map.remove borrows i)
        idx;

      pack_value_vprops vp
        (Seq.upd s (US.v idx) (Some (i, x)))
        (Map.upd m i c)
        (Map.remove borrows i)
        idx
        (vp i x c);

      pack_tperm
        (Seq.upd s (US.v idx) (Some (i, x)))
        (Map.upd m i c)
        (Map.remove borrows i)
        arr

   | Some (i', x') ->

     //
     //The sequence slot was set earlier
     //
     //Whether we have the corresponding vp permission depends on the borrows entry
     //

     let bopt = Map.sel borrows i' in
     match bopt with
     | None ->

       //
       //borrows does not contains i;
       //
       //unpack with (vp ...) at i' and pack with (vp ...) at i
       //
       //note that both i and i' map to the same slot
       //

       unpack_value_vprops vp s m borrows idx (vp i' x' (Some?.v (Map.sel m i')));
       drop (vp i' x' (Some?.v (Map.sel m i')));

       value_vprops_prefix_suffix_put h vp s m borrows (US.v idx) i x c;
       rewrite_value_vprops_prefix_and_suffix vp
         s (Seq.upd s (US.v idx) (Some (i, x)))
         m (Map.upd m i c)
         borrows (Map.remove borrows i)
         idx;

       pack_value_vprops vp
         (Seq.upd s (US.v idx) (Some (i, x)))
         (Map.upd m i c)
         (Map.remove borrows i)
         idx
         (vp i x c);

       pack_tperm
         (Seq.upd s (US.v idx) (Some (i, x)))
         (Map.upd m i c)
         (Map.remove borrows i)
         arr

     | _ ->

       //
       //borrow contains i', so we unpack with emp and pack with (vp ...)
       //

       unpack_value_vprops vp s m borrows idx emp;

       value_vprops_prefix_suffix_put h vp s m borrows (US.v idx) i x c;
       rewrite_value_vprops_prefix_and_suffix vp
         s (Seq.upd s (US.v idx) (Some (i, x)))
         m (Map.upd m i c)
         borrows (Map.remove borrows i)
         idx;

       pack_value_vprops vp
         (Seq.upd s (US.v idx) (Some (i, x)))
         (Map.upd m i c)
         (Map.remove borrows i)
         idx
         (vp i x c);

       pack_tperm
         (Seq.upd s (US.v idx) (Some (i, x)))
         (Map.upd m i c)
         (Map.remove borrows i)
         arr

/// `put`

let put #k #v #contents #vp #h #m #borrows a i x c =
  let s = elim_exists () in
  elim_pure (pure_invariant a m borrows s);
  A.pts_to_length a.store s;
  let idx = h i `US.rem` a.store_len in

  A.write a.store idx (Some (i, x));

  put_vprops_aux a m borrows s i x c idx ()

/// `ghost_put`
val ghost_put (#opened:_)
  (#k:eqtype)
  (#v:Type0)
  (#contents:Type)
  (#vp:vp_t k v contents)
  (#h:hash_fn k)
  (#m:G.erased (repr k contents))
  (#borrows:G.erased (Map.t k v))
  (a:tbl vp h)
  (i:k)
  (x:v)
  (c:G.erased contents)
  : STGhost unit
            opened
            (tperm a m borrows `star` vp i x c)
            (fun _ -> tperm a (Map.upd m i c) (Map.remove borrows i))
            (requires Map.sel borrows i == Some x)
            (ensures fun _ -> True)
a: Steel.ST.EphemeralHashtbl.tbl vp h -> i: k -> x: v -> c: FStar.Ghost.erased contents
  -> Steel.ST.Effect.Ghost.STGhost Prims.unit