Mesures de performance

English · Type : référence · Public : contributeur · Contexte : dépôt du moteur · Statut : prête · S'applique depuis : 4.1.13

Un jeu généré de n'importe quelle taille

Ce que coûtent les outils du moteur sur un jeu d'une taille donnée, mesuré sur des jeux générés, et l'histoire du solveur racontée par ses mesures. Chaque chiffre ci-dessous est daté, avec sa version et sa machine. Les chiffres bougent avec la machine ; les rapports, non. Les premiers tableaux ont été mesurés le 3 octobre 2026 (v2.3.0) sur un portable ; chaque section suivante donne sa propre date.

# dans le dépôt du moteur
npm run bench -- --rooms=40 --players=3 --items=30 --flags=100 --npcs=5 --scripts=10 --topics=40 --max=200000

Cette commande génère un jeu de cette taille (src/engine/tools/stress.ts) et chronomètre chaque outil dessus : validate, solve (global et par chapitre, simple et avec la réduction d'ordre partiel), le rapport de contenu, les graphes du monde et des énigmes, l'extraction et la traduction des textes, une migration de sauvegarde. Le jeu est une chaîne : l'objet de chaque lieu ouvre le verrou du suivant, les personnages jouables se relaient aux frontières de chapitre, des promeneurs patrouillent entre deux lieux et émettent des événements, des horloges tournent un lieu sur deux, des sujets enchaînent des flags, des babioles vont dans des bacs, dix migrations de sauvegarde artificielles mènent à la version courante, un checkpoint avec objectifs clôt chaque chapitre, deux invariants surveillent le premier objet. Pas d'images : les layouts sont des rectangles. Une version à dix lieux tourne dans tests/bench.test.ts.

Les autres modes de tools/bench.ts :

La matrice de preuve de la 4.1.13 a sa propre commande, lancée la nuit, jamais sur une pull request :

# dans le dépôt du moteur
npm run prove:matrix -- --only=c11,o21 --time=600 --max=10000000 --mem=4096 --json=matrix.json

Elle prouve chacune des douze instances de PROOF-MATRIX.md dans son propre processus, sous les budgets publiés, affiche une ligne par instance et ne sort en 1 que sur un verdict faux (proved là où un softlock est attendu, ou l'inverse, ou une erreur de recherche) ; une instance hors budget est unknown (tronquée), jamais proved. --representation=objects|compact, --checkpoint-dir=<dir> et --workers=N sont transmis au solveur.

Résultats (3 octobre 2026, v2.3.0)

fonction apparue en 2.3.0

Tous les outils sauf le solveur sont linéaires et instantanés. Le solveur est celui à surveiller.

La v2.3 lui fait faire trois fois moins d'exécutions du moteur pour les mêmes états : une action à laquelle aucune règle écrite ne peut répondre (quelles que soient les conditions) ne peut que retomber sur une réplique Regarder, une réaction par genre ou la réplique de repli ; elle n'est donc plus exécutée du tout (le profil la compte en skipped). Sur le jeu d'exemple : 2 076 exécutions sont devenues 280 pour les mêmes 35 états.

Ce que le solveur fait d'un gros jeu

L'espace d'états d'un jeu d'aventure est le produit de tout ce qui peut varier indépendamment. Avant la v2.1, le solveur hachait chaque flag, chaque objet et chaque position de script : la version à dix lieux de ce jeu, avec ses horloges, ses promeneurs, ses flags « regardé » et ses babioles, atteignait la limite de 20 000 états après 54 secondes sans finir.

La v2.1 demande au graphe des énigmes ce qui peut encore changer l'issue (liveness dans src/engine/tools/puzzle.ts) : les lieux, les lieux de la carte, les joueurs, la fin et les objectifs de chapitre sont vivants ; une action est vivante quand un de ses effets atteint quelque chose de vivant ; une chose (objet, flag, accessoire, position d'un personnage, événement) est vivante quand une action vivante la lit. Le reste sort de l'état et des actions essayées : un flag que seul son poseur lit (un marqueur « regardé »), une babiole qu'aucune porte n'exige, une horloge que personne ne lit, un promeneur que personne n'attend, une chaîne de sujets qui finit dans un flag que rien n'utilise. Le même jeu à dix lieux prend maintenant 102 états ; celui à quarante 624 ; celui à cent 2 901.

Ce qui multiplie encore les états, par construction, c'est ce qui compte : les choses vivantes indépendantes. Dix objets facultatifs qui ouvrent chacun quelque chose, dans n'importe quel ordre, font 2^10 états. La réponse honnête pour un jeu long reste :

1. Les chapitres (checkpoints avec goals, npm run solve -- --chapters) : chaque chapitre est prouvé depuis le checkpoint précédent, avec seulement ses propres choses vivantes. Le dernier chapitre ci-dessus coûte 3 290 états ; le jeu entier 2 901, parce que la recherche globale abandonne ce que les chapitres précédents ont consommé.
2. Les invariants pour les bugs « plus jamais », vérifiés sur chaque état exploré.
3. Le graphe des énigmes pour voir, avant de résoudre, de quoi une chose dépend et ce qu'elle débloque.

Limite · scale-not-a-promise Résoudre globalement un jeu de 100 lieux et 5 joueurs en six secondes ne promet pas que chaque jeu de 15 heures sera prouvé d'un coup. Cela dit que les outils du moteur suivent le contenu, et que le solveur dépense son budget sur les énigmes. Ce qu'un témoin ou une preuve permet de conclure : Ce que prouve le solveur.

Quand ça devient lent : le profil

npm run solve -- --profile (le « Solver health » de l'onglet Check, l'outil MCP solve avec profile: true) dit pourquoi (la sortie reste en anglais) :

SOLVER PROFILE
  states explored       35
  engine runs           280  (211 changed nothing, 35 landed on a known state)
  actions not run       1808  (no rule could answer them)
  actions per state     22.3 on average, 27 at most (house, 3 items in the bag…)

What splits the states (states that would merge without it):
      13  room  (3 values)
       4  player hero  (11 values)
       3  flag lou_has_key  (2 values)
…
Use / give combinations per room (over its expansions):
  garden: 272 candidates, 2 answered by a rule, 271 could only fall back (100% useless)
Independent dimensions (their combinations multiply the states; a checkpoint between them would cut it):
  ⚠ item rope, item coin, item book: 8 of 8 combinations seen
Monotonic (never lost once gained): 9 flags, 1 items (shell_phone)

Chaque dimension de l'état (un objet dans le sac, un flag, l'état d'un accessoire, la position d'un script…) est notée par le nombre d'états qui fusionneraient si on la retirait : le haut de cette liste, c'est ce dont la logique du jeu est faite, ou l'énigme devenue combinatoire. Les groupes de dimensions à deux valeurs dont toutes les combinaisons apparaissent évoluent indépendamment : un checkpoint avec objectifs entre eux rend petite la recherche de chaque chapitre. La carte de chaleur du graphe des énigmes (onglet Check) montre les mêmes chiffres sur les règles et les lieux ; « why is this live? » sur une fiche explique pourquoi le solveur garde une chose dans son état. Toutes les options du solveur : Options du solveur.

