PD-280 — PV Proof : implementer etat PENDING (verification en cours)¶

1. Contexte¶

Le modele TLA+ PV_Proof.tla definit 4 resultats de verification pour les maillons de la chaine de preuve :

CheckResults == {"OK", "KO", "INDETERMINATE", "PENDING"}

Le code TypeScript actuel n'implemente que 3 valeurs dans l'enum CheckResult : OK, KO, INDETERMINATE. L'etat PENDING est absent.

Le fichier d'ancrage formel _AnchoredFacts_PROOF.tla definit :

RealStates == {"OK", "KO", "INDETERMINATE"}

L'ASSUME CheckResults ⊆ RealStates echoue car PENDING ∉ RealStates. L'ecart a ete detecte par l'audit de verification formelle du 2026-03-01.

2. Probleme¶

L'absence de l'etat PENDING empeche de distinguer deux situations fondamentalement differentes :

• PENDING : la verification est en cours, le resultat est attendu sous delai borne (transitoire). Exemple : batch blockchain en PENDING_FINALITY, transaction pas assez confirmee, job d'export non termine.
• INDETERMINATE : la verification ne peut pas conclure, potentiellement durable ou hors SLA. Exemple : blockchain inaccessible, preuve Merkle inverifiable, TSA non verifiable (chaine de certificats inconnue).

Aujourd'hui, les deux cas sont confondus sous INDETERMINATE, ce qui : - Viole le modele formel (ASSUME echoue) - Empeche le client de savoir s'il doit attendre (polling) ou accepter une situation degradee - Interdit la mise en oeuvre d'un pattern de verification asynchrone

3. Besoin fonctionnel¶

3.1 Modelisation a deux niveaux¶

Niveau processus (job de verification) : - Nouveau champ verificationStatus : PENDING | DONE - PENDING = au moins un maillon n'a pas encore ete evalue - DONE = tous les maillons ont un resultat definitif (OK, KO ou INDETERMINATE)

Niveau maillon (CheckResult) : - Ajouter PENDING a l'enum CheckResult : OK | KO | INDETERMINATE | PENDING - Un maillon est PENDING tant que sa verification n'a pas abouti - Un maillon PENDING DOIT se resoudre en OK, KO ou INDETERMINATE sous delai borne (SLA)

3.2 Contrat API (verification)¶

L'endpoint de verification expose le statut global du job ET les resultats par maillon :

En cours de verification :

{
  "proofId": "...",
  "verificationStatus": "PENDING",
  "pendingReason": "ANCHOR_BATCH_NOT_FINALIZED",
  "nextCheckAfterSeconds": 60,
  "linkResults": {
    "DOCUMENT_HASH": "OK",
    "MERKLE_PROOF": "OK",
    "TSA_TIMESTAMP": "OK",
    "BLOCKCHAIN_ANCHOR": null
  }
}

Verification terminee :

{
  "proofId": "...",
  "verificationStatus": "DONE",
  "linkResults": {
    "DOCUMENT_HASH": "OK",
    "MERKLE_PROOF": "OK",
    "TSA_TIMESTAMP": "OK",
    "BLOCKCHAIN_ANCHOR": "OK"
  }
}

Regles : - Un linkResult a null signifie que le maillon est en cours de verification (PENDING) - verificationStatus = "PENDING" si au moins un linkResult est null - verificationStatus = "DONE" si tous les linkResults sont non-null - pendingReason et nextCheckAfterSeconds sont presents uniquement quand verificationStatus = "PENDING"

3.3 Semantique PENDING vs INDETERMINATE (clarification RFC)¶

Reclassification des cas : - PENDING_FINALITY (batch blockchain) : PENDING (etait incorrectement INDETERMINATE) - BLOCKCHAIN_UNREACHABLE : INDETERMINATE (correct) - Preuve Merkle inverifiable (donnees manquantes) : INDETERMINATE (correct) - TSA non verifiable (chaine cert inconnue) : INDETERMINATE (correct) - Transaction pas assez confirmee : PENDING (etait incorrectement INDETERMINATE)

3.4 Alignement TLA+¶

• CheckResult enum passe a 4 valeurs : aligne avec CheckResults du modele TLA+
• _AnchoredFacts_PROOF.tla : RealStates passe a 4 valeurs → ASSUME satisfait
• norm.yaml : ajouter mapping PENDING: PENDING
• INV-04 (ChainLinkExplicit) : invariant preservee — PENDING interdit apres finalisation (proof_finalized = TRUE → tous les maillons ∈ {OK, KO, INDETERMINATE})

4. Criteres d'acceptation¶

• CA-01 : L'enum CheckResult contient 4 valeurs : OK, KO, INDETERMINATE, PENDING
• CA-02 : L'endpoint de verification retourne verificationStatus (PENDING | DONE) et linkResults avec null pour les maillons en cours
• CA-03 : Un batch blockchain en PENDING_FINALITY produit un maillon PENDING (et non INDETERMINATE)
• CA-04 : verificationStatus = DONE ssi tous les linkResults sont non-null
• CA-05 : pendingReason et nextCheckAfterSeconds sont presents uniquement quand verificationStatus = PENDING
• CA-06 : L'ASSUME TLA+ RealStates ⊆ CheckResults ∧ CheckResults ⊆ RealStates est satisfait
• CA-07 : INV-04 (ChainLinkExplicit) reste valide : aucun maillon PENDING apres finalisation d'une preuve
• CA-08 : Les tests existants de verification continuent a passer (non-regression)
• CA-09 : La RFC PV-PROOF est mise a jour pour clarifier la semantique PENDING vs INDETERMINATE

5. Hors perimetre¶

• Mise en oeuvre du pattern async complet (queue BullMQ pour verification asynchrone) → story separee
• Modification de l'endpoint de creation de preuve
• Modification de la logique de finalisation des preuves

6. Contraintes techniques¶

• L'enum CheckResult est utilise dans le module integrity (service, interfaces, tests)
• Le changement de l'enum impacte potentiellement les DTOs, les entites TypeORM et les migrations
• La valeur PENDING en base de donnees doit etre compatible avec les colonnes existantes (type varchar/enum)

7. Risques¶

• R-01 : Migrations DB si les colonnes utilisent un type enum PostgreSQL au lieu de varchar → necessite ALTER TYPE ADD VALUE
• R-02 : Impact sur les consumers existants de l'API qui ne connaissent pas PENDING → backward compatibility
• R-03 : Coherence avec la double verification PD-251 qui utilise CheckResult → verifier que PENDING ne perturbe pas la logique de gel

8. Learnings injectes¶

• PD-40 (crypto) : Append-only simplifie la gestion d'erreurs ; canonicalisation RFC 8785 systematique
• PD-86 (verification stubs) : Plan doit documenter la strategie de verification pour les dependances stubees