← 워크벤치 SPECIFICATION · .RL v0.4 v0.4.0 DOI: 10.5281/zenodo.23722094

Rul (.rl) v0.4 바이너리 사양서 — 128비트 ISA 및 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 프로그램은 직접 제로카피 메모리 매핑(mmap)을 위해 16바이트 및 64바이트 경계에 정렬된 플랫 바이너리 .rl 이미지입니다. 코어 실행 엔진에는 텍스트 렉서나 AST 파서가 전혀 포함되어 있지 않습니다.

1. 바이너리 우선 (Binary-First)

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바이트, 캐시 라인 정렬)

바이트 오프셋	필드	타입	설명
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 길이)
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바이트)

알고리즘 레인 (무엇을 계산할지: Opcode / 피연산자) 스케줄 레인 (어떻게 실행할지: 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: 중간 힙 할당 없이 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	마스크 제외 레인을 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)	일치하는 요소를 연속으로 패킹하는 스트림 컴팩션.
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가 보증하는 인증된 간접 인덱스 수집(Gather).
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)

4가지 단일 패스 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에 일치하는 비트가 있어야 하며, 없으면 실행 전에 거부됩니다.