6.2.1. Ce qu'un rejet dit🔗

Quatre choses, et la dernière est ce qui rend les trois premières utilisables : l'obligation non déchargée, énoncée dans le vocabulaire de la source et non dans celui du solveur ; sa localisation ; le compte de ressource consommé ; et l'état du solveur à l'épuisement. De cette forme suit une propriété que le développeur peut exiger.

6.2.2. Ce qu'un rejet propose, et pourquoi il n'y a que trois voies🔗

Le solveur reçoit exactement trois choses : une formule, des indices, une borne de ressource. Une obligation qu'il ne décharge pas ne peut donc être secourue qu'en agissant sur l'une des trois — découper l'obligation, fournir un indice, relever la borne. Il n'y a pas de quatrième voie, et ce n'est pas une limite d'imagination : c'est la clôture de ce dont la procédure dispose. Le raisonnement est celui que le chapitre 1 tient pour les trois strates du jugement — trois entrées, trois recours, et aucune quatrième place à inventer.

Les deux premières voies emploient ce que le document possède déjà : le découpage est une écriture, et les indices invariant, witness et lemma sont soumis au test par propriétés décrit ci-dessus. La troisième porte une contrainte, et elle est structurelle plutôt que stylistique : le budget relevé doit être écrit dans la source. S'il vivait dans une configuration, la reproductibilité que le théorème 66 établit se perdrait aussitôt — le message dépendrait d'un fichier que la source ne mentionne pas, et l'objectif de compilation reproductible deviendrait inatteignable.

6.2.3. Comment le coût se voit avant le rejet🔗

Un profil de vérification par obligation, inspectable comme les grades le sont. Le budget cesse alors d'être un couperet pour devenir une mesure, et une mesure visible est un profileur de preuve : le développeur voit quelles obligations coûtent, comme il voit aujourd'hui ce qu'une structure alloue.

Une conséquence en découle, qui n'est pas affaire d'outillage. Le profil doit être disponible sur les compilations qui réussissent, et pas seulement sur celles qui échouent. Un profil réservé à l'échec n'apprendrait le coût qu'au moment où il est devenu fatal, ce que P3 refuse : une abstraction dissimulerait son coût de vérification jusqu'au dernier instant. C'est le postulat, et non une préférence d'ergonomie, qui commande ici la disponibilité permanente.

6.2.4. Ce que devient une obligation non déchargée🔗

Elle se rend comme un trou typé. Le chapitre 3 (§3.2) pose déjà le trou comme le terme le moins précis pour un type donné, et la complétion par narrowing comme sa réponse ; une obligation non déchargée en est un cas. Le compilateur rend alors la contrainte que le trou doit satisfaire au lieu d'un refus, et le rejet devient un dialogue.

Une distinction achève ce point, faute de quoi on croirait la décision de rejeter revenue. Le rejet reste terminal au niveau de l'artefact — aucun binaire n'est produit, et rien de ce qui a été arbitré n'est défait. Il cesse de l'être au niveau de la session d'édition, où le trou permet de continuer à travailler sur un programme incomplet. La frontière entre l'erreur et l'incomplétude s'efface pour l'éditeur sans s'effacer pour le compilateur, et les deux exigences qui semblaient s'opposer tiennent ensemble.

6.2.5. Sur quoi ces quatre points reposent🔗

Ce document exige de lui-même que toute affirmation d'ergonomie dise si elle repose sur un effet mesuré, une préférence esthétique ou une contrainte structurelle, et cette exigence vaut ici aussi.

Aucun de ces cinq points ne repose sur un effet mesuré, et aucun n'en a besoin : ce sont des conséquences de l'appareil. Mais ce que ce chapitre ne peut pas établir est qu'un développeur placé devant ces messages s'en sorte mieux qu'avec d'autres. Cette question est empirique, elle appelle un protocole, et le domaine est saturé d'affirmations qui n'en ont jamais reçu. Le protocole existe et n'attend aucun prototype ; sa conduite est la seule chose qui manque à cette section.

