Comprendre.
Formaliser. Vérifier.

CHAPITRE 01

Cadre scientifique

Question de recherche, vocabulaire et limites

ASMXperience cherche des programmes dans un langage restreint afin de satisfaire des spécifications vérifiables. Un candidat est une fonction entière de 32 bits, et non un agent capable d’inventer sa propre finalité. Le générateur propose ; l’oracle de référence définit ce qui compte comme une réponse correcte. Cette distinction sépare la synthèse de programmes d’une interprétation biologique de la machine.

Le terme émergence désigne ici l’apparition, au cours de la recherche, de compositions d’instructions non écrites individuellement par l’expérimentateur. Il n’implique ni conscience, ni intention, ni nouveauté scientifique. La grammaire, les objectifs, les constantes privilégiées et la sélection sont conçus par l’humain. Ils orientent nécessairement les solutions observables.

Le travail expérimental consiste à définir une question falsifiable : à budget égal, une variante de mutation résout-elle davantage de tâches ? Une population plus diverse atteint-elle un score donné plus rapidement ? Une fonction retenue est-elle plus courte à comportement équivalent ? « Laisser tourner longtemps » est une condition d’observation, pas une hypothèse scientifique suffisante.

Enfin, l’existence d’une fonction correcte ne prouve pas son originalité. Les manipulations de bits sont un domaine ancien ; une revendication de nouveauté demanderait une comparaison avec les publications, les compilateurs et les routines spécialisées connues.

CHAPITRE 02

Modèle mathématique

Des mots binaires, pas des entiers sans borne

Notons B₃₂ = {0,1}³² et U₃₂ = {0,…,2³²−1}. Un mot binaire et son entier non signé sont deux représentations du même objet. Les opérations arithmétiques du moteur sont calculées modulo 2³² ; les opérations logiques agissent coordonnée par coordonnée. Cette distinction évite d’appliquer des identités sur ℤ à une machine à largeur finie sans vérifier leurs hypothèses.

L’addition et la multiplication donnent l’anneau ℤ/2³²ℤ. XOR et AND donnent, bit par bit, une autre structure : XOR est l’addition dans l’espace vectoriel 𝔽₂³². L’addition entière et XOR ne sont pas interchangeables, car les retenues de l’addition couplent les positions binaires.

Exemple : 0xffffffff ⊞ 1 = 0, tandis que 0xffffffff XOR 1 = 0xfffffffe. Pour les décalages, le moteur utilise un compte n & 31, donc compris entre 0 et 31. Son SHR est logique : des zéros entrent à gauche. Une sémantique SMT de décalage ne doit pas être supposée identique pour un compte ≥ 32 : il faut y encoder explicitement ce masquage.

La théorie SMT-LIB des vecteurs de bits fournit un vocabulaire formel pour exprimer ces opérations ; le contrat exact de chaque instruction reste celui du processeur et du compilateur de candidats. Référence : FixedSizeBitVectors.

CHAPITRE 03

Sémantique des candidats

États, registres et composition de transitions

Une fonction candidate manipule un accumulateur a, un temporaire b et une entrée immuable x. Son état initial est (a,b,x) = (x,0,x). Chaque gène définit une transition totale de cet état. La fonction renvoyée est la projection de l’état final sur a.

Cette définition permet un interpréteur indépendant de l’encodage natif. Une instruction mov r8d,eax remplace b par a ; xor eax,r8d remplace a par a XOR b ; mov eax,ecx recharge l’entrée x. La grammaire n’autorise pas d’accès arbitraire à la mémoire, de branchement, de boucle générée ou d’appel système.

L’absence de branchement donne une borne simple sur le nombre d’instructions générées, mais ne transforme pas l’exécution native en preuve de sûreté du superviseur. Le pont NASM, le compilateur, les API Windows et l’isolation restent du code à vérifier. La propriété « toujours terminer » est une propriété du langage candidat prévu, sous réserve d’un encodage correct et d’un environnement d’exécution fonctionnel.

