val loc_vector_within_union_rev:
  #a:Type -> vec:vector a ->
  i:uint32_t -> j:uint32_t{i < j && j <= size_of vec} ->
  Lemma (requires True)
        (ensures (loc_vector_within vec i j ==
                 loc_union (loc_vector_within vec i (j - 1ul))
                           (loc_vector_within vec (j - 1ul) j)))
        (decreases (U32.v (j - i)))
let rec loc_vector_within_union_rev #a vec i j =
  if i = j - 1ul then ()
  else begin
    loc_vector_within_union_rev vec (i + 1ul) j;
    loc_union_assoc (B.loc_buffer (B.gsub (Vec?.vs vec) i 1ul))
                    (loc_vector_within vec (i + 1ul) (j - 1ul))
                    (loc_vector_within vec (j - 1ul) j)
  end
val loc_vector_within_union_rev:
  #a:Type -> vec:vector a ->
  i:uint32_t -> j:uint32_t{i < j && j <= size_of vec} ->
  Lemma (requires True)
        (ensures (loc_vector_within vec i j ==
                 loc_union (loc_vector_within vec i (j - 1ul))
                           (loc_vector_within vec (j - 1ul) j)))
        (decreases (U32.v (j - i)))
let rec loc_vector_within_union_rev #a vec i j =
if i = j - 1ul
then ()
else
  (loc_vector_within_union_rev vec (i + 1ul) j;
    loc_union_assoc (B.loc_buffer (B.gsub (Vec?.vs vec) i 1ul))
      (loc_vector_within vec (i + 1ul) (j - 1ul))
      (loc_vector_within vec (j - 1ul) j))
