Aller au contenu

PD-275 — Specification Review

Documents d'entrée

  • Spécification : PD-275-specification.md
  • Tests : PD-275-tests.md
  • Domaine : crypto-proof (conformité formelle Prolog)

Learnings injectés

  • PD-274 (Gate ⅜) : stories conformité formelle convergent en v1 GO (>9.0) — faux positifs ~70%
  • PD-277 (Gate ⅗) : contractualiser format + faits Prolog + types SQL dès v1
  • PD-55 (Gate 3) : définir RFC/formats/bornes dès la spec pour éviter itérations
  • PD-264 (REX) : contractualiser migrations DDL dans la spec avant Gate 3

1) Ambiguïtés

A-01

Type : Ambiguïté
Référence : Spec §3 (Définitions) / §5 (Modèle d'états batch)
Description : L'état `NON_FINALIZED` est utilisé dans le modèle d'états batch (§5) comme
  état source de la transition vers `FINALIZED`, mais n'est défini nulle part dans §3
  (Définitions). Est-ce un état unique ou un alias pour plusieurs états existants de
  `anchor_batch` ? Q-02 reconnaît l'incomplétude mais le modèle d'états utilise
  `NON_FINALIZED` comme si c'était un état formel.
Impact : TC-INV-07B teste les transitions sortantes de `NON_FINALIZED` et `FINALIZED`,
  mais si `NON_FINALIZED` est un alias pour N états, les transitions sortantes de chacun
  doivent être documentées individuellement pour satisfaire INV-275-07.
Gravité : Majeur

A-02

Type : Ambiguïté
Référence : Spec §5 Flux F1 / INV-275-03-confirmation-persistence
Description : Le mécanisme de mise à jour de `confirmation_count` n'est pas spécifié.
  Flux F1 dit "Le nombre observé est persisté" sans définir l'interface (API, événement,
  job interne). INV-275-03 réfère à "le mécanisme de suivi des confirmations" sans le
  nommer. Note domaine crypto-proof : si ce mécanisme est hors scope PD-275
  (pré-existant), la spec devrait le déclarer explicitement en §2 ou en hypothèse.
Impact : TC-NOM-01 assume "une mise à jour de confirmations valide est appliquée" —
  le test est formulable mais l'interface à tester est ambiguë.
Gravité : Mineur

A-03

Type : Ambiguïté
Référence : Spec §5 Flux F1 step 4
Description : "Le batch reste dans son état courant tant que les conditions de finalisation
  ne sont pas remplies" — cela implique-t-il que la mise à jour de `confirmation_count`
  pourrait déclencher implicitement une finalisation si les conditions sont remplies ?
  Ou la finalisation est-elle toujours un acte explicite (Flux F2) ? La distinction entre
  mise à jour passive (F1) et finalisation active (F2) n'est pas contractualisée.
