Traduction ingénierie des théorèmes formels
L'article §4.4 donne 6 théorèmes métathéoriques centraux. Nous ne listons pas les preuves ici ; nous traduisons seulement chaque théorème en « ce que cela signifie pour un véritable Agent Runtime ». Comprendre Confluence est la clé pour comprendre la valeur de tout l'article.
Table de traduction ingénierie des six théorèmes
[Conclusion originale de l'article §4.4]
| Théorème | Section | Traduction ingénierie |
|---|---|---|
| Preservation (Thm 59) | §4.4.1 | Après l'application de n'importe quelle règle, le registry reste well-formed : les pointeurs parent restent dans le registry, les provisions de différents fibers sont disjoints, et le committed view ne pointe que vers des fibers installed. Sens : le runtime ne se trouvera jamais dans un état avec « référence de fiber dangling » ou « deux plugins prétendant tous deux fournir 'database' ». |
| Recovery Exactness (Thm 61) | §4.4.2 | Sous l'hypothèse de pairwise independence, pour l'episode [b, u] d'un fiber n, appliquer son accumulator équivaut à l'état « n n'a jamais été chargé » (à l'exception des control fields). Sens : après avoir déchargé un plugin, l'état de l'environnement équivaut à ce qu'il n'a jamais existé — crucial pour HMR et le remplacement à chaud de plugins. |
| Ordering (Thm 63) | §4.4.3 | Les Providers doivent s'activer avant les Consumers et se décharger après ; la résolution de dépendances (committed view) qu'un Consumer lit durant tout un episode est invariante. Sens : les pools de connexions ne sont pas fermés tant que toutes les connexions ne sont pas rendues ; les bases de données ne sont pas fermées tant que toutes les transactions ne sont pas committées ; pas de « race condition où le consumer lit un provider à moitié fermé ». |
| Resolution Coherence (Thm 64) | §4.4.3 | Toutes les iterations d'une transition s'exécutent sous le même committed view ; si le target change en cours, soit la transition se complète vers Active, soit elle entre dans Unloading via L-Divert/L-Raise et se révertit complètement. Sens : pas de « à moitié ancien, à moitié nouveau » lors du chargement asynchrone de composants — une partie des effects ne peut pas utiliser l'ancienne dépendance tandis qu'une autre utilise la nouvelle. |
| Progress (Thm 66) | §4.4.4 | Sous les hypothèses que ≺ est acyclique, len(e_n) ≤ K, et que les noms de fibers sont finis, un état non-quiescent a toujours une règle applicable, et le nombre de steps par fiber est borné. Sens : le système ne peut pas deadlock (les guards se libèrent toujours) ; chaque changement de configuration atteint finalement un état stable. |
| Confluence (Thm 73) | §4.4.5 | Sous les hypothèses de pairwise independence, component total on provision, et no failure, peu importe le nombre de chargements/déchargements/remplacements, tant que la configuration finale est la même, l'état stable équivaut à un démarrage propre unique depuis cette configuration finale. Sens : l'histoire dynamique ne laisse pas de trace — après qu'un Agent a remplacé ses propres composants à plusieurs reprises, cela équivaut à un démarrage unique de la configuration finale. C'est la pierre angulaire théorique de l'« Agent auto-évolutif ». |
Confluence : l'histoire dynamique ne laisse pas de trace
Confluence est le point culminant de cette théorie et mérite un développement séparé.
Énoncé intuitif : après que le système a subi un nombre quelconque de chargements, déchargements et remplacements dynamiques, tant que la configuration finale est la même, son état stable doit être équivalent à celui obtenu en démarrant proprement depuis la configuration finale.
Pour un Agent auto-évolutif, cela signifie : supposons que l'Agent remplace l'outil A trois fois de suite, décharge et réinstalle le Skill B deux fois, et ajuste le isolation realm du sous-Agent C ; tant que sa configuration finale de composants est identique à celle d'« un certain démarrage propre », alors l'état stable du runtime (quels composants sont actifs, leurs committed views, l'état d'environnement accumulé) est équivalent à ce démarrage propre. L'histoire dynamique ne laisse aucune trace.
C'est une garantie que les autres frameworks DI/HMR ne fournissent pas :
- La DI traditionnelle ne supporte pas le remplacement à l'exécution, donc aucune Confluence à parler ;
- Le HMR exige des développeurs qu'ils écrivent à la main les fonctions de migration d'état, sans garantie formelle de leur correction ;
- L'orchestration de conteneurs « redémarrer = propre » discard tout l'état de manière grossière, ce n'est pas une équivalence de même granularité.
[Conclusion originale de l'article §4.4.5] Notez les préconditions de Confluence :
- pairwise independence : les effects sont indépendants entre eux ou commutent (Def 19) ;
- component total on provision : chaque component installe effectivement toutes les keys qu'il déclare (Def 69) ;
- no failure : les scénarios de failure sont exclus.
[Conclusion originale de l'article §4.4.5] Confluence exclut les scénarios de failure (L-Raise dans §4.3.4) — parce que les failures sont une véritable source de divergence : un schedule peut échouer tandis qu'un autre peut réussir, mais Cor 62 garantit que la contribution d'un fiber failed au state est 0 (les effets de bord du composant échoué sont entièrement révertis et n'affectent pas les autres fibers). Ainsi « failure » ne rompt pas la cohérence de l'état, mais fait diverger deux chemins dynamiques (l'un avec failure, l'autre sans).
Ce que cette preuve ne garantit pas
[Conclusion originale de l'article §6.1, §6.3] Les preuves formelles ne couvrent que les effets de bord gérés via le Context. Elles ne garantissent pas que :
- Les inverses écrits par les développeurs soient nécessairement corrects (la condition witness
g(δ)=γest une obligation, non vérifiée) ; - Les effets de bord hors Context (modification directe de variables globales, fichiers, bases de données, systèmes externes) puissent être révertis ;
- Les emissions externes (requêtes réseau, messages, emails, paiements) puissent être révertis automatiquement — une fois émis, ils franchissent la frontière du système ;
- La sécurité des plugins non fiables — le contrôle d'accès au niveau Context ne peut pas remplacer un sandbox processus/conteneur/WASM ;
- La Confluence sous scénarios de failure (explicitement exclue) ;
- La compatibilité de version et structurelle des clés de dépendance (§6.6 open problem).
Pour les préconditions et limitations détaillées voir Limites et évaluation globale. Pour la manière dont cette théorie atterrit sur DeepSeek Harness voir La relation avec DeepSeek Harness.