Бинарная спецификация Rul (.rl) v0.4 — 128-битная ISA и O(N) верификатор
Официальная спецификация бинарного формата Rul (.rl) v0.4: 64-байтный RulHeader, 16-байтный ArenaDescriptor, 16-байтный ProofEntry, 128-битный NodeFrame (29 опкодов) и однопроходная O(N) верификация.
[0x01] CORE EQUATION
Artifact (.rl) = Algorithm + Schedule + Proof
Каждая исполняемая программа Rul представляет собой плоский бинарный образ .rl, выровненный по границам 16 и 64 байт для прямого отображения в память без копирования (mmap). Ядро выполнения не содержит текстовых лексеров или парсеров AST.
1. Приоритет бинарного кода
Двустороннее преобразование без потерь .rls <-> .rl за ~8.8 мкс на границе через src/transpiler.rs.
2. Топологический SSA-DAG
Каждый узел инструкции i может ссылаться только на операнды строго < i, что гарантирует завершение.
3. Разделение безопасности и замысла
Уровень 1 доказывает безопасность памяти и границ за 5.78 нс/узел; Уровень 2 проверяет AssertContract и rul trace.
[0x02] SECTION 1 OF .RL
RulHeader (64 байта, выровнен по кэш-линии)
| СМЕЩЕНИЕ БАЙТ | ПОЛЕ | ТИП | ОПИСАНИЕ |
|---|---|---|---|
| 0..8 | magic | [u8; 8] | Каноническая магическая сигнатура: b"RUL\x00\x01\x00\x00\x00" |
| 8..16 | graph_hash | u64 | 64-битный хэш целостности FNV-1a по таблицам Arena, Proof и Node |
| 16..24 | capability_mask | u64 | Маска аппаратной песочницы ввода-вывода (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 | Индекс (с 0) основного выходного узла SSA |
| 40..64 | reserved | [u8; 24] | Заполненный нулями отступ, выравнивающий заголовок до 64-байтной кэш-линии CPU |
[0x03] SECTIONS 2 & 3 OF .RL
ArenaDescriptor (16 байт) и ProofEntry (16 байт)
| СМЕЩЕНИЕ БАЙТ | ArenaDescriptor | ТИП | ОПИСАНИЕ |
|---|---|---|---|
| 0..4 | arena_id | u32 | Идентификатор колоночной арены (0 .. arena_count - 1) |
| 4..8 | element_count | u32 | Количество элементов однородной колонки (длина Shape) |
| 8 | type_lane | u8 | Тип элемента и ширина канала SIMD (например, 0x18 = f64x8) |
| 9 | mutability | u8 | 0 = Неизменяемый вход | 1 = Линейная изменяемая область |
| 10..12 | alignment | u16 | Требование к выравниванию в байтах (64 байта для AVX-512 / кэш-линии) |
| 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 | Целевой ID арены, строго привязанный к origin_arena операнда |
| 4..8 | bound_lo | u32 | Неотрицательная нижняя граница индекса |
| 8..12 | bound_hi | u32 | Верхняя граница <= effective_target_len |
| 12..16 | witness_node | u32 | Индексный узел-свидетель SSA (in_b для инструкции Gather) |
[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 BITSПОБИТОВЫЙ РАЗБОР 8-БИТНОГО РЕГИСТРА · 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) меняет режим CPU без изменения доказательств безопасности.
Узел #3: Поэлементное 8-канальное векторное возведение в квадрат ($n0 * $n0) в регистрах кэша L1 без промежуточных аллокаций в куче.
[0x05] 29-OPCODE ISA (v0.4.0)
Полный набор из 29 инструкций (ISA v0.4.0)
| HEX | OPCODE | КАТЕГОРИЯ | СЕМАНТИКА | ОПИСАНИЕ |
|---|---|---|---|---|
| 0x01 | ArenaInput | Memory & Arena | ArenaDescriptor[in_a] -> Column | Загрузка колоночного среза из ArenaDescriptor[in_a] с билетом ReadLease. |
| 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 | Подсрез без копирования (zero-copy) колонки in_a, заверенный через ProofEntry. |
| 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] | Поэлементное SIMD-деление по стандарту IEEE-754 (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]) | Безветвевое округление к -Infinity (VROUNDPD). |
| 0x1D | Ceil | Arithmetic & Math | out[i] = ceil(a[i]) | Безветвевое округление к +Infinity (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] | Побитовая конъюнкция булевых масок (И). |
| 0x26 | MaskOr | Predicate & Mask | mask[i] = a[i] || b[i] | Побитовая дизъюнкция булевых масок (ИЛИ). |
| 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) проверяет изменяемость и увеличивает live_version[a] через checked_add(1).
3. Доказательство границ с привязкой к источнику
ArenaSlice и Gather проверяют ProofEntry.target_arena == origin_arena и условие bound_lo <= bound_hi <= effective_target_len.
4. Песочница нулевого доверия CapabilityMask
Опкоды аппаратного ввода-вывода (0x30 RingEnqueue) требуют соответствующего бита в RulHeader.capability_mask, иначе отклоняются до запуска.