val as_seq_seq_eq:
  #a:Type0 -> #rst:Type -> rg:regional rst a ->
  h:HS.mem -> rs1:S.seq a -> rs2:S.seq a ->
  i:nat ->
  j:nat{i <= j /\ j <= S.length rs1 /\ rs_elems_inv rg h rs1 i j} ->
  k:nat ->
  l:nat{k <= l /\ l <= S.length rs2 /\ rs_elems_inv rg h rs2 k l} ->
  Lemma (requires (S.equal (S.slice rs1 i j) (S.slice rs2 k l)))
        (ensures (S.equal (as_seq_seq rg h rs1 i j)
                          (as_seq_seq rg h rs2 k l)))
let as_seq_seq_eq #a #rst rg h rs1 rs2 i j k l =
  assert (forall (a:nat{a < j - i}).
           S.index (as_seq_seq rg h rs1 i j) a ==
           Rgl?.r_repr rg h (S.index rs1 (i + a)));
  assert (forall (a:nat{a < l - k}).
           S.index (as_seq_seq rg h rs2 k l) a ==
           Rgl?.r_repr rg h (S.index rs2 (k + a)));
  assert (S.length (S.slice rs1 i j) = j - i);
  assert (S.length (S.slice rs2 k l) = l - k);
  assert (forall (a:nat{a < j - i}).
           S.index (S.slice rs1 i j) a ==
           S.index (S.slice rs2 k l) a);
  assert (forall (a:nat{a < j - i}).
           S.index rs1 (i + a) == S.index rs2 (k + a))
val as_seq_seq_eq:
  #a:Type0 -> #rst:Type -> rg:regional rst a ->
  h:HS.mem -> rs1:S.seq a -> rs2:S.seq a ->
  i:nat ->
  j:nat{i <= j /\ j <= S.length rs1 /\ rs_elems_inv rg h rs1 i j} ->
  k:nat ->
  l:nat{k <= l /\ l <= S.length rs2 /\ rs_elems_inv rg h rs2 k l} ->
  Lemma (requires (S.equal (S.slice rs1 i j) (S.slice rs2 k l)))
        (ensures (S.equal (as_seq_seq rg h rs1 i j)
                          (as_seq_seq rg h rs2 k l)))
let as_seq_seq_eq #a #rst rg h rs1 rs2 i j k l =
assert (forall (a: nat{a < j - i}).
      S.index (as_seq_seq rg h rs1 i j) a == Rgl?.r_repr rg h (S.index rs1 (i + a)));
assert (forall (a: nat{a < l - k}).
      S.index (as_seq_seq rg h rs2 k l) a == Rgl?.r_repr rg h (S.index rs2 (k + a)));
assert (S.length (S.slice rs1 i j) = j - i);
assert (S.length (S.slice rs2 k l) = l - k);
assert (forall (a: nat{a < j - i}). S.index (S.slice rs1 i j) a == S.index (S.slice rs2 k l) a);
assert (forall (a: nat{a < j - i}). S.index rs1 (i + a) == S.index rs2 (k + a))
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.Monotonic.HyperStack.mem FStar.Seq.Base.seq FStar.Integers.nat Prims.l_and Prims.b2t FStar.Integers.op_Less_Equals FStar.Integers.Signed FStar.Integers.Winfinite FStar.Seq.Base.length LowStar.RVector.rs_elems_inv Prims._assert Prims.l_Forall FStar.Integers.op_Less FStar.Integers.op_Subtraction Prims.eq2 FStar.Seq.Base.index FStar.Integers.op_Plus Prims.unit FStar.Seq.Base.slice Prims.op_Equality Prims.int LowStar.Regional.__proj__Rgl__item__repr LowStar.RVector.as_seq_seq LowStar.Regional.__proj__Rgl__item__r_repr
(*
   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)
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_includes:
  #a:Type0 -> #rst:Type -> rg:regional rst a ->
  rs:S.seq a ->
  i:nat -> j:nat{i <= j && j <= S.length rs} ->
  k:nat{i <= k && k < j} ->
  Lemma (loc_includes (rs_loc_elems rg rs i j)
                      (rs_loc_elem rg rs k))
let rec rs_loc_elems_includes #a #rst rg rs i j k =
  if k = j - 1 then ()
  else rs_loc_elems_includes #a #rst rg rs i (j - 1) k

val loc_all_exts_from:
  preserve_liveness: bool -> r: HS.rid -> GTot loc
