// Step 6 (final) of this capstone's build-up: `token` is now `auto`, which
// trivializes `token_unique`'s proof to an empty body and removes the
// explicit `fold token(p)` in `fork` and the explicit call to
// `token_unique` in `join` that `fork_join_explicit.rav` (step 5) still
// needed -- Raven now does that reasoning on its own, every time `token(p)
// && token(p)` appears, because `token`'s definition is transparent.

// A resource algebra for a single non-duplicable token: `excl` and `excl`
// don't compose (composing them gives the invalid `top`), so holding one is
// proof nobody else can be holding another. This is worth writing out by
// hand once, even though `Library.Excl[Library.UnitRA]` already gives you
// exactly this -- so you've seen what a resource algebra actually *is*
// before treating one as a black box. Compare this to Appendix A's `RA`
// axioms: every one of them is either immediate from the `top`/`id` case
// split here, or (for `fpuAllowed`, which is simply `false`) vacuously true,
// since an algebra that never allows an update trivially satisfies whatever
// soundness condition that update would have needed.
module Excl : Library.ResourceAlgebra {
  rep type T = data {
    case bot;
    case excl;
    case top
  }

  val id: T = bot

  func valid(a: T) returns (res: Bool) {
    a != top
  }

  func comp(a: T, b: T) returns (res: T) {
    a == id ? b : (b == id ? a : top)
  }

  func frame(a: T, b: T) returns (res: T) {
    b == id ? a : (a == excl && b == excl ? id : top)
  }

  func fpuAllowed(a: T, b: T) returns (res: Bool) {
    false
  }
}

// The interface `ForkJoin` is parameterized over: whatever `task` computes,
// and whatever resource it hands back. Compare this to Part 5b's
// `LockResource`/`Lock` split -- same pattern (a functor abstracting over a
// client-supplied resource and a client-supplied operation producing it),
// applied here to a one-shot computation instead of a lock.
interface Instance {
  type R

  pred resource(r: R)

  proc task() returns (r: R)
    ensures resource(r)
}

module ForkJoin[I: Instance] {
  import I._
  import Library.Option

  // The channel the worker thread uses to hand its result to the joiner.
  field value: Option[R]
  // The non-duplicable token: whoever holds it is the one thread allowed to
  // claim the result once it's ready.
  ghost field ex: Excl

  // `auto` means `token(p)` and its definition are, as far as any proof is
  // concerned, simply two ways of writing the same assertion -- no `fold`/
  // `unfold` ever needed to move between them.
  auto pred token(p: Ref) {
    own(p.ex, Excl.excl)
  }

  // Tokens really are non-duplicable -- this follows straight from `Excl`'s
  // `comp`, and isn't invoked anywhere below; the SMT solver already knows
  // it whenever `token(p) && token(p)` appears, because `token` is `auto`.
  lemma token_unique(p: Ref)
    requires token(p) && token(p)
    ensures false
  {
  }

  // The shared invariant. `o` tracks whether the worker has posted a result
  // yet; `b` distinguishes "posted, but not yet claimed" from "already
  // claimed" -- exactly the same existentials-plus-boolean-flag shape as
  // Part 5b's `lock_inv`, just for a handoff instead of a lock. While no
  // result has been posted (`o == none`), neither `token(p)` nor
  // `resource(...)` is owned by the invariant at all -- both are still with
  // whoever holds them at that point (the joiner holds the token from
  // `fork`; nobody yet holds `resource`, since the worker hasn't produced it).
  inv is_forkjoin(p: Ref) {
    exists o: Option[R], b: Bool ::
      own(p.value, o) &&
      (o == Option.none ? true : (b ? token(p) : resource(o.Option.value)))
  }

  // The worker computes the task's result and posts it, trading `token(p)`
  // out of its own hands (it never held it to begin with) for putting
  // `resource(r)` into the invariant instead.
  proc worker(p: Ref)
    requires is_forkjoin(p)
  {
    val r := task()
    unfold is_forkjoin(p)
    p.value := Option.some(r)
    fold is_forkjoin(p)[b := false]
  }

  // `fork` allocates the shared state, spawns the worker, and returns both a
  // handle on the data structure and the one token that will let its holder
  // claim the result later.
  proc fork() returns (p: Ref)
    ensures is_forkjoin(p) && token(p)
  {
    p := new (value: Option.none, ex: Excl.excl)
    fold is_forkjoin(p)[b := false]
    spawn worker(p)
  }

  // `join` trades the token for the posted resource -- if the worker hasn't
  // posted yet, it retries. Nothing here proves this retry loop terminates
  // (there's no `decreases` measure a caller could see; termination depends
  // on the *other* thread eventually finishing), which mirrors exactly how
  // Part 5b's `wait_loop` retries a spin lock's acquire.
  proc join(p: Ref) returns (r: R)
    requires is_forkjoin(p) && token(p)
    ensures resource(r)
  {
    ghost var b0: Bool
    unfold is_forkjoin(p)[b0 := b]
    val o := p.value
    fold is_forkjoin(p)[b := true]

    if (o == Option.none) {
      r := join(p)
      return r
    } else {
      r := o.Option.value
      return r
    }
  }
}

// A client, instantiating `Instance` with a task that allocates a
// zero-initialized cell -- deliberately reusing Part 2/4's `field count:
// Int` shape, since nothing about fork/join itself cares what the task
// actually computes.
field count: Int

module ClientInstance : Instance {
  type R = Ref

  pred resource(r: Ref) {
    own(r.count, 0)
  }

  proc task() returns (r: Ref)
    ensures resource(r)
  {
    r := new (count: 0)
    fold resource(r)
  }
}

module FJ = ForkJoin[ClientInstance]

proc client()
{
  var p := FJ.fork()
  // ... do other work while the worker runs concurrently ...
  var r := FJ.join(p)
  unfold ClientInstance.resource(r)
  val y := r.count
}