Executable plane of getMappingN/setMappingN/structMember(2) is a pure-0/no-op stub (nested and struct mappings have no state)

Found while translating IdleCreditVault (Pareto Credit Vault) into a verity_contract on top of #2413 (c907fef0).

The executable plane of nested mappings and struct mappings is a stub:

-- Contracts/Common.lean
def getMappingN {κ α : Type} (_slot : StorageSlot α) (_keys : List κ) : Contract Uint256 := pure 0
def setMappingN {κ α : Type} (_slot : StorageSlot α) (_keys : List κ) (_value : Uint256) : Contract Unit := pure ()
def structMember {κ α : Type} [Inhabited α] (_field : String) (_key : κ) (_member : String) : Contract α := pure default
def setStructMember {κ α : Type} (_field : String) (_key : κ) (_member : String) (_value : α) : Contract Unit := pure ()
-- same for structMember2 / setStructMember2 / getMappingWord / setMappingWord

So a contract with

apr0Users : MappingStruct(Address, [principal @word 0, principalEpoch @word 1, settledPrincipal @word 2, settledInterest @word 3]) := slot 219
withdrawsRequestsByEpoch : Address → Uint256 → Uint256 := slot 226

has a correct compilation model but an executable model in which every read of these fields is 0 and every write is a no-op. In Pareto that silently voids the APR-0 receipt bucket, the per-epoch receipt maps and the loss/default claim paths, so no executable-plane theorem about claims can be trusted.

Two smaller problems on the same surface:

• getMappingN field [u, e] with an Address key and a Uint256 key does not typecheck in the executable plane (List κ is homogeneous), so mapping(address => mapping(uint256 => uint256)) cannot be read even as a stub; MappingStruct2(Address, Uint256, [amount @word 0]) is the only compiling encoding.
• The stubs are silently accepted; nothing warns that the field has no executable semantics.

Ask: give these accessors real ContractState semantics (e.g. a hashed-key channel next to storageMap/storageMapUint/storageMap2, or StorageKey.contractSlot with an injective key encoding), and until then fail closed or warn when a contract declares such a field.

Closure-side tracking: audit/VERITY-GAPS.md G2.

Start in Contracts/Common.lean, reading the executable accessors alongside storageMap, storageMapUint, and storageMap2. Trace the ContractState path for nested and struct mappings, then verify that reads and writes have real state semantics and that unsupported declarations fail closed or warn; audit/VERITY-GAPS.md tracks this as G2.