15 — Théorie des bit-vectors Z3 : vérifier le débordement arithmétique

Notebook de la série Z3 / SMT (Track C#, Z3.Linq fork). Démontre une théorie Z3 jamais exercée dans les 14 notebooks précédents : les bit-vectors (BV8/BV16/BV32/BV64), le domaine SMT canonique pour la vérification matérielle et logicielle (entiers bornés, débordement, arithmétique modulaire). Stack : B — API brute Microsoft.Z3 (MkBV/MkBVAdd/MkBVULT/MkExtract), pas le DSL Z3.Linq : la théorie des bit-vectors n’est pas exposée par le binding.

Pourquoi ce notebook

Les notebooks 01-14 couvrent les entiers non bornés (IntSort) : Sudoku, coloration de graphe, cryptarithmétique, planification. Mais aucun ne manipule de bit-vectors — or c’est la théorie Z3 originelle (Z3 est né chez Microsoft Research pour la vérification de drivers et de matériel). La question que ce notebook pose, et qu’aucun entier non borné ne saurait formaliser :

Pour des entiers 32 bits, l’addition a + b déborde-t-elle ? Et peut-on le prouver ?

L’arithmétique machine enveloppe (3000000000 + 1500000000 ne donne pas 4500000000 en uint32), là où l’arithmétique mathématique ne déborde jamais. Z3 sait raisonner modulo 2³² ET prouver qu’un débordement se produit (ou n’en produit pas) pour des entrées données — exactement le service qu’un compilateur sûr ou un vérificateur de code attend d’un solveur SMT.

Prong-B (non-trivial) : le cas n’est pas dégénéré. Sur des entiers non bornés, a + b ≥ a toujours (addition croissante) — l’overflow est impossible par construction. C’est précisément la borne 32 bits qui rend le débordement possible et sa preuve intéressante : la théorie BV crée le phénomène que l’on demande ensuite à Z3 de certifier. Un notebook d’entiers non bornés ne pourrait pas le faire.

1. Théorie des bit-vectors (SMT-LIB `BitVec`)

Un bit-vector est une suite de n bits interprétée comme un entier modulo 2ⁿ. Z3 en fait une théorie de décision (pas une approximation) : l’addition, la multiplication, les comparaisons et les opérations bit-à-bit sont définies modulo 2ⁿ et décidables.

Sorte	Plage (non signé)	Usage canonique
`BV8`	0 … 255	octets, `char`
`BV16`	0 … 65 535	`uint16`, ports
`BV32`	0 … 4 294 967 295	`uint32`, pointeurs 32 bits
`BV64`	0 … 1.8 × 10¹⁹	`uint64`, horodatages

Deux lectures coexistent pour un même motif binaire : non signé (UGE/ULT — unsigned greater/less than) et signé (SGE/SLT — interprétation complément à 2). C’est cette dualité qui rend les bugs d’overflow subtils : un calcul peut être correct en non signé et déborder en signé, ou inversement.

#r "../Z3.Linq/.deploy/Microsoft.Z3.dll"
#r "../Z3.Linq/.deploy/ExpressionUtils.dll"
#r "../Z3.Linq/.deploy/Z3.Linq.dll"
using Z3.Linq; using Microsoft.Z3; using System; using System.Text;
Console.OutputEncoding = Encoding.UTF8;

var ctx = new Context();
// Sorte bit-vector 32 bits (entiers modulo 2^32)
BitVecSort bv32 = ctx.MkBitVecSort(32);

// Preuve de vie du solveur sur cette théorie
var s0 = ctx.MkSolver();
s0.Assert(ctx.MkTrue());
Console.WriteLine($"Z3 .NET charge sur la théorie BitVec. Trivia check : {s0.Check()}");
Console.WriteLine($"Sorte créée : {bv32}  (entiers modulo 2^32 = {(ulong)Math.Pow(2,32):N0})");

Z3 .NET charge sur la théorie BitVec. Trivia check : SATISFIABLE
Sorte créée : (_ BitVec 32)  (entiers modulo 2^32 = 4 294 967 296)

2. Le débordement se produit (et Z3 le calcule)

Additionnons deux valeurs dont la somme mathématique dépasse 2³². En uint32, 3 000 000 000 + 1 500 000 000 = 4 500 000 000 mathématiquement, mais la valeur machine enveloppe (retranche 2³²).

// Deux valeurs dont la somme dépasse 2^32 = 4 294 967 296
BitVecExpr a = ctx.MkBV(3000000000U, 32);   // 3 milliards : tient en uint32, dépasse Int32 signé
BitVecExpr b = ctx.MkBV(1500000000U, 32);   // 1,5 milliard

BitVecExpr somme = ctx.MkBVAdd(a, b);       // addition modulo 2^32

uint va = ((BitVecNum)a).UInt;
uint vb = ((BitVecNum)b).UInt;
uint vs = ((BitVecNum)somme.Simplify()).UInt;   // Simplify() force l'évaluation concrète
ulong mathematique = (ulong)va + vb;        // somme non bornée (ulong)

Console.WriteLine($"  a = {va:N0}");
Console.WriteLine($"  b = {vb:N0}");
Console.WriteLine($"  a + b (mathématique)   = {mathematique:N0}");
Console.WriteLine($"  BV32(a + b)            = {vs:N0}   <-- valeur machine");
Console.WriteLine($"  Perte par enveloppe    = {mathematique - vs:N0}");
Console.WriteLine();
Console.WriteLine("-> Le débordement a BIEN eu lieu : la valeur machine n'égale pas la somme mathématique.");

  a = 3 000 000 000
  b = 1 500 000 000
  a + b (mathématique)   = 4 500 000 000
  BV32(a + b)            = 205 032 704   <-- valeur machine
  Perte par enveloppe    = 4 294 967 296

-> Le débordement a BIEN eu lieu : la valeur machine n'égale pas la somme mathématique.

3. Détecter le débordement (Z3 comme vérificateur)

Calculer le débordement ne suffit pas — on veut le certifier. Un débordement non signé se détecte par un test simple : après une addition somme = a + b de valeurs non signées, si somme < a alors le débordement s’est produit (car sans débordement on aurait toujours somme ≥ a puisque b ≥ 0). Demandons à Z3 si ce test est satisfait pour nos deux entrées fixes :

// Pour a, b fixés : la condition somme < a (unsigned) est-elle vraie ?
var solver = ctx.MkSolver();
solver.Assert(ctx.MkBVULT(somme, a));   // somme < a  (unsigned less-than) = débordement
Status st = solver.Check();

Console.WriteLine($"Requête « somme < a » pour a=3e9, b=1.5e9 : {st}");
Console.WriteLine(st == Status.SATISFIABLE
    ? "  -> SAT : Z3 confirme que le débordement s'est produit sur ces entrées."
    : "  -> inattendu (somme < a devrait être vrai ici).");

Requête « somme < a » pour a=3e9, b=1.5e9 : SATISFIABLE
  -> SAT : Z3 confirme que le débordement s'est produit sur ces entrées.

Démonstration par réfutation (UNSAT)

Mieux : prouvons que le débordement est inévitable pour toute entrée assez grande. C’est la forme canonique d’une preuve de propriété en SMT : nier la propriété, obtenir UNSAT, conclure.

Théorème : pour tout x, y ≥ 2³¹, l’addition x + y déborde en BV32.

Pourquoi 2³¹ ? Si x, y ≥ 2³¹ alors x + y ≥ 2³² exactement — la borne de uint32 — donc l’enveloppement est inévitable. (Avec 2³⁰ ce serait faux : 2³⁰ + 2³⁰ = 2³¹ < 2³², pas de débordement — d’où la précision du seuil.)

On nie : « préconditions x,y ≥ 2³¹ ET pas de débordement (somme ≥ x) » et on demande à Z3. Si UNSAT, le théorème est prouvé.

// Pour x, y SYMBOLES (quelconques), prouvons : x,y >= 2^31  =>  x+y déborde
BitVecExpr x = (BitVecExpr)ctx.MkConst("x", bv32);
BitVecExpr y = (BitVecExpr)ctx.MkConst("y", bv32);
BitVecExpr sxy = ctx.MkBVAdd(x, y);

BoolExpr preconditions = ctx.MkAnd(
    ctx.MkBVUGE(x, ctx.MkBV(0x80000000U, 32)),   // x >= 2^31 = 2 147 483 648
    ctx.MkBVUGE(y, ctx.MkBV(0x80000000U, 32))    // y >= 2^31
);
BoolExpr pasDebord = ctx.MkBVUGE(sxy, x);          // somme >= x  = pas de débordement

// Nions la propriété : preconditions ET pas de débordement
var s2 = ctx.MkSolver();
s2.Assert(ctx.MkAnd(preconditions, pasDebord));
Status st2 = s2.Check();
Console.WriteLine($"« x,y >= 2^31 ET somme >= x (pas de débord) » : {st2}");
Console.WriteLine(st2 == Status.UNSATISFIABLE
    ? "  -> UNSAT : Z3 PROUVE que pour x,y >= 2^31, le débordement est inévitable."
    : "  -> SAT : contre-exemple trouvé (le théorème est faux).");
if (st2 == Status.SATISFIABLE) {
    var m = s2.Model;
    Console.WriteLine($"     Contre-exemple : x={((BitVecNum)m.ConstInterp(x)).UInt}, y={((BitVecNum)m.ConstInterp(y)).UInt}");
}

« x,y >= 2^31 ET somme >= x (pas de débord) » : UNSATISFIABLE
  -> UNSAT : Z3 PROUVE que pour x,y >= 2^31, le débordement est inévitable.

4. Réciproque : prouver l’absence de débordement

La même mécanique prouve l’absence de débordement sous une précondition. C’est le cas d’usage réel des analyseurs statiques : « si les entrées sont petites, l’addition est sûre ». On nie : « p,q < 1000 ET débordement » et on attend UNSAT.

// Propriété : si p < 1000 ET q < 1000, alors p+q ne déborde pas (somme >= p)
BitVecExpr p = (BitVecExpr)ctx.MkConst("p", bv32);
BitVecExpr q = (BitVecExpr)ctx.MkConst("q", bv32);
BitVecExpr spq = ctx.MkBVAdd(p, q);

BoolExpr petites = ctx.MkAnd(
    ctx.MkBVULT(p, ctx.MkBV(1000, 32)),
    ctx.MkBVULT(q, ctx.MkBV(1000, 32))
);
BoolExpr debord = ctx.MkBVULT(spq, p);   // débordement = somme < p

// Nions : petites ET débordement -> UNSAT prouve « petites => pas de débordement »
var s3 = ctx.MkSolver();
s3.Assert(ctx.MkAnd(petites, debord));
Status st3 = s3.Check();
Console.WriteLine($"« p,q < 1000 ET débordement » : {st3}");
Console.WriteLine(st3 == Status.UNSATISFIABLE
    ? "  -> UNSAT : Z3 PROUVE que pour p,q < 1000, l'addition uint32 ne déborde jamais."
    : "  -> SAT : contre-exemple trouvé (improbable).");

« p,q < 1000 ET débordement » : UNSATISFIABLE
  -> UNSAT : Z3 PROUVE que pour p,q < 1000, l'addition uint32 ne déborde jamais.

5. Opérations bit-à-bit et extraction de champs

Les bit-vectors ne sont pas que de l’arithmétique modulaire : Z3 raisonne aussi sur les opérations bit-à-bit (ET, OU, XOR, décalages) et l’extraction de sous-champs (MkExtract) — la brique des analyseurs de protocoles et de formats binaires, où l’on isole un octet ou un drapeau dans un mot de 32 bits.

// Combiner arithmétique et bit-à-bit : extraction de champ
BitVecExpr n = (BitVecExpr)ctx.MkConst("n", bv32);

// Extraire l'octet de poids faible (bits 0-7) et l'octet suivant (bits 8-15)
BitVecExpr octet0 = ctx.MkExtract(7, 0, n);    // bits 7..0   -> BV8
BitVecExpr octet1 = ctx.MkExtract(15, 8, n);   // bits 15..8  -> BV8

// Question : existe-t-il n NON NUL tel que octet0 == octet1 (les deux octets bas égaux) ?
var s4 = ctx.MkSolver();
s4.Assert(ctx.MkEq(octet0, octet1));
s4.Assert(ctx.MkNot(ctx.MkEq(n, ctx.MkBV(0, 32))));   // forcer un témoin non trivial
Status st4 = s4.Check();
Console.WriteLine($"« octet bas == octet suivant » : {st4}");
if (st4 == Status.SATISFIABLE) {
    var m4 = s4.Model;
    uint vn = ((BitVecNum)m4.ConstInterp(n)).UInt;
    uint o0 = ((BitVecNum)m4.Eval(octet0, true)).UInt;
    uint o1 = ((BitVecNum)m4.Eval(octet1, true)).UInt;
    Console.WriteLine($"  Témoin : n = {vn} = 0x{vn:X8}");
    Console.WriteLine($"    octet0 (bits 7..0)  = 0x{o0:X2}");
    Console.WriteLine($"    octet1 (bits 15..8) = 0x{o1:X2}");
}
Console.WriteLine();
Console.WriteLine("-> MkExtract + égalité = raisonnement au niveau champ binaire (protocoles, formats).");

« octet bas == octet suivant » : SATISFIABLE
  Témoin : n = 4294836481 = 0xFFFE0101
    octet0 (bits 7..0)  = 0x01
    octet1 (bits 15..8) = 0x01

-> MkExtract + égalité = raisonnement au niveau champ binaire (protocoles, formats).

B4 - Largeur de bit-vector declarative (DSL `[BitVecWidth(n)]`)

Tout le notebook jusqu’ici cable la sorte BitVec a la main (ctx.MkBitVecSort(32), MkBVAdd, MkBVULT). Cote DSL, le binding Z3.Linq laisse declarer la largeur par un attribut C# - [BitVecWidth(n)] sur une propriete entiere d’une classe ordinaire - et route automatiquement +/-/* vers les opérateurs modulaires et les comparaisons vers l’ordre non signe (ExpressionVisitor.cs:120, largeur lue en Theorem.cs:548). Sans cet attribut, toute variable entiere d’un theoreme Z3.Linq est un entier mathematique non borne - et le debordement, coeur de ce notebook, devient inexprimable.

Stack : A + B - pourquoi. Ce bloc appartient a la famille “théorie cachee” (comme les reels ou les UNSAT cores) : l’attribut [BitVecWidth(n)] encode une sémantique (l’arithmetique modulo 2^n) qu’aucune ligne de code n’affiche - elle vit dans le type. Le raw MkBitVecSort + MkBVAdd + MkBVULT materialise cette même sémantique en appels Z3 explicites. Le contraste rend visible ce que la largeur fixe achete : le predicat a + b < a (debordement) est SAT en 4 bits mais UNSAT sur les entiers - même requête, deux théories.

// B4 - Largeur de bit-vector declarative "[BitVecWidth(n)]" : deux stacks sur le MEME predicat de debordement.
// Predicat non-trivial : "a + b < a" avec b >= 1
//   - SAT   sur bit-vectors 4 bits (la somme enveloppe modulo 16, sous a)   <- theorie BitVec
//   - UNSAT sur entiers non bornes (une somme a addend positif ne decroit jamais)  <- theorie Int
// Ce contraste EST ce que la largeur fixe achete : sans elle, le debordement est inexprimable.

// Classes au niveau cellule (requises par NewTheorem<T>) : la largeur vit dans le TYPE.
public class Reg4      { [BitVecWidth(4)] public int A { get; set; }  [BitVecWidth(4)] public int B { get; set; } }  // registres 4 bits, 0..15, mod 16
public class PlainPair { public int A { get; set; }  public int B { get; set; } }                                    // meme forme, SANS largeur = entiers non bornes

// =====================================================================
// BLOC RAW (API brute Microsoft.Z3) : on cable la sorte BV4 et les operateurs modulaires a la main
// =====================================================================
{
    using var z3 = new Microsoft.Z3.Context();
    BitVecSort bv4 = z3.MkBitVecSort(4);
    BitVecExpr ra = (BitVecExpr)z3.MkConst("a", bv4);
    BitVecExpr rb = (BitVecExpr)z3.MkConst("b", bv4);

    var sBv = z3.MkSolver();
    sBv.Assert(z3.MkBVUGE(rb, z3.MkBV(1, 4)));                 // b >= 1        (unsigned)
    sBv.Assert(z3.MkBVULT(z3.MkBVAdd(ra, rb), ra));            // a + b < a     (unsigned) = debordement
    Status stBv = sBv.Check();
    Console.WriteLine($"[RAW] BV4  : \" a+b < a  avec b>=1 \" -> {stBv}");
    if (stBv == Status.SATISFIABLE) {
        var mBv = sBv.Model;
        uint wa = ((BitVecNum)mBv.ConstInterp(ra)).UInt;
        uint wb = ((BitVecNum)mBv.ConstInterp(rb)).UInt;
        Console.WriteLine($"[RAW]   Temoin : a={wa}, b={wb} -> (a+b) mod 16 = {(wa + wb) % 16} < a={wa}   (enveloppe)");
    }

    // Le meme predicat sur des entiers non bornes (sorte Int) : pas de debordement possible
    var sInt = z3.MkSolver();
    IntExpr ia = z3.MkIntConst("a");
    IntExpr ib = z3.MkIntConst("b");
    sInt.Assert(z3.MkGe(ia, z3.MkInt(0)));
    sInt.Assert(z3.MkGe(ib, z3.MkInt(1)));
    sInt.Assert(z3.MkLt(z3.MkAdd(ia, ib), ia));               // a + b < a  sur les entiers
    Console.WriteLine($"[RAW] Int  : meme predicat sur entiers non bornes -> {sInt.Check()}   (aucun debordement)");
}

// =====================================================================
// BLOC DSL (Z3.Linq) : la largeur est declaree par attribut, les operateurs sont routes automatiquement
// =====================================================================
{
    using var thCtx = new Z3Context();

    // Stack DSL, theorie BV4 : le meme predicat de debordement, ecrit en arithmetique C# naturelle
    var bv = thCtx.NewTheorem<Reg4>()
        .Where(r => r.B >= 1)
        .Where(r => r.A + r.B < r.A)      // + route vers MkBVAdd, < vers MkBVULT (Theorem.cs:548)
        .Solve();
    Console.WriteLine($"[DSL] Reg4 ([BitVecWidth(4)]) : predicat de debordement -> {(bv != null ? "SAT" : "UNSAT")}");
    if (bv != null)
        Console.WriteLine($"[DSL]   Temoin : A={bv.A}, B={bv.B} -> (A+B) mod 16 = {(bv.A + bv.B) % 16} < A={bv.A}   (enveloppe)");

    // Meme requete SANS l'attribut = entiers non bornes : le debordement disparait
    var noWidth = thCtx.NewTheorem<PlainPair>()
        .Where(p => p.A >= 0)
        .Where(p => p.B >= 1)
        .Where(p => p.A + p.B < p.A)
        .Solve();
    Console.WriteLine($"[DSL] PlainPair (entiers non bornes) : meme predicat -> {(noWidth != null ? "SAT" : "UNSAT")}");
    Console.WriteLine(noWidth == null
        ? "[DSL]   -> UNSAT : sans largeur fixe, \" a+b < a \" est impossible. L'attribut EST la semantique."
        : "[DSL]   -> inattendu.");
}

[RAW] BV4  : " a+b < a  avec b>=1 " -> SATISFIABLE
[RAW]   Temoin : a=15, b=3 -> (a+b) mod 16 = 2 < a=15   (enveloppe)
[RAW] Int  : meme predicat sur entiers non bornes -> UNSATISFIABLE   (aucun debordement)
[DSL] Reg4 ([BitVecWidth(4)]) : predicat de debordement -> SAT
[DSL]   Temoin : A=15, B=3 -> (A+B) mod 16 = 2 < A=15   (enveloppe)
[DSL] PlainPair (entiers non bornes) : meme predicat -> UNSAT
[DSL]   -> UNSAT : sans largeur fixe, " a+b < a " est impossible. L'attribut EST la semantique.

Lecture B4 - l’attribut porte la théorie

Les deux stacks posent le même predicat non-trivial - a + b < a avec b >= 1 - et arrivent au même double verdict : SAT sur 4 bits (la somme enveloppe sous a), UNSAT sur les entiers non bornes (une somme a addend positif ne decroit jamais). La différence est ou vit la largeur :

Aspect	RAW (`MkBitVecSort + MkBV*`)	DSL (`[BitVecWidth(n)]` + `Solve`)
Declaration de la largeur	Imperative : `MkBitVecSort(4)` a chaque variable	Declarative : attribut sur la propriete
Choix des opérateurs	Explicite : `MkBVAdd`, `MkBVULT` (l’utilisateur sait que c’est modulaire)	Implicite : `+` et `<` routes vers les variantes BV (ExpressionVisitor.cs:120)
Lisibilite du predicat	`MkBVULT(MkBVAdd(a,b), a)`	`r.A + r.B < r.A` (arithmetique C# naturelle)
Risque d’erreur	Confondre `MkBVSLT` (signe) et `MkBVULT` (non signe)	Le routage non signe est fixe par le binding
Sans largeur	(choix impossible a oublier)	Entier non borne : debordement inexprimable (UNSAT)

Ligne de contraste (a retenir) : le raw expose la sorte et les opérateurs modulaires (contrôle total : signe vs non signe, largeurs mixtes) ; le DSL deplace la largeur dans le type - l’attribut [BitVecWidth(4)] est la declaration que “ces entiers sont des registres 4 bits”, et le debordement en decoule sans un seul appel Z3 ecrit a la main. Même théorie SMT ((_ BitVec 4) dans les deux), deux endroits ou la largeur est ecrite.

Cas d’usage : on prefere le DSL quand le modèle a des champs de largeur fixe naturels (registres, octets de protocole, compteurs qui enveloppent) - la largeur devient une propriete du type, pas un paramètre repete. On bascule en raw pour les largeurs dynamiques, l’arithmetique signee, ou l’Extract/Concat au niveau bit (cf section 5) que l’attribut ne couvre pas.

6. Ce que ce notebook a démontré

Le débordement arithmétique est impossible sur les entiers non bornés (par construction a+b ≥ a) et décidable sur les bit-vectors (théorie SMT complète). Ce notebook a exercé la théorie BitVec jamais couverte par les notebooks 01-14 :

Calcul du débordement (3e9 + 1.5e9 enveloppe à 205032704 en uint32, perte exacte de 2³²).
Détection pour des entrées fixes (somme < a ⟹ SAT = débordement confirmé).
Preuve universelle par réfutation (UNSAT) : pour tout x,y ≥ 2³¹, le débordement est inévitable.
Réciproque : preuve d’absence de débordement sous p,q < 1000.
Bit-à-bit : extraction de champs (MkExtract) et recherche de témoin.

La leçon SMT : un solveur ne se limite pas à trouver des solutions (SAT) — il certifie des propriétés (UNSAT = preuve). C’est exactement la frontière entre « ça a l’air de marcher » (tests) et « c’est prouvé » (vérification formelle), et c’est le service que Z3 rend à la vérification de code, à la cryptographie et à la conception matérielle.

Prochaines étapes

Vers l’optimisation : le notebook 11_Optimize_MaxSAT aborde les théories d’optimisation ; un prolongement naturel serait les UNSAT cores (quelles contraintes causent l’insatisfiabilité ?) pour le débogage de spécifications.
Vers la vérification de programmes : combiner BitVec avec les quantificateurs pour vérifier des invariants de boucles (preuve de terminaison / correction de boucles critiques sur des entiers machine).

7. Exercices

Trois exercices pour approfondir. Stubs incomplets (return / TODO) — le notebook s’exécute de bout en bout même non complété (convention C.1).

Exercice 1 — Débordement signé vs non signé

La valeur 0xFFFFFFFF vaut 4294967295 non signé mais -1 signé (complément à 2). Construisez une addition qui déborde en signé mais pas en non signé.

Indice : MkBVSLT (signed less-than) détecte le débordement signé ; MkBVULT (unsigned) le non signé. Choisissez a, b proches de Int32.MaxValue = 2147483647.

// Exercice 1 : compléter la démo signé-vs-non-signé
void DemoSigneVsNonSigne(Context ctx) {
    BitVecSort bv32 = ctx.MkBitVecSort(32);
    // TODO etudiant : a, b tels que a+b déborde en SIGNE mais pas en non signé
    // Etape 1 : choisir a, b (valeurs proches de Int32.MaxValue = 2147483647)
    // Etape 2 : montrer que MkBVUGE(somme,a) est vrai (pas de débord non signé)
    //           mais que MkBVSLT(somme, 0) est vrai (débord signé -> négatif)
    Console.WriteLine("Exercice 1 à compléter.");
    return;
}
DemoSigneVsNonSigne(ctx);

Exercice 1 à compléter.

Exercice 2 — Borne exacte du débordement

Pour a = b = t, trouvez la plus grande valeur de t telle que t + t ne déborde pas en BV32. Vérifiez votre réponse avec Z3 (encoder t + t < t et chercher le seuil).

Indice : t + t < 2^32 ⟺ t < 2^31. La réponse est donc 2^31 - 1. Encodez la propriété de débordement MkBVULT(tt, t) et vérifiez qu’elle devient SAT exactement à t = 2^31.

// Exercice 2 : trouver la borne exacte du débordement pour a=b=t
BitVecExpr t = (BitVecExpr)ctx.MkConst("t", bv32);
BitVecExpr tt = ctx.MkBVAdd(t, t);
// TODO etudiant : encoder « t + t déborde » (tt < t unsigned) et trouver la plus petite t SAT
// Etape 1 : BoolExpr debord = ctx.MkBVULT(tt, t);
// Etape 2 : solver.Check avec contrainte t >= 2^31 -> SAT ; avec t = 2^31-1 -> pas de débord
Console.WriteLine("Exercice 2 à compléter.");

Exercice 2 à compléter.

Exercice 3 — Multiplication et débordement

L’addition déborde à partir de sommes ≥ 2³². La multiplication déborde bien plus tôt. Prouvez que 65536 * 65536 déborde en BV32 (résultat mathématique = 2³², exactement la borne — donc enveloppement à 0).

Indice : MkBVMul, puis vérifiez que le produit < 65536 (unsigned) ou == 0.

// Exercice 3 : prouver que 65536 * 65536 déborde en BV32
BitVecExpr m1 = ctx.MkBV(65536, 32);
BitVecExpr m2 = ctx.MkBV(65536, 32);
// TODO etudiant : BitVecExpr produit = ctx.MkBVMul(m1, m2);
// Etape 1 : encoder le débordement (produit < m1 unsigned, ou produit == 0)
// Etape 2 : solver.Assert(...) -> Check -> prouver
Console.WriteLine("Exercice 3 à compléter.");

Exercice 3 à compléter.

Conclusion

Ce notebook introduit la théorie des bit-vectors, dernier domaine SMT canonique non couvert par les notebooks 01-14 (limités aux entiers non bornés IntSort) et brique fondamentale de la vérification matérielle et logicielle (entiers bornés, débordement, arithmétique modulaire) :

Le débordement y est décidable (et non approché) : addition, multiplication, comparaisons et opérations bit-à-bit sont définies modulo 2ⁿ, Z3 en fait une théorie complète.
La preuve par réfutation est le patron canonique : nier la propriété universelle (« tout x, y ≥ 2³¹ déborde ») et obtenir UNSAT certifie le théorème ; nier la sûreté (« p, q < 1000 et débordement ») prouve la réciproque d’absence.
Les deux stacks convergent vers le même prédicat non-trivial a + b < a : l’API brute MkBV* câble la sorte à la main, le DSL [BitVecWidth(n)] déporte la largeur dans un attribut déclaratif — double verdict SAT sur 4 bits (enveloppement), UNSAT sur les entiers non bornés.

Points clés :

Le débordement est impossible par construction sur les entiers non bornés (a + b ≥ a), mais inévitable et calculable sur les bit-vectors : c’est l’écart exact que la théorie BitVec capture.
MkExtract (extraction de champs) ouvre la modélisation des formats binaires et protocoles, où l’on isole un octet ou un drapeau dans un mot de 32 bits.
Le seuil 2³¹ (et non 2³⁰) pour le théorème d’inévitabilité n’est pas anecdotique : 2³⁰ + 2³⁰ = 2³¹ < 2³² ne déborde pas — la précision de la borne est elle-même une leçon de modélisation.

Référence : la théorie BitVec est normalisée par SMT-LIB (logiques QF_BV et BV) et constitue le socle des model checkers matériels (STP, Boolector, Z3) pour la vérification de circuits et d’analyseurs statiques. La suite (notebook 16 — Real Arithmetic) quitte le domaine discret pour l’arithmétique des réels.

Retour au sommet