val mk_chan (#p: prot) (send recv: ref chan_val) (v: init_chan_val p)
    : SteelT (chan_t_sr p send recv)
      ((pts_to send half v) `star` (pts_to recv half v))
      (fun c -> chan_inv c)
let mk_chan (#p:prot) (send recv:ref chan_val) (v:init_chan_val p)
  : SteelT (chan_t_sr p send recv)
           (pts_to send half v `star` pts_to recv half v)
           (fun c -> chan_inv c)
  = let tr: trace_ref p = MRef.alloc (extended_to #p) (initial_trace p) in
    let c = Mkchan_t send recv tr in
    rewrite_slprop
      (MRef.pts_to tr full_perm (initial_trace p))
      (MRef.pts_to c.trace full_perm (initial_trace p)) (fun _ -> ());
    intro_trace_until_init c v;
    rewrite_slprop
      (pts_to send half v `star` pts_to recv half v)
      (pts_to c.send half v `star` pts_to c.recv half v)
      (fun _ -> ());
    intro_chan_inv #p c v;
    let c' : chan_t_sr p send recv = c in
    rewrite_slprop (chan_inv c) (chan_inv c') (fun _ -> ());
    return c'
val mk_chan (#p: prot) (send recv: ref chan_val) (v: init_chan_val p)
    : SteelT (chan_t_sr p send recv)
      ((pts_to send half v) `star` (pts_to recv half v))
      (fun c -> chan_inv c)
let mk_chan (#p: prot) (send recv: ref chan_val) (v: init_chan_val p)
    : SteelT (chan_t_sr p send recv)
      ((pts_to send half v) `star` (pts_to recv half v))
      (fun c -> chan_inv c) =
let tr:trace_ref p = MRef.alloc (extended_to #p) (initial_trace p) in
let c = Mkchan_t send recv tr in
rewrite_slprop (MRef.pts_to tr full_perm (initial_trace p))
  (MRef.pts_to c.trace full_perm (initial_trace p))
  (fun _ -> ());
intro_trace_until_init c v;
rewrite_slprop ((pts_to send half v) `star` (pts_to recv half v))
  ((pts_to c.send half v) `star` (pts_to c.recv half v))
  (fun _ -> ());
intro_chan_inv #p c v;
let c':chan_t_sr p send recv = c in
rewrite_slprop (chan_inv c) (chan_inv c') (fun _ -> ());
return c'
Steel.Channel.Simplex.fst.checked
Steel.Utils.fst.checked Steel.SpinLock.fsti.checked Steel.MonotonicHigherReference.fsti.checked Steel.Memory.fsti.checked Steel.HigherReference.fsti.checked Steel.FractionalPermission.fst.checked Steel.Effect.Atomic.fsti.checked Steel.Effect.fsti.checked Steel.Channel.Protocol.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Steel.Channel.Simplex.fst
Steel.Channel.Simplex.prot Steel.HigherReference.ref Steel.Channel.Simplex.chan_val Steel.Channel.Simplex.init_chan_val Steel.Effect.Atomic.return Steel.Channel.Simplex.chan_t_sr FStar.Ghost.hide FStar.Set.set Steel.Memory.iname FStar.Set.empty Steel.Channel.Simplex.chan_inv Steel.Effect.Common.vprop Prims.unit Steel.Effect.Atomic.rewrite_slprop Steel.Memory.mem Steel.Channel.Simplex.intro_chan_inv Steel.Effect.Common.star Steel.HigherReference.pts_to Steel.Channel.Simplex.half Steel.Channel.Simplex.__proj__Mkchan_t__item__send Steel.Channel.Simplex.__proj__Mkchan_t__item__recv Steel.Channel.Simplex.intro_trace_until_init Steel.MonotonicHigherReference.pts_to Steel.Channel.Protocol.partial_trace_of Steel.Channel.Protocol.extended_to Steel.FractionalPermission.full_perm Steel.Channel.Simplex.initial_trace Steel.Channel.Simplex.__proj__Mkchan_t__item__trace Steel.Channel.Simplex.chan_t Steel.Channel.Simplex.Mkchan_t Steel.Channel.Simplex.trace_ref Steel.MonotonicHigherReference.alloc Steel.MonotonicHigherReference.ref
(*
   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.Channel.Simplex
module P = Steel.Channel.Protocol
open Steel.SpinLock
open Steel.Memory
open Steel.Effect.Atomic
open Steel.Effect
open Steel.HigherReference
open Steel.FractionalPermission
module MRef = Steel.MonotonicHigherReference
module H = Steel.HigherReference

let sprot = p:prot { more p }

noeq
type chan_val = {
  chan_prot : sprot;
  chan_msg  : msg_t chan_prot;
  chan_ctr  : nat
}

let mref a p = MRef.ref a p
let trace_ref (p:prot) = mref (partial_trace_of p) extended_to

noeq
type chan_t (p:prot) = {
  send: ref chan_val;
  recv: ref chan_val;
  trace: trace_ref p;
}

let half : perm = half_perm full_perm

let step (s:sprot) (x:msg_t s) = step s x

let chan_inv_step_p (vrecv vsend:chan_val) : prop =
  (vsend.chan_prot == step vrecv.chan_prot vrecv.chan_msg /\
   vsend.chan_ctr == vrecv.chan_ctr + 1)

let chan_inv_step (vrecv vsend:chan_val) : vprop =
  pure (chan_inv_step_p vrecv vsend)

let chan_inv_cond (vsend:chan_val) (vrecv:chan_val) : vprop =
    if vsend.chan_ctr = vrecv.chan_ctr
    then pure (vsend == vrecv)
    else chan_inv_step vrecv vsend

let trace_until_prop #p (r:trace_ref p) (vr:chan_val) (tr: partial_trace_of p) : vprop =
  MRef.pts_to r full_perm tr `star`
  pure (until tr == step vr.chan_prot vr.chan_msg)

let trace_until #p (r:trace_ref p) (vr:chan_val) =
  h_exists (trace_until_prop r vr)

let chan_inv_recv #p (c:chan_t p) (vsend:chan_val) =
  h_exists (fun (vrecv:chan_val) ->
      pts_to c.recv half vrecv `star`
      trace_until c.trace vrecv `star`
      chan_inv_cond vsend vrecv)

let chan_inv #p (c:chan_t p) : vprop =
  h_exists (fun (vsend:chan_val) ->
    pts_to c.send half vsend `star` chan_inv_recv c vsend)

let intro_chan_inv_cond_eqT (vs vr:chan_val)
  : Steel unit emp
               (fun _ -> chan_inv_cond vs vr)
               (requires fun _ -> vs == vr)
               (ensures fun _ _ _ -> True)
  = intro_pure (vs == vs);
    rewrite_slprop (chan_inv_cond vs vs) (chan_inv_cond vs vr) (fun _ -> ())

let intro_chan_inv_cond_stepT (vs vr:chan_val)
  : SteelT unit (chan_inv_step vr vs)
                (fun _ -> chan_inv_cond vs vr)
  = Steel.Utils.extract_pure (chan_inv_step_p vr vs);
    rewrite_slprop (chan_inv_step vr vs) (chan_inv_cond vs vr) (fun _ -> ())

let intro_chan_inv_auxT #p  (#vs : chan_val)
                            (#vr : chan_val)
                            (c:chan_t p)
  : SteelT unit (pts_to c.send half vs `star`
                 pts_to c.recv half vr `star`
                 trace_until c.trace vr `star`
                 chan_inv_cond vs vr)
                 (fun _ -> chan_inv c)
  = intro_exists _ (fun (vr:chan_val) -> pts_to c.recv half vr `star` trace_until c.trace vr `star` chan_inv_cond vs vr);
    intro_exists _ (fun (vs:chan_val) -> pts_to c.send half vs `star` chan_inv_recv c vs)

let intro_chan_inv_stepT #p (c:chan_t p) (vs vr:chan_val)
  : SteelT unit (pts_to c.send half vs `star`
                 pts_to c.recv half vr `star`
                 trace_until c.trace vr `star`
                 chan_inv_step vr vs)
                 (fun _ -> chan_inv c)
  = intro_chan_inv_cond_stepT vs vr;
    intro_chan_inv_auxT c

let intro_chan_inv_eqT #p (c:chan_t p) (vs vr:chan_val)
  : Steel unit (pts_to c.send half vs `star`
                 pts_to c.recv half vr `star`
                 trace_until c.trace vr)
                 (fun _ -> chan_inv c)
                 (requires fun _ -> vs == vr)
                 (ensures fun _ _ _ -> True)
  = intro_chan_inv_cond_eqT vs vr;
    intro_chan_inv_auxT c

noeq
type chan p = {
  chan_chan : chan_t p;
  chan_lock : lock (chan_inv chan_chan)
}

let in_state_prop (p:prot) (vsend:chan_val) : prop =
  p == step vsend.chan_prot vsend.chan_msg

irreducible
let next_chan_val (#p:sprot) (x:msg_t p) (vs0:chan_val { in_state_prop p vs0 })
  : Tot (vs:chan_val{in_state_prop (step p x) vs /\ chan_inv_step_p vs0 vs})
  = {
      chan_prot = (step vs0.chan_prot vs0.chan_msg);
      chan_msg = x;
      chan_ctr = vs0.chan_ctr + 1
    }

[@@__reduce__]
let in_state_slprop (p:prot) (vsend:chan_val) : vprop = pure (in_state_prop p vsend)

let in_state (r:ref chan_val) (p:prot) =
  h_exists (fun (vsend:chan_val) ->
    pts_to r half vsend `star` in_state_slprop p vsend)

let sender #q (c:chan q) (p:prot) = in_state c.chan_chan.send p
let receiver #q (c:chan q) (p:prot) = in_state c.chan_chan.recv p

let intro_chan_inv #p (c:chan_t p) (v:chan_val)
  : SteelT unit (pts_to c.send half v `star`
                 pts_to c.recv half v `star`
                 trace_until c.trace v)
                (fun _ -> chan_inv c)
  = intro_chan_inv_eqT c v v

let chan_val_p (p:prot) = (vs0:chan_val { in_state_prop p vs0 })
let intro_in_state (r:ref chan_val) (p:prot) (v:chan_val_p p)
  : SteelT unit (pts_to r half v) (fun _ -> in_state r p)
  = intro_pure (in_state_prop p v);
    intro_exists v (fun (v:chan_val) -> pts_to r half v `star` in_state_slprop p v)

let msg t p = Msg Send unit (fun _ -> p)
let init_chan_val (p:prot) = v:chan_val {v.chan_prot == msg unit p}

let initial_trace (p:prot) : (q:partial_trace_of p {until q == p})
  = { to = p; tr=Waiting p}

let intro_trace_until #q (r:trace_ref q) (tr:partial_trace_of q) (v:chan_val)
  : Steel unit (MRef.pts_to r full_perm tr)
               (fun _ -> trace_until r v)
               (requires fun _ -> until tr == step v.chan_prot v.chan_msg)
               (ensures fun _ _ _ -> True)
  = intro_pure (until tr == step v.chan_prot v.chan_msg);
    intro_exists tr
          (fun (tr:partial_trace_of q) ->
             MRef.pts_to r full_perm tr `star`
             pure (until tr == (step v.chan_prot v.chan_msg)));
    ()

let chan_t_sr (p:prot) (send recv:ref chan_val) = (c:chan_t p{c.send == send /\ c.recv == recv})

let intro_trace_until_init  #p (c:chan_t p) (v:init_chan_val p)
  : SteelT unit (MRef.pts_to c.trace full_perm (initial_trace p))
                (fun _ -> trace_until c.trace v)
  = intro_pure (until (initial_trace p) == step v.chan_prot v.chan_msg);
    //TODO: Not sure why I need this rewrite
    rewrite_slprop (MRef.pts_to c.trace full_perm (initial_trace p) `star`
                          pure (until (initial_trace p) == step v.chan_prot v.chan_msg))
                   (MRef.pts_to c.trace full_perm (initial_trace p) `star`
                          pure (until (initial_trace p) == step v.chan_prot v.chan_msg))
                   (fun _ -> ());
    intro_exists (initial_trace p) (trace_until_prop c.trace v)

let mk_chan (#p:prot) (send recv:ref chan_val) (v:init_chan_val p)
  : SteelT (chan_t_sr p send recv)
           (pts_to send half v `star` pts_to recv half v)
val mk_chan (#p: prot) (send recv: ref chan_val) (v: init_chan_val p)
    : SteelT (chan_t_sr p send recv)
      ((pts_to send half v) `star` (pts_to recv half v))
      (fun c -> chan_inv c)

    send: Steel.HigherReference.ref Steel.Channel.Simplex.chan_val ->
    recv: Steel.HigherReference.ref Steel.Channel.Simplex.chan_val ->
    v: Steel.Channel.Simplex.init_chan_val p
  -> Steel.Effect.SteelT (Steel.Channel.Simplex.chan_t_sr p send recv)