The Theorem Holds for the Wrong Function

The previous post proved, for every finite list, that reversing twice gives back the list. Here is another function with the same property:

def revId {α : Type} (xs : List α) : List α := xs

theorem revId_twice {α : Type} (xs : List α) :
    revId (revId xs) = xs := rfl

revId returns its input. It reverses nothing, and the theorem holds for it, with a one-word proof. Lean is correct to accept it. Doing nothing twice does give back the list.

So rev_twice was never a proof that rev reverses. It was a proof of the sentence I wrote down, and the sentence was weaker than what I meant. That is the first of three limits, and none of them is specific to this toy.

Limit one: the statement

The same weakness was in the tests all along. The round-trip property from the first post passes for the identity function in both languages:

// Wrong on purpose: returns its input.
func revId(xs []int) []int {
	return xs
}

func TestIdentityAlsoPasses(t *testing.T) {
	rule := func(xs []int) bool {
		return slices.Equal(
			revId(revId(xs)), xs)
	}
	if err := quick.Check(rule, nil); err != nil {
		t.Fatal(err)
	}
}

A statement that pins the behaviour down says where each element ends up: the result has the same length, and position i holds what was at position length - 1 - i. Here it is in C#, run against RevId, which like the Go function above returns its argument:

var mirrored =
    from xs in lists.ForAll()
    let a = xs.ToArray()
    let b = RevId(a)
    select a.Length == b.Length
        && Enumerable.Range(0, a.Length)
            .All(i => b[i] == a[a.Length - 1 - i]);

mirrored.Check();

Against the identity function, Hedgehog 2.0.4 reports this, with the line that gives the seed for a rerun left out:

*** Failed! Falsifiable (after 1 test and 9 shrinks):

Generated values:
  [-100; -99]

Two different elements are the smallest list on which “unchanged” and “reversed” disagree, and shrinking found it.

On the Lean side, the lemma from the previous post already does this job. rev_append says rev (xs ++ ys) = rev ys ++ rev xs. For the identity function that would claim [1, 2] = [2, 1], so it cannot be proved. The helper turned out to say more about reversing than the headline theorem did.

Moving from tests to proofs did not remove the need to ask whether the statement is the right one. It raised the price of asking late.

Limit two: the thing it is about

rev_twice is about a Lean definition over mathematical lists. The code that runs is this:

static int[] Rev(int[] xs)
{
    var ys = (int[])xs.Clone();
    Array.Reverse(ys);
    return ys;
}

Nothing connects the two. The C# method works on a machine array with a 32-bit length, calls a library routine and allocates memory. The Lean definition does none of that. The proof would be untouched if the C# method were replaced by one that throws.

There are three honest ways to connect them, in rising order of cost:

Test the running code against the proved definition. The Lean function becomes the oracle for a property test or a fuzzer. This shows agreement on the inputs tried, and it is cheap.
Run the proved code itself, by compiling the Lean definition and calling it. Then the compiler and runtime are trusted instead.
Model the C# or Go semantics, including machine integers, and prove the real function equal to the definition. This is the only one that earns the word “verified” for the client code, and it is a project, not an afternoon.

Machine integers deserve their own mention. Lean’s Nat never overflows. A sum that wraps around, or a conversion between integer types that changes the value, simply does not exist in a model written with Nat. A proof over Nat is silent about the exact place such a bug lives.

Limit three: writing it in Lean

Lean is also a programming language, and a program written in it is not proved by being written in it. Take the proved function and add logging:

def revLogged (xs : List Nat) : IO (List Nat) := do
  IO.println s!"input: {xs}"
  pure (rev xs)

def twiceLogged (xs : List Nat) : IO (List Nat) := do
  let ys ← revLogged xs
  revLogged ys

For [10, 20, 30] this prints two lines and returns [10, 20, 30]. The returned list is restored. The two writes still happened. rev_twice says nothing about what was printed, whether printing can fail, or whether those values should be in a log at all. Claims about effects need their own specification and their own proof.

The same holds for the rest of the language. Each of these is ordinary Lean and each sits outside what a theorem about rev covers:

partial def accepts a function without a termination argument.
xs[i]! indexes without a bounds proof and panics at run time when the index is out of range.
sorry closes any goal. #print axioms on a theorem shows whether one is hiding underneath it.
@[extern] and @[implemented_by] swap a definition for other code that the proofs never looked at.
Time and memory are not part of the statement. A proved function can still be made to run for an hour.

What a proof covers

A proof establishes its statement, about its definitions, under its assumptions. Within that it is complete in a way no test is, and I would take one over a thousand green runs. Outside that it says nothing.

So when someone tells me a piece of code is formally verified, I ask four things:

What is the statement, in one sentence? Would a wrong implementation also satisfy it?
What is it a statement about: the code that runs, or a model of it? If a model, what ties the two together?
What does it assume? Which axioms, which unproved parts, which compiler and runtime?
What is outside it? I/O, resource use, timing, everything upstream of the function.

None of this argues for skipping proofs. It argues for spending them where the answers are good: small, pure pieces with a statement short enough to check by eye, such as an offset calculation, a parser for a fixed format, or a state transition. There the proved definition also gives every implementation the same oracle to test against. The tests, the properties and the fuzzer keep doing what a proof does not: running the real code on real inputs.

The last post in this series applies all three to a real bug.