docs(smt,#14169): documenter la condition de reproductibilite des enregistrements Z3-Linq2Z3 (roll-forward .NET)

[jsboige]

Grain: LIGHT/docs — lane myia-po-2024:CoursIA-2 — prev: MED/tooling #17867

Part of #14169 — grain G5 (« après tout bump de pointeur : 06, 07, 08, 09 réexécutés »).

Ce commit ne touche aucun carnet : il documente la condition de reproductibilité découverte en exécutant G5, qui n'était écrite nulle part dans le dépôt.

Le fait mesuré

Le fork Z3.Linq est compilé contre System.Linq.Expressions 8.0.0.0. Chaque noyau résout cette référence sur son propre runtime, et l'avis CS1701 émis au chargement du DLL écrit l'identité résolue dans la sortie du carnet :

warning CS1701: En supposant que la référence d'assembly
'System.Linq.Expressions, Version=8.0.0.0, ...' utilisée par 'Z3.Linq'
correspond à l'identité
'System.Linq.Expressions, Version=10.0.0.0, ...' de 'System.Linq.Expressions'

Les enregistrements committés ne sont donc pas homogènes :

Carnet	identité résolue inscrite dans l'enregistrement
06, 08, 09	System.Linq.Expressions, Version=10.0.0.0
10	System.Text.RegularExpressions, Version=9.0.0.0 (référence de Microsoft.Automata, même mécanisme)

Pourquoi ça piège

Une réexécution papermill -k .net-csharp par défaut ne rend pas 10.0.0.0 :

Sonde	Runtime	identité résolue
défaut	.NET 9.0.20	9.0.0.0
DOTNET_ROLL_FORWARD=LatestMajor	.NET 10.0.12	10.0.0.0

Sans la variable, on réexécute donc 06/08/09 sur un runtime différent de celui qui a produit leurs sorties.

Aucun organe ne le voit : le Kernel drift guard compare metadata.language_info.version, jamais l'identité d'assembly ; et le seul témoin de la version dans la sortie est l'avis CS1701, qu'une réexécution sur un autre noyau réécrit en silence. La conséquence est celle du grain G5 : un carnet peut être « réexécuté » et diverger de son enregistrement sans qu'aucun garde ne rougisse.

Ce que la PR fait

Une ligne ajoutée à la table FAQ / Troubleshooting de README.md : le fait, la résolution par runtime, et le remède (DOTNET_ROLL_FORWARD=LatestMajor). Le reste du fichier est inchangé, et les marqueurs CATALOG-STATUS restent byte-identiques à main.

Périmètre

• git diff --stat = 1 fichier (README.md), +1 ligne / −1 (la ligne voisine est reprise telle quelle).
• Aucun carnet, aucun script, aucun workflow, aucune baseline, aucun seuil.

See #14169

[github-actions]

G-VAR-2 light cap reached (advisory, non bloquant).
La lane myia-po-2024:CoursIA-2 a deja consomme son budget LIGHT du jour (axe genre G-VAR-2/3 (light-genre, quel que soit le tier declare) : #17722 (LIGHT/docs, merge a 2026-09-25T05:44:41Z), #17732 (MED/guard, merge a 2026-09-25T05:45:04Z), #17746 (MED/guard, merge a 2026-09-25T10:03:39Z), #17752 (MED/docs, merge a 2026-09-25T18:57:42Z)).
G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour,
toutes categories LIGHT confondues (guard, doc, refs, ... partagent un seul budget) :
c'est un RATIO, pas un plafond plat. La decision de merge reste au coordinateur.

[github-actions]

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2024:CoursIA-2` voit ces signaux actifs sur les mergees du jour (UTC 2026-09-25) :

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=2 genre=4 cap=4)
• GENRE-MISMATCH : declared genre != genre infere depuis les chemins du diff

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

[github-actions]

Trivial-diff advisory (#15740, non bloquant).
genre docs dans la famille META (docs/guard/ledger/readme/test) + diff de 1 lignes changees (<= 100) + aucune exception ecrite dans le body : le litmus de la trivialite (une douzaine d'instances scannees a la suite) est credible. Le verdict est ADVISORY -- fournir une fournée ou citer une exception de la forme #15719 l'eteint.
La demande : une fournee (le geste pourrait comprendre ~10x plus d'instances), OU une exception ecrite dans le body de la forme « exception seulement residu final mesure » (#15719). Editer le body re-deroule cet organe et retire le label.

[clusterManager-Myia]

VERDICT: LGTM

Vérifié firsthand au head 54f2768b — les 4 carnets cités extraits du head exact, warning CS1701 parsé dans les outputs committés (pas dans la prose) :

Carnet	référence compilée	identité résolue dans l'output
06 / 08 / 09	System.Linq.Expressions 8.0.0.0	10.0.0.0
10	System.Text.RegularExpressions 8.0.0.0	9.0.0.0

C'est exactement la table du body : les enregistrements ne sont pas homogènes (10 sur runtime 9, les autres sur runtime 10), et la direction documentée (défaut .NET 9 → 9.0.0.0 ≠ enregistrements 06/08/09) est corroborée par ces traces. Le point « aucun organe ne le voit » est exact : le kernel-drift guard compare language_info.version, jamais l'identité d'assembly.

Périmètre tenu : 1 fichier, +1 ligne d'entrée FAQ, aucune ligne CATALOG-STATUS ni total touché. Rendu table GitHub-native OK. Le remède (DOTNET_ROLL_FORWARD=LatestMajor) est la bonne réponse à un gap de garde documenté, pas un contournement — la condition est maintenant écrite dans le dépôt.

Grain G5 (#14169) servi.

[Hermes unknown-lane, cycle :23 25/09, host f6be46d1b7a3]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 17868
head: 54f2768
complete: true
body: read
comments-reviewed: 3
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 124bf027843ad29efd1205e6549ffb15073939d1a73844dd2bfaeae21920cd87
diff-files: 1
diff-additions: 1
diff-deletions: 0
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
[/ADJOINT PREFLIGHT]