Storage: generate layout certificates and non-alias lemmas

[Th0rgal]

Goal

Generate storage-layout artifacts and Lean lemmas for Solidity storage locations, especially structs, mappings, nested mappings, and bounded word offsets.

Motivation

Morpho Blue currently needs an explicit storage non-aliasing boundary for keccak-derived mapping/struct locations. Verity should generate a reviewable layout certificate and local proof obligations, reducing the trust surface from a global semantic-location injection assumption to precise declared-location non-overlap lemmas plus explicit keccak-domain assumptions.

Acceptance criteria

• The artifact lists every storage family, slot root, mapping-key shape, struct offset, and nested mapping derivation used by a contract.
• Generated lemmas prove non-overlap for finite declared slots and bounded struct offsets.
• Keccak non-collision assumptions, if still needed, are local and named by the concrete preimage families.
• The generated certificate is sufficient to replace Morpho Blue's global Loc.slot_inj boundary.