I have the following lemma which feels fairly straightforward but it takes quite a while and a good amount of resources to verify. I don’t think it should take so long but it isn’t immediately obvious to me how to improve the performance. I’ve removed as many assertions that were unneeded but it still uses about 27M and still takes a couple of seconds to verify. According to the Dafny blog we should shoot for under 1M of resources.

    lemma {:induction false} msorted_equal(xs: seq<int>, ys: seq<int>)
        requires sortedRec(xs)
        requires multiset(xs) == multiset(ys)
        decreases xs
        ensures xs == msort_bu(ys)
    {
        if xs == [] {
        } else {
            assert ys != [];
            assert xs == [xs[0]] + xs[1..];
            assert ys == [ys[0]] + ys[1..];
            assert xs[0] == msort_bu(ys)[0] by {
                assert forall x :: x in xs ==> x in multiset(xs) && x in multiset(ys) && x in ys;
                assert forall y :: y in ys ==> y in multiset(ys) && y in multiset(xs) && y in xs && y in msort_bu(ys);
                assert forall yy :: yy in msort_bu(ys)[1..] ==> msort_bu(ys)[0] <= yy;
                assert forall xx :: xx in xs ==> xs[0] <= xx;
                if xs[0] != msort_bu(ys)[0] {
                    if xs[0] < ys[0] {
                        assert xs[0] in msort_bu(ys)[1..];
                    } else {
                        assert ys[0] in xs[1..];
                    }
                    assert false;
                }

            }
            assert msort_bu(ys)[0] in multiset(msort_bu(ys)) && msort_bu(ys)[0] in ys;
            var ys1 := subtractOneFromList(ys, msort_bu(ys)[0]);
            subtractOneFromListLemma(ys, msort_bu(ys)[0]);
            assert multiset(xs) == multiset([xs[0]]) + multiset(xs[1..]);
            assert multiset(xs) == multiset(xs[1..]) + multiset{msort_bu(ys)[0]};
            assert multiset(xs[1..]) == multiset(ys1);
            assert msort_bu(ys) == [msort_bu(ys)[0]] + msort_bu(ys)[1..];
            assert multiset(ys1) == multiset(msort_bu(ys)[1..]) by {
                // assert multiset(msort_bu(ys)) == multiset{msort_bu(ys)[0]} + multiset(msort_bu(ys)[1..]);
                assert multiset(msort_bu(ys)) - multiset{msort_bu(ys)[0]} == multiset(msort_bu(ys)[1..]);
                assert multiset(ys) - multiset{msort_bu(ys)[0]} == multiset(msort_bu(ys)[1..]);
                assert multiset(ys1) == multiset(ys) - multiset{msort_bu(ys)[0]};
                // assert multiset(ys) == multiset(ys1) + multiset{msort_bu(ys)[0]};
            }
            msorted_equal(xs[1..], ys1);
            assert xs[1..] == msort_bu(ys1);
            multisetsEqualSortedAreEqual(msort_bu(ys1), msort_bu(ys)[1..]);
            assert msort_bu(ys) == [msort_bu(ys)[0]] + msort_bu(ys1);
            assert xs == msort_bu(ys);
        }
    }