Il faut aussi distinguer état du candidat et état du processus. Les drapeaux CPU peuvent être modifiés, mais ne sont pas observés par la grammaire actuelle. La pile est utilisée par l’appel et le retour ; elle n’est pas un espace de mutation accessible aux gènes. Ajouter des branchements demanderait une nouvelle sémantique et des budgets d’exécution explicites.

CHAPITRE 04

Grammaire native

Les quinze opérations réellement disponibles

Le génome contient une longueur puis des couples (opération, immédiat). Un immédiat est un mot de 32 bits ; certaines opérations ne le consultent pas. Deux génomes différents peuvent donc encoder exactement la même fonction. L’initialisation native fixe l’accumulateur et le temporaire ; une instruction RET termine la fonction.

Les constantes initiales privilégient notamment 0, 1, les puissances utiles et des masques de bits ; une part des immédiats provient directement du générateur pseudo-aléatoire. Il s’agit d’un biais de recherche explicite, pas d’une exploration uniforme de tous les octets.

Une majoration très grossière du nombre de génomes de longueur au plus 48 est Σ_l=0…48(15·2³²)^l. Cette borne compte les immédiats inutilisés et de nombreuses redondances ; elle ne mesure ni les fonctions distinctes ni leur accessibilité sous la sélection. La borne souligne seulement l’explosion combinatoire du langage.

CHAPITRE 05

Spécifications de référence

Trois problèmes, trois contrats explicites

Comptage de bits : popcount32

La routine de référence supprime à chaque étape le bit à 1 le moins significatif avec x & (x−1). Elle termine après exactement pc(x) itérations. C’est une manière de calculer la réponse attendue, pas une contrainte imposant la même structure à la fonction synthétisée.

Code de Gray : gray32

Sur l’ordre naturel des entiers, deux valeurs successives du code de Gray diffèrent d’un seul bit. Si x possède r bits de poids faible à 1 avant l’incrément, le masque x XOR (x+1) vaut 2^r+1−1 ; appliquer g à ce masque ne conserve que le bit r. Le passage circulaire du dernier mot au premier se traite séparément.

Inversion : reverse_bits32

Le bit 0 devient le bit 31, sans renverser l’ordre des octets seulement. Par exemple, rev(0x00000001) = 0x80000000. Des masques et des échanges de groupes peuvent réaliser cette fonction sans boucle, mais l’expérience ne suppose pas que la recherche retrouvera rapidement une telle décomposition.

CHAPITRE 06

Identités et démonstrations

Des propriétés utiles pour construire des tests

Gray est une bijection linéaire sur 𝔽₂³²

Soit S le décalage logique d’un bit vers la droite. Alors g = I + S, où + désigne XOR. Puisque S³² = 0, on obtient (I + S)(I + S + … + S³¹) = I + S³² = I. Les termes intermédiaires s’annulent en caractéristique 2.

Cette démonstration concerne la définition mathématique de Gray. Elle ne certifie un candidat que si l’on établit aussi l’équivalence de sa suite d’instructions avec cette expression pour toutes les entrées.

L’inversion est une involution

La permutation i ↦ 31−i appliquée deux fois redonne i. Ainsi rev(rev(x)) = x. De plus, rev(x XOR y) = rev(x) XOR rev(y), car une permutation de coordonnées commute avec XOR. Une fonction qui satisfait seulement l’involution peut néanmoins être fausse : l’identité est aussi une involution.

Relations de popcount

La seconde égalité se démontre séparément pour les quatre couples possibles de bits (0,0), (0,1), (1,0), (1,1), puis par sommation sur les positions. Ces identités alimentent des tests métamorphiques : elles augmentent la capacité de détection d’erreurs, sans se substituer à une spécification complète.

CHAPITRE 07

Fonction de score

Pourquoi un score élevé peut rester trompeur

