Program with array class member does not verify with parallel block

[sakehl]

The following program does not verify

class Ghost {
  bool[] written;

    requires N >= 0;
    context Perm(written, write);
    ensures written != null && written.length == N;
    ensures (\forall* int i=0..N; Perm({:written[i]:},write));
    ensures (\forall int i=0..N; {:written[i]:} == false);
  void initialize(int N){
    written = new bool[N];
  }
}

  context N >= 0;
  context_everywhere |inp| == N;
void parallel_sum(seq<int> inp, int N){
  Ghost g = new Ghost();
  g.written = new bool[N];

  bool[] written = g.written;


  {
    par (int tid = 0 .. N)
      context tid >= 0 && tid < N;
      context |inp| == N;
      context Perm(g.written, 1\(2*N)) ** \array(g.written, N) ** Perm(g.written[tid], write);
      // context written == g.written; // Do not comment this, and it works
      requires !g.written[tid];
      ensures g.written[tid];
    {
      g.written[tid] = true;
    }
  }
}

with error:

vct.col.origin.BlameUnreachable: An error condition was reached, which should be statically unreachable. schematic. Inner failure:
 > ======================================
 > At /home/lars/data/VerifyThisTraining/Training1/minimize_bug.pvl
 > --------------------------------------
 >    22  
 >    23    {
 >           [------------------------
 >    24      par (int tid = 0 .. N)
 >    25        context tid >= 0 && tid < N;
 >    26        context |inp| == N;
 >        ... (4 lines omitted)
 >    31      {
 >    32        g.written[tid] = true;
 >    33      }
 >        -----]
 >    34    }
 >    35  }
 > --------------------------------------
 > There may be insufficient permission to access this field here. (https://utwente.nl/vercors#perm)
 > ======================================
        at vct.col.origin.PanicBlame.blame(Blame.scala:948)
        at viper.api.backend.SilverBackend.defer(SilverBackend.scala:321)
        at viper.api.backend.SilverBackend.defer$(SilverBackend.scala:315)

Observations:

1. Adding the option --no-infer-heap-context-into-frame does let it verify.
2. Remove the method initialize does let it verify.
3. Add context written == g.written to the parallel contract, and it does verify.
4. The vpr file says this (from the --backend-file-base option):
   Contract might not be well-formed. There might be insufficient permission to access obj.bool (parallel_atomic_sum-0.vpr@297.21--310.18)
   And these are the lines it fails on:

invariant once ==>
            |inp| == n &&
            (0 <= tid3 && tid3 < n && |inp| == n &&
            (acc(g.written, 1 * write / (2 * n)) &&
            (g.written != (none1(): Option[Array]) &&
            alen(optGet1(g.written)) == n) &&
            acc(aloc(optGet1(g.written), tid3).bool, write)) &&
            !aloc(optGet1(g.written), tid3).bool) &&
            [(forperm
              obj: Ref [obj.bool] :: obj.bool == old[BEFOREFRAME](obj.bool)) &&
            (forperm
              obj: Ref [obj.written] :: obj.written ==
              old[BEFOREFRAME](obj.written)),
            true]

parallel_atomic_sum-0.vpr.txt

[sakehl]

Changing:

[(forperm
              obj: Ref [obj.bool] :: obj.bool == old[BEFOREFRAME](obj.bool)) &&
            (forperm
              obj: Ref [obj.written] :: obj.written ==
              old[BEFOREFRAME](obj.written)),
            true]

to

[(forperm
              obj: Ref [obj.written] :: obj.written ==
              old[BEFOREFRAME](obj.written)) && (forperm
              obj: Ref [obj.bool] :: obj.bool == old[BEFOREFRAME](obj.bool)),
            true]

(switching the forperms) does let it verify. Maybe this is a silicon bug?

I tried verifying with Carbon, and that succeeded.

I have no clue what the these forperms are for, so hard to say what happens.

[pieter-bos]

This is an instance of #1101 (it's not a silicon bug, but a vercors bug, although I would love for viper to support Frame directly)