PD-296 — Review de spécification (Gate 3)¶

Type : Contradiction
Référence : §5.2 (mandatory_gates_formal=3) vs §5.5 (F-296-01..05) vs D-296-03
Description : §5.2 déclare « mandatory_gates_formal=3 » correspondant aux Gates 3/5/8.
  Or D-296-03 ne définit aucun checkpoint_id pour Gate 3 — seuls GATE5_PLAN_FORMAL
  et GATE8_FINAL_FORMAL existent. Aucun flux Gate 3 n'apparaît en §5.5.
  Le diagramme de séquence §5bis ne montre pas non plus de checkpoint Gate 3.
  Le document tests §9 confirme cette incohérence comme « Bloquant ».
Impact : Le paramètre mandatory_gates_formal=3 est non vérifiable. Soit il faut
  ajouter un checkpoint Gate 3, soit corriger la borne à 2.
Gravité : Bloquant

Type : Contradiction
Référence : CA-296-01 vs INV-296-01 vs §5.5
Description : CA-296-01 exige que « coherence est exécuté après step 0 ET step 1 »
  avec « deux exécutions distinctes ». Or INV-296-01 exige « exactement 5 checkpoints
  formels » et la liste §5.5 n'inclut pas de checkpoint step 0.
  Le test TC-NOM-06 suppose deux exécutions de coherence avec correlation_id distincts,
  mais seul STEP1_SPEC_COHERENCE est un checkpoint officiel.
  Question : l'exécution step 0 est-elle un checkpoint formel comptabilisé (=> 6
  checkpoints, pas 5) ou une exécution hors comptage (=> CA-296-01 ambiguë) ?
Impact : INV-296-01 et CA-296-01 ne peuvent pas être vrais simultanément sans
  clarification du statut de l'exécution step 0.
Gravité : Bloquant

Type : Incohérence Spec↔Tests
Référence : Tests §2 matrice de couverture + §5 + §7
Description : La matrice de couverture §2 et les tables §5/§7 référencent les tests
  TC-INV-01, TC-INV-02, TC-INV-03 et TC-INV-04. Aucun de ces 4 tests n'a de
  scénario GIVEN/WHEN/THEN défini dans le document.
  - TC-INV-01 : vérifie FSM fermée aux 4 états (INV-296-12)
  - TC-INV-02 : transitions non listées rejetées (INV-296-13)
  - TC-INV-03 : absence mode warning/skip (INV-296-17)
  - TC-INV-04 : audit couverture INV/CA vs tests (INV-296-18)
Impact : 4 invariants critiques (INV-296-12, 13, 17, 18) n'ont pas de scénario
  de test exécutable. La matrice de couverture déclare « Oui » pour ces invariants
  mais les tests n'existent pas.
Gravité : Bloquant

Type : Hypothèse dangereuse
Référence : §5.4 (PASSED -> * : INTERDITE)
Description : PASSED est déclaré « état terminal ». Or les gates 3/5/8 incluent
  une boucle de correction (v1 -> v2 -> v3) : si la spec est modifiée après Gate 3
  NON_CONFORME, STEP1_SPEC_COHERENCE est déjà PASSED mais porte sur un artefact
  obsolète. Aucun mécanisme ne permet de ré-évaluer un checkpoint PASSED après
  modification de l'artefact source.
  Même situation pour STEP6_CODE_FORMAL : si Gate 8 échoue et le code est corrigé,
  le checkpoint step 6 doit pouvoir être relancé.
Impact : Soit le checkpoint PASSED doit pouvoir être réinitialisé (transition
  PASSED -> PENDING manquante), soit la spec doit expliciter que les corrections
  post-gate ne nécessitent pas de ré-évaluation formelle (hypothèse dangereuse).
Gravité : Bloquant

Type : Ambiguïté
Référence : §5.4, §5.7, CLAUDE.local.md (transitions Jira)
Description : La spec définit le cycle de vie des checkpoints dans le workflow
  nominal et la correction (FAILED_BLOCKING -> PENDING). Mais aucun comportement
  n'est spécifié pour :
  - Transition Jira « REJECTED » (TID=3) — les checkpoints sont-ils purgés ?
  - Transition Jira « To Do » (TID=11, reset) — retour à zéro des checkpoints ?
  - Transition Jira « DONE with anomaly » (TID=2) — même contrainte que Done ?
  INV-296-09 interdit Done avec FAIL ouvert, mais ne mentionne pas ces 3 autres
  transitions terminales ou de reset.
Impact : Un opérateur pourrait contourner le blocage formel en utilisant la
  transition « DONE (with anomaly) » au lieu de « Done ».
Gravité : Majeur

Type : Hypothèse dangereuse
Référence : D-296-10
Description : La regex d'artifact_path est fixée à
  `^/Users/loic/Developpement/ProbatioVault/ProbatioVault-[a-z-]+/.+$`.
  Cette contrainte encode un chemin de poste développeur unique. Si le workflow
  est exécuté par un autre opérateur, sur CI, ou sur un chemin différent, tout
  checkpoint sera rejeté en FAILED_BLOCKING.
Impact : L'invariant INV-296-16 (rejet données invalides) devient un faux positif
  systématique hors du poste de Loïc. Contredit implicitement INV-296-10
  (applicabilité tous projets) si exécution multi-poste.
Gravité : Majeur

Type : Ambiguïté
Référence : §5.6 (Clearing conditionnel), §5.2 (clearing_success_cycles_required)
Description : Le mécanisme de clearing exige « N cycles PASSED consécutifs » pour
  lever un « état dégradé ». Mais la notion d'état dégradé n'est définie nulle part :
  - Quand entre-t-on en état dégradé ? Après un FAILED_BLOCKING ? Après réconciliation ?
  - Quel est le scope (par story ? par checkpoint ? global) ?
  - Où est stocké cet état ?
  TC-NOM-12 teste ce mécanisme mais la condition d'entrée en état dégradé est
  implicite (« État dégradé actif » dans le GIVEN).