Impact : Si F1 peut déclencher implicitement F2, le modèle de test change (TC-NOM-01
  devrait vérifier l'absence de transition implicite).
Gravité : Mineur

A-04

Type : Ambiguïté
Référence : Spec §5 Flux F4 / H-01
Description : Flux F4 requiert "une identité signer" à la soumission, mais ne précise
  pas comment cette identité est transmise (paramètre explicite, dérivée du contexte
  d'authentification, extraite du batch). H-01 reconnaît la dépendance PD-177 mais ne
  fournit pas de contrat d'interface.
Impact : L'implémentation de CA-05 est bloquée si le mécanisme de résolution signer
  n'est pas contractualisé.
Gravité : Majeur

2) Contradictions

C-01

Type : Contradiction
Référence : Spec CA-02 (observable) vs Tests TC-NOM-03 (matrice couverture §2)
Description : CA-02 est formulé exclusivement en termes de refus : "finalizeBatch()
  refuse si confirmation_count < FINALITY_DEPTH". Or TC-NOM-03 teste le chemin
  d'acceptation (confirmation_count = D → transition autorisée) et est mappé à CA-02
  dans la matrice de couverture. CA-02 ne couvre pas contractuellement le chemin
  d'acceptation — il manque un critère d'acceptation explicite pour "finalizeBatch()
  autorise si confirmation_count >= FINALITY_DEPTH".
Impact : Le chemin nominal d'acceptation n'a pas de CA dédié. Un auditeur pourrait
  contester la couverture de TC-NOM-03.
Gravité : Majeur

C-02

Type : Contradiction
Référence : Tests §3 TC-NOM-02 (Flux nominaux) vs §4 TC-ERR-02 (Cas d'erreur)
Description : TC-NOM-02 et TC-ERR-02 testent exactement le même scénario (finalizeBatch
  avec confirmation_count = D-1 → refus ERR-FINALITY-INSUFFICIENT). TC-NOM-02 est classé
  dans "Flux nominaux" alors qu'il teste un refus. Duplication exacte avec classification
  contradictoire.
Impact : Ambiguïté sur le test faisant foi. Risque de double maintenance.
Gravité : Mineur

C-03

Type : Contradiction
Référence : Tests §3 TC-NOM-07 vs §4 TC-ERR-04
Description : TC-ERR-04 et TC-NOM-07 testent le même scénario (submitBatch avec adresse
  absente → ERR-SIGNER-NOT-FOUND). Duplication exacte entre sections.
Impact : Même que C-02.
Gravité : Mineur

C-04

Type : Contradiction
Référence : Tests §3 TC-NOM-06 vs §4 TC-ERR-05
Description : TC-ERR-05 et TC-NOM-06 testent le même scénario (submitBatch avec signer
  REVOKED → ERR-SIGNER-REVOKED). Duplication exacte entre sections.
Impact : Même que C-02.
Gravité : Mineur

3) Règles non testables

NT-01

Type : Non testable
Référence : INV-275-08-envelope-encryption / TC-INV-08
Description : TC-INV-08 inspecte "les artefacts temporaires éventuels produits par ces
  flux". Le mot "éventuels" rend l'observable conditionnel. Si PD-275 ne produit aucun
  artefact cryptographique temporaire (aucun flux ne mentionne de DEK, ReKey ou fragment),
  le test est vacuement vrai et l'invariant est non falsifiable dans ce périmètre.
Impact : L'invariant ne peut pas échouer, donc il n'apporte aucune garantie testable.
Gravité : Mineur

NT-02

Type : Non testable
Référence : INV-275-07-state-machine-complete / TC-INV-07B
Description : TC-INV-07B vérifie la complétude du modèle d'états batch, mais le document
  de test §9 reconnaît que l'exhaustivité des états `anchor_batch` hors `FINALIZED` est
  "incompletable sans liste canonique" (Q-02). Le test ne peut vérifier que le modèle
  partiel déclaré, pas la complétude réelle. L'invariant INV-275-07 exige pourtant
  "Toute transition sortante des états identifiés est explicitement autorisée ou interdite".
Impact : INV-275-07 est satisfait syntaxiquement mais pas sémantiquement pour le batch.
Gravité : Bloquant (cohérent avec le verdict tests §9)

4) Incohérences Spec ↔ Tests

IST-01

Type : Incohérence Spec↔Tests
Référence : Spec CA-07 / Tests TC-NR-01
Description : CA-07 exige "Les tests couvrent les 5 comportements nouveaux (checks
  28–32)". TC-NR-01 est un méta-test : "Rapport de tests mappé vers
  TC-NOM-01/02/04/05/06/07/08". Ce n'est pas un test comportemental mais une vérification
  de traçabilité. Le mapping liste 7 tests pour 5 checks sans expliciter la
  correspondance check→test.
Impact : L'observable "Rapport de tests prouvant les scénarios requis" est un artefact
  documentaire, pas un test exécutable automatisé.
Gravité : Mineur

IST-02

Type : Incohérence Spec↔Tests
Référence : Spec §6 ERR-SIGNER-NOT-FOUND / Tests TC-ERR-03
Description : TC-ERR-03 teste revokeSigner(address) avec adresse absente du registre.
  La spec §6 mentionne ERR-SIGNER-NOT-FOUND pour "soumission/révocation" mais le Flux F3
  (révocation) ne traite pas explicitement le cas adresse absente — il dit "Le système
  résout l'entrée signer_registry correspondante" puis "Si statut ACTIVE". Le cas
  "adresse introuvable" dans le flux de révocation n'a pas de step explicite dans F3.
Impact : Le test suppose un comportement (refus fail-closed) cohérent avec INV-275-01,
  mais le flux ne le documente pas.
Gravité : Mineur

IST-03

Type : Incohérence Spec↔Tests
Référence : Matrice couverture §2 / TC-NOM-09
Description : La matrice mappe TC-NOM-09 à INV-275-03-confirmation-persistence et CA-08.
  Or TC-NOM-09 teste la réversibilité migration (up/down/up). Le lien avec INV-275-03
  est indirect — TC-NOM-09 vérifie que le schéma est restauré, pas que confirmation_count
  est correctement persisté. Le mapping devrait pointer vers CA-08 seul.
