소스부터 결과까지 이어지는 예제는 검증된 바이트코드 실행하기에서 따라 하세요.
예제의 refund-window.lpxbc에는 명령이 들어갑니다.
검사와 비교 JSON은 그 파일이나 실행 결과를 설명합니다.
검사 보고서 읽기
가이드의 환불 규칙을 bytecode inspect로 검사하면 보고서에 다음 필드가 나옵니다.
{
"requirements": ["explicit-input"],
"source_map_coverage": {
"complete": true,
"mapped_instructions": 22,
"referenced_anchors": 11,
"schema": "lispex.bytecode-source-map/v1",
"total_anchors": 11,
"total_instructions": 22
}
}이 파일은 명시적 입력을 요구합니다. 명령 22개 모두에 소스 위치가 있으며 서로 다른 위치 11개를 참조합니다. 앵커는 원래 소스의 행과 열을 뜻합니다.
전체 보고서에는 소스와 Core IR과 바이트코드의 식별자, 테이블별 개수, 종류별 명령 수, 루트 위치도 있습니다.
루트는 최상위 표현식입니다.
보고서에는 execution: "not-run"과 authority: "integrity-only"가 표시됩니다.
bytecode validate는 엄격하게 읽고 검증하고 다시 인코딩한 뒤 valid: true를 반환합니다.
컴파일과 식별자
네이티브는 소스를 읽고 축약 문법을 Core 형식으로 바꾼 뒤 lispex.core-ir/v1에서 이름의 참조를 정합니다.
바이트코드 컴파일러는 그 파일을 lispex.bytecode/v1으로 바꿉니다.
리스펙스 VM이 실행하기 전에 읽기 도구와 검증기가 바이트코드를 검사합니다.
이 과정은 lispex-profile-1.5의 문법, 데이터 종류, 내장 프로시저와 언어 동작을 구현합니다.
리스펙스 인터프리터는 기준 구현이며 소스 실행의 기본 엔진입니다.
| 항목 | 식별자 |
|---|---|
| 바이트코드 스키마 | 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 |
| 언어 프로파일 | lispex-profile-1.5 |
| 입력 Core IR | lispex.core-ir/v1 |
| 내장 프로시저 목록 | lispex.primitive-registry/v1 |
헤더에는 정확한 소스와 Core IR의 식별자, 내장 프로시저 목록의 태그와 해시, 언어 프로파일이 들어갑니다. 명령과 소스 맵과 비용 모델과 생성 도구의 식별자, 정렬된 입력 요구사항도 기록합니다. 도구의 보고서는 제품 버전을 이 고정 식별자와 함께 기록합니다. 생성 도구 식별자는 수신자 정책에서 사용할 컴파일 출처를 나타냅니다.
바이트코드 식별자는 다음 해시 도메인을 사용합니다.
SHA-256("lispex/bytecode-hash/v1" || 0x00 || canonical-bytecode-bytes)정규 형식은 정확한 소스 식별자를 포함한 모든 기록 정보의 바이트 표현을 하나로 정합니다. 결과가 같은 프로그램도 소스와 바이트코드의 식별자는 다를 수 있습니다.
바이너리 인코딩
파일은 8바이트의 형식·버전 접두어와 고정 섹션 수로 시작합니다.
알려진 섹션 태그는 오름차순이어야 합니다.
각 내용 앞에는 빅 엔디언 u32로 바이트 길이를 기록하며 채움 바이트나 꼬리 데이터는 없습니다.
빅 엔디언은 가장 큰 자릿값의 바이트를 먼저 쓰는 방식입니다.
섹션 순서는 다음과 같이 고정됩니다.
identity
strings
constants
anchors
bindings
globals
scopes
functions
guards
blocks
roots색인과 개수는 빅 엔디언 u32 값입니다.
텍스트는 바이트 길이와 정확한 UTF-8로 기록합니다.
문자열과 상수, 앵커와 ID, 참조에는 각각 정해진 순서와 표현이 있습니다.
읽기 도구는 메모리 할당 전에 한도를 확인하며 계산의 오버플로도 검사합니다. UTF-8과 각 테이블의 타입을 확인합니다. 이어서 파일을 다시 인코딩하고 원본과 바이트 단위로 같은지 확인합니다.
명령과 검증
| 계열 | 명령 |
|---|---|
| 값과 접근 | constant, load-lexical, load-global, load-primitive, make-closure, require-one, discard, make-values |
| 변경과 범위 | 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 |
블록에는 명령이 순서대로 들어갑니다. 점프는 바이트 위치 대신 해독한 명령의 색인을 가리킵니다. 컴파일러는 소스 순서와 Core IR의 참조와 꼬리 호출 위치를 유지합니다. 상수 접기, 도달하지 않는 코드 제거, 재정렬, 인라인화, 수치 재결합, 꼬리 위치 재추론은 수행하지 않습니다.
검증기는 실행용 상수와 전역 변수, 클로저와 입력 바인딩, VM 상태를 만들기 전에 다음을 순서대로 확인합니다.
- 형식 접두어, 섹션, 길이, 정규 인코딩과 고정 식별자
- 중복 없이 정렬한 공유 데이터 모음, 정확한 데이터 표기, 연속 ID, 테이블 역할과 참조
- 내장 프로시저와 전역 변수 ID, 이름이 보이는 범위, 전달 셀, 함수 캡처, 예외 처리 영역과 소스 위치
- 도달 가능한 제어 흐름, 점프 대상, 스택과 결과의 형태, 범위 균형, 분기 합류점, 마지막 꼬리 호출과 완전한 반환
- 명령별 비용과 전체 자원 한도
캡처는 함수가 보관하는 바깥 변수의 셀입니다. 전달 셀은 실행 중 활성화한 정의와 참조를 연결합니다. 예외 처리 영역은 guard 서술자에 기록합니다. 분기 합류점에서는 들어오는 스택과 범위 상태가 맞아야 합니다.
알 수 없는 명령 코드, 끊어진 참조, 정규 형식이 아닌 상수, 잘못된 합류점은 거부합니다. 남은 스택 값, 맞지 않는 범위, 빠진 반환, 도달 불가능한 명령도 거부합니다. 검증은 구조의 유효성을 확인합니다. 서명된 배포는 제작자를 식별하고 엔진 비교는 실행 결과의 일치를 기록합니다.
자원 한도와 진단
| 항목 | 한도나 계산 규칙 |
|---|---|
| 바이트코드 파일 | 최대 32 MiB |
| 주요 데이터 모음이나 테이블 | 각각 최대 100,000개 |
| 가변 길이 피연산자 리스트 | 각각 최대 100,000개 |
| 정적 검증 작업 | 명령과 제어 흐름 연결 수에 비례하는 작업량 검사 |
| 실행 작업 | 명령 실행과 내장 프로시저 호출과 게스트 프로시저 전환에 버전별 음이 아닌 비용 적용 |
게스트 프로시저는 리스펙스 프로그램에서 정의한 프로시저입니다. 실행 보고서는 선택한 한도, 사용한 전환 수, 출력 바이트, 제어 프레임 최고치, 완료한 루트, 금지된 대체 실행 횟수를 기록합니다. 출력 한도는 내장 프로시저의 출력과 최상위 자동 출력에 실행 순서대로 적용됩니다. 자원이 고갈되면 엔진은 종료합니다. tree 재귀 깊이와 VM 전환 수에는 서로 다른 자원 프로파일을 사용합니다.
각 명령에는 Core IR의 양수 행·열 위치가 붙습니다. 호출 애플리케이션은 경로, 호스트 이름, 시각, 플랫폼 개행을 기록합니다. 실행 오류는 현재 명령의 소스 위치를 사용합니다. 따라서 tree와 VM을 비교할 때 진단 코드와 위치와 메시지, 부분 출력과 경고를 함께 볼 수 있습니다.
리스펙스 VM 실행
VM은 실행 중인 코드, 지역 범위, 반환 위치, 예외 처리기, guard와 dynamic-wind 상태를 명시적으로 관리합니다.
일회성 연속도 지원합니다.
꼬리 호출은 호스트 호출 스택을 늘리지 않고 현재 실행 기록을 교체합니다.
클로저는 동적 정의의 전달 셀을 포함한 변경 가능한 셀을 공유합니다.
내장 프로시저 205개를 모두 호출할 수 있습니다.
일반 내장 프로시저는 값과 수, 복합 값, 표시와 진단과 쓰기에 Rust 코드를 공유합니다.
게스트 프로시저를 호출하는 내장 프로시저 18개는 VM의 반복 상태 기계로 실행합니다.
여기에는 매핑, 접기, apply, call-with-values, 예외 처리기, 연속, dynamic-wind가 포함됩니다.
리스펙스 인터프리터는 이 프로시저의 기준 구현을 사용합니다.
tree와 VM은 같은 Rust 제품 계열에 속합니다. 두 엔진의 비교는 그 계열 안에서 서로 다른 실행 방식의 결과를 기록합니다.
엔진 선택과 비교
| 선택이나 명령 | 동작과 출력 |
|---|---|
run --backend rust | 기본값 --engine tree |
run --backend rust --engine vm | 메모리에서 컴파일하고 검증한 뒤 실행 |
compare-engines --receipt FILE SOURCE | lispex.rust-engine-comparison/v1에 tree와 VM 결과 기록 |
선택한 VM에서 실패하면 다른 방식으로 바꾸지 않고 해당 실행 결과를 반환합니다. 실행 엔진 참조에서 현재 리스펙스 실행과 LIL/LIT 퇴역을 설명합니다. 비교 보고서는 새 경로에 전체를 한 번에 저장합니다.
네이티브 플랫폼은 바이트코드 도구와 리스펙스 VM을 제공합니다. npm과 공개 WASM과 플레이그라운드는 소스 tree 실행과 리스펙스 이미지 기능을 제공합니다. 플랫폼별 내용은 제품 카탈로그에서 확인하세요.
리스펙스 바우치의 컴파일된 바이트코드
리스펙스 바우치는 csk.checked-profile/v1이 받는 소스로 lispex.vouch-compiled-artifact/v1을 만듭니다.
다음 전체 소스를 vouch-rule.lspx로 저장한 뒤 묶음을 만들고 검증하세요.
(if (exact-integer? input) (decision-approve) (decision-deny))lispex vouch compiled build --source vouch-rule.lspx --out vouch-rule.lpxvca
lispex vouch compiled validate --artifact vouch-rule.lpxvca --source vouch-rule.lspx두 명령의 종료값은 0입니다.
첫 명령은 vouch-rule.lpxvca를 만들고 lispex.vouch-compiled-artifact-build/v1 보고서를 출력합니다.
둘째 명령은 다음 필드가 있는 검증 보고서를 출력합니다.
{
"compiled_artifact_validation": "lispex.vouch-compiled-artifact-validation/v1",
"derivation": "exact-source",
"execution": "not-run",
"valid": true
}가이드의 환불 소스는 csk.checked-profile/v1에 맞지 않습니다.
이 소스를 빌드 명령에 전달하면 compiled-artifact-source-invalid와 종료값 1을 반환합니다.
컴파일 묶음을 준비할 때는 이 프로파일에 맞게 소스를 작성하세요.
컴파일된 바우치 요청에는 정확한 외부 소스와 소비자 입력을 유지합니다. 정규 리스펙스 이미지에서도 소스를 복원할 수 있습니다. 발급자 인증, 수신자 정책, 요청 연결, 엔진 일치, 결정 게이트에는 각각 별도 기록이 있습니다.
vouch verify --reexecute와 vouch gate의 --compiled-artifact 옵션으로 이 묶음을 선택합니다.
네이티브는 요청을 인증하고 고정한 뒤 소스에서 Core IR과 바이트코드를 다시 만듭니다.
현재 tree와 Meaning의 일치를 확인하고 검증된 리스펙스 VM의 실행 기록을 비교합니다.
검사와 검증, 재실행과 게이트 보고서는 각 단계의 결과를 담습니다.
컴파일된 바우치 흐름은 소비자의 정확한 소스에서 만든 리스펙스 VM 결과 파일을 사용합니다.