← Bancada SPECIFICATION · .RL v0.4 v0.4.0 DOI: 10.5281/zenodo.23722094

Especificação Binária Rul (.rl) v0.4 — ISA de 128 Bits & Verificador O(N)

Especificação oficial de layout binário do Rul (.rl) v0.4: RulHeader de 64 bytes, ArenaDescriptor de 16 bytes, ProofEntry de 16 bytes, NodeFrame de 128 bits em 29 opcodes e regras de verificação O(N) em passagem única.

[0x01] CORE EQUATION

Artifact (.rl) = Algorithm + Schedule + Proof

Todo programa Rul executável é uma imagem binária plana .rl alinhada em limites de 16 e 64 bytes para mapeamento direto de memória zero-copy (mmap). O motor central de execução contém zero analisadores léxicos textuais ou parsers de AST.

1. Binário em Primeiro Lugar

Conversão bidirecional sem perdas .rls <-> .rl em ~8.8 µs na fronteira via src/transpiler.rs.

2. SSA-DAG Topológico

Cada nó de instrução i só pode referenciar operandos estritamente < i, garantindo a terminação.

3. Divisão Segurança + Intenção

A Camada 1 prova a segurança de memória/limites em 5.78 ns/nó; a Camada 2 verifica AssertContract & rul trace.

[0x02] SECTION 1 OF .RL

RulHeader (64 Bytes, Alinhado à Linha de Cache)

