val is_full_array (#elt: Type) (a: array elt) : Tot prop
let is_full_array (#elt: Type) (a: array elt) : Tot prop =
  length a == base_len (base (ptr_of a))
val is_full_array (#elt: Type) (a: array elt) : Tot prop
let is_full_array (#elt: Type) (a: array elt) : Tot prop =
length a == base_len (base (ptr_of a))
Steel.ST.Array.fsti.checked
Steel.ST.Util.fsti.checked Steel.FractionalPermission.fst.checked prims.fst.checked FStar.SizeT.fsti.checked FStar.Seq.fst.checked FStar.PtrdiffT.fsti.checked FStar.Pervasives.fsti.checked FStar.Int.fsti.checked FStar.Ghost.fsti.checked
Steel.ST.Array.fsti
Steel.ST.Array.array Prims.eq2 Prims.nat Steel.ST.Array.length Steel.ST.Array.base_len Steel.ST.Array.base Steel.ST.Array.ptr_of Prims.prop
(*
   Copyright 2020, 2021, 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.
*)

module Steel.ST.Array

/// C arrays of universe 0 elements, with selectors.

module P = Steel.FractionalPermission
module US = FStar.SizeT
module UP = FStar.PtrdiffT

open Steel.ST.Util

/// NOTE: This module is defined on top of Steel.HigherArray, so its
/// definitions are all meant to be inlined and benefit from the
/// latter module's primitive extraction. We seal it under an
/// interface to avoid unpleasantly leaking the lifting of values
/// of lower universes into the SMT context. Due to this interface,
/// cross-module inlining must be enabled using F*'s --cmi option.

/// An abstract type to represent a base array (whole allocation
/// unit), exposed for proof purposes only
[@@erasable]
val base_t (elt: Type0) : Tot Type0
val base_len (#elt: Type) (b: base_t elt) : GTot nat

/// An abstract type to represent a C pointer, as a base and an offset
/// into its base
inline_for_extraction
[@@noextract_to "krml"]
val ptr ([@@@unused] elt: Type0) : Type0
inline_for_extraction
[@@noextract_to "krml"]
val null_ptr (elt: Type0) : ptr elt
// TODO: turn into a stateful operation to avoid comparing dangling pointers
inline_for_extraction
[@@noextract_to "krml"]
val is_null_ptr (#elt: Type0) (p: ptr elt) : Pure bool
  (requires True)
  (ensures (fun res -> res == true <==> p == null_ptr elt))
val base (#elt: Type) (p: ptr elt) : Tot (base_t elt)
val offset (#elt: Type) (p: ptr elt) : Ghost nat (requires True) (ensures (fun offset -> offset <= base_len (base p)))
val ptr_base_offset_inj (#elt: Type) (p1 p2: ptr elt) : Lemma
  (requires (
    base p1 == base p2 /\
    offset p1 == offset p2
  ))
  (ensures (
    p1 == p2
  ))
val base_len_null_ptr (elt: Type0) : Lemma
  (base_len (base (null_ptr elt)) == 0)
  [SMTPat (base_len (base (null_ptr elt)))]

/// A concrete type to represent a C array, as a C pointer and a ghost
/// array length.  By virtue of the length being ghost, Karamel will
/// extract this type as just ptr, but to inline the definition of
/// this type, we use standard dependent pairs instead of a custom
/// record type.
inline_for_extraction
[@@noextract_to "krml"]
let array ([@@@strictly_positive] elt: Type0) : Tot Type0 =
  (p: ptr elt & (length: Ghost.erased nat {offset p + length <= base_len (base p)}))

inline_for_extraction
[@@noextract_to "krml"]
let null (#a: Type0) : array a
= (| null_ptr a, Ghost.hide 0 |)

/// This will extract to "let p = a"
inline_for_extraction
[@@noextract_to "krml"]
let ptr_of
  (#elt: Type)
  (a: array elt)
: Tot (ptr elt)
= match a with // dfst is not marked inline_for_extraction, so we need to reimplement it
  | (| p, _ |) -> p

inline_for_extraction
[@@noextract_to "krml"]
let is_null (#a: Type0) (p: array a) : Pure bool
  (requires True)
  (ensures (fun res -> res == true <==> p == null))
= is_null_ptr (ptr_of p)

/// Returns the length of the array. Usable for specification and proof purposes,
/// as modeled by the GTot effect
let length (#elt: Type) (a: array elt) : GTot nat =
  dsnd a

val length_fits (#elt: Type) (a: array elt) : Lemma (US.fits (length a))

/// An abbreviation refining an array by its length
inline_for_extraction
[@@noextract_to "krml"]
let larray (t:Type) (n:nat) = a:array t{ length a = n }

/// The main representation predicate:
/// A Steel separation logic heap predicate to describe that an array
/// a points to some element sequence s with some permission p.
///
/// A big design decision in this library was whether the second index
/// of this predicate should be a [lseq t (length a)] or just a [seq t].
///
/// Making it an [lseq] forces every specification to be strongly
/// typed, in the sense that the logical representation of an array
/// has to be a sequence of the right length. This can be a little
/// cumbersome in specifications, particularly as the refinement appears
/// in some cases beneath the [erased] constructor.
///
/// So, we opted instead to let the index be just a [seq t], and
/// requiring length refinements on it in certain functions, only when
/// necessary.
val pts_to
  (#elt: Type0) (a: array elt)
  (p: P.perm)
  ([@@@ smt_fallback ] s: Seq.seq elt)
: Tot vprop

/// A stateful lemma to relate the size of an array with the size
/// of the element sequence it points to
/// This ghost function proves that an array always points to a
/// sequence of the appropriate length
val pts_to_length
  (#opened: _)
  (#elt: Type0)
  (#p: P.perm)
  (a: array elt)
  (s: Seq.seq elt)
: STGhost unit opened
    (pts_to a p s)
    (fun _ -> pts_to a p s)
    (True)
    (fun _ -> Seq.length s == length a)

val pts_to_not_null
  (#opened: _)
  (#elt: Type0)
  (#p: P.perm)
  (a: array elt)
  (s: Seq.seq elt)
: STGhost unit opened
    (pts_to a p s)
    (fun _ -> pts_to a p s)
    (True)
    (fun _ -> a =!= null)

/// An injectivity property, needed only to define a selector.  Such a
/// selector can be only defined in universe 0, and universes are not
/// cumulative, so we need to define a separate module for arrays of
/// universe 0 elements with selectors, reusing definitions from this
/// interface, but we do not want to use `friend`.
val pts_to_inj
  (#elt: Type0) (a: array elt)
  (p1: P.perm)
  (s1: Seq.seq elt)
  (p2: P.perm)
  (s2: Seq.seq elt)
  (m: mem)
: Lemma
  (requires (
    interp (hp_of (pts_to a p1 s1)) m /\
    interp (hp_of (pts_to a p2 s2)) m
  ))
  (ensures (
    s1 == s2
  ))

/// Allocating a new array of size n, where each cell is initialized
/// with value x. We define the non-selector version of this operation
/// (and others) with a _pt suffix in the name.
val is_full_array (#elt: Type) (a: array elt) : Tot prop
a: Steel.ST.Array.array elt -> Prims.prop