feat(formal): real-lift R2-loops — backward jumps (Loop/Br/BrIf) + while simulation (settles #601)

feat(formal): real-lift R2-loops — backward jumps (Loop/Br/BrIf) + while simulation (settles #601) #1279