Toutes les composantes du jugement sont désormais établies. C'est seulement à ce titre que la compilation peut réécrire le terme : toute réécriture doit se justifier par un argument qui lui est propre, syntaxique ou fondé sur le modèle mémoire ; leur formulation comme isomorphismes naturels dans C relève de l'obligation P1b. Quatre familles s'y rangent.

• L'adjonction curry/uncurry et l'isomorphisme de Yoneda du chapitre 2 (§2.4) en fournissent deux instances.

• La déforestation et la fusion de boucles éliminent les structures intermédiaires.

• La saturation par égalité explore un graphe de réécritures borné par un grade.

• La défonctionnalisation et l'inlining statique des effets (chapitre 2, §2.3) achèvent d'effacer toute indirection restante. Les projections de Futamura, réservées aux fonctions pures de couche 3 dont la terminaison est déjà prouvée, spécialisent un programme par évaluation partielle sans jamais risquer d'en changer le sens.

L'une de ces réécritures illustre ce que la composante \mathcal{E} achète concrètement. La curryfication ne s'optimise pas sûrement dans un langage ordinaire : décider si l'on peut regrouper les arguments d'une fonction partiellement appliquée suppose de savoir si l'évaluation d'une expression produira un effet, et l'expérience d'une bibliothèque écrite avec soin est qu'on ne le sait souvent pas [16]. Chez K7PL, la question ne demande aucune analyse : le jugement porte la réponse, et une expression d'effet neutre est reconnue comme telle par lecture de son type. Un obstacle documenté à l'optimisation devient une conséquence du jugement, et c'est le genre de bénéfice qu'une composante d'effet rend sans qu'on l'ait ajoutée pour lui.

Deux réécritures appellent une correction du même ordre, et dans les deux cas c'est le grade qui la porte. L'intégration d'abord : ce chapitre en fait une exception à la décroissance — elle ne retire une indirection qu'en dupliquant un corps — et en conclut que sa terminaison exige d'être budgétée. Le budget est inutile sur le fragment qui compte. N'intégrer que les fonctions appelées une seule fois donne un système rétrécissant, dont la mesure décroît par construction, normalisable en temps linéaire et confluent, de sorte que le choix de l'algorithme n'affecte pas la qualité du code final [17]. Or « appelée une seule fois » est ce que la composante d'usage du grade déclare : là où un compilateur ordinaire a besoin d'une analyse pour l'établir, le jugement gradué la porte. Le budget se restreint donc au fragment hors grade, et la confluence est acquise sur le reste — ce qui retire l'obligation de justifier un ordre d'intégration.

La défonctionnalisation ensuite, où deux énoncés sont confondus en un. Qu'elle soit un isomorphisme naturel établit sa transparence sémantique, et ce chapitre en tire implicitement que son résultat est bon. La transparence vaut de la transformation ; la qualité du résultat dépend d'un choix que l'isomorphisme ne détermine pas, l'unité de spécialisation — une fonction d'ordre supérieur employée avec deux arguments fonctionnels distincts se spécialise en deux fonctions distinctes, et il faut décider si c'est ce qu'on veut [18]. L'argument de transparence est conservé ; ce qui ne l'est pas est la conclusion de qualité qu'on en tirait.

Deux mécanismes de cette phase ont un compte rendu attesté. Les opérations d'effet et leurs gestionnaires compilent par le style à passage de capacités combiné au passage de continuations itéré, l'idiome que ce document possède déjà — une capacité de couche 1 étant un canal linéaire. La technique est générale : elle engendre du code dans tout langage à fonctions de première classe, sans hypothèse sur la cible, avec des accélérations mesurées sur les langages existants à gestionnaires ou à opérateurs de contrôle [19]. Le comptage de références, que la couche 1 emploie là où le partage est gradué, n'est pas davantage un expédient d'implantation à côté de la théorie. La relation entre la correction du typage linéaire et celle d'une interprétation par comptage de références est établie au niveau d'abstraction exact dont un abaissement a besoin : assez bas pour exprimer le partage et la copie, assez haut pour ne rien dire de la disposition mémoire [20].

