Note d’étude — un trait de backend std::sys : proposition d’RFC à la Rust Teams libs

Statut : note d’étude, NON normative — matière à discussion pré-RFC. Explore un mécanisme à proposer en amont à l’équipe Rust libs : formaliser la frontière per-OS de std::sys (imp) en un trait de backend OS-neutre, sur lequel std s’appuie pour sa couche hors-plateforme, et qu’un provider (Air, mais aussi tout futur OS userland Rust) implémente. Prolonge la note etude-std-pal-air-safe-fr.md et la décision ADR-088. Rien n’engage encore le code ; l’RFC amont ne serait déposé qu’après la preuve downstream (jalon hello-std sur PAL safe).

Ancrage empirique : la frontière du trait n’est pas théorique — c’est exactement la liste des « murs durs » (A1–A4) + le Tier B relevés par la reconnaissance de l’incrément 0 du chantier PAL (voir rt/DECISIONS.md, ADR-088). L’implémentation réelle du backend air est la preuve d’existence qui sous-tend cette proposition.

1. Le problème, vu des deux côtés

Côté équipe libs. std::sys a été profondément réusiné (chantier amont « FIXME(117276) ») pour séparer une couche générique réutilisable (read_dir, copy, each_addr, les impls sync/*/futex.rs…) d’un noyau per-OS imp sélectionné par cfg_select!. Cette frontière imp existe déjà et est curée — mais le contrat qu’elle impose est implicite : il n’est défini que par « est-ce que std compile pour cet OS ? ». Ajouter/mainteneur un OS = éditer le cfg_select! de ~15 fichiers sys/<domaine>/mod.rs, sans filet de type.

Côté provider (Air). Pour brancher un backend, il faut forker rust-src et insérer un bras target_os="air" dans chacun de ces ~15 dispatchs — puis rebaser ce fork à chaque nightly. C’est précisément la dette que le chantier PAL subit aujourd’hui (ADR-088, §Réversibilité).

Thèse de la note. La frontière imp — déjà tracée par l’équipe — gagnerait à être cristallisée en trait. Pas un rewrite : une formalisation de l’existant, qui (a) documente et fait vérifier par le compilateur le contrat, (b) réduit le point d’ajout d’un backend de 15 dispatchs à 1 sélection, et (c) ouvre la voie à un backend hors-arbre.

2. Ce qu’un trait apporte — et ce qu’il n’apporte PAS

Il n’apporte PAS de polymorphisme à l’exécution, et c’est voulu : un binaire = un OS = un backend, figé à la compilation. Le trait n’est pas un dyn runtime ; c’est un contrat statique. Sa valeur est triple :

1. Contrat explicite, checké. impl Platform for Air échoue à la compilation si une opération manque ou a la mauvaise signature — au lieu d’une erreur cfg_select! obscure à l’autre bout de l’arbre.
2. Point d’extension sanctionné. Un backend = une impl, pas 15 patchs de dispatch.
3. (Horizon) backend hors-arbre. Le provider implémente le trait dans sa propre crate (pour Air : les Managers couche 1), sans forker std.

3. Décision de conception n°1 — un trait OS-neutre, PAS unix-*

Tentation naturelle (et à écarter) : nommer les traits UnixThread, UnixProcess, ou LinuxThread… unix n’est pas un OS, c’est une famille qui présuppose *libc + errno in-band

• sémantique POSIX*. Air est Linux (le kernel est la bible) mais hors unix-family (pas de libc, safe) — un trait UnixThread traînerait l’hypothèse libc et réintroduirait le problème même qu’Air résout.

⇒ Traits neutres : PlatformThread, PlatformFs… dont unix est un implémenteur parmi d’autres (windows, hermit, air…). « unix » redevient une impl concrète, pas un contrat.

Nuance offrable à l’équipe : une crate d’aide unix-common peut fournir des impl partagées du trait neutre pour les backends libc — au-dessus du contrat, jamais en le définissant. La factorisation unix reste possible sans contaminer l’abstraction.

4. Décision de conception n°2 — plusieurs petits traits, agrégés par un supertrait

Un Platform monolithique serait ingérable et empêcherait la réutilisation. Mieux : un trait par sous-système (ce sont exactement les frontières que la reconnaissance a listées), composés par un supertrait à types associés :

#![allow(unused)]
fn main() {
// std::sys::platform  (esquisse)
pub trait Platform: 'static {
    const NAME: &'static str;

    // Types concrets fournis par le backend (portés par des sous-traits) :
    type Fs:      PlatformFs;
    type Net:     PlatformNet;
    type Thread:  PlatformThread;
    type Sync:    PlatformSync;    // le futex : débloque Mutex/Condvar/RwLock/Once/Parker
    type Alloc:   PlatformAlloc;
    type Process: PlatformProcess;
    type Stdio:   PlatformStdio;

    // Opérations transverses :
    unsafe fn init(argc: isize, argv: *const *const u8, sigpipe: u8);
    unsafe fn cleanup();
    fn abort_internal() -> !;
    fn exit(code: i32) -> !;                                    // évite le repli abort()
    fn getrandom(buf: &mut [u8]) -> io::Result<()>;            // A3
    fn decode_error_kind(errno: RawOsError) -> io::ErrorKind;  // A2
    fn error_string(errno: RawOsError) -> String;             // A2
}

/// La primitive qui, seule, débloque TOUTE la synchro générique de std.
pub trait PlatformSync {
    type Futex;   // typiquement AtomicU32
    fn futex_wait(f: &Self::Futex, expected: u32, timeout: Option<Duration>) -> bool;
    fn futex_wake(f: &Self::Futex) -> bool;
    fn futex_wake_all(f: &Self::Futex);
    // Mutex / Condvar / RwLock / Once / Parker restent GÉNÉRIQUES au-dessus (sync/*/futex.rs).
}

