From e94d9404f8a09da2e16a9767c78debaeb40f9625 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 27 May 2026 11:14:58 +0000
Subject: [PATCH 01/13] Add storage array support modeled on storage mapping

Adds an array(member, index) data type to std alongside mapping(member,
index), with parallel Typedef, StorageSize, CanStore, LValueIdxAccess
and RValueIdxAccess instances. Slot for arr[i] follows Solidity's
dynamic array layout: keccak256(p) + i. Also exports larr/rarr
helpers analogous to lidx/ridx.
---
 std/std.solc | 64 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 64 insertions(+)

diff --git a/std/std.solc b/std/std.solc
index fc53d7335..278478158 100644
--- a/std/std.solc
+++ b/std/std.solc
@@ -45,6 +45,7 @@ export {
   address(*),
   allocate_memory,
   and,
+  array(*),
   assert,
   byte(*),
   bytes,
@@ -72,6 +73,7 @@ export {
   hash2,
   keccak256_,
   keccakLit,
+  larr,
   le,
   lidx,
   loadBytesFromStorage,
@@ -87,6 +89,7 @@ export {
   not,
   or,
   out_of_bounds,
+  rarr,
   readStorage,
   returndata(*),
   revertLit,
@@ -760,6 +763,8 @@ forall t . instance returndata(t) : Typedef(word) {
 
 data mapping(member, index) = mapping(word) ;
 
+data array(member, index) = array(word) ;
+
 // --- Low-level memory ops
 
 function mload(a:word) -> word {
@@ -1704,6 +1709,26 @@ instance mapping(index, member):StorageSize {
     }
 }
 
+forall member index . instance array(member, index):Typedef(word) {
+    function rep(x:array(member, index)) -> word {
+        match x {
+            | array(y) => return y;
+        }
+    }
+    function abs(x:word) -> array(member, index) {
+        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 index .
+instance array(member, index):StorageSize {
+    function size(x:Proxy(array(member, index))) -> word {
+        return 1;
+    }
+}
+
 forall self memberRefType.
 class self:LVA(memberRefType) {
     function acc(x:self) -> memberRefType;
@@ -1804,6 +1829,19 @@ forall k v.
     }
 }
 
+forall v i.
+ instance storage(array(v,i)):CanStore(storage(array(v,i))) {
+    function store(l:storage(array(v,i)), r:storage(array(v,i))) -> () {
+      // StorageType.store(Typedef.rep(l), r);
+      unimplemented();
+    }
+    function load(l:storage(array(v,i))) -> storage(array(v,i)) {
+      // 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 +1969,22 @@ instance (storage(mapping(i,a)), i): RValueIdxAccess(a) {
   }
 }
 
+forall a i . i:Typedef(word) =>
+instance (storage(array(a,i)), i): LValueIdxAccess(storage(a)) {
+  function lookup(xi : (storage(array(a,i)), i)) -> storage(a) {
+    match(xi) {
+      | (x, i) => return storage(addWord(hash1(Typedef.rep(x)), Typedef.rep(i)));
+    }
+  }
+}
+
+forall a i . a:StorageType, i:Typedef(word) =>
+instance (storage(array(a,i)), i): RValueIdxAccess(a) {
+  function lookup(xi : (storage(array(a,i)), i)) -> a {
+    return readStorage(LValueIdxAccess.lookup(xi));
+  }
+}
+
 forall a. a:StorageType =>
 function readStorage(x:storage(a)) -> a {
   return StorageType.load(Typedef.rep(x));
@@ -1957,6 +2011,16 @@ function ridx( m: storage(mapping(i,a)), x:i) -> a {
   return StorageType.load(hash2(Typedef.rep(m), Typedef.rep(x)));
 }
 
+forall a i . i:Typedef(word) =>
+function larr( m: storage(array(a,i)), x:i) -> storage(a) {
+  return storage(addWord(hash1(Typedef.rep(m)), Typedef.rep(x)));
+}
+
+forall a i . i:Typedef(word), a:StorageType  =>
+function rarr( m: storage(array(a,i)), x:i) -> a {
+  return StorageType.load(addWord(hash1(Typedef.rep(m)), Typedef.rep(x)));
+}
+
 // Concatenation
 
 

From 53588cf960282cb10b4acae4ca79be9df2ff1c48 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 27 May 2026 11:25:38 +0000
Subject: [PATCH 02/13] Add storage array spec test

Adds 129arraystorage.solc which constructs a storage(array(uint256,
uint256)) at a fixed slot, writes two elements via Assign + larr, and
reads them back via rarr. Registered alongside the storage mapping
tests in test/Cases.hs.
---
 test/Cases.hs                           |  3 ++-
 test/examples/spec/129arraystorage.solc | 24 ++++++++++++++++++++++++
 2 files changed, 26 insertions(+), 1 deletion(-)
 create mode 100644 test/examples/spec/129arraystorage.solc

diff --git a/test/Cases.hs b/test/Cases.hs
index dc5f0472b..9907fe29c 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -73,7 +73,8 @@ 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
     ]
   where
     specFolder = "./test/examples/spec"
diff --git a/test/examples/spec/129arraystorage.solc b/test/examples/spec/129arraystorage.solc
new file mode 100644
index 000000000..383a3586c
--- /dev/null
+++ b/test/examples/spec/129arraystorage.solc
@@ -0,0 +1,24 @@
+// Exercises storage arrays (array(member, index)) 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
+    // (logical) length; elements live at keccak256(slot) + i.
+    let arr : storage(array(uint256, uint256)) = storage(0x100);
+
+    // arr[0] = 42; arr[1] = 100
+    Assign.assign(larr(arr, uint256(0)), uint256(42));
+    Assign.assign(larr(arr, uint256(1)), uint256(100));
+
+    // arr[0] + arr[1]
+    let a0 : uint256 = rarr(arr, uint256(0));
+    let a1 : uint256 = rarr(arr, uint256(1));
+    return Num.add(a0, a1);
+  }
+}

From c178c01554c4a11de54317aacbde6ed0de64af1a Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 27 May 2026 11:29:12 +0000
Subject: [PATCH 03/13] Simplify array to single type parameter; add
 contract-field test

Drops the index type parameter from array since the index is always a
Typedef(word) value, leaving the element type as the sole parameter
(matching Solidity's T[] surface form). Updates the existing storage
test and adds a new test that defines a contract field
`arr : array(uint256)` and accesses it via larr/rarr.
---
 std/std.solc                            | 34 ++++++++++++-------------
 test/Cases.hs                           |  3 ++-
 test/examples/spec/129arraystorage.solc |  4 +--
 test/examples/spec/130arrayfield.solc   | 22 ++++++++++++++++
 4 files changed, 43 insertions(+), 20 deletions(-)
 create mode 100644 test/examples/spec/130arrayfield.solc

diff --git a/std/std.solc b/std/std.solc
index 278478158..e711477e7 100644
--- a/std/std.solc
+++ b/std/std.solc
@@ -763,7 +763,7 @@ forall t . instance returndata(t) : Typedef(word) {
 
 data mapping(member, index) = mapping(word) ;
 
-data array(member, index) = array(word) ;
+data array(member) = array(word) ;
 
 // --- Low-level memory ops
 
@@ -1709,22 +1709,22 @@ instance mapping(index, member):StorageSize {
     }
 }
 
-forall member index . instance array(member, index):Typedef(word) {
-    function rep(x:array(member, index)) -> word {
+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, index) {
+    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 index .
-instance array(member, index):StorageSize {
-    function size(x:Proxy(array(member, index))) -> word {
+forall member .
+instance array(member):StorageSize {
+    function size(x:Proxy(array(member))) -> word {
         return 1;
     }
 }
@@ -1829,13 +1829,13 @@ forall k v.
     }
 }
 
-forall v i.
- instance storage(array(v,i)):CanStore(storage(array(v,i))) {
-    function store(l:storage(array(v,i)), r:storage(array(v,i))) -> () {
+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,i))) -> storage(array(v,i)) {
+    function load(l:storage(array(v))) -> storage(array(v)) {
       // return StorageType.load(Typedef.rep(l));
       unimplemented();
       return l;
@@ -1970,8 +1970,8 @@ instance (storage(mapping(i,a)), i): RValueIdxAccess(a) {
 }
 
 forall a i . i:Typedef(word) =>
-instance (storage(array(a,i)), i): LValueIdxAccess(storage(a)) {
-  function lookup(xi : (storage(array(a,i)), i)) -> storage(a) {
+instance (storage(array(a)), i): LValueIdxAccess(storage(a)) {
+  function lookup(xi : (storage(array(a)), i)) -> storage(a) {
     match(xi) {
       | (x, i) => return storage(addWord(hash1(Typedef.rep(x)), Typedef.rep(i)));
     }
@@ -1979,8 +1979,8 @@ instance (storage(array(a,i)), i): LValueIdxAccess(storage(a)) {
 }
 
 forall a i . a:StorageType, i:Typedef(word) =>
-instance (storage(array(a,i)), i): RValueIdxAccess(a) {
-  function lookup(xi : (storage(array(a,i)), i)) -> a {
+instance (storage(array(a)), i): RValueIdxAccess(a) {
+  function lookup(xi : (storage(array(a)), i)) -> a {
     return readStorage(LValueIdxAccess.lookup(xi));
   }
 }
@@ -2012,12 +2012,12 @@ function ridx( m: storage(mapping(i,a)), x:i) -> a {
 }
 
 forall a i . i:Typedef(word) =>
-function larr( m: storage(array(a,i)), x:i) -> storage(a) {
+function larr( m: storage(array(a)), x:i) -> storage(a) {
   return storage(addWord(hash1(Typedef.rep(m)), Typedef.rep(x)));
 }
 
 forall a i . i:Typedef(word), a:StorageType  =>
-function rarr( m: storage(array(a,i)), x:i) -> a {
+function rarr( m: storage(array(a)), x:i) -> a {
   return StorageType.load(addWord(hash1(Typedef.rep(m)), Typedef.rep(x)));
 }
 
diff --git a/test/Cases.hs b/test/Cases.hs
index 9907fe29c..0773e9189 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -74,7 +74,8 @@ spec =
       runTestForFile "126nanoerc20.solc" specFolder,
       runTestForFile "127microerc20.solc" specFolder,
       runTestForFile "128minierc20.solc" specFolder,
-      runTestForFile "129arraystorage.solc" specFolder
+      runTestForFile "129arraystorage.solc" specFolder,
+      runTestForFile "130arrayfield.solc" specFolder
     ]
   where
     specFolder = "./test/examples/spec"
diff --git a/test/examples/spec/129arraystorage.solc b/test/examples/spec/129arraystorage.solc
index 383a3586c..7cca98034 100644
--- a/test/examples/spec/129arraystorage.solc
+++ b/test/examples/spec/129arraystorage.solc
@@ -1,4 +1,4 @@
-// Exercises storage arrays (array(member, index)) modeled on storage mappings.
+// Exercises storage arrays (array(member)) modeled on storage mappings.
 import std.{*};
 pragma no-patterson-condition ;
 pragma no-coverage-condition ;
@@ -10,7 +10,7 @@ contract ArrayStorage {
   function main() -> uint256 {
     // A storage array sitting at a fixed slot. The slot itself stores the
     // (logical) length; elements live at keccak256(slot) + i.
-    let arr : storage(array(uint256, uint256)) = storage(0x100);
+    let arr : storage(array(uint256)) = storage(0x100);
 
     // arr[0] = 42; arr[1] = 100
     Assign.assign(larr(arr, uint256(0)), uint256(42));
diff --git a/test/examples/spec/130arrayfield.solc b/test/examples/spec/130arrayfield.solc
new file mode 100644
index 000000000..90d351cfc
--- /dev/null
+++ b/test/examples/spec/130arrayfield.solc
@@ -0,0 +1,22 @@
+// 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 {
+    // `arr` desugars to RVA.acc(...) which, via the
+    // storage(array(v)):CanStore(storage(array(v))) instance,
+    // yields a `storage(array(uint256))` reference to the field.
+    Assign.assign(larr(arr, uint256(0)), uint256(42));
+    Assign.assign(larr(arr, uint256(1)), uint256(100));
+
+    let a0 : uint256 = rarr(arr, uint256(0));
+    let a1 : uint256 = rarr(arr, uint256(1));
+    return Num.add(a0, a1);
+  }
+}

From ba9db953df113c013d3b839954fd96538846f99a Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 2 Jun 2026 18:53:09 +0000
Subject: [PATCH 04/13] Use + operator instead of addWord in array storage
 helpers

---
 std/std.solc | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/std/std.solc b/std/std.solc
index e711477e7..6b8306443 100644
--- a/std/std.solc
+++ b/std/std.solc
@@ -1973,7 +1973,7 @@ 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) => return storage(addWord(hash1(Typedef.rep(x)), Typedef.rep(i)));
+      | (x, i) => return storage(hash1(Typedef.rep(x)) + Typedef.rep(i));
     }
   }
 }
@@ -2013,12 +2013,12 @@ function ridx( m: storage(mapping(i,a)), x:i) -> a {
 
 forall a i . i:Typedef(word) =>
 function larr( m: storage(array(a)), x:i) -> storage(a) {
-  return storage(addWord(hash1(Typedef.rep(m)), Typedef.rep(x)));
+  return storage(hash1(Typedef.rep(m)) + Typedef.rep(x));
 }
 
 forall a i . i:Typedef(word), a:StorageType  =>
 function rarr( m: storage(array(a)), x:i) -> a {
-  return StorageType.load(addWord(hash1(Typedef.rep(m)), Typedef.rep(x)));
+  return StorageType.load(hash1(Typedef.rep(m)) + Typedef.rep(x));
 }
 
 // Concatenation

From 020accd176336490a5251390dc604ea4360e692f Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 2 Jun 2026 18:55:09 +0000
Subject: [PATCH 05/13] Use + operator instead of Num.add in array storage
 tests

---
 test/examples/spec/129arraystorage.solc | 2 +-
 test/examples/spec/130arrayfield.solc   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/test/examples/spec/129arraystorage.solc b/test/examples/spec/129arraystorage.solc
index 7cca98034..332b7a06f 100644
--- a/test/examples/spec/129arraystorage.solc
+++ b/test/examples/spec/129arraystorage.solc
@@ -19,6 +19,6 @@ contract ArrayStorage {
     // arr[0] + arr[1]
     let a0 : uint256 = rarr(arr, uint256(0));
     let a1 : uint256 = rarr(arr, uint256(1));
-    return Num.add(a0, a1);
+    return a0 + a1;
   }
 }
diff --git a/test/examples/spec/130arrayfield.solc b/test/examples/spec/130arrayfield.solc
index 90d351cfc..771de68c1 100644
--- a/test/examples/spec/130arrayfield.solc
+++ b/test/examples/spec/130arrayfield.solc
@@ -17,6 +17,6 @@ contract ArrayField {
 
     let a0 : uint256 = rarr(arr, uint256(0));
     let a1 : uint256 = rarr(arr, uint256(1));
-    return Num.add(a0, a1);
+    return a0 + a1;
   }
 }

From 821695a5a36802de8553473d08351401e36d2da5 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 9 Jun 2026 13:10:18 +0000
Subject: [PATCH 06/13] Add dispatch test for storage array of addresses

Adds test/examples/dispatch/storage.{solc,json} which exercises a
MemberRegistry contract with a storage array of addresses:
- addMember(address) appends to the array
- removeMember(address) performs swap-pop, reverting if not found
- numberOfMembers() returns the count
- getMembers() returns the full address[]

The contract maintains a separate memberCount alongside the storage
array. It also defines an ABIEncode/ABIAttribs instance for
memory(DynArray(t)) (t:Typedef(word)) so that getMembers can return a
true dynamic array via the dispatch ABI encoder.
---
 test/Cases.hs                       |   3 +-
 test/examples/dispatch/storage.json | 148 ++++++++++++++++++++++++++++
 test/examples/dispatch/storage.solc |  89 +++++++++++++++++
 3 files changed, 239 insertions(+), 1 deletion(-)
 create mode 100644 test/examples/dispatch/storage.json
 create mode 100644 test/examples/dispatch/storage.solc

diff --git a/test/Cases.hs b/test/Cases.hs
index 0773e9189..ce678b01f 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -90,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..0ec16abdf
--- /dev/null
+++ b/test/examples/dispatch/storage.solc
@@ -0,0 +1,89 @@
+import std.{*};
+import std.dispatch.{*};
+pragma no-patterson-condition ;
+pragma no-coverage-condition ;
+pragma no-bounded-variable-condition ;
+
+// ABI encoding for memory(DynArray(t)) where each element fits in a word.
+// We assume the memory layout has length at srcPtr and elements at srcPtr+32,
+// srcPtr+64, ... — i.e. the same shape as the on-the-wire tail of `t[]`.
+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;
+    }
+}
+
+forall t . instance memory(DynArray(t)):ABIAttribs {
+    function headSize(ty : Proxy(memory(DynArray(t)))) -> word { return 32; }
+    function isStatic(ty : Proxy(memory(DynArray(t)))) -> bool { return false; }
+}
+
+contract MemberRegistry {
+  // forge uses at least 1 storage slot
+  reserved : word;
+  memberCount : uint256;
+  members : array(address);
+
+  constructor() {}
+
+  function addMember(addr : address) -> () {
+    let i : uint256 = memberCount;
+    Assign.assign(larr(members, i), addr);
+    memberCount = memberCount + uint256(1);
+  }
+
+  // MemberNotFound() selector
+  function removeMember(addr : address) -> () {
+    let count : uint256 = memberCount;
+    let found : bool = false;
+    let foundIdx : uint256 = uint256(0);
+    let i : uint256;
+    for (i = uint256(0); i < count; i = i + uint256(1)) {
+      if (rarr(members, i) == addr) {
+        foundIdx = i;
+        found = true;
+      }
+    }
+    require(found, Error(0xdeadbeef));
+
+    let lastIdx : uint256 = count - uint256(1);
+    let last : address = rarr(members, lastIdx);
+    Assign.assign(larr(members, foundIdx), last);
+    memberCount = lastIdx;
+  }
+
+  function numberOfMembers() -> uint256 {
+    return memberCount;
+  }
+
+  function getMembers() -> memory(DynArray(address)) {
+    let count : word = Typedef.rep(memberCount);
+    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 = rarr(members, uint256(i));
+      let addrWord : word = Typedef.rep(addr);
+      mstore(ptr + 32 + i * 32, addrWord);
+    }
+    return Typedef.abs(ptr) : memory(DynArray(address));
+  }
+}

From ee2c728bf65acd6872fa27cc060dc153e48a2ae0 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 9 Jun 2026 13:12:27 +0000
Subject: [PATCH 07/13] Move memory(DynArray(t)) ABIEncode/ABIAttribs from test
 to std

---
 std/std.solc                        | 30 +++++++++++++++++++++++++++++
 test/examples/dispatch/storage.solc | 30 -----------------------------
 2 files changed, 30 insertions(+), 30 deletions(-)

diff --git a/std/std.solc b/std/std.solc
index 6b8306443..baa9d5869 100644
--- a/std/std.solc
+++ b/std/std.solc
@@ -1227,6 +1227,36 @@ 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.
+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;
+    }
+}
+
+forall t . instance memory(DynArray(t)):ABIAttribs {
+    function headSize(ty : Proxy(memory(DynArray(t)))) -> word { return 32; }
+    function isStatic(ty : Proxy(memory(DynArray(t)))) -> bool { return false; }
+}
+
 instance ():ABIEncode {
     // a unit256 is written directly into the head
     function encodeInto(x:(), basePtr:word, offset:word, tail:word) -> word {
diff --git a/test/examples/dispatch/storage.solc b/test/examples/dispatch/storage.solc
index 0ec16abdf..4fc97e0d4 100644
--- a/test/examples/dispatch/storage.solc
+++ b/test/examples/dispatch/storage.solc
@@ -4,36 +4,6 @@ pragma no-patterson-condition ;
 pragma no-coverage-condition ;
 pragma no-bounded-variable-condition ;
 
-// ABI encoding for memory(DynArray(t)) where each element fits in a word.
-// We assume the memory layout has length at srcPtr and elements at srcPtr+32,
-// srcPtr+64, ... — i.e. the same shape as the on-the-wire tail of `t[]`.
-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;
-    }
-}
-
-forall t . instance memory(DynArray(t)):ABIAttribs {
-    function headSize(ty : Proxy(memory(DynArray(t)))) -> word { return 32; }
-    function isStatic(ty : Proxy(memory(DynArray(t)))) -> bool { return false; }
-}
-
 contract MemberRegistry {
   // forge uses at least 1 storage slot
   reserved : word;

From becbf34d201fb9a7a21840b9d8ad4d9ccd2825e8 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 9 Jun 2026 13:15:37 +0000
Subject: [PATCH 08/13] Track array length in the array slot via Array
 typeclass
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Adds an Array typeclass to std with length/setLength methods and an
instance for storage(array(t)) that reads/writes the slot itself (Solidity
storage layout: length at slot p, elements at keccak256(p) + i).

The dispatch test no longer carries a separate memberCount field — it
calls Array.length(members) and Array.setLength(members, n) instead.
---
 std/std.solc                        | 18 ++++++++++++++++++
 test/examples/dispatch/storage.solc | 13 ++++++-------
 2 files changed, 24 insertions(+), 7 deletions(-)

diff --git a/std/std.solc b/std/std.solc
index baa9d5869..9ba1f668a 100644
--- a/std/std.solc
+++ b/std/std.solc
@@ -8,6 +8,7 @@ export {
   ABIEncode,
   ABITuple(*),
   Add,
+  Array,
   Assign,
   Bounded,
   CalldataWordReader(*),
@@ -1759,6 +1760,23 @@ instance array(member):StorageSize {
     }
 }
 
+// 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) -> ();
+}
+
+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));
+    }
+}
+
 forall self memberRefType.
 class self:LVA(memberRefType) {
     function acc(x:self) -> memberRefType;
diff --git a/test/examples/dispatch/storage.solc b/test/examples/dispatch/storage.solc
index 4fc97e0d4..fef6c0190 100644
--- a/test/examples/dispatch/storage.solc
+++ b/test/examples/dispatch/storage.solc
@@ -7,20 +7,19 @@ pragma no-bounded-variable-condition ;
 contract MemberRegistry {
   // forge uses at least 1 storage slot
   reserved : word;
-  memberCount : uint256;
   members : array(address);
 
   constructor() {}
 
   function addMember(addr : address) -> () {
-    let i : uint256 = memberCount;
+    let i : uint256 = Array.length(members);
     Assign.assign(larr(members, i), addr);
-    memberCount = memberCount + uint256(1);
+    Array.setLength(members, i + uint256(1));
   }
 
   // MemberNotFound() selector
   function removeMember(addr : address) -> () {
-    let count : uint256 = memberCount;
+    let count : uint256 = Array.length(members);
     let found : bool = false;
     let foundIdx : uint256 = uint256(0);
     let i : uint256;
@@ -35,15 +34,15 @@ contract MemberRegistry {
     let lastIdx : uint256 = count - uint256(1);
     let last : address = rarr(members, lastIdx);
     Assign.assign(larr(members, foundIdx), last);
-    memberCount = lastIdx;
+    Array.setLength(members, lastIdx);
   }
 
   function numberOfMembers() -> uint256 {
-    return memberCount;
+    return Array.length(members);
   }
 
   function getMembers() -> memory(DynArray(address)) {
-    let count : word = Typedef.rep(memberCount);
+    let count : word = Typedef.rep(Array.length(members));
     let totalBytes : word = (count + 1) * 32;
     let ptr : word = allocate_memory(totalBytes);
     mstore(ptr, count);

From a27ce0a6046fb16b111aba4af0c20890d69aeefc Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 9 Jun 2026 13:34:36 +0000
Subject: [PATCH 09/13] Rework storage arrays: push/pop, bounded arr[i], UFCS
 method calls

- Array typeclass gains push/pop methods (with element type as a class
  parameter); push grows the length, pop shrinks it (and reverts on empty).
- Array bounds-check: LValueIdxAccess/RValueIdxAccess on storage(array(a))
  now consult Array.length and revert via out_of_bounds when i >= length.
- lidx/ridx become generic typeclass wrappers (LValueIdxAccess/
  RValueIdxAccess), so arr[i] works for both mappings and arrays via the
  shared FieldAccess desugaring; larr/rarr are dropped.
- NameResolution learns a small UFCS rule: when the receiver of a
  method-style call resolves to a contract field (`field.method(args)`)
  and no class is otherwise selected, search the class env for a
  uniquely-named method and rewrite to `Class.method(field, args)`. This
  enables `members.push(addr)`, `members.length()`, `members.pop()`.
- Tests updated accordingly: dispatch/storage.solc no longer carries a
  separate memberCount; spec/129arraystorage and spec/130arrayfield use
  push and the bounds-checked accessors.
---
 src/Solcore/Frontend/Syntax/NameResolution.hs | 33 +++++++++++
 std/std.solc                                  | 59 +++++++++++--------
 test/examples/dispatch/storage.solc           | 22 +++----
 test/examples/spec/129arraystorage.solc       | 16 ++---
 test/examples/spec/130arrayfield.solc         | 13 ++--
 5 files changed, 89 insertions(+), 54 deletions(-)

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 9ba1f668a..0b82f51cb 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;
+pragma no-coverage-condition ABIDecode, MemoryType, Array;
 
 export {
   ABIAttribs,
@@ -74,7 +74,6 @@ export {
   hash2,
   keccak256_,
   keccakLit,
-  larr,
   le,
   lidx,
   loadBytesFromStorage,
@@ -90,7 +89,6 @@ export {
   not,
   or,
   out_of_bounds,
-  rarr,
   readStorage,
   returndata(*),
   revertLit,
@@ -1762,19 +1760,32 @@ instance array(member):StorageSize {
 
 // 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 {
+forall self elem . class self:Array(elem) {
     function length(arr:self) -> uint256;
     function setLength(arr:self, n:uint256) -> ();
+    function push(arr:self, val:elem) -> ();
+    function pop(arr:self) -> ();
 }
 
-forall t .
-instance storage(array(t)):Array {
+forall t . t:StorageType =>
+instance storage(array(t)):Array(t) {
     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 push(arr:storage(array(t)), val:t) -> () {
+        let n : uint256 = Array.length(arr);
+        let slot : word = hash1(Typedef.rep(arr)) + Typedef.rep(n);
+        StorageType.store(slot, val);
+        Array.setLength(arr, n + uint256(1));
+    }
+    function pop(arr:storage(array(t))) -> () {
+        let n : uint256 = Array.length(arr);
+        if (n == uint256(0)) { out_of_bounds(); }
+        Array.setLength(arr, n - uint256(1));
+    }
 }
 
 forall self memberRefType.
@@ -2017,11 +2028,15 @@ instance (storage(mapping(i,a)), i): RValueIdxAccess(a) {
   }
 }
 
-forall a i . i:Typedef(word) =>
+forall a i . a:StorageType, i:Typedef(word) =>
 instance (storage(array(a)), i): LValueIdxAccess(storage(a)) {
   function lookup(xi : (storage(array(a)), i)) -> storage(a) {
     match(xi) {
-      | (x, i) => return storage(hash1(Typedef.rep(x)) + Typedef.rep(i));
+      | (x, i) =>
+          let idx : word = Typedef.rep(i);
+          let len : uint256 = Array.length(x);
+          if (idx >= Typedef.rep(len)) { out_of_bounds(); }
+          return storage(hash1(Typedef.rep(x)) + idx);
     }
   }
 }
@@ -2049,24 +2064,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)));
-}
-
-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 a i . i:Typedef(word) =>
-function larr( m: storage(array(a)), x:i) -> storage(a) {
-  return storage(hash1(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 a i . i:Typedef(word), a:StorageType  =>
-function rarr( m: storage(array(a)), x:i) -> a {
-  return StorageType.load(hash1(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/examples/dispatch/storage.solc b/test/examples/dispatch/storage.solc
index fef6c0190..4c01feee8 100644
--- a/test/examples/dispatch/storage.solc
+++ b/test/examples/dispatch/storage.solc
@@ -12,19 +12,17 @@ contract MemberRegistry {
   constructor() {}
 
   function addMember(addr : address) -> () {
-    let i : uint256 = Array.length(members);
-    Assign.assign(larr(members, i), addr);
-    Array.setLength(members, i + uint256(1));
+    members.push(addr);
   }
 
   // MemberNotFound() selector
   function removeMember(addr : address) -> () {
-    let count : uint256 = Array.length(members);
+    let count : uint256 = members.length();
     let found : bool = false;
     let foundIdx : uint256 = uint256(0);
     let i : uint256;
     for (i = uint256(0); i < count; i = i + uint256(1)) {
-      if (rarr(members, i) == addr) {
+      if (members[i] == addr) {
         foundIdx = i;
         found = true;
       }
@@ -32,26 +30,24 @@ contract MemberRegistry {
     require(found, Error(0xdeadbeef));
 
     let lastIdx : uint256 = count - uint256(1);
-    let last : address = rarr(members, lastIdx);
-    Assign.assign(larr(members, foundIdx), last);
-    Array.setLength(members, lastIdx);
+    members[foundIdx] = members[lastIdx];
+    members.pop();
   }
 
   function numberOfMembers() -> uint256 {
-    return Array.length(members);
+    return members.length();
   }
 
   function getMembers() -> memory(DynArray(address)) {
-    let count : word = Typedef.rep(Array.length(members));
+    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 = rarr(members, uint256(i));
-      let addrWord : word = Typedef.rep(addr);
-      mstore(ptr + 32 + i * 32, addrWord);
+      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
index 332b7a06f..eb27dcedd 100644
--- a/test/examples/spec/129arraystorage.solc
+++ b/test/examples/spec/129arraystorage.solc
@@ -9,16 +9,16 @@ contract ArrayStorage {
 
   function main() -> uint256 {
     // A storage array sitting at a fixed slot. The slot itself stores the
-    // (logical) length; elements live at keccak256(slot) + i.
+    // length; elements live at keccak256(slot) + i.
     let arr : storage(array(uint256)) = storage(0x100);
 
-    // arr[0] = 42; arr[1] = 100
-    Assign.assign(larr(arr, uint256(0)), uint256(42));
-    Assign.assign(larr(arr, uint256(1)), uint256(100));
+    // push appends and grows the length automatically.
+    Array.push(arr, uint256(42));
+    Array.push(arr, uint256(100));
 
-    // arr[0] + arr[1]
-    let a0 : uint256 = rarr(arr, uint256(0));
-    let a1 : uint256 = rarr(arr, uint256(1));
-    return a0 + a1;
+    // `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
index 771de68c1..913f4d71e 100644
--- a/test/examples/spec/130arrayfield.solc
+++ b/test/examples/spec/130arrayfield.solc
@@ -9,14 +9,11 @@ contract ArrayField {
   arr : array(uint256);
 
   function main() -> uint256 {
-    // `arr` desugars to RVA.acc(...) which, via the
-    // storage(array(v)):CanStore(storage(array(v))) instance,
-    // yields a `storage(array(uint256))` reference to the field.
-    Assign.assign(larr(arr, uint256(0)), uint256(42));
-    Assign.assign(larr(arr, uint256(1)), uint256(100));
+    // push appends and grows the length automatically.
+    arr.push(uint256(42));
+    arr.push(uint256(100));
 
-    let a0 : uint256 = rarr(arr, uint256(0));
-    let a1 : uint256 = rarr(arr, uint256(1));
-    return a0 + a1;
+    // arr[i] — bounds-checked indexed access.
+    return arr[uint256(0)] + arr[uint256(1)];
   }
 }

From d15c1cc5b9c20753e9047745d65a5abfb1b680d0 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 9 Jun 2026 13:36:32 +0000
Subject: [PATCH 10/13] Drop redundant memory(DynArray(t)):ABIAttribs instance

memory(ty):ABIAttribs (for any ty:ABIAttribs) + DynArray(t):ABIAttribs
already derive it. Keep only the ABIEncode instance, which has no
generic alternative (the commented-out memory(ty):ABIEncode based on
MemoryType still fails patterson/coverage).
---
 std/std.solc | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/std/std.solc b/std/std.solc
index 0b82f51cb..0f928f23d 100644
--- a/std/std.solc
+++ b/std/std.solc
@@ -1229,6 +1229,8 @@ 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 {
@@ -1251,11 +1253,6 @@ instance memory(DynArray(t)):ABIEncode {
     }
 }
 
-forall t . instance memory(DynArray(t)):ABIAttribs {
-    function headSize(ty : Proxy(memory(DynArray(t)))) -> word { return 32; }
-    function isStatic(ty : Proxy(memory(DynArray(t)))) -> bool { return false; }
-}
-
 instance ():ABIEncode {
     // a unit256 is written directly into the head
     function encodeInto(x:(), basePtr:word, offset:word, tail:word) -> word {

From 26689de84bb6689cdc07e631d322dd9840398eab Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 9 Jun 2026 13:44:45 +0000
Subject: [PATCH 11/13] Rewrite removeMember to use sentinel + shift-down
 pattern

Switches removeMember from swap-pop to the user-specified pattern:
foundIdx starts at length() as a not-found sentinel, the scan keeps
going past the match (solcore has no break), then subsequent elements
are shifted one slot down to close the gap and pop() drops the
duplicated last item. Preserves order of remaining members.
---
 test/examples/dispatch/storage.solc | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/test/examples/dispatch/storage.solc b/test/examples/dispatch/storage.solc
index 4c01feee8..83ada684e 100644
--- a/test/examples/dispatch/storage.solc
+++ b/test/examples/dispatch/storage.solc
@@ -17,20 +17,22 @@ contract MemberRegistry {
 
   // MemberNotFound() selector
   function removeMember(addr : address) -> () {
-    let count : uint256 = members.length();
-    let found : bool = false;
-    let foundIdx : uint256 = uint256(0);
+    // foundIdx == length() acts as the "not found" sentinel.
+    let foundIdx : uint256 = members.length();
     let i : uint256;
-    for (i = uint256(0); i < count; i = i + uint256(1)) {
+    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;
-        found = true;
       }
     }
-    require(found, Error(0xdeadbeef));
+    require(foundIdx != members.length(), Error(0xdeadbeef));
 
-    let lastIdx : uint256 = count - uint256(1);
-    members[foundIdx] = members[lastIdx];
+    // 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();
   }
 

From c7ac5d0ca7890041fe7325aea632251cd3b1783a Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 10 Jun 2026 10:45:20 +0000
Subject: [PATCH 12/13] Inline Array.push/pop bodies and array bounds-check

The previous Array.push/pop bodies dispatched recursively through
Array.length/Array.setLength on the same instance, which the specialiser
appears to have trouble pinning down for the storage(array(t)):Array(t)
MPTC instance (it produced 'no resolution found for StorageType.store :
word -> array(address) -> ()'). Inlining the slot/length arithmetic with
sload_/sstore_/StorageType.store directly avoids the recursive class
dispatch entirely. Same inlining for the LValueIdxAccess bounds check
(also drops its previously redundant a:StorageType constraint).
---
 std/std.solc | 28 +++++++++++++++++-----------
 1 file changed, 17 insertions(+), 11 deletions(-)

diff --git a/std/std.solc b/std/std.solc
index 0f928f23d..eda45a80c 100644
--- a/std/std.solc
+++ b/std/std.solc
@@ -1772,16 +1772,20 @@ instance storage(array(t)):Array(t) {
     function setLength(arr:storage(array(t)), n:uint256) -> () {
         sstore_(Typedef.rep(arr), Typedef.rep(n));
     }
+    // Inlined to avoid re-dispatching through Array.length / Array.setLength
+    // inside the same instance (the specialiser otherwise has to recursively
+    // resolve `storage(array(t)):Array(t)` against its own body).
     function push(arr:storage(array(t)), val:t) -> () {
-        let n : uint256 = Array.length(arr);
-        let slot : word = hash1(Typedef.rep(arr)) + Typedef.rep(n);
-        StorageType.store(slot, val);
-        Array.setLength(arr, n + uint256(1));
+        let slot : word = Typedef.rep(arr);
+        let n : word = sload_(slot);
+        StorageType.store(hash1(slot) + n, val);
+        sstore_(slot, n + 1);
     }
     function pop(arr:storage(array(t))) -> () {
-        let n : uint256 = Array.length(arr);
-        if (n == uint256(0)) { out_of_bounds(); }
-        Array.setLength(arr, n - uint256(1));
+        let slot : word = Typedef.rep(arr);
+        let n : word = sload_(slot);
+        if (n == 0) { out_of_bounds(); }
+        sstore_(slot, n - 1);
     }
 }
 
@@ -2025,15 +2029,17 @@ instance (storage(mapping(i,a)), i): RValueIdxAccess(a) {
   }
 }
 
-forall a i . a:StorageType, i:Typedef(word) =>
+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);
-          let len : uint256 = Array.length(x);
-          if (idx >= Typedef.rep(len)) { out_of_bounds(); }
-          return storage(hash1(Typedef.rep(x)) + idx);
+          // 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);
     }
   }
 }

From 4a0d3a31ff083a0e107461f7633ac47f05d2fcda Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 10 Jun 2026 11:01:17 +0000
Subject: [PATCH 13/13] Split Array into Array (length/setLength/pop) +
 ArrayPush(elem) (push)

Restructure to avoid MPTC inference issues on length/setLength/pop,
which never mention elem in their signatures. push, which actually
binds the element type via val:elem, lives in its own MPTC class
ArrayPush(elem). UFCS still finds each method via the class-method
search, so members.push(addr), members.length(), members.pop() all
keep working unchanged in the tests.
---
 std/std.solc | 38 +++++++++++++++++++++++---------------
 1 file changed, 23 insertions(+), 15 deletions(-)

diff --git a/std/std.solc b/std/std.solc
index eda45a80c..d633f4968 100644
--- a/std/std.solc
+++ b/std/std.solc
@@ -1,5 +1,5 @@
-pragma no-patterson-condition ABIEncode, Num, Array;
-pragma no-coverage-condition ABIDecode, MemoryType, Array;
+pragma no-patterson-condition ABIEncode, Num, Array, ArrayPush;
+pragma no-coverage-condition ABIDecode, MemoryType, Array, ArrayPush;
 
 export {
   ABIAttribs,
@@ -9,6 +9,7 @@ export {
   ABITuple(*),
   Add,
   Array,
+  ArrayPush,
   Assign,
   Bounded,
   CalldataWordReader(*),
@@ -1757,30 +1758,27 @@ instance array(member):StorageSize {
 
 // Dynamic storage arrays carry their length at the slot itself (matching the
 // Solidity convention) while elements live at keccak256(slot) + i.
-forall self elem . class self:Array(elem) {
+forall self . class self:Array {
     function length(arr:self) -> uint256;
     function setLength(arr:self, n:uint256) -> ();
-    function push(arr:self, val:elem) -> ();
     function pop(arr:self) -> ();
 }
 
-forall t . t:StorageType =>
-instance storage(array(t)):Array(t) {
+// 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));
     }
-    // Inlined to avoid re-dispatching through Array.length / Array.setLength
-    // inside the same instance (the specialiser otherwise has to recursively
-    // resolve `storage(array(t)):Array(t)` against its own body).
-    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);
-    }
     function pop(arr:storage(array(t))) -> () {
         let slot : word = Typedef.rep(arr);
         let n : word = sload_(slot);
@@ -1789,6 +1787,16 @@ instance storage(array(t)):Array(t) {
     }
 }
 
+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;