PD-297 — Boucle d’enrichissement formel contractuelle (capitalisation inter-stories)¶

1. Objectif¶

La User Story PD-297 DOIT fermer la boucle formelle du workflow /gov : à chaque story DONE, la base formelle DOIT être enrichie de manière traçable et idempotente (Prolog, TLA+, Alloy, Z), puis validée par non-régression. Les scopes contracts, code et full DOIVENT produire un verdict GO ou FAIL (jamais SKIP).

2. Périmètre / Hors périmètre¶

Inclus¶

• Enrichissement append-only des prédicats de story dans ProbatioVault-formal.
• Persistance des invariants dérivés des code-contracts dans les 4 formalismes (prolog, tla, alloy, z).
• Vérification de non-régression sur base formelle étendue.
• Verdict formel obligatoire GO|FAIL pour contracts, code, full.
• Intégration contractuelle au step 10 (gov-retrospective).
• Protection distribuée (lock, idempotence, réconciliation, rate-limit, clearing).
• Traçabilité story-source de tout artefact enrichi.

Exclu¶

• Modification du contenu normatif existant (hors append-only d’enrichissement).
• Enrichissement rétroactif des stories historiques déjà DONE.
• Changement de comportement fonctionnel hors PD-297 dans les autres steps.
• Toute règle non testable est hors périmètre.

3. Définitions¶

4. Invariants (non négociables)¶

5. Flux nominaux¶

5.1 Modèle de données contractuel (source unique des formats)¶

Référencement unique: toutes les sections suivantes réutilisent ces IDs (D-297-*) sans redéfinir les formats.

5.2 Bornes numériques contractuelles¶

5.3 SLA temporels (transitions d’état)¶

Aucune autre transition temporelle identifiée.

5.4 Flux nominaux contractuels¶

1. F-297-01 — Déclenchement step 10
2. Entrées minimales valides: D-297-01 à D-297-05, D-297-09, D-297-17 à D-297-21.
3. Le lock distribué (D-297-18) DOIT être acquis avant toute écriture.

4. Transition: PENDING -> EXTRACTING.

5. F-297-02 — Extraction/persistance Prolog

6. Transformation obligatoire: spec_markdown + code_contracts -> predicate_atom[] (D-297-11) + fingerprint (D-297-12).
7. Persistance append-only dans D-297-10, avec trace_source (D-297-16) pour chaque entrée.

8. En cas d’erreur/timeout extraction ou persistance: EXTRACTING -> ENRICHMENT_DEGRADED.

9. F-297-03 — Enrichissement TLA+/Alloy/Z

10. Transformation obligatoire: code_contracts -> invariant_id[] (D-297-15) + cibles D-297-14 pour formalism (D-297-13).
11. Les 4 formalismes sont obligatoires pour un run validé.

12. Échec partiel sur un formalisme: état non validable (ENRICHMENT_DEGRADED puis FAILED_BLOCKING).

13. F-297-04 — Non-régression formelle

14. Le check de cohérence DOIT s’exécuter sur la base étendue.

15. Contradiction détectée: ENRICHED -> FAILED_BLOCKING, failure_code=NON_REGRESSION_CONTRADICTION.

16. F-297-05 — Vérification scopes contracts, code, full

17. Pour chaque scope (D-297-05), verdict obligatoire (D-297-07) sur D-297-21.
18. SKIP est contractuellement interdit et traité comme FAIL (failure_code=SKIP_FORBIDDEN).
19. Tous scopes GO + non-régression GO => ENRICHED -> VERIFICATION_PASSED.

20. Sinon => ENRICHED -> FAILED_BLOCKING.

21. F-297-06 — Clôture step 10

22. Seul VERIFICATION_PASSED -> DONE autorise la clôture.
23. Tant que l’état n’est pas DONE, la transition de clôture story est interdite.

5.5 Machine d’états (transitions retour explicites)¶

États: PENDING, EXTRACTING, ENRICHED, ENRICHMENT_DEGRADED, VERIFICATION_PASSED, FAILED_BLOCKING, DONE.

État PENDING¶

État EXTRACTING¶

État ENRICHED¶

État ENRICHMENT_DEGRADED¶

État VERIFICATION_PASSED¶

État FAILED_BLOCKING¶

État DONE (terminal)¶

Comportement de retour/downgrade: - ENRICHED -> FAILED_BLOCKING: les données déjà enrichies sont conservées (aucune suppression), clôture interdite. - FAILED_BLOCKING -> PENDING: historique conservé, quotas/rate-limit réappliqués immédiatement, verrouillages maintenus jusqu’à DONE. - Transition inverse directe non listée: interdite.

