unregistered verification error: [application.precondition:insufficient.permission; 0]

[Pointerbender]

The below program outputs a rather mysterious error:

pub struct A {
    inner: [usize; 4],
}

impl A {
    #[pure]
    #[requires(index < self.inner.len())]
    pub fn is_valid(&self, index: usize) -> bool {
        self.inner[index] <= isize::MAX as usize
    }
    
    #[pure]
    #[ensures(forall(|i: usize| (result && index < self.inner.len() && 0 <= i && i <= index) ==> (self.is_valid(i))) )]
    pub fn test(&self, index: usize) -> bool {
        match index {
            index if 0 < index && index < self.inner.len() => self.is_valid(index) && self.test(index - 1),
            index if index == 0 => self.is_valid(index),
            _ => false,
        }
    }
}

The full error message is "unregistered verification error: [application.precondition:insufficient.permission; 0] Precondition of function snap$__$TY$__struct$m_A$Snap$struct$m_A might not hold. There might be insufficient permission to access struct$m_A(_old$pre$0)". The error message seems similar to the one in #25, however that example differs in using mutable borrows instead of immutable borrows in this new example.

The above example succeeds if the #[ensures] post-condition is removed. It looks like it is related to the universal quantifier forall. In the resulting Viper program for A::test, the relevant statements look like this (verification fails on the non-trivial assert statement):

--- SNIP ---

  label l10
  // ========== bb20 ==========
  
  __t20 := true
  // [mir] return
  
  // ========== return ==========
  
  // Target of any 'return' statement.
  
  // Exhale postcondition
  
  label l36
  // Fold predicates for &mut args and transfer borrow permissions to old
  
  fold acc(struct$m_A(_1.val_ref), read$())
  // obtain acc(struct$m_A(_1.val_ref), write)
  
  _old$pre$0 := _1.val_ref
  // Fold the result
  
  fold acc(bool(_0), write)
  // obtain acc(bool(_0), write)
  
  // Assert possible strengthening
  
  // Assert functional specification of postcondition
  
  unfold acc(bool(_0), write)
  assert (unfolding acc(struct$m_A(_old$pre$0), read$()) in (let _LET_0 == (_0.val_bool) in (let _LET_2 == (old[pre](_2.val_int)) in (let _LET_1 == (old[pre](_2.val_int) < len$Snap$Slice$usize$__$TY$__Snap$Slice$usize$$int$(cons$Snap$Slice$usize$__$TY$__Seq$$int$$Snap$Slice$usize(Seq(read$Snap$Array$4$usize$__$TY$__Snap$Array$4$usize$$int$$$int$(snap$__$TY$__Array$4$usize$Snap$Array$4$usize(_old$pre$0.f$inner), 0), read$Snap$Array$4$usize$__$TY$__Snap$Array$4$usize$$int$$$int$(snap$__$TY$__Array$4$usize$Snap$Array$4$usize(_old$pre$0.f$inner), 1), read$Snap$Array$4$usize$__$TY$__Snap$Array$4$usize$$int$$$int$(snap$__$TY$__Array$4$usize$Snap$Array$4$usize(_old$pre$0.f$inner), 2), read$Snap$Array$4$usize$__$TY$__Snap$Array$4$usize$$int$$$int$(snap$__$TY$__Array$4$usize$Snap$Array$4$usize(_old$pre$0.f$inner), 3))))) in (forall _2_quant_a5335780e8534827844b904391c584f3_101: Int :: 0 <= _2_quant_a5335780e8534827844b904391c584f3_101 && _2_quant_a5335780e8534827844b904391c584f3_101 <= 18446744073709551615 ==> _LET_0 && (_LET_1 && (0 <= _2_quant_a5335780e8534827844b904391c584f3_101 && _2_quant_a5335780e8534827844b904391c584f3_101 <= _LET_2)) ==> m_is_valid__$TY$__Snap$struct$m_A$$int$$$bool$(snap$__$TY$__struct$m_A$Snap$struct$m_A(_old$pre$0), _2_quant_a5335780e8534827844b904391c584f3_101))))))
  // Assert type invariants
  
  fold acc(bool(_0), write)
  assert true
  // Exhale permissions of postcondition (1/3)
  
  exhale acc(struct$m_A(_old$pre$0), read$())
  // Exhale permissions of postcondition (2/3)
  
  exhale acc(bool(_0), write)
  // Exhale permissions of postcondition (3/3)
  
  goto end_of_method

--- SNIP ---