Pour un objectif t et un jeu D de 128 entrées, la fitness actuelle compte les bits corrects de chaque sortie. La distance de Hamming entre deux mots est le popcount de leur XOR.

Un second indicateur compte les réponses entièrement exactes : E_D(f) = Σ 𝟙[f(x)=t(x)]. Les deux indicateurs ne sont pas équivalents. Pour une entrée dont la réponse attendue est 2, une fonction qui renvoie 0 obtient 31 bits corrects sur 32, mais sa réponse reste fausse.

Le biais est particulièrement important pour popcount32 : ses sorties appartiennent à [0,32]. Leurs 26 bits de poids fort sont toujours nuls. Une fonction qui renvoie zéro obtient donc au moins 26 points sur 32 par entrée, même lorsqu’elle ne résout rien d’utile. Lire « 96 % des bits corrects » comme « 96 % des entrées résolues » serait une erreur.

Implémenté : le meilleur candidat est choisi par score, puis par longueur plus courte en cas d’égalité. Le remplacement dans la population utilise sa propre règle d’admission et ne réalise pas une optimisation explicite du temps CPU. Perspective : un objectif multi-critères pourrait distinguer exactitude, taille et coût mesuré, avec une frontière de Pareto plutôt qu’un unique nombre opaque.

CHAPITRE 08

Dynamique évolutive

Sélection, variation et maintien de solutions

Le moteur conserve 64 membres pour chacun des trois objectifs. À chaque tentative, un objectif est choisi à tour de rôle. Un tournoi compare quatre tirages avec remise et fournit un parent. Une branche de l’opérateur peut choisir une population source différente, ce qui permet le transfert de fragments entre problèmes.

Les opérations de variation sont l’insertion d’un gène, sa suppression, son remplacement ou la bascule d’un bit d’immédiat. Un croisement conserve un préfixe du premier parent et lui ajoute un suffixe d’un second, dans la limite de 48 gènes. Une branche de réinitialisation produit un génome court neuf, de longueur comprise entre 0 et 8.

Dans le code actuel, ces branches utilisent des tests de modulo du générateur : réinitialisation sur un cas parmi 32, choix d’une source parmi les objectifs sur un cas parmi 16, croisement sur un cas parmi 4 quand la réinitialisation n’a pas eu lieu. Ce sont des descriptions du mécanisme ; la composition des branches et le modulo ne justifient pas une affirmation d’échantillonnage parfaitement uniforme.

L’élite est épargnée par le remplacement. Parmi les autres membres, un candidat peut prendre la place d’un mauvais membre s’il améliore sa fitness, ou dans certains cas d’égalité. Cela protège les meilleurs scores observés, mais peut aussi réduire la diversité et bloquer la recherche sur un plateau.

Un compteur qui augmente prouve seulement que des propositions sont évaluées. Pour mesurer l’évolution, il faut également suivre les changements de score, de longueur, de comportement et la fréquence des améliorations à budget comparable.

CHAPITRE 09

Paysage de recherche

Redondance, neutralité et absence de garantie globale

Le génome est une syntaxe ; la fonction calculée est sa sémantique. La relation G ≈ H si ∀x, f_G(x)=f_H(x) partitionne l’espace des génomes en classes de comportements. Une instruction sans effet observable peut modifier la syntaxe sans quitter une classe. L’égalité sur le seul jeu d’entraînement définit une relation encore plus grossière.

Les instructions qui n’affectent pas le résultat sont parfois appelées introns. Elles peuvent servir de réserve de variation, mais aussi allonger les programmes et ralentir l’évaluation. Le meilleur score ne révèle donc pas à lui seul le taux d’innovation comportementale. Une signature sur un panel d’entrées aiderait à distinguer répétition syntaxique et diversité sémantique.

L’état complet du système comprend populations, compteur et état pseudo-aléatoire. Avec un PRNG déterministe, la transition est déterministe une fois cet état fixé. La métaphore d’une chaîne de Markov stochastique suppose un modèle idéalisé de la source aléatoire ; elle n’est pas une preuve de convergence du programme concret.