Checklist machine à états: - [x] Chaque état liste ses transitions sortantes (autorisées ou interdites). - [x] État terminal explicite: DONE -> * : INTERDITE (état terminal, résolution manuelle uniquement). - [x] Modèle couvert par invariants dédiés (INV-297-09 à INV-297-19).

5.6 Mécanismes de protection distribuée¶

Checklist protection distribuée: - [x] Lock: scope + TTL + comportement lock non acquis. - [x] Idempotence: clé + durée de déduplication. - [x] Réconciliation: intervalle + seuil orphelin + rattrapage. - [x] Rate-limit: granularité + quota + comportement dépassement. - [x] Clearing: nombre de cycles + mécanisme de comptage.

5.7 Contraintes inter-modules¶

5.8 Clauses obligatoires “non applicables”¶

• Stratégie de migration DDL: non applicable (aucune colonne SQL modifiée).
• Atomicité multi-composant DB + queue/append-only: non applicable (pas de flux DB+queue dans PD-297).
• Invariant envelope encryption crypto: non applicable (domaine formal/tooling, pas crypto/crypto-proof).

5bis. Diagrammes (obligatoire)¶

Diagramme d’état (stateDiagram-v2)¶

stateDiagram-v2
    [*] --> PENDING

    PENDING --> EXTRACTING: trigger_step10 + lock_ok
    PENDING --> ENRICHED: INTERDITE
    PENDING --> ENRICHMENT_DEGRADED: INTERDITE
    PENDING --> VERIFICATION_PASSED: INTERDITE
    PENDING --> FAILED_BLOCKING: INTERDITE
    PENDING --> DONE: INTERDITE

    EXTRACTING --> ENRICHED: extraction+persistance 4 formalismes OK
    EXTRACTING --> ENRICHMENT_DEGRADED: timeout|error extraction/persistance
    EXTRACTING --> PENDING: INTERDITE
    EXTRACTING --> VERIFICATION_PASSED: INTERDITE
    EXTRACTING --> FAILED_BLOCKING: INTERDITE
    EXTRACTING --> DONE: INTERDITE

    ENRICHED --> VERIFICATION_PASSED: non_regression=GO + contracts/code/full=GO
    ENRICHED --> FAILED_BLOCKING: contradiction|timeout|error|SKIP_FORBIDDEN
    ENRICHED --> PENDING: INTERDITE
    ENRICHED --> EXTRACTING: INTERDITE
    ENRICHED --> ENRICHMENT_DEGRADED: INTERDITE
    ENRICHED --> DONE: INTERDITE

    ENRICHMENT_DEGRADED --> FAILED_BLOCKING: fail_closed obligatoire
    ENRICHMENT_DEGRADED --> PENDING: INTERDITE
    ENRICHMENT_DEGRADED --> EXTRACTING: INTERDITE
    ENRICHMENT_DEGRADED --> ENRICHED: INTERDITE
    ENRICHMENT_DEGRADED --> VERIFICATION_PASSED: INTERDITE
    ENRICHMENT_DEGRADED --> DONE: INTERDITE

    FAILED_BLOCKING --> PENDING: correction + relance explicite
    FAILED_BLOCKING --> EXTRACTING: INTERDITE
    FAILED_BLOCKING --> ENRICHED: INTERDITE
    FAILED_BLOCKING --> ENRICHMENT_DEGRADED: INTERDITE
    FAILED_BLOCKING --> VERIFICATION_PASSED: INTERDITE
    FAILED_BLOCKING --> DONE: INTERDITE

    VERIFICATION_PASSED --> DONE: cloture_step10
    VERIFICATION_PASSED --> PENDING: INTERDITE
    VERIFICATION_PASSED --> EXTRACTING: INTERDITE
    VERIFICATION_PASSED --> ENRICHED: INTERDITE
    VERIFICATION_PASSED --> ENRICHMENT_DEGRADED: INTERDITE
    VERIFICATION_PASSED --> FAILED_BLOCKING: INTERDITE

    DONE --> PENDING: INTERDITE
    DONE --> EXTRACTING: INTERDITE
    DONE --> ENRICHED: INTERDITE
    DONE --> ENRICHMENT_DEGRADED: INTERDITE
    DONE --> VERIFICATION_PASSED: INTERDITE
    DONE --> FAILED_BLOCKING: INTERDITE
    DONE --> [*]

Diagramme de séquence (sequenceDiagram)¶

