It is less clear that the instances of ABA can be bounded; as written, the ABA protocol proceeds in rounds, each round making use of a common COIN, until a termination condition is reached, which does not occur with any a priori bound. However, the running time analysis of the protocol suggests that even in the worst case, an instance of ABA requires more than k coins with probability O(2^-k). Thus it suffices to establish a bound, say k=120.
From amiller/honeybadgerbft#57:
Potentially related: https://github.com/amiller/HoneyBadgerBFT/issues/63