La fondation : ArithSpec

C’est le document fondateur du programme, et le plus ancien des cinq dépôts. Il spécifie une arithmétique entière assez complètement pour que deux machines quelconques produisent le même résultat au bit près — avec un arrondi au plus proche pair contrôlé par trois bits de garde, et une saturation explicite.

Ses propriétés algébriques ont été explorées par énumération exhaustive bornée : cinq modèles formels (un dans l’article, quatre dans une note non encore publiée), dont deux sont des contre-exemples volontaires montrant où la structure cesse d’être associative. La page dédiée déroule tout cela en détail.

Portée du résultat