depending on (State1) { Validate State2; }
Results in State2 getting initialized before State1. If both states are in the same partition, that means that the algo continues in State1 instead of State2. This will not occur if the partition is already in State1, so it is essentially a race condition.
It appears that the "simple" solution is to ensure that tma_init_state() is called before any other side effects are executed. Whether that is actually easy to implement is yet to be determined.
depending on (State1) { Validate State2; }
Results in State2 getting initialized before State1. If both states are in the same partition, that means that the algo continues in State1 instead of State2. This will not occur if the partition is already in State1, so it is essentially a race condition.It appears that the "simple" solution is to ensure that tma_init_state() is called before any other side effects are executed. Whether that is actually easy to implement is yet to be determined.
This of course applies to arp-das also.