pub trait PlatformAlloc {                                       // A1
    fn alloc(layout: Layout) -> *mut u8;
    unsafe fn dealloc(ptr: *mut u8, layout: Layout);
    unsafe fn realloc(ptr: *mut u8, layout: Layout, new_size: usize) -> *mut u8;
    fn alloc_zeroed(layout: Layout) -> *mut u8;
}

pub trait PlatformFs {
    type File;
    type ReadDir;
    type DirEntry;
    fn open(path: &Path, opts: &OpenOptions) -> io::Result<Self::File>;
    fn read(f: &Self::File, buf: &mut [u8]) -> io::Result<usize>;
    fn write(f: &Self::File, buf: &[u8]) -> io::Result<usize>;
    fn read_dir(path: &Path) -> io::Result<Self::ReadDir>;
    // … (la couche générique read_to_end/copy/canonicalize reste au-dessus)
}
}

Composabilité — le gain décisif. Un backend qui ne fournit pas un sous-système réutilise l’impl Unsupported existante, typée : type Process = unsupported::Process;. C’est le mécanisme unsupported d’aujourd’hui, mais vérifié — un unikernel sans processus reste légal, et le compilateur le sait. Symétriquement, la couche générique de std ne bouge pas : on ne trace le trait qu’à la frontière imp déjà curée. C’est une cristallisation d’une frontière existante, pas une révolution — l’argument-clé d’acceptabilité.

5. Cartographie sous-système → trait → (côté Air) Manager couche 1

Empruntée à la reconnaissance de l’incrément 0 — chaque bras imp de std a son trait candidat et, pour Air, son Manager couche 1 fournisseur (preuve que le contrat est réalisable safe) :

6. Les deux vrais obstacles (honnêteté d’ingénierie)

a. Le churn des sites d’appel. std référence des types concrets (sys::fs::File), pas <P as Platform>::Fs::File. Threader des types associés dans tout std = gros diff, et l’équipe libs sort épuisée de 117276. Mitigation : conserver les façades type-alias actuelles, résolues par une seule sélection au lieu de 15 :

