From bef741e1bae49198bff740a7cecd83621383df0d Mon Sep 17 00:00:00 2001 From: coolguy Date: Sun, 30 Aug 2026 00:42:18 +0900 Subject: [PATCH] =?UTF-8?q?thesis:=20Alias/Move=20=EB=AA=A8=EB=8D=B8?= =?UTF-8?q?=EC=9D=84=20v0=20=ED=95=84=EC=88=98=EB=A1=9C=20=EC=8A=B9?= =?UTF-8?q?=EA=B2=A9=ED=95=98=EA=B3=A0=20incremental=20=EA=B7=9C=EC=B9=99?= =?UTF-8?q?=20=EC=A0=95=EC=A0=95?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit "일반 ownership은 v0 제외"를 폐기한다. 없는 것은 borrow checker와 lifetime이지 alias 규칙이 아니며, 최소 move 모델 없이는 "safe code에 data race 없음" 주장이 closure·channel·container 경로에서 새어나간다. 신설: - Alias/Move 모델: copyable/affine 이분, 전 경로 move, first-class reference 없음. 검사는 함수 로컬 데이터플로우로 결정. - Capability 전달: second-class use가 기본(탈출 금지), 이전 시에만 move. non-duplication은 복제 금지이지 재사용 금지가 아니다. - Affinity 전이: affine 필드를 가진 타입은 자동 affine. 없으면 wrapper 복사로 non-duplication 정리가 깨진다. - Effect의 정적/동적 층 분리: 정적 층은 타입 수준까지, 값 identity 귀속은 동적/툴링 층. 정정: - interface hash 입력을 exported surface 전체의 의미적 정규형으로 재정의. - invalidation을 "direct dependents로만 전파"에서 hash 고정점 규칙으로 교체. v0 측정 시나리오를 본문 수정 / 시그니처 수정 둘로 분리. - 형식 명세 투자 범위를 affine 전이 규칙과 non-duplication까지 확장. - v0 포함/제외 목록과 v1 계획(제한적 second-class borrow) 갱신. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_019ZVDeU6KLuUVL3gs18Hm3E --- docs/thesis.md | 87 ++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 78 insertions(+), 9 deletions(-) diff --git a/docs/thesis.md b/docs/thesis.md index bfc55f5..9281f41 100644 --- a/docs/thesis.md +++ b/docs/thesis.md @@ -18,6 +18,7 @@ AI의 코드 생성 속도 >> 신뢰 확보 속도. 3. 피해는 더 좁게: 권한은 명시적 capability로만 전달 → ambient authority 없음. AI가 틀려도 언어가 폭발 반경 봉쇄 → 자원(File, Lock, Secret 등)은 affine ownership + → affine은 전이된다: affine 필드를 가진 타입은 자동으로 affine 4. 리뷰는 의미 단위로: 도구가 semantic diff 제공 → "Effects: +payment.refund" 수준으로 리뷰 압축 5. 한 개념 = 한 방식: syntax variant 최소화, 공식 formatter 하나, @@ -25,11 +26,49 @@ AI의 코드 생성 속도 >> 신뢰 확보 속도. ■ 파생 결정 -동시성 (철학 1,2,3에서 파생): +Alias/Move 모델 (철학 1,3에서 파생 — 언어 전체의 토대): +※ 없는 것은 borrow checker와 lifetime이지 alias 규칙이 아니다. + 최소 move 모델은 v0 필수다. +- 모든 타입은 copyable 또는 affine 둘 중 하나. + 일반 데이터는 copyable, 자원·capability는 affine +- affine 값은 모든 경로에서 move다: 대입, 함수 인자, 반환, channel 전송, + container 삽입, closure by-move capture. moved 이후 사용은 compile error + ※ 이 검사는 함수 로컬 데이터플로우만으로 결정된다 (전역 분석 불필요) +- v0에 first-class reference는 없다. mutable 데이터는 소유 변수를 통해서만 변경 +- 공유는 deep immutable 값만 가능 (내부 가변성 타입은 v0에 없음) +근거: "safe code에 data race 없음"은 spawn만 막아서 성립하지 않는다. closure, +channel, container, 인자/반환 전 경로에서 mutable alias가 없어야 하며, 값 의미론 ++ move-only가 이를 borrow 분석 없이 닫는 유일한 단순 모델이다. +대가: 값을 "빌려주고 돌려받는" 패턴은 반환으로 명시해야 한다. + v1에서 제한적 second-class borrow로 완화 예정. + +Capability 전달 (Alias/Move 모델의 제3의 규칙): +※ 매 호출 move는 실용성이 붕괴하고, 자유 참조는 non-duplication이 붕괴한다. + capability는 second-class "use" 전달을 기본으로 한다. +- 기본은 use(호출 동안의 임시 접근): 호출자는 호출 후에도 계속 보유하고, + 피호출자는 사용만 할 수 있다 +- use로 받은 capability는 탈출 불가: 반환 금지, struct 저장 금지, + channel 전송 금지, 호출보다 오래 사는 closure에 capture 금지 + ※ 탈출 검사는 함수 로컬로 결정 가능 +- 소유권 이전이 필요할 때만 명시적 move +근거: non-duplication은 "복제 금지"이지 "재사용 금지"가 아니다. use는 복제를 +만들지 않으므로 보안 정리와 양립하고, 탈출 금지가 locality를 보존한다. + +Affinity 전이 (보안 주장의 필수 전제): +- capability(또는 affine 타입)를 필드로 포함하는 타입은 자동으로 affine이다. + 컴파일러가 타입 정의에서 유도하며 전이적으로 적용된다 +- copyable 선언과 affine 필드의 공존은 compile error +- 타입의 affinity는 exported interface surface의 일부이며 interface hash에 포함된다 +근거: 이 규칙이 없으면 Box{pay}를 복사하는 것만으로 capability가 사실상 복제되어 +non-duplication 정리가 깨진다. + +동시성 (철학 1,2,3에서 파생 — Alias/Move 모델의 특수 사례): - green thread (async/await의 function coloring은 철학 5 위반) - structured concurrency만 허용: 태스크 수명 = 블록 구조 (locality) - 데이터 경쟁은 격리로: mutable은 단일 소유, channel로 소유권 이동, - 공유는 immutable만 (borrow checker는 complexity budget 초과) + 공유는 deep immutable만 (borrow checker는 complexity budget 초과) +- spawn closure는 by-move capture 또는 immutable capture만 허용. + mutable 참조 capture는 문법적으로 금지 - spawn은 effect로 선언 → 동시성이 시그니처에 드러남 Effect 다형성 (철학 2,5에서 파생): @@ -48,12 +87,34 @@ Effect 다형성 (철학 2,5에서 파생): - 완화 장치 하나만 예약: 클로저 인자의 effects 생략 시 {}로 기본 해석 (추론이 아니라 기본값이므로 헌법 위반 아님) +Effect의 정적/동적 층 분리 (철학 2,4에서 파생): +- 정적 층(effect check)은 타입 수준까지만 다룬다: PaymentGateway.refund. + capability 값의 identity는 unification에 등장하지 않는다 (결정성·단순성 확보) +- "어느 capability 값이 쓰였는가"는 동적/툴링 층의 몫: capability는 unforgeable + 하므로 값 전달 경로 추적, audit id, semantic diff로 귀속한다 +- 즉 폭발 반경의 상한은 타입이 정적으로 보장하고, 정확한 귀속은 동적 층이 담당한다 + 인터페이스 경계 (철학 2 + incremental + AI context locality가 한 점에서 만남): - public 함수 경계에서 타입과 effect는 전부 명시 - 본문의 추론 결과는 어떤 것도 인터페이스로 새지 않는다 -- interface hash는 명시된 시그니처 텍스트(정규화 후)만으로 계산한다 ※ 본문 한 줄 수정이 해시를 흔들면 incremental 전제가 무너진다 +interface hash의 입력 = 모듈 exported surface 전체의 의미적 정규형: +- exported 함수 시그니처 (effect 포함) +- exported type 정의 본문 (struct 필드, enum variant — exhaustiveness에 직결) +- 타입의 affinity (copyable / affine) +- exported constant의 타입과 값 +- capability/effect 선언 +- re-export 목록 +원칙: downstream 검사 결과에 영향을 줄 수 있는 모든 것을 포함한다. 의심스러우면 +넣는다 — 과잉 포함의 비용은 재검사지만 누락의 비용은 잘못된 캐시라는 비대칭. + +invalidation 전파 = 고정점 규칙 ("direct dependents로만 전파"가 아니다): +1. 변경된 모듈의 direct dependents를 재검사 +2. 그중 interface hash가 실제로 바뀐 모듈만 다음 단계로 전파 +3. hash가 안정되는 지점에서 중단 +※ implementation-only 변경은 1단계에서 멈춘다 (hash 불변 → 전파 0) + Generics (철학 2에서 파생): - 기본 shared implementation, monomorphization은 명시적 요청 시만 - "compile speed by default, runtime specialization by request" @@ -69,10 +130,11 @@ Generics (철학 2에서 파생): 명세 (철학 3에서 파생): - Go식 산문 명세 + conformance test suite - 형식 명세는 보안 주장을 지탱하는 최소 단위에만 투자: - effect + capability + capability를 담는 자원의 affine 규칙 + effect + capability + affine 전이 규칙 + non-duplication 성질 ※ 주장은 두 정리의 결합이다 — (i) capability 없이는 effect를 수행할 수 없다, - (ii) capability는 safe code에서 복제·위조되지 않는다. - (ii)가 빠지면 핸들 복제 한 번으로 (i)이 공허해진다 + (ii) safe code에서 capability는 복제·위조되지 않는다. + (ii)가 빠지면 핸들 복제 한 번으로 (i)이 공허해지고, + (ii)에는 affinity 전이가 필수 전제다 (없으면 wrapper 복사로 우회된다) ※ 일반 데이터의 ownership 전체는 형식화 대상이 아니다. 보안 주장을 지탱하는 non-duplication 성질만 증명 대상 - 명세와 구현을 같이 키우되 충돌 시 명세가 이긴다 @@ -83,8 +145,10 @@ Generics (철학 2에서 파생): ■ v0 — "기능의 서브셋, 아키텍처의 풀셋" 목표: 시스템 속성(빠른 검증 루프)은 측정으로만 증명된다. -성공 기준(숫자): 10만 줄 규모에서 함수 수정 시 check 50ms 이내, -invalidation은 direct dependents로만 전파. +성공 기준(숫자): 10만 줄 규모에서 함수 수정 시 check 50ms 이내. +측정 시나리오는 둘로 분리한다 — + (a) 본문만 수정(implementation-only): downstream 재검사 0건 + (b) 시그니처 수정(interface 변경): hash 고정점까지만 전파 성공 기준(체감): 표준 라이브러리급 코드 샘플을 이 규칙(명시 effect 변수 포함)으로 작성해 리뷰 가능성 확인. 시그니처가 effect 변수로 도배되면 설계 실패다. ※ 최우선 검증 대상은 성능만이 아니다 — "이 설계로 짠 일상 코드가 읽을 만한가"가 @@ -92,6 +156,8 @@ invalidation은 direct dependents로만 전파. 포함 (되돌리기 비싼 것 전부): - parse → name resolution → type check → effect/capability check +- move/affinity 검사, capability use 규칙, affinity 전이 +- effect 변수 (effect 다형성) - interface artifact + hash 기반 incremental invalidation - cool check - 얇은 typed IR + tree-walking interpreter (cool run 대용) @@ -99,7 +165,9 @@ invalidation은 direct dependents로만 전파. ※ effect check가 fast path 예산 안에 드는지가 사활 → 최우선 검증 대상 제외 (아키텍처 검증 후 얹어도 되는 것): -- generics, contracts, 일반 ownership(자원 몇 개 하드코딩으로 대체) +- generics, contracts +- borrow checker, lifetime, first-class reference, 내부 가변성 타입 +- second-class borrow의 일반화 (v1) - LLVM/cranelift, release build, 독립 verifier, semantic diff - Mutex 등 공유 mutable 탈출구 (필요가 증명되기 전 열지 않음) @@ -114,6 +182,7 @@ invalidation은 direct dependents로만 전파. - 독립 verifier: compiler를 통짜로 신뢰하지 않고 IR invariants 재검증 - semantic diff, IR 기반 semantic operations (AI 툴링) - generics 완성, contracts, 공유 mutable 탈출구(명시적 타입 하나) +- 제한적 second-class borrow (Alias/Move 모델의 "반환으로 돌려받기" 대가 완화) ■ 검증 계층 (fast/slow 분리의 구체화) L0 parse / L1 type·effect·capability·ownership → 매번, ms 단위