# Rul (.rl) — Complete 1-Shot Technical Specification & AI Agent Context (v0.4.0)

- **Canonical Repository**: https://github.com/rul-lang/rul
- **Zenodo DOI**: https://doi.org/10.5281/zenodo.23722094 (10.5281/zenodo.23722094)
- **Maintained By**: Rul Core Architecture Team (https://github.com/rul-lang)
- **License**: MIT OR Apache-2.0
- **Core Equation**: `Artifact (.rl) = Algorithm + Schedule + Proof`

---

## 1. Binary Layout of a `.rl` Program

Every executable `.rl` program is a flat binary image aligned on 16-byte and 64-byte boundaries for zero-copy `mmap`:
1. `RulHeader` (64 bytes, 64-byte aligned)
2. `ArenaDescriptor` Table (`arena_count * 16 bytes`)
3. `ProofEntry` Sidecar Table (`proof_count * 16 bytes`)
4. `NodeFrame` Instruction Array (`node_count * 16 bytes` — 128-bit Topological SSA-DAG)

### 1.1. RulHeader (64 Bytes)
| 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 |

### 1.2. ArenaDescriptor (16 Bytes)
| Byte Offset | Field | 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) |

### 1.3. ProofEntry Sidecar Table (16 Bytes)
| Byte Offset | Field | 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) |

### 1.4. 128-Bit NodeFrame Instruction Layout (Bytes 0..15)
| Byte / Bits | Field & Type | Lane | O(N) Verifier Invariant Checked |
| :--- | :--- | :--- | :--- |
| Byte `0` (`b0..b7`) | `opcode` (`u8`) | `ALGORITHM` | Validates instruction opcode is in the 29-opcode v0.4 ISA and checks CapabilityMask if opcode == 0x30 (RingEnqueue). |
| Byte `1` (`b8..b15`) | `type_lane` (`u8`) | `ALGORITHM` | Unifies operand element types (0x1=F64, 0x2=I64, 0x3=Mask) and SIMD lane width (0x1=Scalar, 0x4=AVX2, 0x8=8-Way). |
| Byte `2` (`b16..b23`) | `schedule_hint` (`u8`) | `SCHEDULE` | Orthogonal hardware schedule byte: mutating 0x11 (SimdStream) -> 0x12 (MultiCore) changes CPU execution without altering safety proofs. |
| Byte `3` (`b24..b31`) | `proof_idx` (`u8`) | `PROOF` | O(1) bounds certificate check: 0 proves equal column length by construction; >0 verifies SliceBounds or GatherIndexInBounds. |
| Byte `4` (`b32..b39`) | `token_op (ver_lo)` (`u32 [7:0]`) | `PROOF` | Checks live_version[arena_id] == token_version (1). Rejects stale versions immediately with StaleOrConsumedToken. |
| Byte `5` (`b40..b47`) | `token_op (ver_hi)` (`u32 [15:8]`) | `PROOF` | Guards 16-bit version counter against wraparound on AffineConsume via checked_add(1) <= u16::MAX (TokenVersionOverflow). |
| Byte `6` (`b48..b55`) | `token_op (arena_lo)` (`u32 [23:16]`) | `PROOF` | Verifies target arena_id < RulHeader.arena_count and checks ArenaDescriptor[id].mutability == 1 for AffineConsume. |
| Byte `7` (`b56..b63`) | `token_op (mode)` (`u32 [31:24]`) | `PROOF` | Enforces linear ownership conservation in a single forward scan without Rust borrow-checker constraint solving. |
| Byte `8` (`b64..b71`) | `in_a (byte 0)` (`u32 [7:0]`) | `ALGORITHM` | Topological SSA-DAG invariant: strictly enforces in_a < current_node_idx, mathematically preventing cycles and infinite loops. |
| Byte `9` (`b72..b79`) | `in_a (byte 1)` (`u32 [15:8]`) | `ALGORITHM` | Resolves upstream node shape and origin_arena in O(1) array lookup from verified_nodes[in_a]. |
| Byte `10` (`b80..b87`) | `in_a (byte 2)` (`u32 [23:16]`) | `ALGORITHM` | Part of 32-bit operand index in_a (or lower 32 bits of IEEE-754 f64 payload for ConstF64). |
| Byte `11` (`b88..b95`) | `in_a (byte 3)` (`u32 [31:24]`) | `ALGORITHM` | High byte of in_a: guarantees zero out-of-range node references before code generation begins. |
| Byte `12` (`b96..b103`) | `in_b (byte 0)` (`u32 [7:0]`) | `ALGORITHM` | Topological SSA-DAG invariant: strictly enforces in_b < current_node_idx and verifies shape compatibility with in_a. |
| Byte `13` (`b104..b111`) | `in_b (byte 1)` (`u32 [15:8]`) | `ALGORITHM` | For Gather (0x23), binds witness_node = in_b to ProofEntry[proof_idx - 1] bounds certificate. |
| Byte `14` (`b112..b119`) | `in_b (byte 2)` (`u32 [23:16]`) | `ALGORITHM` | For ConstF64 (0x02), stores bits 48..55 of the 64-bit IEEE-754 floating-point constant (0x59 for 100.0). |
| Byte `15` (`b120..b127`) | `in_b (byte 3)` (`u32 [31:24]`) | `ALGORITHM` | Completes the 16-byte (128-bit) cache-aligned NodeFrame; for ConstF64, verifies constant is finite (!is_nan() && is_finite()). |

