바이트코드, 검증기, 네이티브 VM

제품 파이프라인

정확한 소스
  -> reader와 위생적 normalizer
  -> lispex.core-ir/v1
  -> 결정적 바이트코드 compiler
  -> lispex.bytecode/v1
  -> strict reader와 verifier
  -> lispex-rust-vm/v1
  -> 기존 리스펙스 outcome·출력·경고·진단

이 흐름은 기존 lispex-profile-1.5를 컴파일합니다. 문법, datum, 내장 프로시저, 주변 I/O, 의미 프로필을 추가하지 않습니다. tree 인터프리터는 계속 Rust 의미 레퍼런스이자 기본 엔진입니다.

고정 식별자

헤더는 정확한 소스 식별자, Core IR 해시, 프리미티브 registry tag와 해시, 프로필, 명령·source-map·비용 식별자, 제작자, 정렬된 요구사항을 결속합니다. 제품 버전은 도구가 보고하지만 안정적인 의미 바이트에는 넣지 않습니다.

아티팩트 식별자는 다음과 같습니다.

SHA-256("lispex/bytecode-hash/v1" || 0x00 || canonical-bytecode-bytes)

제작자 표지는 출처 정보이지 신뢰 승인이 아닙니다.

정규 바이너리 봉투

바이너리는 8바이트 magic/version prefix 하나, 고정 section 수, 오름차순의 알려진 section tag, 각 payload 앞의 big-endian u32 길이로 구성됩니다. padding과 trailer는 없습니다.

허용되는 section 순서는 하나뿐입니다.

identity
strings
constants
anchors
bindings
globals
scopes
functions
guards
blocks
roots

색인과 개수는 big-endian u32입니다. 텍스트는 바이트 길이가 앞에 붙은 정확한 UTF-8입니다. 문자열, 상수, 소스 위치, ID, 테이블 참조에는 각각 하나의 정규 순서와 표현만 있습니다. strict reader는 메모리 할당 전에 상한을 확인하고 checked arithmetic을 쓰며 UTF-8과 모든 typed table을 검사합니다. 마지막에는 다시 인코딩해 원본과 바이트 단위로 같아야 합니다.

명령 계열

block은 선형 명령열입니다. jump operand는 byte offset이 아니라 해독된 명령 색인입니다. 소스 순서를 보존하며 constant folding, dead-code 제거, 재정렬, inlining, 수치 재결합, 새로운 tail 추론을 하지 않습니다. Core IR이 이미 해석해 둔 계약을 그대로 옮깁니다.

검증 순서

상수, global, closure, 입력, VM 상태가 생기기 전에 verifier는 다음을 순서대로 확인합니다.

1. magic과 section, 길이, 정규 인코딩, 고정 식별자 전부
2. 정렬되어 있고 중복이 없는 pool, 정확한 datum 표기, 빈틈없이 이어지는 ID, table의 역할, 모든 참조
3. 프리미티브와 global의 identity, 어휘 가시성, forwarding overlay, 함수가 포획한 값, guard 서술자, 소스 위치
4. 도달 가능한 제어 흐름, 허용된 jump 대상, stack과 결과 모양, scope 균형, 분기 합류점, 마지막 자리의 꼬리 호출, 빠짐없는 return
5. 명령마다 매기는 비용과 전체 자원 상한

알 수 없는 opcode, 끊어진 참조, 비정규 상수, 맞지 않는 merge, 남은 stack, scope 불균형, 빠진 return, 도달 불가능한 명령은 모두 닫힌 채로 거부합니다. 검증은 구조적 허용성만 성립시킬 뿐, 의미 동등성이나 제작자 신뢰를 증명하지 않습니다.

고정 상한과 자원 모델

• 아티팩트 크기는 최대 32 MiB
• 주요 pool과 table은 각각 최대 100,000개
• 가변 길이 operand 목록은 각각 최대 100,000개
• 정적 검증 작업은 checked instruction·edge 수에 대한 선형 작업

