// program inspired by "Proving Copyless Message Passing" (Villard, Lozes and Calcagno, APLAS 2009)

// msg tag indicates what the type of the message
// channel is freed by Getter when it completes
// ack-channel instead of single channel with ack message channel
// using Owicki-Gries ghostfields can be used to remove the "assume false;" statements

// Conjecture: it is ok to send debit credit(d, -x) over a channel c as long as
// a) d.mu << c.mu
// b) leaking positive or negative debit is not allowed

channel AckChannel(ch: C) where ch != null && credit(ch, -1); // ack

channel C(msg: bool, n: Node, ackC: AckChannel) where 
  (!msg ==> acc(this.mu, 50) && acc(ackC.mu, 50)) &&
  (msg ==> n != null && acc(n.next) && acc(n.mu) && ackC != null && credit(ackC, -1)); // cell 

class Node {
  var next: Node;
  
  function length(): int
    requires this.list;
  {
    unfolding this.list in 1 + (next == null ? 0 : next.length())
  }
  
  predicate list {
    acc(next) && acc(mu) && (next != null ==> next.list)
  }
}

class Program {
  method Putter(e: C, x0: Node, ackC: AckChannel) 
    requires e!= null && acc(e.mu, 50) && e.mu == waitlevel && acc(ackC.mu, 50) && e.mu << ackC.mu && (x0 != null ==> x0.list) && (x0 != null ==> credit(e, - 1));
  {
    var x: Node := x0;
    var t: Node;
    
    while(x != null) 
      invariant (x != null ==> x.list) && acc(e.mu, 50) && acc(ackC.mu, 50) && e.mu << ackC.mu && credit(e, - 1);
    {
      unfold x.list;
      t := x.next;
      send e(true, x, ackC);
      x := t;
      var ack;
      assume waitlevel << ackC.mu; // Chalice should be able to figure this out itself?
      var ctmp: C;
      receive ctmp := ackC;
      if(ctmp != e) { assume false; /* abort */ }
    }
    send e(false, null, ackC);
  }  
  
  method Getter(f: C, ackC: AckChannel) 
    requires f!= null && credit(f, 1) && acc(f.mu, 50) && waitlevel << f.mu && ackC != null && acc(ackC.mu, 50) && f.mu << ackC.mu;
  {
    var x: Node := null;
    var msg: bool := true;
    while(msg)
      invariant acc(f.mu, 50) && waitlevel << f.mu && (msg ==> credit(f, 1)) && (!msg ==> acc(f.mu, 50) && acc(ackC.mu, 50));
    {
      var ackC2: AckChannel;
      receive msg, x, ackC2 := f;
      if(ackC2 != ackC) { assume false; /* abort */ }
      if(msg) {
        free x;
        send ackC(f);
      }
    }
    free f; // close the channel
  } 

  method Main(x: Node)
    requires x != null;
    requires x.list;
  {
    var e := new C;
    var ackC := new AckChannel above e;
    fork Putter(e, x, ackC);
    fork Getter(e, ackC);
  }  
}