Allow multiple storage_namespace blocks in one verity_contract

[Th0rgal]

Summary

verity_contract accepts exactly one storage_namespace declaration (Verity/Macro/Syntax.lean:54-55 + the grammar's (verityNamespaceSpec)? line at 81). This works for contracts with a single ERC-7201 namespace, but rules out faithful translations of upstream Solidity contracts that compose multiple namespaced storage layouts in one address.

Concrete blocker

UnlinkPool.sol (unlink-xyz/monorepo@4bc46c1f) carries three logically distinct ERC-7201 namespaces:

• unlink.storage.State (in State.sol)
• unlink.storage.UnlinkPoolRelayers (in UnlinkPool.sol)
• The implicit unlink.storage.LazyIMTData carried by InternalLazyIMT

In cases/unlink_xyz/pool (feat/unlink-pool-port-scratchpad-helpers), the case currently flattens all three into a single storage_namespace "unlink.storage.UnlinkPoolRelayers" block, which loses the per-namespace slot rebasing that Solidity uses.

Proposal

Either:

(a) Multiple storage_namespace blocks — verityNamespaceSpec becomes * instead of ?. Subsequent storage blocks attach to the most recent namespace declaration. The macro would walk the namespace list and rebase each storage block onto its keccak-namespace key.

(b) storage_block "<namespace>" { ... } form — a single verity_contract hosts multiple keyword blocks, each carrying its own ERC-7201 layout. Existing storage_namespace "..." + storage ... form remains as the single-namespace shortcut.

Relation to #1730

#1730 (Axis 4 — automatic ERC-7201 namespaced storage) discusses making the namespace automatic per contract. That conversation is broader than this single-vs-multi-namespace gap. We're filing this as a self-contained ticket because:

1. It unblocks faithful Unlink translation today, regardless of which way Axis 4: Storage safety — automatic EIP-7201 namespaced storage #1730 lands.
2. It's a syntactic / translator change rather than a default-policy change.

Definition of done

• verity_contract accepts ≥1 storage_namespace/storage block pairs.
• Smoke contract under Contracts/Smoke.lean exercises two namespaces in one contract (with #check_contract verifying storage-slot derivation).
• #guard_msgs test pinning the rejection diagnostic when the same namespace key appears twice.
• verity-benchmark cases/unlink_xyz/pool re-translation lands separate State / RelayerStorage / PoolStorage namespaces.

Subsumes the "W7" workaround listed in the spec-review of verity-benchmark#42.

[Th0rgal]

Status update from the current Unlink translation work (local branches, not yet merged):

• verity_contract storage parsing now accepts namespace switches inside one storage block, so one contract can contain multiple namespaced storage sections.
• Added explicit storage_namespace erc7201 "..." support using the ERC-7201 formula:
  keccak256(abi.encode(uint256(keccak256(key)) - 1)) & ~bytes32(uint256(0xff)).
• Contracts.Smoke.MultiNamespaceStorageSmoke exercises both Unlink roots in one contract:
  • unlink.storage.State => 0xd7df...cb000
  • unlink.storage.UnlinkPoolRelayers => 0xd8b6...19b00
• verity-benchmark UnlinkPool now represents these as separate namespace sections, and Benchmark.Cases.UnlinkXyz.Pool.Compile checks the generated slots against the upstream Solidity constants.

I would close this issue after the Verity and benchmark changes are merged. One acceptance item from the original issue remains optional/follow-up: a duplicate-namespace diagnostic guard. The Unlink blocker itself is addressed by the local implementation.

[Th0rgal]

Closed by verity#1900 and exercised in verity-benchmark#71.

Post-merge evidence:

• Verity now accepts multiple declarations in one , including .
• covers the macro path.
• The Unlink pool benchmark now uses separate ERC-7201 namespaces for and .
• checks the namespace slot constants against the Solidity source roots.

The optional duplicate-namespace diagnostic mentioned earlier can be tracked separately if we want a nicer error, but it is no longer blocking the Unlink translation.

[Th0rgal]

Cleaned-up closure evidence for the comment above:

• Verity now accepts multiple storage_namespace declarations in one verity_contract, including storage_namespace erc7201 "...".
• Contracts.Smoke.MultiNamespaceStorageSmoke covers the macro path.
• The Unlink pool benchmark now uses separate ERC-7201 namespaces for unlink.storage.State and unlink.storage.UnlinkPoolRelayers.
• Benchmark.Cases.UnlinkXyz.Pool.Compile checks the namespace slot constants against the Solidity source roots.

The optional duplicate-namespace diagnostic mentioned earlier can be tracked separately if we want a nicer error, but it is no longer blocking the Unlink translation.