Coq și Isabelle/HOL — Demonstrație asistată de calculator în logica de ordin superior

Ce este un theorem prover?

Un theorem prover (demonstrator de teoreme) este un instrument software care permite utilizatorului să scrie demonstrații matematice și le verifică automat, pas cu pas. Dacă un SMT solver (ca Z3) decide automat dacă o formulă e satisfiabilă, un theorem prover cere utilizatorului să ghideze demonstrația, dar garantează corectitudinea fiecărui pas.

Coq și Isabelle/HOL sunt cele mai mature și mai utilizate astfel de instrumente. Ele au fost folosite pentru a verifica:

• CompCert — un compilator C verificat formal (Coq)
• seL4 — un microkernel verificat matematic (Isabelle/HOL)
• Teorema celor 4 culori — prima demonstrație matematică verificată de calculator (Coq)
• Teorema Feit–Thompson — o demonstrație masivă în Coq

Partea 1: Coq

1.1 Ce este Coq?

Coq (dezvoltat de INRIA, Franța, din 1989) este un theorem prover bazat pe Calculul Construcțiilor Inductive (CIC) — un sistem de tipuri lambda-calcul de ordin superior.

Caracteristici fundamentale:

• Bazat pe lambda-calcul — programele și demonstrațiile sunt același lucru (Curry-Howard)
• Tipuri dependente — tipurile pot depinde de valori
• Tactici interactive — utilizatorul scrie demonstrația pas cu pas
• Extracție de cod — din demonstrație poți extrage programe OCaml/Haskell/Scheme
• Inducție structurală — definită de utilizator prin tipuri inductive

1.2 Corespondența Curry-Howard

În Coq, a demonstra o teoremă și a scrie un program sunt același lucru:

Exemplu: O demonstrație a lui $A \Rightarrow A$ e o funcție care primește un argument de tip A și returnează același argument:

Theorem identity : forall (A : Prop), A -> A.
Proof.
  intros A H.
  exact H.
Qed.
(* Echivalent cu: fun (A : Prop) (H : A) => H *)

1.3 Tipuri inductive

Baza oricărei demonstrații în Coq: tipuri inductive (definite de utilizator):

(* Numere naturale *)
Inductive nat : Type :=
  | O : nat
  | S : nat -> nat.

(* Liste polimorfe *)
Inductive list (A : Type) : Type :=
  | nil : list A
  | cons : A -> list A -> list A.

Fiecare tip inductiv generează automat:

• Principiu de inducție — pentru demonstrații prin inducție structurală
• Constructorii — modurile de a construi termeni
• Eliminatorii — match pentru a distruge termeni

1.4 Tactici fundamentale

O demonstrație în Coq se scrie folosind tactici — comenzi care transformă scopul curent în sub-scopuri mai simple:

1.5 Exemplu complet: suma primelor n numere

(* Definim o funcție pentru suma primelor n numere *)
Fixpoint sum_n (n : nat) : nat :=
  match n with
  | O => 0
  | S m => n + sum_n m
  end.

(* Definim formula inchisa: n*(n+1)/2 *)
Definition closed_form (n : nat) : nat :=
  n * (n + 1) / 2.

(* Teorema: sum_n n = closed_form n *)
Theorem sum_formula : forall n : nat, sum_n n = closed_form n.
Proof.
  induction n as [| n IH].
  - (* Cazul n = 0 *)
    simpl. reflexivity.
  - (* Cazul n = S n, cu ipoteza IH: sum_n n = closed_form n *)
    simpl.
    rewrite IH.
    unfold closed_form.
    (* Aici am nevoie de o lemă de aritmetică *)
    (* Omite detaliile aritmetice pentru simplitate *)
    admit.
Qed.

(În practică, am avea nevoie de biblioteca Arith pentru proprietăți aritmetice.)

1.6 Exemplu: corectitudinea unei funcții de căutare

Require Import List.
Import ListNotations.

(* Căutare binară pe o listă sortată *)
Fixpoint is_sorted (l : list nat) : bool :=
  match l with
  | [] => true
  | [x] => true
  | x :: y :: tl => if x <=? y then is_sorted (y :: tl) else false
  end.

(* Funcția de căutare liniară *)
Fixpoint find (l : list nat) (x : nat) : bool :=
  match l with
  | [] => false
  | h :: tl => if h =? x then true else find tl x
  end.

(* Proprietate: dacă find l x = true, atunci x apare în l *)
Theorem find_sound : forall (l : list nat) (x : nat),
  find l x = true -> In x l.
Proof.
  induction l as [| h tl IH]; intros x Hfind.
  - simpl in Hfind. discriminate Hfind.
  - simpl in Hfind. destruct (h =? x) eqn:Heq.
    + simpl. left. apply Nat.eqb_eq. exact Heq.
    + simpl. right. apply IH. exact Hfind.
Qed.

1.7 Extrația de cod

Unul dintre cele mai puternice feature-uri ale lui Coq: poți extrage cod executabil dintr-o demonstrație:

