How CompCert "proves" different things in its codebase

Question

In order to understand examples of formal proofs, I am interested in how CompCert applies "proof" techniques. Specifically, I am wondering what a particular example is of something CompCert "proves" in their GitHub repo, so I can get a grasp of how proofs are applied in practice (to something that is somewhat familiar, compiler technology). I have had some minimal experience with Coq so I should be able to follow along. I also have some experience with x86, so perhaps something in the x86 folder would be a good example. Or perhaps something directly to do with the C language (such as Clight), or with memory.

In x86/Asm.v, they have several Inductive definitions, which I think is a proof in itself. For example:

Inductive ireg: Type :=
  | RAX | RBX | RCX | RDX | RSI | RDI | RBP | RSP
  | R8  | R9  | R10 | R11 | R12 | R13 | R14 | R15.

Inductive instruction: Type :=
  ...

Then they have some Definition definitions:

Definition code := list instruction.

Definition is_label (lbl: label) (instr: instruction) : bool :=
  match instr with
  | Plabel lbl' => if peq lbl lbl' then true else false
  | _ => false
  end.

Wondering if this is also a "proof" of some sort since (I think) it is some sort of type.

They also have Lemma definitions, where the explicit proofs are:

Lemma is_label_correct:
  forall lbl instr,
  if is_label lbl instr then instr = Plabel lbl else instr  Plabel lbl.
Proof.
  intros.  destruct instr; simpl; try discriminate.
  case (peq lbl l); intro; congruence.
Qed.

I understand about Coq tactics, but haven't actually written any proofs myself so don't have applied knowledge.

So here we have Inductive is used in a Definition which is used in a Lemma. And then it looks like that lemma is used by other lemmas:

Lemma transl_code_label:
  forall lbl f c ep tc,
  transl_code f c ep = OK tc ->
  match Mach.find_label lbl c with
  | None => find_label lbl tc = None
  | Some c' => exists tc', find_label lbl tc = Some tc' /\ transl_code f c' false = OK tc'
  end.
Proof.
  induction c; simpl; intros.
  inv H. auto.
  monadInv H. rewrite (transl_instr_label' lbl _ _ _ _ _ EQ0).
  generalize (Mach.is_label_correct lbl a).
  destruct (Mach.is_label lbl a); intros.
  subst a. simpl in EQ. exists x; auto.
  eapply IHc; eauto.
Qed.

In this question I am wondering what a proof consists of in CompCert, given some example like the above. I would like to be able to know what I need to write a proof for my own software, by first knowing what CompCert is actually "proving", and how they are "proving it". It seems that there are types (Inductive and Definition), and then proofs (Lemma and Proof). Not sure if the Inductive/Definition things are proofs in and of themselves. Proofs traditionally are essentially just derivation trees of applying rules, but I'm not exactly sure if that is what is happening here. It seems the Coq tactics are just creating a derivation tree, correct me if I'm wrong. Then the lemma/proof is just a derivation tree (a bunch of rules applied) down to the "axioms" (definitions and inductive types). The fact that there could be an electronics error isn't accounted for (I don't think), so the proof is really of a "pure" system in some sense. So practical proofs are applied to pure systems that make some assumptions about the environment.

In the end, I'm wondering, the kind of "proof system" CompCert is. What is making it a good system of formal proofs. Knowing that, I would be able to apply "proofs" to stuff outside of CompCert but in other programming contexts. Also wondering if there is some sort of "specification" that CompCert is formally verified against, or if it is just the "model" (as in the model in model checking vs. specification).

Answer 1

I am not very sure what you are asking, and I am also not sure that you have the background to understand CompCert. It seems that you are still confused by some basic concepts in Coq.

I would suggest you start with Software Foundations. Most of your questions would be answered there.

But, basically:

• Definition and Fixpoint are like OCaml's let and let rec, respectively. They are used to define values and functions (and, of course, propositions).

• Inductive is like type in OCaml, or datatype in SML. They are used to define algebraic data types (or "inference rules").

• Prop is the sort of propositions, so Definition and Inductive that return Props are defining propositions (i.e., "proof rules"). The Definition and Inductives are not themselves proofs.

• Lemma, Theorem, Corollary, etc...are used for proofs.

• Coq is based on the Curry-Howard correspondence: a proof of the proposition $A \rightarrow B$ is a function that takes something of type $A$ and produces something of type $B$, a proof by induction corresponds to a recursive function, etc. A proof of $A = B$ is obtained by transforming both sides and applying the only constructor of the type $=$, which is Refl of x * x (not Coq syntax, but you should get it). So, all proofs by tactic actually expand into programs!

• In other words, Coq tactics are just another style of programming. You can use Definition and/or Fixpoint to write proofs, or use Proof to write programs. Of course, you should not do so; but you can.

• CompCert is indeed proved against a formal specification. Which one? The official C programming language specification! Of course, you can't really prove anything against the text of the specification, so they encoded the specification in Coq using Definitions and Inductives.

In Software Foundations, there are examples of verifying a few toy interpreters and some toy programs, as well as more serious examples of verifying algorithms like red-black tree insertions and graph coloring. It does a pretty good job of explaining what and how to prove when you are writing programs in Coq. I would suggest that you start from there.