Rust'un `core` ve `alloc` crate'lerini Coq'ya çevirerek biçimsel doğrulama

Rust'un core ve alloc crate'lerinin çevirisi

İlk çalıştırma 🐥

• Rust'un alloc ve core crate'leri coq-of-rust kullanılarak ilk kez çalıştırıldığında, yüz binlerce satırlık iki Coq kod dosyası üretildi.
• Bu, aracın büyük kod tabanlarında da çalıştığını gösteriyor; ancak üretilen Coq kodu derlenmiyor. Hatalar seyrek görülüyor (birkaç bin satırda bir kez).

Girdi Rust kodunun boyutu (cloc komutuna göre)

• alloc: 26.299 satır Rust kodu

• core: 54.192 satır Rust kodu

• Makrolar genişletilerek çevrilmek zorunda olduğundan, fiilen çevrilmesi gereken boyut daha büyük.

Üretilen kodun bölünmesi 🪓

• Ana değişiklik, coq-of-rust tarafından üretilen çıktının her bir girdi Rust dosyası için bir dosya olacak şekilde bölünmesi oldu.
• Bu, tanım sırasından bağımsız olarak çeviri yapılabildiği için mümkün. Rust dosyaları arasındaki döngüsel bağımlılıklar Coq'da yasak olsa da, yine de bölme yapılabiliyor.

Çıktı boyutu

• alloc: 54 Coq dosyası, 171.783 satır Coq kodu
• core: 190 Coq dosyası, 592.065 satır Coq kodu

Kod bölmenin avantajları

• Üretilen kodu okumak ve içinde gezinmek daha kolay
• Paralel derleme yapılabildiği için derlemek daha kolay
• Tek bir dosyaya odaklanarak hata ayıklamak daha kolay
• Derlenmeyen dosyaları yok saymak daha kolay
• Tekil dosyalardaki değişiklikleri izlemek daha kolay olduğundan bakım daha kolay

Bazı hataların düzeltilmesi 🐞

• Modül adları arasındaki çakışmadan kaynaklanan bir hata vardı. Bu, impl blokları için modül adı seçilirken oluşuyordu.
• Benzersizliği artırmak için modül adına daha fazla bilgi eklendi. Örneğin, where koşulu eklendi.

Örnek

• Default trait'i için Mapping türü implementasyonu:

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

• Önceki Coq kodu:

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

• Düzeltilmiş Coq kodu:

  Module Impl_core_default_Default_where_core_default_Default_K_where_core_default_Default_V_for_dns_Mapping_K_V.
  (* ... *)
  

Derlenmeyen dosyaların listesi

• 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

• Bu, toplam dosyaların %4'üne karşılık geliyor. Derlenen dosyalarda da işlenmemiş Rust yapıları bulunabilir.

Örnek 🔎

Option türünün unwrap_or_default metodunun kaynak kodu

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

Çevrilen Coq kodu

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.

Basitleştirilmiş fonksiyon kodu

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.

• Bu basitleştirilmiş tanım, kod doğrulamasında kullanılıyor. Eşdeğerlik ispatı CoqOfRust/core/proofs/option.v içinde yer alıyor.

Sonuç

• Standart kütüphanenin biçimselleştirilmesi sayesinde Rust programı doğrulama çalışmasına güven duyulabiliyor.

• Bir sonraki hedef, hâlâ zahmetli olan ispat sürecini basitleştirmek. Özellikle simülasyonun özgün Rust koduyla eşdeğer olduğunu gösterirken ad çözümleme, gelişmiş türlerin tanıtılması ve yan etkilerin kaldırılması gibi adımları ayırmak isteniyor.

• Rust projelerinin biçimsel doğrulamasıyla ilgileniyorsanız [e-mail] adresine ulaşabilirsiniz. Biçimsel doğrulama, verilen bir belirtime göre hatasızlığı matematiksel olarak garanti eden en yüksek güvenlik düzeyini sunar.

Etiketler:

• coq-of-rust
• Rust
• Coq
• çeviri
• core
• alloc

GN⁺ görüşü