L'histoire du solveur, mesurée

Chaque section ci-dessous est la mesure de sa version, gardée telle quelle (la machine de la section, cache coupé sauf mention contraire). Elles expliquent pourquoi le solveur fonctionne comme il le fait aujourd'hui.

Moins d'ordres : la réduction d'ordre partiel (historique, v2.3)

Limite · por-not-for-proofs Ne jamais utiliser la réduction d'ordre partiel pour certifier qu'un jeu n'a pas de softlock. Mesurée en mode preuve en 3.3, elle a signalé un softlock qui n'existe pas (plus bas). --por ne s'applique qu'aux recherches de témoin : en mode preuve, le solveur l'ignore et le dit. Cette section est la mesure de la v2.3, gardée telle quelle.

Deux actions qui touchent des choses différentes commutent : prendre la corde puis la pièce, ou la pièce puis la corde, mène au même état. Le solveur fusionne déjà les états (un hash) ; ce qu'il payait encore, ce sont les ordres entre les deux : k ramassages indépendants avant une porte font 2^k états quand la recherche ne peut pas finir (la preuve d'une impasse, une recherche tronquée). npm run solve -- --por=sleep|stubborn (src/engine/tools/por.ts) utilise ce que le moteur a noté pendant chaque action (ce qu'elle a lu, ce qu'elle a changé, dans les dimensions de l'état) et, pour les actions qu'une condition retient encore, ce que le graphe des énigmes dit qu'elles exigent :

sleep ne saute que des exécutions du moteur (une action essayée avant une action indépendante n'est pas réessayée au retour) ; stubborn n'explore qu'une action commutante à la fois, donc les états tombent aussi. Sur le jeu de charge en chaîne, rien ne commute et rien ne change ; sur un vrai jeu avec des quêtes annexes facultatives, c'est la différence entre une preuve et un dépassement de temps (dans une recherche de témoin : voir l'avertissement plus haut). La réduction est désactivée par défaut : la recherche simple est la preuve.

v3.1 : schéma 3 et preuve exhaustive (4 octobre 2026)

npm run bench -- --v3 génère le jeu de charge avec des ids stables (assignIds), comme un vrai jeu v3 ; --prove ajoute la recherche exhaustive (solve -- --prove : tous les états atteignables, les softlocks). Même portable.

Le témoin n'a pas bougé entre la v2.3 et la v3.1 (mêmes états, mêmes exécutions : les ids stables ne changent rien à la recherche). La preuve exhaustive, c'est autre chose : elle visite chaque état atteignable, la réduction d'ordre partiel est coupée dans ce mode (une réduction ne doit pas retirer une branche perdante d'une preuve tant qu'elle n'a pas sa propre preuve d'équivalence), et un jeu de 40 lieux dépasse déjà un budget de 50 000 états. npm run prove:game est donc une porte de release pour un petit jeu (la démo se prouve en 1,3 s) et un travail hebdomadaire borné pour un grand (.github/workflows/prove.yml) ; sur un jeu long, on prouve chapitre par chapitre (--prove --chapters), chaque recherche étant bornée par ses objectifs. Amener la réduction en mode preuve, avec les tests d'équivalence de tests/por.test.ts pour preuve, était alors le prochain pas du solveur.

v3.2 : causes des softlocks, preuve par chapitres, et où la preuve s'arrête (4 octobre 2026)

Une preuve rapporte désormais chaque état de softlock atteignable (softlockCount), regroupés par l'étape qui a perdu la partie (softlockCauses : la première action qui mène d'un état encore gagnable à un état qui ne l'est plus), et une preuve depuis « Nouvelle partie » explore aussi les choix de l'introduction (la preuve de la démo passe de 2 176 à 6 528 états : elle n'avait prouvé que la réponse par défaut). npm run solve -- --prove --chapters prouve chaque chapitre depuis chaque état frontière atteignable du précédent (chaque état où ses objectifs tiennent, dédoublonné par ce que le chapitre suivant lit) et signale un checkpoint qui n'en égale aucun, avec les dimensions qui diffèrent : il a trouvé trois des quatre checkpoints de la démo en désaccord avec le contenu (la place de Biscuit et le tuyau déjà utilisé, un écouteur once déjà déclenché, le lieu où l'on trouve la clé), tous corrigés. Un seul budget d'états couvre toute la preuve (maxStates × 10, au plus 1 000 départs par chapitre) : au-delà, le résultat est truncated, jamais vert.

Même portable ; 12 objets, 30 flags, 1 promeneur, 2 scripts, 8 sujets ; maxStates 20 000 :

Ce que cela disait, simplement : la preuve exhaustive est complète et rapide pour une chaîne de 40 lieux à un seul personnage ; avec plusieurs personnages jouables, les états atteignables se multiplient (le lieu et le sac de chacun) et les deux preuves s'arrêtent au budget en le disant. C'était une limite de la recherche explicite telle qu'elle était écrite, pas du moteur : l'état gardait le lieu exact de chaque personnage et le personnage actif, et un changement de personnage était une transition à part entière, si bien que des états équivalents étaient explorés des milliers de fois (trois personnages libres dans 30 lieux : 81 000 combinaisons de positions avant le moindre flag). La piste solveur de la 3.3 s'est attaquée précisément à cela. Découper en chapitres n'y change rien, car le premier chapitre contient déjà le produit ; cela vérifie les checkpoints et prouve chaque chapitre depuis toutes ses entrées, ce dont un long jeu à un personnage a besoin. Sans argument d'équivalence écrit, les réductions restent coupées en mode preuve, et la suite différentielle (tests/por.test.ts) montre pourquoi : les ensembles sleep inventent des softlocks sur trois fixtures sur huit (les arêtes retirées nourrissent l'atteignabilité arrière qui les classe), les ensembles stubborn s'accordent sur les huit. Un long jeu à plusieurs personnages se prouve personnage par personnage (un checkpoint où les autres attendent) ou s'appuie sur le témoin, les témoins par chapitre et les playtests.

Les prochains pas du solveur, alors, dans l'ordre (une relecture extérieure, LOG #38) : mesurer où part le temps (exécutions du moteur, clones, hachages, file) ; une frontière de preuve sans ordre best-first ni chemins copiés ; le personnage actif hors de l'état (les actions de chaque personnage proposées depuis un état canonique, un changement gardé explicite seulement s'il a un effet) ; les régions de mobilité (les lieux reliés par des sorties réversibles et silencieuses fusionnés en une région par personnage, les déplacements en macro-étapes dont le trajet est gardé pour la solution) ; des interfaces de chapitre projetées sur ce que la suite lit ; une réduction sûre pour la preuve (fermeture par dépendance, visibilité des objectifs et invariants, blocages, condition de cycle, puisque la propriété est « depuis tout état atteignable, la fin reste atteignable »), validée contre la recherche explicite sur des milliers de jeux générés, chaque contre-exemple rejoué sur le vrai moteur ; puis des frontières en parallèle. Critère de sortie : le jeu de charge de 40 lieux prouvé avec 1, 2 et 3 personnages, un nombre d'états qui ne croît plus comme le produit des positions, aucun jeu généré où les verdicts réduit et explicite diffèrent, et une troncature qui reste une troncature.

v3.3 « Scale » : la matrice de référence (4 octobre 2026)

npm run bench -- --matrix --max=20000 : la preuve exhaustive sur des chaînes générées de 20 et 40 lieux avec 1, 2 et 3 personnages jouables (12 objets, 30 flags, 1 promeneur, 2 scripts, 8 sujets). Positions compte les combinaisons distinctes (personnage actif, lieu de chaque personnage) parmi les états ; la répartition du temps vient du profil du solveur lui-même (profile.timing).

Deux causes, mesurées. Les états sont des positions : avec deux personnages sur 20 lieux, les 800 positions font exactement 20 × 20 × 2, toutes les combinaisons ; avec trois, les positions forment l'essentiel des états. Le temps part dans la file dès que les états s'accumulent : la file best-first insérait en O(n) (splice), 83 à 89 % du temps avec trois personnages ; avec un seul, l'exécution du moteur (environ la moitié) et la copie des états (environ un quart) dominent. Les branches de la 3.3 s'y sont attaquées dans cet ordre : un cœur de preuve exact (frontière en O(1), pointeurs vers le parent), puis le personnage canonique et les régions de mobilité pour les positions.

Après v33-proof-core (exact : mêmes témoins, mêmes preuves, même sortie imprimée sur la démo)

La frontière est un tas binaire dans l'ordre de l'ancienne liste (score, puis arrivée), et un état garde un pointeur vers son parent et son dernier pas au lieu d'une copie de tout le chemin et de la session.

La file disparaît du profil (89 % → 0 %) et le cas le plus lourd va 8 fois plus vite pour les mêmes 20 000 états (50,9 s → 6,2 s). Le nombre d'états ne bouge pas, comme il se doit : restent le moteur (environ la moitié), les copies d'état (environ 30 %), et surtout le nombre d'états, auquel se sont attaquées les branches suivantes.

Après v33-player-canonical (mêmes verdicts, vérifiés contre la recherche explicite)

En mode preuve, des états qui ne diffèrent que par le personnage actif sont un seul état, et chaque état propose les actions de chaque personnage (Switch to X › action) quand le changement ne modifie rien de ce que lit le solveur ; un changement qui modifie quelque chose reste une étape explicite, et les invariants sont vérifiés du point de vue de chaque personnage. Preuve de la démo : 6 528 → 3 480 états, même verdict.

Le personnage actif n'est plus un facteur (positions 18 796 → 112 à trois personnages), mais les chaînes de charge restent tronquées : le lieu exact et le sac de chaque personnage fragmentent maintenant les états. C'est le travail des régions de mobilité.

Après v33-mobility : régions de mobilité, et la preuve de référence

Le lieu exact d'un personnage est remplacé par sa région : les lieux entre lesquels il peut marcher en silence (sorties générées et voyages par la carte vers des lieux sans onEnter, dont rien ne lit le visited, et qu'aucune condition ne nomme), la partie fortement connexe autour de lui, vue avec son propre sac. La preuve propose les actions de chaque lieu de la région sous la forme Go to <room> › action ; le trajet est joué une fois par lieu, chaque pas vérifié (il arrive, il ne change rien de ce que lit le solveur), et un pas qui n'est pas silencieux relance la recherche avec les lieux exacts (profile.mobility.reason). Le témoin d'une preuve par régions se rejoue sur le vrai moteur.

La référence (npm run bench -- --matrix --eras, makeStressGame({ eras: true })) : chaque personnage confiné dans son époque, l'objet qui ouvre la première serrure de l'époque suivante envoyé par une goulotte temporelle ({ transfer }), goulottes à sens unique, promeneurs, scripts et sujets ; softlock: true ajoute une poubelle qui détruit l'objet 0. Mode preuve, budget de 200 000 états :

L'objectif de la 3.3 est atteint sur elle : 40 lieux × 3 personnages prouvés en 578 états et 4,2 s. Sur des versions à 12 lieux, la recherche explicite (les deux abstractions coupées) donne les mêmes verdicts avec 13 à 15 fois plus d'états (2 906 contre 230 à deux personnages, 16 944 contre 1 100 à trois), et trouve le même softlock dans la variante négative (tests/reference-proof.test.ts).

La chaîne ouverte reste hors de portée, et c'est le jeu, pas l'abstraction. Sans époques, chaque personnage peut parcourir toute la chaîne et ramasser l'objet de n'importe qui : quel personnage porte quel objet est un vrai produit que la preuve doit couvrir (budget de 20 000 états) :

Aucune réduction exacte ne peut retirer ces états ; un jeu construit ainsi se vérifie par le témoin, les témoins par chapitre et les playtests, ou en bornant qui peut porter quoi. Avec un seul personnage, les régions réduisent aussi la chaîne ouverte (40 lieux : 3 197 → 163 états).

Après v33-chapter-interfaces : une recherche par chapitre, depuis tous les états frontière à la fois

Un chapitre se prouve désormais par une seule recherche qui part de tous ses états frontière ensemble et partage ce qu'elle a vu (un état est sûr ou non quel que soit le départ qui l'a atteint) : il coûte l'union de ce que les départs atteignent, pas la somme. La comparaison avec la recherche explicite lancée depuis chaque départ a trouvé un vrai défaut, antérieur à la 3.3 : un objectif de chapitre qui lit le sac du personnage actif ({ has: 'token' }) était évalué sur le personnage que l'état fusionné avait gardé, et des états frontière se perdaient. Un état canonique atteint maintenant l'objectif dès qu'un personnage, vu comme actif, le satisfait. Sur la démo, la recherche partagée abstraite trouve exactement les frontières de la recherche explicite à chaque chapitre (tests/reference-proof.test.ts), avec 15 à 36 fois moins d'états.

La mobilité est coupée sur la démo, et le profil dit pourquoi (no move of this game can be silent : chaque lieu a un onEnter ou est nommé par une condition), ce qui épargne aussi le calcul des régions à chaque hachage.

Après v33-noop-memo : pas de réduction d'ordre partiel dans les preuves, une mémoire des no-ops à la place

La réduction, mesurée en mode preuve. Les ensembles sleep visitent tous les états mais sautent des arêtes : une action déjà essayée dans un ordre qui commute n'est pas relancée. La preuve classe les états par atteignabilité arrière sur ces arêtes, donc une arête sautée peut cacher le seul chemin vers le but. Sur le jeu par époques, c'est le cas : 20 lieux × 3 personnages signale un softlock que la preuve simple n'a pas (40 × 3 aussi), pour moins de 2 % des exécutions du moteur évitées et 20 à 25 % de temps en plus (tests/por.test.ts, « why proof mode keeps the reductions off »). Les réductions restent coupées en preuve ; le coût est ailleurs : 78 % des exécutions du moteur de la démo (92 % sur le jeu par époques) ne changent rien.

La mémoire des no-ops. Le moteur enregistre ce qu'une exécution écrit (Engine.writes, à côté d'Engine.reads), même une valeur déjà en place. Une exécution qui n'écrit rien de ce que le solveur hache est gardée avec les valeurs qu'elle a lues ; la même action sur un état aux mêmes valeurs est un no-op aussi, et n'est pas lancée. Elle ne retire aucune arête (un no-op est une boucle), donc la preuve est la même. Elle suppose que la trace des lectures est complète : un saut sur 16 est lancé quand même et comparé, et une différence est une erreur, jamais un saut silencieux. tests/memo.test.ts lance chaque saut quand même sur douze fixtures (témoin et preuve) et sur la démo : mêmes verdicts, états, softlocks, témoins et compteurs d'atteignabilité.

Limite · memo-corpus-equivalence L'équivalence de la mémoire des no-ops est vérifiée sur ce corpus, pas prouvée pour tout jeu : une future condition ou commande qui oublierait de déclarer une lecture la casserait, et seule une vérification qui lance chaque saut le verrait (npm run solve -- --audit-abstractions, 3.3.1).

npm run solve -- --profile termine son en-tête par ce que chaque abstraction a fait, ou pourquoi elle est coupée (la sortie reste en anglais) :

Abstractions (what each one did, or why it is off):
  canonical character   3048 switches folded, 0 kept explicit
  mobility regions      off (no move of this game can be silent)
  no-op memo            95625 runs skipped (5976 of them run anyway and identical), 522 kept, 4728 refused

3.3.0, mesurée sur la release (5 octobre 2026, cache coupé)

Avec le cache de preuve chaud, la preuve globale de la démo répond en 0,17 s et ses chapitres en 1,1 s. La matrice ouverte (personnages non confinés à une époque, objets qui circulent librement) tronquait toujours avec 2 et 3 personnages : voir Après v33-mobility.

3.3.1 : les abstractions auditées (5 octobre 2026)

npm run solve -- --audit-abstractions (src/engine/tools/audit.ts) prouve le jeu sélectionné deux fois : avec les abstractions, chaque saut de la mémoire lancé quand même et comparé, et avec toutes coupées. Il échoue (sortie 1) sur toute différence de verdict, d'invariants cassés, d'existence de softlocks, ou de flags, lieux et emplacements atteints ; il dit partial (sortie 2) quand la recherche explicite ne tient pas dans le budget, parce qu'alors les verdicts n'ont pas été comparés. Sur la démo : same, 3 480 états contre 6 528, 95 625 sauts tous identiques, 9,5 s. release-check le lance.

tests/audit.test.ts lance le même audit sur 120 jeux aléatoires (tests/gen/random-game.ts : 2 à 4 lieux, 1 ou 2 personnages, has négatif, consommation, transferts, compteurs, once / nth / cycle, if imbriqués), et sur un jeu par commande et par condition du DSL (les deux tables sont vérifiées contre les types Cmd et Cond : une nouvelle variante sans exemple ne compile pas). Sur les 120 jeux aléatoires, 92 sont same (la recherche explicite : 26 résolus, 18 avec softlocks, 48 non résolus) et 28 partial à 3 000 états ; aucun n'a divergé.

Ce qu'il a trouvé, et qui a été corrigé :

• Un flag mort qui ne l'était pas. La première règle écrite qui correspond répond. Un flag qui ne garde qu'une règle antérieure, laquelle ne touche que ce flag, semblait mort à l'analyse de vivacité ; pourtant il décide si c'est la règle antérieure ou une suivante qui répond. Le solveur fusionnait les deux états et perdait tout chemin passant par la règle suivante ; sur un jeu aléatoire, les abstractions atteignaient par hasard un flag que la recherche explicite n'atteignait pas. C'était un défaut de la recherche de base, pas d'une abstraction. Le graphe des énigmes relie maintenant la condition d'une règle antérieure à chaque règle suivante qu'elle peut masquer (puzzleGraph) ; la démo et le jeu de référence gardent exactement les mêmes nombres d'états.
• Lieux atteints. Avec le personnage canonique, un lieu où seul un autre personnage jouable se tenait manquait à roomsReached (et le lint pouvait donc le dire jamais atteint). Le point de vue de chaque personnage compte maintenant.

3.4 : le chapitre de référence (5 octobre 2026)

games/reference, « Le Marché de nuit » : 8 lieux, 9 objets, 5 personnages dont deux jouables (Pixel et Biscuit, qui se passent des objets et s'ouvrent des lieux), un marché mis en scène (Canvas, 960 de large, 6 calques avec parallaxe, 3 occultants, 2 zones de marche reliées par un escalier), une cour sur deux plans (une échelle ouverte par un flag, un saut réservé à Biscuit), un script autonome, un mini-jeu, un final sur la timeline. Mesuré sur un portable M-series, cache coupé.

Joué jusqu'au bout par la CI : au clavier dans Chromium et WebKit, en français sans défaut anglais visible, et par le harnais générique avec axe et un aller-retour de sauvegarde.

3.4.0, mesurée sur la release (5 octobre 2026, cache coupé)

La 3.4 a changé l'image, pas la logique : chaque nombre d'états est celui que la 3.3.0 mesurait ; les temps bougent dans le bruit d'un portable.

3.5 : les workers de preuve (5 octobre 2026)

npm run solve -- --prove --workers=N (src/engine/tools/solve-pool.ts) : la recherche prend un lot de nœuds dans sa frontière (64 par défaut, les meilleurs d'abord, --batch), chaque nœud part vers le worker libre, et les expansions reviennent être fusionnées dans l'ordre du lot. Une expansion ne lit rien de la recherche (ni seen, ni la frontière) : ce sont les essais du nœud joués sur le moteur, construits depuis le jeu et les options seuls (makeExpander), les mêmes dans chaque fil. La fusion, dans le fil de la recherche, est l'endroit où seen, les objectifs, les arêtes et la frontière changent. Le résultat dépend donc du lot et jamais du nombre de workers ; un seul worker, c'est la même recherche par lots dans le fil de la recherche. Sans --workers, rien ne change : un nœud à la fois, les mêmes témoins et preuves qu'en 3.4 (vérifié octet pour octet sur la démo et le chapitre de référence, témoin et preuve). Un worker qui ne démarre pas, ou s'arrête, laisse ses nœuds au fil de la recherche (le résultat ne change pas ; profile.workers.reason le dit) ; les commandes sur mesure arrivent aux workers par le module du jeu ; la réduction d'ordre partiel les tient éteints. --time arrête une recherche, avec ou sans workers.

Mesuré avec npm run bench -- --workers-table sur un portable à 10 cœurs, cache coupé.

La chaîne ouverte, 20 lieux × 2 personnages, objets libres, arrêtée à 40 000 états :

La référence par époques, 40 lieux × 3 personnages (résolue) :

La porte de la 3.5 (×2 avec 4 workers sur une grosse preuve, le même résultat pour 1, 2, 4 et 8) est passée. Le résultat sans workers a une autre signature : l'ordre d'une recherche par lots diffère (les mêmes états et le même verdict, d'autres premiers chemins trouvés) ; tests/workers.test.ts vérifie les deux. Ce qui ne passe pas à l'échelle : la fusion (les états passent d'un fil à l'autre, le fil de la recherche vérifie chacun), et le démarrage des workers (environ 0,3 s) : une petite preuve, comme chacun des chapitres du jeu d'exemple, n'est pas plus rapide. Les workers restent donc éteints sauf demande ; --workers=auto (les cœurs moins un, 8 au plus) est le réglage d'un gros jeu.

3.5 : qui porte quoi (5 octobre 2026)

Le propriétaire canonique (preuves, actif par défaut avec le personnage canonique et les régions de mobilité ; --ownership=off). Avec plusieurs personnages jouables, lequel porte un objet multiplie les états : trois personnages et douze objets qui circulent librement, c'est la matrice ouverte que la 3.3 ne prouvait pas. Un objet qu'aucune condition ne lit (son absence ne décide donc de rien : pas de else, pas de règle masquée par une qui l'exige), dans aucun invariant ni objectif, perdu ou déplacé seulement par une action sur lui, et donné par aucune règle ni réaction par genre (poolableItems), est mis en commun tant que deux personnages quelconques peuvent se rejoindre : l'état garde combien de chaque objet commun existent, pas qui les porte. Avant d'essayer les actions d'un personnage, les remises qui lui donnent le fonds commun sont jouées sur le moteur : l'autre porteur prend la main, les deux marchent jusqu'à un lieu que leurs régions partagent, les objets sont donnés, la main revient, et chaque pas doit laisser l'état tel que la recherche le voit. Un pas qui ne le fait pas relance la preuve sans mise en commun (profile.ownership.reason), comme la mobilité.

Vérifié contre la recherche explicite (--audit-abstractions, tests/audit.test.ts) : le chapitre de référence same, 288 états contre 83 672 ; 60 jeux aléatoires à objets libres, aucune divergence (32 comparés sous 3 000 états, dont 10 avec des remises jouées ; 44 comparés sous 20 000, dont 14 avec des remises, aucun divergent). La première version divergeait sur 3 des 60 : le fonds commun listait des objets que la recherche ignore par ailleurs (morts), et l'audit l'a attrapé.

L'objectif de la 3.5, la matrice ouverte 20 × 3 dans le budget, n'a pas été atteint. Le propriétaire ne s'applique que tant que deux personnages quelconques peuvent se rejoindre, et dans la chaîne ouverte des portes fermées les séparent la plupart du temps (1 817 remises sur 200 000 états). Comme décidé, cela n'a pas bloqué la 3.5 ; c'était la question ouverte pour la suite.

La dominance pour un témoin (--dominance, témoins seulement : elle ne peut élaguer une preuve). Un état qui n'a pas plus de progrès qu'un état déjà vu (tout le reste égal ; ses objets et flags booléens monotones, ceux dont rien ne lit l'absence, un sous-ensemble) n'est pas exploré. Une recherche de témoin qui ne trouve rien avec elle est relancée sans, elle ne rend donc jamais unsolved d'elle-même. Mesuré : elle n'élague rien sur le jeu d'exemple, le chapitre de référence ni les jeux de charge. La recherche « le meilleur d'abord » atteint un témoin avant qu'un état dominé ne sorte, et un état dominé ne sort qu'une fois les meilleurs épuisés, ce qui (quand l'absence n'est jamais lue) veut dire que la recherche échoue de toute façon. Elle reste une option, éteinte par défaut.

3.5.0, mesurée sur la release (5 octobre 2026, cache coupé)

3.5.1 : ce que les workers coûtent en mémoire (5 octobre 2026)

# dans le dépôt du moteur
NODE_OPTIONS=--expose-gc npm run bench -- --workers-table --max=20000

La chaîne ouverte de 20 lieux × 2 personnages, lots de 64. La table a une colonne de RSS maximal depuis la 3.5.1 : tout le processus, threads des workers compris, échantillonné toutes les 20 ms, avec un ramasse-miettes avant chaque ligne. La mémoire qu'une passe libère n'est pas toujours rendue au système, donc les lignes suivantes sont une borne haute.

Chaque worker charge son propre moteur et son jeu : environ 150 à 350 Mo de plus par worker. Quatre workers coûtent plus du double de la mémoire d'une recherche seule, pour ×2,6 de vitesse. C'est une raison de plus pour qu'ils restent éteints sauf demande. Cela montrait aussi que davantage de workers n'atteindraient pas 20 × 3 : il fallait moins d'états (3.6).

Un worker qui s'arrête en pleine recherche quitte le pool pour de bon : son nœud repart aux autres, ou au fil de la recherche s'il n'en reste aucun. stats() n'interroge que les workers vivants, 2 s au plus chacun. tests/workers.test.ts arrête un worker sur quatre après 5 expansions, puis les trois sur trois, par sortie comme par erreur non rattrapée : la preuve est la même.

3.6 : la mise en commun par groupe, une fuite, et un corpus (5 octobre 2026)

La mise en commun par groupe. La 3.5 ne mettait les objets libres en commun que si chaque paire de personnages jouables pouvait se rejoindre. À trois dans la chaîne ouverte, c'était rarement le cas : qui portait chaque clé multipliait les états. La 3.6 répartit les personnages selon qui peut rejoindre qui. Un groupe dont chaque paire peut se rejoindre partage un seul fonds des objets libres que portent ses membres ; un personnage hors de tout groupe garde son sac. Les remises avant qu'un personnage agisse ne se jouent que dans son groupe, vérifiées comme en 3.5.

Vérifié contre la recherche explicite :

• la chaîne de 7 lieux à trois personnages, avec et sans softlock : same (4 909 états contre 97 257, 2 599 remises) ;
• 40 jeux aléatoires à trois personnages (tests/audit.test.ts) ;
• npm run audit:corpus -- --seeds=300 : 900 jeux, 549 comparés jusqu'au bout, dont 196 avec des remises jouées. Aucune divergence (599 s). Il tourne chaque nuit sur 500 graines (.github/workflows/nightly.yml) ; 351 des 900 se sont arrêtés partiels (la recherche explicite a atteint ses 3 000 états) et n'ont pas été comparés : une affirmation dit « 900 essayés, 549 comparés ».

Le premier corpus a signalé trois divergences, toutes dans des jeux insolubles : chaque flag y est mort, donc absent des états, et les flags affichés comme atteints dépendent de l'état gardé à la fusion. L'audit ne compare plus que les flags vivants (SolveResult.liveFlags). Le corpus a aussi manqué de mémoire. Le solveur laissait un minuteur à délai nul en file à chaque action, environ 15 Mo par recherche, jusqu'à ce que le processus soit inactif. Corrigé : 918 Mo après 60 audits avant, 9 Mo après.

20 lieux × 3 personnages : toujours tronquée, à 600 000 états en 2 375 s, 7,6 Go au maximum (1 879 041 remises, 2 407 positions distinctes). La mise en commun par groupe repousse la limite de 10 à 14 lieux, pas jusqu'à 20. Ce qui reste, c'est où se tiennent les personnages : trois dans des régions séparées, avec les portes que chacun a ouvertes. Il faut une abstraction des personnages qui ne peuvent pas se rejoindre, la question ouverte depuis la 3.3.

Pas fait du plan 3.6 : retirer les objets qu'aucune condition restante ne lit (le groupe était le levier que le profil désignait), et compter le trafic entre workers.

4.1.13 : la matrice de preuve, un stockage compact, des points de reprise (7 octobre 2026)

docs/dev/PROOF-MATRIX.md fixe la classe de jeux sur laquelle le solveur est mesuré, avant tout code de la 4.1.13 : douze jeux générés (matrixGame, tests/gen/random-game.ts) de 20 à 40 lieux et trois personnages jouables, six contraints et six ouverts, avec des énigmes de clés croisées, des dialogues, un script et un événement par zone, des babioles libres et un four. Budget par instance : 10 000 000 d'états, 10 minutes sur le Mac du mainteneur (Apple M5, Node 22.14 ; mesuré avec --time=590), 4 Go de tas. npm run prove:matrix -- --only=<id> --time=590 --json=…, une instance par processus, une à la fois. « Avant », c'est le solveur de la 4.1.8 (ses sources avec seulement le générateur et l'outil de la matrice ajoutés) ; « après », la 4.1.13, stockage compact, sans workers.

Mesure · proof-matrix-memory Le stockage compact divise la mémoire de la matrice de preuve par 9 en tas et 4,5 en RSS (les douze pics additionnés : 11 069 → 1 230 Mo de tas, 13 247 → 2 926 Mo de RSS), à temps inchangé (×1,03 en moyenne géométrique). Une observation sur cette matrice et cette machine, pas une promesse pour un autre jeu.

• date: 2026-10-07
• version: 4.1.13
• volume: les douze instances de la matrice de preuve, 20 à 40 lieux, trois personnages jouables
• conditions: le Mac du mainteneur (Apple M5, Node 22.14), --time=590, 4 Go de tas, sans workers, une instance par processus
• source: docs/en/BENCH.md, 4.1.13

Mémoire : ÷9 en tas, ÷4,5 en RSS sur la matrice (le RSS contient environ 160 Mo de Node et du moteur quelle que soit la recherche). Sur les grosses preuves ouvertes, le tas baisse de 16 à 20 fois : o21 tenait 31,6 Ko par état, il en tient 1,6. Temps : inchangé (×0,93 à ×1,12 selon l'instance, ×1,03 en moyenne géométrique) : le temps par état, ce sont les exécutions du moteur, qu'une représentation ne touche pas. Les verdicts et les nombres d'états sont les mêmes là où les deux ont fini (l'oracle, plus bas). L'objectif n'a pas été atteint : les mêmes huit instances sur douze finissent dans le budget ; o22 à o25 manquent toujours de temps, désormais avec 4 Go de tas presque intacts. La 4.1.13 s'appelle donc « Solver Research » ; le rapport d'écart est la section 8 de docs/dev/PROOF-MATRIX.md.

Avec quatre workers (--workers=4, la table des états vus partagée), o23 atteint 237 618 états dans les mêmes 590 s (403 états/s, ×2,7 sur un seul fil ; 787 Mo de RSS avec les quatre moteurs) et reste tronquée, sa frontière en croissance (2 920 états en file à la fin).

L'oracle. tests/solver-oracle.test.ts : le jeu d'exemple (témoin et preuve), la preuve du jeu de référence et 200 jeux générés (preuves dans 3 000 états) donnent, avec le stockage compact, exactement ce que l'implémentation de la 4.1.8 a écrit dans tests/fixtures/solver-oracle.json avant tout changement : le verdict, le chemin et ses entrées de session, les softlocks et leurs causes, les impasses, les flags et lieux atteints et tout l'ensemble atteignable, état pour état (203 recherches, 90 s). tests/compact.test.ts compare compact et objects champ par champ sur le jeu d'exemple, 40 jeux générés et deux instances de la matrice.

Le reste du lot, mesuré. Le corpus de la nuit sur ce code (npm run audit:corpus, 500 graines × 3 sortes en quatre tranches de 250 à 278 s) : 1 500 jeux, 909 comparés à la recherche explicite, 0 divergence (591 partiels). Un point de reprise d'o23 pèse 1,7 Mo à 8 796 états et 3,2 Mo à 17 968 (environ 180 octets par état, états moteur de la frontière compris) ; reprise avec un second budget de 60 s, la recherche est passée de 8 796 à 17 968 états. Les objets symétriques (--symmetry), sur 30 jeux générés avec des pièces jumelles : 0 divergence contre la recherche explicite (14 comparés, 16 partiels), 11 616 → 8 802 états sur les 19 qui ont fini dans les deux cas (÷1,3) ; aucun dans les jeux fournis ni dans la matrice, l'option reste donc désactivée par défaut. La dominance dans une preuve (--dominance avec l'option de test unsafeReduction) : 1 verdict changé sur 43 jeux générés comparés, elle reste donc désactivée dans les preuves. La table des états vus partagée renvoie les états des workers sans leur état moteur (la ligne shared du profil les compte) ; le résultat est le même pour 1, 2 et 4 workers (tests/partition.test.ts). Pas fait : le backend symbolique (BDD, SAT/SMT, CEGAR) n'a pas été essayé.

Voir aussi

• Ce que prouve le solveur, Options du solveur, Quels tests tournent quand (les tests lourds de la nuit, le corpus, la matrice de preuve).
• tools/bench.ts, tools/prove-matrix.ts, docs/dev/PROOF-MATRIX.md, docs/dev/PROOF-PROFILE.md.

Modifier la source de cette page · Signaler une erreur