제한 평가기 계약

제한 프로필, 작업량·할당 모델, import-free Wasm ABI, portable core 범주, 보존과 지원 경계를 정확히 설명합니다.

이 페이지는 v1.14을 설명합니다. 현재 매뉴얼인지 여부는 여기에서 확인하세요: /version.json

동결된 계약 집합

계약식별자
의미 프로필lispex/r7rs-rule-embedded-core/1
작업량·논리 할당 모델lispex-vm-meter/1
값 codeclispex.embed-value/v1
transcriptlispex.embed-transcript/v1
Wasm ABIlispex.embed-wasm-abi/v1
portable corelispex.embed-receipt-core/v1

provider는 bundle manifest가 지목한 정확한 Wasm 바이트입니다. 임의의 재빌드나 Lispex 버전 문자열이 아닙니다. 재빌드의 SHA-256이 같을 때만 같은 보장을 이어받습니다.

ABI와 생명주기

모듈의 import는 0개입니다. memory는 하나이며 처음 18 page, 최대 256 page입니다. export는 할당, 해제, ABI 버전, 준비, 평가 함수와 표준 memory 경계 global뿐입니다. 요청은 크기가 제한된 big-endian length-delimited 값입니다.

작업마다 새 Wasmtime Store, Instance, memory, allocator, guest heap, interner, cell, continuation, meter, transcript, result buffer를 만듭니다. immutable compiled Module은 정확한 Wasm 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을 소비하지 않습니다.

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

Identity와 core

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

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

제한 프로필

첫 프로필은 bundle이 검증한 닫힌 operation 집합만 허용합니다. 일반 전체 lispex-profile-1.5 tree 인터프리터는 별도입니다. 지원하지 않는 형식과 primitive는 VM 실행 전에 fail-closed로 거부합니다. provider는 tree, Rust route 제품, Topaz, AOT, 과거 평가기, fallback을 호출하지 않습니다.

Native 결정 디렉터리 계약

Native의 rule wrapper는 제한 평가기를 하나의 원자적 로컬 흐름으로 제공합니다.

rule run -> inspect -> verify -> replay

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

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

파일역할
prepared.lpxembed정확한 준비 규칙 아티팩트
canonical-input.lpxvalue정규 평가 입력
result.lpxembed결정적 결과와 정확한 요청 결속
receipt-core.lpxreceipt발급 가능한 portable core
summary.json파생된 비권위적 요약

기존 경로를 덮어쓰지 않고 출력 디렉터리를 만듭니다. inspectverify는 평가하지 않습니다. replay는 새 평가기 인스턴스를 사용하며 재현한 결과와 portable core가 일치해야 합니다. 파일이 없거나, 변조되거나, 더 들어 있거나, 심볼릭 링크라면 fail-closed로 거부합니다.

이 흐름은 Native 제품이 제공합니다. 제출한 소스를 복원하거나 보존하지 않고, 다른 평가기를 탐색하거나 fallback을 호출하지 않습니다. 호스트 capability, 원격 서비스, Vouch evidence 승격, 외부 행동 권한도 제공하지 않습니다.

배포와 보존

Native는 정확한 provider 바이트를 포함합니다. 릴리스는 Wasm bundle, manifest, golden vector, verifier 자료, SBOM/dependency disposition, safety evidence, append-only release DAG record도 공개합니다. 보안 수정은 새 artifact identity와 admission을 만듭니다. 과거 receipt는 보존된 과거 바이트와 계약으로 계속 검증할 수 있지만 새 adversarial 평가에는 거부될 수 있습니다.

평가기 component는 Topaz build dependency가 없습니다. 독립 AOT component는 자기 Topaz compiler pin을 그대로 유지합니다. Topaz consumer는 이후 별도 승인을 받은 릴리스에서 이 evaluator component의 digest를 고정해야 합니다.

보장하지 않는 것

이 계약은 기밀성, 발행자 인증, Vouch 권한, 규칙의 정당성, provenance, freshness, 외부 행동 허가, 시간 은닉, cache 격리, microarchitecture side channel 저항성을 제공하지 않습니다. 브라우저와 두 번째 embedded engine도 첫 릴리스 범위 밖입니다.

다음으로

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