Light Client spec has been merged: #1336

The following remain TODO:

• update how the spec handles the UNBONDING PERIOD (need a new condition so if unbonding period has passed, we flame out and revert back to social consensus to get a new validator hash)
• implement the LastHeader RPC call in Tendermint, or provide a convenience function to simulate it, so we can get the latest header with a given validator height
• change the validator change mechanism so the validator set changes at H+2 (instead of H+1) for changes returned during block H
• possibly improve the notation/clarity in the spec, especially around global mutable variables vs local variables