feat(symbolic): Cancun SELFDESTRUCT semantics

[mablr]

Summary

Models fork-aware symbolic SELFDESTRUCT semantics for Cancun/EIP-6780.

Closes OSS-365

Changes

• Pre-Cancun and same-transaction-created contracts still delete.
• Cancun+ existing contracts transfer balance and halt while preserving code/storage.
• Transaction-scoped created accounts are tracked for this decision.

Tests

• Added Cancun preservation, same-transaction deletion, and false-pass prevention coverage.
• Added unit coverage for created-account tracking across snapshots.

[grandizzy]

One blocking concern: symbolic beneficiaries can produce a false PASS. An unconstrained symbolic beneficiary resolves to a synthetic representative address that is never equal to state.address, so the beneficiary != address guard is always true and the beneficiary == self branch is never explored. For an existing Cancun contract, real EVM keeps the balance when the target is itself — the model transfers it away and can prove a property that doesn't actually hold. This matters more now that symbolic_selfdestruct_accepts_symbolic_beneficiary flips from incomplete → [PASS].

Suggested resolution: either report incomplete when a symbolic beneficiary may alias state.address, or fork on beneficiary_word == state.address_word. A few extra tests (self-beneficiary no-burn, CREATE2 same-tx, reverted-CREATE, sequence boundary) would also round out coverage. Details inline.

[grandizzy]

lgtm!

[figtracer]

lgtm