How to read into array<array<nat>>?

[ChuyueSun]

ghost predicate pre_original(arr: array<array<nat>>,index1: nat,index2: nat,val: nat,i: nat,j:nat,some_index1: nat,some_index2: nat)
reads arr
{
( index1 < arr.Length) && ( index2 < arr[index1].Length) && 
( forall i: nat, j:nat :: i < arr.Length && j < arr.Length &&  i != j
 ==> arr[i] != arr[j])
}

twostate predicate post_original(arr: array<array<nat>>,index1: nat,index2: nat,val: nat,i: nat,j:nat,some_index1: nat,some_index2: nat)
requires pre_original(arr,index1,index2,val,i,j,some_index1,some_index2)
reads arr
reads arr[index1]
{
forall some_index1: nat, some_index2: nat ::
        0<=some_index1 < arr.Length && 0<=some_index2 < arr[some_index1].Length ==>
    arr[some_index1][some_index2] == (if index1 == some_index1 && index2 == some_index2
        then val else old(arr[some_index1][some_index2]))
}

will produce the error insufficient reads clause to read array element at arr[some_index1][some_index2] and index out of range at old(arr[some_index1][some_index2]). How do I make it work?

[MikaelMayer]

@jtristan

[rdivyanshu]

@ChuyueSun

For first and second predicate, additional reads clauses are required - It can read all arrays inside arr.
For second predicate, additional precondition which is required - length of arrays inside arr doesn't increases.

ghost predicate pre_original(arr: array<array<nat>>, index1: nat, index2: nat, val: nat, i: nat, j:nat, some_index1: nat, some_index2: nat)
  reads arr, arr[..]
{
  (index1 < arr.Length) && (index2 < arr[index1].Length) && (forall i: nat, j: nat :: i < arr.Length && j < arr.Length &&  i != j ==> arr[i] != arr[j])
}

twostate predicate post_original(arr: array<array<nat>>, index1: nat, index2: nat, val: nat, i: nat, j:nat, some_index1: nat, some_index2: nat)
  reads arr, arr[..]
  requires forall i :: 0 <= i < arr.Length ==> arr[i].Length <= old(arr[i].Length)
  requires pre_original(arr, index1, index2, val, i, j, some_index1, some_index2)
{
  forall i: nat, j: nat ::
    (0 <= i < arr.Length && 0 <= j < arr[i].Length) ==>
    (arr[i][j] == (if index1 == some_index1 && index2 == some_index2
    then val else old(arr[i][j])))
}