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

선언해 둔 한도 안에서 규칙 하나만 실행하는 네이티브 엔진을 restricted 쪽이나 현재 프로필 전체 쪽으로 고르고, 준비와 평가의 한도를 따로 적용한 뒤, 규칙과 입력과 한도와 결과를 한데 묶은 휴대 코어를 검증합니다.

선언한 한도 안에서 도는 제품 고르기

일반 lispex rule.lspx는 소스를 그대로 읽어 내려가는 내장 인터프리터이며 프로필 전체를 다룹니다. 더 작은 lispex/r7rs-rule-embedded-core/1 안에서 결정적인 작업량과 논리 할당량을 제한해야 할 때 lispex embed를 사용하세요.

restricted 네이티브 제품에는 바깥에서 아무것도 끌어다 쓰지 않는 정확한 WebAssembly 엔진 하나가 들어 있습니다. 이 엔진이 규칙을 실행합니다. 엔진 경로를 넘기거나, 다른 엔진을 찾거나 내려받거나, 대체 엔진을 요청할 수 없습니다.

다운로드 페이지에서는 엔진 바이트를 직접 소비하는 애플리케이션을 위해 정확한 lispex-embed-evaluator.wasm, 컴포넌트 매니페스트, 기준 벡터, 그리고 짝이 되는 SHA-256 체크섬 파일도 제공합니다.

별도 전체 프로필 컴포넌트를 명시적으로 선택하세요

규칙에 lispex-profile-1.5 전체가 필요하면 lispex embed full을 사용하세요. 준비 파일과 결과 파일은 .lpxfull이고, 같은 다섯 작업은 모두 별도의 명시적 명령 이름 아래에 있습니다.

SH
lispex embed full prepare --source policy.lspx --limits prepare-limits.json --out policy.lpxfull
lispex embed full evaluate --prepared policy.lpxfull --input input.lpxvalue --limits evaluation-limits.json --out result.lpxfull
lispex embed full inspect --artifact result.lpxfull
lispex embed full verify --artifact result.lpxfull
lispex embed full replay --artifact result.lpxfull

이 제품은 lispex/r7rs-rule-current-profile-bounded/1lispex-full-vm-meter/1 식별자를 가진, 바깥에서 아무것도 끌어다 쓰지 않는 두 번째 정확한 컴포넌트입니다. 생성된 닫힌 목록 205행 전체를 다루고 작업마다 새 인스턴스를 만듭니다. restricted 컴포넌트의 이름이나 범위를 바꾸지 않습니다. 다운로드 페이지는 전체 프로필용 Wasm과 매니페스트, 제공자 벡터, 재배포 묶음, 체크섬을 따로 제공합니다.

1. 규칙을 준비합니다

prepare-limits.json을 만드세요.

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

소스를 준비합니다.

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

준비 단계는 UTF-8을 받아들이고, 프로그램을 읽고 정규화하고, 허용되는 하나의 형식으로 바이트코드를 만들고 검증한 뒤 제한 프로필을 확인합니다. 제출한 소스, 허용 형식으로 정리한 소스, 의미 규칙, 기능 집합, 바이트코드, 규칙을 실행하는 프로그램, 정확한 한도의 식별자를 기록합니다. 규칙을 실행하지는 않습니다.

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

입력은 허용되는 형식으로 적은 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
}

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

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

준비 단계의 사용량은 평가 사용량에 섞이지 않습니다. 따라서 준비 아티팩트를 다시 써도 평가에 매겨지는 비용이나 휴대 코어가 달라지지 않습니다. 휴대 코어란 규칙과 입력, 한도, 결과를 한데 묶어 둔 부분입니다.

3. 살펴보고 검증합니다

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

inspect는 안정된 JSON 요약을 보여줍니다. verify는 규칙을 실행하지 않고 봉투, 정확한 해시, 범주, 한도, 휴대 코어를 다시 계산합니다. 둘 다 발행자를 인증하거나 바우치 권한을 만들지 않습니다.

먼저 결과 범주를 보세요

범주휴대 코어
결정적 의미 결과값, 실행 진단, 자원 소진, 옮길 수 없는 결과 중 하나에 결정적으로 도달했습니다있음
결정적 요청 거부허용된 평가를 시작하기 전에 정확한 요청을 거부했습니다있음
운영 중단결과가 확정되기 전에 호출자가 취소했거나 실행기가 멈췄습니다없음
엔진 결함규칙을 실행하는 프로그램, 바이너리 인터페이스, 할당기, 안전 상한 가운데 하나가 계약을 지키지 못했습니다없음

사용한 작업량은 로컬 진단에는 유용하지만 휴대 코어 안에는 들어가지 않습니다. 대신 휴대 코어는 정확한 한도, 프로필, 모델, 소스, 입력, 요청, 규칙을 실행하는 프로그램의 아티팩트, 실행 기록, 결과 식별자를 묶습니다.

경계

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

이 기능은 네이티브와 독립 엔진 묶음에서 제공합니다. npm, 공개 브라우저 WebAssembly 래퍼, 플레이그라운드, 브라우저 내장은 제공하지 않습니다. 시간, 캐시, 마이크로아키텍처 부채널은 기술 보장 범위 밖입니다. 같은 프로세스 안에서 도는 첫 제품에서 호스트 프로세스의 생존은 운영 목표이며 보안 보장은 아닙니다.

아티팩트와 휴대 코어는 검사 자료입니다. 바우치 서명, 인증된 증거, 게이트 통과, 규칙의 정당성, 외부 행동 허가는 아닙니다.

다음으로

선언해 둔 한도 안에서 규칙 하나만 실행하는 작은 엔진의 정확한 ID, 자원 축, 결과 범주, 묶음 계약은 제한 평가기 계약에서 확인하세요.