如何提升Dafny中msorted_equal引理的性能并降低资源占用？

我编写了如下msorted_equal引理，逻辑看似简单，但验证耗时久、资源占用高。我已移除不必要的断言，但其仍占用约27M资源，验证需数秒。根据Dafny官方博客，资源占用应控制在1M以内。

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

修改说明 #

经过以下修改后，资源占用降至1.28M RU，但仍未达标。我不清楚为何保留与函数/引理后置条件等价的断言有时能降低资源占用，因为这些本应是调用后已确立的事实。

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

相关定义 #

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

内容的提问来源于stack exchange，提问作者Hath995