val rs_loc_elems_rec_inverse:
  #a:Type0 -> #rst:Type -> rg:regional rst a ->
  rs:S.seq a ->
  i:nat -> j:nat{i < j && j <= S.length rs} ->
  Lemma (requires true)
        (ensures (rs_loc_elems rg rs i j ==
                 loc_union (rs_loc_elem rg rs i)
                           (rs_loc_elems rg rs (i + 1) j)))
        (decreases j)
let rec rs_loc_elems_rec_inverse #a #rst rg rs i j =
  if i + 1 = j then ()
  else (assert (rs_loc_elems rg rs i j ==
               loc_union (rs_loc_elems rg rs i (j - 1))
                         (rs_loc_elem rg rs (j - 1)));
       assert (rs_loc_elems rg rs (i + 1) j ==
              loc_union (rs_loc_elems rg rs (i + 1) (j - 1))
                        (rs_loc_elem rg rs (j - 1)));
       rs_loc_elems_rec_inverse rg rs i (j - 1);
       assert (rs_loc_elems rg rs i j ==
              loc_union (loc_union
                          (rs_loc_elem rg rs i)
                          (rs_loc_elems rg rs (i + 1) (j - 1)))
                        (rs_loc_elem rg rs (j - 1)));
       loc_union_assoc (rs_loc_elem rg rs i)
                       (rs_loc_elems rg rs (i + 1) (j - 1))
                       (rs_loc_elem rg rs (j - 1)))
val rs_loc_elems_rec_inverse:
  #a:Type0 -> #rst:Type -> rg:regional rst a ->
  rs:S.seq a ->
  i:nat -> j:nat{i < j && j <= S.length rs} ->
  Lemma (requires true)
        (ensures (rs_loc_elems rg rs i j ==
                 loc_union (rs_loc_elem rg rs i)
                           (rs_loc_elems rg rs (i + 1) j)))
        (decreases j)
let rec rs_loc_elems_rec_inverse #a #rst rg rs i j =
if i + 1 = j
then ()
else
  (assert (rs_loc_elems rg rs i j ==
        loc_union (rs_loc_elems rg rs i (j - 1)) (rs_loc_elem rg rs (j - 1)));
    assert (rs_loc_elems rg rs (i + 1) j ==
        loc_union (rs_loc_elems rg rs (i + 1) (j - 1)) (rs_loc_elem rg rs (j - 1)));
    rs_loc_elems_rec_inverse rg rs i (j - 1);
    assert (rs_loc_elems rg rs i j ==
        loc_union (loc_union (rs_loc_elem rg rs i) (rs_loc_elems rg rs (i + 1) (j - 1)))
          (rs_loc_elem rg rs (j - 1)));
    loc_union_assoc (rs_loc_elem rg rs i)
      (rs_loc_elems rg rs (i + 1) (j - 1))
      (rs_loc_elem rg rs (j - 1)))
LowStar.RVector.fst.checked
prims.fst.checked LowStar.Vector.fst.checked LowStar.Regional.fst.checked LowStar.Modifies.fst.checked LowStar.Buffer.fst.checked FStar.UInt32.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.Integers.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
LowStar.RVector.fst
LowStar.Regional.regional FStar.Seq.Base.seq FStar.Integers.nat Prims.b2t Prims.op_AmpAmp FStar.Integers.op_Less FStar.Integers.Signed FStar.Integers.Winfinite FStar.Integers.op_Less_Equals FStar.Seq.Base.length Prims.op_Equality FStar.Integers.int_t FStar.Integers.op_Plus Prims.bool LowStar.Monotonic.Buffer.loc_union_assoc LowStar.RVector.rs_loc_elem LowStar.RVector.rs_loc_elems FStar.Integers.op_Subtraction Prims.unit Prims._assert Prims.eq2 LowStar.Monotonic.Buffer.loc LowStar.Monotonic.Buffer.loc_union LowStar.RVector.rs_loc_elems_rec_inverse
(*
   Copyright 2008-2018 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.
*)

module LowStar.RVector

open FStar.Classical
open FStar.Integers
open LowStar.Modifies
open LowStar.Regional
open LowStar.Vector

module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module S = FStar.Seq
module B = LowStar.Buffer
module V = LowStar.Vector

module U32 = FStar.UInt32

/// Utilities

