Formally Verify `getTransactionHash() == keccak256(encodeTransactionData())`

[nlordell]

          Should we have an FV invariant that checks this? (Could be outside of this PR)

Originally posted by @remedcu in #959 (comment)