Sync executable with formal spec - UTXO STS

[uroboros]

• the exec. spec does not implement the highlighted preconditions.
• the use of helper functions like validNoReplay obscures the precondition txins /= Empty (while providing re-use) - I think in the absence of need to reuse preconditions, we should inline the preconditions instead