---

## 2. Complete 29-Opcode Instruction Set (v0.4.0)

| Opcode | Mnemonic | Category | Signature | 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. |

---

## 3. Canonical 7-Node `.rls` Assembly & White-Box Trace Example

### 3.1. Symbolic Assembly (`src/main.rls` — 208 Bytes in `.rl` -> 817-Byte Standalone Linux ELF64)
```text
cap 0x0
arena 0 len=4096 lane=f64x8 mut=false align=64 ver=1
node $n0 = ArenaInput f64x8 fg=1 pol=simd proof=0 tok=read(0,1) a=0 b=0
node $n1 = ConstF64   f64x1 fg=1 pol=simd proof=0 tok=pure const=100.0
node $n2 = CmpGt      maskx8 fg=1 pol=simd proof=0 tok=pure a=$n0 b=$n1
node $n3 = Mul        f64x8 fg=1 pol=simd proof=0 tok=pure a=$n0 b=$n0
node $n4 = SelectZero f64x8 fg=1 pol=simd proof=0 tok=pure a=$n2 b=$n3
node $n5 = ReduceSum  f64x1 fg=1 pol=simd proof=0 tok=pure a=$n4 b=0
node $n6 = AssertContract f64x1 fg=1 pol=simd proof=0 tok=pure a=$n5 b=0
output $n6
```

### 3.2. White-Box Execution Trace (`rul trace`)
| Node | Opcode | Kind | Len | Min | Max | Sum/Trues | NaN/Inf | Sample[0..4] |
| :--- | :--- | :--- | ---: | ---: | ---: | ---: | ---: | :--- |
| `#0` | `ArenaInput` | `ColumnF64` | `4096` | `0.5000` | `249.5000` | `504608.0000` | `0` | `[0.500, 1.500, 2.500, 3.500]` |
| `#1` | `ConstF64` | `Scalar` | `1` | `100.0000` | `100.0000` | `100.0000` | `0` | `[100.000]` |
| `#2` | `CmpGt` | `ColumnMask` | `4096` | `0.0000` | `1.0000` | `2400.0000` | `0` | `[0.000, 0.000, 0.000, 0.000]` |
| `#3` | `Mul` | `ColumnF64` | `4096` | `0.2500` | `62250.2500` | `83627904.0000` | `0` | `[0.250, 2.250, 6.250, 12.250]` |
| `#4` | `SelectZero` | `ColumnF64` | `4096` | `0.0000` | `62250.2500` | `77999800.0000` | `0` | `[0.000, 0.000, 0.000, 0.000]` |
| `#5` | `ReduceSum` | `Scalar` | `1` | `77999800.0000` | `77999800.0000` | `77999800.0000` | `0` | `[77999800.000]` |
| `#6` | `AssertContract` | `Scalar` | `1` | `77999800.0000` | `77999800.0000` | `77999800.0000` | `0` | `[77999800.000]` |

