Rust के core और alloc crates का Coq में अनुवाद कर औपचारिक सत्यापन

 (formal.land)
1 पॉइंट द्वारा GN⁺ 2024-05-16 | 1 टिप्पणियां | WhatsApp पर शेयर करें

Rust के core और alloc crates का अनुवाद

प्रारंभिक रन 🐥

  • coq-of-rust का उपयोग करके Rust के alloc और core crates पर प्रारंभिक रन चलाने पर Coq कोड की दो फ़ाइलें बनीं, जिनमें प्रत्येक में कई लाख पंक्तियाँ थीं.
  • इसका मतलब है कि यह टूल बड़े codebase पर भी काम करता है, लेकिन जनरेट किया गया Coq कोड compile नहीं होता. errors बहुत कम आती हैं (हर कुछ हज़ार पंक्तियों में एक बार).

इनपुट Rust कोड का आकार (cloc कमांड के आधार पर)

  • alloc: Rust कोड की 26,299 पंक्तियाँ

  • core: Rust कोड की 54,192 पंक्तियाँ

  • क्योंकि macros को expand करके अनुवाद करना पड़ता है, इसलिए वास्तविक अनुवादित आकार इससे बड़ा है.

जनरेट किए गए कोड का विभाजन 🪓

  • मुख्य बदलाव यह था कि coq-of-rust द्वारा जनरेट किए गए output को हर इनपुट Rust फ़ाइल के लिए एक-एक फ़ाइल में बाँट दिया गया.
  • यह इसलिए संभव है क्योंकि definitions के क्रम से स्वतंत्र होकर अनुवाद किया जा सकता है. Rust फ़ाइलों के बीच circular dependencies Coq में निषिद्ध हैं, फिर भी विभाजन संभव है.

आउटपुट का आकार

  • alloc: 54 Coq फ़ाइलें, Coq कोड की 171,783 पंक्तियाँ
  • core: 190 Coq फ़ाइलें, Coq कोड की 592,065 पंक्तियाँ

कोड विभाजन के लाभ

  • जनरेट किए गए कोड को पढ़ना और खोजना आसान होता है
  • parallel में compile किया जा सकता है, इसलिए compilation आसान होती है
  • एक फ़ाइल पर ध्यान केंद्रित करके debugging करना आसान होता है
  • जो फ़ाइलें compile नहीं होतीं उन्हें नज़रअंदाज़ करना आसान होता है
  • एकल फ़ाइल में हुए बदलावों को track करना आसान होता है, इसलिए maintenance आसान होती है

कुछ bugs को ठीक करना 🐞

  • module names के बीच टकराव के कारण एक bug था. यह impl block के लिए module name चुनते समय होता था.
  • uniqueness बढ़ाने के लिए module name में अधिक जानकारी जोड़ी गई. उदाहरण के लिए, where clause जोड़ा गया.

उदाहरण

  • Default trait के Mapping type implementation:

    #[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.
(* ... *)

compile न होने वाली फ़ाइलों की सूची

  • 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% है. जो फ़ाइलें compile हो जाती हैं उनमें भी ऐसे Rust constructs हो सकते हैं जिन्हें अभी handle नहीं किया गया है.

उदाहरण 🔎

Option type की unwrap_or_default method का मूल कोड

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.

सरल किया गया function कोड

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.
  • यह सरल की गई definition कोड सत्यापन में उपयोग होती है. equivalence proof CoqOfRust/core/proofs/option.v में है.

निष्कर्ष

  • standard library का formalization होने से Rust programs के verification कार्य पर भरोसा किया जा सकता है.

  • अगला लक्ष्य अभी भी जटिल proof process को सरल बनाना है. खास तौर पर, simulation के original Rust code के समकक्ष होने को दिखाने की प्रक्रिया में name resolution, advanced types की शुरुआत, और side effects हटाने जैसे चरणों को अलग करना है.

  • यदि आप Rust projects के formal verification में रुचि रखते हैं, तो contact@formal.land पर संपर्क करें. formal verification किसी दिए गए specification के लिए bugs न होने की गणितीय गारंटी देकर सुरक्षा का सबसे उच्च स्तर प्रदान करता है.

