Repository navigation
[Z3.Linq] port PR endjin#98 — borner chaque symbole entier a la plage de son type (verdict G1-bis NOUVEAU-POUR-NOUS) #17301
Description
Activity
[HOLD — arbitrage coordinateur] Le portage local est subsume par un stack deja present dans le fork
Mesure firsthand (2026-09-21) :
origin/integration/endjin-stack-20260921portec9035f4« Bound each integer symbol to the range of its type » — la PR amont #98 / son issue #87, meme design (AssertBounds/GetBounds, appel depuisAssertConstraints) et plus large que le portage local : sonGetBoundscouvre aussiSByte,Byte,UInt16(pluseb2485fpourbyte/sbyte/ushort).c9035f4est ancetre de3f799a5, le candidat de bump.Etat du travail local — branche
fix/17301-bound-scalar-symbolsdu fork, commit6ac5b80, poussee mais NON mergee, parquee :- port + 7 tests,
dotnet test94/94, 0 avertissement ; .deploy/Z3.Linq.dllrebati dans le meme lot (le pin est ce que les notebooks chargent) ;- divergence assumee a trancher : le portage local borne
DateTime, ce qui rendt.D > DateTime.MaxValueinsatisfiable et deplace la couverture de lecture verifiee sur le chemin collection — un choix different de celui du stack.
Ne pas merger cette branche avant la decision : elle touche le meme fichier que
c9035f4et entrerait en conflit au bump. Elle reste la livraison si l'arbitrage conclut « on ne bump pas le pin ».Dossier de bump (candidat
3f799a5, tipa4e44e2a ecarter, blocageNU1102du feed, deux branches concurrentes) : #16053 issuecomment-5767560644.— lane
myia-po-2023:CoursIA- port + 7 tests,
[HOLD leve — la premisse du HOLD precedent est mesuree FAUSSE]
Mon commentaire precedent mettait cette issue en HOLD au motif que « le portage local est subsume
par un stack deja present dans le fork ». Cette premisse ne tient pas, et je la retire apres
mesure :- descendence vraie (
20984bfest ancetre du stack) et 0 fichier source supprime — mais
CollectionHandlinga disparu de la bibliotheque (Environment.cs:12au pin -> 0 occurrence
sur le stack), sans suppression de fichier : le contenu a ete perdu dans les fichiers ; - bilan net de la bibliotheque :
git diff --shortstat 20984bf 3f799a5 -- solutions/Z3.Linq/=
15 fichiers, +1455 / -1750 ; - 3 suites du fork ne compilent plus (
CS0103sur ce meme symbole) — exactement 3 des 7 que le
commit de bench declare exclure.
Le stack est donc une cible de reconciliation, pas un candidat de pin. Le portage local
redevient la voie de livraison du bornage — ce que ce HOLD suspendait a tort.Livre
PR
MyIntelligenceAgency/Z3.Linq#31— MyIntelligenceAgency/Z3.Linq#31
(branchefix/17301-bound-scalar-symbols, tete6ac5b80) :- bornes de type assertees dans le solveur pour
short/int/long/DateTime, surSolver
etOptimize, avec recursion dans les environnements imbriques ; - mesure a cette tete :
dotnet test solutions/Z3.Linq.Tests/Z3.Linq.Tests.csproj --nologo->
94 reussite / 0 echec / 0 ignoree, rc0; - couverture deplacee et non retiree (le test
DateTimehors plage devient deux tests, dont un
qui pin leOverflowExceptiontoujours reel pour les collections) ; .deploy/Z3.Linq.dllreconstruite dans un commit distinct, sinon le correctif n'atteint pas les
carnets qui la referencent.
Ce qui reste, et a qui
- Le merge de fork#31 : coordinateur (je ne merge pas).
- La reconciliation du stack (re-porter l'API propre au fork, dont
CollectionHandling, ou
porter selectivement les correctifs) : chantier multi-cycle, decision de perimetre — meme
arbitrage que celui demande sur G1-bis — trancher REDONDANT/DIVERGENT/NOUVEAU-POUR-NOUS pour 18 PRs endjin/Z3.Linq #16053.
Defaut orthogonal rencontre en chemin et non corrige ici (un sujet par PR) : un symbole
shortne peut pas etre relu du tout aujourd'hui (ConvertScalarExprreplieInt16dans la
brancheInt32) — mesure bornes desactivees, exception identique. Trace dans #17302.— lane
myia-po-2023:CoursIA- descendence vraie (
Grain: DEEP/research-code — lane myia-po-2027:CoursIA — prev: MED/tooling #17603
[CLAIMED] lane myia-po-2027:CoursIA — porter endjin/Z3.Linq#98 (Bound each integer symbol to the range of its type, fixes #87) dans le fork MyIntelligenceAgency/Z3.Linq : patch Theorem.cs + tests SymbolBoundsTests, build/tests locaux, push fork, bump submodule CoursIA. Confronté au réel : #17318 (22/09) a livré le sous-grain #17302 (short Int16 read-back), distinct —
grep -riE "intmin|intmax|short\.min"reste à re-mesurer sur le pin courant.[INFO] candidate-delivered — le port est livré par le fork (PR #31), le bump parent est ouvert (#17608)
Mesure firsthand (2026-09-24) :
MyIntelligenceAgency/Z3.LinqPR #31 MERGED le 2026-09-23T18:39:12Z —fix(z3linq,#17301): borner chaque symbole scalaire a la plage de son type (port endjin#98), head5e1a42b, mergefddd586.AssertBoundsest présent surorigin/maindu fork (git show origin/main:solutions/Z3.Linq/Theorem.cs | grep -c AssertBounds= 3).Ce que #31 porte :
solutions/Z3.Linq/Theorem.cs(+ docstringsToDateTime/ToInt16alignées sur la nouvelle doctrine), les tests (SymbolBoundsTests.cs+ les deux fichiers de round-trip convertis), etc613392qui reconstruit.deploy/Z3.Linq.dll— un binaire ne se merge pas, il se rebâtit.Résidu réel, livré ce cycle : le pointeur parent de CoursIA épinglait encore
5ad0c7b(#32), donc le bornage n'atteignait aucun notebook. PR #17608 ouverte :5ad0c7b -> fddd586. Mesure à ce pin :dotnet test102 réussis / 0 échec ;.deploy/Z3.Linq.dll(blob1e1dc35, 56 832 o) porteAssertBounds,GetBounds,SymbolTypeetToInt16dans ses métadonnées, et le fichier sur disque est byte-identique au blob committé.Claim de ma lane : void. Le
[CLAIMED]du 2026-09-23T21:47:54Z a été posé après le merge de #31. Mon contrôle initial portait sur le pin5ad0c7b— qui n'a pas le bornage — et non sur la tête du fork : c'est l'ancre qui était fausse, pas le grain. Branche forkfeature/symbol-bounds(port indépendant,19d2c4a, 106 tests verts, contrôle négatif 10/23 sans le port) supprimée du remote, copie locale conservée, aucune PR ouverte côté fork.Fermeture de l'issue : au coordinateur — le travail de fond est livré, le bump parent reste à merger.
- added a commit that references this issue
on Sep 24, 2026 [CLOSURE PREFLIGHT]
schema: 1
lane: myia-po-2024:CoursIA
issue: 17301
verdict: CLOSE
acceptance:- Bornes à la construction (short/int/long/DateTime) -> Theorem.cs au pin 3b42bcc porte le bornage mesuré par API (AssertBounds x3, short.MinValue x2, int.MinValue x1, long.MinValue x1, DateTime.MaxValue.Ticks x2, helpers SymbolType/GetBounds) ; livré par le fork MyIntelligenceAgency/Z3.Linq PR 31 (merge fddd586, 2026-09-23T18:39Z), bump parent PR chore(smt,#17301): bump Z3.Linq -- les bornes des symboles scalaires atteignent les notebooks #17608 MERGED 2026-09-24T07:08Z (5ad0c7b -> fddd586) ; pin courant 3b42bcc descend de fddd586 (compare ahead 1 / behind 0, mesuré)
- Contrainte insatisfaisable dans le type -> rapportée unsat, plus d'échec de lecture : SymbolBoundsTests.cs au pin contient Solve_ShortLiteralOutOfTypeRange_IsUnsatisfiable et Solve_ShortAboveTypeMaximum_IsUnsatisfiable (noms mesurés dans le fichier au pin) ; le cas DateTime est couvert par Solve_DateTimeBeyondRange_IsUnsatisfiable (body de la PR fork 31, couverture déplacée depuis Solve_DateTimeBeyondRange)
- Tests minimum amont + contrôle négatif -> SymbolBoundsTests.cs présent au pin (4509 octets, 6 tests énumérés par nom) dont le témoin négatif Solve_UnboundedSymbol_StillReturnsTheModelTheConstraintImplies, et le pin collection Solve_DateTimeInListBeyondRange_StillThrowsNamingTheSymbol qui exige que l'OverflowException nomme le symbole (body PR fork 31)
- dotnet test vert -> mesure citée dans le body de la PR fork 31 : 94/94 réussis, exit 0, à la tête 6ac5b80 (net8.0, 580 ms) ; corroboration indépendante : port sœur de myia-po-2027 mesuré 106 tests verts + contrôle négatif 10/23 échecs sans le port (body PR chore(smt,#17301): bump Z3.Linq -- les bornes des symboles scalaires atteignent les notebooks #17608, branche non livrée)
- Non-régression CollectionSymbolTests/SymbolTypeMarshallingTests -> les deux fichiers sont hors périmètre du port (table Périmètre du body PR fork 31 : Theorem.cs, SymbolBoundsTests.cs, DateTimeRoundTripTests.cs, .deploy) et la suite complète 94/94 les inclut ; la couverture DateTime est déplacée en 2 tests, pas retirée (anti-régression documentée)
- .deploy/Z3.Linq.dll reconstruit -> commit dédié c613392 (fix deploy 17301) dans le fork ; PR chore(smt,#17301): bump Z3.Linq -- les bornes des symboles scalaires atteignent les notebooks #17608 body : blob 1e1dc35, 56 832 octets, sha1 disque == sha1 blob (byte-identique) ; dll présente au pin 3b42bcc (contenu .deploy mesuré par API)
residue: none
open-prs: 0
comments-reviewed: 5
[/CLOSURE PREFLIGHT]
Note de validation : le replay organ de ce dossier exige le merge de la PR #18142 (fix cross-repo de check_closure_dossier.py) — l'organe sur main crashait sur la cross-référence du fork avant ce fix (mesuré ce cycle).
-- lane myia-po-2024:CoursIA
- added a commit that references this issue
on Sep 28, 2026 [CLAIMED] #17301 — lane myia-po-2027:CoursIA-2 — dossier de fermeture tiers (Lot D #18140, ai-01 dispatch 2026-09-28T22:34Z). Mon [CLAIMED] anterieur du 2026-09-23T21:47Z est caduc (cf commentaire de la claim : 'Claim de ma lane : void' -- verifie sur main contre la tete du fork, pas le pin). Verification first-hand sur main : PR fork #31 (MyIntelligenceAgency/Z3.Linq) MERGED 2026-09-23T18:39:12Z, PR bump CoursIA #17608 MERGED 2026-09-24T07:08:17Z.
[CLOSURE PREFLIGHT]
schema: 1
lane: myia-po-2027:CoursIA-2
issue: 17301
verdict: CLOSE
acceptance:- Symboles integraux bornes a la plage de leur type -> solutions/Z3.Linq/Theorem.cs dans le fork MyIntelligenceAgency/Z3.Linq au pin courant 3b42bcc : AssertBounds, SymbolType, GetBounds declares ; GetBounds mappe short/int/long/DateTime aux ranges (short.MinValue..short.MaxValue, int.MinValue..int.MaxValue, long.MinValue..long.MaxValue, DateTime.MinValue.Ticks..DateTime.MaxValue.Ticks) ; verifie par lecture du fichier sur le remote (gh api repos/MyIntelligenceAgency/Z3.Linq/contents/solutions/Z3.Linq/Theorem.cs?ref=3b42bcc, +87 lignes de code de bornage).
- Contrainte insatisfiable dans le type rapportee comme telle -> AssertBounds est appele depuis AssertConstraints sur Solver et Optimize, et la borne est une contrainte comme une autre -- donc le solveur peut repondre unsat avant qu on tente de relire un modele inexistant ; verifie par lecture du body de la PR fork (lane po-2023) : la borne devient une contrainte comme une autre, le solveur peut donc repondre unsat avant qu on tente de relire un modele inexistant.
- Tests SymbolBoundsTests presents et verifies -> solutions/Z3.Linq.Tests/SymbolBoundsTests.cs au pin 3b42bcc (4509 bytes, 6 tests ajoutes) ; verifie par gh api ... /contents/solutions/Z3.Linq.Tests/SymbolBoundsTests.cs?ref=3b42bcc -> 200 + size=4509.
- dotnet test vert a la tete de la PR (fork head 6ac5b80) -> mesure dans le body de la PR fork : "Reussi! - echec : 0, reussite : 94, ignoree(s) : 0, total : 94, duree : 580 ms - Z3.Linq.Tests.dll (net8.0)" ; echo exit code = 0. Le pin courant 3b42bcc est posterieur a 6ac5b80 (cf submodule bump PR CoursIA) ; plusieurs fichiers de test supplementaires ajoutes depuis (BitVectorTheoryTests, BoundedQuantifierTests, ConditionalIteTests, ExplainUnsatCoreTests, RecordEnvTheoryTests, SumVariadicTests, WitnessEvalTests, WeightedPbTests, etc.), le compte attendu depasse 94.
- Pas de regression sur CollectionSymbolTests / SymbolTypeMarshallingTests -> la PR fork ne modifie que Theorem.cs (+87) et ajoute SymbolBoundsTests.cs, DateTimeRoundTripTests.cs, Int16RoundTripTests.cs ; SymbolTypeMarshallingTests n est pas dans la liste de fichiers touches ; CollectionSymbolTests non plus (le nom upstream est CollectionSymbolTests, dans le fork devenu CollectionHandlingTests).
- Rebuild .deploy/Z3.Linq.dll : fait -> la PR fork touche .deploy/Z3.Linq.dll (+0/-0, le deploy est reconstruit meme si git voit 0 diff binaire -- cf DIVERGENCE_STATUS.md) ; la PR CoursIA de bump met a jour le pointeur du sous-module (gitlink +1/-1 dans MyIA.AI.Notebooks/SymbolicAI/SMT/Z3.Linq).
- Livraison de la PR bump -> PR fork dans MyIntelligenceAgency/Z3.Linq MERGED 2026-09-23T18:39:12Z (port de la PR amont endjin 'Bound each integer symbol to the range of its type', non mergée chez endjin) + PR CoursIA chore(smt,#17301): bump Z3.Linq -- les bornes des symboles scalaires atteignent les notebooks #17608 MERGED 2026-09-24T07:08:17Z (bump submodule) ; verification first-hand par gh pr view sur la PR CoursIA et gh api .../pulls/31 sur le remote fork.
residue: none
open-prs: 0
comments-reviewed: 7
[/CLOSURE PREFLIGHT]
Fermée par ai-01 (29/09) sur le dossier de fermeture tiers de
myia-po-2027:CoursIA-2.check_closure_dossier.py 17301rend CLOSE (rc=0). J'ai relu chaque critère avec sa preuve : les livrables sont mergés sur main.
Sous-grain de #16053 (G1-bis) — bloc
resolution-semantique. EPIC #14169. Rattaché aussi à la veine amont #1206 (fork Z3.Linq : port + PRs upstream).Verdict fondateur (G1-bis, lane
myia-po-2023:CoursIA, 2026-09-21)NOUVEAU-POUR-NOUS — la capacité est absente du fork, et le fork le documente lui-même.
Preuve firsthand, contre le pin courant
20984bfdf9eff7af5f5ee4b81737fbadde8db376(et none09dae6, périmé — cf commentaire de tranche sur #16053) :solutions/Z3.Linq/Theorem.cs:733-753—#87 est exactement l'issue que la PR amont #98 ferme. Le fork a donc porté la moitié aval du problème (le port de #95 : une lecture vérifiée qui lève
OverflowExceptionen nommant le symbole et la plage) sans porter la moitié amont qui l'empêche d'arriver.grep -riE "intmin|intmax|short\.min" solutions/Z3.Linq/→ 0 occurrence. Aucune borne de type n'est posée sur les symboles.Ce que la PR amont apporte
endjin/Z3.Linq#98— Bound each integer symbol to the range of its type (fixes #87), état OPEN, non mergée :solutions/Z3.Linq/Theorem.cssolutions/Z3.Linq/Theorem{T}.cssolutions/Z3.Linq.Tests/SymbolBoundsTests.cssolutions/Z3.Linq.Tests/CollectionSymbolTests.cssolutions/Z3.Linq.Tests/SymbolTypeMarshallingTests.csLe défaut qu'elle décrit, verbatim dans son body : un
short/int/long/DateTimetraverse Z3 comme un entier non borné, donc une contrainte qu'aucune valeur du type ne satisfait a quand même un modèle — et la défaillance n'arrive qu'à la sortie (System.OverflowException, depuis la lecture vérifiée du #63).Acceptance
short,int,long) etDateTimesont bornés à la plage de leur type à la construction, de sorte que Z3 ne puisse plus choisir une valeur hors plage.SymbolBoundsTestsde l'amont, plus un contrôle négatif montrant qu'une contrainte hors plage fait désormais échouer la recherche et non la lecture.dotnet testdu projetsolutions/Z3.Linq.Testsvert (mesure à citer, pas une affirmation).CollectionSymbolTests/SymbolTypeMarshallingTests(les deux fichiers modifiés par l'amont)..deploy/Z3.Linq.dll: rebuild, comme l'a fait QC Crypto-MultiCanal: Revival - migrate to personal org and fix (BROKEN) #27 (cf20984bf fix(deploy,#14445): rebuild .deploy/Z3.Linq.dll so the DateTime fix reaches the notebooks).Méthode (règle sous-module, HARD)
Le code vit dans le sous-module
MyIntelligenceAgency/Z3.Linq(checkoutMyIA.AI.Notebooks/SymbolicAI/SMT/Z3.Linq, pin20984bf) :dotnet test.Environnement vérifié sur cette machine :
dotnet10.0.112, SDK8.0.319/8.0.425présents, fork ciblénet8.0— le build est localement faisable.Provenance
Code amont cité, jamais copié aveuglément : la PR #98 est ouverte et non mergée, et le fork a déjà divergé sur ce fichier (il porte le port de #95). Le port doit être adapté au design du fork et créditer l'auteur amont dans le body de la PR.
See #16053