실행된 명령, 프리미티브 dispatch, 게스트 프로시저 transition에는 모두 버전된 음이 아닌 비용이 있습니다. 실행 결과는 선택된 한도, 사용 transition, 출력 바이트, 명시적 제어 frame 최고치, 완료 root, 금지된 폴백 횟수를 기록합니다. 출력 상한은 프리미티브 효과와 top-level 자동 출력의 정확한 순서 전체에 적용됩니다.

자원 고갈은 catch할 수 있는 리스펙스 condition이 아니라 엔진 실패입니다. tree 재귀 깊이와 VM transition은 서로 다른 호스트 자원 프로필이므로, 의미가 같다고 숫자 한도까지 같지는 않습니다.

소스 맵과 진단

모든 명령에는 Core IR에서 물려받은 양의 행·열 소스 위치가 하나씩 붙습니다. 경로, 호스트 이름, 시각, 플랫폼 개행은 저장하지 않습니다. 실행 오류는 현재 명령 위치를 사용하므로 tree/VM 비교는 진단 코드, 위치, 메시지, 부분 출력, 경고를 의미 축으로 함께 검사할 수 있습니다.

Rust VM 실행 모델

VM은 code activation, lexical scope, return frame, handler, guard 상태, wind 상태, 일회성 연속을 명시적으로 관리합니다. 꼬리 호출은 호스트 호출 stack을 늘리지 않고 현재 activation을 교체합니다. closure는 dynamic definition의 forwarding overlay를 포함한 공유 mutable cell을 유지합니다.

현재 프리미티브 205행 전부를 dispatch할 수 있습니다. 일반 프리미티브 잎은 설치된 Rust의 값, 수, aggregate, rendering, 진단, writer 코드를 공유합니다. 게스트 프로시저를 호출하는 18개 내장 프로시저는 mapping, fold, apply, call-with-values, exception handler, 연속, dynamic-wind를 포함해 VM 자체의 반복 상태 기계로 실행합니다. tree 인터프리터로 들어가지 않습니다.

따라서 VM은 tree 엔진과 실행 구조가 다르지만 같은 Rust 제품 계보입니다. 차등 실행 경로이지 네 번째 독립 백엔드 계보가 아닙니다.

정확한 토파즈 VM 경계

선택적 토파즈 경로는 토파즈로 작성한 별도의 strict reader, verifier, 명시적 제어 VM으로 같은 정규 바이트를 소비합니다. 정확한 토파즈 5.11 제품 루트를 별도로 설치한 macOS ARM64 네이티브에서만 사용할 수 있습니다.

실행 전에는 provider manifest, 토파즈 artifact, 실행 파일, wrapper, 관리 파일, 소스·compiler 계보, 대상, 프리미티브 registry, 0인 폴백 카운터 5개가 모두 정확한지 검사합니다. 닫힌 요청은 소스·Core IR·바이트코드·선택 입력, full u64 transition 한도, 구조 한도, 제품 identity를 결속합니다. private staging은 0700입니다. 자식 프로세스는 고정 시스템 PATH와 C 로케일만 있는 초기화된 환경을 받습니다. 프로세스 출력과 결과 JSON에는 상한과 시간 제한이 있습니다.

결과도 요청 해시, invocation, identity, 정규 10진수 u64, status/exit, 출력 계산, 구조 수, 대상, 계보, 폴백 0을 다시 검사하기 전에는 신뢰하지 않습니다. PATH, 저장소, 네트워크, Rust/tree/LIL/LIT 재시도, 예전 토파즈 폴백은 없습니다.

정적 토파즈 AOT 갈래

