Especificación binaria de Rul (.rl) v0.4 — ISA de 128 bits y verificador O(N)
Especificación oficial del diseño binario de Rul (.rl) v0.4: RulHeader de 64 bytes, ArenaDescriptor de 16 bytes, ProofEntry de 16 bytes, NodeFrame de 128 bits en 29 opcodes y reglas de verificación lineal O(N).
[0x01] CORE EQUATION
Artifact (.rl) = Algorithm + Schedule + Proof
Todo programa ejecutable de Rul es una imagen binaria plana .rl alineada en límites de 16 y 64 bytes para mapeo directo en memoria sin copia (mmap). El motor de ejecución central no contiene analizadores léxicos ni árboles AST de texto.
1. Primero el binario
Conversión bidireccional sin pérdidas .rls <-> .rl en ~8,8 µs en la frontera mediante src/transpiler.rs.
2. SSA-DAG topológico
Cada nodo de instrucción i solo puede referenciar operandos estrictamente < i, garantizando la terminación.
3. Separación Seguridad e Intención
La capa 1 demuestra seguridad de memoria y límites en 5,78 ns/nodo; la capa 2 verifica AssertContract y rul trace.
[0x02] SECTION 1 OF .RL
RulHeader (64 bytes, alineado a línea de caché)
| OFFSET DE BYTE | CAMPO | TIPO | DESCRIPCIÓN |
|---|---|---|---|
| 0..8 | magic | [u8; 8] | Firma mágica canónica: b"RUL\x00\x01\x00\x00\x00" |
| 8..16 | graph_hash | u64 | Hash de integridad FNV-1a de 64 bits sobre las secciones Arena, Proof y Node |
| 16..24 | capability_mask | u64 | Máscara de sandbox de E/S de hardware (0x00 = Cómputo puro, 0x01 = NetRing, 0x02 = StorageDMA, 0x04 = GpuDispatch) |
| 24..28 | arena_count | u32 | Número de entradas ArenaDescriptor de 16 bytes |
| 28..32 | proof_count | u32 | Número de certificados de límites ProofEntry de 16 bytes |
| 32..36 | node_count | u32 | Número de instrucciones NodeFrame de 128 bits (16 bytes) |
| 36..40 | output_node | u32 | Índice basado en 0 del nodo SSA de salida principal |
| 40..64 | reserved | [u8; 24] | Relleno de ceros que alinea la cabecera a una línea de caché de CPU de 64 bytes |
[0x03] SECTIONS 2 & 3 OF .RL
ArenaDescriptor (16 bytes) y ProofEntry (16 bytes)
| OFFSET DE BYTE | ArenaDescriptor | TIPO | DESCRIPCIÓN |
|---|---|---|---|
| 0..4 | arena_id | u32 | Identificador de Arena columnar (0 .. arena_count - 1) |
| 4..8 | element_count | u32 | Longitud de columna homogénea (Longitud Shape) |
| 8 | type_lane | u8 | Tipo de elemento y ancho de carril SIMD (p. ej. 0x18 = f64x8) |
| 9 | mutability | u8 | 0 = Entrada inmutable | 1 = Región mutable lineal |
| 10..12 | alignment | u16 | Requisito de alineación en bytes (64 bytes para AVX-512 / línea de caché) |
| 12..16 | initial_version | u32 | Versión inicial de AffineToken (empieza en 1) |
| OFFSET DE BYTE | ProofEntry | TIPO | DESCRIPCIÓN |
|---|---|---|---|
| 0..2 | rule_kind | u16 | 1 = SliceBounds (lo <= hi <= len) | 2 = GatherIndexInBounds (max_idx <= target_len) |
| 2..4 | target_arena | u16 | ID de Arena destino estrictamente vinculado al origin_arena del operando |
| 4..8 | bound_lo | u32 | Límite inferior de índice no negativo |
| 8..12 | bound_hi | u32 | Límite superior <= effective_target_len |
| 12..16 | witness_node | u32 | Nodo de índice SSA testigo (in_b para Gather) |
[0x04] SECTION 4 OF .RL
Diseño de NodeFrame de 128 bits (16 bytes)
Carril de Algoritmo (Qué calcular: Opcode / Operandos) Carril de Planificación (Cómo ejecutar: SIMD / Multinúcleo) Carril de Prueba (Seguridad: Ticket de versión / Límites)
NODE #3 ($n3) node $n3 = Mul f64x8 fg=1 pol=simd proof=0 tok=pure a=$n0 b=$n0
16 BYTES = 128 BITSDESGLOSE DEL REGISTRO DE 8 BITS · 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
Campo: schedule_hint Tipo: u8
✓ Invariante del verificador O(N) comprobado al cargar (~5.78 ns) (fusion_group << 4) | exec_policy
Byte de planificación de hardware ortogonal: mutar 0x11 (SimdStream) -> 0x12 (MultiCore) cambia la ejecución de la CPU sin alterar las pruebas de seguridad.
Nodo #3: Cuadrado vectorial de 8 carriles elemento por elemento ($n0 * $n0) fusionado en registros de caché L1 sin asignaciones intermedias en el heap.
[0x05] 29-OPCODE ISA (v0.4.0)
Conjunto completo de 29 instrucciones (ISA v0.4.0)
| HEX | OPCODE | CATEGORÍA | SEMÁNTICA | DESCRIPCIÓN |
|---|---|---|---|---|
| 0x01 | ArenaInput | Memory & Arena | ArenaDescriptor[in_a] -> Column | Carga una rebanada columnar desde ArenaDescriptor[in_a] con ReadLease. |
| 0x02 | ConstF64 | Memory & Arena | in_a | (in_b << 32) -> Scalar f64 | Constante escalar de coma flotante IEEE-754 de 64 bits inmediata. |
| 0x03 | ArenaSlice | Memory & Arena | Slice(in_a, ProofEntry[proof_idx]) -> Column | Sub-rebanada sin copia de la columna in_a certificada por ProofEntry. |
| 0x04 | ArenaMutate | Memory & Arena | Mutate(Arena[in_a], in_b) -> ver + 1 | Mutación lineal in situ consumiendo AffineToken (ver -> ver + 1). |
| 0x10 | Add | Arithmetic & Math | out[i] = a[i] + b[i] | Suma SIMD elemento por elemento (VADDPD). |
| 0x11 | Sub | Arithmetic & Math | out[i] = a[i] - b[i] | Resta SIMD elemento por elemento (VSUBPD). |
| 0x12 | Mul | Arithmetic & Math | out[i] = a[i] * b[i] | Multiplicación SIMD elemento por elemento (VMULPD). |
| 0x13 | Div | Arithmetic & Math | out[i] = a[i] / b[i] | División SIMD IEEE-754 elemento por elemento (VDIVPD). |
| 0x14 | CmpGt | Predicate & Mask | mask[i] = a[i] > b[i] | Máscara de predicado «mayor que» sin saltos (VCMPPD). |
| 0x15 | SelectZero | Predicate & Mask | out[i] = mask[i] ? val[i] : 0.0 | Selección por predicado sin saltos que pone a cero los carriles filtrados (VANDPD). |
| 0x16 | Min | Arithmetic & Math | out[i] = min(a[i], b[i]) | Mínimo elemento por elemento sin saltos (VMINPD). |
| 0x17 | Max | Arithmetic & Math | out[i] = max(a[i], b[i]) | Máximo elemento por elemento sin saltos (VMAXPD). |
| 0x18 | CmpLt | Predicate & Mask | mask[i] = a[i] < b[i] | Máscara de predicado «menor que» sin saltos. |
| 0x19 | CmpEq | Predicate & Mask | mask[i] = a[i] == b[i] | Máscara de predicado de igualdad sin saltos. |
| 0x1A | Abs | Arithmetic & Math | out[i] = |a[i]| | Valor absoluto sin saltos limpiando el bit de signo IEEE-754. |
| 0x1B | Sqrt | Arithmetic & Math | out[i] = sqrt(a[i]) | Raíz cuadrada SIMD por hardware (VSQRTPD). |
| 0x1C | Floor | Arithmetic & Math | out[i] = floor(a[i]) | Redondeo sin saltos hacia -Infinito (VROUNDPD). |
| 0x1D | Ceil | Arithmetic & Math | out[i] = ceil(a[i]) | Redondeo sin saltos hacia +Infinito (VROUNDPD). |
| 0x1E | Ln | Arithmetic & Math | out[i] = ln(a[i]) | Logaritmo natural elemento por elemento. |
| 0x1F | Exp | Arithmetic & Math | out[i] = exp(a[i]) | Exponencial natural elemento por elemento. |
| 0x20 | FilterCompact | Reduction & Compaction | Compact(mask=in_a, vals=in_b) | Compactación de flujo que empaqueta elementos coincidentes de forma contigua. |
| 0x21 | ReduceSum | Reduction & Compaction | sum(in_a) -> Scalar f64 | Reducción horizontal de suma de 8 acumuladores a un escalar. |
| 0x22 | ReduceMax | Reduction & Compaction | max(in_a) -> Scalar f64 | Reducción horizontal del máximo a un escalar. |
| 0x23 | Gather | Reduction & Compaction | target[indices[i]] (proof_idx > 0) | Recolección indexada indirecta certificada por ProofEntry. |
| 0x24 | ReduceMin | Reduction & Compaction | min(in_a) -> Scalar f64 | Reducción horizontal del mínimo a un escalar. |
| 0x25 | MaskAnd | Predicate & Mask | mask[i] = a[i] && b[i] | Conjunción bit a bit de máscaras booleanas (AND). |
| 0x26 | MaskOr | Predicate & Mask | mask[i] = a[i] || b[i] | Disyunción bit a bit de máscaras booleanas (OR). |
| 0x30 | RingEnqueue | Hardware & Contract | Enqueue(in_a) [Requires CAP_NET_RING] | Salida a búfer en anillo de hardware controlada por permisos (CAP_NET_RING). |
| 0x40 | AssertContract | Hardware & Contract | Assert(!is_nan(in_a) && is_finite(in_a)) | Contrato de dominio en tiempo de ejecución que verifica una salida finita y sin NaN. |
[0x06] STATIC VERIFICATION (~5.78 NS/NODE)
Cuatro reglas de verificación lineal O(N) en un solo pase
1. Regla topológica SSA
Todo nodo en el índice i debe satisfacer in_a < i e in_b < i, impidiendo matemáticamente cualquier ciclo.
2. Conservación lineal de la propiedad de memoria
ReadLease(a, ver) comprueba live_version[a] == ver. AffineConsume(a, ver) comprueba la mutabilidad e incrementa live_version[a] mediante checked_add(1).
3. Prueba de límites vinculada al origen
ArenaSlice y Gather verifican ProofEntry.target_arena == origin_arena y bound_lo <= bound_hi <= effective_target_len.
4. CapabilityMask de confianza cero
Los opcodes de E/S de hardware (0x30 RingEnqueue) requieren el bit correspondiente en RulHeader.capability_mask o son rechazados antes de la ejecución.