Verify Climbing Stairs

Verify LeetCode Question: 70. Climbing Stairs

The question is a counting problem. It asks in how many ways can a person reach the top of n steps when they can either take 1 or 2 steps at a time.

Implementation

Here is how we could solve this in TypeScript.

function climbStairs(n: number): number {
    let steps = new Array(n+1);
    steps[0] = 0;
    steps[1] = 1;
    steps[2] = 2;
    for(let i = 3; i <= n; i++) {
        steps[i] = steps[i-1] + steps[i-2];
    }
    return steps[n];
};

We setup a steps array to contain the count of ways to reach a step x. We begin by filling the known values for the beginning steps. After that for every given step we add at the number of ways we could have reached the previous step and the step two below our current step.

Specifying the implementation

We begin translating the problem definition to a method, and predicates (functions that return true and false for some value).

datatype Steps = One | Two

function stepSum(xs: seq<Steps>): nat {
    if xs == [] then 0 else (match xs[0] {
        case One => 1
        case Two => 2
    } + stepSum(xs[1..]))
}

ghost predicate stepEndsAt(xs: seq<Steps>, n: nat) {
    stepSum(xs) == n
}

ghost predicate allEndAtN(ss: set<seq<Steps> >, n: nat) {
    forall xs :: xs in ss ==> stepEndsAt(xs, n)
}

method climbStairs(n: nat) returns (count: nat) 
    ensures exists ss: set< seq<Steps> > :: count == |ss| && allEndAtN(ss, n)
{
}

We define the action of taking steps with a datatype Steps. Given a sequence of steps we can sum them using the stepSum function. You could just as well imagine an array of number with just 1 or 2 but using a datatype eliminates the possibility of numbers other 1 or 1 being present.

We define the stepEndsAt predicate to ask "given a sequence of steps does it end at step n?"

Then if we are given a set of different sequences of steps allEndAtN asks "do all of these sequences of steps end at step n?"

Finally, with those definitions we can return to the problem. The method climbStairs is the program we are trying to verify. The method says that given a step n then it will return a count which is equal to the size of the set of sequences of steps which all end at n. n is a natural number meaning 0 or above in Dafny.

Verifying the implementation

There are some differences between the Dafny and TypeScript solution because JavaScript, which underlies TypeScript, is very lenient with array sizes because it has dynamically sized arrays. Dafny does not so there are some additional checks to satisfy the the compiler but the behavior is the same.

method climbStairs(n: nat) returns (count: nat) 
    ensures exists ss: set< seq<Steps> > :: count == |ss| && allEndAtN(ss, n)
{
    var steps := new nat[n+1];
    steps[0] := 0;
    if n > 0 {
        steps[1] := 1;
    }
    if n > 1 {
        steps[2] := 2;
    }
    stepBaseZero();
    stepBaseOne();
    stepBaseTwo();
    if n < 3 {
        return steps[n];
    }
    // assert steps[0] == 0;
    // assert steps[1] == 1;
    // assert steps[2] == 2;
    // assert forall k: nat :: k < 3 ==> exists ss: set< seq<Steps> > :: steps[k] == |ss| && allEndAtN(ss, k);
    var i := 3;
    while i <= n 
        invariant 3 <= i <= n+1
        invariant forall k: nat :: k < i ==> exists ss: set< seq<Steps> > :: steps[k] == |ss| && allEndAtN(ss, k)
    {   
        steps[i] := steps[i-1] + steps[i-2];
        stepSetsAdd(i, steps);
        i := i + 1;
    }
    return steps[n];
}

Proving the base cases

To show the bases cases of 0, 1, and 2 satisfy our specification for the count we can define lemmas in dafny to show that steps sets exists and exactly what they are.

lemma stepBaseZero() 
    ensures exists ss: set< seq<Steps> > :: allEndAtN(ss, 0) && |ss| == 0
{
    assert allEndAtN({[]}, 0);
}

lemma stepBaseOne() 
    ensures exists ss: set< seq<Steps> > :: allEndAtN(ss, 1) && |ss| == 1
{
    assert allEndAtN({[One]}, 1);
}

lemma stepBaseTwo() 
    ensures exists ss: set< seq<Steps> > :: allEndAtN(ss, 2) && |ss| == 2
{
    assert allEndAtN({[One,One], [Two]}, 2);
}

Proving the induction

We have to show that with in the loop we maintain the count for the given step. Dafny cannot prove this automatically, so we write some lemma's to show that it is true.

As induction traditionally goes, we assume that for all steps less than i, our property was true, which is the requirements specified in the lemma. Then we show that adding those values maintains the property.

