Creusot 0.14.0 출시 - Rust 계약을 형식 검증으로 증명하기

Rust 형식 검증 도구 Creusot 0.14.0이 부분 순서 명세, 스냅샷의 검증 조건 생성, rust-analyzer의 Pearlite 명세 이동 기능을 추가했습니다. 프로그램 코드와 증명 명세를 분리해 다루면서 증명 오류를 일찍 찾고 명세 안에서 정의를 탐색하기 쉬워졌습니다.

주제: Rust 형식 검증 개발 도구

에디터 노트

이번 변경에서 실용적인 차이는 스냅샷을 증명 전용 표현으로 분명히 구분하면서도 그 안의 명제를 검증한다는 점입니다. 특히 보조정리의 인수를 대입한 전제와 결론을 생성해 전칭 양화사 자동 인스턴스화에 기대지 않는 방식은 원문이 구체적으로 설명한 개선입니다. 기존 프로그램 함수 호출과 달리 실행 코드와 borrow checker 부담을 추가하지 않습니다. Lobsters 댓글은 Creusot과 Verus의 차이를 가변 대여 지원, solver 조정, IDE 구조, 문법으로 나눠 설명하지만 이는 댓글 작성자의 비교이며 공식 비교 결과는 아닙니다. 댓글에서도 Verus의 가변 대여 지원이 따라잡고 있다는 전언이 나옵니다. 따라서 이번 릴리스만으로 두 도구의 우열을 판단하기는 어렵고, Creusot이 부분 순서와 증명 편의, 명세 탐색을 개선했다는 범위가 확인됩니다.

AI 요약

Creusot 0.14.0은 Rust 프로그램의 계약을 형식 검증하는 도구의 새 버전입니다. 이번 안내에서는 부분 순서 명세, 스냅샷에서 검증 조건을 생성하는 기능, rust-analyzer 통합을 소개합니다.

부분 순서 명세

이전 Creusot은 PartialOrd 명세를 전체 순서로 제한했습니다. 기존 OrdLogic은 cmp와 대응하는 논리 함수 cmp_log가 Less, Equal, Greater 중 하나를 반환한다고 정의했습니다. 반환형이 Ordering이므로 두 원소를 비교하면 반드시 세 결과 중 하나가 나온다는 전체성 조건이 타입에 포함됐습니다.

0.13.0부터는 부분 순서도 명세할 수 있도록 바뀌었습니다. 새 PartialOrdLogic은 불리언 함수 lt_log로 비교를 표현하며, 비반사성과 추이성을 법칙으로 둡니다. 전체 순서가 필요한 OrdLogic은 별도 법칙으로 x < y, x == y, y < x 가운데 하나가 성립한다고 명시합니다. 개발팀은 기존 증명들이 이 변경에도 영향을 받지 않았고 자동 증명기가 그대로 처리했다고 밝혔습니다.

스냅샷의 검증 조건

Creusot은 이제 Rust 프로그램 안에 넣는 논리 표현식인 snapshot!에서도 검증 조건(VC)을 생성합니다. 이 기능은 증명 도구에서 흔히 쓰는 보조정리 함수(lemma function)를 논리 함수로 작성하도록 합니다. 예를 들어 함수의 전제조건을 hyp(x), 사후조건을 concl(x)로 두면, snapshot!(lemma(n)) 호출을 전제로 hyp(n)이 참인지 확인하고 concl(n)을 가정하는 명제로 바꿉니다. 인수 n을 대입한 명제를 직접 만들기 때문에 자동 증명기가 forall<x> hyp(x) -> concl(x)의 전칭 양화사를 적절히 적용하기를 기다리지 않아도 됩니다.

이전에도 프로그램 함수에 전제조건과 사후조건을 붙여 비슷한 보조정리를 호출할 수 있었습니다. 다만 실제 Rust 함수 호출이 생기고 borrow checker를 통과해야 했습니다. 증명에 필요한 사실만 적으려는 경우에는 이를 우회하는 코드가 필요할 수 있습니다. 스냅샷은 실행 시 제거되므로 프로그램 동작과 증명 내용을 분리해 표현합니다. 개발팀은 스냅샷에서 검증 조건을 생성하는 일이 soundness에 필수는 아니었지만, 범위를 벗어난 인덱싱처럼 명세의 실수를 더 빨리 잡고 새로운 증명 기법을 지원한다고 설명합니다.

rust-analyzer와 Pearlite

