diff --git a/src/Solcore/Frontend/Syntax/NameResolution.hs b/src/Solcore/Frontend/Syntax/NameResolution.hs
index 4bde7f2e8..f1310cc83 100644
--- a/src/Solcore/Frontend/Syntax/NameResolution.hs
+++ b/src/Solcore/Frontend/Syntax/NameResolution.hs
@@ -522,6 +522,13 @@ unwrapQualifierReceiver (Just (Con (QualName d conName) []))
   | pretty d == conName = Just (Var d)
 unwrapQualifierReceiver me = me
 
+-- True for receivers that should trigger UFCS-style method-call rewriting.
+-- For now this only covers (unresolved) contract field accesses, so
+-- `members.push(addr)` resolves into `Array.push(members, addr)`.
+isUfcsReceiver :: Exp Name -> Bool
+isUfcsReceiver (FieldAccess Nothing _) = True
+isUfcsReceiver _ = False
+
 instance Resolve S.Exp where
   type Result S.Exp = Exp Name
 
@@ -683,6 +690,14 @@ instance Resolve S.Exp where
           pure (Call Nothing n es')
         (_, Just TParameter) ->
           pure (Call Nothing n es')
+        -- UFCS-style method call on a value receiver:
+        -- `receiver.method(args)` -> `Class.method(receiver, args)` when there
+        -- is a unique class containing a method named `n`.
+        (Just receiver, _) | isUfcsReceiver receiver -> do
+          mClass <- findClassWithMethod n
+          case mClass of
+            Just c -> pure (Call Nothing (QualName c (pretty n)) (receiver : es'))
+            Nothing -> undefinedName n
         -- error
         _ -> do
           sameName <- isSameNameConstructor n
@@ -1017,6 +1032,24 @@ lookupName n =
         fdt = Map.lookup n (fieldEnv env)
     pure (ldt <|> gdt <|> cdt <|> fdt)
 
+-- For UFCS-style method calls (`value.method(args)`): find a class that has
+-- a method named `m` so we can rewrite the call as `Class.method(value,args)`.
+-- Returns the first match; ambiguity across multiple classes falls back to
+-- the regular undefined-name path.
+findClassWithMethod :: Name -> ResolveM (Maybe Name)
+findClassWithMethod m =
+  do
+    env <- get
+    let classes = Map.keys (classEnv env)
+        matches =
+          [ c
+          | c <- classes,
+            Map.lookup (QualName c (pretty m)) (scopeEnv env) == Just TFunction
+          ]
+    pure $ case matches of
+      [c] -> Just c
+      _ -> Nothing
+
 wrapError :: (Pretty b) => ResolveM a -> b -> ResolveM a
 wrapError m e =
   catchError m handler
diff --git a/std/std.solc b/std/std.solc
index fc53d7335..d633f4968 100644
--- a/std/std.solc
+++ b/std/std.solc
@@ -1,5 +1,5 @@
-pragma no-patterson-condition ABIEncode, Num;
-pragma no-coverage-condition ABIDecode, MemoryType;
+pragma no-patterson-condition ABIEncode, Num, Array, ArrayPush;
+pragma no-coverage-condition ABIDecode, MemoryType, Array, ArrayPush;
 
 export {
   ABIAttribs,
@@ -8,6 +8,8 @@ export {
   ABIEncode,
   ABITuple(*),
   Add,
+  Array,
+  ArrayPush,
   Assign,
   Bounded,
   CalldataWordReader(*),
@@ -45,6 +47,7 @@ export {
   address(*),
   allocate_memory,
   and,
+  array(*),
   assert,
   byte(*),
   bytes,
@@ -760,6 +763,8 @@ forall t . instance returndata(t) : Typedef(word) {
 
 data mapping(member, index) = mapping(word) ;
 
+data array(member) = array(word) ;
+
 // --- Low-level memory ops
 
 function mload(a:word) -> word {
@@ -1222,6 +1227,33 @@ instance memory(bytes):ABIEncode {
     }
 }
 
+// ABI encoding for a memory dynamic array whose elements fit in a single word.
+// Assumes memory layout `[ length | elem_0 | elem_1 | ... ]`, which matches the
+// on-the-wire tail of `t[]` so the body can be `mcopy`d verbatim.
+// `memory(DynArray(t)):ABIAttribs` is already derivable from the generic
+// `memory(ty):ABIAttribs` + `DynArray(t):ABIAttribs` instances above.
+forall t . t:Typedef(word) =>
+instance memory(DynArray(t)):ABIEncode {
+    function encodeInto(x:memory(DynArray(t)), basePtr:word, offset:word, tail:word) -> word {
+        let srcPtr : word = Typedef.rep(x);
+        let len : word = mload(srcPtr);
+        let totalBytes : word = (len + 1) * 32;
+
+        // head slot: relative pointer from basePtr to tail
+        mstore(basePtr + offset, tail - basePtr);
+
+        // copy length + elements verbatim into the tail
+        let s : word = srcPtr;
+        let t_ : word = tail;
+        let n : word = totalBytes;
+        assembly {
+            mcopy(t_, s, n)
+        }
+
+        return tail + totalBytes;
+    }
+}
+
 instance ():ABIEncode {
     // a unit256 is written directly into the head
     function encodeInto(x:(), basePtr:word, offset:word, tail:word) -> word {
@@ -1704,6 +1736,67 @@ instance mapping(index, member):StorageSize {
     }
 }
 
+forall member . instance array(member):Typedef(word) {
+    function rep(x:array(member)) -> word {
+        match x {
+            | array(y) => return y;
+        }
+    }
+    function abs(x:word) -> array(member) {
+        return array(x);
+    }
+}
+
+// cf https://docs.soliditylang.org/en/latest/internals/layout_in_storage.html#mappings-and-dynamic-arrays
+// the slot itself stores the array length; elements live at keccak256(slot) + i
+forall member .
+instance array(member):StorageSize {
+    function size(x:Proxy(array(member))) -> word {
+        return 1;
+    }
+}
+
+// Dynamic storage arrays carry their length at the slot itself (matching the
+// Solidity convention) while elements live at keccak256(slot) + i.
+forall self . class self:Array {
+    function length(arr:self) -> uint256;
+    function setLength(arr:self, n:uint256) -> ();
+    function pop(arr:self) -> ();
+}
+
+// push is split into its own MPTC so its element type only shows up where it
+// actually matters (the value being appended), without forcing `length`/
+// `setLength`/`pop` to drag along an unconstrained `elem` parameter.
+forall self elem . class self:ArrayPush(elem) {
+    function push(arr:self, val:elem) -> ();
+}
+
+forall t .
+instance storage(array(t)):Array {
+    function length(arr:storage(array(t))) -> uint256 {
+        return uint256(sload_(Typedef.rep(arr)));
+    }
+    function setLength(arr:storage(array(t)), n:uint256) -> () {
+        sstore_(Typedef.rep(arr), Typedef.rep(n));
+    }
+    function pop(arr:storage(array(t))) -> () {
+        let slot : word = Typedef.rep(arr);
+        let n : word = sload_(slot);
+        if (n == 0) { out_of_bounds(); }
+        sstore_(slot, n - 1);
+    }
+}
+
+forall t . t:StorageType =>
+instance storage(array(t)):ArrayPush(t) {
+    function push(arr:storage(array(t)), val:t) -> () {
+        let slot : word = Typedef.rep(arr);
+        let n : word = sload_(slot);
+        StorageType.store(hash1(slot) + n, val);
+        sstore_(slot, n + 1);
+    }
+}
+
 forall self memberRefType.
 class self:LVA(memberRefType) {
     function acc(x:self) -> memberRefType;
@@ -1804,6 +1897,19 @@ forall k v.
     }
 }
 
+forall v.
+ instance storage(array(v)):CanStore(storage(array(v))) {
+    function store(l:storage(array(v)), r:storage(array(v))) -> () {
+      // StorageType.store(Typedef.rep(l), r);
+      unimplemented();
+    }
+    function load(l:storage(array(v))) -> storage(array(v)) {
+      // return StorageType.load(Typedef.rep(l));
+      unimplemented();
+      return l;
+    }
+}
+
 
 instance storage(string):CanStore(memory(string)) {
   function store(dst:storage(string), src:memory(string)) -> () {
@@ -1931,6 +2037,28 @@ instance (storage(mapping(i,a)), i): RValueIdxAccess(a) {
   }
 }
 
+forall a i . i:Typedef(word) =>
+instance (storage(array(a)), i): LValueIdxAccess(storage(a)) {
+  function lookup(xi : (storage(array(a)), i)) -> storage(a) {
+    match(xi) {
+      | (x, i) =>
+          let slot : word = Typedef.rep(x);
+          let idx : word = Typedef.rep(i);
+          // Bounds check: idx must be in [0, length). Length lives at the
+          // slot itself; inlined to avoid an Array(t) dispatch here.
+          if (idx >= sload_(slot)) { out_of_bounds(); }
+          return storage(hash1(slot) + idx);
+    }
+  }
+}
+
+forall a i . a:StorageType, i:Typedef(word) =>
+instance (storage(array(a)), i): RValueIdxAccess(a) {
+  function lookup(xi : (storage(array(a)), i)) -> a {
+    return readStorage(LValueIdxAccess.lookup(xi));
+  }
+}
+
 forall a. a:StorageType =>
 function readStorage(x:storage(a)) -> a {
   return StorageType.load(Typedef.rep(x));
@@ -1947,14 +2075,18 @@ function lval(x:r) -> a {
 }
 */
 
-forall i a . i:Typedef(word) =>
-function lidx( m: storage(mapping(i,a)), x:i) -> storage(a) {
-  return storage(hash2(Typedef.rep(m), Typedef.rep(x)));
+// lidx/ridx are the generic indexed-access helpers used by the `arr[i]`
+// desugaring. They dispatch through LValueIdxAccess / RValueIdxAccess, so any
+// collection (mapping, array, ...) that provides those instances supports the
+// `arr[i]` syntax.
+forall col idx ref . (col, idx):LValueIdxAccess(ref) =>
+function lidx(c: col, i: idx) -> ref {
+    return LValueIdxAccess.lookup((c, i));
 }
 
-forall i a . i:Typedef(word), a:StorageType  =>
-function ridx( m: storage(mapping(i,a)), x:i) -> a {
-  return StorageType.load(hash2(Typedef.rep(m), Typedef.rep(x)));
+forall col idx val . (col, idx):RValueIdxAccess(val) =>
+function ridx(c: col, i: idx) -> val {
+    return RValueIdxAccess.lookup((c, i));
 }
 
 // Concatenation
diff --git a/test/Cases.hs b/test/Cases.hs
index dc5f0472b..ce678b01f 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -73,7 +73,9 @@ spec =
       runTestForFile "121counter.solc" specFolder,
       runTestForFile "126nanoerc20.solc" specFolder,
       runTestForFile "127microerc20.solc" specFolder,
-      runTestForFile "128minierc20.solc" specFolder
+      runTestForFile "128minierc20.solc" specFolder,
+      runTestForFile "129arraystorage.solc" specFolder,
+      runTestForFile "130arrayfield.solc" specFolder
     ]
   where
     specFolder = "./test/examples/spec"
@@ -88,7 +90,8 @@ dispatches =
       runDispatchTest "Revert.solc",
       runDispatchTest "hashes.solc",
       runDispatchTest "empty.solc",
-      runDispatchTest "empty_no_constructor.solc"
+      runDispatchTest "empty_no_constructor.solc",
+      runDispatchTest "storage.solc"
     ]
   where
     runDispatchTest file = runTestForFileWith (emptyOption mempty) file "./test/examples/dispatch"
diff --git a/test/examples/dispatch/storage.json b/test/examples/dispatch/storage.json
new file mode 100644
index 000000000..e92a8bca7
--- /dev/null
+++ b/test/examples/dispatch/storage.json
@@ -0,0 +1,148 @@
+{
+  "storage": {
+    "bytecode": "_CODE",
+    "contract": "MemberRegistry",
+    "tests": [
+      {
+        "input": {
+          "comment": "constructor()",
+          "calldata": "",
+          "value": "0"
+        },
+        "kind": "constructor"
+      },
+      {
+        "input": {
+          "text-calldata": "numberOfMembers()(uint256) - initially 0",
+          "calldata": "a30e3fa9",
+          "value": "0"
+        },
+        "kind": "call",
+        "output": {
+          "returndata": "0000000000000000000000000000000000000000000000000000000000000000",
+          "status": "success"
+        }
+      },
+      {
+        "input": {
+          "text-calldata": "getMembers()(address[]) - initially empty",
+          "calldata": "9eab5253",
+          "value": "0"
+        },
+        "kind": "call",
+        "output": {
+          "returndata": "00000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000000",
+          "status": "success"
+        }
+      },
+      {
+        "input": {
+          "text-calldata": "addMember(0x1)",
+          "calldata": "ca6d56dc0000000000000000000000000000000000000000000000000000000000000001",
+          "value": "0"
+        },
+        "kind": "call",
+        "output": {
+          "returndata": "",
+          "status": "success"
+        }
+      },
+      {
+        "input": {
+          "text-calldata": "addMember(0x2)",
+          "calldata": "ca6d56dc0000000000000000000000000000000000000000000000000000000000000002",
+          "value": "0"
+        },
+        "kind": "call",
+        "output": {
+          "returndata": "",
+          "status": "success"
+        }
+      },
+      {
+        "input": {
+          "text-calldata": "addMember(0x3)",
+          "calldata": "ca6d56dc0000000000000000000000000000000000000000000000000000000000000003",
+          "value": "0"
+        },
+        "kind": "call",
+        "output": {
+          "returndata": "",
+          "status": "success"
+        }
+      },
+      {
+        "input": {
+          "text-calldata": "numberOfMembers()(uint256) - now 3",
+          "calldata": "a30e3fa9",
+          "value": "0"
+        },
+        "kind": "call",
+        "output": {
+          "returndata": "0000000000000000000000000000000000000000000000000000000000000003",
+          "status": "success"
+        }
+      },
+      {
+        "input": {
+          "text-calldata": "getMembers()(address[]) - [0x1, 0x2, 0x3]",
+          "calldata": "9eab5253",
+          "value": "0"
+        },
+        "kind": "call",
+        "output": {
+          "returndata": "00000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000003000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000003",
+          "status": "success"
+        }
+      },
+      {
+        "input": {
+          "text-calldata": "removeMember(0x2) - swap-pop, 0x3 moves to index 1",
+          "calldata": "0b1ca49a0000000000000000000000000000000000000000000000000000000000000002",
+          "value": "0"
+        },
+        "kind": "call",
+        "output": {
+          "returndata": "",
+          "status": "success"
+        }
+      },
+      {
+        "input": {
+          "text-calldata": "numberOfMembers()(uint256) - now 2",
+          "calldata": "a30e3fa9",
+          "value": "0"
+        },
+        "kind": "call",
+        "output": {
+          "returndata": "0000000000000000000000000000000000000000000000000000000000000002",
+          "status": "success"
+        }
+      },
+      {
+        "input": {
+          "text-calldata": "getMembers()(address[]) - [0x1, 0x3]",
+          "calldata": "9eab5253",
+          "value": "0"
+        },
+        "kind": "call",
+        "output": {
+          "returndata": "0000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000010000000000000000000000000000000000000000000000000000000000000003",
+          "status": "success"
+        }
+      },
+      {
+        "input": {
+          "text-calldata": "removeMember(0x9) - not in array, should revert with MemberNotFound()",
+          "calldata": "0b1ca49a0000000000000000000000000000000000000000000000000000000000000009",
+          "value": "0"
+        },
+        "kind": "call",
+        "output": {
+          "returndata": "deadbeef",
+          "status": "failure"
+        }
+      }
+    ]
+  }
+}
diff --git a/test/examples/dispatch/storage.solc b/test/examples/dispatch/storage.solc
new file mode 100644
index 000000000..83ada684e
--- /dev/null
+++ b/test/examples/dispatch/storage.solc
@@ -0,0 +1,56 @@
+import std.{*};
+import std.dispatch.{*};
+pragma no-patterson-condition ;
+pragma no-coverage-condition ;
+pragma no-bounded-variable-condition ;
+
+contract MemberRegistry {
+  // forge uses at least 1 storage slot
+  reserved : word;
+  members : array(address);
+
+  constructor() {}
+
+  function addMember(addr : address) -> () {
+    members.push(addr);
+  }
+
+  // MemberNotFound() selector
+  function removeMember(addr : address) -> () {
+    // foundIdx == length() acts as the "not found" sentinel.
+    let foundIdx : uint256 = members.length();
+    let i : uint256;
+    for (i = uint256(0); i < members.length(); i = i + uint256(1)) {
+      if (members[i] == addr) {
+        // NOTE: solcore has no `break`, so we keep scanning.
+        foundIdx = i;
+      }
+    }
+    require(foundIdx != members.length(), Error(0xdeadbeef));
+
+    // Shift subsequent elements down one slot to close the gap.
+    for (; foundIdx < members.length() - uint256(1); foundIdx = foundIdx + uint256(1)) {
+      members[foundIdx] = members[foundIdx + uint256(1)];
+    }
+    // Drop the (now-duplicated) last item and adjust the length.
+    members.pop();
+  }
+
+  function numberOfMembers() -> uint256 {
+    return members.length();
+  }
+
+  function getMembers() -> memory(DynArray(address)) {
+    let count : word = Typedef.rep(members.length());
+    let totalBytes : word = (count + 1) * 32;
+    let ptr : word = allocate_memory(totalBytes);
+    mstore(ptr, count);
+
+    let i : word;
+    for (i = 0; i < count; i = i + 1) {
+      let addr : address = members[uint256(i)];
+      mstore(ptr + 32 + i * 32, Typedef.rep(addr));
+    }
+    return Typedef.abs(ptr) : memory(DynArray(address));
+  }
+}
diff --git a/test/examples/spec/129arraystorage.solc b/test/examples/spec/129arraystorage.solc
new file mode 100644
index 000000000..eb27dcedd
--- /dev/null
+++ b/test/examples/spec/129arraystorage.solc
@@ -0,0 +1,24 @@
+// Exercises storage arrays (array(member)) modeled on storage mappings.
+import std.{*};
+pragma no-patterson-condition ;
+pragma no-coverage-condition ;
+pragma no-bounded-variable-condition ;
+
+contract ArrayStorage {
+  reserved : word; // forge uses at least 1 storage slot
+
+  function main() -> uint256 {
+    // A storage array sitting at a fixed slot. The slot itself stores the
+    // length; elements live at keccak256(slot) + i.
+    let arr : storage(array(uint256)) = storage(0x100);
+
+    // push appends and grows the length automatically.
+    Array.push(arr, uint256(42));
+    Array.push(arr, uint256(100));
+
+    // `arr[i]` syntax only desugars for contract fields, so use the
+    // explicit ridx helper for this local-variable array. ridx dispatches
+    // through RValueIdxAccess, which bounds-checks against Array.length.
+    return ridx(arr, uint256(0)) + ridx(arr, uint256(1));
+  }
+}
diff --git a/test/examples/spec/130arrayfield.solc b/test/examples/spec/130arrayfield.solc
new file mode 100644
index 000000000..913f4d71e
--- /dev/null
+++ b/test/examples/spec/130arrayfield.solc
@@ -0,0 +1,19 @@
+// Storage array as a contract field: `arr : array(uint256)`.
+import std.{*};
+pragma no-patterson-condition ;
+pragma no-coverage-condition ;
+pragma no-bounded-variable-condition ;
+
+contract ArrayField {
+  reserved : word; // forge uses at least 1 storage slot
+  arr : array(uint256);
+
+  function main() -> uint256 {
+    // push appends and grows the length automatically.
+    arr.push(uint256(42));
+    arr.push(uint256(100));
+
+    // arr[i] — bounds-checked indexed access.
+    return arr[uint256(0)] + arr[uint256(1)];
+  }
+}