Preuves Coq

Vérification mécanisée de fragments de Catnip : grammaire, précédence, modèle dimensionnel, IR, scopes, pattern matching, fonctions/TCO, et passes d'optimisation.

TL;DR

9 fichiers Coq dans proof/ prouvent des invariants structurels et sémantiques couvrant le parsing, le broadcasting, la résolution de scopes, le pattern matching, le trampoline TCO et 4 passes d'optimisation IR. Si make proof passe, les théorèmes sont validés mécaniquement. Ces preuves portent sur des modèles formels alignés avec le code Rust, pas sur l'exécution du runtime en production. L'alignement est maintenu explicitement dans les commentaires en tête de chaque fichier .v.

Un parseur sans preuve est un parseur qui ne sait pas encore qu'il a tort.

Pourquoi des preuves formelles

Catnip utilise tree-sitter pour parser, et tree-sitter fait son travail correctement. Mais la grammaire déclarée dans grammar.js encode des invariants implicites : la précédence de * sur +, l'associativité gauche de -, le fait que not lie plus fort que and. Ces propriétés ne sont vérifiées par aucun test unitaire classique -- un test vérifie qu'un cas marche, pas que tous les cas marchent.

Les fichiers dans proof/ couvrent quatre axes :

• Syntaxe -- invariants de parsing de la grammaire (grammar.js) via un parseur à descente récursive formalisé.
• Sémantique -- propriétés structurelles du modèle dimensionnel (broadcast, ND-récursion).
• Runtime -- IR (59 opcodes), scopes (shadowing, isolation), pattern matching (6 types, déterminisme), fonctions (binding, trampoline TCO, tail detection).
• Optimisations -- 4 passes IR (strength reduction, blunt code, DCE, block flattening) avec correction sémantique et idempotence.

Coq vérifie chaque étape de raisonnement : si make proof passe, les propriétés sont vraies.

Ce ne sont pas des preuves du runtime lui-même. L'alignement entre les modèles Coq et le code Rust est maintenu manuellement -- les commentaires en tête de chaque fichier .v citent les définitions correspondantes.

Vue d'ensemble

A. Preuves syntaxiques

Prouvent précédence, associativité, non-ambiguïté et chaînage pour le modèle de parsing.

B. Preuves sémantiques

Prouvent cohérence, confluence, terminaison partielle et universalité du modèle dimensionnel.

C. Modèle IR

Formalise la structure de l'IR et ses invariants structurels.

D. Preuves runtime

Prouvent les invariants des composants d'exécution : scopes, pattern matching, fonctions.

E. Preuves d'optimisation

Prouvent la correction de 4 passes IR (algébriques pures, sans modèle de store).

A. Preuves syntaxiques

GrammarProof.v

Modèle minimal d'une CFG (S -> A B, A -> "a", B -> "b") avec trois résultats :

Soundness des arbres : tout arbre de dérivation produit une séquence de terminaux dérivable depuis le non-terminal racine (tree_sound). La preuve construit la chaîne de réécritures explicitement.

Génération : la grammaire engendre bien [a; b] (generates_example_ab), par application successive des trois productions.

Non-ambiguïté structurelle : pour chaque non-terminal, il n'existe qu'une seule forme d'arbre (grammar_unambiguous_S). La preuve procède par destruction dépendante -- Coq élimine structurellement toute alternative.

Non-ambiguïté via yield : formulation standard en théorie des langages -- si deux arbres pour le même non-terminal produisent la même chaîne de terminaux, les arbres sont identiques (grammar_unambiguous). La preuve passe par yield_injective (injectivité de la fonction yield), puis congruence. La complétude est aussi prouvée : tout arbre pour S engendre [ta; tb] et dérive via la relation (yield_S_unique, tree_complete_S).

Ce fichier ne modélise pas directement le parseur Catnip. Il pose le vocabulaire (dérivation, arbre, ambiguïté) utilisé implicitement par les deux fichiers suivants.

CatnipAddMulProof.v

Formalise le fragment arithmétique de grammar.js :

_additive       -> additive | _multiplicative
additive        -> _additive ("+" | "-") _multiplicative   (left)
_multiplicative -> multiplicative | _exponent
multiplicative  -> _multiplicative ("*" | "/" | "//" | "%") _exponent (left)

