Spécification fondatrice · Architecture de référence
ArithSpec — un substrat arithmétique normatif pour réseaux impulsionnels bit-exacts
Tout le reste de ce projet repose sur une seule décision : calculer en arithmétique entière, définie au bit près, plutôt qu’en virgule flottante. Voici la spécification formelle de l’architecture ArithSpec, fondation normative de l’ensemble de cette recherche.
ARITHSPEC · LA DIFFÉRENCE EN UN REGARD
Même entrée. Deux façons d’obtenir un résultat.
La virgule flottante peut varier selon l’environnement d’exécution. ArithSpec fixe les règles du calcul au bit près : pour un même protocole, des implémentations conformes doivent produire le même résultat.
Virgule flottante
Écart possible
Même entrée, deux exécutions. Une variation numérique peut se propager.
ArithSpec · calcul déterministe
Bit à bit
Même entrée, implémentations conformes : les trajectoires se superposent.
- Entrée
- Calcul
- Arrondi
- Propagation
- Sortie
- Rejeu
- Comparaison
Schéma qualitatif, sans données mesurées. La divergence en virgule flottante n’est pas systématique ; son tracé est volontairement accentué pour rendre le phénomène lisible. Le tracé ArithSpec illustre le résultat prescrit pour des implémentations conformes.
Spécification et résultats de conformité : dépôt ArithSpec · DOI 10.5281/zenodo.20723008
Pourquoi supprimer la virgule flottante
Un même programme en virgule flottante, compilé deux fois avec des options différentes, peut produire deux résultats différents. Sur deux architectures processeur, c’est presque garanti. Les écarts sont minuscules — de l’ordre du milliardième — et parfaitement suffisants pour qu’un neurone franchisse son seuil d’un côté et pas de l’autre.
À partir de cet instant, les deux exécutions divergent, et plus rien n’est comparable. Vous ne pouvez plus rejouer une décision à l’identique, ni la comparer à une référence, ni démontrer à un auditeur que le système embarqué s’est comporté comme la version que vous avez validée.
ArithSpec supprime le problème à la racine : arithmétique entière en virgule fixe, arrondi au plus proche pair avec bits de garde, saturation explicite après arrondi, cinq indicateurs d’anomalie observables, sérialisation canonique. Aucune liberté n’est laissée à l’implémentation.
Ce que « normatif » veut dire
Le mot est employé au sens de l’ingénierie des standards, pas au sens philosophique. Une spécification normative prescrit un comportement exact et ne laisse aucune liberté d’implémentation dans les opérations arithmétiques.
Une implémentation conforme doit produire exactement le résultat spécifié — pas une approximation, pas un résultat « équivalent à ε près ». Exactement identique. Bit pour bit.
C’est une exigence beaucoup plus forte que l’accord numérique habituel. « Presque pareil » est interdit. La spécification v2.5 est gelée depuis le 7 juin 2026 : elle ne peut plus changer sans incrémenter la version majeure, précisément pour qu’une empreinte calculée aujourd’hui reste vérifiable dans dix ans.
La famille : Full, Lite, Mini
ArithSpec n’est pas un format unique mais une famille, pour couvrir du serveur au plus petit microcontrôleur. Chaque membre est bit-exact avec lui-même sur toute plateforme — mais les membres ne sont pas bit-exacts entre eux : ce sont des spécifications distinctes.
| Membre | Format | Type natif | Résolution | Usage | Statut |
|---|---|---|---|---|---|
| ArithSpec-Full | INT64 · Q32.32 | int64 / accumulateur int128 | ≈ 2,3 × 10⁻¹⁰ | Référence, PC et serveur | Référence |
| ArithSpec-Lite | INT32 · Q16.16 | int32 / accumulateur int64 | ≈ 1,5 × 10⁻⁵ | Embarqué — Pi, Pico | Certifiée |
| ArithSpec-Mini | INT16 · Q8.8 | int16 | ≈ 3,9 × 10⁻³ | Ultra-embarqué | Travaux futurs |
C’est une façon de ranger un nombre à virgule dans un entier. « Q16.16 » veut dire : 16 bits pour la partie entière, 16 bits pour la partie après la virgule. Le nombre 1,5 s’écrit alors comme l’entier 98 304 (soit 1,5 × 65 536). Toute l’arithmétique se fait sur ces entiers — et comme les entiers ne « flottent » jamais, deux machines obtiennent exactement le même résultat.
La formule qui décide de tout
Le cœur de la spécification, c’est la multiplication. C’est là que se joue la reproductibilité, parce que multiplier deux nombres à virgule fixe produit trop de bits, et qu’il faut en jeter une partie — donc arrondir. Un arrondi mal spécifié, et deux implémentations divergent. ArithSpec impose l’arrondi au plus proche pair (RNE), avec trois bits de contrôle nommés Garde, Arrondi, Sticky.
La règle exacte (ArithSpec-Lite) : si le reste dépasse la moitié, on ajoute 1 ; s’il vaut exactement la moitié, on n’ajoute 1 que si Q est impair. Cette dernière clause — « ties-to-even » — est ce qui élimine le biais statistique de l’arrondi.
La même logique gouverne l’addition, qui sature au lieu de déborder : si le résultat sort de la plage, il est ramené à la borne et lève un indicateur d’anomalie, au lieu de repartir silencieusement à l’autre extrémité comme le ferait un entier machine ordinaire.
À retenir
Chaque opération est spécifiée jusqu’au bit d’arrondi près. C’est fastidieux — et c’est précisément ce qui manque à beaucoup de bibliothèques, où l’arrondi peut dépendre du compilateur. Cette précision maniaque est la fondation de tout le reste.
L’observable : une empreinte
Comment vérifier que deux implémentations sont d’accord, sans les comparer instruction par instruction ? On enregistre toute la trajectoire de calcul, on en prend le SHA-256, et on compare les empreintes. Deux implémentations sont conformes si, et seulement si, elles produisent la même.
C’est un test binaire, sans zone grise. Une empreinte identique prouve un accord bit pour bit sur des centaines de milliers d’opérations ; une empreinte différente le réfute. Il n’y a rien à négocier.
La chaîne de conformité
C’est le résultat le plus concret de ce travail, et le plus facile à réfuter : si une seule plateforme produisait une empreinte différente, la revendication tomberait.
source : campagne du 8 au 16 juin 2026 (protocole non encore publié)
Un second protocole, indépendant, mesure la même propriété à l’échelle d’un réseau : 1 000 neurones et 24 788 synapses exécutés sur x86-64 Windows et sur ARM64 natif (Raspberry Pi 5) produisent une empreinte identique pour la graine canonique et pour cinq graines supplémentaires (article E, §3.5). Sur chaque plateforme, une double exécution donne la même empreinte — le déterminisme intra-plateforme est établi avant toute comparaison inter-plateforme.
Le microcontrôleur physique
La dernière ligne du tableau mérite qu’on s’y arrête. Ce n’est pas un émulateur : c’est un Raspberry Pi Pico réel, une puce RP2040 à double cœur Cortex-M0+. Flashé en MicroPython, il a exécuté par ce chemin, le 16 juin 2026, trois jours après le dépôt de l’article, les 200 000 opérations et produit — au bit près — l’empreinte de référence e1606bef….
La distinction qui compte
Ce qui est certifié ici, c’est le substrat arithmétique : le calcul entier tourne bit-exact du serveur au microcontrôleur. Ce n’est pas un apprentissage embarqué, ni une boucle de décision embarquée : ceux-là restent des objectifs. La reproductibilité du calcul, elle, est établie sur du matériel réel, jusqu’au microcontrôleur Raspberry Pi Pico (chemin MicroPython).
Les modèles formels
Au-delà de la conformité mesurée, cinq modèles ont été soumis à une énumération exhaustive bornée avec l’outil TLC. Le terme est important : ce n’est pas une vérification formelle universelle, c’est l’exploration complète d’un espace d’états fini et déclaré.
TLC2 v2.19, OpenJDK Temurin 21
Voir les données
| Modèle | États distincts | Résultat |
|---|---|---|
| K0Composition | 19 683 | 5 invariants, aucune erreur |
| ArithSpecMonoidal | 1 679 616 (= 36⁴) | 11 invariants, aucune erreur |
| ArithSpecTrace | 343 (= 7³) | 4 invariants, associativité stricte |
| ArithSpecLaxWitness | — | contre-exemple attendu : x=−1, y=1, z=65536 |
| ArithSpecTrace (témoin) | — | contre-exemple attendu : concaténation non commutative |
Périmètre et Limitations
- ArithSpec n’est pas une spécification d’efficacité. Elle prescrit l’exactitude reproductible, pas la vitesse ni la consommation.
- L’exploration TLC est une énumération exhaustive bornée sur des espaces d’états finis déclarés — jamais une preuve universelle.
- La conformité multi-plateforme porte sur le substrat arithmétique. Elle ne dit rien d’un apprentissage ou d’une boucle comportementale embarquée.
- Sur le microcontrôleur, la conformité a été vérifiée par le chemin MicroPython ; les implémentations Rust, C++ et Python l’ont été sur PC ou sur Raspberry Pi 5 (figure 1).
- ArithSpec-Mini (Q8.8) est un objectif déclaré, pas un résultat.
Reproductibilité algorithmique
Le dépôt public
Le document fondateur est déposé en accès ouvert, sous licence CC BY 4.0, en français et en anglais.
Deux identifiants, un seul document. 10.5281/zenodo.20723008 désigne le concept — il pointe toujours vers la dernière version. 10.5281/zenodo.20723009 désigne la version v1 précisément. Pour citer le travail, utilisez le premier.
Reproduire la conformité
Le protocole est court et entièrement spécifié : graine fixe, 200 000 itérations, multiplication normative Q16.16 avec arrondi GRS+RNE, addition saturante, décharge à seuil, transcription binaire de 14 octets par itération, puis SHA-256 de l’ensemble.
SEED = 0x123456789abce900
N_OPS = 200 000
THETA = 1 << 15 (0,5 en Q16.16)
EMIT_CAP = 15
empreinte attendue :
e1606bef1b34afe155adeace4aae7fd2aa22f0236ada22a61dd71631baae050aUne implémentation qui produit cette empreinte est conforme. Une implémentation qui en produit une autre ne l’est pas — et il n’y a rien à négocier.