리스펙스 문서

(리스펙스)

( 괄호는 구두점이고, 재귀는 운율이다 )

결정 규칙을 위한 작은 리스프입니다. 문법은 의도적으로 Scheme에 가깝습니다. 같은 입력에는 같은 답을 내고, 실행은 나중에 점검할 수 있을 만큼 정확한 기록을 남길 수 있습니다.

도판 I

구조화된 입력이 들어가면, 인쇄할 수 있는 판정이 나옵니다.

레코드는 연관 리스트이고, 경계는 정확한 정수 비교이며, 거절을 포함한 모든 판정은 인쇄하고 비교할 수 있는 평범한 데이터입니다. 새로운 표기법은 없습니다. 표면은 Scheme의 것입니다. 리스펙스의 성격은 고정되어 있는 것들에 있습니다: 닫힌 프로시저 표면, 결정적 오류, 입력 하나당 답 하나.

LISPEX

(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은 현재 capability 205/205행을 지원하고, LIT는 별도로 84/205 경계를 유지하며 그대로 보고됩니다. 네이티브 routes inventory·lock·doctor·measure·run은 정확한 경로 identity와 실패를 숨김없이 보여 줍니다. 어떤 것도 몰래 발견하거나 대체하거나 재시도하지 않습니다. 없는 제품은 보고되는 거절이지 fallback이 아닙니다.

실행 경로 고르기

한정된 실행 하나, 남는 기록 하나

정확한 한도 아래 환불 규칙을 실행하고, 확인한 것을 남기세요.

네이티브 lispex rule run은 검토한 규칙을 준비하고 엄격한 JSON 입력 하나를 받아 bounded 평가기에서 한 번 평가합니다. bounded 평가기는 별도의 import 없는 엔진으로, 선언한 한도 안에서 모든 작업과 할당을 셈해야만 진행합니다. 남는 것은 다섯 구성원의 결정 디렉터리입니다. 준비된 규칙 아티팩트, 정규 입력, 정확한 요청 결속을 담은 결정적 결과, 발급 자격이 있는 portable core, 파생 요약 — 그리고 원본 규칙 소스는 의도적으로 여기에 없습니다.

01검토한 규칙
02엄격한 JSON 입력
03결정: allow
04확인 가능한 portable core

1. 규칙

LISPEX

(let ((days (cdr (car input)))
      (opened (cdr (car (cdr input)))))
  (if (< days 15)
      (if opened "deny" "allow")
      "deny"))

2. 입력

JSON

{
  "days": 14,
  "opened": false
}

3. 한정된 실행 한 번

SHELL

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

4. 결정

유지되는 14일 미개봉 사례에서 한정된 실행이 돌려주는 결정은 allow.

5. 세 방식의 기록 확인

rule inspect는 실행 없이 디렉터리를 요약하고, rule verify는 역시 실행 없이 정확한 구성원 집합·identity·해시·결속을 검사하며, rule replay는 기록된 요청을 새 평가기 인스턴스에서 한 번 평가해 같은 결과를 요구합니다. 셋 모두 권한을 부여하지 않습니다.

portable core가 결속하는 것

의미 규칙, 정규 입력, 정확한 한도, 정확한 평가기 아티팩트, 결정적 결과 — 어떤 질문에 어떤 상한 아래에서 답했는지를 정확히 알기에 충분합니다. 소모했거나 남은 사용량은 portable core에 들어가지 않습니다.

기록이 성립시키지 않는 것

누가 실행했는지, 신선한지, 규칙에 담긴 정책이 공정하거나 옳은지, 같은 결정이 두 번 쓰였는지, 프로세스 밖에서 행동할 권한 — 어느 것도 성립시키지 않습니다.

전체 결정 흐름 따라 하기

정확한 리스펙스 이미지

결정 규칙을 결정적 이미지로 전달할 수 있습니다.

이미지는 규칙의 정확한 소스 바이트를 담는 정규 그림 파일입니다. 여기 담긴 것은 정식 Decision을 반환하는, 검토를 마친 환불 규칙입니다 — 바우치가 증거를 발급할 수 있는 유일한 결과 형태입니다. 로컬에서 소스를 복원하고, 바이트가 정규임이 증명된 뒤에만 실행하고, 증명된 이미지를 아래 바우치 흐름의 정확한 소스로 고정할 수 있습니다. 픽셀이 담는 것은 무결성뿐입니다.

LISPEX

(define days-since-delivery (car input))
(define opened? (car (cdr input)))

(if (<= days-since-delivery 14)
    (if opened?
        (decision-deny)
        (decision-approve))
    (decision-deny))

여기서 한 갈래 길이 아래로 이어집니다. 이 이미지를 복원해 증명하고, 정확한 소스로 고정하고, 네이티브에서 정확한 입력 하나에 대한 서명된 바우치 증거를 발급합니다. 수신자는 자신이 소유한 신뢰 정책으로 그 증거를 인증하고, 자기 머신에서 규칙을 다시 실행해 로컬 gate를 통과시킵니다. 그다음 실제로 행동할지는 외부 애플리케이션이 따로 결정합니다. 이미지 자체는 이 중 무엇도 아닙니다 — 서명된 증거도, 신뢰도, 권한도 아니며, 오직 바이트를 정확히 나를 뿐입니다.

리스펙스 바우치

결정은 영수증을 둘 수 있다.

Vouch는 기록된 결정 하나를 서명된 이식 가능한 증거로 만들고, 증거와 허가를 끝까지 분리합니다.

영수증(receipt)은 실행 한 번의 서명된 기록입니다: 어떤 규칙 바이트가 실행됐고, 어떤 입력 바이트가 들어갔고, 어떤 결정이 나왔는가. 네이티브 릴리스 바이너리의 lispex vouch issue는 검토한 규칙을 직접 실행해 영수증을 만듭니다 — 기록되는 것은 누군가의 주장이 아니라 실제로 일어난 일입니다. 영수증·소스·입력은 하나의 파일, 묶음(bundle)으로 함께 이동할 수 있습니다. 묶음은 누구든 네이티브나 npm의 lispex vouch verify로 인증할 수 있고, 이 인증이 답하는 질문은 정확히 하나입니다: 내가 신뢰하기로 한 키가 이 정확한 바이트에 서명했는가? 그 외에는 의도적으로 아무것도 답하지 않습니다.

리스펙스 바우치 알아보기

요청 결속 Vouch

bundle이 gate가 실행할 요청을 고를 수 없습니다.

재실행은 bundle의 주장이 아니라 당신이 고정한 요청에서 시작합니다.

요청 결속은 당신의 머신이 당신이 요청한 것만 다시 실행한다는 규칙입니다. 묶음은 발행자가 관측한 것을 증명할 뿐, 당신 쪽에서 어떤 규칙과 입력이 실행될지 고를 수 없습니다. 그래서 재실행 전에 요청을 직접 고정합니다: 규칙 소스 — 직접 가진 파일이거나 완전한 정규 증명을 통과한 이미지 — 와 정확한 입력. 검증은 서명을 먼저 인증하고, 그다음 묶음을 고정한 요청과 비교하며, 정확히 일치할 때만 실행으로 이어집니다. 아무것도 고정하지 않으면 검증은 서명 확인에 머물고, 재실행이나 gate에 결코 도달할 수 없습니다.

검증·재실행·gate

재실행은 당신의 머신이 수행하는 비교입니다.

gate는 정확한 살아 있는 일치에서만 성공하며, 그 위에 직접 구성한 trust policy가 놓입니다.

lispex vouch gate는 구체적인 질문 하나를 가진 로컬 검사입니다: 지금, 이 머신에서, 고정한 요청으로 규칙을 다시 실행하면 서명된 결과와 정확히 같은 결정이 나오는가 — 그리고 그 결정이 내가 요구한 결정인가? 증거가 들어가고 종료 코드가 나옵니다. 그 위에 신뢰 정책(trust policy)이 놓입니다: 직접 검토한 공개 키, 정확한 평가기, 받아들일 정확한 규칙 소스나 증명된 이미지를 적어 스스로 작성하고 감사하는 짧은 설정 파일입니다. 유효하게 서명됐어도 정책에 없는 규칙은 거부됩니다. 정책은 그 자체로 아무것도 허가하지 않습니다 — 당신이 검사할 대상을 좁힐 뿐입니다.

의도된 한계

성공한 gate가 주지 않는 것.

아래 경계는 모두 의도된 것입니다. 통과한 보고서는 다음 단계를 위한 증거일 뿐입니다.

통과한 verify·gate 보고서는 허가도, 토큰도, 외부 행동 권한도 아닙니다. 실제로 환불하고 지불하고 배송할지는 애플리케이션이 따로 내리는 결정입니다. 요청 결속이 증명하는 것은 고정한 요청과의 동일성이지 신선도·유일성·재전송 방지가 아닙니다. 이미지는 복원된 소스 바이트가 온전하다는 것만 증명하지, 신뢰해도 된다는 것을 증명하지 않습니다. npm은 검증과 인증만 할 수 있고 발급·재실행·gate는 할 수 없으며, 브라우저 WASM과 플레이그라운드는 평가만 합니다. 그리고 일상 실행의 어떤 것도 — 경로 lock, 측정, 실행 출력 — 바우치 권한이 되지 않습니다.

전체 Vouch 흐름 실행하기

생각의 원형을 담는 언어.

The language that captures the shape of thought.

Язык, воплощающий форму мысли.