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

제품 파이프라인

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

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

고정 식별자

축	식별자
바이트코드 스키마	`lispex.bytecode/v1`
해시 도메인	`lispex/bytecode-hash/v1`
제작자	`lispex-rust-bytecode/v1`
명령 집합	`lispex.bytecode-instructions/v1`
소스 맵	`lispex.bytecode-source-map/v1`
비용 모델	`lispex.bytecode-cost/v1`
검증기	`lispex.bytecode-verifier/v1`
내장 VM 엔진	`lispex-rust-vm/v1`
승인된 외부 VM	`lispex-topaz-vm/v1`
Topaz 요청/결과	`lispex.bytecode-engine-request/v1` / `lispex.bytecode-engine-result/v1`
의미 프로필	`lispex-profile-1.5`
입력 Core IR	`lispex.core-ir/v1`
primitive registry	`lispex.primitive-registry/v1`

헤더는 정확한 소스 식별자, Core IR 해시, primitive-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을 검사합니다. 마지막에는 다시 인코딩해 원본과 바이트 단위로 같아야 합니다.

명령 계열

계열	명령
값과 접근	`constant`, `load-lexical`, `load-global`, `load-primitive`, `make-closure`, `require-one`, `discard`, `make-values`
변경과 scope	`set-lexical`, `set-global`, `define-lexical`, `define-global`, `enter-let`, `enter-recursive-scope`, `initialize-lexical`, `leave-scope`
제어	`jump`, `jump-if-false`, `call`, `tail-call`, `guard`, `return`

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

검증 순서

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

magic, section, 길이, 정규 인코딩, 모든 고정 식별자
정렬되고 중복 없는 pool, 정확한 datum rendering, 연속 ID, table role, 모든 참조
primitive/global identity, lexical visibility, forwarding overlay, function capture, guard descriptor, 소스 위치
도달 가능한 제어 흐름, 합법적인 jump target, stack·outcome 형태, scope 균형, branch join, terminal tail call, 완전한 return
명령 비용과 전체 자원 상한

알 수 없는 opcode, 끊어진 참조, 비정규 상수, 맞지 않는 merge, 남은 stack, scope 불균형, 빠진 return, 도달 불가능한 명령은 fail-closed 거부됩니다. 검증은 구조적 허용성만 세우며 의미 동등성이나 제작자 신뢰를 증명하지 않습니다.

고정 상한과 자원 모델

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

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

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

소스 맵과 진단

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

Rust VM 실행 모델

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

현재 primitive 205행 전부를 dispatch할 수 있습니다. 일반 primitive leaf는 설치된 Rust의 값, 수, aggregate, rendering, 진단, writer 코드를 공유합니다. guest procedure를 호출하는 18개 primitive는 mapping, fold, apply, call-with-values, exception handler, continuation, dynamic-wind를 포함해 VM 자체의 반복 상태 기계로 실행합니다. tree evaluator로 들어가지 않습니다.

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

정확한 Topaz VM 경계

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

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

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

정적 Topaz AOT 갈래

macOS ARM64 네이티브는 검증된 제어 그래프를 읽을 수 있는 Topaz 소스로 내리고, 정확히 설치한 Topaz 5.11 compiler와 Rust tool proxy로 소스 없는 실행 파일을 만들 수도 있습니다. 설치 제품은 소스·Core IR·바이트코드·생성 소스 bundle·source map·topaz.artifact.v1·실행 파일·producer·대상·자원 요청·폴백 0 다섯 개를 결속합니다. 실행 때 바이트코드를 읽거나 다른 엔진에 접속하지 않습니다.

이는 전체 프로필 정확성 경로이지 최적화 ABI나 compiler 의미 보존 증명이 아닙니다. lispex aot build|inspect|validate|run을 사용하고 정확한 설치 제품 흐름은 Topaz AOT 가이드를 보세요.

엔진 선택과 비교

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

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

제품 지원

표면	바이트코드 도구	Rust VM	Topaz VM	Topaz AOT
macOS ARM64 네이티브	지원	내장	정확한 별도 제품	정확한 설치 도구
그 밖의 네이티브	지원	내장	미지원	미지원
npm CLI·패키지 API	미지원	미지원	미지원	미지원
공유 공개 WASM	미지원	미지원	미지원	미지원
플레이그라운드	미지원	미지원	미지원	미지원

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

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

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

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

일반 Topaz VM 경로는 이 체인 밖에 있습니다. 요청·결과·해시·실행 파일 identity·출력·비교 영수증은 컴파일 Vouch 산출물, 재실행 관측, evidence handle, gate grant가 될 수 없습니다.

다음으로

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

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