CODEWITHSUNDEEP
dafny
Shravan
Shravan

Reputation: 2723

Assertion, forall, and maps: Universal quantifiers does not work with maps

In this example, I insert only one value in a map and I try to assert that any two keys in this map is the same. However the assertion fails. Here is the 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
  );
}

The assertion fails only if I use forall to iterate through the map. Any leads on why the assertion fails?

Upvotes: 2

Views: 271

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

Unfortunately, Dafny does not have a built-in understanding of the relationship between cardinality-one and the quantified property you mentioned. Here is one way to convince Dafny of this fact.

We can factor out the reasoning into a generic lemma about maps.

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);
}

This lemma just says that if a map has cardinality one, then it all its keys are equal. The proof invokes a similar lemma about sets, on the set of keys of the map.

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
}

This lemma is the corresponding fact about sets. The proof is a bit strange, and relies on the (undocumented, learned-by-fire) fact that Dafny does understand that a set of cardinality 0 is empty. So we grab an "arbitrary" element z of s, and then construct the set s - {z}. Then we mention the cardinality of this new set, and Dafny all of a sudden notices that this set must be empty, which means s had to contain only z, and we're done.

With the lemma proved, we can return to your code.

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)
  ;
}

You wanted to prove an assertion about all states. To do that, we need to invoke our lemma CardinalityOneMap on s, but s is a variable under a universal quantifier, so we need to use the forall statement to do this. After the statement, we can re-assert the same fact if we want, just to double check that Dafny is now convinced.

Here are a few other answers that might be relevant:

PS: glad to see you're working through the distributed systems course!

Upvotes: 1

Related Questions