Dịch các crate core và alloc của Rust sang Coq
Chạy thử ban đầu 🐥
- Kết quả chạy thử ban đầu trên các crate
allocvàcorecủa Rust bằngcoq-of-rustđã tạo ra hai tệp mã Coq dài tới hàng trăm nghìn dòng. - Điều này cho thấy công cụ vẫn hoạt động với các codebase lớn, nhưng mã Coq được sinh ra không biên dịch được. Lỗi xuất hiện khá hiếm (khoảng một lần mỗi vài nghìn dòng).
Kích thước mã Rust đầu vào (theo lệnh cloc)
-
alloc: 26.299 dòng mã Rust -
core: 54.192 dòng mã Rust -
Do cần mở rộng macro trước khi dịch, quy mô thực tế cần dịch còn lớn hơn.
Chia nhỏ mã được sinh ra 🪓
- Thay đổi chính là đầu ra do
coq-of-rusttạo ra đã được tách thành một tệp cho mỗi tệp Rust đầu vào. - Điều này khả thi vì có thể dịch mà không phụ thuộc vào thứ tự định nghĩa. Dù phụ thuộc vòng giữa các tệp Rust bị cấm trong Coq, việc chia nhỏ vẫn thực hiện được.
Kích thước đầu ra
alloc: 54 tệp Coq, 171.783 dòng mã Coqcore: 190 tệp Coq, 592.065 dòng mã Coq
Lợi ích của việc chia nhỏ mã
- Dễ đọc và điều hướng mã được sinh ra hơn
- Dễ biên dịch hơn vì có thể biên dịch song song
- Dễ gỡ lỗi hơn khi chỉ cần tập trung vào một tệp
- Dễ bỏ qua các tệp không biên dịch được
- Dễ theo dõi thay đổi của từng tệp riêng lẻ nên việc bảo trì thuận tiện hơn
Sửa một số lỗi 🐞
- Có một lỗi do xung đột giữa các tên mô-đun. Lỗi này phát sinh khi chọn tên mô-đun cho các khối
impl. - Đã thêm nhiều thông tin hơn vào tên mô-đun để tăng tính duy nhất. Ví dụ, thêm mệnh đề
where.
Ví dụ
-
Cài đặt kiểu
Mappingcho traitDefault:#[derive(Default)] struct Mapping<K, V> { // ... } -
Mã Coq trước đây:
Module Impl_core_default_Default_for_dns_Mapping_K_V. (* ...trait implementation ... *) End Impl_core_default_Default_for_dns_Mapping_K_V. -
Mã Coq sau khi sửa:
Module Impl_core_default_Default_where_core_default_Default_K_where_core_default_Default_V_for_dns_Mapping_K_V. (* ... *)
Danh sách các tệp không biên dịch được
-
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 -
Chúng chiếm 4% tổng số tệp. Ngay cả trong các tệp biên dịch được vẫn có thể tồn tại những cấu trúc Rust chưa được xử lý.
Ví dụ 🔎
Mã gốc của phương thức unwrap_or_default của kiểu Option
pub fn unwrap_or_default(self) -> T
where
T: Default,
{
match self {
Some(x) => x,
None => T::default(),
}
}
Mã Coq được dịch
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.
Mã hàm đã được đơn giản hóa
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.
- Định nghĩa đã được đơn giản hóa này được dùng khi kiểm chứng mã. Chứng minh tính tương đương nằm trong
CoqOfRust/core/proofs/option.v.
Kết luận
-
Việc hình thức hóa thư viện chuẩn giúp công việc kiểm chứng chương trình Rust trở nên đáng tin cậy.
-
Mục tiêu tiếp theo là đơn giản hóa quy trình chứng minh vốn vẫn còn rườm rà. Cụ thể, muốn tách riêng các bước như phân giải tên, đưa vào các kiểu nâng cao và loại bỏ tác dụng phụ khi chứng minh rằng mô phỏng tương đương với mã Rust gốc.
-
Nếu bạn quan tâm đến kiểm chứng hình thức cho các dự án Rust, hãy liên hệ qua contact@formal.land. Kiểm chứng hình thức mang lại mức độ an toàn cao nhất bằng cách bảo đảm về mặt toán học rằng không có lỗi so với đặc tả đã cho.
Thẻ:
- coq-of-rust
- Rust
- Coq
- dịch
- core
- alloc
Ý kiến của GN⁺
- Tích hợp Rust và Coq: Việc tích hợp Rust và Coq rất hữu ích để nâng cao độ ổn định của các chương trình Rust. Kết hợp tính an toàn của Rust với kiểm chứng hình thức của Coq đặc biệt hữu dụng trong các ứng dụng quan trọng.
- Tầm quan trọng của tự động hóa: Dịch tự động bằng công cụ
coq-of-rustđáng tin cậy hơn làm thủ công. Tuy vậy, vẫn cần thận trọng vì lỗi vẫn có thể xảy ra trong quá trình kiểm chứng. - Quản lý codebase phức tạp: Khi xử lý các codebase lớn, việc chia nhỏ mã rất hữu ích cho bảo trì và gỡ lỗi. Đây là yếu tố đặc biệt quan trọng trong làm việc nhóm.
- Sự cần thiết của kiểm chứng hình thức: Kiểm chứng hình thức là thiết yếu trong các lĩnh vực quan trọng như tài chính, y tế và hàng không. Sự kết hợp giữa Rust và Coq có thể mang lại giá trị lớn trong các lĩnh vực này.
- Các điểm cần cân nhắc khi áp dụng công nghệ: Khi đưa công nghệ mới vào sử dụng, cần cân nhắc đường cong học tập và khả năng tương thích với hệ thống hiện có. Các công cụ kiểm chứng hình thức như Coq có thể có đường cong học tập cao, nên cần đào tạo và chuẩn bị đầy đủ.
1 bình luận
Ý kiến trên Hacker News
Tóm tắt các bình luận trên Hacker News
Độ tin cậy của công cụ dịch tự động
Quy mô chương trình và kiểm chứng
Khả năng phát sinh lỗi trong quá trình dịch
Các bài đăng liên quan đến tiền mã hóa
Giới hạn của kiểm chứng hình thức
Kiểm chứng hình thức cho Rust
unsafehay không.Viết đặc tả cho kiểm chứng hình thức
So sánh với các cách tiếp cận khác
Rust được chấp nhận trong kernel
Thêm backend Rust cho F*