PD-296 — Plan d'implémentation¶

1. Le skill (gov-step, gov-gate, gov-check-plan, gov-accept) atteint un point d'intégration
2. Appel : ./scripts/formal-check.sh <story_id> <project_code> <checkpoint_id> <trigger_event> <artifact_path>
3. formal-check.sh :
   a. Valide les entrées (D-296-01..D-296-05, D-296-10) → si invalide : FAILED_BLOCKING immédiat
   b. Génère correlation_id (uuidgen) et idempotency_key (sha256 du payload)
   c. Acquiert le lock flock sur /tmp/formal-lock-<story_id>-<checkpoint_id>.lock (TTL via timeout)
   d. Vérifie idempotence (fichier .formal-idempotency/<key>) → si replay identique : retourne résultat caché
   e. Met l'état à RUNNING dans .gov-local.json via formal-state.sh
   f. Invoque l'outil formel avec timeout :
      - coherence_spec → /coherence check PD-XX (via unset CLAUDECODE && claude -p)
      - formal_contracts, formal_plan, formal_code → /formal-verify (via unset CLAUDECODE && claude -p)
      - formal_full → /formal-verify pipeline complet
   g. Mappe la sortie vers verdict GO|FAIL :
      - /coherence : "blocking": true + issues > 0 → FAIL, sinon GO
      - /formal-verify : exit code 0 → GO, exit code 1/2/3 → FAIL
      - Timeout (180s) → FAIL + failure_code=TIMEOUT
      - Outil absent → FAIL + failure_code=TOOL_UNAVAILABLE
   h. Construit formal_check_result_json (D-296-14) avec toutes les clés requises
   i. Met l'état à PASSED ou FAILED_BLOCKING via formal-state.sh
   j. Libère le lock, enregistre idempotence, écrit résultat en audit
   k. Retourne le JSON sur stdout (exit 0 si PASSED, exit 1 si FAILED_BLOCKING)
4. Le skill lit le code de retour :
   - exit 0 → continue le workflow
   - exit 1 → affiche les détails, bloque la transition aval, propose correction

1. Le skill affiche les détails d'échec (details[]) à l'utilisateur
2. L'utilisateur corrige l'artefact source (spec, plan, code...)
3. Le skill relance formal-check.sh avec le même checkpoint_id
4. formal-check.sh :
   a. Détecte état courant FAILED_BLOCKING → transition vers PENDING (autorisée)
   b. Génère nouveau correlation_id, nouvelle idempotency_key (payload différent)
   c. Exécute le contrôle formel normalement
   d. Si GO → PASSED, transition aval débloquée
   e. Si FAIL → FAILED_BLOCKING à nouveau, nouvelle boucle

1. Après une gate NON_CONFORME, l'artefact source est modifié (spec v2, code corrigé...)
2. Le skill appelle formal-check.sh avec flag --force-recheck
3. formal-check.sh :
   a. Détecte état courant PASSED + flag --force-recheck → transition vers PENDING
   b. Conserve l'historique du PASSED précédent dans details[]
   c. Exécute le contrôle formel sur l'artefact modifié
   d. Résultat : nouveau PASSED ou FAILED_BLOCKING
Note : Sans --force-recheck, PASSED reste terminal (protection contre les relances inutiles)

TEST-ID: TC-INV-01
Référence spec: INV-296-12

GIVEN
  - Le composant formal-state.sh est chargé
  - Un checkpoint existe dans .gov-local.json avec un état valide (PENDING)
WHEN
  - Une tentative de set_checkpoint_state est faite avec un état invalide ("DONE", "SKIPPED", "WARNING", "N/A")
THEN
  - La fonction retourne exit 1 avec message "Invalid state: <state>. Allowed: PENDING, RUNNING, PASSED, FAILED_BLOCKING"
  - L'état dans .gov-local.json reste inchangé (PENDING)
AND
  - Seuls les 4 états PENDING, RUNNING, PASSED, FAILED_BLOCKING sont acceptés par set_checkpoint_state
  - Le test vérifie les 4 états valides (acceptés) ET au moins 5 états invalides (rejetés)

TEST-ID: TC-INV-02
Référence spec: INV-296-13

GIVEN
  - formal-state.sh est chargé avec la matrice de transitions ALLOWED_TRANSITIONS
  - Un checkpoint est dans l'état RUNNING
WHEN
  - Une transition RUNNING → PENDING est tentée (transition interdite §5.4)
THEN
  - La fonction retourne exit 1 avec message "Forbidden transition: RUNNING -> PENDING"
  - L'état reste RUNNING
AND
  - Le test vérifie exhaustivement les 12 transitions (4 autorisées, 8 interdites) de la matrice §5.4
  - Chaque transition interdite est rejetée avec message explicite
  - Chaque transition autorisée est acceptée

TEST-ID: TC-INV-03
Référence spec: INV-296-17

GIVEN
  - formal-check.sh est disponible sur le PATH
  - Un checkpoint valide est prêt à être déclenché
WHEN
  - L'appel est fait avec des flags de contournement :
    a) --skip
    b) --warning-only
    c) --dry-run
    d) --informative
    e) Variable d'environnement GOV_FORMAL_SKIP=1
THEN
  - Chaque tentative retourne exit 1 avec message "Unknown flag" ou "GOV_FORMAL_SKIP is not supported"
  - Aucun contrôle formel n'est exécuté
  - Aucun changement d'état ne se produit
AND
  - Le code source de formal-check.sh ne contient aucune branche conditionnelle sur ces flags/variables
  - grep -c "warning.only\|skip\|dry.run\|informative" scripts/formal-check.sh == 0 (hors commentaires)

TEST-ID: TC-INV-04
Référence spec: INV-296-18

GIVEN
  - La matrice de couverture tests §2 (TC-* → INV-* → CA-*)
  - Les 18 invariants INV-296-01..18
  - Les 12 critères d'acceptation CA-296-01..12
WHEN
  - Un audit de couverture est exécuté (script ou vérification manuelle)
THEN
  - Chaque INV-296-* est couvert par au moins 1 test TC-*
  - Chaque CA-296-* est couvert par au moins 1 test TC-*
  - Les tests TC-INV-01..04 (ce document) sont définis avec GIVEN/WHEN/THEN
AND
  - Les réserves de testabilité du document tests §9 sont documentées :
    - GATE3_SPEC_FORMAL (nouveau checkpoint) : testable via TC-NOM ajouté
    - Configurabilité SLA : testable via variable d'environnement GOV_FORMAL_TIMEOUT_SEC
    - TC-NOM-07 exhaustif (8 projets) : test par échantillonnage (≥2 projets)
  - L'audit est reproductible (script ou checklist vérifiable)