Motivation

The ERC-4337 v0.9 StakeManager packs five fields into two storage slots per account:

```solidity
struct DepositInfo {
uint256 deposit;
bool staked; // 1 bit (packed into slot 1 top byte)
uint112 stake; // 112 bits
uint32 unstakeDelaySec; // 32 bits
uint48 withdrawTime; // 48 bits
}
mapping(address => DepositInfo) public deposits;
```

Verity supports struct-valued mappings (`mappingStruct`) but each member resolves to its own slot — bitfield packing into a sub-32-byte region isn't expressed. The verity-benchmark ERC-4337 case therefore models DepositInfo as four separate `Address → Uint256` mappings and documents the slot-layout divergence (TRUST_DIVERGENCES.md item 11).

Proposed surface

```lean
storage
deposits : mapping Address → DepositInfo := slot 1 where
DepositInfo
| deposit : Uint256 packed(0) -- slot 0
| staked : Bool packed(slot := 1, offset := 0, width := 1)
| stake : Uint112 packed(slot := 1, offset := 1, width := 112)
| unstakeDelaySec : Uint32 packed(slot := 1, offset := 113, width := 32)
| withdrawTime : Uint48 packed(slot := 1, offset := 145, width := 48)
```

`structMember deposits k "deposit"` then lowers to `sload(mappingSlot(deposits, k))` (the existing path).
`structMember deposits k "staked"` lowers to:
```
let raw := sload(mappingSlot(deposits, k) + 1)
let value := and(shr(0, raw), mask(1))
```
and writes do read-modify-write into slot 1.

Implementation notes

• The existing `structMember` infrastructure carries a `wordOffset` per field; this PR extends it with `(bitOffset : Nat, bitWidth : Nat)` per packed member.
• Storage codegen needs the mask + shift dance for both reads and writes.
• Validators must reject overlapping packings (sum of bitWidths in a slot ≤ 256).
• Frame theorems already handle word-level storage updates; the bitfield variant needs a refinement that says the masked-shifted update preserves orthogonal fields in the same slot.

Unblocks

• `lfglabs-dev/verity-benchmark` ERC-4337 item 11 — DepositInfo packed exactly like upstream.
• ERC-4626 vault state (totalAssets / totalShares packed).
• Solady-style `SafeOwnable` (owner + nominee in one slot).