Extraction Language OCaml.
Extraction "sum_n.ml" sum_n.

Rezultatul e un program OCaml corect prin construcție — demonstrația garantează corectitudinea.

1.8 CompCert: cazul emblematic

CompCert (Leroy et al., 2009) e un compilator C verificat formal în Coq. Include:

• Parser C (sursă → Clight)
• 17 faze de optimizare și transformare
• Demonstrație că semantica se păstrează la fiecare fază
• Generator de cod pentru PowerPC, ARM, x86, RISC-V

Impact practic: CompCert elimină o întreagă clasă de bug-uri de compilator. În teste de fuzzing, GCC și Clang generează cod incorect în ~0.1% din cazuri; CompCert — 0%.

Partea 2: Isabelle/HOL

2.1 Ce este Isabelle/HOL?

Isabelle (Paulson, Cambridge, 1986) e un theorem prover generic — nu e legat de o singură logică. Isabelle/HOL e logica de ordin superior (Higher-Order Logic) instanțiată peste Isabelle.

Caracteristici fundamentale:

• Bazat pe HOL — o logică de ordin superior cu tipuri polimorfe
• Automation puternică — tacticile auto, simp, blast, metis
• Sledgehammer — unealtă care cheamă SMT solvere (Z3, cvc5) automat
• Locurile — demonstrații declarative, lizibile
• Cod generat — din specificații Haskell/ML

2.2 Diferența fundamentală între Coq și Isabelle

2.3 Exemplu: suma primelor n numere în Isabelle

theory SumForm
imports Main
begin

fun sum_n :: "nat ⇒ nat" where
  "sum_n 0 = 0" |
  "sum_n (Suc n) = (Suc n) + sum_n n"

theorem sum_formula: "sum_n n = n * (n + 1) div 2"
  apply (induction n)
   apply auto
  done

end

Observație: apply auto înlocuiește ceea ce în Coq ar necesita mai multe tactici și leme aritmetice. Automation-ul lui Isabelle e semnificativ mai puternic.

2.4 Stilul Isar (declarativ)

Isabelle permite un stil de demonstrație lizibil, asemănător cu o demonstrație matematică clasică:

