Framing verification issue on mutable array in a typical ArrayList Insert operation

Consider the following simple ArrayList implementation:

class ArrayListImpl<T(0)> {
    var xs: array<T>
    var n: nat

    predicate Valid() reads this
    { 0 <= n <= xs.Length }

    constructor(cap:nat) 
      requires cap > 0
      ensures Valid()
    {
      xs := new T[cap];
      n := 0;
    }

    function Size(): nat reads this
      requires Valid()
    { n }

    function Get(i:nat): T
        reads this, {xs}
        requires Valid()
        requires 0 <= i < Size() 
    { xs[i] }

  method Insert(i:nat, x:T)
      modifies this, {xs}

      requires 0 <= n <= xs.Length
      requires 0 <= i <= Size()
      requires !(n == xs.Length)

      ensures  0 <= n <= xs.Length
      ensures  Size() == old(Size()) + 1
      ensures  forall j :: 0 <= j < i           ==> Get(j) == old(Get(j))   
      ensures  forall j :: i < j <= old(Size()) ==> Get(j) == old(Get(j-1))
      ensures  Get(i) == x                                                   
    {
      var k := n;
      while k > i
        invariant 0 <= n <= xs.Length && n == old(n)
        invariant i <= k <= n < xs.Length    
        invariant forall j :: 0 <= j < i ==> xs[j] == old(xs[j])   
        invariant forall j :: k < j <= n ==> xs[j] == old(xs[j-1])  
        invariant forall j :: i <= j < k ==> xs[j] == old(xs[j])      
        invariant xs[i] == old(xs[i]) 
        decreases k - i
      {
        xs[k] := xs[k-1];  // update issue
        k := k - 1;
      }
      xs[k] := x;   // update issue
      n := n + 1;
    }
}

Everything verifies except that, in the insert operation, array xs cant be updated:

assignment might update an array element not in the enclosing context's modifies clause

As per my understanding, my modifies clause covers all the fields in the class and also the elements inside xs.

Hypothesis: It seems to me Dafny doesnt know the elements in the array are still the same after the shifting, we don't create or destroy them. To help with this, i tried to add a ghost oldSlice before loop start in order to show a multiset equality condition between elements so that we also have post condition:

ensures  multiset(xs[..]) == multiset(old(xs[..]))

But this is not enough. What would be missing to convince the prover?

Dafny version: 4.10

Firstly, you can define a ghost sequence which clones the array. You can then write two-state lemmas about the array. I happened to write a blog post about a very similar situation here.

https://dev.to/hath995/verified-ordered-set-in-dafny-2aak