Edit: With the following changes I was able to get it to 1.28M RU but still isn’t under 1M. It’s unclear to me why keeping assertions which should be equivalent to function or lemma post conditions sometimes reduces the usage when it seems like those should already be established facts from making those calls.

    lemma {:induction false} msorted_equal(xs: seq<int>, ys: seq<int>)
        requires sortedRec(xs)
        requires multiset(xs) == multiset(ys)
        decreases xs
        ensures xs == msort_bu(ys)
    {
        if xs == [] {
        } else {
            assert ys != [];
            assert xs == [xs[0]] + xs[1..];
            assert ys == [ys[0]] + ys[1..];
            assert xs[0] == msort_bu(ys)[0] by {
                assert xs[0] in multiset(xs) && xs[0] in multiset(ys) && xs[0] in msort_bu(ys);
                assert msort_bu(ys)[0] in multiset(msort_bu(ys)) && msort_bu(ys)[0] in multiset(ys) && msort_bu(ys)[0] in xs;
                if xs[0] != msort_bu(ys)[0] {
                    if xs[0] < msort_bu(ys)[0] {
                        assert xs[0] in msort_bu(ys)[1..];
                    } else {
                        assert msort_bu(ys)[0] in xs[1..];
                    }
                    assert false;
                }
            }
            var ys1 := subtractOneFromList(ys, msort_bu(ys)[0]);
            subtractOneFromListLemma(ys, msort_bu(ys)[0]);
            calc {
                multiset(xs);
                multiset([xs[0]]) + multiset(xs[1..]);
                multiset{msort_bu(ys)[0]} + multiset(xs[1..]);
            }
            assert msort_bu(ys) == [msort_bu(ys)[0]] + msort_bu(ys)[1..];
            calc {
                multiset(xs[1..]);
                multiset(ys1);
                {
                    assert multiset(msort_bu(ys)) - multiset{msort_bu(ys)[0]} == multiset(msort_bu(ys)[1..]);
                    assert multiset(ys) - multiset{msort_bu(ys)[0]} == multiset(msort_bu(ys)[1..]);
                    assert multiset(ys1) == multiset(ys) - multiset{msort_bu(ys)[0]};
                }
                multiset(msort_bu(ys)[1..]);
            }
            msorted_equal(xs[1..], ys1);
            assert xs[1..] == msort_bu(ys1);
            multisetsEqualSortedAreEqual(msort_bu(ys1), msort_bu(ys)[1..]);
            assert xs == msort_bu(ys);
        }
    }