#![allow(unused)]
fn main() {
cfg_select! {
    target_os = "air"      => { use air_backend::Air  as SelectedSys; }
    target_family = "unix" => { use self::unix::Unix   as SelectedSys; }
    target_os = "windows"  => { use self::windows::Win as SelectedSys; }
    // …
}
pub type Sys  = SelectedSys;                          // LE point de sélection unique
pub type File = <Sys as Platform>::Fs::File;          // façades côté std inchangées
}

⇒ zéro churn aux appelants ; on remplace N dispatchs éparpillés par 1. Introductible sous-système par sous-système, incrémentalement — pas un big-bang.

b. La sélection : in-tree vs hors-arbre. Le trait seul ne dit pas quel type est Sys. Deux niveaux, découplables :

• In-tree (modeste, fort taux d’acceptation) : le cfg_select! choisit Sys. Un provider patche alors une seule ligne au lieu de 15 fichiers. Gain déjà majeur, sans nouvelle machinerie.
• Hors-arbre (l’ambition, la vraie contribution) : un slot de backend résolu par cargo —

  cargo +nightly build -Z build-std -Z build-std-platform=air_std_backend
  

  où air_std_backend est une crate normale exportant impl Platform for Air. Plus aucun fork rust-src. Dépend de la maturation de -Z build-std (encore unstable) ⇒ à proposer comme horizon, pas comme préalable.

7. L’angle différenciant d’Air : le premier backend safe — et il nettoie std

Tous les backends existants bindent une frontière unsafe : unix→libc C-ABI, hermit→ hermit_abi (extern "C"), xous→asm!("ecall"), uefi→r-efi. Air serait le premier dont l’unsafe vit entièrement chez le provider, tout en bas (couche 0, la barrière kernel), le reste du backend étant du Rust safe.

Conséquence concrète pour le trait : ses signatures peuvent être safe — io::Result<T> plutôt qu’errno in-band, pas de *mut exposé là où un &[u8]/OwnedFd suffit. Ce n’est pas qu’esthétique : un contrat exprimé en signatures safe est plus propre pour l’équipe libs elle-même (le type dit ce qui échoue). L’argument de tête de l’RFC n’est donc pas « rendez le non-libc possible » (hermit le prouve déjà) mais : « un point d’extension qui, en prime, permet des backends sans unsafe à la frontière — Air comme preuve d’existence. » Mais un membre du libs team répondra, à juste titre : « qu’est-ce qui me garantit que ce backend est safe ? » — c’est l’objet du §7bis.

7bis. Comment le compilateur vérifie la promesse safe (et où est la limite)

Question du sceptique libs : « une plateforme promet un backend safe — qu’est-ce qui me garantit que c’est vrai, et le compilateur peut-il le vérifier ? » Réponse rigoureuse.

a. « Safe backend » recouvre TROIS claims distincts

1. Signatures safe — les méthodes du trait sont des fn (pas unsafe fn), échangeant des types safe (&[u8], io::Result<T>, OwnedFd), jamais *mut/errno in-band. → trivialement vérifiable : c’est la définition du trait.
2. Corps sans unsafe — l’impl du provider est du Rust safe. → la vraie question, la dure.
3. Respect des invariants dont std dépend (fd valide, pointeur d’alloc conforme au layout…). → sémantique, indécidable (Rice) : aucun compilateur ne la prouve gratis.

b. Deux impossibilités à assumer (sinon l’RFC ment)

• « Zéro unsafe dans tout le graphe » est impossible. Au fond, quelqu’un parle au kernel (syscall = asm/FFI) : la frontière kernel est unsafe par nature. La promesse crédible n’est pas « pas d’unsafe » mais « unsafe confiné, minimal, déclaré ; tout ce qui est au-dessus est vérifié safe » (doctrine Air : unsafe en couche 0 uniquement).
• Le compilateur ne prouvera jamais la correction sémantique de la frontière unsafe. Un allocateur qui ment reste du code qui compile.

c. Ce que le compilateur GARANTIT — la forme (et c’est beaucoup)

c.1 — unsafe trait + unsafe impl = énumération FORCÉE des points de confiance. Les sous-traits dont std dépend pour sa propre soundness (alloc en tête) sont des unsafe trait. On ne peut pas écrire un impl safe d’un unsafe trait : le compilateur exige le mot-clé.

