val same_base_array (#a: Type) (arr1 arr2: array a) : prop
let same_base_array (#a:Type) (arr1 arr2: array a) : prop
 = base (ptr_of arr1) == base (ptr_of arr2)
val same_base_array (#a: Type) (arr1 arr2: array a) : prop
let same_base_array (#a: Type) (arr1 arr2: array a) : prop =
base (ptr_of arr1) == base (ptr_of arr2)
Steel.ArrayArith.fsti.checked
Steel.ST.Array.fsti.checked Steel.FractionalPermission.fst.checked Steel.Effect.Atomic.fsti.checked Steel.Effect.fsti.checked Steel.Array.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Steel.ArrayArith.fsti
Steel.ST.Array.array Prims.eq2 Steel.ST.Array.base_t Steel.ST.Array.base Steel.ST.Array.ptr_of Prims.prop
module Steel.ArrayArith

open Steel.FractionalPermission
open Steel.Effect.Atomic
open Steel.Effect
open Steel.ST.Array
open Steel.Array

(* This module provides a very restricted way of doing pointer arithmetic comparison on Steel arrays.
   Primitives in this module are considered builtins by karamel, and have handwritten C implementations.
   Clients using this module should extract with the krml options
   `-static-header Steel.ArrayArith -no-prefix Steel.ArrayArith`
*)

/// The main predicate of this module. `within_bounds` captures that [p] is part of the same
/// allocation unit as [arr1] and [arr2], and situated in between. It is an abstract predicate,
/// that can only be introduced by the `within_bounds_intro` function below.
val within_bounds (#a: Type) (arr1 p arr2: array a) : prop

/// An abbreviation capturing that [arr1] and [arr2] belong to the same array,
/// and hence to the same allocation unit according to the Steel memory model
unfold
val same_base_array (#a: Type) (arr1 arr2: array a) : prop
arr1: Steel.ST.Array.array a -> arr2: Steel.ST.Array.array a -> Prims.prop