Feuille de route technique Rul (.rl) — Du moteur v0.4 au langage système généraliste v1.0
Feuille de route en quatre jalons étendant Rul (.rl) d'un moteur de calcul colonnaire à 29 opcodes (v0.4) vers un langage système généraliste remplaçant Rust et Go pour les logiciels générés par l'IA (v1.0).
Pourquoi nous avons commencé par les pipelines de données (v0.1 à v0.4)
Pour prouver que le format d'instruction binaire de 16 octets fonctionne sur du vrai silicium avant d'ajouter des constructions généralistes, nous avons restreint les phases v0.1 à v0.4 aux pipelines de tableaux et vecteurs (29 opcodes) — démontrant une vérification O(N) en ~5,78 ns/nœud, une compilation ELF64 autonome en ~6,4 µs et un débit de 51,53 Go/s.
Quatre jalons vers le langage système généraliste v1.0
Cœur SSA-DAG colonnaire à 29 opcodes, traceur boîte blanche & compilateur AVX2 ELF64 AOT
Validation sur matériel réel du format d'instruction binaire de 16 octets, du vérificateur O(N) en une passe (~5,8 ns/nœud), du moteur à 3 niveaux, du serveur rul-mcp et du compilateur Linux ELF64 sans LLVM (~6,4 µs).
- 01. RulHeader de 64 octets, ArenaDescriptor de 16 octets, ProofEntry de 16 octets et NodeFrame de 16 octets sur 29 opcodes.
- 02. Assembleur symbolique bidirectionnel sans perte .rls <-> .rl, CLI autonome rul, rul-bench et serveur rul-mcp à 6 outils.
- 03. Allocateur de registres YMM par balayage linéaire (ymm2..ymm13) atteignant 51,53 Go/s (4,72x plus rapide que C) sur des tableaux de 80 Mo.
Flux de contrôle généraliste, fonctions modulaires & types de données composites
Extension du jeu d'instructions de 16 octets au-delà des tableaux numériques pour gérer scalaires, structs, enums, chaînes UTF-8, tables de hachage, branchements et boucles à terminaison prouvée.
- 01. Prise en charge native de i64, i32, u8, f32, structs à disposition fixe, unions étiquetées algébriques, chaînes UTF-8 validées et tables de hachage en arène.
- 02. SelectBranch : branchement conditionnel exigeant que les deux branches convergent vers un état de version mémoire identique (vérifié en O(1)).
- 03. RegionLoop & Call : boucles bornées avec témoins de terminaison ProofEntry et fonctions modulaires vérifiées sans inlining global.
Propriété du tas de niveau Rust & durées de vie des structs en temps O(N)
Généralisation des versions TokenOp 32 bits et des témoins ProofEntry 16 octets des tableaux plats vers les allocations de régions sur le tas et les emprunts de champs de structs.
- 01. Allocation et désallocation déterministes de régions sur le tas liées à des jetons de propriété linéaire, avec zéro GC et zéro fragmentation malloc/free.
- 02. Témoins ProofEntry pour les mutations disjointes de champs de structs et les durées de vie de sous-tranches sans copie vérifiés en O(1) par instruction.
- 03. Protection complète contre use-after-free, double-free et aliasing sans résolution de contraintes Borrow Checker prenant plusieurs secondes.
Concurrence déterministe de style Go & E/S système contrôlées par CapabilityMask
Introduction de tâches légères, de canaux à transfert de propriété et de bits de capacité fins dans l'en-tête régissant les appels système fichiers, réseau et processus.
- 01. Envoyer un tampon sur un canal typé effectue un AffineConsume sur le jeton émetteur et transfère la propriété au récepteur — éliminant les courses aux données au chargement sans GC.
- 02. Extension du RulHeader.capability_mask 64 bits pour contrôler les lectures/écritures de fichiers, sockets réseau, minuteurs et sous-processus.
- 03. Un binaire .rl avec CAP_NONE (0x0) est mathématiquement bloqué de tout appel réseau ou disque avant même le début de l'exécution.
Backends natifs multi-architectures (x86_64, ARM64, WASI) & preuves formelles Kani
Génération d'exécutables autonomes pour Linux, macOS, Windows et WebAssembly sans LLVM, appuyée par la vérification de modèles Kani et une suite de conformité v1.0 de 50 programmes.
- 01. Génération de code natif zéro-LLVM pour x86_64 et AArch64 (ARM64) sur Linux, macOS et Windows, plus modules WASI déterministes.
- 02. Preuves par model-checking borné (Kani) et fuzzing différentiel continu sur le décodeur binaire, le vérificateur O(N) et le générateur natif.
- 03. Spécification binaire .rl v1.0 figée et suite publique de 50 programmes de test de conformité.
Règles d'ingénierie fondamentales (Non-objectifs)
Chaque propriété de sécurité (types, propriété, bornes, terminaison des boucles, capacités E/S) doit être vérifiable en une seule passe avant O(N).
Zéro pause GC et zéro thread d'exécution caché ; la durée de vie mémoire est suivie explicitement via des arènes et régions versionnées.
Chaque niveau d'exécution (Tier 0, Tier 1, Tier 2 et ELF64 AOT) doit produire des résultats identiques ou s'arrêter en sécurité avec une erreur déterministe.