Teaching has driven me mad...

Sessions.dfy

// Sadly first class types do not exist in dafny, so we have to copy the Rust Approach of abusing generics.
//
// https://docs.rs/session_types/
//
// https://github.com/NicolasLagaillardie/mpst_rust_github
//
// There must be a better way!
datatype Stop        = ActStop

datatype Send<A,B>   = ActSend(A,B)
datatype Recv<A,B>   = ActSecv(A,B)
datatype Select<A,B,C,D> = ActLeft(A,B) | ActRight(C,B)
datatype Offer<A,B,C,D>  = ActOffer(A,B,C,D)

datatype Chan<A> = C(A)

datatype Either<A,B> = Left(A) | Right(B)

method SockClose(chan : Chan<Stop>)

method SockSend<A,B>(msg : A, chan: Chan<Send<A,B>>) returns (newc : Chan<B>)
method SockRecv<A,B>(chan: Chan<Recv<A,B>>) returns (res : A, newc : Chan<B>)

method SockSelectA<A,B,C,D>(msg : A, chan: Chan<Select<A,B,C,D>>) returns (newC : Chan<B>)
method SockSelectB<A,B,C,D>(msg : C, chan: Chan<Select<A,B,C,D>>) returns (newC : Chan<D>)

method SockOffer<A,B,C,D>(chan: Chan<Offer<A,B,C,D>>) returns (newC : Either<(A,Chan<B>),(C,Chan<D>)>)


type EchoC1 = Send<string, Recv<string, Stop>>
type EchoS1 = Recv<string, Send<string, Stop>>

type EchoS2 = Offer<string, EchoS1, string, EchoS1>
type EchoC2 = Select<string, EchoC1, string, EchoC1>

method EchoClient(chan : Chan<EchoC1>)
{
  var newChan1 := SockSend("ping", chan);
  var x, newChan2 := SockRecv(newChan1);
  SockClose(newChan2);
}

method EchoClient2(chan : Chan<EchoC2>)
{
  var newChan1 := SockSelectA("ping", chan);
  var newChan2 := SockSend("ping", newChan1);
  var x, newChan3 := SockRecv(newChan2);
  SockClose(newChan3);
}
method EchoServer22(chan : Chan<EchoS2>)
{
  var newChan1 := SockOffer(chan);
  match newChan1
  {
  case Left((m,rest)) =>
    var m2,rest2 := SockRecv(rest);
    var rest3 := SockSend("Ping", rest2);
    SockClose(rest3);
  case Right((m,rest)) =>
    var m2,rest2 := SockRecv(rest);
    var rest3 := SockSend("Ping", rest2);
    SockClose(rest3);

  }
}

method EchoServer(chan : Chan<EchoS1>)
{
  var newChan1 := SockSend("ping", chan);
  var x, newChan2 := SockRecv(newChan1);
  SockClose(newChan2);
}