Đặc Tả Nhị Phân Rul (.rl) v0.4 — Tập Lệnh 128-Bit & Bộ Kiểm Chứng O(N)
Đặc tả cấu trúc nhị phân chính thức của Rul (.rl) v0.4: RulHeader 64-byte, ArenaDescriptor 16-byte, ProofEntry 16-byte, NodeFrame 128-bit trên 29 opcode và quy tắc kiểm chứng tuyến tính O(N).
[0x01] CORE EQUATION
Artifact (.rl) = Algorithm + Schedule + Proof
Mọi chương trình Rul khả thi là một ảnh nhị phân phẳng .rl căn chỉnh trên ranh giới 16-byte và 64-byte để nạp trực tiếp zero-copy (mmap). Engine lõi không chứa bất kỳ bộ phân tích từ vựng (lexer) hay cây cú pháp (AST) văn bản nào.
1. Ưu Tiên Nhị Phân
Chuyển đổi hai chiều không suy hao giữa .rls và .rl chỉ mất ~8.8 µs qua src/transpiler.rs.
2. Đồ Thị SSA-DAG Topo
Mọi node i chỉ được tham chiếu in_a < i và in_b < i, loại bỏ hoàn toàn vòng lặp vô hạn ẩn.
3. Tách Biệt An Toàn & Ý Định
Tầng 1 kiểm chứng an toàn bộ nhớ trong 5.78 ns/node; Tầng 2 kiểm định hợp đồng AssertContract & rul trace.
[0x02] SECTION 1 OF .RL
RulHeader (64 Bytes, Căn Chỉnh Dòng Cache CPU)
| VỊ TRÍ BYTE | TRƯỜNG | KIỂU | MÔ TẢ CHI TIẾT |
|---|---|---|---|
| 0..8 | magic | [u8; 8] | Chữ ký định danh chuẩn: b"RUL\x00\x01\x00\x00\x00" |
| 8..16 | graph_hash | u64 | Mã băm toàn vẹn FNV-1a 64-bit trên toàn bộ bảng Arena, Proof và Node |
| 16..24 | capability_mask | u64 | Mặt nạ quyền phần cứng (0x00 = Tính toán thuần túy, 0x01 = NetRing, 0x02 = StorageDMA, 0x04 = GpuDispatch) |
| 24..28 | arena_count | u32 | Số lượng mục khai báo vùng nhớ ArenaDescriptor (16 byte/mục) |
| 28..32 | proof_count | u32 | Số lượng chứng chỉ biên trong bảng phụ ProofEntry (16 byte/mục) |
| 32..36 | node_count | u32 | Số lượng khung lệnh 128-bit (16-byte) trong bảng NodeFrame |
| 36..40 | output_node | u32 | Chỉ số (từ 0) của node SSA đầu ra chính |
| 40..64 | reserved | [u8; 24] | Vùng đệm toàn 0 căn chỉnh đúng ranh giới dòng cache CPU 64-byte |
[0x03] SECTIONS 2 & 3 OF .RL
ArenaDescriptor (16 Bytes) & ProofEntry (16 Bytes)
| VỊ TRÍ BYTE | ArenaDescriptor | KIỂU | MÔ TẢ CHI TIẾT |
|---|---|---|---|
| 0..4 | arena_id | u32 | Định danh vùng nhớ cột Arena (0 .. arena_count - 1) |
| 4..8 | element_count | u32 | Số phần tử của cột đồng nhất (Độ dài hình học Shape) |
| 8 | type_lane | u8 | Kiểu dữ liệu & số làn SIMD (ví dụ 0x18 = f64x8) |
| 9 | mutability | u8 | 0 = Đầu vào bất biến | 1 = Vùng khả biến tuyến tính |
| 10..12 | alignment | u16 | Yêu cầu căn chỉnh bộ nhớ (64 bytes cho AVX-512 / cache line) |
| 12..16 | initial_version | u32 | Phiên bản AffineToken khởi tạo của vùng nhớ (bắt đầu từ 1) |
| VỊ TRÍ BYTE | ProofEntry | KIỂU | MÔ TẢ CHI TIẾT |
|---|---|---|---|
| 0..2 | rule_kind | u16 | 1 = SliceBounds (lo <= hi <= len) | 2 = GatherIndexInBounds (max_idx <= target_len) |
| 2..4 | target_arena | u16 | ID của Arena đích, bắt buộc khớp với origin_arena của toán hạng |
| 4..8 | bound_lo | u32 | Cận dưới không âm của lát cắt |
| 8..12 | bound_hi | u32 | Cận trên <= chiều dài hiệu dụng của cột đích |
| 12..16 | witness_node | u32 | Node SSA nhân chứng chứa mảng chỉ số (in_b cho lệnh Gather) |
[0x04] SECTION 4 OF .RL
Cấu Trúc Khung Lệnh 128-Bit NodeFrame (16 Bytes)
Làn Thuật Toán (Làm gì: Opcode / Toán hạng) Làn Lịch Trình (Chạy thế nào: SIMD / Đa nhân) Làn Bằng Chứng (An toàn: Vé phiên bản / Biên)
NODE #3 ($n3) node $n3 = Mul f64x8 fg=1 pol=simd proof=0 tok=pure a=$n0 b=$n0
16 BYTES = 128 BITSGIẢI MÃ THANH GHI 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
Trường: schedule_hint Kiểu: u8
✓ Quy Tắc Kiểm Chứng O(N) Ngay Lúc Nạp File (~5.78 ns) (fusion_group << 4) | exec_policy
Byte lịch trình phần cứng độc lập: đổi 0x11 (SimdStream) -> 0x12 (MultiCore) giúp tăng tốc đa nhân mà không làm đổi bằng chứng an toàn.
Node #3: Nhân bình phương từng phần tử 8 làn vector ($n0 * $n0) hợp nhất ngay trong thanh ghi L1, không cấp phát bộ nhớ trung gian.
[0x05] 29-OPCODE ISA (v0.4.0)
Danh Mục Đầy Đủ 29 Lệnh (ISA v0.4.0)
| HEX | OPCODE | NHÓM LỆNH | NGỮ NGHĨA | MÔ TẢ CHI TIẾT |
|---|---|---|---|---|
| 0x01 | ArenaInput | Memory & Arena | ArenaDescriptor[in_a] -> Column | Nạp cột dữ liệu từ ArenaDescriptor[in_a] kèm khóa đọc ReadLease. |
| 0x02 | ConstF64 | Memory & Arena | in_a | (in_b << 32) -> Scalar f64 | Hằng số thực vô hướng IEEE-754 64-bit nhúng trực tiếp trong khung lệnh. |
| 0x03 | ArenaSlice | Memory & Arena | Slice(in_a, ProofEntry[proof_idx]) -> Column | Cắt lát con zero-copy từ cột in_a được chứng thực bởi ProofEntry. |
| 0x04 | ArenaMutate | Memory & Arena | Mutate(Arena[in_a], in_b) -> ver + 1 | Ghi đè tại chỗ tuyến tính, tiêu thụ AffineToken và nâng phiên bản (ver -> ver + 1). |
| 0x10 | Add | Arithmetic & Math | out[i] = a[i] + b[i] | Cộng từng phần tử theo làn SIMD (VADDPD). |
| 0x11 | Sub | Arithmetic & Math | out[i] = a[i] - b[i] | Trừ từng phần tử theo làn SIMD (VSUBPD). |
| 0x12 | Mul | Arithmetic & Math | out[i] = a[i] * b[i] | Nhân từng phần tử theo làn SIMD (VMULPD). |
| 0x13 | Div | Arithmetic & Math | out[i] = a[i] / b[i] | Chia từng phần tử chuẩn IEEE-754 theo làn SIMD (VDIVPD). |
| 0x14 | CmpGt | Predicate & Mask | mask[i] = a[i] > b[i] | Mặt nạ so sánh lớn hơn không rẽ nhánh (VCMPPD). |
| 0x15 | SelectZero | Predicate & Mask | out[i] = mask[i] ? val[i] : 0.0 | Chọn lọc không rẽ nhánh theo mặt nạ bit (VANDPD). |
| 0x16 | Min | Arithmetic & Math | out[i] = min(a[i], b[i]) | Tìm giá trị nhỏ nhất từng phần tử không rẽ nhánh (VMINPD). |
| 0x17 | Max | Arithmetic & Math | out[i] = max(a[i], b[i]) | Tìm giá trị lớn nhất từng phần tử không rẽ nhánh (VMAXPD). |
| 0x18 | CmpLt | Predicate & Mask | mask[i] = a[i] < b[i] | Mặt nạ so sánh nhỏ hơn không rẽ nhánh. |
| 0x19 | CmpEq | Predicate & Mask | mask[i] = a[i] == b[i] | Mặt nạ so sánh bằng không rẽ nhánh. |
| 0x1A | Abs | Arithmetic & Math | out[i] = |a[i]| | Giá trị tuyệt đối không rẽ nhánh bằng cách xóa bit dấu IEEE-754. |
| 0x1B | Sqrt | Arithmetic & Math | out[i] = sqrt(a[i]) | Căn bậc hai phần cứng SIMD (VSQRTPD). |
| 0x1C | Floor | Arithmetic & Math | out[i] = floor(a[i]) | Làm tròn xuống về -Infinity không rẽ nhánh (VROUNDPD). |
| 0x1D | Ceil | Arithmetic & Math | out[i] = ceil(a[i]) | Làm tròn lên về +Infinity không rẽ nhánh (VROUNDPD). |
| 0x1E | Ln | Arithmetic & Math | out[i] = ln(a[i]) | Logarit tự nhiên từng phần tử. |
| 0x1F | Exp | Arithmetic & Math | out[i] = exp(a[i]) | Hàm mũ tự nhiên e^x từng phần tử. |
| 0x20 | FilterCompact | Reduction & Compaction | Compact(mask=in_a, vals=in_b) | Nén dòng dữ liệu, gom liên tiếp các phần tử thỏa mặt nạ in_a. |
| 0x21 | ReduceSum | Reduction & Compaction | sum(in_a) -> Scalar f64 | Cộng dồn ngang 8 bộ tích lũy về giá trị vô hướng f64. |
| 0x22 | ReduceMax | Reduction & Compaction | max(in_a) -> Scalar f64 | Thu gọn tìm cực đại toàn cột về vô hướng f64. |
| 0x23 | Gather | Reduction & Compaction | target[indices[i]] (proof_idx > 0) | Truy cập gián tiếp theo mảng chỉ số được chứng thực bởi ProofEntry. |
| 0x24 | ReduceMin | Reduction & Compaction | min(in_a) -> Scalar f64 | Thu gọn tìm cực tiểu toàn cột về vô hướng f64. |
| 0x25 | MaskAnd | Predicate & Mask | mask[i] = a[i] && b[i] | Phép hội (AND) hai mặt nạ boolean. |
| 0x26 | MaskOr | Predicate & Mask | mask[i] = a[i] || b[i] | Phép tuyển (OR) hai mặt nạ boolean. |
| 0x30 | RingEnqueue | Hardware & Contract | Enqueue(in_a) [Requires CAP_NET_RING] | Đẩy kết quả ra ring buffer phần cứng (yêu cầu quyền CAP_NET_RING). |
| 0x40 | AssertContract | Hardware & Contract | Assert(!is_nan(in_a) && is_finite(in_a)) | Kiểm định hợp đồng miền giá trị: đảm bảo đầu ra hữu hạn và không phải NaN. |
[0x06] STATIC VERIFICATION (~5.78 NS/NODE)
Bốn Quy Tắc Kiểm Chứng Tuyến Tính 1 Lượt O(N)
1. Quy Tắc Thứ Tự Topo SSA
Mọi node ở chỉ số i bắt buộc thỏa mãn in_a < i và in_b < i, loại bỏ hoàn toàn chu trình bằng toán học.
2. Bảo Toàn Quyền Sở Hữu Tuyến Tính
ReadLease(a, ver) đối chiếu live_version[a] == ver. AffineConsume(a, ver) kiểm tra tính khả biến và tăng live_version[a] qua checked_add(1).
3. Chứng Chỉ Biên Gắn Chặt Cột Gốc
ArenaSlice và Gather xác thực ProofEntry.target_arena == origin_arena và bound_lo <= bound_hi <= effective_target_len.
4. Sandbox Phần Cứng CapabilityMask
Các lệnh I/O phần cứng (0x30 RingEnqueue) bắt buộc có bit quyền tương ứng trong RulHeader.capability_mask nếu không sẽ bị từ chối ngay lúc nạp.