한정 Lispex 결정 애플리케이션 만들기

토파즈 5.18에서는 검사된 애플리케이션 하나가 이름 있는 Lispex 규칙을 한 번 준비하고 여러 정규 값을 평가할 수 있습니다. 경계는 의도적으로 좁습니다. 패키지는 lispex/r7rs-rule-embedded-core/1 프로필과 내장 구성 요소, 모든 규칙 소스와 한도 문서, 애플리케이션 전체 쿼터 문서를 topaz.lock에 고정합니다.

docs/samples/guides/lispex-application의 유지보수 샘플에서 시작하세요. 아래에서 쓰는 정확한 매니페스트와 잠금 파일, 생성 규칙 핸들, 준비된 규칙 산출물, 토파즈 모듈 둘, 실제 도달하는 규칙 넷이 모두 들어 있습니다.

애플리케이션 선언하기

매니페스트에서 토파즈 언어와 표준 라이브러리를 함께 고릅니다. 제한 Lispex 프로필과 애플리케이션 계약도 이름으로 고정합니다.

[package]
name = "bounded_lispex_decision_application"
version = "0.1.0"
language = "5.18"
entry = "src/main.tpz"

[dependencies]
std = "5.18"

[lispex]
profile = "lispex/r7rs-rule-embedded-core/1"
application = "topaz/lispex-decision-application/1"
application_quotas = "rules/application.quotas.json"

[[lispex.rule]]
name = "approve"
source = "rules/approve.lspx"
limits = "rules/approve.limits.json"

규칙을 더 넣을 때도 같은 [[lispex.rule]] 형식을 씁니다. 규칙 이름은 std.lispex.rules의 생성 함수가 됩니다. 실행 중에 파일 경로나 구성 요소를 고르는 선택기가 아닙니다.

규칙과 유한한 한도 작성하기

rules/approve.lspx는 선택한 제한 프로필 안에서 쓰는 일반 Lispex 소스입니다.

(if (< 10 15) "allow" "deny")

rules/approve.limits.json은 준비와 평가의 상한을 고정합니다. 완전한 샘플은 모든 필드를 보존하며, 다음 발췌에는 두 작업량 상한만 보입니다.

{
  "schema": "topaz.lispex-embed-limits/v1",
  "prepare": {
    "prepare_work": 1000000
  },
  "evaluate": {
    "eval_work": 10000
  }
}

rules/application.quotas.json은 애플리케이션 호스트 한도를 따로 정합니다. 샘플은 동시 평가 둘, 대기 평가 둘, 전체 평가 64회와 유한한 벽시계 마감 시간을 허용합니다. 규칙의 의미 한도 소진과 애플리케이션 거부는 서로 다른 타입의 결과입니다.

잠금 파일 만들고 살펴보기

패키지 루트에서 잠금을 만드세요. 구성 요소나 준비 산출물 다이제스트를 손으로 적지 않습니다.

topaz lock --root .

커밋하기 전에 topaz.lock을 살펴보세요. [lispex] 절은 프로필, 애플리케이션 계약, 구성 요소, 평가기, ABI, 값 코덱, 계량 모델, 산출물 계약, 어댑터, 쿼터, 대상 처분과 생성 핸들 카탈로그를 고정합니다. 각 [[lispex.rule]] 행은 소스, 한도, 준비 요청과 제출, 준비 산출물을 고정합니다.

매니페스트, 규칙 소스, 한도, 쿼터, 구성 요소나 프로필을 바꿨다면 잠금을 새로 만들어야 합니다. --locked 빌드는 다른 규칙을 몰래 준비하지 않고 드리프트를 거부합니다.

패키지 검사하고 실행하기

먼저 잠긴 인터프리터 경로를 사용합니다.

topaz check --root . --locked
topaz run --root . --locked -- all

유지보수 all 시나리오는 일반 입력 24개를 평가하고, 규칙 상태가 격리됐는지 확인하고, 의미 한도를 소진하고, 65번째 애플리케이션 평가를 거부합니다. 출력은 정확히 다음과 같습니다.

all:default:24:evidence:verified:replayed:isolation:2:complete:semantic-limit:exhausted:aggregate-quota:64:refused

다른 글자가 나오거나 종료 코드가 0이 아니면 관찰 실패입니다.

잠긴 deadline_probe는 의도적으로 all과 분리합니다. 릴리스 법정은 정확한 패키지를 복제하고 애플리케이션 마감 쿼터만 100밀리초에서 1밀리초로 바꾼 뒤 복제한 잠금에 다시 결합합니다. 이어 고정된 deadline 전용 엔트리로 인터프리터와 재배치된 소스 없는 네이티브 제품에서 DeadlineExceeded를 요구하고, 그 다음 100밀리초 일반 애플리케이션의 성공을 확인합니다. 한 애플리케이션 내부 정리의 권한은 Q1에 그대로 있습니다. 따라서 일반 샘플 출력은 실행 기계의 속도를 전제로 하지 않습니다.

소비자 증거 살펴보고 검증하고 재실행하기

생성 API는 std.lispex에서, 생성 규칙 핸들은 std.lispex.rules에서 가져옵니다.

let 판정 = evaluate(rules.approve(), input, defaultLimits(rules.approve()))
let 기록 = evaluateWithEvidence(
    rules.approve(),
    input,
    defaultLimits(rules.approve()),
)

기록할 수 있는 결정적 결과에는 완전한 샘플이 다음 수명 주기를 그대로 사용합니다.

1. consumerArtifactBytes로 소비자 산출물 전체를 저장합니다.
2. consumerArtifactFromBytes로 저장 바이트를 검사해 다시 받아들입니다.
3. inspectConsumerArtifact로 실행 없이 안정된 식별자를 확인합니다.
4. verifyConsumerArtifact로 구조와 다이제스트, 결합을 검증합니다.
5. 코어가 있으면 portableCoreBytes로 Lispex 형식 바이트를 꺼냅니다.
6. freshReplay로 잠긴 규칙과 입력을 새 게스트에서 평가하고 완전한 산출물이 같을 때만 받아들입니다.

산출물과 이식 가능 코어는 소비자가 만들며 인증되지 않습니다. 발행자, 제공자 승인, 서명 권한, 구성 요소 승인이나 외부 행동 권한을 담지 않습니다. 운영 거부, 취소, 안전 한도 선점과 엔진 실패에는 이식 가능 코어가 생기지 않습니다.

네이티브 제품 빌드하고 실행하기

패키지 루트 바깥에 최적화된 관리형 네이티브 제품을 만듭니다.

topaz build --root . --locked --release --out-dir ../bounded-product

빌드한 OS와 아키텍처에서 결과를 실행합니다.

../bounded-product/target/release/program all

Windows에서는 다음 명령을 씁니다.

..\bounded-product\target\release\program.exe all

네이티브 제품도 위의 정확한 관찰값을 출력해야 합니다. 빌드가 성공했다고 그 실행 파일을 다른 대상으로 옮겨 쓸 수 있는 것은 아닙니다.

제품 경계 확인하기

애플리케이션 계약에는 닫힌 경로 집합이 있습니다.

거부된 경로가 인터프리터나 네이티브 제품으로 폴백하지 않습니다. 전체 프로필 Lispex는 별도 구성 요소, 프로필, 계약, 대상 코트와 승인을 사용합니다. 이 제한 프로필을 제자리에서 넓히지 않습니다.

Rust 백엔드, Python 백엔드, Lispex 평가기와 LIT도 이어서 살펴보세요.