Même dans un modèle aléatoire, l’existence de mutations ne suffit pas à garantir la visite de toutes les solutions : il faudrait établir l’accessibilité des états, les probabilités de transition, la récurrence appropriée et les effets de la sélection. Une barrière de fitness peut empêcher la conservation d’intermédiaires indispensables. Deux ans d’exécution ne suppriment pas cette difficulté.

CHAPITRE 10

Validation expérimentale

Ce que signifie exactement le badge « Réussie »

Le test de régression compare le code natif à un interpréteur de référence, vérifie la routine NASM de score et ses rejets anticipés, puis contrôle les populations après des lots multithreads. Une divergence signale potentiellement un défaut d’encodage, de sémantique ou d’ABI. En production, ces comparaisons ne sont plus répétées intégralement pour chaque proposition : les survivants sont notés en code natif, et les rejets suivent une borne exacte. Un accord des tests n’exclut pas une erreur partagée par les implémentations.

Quand un nouveau meilleur candidat atteint 4 096 points, un processus enfant vérifie 4 162 cas : 32 mots à un bit actif, leurs 32 compléments, zéro, le mot tout à 1 et 4 096 valeurs produites par une séquence pseudo-aléatoire déterministe. Le processus dispose d’un délai mural de trois secondes et de limites de ressources.

Le badge indique une réussite empirique à cette batterie. Il ne signifie ni correction universelle sur les 2³² entrées, ni supériorité de performance, ni originalité. Pour renforcer le protocole, il faudrait séparer entraînement, contre-exemples réutilisables et validation finale indépendante, puis publier les échecs autant que les succès.

CHAPITRE 11

Raisonnement statistique

Quand une borne probabiliste est-elle applicable ?

Supposons une fonction candidate fixée avant le test et n entrées indépendantes issues d’une même distribution. Si son taux réel d’erreur vaut p, la probabilité d’observer zéro erreur est (1−p)ⁿ. En inversant cette relation, zéro échec donne une borne supérieure unilatérale au niveau 1−α :

Cette borne concerne la distribution de test et une hypothèse fixée ; elle n’est pas une preuve pour chaque entrée. Elle ne s’applique pas directement au protocole déterministe actuel. Elle ne s’applique pas non plus naïvement au meilleur résultat choisi après des millions de consultations du même jeu.

La sélection adaptative crée une dépendance entre les essais et les résultats retenus. Tester de très nombreux candidats puis publier seulement celui qui passe amplifie le risque de surapprentissage. Une correction de comparaisons multiples exige un protocole défini ; remplacer simplement n par le compteur de candidats n’a aucun fondement.

Une campagne convaincante rapporte plusieurs graines, une distribution des budgets jusqu’au succès, les échecs au budget maximal et les conditions matérielles. Les courbes de survie des temps jusqu’à résolution peuvent être plus informatives qu’une moyenne calculée uniquement sur les campagnes réussies. Le seuil de succès et la règle d’arrêt doivent être fixés avant d’examiner les résultats.

CHAPITRE 12

Vers la vérification formelle

CEGIS et équivalence de vecteurs de bits

Perspective, non implémentée : encoder le candidat et la référence dans une théorie de vecteurs de bits, puis demander s’il existe une entrée qui les distingue. La question logique n’est pas « cette fonction a-t-elle un bon score ? », mais celle de l’existence d’un contre-exemple.

Si un solveur correct répond SAT, le modèle fournit une entrée à ajouter aux tests. S’il répond UNSAT pour un encodage fidèle et complet, les expressions modélisées sont équivalentes sur le domaine. UNKNOWN ou un dépassement de budget ne prouve rien. L’ABI, les fautes mémoire et l’équivalence entre modèle et octets restent des obligations distinctes.

