리스펙스 문서
(리스펙스)
( 괄호는 구두점이고, 재귀는 운율이다 )
결정 규칙을 쓰기 위한 작은 리스프입니다. 문법은 일부러 Scheme에 가깝게 두었습니다. 같은 입력에는 언제나 같은 답이 나오고, 실행은 나중에 그대로 대조할 수 있을 만큼 정확한 기록을 남길 수 있습니다.
구조화된 입력 하나가 들어가면, 견주고 기록할 수 있는 판정 값 하나가 나옵니다.
레코드는 연관 리스트이고 경계 조건은 정확한 정수 비교입니다. 거절을 포함한 모든 판정은 평범한 데이터 값이라서 그대로 저장하고 견주고 검사할 수 있습니다. 새로 익힐 표기법은 없습니다. 겉모습은 Scheme 그대로입니다. 리스펙스다운 부분은 오히려 움직이지 않는 약속에 있습니다. 프로시저 표면은 닫혀 있고, 오류는 결정적이며, 입력 하나에는 답이 하나입니다.
(define (field key record)
(let ((entry (assq key record)))
(if (pair? entry)
(cdr entry)
(error "missing field" key))))
(define (review-refund request)
(let ((days (field 'days request))
(opened (field 'opened request))
(cents (field 'cents request)))
(cond ((not (exact-integer? days)) '(reject malformed-days))
((>= days 15) '(deny outside-window))
(opened '(deny opened-item))
((> cents 50000) '(escalate manual-review))
(else '(allow within-policy)))))
(map review-refund
'(((days . 14) (opened . #f) (cents . 12900))
((days . 14) (opened . #f) (cents . 82000))
((days . 15) (opened . #f) (cents . 12900))))
; => ((allow within-policy)
; (escalate manual-review)
; (deny outside-window))진입로는 두 갈래입니다. Scheme을 아는 독자를 위한 문법 지도, 그 밖의 모두를 위한 안내 경로.
문법 지도는 일상적으로 쓰는 폼 전부를 실제 관측 결과와 함께 보여 주고, 익숙한 Scheme보다 엄격해지는 지점도 짚어 줍니다. if에는 else 가지가 반드시 있어야 하고, 프로시저 표면은 205개로 닫혀 있으며, 고차 프로시저는 리스트 하나만 받고, 사용자 매크로 층은 없습니다. 학습 경로는 그보다 천천히 걸어서, 시험까지 마친 완전한 환불 규칙 하나로 끝납니다.
- 01첫 프로그램 실행
- 02값과 프로시저에 이름 붙이기
- 03데이터 모양의 결정 고르기
- 04완성된 환불 규칙 시험하기
리스펙스는 서버 없이 실행됩니다. WebAssembly로 컴파일된 레퍼런스 인터프리터가 브라우저 안에서 코드를 바로 평가합니다.
간단한 기본 경로 하나, 명시적인 네이티브 경로 네 개.
브라우저, npm, 네이티브 어디서나 기본은 Rust tree 인터프리터입니다. 네이티브에서는 내장 Rust VM, 정확히 설치한 Topaz VM과 AOT 제품까지 살펴보고 고정할 수 있습니다. 모두 직접 고르는 명시적 경로이지, 조용히 일어나는 업그레이드가 아닙니다.
Rust와 LIL은 현재 기능 행 205/205를 모두 지원합니다. LIT는 84/205 경계를 따로 유지하고 그 사실 그대로 보고됩니다. 네이티브의 routes inventory, lock, doctor, measure, run은 지금 경로가 정확히 무엇인지와 어디서 실패했는지를 숨기지 않습니다. 몰래 찾아내거나 바꿔치우거나 다시 시도하는 일은 없습니다. 제품이 없으면 있는 그대로 거절을 보고할 뿐, 다른 경로로 넘어가지 않습니다.
정확한 한도 아래 환불 규칙을 실행하고, 확인한 것을 남기세요.
네이티브 lispex rule run은 검토한 규칙을 준비하고, 엄격한 JSON 입력 하나를 받아, 한정 평가기에서 한 번만 평가합니다. 한정 평가기는 import가 없는 별도 엔진이라서, 선언해 둔 한도 안에서 작업량과 할당을 전부 셈해야만 앞으로 나아갑니다. 실행이 끝나면 구성원 다섯을 담은 결정 디렉터리가 남습니다. 준비된 규칙 아티팩트, 정규 입력, 정확한 요청 결속을 담은 결정적 결과, 자격을 갖춘 휴대 코어, 파생 요약입니다. 원본 규칙 소스는 일부러 여기에 넣지 않습니다.
- 01검토한 규칙
- 02엄격한 JSON 입력
- 03allow 결정
- 04확인 가능한 휴대 코어
1. 규칙
(let ((days (cdr (car input)))
(opened (cdr (car (cdr input)))))
(if (< days 15)
(if opened "deny" "allow")
"deny"))2. 입력
{
"days": 14,
"opened": false
}3. 한정된 실행 한 번
lispex rule run \
--source refund-window.lspx \
--input day-14-unopened.json \
--prepare-limits prepare-limits.json \
--eval-limits evaluation-limits.json \
--out decision
lispex rule inspect --dir decision
lispex rule verify --dir decision
lispex rule replay --dir decision고정 사례인 14일 미개봉 입력에서 한정된 실행이 돌려주는 결정은 allow.
rule inspect는 실행 없이 디렉터리를 요약합니다. rule verify도 실행 없이 구성원 집합과 식별자와 해시와 결속을 정확히 검사합니다. rule replay는 기록된 요청을 새 평가기 인스턴스에서 한 번 평가해 같은 결과가 나와야만 통과합니다. 셋 모두 권한을 부여하지 않습니다.
휴대 코어가 결속하는 것
의미 규칙, 정규 입력, 정확한 한도, 정확한 평가기 아티팩트, 결정적 결과를 함께 묶습니다. 어떤 질문에 어떤 상한 아래에서 답했는지를 정확히 알기에 충분한 정보입니다. 소모했거나 남은 사용량은 휴대 코어에 들어가지 않습니다.
기록이 성립시키지 않는 것
누가 실행했는지, 지금도 유효한지, 규칙에 담긴 정책이 공정하거나 옳은지, 같은 결정이 두 번 쓰였는지는 알 수 없습니다. 프로세스 밖에서 행동할 권한도 생기지 않습니다.
결정 규칙은 결정적 이미지 한 장으로 옮길 수 있습니다.
이미지는 규칙의 소스 바이트를 정확히 담는 정규 그림 파일입니다. 여기 담긴 규칙은 검토를 마친 환불 규칙이고, 정식 Decision 값을 돌려줍니다. 바우치가 증거를 발급할 수 있는 결과 형태는 이 Decision뿐입니다. 소스는 로컬에서 복원할 수 있고, 바이트가 정규임이 증명된 뒤에만 실행하며, 증명을 마친 이미지는 아래 바우치 흐름에서 정확한 소스로 고정할 수 있습니다. 픽셀이 보증하는 것은 무결성 하나입니다.
(define days-since-delivery (car input))
(define opened? (car (cdr input)))
(if (<= days-since-delivery 14)
(if opened?
(decision-deny)
(decision-approve))
(decision-deny))여기서 길 하나가 아래로 이어집니다. 이 이미지를 복원해 증명하고, 정확한 소스로 고정하고, 네이티브에서 정확한 입력 하나에 대해 서명된 바우치 증거를 발급합니다. 받은 쪽은 자신이 만든 신뢰 정책으로 그 증거를 인증하고, 자기 컴퓨터에서 규칙을 다시 실행해 로컬 게이트로 확인합니다. 그 뒤에 실제로 무엇을 할지는 애플리케이션이 따로 정합니다. 이미지 자체는 이 가운데 무엇도 아닙니다. 서명된 증거도 신뢰도 권한도 아니고, 바이트를 정확히 나르는 일만 합니다.
모든 결정은 서명된 실행 기록을 남길 수 있습니다.
바우치는 기록된 결정 하나를 어디로든 가져갈 수 있는 서명된 증거로 만들고, 그 증거를 허가와 끝까지 구분합니다.
실행 한 번을 서명해 남긴 기록이 있습니다. 어떤 규칙 바이트가 실행됐고, 어떤 입력 바이트가 들어갔고, 어떤 결정이 나왔는지가 담깁니다. 이 기록을 영수증이라고 부릅니다. 네이티브 릴리스 바이너리에서 lispex vouch issue는 검토한 규칙을 직접 실행해 영수증을 만듭니다. 그래서 영수증에 남는 것은 누군가의 주장이 아니라 실제로 일어난 일입니다. 영수증과 소스와 입력은 묶음이라는 한 파일로 함께 이동할 수 있습니다. 묶음은 네이티브에서든 npm에서든 lispex vouch verify로 인증할 수 있고, 이 인증이 답하는 질문은 하나뿐입니다. 내가 신뢰하기로 한 키가 정확히 이 바이트에 서명했는가. 그 밖의 질문에는 일부러 답하지 않습니다.
묶음은 게이트가 실행할 요청을 고르지 못합니다.
재실행은 묶음의 주장이 아니라 수신자가 직접 고정한 요청에서 시작합니다.
요청 결속은 내 컴퓨터가 내가 요청한 것만 다시 실행한다는 규칙입니다. 묶음이 증명하는 것은 발급자가 관측한 내용까지입니다. 수신자 쪽에서 어떤 규칙과 입력이 실행될지는 묶음이 정할 수 없습니다. 그래서 재실행 전에 요청을 직접 고정합니다. 규칙 소스는 직접 보관한 파일이거나 완전한 정규 증명을 통과한 이미지여야 하고, 입력도 정확히 지정해야 합니다. 검증은 서명을 먼저 인증한 다음 묶음을 고정된 요청과 견주고, 정확히 일치할 때만 실행으로 넘어갑니다. 아무것도 고정하지 않으면 검증은 서명 확인에서 멈추며, 재실행이나 게이트에는 닿을 수 없습니다.
재실행은 수신자의 컴퓨터가 직접 해 보는 비교입니다.
게이트는 지금 이 자리의 정확한 일치에서만 성공하고, 그 위에는 직접 작성한 신뢰 정책이 있습니다.
lispex vouch gate는 질문 하나를 확인하는 로컬 검사입니다. 지금 이 컴퓨터에서 고정된 요청으로 규칙을 다시 실행하면 서명된 결과와 정확히 같은 결정이 나오는가, 그리고 그 결정이 내가 요구한 결정인가. 증거가 들어가면 종료 코드가 나옵니다. 그 위에 신뢰 정책이 있습니다. 신뢰 정책은 수신자가 직접 쓰고 감사하는 짧은 설정 파일로, 검토를 마친 공개 키와 정확한 평가기, 받아들일 규칙 소스나 증명된 이미지를 적습니다. 서명이 유효해도 정책에 없는 규칙은 거부됩니다. 정책이 무언가를 허가하는 일은 없습니다. 검사할 대상을 좁힐 뿐입니다.
통과한 게이트가 주지 않는 것.
아래 경계는 모두 의도된 것입니다. 통과 보고서는 다음 단계를 위한 증거일 뿐, 그 이상이 아닙니다.
통과한 검증이나 게이트 보고서는 허가도 토큰도 외부 행동 권한도 아닙니다. 실제로 환불할지, 지불할지, 배송할지는 애플리케이션이 따로 내리는 결정입니다. 요청 결속이 증명하는 것은 고정된 요청과 같다는 사실이지, 신선도나 유일성이나 재전송 방지가 아닙니다. 이미지는 복원한 소스 바이트가 온전하다는 사실만 증명하고, 그 소스를 신뢰해도 된다고 말하지 않습니다. npm은 검증과 인증까지만 할 수 있어서 발급도 재실행도 게이트도 하지 못하고, 브라우저 WASM과 플레이그라운드는 코드를 평가하는 일만 합니다. 그리고 경로 잠금, 측정값, 실행 출력 같은 일상 실행의 결과물은 무엇도 바우치 권한이 되지 않습니다.
생각의 원형을 담는 언어.
The language that captures the shape of thought.
Язык, воплощающий форму мысли.