let property (a:Type)
  = a -> prop
let property (a: Type) =
a -> prop
Steel.GhostMonotonicHigherReference.fsti.checked
Steel.Memory.fsti.checked Steel.FractionalPermission.fst.checked Steel.Effect.Atomic.fsti.checked Steel.Effect.fsti.checked prims.fst.checked FStar.Preorder.fst.checked FStar.Pervasives.fsti.checked FStar.PCM.fst.checked FStar.Ghost.fsti.checked
Steel.GhostMonotonicHigherReference.fsti
Prims.prop
(*
   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.GhostMonotonicHigherReference

open FStar.PCM
open FStar.Ghost
open Steel.FractionalPermission

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

module Preorder = FStar.Preorder

/// A library for Steel references that are monotonic with respect to a user-specified preorder.
/// This library builds on top of Steel.HigherReference, and is specialized to values at universe 1.

/// An abstract datatype for monotonic references
[@@erasable]
val ref (a:Type u#1) (p:Preorder.preorder a)
  : Type u#0

/// The standard points to separation logic predicate
val pts_to_sl (#a:Type) (#p:Preorder.preorder a) (r:ref a p) (f:perm) (v:a)
  : slprop u#1

/// Lifting the standard points to predicate to vprop, with a non-informative selector
[@@ __steel_reduce__]
unfold let pts_to (#a:Type) (#p:Preorder.preorder a) (r:ref a p) (f:perm) (v:a) : vprop =
  to_vprop (pts_to_sl r f v)

/// Allocates a reference with value [x]. We have full permission on the newly
/// allocated reference.
val alloc (#opened: _) (#a:Type) (p:Preorder.preorder a) (v:a)
  : SteelGhostT (ref a p) opened emp (fun r -> pts_to r full_perm v)

/// Writes value [x] in the reference [r], as long as we have full ownership of [r]
val write (#opened: _) (#a:Type) (#p:Preorder.preorder a) (#v:a)
          (r:ref a p) (x:a)
  : SteelGhost unit opened (pts_to r full_perm v)
               (fun v -> pts_to r full_perm x)
               (requires fun _ -> p v x /\ True)
               (ensures fun _ _ _ -> True)

/// A wrapper around a predicate that depends on a value of type [a]
val property : a: Type -> Type
a: Type -> Type