플레이그라운드
(리스펙스)
KOENRU

검증된 바이트코드 실행하기

Core IR을 검증된 바이트코드로 컴파일합니다. 내장 Rust 가상 머신이나 정확히 설치한 토파즈 가상 머신에서 실행한 뒤 둘을 비교합니다.

규칙과 입력 준비하기

다음을 refund-window.lspx로 저장하세요.

LISPEX
(define (decide days)
  (if (<= days 30) 'refund 'review))

(decide input)

입력 datum 하나는 request.lspx로 저장합니다.

LISPEX
14

input은 파일이나 환경 변수를 몰래 읽는 기능이 아닙니다. Core IR과 바이트코드에 요구사항으로 기록되는 값이며, 아래 명령에서 직접 전달합니다.

Core IR을 만들고 바이트코드로 내리기

SH
lispex core-ir build \
  --source refund-window.lspx \
  --out refund-window.lpxir

lispex bytecode build \
  --ir refund-window.lpxir \
  --out refund-window.lpxbc

첫 명령은 규칙을 실행하지 않고 이름, 셀, 캡처, 꼬리 위치, 소스 위치를 해석합니다. 둘째 명령은 그 Core IR을 lispex.bytecode/v1로 내리고, 결과를 검증한 뒤 새 바이너리 파일로 씁니다. 두 명령 모두 기존 파일을 덮어쓰지 않습니다.

실행 전에 살펴보거나 검증하기

SH
lispex bytecode inspect --bytecode refund-window.lpxbc
lispex bytecode validate --bytecode refund-window.lpxbc

inspect는 식별자, 상한이 있는 테이블 수, 입력 요구사항, opcode 수, 루트 소스 위치, source-map 범위를 보여줍니다. validate는 자동화에 알맞은 더 간결한 경계입니다. 엄격하게 읽고 검증한 다음 다시 인코딩합니다. 이 형식이 허용하는 바이트 표현은 단 하나뿐이고 그것만 받아들입니다.

두 명령은 정규 바이트코드 무결성을 성립시킵니다. 서명된 배포가 제작자를 식별하고 애플리케이션 정책이 규칙을 승인하며 바우치가 소비자 요청과 현재 결정을 결속합니다.

검증 뒤에만 실행하기

SH
lispex bytecode run \
  --bytecode refund-window.lpxbc \
  --input request.lspx

OUTPUT
refund

네이티브 CLI는 가상 머신 상태를 만들기 전에 아티팩트 전체를 검증합니다. 잘못된 바이트는 입력 사용, 출력, 프리미티브 호출, 가상 머신의 첫 단계보다 먼저 거부됩니다. 아티팩트가 input을 요구하면 --input을 반드시 주어야 합니다. 요구하지 않는 아티팩트에 입력을 억지로 넣어도 실패합니다.

표준입력 하나로 바이트코드와 입력을 동시에 읽을 수는 없습니다.

SH
lispex bytecode run --bytecode - --input -

이 경우에는 둘 중 하나를 이름 있는 파일로 바꾸세요.

같은 산출물을 토파즈 가상 머신에서 실행하기

Rust는 내장되어 있고 계속 기본값입니다. macOS ARM64에서는 승인된 토파즈 5.11 설치 제품을 명시적으로 고를 수 있습니다.

SH
lispex bytecode run \
  --engine topaz \
  --topaz-vm /absolute/path/to/aarch64-apple-darwin \
  --bytecode refund-window.lpxbc \
  --input request.lspx

제품 루트는 별도로 설치한 lispex-topaz-vm/v1의 절대 경로여야 합니다. 리스펙스는 매니페스트, 토파즈 아티팩트, 실행 파일, 래퍼, 관리 파일, 컴파일러·소스 계보, 대상, 자원 계약, 대체 실행 0회를 검사합니다. PATH, 옆 저장소, 네트워크, 예전 설치본을 찾지 않습니다. 제품이 없거나 바뀌었거나 시간 제한을 넘거나 잘못된 결과를 내면 토파즈 실패가 그대로 드러납니다. Rust로 다시 실행하지 않습니다.

소스에서 가상 머신 직접 선택하기

외부 입력이 필요 없는 소스라면 짧은 형태를 쓸 수 있습니다.

SH
lispex run --backend rust --engine vm rule.lspx

기본 엔진은 계속 tree입니다.

SH
lispex run --backend rust --engine tree rule.lspx

명시적으로 vm을 골랐는데 실패하면 tree로 다시 시도하지 않습니다. --engine은 Rust 백엔드에서만 쓸 수 있습니다. LIL이나 LIT 같은 다른 백엔드, 또는 외부 백엔드 목록과 함께 쓰면 사용법 오류입니다.

