val elem_precedes (#a: Type u#a) (s: t a) (i: nat{i < length s}) : Lemma (index s i << s)
let elem_precedes (#a:Type u#a) (s:t a) (i : nat{i < length s})
  : Lemma (index s i << s)
  = FStar.List.Tot.(
      to_list_precedes s;
      let l = to_list s in
      assert (memP (index l i) l);
      memP_precedes (index l i) l
    )
val elem_precedes (#a: Type u#a) (s: t a) (i: nat{i < length s}) : Lemma (index s i << s)
let elem_precedes (#a: Type u#a) (s: t a) (i: nat{i < length s}) : Lemma (index s i << s) =
let open FStar.List.Tot in
to_list_precedes s;
let l = to_list s in
assert (memP (index l i) l);
memP_precedes (index l i) l
FStar.ImmutableArray.fsti.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.ImmutableArray.Base.fsti.checked
FStar.ImmutableArray.fsti
FStar.ImmutableArray.Base.t Prims.nat Prims.b2t Prims.op_LessThan FStar.ImmutableArray.Base.length FStar.List.Tot.Properties.memP_precedes FStar.List.Tot.Base.index Prims.unit Prims._assert FStar.List.Tot.Base.memP Prims.list FStar.ImmutableArray.to_list FStar.ImmutableArray.to_list_precedes Prims.l_True Prims.squash Prims.precedes FStar.ImmutableArray.Base.index Prims.Nil FStar.Pervasives.pattern
(*
   Copyright 2022 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: N. Swamy
*)

(* This module provides a primitive type of immutable arrays,
   implemented in OCaml by an array.

   The main intended usage of this module, as suggested by Jay Lorch,
   is to provide a sequence-like type with constant-time random access
   of elements, as opposed to FStar.Seq and related types, which
   provide only linear time access.
   
   Both the F* normalizer and NBE engine are aware of this type and
   reduce its three functions, `of_list`, `length`, and `index`, by
   invoking the corresponding operations on the underlying OCaml array
   that represents a `t`.

   See tests/micro-benchmarks/TestImmutableArray.fst for some samples
   
   And also FStar.ImmutableArray, which includes this interface and 
   augments it with various properties of the functions below.
  
*)
module FStar.ImmutableArray
include FStar.ImmutableArray.Base

(* Converting an immutable array back to a list *)
val to_list (#a:Type u#a) (s:t a)
  : Tot (list a)

(* to_list is the inverse of of_list *)
val to_list_of_list (#a:Type u#a) (l:list a)
  : Lemma (to_list (of_list l) == l)
          [SMTPat (of_list l)]

(* of_list is the inverse of to_list *)
val of_list_to_list (#a:Type u#a) (s:t a)
  : Lemma (of_list (to_list s) == s)

(* The length of an immutable array is the length of its corresponding list *)
val length_spec (#a:Type u#a) (s:t a)
  : Lemma (length s == FStar.List.Tot.length (to_list s))
          [SMTPat (length s)]

(* The indexes of an immutable array are in correspondence with its underling list *)
val index_spec (#a:Type u#a) (s:t a) (i:nat{ i < length s })
  : Lemma (index s i == FStar.List.Tot.index (to_list s) i)
          [SMTPat (index s i)]

(* The list of elements precedes the array.*)
val to_list_precedes (#a:Type u#a) (s:t a)
  : Lemma (to_list s << s)

(* Idem. *)
let of_list_precedes (#a:Type u#a) (l:list a)
  : Lemma (l << of_list l)
  = to_list_precedes (of_list l)

(* An explicit proof that elements of the array precede the array. *)
let elem_precedes (#a:Type u#a) (s:t a) (i : nat{i < length s})
val elem_precedes (#a: Type u#a) (s: t a) (i: nat{i < length s}) : Lemma (index s i << s)
s: FStar.ImmutableArray.Base.t a -> i: Prims.nat{i < FStar.ImmutableArray.Base.length s}
  -> FStar.Pervasives.Lemma (ensures FStar.ImmutableArray.Base.index s i << s)