PD-297 — Spécification : Review indépendante¶

• Document audité : PD-297-specification.md (revue contractuelle, aucune reformulation ni implémentation)
• Document associé : PD-297-tests.md (audit limité à ambiguïtés / contradictions / règles non testables / risques)
• Domaine : formal (note contextuelle crypto-proof NON APPLICABLE)

1. Contradictions¶

ECART-01 — Clearing conditionnel incompatible avec la FSM¶

• Type : Contradiction
• Référence : PD-297-specification.md §5.6 "Clearing conditionnel" vs §5.5 ENRICHMENT_DEGRADED + INV-297-16 + INV-297-10 ; PD-297-tests.md TC-NR-04
• Description : §5.6 prévoit la "levée du statut dégradé uniquement après clearing_success_cycles_required cycles conformes consécutifs". Or la FSM §5.5 n'autorise QU'UNE seule transition sortante depuis ENRICHMENT_DEGRADED : -> FAILED_BLOCKING (INV-297-16). Toute autre transition est interdite (INV-297-10). Il n'existe donc aucun chemin contractuel pour "lever" le statut dégradé. Par ailleurs, le terme "cycles" n'est pas défini (durée, granularité, scope story/global).
• Impact : Le mécanisme de clearing est contractuellement inatteignable. TC-NR-04 teste une observable qui ne peut pas se produire dans la FSM spécifiée.
• Gravité : Bloquant

ECART-02 — SKIP simultanément interdit à la source ET converti¶

• Type : Contradiction
• Référence : INV-297-06 (« scopes retournent uniquement GO ou FAIL, jamais SKIP ») vs §5.4 F-297-05 (« SKIP est contractuellement interdit et traité comme FAIL ») et ERR-297-09 / TC-ERR-09 (« scope retourne SKIP » → converti en FAIL)
• Description : L'INV-297-06 pose que les scopes NE PRODUISENT JAMAIS SKIP. Les cas d'erreur et tests décrivent pourtant un SKIP reçu puis converti. Soit le moteur peut émettre SKIP (et l'invariant est faux), soit il ne le peut pas (et le cas d'erreur ERR-297-09 + TC-ERR-09 est inobservable). Ambiguïté de responsabilité : contrat d'émission vs contrat de consommation.
• Impact : Verdict formel ambigu ; un test (TC-ERR-09) documenté comme couvrant INV-297-06 porte sur un événement qu'INV-297-06 déclare impossible.
• Gravité : Majeur

ECART-03 — §5.8 nie des flux de coordination mentionnés en §5.6¶

