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

제품 파이프라인

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

이 흐름은 기존 lispex-profile-1.5를 컴파일하고 문법과 datum과 내장 프로시저와 의미론을 보존합니다. 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, 폴백 0건을 기록합니다. 출력 상한은 프리미티브 효과와 top-level 자동 출력의 정확한 순서 전체에 적용됩니다.

자원 고갈은 엔진의 종료 상태로 기록됩니다. 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을 검사한 뒤 결과를 받습니다. 닫힌 제품 선택은 오류를 선택한 토파즈 경로에 유지합니다.

정적 토파즈 AOT 갈래

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

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

엔진 선택과 비교

• lispex run --backend rust의 기본값은 --engine tree입니다.
• --engine vm은 메모리 안에서 source → Core IR → bytecode → verify → VM 흐름을 수행합니다.
• 선택한 VM의 compile·검증·자원·실행 오류는 선택한 VM 경로에서 반환됩니다.
• LIL과 LIT는 각 백엔드 계보를 통해 선택합니다.
• 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/토파즈 불일치 축을 기록합니다.

보고서는 새 경로에 원자적으로 게시하는 진단 자료입니다. 바우치는 소스에 결속한 별도 compiled artifact를 사용합니다.

제품 지원

각 제품은 문서화된 명령 상태를 반환하고 선택한 엔진을 유지합니다.

검증된 바이트코드가 바우치에 들어가는 방식

바우치는 정확한 소스나 그 소스를 복원하는 정규 리스펙스 이미지에서 컴파일 근거를 유도합니다. 제작자 인증, 수신자 정책, 소비자 입력, 엔진 일치, 결정 게이트는 흐름 안에서 각각 명시적 기록을 유지합니다.

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

토파즈 VM 경로는 요청, 결과, 해시, 실행 파일 식별자, 출력, 비교 영수증을 경로 근거로 공개합니다. 컴파일 바우치 경로는 소비자가 고정한 소스에서 유도한 Rust VM 아티팩트를 사용합니다.

다음으로

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

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