Skip to content

enrich(smt,#13410): prose interpretative Z3-Python-12/14 (densite 759/759 -> 1318/1297) #16021

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
jsboige merged 1 commit into from
Sep 13, 2026
Merged

enrich(smt,#13410): prose interpretative Z3-Python-12/14 (densite 759/759 -> 1318/1297) #16021

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
103 changes: 103 additions & 0 deletions MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-12-Real-Arithmetic.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,27 @@
"print(\"Imports OK : z3-solver (theorie Real)\")\n"
]
},
{
"cell_type": "markdown",
"id": "38bab10e",
"metadata": {},
"source": [
"### Lecture : la théorie se choisit à la déclaration, pas à l'import\n",
"\n",
"Le message d'import nomme la théorie, mais `from z3 import *` n'en fixe aucune : il ne\n",
"charge que l'API. C'est la **sorte** des variables qui décide du fragment logique\n",
"interrogé. `Real('x')` place le solveur dans l'arithmétique des réels — un corps réel\n",
"clos, donc décidable ; `Int('x')` le mettrait dans l'arithmétique de Presburger ou de\n",
"Peano selon les opérations employées, avec des propriétés de décidabilité très\n",
"différentes ; `BitVec('x', 32)` ouvrirait la théorie des bit-vectors, où l'addition est\n",
"modulo `2^32`.\n",
"\n",
"Cette remarque commande toute la lecture du notebook : les résultats qui suivent ne\n",
"dépendent pas du solveur mais de la théorie dans laquelle on l'a placé. Un énoncé faux\n",
"en arithmétique non bornée peut devenir vrai et décidable en arithmétique modulaire —\n",
"c'est précisément le sujet du notebook 14 consacré aux bit-vectors."
]
},
{
"cell_type": "markdown",
"id": "ec9c4659",
Expand Down Expand Up @@ -101,6 +122,27 @@
"print(\"-> Solution rationnelle EXACTE (pas d'arrondi flottant).\")\n"
]
},
{
"cell_type": "markdown",
"id": "7d41f5ee",
"metadata": {},
"source": [
"### Lecture : ce que « x = 2 » veut dire exactement\n",
"\n",
"Le modèle rend `2` et `-1`, pas `2.0` et `-1.0`. L'écart n'est pas cosmétique : `Reals`\n",
"désigne la théorie des corps réels clos, où Z3 représente les valeurs comme des\n",
"rationnels **exacts** — numérateur et dénominateur entiers — jamais comme des flottants\n",
"binaires. Là où une résolution numérique rendrait `2.0000000e+00` avec un résidu\n",
"d'arrondi, la réponse d'ici est exacte par construction : substituer `2` et `-1` dans\n",
"`x + y = 1` et `x - y = 3` produit des égalités **vraies**, pas des égalités à epsilon\n",
"près.\n",
"\n",
"La conséquence pratique est plus forte qu'il n'y paraît : un `check()` qui rend `sat`\n",
"sur un système linéaire certifie l'existence d'une solution exacte *et* en fournit une.\n",
"C'est ce qui rend Z3 utilisable quand les coefficients sont des rationnels non\n",
"représentables en binaire — précisément le cas où un solveur flottant dérive."
]
},
{
"cell_type": "markdown",
"id": "8de9b5bc",
Expand Down Expand Up @@ -151,6 +193,27 @@
" print(\" (le suffixe '?' = affichage approche d'un root-obj exact ; x^2 - 2 = 0)\")\n"
]
},
{
"cell_type": "markdown",
"id": "060a6594",
"metadata": {},
"source": [
"### Lecture du `?` : `1.4142135623?` n'est pas un flottant\n",
"\n",
"C'est le point le plus facile à mal lire du notebook. Z3 n'a **pas** rendu le flottant\n",
"`1.4142135623730951` : il a rendu un **objet-racine** (*root-obj*), et le `?` final est\n",
"la marque de l'affichage. Le modèle porte donc la solution sous forme algébrique\n",
"symbolique — la racine positive du polynôme minimal `x^2 - 2 = 0` — et la forme\n",
"décimale n'est qu'un rendu approché, produit au moment de l'affichage.\n",
"\n",
"L'écart se mesure : `1.4142135623 ** 2` vaut `1.999999999793256`, donc à côté de `2` de\n",
"plus de `2e-10` ; l'objet-racine, lui, vérifie `xs * xs == 2` **exactement**. C'est\n",
"toute la différence entre *représenter* un irrationnel et l'*approcher*. Le degré du\n",
"polynôme minimal est l'information qui compte ici — degré 2 pour la racine carrée — et\n",
"c'est ce qui donne son intérêt à l'exercice 1 : la racine cubique est de degré 3, et la\n",
"théorie la traite par le même mécanisme, sans changement d'API."
]
},
{
"cell_type": "markdown",
"id": "1d4ae8f8",
Expand Down Expand Up @@ -196,6 +259,26 @@
" print(\" -> inattendu (devrait etre impossible sur R).\")\n"
]
},
{
"cell_type": "markdown",
"id": "cdf8bbb8",
"metadata": {},
"source": [
"### Lecture : `unsat` est une preuve, pas un échec de recherche\n",
"\n",
"`unsat` se lit souvent comme « le solveur n'a rien trouvé ». Ici c'est l'inverse : sur\n",
"la théorie des réels, `unsat` signifie que la **négation** de l'énoncé est\n",
"insatisfiable, donc que l'énoncé est valide pour *toutes* les valuations. Z3 ne dit pas\n",
"« je n'ai pas trouvé de `xn` tel que `xn^2 + 1 = 0` » ; il dit qu'un tel `xn` n'existe\n",
"pas dans `R`. La traduction algébrique est immédiate : `xn^2 = -1` n'a pas de solution\n",
"réelle puisque le carré d'un réel est positif ou nul — le `discriminant < 0` du trinôme\n",
"dit exactement la même chose, vue par les coefficients.\n",
"\n",
"Cette bascule `sat` / `unsat` est ce qui fait de Z3 un **prouveur** et non seulement un\n",
"chercheur de solutions. Elle sert directement à l'exercice 2, où discriminer deux\n",
"trinômes revient à comparer un `sat` et un `unsat` sur la même famille de formules."
]
},
{
"cell_type": "markdown",
"id": "9bae86e3",
Expand Down Expand Up @@ -249,6 +332,26 @@
" print(\" -> UNSAT : impossible (1 + 2 = 3 < 5, le plus long cote est trop long).\")\n"
]
},
{
"cell_type": "markdown",
"id": "4ce0760e",
"metadata": {},
"source": [
"### Lecture : le même encodage rend `sat` puis `unsat`\n",
"\n",
"Les deux appels partagent exactement la même formule `triangle(...)` — seule change la\n",
"valuation. `(3, 4, 5)` satisfait les trois inégalités ; `(1, 2, 5)` échoue sur celle qui\n",
"compte, `1 + 2 = 3 < 5`. Le point pédagogique est que le prédicat n'a **pas** été\n",
"réécrit pour le second cas : c'est la même conjonction, et c'est le solveur qui découvre\n",
"laquelle des trois inégalités tombe.\n",
"\n",
"Notez la frontière exacte de cet encodage : avec des inégalités **larges**, un triplet\n",
"`(1, 2, 3)` rendrait `sat` alors que le triangle est plat — le cas dégénéré est accepté.\n",
"Exclure les triangles dégénérés demande la forme stricte. C'est le genre d'ajustement où\n",
"le solveur continue de donner la bonne réponse sans qu'on ait à énumérer les cas\n",
"limites à la main."
]
},
{
"cell_type": "markdown",
"id": "56a96676",
Expand Down
137 changes: 137 additions & 0 deletions MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-14-BitVectors-Overflow.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,26 @@
"print(\"Imports OK : z3-solver (theorie BitVec)\")\n"
]
},
{
"cell_type": "markdown",
"id": "e149711c",
"metadata": {},
"source": [
"### Lecture : une théorie de décision, pas une approximation\n",
"\n",
"`from z3 import *` ne fixe aucune théorie : c'est la **sorte** des variables qui la\n",
"choisit. Ce notebook travaille en `BitVec(..., 32)`, c'est-à-dire en arithmétique\n",
"modulaire sur 32 bits, où l'addition est exacte *modulo* `2^32`. C'est ce qui le\n",
"distingue du notebook 12 : là-bas `Real` donnait des rationnels exacts et non bornés,\n",
"ici les valeurs sont bornées par construction et l'enveloppement n'est pas une erreur\n",
"d'arrondi mais la sémantique même de l'opération.\n",
"\n",
"La conséquence est que Z3 reste une **théorie de décision** dans ce fragment : tout\n",
"énoncé du langage des bit-vectors admet une réponse `sat` ou `unsat` en temps fini, et\n",
"cette réponse ne dépend ni d'un pas d'itération ni d'un échantillonnage. C'est ce qui\n",
"autorise à *prouver* des propriétés de débordement plutôt qu'à les tester."
]
},
{
"cell_type": "markdown",
"id": "49849769",
Expand Down Expand Up @@ -101,6 +121,25 @@
"print(\"-> La valeur machine (%d) est INFERIEURE a a (%d) : il y a eu debordement.\" % (somme.as_long(), a.as_long()))\n"
]
},
{
"cell_type": "markdown",
"id": "bec22bf7",
"metadata": {},
"source": [
"### Lecture : le retournement du comparateur\n",
"\n",
"`4 500 000 000` devient `205 032 704`, et ce n'est pas un artefact d'affichage : en\n",
"uint32 l'addition est **modulo 2^32**, donc\n",
"`4 500 000 000 - 4 294 967 296 = 205 032 704`. Le détail qui mérite qu'on s'arrête est\n",
"le dernier : la somme machine est **inférieure** à l'opérande `a`\n",
"(`205 032 704 < 3 000 000 000`). C'est la signature du débordement non signé, et c'est\n",
"ce qui rend le prédicat `somme < a` correct pour le détecter — une addition qui reste\n",
"dans les bornes ne peut pas produire une somme inférieure à l'un de ses termes positifs.\n",
"\n",
"Retenez ce retournement : il fonde les deux sections suivantes, qui posent la même\n",
"inégalité — d'abord sur des valeurs fixées, puis sur des variables symboliques."
]
},
{
"cell_type": "markdown",
"id": "4392ad35",
Expand Down Expand Up @@ -143,6 +182,24 @@
" print(\"-> SAT : ULT(somme, a) tient, le debordement est confirme.\")\n"
]
},
{
"cell_type": "markdown",
"id": "43c4ef93",
"metadata": {},
"source": [
"### Lecture : constater n'est pas prouver\n",
"\n",
"`somme` est ici une **expression construite** à partir de deux valeurs concrètes, pas\n",
"une variable libre. Le `sat` répond donc à une question déjà instanciée : « pour ces\n",
"deux nombres-là, la condition de débordement tient-elle ? ». La réponse est oui, et elle\n",
"se vérifie à la main.\n",
"\n",
"Cette section sert d'étalon : elle fixe la sémantique de `ULT` (*unsigned less-than*,\n",
"qui compare `205 032 704` et `3 000 000 000` comme des entiers positifs) avant que la\n",
"section suivante ne passe aux variables symboliques — là où plus aucune valeur n'est\n",
"fixée et où la réponse ne se vérifie plus sur une calculette."
]
},
{
"cell_type": "markdown",
"id": "e339ddba",
Expand Down Expand Up @@ -201,6 +258,25 @@
" print(\" -> SAT : contre-exemple trouve (le theoreme est faux).\")\n"
]
},
{
"cell_type": "markdown",
"id": "8a8c4d8b",
"metadata": {},
"source": [
"### Lecture : le quantificateur implicite\n",
"\n",
"La formule soumise au solveur est `preconditions ET pas_de_debord`, et le résultat est\n",
"`unsat`. Lisez-le comme un énoncé quantifié : il **n'existe pas** de `x, y` vérifiant à\n",
"la fois `x, y >= 2^31` et « pas de débordement ». La négation étant insatisfiable,\n",
"l'implication « `x, y >= 2^31` entraîne un débordement » est valide pour *toutes* les\n",
"valeurs.\n",
"\n",
"C'est un changement de nature par rapport à la section précédente : Z3 ne teste plus un\n",
"cas, il caractérise tout un demi-espace. Le seuil `2^31 = 2 147 483 648` n'est pas\n",
"arbitraire — c'est exactement la moitié de `2^32`, donc la plus petite valeur à partir\n",
"de laquelle la somme de deux opérandes égaux sort du domaine représentable."
]
},
{
"cell_type": "markdown",
"id": "99f1a62d",
Expand Down Expand Up @@ -257,6 +333,26 @@
" print(\" -> SAT : contre-exemple trouve (improbable).\")\n"
]
},
{
"cell_type": "markdown",
"id": "dfcad37b",
"metadata": {},
"source": [
"### Lecture : la même preuve, retournée\n",
"\n",
"Le notebook refait le raisonnement dans l'autre sens : au lieu de « au-dessus de la\n",
"borne le débordement est inévitable », il établit « en dessous de 1000 il est\n",
"impossible ». Là encore c'est un `unsat` qui porte la preuve, et là encore le seuil est\n",
"là où on l'attend : `1000 + 1000 = 2000` reste très loin de `2^32`, aucune enveloppe\n",
"n'est atteignable.\n",
"\n",
"La symétrie des deux sections dit quelque chose d'utile au praticien : une même théorie\n",
"sert à **détecter** un risque et à **certifier** son absence, les deux requêtes ayant\n",
"exactement la même forme — préconditions *et* négation de la propriété. C'est ce schéma\n",
"qui se transpose à la vérification de bornes dans un parseur binaire ou un contrat\n",
"intelligent."
]
},
{
"cell_type": "markdown",
"id": "a3796f01",
Expand Down Expand Up @@ -317,6 +413,26 @@
"print(\"-> Extract + egalite = raisonnement au niveau champ binaire (protocoles, formats).\")\n"
]
},
{
"cell_type": "markdown",
"id": "85e5c794",
"metadata": {},
"source": [
"### Lecture du témoin : `0xFBFF0000`\n",
"\n",
"Le solveur ne s'est pas contenté de rendre `sat` : il a fourni un **témoin** concret,\n",
"`n = 4 227 792 896 = 0xFBFF0000`, et le notebook en décompose les deux octets bas —\n",
"`0x00` pour les bits 7..0, `0x00` pour les bits 15..8. Les deux octets comparés sont\n",
"donc égaux, ce qui satisfait `octet0 == octet1`.\n",
"\n",
"Notez la contrainte `n != 0` ajoutée explicitement : sans elle, le témoin trivial\n",
"`n = 0` aurait suffi et n'aurait rien montré. C'est le réflexe à garder devant un `sat`\n",
"qui paraît trop facile — vérifier que la requête n'admet pas une solution dégénérée\n",
"avant de lire le témoin. `Extract` est ce qui permet de raisonner au niveau **champ**\n",
"plutôt qu'au niveau entier : protocoles réseau, formats de fichier, registres, partout\n",
"où la question porte sur des bits précis et non sur la valeur globale."
]
},
{
"cell_type": "markdown",
"id": "db8bc537",
Expand Down Expand Up @@ -384,6 +500,27 @@
"print(\"Int : meme predicat sur entiers non bornes -> %s (aucun debordement)\" % sInt.check())\n"
]
},
{
"cell_type": "markdown",
"id": "bc4ee478",
"metadata": {},
"source": [
"### Lecture : ce que la largeur fixe achète\n",
"\n",
"Deux résultats opposés sur le **même** prédicat `a + b < a` avec `b >= 1` :\n",
"\n",
"- en BV4, `sat`, avec le témoin `a = 13, b = 3` : `(13 + 3) mod 16 = 0`, et `0 < 13` ;\n",
"- en `Int`, `unsat` : sur les entiers non bornés, ajouter un `b` positif ne peut pas\n",
" faire diminuer `a`.\n",
"\n",
"Ce couple est la démonstration la plus nette de la section. La théorie `Int` ne peut\n",
"**pas exprimer** le débordement — l'énoncé y est simplement faux — alors que `BitVec` le\n",
"rend vrai et décidable. Choisir la théorie est donc un acte de modélisation, pas un\n",
"détail d'implémentation : un débordement non modélisé n'apparaît pas comme « non\n",
"prouvé » mais comme « prouvé impossible ». C'est exactement le motif des erreurs qui\n",
"échappent à un raisonnement mené en arithmétique non bornée."
]
},
{
"cell_type": "markdown",
"id": "9d87536f",
Expand Down
Loading