class List {
  ghost var sum: int
  var head: Node
  invariant acc(head) && head != null
  invariant rd(head.val) && head.val == -1
  invariant rd(mu) && acc(head.mu,50) && this << head
  invariant acc(sum,20) && acc(head.sum, 50) && sum == head.sum

  method Main()
  {
    var list := new List
    call list.Init()
    call list.Insert(8)
    call list.Insert(12)
    call list.Insert(4)
    assert list.sum == 24
  }

  method Init()
    requires acc(mu) && mu == lockbottom && acc(head) && acc(sum)
    ensures rd*(mu) && waitlevel << this
    ensures acc(sum,80) && sum == 0
  {
    var t := new Node
    t.val := -1
    t.next := null
    t.sum := 0
    share t
    head := t
    sum := 0
    share this between waitlevel and t
  }

  method Insert(x: int)
    requires rd(mu) && waitlevel << this
    requires acc(sum,80) && 0 <= x
    ensures rd(mu)
    ensures acc(sum,80) && sum == old(sum) + x
  {
    acquire this
    assert waitlevel == this.mu;
    sum := sum + x
    var p: Node := head
    acquire p
    p.sum := p.sum + x
    release this

    while (p.next != null && p.next.val < x)
      invariant p != null && acc(p.next) && acc(p.val,rd(p)) && acc(p.mu,50)
      invariant holds(p) && waitlevel == p.mu
      invariant !old(holds(p)) && !old(rd holds(p))
      invariant p.next != null ==> acc(p.next.mu,50) && p << p.next
      invariant p.next != null ==> acc(p.next.val,rd(p.next)) && p.val <= p.next.val
      invariant acc(p.sum, 50)
      invariant p.next == null ==> p.sum == x
      invariant p.next != null ==> acc(p.next.sum, 50) && p.sum == p.next.val + p.next.sum + x
      invariant p.val <= x
      lockchange p
    {
      var nx: Node := p.next
      acquire nx
      nx.sum := nx.sum + x
      release p
      p := nx
    }
    var t := new Node
    t.val := x
    t.next := p.next
    if (t.next == null) { t.sum := 0 } else { t.sum := p.next.val + p.next.sum }
    share t between p and p.next
    p.next := t
    release p
  }

  method Delete(x: int) returns (wasPresent: bool)
    requires rd(mu) && waitlevel << this
    requires acc(sum,80) && 0 <= x
    ensures acc(sum,80) && (wasPresent ==> sum == old(sum) - x) && (!wasPresent ==> sum == old(sum))
  {
    ghost const c

    acquire this
    sum := sum - c
    var p: Node := head
    acquire p
    p.sum := p.sum - c
    release this

    while (p.next != null && p.next.val < x)
      invariant p != null && acc(p.next) && acc(p.val,rd(p)) && acc(p.mu,50)
      invariant holds(p) && waitlevel == p.mu && !assigned(c)
      invariant !old(holds(p)) && !old(rd holds(p))
      invariant p.next != null ==> acc(p.next.mu,50) && p << p.next
      invariant p.next != null ==> acc(p.next.val,rd(p.next)) && p.val <= p.next.val
      invariant acc(p.sum, 50)
      invariant p.next == null ==> p.sum == 0 - c
      invariant p.next != null ==> acc(p.next.sum, 50) && p.sum == p.next.val + p.next.sum - c
      invariant p.val <= x
      lockchange p
    {
      var nx: Node := p.next
      acquire nx
      nx.sum := nx.sum - c
      release p
      p := nx
    }
    if (p.next != null && p.next.val == x) {
      wasPresent := true
      c := x
      var nx: Node := p.next
      acquire nx
      p.next := nx.next
      unshare nx
    } else {
      wasPresent := false
      c := 0
    }
    release p
  }
}

class Node {
  ghost var sum: int
  var val: int
  var next: Node
  invariant acc(next) && rd(val)
  invariant next != null ==> rd(next.val) && val <= next.val
  invariant acc(sum, 50)
  invariant next == null ==> sum == 0
  invariant next != null ==> acc(next.sum, 50) && sum == next.val + next.sum
  invariant acc(mu,50) && (next != null ==> acc(next.mu,50) && this << next)
}