Rul (.rl) v0.4 二进制规范 — 128 位指令集与 O(N) 验证器
Rul (.rl) v0.4 官方二进制布局规范：64 字节 RulHeader、16 字节 ArenaDescriptor、16 字节 ProofEntry、涵盖 29 个操作码的 128 位 NodeFrame 以及单遍 O(N) 静态验证规则。
[0x01] CORE EQUATION
Artifact (.rl) = Algorithm + Schedule + Proof
每个可执行的 Rul 程序都是一个对齐在 16 字节和 64 字节边界上的平坦二进制 .rl 镜像，支持直接零拷贝内存映射 (mmap)。核心执行引擎不包含任何文本词法分析器或 AST 解析器。
1. 二进制优先
通过 src/transpiler.rs 在边界处以 ~8.8 µs 实现 .rls <-> .rl 无损双向转换。
2. 拓扑 SSA-DAG
每个指令节点 i 只能引用严格小于 i 的操作数，从数学上保证程序必然终止。
3. 安全与意图分离
第 1 层以 5.78 ns/节点证明内存与边界安全；第 2 层通过 AssertContract 与 rul trace 验证业务意图。
[0x02] SECTION 1 OF .RL
RulHeader（64 字节，CPU 缓存行对齐）
| 字节偏移 | 字段名 | 类型 | 说明 |
|---|---|---|---|
| 0..8 | magic | [u8; 8] | 标准魔数签名：b"RUL\x00\x01\x00\x00\x00" |
| 8..16 | graph_hash | u64 | 覆盖 Arena、Proof 和 Node 表的 64 位 FNV-1a 完整性哈希 |
| 16..24 | capability_mask | u64 | 硬件 I/O 沙箱掩码 (0x00 = 纯计算, 0x01 = NetRing, 0x02 = StorageDMA, 0x04 = GpuDispatch) |
| 24..28 | arena_count | u32 | 16 字节 ArenaDescriptor 条目的数量 |
| 28..32 | proof_count | u32 | 16 字节 ProofEntry 边界证书的数量 |
| 32..36 | node_count | u32 | 128 位（16 字节）NodeFrame 指令的数量 |
| 36..40 | output_node | u32 | 主输出 SSA 节点的从 0 开始的索引 |
| 40..64 | reserved | [u8; 24] | 将文件头对齐到 64 字节 CPU 缓存行的全零填充区 |
[0x03] SECTIONS 2 & 3 OF .RL
ArenaDescriptor（16 字节）与 ProofEntry（16 字节）
| 字节偏移 | ArenaDescriptor | 类型 | 说明 |
|---|---|---|---|
| 0..4 | arena_id | u32 | 列式内存池 Arena 标识符 (0 .. arena_count - 1) |
| 4..8 | element_count | u32 | 同质数据列的元素数量（几何形状长度 Shape Length） |
| 8 | type_lane | u8 | 元素类型与 SIMD 通道宽度（例如 0x18 = f64x8） |
| 9 | mutability | u8 | 0 = 不可变输入 | 1 = 线性可变内存区域 |
| 10..12 | alignment | u16 | 字节对齐要求（AVX-512 / 缓存行为 64 字节） |
| 12..16 | initial_version | u32 | 初始 AffineToken 版本号（从 1 开始） |
| 字节偏移 | ProofEntry | 类型 | 说明 |
|---|---|---|---|
| 0..2 | rule_kind | u16 | 1 = SliceBounds (lo <= hi <= len) | 2 = GatherIndexInBounds (max_idx <= target_len) |
| 2..4 | target_arena | u16 | 严格绑定到操作数起源内存池 origin_arena 的目标 Arena ID |
| 4..8 | bound_lo | u32 | 非负下界索引 |
| 8..12 | bound_hi | u32 | 上界索引 <= 目标列有效长度 effective_target_len |
| 12..16 | witness_node | u32 | 见证 SSA 索引节点（Gather 指令的 in_b） |
[0x04] SECTION 4 OF .RL
128 位 NodeFrame 指令帧布局（16 字节）
算法通道（算什么：操作码 / 操作数） 调度通道（怎么跑：SIMD / 多核并行） 证明通道（安全保障：版本票据 / 边界证书）
NODE #3 ($n3) node $n3 = Mul f64x8 fg=1 pol=simd proof=0 tok=pure a=$n0 b=$n0
16 BYTES = 128 BITS8 位寄存器比特分解 · 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
字段: schedule_hint 类型: u8
✓ 加载时检查的 O(N) 验证器不变量 (~5.78 ns) (fusion_group << 4) | exec_policy
正交硬件调度字节：将 0x11 (SimdStream) 突变为 0x12 (MultiCore) 可切换多核执行而不改变安全证明。
节点 #3: 在 L1 缓存寄存器中融合执行的逐元素 8 通道向量平方 ($n0 * $n0)，零中间堆内存分配。
[0x05] 29-OPCODE ISA (v0.4.0)
完整 29 操作码指令集 (v0.4.0)
| HEX | OPCODE | 类别 | 运算语义 | 说明 |
|---|---|---|---|---|
| 0x01 | ArenaInput | Memory & Arena | ArenaDescriptor[in_a] -> Column | 持 ReadLease 从 ArenaDescriptor[in_a] 加载列切片。 |
| 0x02 | ConstF64 | Memory & Arena | in_a | (in_b << 32) -> Scalar f64 | 直接嵌入指令帧的 64 位 IEEE-754 浮点标量常数。 |
| 0x03 | ArenaSlice | Memory & Arena | Slice(in_a, ProofEntry[proof_idx]) -> Column | 由 ProofEntry 认证的列 in_a 零拷贝子切片。 |
| 0x04 | ArenaMutate | Memory & Arena | Mutate(Arena[in_a], in_b) -> ver + 1 | 消耗 AffineToken 的线性原地修改（版本号 ver -> ver + 1）。 |
| 0x10 | Add | Arithmetic & Math | out[i] = a[i] + b[i] | 逐元素 SIMD 加法 (VADDPD)。 |
| 0x11 | Sub | Arithmetic & Math | out[i] = a[i] - b[i] | 逐元素 SIMD 减法 (VSUBPD)。 |
| 0x12 | Mul | Arithmetic & Math | out[i] = a[i] * b[i] | 逐元素 SIMD 乘法 (VMULPD)。 |
| 0x13 | Div | Arithmetic & Math | out[i] = a[i] / b[i] | 逐元素 IEEE-754 SIMD 除法 (VDIVPD)。 |
| 0x14 | CmpGt | Predicate & Mask | mask[i] = a[i] > b[i] | 无分支大于谓词掩码 (VCMPPD)。 |
| 0x15 | SelectZero | Predicate & Mask | out[i] = mask[i] ? val[i] : 0.0 | 无分支谓词选择，将未命中掩码的通道置零 (VANDPD)。 |
| 0x16 | Min | Arithmetic & Math | out[i] = min(a[i], b[i]) | 无分支逐元素最小值 (VMINPD)。 |
| 0x17 | Max | Arithmetic & Math | out[i] = max(a[i], b[i]) | 无分支逐元素最大值 (VMAXPD)。 |
| 0x18 | CmpLt | Predicate & Mask | mask[i] = a[i] < b[i] | 无分支小于谓词掩码。 |
| 0x19 | CmpEq | Predicate & Mask | mask[i] = a[i] == b[i] | 无分支等于谓词掩码。 |
| 0x1A | Abs | Arithmetic & Math | out[i] = |a[i]| | 通过清除 IEEE-754 符号位实现的无分支绝对值。 |
| 0x1B | Sqrt | Arithmetic & Math | out[i] = sqrt(a[i]) | 硬件 SIMD 平方根 (VSQRTPD)。 |
| 0x1C | Floor | Arithmetic & Math | out[i] = floor(a[i]) | 无分支向负无穷向下取整 (VROUNDPD)。 |
| 0x1D | Ceil | Arithmetic & Math | out[i] = ceil(a[i]) | 无分支向正无穷向上取整 (VROUNDPD)。 |
| 0x1E | Ln | Arithmetic & Math | out[i] = ln(a[i]) | 逐元素自然对数算子。 |
| 0x1F | Exp | Arithmetic & Math | out[i] = exp(a[i]) | 逐元素自然指数算子。 |
| 0x20 | FilterCompact | Reduction & Compaction | Compact(mask=in_a, vals=in_b) | 流式压缩，将匹配掩码 in_a 的元素连续打包。 |
| 0x21 | ReduceSum | Reduction & Compaction | sum(in_a) -> Scalar f64 | 8 累加器水平求和归约为标量。 |
| 0x22 | ReduceMax | Reduction & Compaction | max(in_a) -> Scalar f64 | 水平求最大值归约为标量。 |
| 0x23 | Gather | Reduction & Compaction | target[indices[i]] (proof_idx > 0) | 由 ProofEntry 担保的认证间接索引收集。 |
| 0x24 | ReduceMin | Reduction & Compaction | min(in_a) -> Scalar f64 | 水平求最小值归约为标量。 |
| 0x25 | MaskAnd | Predicate & Mask | mask[i] = a[i] && b[i] | 按位布尔掩码逻辑与 (AND)。 |
| 0x26 | MaskOr | Predicate & Mask | mask[i] = a[i] || b[i] | 按位布尔掩码逻辑或 (OR)。 |
| 0x30 | RingEnqueue | Hardware & Contract | Enqueue(in_a) [Requires CAP_NET_RING] | 受权限管控的硬件环形缓冲区输出 (需 CAP_NET_RING)。 |
| 0x40 | AssertContract | Hardware & Contract | Assert(!is_nan(in_a) && is_finite(in_a)) | 验证输出有限且非 NaN 的运行时域契约断言。 |
[0x06] STATIC VERIFICATION (~5.78 NS/NODE)
四项单遍 O(N) 线性静态验证规则
1. 拓扑 SSA 顺序规则
索引 i 处的每个节点必须满足 in_a < i 且 in_b < i，从数学上杜绝循环。
2. 线性内存所有权守恒
ReadLease(a, ver) 检查 live_version[a] == ver。AffineConsume(a, ver) 检查可变性并通过 checked_add(1) 递增版本号。
3. 绑定起源的边界精化证明
ArenaSlice 与 Gather 验证 ProofEntry.target_arena == origin_arena 且 bound_lo <= bound_hi <= effective_target_len。
4. 零信任硬件权限掩码 CapabilityMask
硬件 I/O 操作码 (0x30 RingEnqueue) 要求 RulHeader.capability_mask 中具备对应权限位，否则在执行前直接拒绝。