Computing optimal 8501 instructions for rotations using an SMT solver and Racket with Rosette: https://lab.whitequark.org/notes/2020-04-06/synthesizing-optimal-8051-code/