두 Rust 엔진 비교하기

SH
lispex compare-engines \
  --receipt tree-vm.json \
  rule.lspx

덮어쓰지 않는 보고서에는 정확한 소스·Core IR·바이트코드 식별자, 두 의미 관측, 불일치 축, 가상 머신 자원 측정값, 대체 실행 횟수가 들어갑니다. 보고서는 공유 Rust 값과 primitive leaf를 식별하고 이름 붙은 source와 요청의 회귀 근거로 사용됩니다.

두 바이트코드 가상 머신을 직접 비교하려면 다음 명령을 사용합니다.

SH
lispex compare-vms \
  --topaz-vm /absolute/path/to/aarch64-apple-darwin \
  --receipt rust-topaz.json \
  rule.lspx

바이트코드는 한 번만 만들고 Rust와 토파즈를 각각 실행합니다. 상태, 출력, 값, 경고, 진단, 자원 관측, 완료한 root를 비교합니다. 보고서는 구조가 분리된 토파즈 source와 토파즈 Rust Stage 0 producer 식별자를 차분 경로 근거로 함께 기록합니다.

미리 컴파일해 둔 제품까지 만들었다면 네 가지 실행 방식을 함께 비교합니다.

SH
lispex compare-routes \
  --topaz-vm /absolute/path/to/aarch64-apple-darwin \
  --aot-product /absolute/path/to/refund-window-aot \
  --receipt four-routes.json \
  --input request.lspx \
  refund-window.lspx

이 명령은 한 번의 프런트엔드 결과와 한 검증 바이트코드를 tree, Rust 가상 머신, 토파즈 가상 머신, 미리 컴파일해 둔 제품에 사용합니다. 컴파일한 제품의 소스·Core IR·바이트코드가 다르면 어느 것도 실행하기 전에 거부합니다. 덮어쓰지 않는 영수증은 의미 축과 비교 가능한 자원 축을 따로 기록하고 모든 계보와 대체 실행 여부를 드러냅니다. 바우치는 아래 source 결속 compiled artifact를 사용합니다.

제품별 지원 고르기

제품실행 역할
macOS ARM64 네이티브바이트코드 도구와 내장 Rust 가상 머신과 정확한 토파즈 가상 머신과 미리 컴파일해 둔 제품과 네 방식 비교
그 밖의 지원 네이티브바이트코드 도구와 내장 Rust 가상 머신
npm CLI와 패키지소스 tree 실행과 정확한 이미지 기능
공개 WebAssembly 빌드소스 tree 실행과 정확한 이미지 기능
플레이그라운드대화형 소스 tree 실행과 정확한 이미지 기능

네이티브가 바이트코드 reader와 verifier와 가상 머신을 소유합니다. 다른 제품은 각자의 소스 tree와 정확한 이미지 흐름을 소유합니다.

검증된 바이트코드를 바우치에 더하기

바이트코드 해시는 정확한 바이트를 가리킵니다. 검증은 설정한 자원값에서 구조적 허용성을 성립시키고 로컬 가상 머신 실행은 네이티브 관측을 기록합니다. 바우치는 source 결속 container를 통해 발급자 인증과 수신자 정책과 source·input 결속과 현재 tree·Meaning 일치와 결정 게이트를 더합니다.

기존 바우치 검사에 가상 머신의 일치까지 의도적으로 더하려면 네이티브에서 소스 결속 전용 컨테이너를 만듭니다.

SH
lispex vouch compiled build \
  --source refund-window.lspx \
  --out refund-window.lpxvca

lispex vouch compiled validate \
  --artifact refund-window.lpxvca \
  --source refund-window.lspx

vouch verify --reexecute --compiled-artifact refund-window.lpxvca와 vouch gate --compiled-artifact refund-window.lpxvca는 소비자가 밖에서 제공한 정확한 소스·입력, 신뢰 정책, 인증, 그리고 tree 실행과 의미 기록의 현재 일치를 모두 요구합니다. 네이티브는 검증된 가상 머신을 실행하기 전에 그 소스에서 Core IR과 바이트코드를 다시 유도합니다. container와 hash와 검사 출력과 가상 머신 결과는 살아 있는 바우치 흐름에서 각자의 역할을 유지합니다.

다음으로

정확한 바이너리와 검증 계약은 레퍼런스에서 확인하세요. 컴파일 전에 해석된 의미를 살피고 싶다면 Core IR 가이드로 돌아가세요.

바이트코드와 Rust 가상 머신 레퍼런스 · 미리 컴파일해 둔 제품 만들기 · 네이티브 CLI

검증된 바이트코드 실행하기 · 리스펙스