Une difficulté propre à ce document doit être ajoutée ici, et elle vient de son choix de fondation plutôt que de sa mise en œuvre. La théorie quantitative des types marque le jugement d'un indicateur binaire — effacé ou présent — de sorte que l'effaçabilité d'une abstraction se lit sur le jugement. La théorie graduée, qui la généralise, remplace cet indicateur par une modalité !_q A. Elle gagne en équations définitionnelles, et elle perd précisément cela : il n'est plus apparent qu'une abstraction de type \Pi^q x{:}A.B sera employée à l'exécution ou non, ce qui rend l'effacement des fermetures de fonction difficile [21]. Le coût est donc localisé et il tombe exactement sur la phase décrite ci-dessus. Il ne remet pas en cause le choix de la gradation : la théorie quantitative ne saurait porter les quatre composantes du grade. Mais il oblige à dire que l'effaçabilité d'une fermeture se décide ici par la composante d'usage et non par lecture du jugement — une décision qui est un travail d'analyse là où la théorie quantitative n'en demandait aucun.

Deux précisions rendent cette décision moins arbitraire qu'elle n'en a l'air. La première est que l'effaçabilité au grade nul n'est pas une définition mais un lemme, démontré dans une sémantique à tas instrumentée : deux configurations initiales qui ne diffèrent que par l'affectation de variables graduées zéro produisent des résultats identiques [22]. Le résultat va d'ailleurs au-delà du zéro, et c'est ce qui sert ici : est inutilisable tout grade s pour lequel la contrainte q + 1 \le s est insatisfiable. La classe des ressources effaçables se définit donc par une contrainte du semi-anneau et non par une valeur particulière, ce qui donne à la phase d'effacement un critère décidable plutôt qu'un cas d'espèce.

La seconde est qu'une quatrième conception de l'effacement existe, que ce document n'a pas retenue et dont il doit dire pourquoi. L'annotation y vit au jugement, et la règle d'application la compose par une rencontre plutôt que par la multiplication d'un semi-anneau — l'argument n'étant retenu que si le terme entier l'est et si l'application l'est [23]. Elle traite en outre le filtrage et les motifs forcés, que les autres conceptions laissent de côté. Son interaction avec les univers, elle, se règle en une phrase de ses auteurs : la stratification des univers y est orthogonale au propos, et les implantations sont attendues d'apporter la leur. C'est aussi la position de ce document, et pour la même raison — l'annotation est portée par le jugement, non par la sorte du type —, de sorte que l'interaction ne se produit tout simplement pas.

Elle se produit ailleurs, et la même source dit où : les systèmes qui modélisent l'effacement indirectement, par un univers séparé ou par l'irrélevance, en héritent les limitations, et une partie du calcul inutile cesse d'être effaçable — un programme normalement linéaire pouvant alors s'exécuter en temps exponentiel. Le cas d'école est celui d'un univers réservé aux propositions, où les indices d'une famille de types, qui sont ce que ce document manipule, ne s'effacent pas.

La forme que prendrait un abaissement à types préservés est en revanche connue, et elle est instructive parce qu'elle défait une évidence. Défonctionnaliser dans un cadre dépendant ne consiste pas à remplacer la flèche par un type de données — cette voie, qui fonctionne du simplement typé au polymorphe, échoue en présence de dépendance. Ce qui fonctionne est de remplacer l'abstraction par une étiquette de première classe dans un calcul à contexte double : un contexte de types comme d'ordinaire, et un contexte de définitions d'étiquettes qui associe à chaque étiquette le télescope de ses variables libres, son type et son corps. Deux contraintes le rendent sain, et elles sont sévères : les types peuvent mentionner les étiquettes, jamais l'inverse ; et le corps d'une étiquette se type dans le contexte des étiquettes précédentes, de sorte qu'aucune étiquette ne se référence elle-même. Une boucle infinie devient ainsi mal typée — non par une analyse de terminaison, mais parce que sa signature est mal portée. Ce document a besoin de cette forme au moment où sa Phase 6 défonctionnalise sous des types dépendants pragmatiques, et il n'a pas d'autre voie connue.

