断言，永久和地图：通用量词不适用于地图

问题描述

在此示例中，我仅在一个映射中插入一个值，然后尝试断言该映射中的任何两个键都是相同的。但是断言失败。这是link。

datatype HostState = HostState(counter:nat,Vote: map<nat,set<nat>>)
predicate Hostinit(s:HostState,counter: nat) {
  var default: nat := 0;
  && s.counter == 1
  && |s.Vote| == 1 && default in s.Vote
}

lemma lemma_UniqueKey(){
  var default: nat := 0;
  assert forall s,counter :: Hostinit(s,counter) ==>
  (
    // |s.Vote| == 1 && default in s.Vote // Pass
    (forall t: nat,t': nat :: t in s.Vote && t' in s.Vote ==> t' == t) // Fail
    // (forall t: nat :: t in s.Vote) // Not even this works
  );
}

仅当我使用forall遍历地图时，断言才会失败。为什么断言失败的任何线索？

解决方法

不幸的是，Dafny对基数一和您提到的量化属性之间的关系没有内在的了解。这是一种使达夫尼相信这一事实的方法。

我们可以将推理分解为关于地图的一般引理。

lemma CardinalityOneMap<A,B>(m: map<A,B>)
  requires |m| == 1
  ensures forall x,y | x in m && y in m :: x == y
{
  CardinalityOneSet(m.Keys);
}

这个引理只是说，如果一张地图的基数为1，那么它的所有键都是相等的。证明在地图的键集上调用了关于集的类似引理。

lemma CardinalityOneSet<A>(s: set<A>)
  requires |s| == 1
  ensures forall x,y | x in s && y in s :: x == y
{
  var z :| z in s;
  var s' := s - {z};
  assert |s'| == 0;  // this is enough for dafny to see s' is empty
}

这个引理是关于集合的相应事实。该证明有点奇怪，它依赖于（未记录的，通过射击学习的）事实，即达夫尼确实知道一组基数0为空。因此，我们获取z的“任意”元素s，然后构造集合s - {z}。然后我们提到这个新集合的基数，而Dafny突然注意到该集合必须为空，这意味着s只包含z，就可以了。

证明了引理后，我们可以返回您的代码。

lemma lemma_UniqueKey(){
  var default: nat := 0;
  forall s,counter | HostInit(s,counter) 
    ensures (forall t: nat,t': nat :: t in s.vote && t' in s.vote ==> t' == t)
  {
    CardinalityOneMap(s.vote);
  }

  assert forall s,counter :: HostInit(s,counter) ==>
    (forall t: nat,t': nat :: t in s.vote && t' in s.vote ==> t' == t)
  ;
}

您想证明关于所有状态的断言。为此，我们需要在CardinalityOneMap上调用引理s，但是s是通用量词下的变量，因此我们需要使用forall 声明来做到这一点。声明之后，我们可以根据需要重新声明相同的事实，只需仔细检查一下Dafny现在是否被说服即可。

以下是一些可能相关的答案：

PS：很高兴看到您正在完成分布式系统课程！

dafny