verity_contract lacks top-level nested struct storage fields

[fricoben]

What construct could not be expressed

Cork Phoenix stores pool state in deeply nested structs:

// contracts/libraries/State.sol
struct State {
    Market info;
    Shares shares;
    PoolState pool;
    uint8 referenceDecimals;
    uint8 collateralDecimals;
}

struct PoolState {
    Balances balances;
    uint256 unwindSwapFeePercentage;
    ...
}

struct Balances {
    CollateralAssetManager collateralAsset;
    uint256 swapTokenBalance;
    uint256 referenceAssetBalance;
}

struct CollateralAssetManager {
    address _address;
    uint256 locked;
}

Accessing state.pool.balances.collateralAsset.locked is a standard Solidity pattern for protocol state management.

Verity supports MappingStruct (struct-valued mappings like mapping(address => {field1, field2})), but there is no syntax for standalone nested structs as top-level storage fields.

What we did instead

Flattened the struct hierarchy into individual storage slots:

verity_contract CorkUnwindExerciseOther where
  storage
    collateralAssetLocked : Uint256 := slot 0  -- was: state.pool.balances.collateralAsset.locked
    swapTotalSupply : Uint256 := slot 1
    ...

Proposed Verity improvement

Support nested struct declarations in the storage section, e.g.:

  storage
    pool : struct
      balances : struct
        collateralAsset : struct
          locked : Uint256
        swapTokenBalance : Uint256

This would allow models to mirror the Solidity struct hierarchy, making source-to-model correspondence easier to verify.

Severity

nice-to-have — the flat-slot workaround preserves semantics perfectly. The gap is purely structural (harder to visually verify the model matches the Solidity source).

Context

Encountered while modeling Cork Protocol (Phoenix) unwindExerciseOther for the verity-benchmark. See Benchmark/Cases/Cork/PoolSolvency/Contract.lean.

[fricoben]

Note: this is a concrete instance of the top-level struct gap acknowledged in #1724 (see latest scope comment: "storage strings/bytes and top-level structs" listed as remaining parity work). Filing separately to track the specific use case from Cork Protocol modeling.