# Deduction example: majority

In consensus protocols such as Paxos and Raft, we typically need a
datatype representing a subset of some finite set (the *basis* set)
and we need to test whether subset contains a majority of the basis
elements.

The key fact we need to know about majorities is that two majorities always have an alement in common. We will call this the majority intersection property. Here, we will develop an abstract datatype for subsets of a finite basis set provided with the operations for building subsets and a computable majority prediate satisfying the the majority intersection property.

Our datatype takes a type *basis* as a parameter. This must be a
sequence type equipped with a value `max`

representing the maximum
value of the sequence. Sequence types provide a total order, a zero
element, schemata for induction and recursion, and an arithmetic
theory.

The module provides the following interface:

1) a type *this* representing subsets of the basis type in the range [0,max-1]
2) a *member* relation
3) a predicate `majority`

on sets that is true if the cardinality is > n/2.
4) an action `empty`

returning the empty set
5) an action `add`

that adds an element to a set
6) an action `is_empty`

returning true if a set is empty

Internally, the following are also used:

1) An unbounded sequence type `index`

used for counting elements of `basis`

2) a relation *disjoint* beteween sets
3) a function *card* giving the cardinality of a set as an index
5) a function *cnt* gives the cardinality of the set of the set [0,x]

The index type is needed in order to represent the cardinality of
the set `[0,max]`

, which is `max+1`

and thus cannot be represented
by `basis`

.

Note the functions above are stratified in this order: ```
set -> basis
-> index.t
```

.

The implementation gives computable definitions of card, cnt and majority. The complexity of card and majority is quadratic in n, which is not optimimal but should be acceptable for small n (say, up to 5). In principal, we could add more efficient actions that compute these functions.

The main property provided is that any two majorities have an element in common. To prove this, we use a lemma stating that the sum of the cardinalities of two disjoint sets is <= cnt(n-1). This is proved by induction on n. This lemma implies the majority property.

```
include collections
include order
include deduction
```

The parameters of the module are:

- basis: the basis object (instance of unbounded_sequence)
- index: the index object (instance of unbounded_sequence)

```
module indexset(basis) = {
type set
instance index : unbounded_sequence
relation member(E:basis,S:set)
function card(S:set) : index.t
relation majority(S:set)
action empty returns(s:set)
action add(s:set,e:basis) returns (s:set)
action is_empty(s:set) returns(r:bool)
object spec = {
after empty {
assert ~member(E,s);
}
after add {
assert member(X,s) <-> (member(X,old s) | X = e)
}
after is_empty {
assert r <-> ~ exists X. member(X,s)
}
}
function cnt(E:basis) : index.t
relation disjoint(X:set,Y:set)
isolate disjointness = {
object impl = {
```

The funtion cnt(x) returns the cardinality of the set of ordinals < x. We define it recursively by instantiating the recursion scheman fo the basis type.

Note here we use a definition schema. A definition of the form
`f(x:t) = ...`

is a shorthand for this schema:

```
# {
# individual x :t
# #----------------
# property f(x) = ...
# }
```

The `auto`

tactic will only unfold this definition
schema for ground terms *x* occurring in the proof
goal. Without this, we would exit the decidable
fragment, due to a quantified variable under an
arithmetic operator in the following definition.

```
definition cnt(x:basis) = 1 if x <= 0 else cnt(x-1) + 1
proof
apply rec[basis]
```

We define cardinality in terms of a recursive function cardUpTo that counts the number of elements in a set that are less than or equal to a bound B.

```
function cardUpTo(S:set,B:basis) : index.t
```

Note that again the we use definition schema to stay
decidable. Again, the `rec[t]`

schema is used to admit a
recursive definition.

```
definition cardUpTo(s:set,b:basis) =
(1 if member(b,s) else 0) if b <= 0
else (cardUpTo(s,b-1) + (1 if member(b,s) else 0))
proof
apply rec[basis]
```

The cardinality function is then defined in terms of cardUpTo.

```
definition card(S) = cardUpTo(S,basis.max)
```

A majority is a set whose cardinality is greater than 1/2 of the basis set.

```
definition majority(X) = 2 * card(X) > cnt(basis.max)
object spec = {
```

This is the definition of dijoint sets in terms of the member relation. Notice that there is a quantifier alternation in the direction set -> basis.

```
definition
disjoint(X,Y) = forall E. ~(member(E,X) & member(E,Y))
```

This is our inductive invariant. It says that, for
disjoint sets, the sum of the cardinalities up to
bound B is less than the total number of elements
less than B. We prove it by induction on B, using
the induction schema for type `basis`

. As usual,
we have to giev the induction parameter explicitly,
since Ivy can’t infer it automatically.

Most importantly, notice how arithmetic is used here. Because we used definition schemata, we never have an arithmetic applied to a universally quantified variable. This means our verification condition is is in the essentially uninterpreted fragment.

```
property disjoint(X,Y) -> cardUpTo(X,B) + cardUpTo(Y,B) <= cnt(B)
proof
apply ind[basis] with X = B;
showgoals
}
}
object spec = {
```

With the above lemma, Z3 can prove the “majorities intersect” property. The idea is that the lemma can be specialized to this:

```
# property disjoint(X,Y) -> card(X) + card(Y) <= cnt(basis.max)
```

Since both majorities have cardinality greater than
`cnt(basis.max)/2`

, it follows that majorities cannot be
disjoint, so they must have an element in common.

```
property majority(X) & majority(Y) -> exists E. (member(E,X) & member(E,Y))
}
attribute test = impl
}
with basis.impl,index.impl
```

Note: we use the *implementations* of the basis and index
types. That means both are interpreted. Fortunately, we don’t
run afoul of the fragment checker.

```
isolate api = {
object impl = {
```

Here is the implementation of the set type using an unsorted array.

```
instance arridx : unbounded_sequence
instance arr:array(arridx,basis)
```

Tricky: this is a bit of aspect-orientation. It turns the type `set`

into a struct
with just one field called `repr`

. This field gives the concrete representation of a
set as an array. To an isolate that doesn’t use the definition of `member`

below,
the tpye `set`

will still appear to be uninterpreted.

```
destructor repr(X:set) : arr.t
definition member(y:basis,X:set) = exists Z. 0 <= Z & Z < repr(X).end & repr(X).value(Z) = y
```

These lemmas are needed to prove correctness of is_empty.

```
property member(Y,X) -> repr(X).end ~= 0
property repr(X).end ~= 0 -> member(repr(X).value(0),X)
implement empty {
repr(s) := arr.create(0,0)
}
implement add {
if ~member(e,s) {
repr(s) := arr.resize(repr(s),repr(s).end.next,e)
}
}
implement is_empty {
r := repr(s).end = 0;
}
}
attribute test = impl
} with spec
attribute test = impl
}
```

The following is a test instantiation of `indexset`

, to check that the
verification goes through.

```
instance basis : unbounded_sequence
object basis = { ...
var max : basis
}
instance nset : indexset(basis)
export nset.empty
export nset.add
export nset.is_empty
```