Preuves Coq

Sommaire

Le dossier proof/ contient 69 fichiers Coq, environ 20 000 lignes et aucun Admitted. Il formalise des propriétés du parsing, du broadcasting, de l'IR, du runtime, des optimisations et du pipeline CFG/SSA.

Ces preuves portent sur des modèles alignés avec le code Rust. Elles ne prouvent ni l'exécution du binaire complet, ni Tree-sitter, ni Cranelift. Chaque fichier .v indique les définitions Rust qu'il modélise ; cet alignement reste une obligation de maintenance.

make proof

Si cette commande passe, Coq a vérifié les théorèmes du modèle courant.

Un programme prouvé correct n'a pas de bugs. Il a des hypothèses.

Pourquoi formaliser ces propriétés

Un test confirme un nombre fini d'exemples. Une preuve peut couvrir une famille entière : toute profondeur de pile admise par le modèle, toute expression d'une grammaire donnée ou tout cycle de copies parallèles. Catnip réserve donc Coq aux invariants qui se prêtent à un énoncé mathématique :

  • bijections et round-trips d'encodage ;
  • précédence et associativité ;
  • déterminisme et préservation sémantique ;
  • bornes de pile et de frames ;
  • propriétés de dominance et de forme SSA ;
  • cohérence de hash, de portée et de frontière de valeur.

Le glue code, l'I/O et les interactions avec Python restent couverts par les tests Rust/Python et les différentiels VM/AST.

Une preuve couvre tous les cas de son modèle. Le mot important se trouve à la fin de la phrase.

Carte du corpus

Chaque entrée donne la famille, ses fichiers représentatifs et les contrats couverts :

  • Syntaxe — GrammarProof.v, CatnipAddMulProof.v, CatnipExprProof.v et CatnipExprMonoProof.v : précédence, associativité, non-ambiguïté du modèle et monotonie du carburant.
  • Broadcasting — CatnipDimensional.v, CatnipDimensionalProps.v, CatnipNDRecursion.v et CatnipBroadcastOverload.v : composition, déterminisme, shapes et mémoïsation ND.
  • IR — CatnipIR.v : bijection des opcodes, arité et classes d'opérations.
  • Scopes et fonctions — CatnipScopeProof.v, CatnipPatternProof.v et CatnipFunctionProof.v : shadowing, push/pop, patterns déterministes, binding et trampoline TCO.
  • Optimisations IR — familles CatnipStrengthRed*, CatnipBluntCode*, CatnipDCEFlatten*, CatnipConstFold*, CatnipTailRecLoop* et CatnipPurity* : préservation sémantique des passes vivantes.
  • Liveness et dominance — CatnipVarSet.v, familles CatnipLiveness* et CatnipDominanceProof.v : fixpoint, DSE, chemins CFG et propriétés de dominance.
  • Construction SSA — CatnipCFGSSABase.v et CatnipCFGSSACorrectness.v : single assignment, placement des phis, CSE, GVN, LICM et terminaison DSE.
  • Destruction SSA — CatnipParallelCopyProof.v, CatnipTrivialPhiProof.v, CatnipRegionMergeProof.v et CatnipDestructionBridge.v : copies parallèles, phis triviaux et reconstruction des régions.
  • Valeurs VM — familles CatnipNanBox*, CatnipValueClass*, CatnipBoundary*, CatnipPluginBoundary* et CatnipOwnership* : encodage, promotion entière, classes de tags et sûreté des frontières.
  • Machine virtuelle — familles CatnipVM*, CatnipArithProof.v et CatnipPureFrameProof.v : effets de pile, sauts, frames, liaison d'arguments et arithmétique Python.
  • Objets et dispatch — familles CatnipMRO*, CatnipStruct*, CatnipTrait* et CatnipOpDesugar* : linéarisation C3, héritage, résolution de méthodes et désucrage des opérateurs.
  • Infrastructure — preuves du cache, du freeze et du runtime avancé : FIFO/LRU/TTL, atomicité, hash et contrats inter-runtime.
  • Delta dataflow — proof/delta/ : compaction des deltas et homomorphismes de map, filter et concat.

Les fichiers CatnipOptimProof.v, CatnipLivenessProof.v, CatnipCFGSSAProof.v, CatnipVMProof.v et CatnipMROProof.v sont des façades Require Export. Ils offrent un import stable, mais n'ajoutent pas une seconde preuve du même contrat.

Syntaxe

Le parseur formel est distinct de Tree-sitter. Il encode une grammaire réduite et prouve notamment :

  • la précédence de * sur + ;
  • l'associativité gauche des opérateurs concernés ;
  • la tour or > and > not > comparaison > addition > multiplication du modèle ;
  • le désucrage correct des comparaisons chaînées ;
  • la stabilité du résultat quand on augmente le carburant.

GrammarProof.v établit la non-ambiguïté d'une CFG minimale par unicité du rendement des arbres. CatnipExprProof.v couvre la tour d'expressions et CatnipExprMonoProof.v isole la preuve de monotonie des douze fonctions mutuellement récursives.

Douze fonctions mutuellement récursives. Coq n'a pas bronché. Le reviewer, si.

Ces résultats ne transforment pas Tree-sitter en programme vérifié. Ils explicitent les propriétés attendues de grammar.js et rendent leur dérive visible lors de la mise à jour du modèle.

Sémantique dimensionnelle et ND

