PD-281 — Plan d'implémentation¶

1. Découpage en composants¶

C1 — Discriminateur enum dans extract-facts.py¶

Fichier : scripts/formal/extract-facts.py Responsabilité : Modifier la fonction _collect_zlint_entities() et la boucle de génération enum_states dans write_zlint_config() pour ne produire des checks Anchor enum que pour les colonnes status ou explicitement mappées dans _z_enum_type_mappings.

Modifications :

1. _collect_zlint_entities() (lignes 1498-1522) : Adapter la collecte pour stocker tous les enums d'une entité (pas seulement le dernier), en conservant le nom de colonne (field) pour chaque enum.
2. Boucle enum_states (lignes 1607-1612 dans write_zlint_config()) : Ajouter un filtre de discrimination : seules les entrées dont field == 'status' ou dont le couple (entity_name) est présent dans _z_enum_type_mappings pour le slug courant sont incluses dans anchored_enums.

Mécanisme de discrimination (v2 — correction AMB-02, couple entité+colonne) :

# Pseudo-code du filtre — itère sur le couple (entity_name, field)
for ent_name, enum_list in enum_states.items():
    # enum_list = [{field, values}, ...] (multi-enum par entité)
    for enum_data in enum_list:
        field = enum_data['field']
        values = enum_data['values']
        # DISCRIMINATION sur le couple (ent_name, field)
        if field == 'status':
            # Colonne status → inclusion automatique
            z_type = enum_type_map.get(ent_name, f'{ent_name}_state')
            anchored_enums[ent_name] = {'values': values, 'expected_z_type': z_type}
        elif ent_name in enum_type_map:
            # Mapping explicite dans _z_enum_type_mappings → inclusion
            z_type = enum_type_map[ent_name]
            anchored_enums[ent_name] = {'values': values, 'expected_z_type': z_type}
        # Sinon → exclusion (pas de check Anchor enum pour ce couple)

Observable : Les _generated-z-lint.yaml régénérés ne contiennent plus anchor_batch_event, key_envelope, legal_access_event, legal_mandate, deposit (pour leurs colonnes non-status) dans anchored.enum_states.

C2 — Complétion des types Z dans les fichiers .zed¶

Fichiers :

• docs/normes/rfc-3161/formal/RFC_3161.zed
• docs/normes/nf-z42-013/formal/NF_Z42_013.zed
• docs/normes/iso-14641/formal/ISO_14641.zed
• docs/normes/pv-pre/formal/PV_PRE.zed

Responsabilité : Ajouter les déclarations de types Z manquants dans la SECTION 1 (Basic Types) de chaque fichier .zed cible, avec les valeurs exactes spécifiées.

Types à ajouter :

Observable : Chaque type Z est présent dans le fichier .zed cible avec exactement les valeurs listées, en notation Z standard (TypeName ::= VAL1 | VAL2 | ...).

C3 — Régénération et validation globale¶

Fichiers :

• scripts/formal/extract-facts.py (exécution)
• Tous les _generated-z-lint.yaml (9 normes)
• docs/normes/AUDIT-SYNTHESIS.md

Responsabilité : Exécuter la chaîne complète extract-facts.py → verify-norm.sh sur les 9 normes, valider le résultat SUCCESS global, mettre à jour AUDIT-SYNTHESIS.md.

Observable : verify-norm.sh retourne SUCCESS sur 9/9 normes, AUDIT-SYNTHESIS.md affiche Z-lint 9/9 PASS.

C4 — Règle conditionnelle DepositStatus¶

Fichiers : NF_Z42_013.zed, ISO_14641.zed (conditionnellement)

Responsabilité : Vérifier dans les faits extraits si deposit.status existe comme colonne lifecycle. Si oui, ajouter DepositStatus dans les .zed concernés. Si non, ne rien ajouter.

Mécanisme : Rechercher entity_enum_values(deposit, status, [...]) dans les faits Prolog générés. Présence = colonne lifecycle confirmée. Absence = pas d'exigence DepositStatus.

Observable : Présence/absence de DepositStatus dans les .zed conforme à l'existence de deposit.status dans les faits extraits.

2. Flux techniques¶

Flux A — Discrimination (C1)¶

1. extract-facts.py extrait entity_enum_values depuis les entités TypeORM
2. _collect_zlint_entities() collecte TOUS les enums (entity, field, values)
3. write_zlint_config() itère sur enum_states :
   3a. Si field == 'status' → inclusion (Anchor enum check généré)
   3b. Si entity dans _z_enum_type_mappings pour ce slug → inclusion (mapping explicite)
   3c. Sinon → exclusion (pas de check Anchor enum)
4. anchored.enum_states dans _generated-z-lint.yaml ne contient que les state machines

Flux B — Complétion (C2)¶

1. Identifier les types Z manquants (tableau §5.3 de la spec)
2. Pour chaque type Z manquant :
   2a. Ouvrir le fichier .zed cible
   2b. Localiser SECTION 1 (Basic Types)
   2c. Ajouter la déclaration TypeName ::= VAL1 | VAL2 | ...
   2d. Vérifier cohérence avec les valeurs enum du code (faits Prolog)
3. Sauvegarder sans modifier les autres sections

Flux C — Régénération et validation (C3)¶

1. Exécuter extract-facts.py pour régénérer :
   - _generated-facts.pl (faits Prolog)
   - _generated-z-lint.yaml (configs Z-lint) pour chaque norme
2. Pour chaque norme (9 au total) :
   2a. Exécuter verify-norm.sh <norm-dir> <reports-dir>
   2b. Vérifier statut de sortie = 0 (SUCCESS)
