val p':pcm' stepper
let p' : pcm' stepper = { composable = composable; op = compose; one = None }
val p':pcm' stepper
let p':pcm' stepper =
{ composable = composable; op = compose; one = None }
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
FStar.PCM.Mkpcm' Steel.Stepper.stepper Steel.Stepper.composable Steel.Stepper.compose Steel.Stepper.None
(*
   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
val p':pcm' stepper
FStar.PCM.pcm' Steel.Stepper.stepper