Safety: give cei_safe a proof-backed execution theorem

[Th0rgal]

Problem

The compile-time safety surface from #1728 has several implemented pieces (cei_safe, allow_post_interaction_writes, requires(field), mapping roles, unsafe blocks), but cei_safe is not yet backed by a strong proof story that connects the syntactic/effect checks to an execution-level safety theorem.

Scope

• Specify the exact CEI property Verity claims for cei_safe functions.
• Connect the checker output to an execution/spec theorem, not only a syntactic diagnostic.
• Make allowed escape hatches (allow_post_interaction_writes, unsafe) appear as explicit proof/trust obligations.
• Add tests that distinguish accepted CEI-safe programs from programs that compile only with an explicit escape hatch.