AOT는 미리 컴파일해 두는 방식으로, 실행 전에 규칙을 독립 실행 프로그램으로 만들어 두어 실행 시점에는 아무것도 컴파일하지 않습니다. macOS ARM64 네이티브는 검증된 제어 그래프를 읽을 수 있는 토파즈 소스로 내릴 수 있습니다. 정확히 설치한 토파즈 5.11 compiler와 Rust tool proxy를 쓰면 소스 없는 실행 파일까지 만들 수 있습니다. 설치 제품은 소스, Core IR, 바이트코드, 생성 소스 번들, source map, topaz.artifact.v1, 실행 파일, producer, 대상, 자원 요청, 그리고 0인 폴백 카운터 5개를 결속합니다. 실행 때 바이트코드를 읽거나 다른 엔진에 접속하지 않습니다.

이는 전체 프로필 정확성 경로이지 최적화한 호출 규약이나 compiler 의미 보존 증명이 아닙니다. lispex aot build|inspect|validate|run을 사용하고 정확한 설치 제품 흐름은 미리 컴파일해 둔 제품 만들기를 보세요.

엔진 선택과 비교

• lispex run --backend rust의 기본값은 --engine tree입니다.
• --engine vm은 메모리 안에서 source → Core IR → bytecode → verify → VM 흐름을 수행합니다.
• 선택한 VM에서 compile·검증·자원·실행 오류가 나도 tree로 폴백하지 않습니다.
• LIL과 LIT는 백엔드 계보이며 --engine으로 내부 엔진을 고를 수 없습니다.
• lispex compare-engines --receipt FILE SOURCE는 정확한 중간 식별자와 의미 불일치 축을 lispex.rust-engine-comparison/v1에 기록합니다.
• lispex bytecode run --engine topaz --topaz-vm ROOT --bytecode FILE은 정확히 설치한 토파즈 제품을 고릅니다.
• lispex compare-vms --topaz-vm ROOT --receipt FILE SOURCE는 바이트코드를 한 번 만들고 lispex.topaz-vm-comparison/v1에 Rust/토파즈 불일치 축을 기록합니다.

보고서는 덮어쓰지 않는 진단 자료입니다. 실행하거나 권한으로 승격할 수 없습니다.

제품 지원

미지원 제품은 JavaScript로 바이너리 형식을 흉내 내거나 다른 엔진으로 조용히 낮추지 않습니다.

무결성은 정확한 재유도로만 바우치에 들어갑니다

바이트코드가 정규이고 검증을 통과했다는 사실은 컴파일러의 의미 보존, 제작자 인증, 규칙 승인, 소비자의 입력 선택, 현재 여러 계보의 합의, 게이트 통과를 증명하지 않습니다. 바우치 권한의 뿌리는 계속 정확한 소스, 또는 그 소스를 복원하는 완전히 증명된 리스펙스 이미지입니다. 일반 바이트코드 바이트, 해시, 검사·검증 보고서, VM 결과, tree/VM 비교 보고서는 바우치 입력이 아닙니다.

네이티브는 그 정확한 소스에서 lispex.vouch-compiled-artifact/v1을 명시적으로 만들 수 있습니다. 컴파일 바우치 호출은 요청을 인증하고 고정한 뒤, 산출물의 Core IR과 바이트코드를 그 소스에서 다시 유도하고, 현재 tree/Meaning 일치를 유지한 다음에야 검증된 Rust VM 실행 기록을 비교합니다. 컨테이너는 소스나 입력을 대신할 수 없습니다. 검사·검증·재실행·게이트 보고서도 살아 있는 근거를 만들지 못합니다.

일반 토파즈 VM 경로는 이 체인 밖에 있습니다. 요청·결과·해시·실행 파일 식별자·출력·비교 영수증은 컴파일 바우치 산출물, 재실행 관측, 살아 있는 근거, 게이트 통과가 될 수 없습니다.

다음으로

명령과 복구 흐름은 가이드에서 따라 하고, 해석된 입력 계약은 Core IR 레퍼런스에서 확인하세요.

검증된 바이트코드 실행하기 · Core IR 계약 · 검사된 표면