Getting cardinality from relations

kenmcmil / ivy

IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.

Other

77 stars 24 forks source link

Consider the following protocol.

type node
relation active(N:node)
type int_t
interpret int_t -> int
individual num_active : int_t

after init {
    active(N) := false;
    num_active := 0;
}

action become_active(n:node) = {
    require ~active(n);
    active(n) := true;
    num_active := num_active + 1;
}

The protocol maintains two invariants

invariant num_active <= COUNT n WHERE active(n) is defined (i.e., total number of nodes)
invariant num_active = COUNT n WHERE active(n) is true (i.e., number of active nodes)

However, I cannot find a way to represent either number in Ivy. Does Ivy support reasoning about cardinality of types/relations?

kenmcmil / ivy

Getting cardinality from relations #69