Axis 4: Storage safety — automatic EIP-7201 namespaced storage

[Th0rgal]

Goal

Make proxy-safe storage the default in Verity by automatically computing EIP-7201 namespaced storage slots from the contract name. This prevents proxy storage collisions — a well-known attack vector — without requiring developers to manually compute namespace hashes.

Parent issue: #1726 (Language design improvements)
Connects to: #1724 Wave 3 (storage completeness), #1420 (proxy patterns)

---

Problem

Proxy Storage Collisions

When using `delegatecall`-based proxies (UUPS, transparent proxy), the implementation contract and the proxy share the same storage layout. If two contracts use slot 0 for different purposes, they silently corrupt each other's data. This has caused multiple production incidents.

Inheritance Storage Collisions

Adding a field to a parent contract shifts all child contract storage. This is a deployment-time footgun that Solidity partially addresses with EIP-7201 (namespaced storage) — but it's opt-in and most developers don't use it.

What Verity Already Has

• Explicit slot assignments (`slot 0`, `slot 1`, ...)
• Reserved slot ranges (`reservedSlotRanges`)
• Alias slot mirror writes (`aliasSlots`)
• Compile-time conflict detection (fail-fast on overlapping slots within a contract)

These are good foundations. What's missing is cross-contract collision prevention.

---

Design: Automatic Namespace (Option A)

The macro automatically computes an EIP-7201 namespace from the contract name:

```
verity_contract ERC20Token where
storage
totalSupply : Uint256 := slot 0 -- actual slot: namespace_base + 0
balances : Address → Uint256 := slot 1 -- actual slot: namespace_base + 1
allowances : Address → Address → Uint256 := slot 2
```

The namespace base is computed at elaboration time:
```
namespace_base = keccak256("ERC20Token.storage.v0") - 1
```

This follows the EIP-7201 formula: `keccak256(abi.encode(uint256(keccak256(id)) - 1)) & ~0xff`

How It Works

1. At macro elaboration time: The Lean kernel computes the keccak hash (Keccak is already available — it's used for event signatures and storage keys)
2. All `slot N` declarations are offset: `slot 0` becomes `slot (namespace_base + 0)`
3. Mapping keys are also namespaced: `keccak256(key, namespace_base + slot_offset)`
4. The namespace string is deterministic: `"{ContractName}.storage.v0"`

Override Mechanism

For contracts that need specific slot positions (e.g., to match an existing deployment's layout):

```
verity_contract LegacyToken where
storage @[no_namespace] -- opt out: use raw slot numbers
totalSupply : Uint256 := slot 0
balances : Address → Uint256 := slot 1
```

Or override the namespace string:

```
verity_contract UpgradedToken where
storage @[namespace "eip7201:legacy.token.v2"]
totalSupply : Uint256 := slot 0
balances : Address → Uint256 := slot 1
```

Versioning

The `.v0` suffix enables storage layout versioning. If a contract's storage layout changes in an incompatible way, bump to `.v1` — this naturally produces a completely different namespace, making collision impossible.

---

Implementation Plan

Phase 1: Namespace Computation (1 week)

1. In `Macro/Elaborate.lean`: compute `keccak256("{ContractName}.storage.v0")` using the existing kernel Keccak
2. Store the namespace base as a constant in the generated contract module
3. Emit the namespace base in the ABI JSON (for tooling interop)

Phase 2: Slot Offsetting (1 week)

1. In `Macro/Translate.lean`: when processing `slot N`, replace with `slot (namespace_base + N)`
2. For storage mappings: the mapping's base slot is offset, key computation follows naturally
3. For `reservedSlotRanges`: offset the range bounds

Phase 3: Override Attributes (0.5 weeks)

1. `@[no_namespace]`: skip offsetting for this contract
2. `@[namespace "custom.string"]`: use a custom namespace string instead of the contract name

Phase 4: Verification (0.5 weeks)

1. Add compile-time check: if two contracts in the same project have the same namespace, warn
2. Add `--print-storage-layout` flag that shows the actual computed slot numbers for debugging
3. Integration tests with proxy patterns

Total estimated effort: 2–3 weeks

---

ABI and Tooling

The namespace base should be emitted in the contract's ABI metadata:

```json
{
"contractName": "ERC20Token",
"storageNamespace": "ERC20Token.storage.v0",
"storageNamespaceBase": "0x...",
"storageLayout": [
{ "label": "totalSupply", "slot": "0x...", "offset": 0, "type": "uint256" },
{ "label": "balances", "slot": "0x...", "offset": 0, "type": "mapping(address => uint256)" }
]
}
```

This enables tools (Foundry, Hardhat, block explorers) to correctly decode storage for namespaced contracts.

---

Impact

Before	After
Developer manually picks slot numbers	Slot numbers auto-computed from namespace
Proxy collisions possible if two contracts use same slots	Collision impossible (different contract names → different namespaces)
Storage layout versioning is manual	Bump `.v0` → `.v1` for clean migration
Need expert knowledge of EIP-7201	Automatic — developers don't need to know about namespacing

Related Issues

• Language design improvements: fix Solidity's systemic flaws, inspired by Rust/Cairo/Move #1726 — Parent: language design improvements
• Solidity feature parity: close the gap between verity_contract EDSL and production Solidity #1724 — Solidity parity (Wave 3: storage completeness)
• Verification: proxy and upgradeability semantics on top of native delegatecall support #1420 — Proxy pattern support (namespaced storage is a prerequisite)