• Type : Contradiction
• Référence : §5.8 (« Atomicité multi-composant DB + queue/append-only: non applicable (pas de flux DB+queue dans PD-297) ») vs §5.6 (lock distribué TTL, stockage d'idempotence avec fenêtre idempotency_window_h, compteurs rate-limit, réconciliation périodique)
• Description : Les mécanismes distribués de §5.6 supposent un stockage d'état partagé (lock, idempotence, compteurs, scanner de réconciliation). §5.8 déclare l'atomicité DB+queue « non applicable ». Le support technique de §5.6 n'est donc ni décrit, ni exclu, ni borné.
• Impact : Hypothèse d'exécution opaque ; impossible d'auditer la cohérence du lock / idempotence sans définition du substrat.
• Gravité : Majeur

ECART-04 — Non-régression : scope du verdict hors enum D-297-05¶

• Type : Contradiction
• Référence : D-297-05 formal_scope (contracts|code|full) vs §5.4 F-297-04 (« check de cohérence … verdict »), §5.7 (« verdicts formal_result_json »), INV-297-14 (« non-régression GO »)
• Description : Le check de non-régression produit un verdict (GO/FAIL) mais son formal_scope n'est listé dans aucun enum. Il n'existe pas de formal_result_json typé pour la non-régression. Pourtant CA-297-05 exige qu'un « rapport de non-régression post-enrichissement » soit archivé et INV-297-14 l'agrège aux verdicts scopes.
• Impact : Le format d'archivage / de preuve du check non-régression est indéterminé ; impossible de valider D-297-21 pour cet artefact.
• Gravité : Majeur

ECART-05 — rate_limit : rejet sans failure_code autorisé¶

• Type : Contradiction
• Référence : §5.6 Rate-limiting et TC-NEG-09 (« rejet exécution (équivalent 429) ») vs D-297-08 failure_code (enum fermé : aucun RATE_LIMITED / RATE_LIMIT_EXCEEDED / THROTTLED)
• Description : Le dépassement de quota provoque un rejet, mais aucun failure_code autorisé ne couvre ce cas. Le seul code plausible est CONCURRENT_RUN, or §5.6 distingue explicitement lock (CONCURRENT_RUN) et rate-limit.
• Impact : formal_result_json non conforme à D-297-21 pour les rejets rate-limit, ou bien fusion sémantique avec CONCURRENT_RUN qui masque la cause.
• Gravité : Majeur

2. Ambiguïtés¶

ECART-06 — « Correction validée » (INV-297-18) non défini¶

• Type : Ambiguïté
• Référence : INV-297-18 (« seule transition retour autorisée, après correction explicite ») et TC-NOM-06 (« défaut corrigé explicitement »)
• Description : Ni « correction validée » ni « relance explicite » ne sont rattachés à un observable contractuel (qui valide ? sur quel critère ? quelle preuve ?). Le déclencheur FAILED_BLOCKING -> PENDING est donc subjectif.
• Impact : Transition retour non auditable ; risque de relance non conforme indétectable.
• Gravité : Majeur

ECART-07 — « Cycles conformes consécutifs » non défini¶

• Type : Ambiguïté
• Référence : §5.6 Clearing conditionnel, clearing_success_cycles_required §5.2
• Description : Le terme « cycle » n'est pas défini : intervalle temporel, occurrence d'événement, run entier, passage de réconciliation ? La granularité (par story / globale) est absente.
• Impact : Critère non testable a priori (cf. aussi ECART-01).
• Gravité : Majeur

ECART-08 — details de formal_result_json non typé¶

• Type : Ambiguïté
• Référence : D-297-21 (clé details obligatoire, structure non précisée)
• Description : La présence de details est obligatoire, son schéma n'est pas contractualisé. La spec le reconnaît d'ailleurs en §10.2 (Q-297-04) et les tests le classent NON TESTABLE §9.
• Impact : Hétérogénéité des preuves, audit non comparable entre runs.
• Gravité : Majeur

ECART-09 — Dérivation story_id -> {norme} non spécifiée¶

• Type : Ambiguïté
• Référence : D-297-14 (regex chemin normes/[a-z0-9-]+/formal/), §5.7 (« mapping story -> domaine -> normes »), §10.2 Q-297-02, PD-297-tests.md §9
• Description : Seule la forme du chemin est contrainte ; la règle métier qui choisit {norme} à partir de story_id/domain_slug n'est pas spécifiée. La spec elle-même acte l'inconnue (Q-297-02) mais la maintient en §4 (H-297-01 suppose un mapping « déterministe »).
• Impact : Cible d'enrichissement potentiellement ambiguë → écriture dans la mauvaise norme → faux positifs/négatifs de non-régression.
• Gravité : Majeur

ECART-10 — Ambiguïté terminologique « check » / « scope » / « non-régression »¶

• Type : Ambiguïté (terminologique) / Contradiction interne
• Référence : §5.4, §5.5 ENRICHED, INV-297-14, INV-297-15
• Description : Les termes « scope » (D-297-05), « check » (§5.4, §5.7), « vérification formelle » (§2) et « non-régression » (§5.4 F-297-04) sont utilisés de manière interchangeable pour désigner des artefacts aux types distincts. Ex. INV-297-15 « si un check retourne FAIL, ERROR ou SKIP » introduit ERROR qui n'est ni dans D-297-07 (verdict) ni dans D-297-08 (failure_code enum : ERROR n'existe pas comme valeur de verdict).
• Impact : Catégorisation des retours moteur non univoque ; difficulté de mapper un run réel sur la FSM.
• Gravité : Majeur

