Representing MultiSets

[DavePearce]

In the VerifyThis2019 challenge, a key issue is demonstrating that the result of the sort is a permutation of the input. To do this, Dafny employes multisets which are a built in feature. An interesting is how we can model such multisets in Boogie (and subsequently in Whiley). I'm going to explore this issue here.

@utting Thoughts welcome on this!

[DavePearce]

My initial (broken) Boogie code is this:

function Array#in(a : [int]int, i : int) returns (bool) {
   (i >= 0) && (i < Array#Length(a))
}

function Array#Length([int]int) returns (int);
axiom (forall a:[int]int :: 0 <= Array#Length(a));
axiom (forall a:[int]int,i:int,v:int :: Array#in(a,i) ==> (Array#Length(a) == Array#Length(a[i:=v])));

function Array#Empty(int) returns ([int]int);
axiom (forall l:int,i:int :: ((0 <= i) && (i < l)) || (Array#Empty(l)[i] == 0));
axiom (forall a:[int]int,l:int :: ((0 <= l) && (Array#Empty(l) == a)) ==> (Array#Length(a) == l));

procedure multiset(xs: [int]int) returns (ys: [int]int);
ensures (forall i:int,j:int :: (i < j) ==> ys[i] < ys[j]);
ensures (exists p:[int]int :: (forall i:int :: xs[i] == ys[p[i]]));

procedure test()
{
  var arr1 : [int]int;
  var arr2 : [int]int;  
  arr1 := Array#Empty(2)[0:=1][1:=0];
  arr2 := Array#Empty(2)[0:=0][1:=1];  
  //
  call arr1 := multiset(arr1);
  call arr2 := multiset(arr2);
  //
  assert arr1 == arr2;
}

I'm just putting it here for reference.

[DavePearce]

So, the move prover does it like this:

type {:datatype} Multiset _;
function {:constructor} Multiset<T>(v: [T]int, l: int): Multiset T;

function {:builtin "MapConst"} MapConstMultiset<T>(l: int): [T]int;

function {:inline} EmptyMultiset<T>(): Multiset T {
    Multiset(MapConstMultiset(0), 0)
}

function {:inline} LenMultiset<T>(s: Multiset T): int {
    l#Multiset(s)
}

function {:inline} ExtendMultiset<T>(s: Multiset T, v: T): Multiset T {
    (var len := l#Multiset(s);
    (var cnt := v#Multiset(s)[v];
    Multiset(v#Multiset(s)[v := (cnt + 1)], len + 1)))
}

// This function returns (s1 - s2). This function assumes that s2 is a subset of s1.
function {:inline} SubtractMultiset<T>(s1: Multiset T, s2: Multiset T): Multiset T {
    (var len1 := l#Multiset(s1);
    (var len2 := l#Multiset(s2);
    Multiset((lambda v:T :: v#Multiset(s1)[v]-v#Multiset(s2)[v]), len1-len2)))
}

function {:inline} IsEmptyMultiset<T>(s: Multiset T): bool {
    (l#Multiset(s) == 0) &&
    (forall v: T :: v#Multiset(s)[v] == 0)
}

function {:inline} IsSubsetMultiset<T>(s1: Multiset T, s2: Multiset T): bool {
    (l#Multiset(s1) <= l#Multiset(s2)) &&
    (forall v: T :: v#Multiset(s1)[v] <= v#Multiset(s2)[v])
}

function {:inline} ContainsMultiset<T>(s: Multiset T, v: T): bool {
    v#Multiset(s)[v] > 0
}