Le terme optimisé descend enfin vers MLIR puis LLVM : les tableaux de couche 3 vers memref.alloc, les automates du chapitre 4 vers le dialecte K7PL.FSM. Les correspondances de disposition du chapitre 4 (théorème 36) rendent cette génération de code directe dans le domaine de ce théorème — les tampons de couche 3 vers Arrow, les segments de couche 2 vers Cap'n Proto, pour les scalaires primitifs —, une transposition en O(n) étant requise dès qu'une liste de structures est en jeu. L'édition de liens qui referme le pipeline purge tout bloc de spécification — doctests, assertions comptime — sauf en mode +introspect, garantie que le DAG de dépendance rend structurelle plutôt que déclarative (ERR-TOP-003). Le binaire résultant, adressé par le condensat BLAKE3 de son AST normalisé plutôt que par un numéro de version, identifie par un seul et même condensat deux programmes dont l'écriture diffère mais dont les arbres coïncident après normalisation — la dépendance ne se rompt jamais silencieusement. La normalisation décide ici une égalité syntaxique canonique, et rien de plus : deux programmes de même sens dont les arbres normalisés diffèrent reçoivent deux adresses, l'équivalence sémantique n'étant pas décidable.

Un mode +dev n'exécute que les trois premières phases, plus une version allégée de la Phase 4, quand un mode +release seul engage les phases 5 à 7. Ce cache, comme le reste du pipeline, s'appuie sur ce même hachage pour ne recompiler que ce qui a changé. En production, le remplacement d'un acteur ne repasse jamais par ce pipeline : l'orchestrateur substitue directement l'image compilée par échange de pointeur, draine l'ancien acteur, et rejoue le journal Cap'n Proto pour reconstituer l'état exact — le JIT, lui, reste exclusif au REPL interactif.

Deux choses doivent être dites de cette descente, et la première défait une crainte que le document laissait planer. On suppose volontiers qu'une discipline de ressource s'efface au passage vers une représentation de bas niveau, faute d'une cible capable de la porter. Ce n'est pas le cas : il existe une extension typée de WebAssembly où le type d'une fonction est polymorphe sur les emplacements mémoire, les tailles, les types et les qualificateurs — c'est-à-dire sur les annotations de linéarité elles-mêmes [24]. La couche 1 n'aurait donc pas à abandonner sa discipline pour atteindre une cible portable, et la visée déclarée de cette extension est la situation de la passerelle du chapitre 4 : faire coexister du code sûr et du code étranger sans que le premier perde ses garanties. La même famille de travaux porte les gestionnaires d'effets jusqu'à cette cible [25], ce qui referme le second bout du même trajet.

La seconde est une réserve sur le choix d'infrastructure, et elle vise ce document plutôt qu'un tiers. Écrire un dialecte de types linéaires pour une infrastructure dont le système de types est faible coûte cher, et ce n'est pas la seule voie disponible. Une représentation intermédiaire fondée sur le lambda-calcul et les types dépendants, extensible à tout niveau par des greffons qui prennent en charge l'optimisation et l'abaissement de leurs propres axiomes, porte un grade sans qu'il faille écrire un dialecte [26]. Ce document a choisi son infrastructure sans que la comparaison ait été faite, et le dire est plus honnête que de présenter ce choix comme allant de soi. Ce qui le justifie tient à la maturité de l'outillage et non à une supériorité technique établie.

Cet abaissement appelle un énoncé que le document n'a nulle part, et son absence n'est pas une lacune de présentation. La stabilité du typage par réduction énoncée au chapitre 3 couvre l'évaluation et l'abaissement, mais sans grade ; la préservation graduée du §4.7 (théorème 48) porte les grades, mais ne couvre que l'évaluation. Rien, entre les deux, n'établit que descendre vers MLIR préserve ce que le chapitre 1 a posé — et c'est le trajet qui relie les deux bouts de ce document.

