PD-278 — Agent Developer : Module dip-tla-formal¶

Agent : agent-developer (Agent B) Module : dip-tla-formal Story : PD-278 — NF Z42-013 : ajout contractuel de l'etat DIP Date : 2026-03-01

1. Perimetre¶

2. Analyse du modele existant¶

2.1 Etat du modele TLA+ (NF_Z42_013.tla)¶

Le modele TLA+ contient deja l'etat DIP dans DocStates :

DocStates == {"SIP", "AIP", "DIP", "ELIMINATED"}  \* ligne 54

Les transitions DIP sont deja modelisees :

Les invariants TLA+ couvrent deja DIP :

Conclusion : Le fichier NF_Z42_013.tla est complet pour PD-278. Aucune modification necessaire.

2.2 Etat du fichier _AnchoredFacts_NF.tla (genere par CI)¶

Le fichier genere contient :

RealStates == {"SIP", "AIP", "ELIMINATED"}   \* 3 valeurs — DIP ABSENT

Et l'ASSUME de double inclusion :

ASSUME AnchorAssume_States ==
    /\ RealStates \subseteq DocStates     \* OK : {"SIP","AIP","ELIMINATED"} dans {"SIP","AIP","DIP","ELIMINATED"}
    /\ DocStates \subseteq RealStates     \* FAIL : "DIP" absent de RealStates

Cause racine : norm.yaml ne contenait pas le mapping DIP: DIP dans state_mapping. Le script extract-facts.py genere RealStates a partir de ce mapping.

2.3 Chaine de causalite¶

norm.yaml (state_mapping: 3 entrees)
  --> extract-facts.py (write_tla_constants)
    --> _AnchoredFacts_NF.tla (RealStates = 3 valeurs)
      --> ASSUME DocStates \subseteq RealStates = VIOLATION (DIP absent)

3. Modification effectuee¶

3.1 Fichier modifie : norm.yaml¶

Chemin : ProbatioVault-doc/docs/normes/nf-z42-013/formal/norm.yaml

Diff :

  state_mapping:
    PENDING: SIP
    SEALED: AIP
+   DIP: DIP
    EXPIRED: ELIMINATED

Justification : L'etat DIP porte le meme nom dans le modele TLA+ et dans le code backend (DocumentStatus.DIP). Le mapping est identite (DIP -> DIP), a la difference des autres etats qui ont une traduction OAIS (PENDING->SIP, SEALED->AIP, EXPIRED->ELIMINATED).

3.2 Fichier NON modifie : NF_Z42_013.tla¶

Le modele TLA+ contenait deja DIP dans DocStates et toutes les transitions/invariants associes. Aucune modification necessaire.

3.3 Fichier NON modifie : _AnchoredFacts_NF.tla¶

Interdit par le code contract (forbidden: Modifier _AnchoredFacts_NF.tla directement). Ce fichier sera regenere automatiquement par extract-facts.py lors du prochain build CI, avec le mapping DIP: DIP ajoute dans norm.yaml.

Resultat attendu apres regeneration CI :

RealStates == {"SIP", "AIP", "DIP", "ELIMINATED"}

NormMapping == [s \in {"PENDING", "SEALED", "DIP", "EXPIRED"} |->
    CASE s = "PENDING" -> "SIP"
    []   s = "SEALED" -> "AIP"
    []   s = "DIP" -> "DIP"
    []   s = "EXPIRED" -> "ELIMINATED"
]

ASSUME AnchorAssume_States ==
    /\ RealStates \subseteq DocStates    \* OK : 4 valeurs dans 4 valeurs
    /\ DocStates \subseteq RealStates    \* OK : 4 valeurs dans 4 valeurs (egalite)

4. Verification formelle (TC-FML-01)¶

4.1 Pre-requis pour TLC sans violation¶

Pour que TLC verifie DocStates ⊆ RealStates sans violation, deux conditions doivent etre reunies :

1. norm.yaml contient DIP: DIP dans state_mapping (fait dans cette tache)
2. L'enum TypeORM DocumentStatus contient DIP (fait par agent-entity, module dip-entity-extension)

La condition 2 est necessaire car extract-facts.py extrait les valeurs enum depuis les entities TypeORM. Sans DIP dans l'enum, le script ne generera pas "DIP" dans RealStates meme si norm.yaml contient le mapping.

4.2 Matrice de couverture TLC¶

4.3 Transitions verifiees par TLC¶

4.4 Transitions interdites (verifiees structurellement)¶

5. Correspondance spec PD-278 / modele TLA+¶

5.1 Mapping terminologique¶

Note : RESTITUTED (PD-279) n'a pas d'equivalent OAIS dans NF Z42-013. Il n'apparait pas dans DocStates du modele TLA+ et n'est pas dans norm.yaml. C'est coherent car RESTITUTED est un etat ISO 14641, pas NF Z42-013.

5.2 Invariants spec vs TLA+¶

6. Hypotheses explicites¶

7. Decision architecturale¶

architectural_decisions:
  - decision: "Mapping identite DIP: DIP dans norm.yaml (pas de traduction OAIS)"
    rationale: "DIP est le terme OAIS standard (Dissemination Information Package), identique dans le modele TLA+ et le code backend"
    alternatives_considered:
      - "Creer un terme de mapping different (ex: COMMUNICATED)"
      - "Renommer l'etat code en DISSEMINATED"
    trade_offs:
      - "Avantage: alignement direct OAIS, aucune ambiguite terminologique"
      - "Particularite: seul mapping identite dans la table (les 3 autres ont une traduction)"

8. Matrice de couverture tests¶

Note : TC-FML-01 sera executable apres que : 1. norm.yaml est mis a jour (fait) 2. L'enum TypeORM DocumentStatus contient DIP (module dip-entity-extension, agent-entity) 3. CI execute extract-facts.py pour regenerer _AnchoredFacts_NF.tla 4. TLC est lance sur la configuration NF_Z42_013.cfg

9. Fichiers modifies¶

10. Dependances inter-agents¶

11. Points de vigilance¶