결정 영수증과 CSK Reference

Lispex의 검사 가능한 부분집합은 CSK Reference의 소스 언어입니다. 입력을 고정해 평가하면 결정 영수증이 남고, verify와 replay로 오프라인 검사와 규칙 변경 비교를 합니다.

v1.3부터 Lispex의 검사 가능한 부분집합은 CSK Reference의 공개 소스 언어입니다. 이 약속은 일부러 좁게 잡았습니다. Lispex 프로그램을 실행하는 권위는 여전히 레퍼런스 인터프리터에 있습니다. CSK Reference가 다루는 것은 그중에서도 평가 결과를 나중에 내 컴퓨터에서 다시 확인할 수 있도록 닫아 둔 부분집합입니다.

흐름

작은 결정 규칙을 쓰고, 그 규칙이 읽을 입력을 고정합니다. 규칙을 평가하면 결정 영수증이 남습니다. csk.differential-receipt/v0 형식의 파일 하나가 규칙과 고정된 입력, 그리고 답을 해시로 묶어 줍니다.

영수증이 생긴 뒤에는 두 가지를 할 수 있습니다.

  • lispex verify <receipt>는 영수증과 그 안에 연결된 해시를 오프라인으로 검사합니다. 네트워크도 별도 서비스도 필요 없이 파일 하나면 충분합니다.
  • lispex replay <corpus> --against <version-or-receipts-dir>는 규칙을 고친 뒤 커밋된 결정 코퍼스를 버전 핀이나 영수증 디렉터리와 비교해서 어떤 답이 달라졌는지 보고합니다.

검사 가능한 부분집합이란

같은 규칙에 같은 입력을 주면 언제나 같은 결과가 나오도록 좁게 닫아 둔 Lispex의 일부입니다.

  • 문법은 R7RS 계보를 따르는 고정된 폼만 씁니다. 매크로도 숨은 상태도 없습니다.
  • 내장 프로시저가 고정되어 있고, 입력은 호스트가 명시적으로 바인딩합니다. 규칙이 스스로 데이터를 가져오지 않습니다.
  • 규칙 갤러리 코퍼스에는 기대 아티팩트가 규칙 옆에 나란히 들어 있습니다.
  • 영수증, 리포트, 그래프, 매니페스트, 릴리스 번들은 바이트 단위로 고정된 JSON 규약을 따릅니다.

영수증이 말해 주는 것과 말해 주지 않는 것

영수증은 특정 규칙이 특정 고정 입력에 대해 특정 답을 냈다는 사실, 그리고 기록된 아티팩트들이 서로 어긋나지 않는다는 사실을 보여 줍니다. 그 결정이 실제로 누군가에게 적용됐는지, 언제 누가 적용했는지는 말해 주지 않으며, 사람의 검토를 대신하지도 않습니다. 그런 일은 서명, 타임스탬프, 배포, 리뷰라는 별도의 계층이 다룹니다.

npm으로 설치하는 verifyreplay는 공개 규격 아티팩트를 검사하는 도구입니다. 바이트와 해시를 확인할 뿐, Lispex 소스를 실행하지 않으며 레퍼런스 인터프리터를 대체하지 않습니다.

어디서 무엇을 볼 수 있나

  • 이 사이트의 플레이그라운드에서 검사 가능한 부분집합에 속하는 규칙을 바로 평가해 볼 수 있습니다.
  • npm install -g lispex로 설치한 CLI에서는 lispex run으로 파일을 평가하고, lispex verifylispex replay로 영수증과 코퍼스를 검사합니다. 예제는 시작하기에 있습니다.
  • 부분집합 정의, 영수증 형식, 검증과 재실행 리포트 규약을 담은 규격 문서와 결정 갤러리 코퍼스는 별도의 CSK Reference 공개 배포물로 제공됩니다. 공개 위치가 확정되면 이 문서에서 안내하겠습니다.