Conformance model-based tests for voting

[ghost]

• Complete soundness proof for test model #174
• use decidable voting functions
• ensure code compiles to (and runs) Haskell cleanly and tests the reference implementation

Important

We start postulating IsTreeType and refine it as much as we can, e.g we can live with a partially postulated blocktree implementation for the time being

[bwbush]

I'll be working on these:

• use decidable voting functions
• ensure code compiles to (and runs) Haskell cleanly and tests the reference implementation

[bwbush]

#170 completes the 2nd and 3rd items. We still have the soundness proofs to complete.