theorem sum_formula_isar: "sum_n n = n * (n + 1) div 2"
proof (induction n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  have "sum_n (Suc n) = (Suc n) + sum_n n" by simp
  also have "... = (Suc n) + (n * (n + 1) div 2)" using Suc.IH by simp
  also have "... = (Suc n) * (Suc n + 1) div 2" by auto
  finally show ?case .
qed

2.5 Sledgehammer — automation cognitivă

theorem hard_theorem: "⟦ prime p; p dvd a * b ⟧ ⟹ p dvd a ∨ p dvd b"
  sledgehammer  (* cheamă Z3, cvc5, E, Vampire automat *)

Sledgehammer trimite problema la multiple SMT solvere și prover-e externe, apoi traduce demonstrația găsită înapoi în Isabelle. E unul dintre cele mai impresionante feature-uri de automation din orice theorem prover.

2.6 seL4: cazul emblematic

seL4 (Klein et al., NICTA, 2009) e un microkernel de ~12.000 linii de C/ASM, verificat matematic complet în Isabelle/HOL.

Ce s-a demonstrat:

(* Abstractizare: specificația formală a kernelului *)
definition kernel_spec :: "state ⇒ syscall ⇒ state ⇒ bool" where
  "kernel_spec s syscall s' ≡ ..."

(* Implementarea C e o rafinare a specificației *)
theorem refinement: "C_implementation ⊑ kernel_spec"
  apply (refinement_transfer)
  done

Statistici:

• 12.000 linii de C
• 200.000 linii de demonstrație Isabelle
• 20 persoane-ani
• 0 bug-uri găsite post-verificare în codul verificat

2.7 LCF — arhitectura de încredere

Isabelle (ca și Coq) folosește arhitectura LCF (Logic for Computable Functions):

Nucleul logic e foarte mic (~1000 linii de ML). Orice demonstrație, indiferent cât de complexă, trece prin nucleul care verifică fiecare pas.

Asta înseamnă că:

• Dacă ai un bug într-o tactică, maxim nu se aplică — nu poate genera o demonstrație incorectă
• Doar nucleul trebuie să fie corect
• Poți adăuga tactici noi fără să compromiți corectitudinea

Partea 3: Comparație sistematică

3.1 Tabel comparativ

3.2 Când alegi Coq?

• Ai nevoie de tipuri dependente (ex: vectori cu lungimea în tip)
• Vrei să extragi cod din demonstrație (CompCert, CertiKOS)
• Lucrezi cu matematică fundamentală (teoria grupurilor, topologie)
• Ai nevoie de inducție puternică (tipuri inductive generale)

Exemplu de tip dependent în Coq:

(* Vectori: liste cu lungimea codificată în tip *)
Inductive vec (A : Type) : nat -> Type :=
  | vnil : vec A 0
  | vcons : A -> forall n : nat, vec A n -> vec A (S n).

(* Funcția head e sigură — nu poți apela pe vector gol *)
Definition vhead {A n} (v : vec A (S n)) : A :=
  match v with
  | vcons x _ _ => x
  end.

Acest cod e sigur prin construcție — nu ai nevoie de verificări run-time pentru head pe listă goală.

3.3 Când alegi Isabelle/HOL?

• Ai nevoie de automation puternică (proiecte industriale mari)
• Demonstrațiile trebuie să fie lizibile (Isar)
• Vrei să verifici programe imperative (framework-ul AutoCorres)
• Ai nevoie de Sledgehammer pentru productivitate

3.4 Exemple de automation comparativ

Problema: Demonstrați că $\forall n, 2^n > n$ pentru $n \in \mathbb{N}$.

În Coq:

Theorem two_pow_gt_n : forall n : nat, 2^n > n.
Proof.
  induction n as [| n IH].
  - simpl. lia.
  - simpl.
    assert (2^n >= 1) by (destruct n; simpl; lia).
    lia.
Qed.

În Isabelle/HOL:

theorem "2^n > n"
  apply (induction n)
   apply auto
  done

Isabelle rezolvă aceeași problemă cu auto — automation-ul e semnificativ mai puternic.

Partea 4: Aplicații practice

4.1 Verificare de compilator (CompCert — Coq)

Sursă C (CompCert)
  → Clight (C redus)
  → C#minor
  → Cminor (stack alocat)
  → CminorSel (selecție de instrucțiuni)
  → RTL (Register Transfer Language)
  → LTL (Linearization)
  → Mach (Machina abstractă)
  → ASM (cod mașină)

Fiecare fază e demonstrată în Coq că păstrează semantica.

4.2 Verificare de kernel (seL4 — Isabelle)

(* Proprietatea de izolare: un task nu poate accesa memoria altui task *)
theorem isolation:
  "⟦ current_thread = thread_a; 
     Memory.of thread_b = Some mem_b; 
     cap_a ⊑ thread_a ⟧
   ⟹ cap_a ⊑ mem_b"

4.3 Verificare de algoritmi criptografici

Biblioteca HACL* (Verified Cryptographic Library) e verificată în Coq și F*:

(* Specificația: criptarea AES-GCM *)
Theorem aes_gcm_correct :
  forall (k : key) (iv : nonce) (aad : msg) (pt : msg),
    decrypt k iv aad (encrypt k iv aad pt) = Some pt.
Proof.
  (* Demonstrația acoperă toate cazurile *)
  ...
Qed.

Codul extras din Coq e folosit în Firefox (NSS), WireGuard, Python (cryptography).

Partea 5: Limitări

5.1 Costul demonstrațiilor

Raportul e de obicei între 5:1 și 20:1, ceea ce face verificarea formală impracticabilă pentru majoritatea proiectelor comerciale.

5.2 Stack-ul de încredere (TCB)

Verificarea acoperă doar ce e demonstrat. Nu acoperă:

• Hardware-ul (CPU, RAM, cache)
• Compilatorul (verificat doar în CompCert)
• Bootloader-ul
• Nucleul lui Coq/Isabelle însuși (doar ~1000 linii trebuie de încredere)

5.3 Specificația poate fi greșită

O demonstrație arată că implementarea respectă specificația. Dacă specificația e greșită, programul e incorect dar "verificat".

5.4 Scalabilitate

Sisteme moderne (Linux: ~30M linii) nu pot fi verificate complet cu tehnologia actuală. Soluția: verificare incrementală și pe componente critice.

Concluzie

Coq și Isabelle/HOL sunt instrumente mature care au demonstrat că verificarea formală funcționează în practică — de la compilatoare (CompCert) la kerneluri (seL4) la criptografie (HACL*).

Recomandare: Începe cu Isabelle/HOL dacă vrei să verifici programe mari. Începe cu Coq dacă ești interesat de fundațiile matematice sau de tipuri dependente.

Pentru aprofundare, vezi articolele despre Z3 (SMT solver — complementar theorem prover-elor) și Lambda Calculus (fundația teoretică).

Referințe

• Bertot, Y. & Castéran, P. Interactive Theorem Proving and Program Development. Springer, 2004.
• Nipkow, T., Paulson, L. & Wenzel, M. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, 2002.
• The Coq Development Team. The Coq Proof Assistant Reference Manual. INRIA, 2024.
• Klein, G. et al. seL4: Formal Verification of an OS Kernel. SOSP, 2009.
• Leroy, X. Formal Verification of a Realistic Compiler. CACM, 2009.
• Chlipala, A. Certified Programming with Dependent Types. MIT Press, 2013.
• Paulson, L. Isabelle: A Generic Theorem Prover. Springer, 1994.
• Wenzel, M. The Isabelle/Isar Reference Manual. 2024.