La synthèse guidée par contre-exemples, ou CEGIS, alterne proposition et recherche d’une entrée réfutante. Le candidat suivant doit tenir compte des contre-exemples précédents. Ce mécanisme diffère du simple ajout d’un lot aléatoire identique pour tous les essais. Cours de synthèse du MIT : CEGIS.

Le langage sans branchement d’ASMXperience se prête à une traduction symbolique par composition des transitions. Il faut cependant modéliser le modulo 2³², l’initialisation du temporaire et le masquage des décalages. Oublier une de ces règles peut produire une « preuve » portant sur une autre machine que celle réellement exécutée.

CHAPITRE 13

Exécution native et ABI

Contrats nécessaires pour appeler une fonction générée

Le pont NASM reçoit un pointeur de code et une entrée entière selon la convention Windows x64, puis place l’entrée dans ECX avant de transférer le contrôle. La fonction candidate renvoie son mot de résultat dans EAX. Le temporaire utilise R8D, registre volatil ; les registres non volatils ne doivent pas être altérés par le langage généré.

Un RET correct suppose une pile et une adresse de retour cohérentes. La génération ne modifie pas RSP. Écrire un registre 32 bits en mode 64 bits remet sa moitié haute à zéro ; les résultats observés restent des mots non signés de 32 bits. Pour le contrat d’appel, voir la convention x64 de Microsoft ; pour les instructions, les manuels Intel.

La page est inscriptible pendant l’encodage, puis devient exécutable et non inscriptible. Le programme appelle FlushInstructionCache avant exécution. Microsoft documente la responsabilité du programme pour la cohérence du cache lors de la génération de code : VirtualProtect et FlushInstructionCache.

Ring 3 décrit le niveau de privilège du processus, pas une isolation de ses fichiers. Le bac Sandboxie et la grammaire restreinte répondent à d’autres risques. Aucun de ces mécanismes, pris isolément, ne doit être assimilé à une preuve universelle d’absence de fuite ou de défaut logiciel.

CHAPITRE 14

Débit et reproductibilité

Mesurer le moteur, pas seulement un compteur

Le débit publié correspond à l’augmentation du compteur de propositions divisée par le temps mural entre deux états. Il dépend de la longueur des candidats, des changements de protection mémoire, de l’interprétation de référence, des sauvegardes et des validations. Il ne représente ni des cycles par appel ni le débit d’une application cliente.

Profil natif optimisé : deux threads Win32 de calcul au maximum, priorité réduite et affinité excluant un cœur sur le N100. Un régulateur réduit le parallélisme et insère des repos lorsque les autres processus occupent la machine. Le cache exact préalloué utilise environ 6,3 Mio ; il compare le génome complet après son empreinte. Les changements RW/RX sont amortis sur des lots de 64 fonctions. La recherche reste native ; Node.js ne sert que le site.

Le débit compte des propositions : certaines passent les 128 tests, certaines sont éliminées dès que leur score maximal possible devient insuffisant, d’autres réutilisent un résultat exact du cache. Le dashboard expose ces trois compteurs. Un benchmark local a mesuré environ 152 157 propositions/s sur 20 secondes ; ce résultat ne signifie pas 152 157 évaluations exhaustives/s et dépend de la population et de la charge. Une borne de rejet sûre est : score partiel + 32 × nombre de cas restants < score minimal admissible.

Un démarrage peut afficher zéro : il n’existe pas encore deux mesures comparables. Une baisse n’est pas nécessairement une régression du code trouvé. Inversement, produire davantage de candidats faciles à rejeter peut améliorer r sans améliorer la probabilité de résoudre un problème.

Pour comparer des fonctions natives, il faudrait un protocole distinct : entrées contrôlées, échauffement, répétitions, coût du harnais, stabilité de fréquence et statistiques de dispersion. Il faut aussi considérer les variantes de processeur, la taille de code et les interactions du compilateur. La longueur du génome n’est pas une mesure de latence : une multiplication et un XOR ne coûtent pas nécessairement la même chose.

