In terms of specific implementation I'm not sure, but it may be possible to use a formal modeling tool like TLA+ to prove a particular approach only results in

In terms of specific implementation I'm not sure, but it may be possible to use a formal modeling tool like TLA+ to prove a particular approach only results in outcomes you consider correct. So you could try to model the trade and all the sub states you mention in a naive state machine way, then check if that super messy tangle works as intended or if it has incorrect behavior.