---

## 4. Empirical Benchmark (10,000,000 `f64` Elements = 80 MB Array)

| Implementation | Execution Mode | Median Latency | Effective Bandwidth | Speedup vs C 8-Acc | Speedup vs Legacy AoS |
| :--- | :--- | ---: | ---: | ---: | ---: |
| `[A]` [A] Imperative AoS + Vec::collect() | 1-Core AoS + Heap Allocation | `70.66 ms` | `1.13 GB/s` | `0.10x` | `1.00x` |
| `[B]` [B] Idiomatic Rust SoA (filter().map().sum()) | 1-Core SoA Iterator Chain | `19.12 ms` | `4.18 GB/s` | `0.38x` | `3.70x` |
| `[C]` [C] Hand-Written C/Rust 8-Accumulator SoA | 1-Core 8-Lane Unrolled Baseline | `7.32 ms` | `10.92 GB/s` | `1.00x (Baseline)` | `9.65x` |
| `[D]` [D] Rul (.rl) Tier 2 Fused SIMD (0x11) | 1-Core L1-Tile SIMD (SimdStream) | `5.91 ms` | `13.53 GB/s` | `1.24x (1-Core vs 1-Core)` | `11.95x` |
| `[E]` [E] Rul (.rl) Tier 2 MultiCore (0x12) | All Cores (1-Byte Schedule Mutation) | `3.19 ms` | `25.04 GB/s` | `2.29x (Schedule Byte)` | `22.12x` |
| `[F]` [F] Rul (.rl) Tier 2 MultiCore + ZoneMap | All Cores + O(1) Cold Tile Skipping | `1.55 ms` | `51.53 GB/s` | `4.72x (Peak Speedup)` | `45.51x` |

---

## 5. Model Context Protocol (`rul-mcp`) Tools for Autonomous AI Agents

- **`rul_assemble_and_verify`** (`~8.8 µs + 5.8 ns/node`): `(rls_source: string) -> VerifiedSummary + .rl hex` — Assembles symbolic .rls instructions into a 128-bit binary .rl image and runs the single-pass O(N) static verifier.
- **`rul_test_differential`** (`Tier 0 == Tier 1 == Tier 2`): `(rls_source: string, arenas: ArenaData[]) -> DiffReport` — Executes the verified program across Tier 0 (Oracle), Tier 1 (Stencil), and Tier 2 (L1 Fused) to prove bitwise/ULP equivalence.
- **`rul_autotune_schedule`** (`1-Byte Sweep`): `(rls_source: string) -> Optimal ScheduleHint + Telemetry` — Sweeps AutoL1Tile (0x10), SimdStream (0x11), and MultiCore (0x12) policies and selects the highest GB/s hardware reward score.
- **`rul_compile_standalone`** (`~6.4 µs ELF64`): `(rls_source: string) -> Standalone Linux x86_64 ELF64` — Emits a zero-dependency Linux x86_64 AVX2 ELF64 executable (628 B – 1,037 B) using linear-scan YMM register allocation.
- **`rul_trace`** (`White-Box Inspector`): `(rls_source: string) -> NodeTraceRow[0..N-1]` — Returns exact per-node min, max, sum/trues, NaN/Inf count, and sample[0..4] telemetry across every SSA instruction.
- **`rul_cas_intrinsics`** (`64-Bit FNV-1a CAS`): `(op: sort | hash_join | group_by | simd_scan) -> CasHash` — Executes verified I64/U8 content-addressed kernels (sort, hash_join, group_by, simd_scan_byte) in RulCasStore.

