val contributions : left: Pulse.Lib.GhostReference.ref Prims.int ->
    right: Pulse.Lib.GhostReference.ref Prims.int ->
    i: Prims.int ->
    v: Prims.int
  -> Pulse.Lib.Core.vprop
let contributions (left right: GR.ref int) (i v:int)=
  exists* (vl vr:int).
    GR.pts_to left #one_half vl **
    GR.pts_to right #one_half vr **
    pure (v == i + vl + vr)
module PulseTutorial.ParallelIncrement
open Pulse.Lib.Pervasives
module U32 = FStar.UInt32
module L = Pulse.Lib.SpinLock
module GR = Pulse.Lib.GhostReference
module R = Pulse.Lib.Reference

```pulse //par$
fn par (#pf #pg #qf #qg:_)
       (f: unit -> stt unit pf (fun _ -> qf))
       (g: unit -> stt unit pg (fun _ -> qg))
requires pf ** pg
ensures qf ** qg
{
  parallel 
  requires pf and pg
  ensures qf and qg
  { f () }
  { g () };
  ()
}
```

```pulse
fn incr2 (x y:ref int)
requires pts_to x 'i ** pts_to y 'j
ensures pts_to x ('i + 1) ** pts_to y ('j + 1)
{
  fn incr (x:ref int) (#i:erased int)
  requires pts_to x i
  ensures pts_to x (i + 1)
  {
    let v = !x;
    x := v + 1;
  };
  par (fun _ -> incr x) (fun _ -> incr y);
}
```


[@@expect_failure]
```pulse
fn attempt0 (x:ref int)
requires pts_to x 'i
ensures pts_to x ('i + 2)
{
  fn incr (#i:erased int)
  requires pts_to x i
  ensures pts_to x (i + 1)
  {
    let v = !x;
    x := v + 1;
  };
  par (fun _ -> incr) (fun _ -> incr);
}
```

```pulse //attempt$
fn attempt (x:ref int)
requires pts_to x 'i
ensures emp
{
  let l = L.new_lock (exists* v. pts_to x v);
  fn incr ()
  requires emp
  ensures emp
  {
    L.acquire l;
    let v = !x;
    x := v + 1;
    L.release l
  };
  par incr incr
}
```
/
Pulse.Lib.SpinLock.fsti.checked Pulse.Lib.Reference.fsti.checked Pulse.Lib.Pervasives.fst.checked Pulse.Lib.GhostReference.fsti.checked Pulse.Lib.CancellableInvariant.fst.checked prims.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked
PulseTutorial.ParallelIncrement.fst

    left: Pulse.Lib.GhostReference.ref Prims.int ->
    right: Pulse.Lib.GhostReference.ref Prims.int ->
    i: Prims.int ->
    v: Prims.int
  -> Pulse.Lib.Core.vprop
Pulse.Lib.GhostReference.ref Prims.int Pulse.Lib.Core.op_exists_Star Pulse.Lib.Core.op_Star_Star Pulse.Lib.GhostReference.pts_to Pulse.Lib.Core.one_half Pulse.Lib.Core.pure Prims.eq2 Prims.op_Addition Pulse.Lib.Core.vprop
let contributions (left right: GR.ref int) (i v: int) =
  
exists* (vl: int) (vr: int).
  (GR.pts_to left #one_half vl ** GR.pts_to right #one_half vr) ** pure (v == i + vl + vr)