PD-274 — Conformite formelle PV-ANCHOR-001 (correction des 2 checks Prolog KO)¶

1. Objectif¶

Contractualiser les exigences necessaires et suffisantes pour faire passer a OK les 2 checks Prolog KO de l'audit PV-ANCHOR-001, sans regression fonctionnelle ni de conformite sur le reste du perimetre.

Objectifs mesurables : - Passer de 22/24 a 24/24 checks OK pour PV-ANCHOR-001. - Corriger le gap de detection des enums de statut pour anchor_batch.status. - Rendre observable la capacite du service d'ancrage a traiter un reorg via une methode de service attendue par les regles formelles. - Conserver a OK les 22 checks deja conformes.

2. Perimetre / Hors perimetre¶

Inclus¶

• Specification du comportement attendu de l'extraction de faits pour detecter les valeurs d'enum de anchor_batch.status quand la colonne est stockee en varchar et que la propriete TypeScript est typee par enum.
• Specification du contrat fonctionnel de presence d'une methode de service de gestion de reorg dans le module anchor_batch.
• Verification de conformite Prolog PV-ANCHOR-001 sur l'ensemble des checks.
• Non-regression des tests backend existants.
• Definition explicite du modele d'etats AnchorBatchStatus, y compris transitions retour/interdites.

Exclu¶

• Changement de schema SQL/DDL de anchor_batch.status.
• Refonte du moteur Prolog, du domaine metier blockchain, ou des regles hors PV-ANCHOR-001.
• Optimisations de performance non liees au besoin.
• Evolution API publique non necessaire au passage des checks.
• Toute implementation detaillee (choix de classes, algorithmes internes, snippets de code).

3. Definitions¶

• PV-ANCHOR-001 : Audit formel de conformite du module d'ancrage.
• Check Prolog : Regle de verification formelle evaluee a partir de faits extraits du code.
• entity_enum_values(Entity, Field, Values) : Fait Prolog listant les valeurs d'enum contractuelles d'un champ d'entite.
• service_method(Module, Method) : Fait Prolog attestant qu'une methode existe dans un service du module.
• Reorg : Reorganisation de chaine blockchain invalident une confirmation precedente.
• AnchorBatchStatus : Enum de statut de batch d'ancrage (6 valeurs attendues).
• Etat terminal : Etat sans transition sortante autorisee.
• Stack cible : ProbatioVault-backend = NestJS + TypeORM + PostgreSQL.

4. Invariants (non negociables)¶

5. Flux nominaux¶

FN-01 — Extraction de faits enum pour anchor_batch.status¶

1. Le systeme analyse l'entite anchor_batch.
2. Il identifie le champ status et son type metier enum (AnchorBatchStatus).
3. Il produit le fait entity_enum_values(anchor_batch, status, Values).
4. Values contient exactement les 6 valeurs contractuelles.
5. Le check Prolog check_batch_status_enum est evalue a OK.

FN-02 — Exposition de la capacite service de gestion reorg¶

1. Le module anchor_batch expose une methode de service nommee handleReorg (ou alias accepte par regle formelle).
2. L'extraction de faits produit service_method(anchor_batch, handleReorg) (ou service_method(anchor_batch, reorg) selon contrat de regle).
3. Le check Prolog check_handle_reorg est evalue a OK.

FN-03 — Evaluation globale de conformite PV-ANCHOR-001¶

1. Les faits extraits sont soumis a l'ensemble des checks PV-ANCHOR-001.
2. Les 24 checks sont evalues.
3. Score final attendu: 24/24 OK.

Modele d'etats AnchorBatchStatus et transitions¶

• PENDING → BUILDING : AUTORISEE | → FAILED : AUTORISEE | → * : INTERDITE
• BUILDING → SUBMITTED : AUTORISEE | → FAILED : AUTORISEE | → * : INTERDITE
• SUBMITTED → PENDING_FINALITY : AUTORISEE | → FAILED : AUTORISEE | → * : INTERDITE
• PENDING_FINALITY → FINALIZED : AUTORISEE | → FAILED : AUTORISEE (ex: reorg) | → * : INTERDITE
• FINALIZED → * : INTERDITE (etat terminal)
• FAILED → * : INTERDITE (etat terminal)

5bis. Diagrammes¶

