Added partial specifications for Vote.move.

This was an exploration of a different more top-down specification
methodology. The focus has been on global specifications, so there are
no "aborts_if"s, yet, and the ensures conditions are incomplete.

There are also more global specifications to write.

In the process of specifying and verifying this, I discovered that
an election could be created that has already be accepted, by
requiring 0 votes to pass.  So, I added a new assert to prevent
people from doing that.

Closes: #10090