thesis: Alias/Move 모델을 v0 필수로 승격하고 incremental 규칙 정정

"일반 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) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019ZVDeU6KLuUVL3gs18Hm3E

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) safe code에서 capability는 복제·위조되지 않는다.
-     (ii)가 빠지면 핸들 복제 한 번으로 (i)이 공허해진다
+     (ii)가 빠지면 핸들 복제 한 번으로 (i)이 공허해지고,
+     (ii)에는 affinity 전이가 필수 전제다 (없으면 wrapper 복사로 우회된다)
   ※ 일반 데이터의 ownership 전체는 형식화 대상이 아니다.
      보안 주장을 지탱하는 non-duplication 성질만 증명 대상
 - 명세와 구현을 같이 키우되 충돌 시 명세가 이긴다
@@ -83,8 +145,10 @@ Generics (철학 2에서 파생):
 
 ■ v0 — "기능의 서브셋, 아키텍처의 풀셋"
 목표: 시스템 속성(빠른 검증 루프)은 측정으로만 증명된다.
-성공 기준(숫자): 10만 줄 규모에서 함수 수정 시 check 50ms 이내,
+성공 기준(숫자): 10만 줄 규모에서 함수 수정 시 check 50ms 이내.
-invalidation은 direct dependents로만 전파.
+측정 시나리오는 둘로 분리한다 —
+  (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 단위