제한 평가기 계약

동결된 계약 집합

휴대 코어는 기록 가운데 홀로 옮겨 다닐 수 있는 부분입니다. 무엇을 묶는지는 아래 “Identity와 core”에 적어 두었습니다.

provider는 번들 매니페스트가 지목한 정확한 WebAssembly 바이트입니다. 임의의 재빌드나 리스펙스 버전 문자열이 아닙니다. 재빌드의 SHA-256이 같을 때만 같은 보장을 이어받습니다.

별도의 현재 프로필 전체 컴포넌트

공개 full 컴포넌트는 restricted 프로필의 이름만 바꾼 것이 아닙니다. 생성된 프리미티브 205행 전체와 Deferred 0행 위에 별도 lispex/r7rs-rule-current-profile-bounded/1 의미 프로필과 작업량을 세는 lispex-full-vm-meter/1 모델, lispex-evaluator/rust-vm-current-profile/1 컴포넌트 identity를 더합니다. 기존 인터페이스와 value codec, transcript, 휴대 코어 schema는 충분성을 감사한 뒤 정확한 v1 의미를 그대로 유지합니다. full 아티팩트는 별도 LPXFAR01 봉투를 쓰고, restricted LPXART01 아티팩트와 과거 영수증은 바뀌지 않습니다.

인터페이스와 생명주기

인터페이스는 모듈이 내놓는 함수 집합과 데이터를 주고받는 방식을 고정해 둔 것입니다. 모듈의 import는 0개입니다. memory는 하나이며 처음 18 page, 최대 256 page입니다. 내놓는 함수는 할당, 해제, 인터페이스 버전, 준비, 평가 함수와 표준 memory 경계 global뿐입니다. 요청은 크기가 제한된 big-endian length-delimited 값입니다.

작업마다 Wasmtime 저장소와 인스턴스를 새로 만듭니다. 메모리, 할당기, 게스트 힙, interner, 셀, 연속, 작업량 계수기, transcript, 결과 버퍼도 이때 함께 새로 만듭니다. 컴파일해 둔 모듈은 변경할 수 없으며, WebAssembly SHA-256이 정확히 같을 때만 여러 작업이 나눠 쓸 수 있습니다. 인스턴스를 미리 만들어 두고 돌려 쓰는 instance pooling은 허용하지 않습니다.

분리된 자원 영역

준비 단계는 raw_source_bytes, prepare_work, prepare_logical_allocation, syntax_depth를 소유합니다. 평가 단계는 canonical_input_bytes, eval_work, eval_logical_allocation, semantic_frames, traversal_depth, output_bytes, diagnostic_bytes, transcript_bytes, transcript_events, result_bytes를 소유합니다.

work는 CPU 시간이 아니라 버전이 붙은 결정적 tariff입니다. 논리 할당량은 Rust 객체 크기, allocator capacity, pointer width가 아니라 모델이 정의합니다. 효과보다 먼저 부과하고 환불하지 않으며 full u64를 사용합니다. 정해진 순서에서 처음으로 한도를 넘기는 축이 실패합니다. 올바른 꼬리 호출은 non-tail semantic frame을 소비하지 않습니다.

사용한 양과 남은 양은 휴대 코어에 들어가지 않습니다. tariff, 축, 단위, 순서, overflow, depth, 실패 규칙이 바뀌면 새 model ID가 필요하며 서로 다른 모델의 budget을 변환하지 않습니다.

Identity와 core

core는 작성된 소스 바이트, 하나로 고정된 형태의 소스, 의미 규칙, 하나로 고정된 형태의 입력, 자원 계약, 요청, 규칙을 실행한 아티팩트, 평가, transcript, 결과의 identity를 서로 구분합니다. hash framing은 lispex.evaluation-identity/v1의 length-delimited SHA-256 규칙을 따릅니다.

결정적 의미 결과와 결정적 요청 거부만 core를 가집니다. 운영 중단과 engine fault는 core를 가질 수 없습니다. 발행자는 규칙을 실행하는 프로그램 밖에서 완성된 core 바이트에 서명할 수 있지만, 그 봉투가 결과 범주를 바꾸지는 않습니다.

제한 프로필

첫 프로필은 번들이 검증한 닫힌 operation 집합만 허용합니다. 일반 전체 lispex-profile-1.5 tree 인터프리터는 별도입니다. 지원하지 않는 형식과 내장 프로시저는 가상 머신이 무엇을 실행하기 전에 닫힌 채로 거부합니다. provider는 tree, Rust 쪽 다른 실행 경로 제품, 토파즈, 미리 컴파일해 둔 제품, 과거에 규칙을 실행하던 프로그램, 폴백을 호출하지 않습니다.

네이티브 결정 디렉터리 계약

네이티브의 rule 명령은 한도가 정해진 이 실행기를 하나의 원자적 로컬 흐름으로 제공합니다.

rule run -> inspect -> verify -> replay

rule run은 정확한 소스와 엄격한 JSON 파일, 서로 분리된 준비·평가 한도를 받습니다. JSON object는 record, array는 벡터로 바뀝니다. string, boolean, 정확 정수는 값 종류를 유지하고 null은 빈 리스트가 됩니다. 중복 object key, 부정확한 수, 지원하지 않는 값, 뒤따르는 데이터는 결정적 요청 거부입니다.

성공하면 정확히 다섯 개의 일반 파일을 만듭니다.

기존 경로를 덮어쓰지 않고 출력 디렉터리를 만듭니다. inspect와 verify는 평가하지 않습니다. replay는 실행기를 새 인스턴스로 띄우며 재현한 결과와 휴대 코어가 일치해야 합니다. 파일이 없거나, 변조되거나, 더 들어 있거나, 심볼릭 링크라면 닫힌 채로 거부합니다.

이 흐름은 네이티브 제품이 제공합니다. 제출한 소스를 복원하거나 보존하지 않고, 규칙을 실행할 다른 프로그램을 찾거나 폴백을 호출하지 않습니다. 호스트 capability, 원격 서비스, 바우치 증거로의 승격, 외부 행동 권한도 제공하지 않습니다.

배포와 보존

네이티브에는 provider 바이트가 정확히 그대로 들어 있습니다. 릴리스는 WebAssembly 번들과 매니페스트, 골든 벡터, 검증 자료, 소프트웨어 부품 목록과 의존성 처리 결정, 안전성 근거, 덧붙이기만 가능한 릴리스 DAG 기록도 함께 공개합니다. 보안 수정은 새 아티팩트 identity와 새 승인을 만듭니다. 과거 영수증은 보존해 둔 과거 바이트와 계약으로 계속 검증할 수 있지만, 새로 들어오는 적대적 평가에는 거부될 수 있습니다.

이 컴포넌트는 토파즈 빌드 의존성이 없습니다. 미리 컴파일해 두는 별도 컴포넌트는 자기 토파즈 컴파일러 핀을 그대로 유지합니다. 토파즈 쪽 소비자는 이후 별도로 승인받은 릴리스에서 이 컴포넌트를 정확한 해시로 고정해야 합니다.

보장하지 않는 것

이 계약은 기밀성, 발행자 인증, 바우치 권한, 규칙의 정당성, 출처, 신선도, 외부 행동 허가, 시간 은닉, 캐시 격리, 미세구조 부채널 저항성을 제공하지 않습니다. 브라우저 지원도 이번 릴리스 범위 밖입니다.

다음으로

네이티브 사용 흐름은 신뢰하지 않는 규칙 평가하기를 보세요.