formal-verification - 不变量失败但在循环验证之前断言

Question

在下面的程序中，循环的最后一个不变量验证失败。但是如果我把它作为断言放在 while 循环之前，条件就会验证。如果我添加字段 ia 没有改变，它也会验证。为什么需要这个？读取权限不应该暗示这一点吗？我可以想象 old 以一种奇怪的方式与循环预状态/状态破坏进行交互，但这并不能向我解释它失败的原因。会不会是一个错误？

domain VCTArray[CT] {
  function loc(a: VCTArray[CT], i: Int): CT
  
  function alen(a: VCTArray[CT]): Int
}

//  a field 
field ia: VCTArray[Ref]

//  a field 
field item: Int

method negatefirst(diz: Ref)
requires diz != null
requires acc(diz.ia, 1/2)
requires alen(diz.ia) > 0 ==> acc(loc(diz.ia, 0).item, write)
{
  // Verifies just fine
  assert alen(diz.ia) > 0 ==> (old(loc(diz.ia, 0).item) == old(loc(diz.ia, 0).item))
  while (false)
    invariant acc(diz.ia, 1/4) 
    // invariant diz.ia == old(diz.ia) // Adding this invariant allows the program to verify
    invariant alen(diz.ia) > 0 ==> acc(loc(diz.ia, 0).item, write)
    // Error: insufficient permission to acces loc(diz.ia, 0).item
    invariant alen(diz.ia) > 0 ==> (old(loc(diz.ia, 0).item) == old(loc(diz.ia, 0).item)) 
  { 
    
  }
}

我的芯片版本:

$ ./silicon.sh --help
Silicon 1.1-SNAPSHOT (d45da1d7+)

Answer 1

您观察到的行为是 known difference硅和碳之间，这确实令人困惑。

这就是硅中正在发生的事情:循环体基本上是隔离验证的，即模块化:不变量在空状态下被吸入，然后是循环守卫；然后验证 body 。吸入最后一个不变量时，假定其左侧 alen(diz.ia) > 0(在一条路径上)及其右侧 old(loc(diz.ia, 0).item) == old(loc(diz.ia, 0).item) 被(试图)吸入。现在，回想一下，正在进行的验证是在一个新的状态下孤立地发生的:因此，当前状态下的 diz.ia 可能不会引用与当前状态下的 diz.ia 相同的对象旧 状态。如果是这样，则 alen(diz.ia) > 0(当前状态)并不意味着 old(alen(diz.ia) > 0)，并且字段 old(loc(diz.ia, 0).item) 因此可能无法访问。因此，假设引用在这两个状态之间没有变化——即 invariant diz.ia == old(diz.ia)——使程序验证。

这是纯粹主义者验证循环体的方式；实际上，隔离并不那么严格:两个验证器都将关于局部变量的知识构建到循环中，用于(语法上)未在循环体中分配的变量。这是一个例子:

method test() {
  var i: Int := 0
  var j: Int := 0
  
  while (true)
  {
    assert i == 0 // Verified
    assert j == 0 // Rejected
    j := j
  }
}

Carbon 更进一步，还将有关字段的知识构建到循环体中，对于周围验证范围(例如包含循环的方法体)保留一些权限的字段:

field f: Int

method test(r: Ref, p: Perm) {
  inhale none < p
  inhale acc(r.f, p) && r.f == 0
  
  while (true)
    invariant acc(r.f, p/2) // Verified in Carbon, rejected by Silicon
  {
    assert r.f == 0
  }
}

以上内容按原样在 Carbon 中验证，但如果您将不变量的权限更改为 p(或通过 exhale acc(r.f, p); inhale 破坏字段的值，则不再验证acc(r.f, p) 就在循环之前。

底线:Viper 团队应该决定“正确”的语义，并确保两个验证者都遵守它。