Rul (.rl) v0.4 Binary Specification — 128-Bit ISA & O(N) Verifier
Official binary layout specification of Rul (.rl) v0.4: 64-byte RulHeader, 16-byte ArenaDescriptor, 16-byte ProofEntry, 128-bit NodeFrame across 29 opcodes, and single-pass O(N) verification rules.
[0x01] CORE EQUATION
Artifact (.rl) = Algorithm + Schedule + Proof
Every executable Rul program is a flat binary .rl image aligned on 16-byte and 64-byte boundaries for direct zero-copy memory mapping (mmap). The core execution engine contains zero textual lexers or AST parsers.
1. Binary-First
Lossless bidirectional .rls <-> .rl conversion in ~8.8 µs at the boundary via src/transpiler.rs.
2. Topological SSA-DAG
Every instruction node i may only reference operands strictly < i, guaranteeing termination.
3. Safety + Intent Split
Layer 1 proves memory/bounds safety in 5.78 ns/node; Layer 2 verifies AssertContract & rul trace.
[0x02] SECTION 1 OF .RL
RulHeader (64 Bytes, Cache-Line Aligned)
| BYTE OFFSET | FIELD | TYPE | DESCRIPTION |
|---|---|---|---|
| 0..8 | magic | [u8; 8] | Canonical magic signature: b"RUL\x00\x01\x00\x00\x00" |
| 8..16 | graph_hash | u64 | 64-bit FNV-1a integrity hash over Arena, Proof, and Node sections |
| 16..24 | capability_mask | u64 | Hardware I/O sandbox mask (0x00 = Pure Compute, 0x01 = NetRing, 0x02 = StorageDMA, 0x04 = GpuDispatch) |
| 24..28 | arena_count | u32 | Number of 16-byte ArenaDescriptor entries |
| 28..32 | proof_count | u32 | Number of 16-byte ProofEntry bounds certificates |
| 32..36 | node_count | u32 | Number of 128-bit (16-byte) NodeFrame instructions |
| 36..40 | output_node | u32 | 0-based index of the primary output SSA node |
| 40..64 | reserved | [u8; 24] | Zero-filled padding aligning header to 64-byte CPU cache line |
[0x03] SECTIONS 2 & 3 OF .RL
ArenaDescriptor (16 Bytes) & ProofEntry (16 Bytes)
| BYTE OFFSET | ArenaDescriptor | TYPE | DESCRIPTION |
|---|---|---|---|
| 0..4 | arena_id | u32 | Columnar Arena identifier (0 .. arena_count - 1) |
| 4..8 | element_count | u32 | Homogeneous column length (Shape Length) |
| 8 | type_lane | u8 | Element type & SIMD lane width (e.g. 0x18 = f64x8) |
| 9 | mutability | u8 | 0 = Immutable Input | 1 = Linear Mutable Region |
| 10..12 | alignment | u16 | Byte alignment requirement (64 bytes for AVX-512 / cache line) |
| 12..16 | initial_version | u32 | Initial AffineToken version (starts at 1) |
| BYTE OFFSET | ProofEntry | TYPE | DESCRIPTION |
|---|---|---|---|
| 0..2 | rule_kind | u16 | 1 = SliceBounds (lo <= hi <= len) | 2 = GatherIndexInBounds (max_idx <= target_len) |
| 2..4 | target_arena | u16 | Target Arena ID strictly bound to operand origin_arena |
| 4..8 | bound_lo | u32 | Non-negative lower index bound |
| 8..12 | bound_hi | u32 | Upper bound <= effective_target_len |
| 12..16 | witness_node | u32 | Witness SSA index node (in_b for Gather) |
[0x04] SECTION 4 OF .RL
128-Bit NodeFrame Layout (16 Bytes)
Algorithm Lane (What to compute: Opcode / Operands) Schedule Lane (How to run: SIMD / MultiCore) Proof Lane (Safety: Version Ticket / Bounds)
NODE #3 ($n3) node $n3 = Mul f64x8 fg=1 pol=simd proof=0 tok=pure a=$n0 b=$n0
16 BYTES = 128 BITS8-BIT REGISTER BREAKDOWN · 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
Field: schedule_hint Type: u8
✓ O(N) Verifier Invariant Checked at Load Time (~5.78 ns) (fusion_group << 4) | exec_policy
Orthogonal hardware schedule byte: mutating 0x11 (SimdStream) -> 0x12 (MultiCore) changes CPU execution without altering safety proofs.
Node #3: Elementwise 8-lane vector square ($n0 * $n0) fused in L1 cache registers with zero intermediate heap allocation.
[0x05] 29-OPCODE ISA (v0.4.0)
Complete 29-Opcode Instruction Set
| HEX | OPCODE | CATEGORY | SEMANTICS | DESCRIPTION |
|---|---|---|---|---|
| 0x01 | ArenaInput | Memory & Arena | ArenaDescriptor[in_a] -> Column | Load columnar slice from ArenaDescriptor[in_a] with ReadLease. |
| 0x02 | ConstF64 | Memory & Arena | in_a | (in_b << 32) -> Scalar f64 | Immediate 64-bit IEEE-754 floating-point scalar constant. |
| 0x03 | ArenaSlice | Memory & Arena | Slice(in_a, ProofEntry[proof_idx]) -> Column | Zero-copy sub-slice of column in_a certified by ProofEntry. |
| 0x04 | ArenaMutate | Memory & Arena | Mutate(Arena[in_a], in_b) -> ver + 1 | Linear in-place mutation consuming AffineToken (ver -> ver + 1). |
| 0x10 | Add | Arithmetic & Math | out[i] = a[i] + b[i] | Elementwise SIMD addition (VADDPD). |
| 0x11 | Sub | Arithmetic & Math | out[i] = a[i] - b[i] | Elementwise SIMD subtraction (VSUBPD). |
| 0x12 | Mul | Arithmetic & Math | out[i] = a[i] * b[i] | Elementwise SIMD multiplication (VMULPD). |
| 0x13 | Div | Arithmetic & Math | out[i] = a[i] / b[i] | Elementwise IEEE-754 SIMD division (VDIVPD). |
| 0x14 | CmpGt | Predicate & Mask | mask[i] = a[i] > b[i] | Branchless greater-than predicate mask (VCMPPD). |
| 0x15 | SelectZero | Predicate & Mask | out[i] = mask[i] ? val[i] : 0.0 | Branchless predicated selection zeroing masked-out lanes (VANDPD). |
| 0x16 | Min | Arithmetic & Math | out[i] = min(a[i], b[i]) | Branchless elementwise minimum (VMINPD). |
| 0x17 | Max | Arithmetic & Math | out[i] = max(a[i], b[i]) | Branchless elementwise maximum (VMAXPD). |
| 0x18 | CmpLt | Predicate & Mask | mask[i] = a[i] < b[i] | Branchless less-than predicate mask. |
| 0x19 | CmpEq | Predicate & Mask | mask[i] = a[i] == b[i] | Branchless equality predicate mask. |
| 0x1A | Abs | Arithmetic & Math | out[i] = |a[i]| | Branchless IEEE-754 sign-bit clear absolute value. |
| 0x1B | Sqrt | Arithmetic & Math | out[i] = sqrt(a[i]) | Hardware SIMD square root (VSQRTPD). |
| 0x1C | Floor | Arithmetic & Math | out[i] = floor(a[i]) | Branchless rounding toward -Infinity (VROUNDPD). |
| 0x1D | Ceil | Arithmetic & Math | out[i] = ceil(a[i]) | Branchless rounding toward +Infinity (VROUNDPD). |
| 0x1E | Ln | Arithmetic & Math | out[i] = ln(a[i]) | Elementwise natural logarithm stencil. |
| 0x1F | Exp | Arithmetic & Math | out[i] = exp(a[i]) | Elementwise natural exponential stencil. |
| 0x20 | FilterCompact | Reduction & Compaction | Compact(mask=in_a, vals=in_b) | Stream compaction packing matching elements contiguously. |
| 0x21 | ReduceSum | Reduction & Compaction | sum(in_a) -> Scalar f64 | 8-accumulator horizontal sum reduction to scalar. |
| 0x22 | ReduceMax | Reduction & Compaction | max(in_a) -> Scalar f64 | Horizontal maximum reduction to scalar. |
| 0x23 | Gather | Reduction & Compaction | target[indices[i]] (proof_idx > 0) | Certified indirect indexed gather backed by ProofEntry. |
| 0x24 | ReduceMin | Reduction & Compaction | min(in_a) -> Scalar f64 | Horizontal minimum reduction to scalar. |
| 0x25 | MaskAnd | Predicate & Mask | mask[i] = a[i] && b[i] | Bitwise boolean mask conjunction. |
| 0x26 | MaskOr | Predicate & Mask | mask[i] = a[i] || b[i] | Bitwise boolean mask disjunction. |
| 0x30 | RingEnqueue | Hardware & Contract | Enqueue(in_a) [Requires CAP_NET_RING] | Capability-gated hardware ring buffer output. |
| 0x40 | AssertContract | Hardware & Contract | Assert(!is_nan(in_a) && is_finite(in_a)) | Runtime domain contract verifying finite, non-NaN output. |
[0x06] STATIC VERIFICATION (~5.78 NS/NODE)
Four Single-Pass O(N) Linear Verification Rules
1. Topological SSA Rule
Every node at index i must satisfy in_a < i and in_b < i, mathematically preventing cycles.
2. Linear Ownership Conservation
ReadLease(a, ver) checks live_version[a] == ver. AffineConsume(a, ver) checks mutability and increments live_version[a] via checked_add(1).
3. Origin-Bound Refinement Proof
ArenaSlice and Gather verify ProofEntry.target_arena == origin_arena and bound_lo <= bound_hi <= effective_target_len.
4. Zero-Trust CapabilityMask
Hardware I/O opcodes (0x30 RingEnqueue) require the matching bit in RulHeader.capability_mask or are rejected before execution.