let loc_all_exts_from preserve_liveness r =
  B.loc_regions
    preserve_liveness
    (Set.intersect
      (HS.mod_set (Set.singleton r))
      (Set.complement (Set.singleton r)))

val rs_loc_elem_included:
  #a:Type0 -> #rst:Type -> rg:regional rst a ->
  rs:S.seq a -> prid:HS.rid ->
  i:nat{i < S.length rs} ->
  Lemma (requires (HS.extends (Rgl?.region_of rg (S.index rs i)) prid))
        (ensures (loc_includes (loc_all_exts_from false prid)
                               (rs_loc_elem rg rs i)))
let rs_loc_elem_included #a #rst rg rs prid i = ()

val rs_loc_elems_included:
  #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} ->
  Lemma (requires (rs_elems_reg rg rs prid i j))
        (ensures (loc_includes (loc_all_exts_from false prid)
                               (rs_loc_elems rg rs i j)))
        (decreases j)
let rec rs_loc_elems_included #a #rst rg rs prid i j =
  if i = j then ()
  else (rs_loc_elem_included rg rs prid (j - 1);
       rs_loc_elems_included rg rs prid i (j - 1))

val rv_loc_elems_included:
  #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_reg h rv i j))
        (ensures (loc_includes (loc_all_exts_from false (V.frameOf rv))
                               (rv_loc_elems h rv i j)))
let rv_loc_elems_included #a #rst #rg h rv i j =
  rs_loc_elems_included rg (V.as_seq h rv) (V.frameOf rv) (U32.v i) (U32.v j)

// Properties about disjointness of locations

val rs_loc_elem_disj:
  #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} ->
  k:nat{i <= k && k < j} ->
  l:nat{i <= l && l < j && k <> l} ->
  Lemma (requires (rs_elems_reg rg rs prid i j))
        (ensures (loc_disjoint (rs_loc_elem rg rs k)
                               (rs_loc_elem rg rs l)))
let rs_loc_elem_disj #a #rst rg rs prid i j k l = ()

val rs_loc_elem_disj_forall:
  #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} ->
  Lemma (requires (rs_elems_reg rg rs prid i j))
        (ensures (
          forall (k:nat{i <= k && k < j}).
          forall (l:nat{i <= l && l < j && k <> l}).
            loc_disjoint (rs_loc_elem rg rs k)
                         (rs_loc_elem rg rs l)))
let rs_loc_elem_disj_forall #a #rst rg rs prid i j = ()

val rs_loc_elems_elem_disj:
  #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} ->
  k1:nat{i <= k1} ->
  k2:nat{k1 <= k2 && k2 <= j} ->
  l:nat{i <= l && l < j && (l < k1 || k2 <= l)} ->
  Lemma (requires (rs_elems_reg rg rs prid i j))
        (ensures (loc_disjoint (rs_loc_elems rg rs k1 k2)
                               (rs_loc_elem rg rs l)))
        (decreases k2)
let rec rs_loc_elems_elem_disj #a #rst rg rs prid i j k1 k2 l =
  if k1 = k2 then ()
  else (rs_loc_elem_disj rg rs prid i j (k2 - 1) l;
       rs_loc_elems_elem_disj rg rs prid i j k1 (k2 - 1) l)

val rs_loc_elems_disj:
  #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} ->
  k1:nat{i <= k1} ->
  k2:nat{k1 <= k2 && k2 <= j} ->
  l1:nat{i <= l1} ->
  l2:nat{l1 <= l2 && l2 <= j} ->
  Lemma (requires (rs_elems_reg rg rs prid i j /\ (k2 <= l1 || l2 <= k1)))
        (ensures (loc_disjoint (rs_loc_elems rg rs k1 k2)
                               (rs_loc_elems rg rs l1 l2)))
        (decreases k2)
let rec rs_loc_elems_disj #a #rst rg rs prid i j k1 k2 l1 l2 =
  if k1 = k2 then ()
  else (rs_loc_elems_elem_disj rg rs prid i j l1 l2 (k2 - 1);
       rs_loc_elems_disj rg rs prid i j k1 (k2 - 1) l1 l2)

val rv_loc_elems_disj:
  #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} ->
  k1:uint32_t{i <= k1} ->
  k2:uint32_t{k1 <= k2 && k2 <= j} ->
  l1:uint32_t{i <= l1} ->
  l2:uint32_t{l1 <= l2 && l2 <= j} ->
  Lemma (requires (rv_elems_reg h rv i j /\ (k2 <= l1 || l2 <= k1)))
        (ensures (loc_disjoint (rv_loc_elems h rv k1 k2)
                               (rv_loc_elems h rv l1 l2)))