Diagramme d'etats — AnchorBatchStatus (INV-274-04, INV-274-05)¶

stateDiagram-v2
    [*] --> PENDING

    PENDING --> BUILDING : batch construit
    PENDING --> FAILED : erreur construction

    BUILDING --> SUBMITTED : soumis on-chain
    BUILDING --> FAILED : erreur soumission

    SUBMITTED --> PENDING_FINALITY : tx confirmee (attente finality)
    SUBMITTED --> FAILED : erreur confirmation

    PENDING_FINALITY --> FINALIZED : finality atteinte
    PENDING_FINALITY --> FAILED : reorg detecte (INV-274-03)

    FINALIZED --> [*]
    FAILED --> [*]

    note right of FINALIZED : Etat terminal — aucune\ntransition sortante (INV-274-05)
    note right of FAILED : Etat terminal — aucune\ntransition sortante (INV-274-05)

Diagramme de sequence — Extraction de faits et evaluation Prolog (FN-01, FN-02, FN-03)¶

sequenceDiagram
    participant Extract as extract-facts.py
    participant AST as AST Parser (TypeScript)
    participant Prolog as Moteur Prolog

    Extract->>AST: Analyse entite anchor_batch
    AST-->>Extract: Propriete status: AnchorBatchStatus (enum TS)

    Note over Extract: Genere entity_enum_values<br/>(INV-274-01, INV-274-02)<br/>6 valeurs depuis enum TS,<br/>independamment du type SQL varchar

    Extract->>AST: Analyse service anchor_batch
    AST-->>Extract: Methode handleReorg detectee

    Note over Extract: Genere service_method<br/>(INV-274-03)

    Extract->>Prolog: Soumet faits extraits
    Prolog->>Prolog: check_batch_status_enum (CA-01)
    Prolog->>Prolog: check_handle_reorg (CA-03)
    Prolog->>Prolog: 22 checks existants (INV-274-06)
    Prolog-->>Extract: Rapport 24/24 OK (CA-05)

6. Cas d'erreur¶

7. Criteres d'acceptation (testables)¶

8. Scenarios de test (Given / When / Then)¶

ST-01 — Enum detecte depuis propriete enum TS avec colonne varchar¶

• Given une entite anchor_batch avec colonne status stockee en varchar et propriete typee AnchorBatchStatus
• When l'extraction de faits est executee
• Then le fait entity_enum_values(anchor_batch, status, Values) est present avec 6 valeurs exactes

ST-02 — Presence explicite de FINALIZED et FAILED¶

• Given les faits extraits pour anchor_batch.status
• When la regle check_batch_status_enum est evaluee
• Then FINALIZED et FAILED sont presents dans Values et le check est OK

ST-03 — Methode handleReorg exposee par le service anchor_batch¶

• Given le module anchor_batch
• When l'extraction de faits service est executee
• Then service_method(anchor_batch, handleReorg) est present

ST-04 — Check reorg passe a OK¶

• Given les faits extraits incluant la methode reorg contractuelle
• When check_handle_reorg est evalue
• Then le resultat est OK

ST-05 — Non-regression checks existants¶

• Given un baseline de 22 checks PV-ANCHOR-001 a OK
• When la nouvelle extraction/regles est appliquee
• Then les 22 checks restent OK

ST-06 — Score global conforme¶

• Given l'ensemble des checks PV-ANCHOR-001
• When l'audit formel complet est execute
• Then le resultat global est 24/24 OK

ST-07 — Verrouillage des etats terminaux¶

• Given un batch en statut FINALIZED ou FAILED
• When une transition sortante est sollicitee
• Then la transition est refusee (etat terminal)

ST-08 — Retour d'etat interdit¶

• Given un batch en statut SUBMITTED ou PENDING_FINALITY
• When une transition retour vers un etat precedent est sollicitee
• Then la transition est refusee (retour interdit)

9. Hypotheses explicites¶

References¶

• Epic : BACKEND-3 (crypto-proof)
• JIRA : PD-274
• Repos : ProbatioVault-backend (principal), ProbatioVault-doc (extract-facts.py)
• Norme : PV-ANCHOR-001 (rapport d'audit formel)
• Stories liees : PD-272 (pattern correction PV-PROOF), PD-273 (pattern correction PV-AUDIT)