spec: noyau d.invariants I1-I9 et vérificateurs mécaniques

[atlas-by-clodocapeo]

1. Canonical provenance

• ADR : ZabLaboratory/QueryMe · docs/adr/001-positionnement-et-architecture.md · Status: accepted · Decided: 2026-08-15 · Deciders: @ClodoCapeo
• Révision ADR : celle mergée par ec54f54b1, non amendée. base_revision : main 17e78871d
• ID provisoire : QM-P0-02 · Phase : P0
• Work unit amont : QM-P0-01 · aval : QM-P0-04, QM-P0-05, QM-P0-08, QM-P1-03, QM-P1-04
• Rapport de routage : proposition Atlas du 2026-08-15 sur [anchor] ADR 001 persistence lease #6, graphe validé nommément par Eleven

2. Objective

Chaque invariant I1 à I9 possède un énoncé normatif, un régime de conséquence assigné, et un vérificateur qui le décide mécaniquement sur un manifeste.

3. Work graph

• continues: —
• depends_on: QM-P0-01
• parallelization_group: p0-spec
• initial_state: blocked (attend QM-P0-01)
• recommended_role: forge
• required_agent_reports: forge, probe, bastion (§3.10(4), consultatif ici, terminal sur QM-P0-05)

4. Owned scope

• Énoncé normatif des neuf invariants, verbatim de §3.2, chacun étiqueté de son régime de conséquence : structurel {I1, I2, I4, I5, I6, I8}, budgétaire {I3, I7}, débit {I9}.
• Texte normatif de la partition ternaire et de la revendication en trois temps, dont la mention que le troisième temps est appliqué et non impossible.
• Un vérificateur mécanique par invariant décidable sur le manifeste seul : atteignabilité sur le graphe pour I1 ; énumération rôles × relations atteignables pour I2 ; clôture de la projection pour I4 ; clôture de l'ensemble d'opérateurs pour I5 ; présence des pré/post-conditions d'écriture pour I6 ; présence des deux limites sur toute relation atteignable pour I9 (part structurelle).
• Définition du graphe d'exposition (relations dont au moins un champ figure dans la projection déclarée) et du graphe de mutation (relations qu'une opération déclare modifier), établis comme fonctions pures du manifeste, avec le statut des relations traversées — n'appartenant à aucun des deux.
• Contrainte de majoration par axe énoncée normativement : chaque expression de coût est un majorant sur son axe, elle peut surestimer, jamais sous-estimer (§3.3, propriété 2).
• Fonction de recalcul, depuis le manifeste seul, de l'ensemble des opérations requérant une autorisation et de l'ensemble des relations portant des limites — support d'audit (§3.2 in fine).
• Version du jeu d'invariants, distincte du schéma et du paquet, destinée au tuple d'attestation.

5. Exclusions

• I3 et I7 n'ont pas de vérificateur de dépassement ici : leur régime est budgétaire, la classification borné/budgété est une propriété du compilateur — QM-P1-06. Ce qui est vérifié ici est la déclaration, pas le verdict.
• I8 n'a pas de vérificateur statique : l'auditabilité est réalisée par le répartiteur à l'exécution — QM-P1-17.
• La part appliquée d'I9 — réservation, comptage, fenêtre glissante — est P1 (QM-P1-11 à QM-P1-15). Seule la part structurelle (les deux limites déclarées) est ici.
• Aucune émission d'attestation : les vérificateurs sont des fonctions, l'orchestration et la signature sont QM-P0-05.
• Aucun seuil : « la limite existe » est ici, « la limite vaut au plus X » est QM-P0-04.
• Aucun corpus : QM-P0-06 consomme ces vérificateurs, il ne les contient pas.
• Confusion voisine à écarter : le calcul des deux graphes est défini ici et compilé en QM-P1-04 — la définition est normative, la compilation est de l'artefact.

6. Inputs and outputs

Entrées — le schéma de QM-P0-01 ; ADR §3.2 (I1..I9 verbatim, trois régimes, revendication en trois temps), §3.3 (propriétés normatives 1 à 3), §3.4 (« Assiette — deux graphes, deux axes »).

Sorties — le document normatif du noyau, la bibliothèque de vérificateurs, les fonctions de calcul des deux graphes et des ensembles d'obligations, l'identifiant de version du jeu d'invariants.

7. Acceptance criteria

• RC-12 (I1) — un manifeste comportant une seule relation atteignable sans liaison de cloisonnement est rejeté ; test d'atteignabilité sur le graphe.
• RC-13 (I2) — l'énumération rôles × relations atteignables donne l'ensemble vide pour toute identité non authentifiée, et un manifeste accordant un privilège à un rôle anonyme est rejeté ; énumération mécanique + test de rejet.
• RC-14 (I6) — un manifeste comportant une écriture sans post-condition est rejeté. (Les deux autres volets de RC-14 — vérification dans le corps de la fonction générée, annulation sur échec — sont couverts par QM-P1-03.)
• RC-16 (I9) — un manifeste comportant une relation atteignable dépourvue de l'une ou l'autre de ses deux limites est rejeté ; deux tests de rejet, un par axe.
• RC-16 (suite) — l'ensemble des relations portant des limites, le graphe d'exposition et le graphe de mutation sont recalculables depuis le manifeste seul ; test comparant le recalcul à une référence sur un manifeste multi-relations.
• Une relation traversée par une opération et exposée par une autre appartient au graphe d'exposition de la seconde et à aucun graphe de la première — test dédié (fonde RC-34, exercé en P1).
• Chaque invariant porte son étiquette de régime, et la partition ternaire est reproduite sans altération — contrôle de présence en CI.
• La contrainte de majoration par axe est énoncée séparément pour l'extraction et la mutation — l'axe de mutation n'hérite rien de l'axe d'extraction (§3.10(9), RC-38(a)).
• mypy --strict, ruff, uv lock --check verts.

8. Expected evidence

Matrice invariant → régime → vérificateur → test, complète sur les neuf lignes ; sorties des tests de rejet nommées par RC ; recalcul des deux graphes confronté à sa référence sur le manifeste multi-relations ; SHA signé et run CI vert.

9. Risks and rollback

Risque principal — R2 : c'est ici que se joue la survente. Un invariant étiqueté structurel dont le vérificateur ne décide en réalité qu'une déclaration transforme une impossibilité revendiquée en simple obligation de forme. Le point sensible est I9, dont seule la part déclarative est structurelle et dont tout le reste est appliqué. Contre-mesure : l'étiquette de régime est portée par le code du vérificateur lui-même, pas seulement par la prose, et §3.10(4) instruit la légitimité de la partition avant QM-P0-05.

Rollback — le noyau est consommé par l'évaluateur, le corpus et la clause publique. Un revert après QM-P0-08 laisserait une clause publiée décrivant un noyau retiré : la procédure est donc revert du noyau et retrait simultané de la clause publique dans le même commit, jamais l'un sans l'autre. Avant QM-P0-05, revert simple, sans état résiduel.

10. ADR clauses and invariants covered

§3.2 — « Trois régimes d'invariants » intégralement ; I1, I2, I4, I5, I6 (part déclarative), I8 (énoncé), I9 (part structurelle) ; « La revendication publique se formule donc en trois temps ». §3.3 — propriétés normatives 1 et 2 (les deux fonctions pour toute opération, majoration par axe). §3.4 — « Assiette — deux graphes, deux axes », statut de la relation traversée. §3.9 — P0, « noyau I1..I9 avec vérificateurs mécaniques », « définition des graphes d'exposition et de mutation ».

---

Ancre du cycle : #6 (lien, pas dépendance bloquante).