Set-OPS-Public/wiki/La-preuve.md

138 lines
6.7 KiB
Markdown
Raw Normal View History

# La preuve — prouver, pas affirmer
> **Unité d'apprentissage.** Moule : ① concept → ② Set-OPS → ③ transférable → ④ à toi de jouer.
---
## ① Le concept *(générique)*
Une affirmation sans **vérification rejouable** n'est que du marketing. « C'est sécurisé »,
« c'est sauvegardé », « ça fonctionne » — *prouve-le*. La discipline se résume à une règle :
> **Ne jamais affirmer plus que ce qu'on prouve.**
Trois idées la portent :
- **Registre d'affirmations** — chaque promesse publique est tracée vers une **commande qui la
vérifie**, ou marquée honnêtement « non prouvée ».
- **Harnais rejouable** — une seule commande rejoue *toutes* les preuves et produit une **pièce
justificative datée**. On ne « croit » pas : on **relance**.
- **Le registre a le droit de perdre** — une preuve qui échoue fait *redescendre* l'affirmation.
C'est la seule condition pour qu'un tel registre ait de la valeur.
---
## ② Comment Set-OPS le fait
- **Le registre** : `docs/audit/affirmations.md` — chaque affirmation du dépôt (README, docs,
aide `make`, GUI) reliée à une preuve et un statut (✅/🟡/❌/⚪).
schema du plan : la forme des registres devient derivee, et gardee Etape 2 du chantier « l UI reflete fidelement la structure ». Le GUI porte CHAMPS_ECRITS_PAR_GUI, une liste tenue A LA MAIN de ce qu il sait ecrire, que P19 confronte au reel. C est une copie — gardee, donc honnete, mais une copie : quelqu un doit penser a l allonger. `make schema` produit docs/audit/schema-plan.json : six registres, 42 champs, leurs types, leurs enumerations et ce qui est requis. CE QUE LE SCHEMA EST, ET CE QU IL N EST PAS schema -> la FORME -> generera les champs du formulaire validateurs -> la COHERENCE -> refusent une saisie incoherente Un JSON Schema ne sait pas dire qu un `consommateur` designe une application inexistante, ni qu une integration universelle recopiee au plan est un defaut. Vouloir l y mettre creerait la seconde source de verite que tout ce depot refuse. Les valider_* restent l autorite. LES ENUMERATIONS SONT IMPORTEES, JAMAIS RECOPIEES ETATS_SERVEUR, PORTEES_BD et AUTORITES_DNS viennent des constantes que les validateurs appliquent. Une enumeration recopiee diverge — c est la lecon des neuf resolutions d instance que P41 garde depuis. CE QUE L ETAPE 1 AVAIT TROUVE, ET QUE P61 A CONFIRME Le recensement montrait `categorie` et `service` presents dans TOUS les plans et absents de CHAMPS_ECRITS_PAR_GUI, dont la ligne `nomenclature` est vide : le GUI ne sait pas les editer, l operateur doit ouvrir le YAML. P61 a refuse le premier schema pour cette raison exacte. Les trois tables imbriquees de la nomenclature sont donc DECRITES et non resumees en « object ». 31 champs observes dans l instance courante, 42 decrits par le schema. La difference n est pas du bavardage : observer une instance n est pas un schema. `noeud`, `stockage` et `coeurs` sont legitimes et simplement inutilises ici — un schema derive de l observation les INTERDIRAIT. P61, EPROUVEE DANS LES DEUX SENS fichier genere perime -> REFUSE champ du plan absent du schema -> REFUSE champ decrit mais inutilise au plan -> COMPTE, pas refuse Le troisieme point est delibere : refuser obligerait a retirer du schema un champ valide des que plus personne ne s en sert. Meme mesure que les lacunes nommees de P29. UN DEFAUT DE MON INSTRUMENT, PAYE EN ROUTE P61 comparait des noms a plat quand couverture_gui aplatit les tables imbriquees : elle criait sur un schema correct. L instrument mesurait autre chose que la cible. On aplatit desormais des deux cotes. make prouver : CONFORME, 60 OK, 0 echec, 1 saute. Prochaine etape : generer les formulaires depuis ce schema, et retirer CHAMPS_ECRITS_PAR_GUI. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Crgis8CxCWkAGFA1ecBz3q
2026-09-08 15:19:20 -04:00
- **Le harnais** : `make prouver` rejoue les preuves automatisables (**P01–P61**, sans trou dans la série) et écrit
`docs/audit/preuve-<date>.md`. `make verifier` les inclut : il **échoue** si une preuve échoue.
- **Chaque preuve garde une classe d'erreur.** Extrait :
| Preuve | Ce qu'elle empêche de mentir |
|---|---|
| P03 | l'inventaire n'est pas généré du plan (**diff vide**) |
| P06 | un registre incohérent (dont l'**hôte fantôme**) |
| P17 | un **modèle** invalide (tous, pas seulement le socle) |
| P18 | un **gabarit de voûte** incomplet |
| P19 | un champ du plan que le **GUI** ne sait pas éditer |
| P20 | de l'**adressage stocké** (tout doit dériver du seed) |
| P21 | une **collision d'index** entre instances fédérées |
| P31 | une capacité du dépôt **non expliquée** (script muet, cible sans aide, rôle sans README) |
| P32 | un intrant qu'un rôle **exige** et que l'instance ne fournit pas |
| P33 | deux rôles co-localisés qui **revendiquent le même port** |
portabilite : Technolibre debout, six devis, et P35 L'epreuve de portabilite est passee. Un second ecosysteme souverain complet, monte depuis zero par le meme moteur : 14 hotes, 2583 taches ok, 331 changed, 0 failed. Plan distinct, voute separee, realm technolibre, sa propre AC — et une topologie differente : LDAP et SSO sur des machines separees la ou Chezlepro les co-localise. Cinq devis CONFORME (identite, certificats, PostgreSQL, courriel, frontiere — 55 lignes 0 ecart). Le sixieme dit exactement la bonne chose : les 6 services repondent depuis l'edge, aucun depuis le poste, qui ne resout pas encore technolibre.internal (6 entrees /etc/hosts absentes — le plancher). SIXIEME DEFAUT MOTEUR. Le devis d'identite interrogeait LDAP en `ldapi:///` — un socket UNIX LOCAL — depuis l'hote serveur_keycloak. Cela ne marchait que par CO-LOCATION ACCIDENTELLE. Un tenant qui separe l'annuaire du SSO echouait sur « Failed to import python-ldap » : l'hote SSO n'a pas de client LDAP. Les deux lectures sont deleguees a l'hote DERIVE par resoudre_annuaire. P35 (D-75) : toute application dont le role exige une base en a une au plan. La garde de resoudre_base existait deja, mais s'est declenchee a la 92e tache de collab-01, apres quarante minutes, pour un ecart entierement lisible dans le plan. Rien n'y est code en dur : les roles concernes sont ceux qui INCLUENT resoudre_base, et le groupe reclame est lu dans le DEFAUT de la variable passee — jamais deduit du nom. serveur_icingaweb2 reclame la base de serveur_icinga ; une preuve supposant « role = groupe » aurait crie sur un cas sain. Eprouvee dans les deux sens ET sur les deux tenants, dont les registres n'ont pas la meme portee : base retiree -> ECHEC la nommant ; restauree -> OK. Verifie : prouver.py 35 OK sur les deux instances, ansible-lint production. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
2026-08-10 13:36:44 -04:00
| P35 | une application dont le rôle **exige une base** sans entrée au plan — sinon l'écart n'apparaît qu'après quarante minutes de déploiement |
preuve : P34 — chaque document declare son lecteur (D-74) La refonte de ce matin posait une convention. Une convention qu'on n'outille pas tient tant que quelqu'un y pense : c'est le raisonnement de D-70, applique au corpus documentaire. Etat de depart mesure : 2 documents sur 34 declaraient leur lecteur. Les 32 autres disaient leur SUJET — ce qui avait enfoui le runbook de reprise le plus utile du depot au §6 de autorisation.md. Les 38 le declarent desormais, lecteur determine document par document et non colle au gabarit : l'exploitant (devis, migration de tenant, cycle de vie, gabarit d'or), le mainteneur (conceptions, registres, carte), le lecteur externe (ecosysteme-chezlepro), l'agent IA (MISE-A-JOUR-CODEX-CLAUDE). Deux exemptions DERIVEES, pas listees — un chemin en dur aurait vieilli a la premiere page ajoutee : un document qui s'annonce genere, et un fragment sans titre. Les 13 exemptes verifies un par un ; aucun document ecrit a la main n'est exempte par accident. La preuve ne lit que l'EN-TETE, ce qui empeche frontiere-opnsense.md et plan-et-generation.md — qui parlent de generation dans leur corps — d'etre exemptes a tort. Eprouvee dans les deux sens. Elle a echoue seule des sa premiere execution en nommant deux documents que mon inventaire avait manques (docs/audit/). Puis test negatif delibere : declaration retiree de meta-classe.md -> ECHEC la nommant ; restauree -> OK. Ce qu'elle ne teste pas : que le lecteur declare soit le BON. Ca se juge en revue ; elle garantit qu'on a du y penser. P01–P34. Comptes perimes corriges au passage (AGENTS.md et devis-services.md annoncaient encore 30 preuves). Verifie : prouver.py 0 (34 OK), plan-recette inchange. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
2026-08-10 07:53:04 -04:00
| P34 | un document qui ne **déclare pas son lecteur** — il finirait rangé par sujet, donc introuvable |
> **Ce que ces preuves ne font pas, et il faut le savoir avant de leur faire confiance.** Elles
> sont toutes **statiques** : elles lisent le dépôt, sans un seul appel réseau. Elles établissent
> qu'il est cohérent *avec lui-même* — jamais que le système déployé lui ressemble. C'est dans
> cet angle mort qu'un certificat d'autorité a pu rester expiré huit heures sous un harnais vert.
> La conformité du **déployé** est l'affaire des **devis de service** (voir `docs/devis-services.md`).
Ce n'est pas un framework de test parallèle : le harnais **orchestre** l'outillage existant, il ne
réimplémente aucune validation.
---
## ③ Pourquoi c'est transférable
| Set-OPS | Équivalents ailleurs |
|---|---|
| `make prouver` | tests automatisés, **CI/CD**, `terraform validate` |
| registre d'affirmations | *traçabilité de conformité* (SOC 2, ISO) |
| pièce justificative datée | *audit trail*, preuve d'audit |
| « le registre peut perdre » | un test vert n'est utile que s'il peut virer rouge |
Tu as appris **la vérification rejouable, la preuve d'audit, la culture du test** — pas « le
harnais de Set-OPS ».
---
## ④ À toi de jouer
1. **Produis une preuve.** `make prouver` (voûte exportée). Lis
`docs/audit/preuve-<date>.md` : chaque preuve, son verdict, l'affirmation couverte.
2. **Fais échouer une preuve — exprès.** Introduis un **hôte fantôme** : dans `applications.yml`,
pointe une appli vers un hôte qui n'existe pas dans `serveurs.yml`. `make prouver` : **P06
échoue**, en nommant l'hôte. Corrige (ou via le `<select>` de la GUI) : vert.
3. **Une autre.** Remets de l'adressage dans une nomenclature (`vlan: 42`), `make prouver` :
**P20 échoue**. Retire-le : vert.
4. **Lis le registre.** Ouvre `docs/audit/affirmations.md` : trouve une affirmation ⚪
(*non prouvable localement*) — vois comment elle est **assumée comme intention**, jamais
présentée comme prouvée.
5. **Comprends la valeur.** Demande-toi : *quelle promesse est-ce que je fais sans preuve ?*
C'est exactement ce que ce registre force à regarder en face.
---
## Le défaut le plus dangereux n'est pas l'erreur, c'est la **copie**
Set-OPS pilote plusieurs écosystèmes. Avant d'agir, chaque script doit donc savoir
**lequel il regarde** — par le lien `instance`, ou par la variable `SETOPS_INSTANCE`.
En août 2026, **neuf scripts avaient chacun écrit leur propre réponse** à cette question.
Trois lignes chacun. Aucune n'était fausse en soi.
Le problème n'est pas l'erreur : c'est que **neuf copies ne vieillissent pas ensemble**.
Quand on améliore l'une, les huit autres ne le savent pas. Et personne ne peut le voir,
parce que de l'intérieur d'un fichier, la copie locale a toujours l'air correcte.
### Ce que ça donnait
`make placement-plan` visait un autre tenant et répondait :
```
Devis du placement — tenant « instance »
noeud asgard · stockage TrueNAS · gabarit 99998 → CONFORME
```
C'était vrai — **sur l'autre écosystème**. Sa copie lisait le lien au lieu de la variable.
Comme les deux tenants portaient les mêmes valeurs de placement, le verdict semblait
juste. C'est très exactement la circonstance où une erreur ne se voit pas.
Cinq défauts de cette famille sont sortis en cinq jours. Tous dans des outils qui
**constatent** — preuves et devis — jamais dans ceux qui agissent. C'est moins grave et
plus insidieux : un outil qui agit mal, on le voit ; un outil qui mesure mal dit
« conforme », et on passe à la suite.
### La réponse
Une **source unique** : une fonction, dans un fichier, que tous appellent. Si elle est
fausse, elle l'est partout d'un coup — donc visible, donc corrigée une fois.
Et une preuve, **P41**, qui refuse la prochaine copie. Elle en a trouvé une dixième le
jour de son écriture, dans le fichier des preuves lui-même.
> **C'est la même leçon que `proxmox-hebergeur.yml`** : les nœuds et stockages du cluster
> recopiés chez chaque tenant avaient divergé. Une source, pas N copies — pour les données
> comme pour le code.
---
## Pour aller plus loin *(dépôt)*
- Le mode d'emploi : `docs/audit/README.md`.
- Le registre : `docs/audit/affirmations.md` ; le harnais : `scripts/prouver.py`.
- L'épreuve humaine (« exploitable sans IA ») : `docs/audit/protocole-operateur-independant.md`.