Les preuves dimensionnelles traitent le broadcast comme un relèvement structurel d'une fonction sur des conteneurs. Elles couvrent la loi identité, la composition, la fusion d'évaluations et la préservation des shapes. Les variantes avec surcharge d'opérateurs conservent les mêmes invariants sous les conditions de pureté du modèle.

La ND-récursion est bornée par carburant. nd_eval_deterministic établit que deux évaluations avec le même état donnent le même résultat ; memo_coherence relie l'évaluation mémoïsée au calcul direct. La preuve de terminaison reste partielle : elle porte sur les calculs qui terminent dans le modèle borné, pas sur toute fonction utilisateur.

Optimisations IR

Les cinq passes IR vivantes ont chacune un modèle de réécriture :

  • strength reduction ;
  • blunt code ;
  • dead code elimination ;
  • block flattening ;
  • constant folding.

Les théorèmes principaux établissent que l'évaluation avant et après passe coïncide dans le périmètre du modèle. Les gardes *_untouched sont aussi importantes : elles prouvent qu'une règle retirée ou invalide ne se déclenche plus. Par exemple, les identités algébriques sensibles aux effets ou au type dynamique ne sont pas réintroduites par une réécriture plus large.

CatnipDCEFlattenProof.v prouve aussi l'idempotence de l'aplatissement et la préservation par composition de passes. Son modèle n'inclut ni affectations ni match ; les contraintes de portée et la conservation du scrutinee restent testées sur le runtime réel.

CatnipTailRecLoopProof.v ne prouve pas qu'une passe de conversion arbitraire est active. Il formalise l'invariant vivant du trampoline : un signal terminal peut changer de fonction, ce qui couvre l'auto-récursion et les cycles mutuels.

Chaque règle appliquée a une preuve, et certaines règles absentes en ont une aussi. L'absence est un état du compilateur.

CFG, SSA et destruction

La construction SSA suit l'approche de Braun et al. (2013). Le corpus prouve la définition unique, l'ordre définition-usage, la présence des phis aux frontières requises et les contrats des passes inter-blocs.

Sortir de SSA demande de convertir les phis en copies sur les arêtes. Ces copies sont sémantiquement parallèles : pour un swap, exécuter naïvement a = b; b = a perd une valeur. CatnipParallelCopyProof.v prouve qu'un temporaire frais casse tout cycle et préserve les emplacements extérieurs. dead_copy_invisible justifie l'omission d'une copie dont la destination n'est plus vivante.

CatnipTrivialPhiProof.v relie un phi dont tous les opérandes coïncident à sa définition survivante. CatnipRegionMergeProof.v formalise la recherche forward-only du merge d'un if : suivre une back-edge pourrait faire entrer la reconstruction dans une boucle sœur. CatnipDestructionBridge.v ferme le raccord entre les deux modèles : le lot séquentialisé produit, pour chaque phi du join, la valeur de l'environnement initial.

Références conceptuelles : Briggs et al. (1998) et Boissinot et al. (2009) pour les copies parallèles ; Braun et al. pour la construction SSA.

Valeurs et runtime

Les preuves VM sont réparties par invariant :

  • CatnipNanBoxProof.v couvre l'injectivité des tags modélisés, le round-trip et la promotion SmallInt → BigInt ;
  • CatnipValueClassProof.v partitionne les tags en scalaires, index et pointeurs ;
  • CatnipBoundaryProof.v garantit qu'une frontière de bits bruts ne fabrique pas une valeur pointeur ;
  • CatnipPluginBoundaryProof.v étend le contrat aux canaux de l'ABI plugin ;
  • les modules CatnipVM*.v couvrent effets de pile, séquences, frames, IP et cibles de saut ;
  • CatnipArithProof.v prouve la relation a = q*b + r et les règles de signe du modulo plancher.

Les nombres exacts d'opcodes ou de tags appartiennent à ces modèles et peuvent évoluer avec le code. Les théorèmes de bijection et les tests de synchronisation sont les gardes ; les recopier dans plusieurs paragraphes de documentation créait une seconde source de vérité.

Les familles MRO et structures couvrent la linéarisation C3, la précédence locale, la terminaison de super, la fusion des champs et la résolution déterministe des méthodes. Les preuves de désucrage relient chaque couple (symbole, arité) à un nom de méthode et à l'opcode correspondant, y compris le dispatch inverse.

Technique : récursion à carburant

Coq exige une récursion structurellement décroissante. Un parseur descendant consomme des tokens, mais ce décroissement n'est pas toujours visible dans sa définition. Les modèles utilisent donc un entier fuel :

Fixpoint parse_expr (fuel : nat) (ts : list token)
  : option (expr * list token)

Chaque appel récursif reçoit le prédécesseur du carburant. À zéro, le parseur échoue. fuel_mono établit que si une entrée réussit avec f, elle réussit avec le même résultat pour tout f' >= f. Les exemples calculés par vm_compute fournissent un témoin, puis la monotonie généralise le résultat.

Le parser de production ne fonctionne pas avec ce carburant. Il s'agit d'un dispositif de preuve, pas d'une limite runtime.

Construire et auditer

make proof
make proof-clean
make proof-scan

make proof compile les sources listées dans proof/_CoqProject. make proof-scan refuse Admitted, Abort, les axiomes et certains imports classiques qui court-circuiteraient le niveau de garantie attendu.

Lorsqu'un invariant Rust change, le fichier Coq correspondant et son commentaire d'alignement doivent changer dans le même lot. Une preuve verte contre un ancien modèle ne valide pas le nouveau code.

Références