feat(Codegen): true bytecode immutables (constructor-set values embedded in runtime code)

[Th0rgal]

Problem

Verity has no support for Solidity immutable variables. Constructor-set values that solc embeds in runtime bytecode must currently be modeled as ordinary storage slots.

Concrete instance from the Morpho Midnight port (Th0rgal/morpho-verity): INITIAL_CHAIN_ID is modeled as storage slot 1024 instead of a bytecode constant (Midnight/Contract.lean:2425), with the mapping doc noting "until immutable support lands".

Why it matters

• Fidelity: slot-modeled immutables silently change the storage footprint vs the Solidity source, so storage-layout reports and the "source faithfulness" column cannot be exact.
• Proof interaction: a phantom storage slot participates in frame/footprint reasoning (Frame rule, footprint computation, and coupling invariants for the IR interpreter #1990) and storage non-alias certificates, where the real contract has no such slot.
• Yul drift: solc emits immutables via setimmutable/loadimmutable in deploy/runtime code; Verity's output cannot shape-match this category.

Scope sketch

1. EDSL surface: immutable NAME : Type declared in the contract block, assignable only in the constructor.
2. CompilationModel: a distinct ImmutableRef value kind (not a storage slot), with deploy-time substitution semantics.
3. Codegen: emit setimmutable / loadimmutable (or the equivalent literal-patching layout solc uses).
4. Proofs: interpreter semantics treating immutables as deploy-time-fixed constants of the runtime environment; widen SupportedSpec accordingly.
5. Reports: surface immutables in storage-layout/trust reports as a separate section (zero storage footprint).

Not covered elsewhere

Absent from #1982 (all tiers) and from #1724's open parity scope. Filed as a result of the 2026-06-12 Morpho fidelity analysis.