#![allow(unused)]
fn main() {
pub unsafe trait PlatformAlloc {        // std : "je dépends de ta correction pour MA soundness"
    fn alloc(layout: Layout) -> *mut u8;
    // …
}
unsafe impl PlatformAlloc for Air {     // <- token OBLIGATOIRE, greppable : une assertion visible
    // SAFETY: délègue à air-alloc (couche 1) → mmap couche 0 ; layout respecté ; cf. tests …
}
}

⇒ le libs team obtient la liste exhaustive, vérifiée compilateur, de chaque endroit où le backend assure un invariant unsafe. count(unsafe impl) + count(unsafe fn) = la surface de confiance. Rien d’autre ne peut cacher d’unsafe compromettant std.

c.2 — signatures safe ⇒ un backend buggé produit des erreurs de logique, pas de l’UB. Un getrandom(&mut [u8]) -> io::Result<()> safe : un backend qui rend des octets non-aléatoires est insécure mais pas UB — il ne corrompt pas la mémoire de std. Un open rendant un OwnedFd bidon : type RAII valide, les I/O rendent Err, pas d’UB. Le danger n’existe que là où std s’appuie sur un invariant unsafe : alloc, TLS, from_raw_fd, spawn/join (soundness de thread::scope), init. Ces cas — et eux seuls — restent unsafe trait/unsafe fn. La conception du trait doit donc minimiser et expliciter cette poignée : les marqueurs unsafe du trait documentent exactement où repose la promesse de sûreté de la cible.

c.3 — #![deny(unsafe_code)] + îlot #[allow] localisé ⇒ le compilateur prouve « aucun unsafe hors frontière déclarée ». Le lint unsafe_code attrape blocs unsafe, unsafe fn, unsafe impl/unsafe trait, et même #[no_mangle]/#[export_name] (donc la FFI).

#![allow(unused)]
#![deny(unsafe_code)]                    // deny (pas forbid) : surchargeable localement
fn main() {
mod boundary {
    #![allow(unsafe_code)]               // LE seul îlot autorisé — auditable d'un grep
    unsafe impl PlatformAlloc for Air { /* SAFETY: … */ }
    unsafe impl PlatformTls   for Air { /* SAFETY: … */ }
    // … la poignée irréductible, chacune justifiée, chacune déléguant à la couche 0
}
// tout le reste de l'adaptateur : compilé-vérifié 100 % safe
}

(forbid(unsafe_code) interdirait aussi l’îlot — réservé aux crates à zéro unsafe. Pour la frontière localisée : deny + allow ciblé.)

d. La réponse au sceptique : pas une preuve, une réduction

Le compilateur transforme une confiance non-bornée (« ce backend entier est-il safe ? ») en un audit borné (« ces N assertions unsafe — déclarées, localisées, justifiées — sont-elles correctes ? »), et vérifie mécaniquement tout le reste. C’est exactement le contrat que std offre déjà à ses utilisateurs. L’angle Air : rendre N minimal et le pousser en couche 0. Le libs team peut alors exiger et mesurer, pas croire :

• surface unsafe quantifiée : grep 'unsafe impl' = la liste ; cargo-geiger = le compte du graphe ;
• CI du mainteneur Tier-3 imposant deny(unsafe_code) hors mod boundary ;
• dossier de preuve de la frontière : Miri sur la logique pure, Kani/Prusti (vérif formelle) sur les blocs unsafe, fuzz + 100 % coverage + property tests (déjà la doctrine Air) comme évidence de correction.

e. Le vrai gap — et la contribution d’RFC honnête

Aujourd’hui std/rustc ne peuvent pas imposer deny(unsafe_code) à une crate de backend arbitraire (les lints sont un choix de l’auteur de crate), ni prouver « l’unsafe de mon graphe ne vient que de la crate X (couche 0) ». C’est un manque réel du langage (conversation « unsafe dans le graphe / capabilities de crate », sans mécanisme abouti). ⇒ la demande différenciante à porter au libs team n’est pas « rendez le non-libc possible » mais : « donnez un moyen qu’une cible déclare — et que le compilateur/cargo vérifie — que sa surface unsafe est confinée à une frontière allowlistée et minimale. » Air serait la preuve d’existence : un backend dont l’unsafe est N assertions en mod boundary, toutes déléguant à une couche 0 auditée.

