Make the spec consistent with #904

[pgrange]

          This would not typecheck if we would have written all this in agda :D

I think we need to change the signature of onReq to have ${\mathcal T}{req}^{#}$ as argument, then have an additional wait with $\forall h \in {\mathcal T}{req}^{#} : (h, \cdot) \in {\mathcal T}$ and a resolve statement defining ${\mathcal T}_{res}$, i.e. what I had done here (with $\hat {\mathcal T}$ this time though):

#728 (comment)

Originally posted by @ch1bo in #904 (comment)

[ch1bo]

• Undo the allTxs cleanup
  • Make sure that does not degrade performance
• Update the fig_offchain_prot.tex to match what is currently on master
  • No semantics change!
• Prune transactions from seenTxs and allTxs when handling a ReqSn (code + spec)
  • in the spec
  • in the code
  • No test failures expected one way or the other here
• Rename terms: seenTxs -> localTxs, seenUTxO -> localUTxO, allTxs stays the same
  • in the code
  • in the spec
• Discuss open points and create follow-ups if not directly addressable
  • Why do we need to remove from allTxs when ttl runs out? We have undone that change in step 1 as there might be a valid scenario
    • Discussed in d608de3
  • Coherence of TxInvalid messages, e.g. when receiving invalid txs it's unintuitive to get informed about them; on the other hand, we would like to be informed if transactions are not valid to our local view
    • Captured in Improve TxInvalid notifications #990
  • There is no equivalence for storing the fact that we requested a snapshot in the spec. Do we really need it? If yes, we should have a mention of it in the spec or update the formalism accordingly.
    • Covered by Clarify what is a seen snapshot #982
  • Prune transactions by id? We had that in the past, but not clear why we moved away of this?
    • No: we cannot, because transactions would not be "re-validated" and e.g. timed txs would not get dropped while we expect that
  • .. add any occurring in the steps above
• Make prose and notation/variable sections in the spec consistent with the figure