확률적 Iris를 향한 첫 걸음: 독립성, 조건부 확률, 그리고 동적 힙 할당의 조화

확률적 분리 논리 (probabilistic separation logics) 분야에서 최근 흥미로운 진전이 있었습니다. PSL, Lilac, Bluebell, pcOL을 포함하는 이들의 중요한 하위 클래스는 *범용 확률 논리 (general-purpose probabilistic logics, 줄여서 GPLs)*입니다. 이는 프로그램 상태의 확률 분포에 대한 기본적인 Hoare 스타일의 단언 (assertions)과 함께, 독립성 (independence) 및 *조건부 확률 (conditioning)*과 같은 강력한 모듈성 원칙을 제공함을 의미합니다. 그러나 이러한 논리 중 어느 것도 동적으로 할당된 메모리(즉, 힙(heap) 내의 포인터)에 대한 추론을 지원하지 않으며, Iris와 같은 현대적 분리 논리의 더욱 정교한 자원 대수 기반 고스트 상태 (ghost state)는 말할 것도 없습니다. 우리는 이것이 근본적인 장애물 때문이라고 주장합니다. 즉, 서로 다른 무작위 결과에 따라 메모리의 형태(및 메모리 위치의 정체성)가 달라질 수 있기 때문에, 포인터 소유권 (pointer ownership)을 확률적 독립성 및 조건부 확률과 어떻게 조화시킬 수 있을지가 불분명하기 때문입니다. 또한, 기존의 GPL 중 어느 것도 증명 보조기 (proof assistant)에서 기계화되지 않았습니다. 본 논문에서 우리는 Amaryllis라는 형태로 GPL과 Iris와 같은 현대적 분리 논리를 결합하기 위한 실질적인 첫 걸음을 내딛습니다. Amaryllis는 동적 메모리 할당을 처리하면서 동시에 독립성 및 조건부 추론을 지원하는 최초의 GPL입니다. 앞서 언급한 장애물을 극복하기 위해, 우리는 확률적 단언에 대한 새로운 인덱스된 가치 평가 (indexed valuation) 스타일의 모델을 제안하며, 이를 통해 표준 Iris 스타일의 자원(예: 힙)의 소유권을 일반적인 방식으로 분포 수준의 소유권으로 승격시킬 수 있습니다. 그런 다음 우리는 프레임 보존 업데이트 (frame-preserving update), 권위 있는 자원 대수 (authoritative resource algebras), 그리고 *최약 전제 조건 양상 (weakest precondition modality)*과 같은 Iris의 핵심 개념을 확률적 추론에 대해 건전하게 적응시키고 동적 할당을 검증하는 방법을 보여줍니다. 마지막으로, 우리는 모든 결과를 Rocq 증명 보조기에서 기계화하였으며, Amaryllis 내에서 증명을 수행하기 위한 Iris 기반의 증명 모드를 개발하였습니다.