unsafe powers

unsafe는 권한이 아니라 컴파일러가 못 보는 조건을 사람이 증명하는 표시다

unsafe 블록 안에서도 대여 검사와 타입 검사는 계속 작동한다. 다만 다섯 작업의 전제 조건은 프로그래머가 직접 증명한다.

증명 범위 포인터 유효성, 초기화 상태, 별칭 규칙, 스레드 안전성, 외부 ABI 계약을 코드 근처에 남긴다.

unsafe 슈퍼파워 증명표
허용 작업	무엇을 하는가	사람이 증명할 조건	감싸는 기준
raw pointer 역참조	주소의 값을 직접 읽거나 쓴다.	유효한 주소, 정렬, aliasing 규칙	안전 함수는 잘못된 포인터를 만들지 못하게 한다.
unsafe 함수 호출	호출 전 조건이 있는 함수를 실행한다.	문서의 safety 계약 충족	검사와 변환을 호출 직전에 모은다.
mutable static	전역 변경 상태에 접근한다.	데이터 경합 방지와 동기화	전역 접근 경로를 하나로 좁힌다.
unsafe trait 구현	컴파일러가 모르는 불변조건을 약속한다.	모든 구현 경로의 불변식 유지	타입 생성자에서 깨진 상태를 차단한다.
union 필드 접근	같은 메모리를 다른 필드로 해석한다.	현재 활성 필드와 초기화 상태	읽기 가능한 변형만 API로 노출한다.

Invariant 길이, 정렬, 수명, 중복 접근 조건을 unsafe 근처에 적는다.

Small scope unsafe 블록은 작게 유지하고 안전 API가 경계를 감싼다.

Miri 테스트와 Miri로 포인터·초기화·별칭 문제를 추가 점검한다.

Review 코드 리뷰는 기능보다 safety 계약이 실제로 지켜지는지 본다.