확률론적 프로그램은 많은 응용 분야에서 중요합니다. 특히 보안 응용 분야에서는 임의의 적대자, 즉 알려지지 않은 코드의 존재 하에서도 성립하는 속성을 확립하는 것에 관심이 있습니다. 우리는 Elton을 제시합니다. 이는 알려지지 않은 적대적 코드를 활용하여 고차원 확률론적 프로그램에 대한 추론을 위한 고계(higher-order) 분리 논리입니다. Elton은 언어 수준에서 지연 샘플링(delayed samplings)을 사용하여 분포적 속성(distributional properties)에 대한 불변 조건(invariants)을 명시하기 위한 새로운 논리 시설과, 논리 수준에서 우븐 리소스(urn resources)라고 불리는 새로운 종류의 분리 논리 술어(separation-logic predicate)를 통합합니다. 우리는 이러한 확장 기능들이 건전하며 표준 호출-값 의미론(call-by-value semantics)으로 지워질 수 있음을 보여줍니다. 또한, 불변 조건이나 고스트 리소스(ghost resources)와 같은 다른 기능들과 결합하여, Elton은 광범위한 보안 예제에 대한 오차 경계(error bounds)를 증명할 만큼 충분히 표현력이 높으며, 이 중 일부는 이전 기술의 범위를 넘어섭니다. 모든 증명은 Rocq 증명 보조기와 Iris 분리 논리 프레임워크로 기계화되었습니다.