dafny - 在 Dafny 中验证账户转账

Question

我正在尝试在 Dafny 中验证一个简单的账户转账，这就是我想出的:

function sum(items: seq<int>): int
decreases |items| {
    if items == []
    then 0
    else items[0] + sum(items[1..])
}

method transfer(accounts: array<int>, balance: int, from: int, to: int)
requires from >= 0 && from < accounts.Length;
requires to >= 0 && to < accounts.Length;
requires accounts.Length > 0;
requires sum(accounts[..]) == balance;
ensures sum(accounts[..]) == balance;
modifies accounts;
{
    accounts[from] := accounts[from] - 1;
    accounts[to] := accounts[to] + 1;
    return;
}

我在这里一次只转移一个 token (尽管实际上我想转移任意数量)。不管怎样，它不验证。我想知道我还需要做什么？

Answer 1

这是一种方法。

问题是 Dafny 对 sum 函数一无所知，所以我们必须教它一些事实。

function sum(items: seq<int>): int
decreases |items| {
    if items == []
    then 0
    else items[0] + sum(items[1..])
}

lemma sum_append(xs: seq<int>, ys: seq<int>)
  ensures sum(xs + ys) == sum(xs) + sum(ys)
{
  if xs == [] {
    assert [] + ys == ys;
  } else {
    assert (xs + ys)[1..] == xs[1..] + ys;
  }
}

lemma sum_focus(xs: seq<int>, i: int)
  requires 0 <= i < |xs|
  ensures sum(xs) == sum(xs[..i]) + xs[i] + sum(xs[i+1..])
{
  calc {
    sum(xs);
    { assert xs == xs[..i] + [xs[i]] + xs[i+1..]; }
    sum(xs[..i] + [xs[i]] + xs[i+1..]);
    { forall xs, ys { sum_append(xs, ys); } }
    sum(xs[..i]) + xs[i] + sum(xs[i+1..]);
  }
}

method transfer(accounts: array<int>, balance: int, from: int, to: int)
requires from >= 0 && from < accounts.Length;
requires to >= 0 && to < accounts.Length;
requires accounts.Length > 0;
requires sum(accounts[..]) == balance;
ensures sum(accounts[..]) == balance;
modifies accounts;
{
    sum_focus(accounts[..], from);
    accounts[from] := accounts[from] - 1;
    sum_focus(accounts[..], from);

    sum_focus(accounts[..], to);
    accounts[to] := accounts[to] + 1;
    sum_focus(accounts[..], to);
}

sum_focus 引理允许我们将数组的总和分解为 i 之前元素的总和，加上 i 处的元素，加上i之后的元素之和。这个“聚焦”步骤允许 Dafny 推理写入数组元素 accounts[from] 和 accounts[to] 的赋值语句。

---

sum_focus 的替代版本:

lemma sum_focus(xs: seq<int>, i: int)
  requires 0 <= i < |xs|
  ensures sum(xs) == sum(xs[..i]) + xs[i] + sum(xs[i+1..])
{
  calc {
    sum(xs);
    { assert xs == xs[..i] + [xs[i]] + xs[i+1..]; }
    sum(xs[..i] + [xs[i]] + xs[i+1..]);
    {
      sum_append(xs[..i] + [xs[i]], xs[i+1..]);
      sum_append(xs[..i], [xs[i]]);
    }
    sum(xs[..i]) + xs[i] + sum(xs[i+1..]);
  }
}