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

> Clean Markdown view of GeekNews topic #14837. Use the original source for factual precision when an external source URL is present.

## Metadata

- GeekNews HTML: [https://news.hada.io/topic?id=14837](https://news.hada.io/topic?id=14837)
- GeekNews Markdown: [https://news.hada.io/topic/14837.md](https://news.hada.io/topic/14837.md)
- Type: GN+
- Author: [neo](https://news.hada.io/@neo)
- Published: 2024-05-16T09:53:04+09:00
- Updated: 2024-05-16T09:53:04+09:00
- Original source: [formal.land](https://formal.land/blog/2024/04/26/translation-core-alloc-crates)
- Points: 1
- Comments: 1

## Topic Body

### 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` 타입 구현:
  ```rust
  #[derive(Default)]
  struct Mapping<K, V> {
    // ...
  }
  ```

- 이전 Coq 코드:
  ```coq
  Module Impl_core_default_Default_for_dns_Mapping_K_V.
  (* ...trait implementation ... *)
  End Impl_core_default_Default_for_dns_Mapping_K_V.
  ```

- 수정된 Coq 코드:
  ```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` 메서드 원본 코드

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

##### 번역된 Coq 코드

```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.
```

##### 단순화된 함수 코드

```coq
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와 같은 형식 검증 도구는 높은 학습 곡선을 가질 수 있으므로 충분한 교육과 준비가 필요함.

## Comments



### Comment 25275

- Author: neo
- Created: 2024-05-16T09:53:04+09:00
- Points: 1

###### [Hacker News 의견](https://news.ycombinator.com/item?id=40363744) 
##### 해커뉴스 댓글 모음 요약

* **자동 번역 도구의 신뢰성**
  - 자동 번역 도구가 신뢰를 얻음. 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 백엔드를 추가하는 데 얼마나 많은 작업이 필요한지 궁금해함.