PD-281 — Expression de besoin¶
1. Titre¶
Z-lint : distinguer state vs type/category dans Anchor enum + compléter types Z manquants
2. Contexte¶
2.1 Situation actuelle¶
Le pipeline de vérification formelle (verify-norm.sh) exécute un Z-lint structurel sur 9 normes ProbatioVault. Le script extract-facts.py extrait les faits Prolog depuis le code source (entités TypeORM, migrations SQL, Terraform) et génère des configurations Z-lint (_generated-z-lint.yaml) pour chaque norme.
Le check "Anchor enum" du Z-lint vérifie que chaque entité ayant un entity_enum_values dans les faits extraits possède un type Z correspondant (<entity>_state) dans la spécification .zed.
2.2 Problème¶
Le générateur traite tous les enums de la même manière, sans distinguer :
- Les state machines (champ
status) : lifecycle réel avec transitions (PENDING → FINALIZED → FAILED). Ces colonnes DOIVENT avoir un type Z ancré. - Les types/catégories (champs
event_type,envelope_type,document_category,validation_status) : classifications statiques, pas de lifecycle. Ces colonnes n'ont PAS besoin d'un type Z<entity>_state.
Résultat : 10 échecs Z-lint sur 5 normes, dont la majorité sont des faux positifs.
2.3 Impact¶
- Le score Z-lint dans
AUDIT-SYNTHESIS.mdest dégradé (FAIL sur plusieurs normes) - Les vrais gaps (types Z manquants pour les state machines) sont noyés dans les faux positifs
- La confiance dans le pipeline de vérification formelle est réduite
3. Besoin¶
3.1 Volet 1 — Corriger le générateur Z-lint (extract-facts.py)¶
En tant que responsable qualité, je veux que le générateur Z-lint distingue les colonnes "status" (state machines) des colonnes "type/category" (classifications), afin que seules les vraies state machines génèrent un check "Anchor enum" et que les faux positifs soient éliminés.
Règle de discrimination¶
- Colonnes state machine (génèrent un check Anchor enum) : colonnes nommées
statusou explicitement mappées dans_z_enum_type_mappings - Colonnes type/category (exclues du check) :
event_type,envelope_type,document_category,validation_status, et toute colonne non-status
Entités à exclure du check (faux positifs actuels)¶
| Entité | Colonne | Raison de l'exclusion |
|---|---|---|
anchor_batch_event | event_type | Type d'événement, pas un lifecycle |
key_envelope | envelope_type | Classification (master/device/recovery) |
legal_access_event | event_type | Type d'événement, pas un lifecycle |
legal_mandate | validation_status | Binaire (VALID/INVALID), pas un lifecycle |
deposit | document_category | Classification documentaire |
3.2 Volet 2 — Compléter les types Z manquants dans les specs .zed¶
En tant que responsable conformité, je veux que les vrais state machines aient leur type Z défini dans chaque fichier .zed concerné, afin que le pipeline de vérification formelle valide complètement les machines à états du système.
Types Z à ajouter¶
| Type Z | Fichier .zed | Valeurs | Source |
|---|---|---|---|
TimestampBatchStatus | RFC_3161.zed | OPEN, SEALED, TIMESTAMPED, FAILED | Colonne status de timestamp_batch |
AnchorBatchStatus | NF_Z42_013.zed | PENDING, BUILDING, SUBMITTED, PENDING_FINALITY, FINALIZED, FAILED | Colonne status de anchor_batch |
AnchorBatchStatus | ISO_14641.zed | PENDING, BUILDING, SUBMITTED, PENDING_FINALITY, FINALIZED, FAILED | Colonne status de anchor_batch |
LegalReKeyStatus | PV_PRE.zed | ACTIVE, REVOKED, EXPIRED, COMPLETED, DESTROYED | Colonne status de legal_re_key |
Note : Vérifier si deposit a un champ status (lifecycle) en plus de document_category (classification). Si oui, ajouter DepositStatus dans NF_Z42_013.zed et ISO_14641.zed.
3.3 Volet 3 — Régénérer et valider¶
En tant que ingénieur, je veux que les configurations Z-lint soient régénérées après correction et que verify-norm.sh passe SUCCESS sur les 9 normes, afin de confirmer que tous les faux positifs sont éliminés et tous les vrais gaps comblés.
4. Critères d'acceptation¶
- CA-01 :
verify-norm.shpasse SUCCESS sur les 9 normes (0 échec Z-lint) - CA-02 : Les vrais state machines ont leur type Z dans chaque
.zedconcerné - CA-03 : Le générateur Z-lint (
extract-facts.py) ne produit plus de checks "Anchor enum" pour les colonnes non-status - CA-04 :
AUDIT-SYNTHESIS.mdaffiche Z-lint 9/9 PASS - CA-05 : Les
_generated-z-lint.yamlrégénérés ne contiennent plus les entités exclues dans la sectionanchored.enum_states - CA-06 : Aucune régression sur les checks existants (entités, colonnes requises, enums state machine)
5. Contraintes¶
- Rétrocompatibilité : Les checks "Anchor entity" (entités → schémas Z) ne doivent pas être impactés
- Idempotence : Relancer
extract-facts.py+verify-norm.shdoit donner le même résultat - Aucun impact code backend : Seuls les fichiers du projet
ProbatioVault-docsont modifiés (scripts, specs Z, configs)
6. Normes impactées¶
| Norme | Faux positifs actuels | Vrais gaps |
|---|---|---|
pv-anchor | 1 (anchor_batch_event.event_type) | 0 |
nf-z42-013 | 2 (deposit.document_category + event_type) | 1 (anchor_batch_state) |
iso-14641 | 2 (deposit.document_category + event_type) | 1 (anchor_batch_state) |
rfc-3161 | 1 (event_type) | 1 (timestamp_batch_state) |
pv-envelope | 1 (key_envelope.envelope_type) | 0 |
pv-pre | 3 (event_type, validation_status, document_category) | 1 (legal_re_key_state) |
7. Learnings injectés (capitalisation)¶
- PD-250 : Machine à états formelle — transitions autorisées ET interdites. Pertinent pour la distinction state machine vs classification.
- PD-37 : Vérification indépendante = vraie indépendance. Le Z-lint doit vérifier indépendamment du code, via les specs formelles.
- PD-35 : Scaffolding DEV-ONLY code génère des gaps MAJEUR. Importance de la rigueur dans le mapping enum → type Z.
8. Hors périmètre¶
- Modification des entités TypeORM dans le backend
- Ajout de nouvelles normes au pipeline de vérification formelle
- Refonte complète du système de vérification formelle
- Modification du check "Anchor entity" (entités → schémas Z)