You suggested an M2-like rule with path buts. Path bits increase witness overhead (i.e. not minimal, although more minimal than M3) and add bit-twiddling complexity which is undesirable. Also, your rule has 3x hashing overhead, which may exceed the efficiently computable property (unless you choose a fast hash function and replace “hashes” with “hashes relative to Keccek256 throughput”).
As you noted, in M3-like rules, a proof-of-exclusion requires a path to a descendant leaf to recover path bits. But such a leaf may not come from the access list and may have to be manually added to the witness. This adds witness bloat (breaking minimalness), and opens questions on how to make this unique (need more rules to get uniqueness, also undesirable).