टैग:

  • coq-of-rust
  • Rust
  • Coq
  • अनुवाद
  • core
  • alloc

GN⁺ की राय

  1. Rust और Coq का एकीकरण: Rust और Coq का एकीकरण Rust programs की reliability बढ़ाने में बहुत मददगार है. Rust की safety और Coq के formal verification को मिलाने से, खासकर महत्वपूर्ण applications में, बहुत उपयोगी परिणाम मिलते हैं.
  2. automation का महत्व: coq-of-rust टूल का उपयोग करके किया गया automatic translation manual काम की तुलना में अधिक विश्वसनीय है. लेकिन verification process में फिर भी errors आ सकती हैं, इसलिए सावधानी ज़रूरी है.
  3. जटिल codebase का प्रबंधन: बड़े codebase को संभालने में code विभाजन maintenance और debugging में बहुत मदद करता है. यह खासकर team work में महत्वपूर्ण है.
  4. formal verification की आवश्यकता: formal verification विशेष रूप से finance, healthcare, aviation जैसे महत्वपूर्ण क्षेत्रों में आवश्यक है. Rust और Coq का संयोजन ऐसे क्षेत्रों में बहुत मूल्य दे सकता है.
  5. तकनीक अपनाने के विचार: नई तकनीक अपनाते समय learning curve और मौजूदा systems के साथ compatibility पर विचार करना चाहिए. Coq जैसे formal verification tools की learning curve ऊँची हो सकती है, इसलिए पर्याप्त training और तैयारी की ज़रूरत होती है.

संबंधित पढ़ाई

1 टिप्पणियां

 
GN⁺ 2024-05-16
Hacker News राय

Hacker News टिप्पणियों का सारांश

  • स्वचालित अनुवाद टूल्स की विश्वसनीयता

    • स्वचालित अनुवाद टूल्स ने भरोसा हासिल किया है। coq-of-rust, Rust में लिखा गया है और इसे Coq में बदलकर इसकी correctness सिद्ध की जा सकती है। यह Ken Thompson के हमले को रोकने के तरीके जैसा है।

  • प्रोग्राम के आकार और verification

    • Coq जैसे semi-automatic proof systems से verify किए गए प्रोग्राम आमतौर पर छोटे होते हैं। 100% guarantee की लागत, 99.9999% guarantee की लागत से 10 गुना हो सकती है।

  • अनुवाद प्रक्रिया में त्रुटि की संभावना

    • कोड को Coq में translate करने की प्रक्रिया में त्रुटि होने की संभावना अधिक है। इससे मूल कोड पर verification की वैधता पर संदेह होता है।

  • क्रिप्टोकरेंसी से संबंधित पोस्ट

    • किसी ने क्रिप्टोकरेंसी से कम संबंधित एक ब्लॉग पोस्ट submit की। Python पर इसी तरह के approach वाली एक पोस्ट भी है।

  • formal verification की सीमाएँ

    • किसी को एक formally verified C compiler में bug मिलने का मामला याद है। इससे Coq खुद और translation की विश्वसनीयता पर सवाल उठते हैं।

  • Rust का formal verification

    • सवाल उठाया गया कि अगर Rust की standard library formally verified हो जाए, तो क्या unsafe code का उपयोग न करने पर memory handling के लिए formal verification जैसी quality मिल सकती है।

  • formal verification specifications लिखना

    • पूछा गया कि formal verification specifications लिखना क्या अधिक जटिल property tests लिखने जैसा है। property tests लिखना कठिन और समय लेने वाला होता है।

  • दूसरे approaches के साथ तुलना

    • Aeneas या RustHornBelt की तुलना में इस approach का अंतर समझाने का अनुरोध किया गया। खासकर यह जानने की जिज्ञासा थी कि pointers और mutable borrowing को कैसे संभाला जाता है।

  • Rust को kernel में अपनाना

    • यह भी पूछा गया कि क्या ऐसे प्रयास kernel में Rust को अपनाने की रफ्तार बढ़ा सकते हैं।

  • F में Rust backend जोड़ना*

    • यह जानने की जिज्ञासा थी कि F* में Rust backend जोड़ने के लिए कितना काम करना पड़ेगा।