ECART-11 — « Replay strictement identique » inopérant si timestamp_utc dans le payload¶

• Type : Hypothèse dangereuse (proche ambiguïté)
• Référence : INV-297-03, D-297-17 idempotency_key, D-297-21 (clés obligatoires timestamp_utc, correlation_id)
• Description : INV-297-03 exige même idempotency_key, même payload => même résultat. Mais D-297-21 inclut timestamp_utc et correlation_id dans les clés obligatoires. Si ces champs sont dans le payload, deux runs successifs auront presque toujours un payload différent, déclenchant IDEMPOTENCY_CONFLICT (ERR-297-03) au lieu de la déduplication attendue.
• Impact : Idempotence inatteignable en pratique, ou bien la notion de « payload » est implicitement restreinte à un sous-ensemble non défini.
• Gravité : Majeur

ECART-12 — sha256(predicate_atom) : périmètre exact du hash inconnu¶

• Type : Ambiguïté
• Référence : D-297-12 predicate_fingerprint, diagramme §5bis (« EP→>GR: predicate_atom[] + sha256(predicate_atom) »)
• Description : La spec ne précise pas : hash ligne par ligne ou hash du tableau agrégé ? Avec ou sans espaces/fin de ligne ? Canonisation ?
• Impact : Non-reproductibilité des fingerprints entre implémentations → INV-297-03 (replay → fingerprints inchangés) non vérifiable.
• Gravité : Majeur

ECART-13 — INV-297-22 auto-contradictoire avec §9 des tests¶

• Type : Contradiction
• Référence : INV-297-22 (« Toute règle de cette spec est testable via §7/§8 ; sinon classée hors périmètre ») vs PD-297-tests.md §9 qui liste 5 règles NON TESTABLES dont 4 Majeur (Q-297-02, Q-297-03, Q-297-04, Q-297-06).
• Description : L'invariant pose que toute règle est testable OU hors périmètre. Les tests classent des éléments comme NON TESTABLES sans les déclarer hors périmètre. Les deux documents ne sont pas cohérents.
• Impact : INV-297-22 ne peut pas être validé en Gate 3.
• Gravité : Majeur

3. Règles non testables¶

ECART-14 — INV-297-18 conditionné à « correction explicite »¶

• Type : Non testable
• Référence : INV-297-18, TC-NOM-06
• Description : Sans définition observable de « correction explicite / validée » (ECART-06), aucun test ne peut déterminer si une relance est conforme.
• Impact : INV-297-18 non falsifiable ; TC-NOM-06 s'appuie sur une prémisse subjective.
• Gravité : Majeur

ECART-15 — CA-297-16 dépend de documents non figés¶

• Type : Non testable
• Référence : CA-297-16, TC-NOM-08
• Description : La cohérence des fichiers .claude/rules/procedures.md et workflow-rules.md avec PD-297 est un critère d'acceptation, mais aucun hash / version / périmètre n'est contractualisé. Le test TC-NOM-08 parle de « révision figée » sans définir laquelle.
• Impact : Critère d'acceptation observable uniquement par inspection manuelle sans référentiel stable.
• Gravité : Mineur

ECART-16 — « Dégradation gracieuse » rate-limit / clearing non observable¶

• Type : Non testable (lié à ECART-05 / ECART-07)
• Référence : §5.6, TC-NEG-09, TC-NR-04
• Description : Les rejets rate-limit (sans failure_code) et les levées de clearing (sans transition FSM) ne produisent pas d'observable contractuel dans formal_result_json / FSM.
• Impact : Tests correspondants non exécutables sans hypothèses hors contrat.
• Gravité : Majeur

