Execution of finite Mathlib stack machines

Reuse the exact-run definition from the rational hitting-list development. The TM2 bridge keeps its original definition and proofs in place and exposes that execution convention alongside the bundled Mathlib computation types.