// Part 2's running example: the counter is now a heap-allocated object with one
// field, still touched by a single thread at a time -- concurrency starts in
// Part 4. Every proc below is verified together in this one file.

field count: Int

// `new (count: 0)` allocates a fresh heap object and, in the same step, hands
// full ownership of its `count` field to whoever called `create`.
proc create() returns (c: Ref)
  ensures own(c.count, 0)
{
  c := new (count: 0)
}

// `v` is `implicit ghost`: it exists purely to state the contract (it never
// affects what the code does) and the caller never has to supply it -- Raven
// infers it from whatever `own(c.count, ...)` fact the caller already holds.
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
}

// Fractional permissions: a full (1.0, the default) permission can be split
// into read-only halves and hand out to two different pieces of code, then
// silently recombined afterwards. Nothing here asks for this explicitly --
// Raven's own automatic framing does the splitting and recombining.
proc readHalf(c: Ref, implicit ghost v: Int) returns (r: Int)
  requires own(c.count, v, 0.5)
  ensures own(c.count, v, 0.5) && r == v
{
  r := c.count
}

proc readTwice(c: Ref, implicit ghost v: Int) returns (a: Int, b: Int)
  requires own(c.count, v, 1.0)
  ensures own(c.count, v, 1.0) && a == v && b == v
{
  a := readHalf(c)
  b := readHalf(c)
}

// The frame rule, and anti-aliasing, in one example. The `assert c1 != c2`
// holds before `increment` is ever called -- as a side effect of holding
// *two* full-permission `own` facts at once, Raven can derive that `c1` and
// `c2` must be different locations, with no explicit `c1 != c2` precondition
// anywhere: two full permissions on the very same location would be an
// inconsistent (over-100%) amount of ownership to hold simultaneously. The
// second assert is the frame rule itself, made observable: `increment(c1)`
// only ever touches `c1.count` (that's all its own contract asks for), so
// reading `c2.count` before and after the call is guaranteed to give back
// the same value, even though nothing here says so explicitly.
proc distinctIncrement(c1: Ref, c2: Ref, implicit ghost v1: Int, implicit ghost v2: Int)
  requires own(c1.count, v1) && own(c2.count, v2)
  ensures own(c1.count, v1 + 1) && own(c2.count, v2)
{
  assert c1 != c2 // provable from the requires clause alone, before this line
  var before := c2.count
  increment(c1)
  var after := c2.count
  assert before == after
}