Le modèle Coq garde + et * avec atomes parenthésés. Cinq fonctions mutuellement récursives (parse_expr, parse_expr_tail, parse_term, parse_term_tail, parse_factor) implémentent un RDP classique.

Précédence et associativité (exemples concrets) :

• Précédence (precedence_example) : n + n * n parse comme n + (n * n), pas (n + n) * n
• Associativité gauche (left_assoc_add_example) : n + n + n parse comme (n + n) + n
• Parenthèses (paren_example) : (n + n) * n parse comme (n + n) * n -- les parenthèses forcent la structure

Le déterminisme (parse_expr_deterministic) est trivial : deux appels sur la même entrée produisent le même résultat, par réécriture et inversion.

Monotonie du fuel (fuel_mono) : si le parseur réussit avec un fuel f, il réussit avec le même résultat pour tout f' >= f. Le théorème est un 5-conjonction prouvé par induction sur le fuel, avec lemmes de dépliage (parse_expr_unfold, etc.) pour exposer la structure récursive. Les corollaires parse_expr_mono et parse_full_mono fournissent les projections utiles.

Résultats indépendants du fuel : avec la monotonie, les propriétés de précédence et d'associativité sont généralisées à tout fuel suffisant (precedence_general : forall fuel, fuel >= 5 -> ...). La tactique solve_fuel_general automatise la preuve : fournir un témoin concret, puis lia.

Soundness : une relation de parsing inductive (parses_expr, parses_expr_tail, etc.) avec 8 constructeurs miroir la structure du parseur. Le théorème parser_sound (5-conjonction par induction sur le fuel) prouve que si le parseur retourne Some, le résultat satisfait la relation. Le corollaire parse_full_sound combine soundness et consommation complète de l'entrée.

CatnipExprProof.v

Étend le modèle au tour de précédence complet de Catnip :

bool_or > bool_and > bool_not > comparison > additive > multiplicative > atom

Douze fonctions mutuellement récursives (6 niveaux de précédence, chacun avec sa tail function, plus parse_bool_not et parse_atom). Les tokens couvrent les 4 opérateurs arithmétiques (+, -, *, /), les 6 opérateurs de comparaison (<, <=, >, >=, ==, !=), les 3 opérateurs booléens (and, or, not), les parenthèses et les littéraux.

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

Précédence arithmétique : * lie plus fort que + (mul_over_add), - est associatif gauche (sub_left_assoc).

Précédence booléenne : not > and > or vérifié sur not n < n or false qui parse comme (not (n < n)) or false (not_and_or_precedence). Les comparaisons lient plus fort que and (cmp_over_and).

Parenthèses : forcent la structure à travers tous les niveaux (paren_override_bool).

Opérateurs de comparaison : les 6 opérateurs sont testés individuellement (comparison_ops_examples) -- chacun produit le bon noeud AST.

Chaînage : n < n <= n parse comme (n < n) <= n syntaxiquement (comparison_chain_example). Le fichier inclut aussi un modèle sémantique : eval_comp_chain évalue une chaîne de comparaisons comme une conjonction. Le théorème chain_two_ops_desugars_to_and prouve que a op1 b op2 c est équivalent à (a op1 b) and (b op2 c).

Monotonie du fuel (fuel_mono) : même structure que CatnipAddMulProof.v, mais avec 12 conjonctions (un par fonction mutuellement récursive). Les 6 opérateurs de comparaison sont traités uniformément dans parse_comparison_tail par semi-colon tactique. Corollaires : parse_bool_or_mono, parse_full_mono.

Desugaring des chaînes : extract_chain extrait récursivement la base et les opérateurs d'un AST de comparaisons imbriquées à gauche. Trois propriétés structurelles prouvées : la chaîne n'est jamais vide (extract_chain_nonempty), la base n'est jamais elle-même une comparaison (extract_chain_base_non_cmp), et les non-comparaisons donnent None (extract_chain_non_cmp). La correction sémantique est prouvée pour les chaînes à 1 et 2 opérateurs (chain_desugar_correct_single, chain_desugar_correct_two).

B. Preuves sémantiques

CatnipDimensional.v

Formalise le modèle dimensionnel de Catnip : le domaine de valeurs (Scalar nat | Coll (list Val)), le broadcast (.[op]), le filtrage (.[if p]), et la ND-récursion (@@).