let rv_loc_elems_disj #a #rst #rg h rv i j k1 k2 l1 l2 =
  rs_loc_elems_disj rg (V.as_seq h rv) (V.frameOf rv)
    (U32.v i) (U32.v j) (U32.v k1) (U32.v k2) (U32.v l1) (U32.v l2)

val rs_loc_elems_parent_disj:
  #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} ->
  Lemma (requires (rs_elems_reg rg rs prid i j))
        (ensures (loc_disjoint (rs_loc_elems rg rs i j)
                               (loc_region_only false prid)))
        (decreases j)
let rec rs_loc_elems_parent_disj #a #rst rg rs prid i j =
  if i = j then ()
  else rs_loc_elems_parent_disj rg rs prid i (j - 1)

val rv_loc_elems_parent_disj:
  #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_reg h rv i j))
        (ensures (loc_disjoint (rv_loc_elems h rv i j)
                               (loc_region_only false (V.frameOf rv))))
let rv_loc_elems_parent_disj #a #rst #rg h rv i j =
  rs_loc_elems_parent_disj rg (V.as_seq h rv) (V.frameOf rv) (U32.v i) (U32.v j)

val rs_loc_elems_each_disj:
  #a:Type0 -> #rst:Type -> rg:regional rst a ->
  rs:S.seq a -> drid:HS.rid ->
  i:nat -> j:nat{i <= j && j <= S.length rs} ->
  Lemma (requires (V.forall_seq rs i j
                    (fun r -> HS.disjoint (Rgl?.region_of rg r) drid)))
        (ensures (loc_disjoint (rs_loc_elems rg rs i j)
                               (loc_all_regions_from false drid)))
        (decreases j)
let rec rs_loc_elems_each_disj #a #rst rg rs drid i j =
  if i = j then ()
  else rs_loc_elems_each_disj rg rs drid i (j - 1)

val rv_loc_elems_each_disj:
  #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} ->
  drid:HS.rid ->
  Lemma (requires (V.forall_ h rv i j
                    (fun r -> HS.disjoint (Rgl?.region_of rg r) drid)))
        (ensures (loc_disjoint (rv_loc_elems h rv i j)
                               (loc_all_regions_from false drid)))
let rv_loc_elems_each_disj #a #rst #rg h rv i j drid =
  rs_loc_elems_each_disj rg (V.as_seq h rv) drid (U32.v i) (U32.v j)

// Preservation based on disjointness

val rv_loc_elems_preserved:
  #a:Type0 -> #rst:Type -> #rg:regional rst a -> rv:rvector rg ->
  i:uint32_t -> j:uint32_t{i <= j && j <= V.size_of rv} ->
  p:loc -> h0:HS.mem -> h1:HS.mem ->
  Lemma (requires (V.live h0 rv /\
                  loc_disjoint p (V.loc_vector_within rv i j) /\
                  modifies p h0 h1))
        (ensures (rv_loc_elems h0 rv i j ==
                 rv_loc_elems h1 rv i j))
        (decreases (U32.v j))
let rec rv_loc_elems_preserved #a #rst #rg rv i j p h0 h1 =
  if i = j then ()
  else (V.loc_vector_within_includes rv i j (j - 1ul) j;
       V.get_preserved rv (j - 1ul) p h0 h1;
       assert (V.get h0 rv (j - 1ul) == V.get h1 rv (j - 1ul));
       V.loc_vector_within_includes rv i j i (j - 1ul);
       rv_loc_elems_preserved rv i (j - 1ul) p h0 h1)

val rs_elems_inv_preserved:
  #a:Type0 -> #rst:Type -> rg:regional rst a -> rs:S.seq a ->
  i:nat -> j:nat{i <= j && j <= S.length rs} ->
  p:loc -> h0:HS.mem -> h1:HS.mem ->
  Lemma (requires (rs_elems_inv rg h0 rs i j /\
                  loc_disjoint p (rs_loc_elems rg rs i j) /\
                  modifies p h0 h1))
        (ensures (rs_elems_inv rg h1 rs i j))
        (decreases j)
let rec rs_elems_inv_preserved #a #rst rg rs i j p h0 h1 =
  if i = j then ()
  else (rs_elems_inv_preserved rg rs i (j - 1) p h0 h1;
       Rgl?.r_sep rg (S.index rs (j - 1)) p h0 h1)

