val f_odd (n0: odd) (v: stepper{compatible p (Odd n0) v})
    : GTot (y: stepper{compatible p y v /\ frame_compatible (Odd n0) v y})
let f_odd (n0:odd) (v:stepper{compatible p (Odd n0) v})
  : GTot (y:stepper{compatible p y v /\ frame_compatible (Odd n0) v y})
  = match v with
    | Odd n0 -> Odd n0
    | OddWriteable n0 -> OddWriteable n0
    | V n -> if n = n0 then Odd n0 else OddWriteable n0
val f_odd (n0: odd) (v: stepper{compatible p (Odd n0) v})
    : GTot (y: stepper{compatible p y v /\ frame_compatible (Odd n0) v y})
let f_odd (n0: odd) (v: stepper{compatible p (Odd n0) v})
    : GTot (y: stepper{compatible p y v /\ frame_compatible (Odd n0) v y}) =
match v with
| Odd n0 -> Odd n0
| OddWriteable n0 -> OddWriteable n0
| V n -> if n = n0 then Odd n0 else OddWriteable n0
Steel.Stepper.fst.checked
Steel.PCMReference.fsti.checked Steel.Memory.fsti.checked Steel.Effect.Atomic.fsti.checked Steel.Effect.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.PCM.fst.checked FStar.Ghost.fsti.checked
Steel.Stepper.fst
Steel.Stepper.odd Steel.Stepper.stepper FStar.PCM.compatible Steel.Stepper.p Steel.Stepper.Odd Steel.Stepper.OddWriteable Prims.nat Prims.b2t Prims.op_GreaterThan Prims.op_Equality Prims.l_or Prims.op_disEquality Prims.int Prims.op_Modulus Prims.bool Prims.l_and Steel.Stepper.frame_compatible FStar.Ghost.hide
(*
   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.Stepper

open FStar.PCM

/// A simplified version of the Duplex library, specialized to a simple concrete
/// protocol, where the two parties take turns incrementing a counter.
/// This is modeled using the [stepper] PCM below

(* Some abbreviations and helpers to operate on natural numbers *)

let even = n:nat{n % 2 == 0}
let odd = n:nat{n % 2 <> 0}

let abs (n:int) : nat = if n >= 0 then n else -n
let max (n m:nat) : nat = if n >= m then n else m

/// The elements of the PCM regulating this protocol.
noeq
type stepper : Type u#1 =
  | V : n:nat{n > 0} -> stepper // the real value " whole value "
  | Even : n:even -> stepper
  | Odd  : n:odd -> stepper
  | EvenWriteable : even -> stepper
  | OddWriteable : odd -> stepper
  | None : stepper

let refine (s:stepper) : Tot prop = V? s \/ None? s

/// Specifying which elements of the PCM can be composed.
/// This PCM models a counter that the two parties increment one after the other.
/// As such, the two sides are always at most one apart
let composable' (s0 s1:stepper) : prop =
    match s0, s1 with
    | _, None
    | None, _ -> True
    | Even n, Odd m
    | Odd m , Even n -> abs (m-n) == 1
    | EvenWriteable n, Odd m | Odd m, EvenWriteable n -> m - n == 1
    | OddWriteable n, Even m | Even m, OddWriteable n -> m - n == 1
    | _ -> False

let composable : symrel stepper = composable'

/// The PCM composition function, defined on elements that are composable
let compose (s0:stepper) (s1:stepper{composable s0 s1}) =
    match s0, s1 with
    | a, None
    | None, a -> a
    | Even n, Odd m
    | Odd m, Even n -> V (max n m)
    | Odd m, EvenWriteable n | EvenWriteable n, Odd m -> V m
    | Even m, OddWriteable n | OddWriteable n, Even m -> V m

/// Combining them into the structure of the PCM
let p' : pcm' stepper = { composable = composable; op = compose; one = None }

(* Defining the different lemmas for the commutative monoid structure *)

let lemma_comm (x:stepper) (y:stepper{composable x y}) :
  Lemma (compose x y == compose y x)
  = ()

let lemma_assoc_l (x y:stepper) (z:stepper{composable y z /\ composable x (compose y z)})
  : Lemma (composable x y /\ composable (compose x y) z /\
           compose x (compose y z) == compose (compose x y) z)
  = ()

let lemma_assoc_r (x y:stepper) (z:stepper{composable x y /\ composable (compose x y) z})
  : Lemma (composable y z /\ composable x (compose y z) /\
           compose x (compose y z) == compose (compose x y) z)
  = ()

let lemma_is_unit (x:stepper) : Lemma (composable x None /\ compose x None == x)
  = ()

/// Full definition of the stepper PCM
let p : pcm stepper =
  { p = p';
    comm = lemma_comm;
    assoc = lemma_assoc_l;
    assoc_r = lemma_assoc_r;
    is_unit = lemma_is_unit;
    refine = refine }

open FStar.Ghost
open Steel.Memory
open Steel.Effect.Atomic
open Steel.Effect
open Steel.PCMReference
module PR = Steel.PCMReference

(*** Specializing the reference function for this specific PCM ***)

// Use erased values here to avoid some rewritings
[@@__reduce__]
let pts_to (r:ref stepper p) (v:erased stepper) = pts_to r v

[@@__reduce__]
let v (r:ref stepper p) (n:nat{n > 0}) : vprop = pts_to r (V n)

[@@__reduce__]
let s_even (r:ref stepper p) (n:nat) : Pure vprop (n % 2 == 0) (fun _ -> True)  = pts_to r (Even n)

[@@__reduce__]
let s_odd (r:ref stepper p) (n:nat) : Pure vprop (n % 2 <> 0) (fun _ -> True)  = pts_to r (Odd n)

let frame_compatible (x:erased stepper) (v y:stepper) =
  (forall (frame:stepper). {:pattern (composable x frame)}
            composable x frame /\
            v == compose x frame ==>
            composable y frame /\
            v == compose y frame)

let select_refine' (r:ref stepper p)
                  (x:erased stepper)
                  (f:(v:stepper{compatible p x v}
                      -> GTot (y:stepper{compatible p y v /\
                                  frame_compatible x v y})))
   : SteelT  (v:stepper{compatible p x v /\ refine v})
             (PR.pts_to r x)
             (fun v -> PR.pts_to r (f v))
   = select_refine r x f

let select_refine (r:ref stepper p)
                  (x:erased stepper)
                  (f:(v:stepper{compatible p x v}
                      -> GTot (y:stepper{compatible p y v /\
                                  frame_compatible x v y})))
   : SteelT  (v:stepper{compatible p x v /\ refine v})
             (pts_to r x)
             (fun v -> pts_to r (f v))
   = let v = select_refine' r x f in
     rewrite_slprop (PR.pts_to r (f v)) (pts_to r (f v)) (fun _ -> ());
     return v

(** Updating a ref cell for a user-defined PCM *)

val upd_gen_action (r:ref stepper p)
                   (x y:Ghost.erased stepper)
                   (f:FStar.PCM.frame_preserving_upd p x y)
  : SteelT unit (pts_to r x) (fun _ -> pts_to r y)

let upd_gen_action r x y f = upd_gen r x y f

let f_even (n0:even) (v:stepper{compatible p (Even n0) v})
  : GTot (y:stepper{compatible p y v /\ frame_compatible (Even n0) v y})
  = match v with
    | Even n0 -> Even n0
    | EvenWriteable n0 -> EvenWriteable n0
    | V n -> if n = n0 then Even n0 else EvenWriteable n0

let f_odd (n0:odd) (v:stepper{compatible p (Odd n0) v})
val f_odd (n0: odd) (v: stepper{compatible p (Odd n0) v})
    : GTot (y: stepper{compatible p y v /\ frame_compatible (Odd n0) v y})

    n0: Steel.Stepper.odd ->
    v: Steel.Stepper.stepper{FStar.PCM.compatible Steel.Stepper.p (Steel.Stepper.Odd n0) v}
  -> Prims.GTot
    (y:
      Steel.Stepper.stepper
        { FStar.PCM.compatible Steel.Stepper.p y v /\
          Steel.Stepper.frame_compatible (FStar.Ghost.hide (Steel.Stepper.Odd n0)) v y })