Am I doing something wrong/unsupported, or could this be a bug? Thanks!

[fpoli]

I believe this is an instance of #364: the postcondition requires _old$pre$0 to be folded to call is_valid but also unfolded to access inner. The issue was fixed by encoding pure functions using snapshots, but then the impure encoding of pure functions reintroduced it. @vakaras plans to fix this by only using snapshots in the assertions of impure code. An alternative is to modify the fold-unfold algorithm to generate unfoldings in the leaves of assertions rather than at the top-level, but this would be less efficient in other cases.

A temporary workaround should be to move self.inner.len() to its own pure function.

[Pointerbender]

Thanks for the suggested work-around, that works nicely :) The only change I had to make was:

    #[pure]
    pub const fn len(&self) -> usize {
        self.inner.len()
    }
    
    #[pure]
    #[ensures(forall(|i: usize| (result && index < self.len() && 0 <= i && i <= index) ==> (self.is_valid(i))) )]
    pub fn test(&self, index: usize) -> bool { /* ... */ } // function body remained unchanged

Would it be helpful if I add the failing example program to verify_partial as a regression test for when the snapshot encoding is updated?

[fpoli]

Would it be helpful if I add the failing example program to verify_partial as a regression test for when the snapshot encoding is updated?

Yes, thanks. Since we decided to have verify_partial, adding tests for any open issue looks good to me.

[fpoli]

I gave a better look at this bug. It's not exactly an instance of #364. It turns out that the fold-unfold algorithm generates the correct expression, but then the fix_quantifiers pass breaks the permissions by pulling out all unfolding ... in that are inside forall to outside of forall.

[Pointerbender]

I gave a better look at this bug. It's not exactly an instance of #364. It turns out that the fold-unfold algorithm generates the correct expression, but then the fix_quantifiers pass breaks the permissions by pulling out all unfolding ... in that are inside forall to outside of forall.

I'm currently looking a bit deeper into this one :) At a high level the problem seems to be that there is an implication A ==> B inside the forall, for which the unfolding acc(X) in ... sits inside the antecedent A, but then acc(X) is also required within the consequent B (as a pre-condition to one of the functions called in the consequent B). When the unfolding acc(X) in ... is moved outside of the forall, the acc(X) permission is no longer available to consequent B, because it's already used by the outer unfolding.

One idea I have to fix this is not to pull the unfolding out of the forall if it lives insides an implication by overriding <UnfoldingExtractor as vir::ExprFolder>::fold_bin_op() not to traverse a BinOp of kind BinaryOpKind::Implies. Would this be a sound approach?

I'm planning to skip folding the entire implication in this case, because there could be multiple implications inside a forall, which all could potentially use acc(X) in the antecedent, consequent or both. Pulling just one of those out, could break the permissions for the other implications.

Thanks!

[vakaras]

@Pointerbender FYI: This should be fixed in my refactoring (by completely getting rid of the problematic code). However, I am currently blocked waiting for @Aurel300 to finish his refactoring…

[Pointerbender]

Thanks for the heads up! In that case I'll just apply a temporary hack on my local version of Prusti to disable moving out the unfoldings :)

[Pointerbender]

@vakaras just in case, in the upcoming refactoring, were the only removed optimizations in the fix_quantifiers pass, or will other optimizations also be affected? The reason I'm asking is because I may have found a problem with the optimize_folding pass, which I'm currently investigating (I will open a separate issue once I figured out what is causing it). Thanks!

[vakaras]

@vakaras just in case, in the upcoming refactoring, were the only removed optimizations in the fix_quantifiers pass, or will other optimizations also be affected? The reason I'm asking is because I may have found a problem with the optimize_folding pass, which I'm currently investigating (I will open a separate issue once I figured out what is causing it). Thanks!

All code that works with expressions will be affected in some way. Also, some code that works with statements.

[fpoli]

The program in the first message now panics:

thread 'rustc' panicked at 'not yet implemented', prusti-viper/src/encoder/mir/pure/specifications/encoder_high.rs:34:5

[Pointerbender]

The program in the first message now panics:

thread 'rustc' panicked at 'not yet implemented', prusti-viper/src/encoder/mir/pure/specifications/encoder_high.rs:34:5

For now this panic can be worked around by commenting out this statement and compile a custom build of Prusti:

prusti-dev/prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs

Lines 288 to 294 in 75c09b9

	// Test the new encoding.
	let _ = super::new_encoder::encode_function_decl(
	self,
	proc_def_id,
	proc_def_id,
	substs,
	)?;