4. Incohérences Spec ↔ Tests¶

ECART-17 — TC-NR-04 (clearing) sans chemin FSM¶

• Type : Incohérence Spec↔Tests
• Référence : PD-297-tests.md TC-NR-04 vs FSM §5.5
• Description : Le test observe une « levée dégradée ». La FSM n'autorise pas ce comportement (cf. ECART-01). L'observable du test n'est pas atteignable sous le contrat actuel.
• Impact : Test non réalisable ; couverture INV-297-20 partielle.
• Gravité : Bloquant

ECART-18 — TC-ERR-09 couvre un événement nié par INV-297-06¶

• Type : Incohérence Spec↔Tests
• Référence : TC-ERR-09 vs INV-297-06
• Description : Le test GIVEN « un scope retourne SKIP ». INV-297-06 pose que les scopes ne retournent jamais SKIP. La condition GIVEN n'est donc jamais observable côté scope conforme.
• Impact : Test écrit pour vérifier une défense en profondeur dont la source contractuelle nie la possibilité.
• Gravité : Majeur

ECART-19 — TC-NEG-09 sans failure_code contractuel¶

• Type : Incohérence Spec↔Tests
• Référence : TC-NEG-09 vs D-297-08
• Description : Test attend « rejet exécution (équivalent 429) », sans code d'erreur autorisé par l'enum (cf. ECART-05).
• Impact : Observable du test non aligné sur D-297-21.
• Gravité : Majeur

ECART-20 — Matrice §2 annonce couverture d'INV-297-22 alors que §9 liste des règles non testables¶

• Type : Incohérence Spec↔Tests
• Référence : PD-297-tests.md §2 ligne INV-297-22 | Oui vs PD-297-tests.md §9
• Description : La matrice revendique une couverture globale d'INV-297-22 (« toute règle testable »), alors que §9 liste 5 règles non testables. Cohérent avec ECART-13.
• Impact : Conformité de la matrice de couverture non valide.
• Gravité : Majeur

5. Hypothèses dangereuses¶

ECART-21 — H-297-04 : stockage d'idempotence durable, mais non contractualisé¶

• Type : Hypothèse dangereuse
• Référence : H-297-04, §5.6, §5.8
• Description : L'idempotence dépend d'un stockage durable (fenêtre 24..168h) dont le support, l'atomicité et la politique de purge ne sont pas définis (§5.8 rejette le cadre DB+queue). Une perte de cet état silencieuse rendrait INV-297-03 faux sans signal.
• Impact : Robustesse retry fragile.
• Gravité : Majeur

ECART-22 — Concurrence append-only multi-repo non spécifiée¶

• Type : Hypothèse dangereuse
• Référence : Q-297-03, F-297-02, F-297-03, INV-297-01
• Description : L'enrichissement écrit dans deux dépôts (ProbatioVault-ia-governance orchestrateur / ProbatioVault-formal cible). L'ordre d'écriture, la résolution de conflit Git, la garantie « append-only » en cas de push concurrent ne sont pas définis.
• Impact : Une race condition Git peut produire une écriture non append-only côté branche sans détection ; viole silencieusement INV-297-01.
• Gravité : Majeur

ECART-23 — max_formal_scopes_per_run = 3 (min=max=3)¶

• Type : Ambiguïté / Hypothèse
• Référence : §5.2 ligne max_formal_scopes_per_run
• Description : Le paramètre est figé à 3. Sa présence comme paramètre configurable avec bornes min=max=3 n'apporte aucun levier ; son sens contractuel est flou (garde-fou ? simple constante ?).
• Impact : Bruit dans la table des bornes, risque d'interprétations divergentes d'implémentation.
• Gravité : Mineur

6. Risques sécurité / conformité¶

ECART-24 — Injection Prolog via predicate_atom¶

