Specifica Binaria Rul (.rl) v0.4 — ISA a 128 Bit & Verificatore O(N)
Specifica ufficiale del layout binario di Rul (.rl) v0.4: RulHeader da 64 byte, ArenaDescriptor da 16 byte, ProofEntry da 16 byte, NodeFrame a 128 bit su 29 opcode e regole di verifica O(N) a passata singola.
[0x01] CORE EQUATION
Artifact (.rl) = Algorithm + Schedule + Proof
Ogni programma Rul eseguibile è un'immagine binaria piatta .rl allineata su confini di 16 e 64 byte per la mappatura diretta in memoria zero-copy (mmap). Il motore di esecuzione principale contiene zero lexer testuali o parser AST.
1. Binario Prima di Tutto
Conversione bidirezionale senza perdite .rls <-> .rl in ~8.8 µs al confine tramite src/transpiler.rs.
2. SSA-DAG Topologico
Ogni nodo di istruzione i può fare riferimento solo a operandi strettamente < i, garantendo la terminazione.
3. Separazione Sicurezza + Intento
Il Livello 1 dimostra la sicurezza di memoria/limiti in 5.78 ns/nodo; il Livello 2 verifica AssertContract & rul trace.
[0x02] SECTION 1 OF .RL
RulHeader (64 Byte, Allineato alla Cache Line)
| OFFSET DI BYTE | CAMPO | TIPO | DESCRIZIONE |
|---|---|---|---|
| 0..8 | magic | [u8; 8] | Firma magica canonica: b"RUL\x00\x01\x00\x00\x00" |
| 8..16 | graph_hash | u64 | Hash di integrità FNV-1a a 64 bit sulle sezioni Arena, Proof e Node |
| 16..24 | capability_mask | u64 | Maschera sandbox di I/O hardware (0x00 = Puro Calcolo, 0x01 = NetRing, 0x02 = StorageDMA, 0x04 = GpuDispatch) |
| 24..28 | arena_count | u32 | Numero di voci ArenaDescriptor da 16 byte |
| 28..32 | proof_count | u32 | Numero di certificati dei limiti ProofEntry da 16 byte |
| 32..36 | node_count | u32 | Numero di istruzioni NodeFrame a 128 bit (16 byte) |
| 36..40 | output_node | u32 | Indice basato su 0 del nodo SSA di output primario |
| 40..64 | reserved | [u8; 24] | Padding riempito di zeri che allinea l'header alla cache line della CPU da 64 byte |
[0x03] SECTIONS 2 & 3 OF .RL
ArenaDescriptor (16 Byte) & ProofEntry (16 Byte)
| OFFSET DI BYTE | ArenaDescriptor | TIPO | DESCRIZIONE |
|---|---|---|---|
| 0..4 | arena_id | u32 | Identificatore di Arena colonnare (0 .. arena_count - 1) |
| 4..8 | element_count | u32 | Lunghezza di colonna omogenea (Shape Length) |
| 8 | type_lane | u8 | Tipo di elemento & larghezza di corsia SIMD (es. 0x18 = f64x8) |
| 9 | mutability | u8 | 0 = Input Immutabile | 1 = Regione Mutabile Lineare |
| 10..12 | alignment | u16 | Requisito di allineamento in byte (64 byte per AVX-512 / cache line) |
| 12..16 | initial_version | u32 | Versione iniziale di AffineToken (parte da 1) |
| OFFSET DI BYTE | ProofEntry | TIPO | DESCRIZIONE |
|---|---|---|---|
| 0..2 | rule_kind | u16 | 1 = SliceBounds (lo <= hi <= len) | 2 = GatherIndexInBounds (max_idx <= target_len) |
| 2..4 | target_arena | u16 | ID dell'Arena di destinazione strettamente vincolato a origin_arena dell'operando |
| 4..8 | bound_lo | u32 | Limite inferiore dell'indice non negativo |
| 8..12 | bound_hi | u32 | Limite superiore <= effective_target_len |
| 12..16 | witness_node | u32 | Nodo SSA indice testimone (in_b per Gather) |
[0x04] SECTION 4 OF .RL
Layout NodeFrame a 128 Bit (16 Byte)
Corsia Algoritmo (Cosa calcolare: Opcode / Operandi) Corsia Scheduling (Come eseguire: SIMD / MultiCore) Corsia Prova (Sicurezza: Biglietto di Versione / Limiti)
NODE #3 ($n3) node $n3 = Mul f64x8 fg=1 pol=simd proof=0 tok=pure a=$n0 b=$n0
16 BYTES = 128 BITSANALISI DEL REGISTRO A 8 BIT · 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
Campo: schedule_hint Tipo: u8
✓ Invariante del Verificatore O(N) Controllato al Caricamento (~5.78 ns) (fusion_group << 4) | exec_policy
Byte ortogonale di scheduling hardware: mutare 0x11 (SimdStream) -> 0x12 (MultiCore) cambia l'esecuzione della CPU senza alterare le prove di sicurezza.
Nodo #3: Quadrato vettoriale elemento per elemento a 8 vie ($n0 * $n0) fuso nei registri di cache L1 con zero allocazioni sull'heap.
[0x05] 29-OPCODE ISA (v0.4.0)
Set Completo di Istruzioni a 29 Opcode
| HEX | OPCODE | CATEGORIA | SEMANTICA | DESCRIZIONE |
|---|---|---|---|---|
| 0x01 | ArenaInput | Memory & Arena | ArenaDescriptor[in_a] -> Column | Carica una slice colonnare da ArenaDescriptor[in_a] con ReadLease. |
| 0x02 | ConstF64 | Memory & Arena | in_a | (in_b << 32) -> Scalar f64 | Costante scalare immediata in virgola mobile IEEE-754 a 64 bit. |
| 0x03 | ArenaSlice | Memory & Arena | Slice(in_a, ProofEntry[proof_idx]) -> Column | Sotto-slice zero-copy della colonna in_a certificata da ProofEntry. |
| 0x04 | ArenaMutate | Memory & Arena | Mutate(Arena[in_a], in_b) -> ver + 1 | Mutazione lineare in-place che consuma AffineToken (ver -> ver + 1). |
| 0x10 | Add | Arithmetic & Math | out[i] = a[i] + b[i] | Addizione SIMD elemento per elemento (VADDPD). |
| 0x11 | Sub | Arithmetic & Math | out[i] = a[i] - b[i] | Sottrazione SIMD elemento per elemento (VSUBPD). |
| 0x12 | Mul | Arithmetic & Math | out[i] = a[i] * b[i] | Moltiplicazione SIMD elemento per elemento (VMULPD). |
| 0x13 | Div | Arithmetic & Math | out[i] = a[i] / b[i] | Divisione SIMD IEEE-754 elemento per elemento (VDIVPD). |
| 0x14 | CmpGt | Predicate & Mask | mask[i] = a[i] > b[i] | Maschera di predicato maggiore-di priva di diramazioni (VCMPPD). |
| 0x15 | SelectZero | Predicate & Mask | out[i] = mask[i] ? val[i] : 0.0 | Selezione predicata priva di diramazioni che azzera le corsie mascherate (VANDPD). |
| 0x16 | Min | Arithmetic & Math | out[i] = min(a[i], b[i]) | Minimo elemento per elemento privo di diramazioni (VMINPD). |
| 0x17 | Max | Arithmetic & Math | out[i] = max(a[i], b[i]) | Massimo elemento per elemento privo di diramazioni (VMAXPD). |
| 0x18 | CmpLt | Predicate & Mask | mask[i] = a[i] < b[i] | Maschera di predicato minore-di priva di diramazioni. |
| 0x19 | CmpEq | Predicate & Mask | mask[i] = a[i] == b[i] | Maschera di predicato di uguaglianza priva di diramazioni. |
| 0x1A | Abs | Arithmetic & Math | out[i] = |a[i]| | Valore assoluto privo di diramazioni tramite azzeramento del bit di segno IEEE-754. |
| 0x1B | Sqrt | Arithmetic & Math | out[i] = sqrt(a[i]) | Radice quadrata SIMD hardware (VSQRTPD). |
| 0x1C | Floor | Arithmetic & Math | out[i] = floor(a[i]) | Arrotondamento privo di diramazioni verso -Infinito (VROUNDPD). |
| 0x1D | Ceil | Arithmetic & Math | out[i] = ceil(a[i]) | Arrotondamento privo di diramazioni verso +Infinito (VROUNDPD). |
| 0x1E | Ln | Arithmetic & Math | out[i] = ln(a[i]) | Stencil del logaritmo naturale elemento per elemento. |
| 0x1F | Exp | Arithmetic & Math | out[i] = exp(a[i]) | Stencil esponenziale naturale elemento per elemento. |
| 0x20 | FilterCompact | Reduction & Compaction | Compact(mask=in_a, vals=in_b) | Compattazione del flusso che impacchetta gli elementi corrispondenti in modo contiguo. |
| 0x21 | ReduceSum | Reduction & Compaction | sum(in_a) -> Scalar f64 | Riduzione orizzontale di somma a 8 accumulatori verso scalare. |
| 0x22 | ReduceMax | Reduction & Compaction | max(in_a) -> Scalar f64 | Riduzione orizzontale di massimo verso scalare. |
| 0x23 | Gather | Reduction & Compaction | target[indices[i]] (proof_idx > 0) | Gather indicizzato indiretto certificato supportato da ProofEntry. |
| 0x24 | ReduceMin | Reduction & Compaction | min(in_a) -> Scalar f64 | Riduzione orizzontale di minimo verso scalare. |
| 0x25 | MaskAnd | Predicate & Mask | mask[i] = a[i] && b[i] | Congiunzione bit a bit di maschera booleana. |
| 0x26 | MaskOr | Predicate & Mask | mask[i] = a[i] || b[i] | Disgiunzione bit a bit di maschera booleana. |
| 0x30 | RingEnqueue | Hardware & Contract | Enqueue(in_a) [Requires CAP_NET_RING] | Output su ring buffer hardware controllato da capacità. |
| 0x40 | AssertContract | Hardware & Contract | Assert(!is_nan(in_a) && is_finite(in_a)) | Contratto di dominio a runtime che verifica un output finito e non-NaN. |
[0x06] STATIC VERIFICATION (~5.78 NS/NODE)
Quattro Regole di Verifica Lineare O(N) a Passata Singola
1. Regola SSA Topologica
Ogni nodo all'indice i deve soddisfare in_a < i e in_b < i, prevenendo matematicamente i cicli.
2. Conservazione Lineare della Proprietà
ReadLease(a, ver) controlla live_version[a] == ver. AffineConsume(a, ver) controlla la mutabilità e incrementa live_version[a] tramite checked_add(1).
3. Prova di Raffinamento Vincolata all'Origine
ArenaSlice e Gather verificano ProofEntry.target_arena == origin_arena e bound_lo <= bound_hi <= effective_target_len.
4. CapabilityMask Zero-Trust
Gli opcode di I/O hardware (0x30 RingEnqueue) richiedono il bit corrispondente in RulHeader.capability_mask o vengono rifiutati prima dell'esecuzione.