#lang ivy1.6

include order
include collections

module message_queue(net_msg,seq_num) = {

    relation contents(M:net_msg.t)

    action enqueue(msg:net_msg.t) returns (ok:bool)
    action empty returns (res:bool)
    action pick_one returns (res:net_msg.t)
    action delete_all(seq:seq_num.t)


    object spec = {
	init ~contents(M)

	before enqueue {
	    assert contents(X) -> net_msg.num(X) ~= net_msg.num(msg)
	}

	after enqueue {
	    if ok {
		contents(msg) := true
	    }
	}

	after empty returns (res:bool) {
	    assert contents(M) -> ~res;
	    assert ~res -> exists M. contents(M)
	}

	before pick_one {
	    assert exists M. contents(M)
	}

	after pick_one {
	    assert contents(res)
	}
    
	before delete_all  {
	    contents(M) := contents(M) & ~(net_msg.num(M) <= seq)
	}
    }
    
    object impl = {

	instance imap : ordered_map(seq_num,net_msg.t)

	implement enqueue {
	    call imap.set(net_msg.num(msg),msg);
	    ok := true
	}

	implement empty {
	    res := seq_num.iter.is_end(imap.lub(seq_num.iter.create(0)))
	}
	
	implement delete_all(seq:seq_num.t) {
	    call imap.erase(seq_num.iter.create(0),seq_num.iter.create(seq_num.next(seq)))
	}

	implement pick_one {
	    res := imap.get(seq_num.iter.val(imap.lub(seq_num.iter.create(0))),res)
	}

	conjecture imap.maps(X,Y) -> X = net_msg.num(Y)
	conjecture contents(Y) <-> imap.maps(net_msg.num(Y),Y)

    }

}