1. Rust ve Coq entegrasyonu: Rust ile Coq'nun entegre edilmesi, Rust programlarının güvenilirliğini artırmada büyük fayda sağlar. Rust'un güvenliği ile Coq'nun biçimsel doğrulamasının birleşimi, özellikle kritik uygulamalarda çok yararlıdır.
2. Otomasyonun önemi: coq-of-rust aracıyla yapılan otomatik çeviri, elle yapılan çalışmalara göre daha güvenilirdir. Ancak doğrulama sürecinde yine de hatalar oluşabileceği için dikkat gerekir.
3. Karmaşık kod tabanlarının yönetimi: Büyük kod tabanlarıyla çalışırken kodu bölmek, bakım ve hata ayıklama açısından büyük fayda sağlar. Bu, özellikle ekip çalışmalarında önemli bir unsurdur.
4. Biçimsel doğrulamanın gerekliliği: Biçimsel doğrulama özellikle finans, sağlık ve havacılık gibi kritik alanlarda zorunludur. Rust ile Coq'nun birleşimi bu alanlarda büyük değer sağlayabilir.
5. Teknoloji benimserken dikkat edilmesi gerekenler: Yeni bir teknolojiyi benimserken öğrenme eğrisi ve mevcut sistemlerle uyumluluk dikkate alınmalıdır. Coq gibi biçimsel doğrulama araçları yüksek bir öğrenme eğrisine sahip olabileceğinden yeterli eğitim ve hazırlık gerekir.

[GN⁺]

Hacker News görüşü

Hacker News yorumlarından derlenmiş özet

• Otomatik çeviri araçlarının güvenilirliği

  • Otomatik çeviri araçları güven kazanmaya başlıyor. coq-of-rust, Rust ile yazılmış kodu Coq'a dönüştürüp doğruluğunu kanıtlayabiliyor. Bu, Ken Thompson saldırısını önleme yöntemine benziyor.

• Program boyutu ve doğrulama

  • Coq gibi yarı otomatik ispat sistemleriyle doğrulanan programların boyutu küçük oluyor. %100 garanti maliyeti, %99.9999 garanti maliyetinin 10 katı olabilir.

• Çeviri sürecindeki hata olasılığı

  • Kodun Coq'a çevrilmesi sürecinde hata çıkma ihtimalinin yüksek olduğu düşünülüyor. Bu da özgün kod üzerindeki doğrulamanın geçerliliğini sorgulatıyor.

• Kripto para ile ilgili gönderiler

  • Kripto para içeriği az olan bir blog yazısı paylaşılmış. Python için benzer bir yaklaşımı ele alan bir yazı da var.

• Biçimsel doğrulamanın sınırları

  • Biçimsel olarak doğrulanmış bir C derleyicisinde hata bulunduğu bir örnek hatırlatılıyor. Bu da Coq'un kendisine ve çeviri sürecine duyulan güveni sorgulatıyor.

• Rust'un biçimsel doğrulaması

  • Rust'un temel kütüphanesi biçimsel olarak doğrulanırsa, unsafe kod kullanılmadığı sürece bellek işlemleri için de biçimsel doğrulama düzeyinde güvence sağlanıp sağlanamayacağı merak ediliyor.

• Biçimsel doğrulama spesifikasyonları yazma

  • Biçimsel doğrulama spesifikasyonları yazmanın, daha karmaşık özellik testleri yazmaya benzer olup olmadığı soruluyor. Özellik testleri yazmak zor ve zaman alıcı bulunuyor.

• Diğer yaklaşımlarla karşılaştırma

  • Aeneas veya RustHornBelt ile yaklaşım farklarının karşılaştırılması isteniyor. Özellikle pointer'ların ve mutable borrow'ların nasıl ele alındığı merak ediliyor.

• Rust'un çekirdekte benimsenmesi

  • Bu tür çabaların, Rust'un çekirdek geliştirmede benimsenmesini hızlandırıp hızlandırmayacağı sorgulanıyor.

• F için Rust backend eklenmesi*

  • F*'a Rust backend eklemek için ne kadar çalışma gerektiği merak ediliyor.