OFFSET DE BYTE	CAMPO	TIPO	DESCRIÇÃO
0..8	magic	[u8; 8]	Assinatura mágica canônica: b"RUL\x00\x01\x00\x00\x00"
8..16	graph_hash	u64	Hash de integridade FNV-1a de 64 bits sobre as seções Arena, Proof e Node
16..24	capability_mask	u64	Máscara de sandbox de E/S de hardware (0x00 = Computação Pura, 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 limites ProofEntry de 16 bytes
32..36	node_count	u32	Número de instruções NodeFrame de 128 bits (16 bytes)
36..40	output_node	u32	Índice baseado em 0 do nó SSA de saída principal
40..64	reserved	[u8; 24]	Preenchimento com zeros alinhando o cabeçalho à linha de cache de CPU de 64 bytes

[0x03] SECTIONS 2 & 3 OF .RL

ArenaDescriptor (16 Bytes) & ProofEntry (16 Bytes)

OFFSET DE BYTE	ArenaDescriptor	TIPO	DESCRIÇÃO
0..4	arena_id	u32	Identificador de Arena colunar (0 .. arena_count - 1)
4..8	element_count	u32	Comprimento de coluna homogênea (Shape Length)
8	type_lane	u8	Tipo de elemento & largura de faixa SIMD (ex. 0x18 = f64x8)
9	mutability	u8	0 = Entrada Imutável \| 1 = Região Mutável Linear
10..12	alignment	u16	Requisito de alinhamento de bytes (64 bytes para AVX-512 / linha de cache)
12..16	initial_version	u32	Versão inicial de AffineToken (começa em 1)

OFFSET DE BYTE	ProofEntry	TIPO	DESCRIÇÃO
0..2	rule_kind	u16	1 = SliceBounds (lo <= hi <= len) \| 2 = GatherIndexInBounds (max_idx <= target_len)
2..4	target_arena	u16	ID da Arena alvo estritamente vinculado ao origin_arena do operando
4..8	bound_lo	u32	Limite inferior de índice não negativo
8..12	bound_hi	u32	Limite superior <= effective_target_len
12..16	witness_node	u32	Nó SSA de índice testemunha (in_b para Gather)

[0x04] SECTION 4 OF .RL

Layout NodeFrame de 128 Bits (16 Bytes)

Faixa de Algoritmo (O que calcular: Opcode / Operandos) Faixa de Escalonamento (Como rodar: SIMD / MultiCore) Faixa de Prova (Segurança: Bilhete de Versão / Limites)

NODE #3 ($n3) node $n3 = Mul f64x8 fg=1 pol=simd proof=0 tok=pure a=$n0 b=$n0

16 BYTES = 128 BITS

ANÁLISE DO REGISTRADOR 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 do Verificador O(N) Checado no Carregamento (~5.78 ns) (fusion_group << 4) | exec_policy

Byte ortogonal de escalonamento de hardware: mutar 0x11 (SimdStream) -> 0x12 (MultiCore) altera a execução da CPU sem alterar as provas de segurança.

Nó #3: Quadrado vetorial elemento a elemento de 8 vias ($n0 * $n0) fusionado em registradores de cache L1 com zero alocação no heap.

[0x05] 29-OPCODE ISA (v0.4.0)

Conjunto Completo de Instruções de 29 Opcodes

HEX	OPCODE	CATEGORIA	SEMÂNTICA	DESCRIÇÃO
0x01	ArenaInput	Memory & Arena	ArenaDescriptor[in_a] -> Column	Carrega fatia colunar de ArenaDescriptor[in_a] com ReadLease.
0x02	ConstF64	Memory & Arena	in_a \| (in_b << 32) -> Scalar f64	Constante escalar imediata de ponto flutuante IEEE-754 de 64 bits.
0x03	ArenaSlice	Memory & Arena	Slice(in_a, ProofEntry[proof_idx]) -> Column	Sub-fatia zero-copy da coluna in_a certificada por ProofEntry.
0x04	ArenaMutate	Memory & Arena	Mutate(Arena[in_a], in_b) -> ver + 1	Mutação linear in-place consumindo AffineToken (ver -> ver + 1).
0x10	Add	Arithmetic & Math	out[i] = a[i] + b[i]	Adição SIMD elemento a elemento (VADDPD).
0x11	Sub	Arithmetic & Math	out[i] = a[i] - b[i]	Subtração SIMD elemento a elemento (VSUBPD).
0x12	Mul	Arithmetic & Math	out[i] = a[i] * b[i]	Multiplicação SIMD elemento a elemento (VMULPD).
0x13	Div	Arithmetic & Math	out[i] = a[i] / b[i]	Divisão SIMD IEEE-754 elemento a elemento (VDIVPD).
0x14	CmpGt	Predicate & Mask	mask[i] = a[i] > b[i]	Máscara de predicado maior-que sem ramificação (VCMPPD).
0x15	SelectZero	Predicate & Mask	out[i] = mask[i] ? val[i] : 0.0	Seleção predicada sem ramificação zerando faixas mascaradas (VANDPD).
0x16	Min	Arithmetic & Math	out[i] = min(a[i], b[i])	Mínimo elemento a elemento sem ramificação (VMINPD).
0x17	Max	Arithmetic & Math	out[i] = max(a[i], b[i])	Máximo elemento a elemento sem ramificação (VMAXPD).
0x18	CmpLt	Predicate & Mask	mask[i] = a[i] < b[i]	Máscara de predicado menor-que sem ramificação.
0x19	CmpEq	Predicate & Mask	mask[i] = a[i] == b[i]	Máscara de predicado de igualdade sem ramificação.
0x1A	Abs	Arithmetic & Math	out[i] = \|a[i]\|	Valor absoluto sem ramificação limpando o bit de sinal IEEE-754.
0x1B	Sqrt	Arithmetic & Math	out[i] = sqrt(a[i])	Raiz quadrada SIMD em hardware (VSQRTPD).
0x1C	Floor	Arithmetic & Math	out[i] = floor(a[i])	Arredondamento sem ramificação em direção a -Infinito (VROUNDPD).
0x1D	Ceil	Arithmetic & Math	out[i] = ceil(a[i])	Arredondamento sem ramificação em direção a +Infinito (VROUNDPD).
0x1E	Ln	Arithmetic & Math	out[i] = ln(a[i])	Estêncil de logaritmo natural elemento a elemento.
0x1F	Exp	Arithmetic & Math	out[i] = exp(a[i])	Estêncil exponencial natural elemento a elemento.
0x20	FilterCompact	Reduction & Compaction	Compact(mask=in_a, vals=in_b)	Compactação de fluxo empacotando elementos correspondentes de forma contígua.
0x21	ReduceSum	Reduction & Compaction	sum(in_a) -> Scalar f64	Redução horizontal de soma de 8 acumuladores para escalar.
0x22	ReduceMax	Reduction & Compaction	max(in_a) -> Scalar f64	Redução horizontal de máximo para escalar.
0x23	Gather	Reduction & Compaction	target[indices[i]] (proof_idx > 0)	Coleta indexada indireta certificada apoiada por ProofEntry.
0x24	ReduceMin	Reduction & Compaction	min(in_a) -> Scalar f64	Redução horizontal de mínimo para escalar.
0x25	MaskAnd	Predicate & Mask	mask[i] = a[i] && b[i]	Conjunção bit a bit de máscara booleana.
0x26	MaskOr	Predicate & Mask	mask[i] = a[i] \|\| b[i]	Disjunção bit a bit de máscara booleana.
0x30	RingEnqueue	Hardware & Contract	Enqueue(in_a) [Requires CAP_NET_RING]	Saída de buffer de anel de hardware controlada por capacidade.
0x40	AssertContract	Hardware & Contract	Assert(!is_nan(in_a) && is_finite(in_a))	Contrato de domínio em runtime verificando saída finita e não-NaN.

[0x06] STATIC VERIFICATION (~5.78 NS/NODE)

Quatro Regras de Verificação Linear O(N) em Passagem Única

1. Regra SSA Topológica

Cada nó no índice i deve satisfazer in_a < i e in_b < i, prevenindo ciclos matematicamente.

2. Conservação Linear de Posse

ReadLease(a, ver) verifica live_version[a] == ver. AffineConsume(a, ver) verifica mutabilidade e incrementa live_version[a] via checked_add(1).

3. Prova de Refinamento Vinculada à Origem

ArenaSlice e Gather verificam ProofEntry.target_arena == origin_arena e bound_lo <= bound_hi <= effective_target_len.

4. CapabilityMask Zero-Trust

Opcodes de E/S de hardware (0x30 RingEnqueue) exigem o bit correspondente em RulHeader.capability_mask ou são rejeitados antes da execução.