Add SendOK predicate

Checks whether a send is valid, and if so, whether the rest of the
protocol can depend on the value that was sent.