Effects: strengthen generated annotations into execution frame theorems

[Th0rgal]

Problem

#1729 has landed a useful effect surface (view, modifies, no_external_calls, generated _is_view, _no_calls, _modifies, _frame facts), but the remaining work is proof strengthening.

Today the generated theorems are mostly model-flag and frame-predicate facts. The next milestone should connect effect annotations to execution/spec frame-condition theorems that users can rely on when composing contract proofs.

Scope

• Define the execution-level meaning of view, modifies, and no_external_calls.
• Strengthen generated theorems from model metadata facts to source/interpreter preservation facts where possible.
• Make unsupported effect surfaces fail fast or emit explicit proof obligations.
• Add tests/examples that demonstrate a consumer proof using the stronger frame theorem.