sequenceDiagram
    participant GR as gov-retrospective
    participant EP as extract-eb-predicates
    participant EI as extract-formal-invariants
    participant OF as ProbatioVault-formal (ontology/models)
    participant CO as coherence check
    participant FV as formal-verify
    participant FC as formal-check wrapper

    GR->>EP: parse(spec_markdown + code_contracts_yaml)
    EP-->>GR: predicate_atom[] + sha256(predicate_atom)

    GR->>OF: append_only_write(PD-XXX.pl, predicate_atom[], trace_source)
    GR->>OF: regenerate_ontology(domains+terms+synonyms) -> _ontology-facts.pl

    GR->>EI: parse(code_contracts_yaml) -> invariants{prolog,tla,alloy,z}
    EI-->>GR: invariants_by_formalism
    GR->>OF: append_only_write(normes/{norme}/formal/*, invariants_by_formalism)

    GR->>CO: verify(base_extended + new_predicates)
    CO-->>GR: coherence_result_json{verdict, issues[]}

    alt coherence verdict = FAIL
        GR->>FC: formal_result_json{scope=full, verdict=FAIL}
        FC-->>GR: FAIL
    else coherence verdict = GO
        GR->>FV: verify_contracts(contracts_yaml -> contract_predicates)
        FV-->>GR: formal_result_json{scope=contracts, verdict}
        GR->>FV: verify_code(code_manifest -> code_predicates)
        FV-->>GR: formal_result_json{scope=code, verdict}
        GR->>FV: verify_full(contract_predicates + code_predicates + ontology_facts)
        FV-->>GR: formal_result_json{scope=full, verdict}
    end

    GR->>GR: aggregate verdicts -> job_state (VERIFICATION_PASSED|FAILED_BLOCKING)

6. Cas d’erreur¶

7. Critères d’acceptation (testables)¶

8. Scénarios de test (Given / When / Then)¶

1. TC-NOM-01
   GIVEN une story PD-XXX en step 10 avec artefacts valides
   WHEN le run démarre
   THEN PENDING -> EXTRACTING et lock acquis.

2. TC-NOM-02
   GIVEN extraction et persistance réussies sur les 4 formalismes
   WHEN l’étape d’enrichissement se termine
   THEN EXTRACTING -> ENRICHED.

3. TC-ERR-03
   GIVEN un timeout d’extraction
   WHEN sla_extraction_window expire
   THEN EXTRACTING -> ENRICHMENT_DEGRADED puis blocage en vérification.

4. TC-NR-04
   GIVEN base étendue avec contradiction détectée
   WHEN le check non-régression s’exécute
   THEN ENRICHED -> FAILED_BLOCKING et clôture interdite.

5. TC-SCOPE-05
   GIVEN scope contracts exécuté
   WHEN le moteur retourne un verdict
   THEN la valeur est strictement GO ou FAIL (jamais SKIP).

6. TC-SCOPE-06
   GIVEN scopes contracts, code, full tous GO et non-régression GO
   WHEN l’agrégation est effectuée
   THEN ENRICHED -> VERIFICATION_PASSED -> DONE.

7. TC-IDEMP-07
   GIVEN une relance avec même idempotency_key et même payload
   WHEN le run est rejoué
   THEN résultat identique et aucune duplication de prédicats.

8. TC-CONC-08
   GIVEN deux runs simultanés sur même story_id/story_version
   WHEN le second tente l’acquisition lock
   THEN rejet CONCURRENT_RUN.

9. TC-RET-09
   GIVEN état FAILED_BLOCKING après correction
   WHEN une relance explicite est déclenchée
   THEN FAILED_BLOCKING -> PENDING puis reprise nominale.

10. TC-TERM-10
    GIVEN état DONE
    WHEN une transition sortante est demandée
    THEN rejet explicite (état terminal).

11. TC-FC-11
    GIVEN formal-verify indisponible
    WHEN un scope est invoqué
    THEN verdict FAIL (TOOL_UNAVAILABLE), jamais GO.

12. TC-DATA-12
    GIVEN un predicate_atom hors regex D-297-11
    WHEN persistance est demandée
    THEN rejet + FAILED_BLOCKING.

9. Hypothèses explicites¶

10. Points à clarifier¶

10.1 Contraintes techniques (stack projet cible)¶

Contrainte explicite: aucune substitution de stack n’est autorisée (pas Swift/SwiftUI, pas Spring Boot).

10.2 Questions ouvertes¶

Références¶

• Epic : Référence épique non fournie.
• JIRA : PD-297.
• Repos concernés : ProbatioVault-ia-governance, ProbatioVault-formal.
• Documents associés :
• PD-297-besoin.md
• PD-297-clarifications.md
• formal-check.sh
• procedures.md
• workflow-rules.md
• ProbatioVault-formal/CLAUDE.md