Rul (.rl) v0.4 Binärspezifikation — 128-Bit-ISA & O(N)-Verifizierer
Offizielle Binärlayout-Spezifikation von Rul (.rl) v0.4: 64-Byte-RulHeader, 16-Byte-ArenaDescriptor, 16-Byte-ProofEntry, 128-Bit-NodeFrame über 29 Opcodes und lineare O(N)-Verifikationsregeln.
[0x01] CORE EQUATION
Artifact (.rl) = Algorithm + Schedule + Proof
Jedes ausführbare Rul-Programm ist ein flaches binäres .rl-Abbild, das für direktes Zero-Copy-Memory-Mapping (mmap) an 16-Byte- und 64-Byte-Grenzen ausgerichtet ist. Die Kern-Engine enthält keinerlei Text-Lexer oder AST-Parser.
1. Binary-First
Verlustfreie bidirektionale .rls <-> .rl Umwandlung in ~8,8 µs an der Systemgrenze über src/transpiler.rs.
2. Topologischer SSA-DAG
Jeder Befehlsknoten i darf nur Operanden strikt < i referenzieren, was Terminierung mathematisch garantiert.
3. Trennung von Sicherheit & Absicht
Schicht 1 beweist Speicher-/Grenzsicherheit in 5,78 ns/Knoten; Schicht 2 prüft AssertContract & rul trace.
[0x02] SECTION 1 OF .RL
RulHeader (64 Bytes, Cache-Line-ausgerichtet)
| BYTE-OFFSET | FELD | TYP | BESCHREIBUNG |
|---|---|---|---|
| 0..8 | magic | [u8; 8] | Kanonische Magic-Signatur: b"RUL\x00\x01\x00\x00\x00" |
| 8..16 | graph_hash | u64 | 64-Bit-FNV-1a-Integritätshash über Arena-, Proof- und Node-Tabellen |
| 16..24 | capability_mask | u64 | Hardware-I/O-Sandbox-Maske (0x00 = Reine Berechnung, 0x01 = NetRing, 0x02 = StorageDMA, 0x04 = GpuDispatch) |
| 24..28 | arena_count | u32 | Anzahl der 16-Byte-ArenaDescriptor-Einträge |
| 28..32 | proof_count | u32 | Anzahl der 16-Byte-ProofEntry-Grenzzertifikate |
| 32..36 | node_count | u32 | Anzahl der 128-Bit (16-Byte) NodeFrame-Befehle |
| 36..40 | output_node | u32 | 0-basierter Index des primären Ausgabe-SSA-Knotens |
| 40..64 | reserved | [u8; 24] | Mit Nullen gefülltes Padding zur Ausrichtung auf eine 64-Byte-CPU-Cache-Line |
[0x03] SECTIONS 2 & 3 OF .RL
ArenaDescriptor (16 Bytes) & ProofEntry (16 Bytes)
| BYTE-OFFSET | ArenaDescriptor | TYP | BESCHREIBUNG |
|---|---|---|---|
| 0..4 | arena_id | u32 | Spalten-Arena-Kennung (0 .. arena_count - 1) |
| 4..8 | element_count | u32 | Elementanzahl der homogenen Spalte (Shape-Länge) |
| 8 | type_lane | u8 | Elementtyp & SIMD-Spurbreite (z. B. 0x18 = f64x8) |
| 9 | mutability | u8 | 0 = Unveränderliche Eingabe | 1 = Linear veränderliche Region |
| 10..12 | alignment | u16 | Byte-Ausrichtungsanforderung (64 Bytes für AVX-512 / Cache-Line) |
| 12..16 | initial_version | u32 | Initiale AffineToken-Version (beginnt bei 1) |
| BYTE-OFFSET | ProofEntry | TYP | BESCHREIBUNG |
|---|---|---|---|
| 0..2 | rule_kind | u16 | 1 = SliceBounds (lo <= hi <= len) | 2 = GatherIndexInBounds (max_idx <= target_len) |
| 2..4 | target_arena | u16 | Ziel-Arena-ID, strikt gebunden an die origin_arena des Operanden |
| 4..8 | bound_lo | u32 | Nicht-negative untere Indexgrenze |
| 8..12 | bound_hi | u32 | Obere Grenze <= effective_target_len |
| 12..16 | witness_node | u32 | Zeugen-SSA-Indexknoten (in_b für Gather) |
[0x04] SECTION 4 OF .RL
128-Bit-NodeFrame-Layout (16 Bytes)
Algorithmus-Spur (Was berechnen: Opcode / Operanden) Zeitplan-Spur (Wie ausführen: SIMD / MultiCore) Beweis-Spur (Sicherheit: Versionsticket / Grenzen)
NODE #3 ($n3) node $n3 = Mul f64x8 fg=1 pol=simd proof=0 tok=pure a=$n0 b=$n0
16 BYTES = 128 BITS8-BIT-REGISTERAUFSCHLÜSSELUNG · 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
Feld: schedule_hint Typ: u8
✓ Beim Laden geprüfte O(N)-Verifizierer-Invariante (~5.78 ns) (fusion_group << 4) | exec_policy
Orthogonales Hardware-Zeitplan-Byte: Mutation von 0x11 (SimdStream) -> 0x12 (MultiCore) ändert die CPU-Ausführung ohne Änderung der Sicherheitsbeweise.
Knoten #3: Elementweises 8-Spur-Vektorquadrat ($n0 * $n0), verschmolzen in L1-Cache-Registern ohne Zwischen-Heap-Allokation.
[0x05] 29-OPCODE ISA (v0.4.0)
Vollständiger 29-Opcode-Befehlssatz (v0.4.0)
| HEX | OPCODE | KATEGORIE | SEMANTIK | BESCHREIBUNG |
|---|---|---|---|---|
| 0x01 | ArenaInput | Memory & Arena | ArenaDescriptor[in_a] -> Column | Spalten-Slice aus ArenaDescriptor[in_a] mit ReadLease laden. |
| 0x02 | ConstF64 | Memory & Arena | in_a | (in_b << 32) -> Scalar f64 | Unmittelbare 64-Bit-IEEE-754-Gleitkomma-Skalarkonstante. |
| 0x03 | ArenaSlice | Memory & Arena | Slice(in_a, ProofEntry[proof_idx]) -> Column | Durch ProofEntry zertifizierter Zero-Copy-Sub-Slice der Spalte in_a. |
| 0x04 | ArenaMutate | Memory & Arena | Mutate(Arena[in_a], in_b) -> ver + 1 | Lineare In-Place-Mutation unter Verbrauch des AffineToken (ver -> ver + 1). |
| 0x10 | Add | Arithmetic & Math | out[i] = a[i] + b[i] | Elementweise SIMD-Addition (VADDPD). |
| 0x11 | Sub | Arithmetic & Math | out[i] = a[i] - b[i] | Elementweise SIMD-Subtraktion (VSUBPD). |
| 0x12 | Mul | Arithmetic & Math | out[i] = a[i] * b[i] | Elementweise SIMD-Multiplikation (VMULPD). |
| 0x13 | Div | Arithmetic & Math | out[i] = a[i] / b[i] | Elementweise IEEE-754-SIMD-Division (VDIVPD). |
| 0x14 | CmpGt | Predicate & Mask | mask[i] = a[i] > b[i] | Verzweigungsfreie Größer-Als-Prädikatsmaske (VCMPPD). |
| 0x15 | SelectZero | Predicate & Mask | out[i] = mask[i] ? val[i] : 0.0 | Verzweigungsfreie Prädikatsauswahl mit Nullung ausmaskierter Spuren (VANDPD). |
| 0x16 | Min | Arithmetic & Math | out[i] = min(a[i], b[i]) | Verzweigungsfreies elementweises Minimum (VMINPD). |
| 0x17 | Max | Arithmetic & Math | out[i] = max(a[i], b[i]) | Verzweigungsfreies elementweises Maximum (VMAXPD). |
| 0x18 | CmpLt | Predicate & Mask | mask[i] = a[i] < b[i] | Verzweigungsfreie Kleiner-Als-Prädikatsmaske. |
| 0x19 | CmpEq | Predicate & Mask | mask[i] = a[i] == b[i] | Verzweigungsfreie Gleichheits-Prädikatsmaske. |
| 0x1A | Abs | Arithmetic & Math | out[i] = |a[i]| | Verzweigungsfreier Absolutwert durch Löschen des IEEE-754-Vorzeichenbits. |
| 0x1B | Sqrt | Arithmetic & Math | out[i] = sqrt(a[i]) | Hardware-SIMD-Quadratwurzel (VSQRTPD). |
| 0x1C | Floor | Arithmetic & Math | out[i] = floor(a[i]) | Verzweigungsfreie Rundung gegen -Infinity (VROUNDPD). |
| 0x1D | Ceil | Arithmetic & Math | out[i] = ceil(a[i]) | Verzweigungsfreie Rundung gegen +Infinity (VROUNDPD). |
| 0x1E | Ln | Arithmetic & Math | out[i] = ln(a[i]) | Elementweiser natürlicher Logarithmus. |
| 0x1F | Exp | Arithmetic & Math | out[i] = exp(a[i]) | Elementweise natürliche Exponentialfunktion. |
| 0x20 | FilterCompact | Reduction & Compaction | Compact(mask=in_a, vals=in_b) | Stream-Kompaktierung, die passende Elemente lückenlos packt. |
| 0x21 | ReduceSum | Reduction & Compaction | sum(in_a) -> Scalar f64 | Horizontale 8-Akkumulator-Summenreduktion auf einen Skalar. |
| 0x22 | ReduceMax | Reduction & Compaction | max(in_a) -> Scalar f64 | Horizontale Maximumreduktion auf einen Skalar. |
| 0x23 | Gather | Reduction & Compaction | target[indices[i]] (proof_idx > 0) | Durch ProofEntry abgesichertes indirektes Index-Gather. |
| 0x24 | ReduceMin | Reduction & Compaction | min(in_a) -> Scalar f64 | Horizontale Minimumreduktion auf einen Skalar. |
| 0x25 | MaskAnd | Predicate & Mask | mask[i] = a[i] && b[i] | Bitweise boolesche Masken-Konjunktion (AND). |
| 0x26 | MaskOr | Predicate & Mask | mask[i] = a[i] || b[i] | Bitweise boolesche Masken-Disjunktion (OR). |
| 0x30 | RingEnqueue | Hardware & Contract | Enqueue(in_a) [Requires CAP_NET_RING] | Berechtigungsgesteuerte Hardware-Ringpuffer-Ausgabe (erfordert CAP_NET_RING). |
| 0x40 | AssertContract | Hardware & Contract | Assert(!is_nan(in_a) && is_finite(in_a)) | Laufzeit-Domänenvertrag zur Prüfung auf endliche, Nicht-NaN-Ausgabe. |
[0x06] STATIC VERIFICATION (~5.78 NS/NODE)
Vier lineare Single-Pass O(N)-Verifikationsregeln
1. Topologische SSA-Regel
Jeder Knoten an Index i muss in_a < i und in_b < i erfüllen, was Zyklen mathematisch verhindert.
2. Lineare Eigentumserhaltung
ReadLease(a, ver) prüft live_version[a] == ver. AffineConsume(a, ver) prüft Veränderbarkeit und erhöht live_version[a] über checked_add(1).
3. Ursprungsgebundener Grenzbeweis
ArenaSlice und Gather prüfen ProofEntry.target_arena == origin_arena sowie bound_lo <= bound_hi <= effective_target_len.
4. Zero-Trust-CapabilityMask
Hardware-I/O-Opcodes (0x30 RingEnqueue) erfordern das entsprechende Bit in RulHeader.capability_mask oder werden vor der Ausführung abgelehnt.