let pts_to (#a:Type0) (r:ref a) ([@@@smt_fallback] p:perm) ([@@@ smt_fallback] v:a)
  = to_vprop (pts_to_sl r p v)
let pts_to (#a: Type0) (r: ref a) ([@@@ smt_fallback]p: perm) ([@@@ smt_fallback]v: a) =
to_vprop (pts_to_sl r p v)
Steel.Reference.fsti.checked
Steel.Memory.fsti.checked Steel.FractionalPermission.fst.checked Steel.Effect.Atomic.fsti.checked Steel.Effect.fsti.checked prims.fst.checked FStar.UInt32.fsti.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Steel.Reference.fsti
Steel.Reference.ref Steel.FractionalPermission.perm Steel.Effect.Common.to_vprop Steel.Reference.pts_to_sl Steel.Effect.Common.vprop
(*
   Copyright 2020 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.Reference

open FStar.Ghost
open Steel.FractionalPermission

open Steel.Memory
open Steel.Effect.Atomic
open Steel.Effect


module U32 = FStar.UInt32
module Mem = Steel.Memory

/// The main user-facing Steel library.
/// This library provides functions to operate on references to values in universe 0, such as uints.
/// This library provides two versions, which can interoperate with each other.
/// The first one uses the standard separation logic pts_to predicate, and has a non-informative selector
/// The second one has a selector which returns the contents of the reference in memory, enabling
/// to better separate reasoning about memory safety and functional correctness when handling references.

/// An abstract datatype for references
val ref ([@@@unused] a:Type0) : Type0

/// The null pointer
[@@ noextract_to "krml"]
val null (#a:Type0) : ref a

/// Checking whether a pointer is null can be done in a decidable way
[@@ noextract_to "krml"]
val is_null (#a:Type0) (r:ref a) : (b:bool{b <==> r == null})

(** First version of references: Non-informative selector and standard pts_to predicate.
    All functions names here are postfixed with _pt (for points_to)**)

/// The standard points to separation logic assertion, expressing that
/// reference [r] is valid in memory, stores value [v], and that we have
/// permission [p] on it.
val pts_to_sl (#a:Type0) (r:ref a) (p:perm) (v:a) : slprop u#1

/// Lifting the standard points to predicate to vprop, with a non-informative selector.
/// The permission [p] and the value [v] are annotated with the smt_fallback attribute,
/// enabling SMT rewriting on them during frame inference
[@@ __steel_reduce__]
val pts_to : r: Steel.Reference.ref a -> p: Steel.FractionalPermission.perm -> v: a -> Steel.Effect.Common.vprop
r: Steel.Reference.ref a -> p: Steel.FractionalPermission.perm -> v: a -> Steel.Effect.Common.vprop