Formal Barriers to Longest-Chain Proof-of-Stake Protocols