Dans l’article #1, on avait laissé un trou. Le vérificateur détectait la récursion dans fact, notait que v était borné [0, 10], puis émettait un breadcrumb :
“La profondeur est bornée par la plage déclarée, mais ce n’est pas une preuve mathématique de terminaison. Cette preuve arrivera en Phase C.”
Phase C est là. Le compilateur verbose peut maintenant prouver que certains programmes récursifs terminent — pas juste le supposer. Et quand la preuve tient, le breadcrumb disparaît.
Le problème : pourquoi prouver la terminaison ?
Un programme récursif qui ne termine pas consomme de la pile indéfiniment et finit par crasher (le fameux SIGSEGV de l’article #2). Le bounds-check empêche les entrées invalides, mais il ne prouve pas que la récursion converge vers un cas de base.
Prenons un exemple volontairement cassé :
rule bad_fact
input: n : N
output: out : number
logic:
out = if n.v == 0 then 1 else n.v * bad_fact(N { v: n.v })n.v est passé tel quel — pas n.v - 1. La récursion ne progresse jamais vers le cas de base. Avec le bounds-check, le programme ne crashera pas sur une entrée hors bornes. Mais pour v = 5, il appellera bad_fact(5) indéfiniment jusqu’au stack overflow.
Le bounds-check protège des entrées invalides. La preuve de terminaison protège de la logique invalide.
Les trois preuves de Phase C
Verbose propose trois manières de prouver la terminaison, selon la structure du programme :
flowchart TD
R[Regle recursive] --> Q{Quel type input}
Q -->|concept_group| S[structural : param]
Q -->|champ qui decroit| D[decreasing : field]
Q -->|champ qui croit| I[increasing : field]
S --> OK[Breadcrumb supprime]
D --> OK
I --> OKPreuve 1 — Structural : chaque appel traite un sous-arbre
Quand l’entrée est un type récursif (arbre, liste chaînée — déclaré via concept_group), la preuve structurelle vérifie que chaque appel récursif passe un sous-terme de l’entrée.
concept_group AST
concept Expr
variants:
Int of (value : number)
Add of (lhs : Expr, rhs : Expr)
rule eval
input: e : Expr
output: out : number
logic:
out = match e:
Int(value) => value
Add(lhs, rhs) => eval(lhs) + eval(rhs)
proofs:
termination:
structural : eLe vérificateur identifie que Add a deux champs lhs : Expr et rhs : Expr — des champs auto-référentiels (même type que l’input). Les appels eval(lhs) et eval(rhs) passent des binders issus du match qui lient ces champs. Un arbre est une structure finie ; chaque match descend d’un niveau. La récursion atteint forcément une feuille.
Preuve 2 — Decreasing : un champ numérique décroît
Pour factorial, N n’est pas un type récursif — c’est un simple record. La terminaison vient du fait que v décroît de 1 à chaque appel :
concept N
fields:
v : number [0, 10]
rule fact
input: n : N
output: out : number
logic:
out = if n.v == 0 then 1 else n.v * fact(N { v: n.v - 1 })
proofs:
termination:
decreasing : vLe vérificateur vérifie que :
vest de typeNumberavec une plage déclarée[0, 10]- L’appel récursif
fact(N { v: n.v - 1 })suit le patterninput.field - kaveck > 0
Si quelqu’un écrit fact(N { v: n.v }) (même valeur), le compilateur refuse avec un message explicite.
Preuve 3 — Increasing : un champ croît vers une borne
Le scanner scan_word avance dans un texte. La position croît au lieu de décroître :
concept ScanState
fields:
source : text [..256]
pos : number [0, 256]
rule word_length
input: s : ScanState
output: out : number
logic:
out = if s.pos >= length(s.source) then 0
else if byte_at(s.source, s.pos) >= 97
and byte_at(s.source, s.pos) <= 122
then 1 + word_length(ScanState { source: s.source, pos: s.pos + 1 })
else 0
proofs:
termination:
increasing : posLe vérificateur confirme que pos suit le pattern input.field + k. La borne max 256 garantit la terminaison.
Ce qui change dans le binaire
Rien.
La preuve est un artefact purement compile-time. Zéro octet supplémentaire. Zéro cycle de CPU. Le vérificateur vérifie la preuve, le compilateur note que la preuve existe, le breadcrumb est supprimé.
Le bounds-check (38 octets, article #2) reste — il protège des entrées invalides. La preuve de terminaison protège de la logique invalide. Les deux sont indépendants :
| Mecanisme | Protege contre | Quand | Cout |
|---|---|---|---|
| Bounds-check | Entrees hors bornes | Runtime, 38 octets | ~6 cycles |
| Preuve de terminaison | Logique qui ne converge pas | Compile-time, 0 octet | 0 cycle |
Le breadcrumb : avant et apres
Avant Phase C :
$ verbosec factorial.verbose --native fact
native: rule 'fact' is recursive (cycle through 'fact'); the declared
bound is NOT a termination proof for recursion.Apres (avec decreasing : v) :
$ verbosec factorial.verbose --native fact
[silence — compilation reussie, aucun warning]Le compilateur dit ce qu’il sait et ce qu’il ne sait pas. Quand le breadcrumb est la : “je ne sais pas prouver que ca termine.” Quand il disparait : “j’ai verifie mecaniquement.” Il n’y a pas d’etat intermediaire.
Ce qu’on a appris
-
Trois preuves, trois patterns : structural (sous-termes d’un arbre), decreasing (champ qui decroit), increasing (champ qui croit). Chacune couvre un type de recursion different.
-
La preuve est compile-time, pas runtime. Zero octet dans le binaire. Le compilateur verifie que la logique converge ; le bounds-check (separe) verifie que les entrees sont valides.
-
Le verificateur est conservateur. Il ne reconnait que des patterns simples (
field - k,field + k, binder de match). Si votre expression est plus complexe (n.v / 2), il refusera. Mieux vaut rejeter un programme valide que d’accepter un programme qui boucle. -
Le source n’a presque pas change. Pour factorial, la seule difference entre “pas de preuve” et “preuve verifiee” est une ligne :
decreasing : v. Le programme est le meme. Le binaire est le meme. Ce qui change, c’est la confiance que le compilateur a dans le programme.
Verbose est open source : github.com/verbose-org/verbose Version utilisee dans cet article : v0.6.0 Serie : “Verbose — comprendre ce qui se passe vraiment” Article precedent : #2 — 38 octets de securite