Synthèse §7bis : le compilateur ne prouve pas la sûreté — il garantit la forme (safe partout sauf N points déclarés unsafe) et réduit la confiance à un audit fini. Air s’engage à minimiser N, à le confiner en couche 0, et à l’outiller (Miri/Kani/fuzz). Le mécanisme de langage manquant (confinement d’unsafe vérifié) est la contribution d’RFC.

8. Précédents à citer (crédibilité)

• FIXME(117276) — la frontière générique/imp existe et est curée : l’RFC la nomme, ne l’invente pas.
• #[global_allocator] / #[panic_handler] — précédents d’implémentation fournie de l’extérieur que std/core consomment.
• hermit_abi — std tolère déjà un backend externe (via C-ABI) : la version trait Rust safe en est l’évolution naturelle, pas une rupture.
• WG build-std / std-aware cargo — le véhicule de l’étage 2 (backend hors-arbre).
• restricted_std — précédent de std partiel/gaté pour cibles non-standard.

9. Forme d’RFC recommandée — deux étages découplés

• Étage 1 — « Formaliser la frontière imp en trait Platform OS-neutre ». Landable seul, faible risque : réduit la charge de maintenance amont, self-documenté, vérifié par le compilateur, sélection unique. Bénéfice immédiat pour l’équipe et les providers in-tree. Introduction incrémentale (un sous-système à la fois), façades préservées.
• Étage 2 — « Backend std::sys hors-arbre via -Z build-std-platform ». L’horizon qui débloque Air et tout futur OS userland Rust, couplé à la stabilisation de build-std.

Séquencement côté Air : on prouve d’abord downstream (fork rust-src patché, jalon hello-std sur PAL safe 2 arches — ADR-088), puis on dépose l’RFC avec l’implémentation air en preuve d’existence. L’upstreaming Tier-3 de *-linux-air (ADR-050) est le véhicule qui rend les bras air légitimes en amont.

10. Questions ouvertes (à instruire avant l’RFC)

1. Types associés vs types génériques : Platform à types associés (un backend figé par cible) suffit-il, ou faut-il paramétrer certains sous-systèmes ? (Réponse pressentie : types associés — pas de polymorphisme runtime voulu.)
2. Consts/statics : certaines frontières exposent des constantes (MIN_ALIGN, tables d’erreurs). Les consts associées couvrent-elles tout, ou reste-t-il des items non exprimables en trait ?
3. Lang items entremêlés (alloc error handler, panic) : quels bras restent hors du trait parce que liés à des lang items, et faut-il les traiter à part ?
4. unsafe du trait : quelles méthodes restent unsafe par nécessité (init, dealloc) vs celles qu’on peut rendre safe ? Cartographier le minimum irréductible.
5. Granularité exacte : combien de sous-traits ? (Trop = cérémonie ; trop peu = perte de la composabilité unsupported.) La liste §5 est le point de départ.
6. Stabilité / semver : le trait est-il #[unstable] interne à jamais (contrat de compilation), ou expose-t-on une surface stable aux providers Tier-3 ?

11. Conclusion

L’intuition est juste : std gagnerait un trait de backend, à trois conditions non négociables — (1) neutre, jamais unix-* (sinon on rebranche l’hypothèse libc qu’Air casse) ; (2) vendu comme cristallisation de la frontière imp existante, incrémentale et à façades préservées (pas un rewrite) ; (3) porté par l’argument différenciant du backend safe — Air en preuve d’existence, l’unsafe confiné chez le provider (couche 0), et un contrat plus propre en prime pour l’équipe libs. L’étage 1 (trait in-tree) est déposable seul ; l’étage 2 (backend hors-arbre) suit la maturation de build-std. On avance downstream, on prouve, puis on propose.