PD-273 — Mise en conformité formelle des checks PV-AUDIT-001 (3 PARTIEL → OK)¶

1. Objectif¶

Contractualiser les exigences fonctionnelles de conformité pour que l'exécution de l'audit formel PV-AUDIT-001 produise un résultat conforme sur les 3 checks actuellement en statut PARTIEL, sans régression sur les checks déjà conformes.

Paramètres numériques contractualisés (obligatoires) :

• Percentile/performance device: non applicable (pas de SLA de performance dans ce besoin).

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

Inclus¶

• Alignement contractuel entre faits de conformité audités et règles d'acceptation formelle pour :
• immutabilité du journal d'audit (update/delete interdits),
• capacité de signature des entrées d'audit,
• traçabilité de la séquence de destruction dans le domaine audit/destruction.
• Validation de non-régression sur les checks non ciblés de PV-AUDIT-001.
• Formalisation des états de conformité (PARTIEL, OK) et de leurs transitions.

Exclu¶

• Toute évolution métier hors périmètre des 3 checks en écart.
• Toute exigence de performance (latence, throughput), hors périmètre.
• Toute modification de protocole cryptographique, hors périmètre.
• Toute refonte de l'architecture d'audit globale, hors périmètre.

3. Définitions¶

• PV-AUDIT-001 : audit formel de conformité probatoire.
• Check : règle unitaire de conformité évaluée par le moteur formel.
• Statut PARTIEL : conformité incomplète (au moins une condition d'acceptation non satisfaite).
• Statut OK : conformité complète pour le check.
• Régression : passage d'un check précédemment OK à PARTIEL/KO.
• Faits de conformité : représentations normalisées observées par le moteur de vérification.
• Séquence de destruction : numérotation monotone dédiée au domaine destruction/audit.

4. Invariants (non négociables)¶

5. Flux nominaux¶

Flux F1 — Rétablissement conformité immutabilité audit log¶

1. Le check ciblé est en entrée au statut PARTIEL.
2. Les éléments audités sont évalués par le moteur formel.
3. Le moteur constate la reconnaissance explicite de la règle d'immutabilité.
4. Le check sort en statut OK.

Résultat attendu : check_audit_trigger_update_delete = OK.

Flux F2 — Rétablissement conformité capacité de signature audit¶

1. Le check ciblé est en entrée au statut PARTIEL.
2. Le moteur formel évalue la capacité de signature attendue.
3. La capacité est reconnue selon la sémantique contractuelle du check.
4. Le check sort en statut OK.

Résultat attendu : check_audit_signature_sign = OK.

Flux F3 — Rétablissement conformité séquence destruction¶

1. Le check ciblé est en entrée au statut PARTIEL.
2. Le moteur formel évalue l'existence/traçabilité contractuelle de la séquence destruction.
3. La traçabilité est reconnue selon les critères du check.
4. Le check sort en statut OK.

Résultat attendu : check_destruction_sequence = OK.

Flux F4 — Vérification globale de non-régression¶

1. L'audit complet PV-AUDIT-001 est exécuté.
2. Les 3 checks ciblés sont vérifiés en OK.
3. Les 21 checks non ciblés sont vérifiés sans régression.
4. Le lot de conformité est accepté.

5bis. Diagrammes¶

Diagramme d'états — Conformité d'un check (INV-273-06)¶

Modèle d'états d'un check unitaire de conformité, tel que défini par INV-273-06 (transitions) et détaillé en §10.3.

stateDiagram-v2
    [*] --> PARTIEL : Évaluation initiale (check en écart)
    [*] --> OK : Évaluation initiale (check conforme)

    PARTIEL --> OK : Alignement contractuel vérifié (F1/F2/F3)
    PARTIEL --> PARTIEL : Écart persistant après réévaluation
    OK --> OK : Stabilité confirmée (F4)
    OK --> PARTIEL : Régression détectée (ERR-273-02)

    note right of PARTIEL
        Conformité incomplète.
        Au moins une condition
        d'acceptation non satisfaite.
    end note

    note right of OK
        Conformité complète.
        Toutes conditions satisfaites.
    end note

Diagramme de séquence — Exécution audit PV-AUDIT-001 (F4)¶

Flux nominal de vérification globale incluant les 3 checks ciblés (INV-273-03, INV-273-04, INV-273-05) et le contrôle de non-régression (INV-273-02).

sequenceDiagram
    participant O as Orchestrateur
    participant M as Moteur formel (Prolog)
    participant F as Extracteur de faits
    participant DB as PostgreSQL

    O->>F: extract-facts.py (backend AST + normes)
    F->>DB: Lecture schéma audit (triggers, séquences)
    DB-->>F: Faits bruts (immutabilité, signature, séquence)
    F-->>M: Faits normalisés (.pl)

    rect rgb(230, 245, 255)
        Note over M: Évaluation des 3 checks ciblés
        M->>M: check_audit_trigger_update_delete (INV-273-03)
        M->>M: check_audit_signature_sign (INV-273-04)
        M->>M: check_destruction_sequence (INV-273-05)
    end

    rect rgb(245, 255, 230)
        Note over M: Vérification non-régression
        M->>M: Évaluation 21 checks non ciblés (INV-273-02)
    end

    M-->>O: Rapport PV-AUDIT-001 (24 checks, statuts OK/PARTIEL)

    alt 3 ciblés OK ET 0 régression (INV-273-01, INV-273-02)
        O->>O: Lot accepté (CA-273-01..05)
    else Check ciblé non OK
        O->>O: Lot rejeté (ERR-273-01)
    else Régression détectée
        O->>O: Lot rejeté (ERR-273-02)
    end

6. Cas d'erreur¶

• ERR-273-01-CHECK-NOT-OK : au moins un des 3 checks ciblés reste PARTIEL/KO. Réponse attendue : lot rejeté, liste nominative des checks en écart.
• ERR-273-02-REGRESSION-DETECTED : un ou plusieurs checks non ciblés régressent. Réponse attendue : lot rejeté, preuve de régression par diff des statuts.
• ERR-273-03-UNVERIFIABLE-RULE : exigence formulée sans observable testable. Réponse attendue : exigence classée hors périmètre et exclue du verdict.
• ERR-273-04-AUDIT-RUN-INCOMPLETE : exécution partielle de l'audit (résultat incomplet). Réponse attendue : verdict invalide, relance obligatoire en exécution complète.

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

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

• TC-273-01 — Immutabilité reconnue
• Given un audit PV-AUDIT-001 avec baseline où check_audit_trigger_update_delete est PARTIEL
• When l'audit complet est exécuté après alignement contractuel

• Then check_audit_trigger_update_delete est OK

• TC-273-02 — Signature reconnue

• Given un audit avec baseline où check_audit_signature_sign est PARTIEL
• When l'audit complet est exécuté

• Then check_audit_signature_sign est OK

• TC-273-03 — Séquence destruction reconnue

• Given un audit avec baseline où check_destruction_sequence est PARTIEL
• When l'audit complet est exécuté

• Then check_destruction_sequence est OK

• TC-273-04 — Non-régression globale

• Given une baseline de 21 checks non ciblés conformes
• When l'audit complet est exécuté

• Then 0 check non ciblé ne régresse

• TC-273-05 — Transition retour documentée

• Given un check en état OK
• When une exécution ultérieure détecte une divergence de conformité

• Then le statut peut redevenir PARTIEL et la régression est explicitement reportée

• TC-273-06 — Exécution incomplète

• Given une exécution audit interrompue/incomplète
• When un verdict est demandé
• Then le verdict est invalide (ERR-273-04-AUDIT-RUN-INCOMPLETE)

9. Hypothèses explicites¶

10. Points à clarifier¶

10.1 Contraintes techniques du projet cible (obligatoire)¶

• Projet cible identifié : ProbatioVault-backend.
• Stack contractuelle à respecter : NestJS + TypeORM + PostgreSQL.
• Repos concernés : backend (principal), ProbatioVault-ia-governance (règles d'audit formel Prolog + script extract-facts.py).

10.2 SLA temporels¶

• Aucune transition temporelle identifiée.

10.3 Transitions retour (exigence explicite)¶

• État PARTIEL : transitions sortantes
• PARTIEL -> OK : AUTORISÉE (après alignement de conformité vérifié).
• PARTIEL -> PARTIEL : AUTORISÉE (si écart persistant).
• État OK : transitions sortantes
• OK -> OK : AUTORISÉE (stabilité).
• OK -> PARTIEL : AUTORISÉE (régression détectée).
• État terminal : aucun état terminal défini dans ce modèle.
• Données en cas de downgrade OK -> PARTIEL : conservation intégrale des preuves et rapports historiques ; seul le statut courant se dégrade.

10.4 Stratégie migration DDL¶

• Aucune modification de colonne existante identifiée (type/nullabilité/contrainte/index) dans ce besoin.
• Donc cluster migration DDL : non applicable.

10.5 Atomicité multi-composant (DB + queue/append-only)¶

• Aucun nouveau flux multi-composant à contractualiser dans PD-273.
• Les garanties ACID/async existantes hors besoin restent inchangées (hors périmètre de cette US).

10.6 Contraintes inter-modules¶

• Aucune contrainte inter-module applicable (aucun guard cross-module de routes d'un autre module n'est demandé).

Références¶

• Epic : Conformité formelle PV-AUDIT-001
• JIRA : PD-273
• Repos concernés : ProbatioVault-backend, ProbatioVault-ia-governance
• Documents associés : PV-AUDIT-001, audit formel PV-AUDIT-001 baseline, PD-273-besoin.md