Comment je peux faire confiance aux nombres ?
Quatre crates Rust, une spec TLA+ vérifiée par TLC, quatre property tests gate avant chaque release.
Cette page ne dit pas « ces nombres sont vrais ». Elle dit ce qui aurait dû casser avant qu'un nombre sorte du pipeline. La différence est tout.
Pipeline — d'un .dbn.zst à une rangée de Parquet
Lecture de gauche à droite : un fichier compressé en entrée, une rangée
typée en sortie. La flèche pleine = le flot de données. Le trait pointillé
de salim-core vers salim-pipeline = une dépendance de bibliothèque :
pipeline appelle les fonctions de core (RV, BV, J, classifier) pour
chaque fenêtre, core ne reçoit pas le flot ni ne le réémet. Aucune boucle,
aucun retour en arrière, aucun écrivain vers le disque source. La
frontière \(Rust → Python\) est posée au Parquet — pas de Python dans le
hot path (ADR-0002 §D-1).
Les quatre crates
Chaque coupure passe deux signaux de la règle D-1
(ADR-0002 §D-1) : cycle
de versionnement disjoint, surface de dépendances disjointe, frontière de
confiance, ou public consumer attendu. Le salim-cli n'est pas un crate
mais le binaire qui les assemble.
| Crate | Responsabilité | Path |
|---|---|---|
salim-core | Stats RV/BV/J, classifier state machine, types domain | research/crates/salim-core/ |
salim-dbn-adapter | Décodage DBN \(\to\) domain types (frontière read-only) | research/crates/salim-dbn-adapter/ |
salim-pipeline | Worker tick \(\to\) WindowVerdict, orchestration | research/crates/salim-pipeline/ |
salim-export | Schéma Parquet V1, writer atomique | research/crates/salim-export/ |
+ salim-cli (binary) | Entry-point CLI, parse flags, lance pipeline | research/bins/salim-cli/ |
Le découpage n'est pas une élégance — c'est un test compile-time.
salim-dbn-adapter ne peut pas accidentellement écrire dans le domain :
il ne dépend pas de parquet. salim-core ne peut pas accidentellement
lire un .dbn.zst : il ne dépend pas de dbn. Le typeur Rust applique
la frontière à chaque cargo build.
Validation TLA+ — avant de lancer 11M ticks de calcul
TLA+ n'est pas une preuve que l'algo est juste. C'est une preuve que le graphe d'exécution est terminal et sans deadlock. Sur cette pré-étude on a deux specs model-checkées par TLC.
Spec DAG du pipeline — specs/MCSalimPipelineDAG.tla. Modèle :
1 jour \(\times\) 2 instruments (ARM, IONQ, symétrie permutation) \(\times\) 3 timestamps,
avec 1 tick d'auction. Invariants vérifiés : ordre des étapes
(\(LoadDbn → ComputeStat → Classify → ExportRow → Done\)), pas de skip,
pas de cycle, INV_RO_COSMONDATA (aucun write vers le disque source).
La spec adverse MCSalimPipelineDAGAttack.tla injecte volontairement
une action AttemptWriteCosmonData pour vérifier que la spec elle-même
détecte la violation — un test de la spec, pas du code.
Spec flotte de design — specs/MCDesignFleet.tla. Modèle réduit
pour rester model-checkable : un petit nombre de critiques croisent un
petit nombre de sujets ; les configurations plus grandes sont couvertes
par monotonie (si la spec tient sur le petit panel, l'argument
combinatoire dit qu'elle tient sur les panels plus larges). Invariants :
coverage des sujets (au moins deux critiques indépendantes par sujet),
panel non-vide, terminal cohérent. Sans cette spec, une « délibération »
serait un panel d'opinions ; avec elle, c'est un panel dont on a
vérifié qu'aucune voix ne peut être omise ni doublée silencieusement.
Pourquoi TLA+ avant 11M ticks — un deadlock découvert après 8 heures de calcul coûte 8 heures de calcul. TLC découvre le même deadlock en quelques secondes sur un modèle borné. Une fois la spec verte, on lance.
Gates property-tests — quatre invariants algébriques
Une PR qui casse l'un des quatre est bloquée. Ces tests tournent avant chaque release (ADR-0003 §5).
| Property | Ce qu'elle teste | Référence |
|---|---|---|
prop_rv_positive | \(RV(t,τ) ≥ 0\) pour returns iid (Brownien) | ADR-0003 §5 |
prop_bv_le_rv_no_jump | \(BV ≤ RV\) quand pas de saut injecté | idem |
prop_j_in_unit_interval | \(J ∈ [-ε, 1]\) à fenêtre finie | idem |
prop_classifier_monotonic_dwell | dwell strict croissant tant qu'aucune transition | idem |
Ces 4 tests tournent avant chaque release. Une PR qui casse l'un des quatre est bloquée.
Ce ne sont pas des tests unitaires. Ce sont des propriétés algébriques : elles posent une relation que le calcul doit respecter pour toute entrée valide, et le framework cherche des contre-exemples. Si \(BV ≤ RV\) n'est pas tenu sur 10 000 trajectoires sans saut, ce n'est pas ce test qui a échoué — c'est l'algorithme. À ce moment-là on ne recompile pas le test, on revient au code.
Données — read-only sur le disque source
Les .dbn.zst vivent sur /Volumes/CosmonData/MaQI-Data/databento/. Le
code ne les écrit jamais, ne les déplace jamais, ne les renomme jamais.
La frontière est testée à la fois par le découpage en crates
(salim-dbn-adapter n'a pas de writer) et par la spec TLA+ adverse
(INV_RO_COSMONDATA). Les Parquet dérivés sont gitignored sous
research/.cache/ ; les figures dérivées sous research/plots/out/.
C'est l'invariant DNA D3 de la galaxie, et il est appliqué à trois
niveaux : architecture (crates), preuve formelle (TLC), discipline
opérationnelle (gitignore).
Pour ton cas
Quand tu lis un nombre sorti d'ici, trois questions valent d'être posées : (a) est-ce que le graphe a bien tourné jusqu'au bout (pas de deadlock — c'est la spec TLA+ qui répond), (b) est-ce que les invariants algébriques tiennent encore (property-tests qui ont gate la release), (c) quelle version du code a produit ce nombre — pour pouvoir y revenir (commit hash dans chaque rangée Parquet). Les trois sont câblés dans la stack.
Le hash de commit dans le frontmatter de cette page (51b89624c625) est
le même format que celui inscrit dans la métadonnée de chaque rangée
Parquet exportée. Une figure regénérée six mois plus tard se relie à un
état exact du code — pas à « mai 2026 ».
Limites
- Le model-check TLA+ couvre le DAG, pas l'algo. Un bug dans
stats.rs(mauvaise formule de bipower, mauvais facteur \(π/2\)) ne sera pas détecté par TLC. C'est précisément le travail des property tests — d'où le découplage des deux gates. - Les property tests sont random-input. Un bug à entrée
spécifique (NaN dans une fenêtre boundary, tick à
ts_ns = 0) peut survivre 10 000 tirages aléatoires. Mitigation actuelle : seed fixe reproductible + smoke runs sur jours réels — l'exemple AMC est documenté dans pivot-j-based. - Pas de fuzzing. Pas fait. À reconsidérer si XNAS scale au-delà de 2 instruments.
- Bornes numériques. Sur
N = 60ticks, l'erreur relative surRV_shortest ~18% — c'est \(√(2/N) = √(2/60) ≈ 0.1826\) (l'écart-type asymptotique normalisé de l'estimateur RV sous Brownien iid, Andersen, Bollerslev, Diebold & Labys 2003, Econometrica 71(2), p. 587, éq. (7) ; voir aussi ADR-0003). Ce n'est pas un bug, c'est la statistique du finite-sample — et c'est rendu visible par les bandes de confiance dans realized-variance.
Adversary : structural-decay — risque que le code évolue sans
que cette page suive. Antidote V1 : le commit_hash dans le frontmatter
(51b89624c625) — si le hash diverge de celui du Parquet que tu lis,
tu sais qu'il faut relire. Antidote V2 (avis, à confirmer) : ajouter
un check qui signale, quand un crate salim-* change, les pages de cette
wiki dont le hash n'a pas été mis à jour.
Voir aussi : realized-variance \(\cdot\) bipower-and-jumps \(\cdot\) regime-classifier \(\cdot\) pivot-j-based \(\cdot\) cases-index \(\cdot\) charter