Use nondeterministic data

We abstract away sent and received data because the verification
conditions we are interested in can be checked with assertions
on control registers and buffer descriptors.