LowStar.Vector.fst.checked
prims.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
LowStar.Vector.fst
LowStar.Vector.vector LowStar.Vector.uint32_t Prims.b2t Prims.op_AmpAmp FStar.Integers.op_Less FStar.Integers.Unsigned FStar.Integers.W32 FStar.Integers.op_Less_Equals LowStar.Vector.size_of Prims.op_Equality FStar.UInt32.t FStar.Integers.op_Subtraction FStar.UInt32.__uint_to_t Prims.bool LowStar.Monotonic.Buffer.loc_union_assoc LowStar.Monotonic.Buffer.loc_buffer LowStar.Buffer.trivial_preorder LowStar.Buffer.gsub LowStar.Vector.__proj__Vec__item__vs LowStar.Vector.loc_vector_within FStar.Integers.op_Plus Prims.unit LowStar.Vector.loc_vector_within_union_rev
(*
   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.Vector


(**
 * This module provides support for mutable, partially filled arrays
 * whose contents may grow up to some fixed capacity determined
 * during initialization.
 *
 * Vectors support an insertion operation that may, if the capacity
 * has been reached, involve copying its contents to a new
 * vector of twice the capacity (so long as the capacity has not
 * already reached max_uint32).
 *
 * Conversely, an operation called `flush` is also provided to
 * shrink a vector to some prefix of its current contents.
 *
 * Other operations are fairly standard, and involve reading,
 * writing, and iterating over a vector.
 *
 *)

open FStar.Integers
open LowStar.Modifies

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

type uint32_t = UInt32.t

val max_uint32: uint32_t
let max_uint32 = 4294967295ul // UInt32.uint_to_t (UInt.max_int UInt32.n)

module U32 = FStar.UInt32

/// Abstract vector type

inline_for_extraction noeq type vector_str a =
| Vec: sz:uint32_t ->
       cap:uint32_t{cap >= sz} ->
       vs:B.buffer a{B.len vs = cap} ->
       vector_str a

val vector (a: Type0): Tot Type0
let vector a = vector_str a

/// Specification

val as_seq:
  HS.mem -> #a:Type -> vec:vector a ->
  GTot (s:S.seq a{S.length s = U32.v (Vec?.sz vec)})
let as_seq h #a vec =
  B.as_seq h (B.gsub (Vec?.vs vec) 0ul (Vec?.sz vec))

/// Capacity

inline_for_extraction val size_of: #a:Type -> vec:vector a -> Tot uint32_t
inline_for_extraction let size_of #a vec =
  Vec?.sz vec

inline_for_extraction val capacity_of: #a:Type -> vec:vector a -> Tot uint32_t
inline_for_extraction let capacity_of #a vec =
  Vec?.cap vec

val is_empty: #a:Type -> vec:vector a -> Tot bool
let is_empty #a vec =
  size_of vec = 0ul

val is_full: #a:Type -> vstr:vector_str a -> GTot bool
let is_full #a vstr =
  Vec?.sz vstr >= max_uint32

/// Memory-related

val live: #a:Type -> HS.mem -> vector a -> GTot Type0
let live #a h vec =
  B.live h (Vec?.vs vec)

val freeable: #a:Type -> vector a -> GTot Type0
let freeable #a vec =
  B.freeable (Vec?.vs vec)

val loc_vector: #a:Type -> vector a -> GTot loc
let loc_vector #a vec =
  B.loc_buffer (Vec?.vs vec)

val loc_addr_of_vector: #a:Type -> vector a -> GTot loc
let loc_addr_of_vector #a vec =
  B.loc_addr_of_buffer (Vec?.vs vec)

val loc_vector_within:
  #a:Type -> vec:vector a ->
  i:uint32_t -> j:uint32_t{i <= j && j <= size_of vec} ->
  GTot loc (decreases (U32.v (j - i)))
let rec loc_vector_within #a vec i j =
  if i = j then loc_none
  else loc_union (B.loc_buffer (B.gsub (Vec?.vs vec) i 1ul))
                 (loc_vector_within vec (i + 1ul) j)

val loc_vector_within_includes_:
  #a:Type -> vec:vector a ->
  i:uint32_t ->
  j1:uint32_t{i <= j1 && j1 <= size_of vec} ->
  j2:uint32_t{i <= j2 && j2 <= j1} ->
  Lemma (requires True)
        (ensures (loc_includes (loc_vector_within vec i j1)
                               (loc_vector_within vec i j2)))
        (decreases (U32.v (j1 - i)))
let rec loc_vector_within_includes_ #a vec i j1 j2 =
  if i = j1 then ()
  else if i = j2 then ()
  else begin
    loc_vector_within_includes_ vec (i + 1ul) j1 j2;
    loc_includes_union_l (B.loc_buffer (B.gsub (Vec?.vs vec) i 1ul))
                         (loc_vector_within vec (i + 1ul) j1)
                         (loc_vector_within vec (i + 1ul) j2);
    loc_includes_union_r (loc_vector_within vec i j1)
                         (B.loc_buffer (B.gsub (Vec?.vs vec) i 1ul))
                         (loc_vector_within vec (i + 1ul) j2)
  end

val loc_vector_within_includes:
  #a:Type -> vec:vector a ->
  i1:uint32_t -> j1:uint32_t{i1 <= j1 && j1 <= size_of vec} ->
  i2:uint32_t{i1 <= i2} -> j2:uint32_t{i2 <= j2 && j2 <= j1} ->
  Lemma (requires True)
        (ensures (loc_includes (loc_vector_within vec i1 j1)
                               (loc_vector_within vec i2 j2)))
        (decreases (U32.v (j1 - i1)))
let rec loc_vector_within_includes #a vec i1 j1 i2 j2 =
  if i1 = j1 then ()
  else if i1 = i2 then loc_vector_within_includes_ vec i1 j1 j2
  else begin
    loc_vector_within_includes vec (i1 + 1ul) j1 i2 j2;
    loc_includes_union_l (B.loc_buffer (B.gsub (Vec?.vs vec) i1 1ul))
                         (loc_vector_within vec (i1 + 1ul) j1)
                         (loc_vector_within vec i2 j2)
  end

val loc_vector_within_included:
  #a:Type -> vec:vector a ->
  i:uint32_t -> j:uint32_t{i <= j && j <= size_of vec} ->
  Lemma (requires True)
        (ensures (loc_includes (loc_vector vec)
                               (loc_vector_within vec i j)))
        (decreases (U32.v (j - i)))
let rec loc_vector_within_included #a vec i j =
  if i = j then ()
  else loc_vector_within_included vec (i + 1ul) j

val loc_vector_within_disjoint_:
  #a:Type -> vec:vector a ->
  i1:uint32_t ->
  i2:uint32_t{i1 < i2} ->
  j2:uint32_t{i2 <= j2 && j2 <= size_of vec} ->
  Lemma (requires True)
        (ensures (loc_disjoint (B.loc_buffer (B.gsub (Vec?.vs vec) i1 1ul))
                               (loc_vector_within vec i2 j2)))
        (decreases (U32.v (j2 - i2)))
let rec loc_vector_within_disjoint_ #a vec i1 i2 j2 =
  if i2 = j2 then ()
  else loc_vector_within_disjoint_ vec i1 (i2 + 1ul) j2

val loc_vector_within_disjoint:
  #a:Type -> vec:vector a ->
  i1:uint32_t -> j1:uint32_t{i1 <= j1 && j1 <= size_of vec} ->
  i2:uint32_t{j1 <= i2} -> j2:uint32_t{i2 <= j2 && j2 <= size_of vec} ->
  Lemma (requires True)
        (ensures (loc_disjoint (loc_vector_within vec i1 j1)
                               (loc_vector_within vec i2 j2)))
        (decreases (U32.v (j1 - i1)))
let rec loc_vector_within_disjoint #a vec i1 j1 i2 j2 =
  if i1 = j1 then ()
  else (loc_vector_within_disjoint_ vec i1 i2 j2;
       loc_vector_within_disjoint vec (i1 + 1ul) j1 i2 j2)

val loc_vector_within_union_rev:
  #a:Type -> vec:vector a ->
  i:uint32_t -> j:uint32_t{i < j && j <= size_of vec} ->
  Lemma (requires True)
        (ensures (loc_vector_within vec i j ==
                 loc_union (loc_vector_within vec i (j - 1ul))
                           (loc_vector_within vec (j - 1ul) j)))
        (decreases (U32.v (j - i)))
val loc_vector_within_union_rev:
  #a:Type -> vec:vector a ->
  i:uint32_t -> j:uint32_t{i < j && j <= size_of vec} ->
  Lemma (requires True)
        (ensures (loc_vector_within vec i j ==
                 loc_union (loc_vector_within vec i (j - 1ul))
                           (loc_vector_within vec (j - 1ul) j)))
        (decreases (U32.v (j - i)))

    vec: LowStar.Vector.vector a ->
    i: LowStar.Vector.uint32_t ->
    j: LowStar.Vector.uint32_t{i < j && j <= LowStar.Vector.size_of vec}
  -> FStar.Pervasives.Lemma
      (ensures
        LowStar.Vector.loc_vector_within vec i j ==
        LowStar.Monotonic.Buffer.loc_union (LowStar.Vector.loc_vector_within vec i (j - 1ul))
          (LowStar.Vector.loc_vector_within vec (j - 1ul) j)) (decreases FStar.UInt32.v (j - i))