lemma stepSetsAdd(i: nat, steps: array<nat>) 
    requires i >= 2
    requires steps.Length >= i+1
    requires forall k: nat :: k < i ==> exists ss: set< seq<Steps> > :: steps[k] == |ss| && allEndAtN(ss, k)
    ensures exists sp : set< seq<Steps> > :: |sp| == steps[i-1] + steps[i-2] && allEndAtN(sp, i)
{
    var oneStepBack :| steps[i-1] == |oneStepBack| && allEndAtN(oneStepBack, i-1);
    var twoStepBack :| steps[i-2] == |twoStepBack| && allEndAtN(twoStepBack, i-2);
    var stepForward := addOne(oneStepBack);
    var stepTwoForward := addTwo(twoStepBack);
    assert forall x :: x in stepForward ==> x[0] == One;
    // assert stepForward !! stepTwoForward;
    addOneSize(oneStepBack);
    addTwoSize(twoStepBack);
    var sumSet := stepForward + stepTwoForward;
    assert |sumSet| == steps[i-1]+steps[i-2];
}

We define two helper functions plusOne, and plusTwo. In Dafny version 4 ghost functions are functions which are only used in the verification context and are not compiled to executable code. These functions add either one or two steps to a sequence and return a longer sequence. We can then define addOne and addTwo to do this for our sets of sequences.

ghost function plusOne(x: seq<Steps>): seq<Steps> {
    [One]+x
}

ghost function plusTwo(x: seq<Steps>): seq<Steps> {
    [Two]+x
}

ghost function addOne(ss: set<seq<Steps>>): set<seq<Steps>> 
    ensures forall x :: x in ss ==> plusOne(x) in addOne(ss)
    ensures addOne(ss) == set x | x in ss :: plusOne(x)
{
    set x | x in ss :: plusOne(x)
}

ghost function addTwo(ss: set<seq<Steps>>): set<seq<Steps>> 
    ensures forall x :: x in ss ==> plusTwo(x) in addTwo(ss)
    ensures addTwo(ss) == set x | x in ss :: plusTwo(x)
{
    set x | x in ss :: plusTwo(x)
}

Lastly a key insight to help Dafny verify is the the set of sequences of steps incremented by either one or two steps is the same size as the original set.

lemma UnequalSeqs<T>(xs: seq<T>, ys: seq<T>, someT: T)
    requires xs != ys
    ensures [someT]+xs != [someT]+ys
{
    if |xs| < |ys| {} else if |ys| > |xs| {}
    else if i: nat :| i < |xs| && i <|ys| && xs[i] != ys[i] {
        assert ([someT]+xs)[i+1] != ([someT]+ys)[i+1];
    }
}

lemma plusOneNotIn(ss: set<seq<Steps>>, x: seq<Steps>)
    requires x !in ss
    ensures plusOne(x) !in addOne(ss)
{
    if x == [] {
        assert [] !in ss;
        assert [One]+[] !in addOne(ss);
    }
    if plusOne(x) in addOne(ss) {
        forall y | y in ss 
            ensures y != x
            ensures plusOne(y) in addOne(ss)
            ensures plusOne(y) != plusOne(x)
        {
            UnequalSeqs(x, y, One);
            assert plusOne(y) != [One]+x;
        }
        assert false;
    }
}

lemma addOneSize(ss: set<seq<Steps>>)
    ensures |addOne(ss)| == |ss|
{
    var size := |ss|;
    if x :| x in ss {
        assert |ss - {x}| == size - 1;
        addOneSize(ss - {x});
        assert |addOne(ss-{x})| == size - 1;
        assert addOne(ss) == addOne(ss-{x}) + {[One]+x};
        assert x !in ss-{x};
        plusOneNotIn(ss-{x}, x);
        assert plusOne(x) !in addOne(ss-{x});
        assert |addOne(ss)| == |addOne(ss-{x})| + |{[One]+x}|;
    }else{

    }
}

lemma plusTwoNotIn(ss: set<seq<Steps>>, x: seq<Steps>)
    requires x !in ss
    ensures plusTwo(x) !in addTwo(ss)
{
    if x == [] {
        assert [] !in ss;
        assert [Two]+[] !in addTwo(ss);
    }
    if plusTwo(x) in addTwo(ss) {
        forall y | y in ss 
            ensures y != x
            ensures plusTwo(y) in addTwo(ss)
            ensures plusTwo(y) != plusTwo(x)
        {
            UnequalSeqs(x, y, Two);
            assert plusTwo(y) != [Two]+x;
        }
    }
}

lemma addTwoSize(ss: set<seq<Steps>>)
    ensures |addTwo(ss)| == |ss|
{
    var size := |ss|;
    if x :| x in ss {
        // assert |ss - {x}| == size - 1;
        addTwoSize(ss - {x});
        // assert |addTwo(ss-{x})| == size - 1;
        assert addTwo(ss) == addTwo(ss-{x}) + {[Two]+x};
        // assert x !in ss-{x};
        plusTwoNotIn(ss-{x}, x);
        // assert plusTwo(x) !in addTwo(ss-{x});
        assert |addTwo(ss)| == |addTwo(ss-{x})| + |{[Two]+x}|;
    }
}

Blog