Create a formal specification for the ledger rules for the Shelley release. This includes the delegation design.

This work includes: 1) a LaTeX document describing the operational rules, 2) an executable Haskell model, and 3) property tests and generators. As a bonus we can add proofs of our properties in Coq.