Impact : Traçabilité imprécise dans la matrice de couverture.
Gravité : Mineur

5) Hypothèses dangereuses

HD-01

Type : Hypothèse dangereuse
Référence : Spec §5 Flux F3 / INV-275-05-revocation-atomic-audited
Description : La spec exige "transition atomique" pour la révocation mais ne spécifie pas
  le mécanisme d'atomicité. En contexte PostgreSQL+TypeORM, une transaction suffit. Mais
  si revokedAt/revokedBy sont persistés dans un système distinct (event store, audit log
  externe), l'atomicité cross-système n'est pas garantie. TC-ERR-06 teste l'échec de
  persistance audit mais suppose que l'échec est détectable et rollbackable.
Impact : Si l'audit trail est dans un système non transactionnel avec la DB, l'atomicité
  est compromise.
Gravité : Mineur (probable même DB en contexte PD-275)

HD-02

Type : Hypothèse dangereuse
Référence : Spec §5 Flux F3 / Flux F4 — concurrence
Description : Aucun scénario de concurrence n'est spécifié. Deux revokeSigner() concurrents
  sur le même signer ACTIVE pourraient tous deux lire ACTIVE et tenter la transition.
  Sans garde de concurrence (SELECT FOR UPDATE, version optimiste), un double-write est
  possible avec deux audit trails pour la même révocation. De même, un submitBatch() et
  un revokeSigner() concurrents sur le même signer créent une race condition non
  contractualisée.
Impact : Audit trail potentiellement incohérent. Violation possible de INV-275-05
  (unicité atomicité).
Gravité : Majeur

HD-03

Type : Hypothèse dangereuse
Référence : Spec H-04 / INV-275-01-fail-closed
Description : H-04 reconnaît le risque de "refus généralisés fail-closed en phase initiale"
  si le registre n'est pas seedé. Combiné avec INV-275-01 (deny by default pour signer
  inconnu), un déploiement sans seed stratégie bloque toute soumission. Ce n'est pas
  seulement un risque opérationnel — c'est une conséquence directe et certaine du design
  fail-closed.
Impact : Indisponibilité complète du service d'ancrage post-déploiement si seed non
  effectué.
Gravité : Majeur

6) Risques sécurité / conformité

RS-01

Type : Risque sécu/conformité
Référence : Spec §5 Flux F3 / INV-275-05-revocation-atomic-audited
Description : Le Flux F3 ne spécifie aucun modèle d'autorisation pour revokeSigner().
  Qui est autorisé à révoquer un signer ? Sans contrôle d'accès, tout appelant
  authentifié pourrait révoquer n'importe quel signer, provoquant un déni de service
  sur le système d'ancrage. Le champ revokedBy trace l'auteur mais ne contraint pas
  qui peut être cet auteur.
Impact : Vecteur de déni de service par révocation massive. Violation potentielle du
  principe de moindre privilège.
Gravité : Majeur

RS-02

Type : Risque sécu/conformité
Référence : Spec INV-275-05 / Q-04
Description : revokedBy est exigé comme trace d'audit mais son format n'est pas
  contractualisé (Q-04). Si revokedBy est un paramètre fourni par l'appelant plutôt que
  dérivé du contexte d'authentification, il peut être usurpé. L'audit trail perdrait sa
  valeur probante.
Impact : Falsification possible de l'audit trail de révocation.
Gravité : Majeur

Synthèse

Gravité Nombre IDs
Bloquant 1 NT-02
Majeur 7 A-01, A-04, C-01, HD-02, HD-03, RS-01, RS-02
Mineur 10 A-02, A-03, C-02, C-03, C-04, NT-01, HD-01, IST-01, IST-02, IST-03

Point bloquant : NT-02 est cohérent avec le verdict QA du document de tests (§9 : Q-02 marqué Bloquant). La résolution de Q-02 (liste canonique des états anchor_batch) est nécessaire pour lever ce blocage.

Points majeurs critiques : L'absence de modèle d'autorisation pour revokeSigner() (RS-01) et la race condition non contractualisée (HD-02) sont les risques les plus significatifs au-delà des questions ouvertes déjà identifiées par la spec.

Note domaine crypto-proof : Conformément aux learnings PD-274 (Gate 3), les stories de conformité formelle convergent typiquement en v1 GO avec ~70% de faux positifs LLM. Les écarts identifiés ici sont majoritairement des insuffisances contractuelles réelles (Q-02 non résolu, autorisation absente, concurrence non traitée) et non des faux positifs de forme.