The part I would not gloss over is the key schedule being folded into the state space for ERXP, because that is what lets them get an exact fixed-key quantity instead of a characteristic average that quietly assumes independence. For SIMON and SIMECK, that matters, since the symmetry-breaking constants live in the round function, but the weak-key class estimates can still move once the schedule constraints are accounted for. I would read this less as a trail generator and more as a way to tell when an RX trail you already found is actually compatible with a real key.