▲

GN⁺: Rust의 core 및 alloc 크레이트를 Coq로 번역하여 형식 검증

 (formal.land)
1P by neo 2달전 | favorite | 댓글 1개

Rust의 core 및 alloc 크레이트 번역

초기 실행 🐥

  • coq-of-rust를 사용하여 Rust의 alloc 및 core 크레이트를 초기 실행한 결과, 몇십만 줄의 Coq 코드 파일 두 개가 생성됨.
  • 이는 도구가 큰 코드베이스에서도 작동함을 의미하지만, 생성된 Coq 코드는 컴파일되지 않음. 오류는 드물게 발생함 (몇천 줄마다 한 번).

입력 Rust 코드의 크기 (cloc 명령어 기준)

  • alloc: 26,299 줄의 Rust 코드

  • core: 54,192 줄의 Rust 코드

  • 매크로를 확장하여 번역해야 하므로 실제 번역해야 할 크기는 더 큼.

생성된 코드 분할 🪓

  • 주요 변경 사항은 coq-of-rust가 생성한 출력을 각 입력 Rust 파일마다 하나의 파일로 분할한 것임.
  • 이는 정의 순서와 무관하게 번역이 가능하기 때문에 가능함. Rust 파일 간의 순환 종속성이 Coq에서는 금지되지만, 여전히 분할할 수 있음.

출력 크기

  • alloc: 54개의 Coq 파일, 171,783 줄의 Coq 코드
  • core: 190개의 Coq 파일, 592,065 줄의 Coq 코드

코드 분할의 장점

  • 생성된 코드를 읽고 탐색하기 쉬움
  • 병렬로 컴파일할 수 있어 컴파일이 쉬움
  • 한 파일에 집중하여 디버깅하기 쉬움
  • 컴파일되지 않는 파일을 무시하기 쉬움
  • 단일 파일의 변경 사항을 추적하기 쉬워 유지보수가 쉬움

일부 버그 수정 🐞

  • 모듈 이름 간의 충돌로 인한 버그가 있었음. 이는 impl 블록의 모듈 이름을 선택할 때 발생함.
  • 모듈 이름에 더 많은 정보를 추가하여 고유성을 높임. 예를 들어, where 절을 추가함.

예시

  • Default 트레이트의 Mapping 타입 구현:

    #[derive(Default)]
struct Mapping<K, V> {
  // ...
}

  • 이전 Coq 코드:

    Module Impl_core_default_Default_for_dns_Mapping_K_V.
(* ...trait implementation ... *)
End Impl_core_default_Default_for_dns_Mapping_K_V.

  • 수정된 Coq 코드:

    Module Impl_core_default_Default_where_core_default_Default_K_where_core_default_Default_V_for_dns_Mapping_K_V.
(* ... *)

컴파일되지 않는 파일 목록

  • alloc/boxed.v

  • core/any.v

  • core/array/mod.v

  • core/cmp/bytewise.v

  • core/error.v

  • core/escape.v

  • core/iter/adapters/flatten.v

  • core/net/ip_addr.v

  • 이는 전체 파일의 4%를 차지함. 컴파일되는 파일에도 처리되지 않은 Rust 구조가 존재할 수 있음.

예시 🔎

Option 타입의 unwrap_or_default 메서드 원본 코드

pub fn unwrap_or_default(self) -> T
where
  T: Default,
{
  match self {
    Some(x) => x,
    None => T::default(),
  }
}

번역된 Coq 코드

Definition unwrap_or_default (T : Ty.t) (τ : list Ty.t) (α : list Value.t) : M :=
  let Self : Ty.t := Self T in
  match τ, α with
  | [], [ self ] =>
    ltac:(M.monadic
      (let self := M.alloc (| self |) in
      M.read (|
        M.match_operator (|
          self,
          [
            fun γ =>
              ltac:(M.monadic
                (let γ0_0 :=
                  M.get_struct_tuple_field_or_break_match (|
                    γ,
                    "core::option::Option::Some",
                    0
                  |) in
                let x := M.copy (| γ0_0 |) in
                x));
            fun γ =>
              ltac:(M.monadic
                (M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                    []
                  |)
                |)))
          ]
        |)
      |)))
  | _, _ => M.impossible
  end.

단순화된 함수 코드

Definition unwrap_or_default {T : Set}
  {_ : core.simulations.default.Default.Trait T}
  (self : Self T) :
  T :=
  match self with
  | None => core.simulations.default.Default.default (Self := T)
  | Some x => x
  end.
  • 이 단순화된 정의는 코드 검증 시 사용됨. 동등성 증명은 CoqOfRust/core/proofs/option.v에 있음.

