val seq_props (#k: eqtype) (#v: Type0) (h: hash_fn k) (s: Seq.seq (option (k & v))) : prop
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))
val seq_props (#k: eqtype) (#v: Type0) (h: hash_fn k) (s: Seq.seq (option (k & v))) : prop
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))
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 FStar.Seq.Base.seq FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 Prims.l_and Prims.b2t Prims.op_LessThan FStar.Seq.Base.length FStar.SizeT.fits Prims.l_Forall Prims.nat Prims.l_imp FStar.Pervasives.Native.uu___is_Some FStar.Seq.Base.index Prims.eq2 Prims.l_or FStar.SizeT.mod_spec FStar.SizeT.v Prims.logical Prims.prop
(*
   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
val seq_props (#k: eqtype) (#v: Type0) (h: hash_fn k) (s: Seq.seq (option (k & v))) : prop

    h: Steel.ST.EphemeralHashtbl.hash_fn k ->
    s: FStar.Seq.Base.seq (FStar.Pervasives.Native.option (k * v))
  -> Prims.prop