이번 버전부터 Pearlite 명세에서 Go to Definition을 사용할 수 있습니다. Creusot의 명세 매크로는 일반 컴파일 과정에서 내용이 지워지므로, rust-analyzer가 Creusot과 같은 방식으로 매크로를 확장하도록 설정해야 합니다. 확장된 코드는 Rust 타입 검사는 통과하지만 borrow checker는 통과하지 않을 수 있습니다. rust-analyzer는 borrow checking을 하지 않아 이 방식으로 탐색 기능을 구현할 수 있었습니다.

처음에는 매크로가 만든 토큰의 소스 위치 정보(span)가 너무 넓어 관련 없는 정의까지 검색됐습니다. 예를 들어 Pearlite의 a + b는 내부적으로 AddLogic::add_logic(a, b) 메서드 호출로 바뀌는데, 생성된 모든 토큰이 a + b 전체 범위를 가리켰습니다. 따라서 표현식 안 어디에 커서를 두어도 네임스페이스와 타입 등 여러 정의가 함께 검색됐습니다. Creusot은 add_logic 토큰의 span을 + 기호 위치로 좁히고 나머지 식별자에는 길이가 0인 span을 주도록 고쳤습니다. 개발팀은 이 수정으로 명세 안에서 정의를 탐색하기 편해졌다고 설명합니다.

Lobsters 반응

@david_chisnall — 목표가 Verus와 비슷해 보입니다. 두 접근법을 비교한 자료가 있나요?
- @lyxia — 종합적인 비교 자료는 모릅니다. 최근 Creusot 논문은 Verus 첫 논문에서 처음 발표된 기능을 사용하므로 기술적인 비교는 들어 있습니다. Creusot의 가장 두드러지는 특징은 가변 대여(mutable borrow)를 일급으로 지원한다는 점입니다. index_mut(&mut [T], usize) -> Option<&mut T>처럼 가변 참조를 반환하는 함수를 직접 명세할 수 있습니다. Verus 같은 다른 도구는 과거에 이런 함수나 가변 참조를 Option 같은 자료구조에 담는 함수를 다루기 어려워했지만, 빠르게 따라잡고 있다고 들었습니다. Creusot은 여러 SMT solver를 지원해 각 solver의 장점을 활용합니다. Verus는 solver에 맞춰 목표를 더 세밀하게 조정할 수 있습니다. Verus는 통합된 구조 덕분에 IDE 기능이 좋고 빠릅니다. Creusot은 맞춤형 Rust 컴파일러와 Why3 증명 백엔드를 함께 쓰는 구조라 두 영역을 모두 잘 연결하려면 작업이 더 필요합니다. 문법도 다릅니다. Creusot은 속성을 붙인 Rust 문법을 쓰고 Verus도 비슷한 방식을 지원하지만, 주로 안내하는 작업 방식은 verus! 매크로 안에 코드를 작성하는 것입니다. 이 차이가 실제 사용에 미치는 영향은 아직 불분명합니다.
- @interlandi — 논문에서 다룬 문제는 상당히 까다롭지만 해결책은 읽기 쉽습니다. 제시된 명세가 무엇을 말하는지 분명합니다. Rust를 아주 깊게 쓰지는 않지만 이 접근법이 흥미롭습니다. Ghost<T>를 수동 PCM 대신 맞춤형 자원 대수(resource algebra)를 만드는 데 쓰는 것으로 이해했는데 맞나요? 제가 틀렸다면 알려주세요.
- @bsdinis — Verus에는 Iris가 제공하는 조합 연산 대부분을 갖춘 자원 대수 구성이 있습니다. 보통 Tracked<T> 안에 들어갑니다. Ghost와 Tracked는 실행 영역과 증명 영역을 연결하는 방식입니다. Ghost와 Tracked 인수를 검증되지 않은 호출부의 함수 시그니처를 바꾸지 않고 함수에 추가하도록 문법을 바꾸는 작업도 진행 중입니다.
- @interlandi — 아직 형식 기법을 실제로 다루지는 않고 관심이 많은 입장이라 질문이 단순할 수 있습니다. CIC에서 부분 함수를 피하려는 목적이 없다면 PCM보다 전체 자원 대수를 쓰는 이점은 무엇인가요? 자동화와 관련이 있을 것 같지만 잘 모르겠습니다.
- @bsdinis — 자원 대수도 부분적입니다. 차이는 항등원 값이 존재한다는 점입니다. PCM에는 항등원이 있지만 자원 대수에는 없습니다. 항등원 값은 때때로 합성에 잘 맞지 않는 것이 주된 문제입니다.

원문: Creusot devlog / 번역·요약: Trawling

원문 보기 ↗토론 보기 ↗