결론

  • 표준 라이브러리의 형식화를 통해 Rust 프로그램 검증 작업을 신뢰할 수 있게 됨.

  • 다음 목표는 여전히 번거로운 증명 과정을 단순화하는 것임. 특히, 시뮬레이션이 원본 Rust 코드와 동등함을 보여주는 과정에서 이름 해석, 고급 타입 도입, 부작용 제거 등의 단계를 분리하고자 함.

  • Rust 프로젝트의 형식 검증에 관심이 있다면 contact@formal.land로 연락 바람. 형식 검증은 주어진 명세에 대해 버그가 없음을 수학적으로 보장하는 가장 높은 수준의 안전성을 제공함.

태그:

  • coq-of-rust
  • Rust
  • Coq
  • 번역
  • core
  • alloc

GN⁺의 의견

  1. Rust와 Coq의 통합: Rust와 Coq의 통합은 Rust 프로그램의 안정성을 높이는 데 큰 도움이 됨. Rust의 안전성과 Coq의 형식 검증을 결합하면, 특히 중요한 애플리케이션에서 매우 유용함.
  2. 자동화의 중요성: coq-of-rust 도구를 사용한 자동 번역은 수작업보다 신뢰성이 높음. 하지만 여전히 검증 과정에서 오류가 발생할 수 있으므로 주의가 필요함.
  3. 복잡한 코드베이스 관리: 큰 코드베이스를 다루는 데 있어 코드 분할은 유지보수와 디버깅에 큰 도움이 됨. 이는 특히 팀 작업에서 중요한 요소임.
  4. 형식 검증의 필요성: 형식 검증은 특히 금융, 의료, 항공 등 중요한 분야에서 필수적임. Rust와 Coq의 결합은 이러한 분야에서 큰 가치를 제공할 수 있음.
  5. 기술 도입 고려사항: 새로운 기술을 도입할 때는 학습 곡선과 기존 시스템과의 호환성을 고려해야 함. Coq와 같은 형식 검증 도구는 높은 학습 곡선을 가질 수 있으므로 충분한 교육과 준비가 필요함.
▲
neo 2달전  [-]
Hacker News 의견

해커뉴스 댓글 모음 요약

  • 자동 번역 도구의 신뢰성

    • 자동 번역 도구가 신뢰를 얻음. coq-of-rust는 Rust로 작성되었고, Coq로 변환하여 올바름을 증명할 수 있음. 이는 Ken Thompson의 공격을 방지하는 방법과 유사함.

  • 프로그램 크기와 검증

    • Coq 같은 반자동 증명 시스템으로 검증된 프로그램 크기는 작음. 100% 보증 비용이 99.9999% 보증 비용의 10배가 될 수 있음.

  • 번역 과정의 오류 가능성

    • 코드의 Coq 번역 과정에서 오류가 발생할 가능성이 높음. 원본 코드에 대한 검증의 유효성을 의심함.

  • 암호화폐 관련 게시물

    • 암호화폐 관련 내용이 적은 블로그 게시물을 제출함. Python에 대한 유사한 접근법을 다룬 게시물도 있음.

  • 형식 검증의 한계

    • 형식 검증된 C 컴파일러에서 버그를 발견한 사례를 기억함. Coq 자체와 번역에 대한 신뢰성 문제를 제기함.

  • Rust의 형식 검증

    • Rust의 기본 라이브러리가 형식 검증되면, 안전하지 않은 코드를 사용하지 않는 한 메모리 처리에 대한 형식 검증 품질을 얻을 수 있는지 궁금해함.

  • 형식 검증 사양 작성

    • 형식 검증 사양 작성이 더 복잡한 속성 테스트 작성과 유사한지 궁금해함. 속성 테스트 작성이 어렵고 시간이 많이 걸림.

  • 다른 접근법과의 비교

    • Aeneas나 RustHornBelt와의 접근법 차이를 비교해달라는 요청. 포인터와 가변 대여를 어떻게 처리하는지 궁금해함.

  • Rust의 커널 채택

    • 이러한 노력이 Rust의 커널 채택을 가속화할 수 있을지 궁금해함.

  • F*의 Rust 백엔드 추가

    • F*에 Rust 백엔드를 추가하는 데 얼마나 많은 작업이 필요한지 궁금해함.
답변달기