---

## 6. Roadmap from v0.4.0 to `v1.0` General-Purpose Systems Language

### v0.1.0 → v0.4.0 — 29-Opcode Columnar SSA-DAG Core, White-Box Tracer & Linear-Scan AVX2 ELF64 AOT (Shipped Production Baseline)
Proved the 16-byte binary instruction format, single-pass O(N) verifier (~5.8 ns/node), 3-tier execution engine, rul-mcp server, and zero-LLVM native Linux ELF64 compiler (~6.4 µs) on real hardware.
- 64-byte RulHeader, 16-byte ArenaDescriptor, 16-byte ProofEntry, and 16-byte NodeFrame across 29 opcodes.
- Lossless .rls <-> .rl symbolic assembler, standalone rul CLI, rul-bench, and 6-tool rul-mcp server.
- Linear-scan YMM register allocator (ymm2..ymm13) achieving 51.53 GB/s (4.72x over C) on 80 MB arrays.

### v0.5 — General-Purpose Control Flow, Functions & Composite Data Types (Milestone 1 (Months 1–2))
Expand the 16-byte instruction set beyond numeric arrays to support general scalars, structs, enums, UTF-8 strings, hash maps, conditional branches, and termination-proven loops.
- First-class i64, i32, u8, f32, fixed-layout structs, algebraic tagged unions, validated UTF-8 strings, and arena hash maps.
- SelectBranch: conditional branching requiring both branches to merge at an identical memory version state (checked in O(1)).
- RegionLoop & Call: bounded loops with ProofEntry termination fuel/variant witnesses and modular functions verified without whole-program inlining.

### v0.6 – v0.7 — Rust-Grade Heap Ownership & Struct Lifetimes in O(N) Time (Milestone 2 (Months 2–3))
Generalize 32-bit TokenOp versions and 16-byte ProofEntry witnesses from flat arrays to region-based heap allocations and struct field borrows.
- Deterministic region heap allocation and deallocation tied to linear ownership tokens with zero GC and zero malloc/free fragmentation.
- Sidecar ProofEntry witnesses for disjoint struct field mutations and zero-copy sub-slice lifetimes checked in O(1) per instruction.
- Full protection against use-after-free, double-free, and aliasing without multi-second borrow-checker constraint solving.

### v0.8 – v0.9 — Go-Style Deterministic Concurrency & Capability-Gated OS I/O (Milestone 3 (Months 4–5))
Introduce lightweight tasks, ownership-transferring channels, and fine-grained header capability bits governing file, network, and process syscalls.
- Sending a buffer over a typed channel performs an AffineConsume on the sender token and transfers ownership to the receiver — preventing data races at load time without a GC.
- Extend 64-bit RulHeader.capability_mask to gate filesystem reads/writes, network sockets, timers, and subprocesses.
- A .rl binary with CAP_NONE (0x0) is mathematically blocked from making any network or disk call before execution starts.

### v1.0 — Multi-Architecture Native Backends (x86_64, ARM64, WASI) & Formal Soundness Proofs (Milestone 4 (Month 6))
Emit standalone executables across Linux, macOS, Windows, and WebAssembly without LLVM, backed by Kani model checking and a 50-program v1.0 conformance suite.
- Zero-LLVM native code generation for x86_64 and AArch64 (ARM64) across Linux, macOS, and Windows, plus deterministic WASI modules.
- Bounded model-checking proofs (Kani) and continuous differential fuzzing across the binary decoder, O(N) verifier, and native codegen.
- Frozen .rl v1.0 binary specification and public 50-program conformance test suite.

---

## 7. Frequently Asked Engineering Questions (AEO Reference)