• Type : Risque sécurité/conformité
• Référence : D-297-11 predicate_atom regex ^[a-z_][a-z0-9_]*\(.+\)\.$
• Description : La regex n'impose aucune contrainte sur le contenu entre parenthèses. Un contenu dérivé de la spécification (markdown PO) peut injecter des directives Prolog (ex : closure :- halt. collée dans l'argument, clauses imbriquées). Aucune clause de sanitisation / liste blanche de foncteurs n'est définie dans la spec.
• Impact : Contamination de la base formelle, SWI-Prolog exécutant des directives lors du load. Viole INV-297-01 (append-only), Art. VIII (fail-closed) et l'intégrité de la base partagée entre toutes les stories.
• Gravité : Bloquant

ECART-25 — Aucune clause d'autorisation sur le déclencheur step 10¶

• Type : Risque sécurité/conformité
• Référence : §5.1, §5.7, H-297-03
• Description : Ni le contrôle d'identité du process déclencheur, ni la signature des faits ajoutés, ni la journalisation d'auteur ne sont contractualisés. H-297-03 pose que « les permissions sont disponibles » sans exiger de vérification.
• Impact : Un processus disposant du disque peut injecter des prédicats non traçables à un acteur, rompant l'auditabilité (INV-297-02) au-delà du seul champ trace_source (qui reste déclaratif, non cryptographique).
• Gravité : Majeur

ECART-26 — trace_source déclaratif, non contraint par la source réelle¶

• Type : Risque conformité
• Référence : D-297-16, INV-297-02
• Description : Le format de trace_source est contraint syntaxiquement (PD-\d+:slug:ligne) mais rien n'exige qu'il corresponde effectivement à la source d'extraction (spec MD / code-contracts YAML). Un run peut apposer un trace_source faux et néanmoins respecter le contrat.
• Impact : Traçabilité opposable en façade mais non vérifiable. Invariant INV-297-02 facilement contournable.
• Gravité : Majeur

7. Cohérence des diagrammes (axe 5bis)¶

ECART-27 — Séquence §5bis omet lock / idempotence / rate-limit¶

• Type : Incohérence diagramme ↔ invariants
• Référence : Diagramme de séquence §5bis, §5.6, F-297-01
• Description : Le diagramme sequenceDiagram démarre directement par GR->>EP: parse(...), sans étape d'acquisition de lock, ni vérification d'idempotency_key, ni contrôle rate-limit. Or F-297-01 impose l'acquisition du lock avant toute écriture, et §5.6 impose la déduplication idempotence en amont.
• Impact : La séquence contractuelle ne reflète pas les protections de §5.6 ; un lecteur peut implémenter les écritures sans les garde-fous distribués.
• Gravité : Majeur

ECART-28 — Diagramme d'état : transitions redondantes « INTERDITE »¶

• Type : Cohérence diagramme (mineur)
• Référence : Diagramme stateDiagram-v2 §5bis
• Description : Le diagramme déclare des transitions INTERDITE entre toutes paires d'états, ce qui est contractuellement exact mais rend le diagramme quasi illisible (plus de 30 transitions « INTERDITE »). Aucun écart vs §5.5 n'est introduit.
• Impact : Forme — pas de risque sémantique.
• Gravité : Mineur

ECART-29 — Séquence : transformations formal_scope non typées¶

• Type : Cohérence diagramme ↔ modèle de données
• Référence : Diagramme §5bis, D-297-05, D-297-21
• Description : Les appels verify_contracts / verify_code / verify_full renvoient formal_result_json{scope=..., verdict=...} mais le diagramme ne spécifie pas la forme d'entrée (fichier, payload JSON, CLI args). Les règles axe 5bis exigent que les transformations de données soient explicites côté entrée ET sortie.
• Impact : Ambiguïté d'interface entre gov-retrospective et formal-verify.
• Gravité : Mineur

8. Synthèse (indicatif, non normatif)¶

Écarts Bloquants : ECART-01, ECART-17, ECART-24.

Aucune correction, reformulation ou implémentation n'est proposée (contrat de revue).