Six groupes de résultats :

Cohérence (lois de foncteur) : broadcast_map satisfait identité (v.[id] = v) et composition (xs.[f].[g] = xs.[g . f]). Le broadcast préserve la longueur des collections et fixe le topos vide.

Confluence : l'évaluation des expressions broadcast est totale et déterministe (eval_deterministic). Si une expression évalue vers v1 et v2, alors v1 = v2. La fusion de broadcasts chaînés est prouvée (eval_fusion).

Terminaison partielle : la ND-récursion à carburant (nd_eval) est monotone (plus de carburant ne change pas le résultat), déterministe, et termine quand une mesure mu décroît strictement à chaque appel récursif (nd_partial_termination). La cohérence de la mémoisation est prouvée séparément (memo_coherence).

Universalité : toute opération elementwise (qui préserve la longueur et commute avec l'extraction par index) sur une collection est nécessairement Coll (map op xs) -- c'est-à-dire broadcast_map op (universality). Il n'existe pas d'autre façon de lifter une opération aux collections avec ces propriétés (broadcast_unique). Pour les collections plates, le broadcast est entièrement déterminé par son noyau scalaire (broadcast_minimal_flat). Le broadcast Catnip est caractérisé comme le foncteur libre sur les collections plates sous les axiomes d'elementwise-ness.

# Le broadcast est un foncteur libre (loi de composition)
# Pour des fonctions pures f et g :

# F(id) = id
data.[x => x] == data

# F(f ∘ g) = F(f) ∘ F(g)
# viva la composition
data.[g].[f] == data.[x => f(g(x))]

Propriétés non triviales : lois structurelles prouvées par induction :

• Filter-map pullback (filter_map_pullback) : filtrer après mapper = mapper après filtrer avec le prédicat tiré en arrière p . f. Généralise filter_map_commute sans hypothèse d'invariance.
• Absorption de filtres (filter_filter) : deux filtres successifs = un filtre avec conjonction des prédicats.
• Pullback broadcast-filter-map (broadcast_filter_map) : corollaire au niveau Val.
• Masque booléen (mask_select) : all-true = identité (mask_all_true), all-false = vide (mask_all_false), commutation avec map (mask_map_commute), borne de longueur (mask_length_le).
• Homomorphisme de liste (broadcast_concat) : le broadcast distribue sur la concaténation -- fondation algébrique de la parallélisation.
• Sémantique un-niveau (broadcast_shallow, broadcast_two_levels) : le broadcast opère à exactement un niveau de profondeur ; le broadcast récursif nécessite un emboîtement explicite.
• Homomorphisme de monoide (fold_broadcast_exchange) : quand f distribue sur op et fixe z, f commute avec le fold. Corollaire : fold sur un broadcast = fold avec accumulateur composé (fold_broadcast_map).

Algèbre de pipelines : formalise les pipelines comme séquences d'opérations PMap / PFilt et prouve trois résultats :

• Fusion complète (map_chain_fusion) : toute chaîne de n broadcasts maps se réduit à un seul broadcast avec la fonction composée. Sûre (préserve la sémantique) et complète (n quelconque).
• Equivalence transformationnelle : trois règles de réécriture prouvées correctes -- map;map fusionne (equiv_map_map), map;filter se réordonne en filter;map (equiv_filter_map_swap), filter;filter s'absorbe (equiv_filter_filter).
• Normalisation (pipeline_normalization) : tout pipeline mixte de maps et filters sur une collection se réduit à une forme canonique filter;map. Deux pipelines qui ont la même forme normale sont équivalents (normalization_sound).

C. Modèle IR

CatnipIR.v

Formalise les 59 opcodes de catnip_rs/src/ir/opcode.rs comme un inductif Coq IROpCode avec 59 constructeurs. Chaque opcode reçoit une numérotation via opcode_to_nat : IROpCode -> nat (bijection 1..59) et nat_to_opcode inverse.

Injectivité et roundtrip : opcode_to_nat_injective (numérotation injective), opcode_roundtrip (aller-retour nat -> opcode -> nat = identité). Prouvés par énumération exhaustive.

Classification : prédicats is_literal, is_op, is_pattern, is_collection, is_comparison_op, is_control_flow_op, is_arithmetic_op avec propriétés de disjointness (literal_not_op, control_flow_not_arithmetic).

IRPure : inductif représentant les noeuds IR (IRInt, IRFloat, IRBool, IRStr, IRNone, IROp), avec ir_size (taille structurelle), ir_op (constructeur par opcode + args), ir_binop (spécialisation binaire).

Ce fichier sert de fondation importée par CatnipOptimProof.v.

D. Preuves runtime

CatnipScopeProof.v

Modélise le système de scopes de catnip_rs/src/core/scope.rs. Un environnement (env) est un string -> option Z, un scope est une pile de frames avec opérations push_scope / pop_scope.

Lookup/set : env_lookup_set_same (lire ce qu'on vient d'écrire), env_lookup_set_other (écrire ne touche pas les autres variables). Même résultats liftés au scope : scope_set_lookup_same, scope_set_lookup_other.

Push/pop : scope_push_pop (push puis pop = identité pour les variables pré-existantes), scope_push_preserves_lookup (push ne touche pas les variables existantes).

Shadowing : scope_shadowing (une variable dans un frame enfant masque le parent), scope_pop_restores (pop restaure la valeur d'avant le push), scope_shadow_restore (composition des deux).

Frames isolées : modèle étendu (scope_ex) avec flag d'isolation par frame. scopeex_isolated_shadow (les frames isolées ne voient pas les variables du parent), scopeex_isolated_restore (le pop restaure correctement même avec isolation).

CatnipPatternProof.v

Modélise les 6 types de patterns de catnip_rs/src/core/pattern.rs. Chaque pattern est un inductif (PatWild, PatLit, PatVar, PatOr, PatTuple, PatStruct) avec match_pattern : Pattern -> Value -> option Bindings.

Wildcard : matche toujours, ne capture rien (wildcard_always_matches, wildcard_no_bindings).

Variable : matche toujours, capture la valeur (var_always_matches, var_captures_value, var_single_binding).

Literal : matche si et seulement si les valeurs sont égales (literal_matches_equal, literal_rejects_different).

OR : premier match gagne (or_first_match_wins), singleton = pattern nu (or_singleton), wildcard dans un OR attrape tout (or_with_wildcard).

Tuple/Struct : mismatch de longueur = échec (tuple_length_mismatch), type mismatch = échec (struct_type_mismatch).

Dispatch : match_cases_first_wins (premier case qui matche est sélectionné), match_cases_guard_fail (si le guard échoue, on passe au case suivant), match_cases_wildcard_catches_all (un wildcard en dernier case attrape tout).

Déterminisme : match_pattern_deterministic et match_cases_deterministic -- le résultat du match est unique.

CatnipFunctionProof.v

Modélise les fonctions et le trampoline TCO de catnip_rs/src/core/registry/functions.rs et catnip_rs/src/core/nodes.rs.

Binding de paramètres : bind_params prend une liste de specs (name, default) et une liste d'arguments, produit un environnement. bind_params_exact_length (si autant d'args que de params, chaque param reçoit l'arg correspondant), bind_params_all_defaults (0 args = tous les defaults), bind_params_missing_required (param sans default et sans arg = erreur).

Trampoline TCO : modèle fuel-bounded trampoline fuel scope body. Le body produit soit un Normal v (terminaison), soit un Tail args (tail call = rebind + continuer). trampoline_normal_terminates (un Normal termine immédiatement), trampoline_tail_continues (un Tail rebind les params et relance), trampoline_fuel_monotone, trampoline_two_steps, trampoline_three_steps (exemples multi-itérations).

Scope : trampoline_preserves_scope_depth -- le trampoline ne modifie pas la profondeur du scope.

Tail detection : tail_position_produces_tailcall (si le TCO est actif et la position est tail, un appel récursif produit un TailCall), non_tail_produces_normal (en position non-tail, l'appel est normal), tco_disabled_produces_normal (si TCO désactivé, pas de TailCall).

E. Preuves d'optimisation

CatnipOptimProof.v

Modélise 4 passes d'optimisation IR et prouve leur correction. Source de vérité : catnip_rs/src/semantic/strength_reduction.rs, blunt_code.rs, dead_code_elimination.rs, block_flattening.rs.

Le fichier définit un arbre d'expressions Expr (Const, BConst, Var, BinOp, UnOp, IfExpr, WhileExpr, Block, MatchExpr) avec un évaluateur partiel eval_expr et réutilise IROpCode de CatnipIR.v.

Strength reduction (strength_reduce : Expr -> Expr) : 20 théorèmes individuels couvrant les identités multiplicatives (x * 1 = x, x * 0 = 0), exponentielles (x^2 -> x*x, x^1 = x, x^0 = 1), additives (x + 0 = x, x - 0 = x), division (x / 1 = x), et booléennes (x && True = x, x || False = x, x && False = False, x || True = True). Correction sémantique prouvée pour les cas arithmétiques.

Blunt code (simplify_blunt : Expr -> Expr) : double négation (not not x = x), inversion de comparaisons (not (a < b) = a >= b) avec preuve d'involution de invert_cmp, simplification booléenne (x == True = x), idempotence (x && x = x, x || x = x), complément (x && not x = False, x || not x = True). Les preuves de complément utilisent des lemmes de taille structurelle (expr_eqb_not_self : x n'est jamais structurellement égal à UnOp Not x).

Dead code elimination (eliminate_dead : Expr -> option Expr) : if True { t } else { f } -> t, if False -> f, while False { body } -> eliminated, Block [] -> eliminated, Block [e] -> e. Correction sémantique via eval_expr.

Block flattening (flatten_block : Expr -> Expr) : aplatit les blocs imbriqués (Block [s1, Block [s2, s3], s4] -> Block [s1, s2, s3, s4]). Distributivité sur append (flatten_stmts_app). Idempotence (flatten_stmts_idempotent, flatten_block_idempotent) prouvée via un lemme intermédiaire : la sortie de flatten_stmts ne contient jamais de Block au top-level (flatten_stmts_output_no_blocks).

Composition : compose_passes (fold_left), preserves_eval (une passe préserve la sémantique), compose_preserves_eval (la composition de passes qui préservent la sémantique préserve la sémantique), compose_two_idempotent (conditions d'idempotence pour la composition de deux passes).

Les 6 passes restantes (constant folding/propagation, copy propagation, CSE, dead store elimination, tail recursion to loop) nécessitent un modèle de store et sont hors scope.

Technique : récursion à carburant

Coq exige que toute récursion termine. Un RDP ne termine pas structurellement sur sa liste de tokens -- la tail function consomme des tokens mais Coq ne le voit pas. Les parseurs dans CatnipAddMulProof.v et CatnipExprProof.v utilisent le pattern fuel-based recursion :

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

Le paramètre fuel décroît strictement à chaque appel récursif (destruct fuel as [|fuel'], appel sur fuel'). Quand le fuel est épuisé, le parseur retourne None. Coq accepte la définition parce que fuel est un nat qui décroît structurellement.

En pratique, les théorèmes par réflexivité (Proof. vm_compute; reflexivity. Qed.) calculent le résultat exact du parseur sur une entrée concrète -- Coq exécute le parseur et vérifie que le résultat correspond.

Monotonie : le théorème fuel_mono (prouvé dans les deux fichiers de parsing) établit que si le parseur réussit avec un fuel f, il réussit avec le même résultat pour tout f' >= f. Cela élimine la dépendance aux constantes de fuel spécifiques (32, 64) : les résultats quantifiés universellement (forall fuel, fuel >= k -> ...) sont dérivés en fournissant un témoin concret puis en appliquant la monotonie via lia. La technique utilise des lemmes de dépliage (parse_*_unfold : parse_*(S f) ts = ...) prouvés par reflexivity, qui exposent la structure récursive pour que les hypothèses d'induction soient applicables.

Le parseur réel (tree-sitter) ne fonctionne pas par fuel mais par la structure de la grammaire PEG. Le fuel est un artefact de la preuve, pas du runtime.

Build

make proof          # Compile les fichiers .v, vérifie toutes les preuves
make proof-clean    # Supprime les artefacts Coq (.vo, .glob, Makefile.coq)

Prérequis : Coq installé (coqc, coq_makefile). Le fichier proof/_CoqProject liste les sources.

Références

• The Coq Proof Assistant -- assistant de preuve utilisé
• Braun et al. 2013 -- Simple and Efficient Construction of Static Single Assignment Form (utilisé dans le pipeline SSA de Catnip, ARCHITECTURE)
• grammar.js -- grammaire tree-sitter source de vérité, citée en tête de chaque fichier .v