### Q: What is Rul (.rl) and why does it use a 16-byte binary format instead of human text?
AI thinks in numbers and CPUs run binary — yet languages like C, Go, and Rust force AI to type out thousands of human words and wait seconds for a compiler (rustc/LLVM) to translate that text back into binary. Rul (.rl) deletes the human text middleman: AI agents emit fixed 16-byte (128-bit) binary bricks carrying the Algorithm, CPU Schedule, and Memory Safety Ticket up front — eliminating text parsing (0 ms) and compiling standalone Linux ELF64 executables in ~6.4 µs.

### Q: How does Rul verify Rust-grade memory safety in ~5.8 ns per instruction without a slow borrow checker?
Think of every memory buffer (Arena) as a room with a numbered version ticket starting at version 1. Multiple instructions can read version 1 at the same time using a shared ReadLease (0b01). When an instruction modifies the buffer in-place via AffineConsume (0b10), it checks that the buffer is mutable and bumps the room to version 2. Any later instruction holding a stale version 1 ticket is rejected at the door in O(1) time during a single forward pass (~5.78 ns/node) — no multi-second borrow-checker solver required.

### Q: If humans do not write .rl binary files by hand, how do engineering teams debug and maintain Rul systems?
Humans stay 100% in control without typing binary — just as doctors read X-rays without drawing them by hand: (1) Humans set the rules up front — engineers define data schemas (ArenaDescriptor), hardware permission switches (64-bit CapabilityMask), and acceptance checks (AssertContract), while AI regenerates the verified .rl binary in microseconds; (2) Instant readable text via `rul decompile` converts any .rl file back into symbolic .rls assembly; (3) X-ray inspection via `rul trace` prints the exact min, max, sum, NaN/Inf count, and sample[0..4] values at every instruction step.

### Q: Why is the Rul toolchain implemented in Rust if Rul is designed to replace human text languages for AI agents?
Every new systems language requires an initial host language for its bootstrap compiler — just as the first C compiler was written in assembly and the first Rust compiler was written in OCaml. We built the Rul verifier, 3-tier execution engine, and native ELF64 compiler in dependency-free Rust under #![forbid(unsafe_code)]. Once the standalone `rul` binary is installed, users and AI agents verify, compile, and run .rl programs directly without needing rustc, Cargo, or LLVM.

### Q: How does Rul achieve 51.53 GB/s (4.72x faster than hand-written C) by mutating a single byte?
In Rul, hardware scheduling (Byte 2: schedule_hint) is orthogonal to algorithm logic (Byte 0: opcode). On an 80 MB (10,000,000 f64) filter-square-sum pipeline, single-core Rul (`0x11 SimdStream`) fuses all operations into 1,024-element L1-cache tiles in AVX2 YMM registers, running in 5.91 ms vs. 7.32 ms for hand-written 8-accumulator C (1.24x faster). Mutating Byte 2 from 0x11 to 0x12 (`MultiCore`) parallelizes those L1 tiles across all CPU cores (3.19 ms, 2.29x), and enabling `ArenaZoneMap` block min/max metadata skips cold tiles in O(1) to finish in 1.55 ms (51.53 GB/s, 4.72x faster than 1-core C and 45.51x faster than imperative AoS).

### Q: Can Rul replace Rust and Go for general-purpose backend and systems software?
Yes — that is the exact target of the four-milestone v1.0 roadmap: Milestone 1 (v0.5) adds i64/i32/u8/f32, structs, tagged unions, UTF-8 strings, hash maps, O(1)-verified SelectBranch conditionals, and termination-proven RegionLoop iteration; Milestone 2 (v0.6–0.7) extends TokenOp and ProofEntry to region-based heap allocations and struct field borrows; Milestone 3 (v0.8–0.9) introduces Go-style lightweight tasks and ownership-transferring channels plus fine-grained CapabilityMask OS syscalls; Milestone 4 (v1.0) delivers zero-LLVM native backends for x86_64, ARM64, and WASI backed by Kani formal soundness proofs.