diff options
| author | eunhhu <[email protected]> | 2026-09-24 17:14:54 +0100 |
|---|---|---|
| committer | eunhhu <[email protected]> | 2026-09-24 17:14:54 +0100 |
| commit | b1ce1927022d374198441afafeb27199fc8a052a (patch) | |
| tree | 6021f175f4c67ed03b44240eaa2f90d846f12f6f /docs/design/001-operation-semantics.md | |
| parent | d34f9426d5317a1948f12f229439946728bc342a (diff) | |
| download | pure-b1ce1927022d374198441afafeb27199fc8a052a.tar.gz pure-b1ce1927022d374198441afafeb27199fc8a052a.zip | |
Establish native micro runtime checkpoint
Diffstat (limited to 'docs/design/001-operation-semantics.md')
| -rw-r--r-- | docs/design/001-operation-semantics.md | 126 |
1 files changed, 126 insertions, 0 deletions
diff --git a/docs/design/001-operation-semantics.md b/docs/design/001-operation-semantics.md new file mode 100644 index 0000000..ae2ed5d --- /dev/null +++ b/docs/design/001-operation-semantics.md @@ -0,0 +1,126 @@ +# 연산 의미 초안 0.1 + +상태: **다음 구현을 위한 명세**. 현재 제작 도구의 문법·실행기를 변경하지 않는다. +아래에서 `현재`는 구현을 확인한 동작, `제안`은 후속 구현의 요구조건이다. +현재 동작의 기준은 [Workbench 계약](../../prototypes/workbench/CONTRACT.md)이다. + +## 1. 연산의 구분 + +| 종류 | 읽고 바꾸는 것 | 실패의 의미 | +|---|---|---| +| 순수 계산 | 명시적인 값·읽기 전용 데이터 | 결과 없음; 외부 효과 없음 | +| 상태 전이 | 한 실행 영역의 관리 상태 | 확정 전 실패는 이전 관리 상태 유지 | +| 버퍼 변환 | 입력 구간, 독점 출력 구간, 변환 문맥 | 이번 호출의 유효 출력과 문맥의 재사용 가능 여부를 명시 | +| 외부 작업 | 파일·네트워크·장치·시계 등 | 이미 발생한 효과가 남을 수 있음; 실제 완료로 보고 | + +이 구분은 제안이다. 현재 코어에는 앞의 두 종류와 순수한 표시 계산만 있다. +비용이나 실패 의미가 다른 작업을 모두 숫자 함수처럼 처리하지 않는다. +재계산 가능한 연산은 첫 종류로 제한한다. 파일 쓰기·난수 획득·작업 제출은 재계산으로 반복하지 않는다. + +## 2. 현재 숫자 규칙과 확장 경계 + +현재 상태는 유한한 `f64`다. 대입과 같은 이벤트의 핸들러는 소스 순서로 실행한다. +`if` 조건은 한 번 계산하며 `&&`·`||`는 양쪽을 모두 평가한다. +0 나눗셈, 유한하지 않은 계산 결과, 스택·분기 오류는 이벤트 전체의 숫자 상태 변경을 취소한다. +표시 표현식은 상태·이벤트 진단을 변경하지 않는다. + +현재 시간 입력은 프레임당 1/60초, 일반 입력에서 0이다. +이는 작은 화면 실험의 규칙이다. 서버의 시계나 미디어 타임스탬프에 60Hz를 강제하는 계약이 아니다. +후속 시간·난수·외부 완료는 명시적인 입력 기록으로 전달한다. + +제안하는 데이터 경계 규칙: + +- 바이트·버퍼 길이·오프셋·식별자는 정수로 다룬다. `f64`를 경유해 큰 정수의 정확성을 잃지 않는다. +- 길이·메모리 계산은 검사된 정수 연산을 사용한다. 넘치면 오류다. 축약·순환 연산은 별도 명시가 있어야 한다. +- 정수 폭, 바이트 단위, 정렬 요구와 변환 가능 범위를 각 연산에 기록한다. +- 부동소수점 확장은 연산 순서, 반올림·서브노멀·부호 있는 0 처리와 허용 오차를 명시한 뒤 추가한다. + 현재 테스트는 모든 네이티브 타깃의 비트 단위 일치를 증명하지 않는다. +- 기존 논리 연산을 단락 평가로 바꾸는 일은 의미 변경이다. 최적화라는 이름으로 조용히 바꾸지 않는다. + +Wasm의 수치 형식은 IEEE 754의 이진 형식과 부호 있는 0·NaN 등을 정의한다. +Pure가 허용하는 값·오류와 재생 비교 규칙은 그 위에 별도로 정해야 한다. +[WebAssembly 값 명세](https://webassembly.github.io/spec/core/syntax/values.html#floating-point) + +## 3. 관리 상태 확정과 외부 작업 제출 — 제안 + +한 이벤트에서 다음 순서를 지킨다. + +1. 관리 상태의 다음 값을 계산하고, 필요한 버퍼 대여·요청 슬롯·완료 슬롯을 예약한다. + 준비 중에는 외부 작업을 시작하거나 공유 출력 버퍼를 변경하지 않는다. +2. 검사·예약이 실패하면 준비한 자원을 반납하고 이전 관리 상태를 유지한다. +3. 성공하면 관리 상태와 준비된 작업 목록을 함께 확정한다. 이 단계는 외부 작업의 성공을 의미하지 않는다. +4. 어댑터가 확정된 작업을 실제로 제출한다. 제출 실패도 완료 사건으로 전달한다. +5. 완료 사건을 후속 상태 전이의 입력으로 처리한다. 재시도·보상·사용자 알림은 앱의 명시적 정책이다. + +이미 확정·제출된 파일 쓰기를 이후 이벤트의 실패로 되돌렸다고 보고하지 않는다. +처리 중 프로세스가 종료되는 경우의 내구성·중복 실행 방지는 이 메모리 내 계약에 포함하지 않는다. +영속 작업에는 이후 별도 로그·식별자·복구 계약이 필요하다. + +## 4. 바이트 스트림 연산 — 첫 모듈 프로파일 제안 + +첫 프로파일은 입력 구간 하나, 출력 구간 하나, 유지되는 문맥 하나를 받는다. +각 입력 구간은 유효 데이터 길이, 출력 구간은 쓸 수 있는 용량을 나타낸다. +v0 출력은 유효 길이가 0인 독점 버퍼이며 출력 오프셋은 0이다. 접두부의 유효 길이는 +완료 회수 시 `produced`로 교체한다. 기존 데이터에 덧붙이기·덮어쓰기는 이 프로파일에 없다. +한 번에 최대 32비트 길이의 구간을 다루며 전체 스트림의 누적 길이는 검사된 64비트 정수로 센다. +파일 전체를 한 버퍼에 넣어야 한다는 뜻은 아니다. + +반환값은 `consumed`, `produced`, `status`, `error`다. + +- `consumed`는 이번 입력 구간에서 다시 제공하지 않아도 되는 접두부 길이다. +- `produced`는 출력 구간 시작에서 후속 작업이 사용할 수 있도록 확정된 접두부 길이다. + 임시로 쓴 바이트·내부 복사량과 다르다. 나머지 출력 용량은 유효 데이터가 아니다. +- 각 길이는 제공된 구간 길이 이하여야 한다. 이전 호출의 양을 다시 포함하지 않는다. +- 입력 소비와 출력 생성은 서로 독립적이다. 입력을 다 소비해도 출력·종료 처리가 남을 수 있다. +- v0은 입력·출력에 같은 버퍼를 사용하는 것을 거절한다. 제자리 변환은 별도 협상할 확장이다. +- 요청 하나의 완료와 스트림 전체의 완료는 다르다. `NEED_INPUT/NEED_OUTPUT/MORE`를 + 반환한 요청도 대여를 종료하지만, 해당 스트림 문맥은 다음 요청을 위해 열린 상태로 남는다. + +| 상태 | 의미와 다음 행동 | +|---|---| +| `MORE` | 진전이 있었으며 다시 호출할 수 있음. 양쪽 길이가 0이면 사용할 수 없음 | +| `NEED_INPUT` | 아직 끝나지 않음. 새 입력 또는 입력 종료 통지를 기다림 | +| `NEED_OUTPUT` | 미처리 입력이나 내부 출력이 남음. 새 출력 용량을 마련하고 남은 입력부터 재개 | +| `DONE` | 이 문맥의 스트림 완료. 입력 종료를 단순히 소비했다는 뜻과 다름 | +| `FAILED` | 문맥 종료. 오류 코드 필수, 부분 소비·검증된 출력이 있으면 정확히 보고 | +| `CANCELLED` | 최종 취소 완료. 이미 검증·공개된 부분이 있으면 정확히 보고 | + +종료 통지 `END_INPUT`은 마지막 입력 뒤에 더 이상 입력이 없다는 약속이다. +부분 소비 시 남은 입력과 이 플래그를 함께 재제공한다. 마지막 입력을 모두 소비한 뒤에도 +`NEED_OUTPUT`이면 빈 입력·같은 플래그·새 출력으로 종료 처리를 계속한다. +`END_INPUT`이 설정된 호출에서는 `NEED_INPUT`을 반환하지 않는다. 더 읽어야 하는 잘린 데이터면 `FAILED`다. +`DONE`에 미소비 입력이 있으면 호출자가 다음 스트림·후행 데이터 정책을 결정한다. +`DONE/FAILED/CANCELLED` 문맥은 후속 `step`을 받지 않으며 닫기만 허용한다. + +Zstd는 입력·출력 위치와 종료 진행을 따로 보고하며 내부 윈도 메모리도 필요로 한다. +이 자료는 위 프로파일을 설계하는 근거이며 Zstd의 API를 Pure의 보편 규칙으로 간주하지 않는다. +참조한 매뉴얼은 1.5.1이고 채택할 라이브러리 버전은 아직 결정하지 않았다. +[Zstandard 스트리밍 매뉴얼](https://facebook.github.io/zstd/zstd_manual.html#Chapter7) + +## 5. 부분 성공과 인증 + +위 스트림 프로파일은 바이트 변환의 결과다. 파일·네트워크 출력은 별도 효과 결과로 +실제로 전달한 바이트 수를 보고해야 한다. 변환의 `produced`를 파일에 저장된 양으로 재사용하지 않는다. + +인증 복호화 어댑터는 성공한 인증 단위의 평문만 유효 출력으로 공개한다. +현재 단위의 인증에 실패하면 그 단위의 `produced`는 0이고 임시 평문은 공개하지 않는다. +이전 호출에서 인증·공개된 단위까지 되돌렸다고 주장하지 않는다. +단위 크기와 보류 버퍼에 예산을 두고 검증된 라이브러리의 계약을 따른다. +암호 알고리즘을 이 명세에서 새로 정의하지 않는다. +[libsodium 인증 암호화 API](https://doc.libsodium.org/secret-key_cryptography/secretbox) + +## 6. 컴파일러가 감당하는 작업 + +현재 한도는 소스 32,768바이트, 상태 32개, 입력 8개, 출력 24개, 핸들러 64개, +중간 명령 512개, 스택 64칸이다. JS 파서·AST·맵의 실제 최대 힙은 아직 측정되지 않았다. + +제안: 코어 연산 집합은 버전으로 관리하고 코덱·문서·미디어 라이브러리는 모듈로 연결한다. +라이브러리마다 새 문법·타입별 특수화·컴파일타임 실행을 추가하지 않는다. +모듈 호출 한 개가 적은 작업이라는 가정도 하지 않는다. 데이터 구간·문맥 메모리·한 호출의 +최대 작업량을 별도로 제한한다. 중단할 수 없는 라이브러리 호출에는 엄격한 CPU 시간 보장을 표기하지 않는다. + +추가 기능마다 컴파일러 산출물 크기, 빌드 시간, 피크 메모리, 생성 코드 크기와 실행 비용을 분리 측정한다. +초기 확장에는 전역 타입 추론·사용자 컴파일타임 실행·제한 없는 특수화를 도입하지 않는다. +특수화가 필요해지면 적용 대상을 제한한 후보와 공통 코드 후보를 비교한다. +이는 Pure의 설계 선택이다. Rust는 타입별 코드 생성의 이득과 빌드 시간·바이너리 크기 비용을 문서화한다. +[Rust 단형화 문서](https://rustc-dev-guide.rust-lang.org/backend/monomorph.html) |
