let avalue (#v:Type) (#p:preorder v) (anchors:anchor_rel p)
  = pv:(permission v & vhist p) { anchored anchors pv }
let avalue (#v: Type) (#p: preorder v) (anchors: anchor_rel p) =
pv: (permission v & vhist p){anchored anchors pv}
Steel.FractionalAnchoredPreorder.fst.checked
Steel.Preorder.fst.checked Steel.FractionalPermission.fst.checked prims.fst.checked FStar.Preorder.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.PCM.fst.checked
Steel.FractionalAnchoredPreorder.fst
FStar.Preorder.preorder Steel.FractionalAnchoredPreorder.anchor_rel FStar.Pervasives.Native.tuple2 Steel.FractionalAnchoredPreorder.permission Steel.Preorder.vhist Steel.FractionalAnchoredPreorder.anchored
(*
   Copyright 2021 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.

   Author: N. Swamy
*)
module Steel.FractionalAnchoredPreorder

(** This module provides a partial commutative monoid (PCM) for use in
    the ghost state of a concurrent Steel program.

    Its goal is to facilitate a form of information-sharing between
    multiple threads including the following features: Fractions,
    Preorders, Snapshots, and Anchors --- Anchors are the most
    unusual.

    1. Fractions: Ownership of the state is controlled by a fractional
       permission, so multiple threads may share read-only privileges
       on the state, but only one can have write permission.

    2. Preorders: The ghost state is governed by a preorder p and all
       updates to the state must respect the preorder (a reflexive,
       transitive relation on the state)

    3. Snapshots: Since the state always evolves by a preorder, it is
       possible to take a snapshot of the state. A snapshot does not
       confer any particular ownership on the state, except knowledge
       of a snapshot ensures that the current state is related to the
       snapshot by the preorder.

    4. Anchors are a kind of refinement of the preorder. If a thread
       owns an anchored value [v], then no other thread, even a thread
       owning a full fractional permission, can advance the state "too
       far" from the anchor. In particular, the PCM is parameterized
       by a binary relation on values, [anchors:anchor_relation]. If a
       thread owns the anchor [v], then the current value `cur` of the
       state must be in relation [v `anchors` cur]. This can be used
       to ensure that the knowledge of one thread is never becomes too
       stale.

   For example, this allows one to model a shared monotonically
   increasing counter, where if one thread anchors knowledge of the
   counter at the value 5, no other thread can increase the value of
   the counter beyond, say, 10, (when the anchor relation is y - x <=
   5), until the anchoring thread releases the anchor. Further, at any
   point, a thread can take a snapshot of the counter and rely on the
   fact that the value of the counter in the future will be >= the
   snapshot.
*)
open FStar.PCM
open FStar.Preorder
open Steel.Preorder
open Steel.FractionalPermission

#push-options "--fuel 0 --ifuel 2"

/// A permission: is a pair of
///
///   * an optional fractional permission; with `Some p` indicating
///     some ownership, while `None` is an additional "0" permission
///     value, to encode snapshots.
///
///   * and an optional anchor, where `Some a` indicates the current
///     value can't be too far from `a`.
let permission (v:Type) = option perm & option v

/// Non-zero permission is either a read or write permission
let has_nonzero #v (p:permission v) = Some? (fst p)
/// Has an anchor set
let has_anchor #v (p:permission v) = Some? (snd p)
/// Either an anchor or non-zero
let has_some_ownership #v (p:permission v) = has_nonzero p || has_anchor p
/// The anchoring value
let anchor_of #v (p:permission v { has_anchor p }) : v = Some?.v (snd p)

/// The anchoring relation:
///   -- A binary relation on values
///   -- refining the preorder
///   -- and if x `anchors` z then it also anchors any `y` between `x` and `z`
///
/// Explaining the third clause a bit:
/// Think intuitively of anchoring relations as a kind of distance measure
///
///   if `z` is close enough to `x` then if `z` is further than `y`
///   (since it is ahead of `y` in the preorder) then `y` is also
///   close enough to `x`
let anchor_rel (#v:Type) (p:preorder v) =
  anchors:(v -> v -> prop) {
    (forall v0 v1. anchors v0 v1 ==> p v0 v1) /\
    (forall x z. x `anchors` z  ==> (forall y. p x y /\ p y z ==> x `anchors` y)) //
  }

/// An implementation remark: We use Steel.Preorder here to
/// generically transform any preorder into a PCM. That works by
/// taking the value of the PCM to be a history of values related by
/// the preorder. So, throughout, we'll be using the the [vhist p]
/// from Steel.Preorder, the type of a non-empty history compatible
/// with [p]. The details of the histories don't matter much for our
/// purposes---we only care about the most recent value, for which
/// we'll use [curval v].

/// If the anchor is set, then the current value is anchored by it
let anchored (#v:Type) (#p:preorder v) (anchors:anchor_rel p)
             (pv:(permission v & vhist p))
  = has_anchor (fst pv) ==> anchor_of (fst pv) `anchors` curval (snd pv)

/// A value in our fractional anchored PCM is a pair of a permission
/// and a p-compatible history, refined to ensure that if the anchor
/// is set, then the current value is anchored by it.
val avalue : anchors: Steel.FractionalAnchoredPreorder.anchor_rel p -> Type
anchors: Steel.FractionalAnchoredPreorder.anchor_rel p -> Type