Here are the rest of the definitions.

    predicate sortedRec(list: seq<int>) {
        if list == [] then true else (forall y :: y in list[1..] ==> list[0] <= y) && sortedRec(list[1..])
    }

    function merge(xs: seq<int>, ys: seq<int>): seq<int>
        requires sortedRec(xs)
        requires sortedRec(ys)
        ensures sortedRec(merge(xs, ys))
        ensures multiset(merge(xs,ys)) == multiset(xs)+multiset(ys)
    {
        if xs == [] then ys else
        if ys == [] then xs else
        if xs[0] <= ys[0] then 
            assert xs == [xs[0]] + xs[1..];
            assert ys == [ys[0]] + ys[1..];
            assert forall x :: x in merge(xs[1..], ys) ==> x in xs[1..] || x in ys ==> xs[0] <= x;
            // assert sortedRec(merge(xs[1..], ys));
            var result := [xs[0]] + merge(xs[1..], ys);
            assert forall x :: x in result[1..] ==> x in multiset(xs[1..])+multiset(ys);
            result
        else 
            assert xs == [xs[0]] + xs[1..];
            assert ys == [ys[0]] + ys[1..];
            assert forall x :: x in merge(xs, ys[1..]) ==> x in xs || x in ys[1..] ==> ys[0] <= x;
            var result := [ys[0]] + merge(xs, ys[1..]);
            assert forall x :: x in result[1..] ==>x in multiset(xs) + multiset(ys[1..]);
            result
    }

    function mset_mset(xss: seq<seq<int>>): multiset<int>
        ensures forall xs :: xs in xss ==> forall x :: x in xs ==> x in mset_mset(xss) 
    {
        if xss == [] then multiset{} else
            assert xss == [xss[0]] + xss[1..]; 
            multiset(xss[0]) + mset_mset(xss[1..])
    }

    function {:verify true} merge_adj(xss: seq<seq<int>>): seq<seq<int>>
        requires forall xs :: xs in xss ==> sortedRec(xs)
        ensures |merge_adj(xss)| == (|xss| + 1)/2
        ensures mset_mset(xss) == mset_mset(merge_adj(xss))
        ensures forall xs :: xs in merge_adj(xss) ==> sortedRec(xs)
    {
    if xss == [] then []
    else if |xss| == 1 then xss
    else [merge(xss[0], xss[1])] + merge_adj(xss[2..])
    }

    function {:verify true} merge_all(xss: seq<seq<int>>): seq<int>
        requires forall xs :: xs in xss ==> sortedRec(xs)
        ensures sortedRec(merge_all(xss))
        ensures multiset(merge_all(xss)) == mset_mset(xss)
        decreases |xss|
    {
        if xss == [] then []
        else if |xss| == 1 then xss[0]
        else merge_all(merge_adj(xss))
    }


    function splitSeq(xs: seq<int>): seq<seq<int>>
        ensures multiset(xs) == mset_mset(splitSeq(xs))
        ensures forall ys :: ys in splitSeq(xs) ==> sortedRec(ys)
    {
        if xs == [] then [] else
            assert xs == [xs[0]] + xs[1..];
            [[xs[0]]] + splitSeq(xs[1..])
    }

    function {:verify true} msort_bu(xs: seq<int>): seq<int>
        ensures multiset(xs) == multiset(msort_bu(xs))
        ensures sortedRec(msort_bu(xs))
    {
        merge_all(splitSeq(xs))
    }

    function subtractOneFromList(xs: seq<int>, x: int): seq<int>
        requires x in multiset(xs)
    {
        if xs[0] == x then
            assert xs == [xs[0]] + xs[1..];
            assert multiset(xs) == multiset([xs[0]]) + multiset(xs[1..]);
            assert multiset(xs)-multiset{x} == multiset(xs[1..]);
            xs[1..]
        else
        [xs[0]] + subtractOneFromList(xs[1..], x)
    }

    lemma subtractOneFromListLemma(xs: seq<int>, x: int)
        requires x in multiset(xs)
        ensures multiset(xs)-multiset{x} == multiset(subtractOneFromList(xs, x))
    {
        var retval := subtractOneFromList(xs, x);
        var mset := multiset(xs);
        if xs[0] == x {
            assert xs == [xs[0]] + xs[1..];
            assert mset == multiset([xs[0]]) + multiset(xs[1..]);
            assert mset - multiset{x} == multiset(xs[1..]);
            assert mset - multiset{x} == multiset(retval);
        } else {
            assert xs == [xs[0]] + xs[1..];
            assert mset == multiset([xs[0]]) + multiset(xs[1..]);
        }
    }

    lemma multisetsEqualSortedAreEqual(xs: seq<int>, ys: seq<int>)
        requires multiset(xs) == multiset(ys)
        requires sortedRec(xs)
        requires sortedRec(ys)
        ensures xs == ys
    {
        if xs == [] {
        } else {
            assert xs == [xs[0]] + xs[1..];
            assert ys == [ys[0]] + ys[1..];
            assert xs[0] == ys[0] by {
                assert forall x :: x in xs ==> x in multiset(xs) && x in multiset(ys) &&  x in ys;
                assert forall y :: y in ys ==> y in multiset(ys) && y in multiset(xs) && y in xs;
                if xs[0] != ys[0] {
                    if xs[0] < ys[0] {
                        assert xs[0] in ys[1..];
                        assert ys[0] in xs;
                        assert false;
                    } else {
                        assert ys[0] < xs[0];
                        assert xs[0] in ys[1..];
                        assert ys[0] in xs;
                        assert false;
                    }
                }
            }
            assert multiset(xs) == multiset(ys);
            assert multiset(xs) == multiset([xs[0]]) + multiset(xs[1..]);
            assert multiset(xs) == multiset{xs[0]} + multiset(xs[1..]);
            assert multiset{xs[0]} + multiset(xs[1..]) - multiset{xs[0]} == multiset(xs[1..]);
            assert multiset(ys) == multiset{xs[0]} + multiset(ys[1..]);
            multisetsEqualSortedAreEqual(xs[1..], ys[1..]);
        }
    }