3. Vérifier AUDIT-SYNTHESIS.md : Z-lint = 9/9 PASS
4. Vérifier idempotence : relancer le flux → même résultat

Flux D — Condition DepositStatus (C4)¶

1. Exécuter extract-facts.py
2. Rechercher entity_enum_values(deposit, status, [...]) dans les faits
3. Si trouvé :
   3a. Extraire les valeurs enum
   3b. Ajouter DepositStatus dans NF_Z42_013.zed et ISO_14641.zed
   3c. Mettre à jour _z_enum_type_mappings si nécessaire
4. Si non trouvé :
   4a. Ne rien ajouter
   4b. Vérifier qu'aucun check DepositStatus n'est exigé

3. Mapping invariants → mécanismes¶

4. Mapping critères d'acceptation → mécanismes¶

5. Mapping tests (TC-*) → mécanismes + observables¶

6. Gestion des erreurs¶

7. Impacts sécurité¶

Aucun impact sécurité identifié.

• PD-281 modifie uniquement des scripts d'analyse statique et des spécifications formelles (*.zed)
• Aucune donnée utilisateur traitée
• Aucune modification de code backend (entités, services, controllers)
• Aucun secret, token ou credential manipulé
• Les scripts modifiés (extract-facts.py) ne sont exécutés qu'en CI/CD (pipeline de vérification formelle), pas en production

8. Hypothèses techniques¶

9. Points de vigilance (risques, dette, pièges)¶

9.1 Multi-enum par entité¶

Risque : _collect_zlint_entities() stocke actuellement enum_states[entity_name] = {field, values}, écrasant les enums précédents de la même entité. Si une entité a à la fois status et event_type, seul le dernier extrait sera conservé.

Mitigation : Adapter la structure pour stocker une liste d'enums par entité : enum_states[entity_name] = [{field, values}, ...]. Le filtre itère ensuite sur chaque enum et n'inclut que ceux avec field == 'status' ou mapping explicite.

9.2 TimestampBatchStatus dans RFC_3161.zed¶

Contexte : RFC_3161.zed contient déjà BatchState ::= OPEN | SEALED | TIMESTAMPED | FAILED avec les mêmes valeurs que TimestampBatchStatus.

Décision (v2 — correction Gate 5) : Créer TimestampBatchStatus explicitement dans RFC_3161.zed (SECTION 1), conformément à la Spec §5.3 et au test TC-NOM-05. Le mapping _z_enum_type_mappings pour rfc-3161 doit référencer 'timestamp_batch': 'TimestampBatchStatus' (et non BatchState).

Justification : La Spec est le contrat canonique. BatchState peut coexister comme type interne non lié à l'ancrage Z-lint. L'ajout de TimestampBatchStatus est déclaratif et non-breaking.

9.3 Risque de régression sur les entity checks¶

Risque : La modification de _collect_zlint_entities() pourrait altérer le dict entities utilisé pour anchored_entities (les checks Anchor entity).

Mitigation : Le dict entities et le dict enum_states sont des structures séparées dans le retour de la fonction. La modification porte uniquement sur enum_states. Vérifier par diff que anchored.entities reste identique avant/après.

9.4 Ordre des faits Prolog et idempotence¶

Risque : Si l'ordre d'extraction des faits change entre runs (parcours de fichiers non déterministe), le multi-enum par entité pourrait produire des résultats différents.

Mitigation : extract-facts.py utilise déjà sorted() pour les clés. S'assurer que les valeurs enum sont également triées avant écriture.

9.5 Source de vérité deposit.status¶

Risque : La spec indique que l'existence de deposit.status est "à confirmer" (H-281-05). Si non confirmé au moment de l'implémentation, CA-08 reste en suspens.

Mitigation : Implémenter la logique conditionnelle dans le code. Le test TC-NOM-06/TC-NOM-07 couvrira les deux branches selon la source de vérité disponible.

9.6 Cohérence _z_enum_type_mappings entre normes¶

Attention : Une même entité peut avoir des mappings différents selon la norme. Par exemple anchor_batch est mappé BatchStatus dans pv-anchor mais pourrait nécessiter AnchorBatchStatus dans nf-z42-013 et iso-14641.

Action : Vérifier la cohérence des noms de types Z dans chaque .zed cible et ajuster les mappings par norme.

10. Hors périmètre¶

• Modification des entités TypeORM backend : aucune colonne base de données n'est ajoutée, modifiée ou supprimée
• Ajout de nouvelles normes au pipeline de vérification formelle
• Refonte du système de vérification formelle (architecture TLA+/Alloy/Prolog/Z)
• Modification du check Anchor entity (mapping entité → schéma Z) dans z-notation-lint.py
• Spécification des transitions métier entre valeurs d'état (ex: PENDING → FINALIZED). PD-281 ne définit que l'ancrage des types, pas les workflows.
• Modification de z-notation-lint.py : le linter consomme les configs générées. La correction porte sur le générateur (extract-facts.py) et les specs (.zed), pas sur le linter.

11. Mécanismes cross-module¶

Aucune modification d'autres modules. PD-281 est entièrement contenu dans ProbatioVault-doc (scripts, specs .zed, configs générées). Aucun guard, middleware ou intercepteur n'est ajouté sur d'autres modules.

12. Périmètre de test¶

Tous les niveaux de test sont couverts, aucune exclusion.

La couverture minimale de 80% s'applique à l'ensemble du périmètre. Les tests E2E sont le niveau principal (la chaîne extract-facts.py → verify-norm.sh est l'observable final pour la majorité des CAs).