La forme de l'énoncé manquant est en revanche connue, et la chose a été poussée loin ailleurs : la compilation séparée a été vérifiée jusqu'au format d'exécutable lui-même [27]. La chaîne peut donc être démontrée correcte jusqu'au fichier objet, ce qui déplace la question de l'édition de liens : elle n'est pas de savoir si un éditeur externe est évitable, mais ce que coûte de le vérifier. Ce document ne paie pas ce coût et doit le dire.

Sa difficulté mérite en revanche d'être rapportée, car ce document la rencontrera au même endroit et pour la même raison. Elle tient à deux vues du liage qui ne se recouvrent pas. À l'étage abstrait, un programme est une application partielle des identifiants vers les définitions : le lieur est insensible à l'ordre et peut réarranger à sa guise. À l'étage concret, les définitions sont fondues en sections atomiques suivant un ordre particulier, et le lieur les concatène comme des boîtes noires — l'ordre y décide du résultat. La commutativité entre liage et compilation, sur laquelle repose toute la compilation séparée vérifiée, casse à la transition entre les deux.

La solution retenue est celle qui coûte le moins, et sa forme est le vrai acquis pour ce document. La voie naïve consisterait à donner à l'étage abstrait la vue concrète, après quoi la commutativité devient évidente. Elle a deux prix, nommés par les auteurs : le liage de tous les étages se trouve contraint par la manière dont se lient des fichiers objets, et le cadre de compilation séparée comme ses preuves demandent une lourde retouche. La voie légère introduit à la place une équivalence syntaxique entre programmes et démontre qu'elle commute avec les deux sortes de liage, ce qui permet de transiter de l'un à l'autre sans toucher à aucune preuve existante.

Ce que ce document en retient dépasse le liage, et c'est ce qui rend cette lecture utile ici. L'écart entre un étage insensible à l'ordre et un étage qui en dépend est celui qu'il rencontre deux fois. Une première entre l'espace de noms, sous-catégorie large sans ordre (chapitre 4, §4.5), et les sections de l'abaissement. Une seconde entre un contexte qui est une application finie et le contexte ordonné qu'une discipline d'échange restreint imposerait (chapitre 3, §3.1). Dans les deux cas, la leçon est la même et elle est méthodologique : ne pas concrétiser l'étage abstrait, mais poser une équivalence et démontrer qu'elle commute des deux côtés.

Reste le point propre au grade, et il n'est pas acquis. Aucune de ces vérifications ne porte sur un langage dont le jugement compte les usages~; ce qui transporte est la forme de l'énoncé et la méthode de pontage, non un résultat sur les grades. Écrire que la méthode transporte est donc exact, écrire que le résultat transporte serait faux. Un obstacle plus ancien se tient d'ailleurs en amont de celui-là, et il a un nom : l'équivalence par les noms contre l'équivalence par la structure, compliquée par la générativité — une instance de module engendrant des types nouveaux. Le problème est bien posé depuis longtemps et se traite sans estampilles, ce qui importe ici parce que le hachage par lequel ce chapitre identifie ses unités est précisément une estampille [28]. Ce que ce document adopte reste le hachage, pour ce qu'il donne par ailleurs — le cache et l'équivalence sémantique de deux programmes syntaxiquement distincts —, mais il ne peut plus se présenter comme la seule voie.

La distinction qui commande cet énoncé est celle qu'établit la littérature sur la compilation vérifiée : préserver le comportement et être pleinement abstrait ne sont pas la même exigence [8], et c'est la première qui est en jeu ici.

Ce théorème n'est pas démontré, et le projet se donne pour objectif de le démontrer : la préservation graduée de bout en bout est une revendication déclarée, non une réserve à abandonner. Le chemin n'en dénature pas la portée : la preuve se conduit passe par passe, sur le fragment dont les fonctions d'ordre supérieur sont monomorphisées et inlinées avant l'émission, puis s'étend à mesure que la défonctionnalisation quantitative le permet. Tant qu'elle n'est pas conduite, l'énoncé reste une conjecture et aucune prose ne le dit acquis. RMQ 59. Son absence était invisible tant que deux énoncés voisins passaient pour un seul. Il est énoncé parce que son absence restait invisible tant que la stabilité du chapitre 3 et la préservation du §4.7 passaient pour deux formulations de la même chose. La première est plus large sur ce qu'elle couvre, la seconde plus fine sur ce qu'elle porte : leur intersection laisse l'abaissement gradué sans énoncé.

