== Contract Reduction Language  ==

Given a process `p` that is at a state that a call to a system function `f` is enabled,
if `p` is chosen in the ample set, then the following represents the set of processes other than
`p` that have to be in the ample set as well:

`$ample{ BOOLEAN EXPRESSION }`

    where `BOOLEAN EXPRESSION` is composed of the following functions over `f`'s arguments (`a, ...`).

- `$reach(a, ...)`
    returns true iff the memory unit of the object `a` (and others if present) is reachable by a given process `p'`.

- `$reach_from(a, ...)`
    returns true iff any of the memory units reachable from the object `a` (and others if present) is reachable by a given process `p'`.

- `$write(a, ...)`
    returns true iff the memory unit of the object `a` (and others if present) is to be written now or in the future by a given process `p'`.

- `$write_from(a, ...)`
    returns true iff any of the memory units reachable from the object `a` (and others if present) is to be written now or in the future by a given process `p'`.

- `$ample{$true}`
    any process exists in the state should be in the ample set

- `$ample{$false}`
    any process other than the current process (`$self`) need NOT be in the ample set.

Conditional amples set: `[COND] $ample{EXPR1} : $ample(EXPR2)`
    if `COND` is satisfied then processes satisfying `EXPR1` should be in the ample set;
    otherwise, `EXPR2` is considered.

Absent ample set (DEFAULT case): if no `$ample` expression is present, then the library enabler needs to calculate the ample set.

   
Examples:
- The following means that any process that can reach the memory unit of `comm` should be in the ample set if the current process (`$self`) is to be chosen in the ample set.
{{{
$ample{$reach(comm)}
void comm_deque($comm comm, ....);
}}}

- The following means that any process that can reach any of the memory units reachable from `a` or write any of the memory units reachable from `a` now or in the future should be in the ample set if the current process (`$self`) is to be chosen in the ample set.
{{{
$ample{$reach_from(a) || $write_from(b)}
void strcpy(char *a, char *b);
}}}

- The following means that the current process itself can form the ample set.
{{{
$ample($false)
int $comm_size($comm, ...);
}}}