Add TLA+ formal specifications for bytecode tape optimizer

[gvonness-apolitical]

Summary

• TapeOptimizer.tla: Stepwise state machine modelling CSE + DCE on abstract tapes (5 opcode kinds). 6 phases (build → cse_scan → cse_remap → dce_mark → dce_compact → done), 11 invariants covering structural validity, CSE remap properties, DCE reachability, and post-optimization correctness including no-duplicate CSE entries. Termination as liveness property.
• Idempotency.tla: Pure functional CSE/DCE operators verifying optimize(optimize(tape)) = optimize(tape) for all valid tapes via nondeterministic exhaustive checking.
• CI + docs: Added TapeOptimizer and Idempotency check steps to specs.yml, path trigger for optimize.rs, updated specs/README.md with invariant cross-reference, variable mapping, and parameter sweep recommendations.

All specs pass TLC at default bounds (MaxTapeLen=5, NumInputs=2): TapeOptimizer 960K states in ~20s, Idempotency 55K states in ~1s. Mutation test confirms invariants are non-vacuous (removing commutative normalization triggers PostOptValid violation).

Test plan

• CI TLA+ Specs workflow passes (TapeOptimizer + Idempotency model checking)
• Existing Rust tests unaffected (cargo test all pass)
• Existing Revolve/HintAllocation specs still pass in CI