Proofs: model checkpoint-aware native switch-tail semantics

[Th0rgal]

Problem

The proof-observation framework sketched in #1884 is too broad for the current blocker. The actual obstruction is that native switch-tail lowering can resume after Leave checkpoints and then consult raw matched-flag state in ways the current source/proof observation model does not expose cleanly.

That makes the E2-E7 / F2-F7 / S8 strengthening brittle: the proof-only observation abstraction cannot soundly erase the checkpoint interaction without a more explicit semantic contract for native switch tails.

Clean scope

Add a focused checkpoint-aware treatment for native switch-tail semantics/lowering:

• define the source-side observation for Leave checkpoints and switch-tail continuation explicitly;
• make matched-flag lookup after a checkpoint part of the modeled state transition rather than an incidental Yul variable fact;
• update native switch-tail lowering so the generated IR has a stable proof hook for the checkpoint boundary;
• prove the narrow shape lemmas needed to remove the remaining conditional assumptions in the affected E/F/S cases.

Out of scope

This should not try to solve the entire per-BridgedStraightStmt observation framework in one issue. Once this focused checkpoint/switch-tail contract exists, the broader unconditional-lifting work can be reopened or reduced to a small proof-cleanup task.