val vprop_monoid:CE.cm vprop Steel.Effect.Common.req
let vprop_monoid : CE.cm vprop Steel.Effect.Common.req = Steel.Effect.Common.rm
val vprop_monoid:CE.cm vprop Steel.Effect.Common.req
let vprop_monoid:CE.cm vprop Steel.Effect.Common.req =
Steel.Effect.Common.rm
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.Effect.Common.rm
(*
   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
val vprop_monoid:CE.cm vprop Steel.Effect.Common.req
FStar.Algebra.CommMonoid.Equiv.cm Steel.Effect.Common.vprop Steel.Effect.Common.req