Rul (.rl) v0.4 Binaire Specificatie — 128-Bit ISA & O(N) Verifier
Officiële binaire layoutspecificatie van Rul (.rl) v0.4: 64-byte RulHeader, 16-byte ArenaDescriptor, 16-byte ProofEntry, 128-bit NodeFrame over 29 opcodes en single-pass O(N) verificatieregels.
[0x01] CORE EQUATION
Artifact (.rl) = Algorithm + Schedule + Proof
Elk uitvoerbaar Rul-programma is een platte binaire .rl-image uitgelijnd op grenzen van 16 en 64 bytes voor directe zero-copy geheugenmapping (mmap). De kern-uitvoeringsengine bevat nul tekstuele lexers of AST-parsers.
1. Binair Eerst
Verliesvrije bidirectionele .rls <-> .rl conversie in ~8.8 µs aan de grens via src/transpiler.rs.
2. Topologische SSA-DAG
Elke instructienode i mag alleen verwijzen naar operanden strikt < i, wat beëindiging garandeert.
3. Scheiding Veiligheid + Intentie
Laag 1 bewijst geheugen-/bereikveiligheid in 5.78 ns/node; Laag 2 verifieert AssertContract & rul trace.
[0x02] SECTION 1 OF .RL
RulHeader (64 Bytes, Uitgelijnd op Cachelijn)
| BYTE-OFFSET | VELD | TYPE | BESCHRIJVING |
|---|---|---|---|
| 0..8 | magic | [u8; 8] | Canonieke magische handtekening: b"RUL\x00\x01\x00\x00\x00" |
| 8..16 | graph_hash | u64 | 64-bit FNV-1a integriteitshash over Arena-, Proof- en Node-secties |
| 16..24 | capability_mask | u64 | Hardware I/O-sandboxmasker (0x00 = Pure Compute, 0x01 = NetRing, 0x02 = StorageDMA, 0x04 = GpuDispatch) |
| 24..28 | arena_count | u32 | Aantal 16-byte ArenaDescriptor-items |
| 28..32 | proof_count | u32 | Aantal 16-byte ProofEntry grenscertificaten |
| 32..36 | node_count | u32 | Aantal 128-bit (16-byte) NodeFrame-instructies |
| 36..40 | output_node | u32 | Op 0 gebaseerde index van de primaire uitvoer-SSA-node |
| 40..64 | reserved | [u8; 24] | Met nullen gevulde opvulling die de header uitlijnt op een CPU-cachelijn van 64 bytes |
[0x03] SECTIONS 2 & 3 OF .RL
ArenaDescriptor (16 Bytes) & ProofEntry (16 Bytes)
| BYTE-OFFSET | ArenaDescriptor | TYPE | BESCHRIJVING |
|---|---|---|---|
| 0..4 | arena_id | u32 | Kolom-Arena-identificatie (0 .. arena_count - 1) |
| 4..8 | element_count | u32 | Homogene kolomlengte (Shape Length) |
| 8 | type_lane | u8 | Elementtype & SIMD-baanbreedte (bijv. 0x18 = f64x8) |
| 9 | mutability | u8 | 0 = Onveranderlijke Invoer | 1 = Lineaire Muteerbare Regio |
| 10..12 | alignment | u16 | Vereiste byte-uitlijning (64 bytes voor AVX-512 / cachelijn) |
| 12..16 | initial_version | u32 | Initiële AffineToken-versie (begint bij 1) |
| BYTE-OFFSET | ProofEntry | TYPE | BESCHRIJVING |
|---|---|---|---|
| 0..2 | rule_kind | u16 | 1 = SliceBounds (lo <= hi <= len) | 2 = GatherIndexInBounds (max_idx <= target_len) |
| 2..4 | target_arena | u16 | Doel-Arena-ID strikt gebonden aan operand origin_arena |
| 4..8 | bound_lo | u32 | Niet-negatieve ondergrens van index |
| 8..12 | bound_hi | u32 | Bovengrens <= effective_target_len |
| 12..16 | witness_node | u32 | Getuige SSA-indexnode (in_b voor Gather) |
[0x04] SECTION 4 OF .RL
128-Bit NodeFrame Layout (16 Bytes)
Algoritmestrook (Wat te berekenen: Opcode / Operanden) Schemastrook (Hoe uit te voeren: SIMD / MultiCore) Bewijsstrook (Veiligheid: Versieticket / 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 REGISTEROVERZICHT · 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
Veld: schedule_hint Type: u8
✓ O(N) Verifier-invariant Gecontroleerd bij het Laden (~5.78 ns) (fusion_group << 4) | exec_policy
Orthogonale hardware-schedule byte: het muteren van 0x11 (SimdStream) -> 0x12 (MultiCore) wijzigt de CPU-uitvoering zonder veiligheidsbewijzen aan te tasten.
Node #3: Elementgewijs 8-baans vectorkwadraat ($n0 * $n0) gefuseerd in L1-cacheregisters zonder tussenliggende heap-allocatie.
[0x05] 29-OPCODE ISA (v0.4.0)
Volledige Instructieset van 29 Opcodes
| HEX | OPCODE | CATEGORIE | SEMANTIEK | BESCHRIJVING |
|---|---|---|---|---|
| 0x01 | ArenaInput | Memory & Arena | ArenaDescriptor[in_a] -> Column | Laad kolom-slice uit ArenaDescriptor[in_a] met ReadLease. |
| 0x02 | ConstF64 | Memory & Arena | in_a | (in_b << 32) -> Scalar f64 | Directe 64-bit IEEE-754 drijvende-komma scalaire constante. |
| 0x03 | ArenaSlice | Memory & Arena | Slice(in_a, ProofEntry[proof_idx]) -> Column | Zero-copy sub-slice van kolom in_a gecertificeerd door ProofEntry. |
| 0x04 | ArenaMutate | Memory & Arena | Mutate(Arena[in_a], in_b) -> ver + 1 | Lineaire in-place mutatie die AffineToken consumeert (ver -> ver + 1). |
| 0x10 | Add | Arithmetic & Math | out[i] = a[i] + b[i] | Elementgewijze SIMD-optelling (VADDPD). |
| 0x11 | Sub | Arithmetic & Math | out[i] = a[i] - b[i] | Elementgewijze SIMD-aftrekking (VSUBPD). |
| 0x12 | Mul | Arithmetic & Math | out[i] = a[i] * b[i] | Elementgewijze SIMD-vermenigvuldiging (VMULPD). |
| 0x13 | Div | Arithmetic & Math | out[i] = a[i] / b[i] | Elementgewijze IEEE-754 SIMD-deling (VDIVPD). |
| 0x14 | CmpGt | Predicate & Mask | mask[i] = a[i] > b[i] | Branchless groter-dan predicaatmasker (VCMPPD). |
| 0x15 | SelectZero | Predicate & Mask | out[i] = mask[i] ? val[i] : 0.0 | Branchless geprediceerde selectie die gemaskeerde banen op nul zet (VANDPD). |
| 0x16 | Min | Arithmetic & Math | out[i] = min(a[i], b[i]) | Branchless elementgewijs minimum (VMINPD). |
| 0x17 | Max | Arithmetic & Math | out[i] = max(a[i], b[i]) | Branchless elementgewijs maximum (VMAXPD). |
| 0x18 | CmpLt | Predicate & Mask | mask[i] = a[i] < b[i] | Branchless kleiner-dan predicaatmasker. |
| 0x19 | CmpEq | Predicate & Mask | mask[i] = a[i] == b[i] | Branchless gelijkheidspredicaatmasker. |
| 0x1A | Abs | Arithmetic & Math | out[i] = |a[i]| | Branchless absolute waarde via wissen van IEEE-754 tekenbit. |
| 0x1B | Sqrt | Arithmetic & Math | out[i] = sqrt(a[i]) | Hardware SIMD-vierkantswortel (VSQRTPD). |
| 0x1C | Floor | Arithmetic & Math | out[i] = floor(a[i]) | Branchless afronding richting -Oneindig (VROUNDPD). |
| 0x1D | Ceil | Arithmetic & Math | out[i] = ceil(a[i]) | Branchless afronding richting +Oneindig (VROUNDPD). |
| 0x1E | Ln | Arithmetic & Math | out[i] = ln(a[i]) | Elementgewijze natuurlijke logaritme-stencil. |
| 0x1F | Exp | Arithmetic & Math | out[i] = exp(a[i]) | Elementgewijze natuurlijke exponentiële stencil. |
| 0x20 | FilterCompact | Reduction & Compaction | Compact(mask=in_a, vals=in_b) | Stroomcompactie die overeenkomende elementen aaneengesloten verpakt. |
| 0x21 | ReduceSum | Reduction & Compaction | sum(in_a) -> Scalar f64 | Horizontale somreductie met 8 accumulatoren naar scalair. |
| 0x22 | ReduceMax | Reduction & Compaction | max(in_a) -> Scalar f64 | Horizontale maximumreductie naar scalair. |
| 0x23 | Gather | Reduction & Compaction | target[indices[i]] (proof_idx > 0) | Gecertificeerde indirecte geïndexeerde gather ondersteund door ProofEntry. |
| 0x24 | ReduceMin | Reduction & Compaction | min(in_a) -> Scalar f64 | Horizontale minimumreductie naar scalair. |
| 0x25 | MaskAnd | Predicate & Mask | mask[i] = a[i] && b[i] | Bitgewijze booleaanse maskerconjunctie. |
| 0x26 | MaskOr | Predicate & Mask | mask[i] = a[i] || b[i] | Bitgewijze booleaanse maskerdisjunctie. |
| 0x30 | RingEnqueue | Hardware & Contract | Enqueue(in_a) [Requires CAP_NET_RING] | Door capabilities beveiligde hardware-ringbufferuitvoer. |
| 0x40 | AssertContract | Hardware & Contract | Assert(!is_nan(in_a) && is_finite(in_a)) | Runtime-domeincontract dat eindige, niet-NaN uitvoer verifieert. |
[0x06] STATIC VERIFICATION (~5.78 NS/NODE)
Vier Single-Pass O(N) Lineaire Verificatieregels
1. Topologische SSA-Regel
Elke node op index i moet voldoen aan in_a < i en in_b < i, wat cycli wiskundig voorkomt.
2. Lineair Eigendomsbehoud
ReadLease(a, ver) controleert live_version[a] == ver. AffineConsume(a, ver) controleert muteerbaarheid en verhoogt live_version[a] via checked_add(1).
3. Oorsprongsgebonden Verfijningsbewijs
ArenaSlice en Gather verifiëren ProofEntry.target_arena == origin_arena en bound_lo <= bound_hi <= effective_target_len.
4. Zero-Trust CapabilityMask
Hardware I/O-opcodes (0x30 RingEnqueue) vereisen het overeenkomstige bit in RulHeader.capability_mask of worden vóór uitvoering geweigerd.