// This file is DELIBERATELY BROKEN -- it's the "problem invariants solve,"
// caught in the act.
//
// `increment` is exactly Part 2's ownership-transfer pattern: `requires
// own(c.count, v)`, full permission, handed back afterward. That's fine for
// a single sequential caller. But `client` tries to `spawn` it *twice* on the
// same counter. The first `spawn` consumes the one full permission `create`
// produced. There is nothing left for the second `spawn` to require, and
// Raven catches exactly that:
//
//   [Verification Error] A precondition may not hold for this call
//   [Related Location]   This own predicate may not hold
//
// Plain ownership transfer has no way to express "many threads share access
// to this cell, provided each one's *step* leaves it in a good state" --
// only "one owner has it, then hands it to the next." That's precisely the
// gap `inv` (see ../hit_counter_invariant.rav) fills.
field count: Int

proc increment(c: Ref, implicit ghost v: Int)
  requires own(c.count, v)
  ensures own(c.count, v + 1)
{
  var x := c.count;
  c.count := x + 1;
}

proc create() returns (c: Ref)
  ensures own(c.count, 0)
{
  c := new (count: 0);
}

proc client() returns (c: Ref)
{
  c := create();
  spawn increment(c);
  spawn increment(c);
}