Comment compcert «prouve» différentes choses dans sa base de code

Question

Pour comprendre Exemples de preuves formelles, Je suis intéressé par la façon dont Compcert Applique des techniques de "preuve". Plus précisément, je me demande quel est un exemple particulier de quelque chose que CompCert "prouve" dans leur repo github, afin que je puisse comprendre comment les preuves sont appliquées dans la pratique (à quelque chose qui est quelque peu familier, la technologie du compilateur). J'ai eu une expérience minimale avec le COQ, je devrais donc pouvoir suivre. J'ai aussi de l'expérience avec x86, donc peut-être que quelque chose dans le dossier x86 serait un bon exemple. Ou peut-être quelque chose directement à voir avec la langue C (comme Allumage), ou avec Mémoire.

Dans x86 / asm.v, ils ont plusieurs Inductive Définitions, ce qui, je pense, est une preuve en soi. Par exemple:

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

Inductive instruction: Type :=
  ...

Alors ils ont un peu Definition Définitions:

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.

Je me demande si c'est aussi une "preuve" d'une sorte puisque (je pense) que c'est une sorte de taper.

Ils ont aussi Lemma définitions, où le explicite Les preuves sont:

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.

Je comprends Tactiques de coq, mais je n'ai pas réellement écrit de preuves, donc je n'ai pas appliqué de connaissances.

Alors ici nous avons Inductive est utilisé dans un Definition qui est utilisé dans un Lemma. Et puis il semble que ce lemme soit utilisé par d'autres lemmes:

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.

Dans cette question, je me demande ce qu'une preuve consiste à CompCert, étant donné un exemple comme celui ci-dessus. Je voudrais pouvoir savoir ce dont j'ai besoin pour rédiger une preuve pour mon propre logiciel, en sachant d'abord ce que CompCert "prouve" et comment ils "le prouvent". Il semble qu'il y ait les types (Inductif et définition), puis preuves (Lemme et preuve). Je ne sais pas si les choses inductives / définies sont des preuves en elles-mêmes. Les preuves sont traditionnellement simplement des arbres de dérivation de l'application des règles, mais je ne sais pas exactement si c'est ce qui se passe ici. Il semble que les tactiques CoQ créent simplement un arbre de dérivation, corrigez-moi si je me trompe. Ensuite, le lemme / preuve n'est qu'un arbre de dérivation (un tas de règles appliquées) vers les "axiomes" (définitions et types inductifs). Le fait qu'il puisse y avoir une erreur électronique n'est pas pris en compte (je ne pense pas), donc la preuve est vraiment d'un système "pur" dans un certain sens. Des preuves pratiques sont donc appliquées aux systèmes purs qui font certaines hypothèses sur l'environnement.

En fin de compte, je me demande, le type de compcert "Système de preuve" est. Ce qui en fait un bon système de preuves formelles. Sachant cela, je serais en mesure d'appliquer des «preuves» à des trucs en dehors de CompCert mais dans d'autres contextes de programmation. Je me demande également s'il existe une sorte de "spécification" avec laquelle CompCert est officiellement vérifié, ou si c'est juste le "modèle" (comme dans le modèle dans la vérification du modèle par rapport aux spécifications).