[Arrays] Consistency error: expected the same type, but got Snap$m_A$_beg_$_end_ and Ref (@16.23)

[Pointerbender]

Hi again! I've found another Consistency error: expected the same type, but got Snap$m_A$_beg_$_end_ and Ref error and it's similar to #707. This time it's in the context of arrays. This program triggers two consistency errors:

#[derive(Clone, Copy)]
pub struct A(usize);

#[derive(Clone, Copy)]
pub struct B {
    inner: [A; 16],
}

impl B {
    pub fn new(a: A) -> Self {
        Self { inner: [a; 16] }
        //            ^^^^^^^
        // error: [Prusti internal error] consistency error in B::new:
        // Consistency error: expected the same type, but got Snap$m_A$_beg_$_end_ and Ref
    }
}

pub fn test() {
    let mut b = B::new(A(0));
    b.inner[2] = A(1);
    //     ^^^
    // error: [Prusti internal error] consistency error in test:
    // Consistency error: expected the same type, but got Snap$m_A$_beg_$_end_ and Ref

}

pub fn main() {}

The first one is due to an inhale statement where the left-hand side is snapshot encoded, but the right-hand side is not:

function lookup_pure__$TY$__Array$16$m_A$_beg_$_end_$$int$$Snap$m_A$_beg_$_end_(self: Ref, idx: Int): Snap$m_A$_beg_$_end_
      requires acc(Array$16$m_A$_beg_$_end_(self), read$())
      requires 0 <= idx
      requires idx < 16

method m_new() returns (_0: Ref)
      --- SNIP ---
      var _2: Ref
      var _3: Ref
      --- SNIP ---
      _2 := builtin$havoc_ref()
      inhale acc(Array$16$m_A$_beg_$_end_(_2), write)
      inhale lookup_pure__$TY$__Array$16$m_A$_beg_$_end_$$int$$Snap$m_A$_beg_$_end_(_2, 0) == _3
      --- SNIP ---

The second one has the same problem, but performs a modifying lookup through a temporary variable:

field f$inner: Ref

function lookup_pure__$TY$__Array$16$m_A$_beg_$_end_$$int$$Snap$m_A$_beg_$_end_(self: Ref, idx: Int): Snap$m_A$_beg_$_end_
      requires acc(Array$16$m_A$_beg_$_end_(self), read$())
      requires 0 <= idx
      requires idx < 16

method m_test() returns (_0: Ref)
      --- SNIP ---
      var __t4: Ref
      var _3: Ref
      --- SNIP ---
      __t4 := _3
      label l3
      inhale lookup_pure__$TY$__Array$16$m_A$_beg_$_end_$$int$$Snap$m_A$_beg_$_end_(_1.f$inner, old[l2](_4)) == __t4
      --- SNIP ---

My first guess that this is due to missing snapshot encoding logic in ProcedureEncoder::encode_assign_array_repeat_initializer() and ProcedureEncoder::encode_array_lookup_mut() in prusti-viper/src/encoder/procedure_encoder.rs.

After seeing the return_type.is_snapshot() || return_type.is_domain() fixes in #693 and #707, I was hoping to try my hand to add the same quick fix here. However, this time it is slightly different, in that the bug now lies on the right-hand side and seems present in multiple places (perhaps also in other ProcedureEncoder::encode*{array|slice}*() methods or in prusti-viper/src/encoder/array_encoder.rs?) and that I have not (yet) found any existing snapshot encoding calls for the right-hand side which I can extend with the same fix (sometimes Prusti complains that the corresponding pre-conditions go missing, because I'm currently not sure how to generate the "pre-statements"). I'm eager to try more, although I might need a little mentoring on this one :smile: (I have read Johannes Schilling's master thesis "Specifying and Verifying Sequences and Array Algorithms in a Rust Verifier", which seems to touch on this part of the code, in case that helps - although a friendly disclaimer: I'm still very new to formal verification in general :smile: ). Going to send a first PR that hopefully addresses ProcedureEncoder::encode_assign_array_repeat_initializer() shortly!

[fpoli]

Fixed in https://github.com/viperproject/prusti-dev/pull/710

[fpoli]

Actually, #710 fixes a variant of this issue. I still get the errors described above.

[Pointerbender]

@fpoli Only one of the two consistency errors was fixed by my PR :) There are also some other instances related to the same root cause, @vakaras is currently contemplating how to best fix all of those in one go. I'll see if I can draft up some more regression tests this weekend in order to capture all the edge cases (off the top of my head, these are: array repeat expression initialization, array direct assignment, array lookup, array slicing (shared/mutable), probably the same operations for slices, too - I will double check with the code base this weekend to see if I missed any in the list of use cases).

[Pointerbender]

Just a quick update to summarize the latest activity on this issue: there are now 11 test cases in prusti-tests/tests/verify_partial/fail/issues which reproduce the errors mentioned in this issue (or different related variants thereof). Once the underlying cause is fixed, these test cases can be moved to prusti-tests/tests/verify_overflow/pass/issues to be re-used as regression tests.

[Pointerbender]

It looks like one of the 11 test cases (prusti-tests/tests/verify_partial/fail/issues/issue-709-13.rs) will be fixed soon as a bonus side effect of #603 :) It can then be moved to the pass folder instead.