Impact : Le test TC-NOM-12 n'est pas déterministe — l'état dégradé est un prérequis
  non reproductible sans définition contractuelle.
Gravité : Majeur

Type : Ambiguïté
Référence : D-296-11, §5.6 (Idempotence)
Description : L'idempotency_key est un SHA-256 hex de 64 caractères, mais la spec
  ne précise pas :
  - Qui génère cette clé (appelant ou système) ?
  - Quel est l'input du hash (payload entier ? story_id + checkpoint_id + timestamp ?)
  - Comment éviter les collisions si le hash est laissé à l'appelant ?
  Le test TC-NOM-10 utilise une clé fixe mais ne teste pas la génération.
Impact : Sans contrat de génération, deux implémentations pourraient produire des
  clés incompatibles, rendant l'idempotence non fonctionnelle.
Gravité : Majeur

Type : Incohérence Spec↔Tests (5bis — Cohérence des diagrammes)
Référence : §5bis diagramme de séquence
Description : Le diagramme de séquence montre les appels vers CO (coherence) et
  FV (formal-verify) avec des paramètres informels :
  - CO reçoit `check(predicates(spec_markdown))` — format de predicates non spécifié
  - FV reçoit `verify(invariants(spec) + contracts_yaml + plan_constraints_graph)` — 
    le format de plan_constraints_graph n'est pas un D-296-*
  - FV reçoit `verify_full(extract_facts(code_ast) + TLA+ + Prolog + Alloy + Z)` —
    les formats d'entrée des 4 moteurs ne sont pas contractualisés
  Seul le format de sortie (formal_check_result_json) est spécifié.
Impact : L'interface d'entrée des outils formels n'est pas contractualisable.
  L'hypothèse H-296-01 reconnaît ce risque pour la sortie mais pas pour l'entrée.
Gravité : Majeur

Type : Incohérence Spec↔Tests (5bis — Cohérence des diagrammes)
Référence : §5bis diagramme de séquence vs §5.2 (mandatory_gates_formal=3)
Description : Le diagramme de séquence couvre les flux F-296-01 à F-296-05 mais
  n'inclut aucun checkpoint Gate 3. Ceci est cohérent avec §5.5 mais contredit
  §5.2 (mandatory_gates_formal=3). Le diagramme confirme visuellement l'absence
  de Gate 3 signalée dans l'Écart 1.
Impact : Renforce la contradiction §5.2 vs reste de la spec.
Gravité : Bloquant (lié à Écart 1)

Type : Ambiguïté
Référence : §5.6 (Lock distribué)
Description : Le mécanisme de lock distribué spécifie scope, TTL et comportement
  d'échec, mais pas le backend de lock (fichier .lock, SQLite, Redis, flock...).
  Le projet cible est ia-governance (shell + Python + YAML), pas un service avec
  base de données. Le choix de backend impacte directement la robustesse du lock
  en contexte multi-sessions cmux (LOTR).
Impact : Sans backend contractualisé, deux implémentations pourraient utiliser des
  mécanismes incompatibles (ex: flock vs SQLite), rendant le lock inefficace en
  concurrence inter-sessions.
Gravité : Mineur

Type : Risque sécu/conformité
Référence : Q-296-03, INV-296-17
Description : Q-296-03 demande si le mode « force » existant en escalade gate est
  explicitement interdit pour les échecs formels. INV-296-17 interdit tout mode
  « warning only / informative only / skip », mais ne mentionne pas explicitement
  le mode « force » ou « override » qui existe dans le workflow actuel (cf.
  gov-gate.md v3 NON_CONFORME obligatoire avec choix humain).
  Si l'Article VIII ne couvre pas ce cas, un opérateur pourrait utiliser le
  mécanisme d'escalade existant pour contourner un FAILED_BLOCKING.
Impact : Risque de contournement de l'Article VIII par un mécanisme pré-existant.
Gravité : Majeur

Type : Non testable
Référence : TC-NOM-07
Description : Le test exige l'exécution d'un workflow /gov complet sur 8 stories
  (une par project_code) avec 5 checkpoints chacun et verdicts GO. Cela représente
  40 exécutions de moteurs formels + 8 workflows complets (11 étapes chacun).
  - Temps estimé : 8 × ~2h = ~16h de workflow
  - Dépendances : ChatGPT (steps 1-3, 5, 8), outils formels, Sonar, Jira
  - Coût : significatif en tokens LLM
  Le test est théoriquement valide mais concrètement non exécutable en routine.
Impact : INV-296-10 (pas d'exception projet) ne sera vérifié que par échantillonnage,
  pas par couverture exhaustive.
Gravité : Mineur

Type : Ambiguïté
Référence : §5.2 (rate_limit_checks_per_min_per_story), §5.6
Description : Le rate-limit spécifie « rejet de requête (équivalent 429) » mais
  ne précise pas :
  - Le rejet produit-il un FAILED_BLOCKING ou un simple refus sans changement d'état ?
  - TC-NEG-09 dit « pas de progression » mais pas « FAILED_BLOCKING »
  - Le compteur est-il par fenêtre glissante ou par minute calendaire ?
  §5.6 dit « dépassement => rejet de contrôle (pas de progression) » ce qui suggère
  un refus sans FAILED_BLOCKING, mais c'est en contradiction avec INV-296-16 qui
  exige FAILED_BLOCKING pour toute donnée invalide.
Impact : Ambiguïté sur l'état résultant d'un rate-limit, impactant la FSM.
Gravité : Mineur