#ifndef GHOST_LISTS_H
#define GHOST_LISTS_H

#include "assoc_list.h"

/*@

predicate ghost_list<t>(int id, list<t> xs);
predicate ghost_list_member_handle<t>(int id, t x);

lemma int create_ghost_list<t>();
    requires true;
    ensures ghost_list<t>(result, nil);

lemma void ghost_list_add<t>(int id, t x);
    requires ghost_list<t>(id, ?xs);
    ensures ghost_list(id, cons(x, xs)) &*& [_]ghost_list_member_handle(id, x);

lemma void ghost_list_member_handle_lemma<t>(int id);
    requires [?f1]ghost_list<t>(id, ?xs) &*& [?f2]ghost_list_member_handle<t>(id, ?x);
    ensures [f1]ghost_list(id, xs) &*& [f2]ghost_list_member_handle(id, x) &*& mem(x, xs) == true;

lemma void ghost_list_create_member_handle<t>(int id, t x);
    requires [?f1]ghost_list(id, ?xs) &*& mem(x, xs) == true;
    ensures [f1]ghost_list(id, xs) &*& [_]ghost_list_member_handle(id, x);

predicate ghost_assoc_list(int id, list<pair<void *, void *> > xs);
predicate ghost_assoc_list_member_handle(int id, void **pp);

lemma int create_ghost_assoc_list();
    requires true;
    ensures ghost_assoc_list(result, nil);

lemma void ghost_assoc_list_add(int id, void *x, void *y);
    requires ghost_assoc_list(id, ?xys);
    ensures ghost_assoc_list(id, cons(pair(x, y), xys));

lemma void ghost_assoc_list_update(int id, void **x, void *y);
    requires ghost_assoc_list(id, ?xys) &*& mem_assoc(x, xys) == true;
    ensures ghost_assoc_list(id, update_pairlist(xys, x, y));

lemma void ghost_assoc_list_create_member_handle(int id, void **x);
    requires [?f1]ghost_assoc_list(id, ?xys) &*& mem_assoc(x, xys) == true;
    ensures [f1]ghost_assoc_list(id, xys) &*& [_]ghost_assoc_list_member_handle(id, x);

lemma void ghost_assoc_list_member_handle_lemma(int id, void **x);
    requires [?f1]ghost_assoc_list(id, ?xys) &*& [?f2]ghost_assoc_list_member_handle(id, x);
    ensures [f1]ghost_assoc_list(id, xys) &*& [f2]ghost_assoc_list_member_handle(id, x) &*& mem_assoc(x, xys) == true;

predicate strong_ghost_assoc_list(int id, list<pair<void *, void *> > xys);
predicate strong_ghost_assoc_list_key_handle(int id, void *x);
predicate strong_ghost_assoc_list_member_handle(int id, void *x; void *y);

lemma int create_strong_ghost_assoc_list();
    requires true;
    ensures strong_ghost_assoc_list(result, nil);

lemma void strong_ghost_assoc_list_add(int id, void *x, void *y);
    requires strong_ghost_assoc_list(id, ?xys) &*& !mem_assoc(x, xys);
    ensures strong_ghost_assoc_list(id, cons(pair(x, y), xys)) &*& strong_ghost_assoc_list_member_handle(id, x, y);

lemma void strong_ghost_assoc_list_update(int id, void *x, void *y1);
    requires strong_ghost_assoc_list(id, ?xys) &*& strong_ghost_assoc_list_member_handle(id, x, _);
    ensures strong_ghost_assoc_list(id, update_pairlist(xys, x, y1)) &*& strong_ghost_assoc_list_member_handle(id, x, y1);

lemma void strong_ghost_assoc_list_key_handle_lemma();
    requires strong_ghost_assoc_list(?id, ?xys) &*& [?f]strong_ghost_assoc_list_key_handle(id, ?x);
    ensures strong_ghost_assoc_list(id, xys) &*& [f]strong_ghost_assoc_list_key_handle(id, x) &*& mem_assoc(x, xys) == true;

lemma void create_strong_ghost_assoc_list_key_handle(void *x);
    requires strong_ghost_assoc_list(?id, ?xys) &*& mem_assoc(x, xys) == true;
    ensures strong_ghost_assoc_list(id, xys) &*& [_]strong_ghost_assoc_list_key_handle(id, x);

@*/

#endif