/// A `regional` type `a` is also `copyable` when there exists a copy operator
/// that guarantees the same representation between `src` and `dst`.
/// For instance, the `copy` operation for `B.buffer a` is `B.blit`.
///
/// Here, no reference at run-time is kept to the state argument of the
/// regional; conceivably, the caller will already have some reference handy to
/// the instance of the regional class and can retrieve the parameter from
/// there.
inline_for_extraction
noeq type copyable (#rst:Type) (a:Type0) (rg:regional rst a) =
| Cpy:
    copy: (s:rst{s==Rgl?.state rg} -> src:a -> dst:a ->
      HST.ST unit
        (requires (fun h0 ->
          rg_inv rg h0 src /\ rg_inv rg h0 dst /\
          HS.disjoint (Rgl?.region_of rg src)
                      (Rgl?.region_of rg dst)))
        (ensures (fun h0 _ h1 ->
          modifies (loc_all_regions_from
                     false (Rgl?.region_of rg dst)) h0 h1 /\
          rg_inv rg h1 dst /\
          Rgl?.r_repr rg h1 dst == Rgl?.r_repr rg h0 src))) ->
    copyable a rg

// rst: regional state
type rvector (#a:Type0) (#rst:Type) (rg:regional rst a) = V.vector a

val loc_rvector:
  #a:Type0 -> #rst:Type -> #rg:regional rst a -> rv:rvector rg -> GTot loc
let loc_rvector #a #rst #rg rv =
  loc_all_regions_from false (V.frameOf rv)

/// The invariant of `rvector`
// Here we will define the invariant for `rvector #a` that contains
// the invariant for each element and some more about the vector itself.

val rs_elems_inv:
  #a:Type0 -> #rst:Type -> rg:regional rst a ->
  h:HS.mem -> rs:S.seq a ->
  i:nat -> j:nat{i <= j && j <= S.length rs} ->
  GTot Type0
let rs_elems_inv #a #rst rg h rs i j =
  V.forall_seq rs i j (rg_inv rg h)

val rv_elems_inv:
  #a:Type0 -> #rst:Type -> #rg:regional rst a ->
  h:HS.mem -> rv:rvector rg ->
  i:uint32_t -> j:uint32_t{i <= j && j <= V.size_of rv} ->
  GTot Type0
let rv_elems_inv #a #rst #rg h rv i j =
  rs_elems_inv rg h (V.as_seq h rv) (U32.v i) (U32.v j)

val elems_inv:
  #a:Type0 -> #rst:Type -> #rg:regional rst a ->
  h:HS.mem -> rv:rvector rg ->
  GTot Type0
let elems_inv #a #rst #rg h rv =
  rv_elems_inv h rv 0ul (V.size_of rv)

val rs_elems_reg:
  #a:Type0 -> #rst:Type -> rg:regional rst a ->
  rs:S.seq a -> prid:HS.rid ->
  i:nat -> j:nat{i <= j && j <= S.length rs} ->
  GTot Type0
let rs_elems_reg #a #rst rg rs prid i j =
  V.forall_seq rs i j
    (fun v -> HS.extends (Rgl?.region_of rg v) prid) /\
  V.forall2_seq rs i j
    (fun v1 v2 -> HS.disjoint (Rgl?.region_of rg v1)
                              (Rgl?.region_of rg v2))

val rv_elems_reg:
  #a:Type0 -> #rst:Type -> #rg:regional rst a ->
  h:HS.mem -> rv:rvector rg ->
  i:uint32_t -> j:uint32_t{i <= j && j <= V.size_of rv} ->
  GTot Type0
let rv_elems_reg #a #rst #rg h rv i j =
  rs_elems_reg rg (V.as_seq h rv) (V.frameOf rv) (U32.v i) (U32.v j)

val elems_reg:
  #a:Type0 -> #rst:Type -> #rg:regional rst a ->
  h:HS.mem -> rv:rvector rg ->
  GTot Type0
let elems_reg #a #rst #rg h rv =
  rv_elems_reg h rv 0ul (V.size_of rv)

val rv_itself_inv:
  #a:Type0 -> #rst:Type -> #rg:regional rst a ->
  h:HS.mem -> rv:rvector rg -> GTot Type0
let rv_itself_inv #a #rst #rg h rv =
  V.live h rv /\ V.freeable rv /\
  HST.is_eternal_region (V.frameOf rv)

// This is the invariant of `rvector`.
val rv_inv:
  #a:Type0 -> #rst:Type -> #rg:regional rst a ->
  h:HS.mem -> rv:rvector rg -> GTot Type0
let rv_inv #a #rst #rg h rv =
  elems_inv h rv /\
  elems_reg h rv /\
  rv_itself_inv h rv

val rs_elems_inv_live_region:
  #a:Type0 -> #rst:Type -> rg:regional rst a ->
  h:HS.mem -> rs:S.seq a ->
  i:nat -> j:nat{i <= j && j <= S.length rs} ->
  Lemma (requires (rs_elems_inv rg h rs i j))
        (ensures (V.forall_seq rs i j
                   (fun r -> HS.live_region h (Rgl?.region_of rg r))))
let rec rs_elems_inv_live_region #a #rst rg h rs i j =
  if i = j then ()
  else (Rgl?.r_inv_reg rg h (S.index rs (j - 1));
       rs_elems_inv_live_region rg h rs i (j - 1))

val rv_elems_inv_live_region:
  #a:Type0 -> #rst:Type -> #rg:regional rst a ->
  h:HS.mem -> rv:rvector rg ->
  i:uint32_t -> j:uint32_t{i <= j && j <= V.size_of rv} ->
  Lemma (requires (rv_elems_inv h rv i j))
        (ensures (V.forall_ h rv i j
                   (fun r -> HS.live_region h (Rgl?.region_of rg r))))
let rv_elems_inv_live_region #a #rst #rg h rv i j =
  rs_elems_inv_live_region rg h (V.as_seq h rv) (U32.v i) (U32.v j)

/// Utilities for fine-grained region control

val rs_loc_elem:
  #a:Type0 -> #rst:Type -> rg:regional rst a ->
  rs:S.seq a -> i:nat{i < S.length rs} ->
  GTot loc
let rs_loc_elem #a #rst rg rs i =
  loc_all_regions_from false (Rgl?.region_of rg (S.index rs i))

val rs_loc_elems:
  #a:Type0 -> #rst:Type -> rg:regional rst a ->
  rs:S.seq a -> i:nat -> j:nat{i <= j && j <= S.length rs} ->
  GTot loc (decreases j)
let rec rs_loc_elems #a #rst rg rs i j =
  if i = j then loc_none
  else loc_union (rs_loc_elems rg rs i (j - 1))
                 (rs_loc_elem rg rs (j - 1))

val rv_loc_elems:
  #a:Type0 -> #rst:Type -> #rg:regional rst a ->
  h:HS.mem -> rv:rvector rg ->
  i:uint32_t -> j:uint32_t{i <= j && j <= V.size_of rv} ->
  GTot loc
let rv_loc_elems #a #rst #rg h rv i j =
  rs_loc_elems rg (V.as_seq h rv) (U32.v i) (U32.v j)

val rv_loc_elem:
  #a:Type0 -> #rst:Type -> #rg:regional rst a ->
  h:HS.mem -> rv:rvector rg ->
  i:uint32_t{i < V.size_of rv} ->
  GTot loc
let rv_loc_elem #a #rst #rg h rv i =
  rs_loc_elems rg (V.as_seq h rv) (U32.v i) (U32.v i+1)


// Properties about inclusion of locations

val rs_loc_elems_rec_inverse:
  #a:Type0 -> #rst:Type -> rg:regional rst a ->
  rs:S.seq a ->
  i:nat -> j:nat{i < j && j <= S.length rs} ->
  Lemma (requires true)
        (ensures (rs_loc_elems rg rs i j ==
                 loc_union (rs_loc_elem rg rs i)
                           (rs_loc_elems rg rs (i + 1) j)))
        (decreases j)
val rs_loc_elems_rec_inverse:
  #a:Type0 -> #rst:Type -> rg:regional rst a ->
  rs:S.seq a ->
  i:nat -> j:nat{i < j && j <= S.length rs} ->
  Lemma (requires true)
        (ensures (rs_loc_elems rg rs i j ==
                 loc_union (rs_loc_elem rg rs i)
                           (rs_loc_elems rg rs (i + 1) j)))
        (decreases j)

    rg: LowStar.Regional.regional rst a ->
    rs: FStar.Seq.Base.seq a ->
    i: FStar.Integers.nat ->
    j: FStar.Integers.nat{i < j && j <= FStar.Seq.Base.length rs}
  -> FStar.Pervasives.Lemma (requires true)
      (ensures
        LowStar.RVector.rs_loc_elems rg rs i j ==
        LowStar.Monotonic.Buffer.loc_union (LowStar.RVector.rs_loc_elem rg rs i)
          (LowStar.RVector.rs_loc_elems rg rs (i + 1) j))
      (decreases j)