신뢰하지 않는 규칙 평가하기

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

제한 평가기를 선택하세요

일반 lispex rule.lspx는 전체 프로필을 쓰는 tree 인터프리터입니다. 더 작은 lispex/r7rs-rule-embedded-core/1 안에서 결정적인 작업량과 논리 할당량을 제한해야 할 때 lispex embed를 사용하세요.

Native 실행 파일에는 import가 없는 정확한 Wasm 평가기 하나가 들어 있습니다. 평가기 경로를 넘기거나, 다른 평가기를 찾거나 내려받거나, fallback을 요청할 수 없습니다.

다운로드 페이지에서는 평가기 바이트를 직접 소비하는 애플리케이션을 위해 정확한 lispex-embed-evaluator.wasm, component manifest, golden vector, SHA-256 파일도 제공합니다.

1. 규칙을 준비합니다

prepare-limits.json을 만드세요.

JSON

{
  "raw_source_bytes": 4096,
  "prepare_work": 1000000,
  "logical_allocation": 1000000,
  "syntax_depth": 64
}

소스를 준비합니다.

lispex embed prepare \
  --source policy.lspx \
  --limits prepare-limits.json \
  --out policy.lpxembed

준비 단계는 UTF-8을 받아들이고, 프로그램을 읽고 정규화하고, canonical bytecode를 만들고 검증한 뒤 제한 프로필을 확인합니다. 작성한 소스, canonical 소스, 의미 규칙, 기능 집합, bytecode, 평가기, 정확한 한도의 identity를 기록합니다. 규칙을 실행하지는 않습니다.

2. 준비된 규칙을 평가합니다

입력은 canonical lispex.embed-value/v1 값 하나입니다. evaluation-limits.json을 만드세요.

JSON

{
  "canonical_input_bytes": 4096,
  "eval_work": 1000000,
  "logical_allocation": 1000000,
  "semantic_frames": 1000,
  "traversal_depth": 256,
  "output_bytes": 1000000,
  "diagnostic_bytes": 1000000,
  "transcript_bytes": 1000000,
  "transcript_events": 100,
  "result_bytes": 1000000
}

바로 그 준비 아티팩트를 평가합니다.

lispex embed evaluate \
  --prepared policy.lpxembed \
  --input input.lpxvalue \
  --limits evaluation-limits.json \
  --out result.lpxembed

준비 단계의 사용량은 평가 사용량에 섞이지 않습니다. 따라서 준비 아티팩트를 다시 써도 평가 tariff나 portable core가 달라지지 않습니다.

3. 살펴보고 검증합니다

lispex embed inspect --artifact result.lpxembed
lispex embed verify --artifact result.lpxembed

inspect는 안정된 JSON 요약을 보여줍니다. verify는 규칙을 실행하지 않고 envelope, 정확한 hash, 범주, 한도, portable core를 다시 계산합니다. 둘 다 발행자를 인증하거나 Vouch 권한을 만들지 않습니다.

먼저 결과 범주를 보세요

범주	뜻	Portable core
결정적 의미 결과	값, 실행 진단, 자원 소진, 옮길 수 없는 결과 중 하나에 결정적으로 도달했습니다	있음
결정적 요청 거부	허용된 평가를 시작하기 전에 정확한 요청을 거부했습니다	있음
운영 중단	결과가 확정되기 전에 호출자가 취소했거나 실행기가 멈췄습니다	없음
엔진 결함	평가기, ABI, allocator, safety ceiling이 계약을 지키지 못했습니다	없음

사용한 작업량은 로컬 진단에는 유용하지만 portable core 안에는 들어가지 않습니다. 대신 core는 정확한 한도, 프로필, 모델, 소스, 입력, 요청, 평가기 아티팩트, transcript, 결과 identity를 묶습니다.

경계

첫 제품은 엔진 하나만 사용하며 실행 중 합의를 만들지 않습니다. 공개 전에 릴리스 단위 차등 법정으로 정확한 바이트를 검증합니다. 제한 프로필은 전체 lispex-profile-1.5보다 작습니다. 지원하지 않는 형식과 primitive는 다른 곳에 맡기지 않고 거부합니다.

이 기능은 Native와 독립 평가기 bundle에서 제공합니다. npm, 공개 브라우저 WASM facade, Playground, 브라우저 embedding은 제공하지 않습니다. 시간, cache, microarchitecture side channel은 기술 보장 범위 밖입니다. 첫 in-process 제품에서 host process 생존은 운영 목표이며 보안 보장은 아닙니다.

아티팩트와 core는 검사 자료입니다. Vouch 서명, 인증된 evidence, gate grant, 규칙의 정당성, 외부 행동 허가는 아닙니다.

다음으로

정확한 ID, 자원 축, 결과 범주, bundle 계약은 제한 평가기 계약에서 확인하세요.