Spécification binaire Rul (.rl) v0.4 — ISA 128 bits & vérificateur O(N)
Spécification officielle du format binaire Rul (.rl) v0.4 : RulHeader de 64 octets, ArenaDescriptor de 16 octets, ProofEntry de 16 octets, NodeFrame de 128 bits sur 29 opcodes et vérification linéaire O(N).
[0x01] CORE EQUATION
Artifact (.rl) = Algorithm + Schedule + Proof
Chaque programme Rul exécutable est une image binaire plate .rl alignée sur des frontières de 16 et 64 octets pour une projection directe en mémoire sans copie (mmap). Le moteur d'exécution ne contient aucun analyseur lexical ou syntaxique (AST) textuel.
1. Priorité au binaire
Conversion bidirectionnelle sans perte .rls <-> .rl en ~8,8 µs à la frontière via src/transpiler.rs.
2. SSA-DAG topologique
Chaque nœud d'instruction i ne peut référencer que des opérandes strictement < i, garantissant la terminaison.
3. Séparation Sécurité & Intention
La couche 1 prouve la sécurité mémoire/bornes en 5,78 ns/nœud ; la couche 2 vérifie AssertContract & rul trace.
[0x02] SECTION 1 OF .RL
RulHeader (64 octets, aligné sur ligne de cache)
| OFFSET OCTET | CHAMP | TYPE | DESCRIPTION |
|---|---|---|---|
| 0..8 | magic | [u8; 8] | Signature magique canonique : b"RUL\x00\x01\x00\x00\x00" |
| 8..16 | graph_hash | u64 | Hachage d'intégrité FNV-1a 64 bits sur les sections Arena, Proof et Node |
| 16..24 | capability_mask | u64 | Masque de bac à sable matériel E/S (0x00 = Calcul pur, 0x01 = NetRing, 0x02 = StorageDMA, 0x04 = GpuDispatch) |
| 24..28 | arena_count | u32 | Nombre d'entrées ArenaDescriptor de 16 octets |
| 28..32 | proof_count | u32 | Nombre de certificats de bornes ProofEntry de 16 octets |
| 32..36 | node_count | u32 | Nombre d'instructions NodeFrame de 128 bits (16 octets) |
| 36..40 | output_node | u32 | Index (base 0) du nœud SSA de sortie principal |
| 40..64 | reserved | [u8; 24] | Remplissage de zéros alignant l'en-tête sur une ligne de cache CPU de 64 octets |
[0x03] SECTIONS 2 & 3 OF .RL
ArenaDescriptor (16 octets) & ProofEntry (16 octets)
| OFFSET OCTET | ArenaDescriptor | TYPE | DESCRIPTION |
|---|---|---|---|
| 0..4 | arena_id | u32 | Identifiant d'arène colonnaire (0 .. arena_count - 1) |
| 4..8 | element_count | u32 | Longueur de la colonne homogène (Longueur Shape) |
| 8 | type_lane | u8 | Type d'élément & largeur de voie SIMD (ex. 0x18 = f64x8) |
| 9 | mutability | u8 | 0 = Entrée immuable | 1 = Région mutable linéaire |
| 10..12 | alignment | u16 | Exigence d'alignement en octets (64 octets pour AVX-512 / ligne de cache) |
| 12..16 | initial_version | u32 | Version initiale d'AffineToken (commence à 1) |
| OFFSET OCTET | ProofEntry | TYPE | DESCRIPTION |
|---|---|---|---|
| 0..2 | rule_kind | u16 | 1 = SliceBounds (lo <= hi <= len) | 2 = GatherIndexInBounds (max_idx <= target_len) |
| 2..4 | target_arena | u16 | ID de l'arène cible strictement lié à l'origin_arena de l'opérande |
| 4..8 | bound_lo | u32 | Borne d'index inférieure non négative |
| 8..12 | bound_hi | u32 | Borne supérieure <= effective_target_len |
| 12..16 | witness_node | u32 | Nœud d'index SSA témoin (in_b pour Gather) |
[0x04] SECTION 4 OF .RL
Disposition de la trame NodeFrame 128 bits (16 octets)
Voie Algorithme (Quoi calculer : Opcode / Opérandes) Voie Ordonnancement (Comment exécuter : SIMD / Multi-cœur) Voie Preuve (Sécurité : Ticket de version / Bornes)
NODE #3 ($n3) node $n3 = Mul f64x8 fg=1 pol=simd proof=0 tok=pure a=$n0 b=$n0
16 BYTES = 128 BITSDÉCOMPOSITION DU REGISTRE 8 BITS · BYTE 2 (b16..b23) 0x12
0 2^7
0 2^6
0 2^5
1 2^4
0 2^3
0 2^2
1 2^1
0 2^0
Champ: schedule_hint Type: u8
✓ Invariant du vérificateur O(N) contrôlé au chargement (~5.78 ns) (fusion_group << 4) | exec_policy
Octet d'ordonnancement matériel orthogonal : muter 0x11 (SimdStream) -> 0x12 (MultiCore) change l'exécution CPU sans altérer les preuves de sécurité.
Nœud #3: Élévation au carré vectorielle à 8 voies élément par élément ($n0 * $n0) fusionnée dans les registres de cache L1 sans allocation sur le tas.
[0x05] 29-OPCODE ISA (v0.4.0)
Jeu complet de 29 instructions (ISA v0.4.0)
| HEX | OPCODE | CATÉGORIE | SÉMANTIQUE | DESCRIPTION |
|---|---|---|---|---|
| 0x01 | ArenaInput | Memory & Arena | ArenaDescriptor[in_a] -> Column | Charge une tranche colonnaire depuis ArenaDescriptor[in_a] avec ReadLease. |
| 0x02 | ConstF64 | Memory & Arena | in_a | (in_b << 32) -> Scalar f64 | Constante scalaire flottante IEEE-754 64 bits immédiate. |
| 0x03 | ArenaSlice | Memory & Arena | Slice(in_a, ProofEntry[proof_idx]) -> Column | Sous-tranche sans copie de la colonne in_a certifiée par ProofEntry. |
| 0x04 | ArenaMutate | Memory & Arena | Mutate(Arena[in_a], in_b) -> ver + 1 | Mutation linéaire sur place consommant AffineToken (ver -> ver + 1). |
| 0x10 | Add | Arithmetic & Math | out[i] = a[i] + b[i] | Addition SIMD élément par élément (VADDPD). |
| 0x11 | Sub | Arithmetic & Math | out[i] = a[i] - b[i] | Soustraction SIMD élément par élément (VSUBPD). |
| 0x12 | Mul | Arithmetic & Math | out[i] = a[i] * b[i] | Multiplication SIMD élément par élément (VMULPD). |
| 0x13 | Div | Arithmetic & Math | out[i] = a[i] / b[i] | Division SIMD IEEE-754 élément par élément (VDIVPD). |
| 0x14 | CmpGt | Predicate & Mask | mask[i] = a[i] > b[i] | Masque de prédicat « supérieur à » sans branchement (VCMPPD). |
| 0x15 | SelectZero | Predicate & Mask | out[i] = mask[i] ? val[i] : 0.0 | Sélection par prédicat sans branchement mettant à zéro les voies masquées (VANDPD). |
| 0x16 | Min | Arithmetic & Math | out[i] = min(a[i], b[i]) | Minimum élément par élément sans branchement (VMINPD). |
| 0x17 | Max | Arithmetic & Math | out[i] = max(a[i], b[i]) | Maximum élément par élément sans branchement (VMAXPD). |
| 0x18 | CmpLt | Predicate & Mask | mask[i] = a[i] < b[i] | Masque de prédicat « inférieur à » sans branchement. |
| 0x19 | CmpEq | Predicate & Mask | mask[i] = a[i] == b[i] | Masque de prédicat d'égalité sans branchement. |
| 0x1A | Abs | Arithmetic & Math | out[i] = |a[i]| | Valeur absolue sans branchement par effacement du bit de signe IEEE-754. |
| 0x1B | Sqrt | Arithmetic & Math | out[i] = sqrt(a[i]) | Racine carrée matérielle SIMD (VSQRTPD). |
| 0x1C | Floor | Arithmetic & Math | out[i] = floor(a[i]) | Arrondi sans branchement vers -Infini (VROUNDPD). |
| 0x1D | Ceil | Arithmetic & Math | out[i] = ceil(a[i]) | Arrondi sans branchement vers +Infini (VROUNDPD). |
| 0x1E | Ln | Arithmetic & Math | out[i] = ln(a[i]) | Logarithme naturel élément par élément. |
| 0x1F | Exp | Arithmetic & Math | out[i] = exp(a[i]) | Exponentielle naturelle élément par élément. |
| 0x20 | FilterCompact | Reduction & Compaction | Compact(mask=in_a, vals=in_b) | Compaction de flux regroupant de façon contiguë les éléments filtrés. |
| 0x21 | ReduceSum | Reduction & Compaction | sum(in_a) -> Scalar f64 | Réduction horizontale de somme à 8 accumulateurs vers un scalaire. |
| 0x22 | ReduceMax | Reduction & Compaction | max(in_a) -> Scalar f64 | Réduction horizontale du maximum vers un scalaire. |
| 0x23 | Gather | Reduction & Compaction | target[indices[i]] (proof_idx > 0) | Collecte indexée indirecte certifiée par ProofEntry. |
| 0x24 | ReduceMin | Reduction & Compaction | min(in_a) -> Scalar f64 | Réduction horizontale du minimum vers un scalaire. |
| 0x25 | MaskAnd | Predicate & Mask | mask[i] = a[i] && b[i] | Conjonction bit à bit de masques booléens (ET). |
| 0x26 | MaskOr | Predicate & Mask | mask[i] = a[i] || b[i] | Disjonction bit à bit de masques booléens (OU). |
| 0x30 | RingEnqueue | Hardware & Contract | Enqueue(in_a) [Requires CAP_NET_RING] | Sortie vers tampon circulaire matériel contrôlée par capacité (CAP_NET_RING). |
| 0x40 | AssertContract | Hardware & Contract | Assert(!is_nan(in_a) && is_finite(in_a)) | Contrat de domaine à l'exécution vérifiant une sortie finie et non-NaN. |
[0x06] STATIC VERIFICATION (~5.78 NS/NODE)
Quatre règles de vérification linéaire O(N) en une seule passe
1. Règle SSA topologique
Chaque nœud à l'index i doit satisfaire in_a < i et in_b < i, empêchant mathématiquement tout cycle.
2. Conservation linéaire de la propriété mémoire
ReadLease(a, ver) vérifie live_version[a] == ver. AffineConsume(a, ver) vérifie la mutabilité et incrémente live_version[a] via checked_add(1).
3. Preuve de bornes liée à l'origine
ArenaSlice et Gather vérifient ProofEntry.target_arena == origin_arena et bound_lo <= bound_hi <= effective_target_len.
4. CapabilityMask zéro confiance
Les opcodes d'E/S matérielles (0x30 RingEnqueue) exigent le bit correspondant dans RulHeader.capability_mask sous peine de rejet avant exécution.