How do I prove the while loop terminates in Dafny?

Question

I'm new to Dafny and learning it. For the following Dafny code

method Dummy(s: seq<nat>) returns (ret: nat)
    requires forall k :: 0 <= k < |s| ==> s[k] > 0
{
    ret := 0;
    var se := s;

    while |se| > 0
    {
        // Pick a random index of the seq.
        var i :| 0 <= i < |se|;
        if se[i] == 1 {
            // Remove the seq element if it is 1.
            se := se[..i] + se[i + 1..];
        } else {
            // Replace the seq element with 3 occurences of 1.
            se := [1, 1, 1] + se[..i] + se[i + 1..];
        }
    }

    return;
}

I'm seeing complaints which are

decreases |se| - 0Dafny VSCode
cannot prove termination; try supplying a decreases clause for the loopDafny VSCode

I know that to prove termination, generally I should provide a decreases clause. I just cannot find what to put in the decreases clause in this case. Simply putting

decreases |se|

there will not work, as in the else part of the if statement the seq size may actaully increase.

If this is a pen and paper proof, I would like to argue that for any element that is 1, it will be removed; and for any element that is greater than 1, it will be replaced by 3 occurences of 1, which will still be removed finally. Hence se will be empty in the end and loop terminates.

How do I turn it to codes that Dafny would agree?

Answer 1

The key is to introduce a function that I call "total potential" that computes how many iterations the loop will take to process the list. Its definition is "for every 1 in the list, add 1 to the total potential, for every non-1 in the list, add 4 to the total potential". Then, we will make the decreases clause the total potential. This way, when a 1 gets removed, the potential goes down by 1, and when a non-1 gets removed and replaced by three ones, the potential also goes down by 1.

There is some additional work to convince Dafny that the total potential actually decreases on each loop iteration. You will need a few lemmas about how the total potential relates to slicing and appending sequences.