#ifndef GHOST_CELLS_H
#define GHOST_CELLS_H

/*@

predicate ghost_cell<t>(int id; t value);

lemma int create_ghost_cell<t>(t value);
    requires true;
    ensures ghost_cell<t>(result, value);

lemma void ghost_cell_mutate<t>(int id, t value);
    requires ghost_cell<t>(id, _);
    ensures ghost_cell<t>(id, value);

lemma void ghost_cell_fraction_info<t>(int id);
    requires [?f]ghost_cell<t>(id, ?value);
    ensures [f]ghost_cell<t>(id, value) &*& 0 < f &*& f <= 1;

lemma void ghost_cell_leak<t>(int id); // For people who prefer to avoid "leak" statements.
    requires [?f]ghost_cell<t>(id, ?value);
    ensures [_]ghost_cell<t>(id, value);

@*/

#endif