Formal Verification Hello World
Published:
Goal: what is the meaning of formal verification ?
As a beginner, we often come across this word formally verified software, and we ponder what does it mean? In this post, we are going find out the answer of this question with the help of Coq theorem prover. Imagine you are a software developer and your project leader asks you to write a list library with an append function, which can be used in other projects, that takes two lists and returns a list, concatenation of the two input lists. In addition, the project leader also gives some specification (concrete test cases) to ensure that what they expect from your library. Given that you already have some functional programming experience under your belt, it is not a very difficult task for you. You come up with the following Coq data type to model list data structure.
Inductive List (A : Type) : Type :=
| Nil : List A
| Cons : A -> List A -> List A.
List has two constructors: (i) Nil and (ii) Cons. Nil represents (models) empty list and Cons represents a list having at least one element. For example, Cons 1 (Cons 2 (Cons 3 Nil)) represent a list of natural numbers containing 1, 2, and 3. Furthermore, we write the append function, shown below, that concatenates the two input lists as:
Fixpoint append {A : Type} (lsa lsb : List A) : List A :=
match lsa with
| Nil => lsb
| Cons hlsa tlsa => Cons hlsa (append tlsa lsb)
end.
At this point, if we were using Haskell, OCaml, Scala, or any other language, but not a theorem prover, we would have written some test cases, in addition to the test cases given by the project leader, to ensure that our append function behaves according to the expectations of the project leader. As you can see, this is not rigorous and formal because your project leader may state the requirements vaguely, may miss the corner test cases, etc. But, in this project, we are using the Coq theorem prover, so we don’t need to write test case because we can prove that the append function follows some specifications for all the possible test cases! (you would often see the word correct in the context of formal verification, but I am trying to avoid the usage of word correct and I believe the right word is specification).
Now, you have a difficult and challenging job: finding specifications for the append function! Below are the few specifications that you have come up after a long discussion with your team:
- If you append an empty list Nil in the beginning of a list u, the result should be u, i.e., (append Nil u = u).
- If you append an empty list Nil in the end of a list u, the result should be u, i.e., (append u Nil = u)
- If you have three lists u, v, and w, first appending u and v and then appending the resulting list with w should be the same as appending u with the resulting list of appending v and w, i.e., (append (append u v) w = append u (append v w)).
You write these informal specifications more formally in Coq as:
Theorem append_nil_l {A : Type} : forall (u : List A), append Nil u = u.Theorem append_nil_r {A : Type} : forall (u : List A), append u Nil = u.Theorem append_associative {A : Type} : forall (u v w : List A), append (append u v) w = append u (append v w).
Let me explain what do these formal statements mean: the append_nil_l theorem states that for any arbitrary list u, append Nil u is equal to u (if you are not familiar with quantifier, I highly recommend you getting some introductory logic book. In the mean time, you can have a look at this introduction), and same for append_nil_r. However, append_associative is an interesting case. It says that for any three arbitrary lists u, v, and w, if you first append u and v, represented as (append u v), and then you append w to it, is same as first you append v and w and then you append u to it (by the way, I just told you that list append is a monoid where the set S is A, the binary operator is append, and the identity element is Nil). Finally, if you can prove these three theorems, then you can be confident that the append function follows all the three specifications (I want to reiterate that I am avoiding the the usage of correct and using the word specification).
Conclusion:
The astute reader by now is hopefully familiar, or at least some high level idea, with formal verification. Basically, we write our programs, data structures and functions to manipulate these data structures, in Coq (or pick your any favourite theorem prover Isabelle, Lean, HOL4, PVS, etc.). Finally, we come up with some specification, which intuitively captures the notion of correctness. If we can successfully prove all the specification, then we know that our implementation follows all the specification. It is often this proof step, in my experience, that exposes many corner cases which we have never considered.
Appendix:
You can safely ignore this part because I haven’t told you anything about tactics that I am going to use to write the proofs. I will explain them in the next post, but if you have some functional programming background then check the proofs in mixed mode (program mode and tactic mode). First, I am going to write the proofs, of the above mentioned theorems, using tactics, which may be overwhelming in the beginning but once you wrap your head around it, tactics are one of the best features of Coq because you can write proofs quickly. I will also show you mixed mode (tactic and program) to construct these proofs to demonstrate that these proofs are basically a functional program, that we build internally when we write tactics. Complete Source Code
Tactic Mode
Theorem append_nil_l {A : Type} :
forall (u : List A), append Nil u = u.
Proof.
intros u.
simpl.
reflexivity.
Qed.
Theorem append_nil_r {A : Type} :
forall (u : List A), append u Nil = u.
Proof.
induction u;
simpl.
+ reflexivity.
+ rewrite IHu.
reflexivity.
Qed.
Theorem append_associative {A : Type} :
forall (u v w : List A),
append (append u v) w = append u (append v w).
Proof.
induction u;
simpl.
+ intros *.
reflexivity.
+ intros *.
rewrite IHu.
reflexivity.
Qed.
Mixed Mode (Tactic and Programming)
Theorem append_nil_l_prog {A : Type} :
forall (u : List A), append Nil u = u.
Proof.
refine (fun u => eq_refl).
Qed.
Theorem append_nil_r_prog {A : Type} :
forall (u : List A), append u Nil = u.
Proof.
refine
(fix Fn u {struct u} :=
match u with
| Nil => eq_refl
| Cons h t => _
end); simpl;
rewrite Fn;
exact eq_refl.
Qed.
Theorem append_associative_prog {A : Type} :
forall (u v w : List A),
append (append u v) w = append u (append v w).
Proof.
refine
(fix Fn u {struct u} :=
match u with
| Nil => fun v w => eq_refl
| Cons h t => fun v w => _
end); simpl;
rewrite Fn;
exact eq_refl.
Qed.