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

graph LR
    DBN[".dbn.zst<br/>databento MBP-10"] --> ADAPTER[salim-dbn-adapter]
    ADAPTER --> PIPELINE[salim-pipeline]
    PIPELINE --> CORE[salim-core<br/>RV, BV, J,<br/>classifier]
    CORE --> EXPORT[salim-export<br/>Parquet schema V1]
    EXPORT --> PARQUET[".parquet<br/>WindowVerdict rows"]
    PARQUET --> PYTHON[Python plots<br/>research/plots/]

Lecture de gauche à droite : un fichier compressé en entrée, une rangée typée en sortie. Aucune boucle, aucun retour en arrière, aucun écrivain vers le disque source. Le 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 : panel 5 personas \(\times\) 4 topics (réduit pour rester model-checkable, les 3 autres couverts par monotonie). Invariants : coverage des topics \((\geq\) 2 personas indépendantes par topic), panel non-vide, terminal cohérent. C'est la spec qui a fait passer la délibération delib-20260513-54ed de « panel d'opinions » à « panel vérifié ».

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

Pour Salim : si tu utilises un signal en prod, tu veux savoir (a) que le pipeline ne deadlock pas (TLA+), (b) que les invariants algébriques tiennent (property-tests), et (c) que les nombres ne dérivent pas silencieusement entre deux versions (commit hash dans chaque Parquet row). C'est exactement ce qu'on a câblé.

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 actuellement. À considérer V2 si le pipeline scale au-delà de XNAS / 2 instruments. Pour V1 (pré-étude empirique), le coût/bénéfice ne le justifie pas.
Bornes numériques. Sur N = 60 ticks, l'erreur relative sur RV_short est ~18% (Andersen et al. 2003, cf. 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 la stack évolue sans que cette page suive. Antidote V1 : commit_hash dans le frontmatter (51b89624c625). Antidote V2 (advisory, knuth) : INV-DRIFT-DETECTION — hook de pré-release qui regénère les pages-pilier si un crate salim-* a été touché.

Voir aussi : realized-variance \(\cdot\) bipower-and-jumps \(\cdot\) regime-classifier \(\cdot\) pivot-j-based \(\cdot\) cases-index \(\cdot\) charter