Aller au contenu

PD-297 — Plan d'implémentation

1. Découpage en composants

Module Responsabilité Fichiers
ontology-enricher Extraire prédicats de la spec + contracts, persister dans ProbatioVault-formal/ontology/{domain}/ scripts/enrich-ontology.py
formal-models-extractor Extraire invariants TLA+/Alloy depuis code-contracts, les ajouter aux modèles formels scripts/extract-formal-invariants.py
formal-verify-pipeline Pipeline complet /formal-verify qui charge les modèles et vérifie le code ProbatioVault-formal/formal-verify.py
non-regression-formal Après enrichissement, relancer coherence sur la base étendue scripts/formal-non-regression.sh
compounder-integration Phase 7 dans gov-compounder : appeler les 4 modules ci-dessus .claude/commands/gov-compounder.md (patch)

2. Résolution des conditions RESERVE Gate 3

Condition Résolution
FSM clearing ENRICHMENT_DEGRADED → NOMINAL inatteignable Ajouter transition dans la FSM : ENRICHMENT_DEGRADED → NOMINAL si 2 enrichissements consécutifs réussis
Regex injection Prolog (D-297-11) Sanitizer strict : whitelist [a-z0-9_] pour les atomes Prolog, rejet de tout caractère spécial (:, -, ., !, (, ))
TC-NR-04 teste observable interdite par FSM Corriger TC-NR-04 pour tester la transition ajoutée au point 1

3. Flux technique

3.1 Enrichissement ontologie (step 10 / story DONE)

  1. enrich-ontology.py --story PD-XX --spec-path <path> --contracts-path <path>
  2. Parse la spec : extraire les invariants INV-XXX-NN, les contraintes, les règles métier
  3. Convertir en prédicats Prolog (format identique à extract-eb-predicates.py)
  4. Écrire dans ProbatioVault-formal/ontology/{domain}/PD-XXX.pl
  5. Recompiler la base globale : cat ontology/**/*.pl > ontology/global.pl
  6. Lancer coherence-report.py --full pour vérifier que l'ajout ne crée pas de contradiction

3.2 Extraction modèles formels (step 10)

  1. extract-formal-invariants.py --story PD-XX --contracts-path <path>
  2. Parse code-contracts.yaml : extraire les invariants numérotés
  3. Pour chaque invariant, générer un stub TLA+ et/ou Alloy selon le type :
  4. Invariants de données (types, bornes) → Alloy fact
  5. Invariants de protocole (séquence, état) → TLA+ INVARIANT
  6. Invariants de sécurité (accès, permission) → Prolog rule
  7. Écrire dans ProbatioVault-formal/models/{domain}/PD-XXX.{tla,als,pl}

3.3 Pipeline formal-verify.py

  1. Scope contracts : charger les contracts, extraire les invariants, vérifier cohérence Prolog
  2. Scope code : charger le code produit (git diff), extraire les assertions, vérifier contre les modèles TLA+/Alloy
  3. Scope full : contracts + code + non-régression ontologie complète
  4. Retourne JSON {"verdict":"GO|FAIL","scope":"...","details":{...}}

3.4 Non-régression formelle

  1. formal-non-regression.sh --story PD-XX
  2. Appelle coherence-report.py --full --json
  3. Compare le score avant/après enrichissement
  4. Si score baisse de > 1% → WARNING
  5. Si nouvelles contradictions bloquantes → FAIL

4. Contraintes

  • ProbatioVault-formal doit être accessible depuis ia-governance (chemin relatif ../ProbatioVault-formal/)
  • Les prédicats Prolog extraits sont sanitisés : whitelist [a-z0-9_] pour les atomes, longueur max 128 chars
  • Les modèles TLA+/Alloy générés sont des stubs — la vérification complète (model checking) reste manuelle
  • Outil interne mono-utilisateur — pas de sécurité multi-tenant sur l'ontologie

5. Ordre d'implémentation

  1. enrich-ontology.py (fondation — le reste en dépend)
  2. formal-non-regression.sh (valide que l'enrichissement ne casse rien)
  3. extract-formal-invariants.py (extraction modèles)
  4. formal-verify.py (pipeline complet)
  5. gov-compounder.md patch (intégration workflow)

6. Estimation

~3 jours de dev. Les scripts sont des adaptations de extract-eb-predicates.py et coherence-report.py existants.