val rv_elems_inv_preserved:
  #a:Type0 -> #rst:Type -> #rg:regional rst a -> rv:rvector rg ->
  i:uint32_t -> j:uint32_t{i <= j && j <= V.size_of rv} ->
  p:loc -> h0:HS.mem -> h1:HS.mem ->
  Lemma (requires (V.live h0 rv /\
                  rv_elems_inv h0 rv i j /\
                  loc_disjoint p (V.loc_vector rv) /\
                  loc_disjoint p (rv_loc_elems h0 rv i j) /\
                  modifies p h0 h1))
        (ensures (rv_elems_inv h1 rv i j))
let rv_elems_inv_preserved #a #rst #rg rv i j p h0 h1 =
  rs_elems_inv_preserved rg (V.as_seq h0 rv) (U32.v i) (U32.v j) p h0 h1

val rv_inv_preserved_:
  #a:Type0 -> #rst:Type -> #rg:regional rst a -> rv:rvector rg ->
  p:loc -> h0:HS.mem -> h1:HS.mem ->
  Lemma (requires (rv_inv h0 rv /\
                  loc_disjoint p (loc_vector rv) /\
                  loc_disjoint p (rv_loc_elems h0 rv 0ul (V.size_of rv)) /\
                  modifies p h0 h1))
        (ensures (rv_inv h1 rv))
let rv_inv_preserved_ #a #rst #rg rv p h0 h1 =
  rv_elems_inv_preserved #a #rst #rg rv 0ul (V.size_of rv) p h0 h1

// The first core lemma of `rvector`
val rv_inv_preserved:
  #a:Type0 -> #rst:Type -> #rg:regional rst a -> rv:rvector rg ->
  p:loc -> h0:HS.mem -> h1:HS.mem ->
  Lemma (requires (rv_inv h0 rv /\
                  loc_disjoint p (loc_rvector rv) /\
                  modifies p h0 h1))
        (ensures (rv_inv h1 rv))
        [SMTPat (rv_inv h0 rv);
        SMTPat (loc_disjoint p (loc_rvector rv));
        SMTPat (modifies p h0 h1)]
let rv_inv_preserved #a #rst #rg rv p h0 h1 =
  assert (loc_includes (loc_rvector rv) (V.loc_vector rv));
  rv_loc_elems_included h0 rv 0ul (V.size_of rv);
  assert (loc_includes (loc_rvector rv) (rv_loc_elems h0 rv 0ul (V.size_of rv)));
  rv_inv_preserved_ rv p h0 h1

val rv_inv_preserved_int:
  #a:Type0 -> #rst:Type -> #rg:regional rst a -> rv:rvector rg ->
  i:uint32_t{i < V.size_of rv} ->
  h0:HS.mem -> h1:HS.mem ->
  Lemma (requires (rv_inv h0 rv /\
                  modifies (loc_all_regions_from false
                             (Rgl?.region_of rg (V.get h0 rv i))) h0 h1 /\
                  rg_inv rg h1 (V.get h1 rv i)))
        (ensures (rv_inv h1 rv))
let rv_inv_preserved_int #a #rst #rg rv i h0 h1 =
  rs_loc_elems_elem_disj
    rg (V.as_seq h0 rv) (V.frameOf rv)
    0 (U32.v (V.size_of rv)) 0 (U32.v i) (U32.v i);
  rs_elems_inv_preserved
    rg (V.as_seq h0 rv) 0 (U32.v i)
    (loc_all_regions_from false
      (Rgl?.region_of rg (V.get h1 rv i)))
    h0 h1;
  rs_loc_elems_elem_disj
    rg (V.as_seq h0 rv) (V.frameOf rv)
    0 (U32.v (V.size_of rv))
    (U32.v i + 1) (U32.v (V.size_of rv)) (U32.v i);
  rs_elems_inv_preserved
    rg (V.as_seq h0 rv) (U32.v i + 1) (U32.v (V.size_of rv))
    (loc_all_regions_from false
      (Rgl?.region_of rg (V.get h1 rv i)))
    h0 h1

/// Representation

val as_seq_seq:
  #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 /\
    rs_elems_inv rg h rs i j} ->
  GTot (s:S.seq (Rgl?.repr rg){S.length s = j - i})
       (decreases j)
