val ptr_of (#elt: Type) (a: array elt) : Tot (ptr elt)
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
val ptr_of (#elt: Type) (a: array elt) : Tot (ptr elt)
let ptr_of (#elt: Type) (a: array elt) : Tot (ptr elt) =
match a with | (| p , _ |) -> p
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 Steel.ST.Array.ptr FStar.Ghost.erased Prims.nat Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition Steel.ST.Array.offset FStar.Ghost.reveal Steel.ST.Array.base_len Steel.ST.Array.base
(*
   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)
val ptr_of (#elt: Type) (a: array elt) : Tot (ptr elt)
a: Steel.ST.Array.array elt -> Steel.ST.Array.ptr elt