#ifndef LOCKS_H
#define LOCKS_H

#include "atomics.h"

/*@

predicate_family lock_operation_pre(void *op)(void **pp);
predicate_family lock_operation_post(void *op)(bool success);

typedef lemma void lock_operation();
    requires lock_operation_pre(this)(?pp) &*& [?f]pointer(pp, ?value) &*& value == 0 ? f == 1 : true;
    ensures lock_operation_post(this)(value == 0) &*& value == 0 ? pointer(pp, (void *)1) : [f]pointer(pp, value);

predicate_family lock_context_pre(void *op)(predicate() inv, void **pp);
predicate_family lock_context_post(void *op)();

typedef lemma void lock_context(lock_operation *op);
    requires
        lock_context_pre(this)(?inv, ?pp) &*& inv() &*&
        is_lock_operation(op) &*& lock_operation_pre(op)(pp);
    ensures
        is_lock_operation(op) &*& lock_operation_post(op)(?success) &*& inv() &*&
        success ? lock_context_post(this)() : lock_context_pre(this)(inv, pp);

@*/

void lock(void **lock);
    /*@
    requires
        [?f]atomic_space(?inv) &*&
        is_lock_context(?ctxt) &*& lock_context_pre(ctxt)(inv, lock);
    @*/
    /*@
    ensures
        [f]atomic_space(inv) &*&
        is_lock_context(ctxt) &*& lock_context_post(ctxt)();
    @*/

void unlock(void **lock);
    /*@
    requires
        [?f]atomic_space(?inv) &*&
        is_atomic_store_pointer_context(?ctxt) &*& atomic_store_pointer_context_pre(ctxt)(inv, lock, 0);
    @*/
    /*@
    ensures
        [f]atomic_space(inv) &*&
        is_atomic_store_pointer_context(ctxt) &*& atomic_store_pointer_context_post(ctxt)();
    @*/

#endif