Le checkpoint conserve la population et l’état du PRNG, ce qui facilite une reprise de la séquence de recherche. Il ne suffit pas pour revendiquer une reproductibilité bit à bit entre versions : paramètres, binaire, jeux de tests et formats doivent aussi être fixés. Le compteur de tentatives ne doit pas être confondu avec le nombre de fonctions sémantiquement distinctes.

CHAPITRE 15

Persistance et flux live

Observer sans transformer l’observateur en moteur

Le checkpoint est écrit dans un fichier temporaire, vidé puis remplacé. Une somme FNV-1a détecte certaines corruptions accidentelles ; ce n’est pas une signature cryptographique ni une protection contre une modification intentionnelle. Le format actuel sérialise des structures C : taille, alignement, endianness et version sont donc des contraintes de compatibilité.

Le moteur sauvegarde périodiquement et lors de changements du meilleur candidat. Après une coupure, la reprise revient au dernier état complet durable. Des tentatives postérieures peuvent être recalculées ; la console et le checkpoint peuvent ainsi montrer des frontières temporelles différentes. Les propriétés exactes de durabilité dépendent aussi du système de fichiers et du matériel.

Le site reçoit les mesures et les lignes de console par une connexion SSE persistante. Les changements de fichiers déclenchent la lecture, avec une lecture périodique de secours. Un fragment de ligne sans saut de ligne est conservé jusqu’à complétion. L’affichage ne recharge pas la page pour obtenir de nouvelles lignes.

Pause thermique programmée : après 15 minutes de calcul, le moteur sauvegarde son état et suspend la génération pendant 30 secondes. Il continue à publier son état de repos, avec compteur fixe et débit nul. Le site remplace la console par un compte à rebours, puis la réaffiche lorsque le moteur confirme sa reprise, sans rechargement. Cette cadence est temporelle et ne repose pas sur une sonde de température ; elle repart au démarrage du processus.

Une connexion web active ne prouve pas que le moteur est actif. L’interface distingue le transport et l’âge du dernier état produit ; après dix secondes sans mise à jour, le débit courant n’est plus présenté comme connu. Le terminal garde une fenêtre bornée de lignes en mémoire ; le fichier reste l’historique persistant. Une pause de l’affichage n’arrête pas la recherche.

CHAPITRE 16

Programme de recherche

Des expériences comparables plutôt que des promesses

Ablation des opérateurs. Comparer mutation seule, mutation avec croisement, puis migration entre objectifs, en gardant des budgets et graines publiés. Rapporter le taux de succès, les tentatives jusqu’au succès et la longueur des solutions ; ne pas comparer seulement les meilleures captures d’écran.

Diversité. Mesurer des signatures comportementales, des distances de génomes et la proportion d’individus neutres. Tester une archive de comportements ou plusieurs îlots indépendants. Ces mécanismes ne sont pas présents dans le moteur actuel et leur bénéfice doit être mesuré, pas présumé.

Contre-exemples. Ajouter une boucle CEGIS et comparer le coût total, solveur compris, à l’évaluation empirique. Une réduction du nombre de propositions n’est intéressante que si le temps total ou la confiance obtenue s’améliore.

Superoptimisation. Après établissement de l’équivalence, rechercher un coût inférieur à une référence donnée. Le travail STOKE formule une recherche stochastique de programmes binaires sans boucle avec des contraintes de correction et de performance ; ASMXperience ne reproduit pas actuellement ce système ni ses résultats. Schkufza, Sharma et Aiken, ASPLOS 2013.

Un résultat publiable devrait fournir le problème, le code, les entrées, les graines, le budget, les versions, les machines et la méthode de vérification. « Trouvé par le moteur » est une provenance expérimentale. « Nouveau », « correct pour tout x » et « plus rapide » sont trois revendications supplémentaires qui demandent chacune leurs preuves.