#ifndef RAW_GHOST_LISTS_H
#define RAW_GHOST_LISTS_H

/*@

predicate raw_ghost_list<t>(int id; int n, list<pair<int, t> > elements);
predicate raw_ghost_list_member_handle<t>(int id, int k; t element);

lemma int create_raw_ghost_list<t>();
    requires emp;
    ensures raw_ghost_list<t>(result, 0, nil);

lemma void raw_ghost_list_add<t>(int id, t x);
    requires raw_ghost_list<t>(id, ?n, ?xs);
    ensures raw_ghost_list<t>(id, n + 1, append(xs, cons(pair(n, x), nil))) &*& raw_ghost_list_member_handle<t>(id, n, x);

lemma void raw_ghost_list_match<t>(int id, int k);
    requires raw_ghost_list<t>(id, ?n, ?xs) &*& [?f]raw_ghost_list_member_handle<t>(id, k, ?x);
    ensures raw_ghost_list<t>(id, n, xs) &*& [f]raw_ghost_list_member_handle<t>(id, k, x) &*& mem(pair(k, x), xs) == true;

lemma void raw_ghost_list_remove<t>(int id, int k);
    requires raw_ghost_list<t>(id, ?n, ?xs) &*& raw_ghost_list_member_handle<t>(id, k, ?x);
    ensures raw_ghost_list<t>(id, n, remove(pair(k, x), xs));

@*/

#endif