let rec as_seq_seq #a #rst rg h rs i j =
  if i = j then S.empty
  else S.snoc (as_seq_seq rg h rs i (j - 1))
              (Rgl?.r_repr rg h (S.index rs (j - 1)))

val as_seq_sub:
  #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 /\
    rv_elems_inv h rv i j} ->
  GTot (s:S.seq (Rgl?.repr rg){S.length s = U32.v j - U32.v i})
       (decreases (U32.v j))
let as_seq_sub #a #rst #rg h rv i j =
  as_seq_seq rg h (V.as_seq h rv) (U32.v i) (U32.v j)

val as_seq:
  #a:Type0 -> #rst:Type -> #rg:regional rst a ->
  h:HS.mem -> rv:rvector rg{rv_inv h rv} ->
  GTot (s:S.seq (Rgl?.repr rg){S.length s = U32.v (V.size_of rv)})
let as_seq #a #rst #rg h rv =
  as_seq_sub h rv 0ul (V.size_of rv)

val as_seq_sub_as_seq:
  #a:Type0 -> #rst:Type -> #rg:regional rst a ->
  h:HS.mem -> rv:rvector rg{rv_inv h rv} ->
  Lemma (S.equal (as_seq_sub h rv 0ul (V.size_of rv))
                 (as_seq h rv))
        [SMTPat (as_seq_sub h rv 0ul (V.size_of rv))]
let as_seq_sub_as_seq #a #rst #rg h rv = ()

val as_seq_seq_index:
  #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 /\ rs_elems_inv rg h rs i j} ->
  k:nat{k < j - i} ->
  Lemma (requires true)
        (ensures (S.index (as_seq_seq rg h rs i j) k ==
                 Rgl?.r_repr rg h (S.index rs (i + k))))
        (decreases j)
        [SMTPat (S.index (as_seq_seq rg h rs i j) k)]
let rec as_seq_seq_index #a #rst rg h rs i j k =
  if i = j then ()
  else if k = j - i - 1 then ()
  else as_seq_seq_index rg h rs i (j - 1) k

val as_seq_seq_eq:
  #a:Type0 -> #rst:Type -> rg:regional rst a ->
  h:HS.mem -> rs1:S.seq a -> rs2:S.seq a ->
  i:nat ->
  j:nat{i <= j /\ j <= S.length rs1 /\ rs_elems_inv rg h rs1 i j} ->
  k:nat ->
  l:nat{k <= l /\ l <= S.length rs2 /\ rs_elems_inv rg h rs2 k l} ->
  Lemma (requires (S.equal (S.slice rs1 i j) (S.slice rs2 k l)))
        (ensures (S.equal (as_seq_seq rg h rs1 i j)
                          (as_seq_seq rg h rs2 k l)))
val as_seq_seq_eq:
  #a:Type0 -> #rst:Type -> rg:regional rst a ->
  h:HS.mem -> rs1:S.seq a -> rs2:S.seq a ->
  i:nat ->
  j:nat{i <= j /\ j <= S.length rs1 /\ rs_elems_inv rg h rs1 i j} ->
  k:nat ->
  l:nat{k <= l /\ l <= S.length rs2 /\ rs_elems_inv rg h rs2 k l} ->
  Lemma (requires (S.equal (S.slice rs1 i j) (S.slice rs2 k l)))
        (ensures (S.equal (as_seq_seq rg h rs1 i j)
                          (as_seq_seq rg h rs2 k l)))

    rg: LowStar.Regional.regional rst a ->
    h: FStar.Monotonic.HyperStack.mem ->
    rs1: FStar.Seq.Base.seq a ->
    rs2: FStar.Seq.Base.seq a ->
    i: FStar.Integers.nat ->
    j:
      FStar.Integers.nat
        {i <= j /\ j <= FStar.Seq.Base.length rs1 /\ LowStar.RVector.rs_elems_inv rg h rs1 i j} ->
    k: FStar.Integers.nat ->
    l:
      FStar.Integers.nat
        {k <= l /\ l <= FStar.Seq.Base.length rs2 /\ LowStar.RVector.rs_elems_inv rg h rs2 k l}
  -> FStar.Pervasives.Lemma
      (requires FStar.Seq.Base.equal (FStar.Seq.Base.slice rs1 i j) (FStar.Seq.Base.slice rs2 k l))
      (ensures
        FStar.Seq.Base.equal (LowStar.RVector.as_seq_seq rg h rs1 i j)
          (LowStar.RVector.as_seq_seq rg h rs2 k l))