L'état de l'art doit être donné avec ses statuts, car ils diffèrent. La littérature fournit la forme de la règle que cet énoncé devra porter : dans un calcul défonctionnalisé quantitatif, l'usage total d'une étiquette est la somme des usages de chaque contexte, chacun multiplié par l'usage désigné de son argument — soit \sum_i q_i \Gamma_i, qui est la forme que \boxtimes généralise. Mais les deux moitiés n'ont pas le même statut : la défonctionnalisation dépendante est établie et publiée, tandis que sa version quantitative est présentée comme une conjecture dont les preuves sont annoncées et non faites [21]. La forme est donc connue et le résultat ne l'est pas. Ce document n'a ni à s'appuyer sur ce qui n'existe pas, ni à ignorer que la forme est disponible : il énonce son obligation en sachant quelle règle elle devra satisfaire.

S'il tient, la garantie graduée traverse le compilateur et le binaire produit porte ce que le source promettait. S'il tombe, le grade s'arrête à la sortie du vérificateur, et toute borne de coût annoncée dans une interface cesse de valoir du code exécuté.

Avant cet abaissement final, l'AST aplati — table des symboles, graphe d'appel, annotations de type et de coût — reste lui-même exportable sous forme de tableaux Arrow columnaires, selon un schéma versionné qui en garantit la stabilité. Cette version n'est pas un simple numéro. Chaque enregistrement déclare l'espace réservé à son bloc racine, de sorte qu'un lecteur d'une version antérieure franchit sans le comprendre ce qu'une version ultérieure y a ajouté. Le mécanisme est éprouvé par les encodages binaires à schéma, où la longueur de bloc déclarée est ce qui permet de décoder un message dont le gabarit a été étendu depuis [29].

L'en-tête d'un artefact K7PL porte à cette fin trois champs : un identifiant de schéma, qui désigne la forme d'AST attendue ; une version, qui en donne la révision ; et la longueur du bloc racine, qui borne l'espace réservé aux champs de cette révision. Un lecteur d'une révision antérieure lit les champs qu'il connaît, puis se déplace de la longueur déclarée pour trouver la suite, sans avoir à comprendre ce qui a été inséré entre-temps.

Une limite l'accompagne, et elle est stricte : ce qui peut être sauté ne peut jamais être ce qui est vérifié. Le mécanisme convient à un artefact que l'on transporte, non à une dérivation que l'on contrôle ; la re-vérification que décrit l'annexe D porte sur l'AST entier, jamais sur les seuls champs qu'un lecteur donné sait lire. Cette exigence n'est pas un théorème mais une règle, et elle s'énonce par ce qu'elle interdit~: un vérificateur qui rencontre un identifiant de schéma ou une révision qu'il ne connaît pas rejette l'artefact, au lieu d'en franchir les champs inconnus. Le mécanisme de bloc déclaré reste alors ce pour quoi il est fait — transporter un artefact vers un lecteur qui n'a pas à tout comprendre — sans jamais servir à contrôler une dérivation. Le mode de défaillance que cette règle ferme est précis~: un compilateur qui sauterait des champs vérifierait un programme amputé, puis signerait le programme entier.

Cette sérialisation permet à des outils tiers — vérificateurs formels, analyseurs statiques, assistants fondés sur un modèle de langage — de lire le programme compilé comme une donnée structurée plutôt que comme un texte à reparser, et de proposer des corrections ou des preuves sans jamais toucher au code source. Chaque nœud y porte un provenance_id — fichier, ligne, colonne, composant d'origine — qui traverse le pipeline jusqu'au binaire final via les métadonnées LLVM/DWARF. En cas de panne, le superviseur remonte cette chaîne de causalité jusqu'à la définition source exacte, plutôt que de s'arrêter à l'adresse mémoire fautive.